[m-rev.] for review: symmetric coerce_fails for unrelated du types

[Peter Wang]

On Tue, 04 Aug 2026 01:59:37 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by Peter. Note: this diff is what I wanted those two
> questions answered for.
> 
> Zoltan.

> Use {must_be,need_not_be}_invariant comparisons.
> 
> compiler/typecheck_coerce.m:
>     Stop trying to check both FromType =< ToType and ToType =< FromType.
>     Instead, compare them just once,
> 
>     To make this work, when comparing two du types, don't try to lift
>     just one type towards its base type; lift *both*.
> 
>     Add an XXX about a possible improvement.
> 
> compiler/type_assign.m:
>     Change the representation of the failure of comparing two du types
>     to reflect the now-symmetric nature of the failure.
> 
> compiler/typecheck_errors.m:
>     Generate a symmetric message for this new symmetric failure.
> 
>     Since we no longer generate the repeated-in-mirror-image-form
>     coerce_fails involving at least one non-du type, stop trying
>     to get rid of them.
> 
>     Fix a typo in a the diagnostic for a (so far untested) coerce_fail.
> 
> tests/invalid/coerce_type_error.err_exp:
>     Expect the new symmetric diagnostic for unrelated-by-subtyping
>     du types.

> diff --git a/compiler/typecheck_coerce.m b/compiler/typecheck_coerce.m
> index cca6377c4..62b0c9582 100644
> --- a/compiler/typecheck_coerce.m
> +++ b/compiler/typecheck_coerce.m

>  du_types_compare_as_given(TypeTable, TVarSet, BaseTypeCtor, ArgNum, Comparison,
> -        TypeA, TypeCtorA, ArgTypesA, DuTypeInfoA,
> -        TypeB, _TypeCtorB, _ArgTypesB, _DuTypeInfoB,
> +        TypeA, DuTypeInfoA, TypeB, DuTypeInfoB,
>          !TypeAssign, !CoerceFails) :-
>      (
> -        Comparison = compare_equal(Reason),
> -        CoerceFail = should_be_invariant_arg(BaseTypeCtor,
> -            ArgNum, Reason, TypeA, TypeB),
> +        Comparison = must_be_invariant(Reason),
> +        % Even if TypeA and/or TypeB contain type variables,
> +        % no possible types being bound to those variables
> +        % can fix the mismatch between TypeCtorA amd TypeCtorB.

and

> +        CoerceFail = should_be_invariant_arg(BaseTypeCtor, ArgNum,
> +            Reason, TypeA, TypeB),
>          !:CoerceFails = [CoerceFail | !.CoerceFails]
>      ;
> -        Comparison = compare_equal_lt,
> -        DuTypeInfoA = du_type_info(_, _, TypeDefnA, TypeBodyDuA),
> -        MaybeSuperTypeA = TypeBodyDuA ^ du_type_supertype,
> -        (
> -            MaybeSuperTypeA = subtype_of(SuperTypeA0),
> -            get_supertype_of_subtype(TVarSet,
> -                TypeCtorA, ArgTypesA, TypeDefnA,
> -                SuperTypeA0, SuperTypeA),
> -            types_compare_as_given(TypeTable, TVarSet,
> +        Comparison = need_not_be_invariant,
> +        % XXX If TypeA and TypeB have a common "ancestor" that is
> +        % NOT their common supertype, we could use the nearest
> +        % such common ancestor instead of the base type.
> +        % This would allow us to check the coercability of
> +        % any phantom type parameters that don't make it
> +        % all the way up to the common base type.

(If we decide we want to allow that after all.)

That looks fine.

Peter