GitLab

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