Newtype over (~#)

[Igor Popov]

> 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