Data.Type.Equality.== works better when used at kind * -> * -> Bool
adam vogt
vogt.adam at gmail.com
Sat May 31 05:12:50 UTC 2014
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
More information about the Glasgow-haskell-users
mailing list