Opened 16 months ago

Last modified 12 months ago

#7503 new bug

Bug with PolyKinds, type synonyms & GADTs

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

Description

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 (2)

comment:1 Changed 16 months ago by simonpj

  • Difficulty set to 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

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

comment:2 Changed 12 months ago by igloo

  • Milestone set to 7.8.1
  • Owner set to simonpj
Note: See TracTickets for help on using tickets.