[m-rev.] for review: diagnose errors involving invariant tvars

[Peter Wang]

On Wed, 29 Jul 2026 12:18:12 +0200 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> For review by Peter.
> 
> Zoltan.

> Explain the requirement for invariant type params ...
> 
> ... in the diagnostic when a coerce operation fails.
> 
> compiler/type_assign.m:
>     Add slots to the representation of the should_be_invariant_arg
>     coerce_fail with an explanation of *why* a type parameter
>     should be the same in the from-type and the to-type.
> 
> compiler/typecheck_coerce.m:
>     Record such reasons when computing which type params should be
>     invaraint, and use those recorded reasons when filling in
>     the new slots.
> 
> compiler/typecheck_errors.m:
>     Generate explanations from the values in those slots.
> 
> tests/invalid/coerce_type_error.{m,err_exp}:
>     Expand this test case, and expect updated diagnostics.
> 
> tests/invalid/Mercury.options:
>     Specify --no-intermod-opt for the coerce_type_error test case.
> 
> tests/invalid/coerce_typecheck_eqv.err_exp:
>     Expect an updated diagnostic.

> diff --git a/compiler/typecheck_coerce.m b/compiler/typecheck_coerce.m
> index 303afeb29..78e890b05 100644
> --- a/compiler/typecheck_coerce.m
> +++ b/compiler/typecheck_coerce.m
...
> +    ;
> +        Reason = ir_base_type_ctor(OoMCtorArgPosns),
> +        BaseTypeCtor = type_ctor(_, BaseTypeCtorArity),
> +        ( if
> +            BaseTypeCtorArity = 1,
> +            ArgNum = 1u
> +        then
> +            ArgNumPieces = [words("only parameter")]

I think "only" could be removed, but keep it if you like.

> +        else
> +            ArgNumPieces = [unth_fixed(ArgNum), words("parameter")]
> +        ),
> +        FrontPieces = [words("The")] ++ ArgNumPieces ++
> +            [words("of the type constructor"), unqual_type_ctor(BaseTypeCtor),
> +            words("must be")] ++ color_as_correct([words("invariant,")]) ++
> +            [words("meaning that it must be bound to the same type"),
> +            words("in the coerced-from and coerced-to types.")],
> +        OoMCtorArgPosns = one_or_more(HeadCtorArgPosn, TailCtorArgPosns),
> +        HeadCtorArgPosnPieces = ctor_arg_posn_to_pieces(HeadCtorArgPosn),
> +        (
> +            TailCtorArgPosns = [],
> +            Pieces = FrontPieces ++
> +                [words("The reason for this is that"),
> +                words("this type parameter occurs in")] ++
> +                HeadCtorArgPosnPieces ++ [suffix("."), nl]

Consider shortening that to:

    This is because the type parameter occurs in ...

    This is because it appears in ...

Use a colon to remove "meaning that"?

    The parameter of the type constructor `one_or_more'/1 must be
    invariant: it must be bound to the same type in the coerced-from and
    coerced-to types. This is because it occurs in the type of the
    second argument of the `one_or_more'/2 data constructor, which has a
    type constructor other than `one_or_more'/1, namely `list'/1.

Or use parentheses to make it a single sentence?

    The parameter of the type constructor `one_or_more'/1 must be
    invariant (it must be bound to the same type in the coerced-from and
    coerced-to types) because it occurs in the type of the second
    argument of the `one_or_more'/2 data constructor,
    which has a type constructor other than
    `one_or_more'/1, namely `list'/1.

> +        ;
> +            TailCtorArgPosns = [_ | _],
> +            TailCtorArgPosnPieces =
> +                list.map(ctor_arg_posn_to_pieces, TailCtorArgPosns),
> +            CtorArgPosnPiecesLists =
> +                [HeadCtorArgPosnPieces | TailCtorArgPosnPieces],
> +            list.intersperse_list_last([[suffix(","), nl]],
> +                [[suffix(","), words("and"), nl]], CtorArgPosnPiecesLists,
> +                AllCtorArgPosnPiecesLists),
> +            list.condense(AllCtorArgPosnPiecesLists, AllCtorArgPosnPieces),
> +            Pieces = FrontPieces ++
> +                [words("The reasons for this are that"),
> +                words("this type parameter occurs in")] ++
> +                [nl_indent_delta(1)] ++
> +                AllCtorArgPosnPieces ++
> +                [suffix("."), nl_indent_delta(-1)]
> +        )
> +    ).
> +

Same here.

> +:- func ctor_arg_posn_to_pieces(ctor_arg_posn) = list(format_piece).
> +
> +ctor_arg_posn_to_pieces(CtorArgPosn) = Pieces :-
> +    CtorArgPosn = ctor_arg_posn(DuOrTupleConsId, ArgNum, PosnReason),
> +    Pieces = [words("the type of the"),
> +        unth_fixed(ArgNum), words("argument of the"),
> +        unqual_cons_id_and_maybe_arity(coerce(DuOrTupleConsId)),
> +        % XXX Should we s/data constructor/functionl symbol/?
> +        words("data constructor, which")] ++
> +        posn_invariant_reason_to_pieces(PosnReason).

(function symbol)

I think "data constructor" works better, as in this message:

    The only parameter of the type constructor
    `wrap_ho'/1 must be invariant, meaning that it must
    be bound to the same type in the coerced-from and
    coerced-to types. The reason for this is that this
    type parameter occurs in the type of the first
    argument of the `wrap_ho'/1 data constructor, which
    is a higher order type.

The message already uses "type constructor", so no reason not to use
"data constructor". Since the type constructor and data constructor have
the same function symbol (as would commonly be the case),
the specificity helps.

> +:- func posn_invariant_reason_to_pieces(posn_invariant_reason)
> +    = list(format_piece).
> +
> +posn_invariant_reason_to_pieces(PosnReason) = Pieces :-
> +    % XXX These should be color_as_incorrect, but to be consistent,
> +    % we could need the color to include any comma suffix.
> +    (
> +        PosnReason = pir_du_nonrec(BaseTypeCtor, TypeCtor),
> +        ( if BaseTypeCtor = TypeCtor then
> +            Pieces = [words("applies the base type constructor"),
> +                unqual_type_ctor(BaseTypeCtor),
> +                % XXX Should we s/different/nonrecursive/?
> +                words("to a different list of type parameters")]

Keep it as "different".

That looks good.

Peter