I working on type families in Haskell to get deeper inside this topic, and trying to use polymorphic kinds and type families at the same time.
For example, the beginning of the file has the following language extensions (there is more in the file later than will be shown here):
{-# LANGUAGE TypeFamilies,
StandaloneKindSignatures,
RankNTypes,
PolyKinds,
DataKinds,
TypeOperators,
TypeApplications,
KindSignatures,
ScopedTypeVariables,
UndecidableInstances,
MultiParamTypeClasses,
AllowAmbiguousTypes #-}
Then I'm using polymorphic kinds in type declaration:
data Proxy (a :: k) = Proxy
which works well. But at the time I'm trying to use them inside type families with richer definition:
type family PK (a :: k) :: Type where
PK Int = Char
GHC throws an error:
• Expected kind ‘k’, but ‘Int’ has kind ‘*’
• In the first argument of ‘PK’, namely ‘Int’
In the type family declaration for ‘PK’.
Is there a fix for that? The GHC version is 8.10.7. Thanks for any idea and help in advance.
I recommend you use
StandaloneKindSignatures
:The kind argument is invisible but you can write it explicitly in the type family
PK @Type Int = Char
(requiresTypeApplications
).With GADTs you can write
Proxy
There are proposals to allow visible (kind) applications in the declaration heads:
And we can use "visible dependent quantification" in kinds with
forall->
instead of (implicit) invisibleforall.
Difference between
Proxy
, defined as a uniform datatype (non-GADT or tongue-in-cheek: 'legacy' syntax) or a GADT. They are equivalent (tested on an old GHC 8.10) apart from k beingforall.
) specified = can be specified withTypeApplications
, but is automatically inferred if not specifiedforall{}.
) inferred =TypeApplications
skips it, cannot be specified directlyThis applies both to the type constructor
Proxy
and the data constructor namedP
for disambiguation since both are polymorphic.Proxy
can be specifiedProxy @Nat 42
or inferredProxy 42
depending on the quantification ofk
:And depending on the quantification in
P
, k can be specifiedP @Nat @42
or inferredP @42
:This gives several outcomes
P @42 :: Proxy 42
(P @42 :: Proxy 42
)Proxy
but inferred inP
(P @42 :: Proxy @Nat 42
)Proxy
andP
(P @Nat @42 :: Proxy @Nat 42
)I am waiting for the dust to settle on many of the new and coming changes to quantification and scoping, this may already be out of date.