Re: Superclasses of type families returning constraints?

On Jan 6, 2020, at 08:52, Simon Peyton Jones wrote:

This is rejected, and it's not in the least bit puzzling! You have evidence for (F a b) and you need to prove (a~b) -- for any a and b. Obviously you can't. And in Core you could write (eq @Int @Bool (error "urk")) and you jolly well don’t want it to return Refl.

I’m not sure I totally understand your complaint. If I were to write eq :: a ~ b => a :~: b eq = Refl then in core I could still write `eq @Int @Bool (error "urk")`, and that would be entirely well-typed. It would not really return Refl at runtime, of course, but neither would the example I gave in my original email. Perhaps a better way to phrase my original example is to write it this way: type family F a b where F a b = () -- regular (), not (() :: Constraint) eq :: F a b ~ () => a :~: b eq = Refl In this case, in core, we receive an argument of type `F a b ~ ()`, and we can force that to obtain a coercion of type `F a b ~# ()`. For reasons similar to the mechanisms behind injective type families, that equality really does imply `a ~# b`. The fact that the type family returns an empty constraint tuple is really incidental, and perhaps unnecessarily misleading. Does that clear up your confusion? Or have I misunderstood your concern? Alexis