[m-rev.] for review: infrastructure for diagnosing coerce failures

[Peter Wang]

On Sun, 19 Jul 2026 21:43:10 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by Peter.
> 
> Peter, would you object if I move the test for both from-type and to-type
> being du types up the call chain as far as it is possible to move them?
> I think it could simplify both the main checking code and the error handling.

Ok.

> 
> I think it would also simplify the next change I would like to make.
> At the moment, if you can coerce from a subtype tsub to its sypertype t, then
> 
> - you can coerce from list(tsub) to list(t), but
> - you cannot coerce from one_or_more(tsub) to one_or_more(t).
> 
> This violates the law of least astonishment: why can you coerce list(tsub)
> when it occurs on its own, but not when it occurs as a functor arg?
> 
> The cause is that acc_invariant_tvars_in_ctor_rhs_type treats a functor arg
> whose type_ctor/type_param list is the same as the type_ctor/type_param list
> of whole term (such as the second arg of [|]) differently from a functor arg
> for which is not true (such as the second arg of one_or_more).
> 
> I would propose that when TypeCtor != BaseTypeCtor, the
> acc_invariant_tvars_in_ctor_rhs_type predicate should be allow to descend
> into the definition of Typector, provided that TypeCtor is 
> 
> (a) a du type and
> (b) not on the stack of BaseTypeCtor/BaseTypeParam pairs that
> the current call's ancestors were invoked with.
> 
> This would go with the generalization of TypeCtor = BaseTypeCtor test
> to a test that checks whether TypeCtor appear in that stack of pairs,
> with ArgTypes being tested against the matching BaseTypeParams.
> 
> Can you see any reason why this wouldn't work?

I don't see why it wouldn't work.

The current rule is quite conservative. Since du type definitions don't
declare the variance of their type parameters upfront, the idea was to
keep the type parameter invariance rules to be (mostly) self contained,
so it can be determined, by looking at where the a type parameter
appears in the type definition, and not much beyond that, whether the
type parameter must be invariant. The alternative, as in your
suggestion, requires more non-local reasoning. (Of course, in practice,
users will not really think about type variance until the compiler
reports an error.)

The other problem I wanted to avoid is that a change to a type definition
could potentially affect the variance of a type parameter of some other
type, far away. Maybe not a big problem in practice.

> Do you know of any research relevant to this issue?

I don't know of any languages with the same idea of "subtypes" as
Mercury. I would look at how other languages handle type variance.
https://en.wikipedia.org/wiki/Type_variance

The diff looks fine.

Peter