Superclasses of type families returning constraints?

[Alexis King]

> On Jan 6, 2020, at 08:52, Simon Peyton Jones <simonpj at microsoft.com> 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