[m-rev.] for review: bug fix in existential constraints
Mark Brown
mark at cs.mu.OZ.AU
Thu Apr 14 18:09:29 AEST 2005
Estimated hours taken: 2
Branches: main, release-0.12
Only allow existential constraints to constrain existentially quantified
type variables. Likewise only allow universal constraints to constrain
universally quantified type variables.
We previously didn't check these conditions, and in fact the reference
manual allowed otherwise. However, the implementation did not support
existential constraints on universally quantified type variables, and
will not do so for the foreseeable future. The implementation does support
universal constraints on existentially quantified variables, however these
are not useful since no caller will ever be able to satisfy the constraints.
compiler/check_typeclass.m:
Check these conditions as part of typeclass checking.
Also return a bool from the recently added check for concrete
instances, indicating whether errors were found or not.
compiler/error_util.m:
compiler/hlds_error_util.m:
Add a couple of utility functions for constructing error messages.
compiler/mercury_compile.m:
Stop compilation after checking typeclasses if errors were encountered.
If the above conditions are not met then typechecking may abort.
doc/reference_manual.texi:
Document the condition on typeclass constraints.
tests/invalid/Mmakefile:
tests/invalid/quant_constraint_1.err_exp:
tests/invalid/quant_constraint_1.m:
tests/invalid/quant_constraint_2.err_exp:
tests/invalid/quant_constraint_2.m:
Test cases for the new error messages.
Index: compiler/check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.68
diff -u -r1.68 check_typeclass.m
--- compiler/check_typeclass.m 13 Apr 2005 07:41:27 -0000 1.68
+++ compiler/check_typeclass.m 14 Apr 2005 06:50:35 -0000
@@ -70,6 +70,7 @@
:- import_module check_hlds__type_util.
:- import_module hlds__hlds_code_util.
:- import_module hlds__hlds_data.
+:- import_module hlds__hlds_error_util.
:- import_module hlds__hlds_goal.
:- import_module hlds__hlds_out.
:- import_module hlds__hlds_pred.
@@ -102,10 +103,13 @@
check_typeclass__check_typeclasses(!QualInfo, !ModuleInfo, FoundError, !IO) :-
check_typeclass__check_instance_decls(!QualInfo, !ModuleInfo,
FoundInstanceError, !IO),
- check_for_missing_concrete_instances(!ModuleInfo, !IO),
+ check_for_missing_concrete_instances(!ModuleInfo, FoundMissingError,
+ !IO),
module_info_classes(!.ModuleInfo, ClassTable),
check_for_cyclic_classes(ClassTable, FoundCycleError, !IO),
- FoundError = bool.or(FoundInstanceError, FoundCycleError).
+ check_constraint_quant(!ModuleInfo, FoundQuantError, !IO),
+ FoundError = bool.or_list([FoundInstanceError, FoundMissingError,
+ FoundCycleError, FoundQuantError]).
%---------------------------------------------------------------------------%
@@ -929,9 +933,9 @@
%
:- pred check_for_missing_concrete_instances(
- module_info::in, module_info::out, io::di, io::uo) is det.
+ module_info::in, module_info::out, bool::out, io::di, io::uo) is det.
-check_for_missing_concrete_instances(!ModuleInfo, !IO) :-
+check_for_missing_concrete_instances(!ModuleInfo, FoundError, !IO) :-
module_info_instances(!.ModuleInfo, InstanceTable),
%
% Grab all the abstract instance declarations in the interface
@@ -940,8 +944,8 @@
%
gather_abstract_and_concrete_instances(InstanceTable,
AbstractInstances, ConcreteInstances),
- map.foldl(check_for_corresponding_instances(ConcreteInstances),
- AbstractInstances, !IO).
+ map.foldl2(check_for_corresponding_instances(ConcreteInstances),
+ AbstractInstances, no, FoundError, !IO).
% gather_abstract_and_concrete_instances(Table,
% AbstractInstances, ConcreteInstances).
@@ -1006,17 +1010,19 @@
).
:- pred check_for_corresponding_instances(instance_table::in,
- class_id::in, list(hlds_instance_defn)::in, io::di, io::uo) is det.
+ class_id::in, list(hlds_instance_defn)::in, bool::in, bool::out,
+ io::di, io::uo) is det.
-check_for_corresponding_instances(Concretes, ClassId, InstanceDefns, !IO) :-
- list.foldl(check_for_corresponding_instances_2(Concretes, ClassId),
- InstanceDefns, !IO).
+check_for_corresponding_instances(Concretes, ClassId, InstanceDefns,
+ !FoundError, !IO) :-
+ list.foldl2(check_for_corresponding_instances_2(Concretes, ClassId),
+ InstanceDefns, !FoundError, !IO).
:- pred check_for_corresponding_instances_2(instance_table::in, class_id::in,
- hlds_instance_defn::in, io::di, io::uo) is det.
+ hlds_instance_defn::in, bool::in, bool::out, io::di, io::uo) is det.
check_for_corresponding_instances_2(Concretes, ClassId, AbstractInstance,
- !IO) :-
+ !FoundError, !IO) :-
AbstractTypes = AbstractInstance ^ instance_types,
( multi_map.search(Concretes, ClassId, ConcreteInstances) ->
(
@@ -1054,6 +1060,7 @@
AbstractInstanceContext = AbstractInstance ^ instance_context,
write_error_pieces(AbstractInstanceContext, 0, ErrorPieces,
!IO),
+ !:FoundError = yes,
io.set_exit_status(1, !IO)
;
MissingConcreteError = no
@@ -1166,6 +1173,92 @@
add_path_element(class_id(Name, Arity), RevPieces0) =
[sym_name_and_arity(Name/Arity), words("<=") | RevPieces0].
+
+%---------------------------------------------------------------------------%
+%
+% Check that all types appearing in universal (existential) constraints are
+% universally (existentially) quantified.
+%
+
+:- pred check_constraint_quant(module_info::in, module_info::out,
+ bool::out, io::di, io::uo) is det.
+
+check_constraint_quant(!ModuleInfo, FoundError, !IO) :-
+ module_info_predids(!.ModuleInfo, PredIds),
+ list.foldl3(check_constraint_quant_2, PredIds, !ModuleInfo,
+ no, FoundError, !IO).
+
+:- pred check_constraint_quant_2(pred_id::in,
+ module_info::in, module_info::out, bool::in, bool::out,
+ io::di, io::uo) is det.
+
+check_constraint_quant_2(PredId, !ModuleInfo, !FoundError, !IO) :-
+ module_info_pred_info(!.ModuleInfo, PredId, PredInfo),
+ pred_info_get_exist_quant_tvars(PredInfo, ExistQVars),
+ pred_info_get_class_context(PredInfo, Constraints),
+ Constraints = constraints(UnivCs, ExistCs),
+ prog_type.constraint_list_get_tvars(UnivCs, UnivTVars),
+ solutions((pred(V::out) is nondet :-
+ list.member(V, UnivTVars),
+ list.member(V, ExistQVars)
+ ), BadUnivTVars),
+ maybe_report_badly_quantified_vars(PredInfo, universal_constraint,
+ BadUnivTVars, !ModuleInfo, !FoundError, !IO),
+ prog_type.constraint_list_get_tvars(ExistCs, ExistTVars),
+ list.delete_elems(ExistTVars, ExistQVars, BadExistTVars),
+ maybe_report_badly_quantified_vars(PredInfo, existential_constraint,
+ BadExistTVars, !ModuleInfo, !FoundError, !IO).
+
+:- type quant_error_type
+ ---> universal_constraint
+ ; existential_constraint.
+
+:- pred maybe_report_badly_quantified_vars(pred_info::in, quant_error_type::in,
+ list(tvar)::in, module_info::in, module_info::out,
+ bool::in, bool::out, io::di, io::uo) is det.
+
+maybe_report_badly_quantified_vars(PredInfo, QuantErrorType, TVars,
+ !ModuleInfo, !FoundError, !IO) :-
+ (
+ TVars = []
+ ;
+ TVars = [_ | _],
+ report_badly_quantified_vars(PredInfo, QuantErrorType, TVars,
+ !IO),
+ module_info_incr_errors(!ModuleInfo),
+ !:FoundError = yes,
+ io.set_exit_status(1, !IO)
+ ).
+
+:- pred report_badly_quantified_vars(pred_info::in, quant_error_type::in,
+ list(tvar)::in, io::di, io::uo) is det.
+
+report_badly_quantified_vars(PredInfo, QuantErrorType, TVars, !IO) :-
+ pred_info_typevarset(PredInfo, TVarSet),
+ pred_info_context(PredInfo, Context),
+
+ InDeclaration = [words("In declaration of")] ++
+ describe_one_pred_info_name(should_module_qualify, PredInfo) ++
+ [suffix(":")],
+ TypeVariables = [words("type variable"),
+ suffix(choose_number(TVars, "", "s"))],
+ TVarsStrs = list.map((func(V) = mercury_var_to_string(V, TVarSet, no)),
+ TVars),
+ TVarsPart = list_to_pieces(TVarsStrs),
+ Are = words(choose_number(TVars, "is", "are")),
+ (
+ QuantErrorType = universal_constraint,
+ BlahConstrained = words("universally constrained"),
+ BlahQuantified = words("existentially quantified")
+ ;
+ QuantErrorType = existential_constraint,
+ BlahConstrained = words("existentially constrained"),
+ BlahQuantified = words("universally quantified")
+ ),
+ Pieces = InDeclaration ++ TypeVariables ++ TVarsPart ++
+ [Are, BlahConstrained, suffix(","), words("but"), Are,
+ BlahQuantified, suffix(".")],
+ write_error_pieces(Context, 0, Pieces, !IO).
%---------------------------------------------------------------------------%
Index: compiler/error_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/error_util.m,v
retrieving revision 1.36
diff -u -r1.36 error_util.m
--- compiler/error_util.m 12 Apr 2005 07:58:14 -0000 1.36
+++ compiler/error_util.m 14 Apr 2005 07:00:42 -0000
@@ -92,6 +92,14 @@
:- func component_list_to_pieces(list(format_component)) =
list(format_component).
+ % choose_number(List, Singular, Plural) = Form
+ %
+ % Choose between a singular version and a plural version of something,
+ % based on the length of a list. Chooses the plural if the list is
+ % empty.
+ %
+:- func choose_number(list(T), U, U) = U.
+
% Display the given error message, without a context and with standard
% indentation.
:- pred write_error_pieces_plain(list(format_component)::in,
@@ -223,6 +231,10 @@
list__append(append_punctuation([Component1], ','),
component_list_to_pieces(
[Component2, Component3 | Components])).
+
+choose_number([], _Singular, Plural) = Plural.
+choose_number([_], Singular, _Plural) = Singular.
+choose_number([_, _ | _], _Singular, Plural) = Plural.
write_error_pieces_plain(Components, !IO) :-
write_error_pieces_maybe_with_context(yes, no, 0, Components, !IO).
Index: compiler/hlds_error_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_error_util.m,v
retrieving revision 1.9
diff -u -r1.9 hlds_error_util.m
--- compiler/hlds_error_util.m 22 Mar 2005 06:39:59 -0000 1.9
+++ compiler/hlds_error_util.m 14 Apr 2005 06:03:15 -0000
@@ -35,6 +35,9 @@
:- func describe_one_pred_name(module_info, should_module_qualify, pred_id)
= list(format_component).
+:- func describe_one_pred_info_name(should_module_qualify, pred_info)
+ = list(format_component).
+
:- func describe_one_pred_name_mode(module_info, should_module_qualify,
pred_id, inst_varset, list(mode)) = list(format_component).
@@ -79,8 +82,11 @@
describe_one_pred_name(Module, ShouldModuleQualify, PredId) = Pieces :-
module_info_pred_info(Module, PredId, PredInfo),
- ModuleName = pred_info_module(PredInfo),
+ Pieces = describe_one_pred_info_name(ShouldModuleQualify, PredInfo).
+
+describe_one_pred_info_name(ShouldModuleQualify, PredInfo) = Pieces :-
PredName = pred_info_name(PredInfo),
+ ModuleName = pred_info_module(PredInfo),
Arity = pred_info_orig_arity(PredInfo),
PredOrFunc = pred_info_is_pred_or_func(PredInfo),
PredOrFuncStr = pred_or_func_to_string(PredOrFunc),
Index: compiler/mercury_compile.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_compile.m,v
retrieving revision 1.331
diff -u -r1.331 mercury_compile.m
--- compiler/mercury_compile.m 7 Apr 2005 06:32:11 -0000 1.331
+++ compiler/mercury_compile.m 14 Apr 2005 07:28:19 -0000
@@ -1957,33 +1957,40 @@
% typecheck would get internal errors
%
globals__io_get_globals(Globals, !IO),
+ globals__lookup_bool_option(Globals, verbose, Verbose),
( FoundUndefTypeError = yes ->
!:FoundError = yes,
- globals__lookup_bool_option(Globals, verbose, Verbose),
maybe_write_string(Verbose,
"% Program contains undefined type error(s).\n", !IO),
io__set_exit_status(1, !IO)
;
- mercury_compile__frontend_pass_no_type_error(QualInfo0,
- FoundUndefModeError, !FoundError, !HLDS, !IO)
+ maybe_write_string(Verbose,
+ "% Checking typeclasses...\n", !IO),
+ check_typeclass__check_typeclasses(QualInfo0, QualInfo, !HLDS,
+ FoundTypeclassError, !IO),
+ mercury_compile__maybe_dump_hlds(!.HLDS, 5, "typeclass", !IO),
+ make_hlds__set_module_recompilation_info(QualInfo, !HLDS),
+
+ %
+ % We can't continue after a typeclass error, since typecheck
+ % can get internal errors.
+ %
+ ( FoundTypeclassError = yes ->
+ !:FoundError = yes
+ ;
+ mercury_compile__frontend_pass_no_type_error(
+ FoundUndefModeError, !FoundError, !HLDS, !IO)
+ )
).
-:- pred mercury_compile__frontend_pass_no_type_error(qual_info::in,
- bool::in, bool::in, bool::out, module_info::in, module_info::out,
- io::di, io::uo) is det.
+:- pred mercury_compile__frontend_pass_no_type_error(bool::in, bool::in,
+ bool::out, module_info::in, module_info::out, io::di, io::uo) is det.
-mercury_compile__frontend_pass_no_type_error(QualInfo0,
- FoundUndefModeError, !FoundError, !HLDS, !IO) :-
+mercury_compile__frontend_pass_no_type_error(FoundUndefModeError, !FoundError,
+ !HLDS, !IO) :-
globals__io_get_globals(Globals, !IO),
globals__lookup_bool_option(Globals, verbose, Verbose),
globals__lookup_bool_option(Globals, statistics, Stats),
- maybe_write_string(Verbose,
- "% Checking typeclasses...\n", !IO),
- check_typeclass__check_typeclasses(QualInfo0, QualInfo, !HLDS,
- FoundTypeclassError, !IO),
- mercury_compile__maybe_dump_hlds(!.HLDS, 5, "typeclass", !IO),
- make_hlds__set_module_recompilation_info(QualInfo, !HLDS),
-
globals__lookup_bool_option(Globals, intermodule_optimization,
Intermod),
globals__lookup_bool_option(Globals, use_opt_files, UseOptFiles),
@@ -2056,18 +2063,18 @@
mercury_compile__maybe_dump_hlds(!.HLDS, 20, "puritycheck",
!IO),
+ !:FoundError = !.FoundError `or` FoundTypeError,
+
%
% Stop here if `--typecheck-only' was specified.
%
globals__lookup_bool_option(Globals, typecheck_only,
TypecheckOnly),
( TypecheckOnly = yes ->
- bool__or(FoundTypeError, FoundTypeclassError,
- !:FoundError)
+ true
;
( FoundTypeError = yes
; FoundPostTypecheckError = yes
- ; FoundTypeclassError = yes
)
->
%
@@ -2092,8 +2099,7 @@
% if our job was to write out the `.opt' file,
% then we're done
( MakeOptInt = yes ->
- bool__or(FoundTypeError, FoundTypeclassError,
- !:FoundError)
+ true
;
%
% Now go ahead and do the rest of mode checking
@@ -2101,9 +2107,8 @@
%
mercury_compile__frontend_pass_by_phases(!HLDS,
FoundModeOrDetError, !IO),
- !:FoundError = FoundTypeError
+ !:FoundError = !.FoundError
`or` FoundModeOrDetError
- `or` FoundTypeclassError
)
)
).
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.311
diff -u -r1.311 reference_manual.texi
--- doc/reference_manual.texi 24 Mar 2005 05:34:24 -0000 1.311
+++ doc/reference_manual.texi 14 Apr 2005 07:49:13 -0000
@@ -5247,20 +5247,18 @@
For example:
@example
-% Here `c1(T2)' and `c2(T1, T2)' are existential constraints,
+% Here `c1(T2)' and `c2(T2)' are existential constraints,
% and `c3(T1)' is a universal constraint,
-:- all [T1] some [T2] ((pred p(T1, T2) => (c1(T2), c2(T1, T2))) <= c3(T1)).
+:- all [T1] some [T2] ((pred p(T1, T2) => (c1(T2), c2(T2))) <= c3(T1)).
@end example
-In general, constraints that constrain any existentially quantified
-type variables should be existential constraints, and constraints that
-constrain only universally quantified type variables should be
-universal constraints. (The only time exceptions to this rule would
-make any sense at all would be if there were instance declarations that
-were visible in the definition of the caller but which due to module
-visibility issues were not in the definition of the callee, or vice
-versa. But even then, any exception to this rule would have to involve
-a rather obscure coding style, which we do not recommend.)
+Existential constraints must only constrain type variables
+that are explicitly existentially quantified.
+Likewise, universal constraints must only constrain type variables
+that are universally quantified,
+although in this case the quantification does not have to be explicit
+because universal quantification is the default
+(see @ref{Syntax for explicit type quantifiers}).
@node Existentially typed data types
@section Existentially typed data types
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.163
diff -u -r1.163 Mmakefile
--- tests/invalid/Mmakefile 13 Apr 2005 07:41:28 -0000 1.163
+++ tests/invalid/Mmakefile 14 Apr 2005 06:16:56 -0000
@@ -123,6 +123,8 @@
promise_equivalent_solutions_test \
qual_basic_test2 \
qualified_cons_id2 \
+ quant_constraint_1 \
+ quant_constraint_2 \
record_syntax_errors \
some \
spurious_mode_error \
Index: tests/invalid/quant_constraint_1.err_exp
===================================================================
RCS file: tests/invalid/quant_constraint_1.err_exp
diff -N tests/invalid/quant_constraint_1.err_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/quant_constraint_1.err_exp 14 Apr 2005 07:30:00 -0000
@@ -0,0 +1,7 @@
+quant_constraint_1.m:015: In declaration of predicate `quant_constraint_1.p/2':
+quant_constraint_1.m:015: type variable T2 is universally constrained, but is
+quant_constraint_1.m:015: existentially quantified.
+quant_constraint_1.m:015: In declaration of predicate `quant_constraint_1.p/2':
+quant_constraint_1.m:015: type variable T1 is existentially constrained, but
+quant_constraint_1.m:015: is universally quantified.
+For more information, try recompiling with `-E'.
Index: tests/invalid/quant_constraint_1.m
===================================================================
RCS file: tests/invalid/quant_constraint_1.m
diff -N tests/invalid/quant_constraint_1.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/quant_constraint_1.m 14 Apr 2005 06:20:57 -0000
@@ -0,0 +1,21 @@
+:- module quant_constraint_1.
+:- interface.
+
+:- typeclass c1(T1, T2) where [].
+:- typeclass c2(T1) where [].
+:- typeclass c3(T1) where [].
+
+ % Two errors:
+ % T2 is in universal constraint c2, but is existentially
+ % quantified.
+ %
+ % T1 is in existential constraint c1, but is universally
+ % quantified.
+ %
+:- all [T1] some [T2] ((pred p(T1, T2) => c1(T1, T2)) <= (c2(T2), c3(T1))).
+:- mode p(in, out) is det.
+
+:- implementation.
+
+p(A, A).
+
Index: tests/invalid/quant_constraint_2.err_exp
===================================================================
RCS file: tests/invalid/quant_constraint_2.err_exp
diff -N tests/invalid/quant_constraint_2.err_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/quant_constraint_2.err_exp 14 Apr 2005 07:34:23 -0000
@@ -0,0 +1,4 @@
+quant_constraint_2.m:012: In declaration of function `quant_constraint_2.q/0':
+quant_constraint_2.m:012: type variable T is universally constrained, but is
+quant_constraint_2.m:012: existentially quantified.
+For more information, try recompiling with `-E'.
Index: tests/invalid/quant_constraint_2.m
===================================================================
RCS file: tests/invalid/quant_constraint_2.m
diff -N tests/invalid/quant_constraint_2.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/quant_constraint_2.m 14 Apr 2005 07:33:19 -0000
@@ -0,0 +1,24 @@
+:- module quant_constraint_2.
+:- interface.
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- typeclass c1(T1) where [].
+
+ % Error: T is existentially quantified, but appears in a universal
+ % constraint.
+ %
+:- some [T] (func q = T <= c1(T)).
+
+:- implementation.
+
+:- instance c1(int) where [].
+
+q = 1.
+
+main(!IO) :-
+ q(X),
+ write(X, !IO),
+ nl(!IO).
+
--------------------------------------------------------------------------
mercury-reviews mailing list
post: mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------
More information about the reviews
mailing list