When I say

{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies #-}

module Bug where

import Data.Proxy

class kproxy ~ 'KProxy => C (kproxy :: KProxy k) where
  type F (a :: k)

instance C ('KProxy :: KProxy Bool) where
  type F a = Int

I get

    Type indexes must match class instance head
    Found ‘k’ but expected ‘Bool’
    In the type instance declaration for ‘F’
    In the instance declaration for ‘C (KProxy :: KProxy Bool)’

But the kind of a should really be known to be Bool.

This ticket is broken out from ticket:9063#comment:82569, which was evidently not addressed when fixing that ticket.

Patch coming soon.