Data.Type.Equality.== works better when used at kind * -> * -> Bool

[adam vogt]

Hello List,

Given the following definitions:

> class HEq (x :: k) (y :: k) (b :: Bool) | x y -> b

> instance ((Proxy x == Proxy y) ~ b) => HEq x y b -- (A)

> instance ((x == y) ~ b) => HEq x y b -- (B)

The instance (A) lets HList compile, which can be reproduced with:

 darcs get http://code.haskell.org/~aavogt/HList/
 cd HList
 cabal install -fnew_type_eq

When I select instance (B) instead by uncommenting the alternative
instance in Data/HList/FakePrelude.hs, one of the more informative
type errors suggests that the == type family is getting stuck:

Data/HList/Variant.hs:202:29: Warning:
    Could not deduce (HasField'
                        (l Data.Type.Equality.== l) l (Tagged l (Maybe
e) : v) (Maybe e))
      arising from a use of ‘mkVariant’
    from the context (ConvHList p,
                      SameLength' v v,
                      HMapCxt HMaybeF p v,
                      le ~ Tagged l (Maybe e))

Does this suggest that type (==) should work with all kinds, as it would with:

> type a == b = Proxy a `EqStar` Proxy b

https://github.com/ghc/packages-base/blob/master/Data/Type/Equality.hs
mentions "A poly-kinded instance is /not/ provided, as a recursive
definition for algebraic kinds is generally more useful.", but are
there instances of (==) that behave differently from the poly-kinded
version?

Regards,
Adam