[m-dev.] two questions about coercions

[Peter Wang]

On Sat, 01 Aug 2026 22:08:03 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> In the process of thinking about how to generate good diagnostics
> for coerce failures for unrelated types, I was exploring whether
> we can avoid comparing FromType and ToType twice: once for
> FromType =< ToType, and once for ToType =< FromType.
> The answer is that yes, for all types that contain no du types,
> those two tests will always yield the same result: if FromType
> and ToType can be made identical by applying a substitution
> to any type variables in them, then they are equal, otherwise,
> they are not comparable.
> 
> This means that the two values of the types_comparison type
> should be not so much compare_equal and compare_equal_lt,
> but must_be_invariant and need_not_be_invariant, or we could
> call them must_be_equal and must_be_only_comparable.
> Considering what happens when we compare lists of arguments
> of a du type_ctor in this way then raises a question, for which
> I introduce an example.
> 

> Suppose type tf is a subtype of type t, and foo/2 is a type constructor,
> and neither of its type parameters must be invariant. When we are
> coercing from foo(tf, t) to foo(t, tf). The common base type is of course foo,
> and are_actual_param_type_pairs_as_related_as_needed allows
> the types bound to its two parameters to be related differently.
> Meaning that it allows the from-type's first arg, tf, to be the subtype
> of the to-type's first arg, t, while the subtype relationship goes
> in the other direction for the two second args. However, this
> "direction change" cannot happen *inside* each parameter of foo.

> For example, coercing foo(assoc_list(tf, t), int) to foo(assoc_list(t, tf), int)
> will not be allowed by types_compare_as_given, because neither
> assoc_list(tf, t) =< assoc_list(t, tf) nor its reverse hold.
> 
> My first question is: is this required either by theory, or by our implementation
> (maybe by modecheck_coerce.m), or by neither?
> 

No, the coercion could be allowed in theory. The reason coerce can allow
both upcasts and downcasts is that we rely on the mode system to check
which downcasts are safe. That should apply deeper within a term as well.

> The example for the second issue is this set of subtype relationships:
> 
> :- type base ---> ...
> 
> :- type sub1 =< base ---> ...
> 
> :- type sub2 =< base ---> ...
> 
> At the top level, we require the from-type and to-type to have the same
> base type, which sub1 and sub2 have. However, types_compare_as_given,
> when given two types whose type_ctors are sub1 and sub2, will fail
> even with compare_equal_lt, because neither is a subtype of the other.
> 
> My second question is therefore: is this requied by theory, by our implementation,
> or neither? Or is there some reason why the situation I am asking about
> cannot arise, given the shared base type of the from-type and to-type?

The coercion from sub1 to sub2 is allowed given the shared base type.
Do you have an example where it is not?

Peter