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 <r...@richarde.dev> 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 <mn...@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 > _______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs