[GHC] #14230: Gruesome kind mismatch errors for associated data family instances

14 Sep 2017

      #14230: Gruesome kind mismatch errors for associated data family instances
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.3
  (Type checker)                     |
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:  #14175
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Spun off from https://ghc.haskell.org/trac/ghc/ticket/14175#comment:9.
 This program, which can only really be compiled on GHC HEAD at the moment:

 {{{#!hs
 {-# 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:

 {{{#!hs
 {-# 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).

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