[m-rev.] for post-commit review: report on more kinds of coerce_fails

[Peter Wang]

On Sun, 26 Jul 2026 14:43:57 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by Peter.
> 
> I am requesting feedback on three issues specifically,
> and not just from Peter.
> 
> One issue is that the additional info we include in the diagnostic
> for one new coerce_fail has two quite different versions, with one
> commented out. Which approach do you prefer?
> 

> The second issue is whether coerce diagnostics should refer
> to type variables by number, as they have done before this,
> or by name, as my new additions do. This means that one
> diagnostics now looks like this:
> 
> coerce_unify_tvars.m:063: In clause for predicate `head_type_params'/2:
> coerce_unify_tvars.m:063:   error: cannot coerce `X' from `list.list(V_1)' to
> coerce_unify_tvars.m:063:   `list.list(V_2)'.
> coerce_unify_tvars.m:063:   Type variables such as T2 and T1 cannot be either
> coerce_unify_tvars.m:063:   coerced from, or coerced to.
> 
> It is clear that we should consistently use either names or numbers,
> but which? I would prefer names, even though the source of those names
> is the declaration of the type_ctor involved, not the names used for type
> variables in the predicate in which the error occurs.

I think that could lead to confusion when there are same-named type
variables in the predicate, which doesn't seem unlikely at all.
On the whole, I would stick with the numbers for consistency
with other error messages.

> The third issue is module qualification. We now have this diagnostic:
> 
> coerce_type_error.m:045: In clause for predicate `bad_unrelated'/2:
> coerce_type_error.m:045:   error: cannot coerce `X' from
> coerce_type_error.m:045:   `coerce_type_error.orange_non_fruit' to
> coerce_type_error.m:045:   `coerce_type_error.citrus'.
> coerce_type_error.m:045:   The base type constructor of the coerce-from type is
> coerce_type_error.m:045:   `orange_non_fruit'/0, while for the coerce-to type
> coerce_type_error.m:045:   it is `fruit'/0.
> 
> The initial part includes module qualification, the final part does not.
> 
> I can see three possible approaches.
> 
> - never use module qualification
> - always use module qualification
> - use module qualification only if any module qualification differs
>   between the from-type and the to-type. (Unlike a type_ctor, a full type
>   may contain more than one sym_name.)
> 
> I thin the third option is best in balancing the two concerns of
> 
> - presenting information when it can be helpful
> - not presenting information when it is not useful, but is only clutter.
> 
> What do you think?

That sounds okay.


> Report more kinds of coerce_fail reasons.
> 
> compiler/type_assign.m:
>     Split one coerce_fail into three parts, to simplify the generation
>     of diagnostics that are specialized to their situations.
> 
> compiler/typecheck_errors.m:
>     Generate diagnostics for several coerce_fails, including the new ones.
> 
> compiler/typecheck_coerce.m:
>     Record the new kinds of coerce_fails.
> 
> compiler/typecheck_coerce.m:
> compiler/typecheck_util.m:
>     Move a predicate and its associated types from typecheck_coerce.m
>     to typecheck_util.m to allow the new code in typecheck_errors.m
>     to access it.
> 
> tests/invalid/coerce_type_error.err_exp:
> tests/invalid/coerce_unify_tvars.err_exp:
>     Expect the new diagnostics.

> diff --git a/compiler/typecheck_errors.m b/compiler/typecheck_errors.m
> index 7a577ccc3..dcc16916a 100644
> --- a/compiler/typecheck_errors.m
> +++ b/compiler/typecheck_errors.m
> @@ -229,6 +258,139 @@ describe_coerce_fail(TVarSet, Fail) = Pieces :-
>          Pieces = []
>      ).
>  
> +:- func describe_coerce_fail_different_base_types(tvarset,
> +    mer_type, type_ctor, mer_type, type_ctor) = list(format_piece).
> +
> +describe_coerce_fail_different_base_types(_TVarSet,
> +        _FromType, FromBaseTypeCtor, _ToType, ToBaseTypeCtor) = Pieces :-
> +    FromBaseTypeCtor = type_ctor(FromSymName, _),
> +    ToBaseTypeCtor = type_ctor(ToSymName, _),
> +    % Print the module qualifiers on the type_ctors only if it is relevant.
> +    ( if
> +        FromSymName = qualified(ModuleName, _),
> +        ToSymName = qualified(ModuleName, _)
> +    then
> +        FromBaseCtorPiece = unqual_type_ctor(FromBaseTypeCtor),
> +        ToBaseCtorPiece = unqual_type_ctor(ToBaseTypeCtor)
> +    else
> +        FromBaseCtorPiece = qual_type_ctor(FromBaseTypeCtor),
> +        ToBaseCtorPiece = qual_type_ctor(ToBaseTypeCtor)
> +    ),
> +    Pieces = [words("The base type constructor of the coerce-from type is")] ++
> +        color_as_inconsistent([FromBaseCtorPiece, suffix(",")]) ++
> +        [words("while for the coerce-to type it is")] ++
> +        color_as_inconsistent([ToBaseCtorPiece, suffix(".")]) ++
> +        [nl].
> +% XXX A possible alternative wording.
> +    % FromTypeStr = mercury_type_to_string(TVarSet, print_num_only, FromType),
> +    % ToTypeStr =   mercury_type_to_string(TVarSet, print_num_only, ToType),
> +%   Pieces = [words("You can coerce"),
> +%       words("from one discriminated union type to another"),
> +%       words("only if they have the same base type constructor,"),
> +%       words("meaning that following the chain of supertypes from both"),
> +%       % XXX Should this be included?
> +%       % words("the from-type and the to-type"),
> +%       words("ends up at the same type constructor."),
> +%       words("In this case, the base type constructor of the from-type")] ++
> +%       color_as_subject([words(FromTypeStr)]) ++
> +%       [words("is")] ++
> +%       color_as_inconsistent([FromBaseCtorPiece, suffix(",")]) ++
> +%       [words("while the base type constructor of the to-type")] ++
> +%       color_as_subject([words(ToTypeStr)]) ++
> +%       [words("is")] ++
> +%       color_as_inconsistent([ToBaseCtorPiece, suffix(".")]) ++
> +%       [nl].

I played around with the wording and ended up with:

    You can only coerce between discriminated union types that have the
    same base type constructor. This expression attempts to convert
    [coerce] a value from a type with base type constructor X to a type
    with base type constructor Y.

>  coerce_type_error.m:070: In clause for predicate `bad_phantom'/2:
>  coerce_type_error.m:070:   error: cannot coerce `X' from
>  coerce_type_error.m:070:   `coerce_type_error.phantom(int)' to
>  coerce_type_error.m:070:   `coerce_type_error.phantom(float)'.
> +coerce_type_error.m:070:   Builtin types such as float and int cannot be either
> +coerce_type_error.m:070:   coerced from, or coerced to.
>  coerce_type_error.m:091: In clause for predicate `bad_higher_order'/2:
>  coerce_type_error.m:091:   error: cannot coerce `X' from
>  coerce_type_error.m:091:   `coerce_type_error.wrap_ho(coerce_type_error.citrus)'

Hmm, while it is true that you cannot coerce builtin types,
that isn't happening in this case.

Technically, a coercion from phantom(int) to phantom(float) would be
sound, so we could allow it. We would need to introduce an exemption to
the rule that requires type parameters to be equal or in a subtype
relationship, if the type parameters are unused in the body of the base
type constructor.

> diff --git a/tests/invalid/coerce_unify_tvars.err_exp b/tests/invalid/coerce_unify_tvars.err_exp
> index 7e3294902..ef2d295c2 100644
> --- a/tests/invalid/coerce_unify_tvars.err_exp
> +++ b/tests/invalid/coerce_unify_tvars.err_exp
> @@ -1,3 +1,5 @@
>  coerce_unify_tvars.m:063: In clause for predicate `head_type_params'/2:
>  coerce_unify_tvars.m:063:   error: cannot coerce `X' from `list.list(V_1)' to
>  coerce_unify_tvars.m:063:   `list.list(V_2)'.
> +coerce_unify_tvars.m:063:   Type variables such as T2 and T1 cannot be either
> +coerce_unify_tvars.m:063:   coerced from, or coerced to.

Suggestion:

    The coercion is invalid because the unconstrained type variables V_1
    and V_2 are not known to be equal or to have a subtype relationship.

Peter