5 Feb
2021
5 Feb
'21
7:56 p.m.
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.
I don't really see a problem here. The fact that only a "coercion variable" can be used in a cast should be enforced by the typing rule for cast. That doesn't require having a distinct "syntactic category" of coercion variables, unless I'm missing something. -- mniip