[Haskell-cafe] Limitations of generalization of type constructors

[Tom Ellis]

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!