> On Feb 10, 2021, at 5:43 AM, Igor Popov <mn...@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 _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
