Newtype over (~#)

[Richard Eisenberg]

GHC cheats in this area. The problem is that (a ~# b) is a type, because that is terribly, terribly convenient. But it really shouldn't be.

The problem is that coercion variables are different from regular variables. So, if we say (v :: a ~# b), we must always be careful: is v a coercion variable or not? If it isn't, then v is useless. You cannot, for instance, use v in a cast. In a number of places, GHC must produce a variable binder of a certain type. It will sometimes examine that type; if the type is an equality type, then the binder will be a coercion variable; otherwise, it will be a normal Id. This is wrong, but again, very convenient. (Wrong because we should always know in advance whether we want a coercion variable or an Id.)

I think the problems you're running into are all around this confusion. For example,

(\ (v :: a ~# a) -> v `cast` <a ~# a>_R)
   @~ <a>_N

is ill-formed, whether v is an Id or a CoVar. If it's an Id, then this is wrong because you have an Id with a coercion type. (The theory of the core language does not prevent such things, but I'm not surprised that GHC would fall over if you tried it.) If v is a CoVar, then its use as the left-hand side of `cast` is wrong.

This is all https://gitlab.haskell.org/ghc/ghc/-/issues/17291 <https://gitlab.haskell.org/ghc/ghc/-/issues/17291>.

All that said, I think your original idea is a fine one: a newtype wrapper around ~#. It's possible there is just some Id/CoVar confusion in your implementation, and that's what's causing the trouble. I don't see a correct implementation as impossible.

Is your implementation available somewhere?

I hope this helps!
Richard
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20210205/167e17af/attachment.html>