[m-dev.] for review: handle non-simple typeclass constraints

[Fergus Henderson]

On 08-Apr-1998, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> [Another diff will follow.]

... and here it is.  This diff is relative to the previous one.
As well as addressing DJ's comments, I fixed a bug:
my previous changes broke apply_class_rules.

The log message is as before except for check_typeclass.m.

compiler/check_typeclass.m:
	Change the way we superclass conformance for instance
	declarations to take advantage of the new "DeclaredConstraints"
	argument to typecheck__reduce_context_by_rule_application.

--- old/check_typeclass.m	Thu Apr  9 00:05:41 1998
+++ check_typeclass.m	Thu Apr  9 00:31:18 1998
@@ -413,6 +413,9 @@
 
 %---------------------------------------------------------------------------%
 
+% check that the superclass constraints are satisfied for the
+% types in this instance declaration
+
 :- pred check_superclass_conformance(list(class_constraint), list(var),
 	varset, module_info, hlds_instance_defn, hlds_instance_defn, 
 	list(string), list(string)).
@@ -446,43 +449,18 @@
 	module_info_classes(ModuleInfo, ClassTable),
 
 	(
-			% Reduce the superclass constraints
+			% Try to reduce the superclass constraints,
+			% using the declared instance constraints
+			% and the usual context reduction rules.
 		typecheck__reduce_context_by_rule_application(InstanceTable, 
-			ClassTable, [], TypeSubst,
+			ClassTable, InstanceConstraints, 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,
-			Proofs1, Proofs2, InstanceConstraints,
-			ReducedInstanceConstraints0)
-	->
-		ReducedSuperClasses0 = ReducedSuperClasses,
-		ReducedInstanceConstraints = ReducedInstanceConstraints0,
-		Proofs = Proofs2, 
-		InstanceVarSet = InstanceVarSet2
-	;
-			% This should never happen, since the superclass and
-			% instance constraints must all contain only variables.
-			% Context reduction can only fail if there is a 
-			% constraint with a type with a bound top-level functor
-			% for which there is no instance decl.
-		error("check_superclass_conformance: context reduction failed")
-	),
-
-		% Check for superclass constraints that are unsatisfied by
-		% the instance declaration
-	list__delete_elems(ReducedSuperClasses, ReducedInstanceConstraints,
-		Unsatisfied),
-	(
-		Unsatisfied = []
+			[])
 	->
 		Errors = Errors0,
 		InstanceDefn = hlds_instance_defn(A, InstanceConstraints,
-			InstanceTypes, D, E, InstanceVarSet, Proofs)
+			InstanceTypes, D, E, InstanceVarSet2, Proofs1)
 	;
 			% XXX improve the error message
 		NewError = "superclass constraint unsatisfied",
@@ -491,4 +469,3 @@
 	).
 
 %---------------------------------------------------------------------------%
-
--- old/typecheck.m	Thu Apr  9 00:05:50 1998
+++ typecheck.m	Thu Apr  9 00:19:01 1998
@@ -978,7 +978,7 @@
 			% Arguably, we could do context reduction at
 			% a different point. See the paper:
 			% "Type classes: an exploration of the design
-			% space", S.P. Jones, M. Jones 1997.
+			% space", S. Peyton-Jones, M. Jones 1997.
 			% for a discussion of some of the issues.
 		perform_context_reduction(OrigTypeAssignSet, TypeCheckInfo2,
 			TypeCheckInfo)
@@ -3009,7 +3009,7 @@
 % 	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.
+%	OrigTypeAssignSet (see below).
 %
 % 	Context reduction is the process of eliminating redundant constraints
 % 	from the constraints in the type_assign and adding the proof of the
@@ -3017,6 +3017,8 @@
 % 	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
+%		  (in this case, the proof is trivial, so there is no need
+%		  to record it in the proof map)
 % 		- 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
@@ -3034,9 +3036,9 @@
 %
 %	If all type_assigns from the typecheck_info are rejected, than an
 %	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).
+%	restored to the original one given by OrigTypeAssignSet.
+%	The reason for this is to avoid reporting the same error at
+%	every subsequent call to perform_context_reduction.
 
 :- pred perform_context_reduction(type_assign_set,
 			typecheck_info, typecheck_info).
