> On Jan 6, 2020, at 2:52 PM, Simon Peyton Jones via ghc-devs
> <[email protected]> wrote:
>
> | type family F a b :: Constraint where
> | F a a = ()
> |
> | eq :: F a b => a :~: b
> | eq = Refl
>
> 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.
But how could you possibly have evidence for (F a b) without (a ~ b)? 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.
Why not?
> eq = /\ a b. \ (d :: F a b). case d of Something (co :: a ~# b) -> Refl @a @b
> co
This would obviously require extensions to Core and Haskell, but it's not a
priori wrong to do so.
Richard
_______________________________________________
ghc-devs mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
