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

[Peter Wang]

On Mon, 08 Jul 2024 16:56:51 +1000 "Zoltan Somogyi" <zoltan.somogyi at runbox.com> wrote:
> 
> On 2024-07-08 16:20 +10:00 AEST, "Peter Wang" <novalazy at gmail.com> wrote:
> > 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.
> 

I suppose. I've reworded the announcement, and moved it to the
"Changes to the Mercury compiler" section.

> > 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
...
> 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.

Changed.

> > +:- 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.
> 

Right.

> > +        % 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.
> 

Left it for now.

> > +:- 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>"
> 

This seems like a fairly big change. At least it would take me a while.
Left a comment.

> > +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.
> 

Changed.

> > +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.

I'll leave it to you.

Thanks for the review.

Peter