[m-dev.] two questions about coercions

[Zoltan Somogyi]

On Mon, 3 Aug 2026 15:52:18 +1000, Peter Wang <novalazy at gmail.com> wrote:
> > 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.

That's what I expected, but I wasn't sure.

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

When types_compare_as_given is invoked with compare_equal_lt on two
du types, the call now goes through defined_types_compare_as_given
(which checks if the two type_ctors match) to du_types_compare_as_given.
This replaces TypeA with its lifted version, SuperTypeA, and invokes
types_compare_as_given recursively. The recursion can end successfully
only if TypeB's type_ctor is either TypeA's type_ctor, or TypeA's supertype's
type_ctor, or TypeA's supertype's supertype's type_ctor, and so on.

When are_actual_param_type_pair_as_related_as_needed switches the
roles of TypeA and TypeB, the same thing happens. Neither invocation
of types_compare_as_given from there will work if TypeA and TypeB have
the same base type, but neither is direcly on the path from the other type to
its base type.

That is what I noticed when trying to generate the symmetric error message
you wanted. I found it odd, hence the question.

Given your answers, I believe I know how to proceed. Thank you.

Zoltan.