GHC 8.2 error message around indexes for associated type instances is baffling

This program doesn't typecheck (only in GHC 8.2 and later):

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

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

Trac metadata

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