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
_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
