[GHC] #13972: GHC 8.2 error message around indexes for associated type instances is baffling

[GHC]

#13972: GHC 8.2 error message around indexes for associated type instances is
baffling
-------------------------------------+-------------------------------------
           Reporter:  RyanGlScott    |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1-rc2
  (Type checker)                     |
           Keywords:  TypeFamilies,  |  Operating System:  Unknown/Multiple
  TypeInType                         |
       Architecture:                 |   Type of failure:  Poor/confusing
  Unknown/Multiple                   |  error message
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 This program doesn't typecheck (only in GHC 8.2 and later):

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

 import Data.Kind

 class C (a :: k) where
   type T k :: Type

 instance C Left where
   type T (a -> Either a b) = Int
 }}}

 {{{
 $ /opt/ghc/8.2.1/bin/ghci Bug.hs
 GHCi, version 8.2.0.20170704: http://www.haskell.org/ghc/  :? for help
 Loaded GHCi configuration from /home/rgscott/.ghci
 [1 of 1] Compiling Bug              ( Bug.hs, interpreted )

 Bug.hs:12:8: error:
     • Type indexes must match class instance head
       Expected: T (a -> Either a b)
         Actual: T (a -> Either a b)
     • In the type instance declaration for ‘T’
       In the instance declaration for ‘C Left’
    |
 12 |   type T (a -> Either a b) = Int
    |        ^^^^^^^^^^^^^^^^^^^^^^^^^
 }}}

 Well those expected and actual types look pretty darn similar to me!

 Note that the problem can be worked around by giving an explicit kind
 annotation for `Left`:

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

 import Data.Kind

 class C (a :: k) where
   type T k :: Type

 instance C (Left :: a -> Either a b) where
   type T (a -> Either a b) = Int
 }}}

 I see two things we could do here:

 1. Relax the "Type indexes must match class instance head" check so that
 it doesn't apply to invisible kind variables like `a` and `b`.
 2. Clarify the error message. At the very least, we could say `Expected: T
 (a1 -> Either a1 b1)` as a hint that `a` and `b` aren't the same type
 variables as `a1` and `b1`. In an ideal world, we'd even indicate where
 `a1` and `b1` should be coming from (the kind of `Left`).

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