Strange kind error with type family, GADTs, data kinds, and kind polymorphism
Consider the following test case (I've tried hard to make it minimal, which unfortunately means there's not a lot of intuition left):
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs, TypeOperators #-}
data X (xs :: [k]) = MkX
data Y :: (k -> *) -> [k] -> * where
MkY :: f x -> Y f (x ': xs)
type family F (a :: [[*]]) :: *
type instance F xss = Y X xss
works :: Y X '[ '[ ] ] -> ()
works (MkY MkX) = ()
fails :: F '[ '[ ] ] -> ()
fails (MkY MkX) = ()
This code compiles in GHC 7.6.3, but it fails in GHC 7.8.1 (both rc2 and the actual release) with the following error:
TestCase.hs:14:8:
Couldn't match kind ‘k0’ with ‘*’
Expected type: F '['[]]
Actual type: Y t0 t1
In the pattern: MkY MkX
In an equation for ‘fails’: fails (MkY MkX) = ()
TestCase.hs:14:12:
Couldn't match type ‘t0’ with ‘X’
‘t0’ is untouchable
inside the constraints (t1 ~ (x : xs))
bound by a pattern with constructor
MkY :: forall (f :: k -> *) (x :: k) (xs :: [k]).
f x -> Y f (x : xs),
in an equation for ‘fails’
at TestCase.hs:14:8-14
Expected type: t0 x
Actual type: X x
In the pattern: MkX
In the pattern: MkY MkX
In an equation for ‘fails’: fails (MkY MkX) = ()
I'm puzzled that simply adding the type family invokation makes the type checker fail with a kind error, even though the type family itself itsn't kind-polymorphic.
Trac metadata
Trac field | Value |
---|---|
Version | 7.8.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | |
Operating system | |
Architecture |