[m-rev.] for review: an updated draft of coercions in the reference manual

[Zoltan Somogyi]

On Wed, 5 Aug 2026 17:13:47 +1000, Peter Wang <novalazy at gmail.com> wrote:

> On Tue, 04 Aug 2026 23:39:01 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> > + at heading Lifting a subtype
> > +
> > +If type @samp{S} has the form @samp{S = tc(S1, ..., Sn)}
> > +and there is a visible subtype definition starting with
> > + at w{@samp{:- type tc(RP1, ..., RPn) =< U}},
> > +then we define @samp{lift(S)} as the type that results from
> > +replacing all occurrences of each type parameter @samp{RPi} in @samp{U}
> > +with the corresponding @samp{Si}.
> > +
> > +Since the sypertype @samp{U} in that subtype definition
> 
> supertype

The definition I am referring to is the one that occurs in the
prior paragraph, i.e. @samp{:- type tc(RP1, ..., RPn) =< U}}.
That is a subtype definition.

Would this be clearer if we replaced "that subtype definition"
with "@samp{:- type tc(RP1, ..., RPn) =< U}" itself?

> > + at samp{S} and @samp{T} have identical argument types, and
> > + at item
> > +either
> > +    @itemize
> >      @item
> > -    @var{P} and @var{Q} are either
> > -    both @samp{pred} types, or both @samp{func} types,
> > +    neither @samp{S} and @samp{T} has any higher-order inst information, or
> 
> I suggest "both have no higher-order inst information" to avoid "either
> ... neither".

Done.

> > +Subtyping theory allows @samp{S =< T} to hold for e.g. two predicates
> > +if their arguments are not invariant (meaning they are not identical),
> > +provided that their input arguments are contravariant and
> > +their output arguments are covariant.
> 
> I don't hink you need "if their arguments are not invariant".

You are right, the text would be correct without that phrase.
I included it anyway because the issue I am trying to explain
is concerned with what happens when the arguments are NOT invariant.


> > +A term @samp{FromTerm} may be converted from its type @samp{FromType}
> > +to another type @samp{ToType}
> >  using a type conversion expression of the form:
> >  
> >  @example
> > -coerce(@var{Term})
> > +coerce(@var{FromTerm})
> >  @end example
> >  
> > +whose result it bound, either implicitly or explicitly,
> 
> is bound

Fixed.

