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