for review: handle non-simple typeclass constraints

Fergus Henderson fjh at cs.mu.OZ.AU
Wed Apr 8 13:54:23 AEST 1998


Hi,

DJ, can you please review this one?

--------------------------------------------------

Estimated hours taken: 10

Fix some bugs in the handling of "non-simple" type class constraints
(ones for which the types being constrained are not just type variables).

compiler/prog_io_typeclass.m:
	Ensure that constraints on type class declarations must be "simple".
	This is needed the ensure termination of type checking.
	(We already did this for instance declarations, but not for
	superclass constraints on type class declarations.)

compiler/prog_data.m:
	Document the invariant that the types in a type class constraint
	must not contain any information in their term__context fields.

compiler/type_util.m:
compiler/equiv_type.m:
compiler/polymorphism.m:
compiler/prog_io_typeclass.m:
	Enforce the above-mentioned invariant.
	
compiler/typecheck.m:
	Allow the declared constraints to be a superset of the
	inferred constraints.
	When performing context reduction, eliminate declared
	constraints at each step rather than only at the end.
	Remove declared constraints and apply superclass rules
	before applying instance rules.
	When applying instance rules, make sure that it is a type
	error if there is no matching instance rule for a ground
	constraint.
	If context reduction results in an error, restore the
	original type assign set, to avoid repeating the same
	error message at every subsequent call to perform_context_reduction.

