[m-rev.] for review: Require subtypes to repeat existential type vars and constraints exactly.
Peter Wang
novalazy at gmail.com
Mon Jul 8 16:20:59 AEST 2024
We required a one-to-one mapping from the existentially quantified type
variables for a subtype constructor to those of the supertype. However,
the _order_ that existentially quantified type variables and existential
class constraints are listed in a du constructor definition is reflected
in the order of type_info and type_class_info arguments in a heap cell,
e.g.
:- type pair1
---> some [A, B] pair(A, B).
:- type pair2 =< pair1
---> some [B, A] pair(A, B).
A heap cell representing the term pair(1, "two") of type pair1 would
have type_info arguments in the order [int, string],
whereas a heap cell representing the same term of type pair2 would
have type_info arguments in the opposite order [string, int].
Similarly for existential class constraints.
For safe conversion between a subtype and supertype, all type_info and
type_class_info arguments must be in the same order in the heap cell.
This change tightens subtype definitions, requiring that existentially
quantified type variables for a subtype constructor and any existential
class constraints, be repeated in the same order as in the supertype
constructor definition.
doc/reference_manual.texi:
Document the new rules.
Add a XXX about a dubious language feature.
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.
+
Changes to the Mercury compiler
-------------------------------
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
@@ -1696,64 +1696,163 @@ check_subtype_ctor(TypeTable, TVarSet, TypeStatus, Ctor, SuperCtor,
Ctor = ctor(_, MaybeExistConstraints, CtorSymName, Args, Arity, Context),
SuperCtor = ctor(_, MaybeSuperExistConstraints, _SuperCtorName, SuperArgs,
_SuperArity, _SuperContext),
- list.foldl4_corresponding(
- check_subtype_ctor_arg(TypeTable, TVarSet, TypeStatus,
- CtorSymName, MaybeExistConstraints, MaybeSuperExistConstraints),
- Args, SuperArgs,
- 1, _, bimap.init, ExistQVarsMapping,
- did_not_find_invalid_type, FoundInvalidType, !Specs),
+ CtorSymNameArity = sym_name_arity(CtorSymName, Arity),
+ check_subtype_ctor_exist_constraints(CtorSymNameArity, Context,
+ MaybeExistConstraints, MaybeSuperExistConstraints,
+ MaybeExistQVarsMapping, !Specs),
(
- FoundInvalidType = did_not_find_invalid_type,
+ MaybeExistQVarsMapping = yes(ExistQVarsMapping),
+ list.foldl3_corresponding(
+ check_subtype_ctor_arg(TypeTable, TVarSet, TypeStatus,
+ CtorSymName, ExistQVarsMapping),
+ Args, SuperArgs,
+ 1, _, did_not_find_invalid_type, FoundInvalidType, !Specs),
(
- MaybeExistConstraints = no_exist_constraints,
- MaybeSuperExistConstraints = no_exist_constraints
+ FoundInvalidType = did_not_find_invalid_type
;
- MaybeExistConstraints = exist_constraints(Constraints),
- MaybeSuperExistConstraints = exist_constraints(SuperConstraints),
- CtorSymNameArity = sym_name_arity(CtorSymName, Arity),
- check_subtype_ctor_exist_constraints(CtorSymNameArity,
- Constraints, SuperConstraints, ExistQVarsMapping, Context,
- !FoundInvalidType, !Specs)
- ;
- MaybeExistConstraints = no_exist_constraints,
- MaybeSuperExistConstraints = exist_constraints(_),
- unexpected($pred, "exist_constraints mismatch")
- ;
- MaybeExistConstraints = exist_constraints(_),
- MaybeSuperExistConstraints = no_exist_constraints,
- unexpected($pred, "exist_constraints mismatch")
+ FoundInvalidType = found_invalid_type,
+ !:FoundInvalidType = FoundInvalidType
)
;
- FoundInvalidType = found_invalid_type,
- !:FoundInvalidType = FoundInvalidType
+ MaybeExistQVarsMapping = no,
+ !:FoundInvalidType = found_invalid_type
).
%---------------------%
- % A map from existential type variable in the supertype constructor
+ % A map from an existential type variable in the supertype constructor
% to an existential type variable in the subtype constructor.
%
:- type existq_tvar_mapping == bimap(tvar, tvar).
-:- 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
+ ).
+
+:- 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.
+ % For now, this allows duplicate variables in subtype constructor
+ % definitions as well.
+ bimap.forward_search(!.ExistQVarsMapping, VarB, VarA)
+ ).
+
+:- 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]
+ ),
+ Spec = spec($pred, severity_error, phase_pt2h, Context, Pieces),
+ !:Specs = [Spec | !.Specs],
+ Result = no
+ ).
+
+%---------------------%
+
+:- pred check_subtype_ctor_arg(type_table::in, tvarset::in, type_status::in,
+ sym_name::in, existq_tvar_mapping::in,
+ constructor_arg::in, constructor_arg::in, int::in, int::out,
found_invalid_type::in, found_invalid_type::out,
list(error_spec)::in, list(error_spec)::out) is det.
check_subtype_ctor_arg(TypeTable, TVarSet, OrigTypeStatus, CtorSymName,
- MaybeExistConstraints, MaybeSuperExistConstraints,
- CtorArg, SuperCtorArg,
- ArgNum, ArgNum + 1, !ExistQVarsMapping, !FoundInvalidType, !Specs) :-
+ ExistQVarsMapping, CtorArg, SuperCtorArg, ArgNum, ArgNum + 1,
+ !FoundInvalidType, !Specs) :-
CtorArg = ctor_arg(_FieldName, ArgType, Context),
SuperCtorArg = ctor_arg(_SuperFieldName, SuperArgType, _SuperContext),
( if
- check_is_subtype(TypeTable, TVarSet, OrigTypeStatus,
- ArgType, SuperArgType,
- MaybeExistConstraints, MaybeSuperExistConstraints,
- !ExistQVarsMapping)
+ check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, ExistQVarsMapping,
+ ArgType, SuperArgType)
then
true
else
@@ -1779,12 +1878,10 @@ check_subtype_ctor_arg(TypeTable, TVarSet, OrigTypeStatus, CtorSymName,
%---------------------%
:- pred check_is_subtype(type_table::in, tvarset::in, type_status::in,
- mer_type::in, mer_type::in,
- maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
- existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
+ existq_tvar_mapping::in, mer_type::in, mer_type::in) is semidet.
-check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
+check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, ExistQVarsMapping,
+ TypeA, TypeB) :-
require_complete_switch [TypeA]
(
TypeA = builtin_type(BuiltinType),
@@ -1792,8 +1889,7 @@ check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
;
TypeA = type_variable(VarA, Kind),
TypeB = type_variable(VarB, Kind),
- check_is_subtype_var_var(VarA, VarB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+ check_is_subtype_var_var(ExistQVarsMapping, VarA, VarB)
;
TypeA = defined_type(NameA, ArgTypesA, Kind),
TypeB = defined_type(NameB, ArgTypesB, Kind),
@@ -1806,9 +1902,7 @@ check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
% TypeA and TypeB have the same type constructor.
% Check their corresponding argument types.
check_corresponding_args_are_subtype(TypeTable, TVarSet0,
- OrigTypeStatus, ArgTypesA, ArgTypesB,
- MaybeExistConstraintsA, MaybeExistConstraintsB,
- !ExistQVarsMapping)
+ OrigTypeStatus, ExistQVarsMapping, ArgTypesA, ArgTypesB)
else
% TypeA and TypeB have different type constructors.
% Find a subtype definition s(S1, ..., Sn) =< t(T1, ..., Tk)
@@ -1839,9 +1933,7 @@ check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
% Check that t(T1', ..., Tk') =< TypeB.
check_is_subtype(TypeTable, TVarSet, OrigTypeStatus,
- RenamedSuperTypeA, TypeB,
- MaybeExistConstraintsA, MaybeExistConstraintsB,
- !ExistQVarsMapping)
+ ExistQVarsMapping, RenamedSuperTypeA, TypeB)
)
;
TypeA = tuple_type(ArgTypesA, Kind),
@@ -1849,8 +1941,7 @@ check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
list.length(ArgTypesA, Arity),
list.length(ArgTypesB, Arity),
check_corresponding_args_are_subtype(TypeTable, TVarSet0,
- OrigTypeStatus, ArgTypesA, ArgTypesB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+ OrigTypeStatus, ExistQVarsMapping, ArgTypesA, ArgTypesB)
;
TypeA = higher_order_type(PredOrFunc, ArgTypesA, HOInstInfoA, Purity),
TypeB = higher_order_type(PredOrFunc, ArgTypesB, HOInstInfoB, Purity),
@@ -1872,94 +1963,51 @@ check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
MaybeArgModesB = no
),
check_is_subtype_higher_order(TypeTable, TVarSet0, OrigTypeStatus,
- ArgTypesA, ArgTypesB, MaybeArgModesA, MaybeArgModesB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+ ExistQVarsMapping, ArgTypesA, ArgTypesB,
+ MaybeArgModesA, MaybeArgModesB)
;
TypeA = apply_n_type(_, _, _),
fail
;
TypeA = kinded_type(TypeA1, Kind),
TypeB = kinded_type(TypeB1, Kind),
- check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA1, TypeB1,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping)
+ check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus,
+ ExistQVarsMapping, TypeA1, TypeB1)
).
-:- pred check_is_subtype_var_var(tvar::in, tvar::in,
- maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
- existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
-
-check_is_subtype_var_var(VarA, VarB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
- ( if VarA = VarB then
- % Double check that VarA (and VarB) are universally quantified.
- is_univ_quantified(MaybeExistConstraintsA, VarA)
- else
- % VarA and VarB should both be existentially quantified.
- % There must be a one-to-one correspondence between existentially
- % quantified type variables in the subtype and the supertype.
- ( if bimap.forward_search(!.ExistQVarsMapping, VarB, PrevVar) then
- % VarB was seen already; it should be mapped to VarA.
- PrevVar = VarA
- else
- % VarB was not seen yet.
- MaybeExistConstraintsA = exist_constraints(ExistConstraintsA),
- MaybeExistConstraintsB = exist_constraints(ExistConstraintsB),
- ExistConstraintsA = cons_exist_constraints(_ExistQVarsA,
- _ConstraintsA, UnconstrainedExistQVarsA, ConstrainedExistQVarsA),
- ExistConstraintsB = cons_exist_constraints(_ExistQVarsB,
- _ConstraintsB, UnconstrainedExistQVarsB, ConstrainedExistQVarsB),
- % VarA and VarB should both be unconstrained, or both be
- % constrained.
- (
- list.contains(UnconstrainedExistQVarsA, VarA),
- list.contains(UnconstrainedExistQVarsB, VarB)
- ;
- list.contains(ConstrainedExistQVarsA, VarA),
- list.contains(ConstrainedExistQVarsB, VarB)
- ),
- % Record the correspondence between VarB and VarA.
- % This fails if another type variable was mapped to VarA already.
- bimap.insert(VarB, VarA, !ExistQVarsMapping)
- )
- ).
-
-:- pred is_univ_quantified(maybe_cons_exist_constraints::in, tvar::in)
+:- pred check_is_subtype_var_var(existq_tvar_mapping::in, tvar::in, tvar::in)
is semidet.
-is_univ_quantified(MaybeExistConstraints, TVar) :-
- (
- MaybeExistConstraints = no_exist_constraints
- ;
- MaybeExistConstraints = exist_constraints(ExistConstraints),
- ExistQVars = ExistConstraints ^ cons_existq_tvars,
- not list.contains(ExistQVars, TVar)
+check_is_subtype_var_var(ExistQVarsMapping, VarA, VarB) :-
+ ( if VarA = VarB then
+ % Double check that VarA and VarB are universally quantified.
+ not bimap.forward_search(ExistQVarsMapping, VarB, _)
+ else
+ % Check that VarA and VarB are corresponding existentially quantified
+ % type variables.
+ bimap.forward_search(ExistQVarsMapping, VarB, VarA)
).
:- pred check_corresponding_args_are_subtype(type_table::in, tvarset::in,
- type_status::in, list(mer_type)::in, list(mer_type)::in,
- maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
- existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
+ type_status::in, existq_tvar_mapping::in,
+ list(mer_type)::in, list(mer_type)::in) is semidet.
check_corresponding_args_are_subtype(_TypeTable, _TVarSet, _OrigTypeStatus,
- [], [],
- _MaybeExistConstraintsA, _MaybeExistConstraintsB, !ExistQVarsMapping).
+ _ExistQVarsMapping, [], []).
check_corresponding_args_are_subtype(TypeTable, TVarSet, OrigTypeStatus,
- [TypeA | TypesA], [TypeB | TypesB],
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
- check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, TypeA, TypeB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping),
+ ExistQVarsMapping, [TypeA | TypesA], [TypeB | TypesB]) :-
+ check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, ExistQVarsMapping,
+ TypeA, TypeB),
check_corresponding_args_are_subtype(TypeTable, TVarSet, OrigTypeStatus,
- TypesA, TypesB, MaybeExistConstraintsA, MaybeExistConstraintsB,
- !ExistQVarsMapping).
+ ExistQVarsMapping, TypesA, TypesB).
:- pred check_is_subtype_higher_order(type_table::in, tvarset::in,
- type_status::in, list(mer_type)::in, list(mer_type)::in,
- maybe(list(mer_mode))::in, maybe(list(mer_mode))::in,
- maybe_cons_exist_constraints::in, maybe_cons_exist_constraints::in,
- existq_tvar_mapping::in, existq_tvar_mapping::out) is semidet.
+ type_status::in, existq_tvar_mapping::in,
+ list(mer_type)::in, list(mer_type)::in,
+ maybe(list(mer_mode))::in, maybe(list(mer_mode))::in) is semidet.
check_is_subtype_higher_order(_TypeTable, _TVarSet, _OrigTypeStatus,
- [], [], MaybeModesA, MaybeModesB, _, _, !ExistQVarsMapping) :-
+ _ExistQVarsMapping, [], [], MaybeModesA, MaybeModesB) :-
(
MaybeModesA = no,
MaybeModesB = no
@@ -1968,14 +2016,14 @@ check_is_subtype_higher_order(_TypeTable, _TVarSet, _OrigTypeStatus,
MaybeModesB = yes([])
).
check_is_subtype_higher_order(TypeTable, TVarSet, OrigTypeStatus,
- [TypeA | TypesA], [TypeB | TypesB], MaybeModesA0, MaybeModesB0,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
+ ExistQVarsMapping,
+ [TypeA | TypesA], [TypeB | TypesB], MaybeModesA0, MaybeModesB0) :-
% Check arguments of higher order term have the same type.
% This could be more efficient, but should be rarely used anyway.
- check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, TypeA, TypeB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping),
- check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, TypeB, TypeA,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping),
+ check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, ExistQVarsMapping,
+ TypeA, TypeB),
+ check_is_subtype(TypeTable, TVarSet, OrigTypeStatus, ExistQVarsMapping,
+ TypeB, TypeA),
% Argument modes, if available, must match exactly.
(
@@ -1993,38 +2041,7 @@ check_is_subtype_higher_order(TypeTable, TVarSet, OrigTypeStatus,
),
check_is_subtype_higher_order(TypeTable, TVarSet, OrigTypeStatus,
- TypesA, TypesB, MaybeModesA, MaybeModesB,
- MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping).
-
-%---------------------%
-
-:- pred check_subtype_ctor_exist_constraints(sym_name_arity::in,
- cons_exist_constraints::in, cons_exist_constraints::in,
- existq_tvar_mapping::in, prog_context::in,
- found_invalid_type::in, found_invalid_type::out,
- list(error_spec)::in, list(error_spec)::out) is det.
-
-check_subtype_ctor_exist_constraints(CtorSymNameArity,
- ExistConstraints, SuperExistConstraints, ExistQVarsMapping, Context,
- !FoundInvalidType, !Specs) :-
- ExistConstraints = cons_exist_constraints(_, Constraints, _, _),
- SuperExistConstraints = cons_exist_constraints(_, SuperConstraints0, _, _),
- ExistQVarsRenaming = bimap.forward_map(ExistQVarsMapping),
- apply_variable_renaming_to_prog_constraint_list(ExistQVarsRenaming,
- SuperConstraints0, SuperConstraints),
- list.sort(Constraints, SortedConstraints),
- list.sort(SuperConstraints, SortedSuperConstraints),
- ( if SortedConstraints = SortedSuperConstraints then
- true
- else
- Pieces = [words("Error: existential class constraints for")] ++
- color_as_subject([unqual_sym_name_arity(CtorSymNameArity)]) ++
- color_as_incorrect([words("differ")]) ++
- [words("in the subtype and supertype."), nl],
- Spec = spec($pred, severity_error, phase_pt2h, Context, Pieces),
- !:Specs = [Spec | !.Specs],
- !:FoundInvalidType = found_invalid_type
- ).
+ ExistQVarsMapping, TypesA, TypesB, MaybeModesA, MaybeModesB).
%---------------------%
diff --git a/compiler/prog_data.m b/compiler/prog_data.m
index 0d7652eaf..2d007c58e 100644
--- a/compiler/prog_data.m
+++ b/compiler/prog_data.m
@@ -2,7 +2,7 @@
% vim: ft=mercury ts=4 sw=4 et
%---------------------------------------------------------------------------%
% Copyright (C) 1996-2012 The University of Melbourne.
-% Copyright (C) 2014-2022 The Mercury team.
+% Copyright (C) 2014-2024 The Mercury team.
% This file may only be copied under the terms of the GNU General
% Public License - see the file COPYING in the Mercury distribution.
%---------------------------------------------------------------------------%
@@ -514,7 +514,7 @@ cons_id_is_const_struct(ConsId, ConstNum) :-
:- type cons_exist_constraints
---> cons_exist_constraints(
- % Neither list may be empty.
+ % cons_existq_tvars cannot be empty.
cons_existq_tvars :: existq_tvars,
cons_constraints :: list(prog_constraint),
diff --git a/doc/reference_manual.texi b/doc/reference_manual.texi
index bf3ac3f4d..de250f2b1 100644
--- a/doc/reference_manual.texi
+++ b/doc/reference_manual.texi
@@ -3386,16 +3386,16 @@ And this is an example of the second:
(There are more examples below.)
-If the subtype retains a constructor from the super type
+If the subtype retains a constructor from the supertype
that has one or more existentially quantified type variables,
-then there must be a one-to-one mapping between
-the existentially quantified type variables
-for the constructor in the subtype definition
-and the same constructor in the supertype definition.
-The subtype constructor must repeat
-exactly the same set of existential class constraints
-on its existentially quantified type variables as in the supertype;
-the subtype constructor cannot add or remove any existential class constraints.
+then the subtype constructor must repeat
+the list of existentially quantified type variables
+from the supertype constructor,
+and all existential class constraints,
+with no additions, removals, or reordering.
+(The type variables do not need to have the same names
+in the subtype as the supertype,
+but, stylistically, it makes more sense if they do.)
As mentioned above,
any universally quantified type variable
diff --git a/tests/invalid/subtype_exist_constraints.err_exp b/tests/invalid/subtype_exist_constraints.err_exp
index 1334dd2d9..f4ff2fe73 100644
--- a/tests/invalid/subtype_exist_constraints.err_exp
+++ b/tests/invalid/subtype_exist_constraints.err_exp
@@ -1,6 +1,5 @@
-subtype_exist_constraints.m:020: Error: [38;5;87mthe first argument of `lemon'[39;49m has a
-subtype_exist_constraints.m:020: type, [38;5;203m`L', which is not a subtype[39;49m of the
-subtype_exist_constraints.m:020: corresponding argument type [38;5;40m`L'[39;49m in the
+subtype_exist_constraints.m:020: Error: existential class constraints for
+subtype_exist_constraints.m:020: [38;5;87m`lemon'/1[39;49m [38;5;203mdiffer[39;49m in the subtype and
subtype_exist_constraints.m:020: supertype.
subtype_exist_constraints.m:023: Error: existential class constraints for
subtype_exist_constraints.m:023: [38;5;87m`lemon'/1[39;49m [38;5;203mdiffer[39;49m in the subtype and
@@ -8,3 +7,8 @@ subtype_exist_constraints.m:023: supertype.
subtype_exist_constraints.m:026: Error: existential class constraints for
subtype_exist_constraints.m:026: [38;5;87m`lemon'/1[39;49m [38;5;203mdiffer[39;49m in the subtype and
subtype_exist_constraints.m:026: supertype.
+subtype_exist_constraints.m:035: Error: existential class constraints for
+subtype_exist_constraints.m:035: [38;5;87m`foo'/4[39;49m [38;5;203mdiffer[39;49m in the subtype and supertype.
+subtype_exist_constraints.m:038: Error: existential class constraints for
+subtype_exist_constraints.m:038: [38;5;87m`foo'/4[39;49m [38;5;203mdiffer[39;49m in order in the subtype and
+subtype_exist_constraints.m:038: supertype.
diff --git a/tests/invalid/subtype_exist_constraints.m b/tests/invalid/subtype_exist_constraints.m
index 94b4c98f5..cfedaddb6 100644
--- a/tests/invalid/subtype_exist_constraints.m
+++ b/tests/invalid/subtype_exist_constraints.m
@@ -24,3 +24,15 @@
:- type extra_constraint =< fruit
---> some [L] lemon(L) => (sour(L), sweet(L)).
+
+:- type foo
+ ---> some [A, B, C, D] foo(A, B, C, D) => (sweet(B), sour(C)).
+
+:- type constraints_same_order =< foo
+ ---> some [X4, X3, X2, X1] foo(X4, X3, X2, X1) => (sweet(X3), sour(X2)).
+
+:- type constraints_differ =< foo
+ ---> some [X4, X3, X2, X1] foo(X4, X3, X2, X1) => (sweet(X2), sour(X3)).
+
+:- type constraints_different_order =< foo
+ ---> some [X4, X3, X2, X1] foo(X4, X3, X2, X1) => (sour(X2), sweet(X3)).
diff --git a/tests/invalid/subtype_exist_vars.err_exp b/tests/invalid/subtype_exist_vars.err_exp
index 562efaf92..3cd7bd438 100644
--- a/tests/invalid/subtype_exist_vars.err_exp
+++ b/tests/invalid/subtype_exist_vars.err_exp
@@ -1,15 +1,25 @@
-subtype_exist_vars.m:020: Error: [38;5;87mthe first argument of `orange'[39;49m has a type,
-subtype_exist_vars.m:020: [38;5;203m`T', which is not a subtype[39;49m of the corresponding
-subtype_exist_vars.m:020: argument type [38;5;40m`O'[39;49m in the supertype.
-subtype_exist_vars.m:023: Error: [38;5;87mthe first argument of `apple'[39;49m has a type, [38;5;203m`T',[39;49m
-subtype_exist_vars.m:023: [38;5;203mwhich is not a subtype[39;49m of the corresponding
-subtype_exist_vars.m:023: argument type [38;5;40m`int'[39;49m in the supertype.
-subtype_exist_vars.m:029: Error: [38;5;87mthe second argument of `lemon'[39;49m has a type,
-subtype_exist_vars.m:029: [38;5;203m`B', which is not a subtype[39;49m of the corresponding
-subtype_exist_vars.m:029: argument type [38;5;40m`T'[39;49m in the supertype.
-subtype_exist_vars.m:032: Error: [38;5;87mthe second argument of `lemon'[39;49m has a type,
-subtype_exist_vars.m:032: [38;5;203m`A', which is not a subtype[39;49m of the corresponding
-subtype_exist_vars.m:032: argument type [38;5;40m`T'[39;49m in the supertype.
-subtype_exist_vars.m:035: Error: [38;5;87mthe second argument of `pear'[39;49m has a type, [38;5;203m`A',[39;49m
-subtype_exist_vars.m:035: [38;5;203mwhich is not a subtype[39;49m of the corresponding
-subtype_exist_vars.m:035: argument type [38;5;40m`U'[39;49m in the supertype.
+subtype_exist_vars.m:021: Error: [38;5;87m`orange'/1[39;49m has wrong number of existentially
+subtype_exist_vars.m:021: quantified type variables ([38;5;203m0[39;49m, expected [38;5;40m1[39;49m).
+subtype_exist_vars.m:024: Error: [38;5;87m`apple'/1[39;49m has wrong number of existentially
+subtype_exist_vars.m:024: quantified type variables ([38;5;203m1[39;49m, expected [38;5;40m0[39;49m).
+subtype_exist_vars.m:030: Error: [38;5;87mthe second argument of `lemon'[39;49m has a type,
+subtype_exist_vars.m:030: [38;5;203m`B', which is not a subtype[39;49m of the corresponding
+subtype_exist_vars.m:030: argument type [38;5;40m`T'[39;49m in the supertype.
+subtype_exist_vars.m:033: Error: [38;5;87mthe first argument of `lemon'[39;49m has a type, [38;5;203m`B',[39;49m
+subtype_exist_vars.m:033: [38;5;203mwhich is not a subtype[39;49m of the corresponding
+subtype_exist_vars.m:033: argument type [38;5;40m`T'[39;49m in the supertype.
+subtype_exist_vars.m:033: Error: [38;5;87mthe third argument of `lemon'[39;49m has a type,
+subtype_exist_vars.m:033: [38;5;203m`subtype_exist_vars.foo(A)', which is not a subtype[39;49m
+subtype_exist_vars.m:033: of the corresponding argument type
+subtype_exist_vars.m:033: [38;5;40m`subtype_exist_vars.foo(U)'[39;49m in the supertype.
+subtype_exist_vars.m:036: Error: [38;5;87m`pear'/2[39;49m has wrong number of existentially
+subtype_exist_vars.m:036: quantified type variables ([38;5;203m1[39;49m, expected [38;5;40m2[39;49m).
+subtype_exist_vars.m:039: Error: [38;5;87mthe first argument of `pear'[39;49m has a type, [38;5;203m`B',[39;49m
+subtype_exist_vars.m:039: [38;5;203mwhich is not a subtype[39;49m of the corresponding
+subtype_exist_vars.m:039: argument type [38;5;40m`T'[39;49m in the supertype.
+subtype_exist_vars.m:039: Error: [38;5;87mthe second argument of `pear'[39;49m has a type, [38;5;203m`A',[39;49m
+subtype_exist_vars.m:039: [38;5;203mwhich is not a subtype[39;49m of the corresponding
+subtype_exist_vars.m:039: argument type [38;5;40m`U'[39;49m in the supertype.
+subtype_exist_vars.m:045: Error: existentially quantified type variables for
+subtype_exist_vars.m:045: [38;5;87m`nondistinct'/2[39;49m [38;5;203mdo not correspond[39;49m one-to-one in the
+subtype_exist_vars.m:045: subtype and supertype.
diff --git a/tests/invalid/subtype_exist_vars.m b/tests/invalid/subtype_exist_vars.m
index 0f0084a0e..adf93a545 100644
--- a/tests/invalid/subtype_exist_vars.m
+++ b/tests/invalid/subtype_exist_vars.m
@@ -11,7 +11,8 @@
---> apple(A)
; some [O] orange(O)
; some [T, U] lemon(T, T, foo(U))
- ; some [T, U] pear(T, U).
+ ; some [T, U] pear(T, U)
+ ; some [T, T] nondistinct(T, T). % weird
:- type foo(T)
---> foo(T).
@@ -33,3 +34,12 @@
:- type exist_vars_mismatch3 =< fruit
---> some [A] pear(A, A).
+
+:- type exist_vars_mismatch4 =< fruit
+ ---> some [A, B] pear(B, A). % order of quantified vars is significant
+
+:- type nondistinct_allowed =< fruit
+ ---> some [A, A] nondistinct(A, A).
+
+:- type nondistinct_mismatch =< fruit
+ ---> some [A, B] nondistinct(A, B).
--
2.44.0
More information about the reviews
mailing list