[m-rev.] for review: expand the class of allowed coercions

[Peter Wang]

On Thu, 30 Jul 2026 22:35:27 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by Peter.
> 
> I am in two minds about whether the small database built up
> by this diff, mapping type_ctors to the set of their invariant type
> parameters, should be added to the typecheck_info structure, or not.
> 
> On the one hand, adding it to the typecheck_info can prevent
> redundant computations, which can be non-trivial if we ever get
> coercions between types whose definitions are large. (This can
> happen after this diff.)
> 
> On the other hand, expanding typecheck_(sub_)_info imposes a
> cost on all compiler invocations, even the ones that do not involve
> any coercions.
> 
> I am leaning towards leaving things as they are, with a note to
> revisit the issue if and when coerces of large types become
> more commonplace.

Yes, I agree.

> Keep a map from type_ctors to their invariant tparams.
> 
> When comparing the type of an argument of a data constructor
> between the from-type and the to-type, we used to regard any appearance
> of any type_ctor other than the one on the left-hand-side of the
> type definition as requiring any type variable appearing in the type
> as having to be invariant.
> 
> This prevented coercions from e.g. one_or_more(err_spec) to
> one_or_more(diag_spec) despite err_spec being a subtype of diag_spec,
> because this rule applied to the  appearance of list(T) in the type of
> the second arg of the one_or_more data constructor.
> 
> Fix this situation by changing the code that did to allow it to
> test, while gathering the invariant type parameters of the one_or_more/1
> type_ctor, to invoke itself recursively to compute the set of invariant
> type parameters of list/1 as well. In general, we can now look
> arbitrarily deep into type structures, subject to some limitations.
> 
> - The first limitation is that we keep a stack of the type_ctors
>   whose sets of invariant type params is being computed, and use it
>   to return a conservative approximation of the actual result
>   instead of descending into infinite recursion.
> 
> - The second is that we do not keep track of any substitutions
>   of any type parameters. This means that for any type_ctor
>   other than the one at the top level, all we care about is
>   whether it may have any invariant type params; if it may,
>   then we treat *all* its type params as having to be invariant.

Please update the reference manual to reflect the rules.

> The extent, if any, to which these limitations are a problem
> in practice is something we can find out only via experience.
> 
> compiler/typecheck_coerce.m:
>     Make the change described above.
> 
> tests/invalid/coerce_type_error.err_exp:
>     Stop expecting an error message about coercing one_or_mores.
> 
> tests/invalid/coerce_typecheck_eqv_helper_1.m:
>     Change a type definition to give second/2 type_ctor some
>     type parameters that must be invariant. Without this change,
>     the compilation of the coerce_typecheck_eqv test case would have
>     succeeded, which means the test case would "fail to fail".
> 
> tests/invalid/coerce_typecheck_eqv.err_exp:
>     Expect the diagnostics appropriate to the changed test case.

> diff --git a/compiler/typecheck_coerce.m b/compiler/typecheck_coerce.m
> index 9b107f500..0a8370cc6 100644
> --- a/compiler/typecheck_coerce.m
> +++ b/compiler/typecheck_coerce.m
> @@ -138,8 +138,10 @@ typecheck_coerce_in_type_assign(Info, Context, FromVar, ToVar,
>          % NOTE The following block of code has a near-duplicate below
>          % in check_coerce_constraint_if_ready, though the two places differ
>          % in how they handle both resolved and not-yet-resolved constraints.
> +        % XXX Should we make known_type_ctors part of typecheck_info?
>          typecheck_coerce_between_types(TypeTable, TVarSet0,
> -            FromType, ToType, TypeAssign2, TypeAssign3, CoerceFails),
> +            FromType, ToType, TypeAssign2, TypeAssign3,
> +            init_known_type_ctors, _, CoerceFails),

Name the anonymous variable.

