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.