Hello Cafe, Generalization of types in type constructors behaves strangely compared to the same behaviour at the term level. I was wondering whether this is expected, whether it's a known issue that's due to be resolved, or is a known issue that can't be resolved for some technical reason. This mail is a literate Haskell file.

{-# LANGUAGE DataKinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-}

{-# OPTIONS_GHC -Wall #-} {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}

import Prelude hiding (const) import Data.Kind (Type)

`f` takes an argument of polymorphic type

f :: (forall (z :: Type). Maybe z -> Int) -> Int f k = k (Just True)

`c1` is an argument that will fit there. Its type matches exactly.

c1 :: forall (z :: Type). Maybe z -> Int c1 _ = 0

fc1 :: Int fc1 = f c1

`c2` will fit there but its type doesn't match exactly. `z` will have to be substituted with `Maybe z`, obtaining the type forall (z :: Type). Maybe z -> Int which does fit exactly.

c2 :: forall (z :: Type). z -> Int c2 _ = 0

fc2 :: Int fc2 = f c2

`const` will fit there, once `z` is substituted with `Maybe z`, the `Int` argument applied and the quantifer moved, obtaining the type forall (z :: Type). Maybe z -> Int which does fit exactly.

const :: forall (z :: Type). Int -> z -> Int const x _ = x

fc3 :: Int fc3 = f (const 0)

The story for type constructors is not so pleasant. I can define an analogue of `f` on the type level:

type F :: (forall (z :: Type). Maybe z -> Type) -> Type newtype F k = F (k (Just Bool))

and the analogue of `c1` fits exactly:

type C1 :: forall (z :: Type). Maybe z -> Type data C1 m = C1

type FC1 :: Type type FC1 = F C1

but the analogue of `c2` does not:

type C2 :: forall (z :: Type). z -> Type data C2 m = C2

-- Occurs check: cannot construct the infinite kind: z ~ Maybe z -- type FC2 :: Type -- type FC2 = F C2

nor does the analogue of `const`:

type Const :: forall (z :: Type). Type -> Maybe z -> Type newtype Const z a = Const z

-- • Expected kind ‘forall z. Maybe z -> *’, -- but ‘Const ()’ has kind ‘Maybe a0 -> *’ -- type FC3 :: Type -- type FC3 = F (Const ())

To get the analogue of `const` we have to be much more specific:

type OtherConst :: Type -> forall (z :: Type). Maybe z -> Type newtype OtherConst z b = OtherConst z

type FC4 :: Type type FC4 = F (OtherConst ())

This is rather unfortunate because it limits generic programming at the type level!