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

[Peter Wang]

On Tue, 04 Aug 2026 23:39:01 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by both Peter and Julien. This draft is almost complete,
> the only part missing is the part after the new "Which types can be
> coerced to which other types?" heading, for which we need to agree
> a name first. The idea is that this concept describes what the predicate
> types_compare_as_given implements with need_not_be_invariant.
> 
> Zoltan.

> diff --git a/doc/mercury_reference_manual.texi b/doc/mercury_reference_manual.texi
> index ebed23b19..0ae5fb1a4 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 = 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

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

> + at noindent
> +3. For all other types,
> + at samp{S =< T} if and only if @samp{S = T},
> +i.e.@: they are syntactically identical.
> +
> +Note that this last category includes higher order types.
> +If @samp{S} and @samp{T} are both higher order types, then
> + at samp{S =< T} can hold only if
> +
> + at itemize @minus
> + at item
> + at samp{S} and @samp{T} are either
> +both @samp{pred} types, or both @samp{func} types,
> + at item
> +they have the same arity,
> + at item
> + 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".

>      @item
> -    they have the same arity,
> -    @item
> -    @var{P} and @var{Q} have the same argument types
> -    (the current implementation does not allow subtyping
> -    in higher-order arguments), and
> -    @item
> -    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,
> -    i.e.@: their higher-order inst information must specify
> +    both @samp{S} and @samp{T} have the same higher-order inst information,
> +    meaning that they both specify
>      the same argument modes, determinism, and purity.
>      @end itemize
>  @end itemize

>  
> - at noindent
> -4. For all other types,
> - at samp{S =< T} if and only if @samp{S = T},
> -i.e.@: they are syntactically identical.
> +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".

> +However, in Mercury, an argument of a predicate
> +can be an input in one mode and an output in another mode.
> +Requiring all arguments to be invariant
> +is the simplest way for the Mercury typechecker
> +to handle the fact that in many cases,
> +it will not have access to such mode information.

> @@ -8507,50 +8641,243 @@ good_example3_univ("bar"::in(bound("bar")), univ("blah")::out).
>  @node Type conversions
>  @chapter Type conversions
>  
> -(This is a new and experimental feature, subject to change.)
> +(This is a relatively new feature, and is subject to change.)
>  
> -A term may be converted from one type @var{FromType}
> -to another type @var{ToType}
> +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

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

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

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

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

> +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: ...

> + 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"?

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

> + 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

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

> + at itemize @minus
> + at item
> +the input and output arguments of predicates and functions
> +have opposite variance requirements
> +(inputs must be contravariant while outputs must be covariant);
> + at item
> +without guaranteed access to mode information,
> +the Mercury typechecker must require all arguments to meet
> +both requirements at the same time; and
> + at item
> +the only way to do so is to require all arguments to be invariant.
> + at end itemize

> +
> +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 ;)
I don't have a suggestion at this time.

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

> +
> +The reason for the third bullet point is to allow coercions to happen

Suggestion: s/allow coercions to happen/allow a type conversion/

> +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".

> +(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

> + at example
> +:- type list(T)
> +    --->    []                  % nil
> +    ;       [T | list(T)].      % cons(T, list(T))
> + at end example
> +
> +This rule means that the @samp{one_or_more} type's one parameter
> +also does not need to be invariant:
> + at example
> +:- type one_or_more(T)
> +    --->    one_or_more(T, list(T)).
> + at end example
> +

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

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

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

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.

Peter