[m-rev.] diff: relax restrictions on existential data
Mark Brown
mark at cs.mu.OZ.AU
Fri May 13 12:23:35 AEST 2005
Estimated hours taken: 1.5
Branches: main
Relax the restriction on the constraints on existentially quantified data
structures. The type variables in constraints must be determined by the
constructor arguments and functional dependencies, but don't necessarily
have to appear directly in the constructor arguments.
compiler/check_typeclass.m:
Implement a check for type declarations which is analogous to the
existing check for pred/func declarations.
compiler/prog_io.m:
Relax the existing restriction, which was applied at parse-time.
Now we just check that all existentially quantified type vars appear
somewhere, either in the arguments or in the constraints.
Remove an XXX comment that asked whether the check that all
constrained variables were existentially quantified was overly
restrictive. The answer is no: we don't support existential
constraints with universal arguments, and we won't support it in
the foreseeable future.
tests/invalid/Mmakefile:
tests/invalid/fundeps_unbound_in_ctor.err_exp:
tests/invalid/fundeps_unbound_in_ctor.m:
New test case for the new and changed error messages.
tests/invalid/type_vars.err_exp:
Updated test case.
tests/valid/Mmakefile:
tests/valid/fundeps.m:
New test case.
Index: compiler/check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.73
diff -u -r1.73 check_typeclass.m
--- compiler/check_typeclass.m 24 Apr 2005 01:47:54 -0000 1.73
+++ compiler/check_typeclass.m 12 May 2005 17:54:00 -0000
@@ -1482,7 +1482,10 @@
% Look for pred or func declarations for which the type variables in
% the constraints are not all determined by the type variables in the
- % type and the functional dependencies.
+ % type and the functional dependencies. Likewise look for
+ % constructors for which the existential type variables in the
+ % constraints are not all determined by the type variables in the
+ % constructor arguments and the functional dependencies.
%
:- pred check_typeclass.check_constraints(module_info::in,
module_info::out, bool::out, io::di, io::uo) is det.
@@ -1490,7 +1493,11 @@
check_typeclass.check_constraints(!ModuleInfo, FoundError, !IO) :-
module_info_predids(!.ModuleInfo, PredIds),
list.foldl3(check_pred_constraints, PredIds, !ModuleInfo,
- no, FoundError, !IO).
+ no, FoundError0, !IO),
+ module_info_types(!.ModuleInfo, TypeTable),
+ map.keys(TypeTable, TypeCtors),
+ list.foldl3(check_ctor_constraints(TypeTable), TypeCtors, !ModuleInfo,
+ FoundError0, FoundError, !IO).
:- pred check_pred_constraints(pred_id::in, module_info::in,
module_info::out, bool::in, bool::out, io::di, io::uo) is det.
@@ -1523,24 +1530,69 @@
check_pred_type_ambiguities(PredInfo, !ModuleInfo, !FoundError, !IO) :-
pred_info_arg_types(PredInfo, ArgTypes),
- TVars = list_to_set(term.vars_list(ArgTypes)),
pred_info_get_class_context(PredInfo, Constraints),
- module_info_classes(!.ModuleInfo, ClassTable),
- InducedFunDeps = induced_fundeps(ClassTable, Constraints),
- FunDepsClosure = fundeps_closure(InducedFunDeps, TVars),
- solutions(constrained_var_not_in_closure(Constraints, FunDepsClosure),
- UnboundTVars),
+ TVars = term.vars_list(ArgTypes),
+ get_unbound_tvars(TVars, Constraints, !.ModuleInfo, UnboundTVars),
(
UnboundTVars = []
->
true
;
- report_unbound_tvars_in_class_context(UnboundTVars, PredInfo,
+ report_unbound_tvars_in_pred_context(UnboundTVars, PredInfo,
!IO),
!:FoundError = yes,
module_info_incr_errors(!ModuleInfo)
).
+:- pred check_ctor_constraints(type_table::in, type_ctor::in, module_info::in,
+ module_info::out, bool::in, bool::out, io::di, io::uo) is det.
+
+check_ctor_constraints(TypeTable, TypeCtor, !ModuleInfo, !FoundError, !IO) :-
+ map.lookup(TypeTable, TypeCtor, TypeDefn),
+ get_type_defn_body(TypeDefn, Body),
+ (
+ Body = du_type(Ctors, _, _, _, _, _)
+ ->
+ list.foldl3(check_ctor_type_ambiguities(TypeCtor, TypeDefn),
+ Ctors, !ModuleInfo, !FoundError, !IO)
+ ;
+ true
+ ).
+
+:- pred check_ctor_type_ambiguities(type_ctor::in, hlds_type_defn::in,
+ constructor::in, module_info::in, module_info::out,
+ bool::in, bool::out, io::di, io::uo) is det.
+
+check_ctor_type_ambiguities(TypeCtor, TypeDefn, Ctor, !ModuleInfo,
+ !FoundError, !IO) :-
+ Ctor = ctor(ExistQVars, Constraints, _, CtorArgs),
+ assoc_list.values(CtorArgs, ArgTypes),
+ ArgTVars = term.vars_list(ArgTypes),
+ list.filter((pred(V::in) is semidet :- list.member(V, ExistQVars)),
+ ArgTVars, ExistQArgTVars),
+ get_unbound_tvars(ExistQArgTVars, constraints([], Constraints),
+ !.ModuleInfo, UnboundTVars),
+ (
+ UnboundTVars = []
+ ->
+ true
+ ;
+ report_unbound_tvars_in_ctor_context(UnboundTVars, TypeCtor,
+ TypeDefn, !IO),
+ !:FoundError = yes,
+ module_info_incr_errors(!ModuleInfo)
+ ).
+
+:- pred get_unbound_tvars(list(tvar)::in, prog_constraints::in,
+ module_info::in, list(tvar)::out) is det.
+
+get_unbound_tvars(TVars, Constraints, ModuleInfo, UnboundTVars) :-
+ module_info_classes(ModuleInfo, ClassTable),
+ InducedFunDeps = induced_fundeps(ClassTable, Constraints),
+ FunDepsClosure = fundeps_closure(InducedFunDeps, list_to_set(TVars)),
+ solutions(constrained_var_not_in_closure(Constraints, FunDepsClosure),
+ UnboundTVars).
+
:- pred constrained_var_not_in_closure(prog_constraints::in, set(tvar)::in,
tvar::out) is nondet.
@@ -1640,11 +1692,16 @@
% very_long_module_name:002: error in type class constraints: type variable
% very_long_module_name:002: T occurs in the constraints, but is not
% very_long_module_name:002: determined by the predicate's argument types.
+%
+% very_long_module_name:002: In declaration for type `long_type/3':
+% very_long_module_name:002: error in type class constraints: type variable
+% very_long_module_name:002: T occurs in the constraints, but is not
+% very_long_module_name:002: determined by the constructor's argument types.
-:- pred report_unbound_tvars_in_class_context(list(tvar)::in, pred_info::in,
+:- pred report_unbound_tvars_in_pred_context(list(tvar)::in, pred_info::in,
io::di, io::uo) is det.
-report_unbound_tvars_in_class_context(Vars, PredInfo, !IO) :-
+report_unbound_tvars_in_pred_context(Vars, PredInfo, !IO) :-
pred_info_context(PredInfo, Context),
pred_info_arg_types(PredInfo, TVarSet, _, ArgTypes),
PredName = pred_info_name(PredInfo),
@@ -1674,6 +1731,31 @@
PredOrFunc = function,
Msg = Msg0 ++ [words("function's argument or result types.")]
),
+ write_error_pieces(Context, 0, Msg, !IO),
+ io__set_exit_status(1, !IO).
+
+:- pred report_unbound_tvars_in_ctor_context(list(tvar)::in, type_ctor::in,
+ hlds_type_defn::in, io::di, io::uo) is det.
+
+report_unbound_tvars_in_ctor_context(Vars, TypeCtor, TypeDefn, !IO) :-
+ get_type_defn_context(TypeDefn, Context),
+ get_type_defn_tvarset(TypeDefn, TVarSet),
+ TypeCtor = SymName - Arity,
+
+ VarsStrs = list.map(
+ (func(Var) = mercury_var_to_string(Var, TVarSet, no)),
+ Vars),
+
+ Msg = [words("In declaration for type"),
+ sym_name_and_arity(SymName / Arity),
+ suffix(":"), nl,
+ words("error in type class constraints:"),
+ words(choose_number(Vars, "type variable", "type variables"))]
+ ++ list_to_pieces(VarsStrs) ++
+ [words(choose_number(Vars, "occurs", "occur")),
+ words("in the constraints, but"),
+ words(choose_number(Vars, "is", "are")),
+ words("not determined by the constructor's argument types.")],
write_error_pieces(Context, 0, Msg, !IO),
io__set_exit_status(1, !IO).
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.242
diff -u -r1.242 prog_io.m
--- compiler/prog_io.m 1 Apr 2005 14:29:00 -0000 1.242
+++ compiler/prog_io.m 12 May 2005 17:39:26 -0000
@@ -278,6 +278,7 @@
:- import_module parse_tree__prog_io_util.
:- import_module parse_tree__prog_mode.
:- import_module parse_tree__prog_out.
+:- import_module parse_tree__prog_type.
:- import_module parse_tree__prog_util.
:- import_module recompilation.
:- import_module recompilation__version.
@@ -2356,25 +2357,22 @@
"shadows argument type)", Body)
% check that all type variables in existential quantifiers
- % occur somewhere in the constructor argument types
- % (not just the constraints)
+ % occur somewhere in the constructor argument types or constraints.
;
list__member(Ctor, Ctors),
- Ctor = ctor(ExistQVars, _Constraints, _CtorName, CtorArgs),
+ Ctor = ctor(ExistQVars, Constraints, _CtorName, CtorArgs),
list__member(Var, ExistQVars),
assoc_list__values(CtorArgs, CtorArgTypes),
- \+ term__contains_var_list(CtorArgTypes, Var)
+ \+ term__contains_var_list(CtorArgTypes, Var),
+ constraint_list_get_tvars(Constraints, ConstraintTVars),
+ \+ list__member(Var, ConstraintTVars)
->
Result = error("type variable in existential " ++
"quantifier does not occur in " ++
- "arguments of constructor", Body)
+ "arguments or constraints of constructor", Body)
+
% check that all type variables in existential constraints
% occur in the existential quantifiers
- % (XXX is this check overly conservative? Perhaps we should
- % allow existential constraints so long as they contain
- % at least one type variable which is existentially quantified,
- % rather than requiring all variables in them to be
- % existentially quantified.)
;
list__member(Ctor, Ctors),
Ctor = ctor(ExistQVars, Constraints, _CtorName, _CtorArgs),
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.168
diff -u -r1.168 Mmakefile
--- tests/invalid/Mmakefile 7 May 2005 15:49:31 -0000 1.168
+++ tests/invalid/Mmakefile 12 May 2005 17:41:01 -0000
@@ -81,6 +81,7 @@
func_errors \
funcs_as_preds \
fundeps_vars \
+ fundeps_unbound_in_ctor \
ho_default_func_1 \
ho_default_func_3 \
ho_type_mode_bug \
Index: tests/invalid/fundeps_unbound_in_ctor.err_exp
===================================================================
RCS file: tests/invalid/fundeps_unbound_in_ctor.err_exp
diff -N tests/invalid/fundeps_unbound_in_ctor.err_exp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/fundeps_unbound_in_ctor.err_exp 12 May 2005 17:56:47 -0000
@@ -0,0 +1,8 @@
+fundeps_unbound_in_ctor.m:012: Error: type variables in class constraints introduced with `=>' must be explicitly existentially quantified using `some': some [_2, _3] baz(_2, _3, _1) => foo(_2, _3, _1).
+fundeps_unbound_in_ctor.m:008: In declaration for type
+fundeps_unbound_in_ctor.m:008: `fundeps_unbound_in_ctor.bar'/0:
+fundeps_unbound_in_ctor.m:008: error in type class constraints: type variable
+fundeps_unbound_in_ctor.m:008: C occurs in the constraints, but is not
+fundeps_unbound_in_ctor.m:008: determined by the constructor's argument
+fundeps_unbound_in_ctor.m:008: types.
+For more information, try recompiling with `-E'.
Index: tests/invalid/fundeps_unbound_in_ctor.m
===================================================================
RCS file: tests/invalid/fundeps_unbound_in_ctor.m
diff -N tests/invalid/fundeps_unbound_in_ctor.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/invalid/fundeps_unbound_in_ctor.m 12 May 2005 17:44:08 -0000
@@ -0,0 +1,13 @@
+:- module fundeps_unbound_in_ctor.
+:- interface.
+
+:- typeclass foo(A, B, C) <= (A -> B) where [].
+
+ % Error: C is unbound.
+ %
+:- type bar ---> some [A, B, C] bar(A) => foo(A, B, C).
+
+ % Error: C is universally quantified.
+ %
+:- type baz(C) ---> some [A, B] baz(A, B, C) => foo(A, B, C).
+
Index: tests/invalid/type_vars.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/type_vars.err_exp,v
retrieving revision 1.2
diff -u -r1.2 type_vars.err_exp
--- tests/invalid/type_vars.err_exp 16 Aug 2000 08:54:19 -0000 1.2
+++ tests/invalid/type_vars.err_exp 13 May 2005 02:00:01 -0000
@@ -1,5 +1,8 @@
-type_vars.m:006: Error: type variable in existential quantifier does not occur in arguments of constructor: some [_1, _2] foo(_1) => c(_2).
-type_vars.m:007: Error: type variable in existential quantifier does not occur in arguments of constructor: some [_1, _2] bar(_1).
+type_vars.m:007: Error: type variable in existential quantifier does not occur in arguments or constraints of constructor: some [_1, _2] bar(_1).
type_vars.m:008: Error: type variable has overlapping scopes (explicit type quantifier shadows argument type): some [_1] bar(_1).
type_vars.m:009: Error: type variables in class constraints introduced with `=>' must be explicitly existentially quantified using `some': some [_1] bar(_1) => c(_2).
+type_vars.m:006: In declaration for type `type_vars.t1'/0:
+type_vars.m:006: error in type class constraints: type variable T2 occurs in
+type_vars.m:006: the constraints, but is not determined by the constructor's
+type_vars.m:006: argument types.
For more information, try recompiling with `-E'.
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.152
diff -u -r1.152 Mmakefile
--- tests/valid/Mmakefile 2 May 2005 08:19:08 -0000 1.152
+++ tests/valid/Mmakefile 12 May 2005 15:15:47 -0000
@@ -22,6 +22,7 @@
complex_constraint \
constraint_proof_bug \
func_method \
+ fundeps \
instance_superclass \
instance_unconstrained_tvar \
mpj2 \
Index: tests/valid/fundeps.m
===================================================================
RCS file: tests/valid/fundeps.m
diff -N tests/valid/fundeps.m
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ tests/valid/fundeps.m 12 May 2005 15:11:05 -0000
@@ -0,0 +1,6 @@
+:- module fundeps.
+:- interface.
+
+:- typeclass foo(A, B) <= (A -> B) where [].
+
+:- type bar ---> some [A, B] bar(A) => foo(A, B).
--------------------------------------------------------------------------
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