Haskell PolyKinds extension and type families-CodePudding

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.

CodePudding user response：

I recommend you use StandaloneKindSignatures:

..
{-# Language StandaloneKindSignatures #-}

type Id :: k -> k
type Id a = a

type Proxy :: k -> Type
data Proxy a = Proxy

type
  PK :: k -> Type
type family
  PK a where
  PK Int = Char

The kind argument is invisible but you can write it explicitly in the type family PK @Type Int = Char (requires TypeApplications).

With GADTs you can write Proxy

type Proxy :: k -> Type
data Proxy a where
  Proxy :: Proxy @k a

There are proposals to allow visible (kind) applications in the declaration heads:

type Id :: k -> k
type Id @k a = a

type Proxy :: k -> Type
data Proxy @k a = Proxy

type
  PK :: k -> Type
type family
  PK @k    a where
  PK @Type Int = Char

And we can use "visible dependent quantification" in kinds with forall-> instead of (implicit) invisible forall.


type Id :: forall k -> k -> k
type Id k a = a

type Proxy :: forall k -> k -> Type
data Proxy k a = Proxy

type
  PK :: forall k -> k -> Type
type family
  PK k    a where
  PK Type Int = Char

CodePudding user response：

You were one language extension away. If you enable the CUSKs extension too, then what you wrote will do what you want.