Gruesome kind mismatch errors for associated data family instances

Spun off from #14175 (closed)##14230 (closed). This program, which can only really be compiled on GHC HEAD at the moment:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

class C k where
  data CD :: k -> k -> *

instance C (Maybe a) where
  data CD :: (k -> *) -> (k -> *) -> *

Gives a heinous error message:

Bug.hs:11:3: error:
    • Expected kind ‘(k -> *) -> (k -> *) -> *’,
        but ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe a
                                                        -> Maybe a -> *’
    • In the data instance declaration for ‘CD’
      In the instance declaration for ‘C (Maybe a)’
   |
11 |   data CD :: (k -> *) -> (k -> *) -> *
   |   ^^^^^^^

• We shouldn't be expecting kind (k -> *) -> (k -> *) -> *, but rather kind Maybe a -> Maybe a -> *, due to the instance head itself.
• The phrase ‘CD :: (k -> *) -> (k -> *) -> *’ has kind ‘Maybe -> Maybe a -> *’ is similarly confusing. This doesn't point out that the real issue is the use of (k -> *).

Another program in a similar vein:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
module Bug where

import Data.Kind

class C a where
  data CD k (a :: k) :: k -> *

instance C (Maybe a) where
  data CD k (a :: k -> *) :: (k -> *) -> *

Bug.hs:13:3: error:
    • Expected kind ‘(k -> *) -> *’,
        but ‘CD k (a :: k -> *) :: (k -> *) -> *’ has kind ‘k -> *’
    • In the data instance declaration for ‘CD’
      In the instance declaration for ‘C (Maybe a)’
   |
13 |   data CD k (a :: k -> *) :: (k -> *) -> *
   |   ^^^^^^^^^^^^^^^^^^^^^^^

This error message is further muddled by the incorrect use of k as the first type pattern (instead of k -> *, as subsequent kind signatures would suggest).

Trac metadata

Trac field	Value
Version	8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture