> On Jan 6, 2020, at 08:52, Simon Peyton Jones <[email protected]> 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
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
