[m-rev.] for review: Require subtypes to repeat existential type vars and constraints exactly.

[Zoltan Somogyi]

On 2024-07-08 16:20 +10:00 AEST, "Peter Wang" <novalazy at gmail.com> wrote:

> compiler/add_type.m:
>     Check the new rules. Unlike before, we first check the conditions on
>     existential type vars and existential class constraints before
>     checking the types of constructor arguments.
> 
> compiler/prog_data.m:
>     Fix a comment.
> 
> tests/invalid/subtype_exist_vars.m:
> tests/invalid/subtype_exist_vars.err_exp:
> tests/invalid/subtype_exist_constraints.m:
> tests/invalid/subtype_exist_constraints.err_exp:
>     Extend test cases.
> 
> tests/invalid/subtype_exist_constraints.err_exp:
>     Update expected output.
> 
> NEWS.md:
>     Announce change to the language.
> ---
>  NEWS.md                                       |   4 +
>  compiler/add_type.m                           | 331 +++++++++---------
>  compiler/prog_data.m                          |   4 +-
>  doc/reference_manual.texi                     |  18 +-
>  .../invalid/subtype_exist_constraints.err_exp |  10 +-
>  tests/invalid/subtype_exist_constraints.m     |  12 +
>  tests/invalid/subtype_exist_vars.err_exp      |  40 ++-
>  tests/invalid/subtype_exist_vars.m            |  12 +-
>  8 files changed, 244 insertions(+), 187 deletions(-)
> 
> diff --git a/NEWS.md b/NEWS.md
> index af466fb02..f740d7b2a 100644
> --- a/NEWS.md
> +++ b/NEWS.md
> @@ -1226,6 +1226,10 @@ Changes to the Mercury language
>  * You can now use the escape sequence '\e' to refer to the ESC (escape)
>    character, just as you can use '\n' to refer to the newline character.
>  
> +* Existentially quantified type variables and existential class constraints
> +  in a subtype definition now must be listed in the same order as in the
> +  supertype definition.

