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

[Peter Wang]

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.

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

> diff --git a/doc/mercury_reference_manual.texi b/doc/mercury_reference_manual.texi
> index ebed23b19..357e95d79 100644
> --- a/doc/mercury_reference_manual.texi
> +++ b/doc/mercury_reference_manual.texi
...
> + at heading Lifting a subtype
> +
> +If type @samp{S} has the form @samp{S = f(S1, ..., Sn)}
> +and there is a visible subtype definition starting with
> + at w{@samp{:- type f(RP1, ..., RPn) =< U}},
> +then we define @samp{lift(S)} as the type that results from
> +replacing all occurrences of each @samp{RPi} in @samp{U}
> +with the corresponding @samp{Si}.
> +
> +Since the sypertype U in that subtype definition
> +must have the form of a type constructor
> +applied to zero or more argument types,
> +the result of the substitution must also have the same form.
> +If the supertype's type constructor is also a subtype,
> +then lifting may be applied to it as well.
> +
> +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.

> + at itemize @bullet
> + at item
> + at samp{S}, if the principal type constructor of @samp{S} is @samp{f/n};
> + at item
> + at samp{lift_to(f, n, lift(S))},
> +if the principal type constructor of @samp{S} is not @samp{f/n},
> +but that principal type constructor does have a visible subtype definition; and
> + at item
> + at samp{S}, otherwise.
> + at end itemize
> +
> + at heading The subtype relation
> +
>  (In the following discussion,
>  we assume that all equivalence types have been expanded out.)
>  
> @@ -3456,8 +3504,34 @@ and if @samp{S = f(S1, ..., Sn)}, @samp{S =< T} holds if
>  In other words, if all occurrences of @var{Ri} in @var{U}
>  are replaced by the corresponding @var{Si} to give @var{Usub},
>  then @samp{Usub =< T} must hold.
> +This is alternative 1.
> +
> +XXX We could replace the second item @emph{either} with just:
> +
> +If @samp{S} and @samp{T} have different principal type constructors,
> + at samp{S =< T} holds if @samp{lift(S) =< T}.
> +This is alternative 2.
> +

> + at emph{or} with
> +
> +If @samp{S} and @samp{T} have different principal type constructors,
> +say @samp{s/n} and @samp{t/m} respectively,
> + at samp{S =< T} holds if @samp{lift_to(t, m, S) =< T}.
> +This is alternative 3.
> +
> +Only the latter would require defining lift_to above,
> +but I think it would be easier for people to understand,
> +since it makes explicit the iteration involved.
> +
>  @end itemize
>  
> +And we could express the entire subtype test as just
> +the first item @emph{after} trying to lift S to the same typector as T.
> +This is alternative 4.
> +
> +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.

> @@ -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.

Peter