Opened 6 years ago

Last modified 9 days 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, TypeInType Cc:
Operating System: Linux Architecture: x86_64 (amd64)
Type of failure: GHC rejects valid program Test Case: typecheck/should_compile/T7503a
Blocked By: Blocking:
Related Tickets: #14451, #12088 Differential Rev(s):
Wiki Page: https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference

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

comment:1 Changed 6 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

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 6 years ago by igloo

Milestone: 7.8.1
Owner: set to simonpj

comment:3 Changed 5 years ago by thoughtpolice

Milestone: 7.8.37.10.1

Moving to 7.10.1

comment:4 Changed 4 years ago by thoughtpolice

Milestone: 7.10.17.12.1

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 3 years ago by thoughtpolice

Milestone: 7.12.18.0.1

Milestone renamed

comment:6 Changed 3 years ago by thomie

Keywords: GADTs added

comment:7 Changed 3 years ago by thomie

Milestone: 8.0.1

comment:8 Changed 10 months ago by simonpj

Keywords: TypeInType added

Adding this to TypeInType because it's really the same as #14451 which is so labelled.

comment:9 Changed 10 months ago by kcsongor

Wiki Page: https://ghc.haskell.org/trac/ghc/wiki/GhcKinds/KindInference

comment:10 Changed 13 days ago by RyanGlScott

Continuing my journey started in https://ghc.haskell.org/trac/ghc/ticket/14451#comment:7, it appears that something changed between GHC 8.4 and 8.6 that affects the programs in this ticket. Amazingly, the original 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

Now typechecks with GHC 8.6.2 and HEAD!

Unfortunately, it might be too early to declare victory here, since the program in comment:1:

{-# LANGUAGE ExistentialQuantification, DataKinds, PolyKinds, KindSignatures, GADTs #-}
module TestConstraintKinds where

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

Still refuses to typecheck, even on GHC 8.6.2 and HEAD.

comment:11 Changed 12 days ago by Ryan Scott <ryan.gl.scott@…>

In aef5d825/ghc:

Add test cases for #7503, #14451

At some point between 8.4 and 8.6, two things were fixed:

* The entirety of #14451.
* One of the test cases in #7503. I've added this as T7503a. The
  other test case from that ticket still does /not/ work, so we'll
  have to add T7503b some other day.

comment:12 Changed 12 days ago by RyanGlScott

Test Case: typecheck/should_compile/T7503a

I've added a test case for the first program in comment:10 as T7503a. A test case for the other program—which I'd assume would be called T7503b—must wait for another day.

comment:13 Changed 9 days ago by simonpj

#12088 seems to be in the same territory

Note: See TracTickets for help on using tickets.