On Fri, Aug 11, 2017 at 11:39 AM, Richard Eisenberg
If (==) is to be useful in a type system, we would need such a guarantee. (By "useful", I mean that this is implementable:
reifyEq :: forall a b. ((a == b) ~ True, Typeable a, Typeable b) => a :~: b [The above is edited slightly]
Let's get back to this for a moment. I tried actually implementing this for the simple polykinded version you suggested on my differential: infix 4 == type family (a :: k) == (b :: k) :: Bool where f a == g b = f == g && a == b a == a = 'True _ == _ = 'False Sadly, it doesn't seem to be possible to really do it properly. First, there's no way to prove (f == g) ~ 'True or (x == y) ~ 'True from just (f x == g y) ~ 'True. The latter reduces to (f == g && x == y) ~ 'True, but (&&) is not a constructive "and", so we can't actually extract any information from it. Thus we can't work from top to bottom. Second, pattern matching on TypeReps can only expose equality and not inequality (as we have no first-class notion of inequality). So if we try to work from bottom to top, foo :: TypeRep a -> TypeRep b -> Either ((a == b) :~: 'False) ((a == b) :~: 'True) we will get well and thoroughly stuck on the non-recursive cases. So the only way I see to implement reifyEq is reifyEq = case eqTypeRep (typeRep :: TypeRep a) (typeRep :: TypeRep b) of Just HRefl -> Refl Nothing -> error "unreachable" That doesn't really seem terribly satisfying.