[GHC] #15515: Bogus "No instance" error when type families appear in kinds

13 Aug 2018

      #15515: Bogus "No instance" error when type families appear in kinds
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.8.1
          Component:  Compiler       |           Version:  8.4.3
  (Type checker)                     |
           Keywords:  TypeInType,    |  Operating System:  Unknown/Multiple
  TypeFamilies                       |
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 The following code typechecks:

 {{{#!hs
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeInType #-}
 module Bug where

 import Data.Kind
 import Data.Proxy

 class C a where
   c :: Proxy a

 type family F

 data D :: F -> Type

 instance C (D :: F -> Type) where
   c = undefined
 }}}

 However, if we try to actually //use// that `C D` instance, like so:

 {{{#!hs
 c' :: Proxy (D :: F -> Type)
 c' = c @(D :: F -> Type)
 }}}

 Then GHC gives a rather flummoxing error message:

 {{{
 $ /opt/ghc/8.4.3/bin/ghc Bug.hs
 [1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

 Bug.hs:20:6: error:
     • No instance for (C D) arising from a use of ‘c’
     • In the expression: c @(D :: F -> Type)
       In an equation for ‘c'’: c' = c @(D :: F -> Type)
    |
 20 | c' = c @(D :: F -> Type)
    |      ^^^^^^^^^^^^^^^^^^^
 }}}

 But that error is clearly misleading, as we defined such a `C D` instance
 directly above it!

 The use of the type family `F` in the kind of `D` appears to play an
 important role in this bug. If I change `F` to be a data type (e.g., `data
 F`), then `c'` is accepted.

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