[m-rev.] for review: expand the class of allowed coercions

[Zoltan Somogyi]

On Mon, 3 Aug 2026 14:37:37 +1000, Peter Wang <novalazy at gmail.com> wrote:

> On Sat, 01 Aug 2026 13:51:10 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> > 
> > In the attached updated diff, I defined this operation, and gave it the name
> > "lift", as from subtype to supertype. Better names welcome; any link
> > to an existing name for this operation would be even more welcome,
> > since a standard name is better than a good name :-(
> > 
> 
> I know "lift" already has other meanings in PLT and other languages,
> so I would try to avoid that.

I know, but I don't think any are close enough to be confusable with this op.
Can you think of any?

> Is talking about performing a "substitution" insufficient?
> The function could be called "sub" or "subst".

We already use "substitution" for other purposes, so I am sure
that would be more confusing than helpful. This is definitely *is* too close.

However, I still welcome other names.

"raise" is a possibility. It is used for exceptions, but there are none
involved here. I don't like "elevate", but could live with it if you guys prefer it.

> > +We define @samp{lift_to(f, n, S)} as
> 
> You could write that as `lift_to(f/n, S)'. I think it would be clearer.

Will do.
 
> > +Which of these four alternatives do people prefer?
> > +I (zs) prefer #4.
> > +
> >  @noindent
> >  2. For two tuple types
> >  @samp{S = @{S1, ..., Sn@}} and @samp{T = @{T1, ..., Tn@}},
> 
> Ok. Alternative 4 seems good to me.

I will flesh that out then.

> > @@ -3496,6 +3571,9 @@ if and only if all of the following conditions hold:
> >      the same argument modes, determinism, and purity.
> >      @end itemize
> >  @end itemize
> > + at c XXX I (zs) do not see how this differs from
> > + at c requiring P and Q to be identical.
> > + at c If there *is* a difference, we should use S and T, not P and Q.
> 
> Yes, there's no difference as we don't allow subtyping in higher-order
> arguments. I think there is some value in being explicit in what
> identical means, as the part about higher-order insts may not be
> obvious. The current text is a bit more verbose than the original text.

You say "there is no difference", but the definition being quoted above says:

"if either of @var{P} and @var{Q} has higher-order inst information,
then @var{P} and @var{Q} must have
the @emph{same} higher-order inst information",

meaning that they *can* differ in the presence vs absence of the
higher order inst, but the check_is_subtype predicate requires
agreement: either both have higher order inst info, or neither does.

I will change the wording to match the code.

Zoltan.