compiler/check_typeclass.m:
	When checking superclass conformance for instance declarations,
	pass `[]' for the extra "DeclaredConstraints" argument that is
	now needed by typecheck__reduce_context_by_rule_application.

cvs diff: Diffing .
Index: check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.4
diff -u -u -r1.4 check_typeclass.m
--- check_typeclass.m	1998/03/03 17:33:38	1.4
+++ check_typeclass.m	1998/04/08 02:10:51
@@ -448,13 +448,15 @@
 	(
 			% Reduce the superclass constraints
 		typecheck__reduce_context_by_rule_application(InstanceTable, 
-			ClassTable, TypeSubst, InstanceVarSet1, InstanceVarSet2,
+			ClassTable, [], TypeSubst,
+			InstanceVarSet1, InstanceVarSet2,
 			Proofs0, Proofs1, SuperClasses, 
 			ReducedSuperClasses0),
 
 			% Reduce the constraints from the instance declaration
 		typecheck__reduce_context_by_rule_application(InstanceTable, 
-			ClassTable, TypeSubst, InstanceVarSet2, InstanceVarSet2,
+			ClassTable, [], TypeSubst,
+			InstanceVarSet2, InstanceVarSet2,
 			Proofs1, Proofs2, InstanceConstraints,
 			ReducedInstanceConstraints0)
 	->
Index: equiv_type.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/equiv_type.m,v
retrieving revision 1.14
diff -u -u -r1.14 equiv_type.m
--- equiv_type.m	1998/03/03 17:34:09	1.14
+++ equiv_type.m	1998/04/08 01:06:13
@@ -203,7 +203,10 @@
 equiv_type__replace_in_class_constraint(Constraint0, VarSet0, EqvMap,
 				Constraint, VarSet) :-
 	Constraint0 = constraint(ClassName, Ts0),
-	equiv_type__replace_in_type_list(Ts0, VarSet0, EqvMap, Ts, VarSet, _),
+	equiv_type__replace_in_type_list(Ts0, VarSet0, EqvMap, Ts1, VarSet, _),
+	% we must maintain the invariant that types in class constraints
+	% do not contain any info in their term__context fields
+	strip_term_contexts(Ts1, Ts),
 	Constraint = constraint(ClassName, Ts).
 
 %-----------------------------------------------------------------------------%
Index: polymorphism.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/polymorphism.m,v
retrieving revision 1.131
diff -u -u -r1.131 polymorphism.m
--- polymorphism.m	1998/03/30 03:09:06	1.131
+++ polymorphism.m	1998/04/08 01:32:29
@@ -1159,7 +1159,10 @@
 	term__vars_list(NewConstrainedTypes, NewConstrainedVars),
 	list__append(NewConstrainedVars, ConstrainedVars0, ConstrainedVars),
 	term__apply_rec_substitution_to_list(NewConstrainedTypes, TypeSubst, 
-		ConstrainedTypes),
+		ConstrainedTypes0),
+	% we need to maintain the invariant that types in class constraints
+	% do not contain any information in their term__context fields
+	strip_term_contexts(ConstrainedTypes0, ConstrainedTypes),
 	NewC = constraint(ClassName, ConstrainedTypes),
 
 	Info0 = poly_info(VarSet0, VarTypes0, TypeVarSet0, TypeInfoMap0, 
@@ -1318,7 +1321,11 @@
 			SubClassConstraint0 = 
 				constraint(SubClassName, SubClassTypes0),
 			term__apply_substitution_to_list(SubClassTypes0, Subst,
-				SubClassTypes),
+				SubClassTypes1),
+			% we need to maintain the invariant that types in
+			% class constraints do not contain any information
+			% in their term__context fields
+			strip_term_contexts(SubClassTypes1, SubClassTypes),
 			SubClassConstraint = 
 				constraint(SubClassName, SubClassTypes),
 			list__length(SubClassTypes, SubClassArity),
Index: prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.33
diff -u -u -r1.33 prog_data.m
--- prog_data.m	1998/03/24 00:06:57	1.33
+++ prog_data.m	1998/04/08 01:22:08
@@ -223,7 +223,19 @@
 	;	share
 	;	automatic.
 
-:- type class_constraint	---> constraint(class_name, list(type)).
+	% A class constraint represents a constraint that a given
+	% list of types is a member of the specified type class.
+	% It is an invariant of this data structure that
+	% the types in a class constraint do not contain any
+	% information in their term__context fields.
+	% This invariant is needed to ensure that we can do
+	% unifications, map__lookups, etc., and get the
+	% expected semantics.
+	% Any code that creates new class constraints must
+	% ensure that this invariant is preserved,
+	% probably by using strip_term_contexts/2 in type_util.m.
+:- type class_constraint
+	---> constraint(class_name, list(type)).
 
 :- type class_name == sym_name.
 
Index: prog_io_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_typeclass.m,v
retrieving revision 1.6
diff -u -u -r1.6 prog_io_typeclass.m
--- prog_io_typeclass.m	1998/03/03 17:35:48	1.6
+++ prog_io_typeclass.m	1998/04/08 02:11:57
@@ -93,7 +93,7 @@
 :- mode parse_constrained_class(in, in, in, in, out) is det.
 
 parse_constrained_class(ModuleName, Decl, Constraints, VarSet, Result) :-
-	parse_class_constraints(ModuleName, Constraints, 
+	parse_superclass_constraints(ModuleName, Constraints,
 		ParsedConstraints),
 	(
 		ParsedConstraints = ok(ConstraintList),
@@ -118,6 +118,34 @@
 		Result = error(String, Term)
 	).
 
+:- pred parse_superclass_constraints(module_name, term, 
+	maybe1(list(class_constraint))).
+:- mode parse_superclass_constraints(in, in, out) is det.
+
+parse_superclass_constraints(ModuleName, Constraints, Result) :-
+	parse_class_constraints(ModuleName, Constraints, ParsedConstraints),
+	(
+		ParsedConstraints = ok(ConstraintList),
+		(
+			NonVarArg = lambda([C::in, NonVar::out] is semidet, (
+				C = constraint(_, Types),
+				list__filter(
+					lambda([A::in] is semidet, 
+						\+ type_util__var(A, _)),
+					Types, [NonVar | _])
+			)),
+			list__filter_map(NonVarArg, ConstraintList, [E|_Es])
+		->
+			Result = error("constraints on class declaration may only constrain type variables, not compound types", E)
+		;
+			Result = ParsedConstraints
+		)
+	;
+		ParsedConstraints = error(_, _),
+		Result = ParsedConstraints
+	).
+
+
 :- pred parse_unconstrained_class(module_name, term, varset, maybe1(item)).
 :- mode parse_unconstrained_class(in, in, in, out) is det.
 
@@ -263,8 +291,12 @@
 parse_class_constraint(_ModuleName, Constraint, Result) :-
 	(
 		parse_qualified_term(Constraint, Constraint, "class constraint",
-			ok(ClassName, Args))
+			ok(ClassName, Args0))
 	->
+		% we need to enforce the invariant that types in type class
+		% constraints do not contain any info in their term__context
+		% fields
+		strip_term_contexts(Args0, Args),
 		Result = ok(constraint(ClassName, Args))
 	;
 		Result = error("expected atom as class name", Constraint)
@@ -337,17 +369,16 @@
 	(
 		ParsedConstraints = ok(ConstraintList),
 		(
-			NonVarArg = lambda([C::in, NonVar::out] is semidet,
-				(
-					C = constraint(_, Types),
-					list__filter(
-						lambda([A::in] is semidet, 
-							\+ type_util__var(A,_)),
-						Types, [NonVar|_])
-				)),
+			NonVarArg = lambda([C::in, NonVar::out] is semidet, (
+				C = constraint(_, Types),
+				list__filter(
+					lambda([A::in] is semidet, 
+						\+ type_util__var(A, _)),
+					Types, [NonVar | _])
+			)),
 			list__filter_map(NonVarArg, ConstraintList, [E|_Es])
 		->
-			Result = error("expected variables in constraints of instance declaration", E)
+			Result = error("constraints on instance declaration may only constrain type variables, not compound types", E)
 		;
 			Result = ParsedConstraints
 		)
Index: type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.51
diff -u -u -r1.51 type_util.m
--- type_util.m	1998/03/03 17:36:23	1.51
+++ type_util.m	1998/04/08 01:50:58
@@ -64,7 +64,7 @@
 
 	% Given a variable type, return its type variable.
 	
-:- pred type_util__var(type, var).
+:- pred type_util__var(type, tvar).
 :- mode type_util__var(in, out) is semidet.
 :- mode type_util__var(out, in) is det.
 
@@ -181,6 +181,12 @@
 	class_constraint).
 :- mode apply_subst_to_constraint(in, in, out) is det.
 
+% strip out the term__context fields, replacing them with empty
+% term__contexts (as obtained by term__context_init/1)
+% in a type or list of types
+:- pred strip_term_contexts(list(term)::in, list(term)::out) is det.
+:- pred strip_term_context(term::in, term::out) is det.
+
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
@@ -720,7 +726,10 @@
 
 apply_rec_subst_to_constraint(Subst, Constraint0, Constraint) :-
 	Constraint0 = constraint(ClassName, Types0),
-	term__apply_rec_substitution_to_list(Types0, Subst, Types),
+	term__apply_rec_substitution_to_list(Types0, Subst, Types1),
+	% we need to maintain the invariant that types in class constraints
+	% do not have any information in their term__context fields
+	strip_term_contexts(Types1, Types),
 	Constraint  = constraint(ClassName, Types).
 
 apply_subst_to_constraints(Subst, Constraints0, Constraints) :-
@@ -730,6 +739,14 @@
 	Constraint0 = constraint(ClassName, Types0),
 	term__apply_substitution_to_list(Types0, Subst, Types),
 	Constraint  = constraint(ClassName, Types).
+
+strip_term_contexts(Terms, StrippedTerms) :-
+	list__map(strip_term_context, Terms, StrippedTerms).
+	
+strip_term_context(term__variable(V), term__variable(V)).
+strip_term_context(term__functor(F, As0, _C0), term__functor(F, As, C)) :-
+	term__context_init(C),
+	strip_term_contexts(As0, As).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
Index: typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.233
diff -u -u -r1.233 typecheck.m
--- typecheck.m	1998/03/30 13:28:13	1.233
+++ typecheck.m	1998/04/08 03:52:01
@@ -159,11 +159,11 @@
 	% the instance rules or superclass rules, building up proofs for
 	% redundant constraints
 :- pred typecheck__reduce_context_by_rule_application(instance_table,
-	class_table, tsubst, tvarset, tvarset, 
+	class_table, list(class_constraint), tsubst, tvarset, tvarset, 
 	map(class_constraint, constraint_proof), 
 	map(class_constraint, constraint_proof),
 	list(class_constraint), list(class_constraint)).
-:- mode typecheck__reduce_context_by_rule_application(in, in, in, in, out, 
+:- mode typecheck__reduce_context_by_rule_application(in, in, in, in, in, out, 
 	in, out, in, out) is semidet.
 
 %-----------------------------------------------------------------------------%
@@ -909,6 +909,8 @@
 	typecheck_info_set_called_predid(PredCallId, TypeCheckInfo0,
 		TypeCheckInfo1),
 
+	typecheck_info_get_type_assign_set(TypeCheckInfo1, OrigTypeAssignSet),
+
 		% look up the called predicate's arg types
 	typecheck_info_get_module_info(TypeCheckInfo1, ModuleInfo),
 	module_info_get_predicate_table(ModuleInfo, PredicateTable),
@@ -978,7 +980,8 @@
 			% "Type classes: an exploration of the design
 			% space", S.P. Jones, M. Jones 1997.
 			% for a discussion of some of the issues.
-		perform_context_reduction(TypeCheckInfo2, TypeCheckInfo)
+		perform_context_reduction(OrigTypeAssignSet, TypeCheckInfo2,
+			TypeCheckInfo)
 
 	;
 		invalid_pred_id(PredId),
@@ -1649,8 +1652,11 @@
 typecheck_unification(X, var(Y), var(Y)) -->
 	typecheck_unify_var_var(X, Y).
 typecheck_unification(X, functor(F, As), functor(F, As)) -->
+	=(OrigTypeCheckInfo),
+	{ typecheck_info_get_type_assign_set(OrigTypeCheckInfo,
+		OrigTypeAssignSet) },
 	typecheck_unify_var_functor(X, F, As),
-	perform_context_reduction.
+	perform_context_reduction(OrigTypeAssignSet).
 typecheck_unification(X, 
 		lambda_goal(PredOrFunc, NonLocals, Vars, Modes, Det, Goal0),
 		lambda_goal(PredOrFunc, NonLocals, Vars, Modes, Det, Goal)) -->
@@ -2910,10 +2916,7 @@
 typecheck_constraints(yes, TypeCheckInfo, TypeCheckInfo).
 typecheck_constraints(no, TypeCheckInfo0, TypeCheckInfo) :-
 		% get the declared constraints
-	typecheck_info_get_constraints(TypeCheckInfo0, DeclaredConstraints0),
-		% put them in the canonical order
-	list__sort_and_remove_dups(DeclaredConstraints0, DeclaredConstraints),
-
+	typecheck_info_get_constraints(TypeCheckInfo0, DeclaredConstraints),
 
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
 
@@ -2923,13 +2926,9 @@
 				CalculatedConstraints0),
 			type_assign_get_type_bindings(TypeAssign, Bindings),
 			apply_rec_subst_to_constraints(Bindings,
-				CalculatedConstraints0, CalculatedConstraints1),
-			list__sort_and_remove_dups(CalculatedConstraints1, 
-				CalculatedConstraints),
-				% XXX. This needs thought. _When_ exactly
-				% do two constraint sets match? This is
-				% certainly too strict.
-			CalculatedConstraints = DeclaredConstraints
+				CalculatedConstraints0, CalculatedConstraints),
+			constraints_match(CalculatedConstraints,
+				DeclaredConstraints)
 		)),
 
 		% reject any type assignment whose constraints don't match the
@@ -2948,12 +2947,21 @@
 			TypeAssignSet, TypeCheckInfo)
 	).
 
+			
+	% The calculated constraints must be a subset of the declared
+	% constraints.
+:- pred constraints_match(list(class_constraint)::in,
+		list(class_constraint)::in) is semidet.
+constraints_match(CalculatedConstraints, DeclaredConstraints) :-
+	all [C] list__member(C, CalculatedConstraints) =>
+		list__member(C, DeclaredConstraints).
+
 %-----------------------------------------------------------------------------%
 
-:- pred report_unsatisfied_constraints(type_assign_set,
-	typecheck_info, typecheck_info).
-:- mode report_unsatisfied_constraints(in,
-	typecheck_info_di, typecheck_info_uo) is det.
+:- pred report_unsatisfied_constraints(type_assign_set, typecheck_info,
+					typecheck_info).
+:- mode report_unsatisfied_constraints(in, typecheck_info_di,
+					typecheck_info_uo) is det.
 
 report_unsatisfied_constraints(TypeAssignSet, TypeCheckInfo0, TypeCheckInfo) :-
 	typecheck_info_get_io_state(TypeCheckInfo0, IOState0),
@@ -2982,7 +2990,7 @@
 			io__write_string("  ", IO1, IO2),
 			io__write_list(Unsatisfied, ", ",
 				mercury_output_constraint(TheVarSet), IO2, IO3),
-			io__write_char('\n', IO3, IO)
+			io__write_string(".\n", IO3, IO)
 		)),
 
 		% XXX this won't be very pretty when there are
@@ -2995,20 +3003,26 @@
 
 %-----------------------------------------------------------------------------%
 
-% perform_context_reduction(TypeCheckInfo0, TypeCheckInfo) is true iff
+% perform_context_reduction(OrigTypeAssignSet, TypeCheckInfo0, TypeCheckInfo)
+%	is true iff either
 % 	TypeCheckInfo is the typecheck_info that results from performing
-% 	context reduction on the type_assigns in TypeCheckInfo0.
+% 	context reduction on the type_assigns in TypeCheckInfo0,
+%	or, if there is no valid context reduction, then
+%	TypeCheckInfo is TypeCheckInfo0 with the type assign set replaced by
+%	OrigTypeAssignSet.
 %
 % 	Context reduction is the process of eliminating redundant constraints
 % 	from the constraints in the type_assign and adding the proof of the
 % 	constraint's redundancy to the proofs in the same type_assign. There
-% 	are two ways in which a constraint may be redundant:
-% 		- if there is an instance declaration that may be applied, the
-% 		  constraint is replaced by the constraints from that instance
-% 		  declaration
+% 	are three ways in which a constraint may be redundant:
+%		- if a constraint occurs in the pred/func declaration for this
+%		  predicate or function, then it is redundant
 % 		- if a constraint is present in the set of constraints and all
 % 		  of the "superclass" constraints for the constraints are all
 % 		  present, then all the superclass constraints are eliminated
+% 		- if there is an instance declaration that may be applied, the
+% 		  constraint is replaced by the constraints from that instance
+% 		  declaration
 %
 % 	In addition, context reduction removes repeated constraints.
 %
@@ -3019,17 +3033,24 @@
 %	instance declaration for that type.
 %
 %	If all type_assigns from the typecheck_info are rejected, than an
-%	appropriate error message is given.
+%	appropriate error message is given, and the type_assign_set is
+%	restored to the original one given by OrigTypeAssignSet
+%	(this is to avoid reporting the same error at every subsequent call
+%	to perform_context_reduction).
 
-:- pred perform_context_reduction(typecheck_info, typecheck_info).
-:- mode perform_context_reduction(typecheck_info_di, typecheck_info_uo) is det.
+:- pred perform_context_reduction(type_assign_set,
+			typecheck_info, typecheck_info).
+:- mode perform_context_reduction(in,
+			typecheck_info_di, typecheck_info_uo) is det.
 
-perform_context_reduction(TypeCheckInfo0, TypeCheckInfo) :-
+perform_context_reduction(OrigTypeAssignSet, TypeCheckInfo0, TypeCheckInfo) :-
 	typecheck_info_get_module_info(TypeCheckInfo0, ModuleInfo),
+	typecheck_info_get_constraints(TypeCheckInfo0, DeclaredConstraints),
 	module_info_classes(ModuleInfo, ClassTable),
 	module_info_instances(ModuleInfo, InstanceTable),
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
-	list__filter_map(reduce_type_assign_context(ClassTable, InstanceTable), 
+	list__filter_map(reduce_type_assign_context(ClassTable, InstanceTable,
+			DeclaredConstraints), 
 		TypeAssignSet0, TypeAssignSet),
 	(
 			% Check that this context reduction hasn't eliminated
@@ -3038,17 +3059,19 @@
 		TypeAssignSet0 \= []
 	->
 		report_unsatisfied_constraints(TypeAssignSet0,
-			TypeCheckInfo0, TypeCheckInfo)
+			TypeCheckInfo0, TypeCheckInfo1),
+		typecheck_info_set_type_assign_set(TypeCheckInfo1,
+			OrigTypeAssignSet, TypeCheckInfo)
 	;
 		typecheck_info_set_type_assign_set(TypeCheckInfo0,
 			TypeAssignSet, TypeCheckInfo)
 	).
 
-:- pred reduce_type_assign_context(class_table, instance_table, 
-	type_assign, type_assign).
-:- mode reduce_type_assign_context(in, in, in, out) is semidet.
+:- pred reduce_type_assign_context(class_table, instance_table,
+		list(class_constraint), type_assign, type_assign).
+:- mode reduce_type_assign_context(in, in, in, in, out) is semidet.
 
-reduce_type_assign_context(ClassTable, InstanceTable, 
+reduce_type_assign_context(ClassTable, InstanceTable, DeclaredConstraints,
 		TypeAssign0, TypeAssign) :-
 	type_assign_get_typeclass_constraints(TypeAssign0, Constraints0),
 	type_assign_get_type_bindings(TypeAssign0, Bindings),
@@ -3056,7 +3079,8 @@
 	type_assign_get_constraint_proofs(TypeAssign0, Proofs0),
 
 	typecheck__reduce_context_by_rule_application(InstanceTable, 
-		ClassTable, Bindings, Tvarset0, Tvarset, Proofs0, Proofs,
+		ClassTable, DeclaredConstraints,
+		Bindings, Tvarset0, Tvarset, Proofs0, Proofs,
 		Constraints0, Constraints),
 
 	type_assign_set_typeclass_constraints(TypeAssign0, Constraints,
@@ -3066,38 +3090,56 @@
 
 
 typecheck__reduce_context_by_rule_application(InstanceTable, ClassTable, 
-		Bindings, Tvarset0, Tvarset, Proofs0, Proofs, 
-		Constraints0, Constraints) :-
-	apply_instance_rules(Constraints0, InstanceTable, Bindings, 
-		Tvarset0, Tvarset1, Proofs0, Proofs1, Constraints1, Changed1),
-	apply_class_rules(Constraints1, ClassTable, Bindings, Tvarset1,
-		Proofs1, Proofs2, Constraints2, Changed2),
+		DeclaredConstraints, Bindings, Tvarset0, Tvarset,
+		Proofs0, Proofs, Constraints0, Constraints) :-
+	apply_rec_subst_to_constraints(Bindings, Constraints0, Constraints1),
+	eliminate_declared_constraints(Constraints1, DeclaredConstraints,
+		Constraints2, Changed1),
+	apply_class_rules(Constraints2, ClassTable, Tvarset0,
+		Proofs0, Proofs1, Constraints3, Changed2),
+	apply_instance_rules(Constraints3, InstanceTable, 
+		Tvarset0, Tvarset1, Proofs1, Proofs2, Constraints4, Changed3),
 	(
-		Changed1 = no, Changed2 = no
+		Changed1 = no, Changed2 = no, Changed3 = no
 	->
 			% We have reached fixpoint
-		list__sort_and_remove_dups(Constraints2, Constraints),
+		list__sort_and_remove_dups(Constraints4, Constraints),
 		Tvarset = Tvarset1,
 		Proofs = Proofs2
 	;
 		typecheck__reduce_context_by_rule_application(InstanceTable,
-			ClassTable, Bindings, Tvarset1, Tvarset, Proofs2,
-			Proofs, Constraints2, Constraints)
+			ClassTable, DeclaredConstraints, Bindings, Tvarset1,
+			Tvarset, Proofs2, Proofs, Constraints4, Constraints)
+	).
+
+:- pred eliminate_declared_constraints(list(class_constraint), 
+	list(class_constraint), list(class_constraint), bool).
+:- mode eliminate_declared_constraints(in, in, out, out) is det.
+
+eliminate_declared_constraints([], _, [], no).
+eliminate_declared_constraints([C|Cs], DeclaredCs, NewCs, Changed) :-
+	eliminate_declared_constraints(Cs, DeclaredCs, NewCs0, Changed0),
+	(
+		list__member(C, DeclaredCs)
+	->
+		NewCs = NewCs0,
+		Changed = yes
+	;
+		NewCs = [C|NewCs0],
+		Changed = Changed0
 	).
 
 :- pred apply_instance_rules(list(class_constraint), instance_table,
-	tsubst, tvarset, tvarset, map(class_constraint, constraint_proof),
+	tvarset, tvarset, map(class_constraint, constraint_proof),
 	map(class_constraint, constraint_proof), list(class_constraint), bool).
-:- mode apply_instance_rules(in, in, in, in, out, in, out, out, out) is semidet.
+:- mode apply_instance_rules(in, in, in, out, in, out, out, out) is semidet.
 
-apply_instance_rules([], _, _, Names, Names, Proofs, Proofs, [], no).
-apply_instance_rules([C|Cs], InstanceTable, Bindings, 
-		TVarSet, NewTVarSet, Proofs0, Proofs, 
-		Constraints, Changed) :-
-	C = constraint(ClassName, Types0),
-	list__length(Types0, Arity),
+apply_instance_rules([], _, Names, Names, Proofs, Proofs, [], no).
+apply_instance_rules([C|Cs], InstanceTable, TVarSet, NewTVarSet,
+		Proofs0, Proofs, Constraints, Changed) :-
+	C = constraint(ClassName, Types),
+	list__length(Types, Arity),
 	map__lookup(InstanceTable, class_id(ClassName, Arity), Instances),
-	term__apply_rec_substitution_to_list(Types0, Bindings, Types),
 	(
 		find_matching_instance_rule(Instances, ClassName, Types,
 			TVarSet, NewTVarSet0, Proofs0, Proofs1,
@@ -3109,13 +3151,31 @@
 		Proofs2 = Proofs1,
 		Changed1 = yes
 	;
+			%
+			% Check that the constraint is not a ground
+			% constraint.  We disallow ground constraints
+			% for which there are no matching instance rules,
+			% even though the module system means that it would
+			% make sense to allow them: even if there
+			% is no instance declaration visible in the current
+			% module, there may be one visible in the caller.
+			% The reason we disallow them is that in practice
+			% allowing this causes type inference to let too
+			% many errors slip through, with the error diagnosis
+			% being too far removed from the real cause of the
+			% error.  Note that ground constraints *are* allowed
+			% if you declare them, since we removed declared
+			% constraints before checking instance rules.
+			%
+		term__contains_var_list(Types, _TVar),
+
 			% Put the old constraint at the front of the list
 		NewConstraints = [C],
 		NewTVarSet1 = TVarSet,
 		Proofs2 = Proofs0,
 		Changed1 = no
 	),
-	apply_instance_rules(Cs, InstanceTable, Bindings, NewTVarSet1,
+	apply_instance_rules(Cs, InstanceTable, NewTVarSet1,
 		NewTVarSet, Proofs2, Proofs, TheRest, Changed2),
 	bool__or(Changed1, Changed2, Changed),
 	list__append(NewConstraints, TheRest, Constraints).
@@ -3184,14 +3244,13 @@
 	% if so, delete the superclass from the constraint list as it is
 	% redundant.
 :- pred apply_class_rules(list(class_constraint), class_table,
-	tsubst, tvarset, map(class_constraint, constraint_proof),
+	tvarset, map(class_constraint, constraint_proof),
 	map(class_constraint, constraint_proof), list(class_constraint), bool).
-:- mode apply_class_rules(in, in, in, in, in, out, out, out) is det.
+:- mode apply_class_rules(in, in, in, in, out, out, out) is det.
 
-apply_class_rules(Constraints0, ClassTable, Bindings, TVarSet, 
+apply_class_rules(Constraints0, ClassTable, TVarSet, 
 		Proofs0, Proofs, Constraints, Changed) :-
-	apply_rec_subst_to_constraints(Bindings, Constraints0, Constraints1),
-	apply_class_rules_2(Constraints1, Constraints1, ClassTable,
+	apply_class_rules_2(Constraints0, Constraints0, ClassTable,
 		TVarSet, Proofs0, Proofs, Constraints, Changed).
 
 :- pred apply_class_rules_2(list(class_constraint), list(class_constraint),
cvs diff: Diffing notes

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.



More information about the developers mailing list