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

That's a really interesting quirk. That kind of explains why an argument to a cast has to be a CoVar, we want all casts to be guarded by a case-of. But do we still need the restriction that an Id cannot have a coercion type? Either case it seems like we need to be extremely careful with how the wrapper and the matcher works for such a constructor. I was hoping a sledgehammer approach would work where we kind of just force (a ~# b) as a field into a newtype, and the existing machinery magically works with it. The construction is then chock full of questions: axiom N::~:# :: forall k. (:~:#) @k ~R (~#) @k Is this valid? mkPrimEqPred says it doesn't like equalities on either side (I'm assuming this applies to eta-contracted equalities as well). mkReprPrimEqPred doesn't. Who to believe and what are the pitfalls? Refl# :: forall k (a b :: k). a ~# b -> a :~:# b Refl# = \@k @a @b v -> v `cast` Sym (N::~:# k) <a> <b> Is this valid? You say that v has to be bound as a CoVar (current newtype machinery will not do this). Can a CoVar appear in the LHS of a cast? The result is definitely a type and can be bound to an Id, I guess. $WRefl# :: forall k (a :: k). a :~:# a $WRefl# = \@k @a -> Refl# @k @a @a <a> Relatively tame, but however once we inline the definition of Refl# (simpleOptExpr will do this when registering an unfolding), we get: <a> `cast` Sym (N::~:# k) <a> <a> Is this valid? The matcher/boxer (is that the word) has to be carefully constructed as well: we have to desugar case x of Refl# -> e where (x :: a :~:# b) into: case x `cast` N::~:# k <a> <b> of co -> e where co is now a CoVar. Can a cast's result type be a coercion? Can a coercion be the scrutinee of a case-of? (Judging by the code we generate for eq_sel the answer is yes). -- mniip On Sun, Feb 7, 2021 at 7:41 PM Richard Eisenberg wrote:

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 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