[m-dev.] two questions about coercions

[Zoltan Somogyi]

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?

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?

Zoltan.