<html><head><meta http-equiv="Content-Type" content="text/html; charset=us-ascii"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">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.<div class=""><br class=""></div><div class="">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.)</div><div class=""><br class=""></div><div class="">I think the problems you're running into are all around this confusion. For example,</div><div class=""><br class=""></div><div class="">(\ (v :: a ~# a) -> v `cast` <a ~# a>_R)<br class=""> @~ <a>_N</div><div class=""><br class=""></div><div class="">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.<br class=""><div><br class=""></div></div><div>This is all <a href="https://gitlab.haskell.org/ghc/ghc/-/issues/17291" class="">https://gitlab.haskell.org/ghc/ghc/-/issues/17291</a>.</div><div><br class=""></div><div>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.</div><div><br class=""></div><div>Is your implementation available somewhere?</div><div><br class=""></div><div>I hope this helps!</div><div>Richard</div></body></html>