[GHC] #8985: Strange kind error with type family, GADTs, data kinds, and kind polymorphism

[GHC]

#8985: Strange kind error with type family, GADTs, data kinds, and kind
polymorphism
-------------------------------------+-------------------------------------
       Reporter:  kosmikus           |             Owner:
           Type:  bug                |            Status:  new
       Priority:  normal             |         Milestone:
      Component:  Compiler (Type     |           Version:  7.8.1
  checker)                           |  Operating System:  Unknown/Multiple
       Keywords:                     |   Type of failure:  GHC rejects
   Architecture:  Unknown/Multiple   |  valid program
     Difficulty:  Unknown            |         Test Case:
     Blocked By:                     |          Blocking:
Related Tickets:                     |
-------------------------------------+-------------------------------------
 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.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/8985>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler