Data.Type.Equality.== works better when used at kind * -> * -> Bool
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
On May 31, 2014, at 1:12 AM, adam vogt
are there instances of (==) that behave differently from the poly-kinded version?
Yes. To be concrete, here would be the polykinded instance:
type family EqPoly (a :: k) (b :: k) where EqPoly a a = True EqPoly a b = False type instance (a :: k) == (b :: k) = EqPoly a b
Note that this overlaps with every other instance -- if this were defined, it would be the only instance for (==). Now, consider
data Nat = Zero | Succ Nat
Suppose I want
foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True) foo = Refl
This would not type-check with the poly-kinded instance. `Succ n == Succ m` quickly becomes `EqPoly (Succ n) (Succ m)` but then is stuck. We don't know enough about `n` and `m` to reduce further. On the other hand, consider this:
type family EqNat (a :: Nat) (b :: Nat) where EqNat Zero Zero = True EqNat (Succ n) (Succ m) = EqNat n m EqNat n m = False type instance (a :: Nat) == (b :: Nat) = EqNat a b
With this instance, `foo` type-checks fine. `Succ n == Succ m` becomes `EqNat (Succ n) (Succ m)` which becomes `EqNat n m`. Thus, we can conclude `(n == m) ~ True` as desired. So, the Nat-specific instance allows strictly more reductions, and is thus preferable to the poly-kinded instance. But, if we introduce the poly-kinded instance, we are barred from writing the Nat-specific instance, due to overlap. Even better than the current instance for * would be one that does this sort of recursion for all datatypes, something like this:
type family EqStar (a :: *) (b :: *) where EqStar Bool Bool = True EqStar (a,b) (c,d) = a == c && b == d EqStar (Maybe a) (Maybe b) = a == b ... EqStar a b = False
The problem is the (...) is extensible -- we would want to add new cases for all datatypes in scope. This is not currently possible for closed type families. Perhaps it would be an improvement to write the cases for all types in scope in Data.Type.Equality -- that is, the types exported from `base`. I hope this is helpful. In any case, I will put some of the text in this email into the comments in Data.Type.Equality for the next person who looks. Richard
participants (2)
-
adam vogt -
Richard Eisenberg