> > +to another term that here we call @samp{ToTerm}
> > +(which is usually a variable).
> > +
> 
> >  The expression is type-correct if and only if
> > - at var{FromType} and @var{ToType} are both discriminated union types,
> > -and after replacing the principal type constructors with base types
> > -(@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.
> > + at itemize @bullet
> > + at item
> > + at samp{FromType} and @samp{ToType} are both discriminated union types;
> > + at c XXX It should be possible to extend this to allow both to be tuples
> > + at c of equal arities, by simply requiring each tuple arg to be coercable.
> 
> Yes, it is possible.

I will keep the XXX until the code is changed to allow that.

> > + at item
> > + at samp{lift_to_base(FromType)} and @samp{lift_to_base(ToType)}
> > +have the same type constructor, being e.g.
> > + at samp{base_tc(BaseFromArgType1, ..., BaseFromArgTypen)} and
> > + at samp{base_tc(BaseToArgType1, ..., BaseToArgTypen)} respectively,
> > +with the type parameters of the type constructor
> > + at samp{base_tc} in its declaration being @samp{BP1, ..., BPn};
> > + at item
> > +for all @var{i} in @samp{1..n} where @samp{BPi} must be invariant,
> > + at samp{BaseFromArgTypei} is identical to @samp{BaseToArgTypei}; and
> > + at c XXX Should we instead phrase this as
> > + at c "where the i'th parameter of base_tc must be invariant"?
> > + at item
> > +for all @var{i} in @samp{1..n} where @samp{BPi} need not be invariant,
> > + at samp{BaseFromArgTypei} is coercable to @samp{BaseToArgTypei}.
> > + at c XXX "coercable" is probably not the best name for this concept.
> > + at c Alternatives may be phrases like "related by subtyping".
> > + at end itemize
> 
> "coercable" sounds self referential.

Which is the main reason I don't like it either.

> I would say: are related by subtyping, are in a subtyping relation,
> or use the =< operator defined previously.

I am trying to avoid using the =< operator, for two reasons.
First, it is maths, and match operators need a non-maths name
as well, and second, the obvious use of =< is S =< T, and that is NOT
what I am trying to specify, but rather S =< B, T =< B.

How about "have a common ancestor"? With the first definition
of the phrase explicitly saying that this means S =< B, T =< B.

Or would "have a shared ancestor" be better?

However, both of those phrases describe the relations needed
for type conversions ONLY for du types. For the relation needed
for type conversions for types that are not du types but CONTAIN
du types, we will need an acceptable name, and I still don't have one.

> > +The last two conditions raise two new questions.
> > +Given a base type constructor, which of its parameters must be invariant?
> > +And what does it mean for one type to be coercable to another type?
> > +
> 
> > + at heading Must-be-invariant type parameters
> > +
> 
> Can we name this "Type parameter variance"? I don't like
> must-be-invariant.

I think that is

I think that would be misleading for most readers. The distinction I am
trying to make is definititely must-be-invariant vs need-not-be-invariant,
because regardless of which category a type parameter falls into,
the corresponding arg types in the from-type and to-type ARE allowed
to be invariant.

I think even "must-be-invariant" is a bit too abstract, because
it is not the parameter that must be invariant, but the arg types
bound to it. I just cannot think of a phrase to describe all that
that is short enough to be useful as a name for the concept.

> > +A base type must be a discriminated union type,
> > +which means its definition must have the form
> > +
> > + at example
> > +:- type base_tc(BP1, ..., BPn)
> > +    --->    f1(T11, ...)
> > +    ;       ...
> > +    ;       fm(Tm1, ...).
> > + at end example
> > +
> > +The parameter types @samp{BP1} ... @samp{BPn} 
> > +will typically occur in one or more of the @samp{Tij},
> > +where @var{i} is in @samp{1..m}, and
> > +the value of @var{j} after a given value of @var{i}
> > +must be between 1 and the arity of @samp{fi}.
> > +(It is also possible, though rare, for some @samp{BPk}
> > +to occur in none of the @samp{Tij}.)
> > +
> > +Parameter @var{k} of @samp{base_tc} must be invariant
> > +if and only if @samp{BPk} occurs in one or more of the @samp{Tij}
> > +for which any of the following holds:
> > +
> 
> I think defining Tij is distracting, and doesn't add anything.
> I suggest we say that BPi must be invariant if it occurs in a
> constructor argument of type ArgT, where: ...

Agreed. I went with a minor variation of what you wrote.

> > + at itemize @bullet
> > +
> > + at item
> > + at samp{Tij} is a higher order type;
> > +
> > + at item
> > + at samp{Tij} is a discriminated union type
> > +whose type constructor is @samp{base_tc},
> > +but whose arguments differ from the type constructor's parameter list,
> > +(meaning that it is any type other than
> > + at samp{base_tc(BP1, ..., BPn)});
> > +
> 
> > + at item
> > + at samp{Tij} is a discriminated union type
> > +whose type constructor is not @samp{base_tc},
> > +but that type constructor is not known to have
> > +an empty list of must-be-invariant type parameters; or
> > +
> 
> Can we call them "invariant type parameters"?

I don't think so, for the reason explained above.

> > + at item
> > + at samp{Tij} is a foreign type, a solver type, or an abstract type.
> > + at c XXX We should not mention solver types if they cannot occur
> > + at c in du types, but I (zs) don't know whether they can occur or not.
> > + at c XXX We currently make a type parameter must-be-invariant for a foreign type,
> > + at c but I (zs) don't know the justification for that.
> > +
> 
> For the same reason the type parameter in any mutable type must be
> invariant. If you can coerce a variable from mutvar(dog) to mutvar(animal),
> then you can put a cat in where an animal is accepted,
> then pull a cat out where a dog is expected.

OK, I will add something to that effect.

I notice you did not say anything about solver types.
Does anyone know whether they can occur in du type definitions?
I don't.

> > + at end itemize
> > +
> > +Basically, the reason for requiring @emph{any}
> > +type paramaters to be invariant,
> > +and thus saying that the corresponding pairs of argument types
> > +in @samp{lift_to_base(FromType)} and @samp{lift_to_base(ToType)}
> > +must be identical, is that
> 
> s/paramaters/parameters

Fixed.

> The start of the paragraph should say it explains the rationale for
> higher-order types (and not other types).

That depends on what "for" means in your sentence. Yes, the
requirement comes from higher order types, but it propagates
to *every* type that contains or even MAY contain a higher order type.
Because of this propagation, the rationale applies also to du types
and tuple types.

> > +That is the reason for the first bullet point above.
> > +The reason for the second is that any data constructor argument
> > +whose type is recursive but does not meet the imposed condition
> > +(possibly because it includes the parameters in a different order)
> > +may create a link that says
> > +"if this specific parameter of @samp{base_tc} must be invariant,
> > +then another specific parameter must also be invariant",
> > +and the implications of such links are hard for humans to understand.
> 
> Maybe so, but it doesn't sound very reference manual-y ;)

Agreed.

> I don't have a suggestion at this time.

I will keep the text until I get a suggestion for a better reason :-(

> > +In any case, in the vast majority of definitions of discriminated union types
> > +either have no recursively-typed arguments,
> > +or all their recursively-typed arguments
> > +exactly repeat the type constructor's parameter list.
> > + at c (Consider the definitions of pretty much all collection types,
> > + at c such as lists or maps.)
> > +Therefore in practice,
> > +the second bullet point rarely requires parameters to be invariant.
> 
> Maybe: rarely imposes invariance on type parameters.

I think what I wrote is clearer. Julien?

> > +The reason for the third bullet point is to allow coercions to happen
> 
> Suggestion: s/allow coercions to happen/allow a type conversion/

Done.

> > +when @samp{base_tc}'s definition includes data constructors with arguments
> > +whose types have definitions that cannot themselves require invariance.
> 
> I think you could delete "have definitions".

Yes, the sentence would be correct without it. However, I think it is
more *understandable* with it, because reasons for requiring a parameter
to be invariant come from the arg types in the type definitions.

> > +(The types bound to their type parameters are a separate question.)
> > +This rule means that
> > +e.g.@: an argument type of the form @samp{list(ElemType)} will never require
> > +any type parameters occurring inside @samp{ElemType} to be invariant,
> > +due to the @samp{list} type's one parameter not needing to be invariant:
> 
> s/never/not

Again, both are correct, but I think "never" is the one that better expresses
the point I am trying to get across.

> > +The main limitation that this bullet point imposes
> > +is on mutually recursive sets of type constructors
> > +that each have one or more parameters.
> > +(A type constructor obviously has no parameters that must be invariant
> > +if it has no parameters at all.)
> > +Consider two such types, say @samp{foo} and @samp{bar}.
> > +While computing which of @samp{foo}'s parameters must be invariant,
> > +we cannot already know whether any of @samp{bar}'s parameters must be invariant,
> > +and vice versa.
> > +Therefore in practice, this rule says that
> > +any type parameters that occur in mutually-recursive types
> > +must be invariant.
> > +
> 
> Hmm, a computation could assume that a parameter is NOT invariant, only
> failing if the assumption does not hold. I think the text may imply that
> the limitation is fundamental, not one of the implementation.

Agreed. I will try to work that point in there somewhere.

> > +The reason for the fourth bullet point,
> > +as applied to abstract type constructors, is simple.
> > +If the compiler does not have access to the definition of a type,
> > +it cannot know whether it contains any cause for requiring
> > +the type variables occurring in that type to be invariant.
> > +The only safe way to handle such situations
> > +is to assume that it does contain such causes.
> 
> This should discuss foreign types / mutable types as well.
> 
> Here is some text that you might want to incorporate or modify, or not:
> 
>     In Mercury, type parameter variance is inferred from the type
>     definition. When the definition of a type is hidden or unavailable,
>     as is the case for an abstract type, the only safe conclusion is
>     that its type parameters must be invariant.

Will consider this.

> > + at heading Which types can be coerced to which other types?
> > +
> > +ZZZ The rest is to be done once we agree on what to call this concept,
> > +but the approach I intend to take is
> > +- to view types as trees,
> > +- the non-du parts of the tree must be identical in the from-type and to-type,
> > +- while the du parts need only have a common base type.
> > +  (After the most recent change, we do not require either S =< T nor T =< S;
> > +  we require only S =< B and T =< B.)
> 
> That sounds fine.

Thanks.

> In the manual, I originally used the term "type conversion" instead of
> "coercion", "coercible", etc. "coerce" is more jargony, and obviously
> has a negative connotation outside of a programming context.
> The language uses "coerce" for expressions, since "convert" would be
> too general, and "cast" seemed too suggestive of unsafe/unchecked casts
> in other languages.

Yep, I agree with that.

Thanks for the review.

Zoltan.