Superclasses of type families returning constraints?
Alexis King
lexi.lambda at gmail.com
Mon Jan 6 18:05:10 UTC 2020
> 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
More information about the ghc-devs
mailing list