[GHC] #8707: Kind inference fails in data instance definition

[GHC]

#8707: Kind inference fails in data instance definition
------------------------------------+-------------------------------------
       Reporter:  goldfire          |             Owner:
           Type:  bug               |            Status:  new
       Priority:  normal            |         Milestone:
      Component:  Compiler          |           Version:  7.7
       Keywords:                    |  Operating System:  Unknown/Multiple
   Architecture:  Unknown/Multiple  |   Type of failure:  None/Unknown
     Difficulty:  Unknown           |         Test Case:
     Blocked By:                    |          Blocking:
Related Tickets:                    |
------------------------------------+-------------------------------------
 Consider the following shenanigans:

 {{{
 {-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, GADTs #-}

 data family SingDF (a :: (k, k2 -> *))
 data Ctor :: k -> *

 data instance SingDF (a :: (Bool, Bool -> *)) where
   SFalse :: SingDF '(False, Ctor)
 }}}

 HEAD reports (with `-fprint-explicit-kinds`)

 {{{
     Data constructor ‛SFalse’ returns type ‛SingDF
                                               Bool k '('False, Ctor k)’
       instead of an instance of its parent type ‛SingDF Bool Bool a’
     In the definition of data constructor ‛SFalse’
     In the data instance declaration for ‛SingDF’
 }}}

 I see two problems here:

 1) Kind inference should fix the problem. If I add a kind annotation to
 `Ctor`, the code works. GHC should be able to infer this kind annotation
 for me.

 2) The error message is not particularly helpful. GHC 7.6.3 had a more
 verbose, but more helpful message.

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