> @@ -290,7 +292,8 @@ check_coerce_constraint_if_ready(TypeTable, Coercion0, Action, !TypeAssign) :-
>              % in how they handle both resolved and not-yet-resolved
>              % constraints.
>              typecheck_coerce_between_types(TypeTable, TVarSet0,
> -                FromType, ToType, TypeAssign0, TypeAssign1, CoerceFails),
> +                FromType, ToType, TypeAssign0, TypeAssign1,
> +                init_known_type_ctors, _, CoerceFails),
>              (
>                  CoerceFails = [],
>                  type_assign_get_type_bindings(TypeAssign1, TypeBindings1),

Likewise.

> @@ -356,12 +359,31 @@ coerce_constraint_is_satisfied(Coercion) :-
>  % Part 3.
>  %
>  
> -:- pred typecheck_coerce_between_types(type_table::in, tvarset::in,
> -    mer_type::in, mer_type::in, type_assign::in, type_assign::out,
> +    % The type_ctors that we are currently trying to add to known_type_ctors.
> +    %
> +:- type active_type_ctors == list(type_ctor).
> +
> +    % The set of type_ctors for which we know whether they have any
> +    % type parameters which must be invariant.
> +    %
> +    % XXX A better name than known_type_ctors would be nice.
> +    % Maybe known_invariant_tparam_type_ctors, but it is kind of long.
> +    %
> +:- type known_type_ctors == map(type_ctor, invariant_tvars).
> +
> +:- func init_known_type_ctors = known_type_ctors.
> +
> +init_known_type_ctors = map.init.
> +

type_ctor_invariant_tvars_map or invariant_tvars_map?
Not very short, but more descriptive.

> diff --git a/tests/invalid/coerce_typecheck_eqv.err_exp b/tests/invalid/coerce_typecheck_eqv.err_exp
> index 6542293fe..73670338a 100644
> --- a/tests/invalid/coerce_typecheck_eqv.err_exp
> +++ b/tests/invalid/coerce_typecheck_eqv.err_exp
> @@ -1,3 +1,12 @@
> +coerce_typecheck_eqv.m:030: In clause for predicate `test1'/2:
> +coerce_typecheck_eqv.m:030:   error: cannot coerce `X' from `good(citrus)' to
> +coerce_typecheck_eqv.m:030:   `good(fruit)'.
> +coerce_typecheck_eqv.m:030:   The only parameter of the type constructor
> +coerce_typecheck_eqv.m:030:   `good'/1 must be invariant (meaning that it must
> +coerce_typecheck_eqv.m:030:   be bound to the same type in the coerced-from and
> +coerce_typecheck_eqv.m:030:   coerced-to types) because it occurs in the type
> +coerce_typecheck_eqv.m:030:   of the first argument of the `good'/1 data
> +coerce_typecheck_eqv.m:030:   constructor, which is an abstract type.
>  coerce_typecheck_eqv.m:039: In clause for predicate `test2'/2:
>  coerce_typecheck_eqv.m:039:   error: cannot coerce `X' from `bad(citrus)' to
>  coerce_typecheck_eqv.m:039:   `bad(fruit)'.
> @@ -6,5 +15,4 @@ coerce_typecheck_eqv.m:039:   `bad'/1 must be invariant (meani
>  coerce_typecheck_eqv.m:039:   be bound to the same type in the coerced-from and
>  coerce_typecheck_eqv.m:039:   coerced-to types) because it occurs in the type
>  coerce_typecheck_eqv.m:039:   of the first argument of the `bad'/1 data
> -coerce_typecheck_eqv.m:039:   constructor, which has a type constructor other
> -coerce_typecheck_eqv.m:039:   than `bad'/1, namely `list'/1.
> +coerce_typecheck_eqv.m:039:   constructor, which is an abstract type.

Both test1 and test2 are the same now, which is fine, but good/1
is now "bad" as well.

Actually, test1 should not have been accepted before. Since second(T, U)
is abstract exported, first(int, T) should only have been expanded out
to second(T, int), so T should be an invariant type parameter.
But I guess it is another case of the compiler expanding out
abstract equivalence types when it shouldn't do.

> diff --git a/tests/invalid/coerce_typecheck_eqv_helper_1.m b/tests/invalid/coerce_typecheck_eqv_helper_1.m
> index 868c180ff..4fe2e4b39 100644
> --- a/tests/invalid/coerce_typecheck_eqv_helper_1.m
> +++ b/tests/invalid/coerce_typecheck_eqv_helper_1.m
> @@ -13,4 +13,6 @@
>  
>  :- import_module list.
>  
> -:- type second(T, U) == list(U).
> +:- type second(T, U)
> +    --->    second_base
> +    ;       second_rec(T, second(U, T)).

You should update the comments in coerce_typecheck_eqv.m

Peter