Superclasses of type families returning constraints?

[Richard Eisenberg]

> On Jan 6, 2020, at 2:52 PM, Simon Peyton Jones via ghc-devs <ghc-devs at haskell.org> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20200106/bd74161c/attachment.html>