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!