Newtype over (~#)

[Richard Eisenberg]

We do need a separate category, though: otherwise, we could cast by `f x`, where `f` is a non-terminating functions. We erase casts, so the function would never get called. Maybe if we required that casts are always by variables (essentially, A-normalize casts) we could avoid this? But then would we require A-normalization to build coercions from pieces (as opposed to calling functions)? It's unclear.

I think the first versions of this idea didn't require the separate syntactic category, but all work for the past decade has. I think there are other ways, but the way GHC handles this now is somewhat poor, because of #17291.

Richard

> On Feb 5, 2021, at 7:56 PM, Igor Popov <mniip at typeable.io> wrote:
> 
>> 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