To be pedantic, the compiler *already* required all that. It's just the form
of its disapproval for violations was not an error message, but the generation
of code that would cause a core dump :-(

I would reword the above to avoid giving the impression that this is a
*totally* new requirement.

> diff --git a/compiler/add_type.m b/compiler/add_type.m
> index 3cc665754..e95a08cde 100644
> --- a/compiler/add_type.m
> +++ b/compiler/add_type.m

> -:- pred check_subtype_ctor_arg(type_table::in, tvarset::in, type_status::in,
> -    sym_name::in,
> +:- pred check_subtype_ctor_exist_constraints(sym_name_arity::in,
> +    prog_context::in,
>      maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
> -    constructor_arg::in, constructor_arg::in,
> -    int::in, int::out, existq_tvar_mapping::in, existq_tvar_mapping::out,
> +    maybe(existq_tvar_mapping)::out,
> +    list(error_spec)::in, list(error_spec)::out) is det.
> +
> +check_subtype_ctor_exist_constraints(CtorSymNameArity, Context,
> +        MaybeExistConstraints, MaybeSuperExistConstraints, Result, !Specs) :-
> +    (
> +        MaybeExistConstraints = no_exist_constraints,
> +        ExistQVars = [],
> +        Constraints = []
> +    ;
> +        MaybeExistConstraints = exist_constraints(ExistConstraints),
> +        ExistConstraints = cons_exist_constraints(ExistQVars, Constraints, _, _)
> +    ),
> +    (
> +        MaybeSuperExistConstraints = no_exist_constraints,
> +        SuperExistQVars = [],
> +        SuperConstraints = []
> +    ;
> +        MaybeSuperExistConstraints = exist_constraints(SuperExistConstraints),
> +        SuperExistConstraints = cons_exist_constraints(SuperExistQVars,
> +            SuperConstraints, _, _)
> +    ),
> +    list.length(ExistQVars, NumExistQVars),
> +    list.length(SuperExistQVars, NumSuperExistQVars),
> +    ( if NumExistQVars = NumSuperExistQVars then
> +        ( if
> +            list.foldl_corresponding(build_existq_tvars_mapping,
> +                ExistQVars, SuperExistQVars, bimap.init, ExistQVarsMapping)
> +        then
> +            check_subtype_ctor_exist_constraints(CtorSymNameArity, Context,
> +                ExistQVarsMapping, Constraints, SuperConstraints,
> +                ConstraintsOk, !Specs),
> +            (
> +                ConstraintsOk = yes,
> +                Result = yes(ExistQVarsMapping)
> +            ;
> +                ConstraintsOk = no,
> +                Result = no
> +            )
> +        else
> +            Pieces =
> +                [words("Error: existentially quantified type variables"),
> +                words("for")] ++
> +                color_as_subject([unqual_sym_name_arity(CtorSymNameArity)]) ++
> +                color_as_incorrect([words("do not correspond")]) ++
> +                [words("one-to-one in the subtype and supertype."), nl],
> +            Spec = spec($pred, severity_error, phase_pt2h, Context, Pieces),
> +            !:Specs = [Spec | !.Specs],
> +            Result = no
> +        )
> +    else
> +        Pieces = [words("Error:")] ++
> +            color_as_subject([unqual_sym_name_arity(CtorSymNameArity)]) ++
> +            [words("has wrong number of"),
> +            words("existentially quantified type variables"), prefix("(")] ++
> +            color_as_incorrect([int_fixed(NumExistQVars)]) ++
> +            [suffix(","), words("expected")] ++
> +            color_as_correct([int_fixed(NumSuperExistQVars)]) ++
> +            [suffix(")."), nl],
> +        Spec = spec($pred, severity_error, phase_pt2h, Context, Pieces),
> +        !:Specs = [Spec | !.Specs],
> +        Result = no
> +    ).

Your predicates here return their success/failure indications separately
from the error_specs reporting the failures. In most parts of the compiler,
it is preferable to return them together, using the maybeN family of types
in compiler/maybe_error.m. We make an exception for compiler components
that are performance critical, where the allocation of the okN or errorN wrappers
may contribute to a bottleneck, but subtype checking is never going to be
such a bottleneck.

> +:- pred build_existq_tvars_mapping(tvar::in, tvar::in,
> +    existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
> +
> +build_existq_tvars_mapping(VarA, VarB, !ExistQVarsMapping) :-
> +    ( if bimap.insert(VarB, VarA, !ExistQVarsMapping) then
> +        true
> +    else
> +        % The reference manual does not require distinct type variables in a
> +        % existential quantifier list of a constructor definition (whether or
> +        % not a du type is a subtype). This might be an oversight.

I don't think it "might be"; like you, I think it *is* an oversight. It should be fixed,
though probably in a separate diff.

> +        % For now, this allows duplicate variables in subtype constructor
> +        % definitions as well.
> +        bimap.forward_search(!.ExistQVarsMapping, VarB, VarA)
> +    ).

I would make this a det predicate that either updates the mapping
or adds an error_spec giving all three variables involved to a list.
If you can't map A to B, it can bebecause either A is already mapped to C,
a clash in the forward map, or because C is already mapped to B, a clash
in the reverse map. Users need to know which.

This error message would requiring in the tvarsets of both the subtype
and the supertype, and would be easier with separate forward and reverse maps.

> +:- pred check_subtype_ctor_exist_constraints(sym_name_arity::in,
> +    prog_context::in, existq_tvar_mapping::in,
> +    list(prog_constraint)::in, list(prog_constraint)::in, bool::out,
> +    list(error_spec)::in, list(error_spec)::out) is det.
> +
> +check_subtype_ctor_exist_constraints(CtorSymNameArity, Context,
> +        ExistQVarsMapping, Constraints, SuperConstraints0, Result, !Specs) :-
> +    ExistQVarsRenaming = bimap.forward_map(ExistQVarsMapping),
> +    apply_variable_renaming_to_prog_constraint_list(ExistQVarsRenaming,
> +        SuperConstraints0, SuperConstraints),
> +    ( if Constraints = SuperConstraints then
> +        Result = yes
> +    else
> +        Pieces0 = [words("Error: existential class constraints for")] ++
> +            color_as_subject([unqual_sym_name_arity(CtorSymNameArity)]) ++
> +            color_as_incorrect([words("differ")]),
> +        list.sort(Constraints, SortedConstraints),
> +        list.sort(SuperConstraints, SortedSuperConstraints),
> +        ( if SortedConstraints = SortedSuperConstraints then
> +            Pieces = Pieces0 ++
> +                [words("in order in the subtype and supertype."), nl]
> +        else
> +            Pieces = Pieces0 ++
> +                [words("in the subtype and supertype."), nl]
> +        ),

I would add "Expected <constraint from supertype>, got <constraint from subtype>"

> +subtype_exist_vars.m:021: Error: `orange'/1 has wrong number of existentially
> +subtype_exist_vars.m:021:   quantified type variables (0, expected 1).

In similar error messages, we use the template "expected X, got Y".
I think this message should follow that template as well.

> +subtype_exist_vars.m:045: Error: existentially quantified type variables for
> +subtype_exist_vars.m:045:   `nondistinct'/2 do not correspond one-to-one in the
> +subtype_exist_vars.m:045:   subtype and supertype.

As I mentioned above, this diagnostic could use more info.
If you don't want to do it, say so, and I will do it in a few days.

The diff is otherwise fine.

Zoltan.