Newtype over (~#)

[Richard Eisenberg]

> On Feb 10, 2021, at 5:43 AM, Igor Popov <mniip at typeable.io> wrote:
> 
> 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?

No, we wouldn't need the restriction if GHC were implemented correctly -- that is, without the mkLocalIdOrCoVar abomination that looks at the type of a binder to determine whether it's a CoVar.

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

I don't see any equalities on either side here. Instead, this is a relationship between equality *types*. That should be just fine; GHC even produces such things already from time to time. I do think you'll need two `@k`s on the right, though. The rule you're worried about forbids constructions like (cv1 ~R cv2), where cv1 and cv2 have been injected into types via CoercionTy.

> mkReprPrimEqPred doesn't. Who to believe and what are the pitfalls?

mkReprPrimEqPred has the same properties here; the comments should be better.

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

No, it can't. This may be a real blocker. I hadn't thought about this part of the problem.
> 
> 
>    <a> `cast` Sym (N::~:# k) <a> <a>
> 
> Is this valid?

No, for the same reasons.

This is unfortunate, as I thought this was a good idea. Yet I'm not hopeful that there's an easy way out of this particular trap.

Richard