@@ -3095,8 +3097,8 @@
 	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_class_rules(Constraints2, DeclaredConstraints, ClassTable,
+		Tvarset0, Proofs0, Proofs1, Constraints3, Changed2),
 	apply_instance_rules(Constraints3, InstanceTable, 
 		Tvarset0, Tvarset1, Proofs1, Proofs2, Constraints4, Changed3),
 	(
@@ -3238,19 +3240,21 @@
 			Proofs, NewConstraints)
 	).
 
-	% To reduce the context using class declarations, we scan the 
-	% context one constraint at a time. For each class in the constraint,
-	% we check to see if any of its superclasses is also a constraint, and 
-	% if so, delete the superclass from the constraint list as it is
-	% redundant.
-:- pred apply_class_rules(list(class_constraint), class_table,
-	tvarset, map(class_constraint, constraint_proof),
+	% To reduce the context using class declarations, we scan the
+	% declared contexts plus the current inferred context one
+	% constraint at a time.  For each such class constraint, we
+	% check to see if any of its superclasses is also a constraint,
+	% and if so, delete the superclass from the current constraint
+	% list as it is redundant.
+:- pred apply_class_rules(list(class_constraint), list(class_constraint),
+	class_table, tvarset, map(class_constraint, constraint_proof),
 	map(class_constraint, constraint_proof), list(class_constraint), bool).
-:- mode apply_class_rules(in, in, in, in, out, out, out) is det.
+:- mode apply_class_rules(in, in, in, in, in, out, out, out) is det.
 
-apply_class_rules(Constraints0, ClassTable, TVarSet, 
+apply_class_rules(Constraints0, DeclaredConstraints, ClassTable, TVarSet, 
 		Proofs0, Proofs, Constraints, Changed) :-
-	apply_class_rules_2(Constraints0, Constraints0, ClassTable,
+	list__append(DeclaredConstraints, Constraints0, AllConstraints),
+	apply_class_rules_2(AllConstraints, Constraints0, ClassTable,
 		TVarSet, Proofs0, Proofs, Constraints, Changed).
 
 :- pred apply_class_rules_2(list(class_constraint), list(class_constraint),
@@ -3258,12 +3262,13 @@
 	map(class_constraint, constraint_proof), list(class_constraint), bool).
 :- mode apply_class_rules_2(in, in, in, in, in, out, out, out) is det.
 
-	% The first argument is the list of constraints left to be checked.
-	% The second argument is the list of constraints that have not been
-	% rejected. If a redundant constraint is found, it is deleted from
-	% both (if it is still in the first list).
+	% The first argument is the list of declared or inferred constraints
+	% left to be checked.
+	% The second argument is the list of currently inferred constraints
+	% that have not been rejected. If a redundant constraint is found,
+	% it is deleted from both (if it is still in the first list).
 apply_class_rules_2([], Constraints, _, _, Proofs, Proofs, Constraints, no).
-apply_class_rules_2([C|Cs], AllConstraints, ClassTable, TVarSet,
+apply_class_rules_2([C|Cs], Constraints0, ClassTable, TVarSet,
 		Proofs0, Proofs, Constraints, Changed) :-
 	C = constraint(ClassName, Types),
 	list__length(Types, Arity),
@@ -3283,14 +3288,13 @@
 			type_list_subsumes(NewClassTypes, Types, Subst),
 			apply_rec_subst_to_constraint(Subst, ThisConstraint, 
 				RenamedConstraint),
-			list__member(RenamedConstraint, AllConstraints)
+			list__member(RenamedConstraint, Constraints0)
 		)),
 	list__filter_map(IsRedundant, ParentClassConstraints,
 		RedundantConstraints),
 
 		% Delete the redundant constraints
-	list__delete_elems(AllConstraints, RedundantConstraints,
-		NewConstraints),
+	list__delete_elems(Constraints0, RedundantConstraints, Constraints1),
 	list__delete_elems(Cs, RedundantConstraints, NewCs),
 
 		% Remember why the constraints were redundant
@@ -3309,7 +3313,7 @@
 		Changed1 = yes
 	),
 
-	apply_class_rules_2(NewCs, NewConstraints, ClassTable,
+	apply_class_rules_2(NewCs, Constraints1, ClassTable,
 		NewTVarSet, Proofs1, Proofs, Constraints, Changed2),
 	bool__or(Changed1, Changed2, Changed).
 


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