Opened 4 years ago

Last modified 16 months ago

#7503 new bug

Bug with PolyKinds, type synonyms & GADTs

Reported by: Ashley Yakeley Owned by: simonpj
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.6.1
Keywords: GADTs Cc:
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:


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.

Change History (7)

comment:1 Changed 4 years ago by simonpj

difficulty: Unknown

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

    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.


comment:2 Changed 4 years ago by igloo

Milestone: 7.8.1
Owner: set to simonpj

comment:3 Changed 3 years ago by thoughtpolice


Moving to 7.10.1

comment:4 Changed 2 years ago by thoughtpolice


Moving to 7.12.1 milestone; if you feel this is an error and should be addressed sooner, please move it back to the 7.10.1 milestone.

comment:5 Changed 21 months ago by thoughtpolice


Milestone renamed

comment:6 Changed 16 months ago by thomie

Keywords: GADTs added

comment:7 Changed 16 months ago by thomie

Milestone: 8.0.1
Note: See TracTickets for help on using tickets.