Re: Newtype over (~#)

On Feb 10, 2021, at 5:43 AM, Igor Popov 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