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