Bug with PolyKinds, type synonyms & GADTs

[Ashley Yakeley]

GHC incorrectly rejects this program:

{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #-}
module TestConstraintKinds where
    import GHC.Exts hiding (Any)

    data WrappedType = forall a. WrapType a

    data A :: WrappedType -> * where
        MkA :: forall (a :: *). AW a -> A (WrapType a)

    type AW  (a :: k) = A (WrapType a)
    type AW' (a :: k) = A (WrapType a)

    class C (a :: k) where
        aw :: AW a -- workaround: AW'

    instance C [] where
        aw = aw

GHC accepts the program when AW is replaced with AW' on that line.

[simonpj]

Hmm. As stated, it fails both with AW and AW' in the commented line. But this simpler one fails:

data Wrap a --  Wrap :: forall k. k -> *

data A a = MkA a (AW a)

type AW  a = A (Wrap a)
type AW2 a = A (Wrap a)

class C (a :: k) where
    aw :: AW a -- workaround: AW2

With AW in the last line we get

T7503.hs:15:14:
    The first argument of `AW' should have kind `*',
      but `a' has kind `k1'
    In the type `AW a'
    In the class declaration for `C'

Replacing with the identical (!) AW2 makes it go through. Here is what is happening:

• Type synonym AW and data type A are mutually recursive.
• So they are kind-checked together, with AW being monomorphic.
• AW is applied to a::* in the data type declaration of A, so AW ends up with kind *->*.
• But that is insufficiently polymorphic for its use in the class declaration.
• On the other hand AW2 is not mutually recursive with A, so it is kind-checked after A is done, and gets the polymorphic kind AW2 :: forall k. k -> *.

Very similar things happen in the world of terms. We solve them by breaking the mutual recursion at a type signature, and in principle we could do the same here. After all, A is given a full kind signature.

Still, it's not entirely trivial to implement. And we don't have a general mechanism for giving kind signatures; for example, how would you give a kind signature for a type synonym?

Worth thinking about. But perhpas not urgent. Yell if it is hurting you.

Simon