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

[Peter Wang]

On Fri, 31 Jul 2026 15:09:09 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> 
> On Fri, 31 Jul 2026 12:16:57 +0200 (CEST), "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> > > Please update the reference manual to reflect the rules.
> > 
> > I will do so in a separate diff, to allow for easier review.
> 
> The attached diff does not do that yet, but I need feedback
> on it before I can go further. This diff mostly notes issues
> with the current text, and contains proposals for how to
> make it better.
> 
> For review by both Peter and Julien.
> 
> Zoltan.

> diff --git a/doc/mercury_reference_manual.texi b/doc/mercury_reference_manual.texi
> index ebed23b19..b2286d571 100644
> --- a/doc/mercury_reference_manual.texi
> +++ b/doc/mercury_reference_manual.texi
...
> @@ -8520,39 +8524,64 @@ coerce(@var{Term})
>  The expression is type-correct if and only if
>  @var{FromType} and @var{ToType} are both discriminated union types,
>  and after replacing the principal type constructors with base types
> + at c XXX This reads like a category error:
> + at c you replace a type_ctor with another type_ctor,
> + at c or a type_ctor with another type;
> + at c you do not replace a type_ctor with a complete type.
>  (@pxref{Subtypes})
>  the two types have the same type constructor,
>  and the arguments of the common type constructor
>  satisfy the type parameter variance restrictions below.
>  

You're right.

    The expression is type-correct if and only if
    @var{FromType} and @var{ToType} are both discriminated union types
    and, after replacing the principal type constructors
    with their base type constructors,
    the resulting types have the same principal type constructor,
    and the arguments of that principal type constructor
    satisfy the type parameter variance restrictions below.

>  Let @var{FromType} expand out to @samp{base(S1, ..., Sn)}
> + at c XXX In the subtype section, we use "expand" only in the sense of
> + at c expanding out equivalence types. Here, we also include replacing each
> + at c subtype with its supertype, using the head of the subtype's definition.
> + at c Do we have a specific name for that operation?
> + at c If not, *should* we give it a name?

Maybe "resolve to"?

>  and @var{ToType} expand out to @samp{base(T1, ..., Tn)},
>  where @samp{base(B1, ..., Bn)} is the common base type,
>  and @var{Bi} is the i'th type parameter,
>  which is bound to @var{Si} in @var{FromType}
>  and @var{Ti} in @var{ToType}.
> + at c XXX Wouldn't Fi be better notation than Si?
> + at c Si would make sense if we talked about source types, but
> + at c we call them about from-types.

S and T are pretty common for types, e.g.
https://en.wikipedia.org/wiki/Subtyping

F is probably more suggestive of a function, I guess.

Also, subtyping relations are often written with a <: operator.
We could do that as well.

> + at c XXX And wouldn't BPi be better notation than just Bi?
> + at c It would clarify that BPi are type parameters, i.e. type variables,
> + at c while the Si/Fi/Ti are complete types.
>  

Perhaps, or BVi (for variable)?

> -Otherwise, the @code{coerce} expression is not type-correct.
> +If none of the above is true, i.e.@: if @samp{Si} and @samp{Ti} are not related.
> +then the @code{coerce} expression is not type-correct.
>  @c NOTE: we deliberately disallow coercion between arbitrary phantom types.
>  
> + at c I wouild approach the above by
> + at c - first defining the @samp{S =< T} relation,
> + at c - defining four categories (2x2) based on whether S=<T and T=<S hold,
> + at c - dividing the base type_ctor's parameters into
> + at c   - the must-be-invariant parameters for which S=T must hold, and
> + at c   - the need-not-be-invariant parameters for which one or both of
> + at c     S=<T and T=<S must hold
> + at c - and THEN saying which parameters must be invariant.
> +

Ok.

Peter