Newtype over (~#)

[Igor Popov]

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 <rae at 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 <mniip at 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
>