[m-rev.] for review: fix typeclass bug

[Simon Taylor]

Estimated hours taken: 5
Branches: main

compiler/typecheck.m:
	Fix a bug in the handling of superclass constraints where
	some of the argument variables of the subclass don't appear
	in the superclass constraint, such as in class `bar' below.
	:- typeclass foo(T, U) <= bar(T, U).
	:- typeclass bar(T, U) <= baz(T).

	When calling a method of baz with a universal constraint in
	the predicate declaration of foo(A, B), the variable B
	was not being substituted correctly in the constraint
	proofs, resulting in an abort in polymorphism.

	Simplify the code by separating out some complicated
	lambdas into separate predicates.

tests/hard_coded/typeclasses/Mmakefile:
tests/hard_coded/typeclasses/superclass_bug3.{m,exp}:
	Test case.

Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.323
diff -u -u -r1.323 typecheck.m
--- compiler/typecheck.m	26 Jul 2002 06:33:12 -0000	1.323
+++ compiler/typecheck.m	26 Jul 2002 06:48:16 -0000
@@ -4487,7 +4487,7 @@
 		Constraints, Changed) :-
 	(
 		Parents = [],
-		eliminate_constraint_by_class_rules(C, HeadTypeParams, 
+		eliminate_constraint_by_class_rules(C, _, _, HeadTypeParams, 
 			AssumedConstraints,
 			SuperClassTable, TVarSet, Parents, Proofs0, Proofs1)
 	->
@@ -4512,15 +4512,16 @@
 	% original constraint that we are trying to prove. (These are the
 	% type variables that must not be bound as we search through the
 	% superclass relation).
-:- pred eliminate_constraint_by_class_rules(class_constraint, list(tvar),
+:- pred eliminate_constraint_by_class_rules(class_constraint, class_constraint,
+	tsubst, list(tvar),
 	list(class_constraint), superclass_table, tvarset,
 	list(class_constraint),
 	map(class_constraint, constraint_proof),
 	map(class_constraint, constraint_proof)).
-:- mode eliminate_constraint_by_class_rules(in, in, in, in, in, in, in, out) 
-	is semidet.
+:- mode eliminate_constraint_by_class_rules(in, out, out,
+	in, in, in, in, in, in, out) is semidet.
 
-eliminate_constraint_by_class_rules(C, ConstVars,
+eliminate_constraint_by_class_rules(C, SubstC, SubClassSubst, ConstVars,
 		AssumedConstraints, SuperClassTable,
 		TVarSet, ParentConstraints, Proofs0, Proofs) :-
 
@@ -4536,60 +4537,21 @@
 		% Convert all the subclass_details into class_constraints by
 		% doing the appropriate variable renaming and applying the
 		% type variable bindings.
-	SubDetailsToConstraint = (pred(SubClassDetails::in, SubC::out) 
-			is det :-
-		SubClassDetails = subclass_details(SuperVars0, SubID,
-			SubVars0, SuperVarset),
-
-			% Rename the variables from the typeclass
-			% declaration into those of the current pred
-		varset__merge_subst(TVarSet, SuperVarset, _NewTVarSet, 
-			RenameSubst),
-		term__var_list_to_term_list(SubVars0, SubVars1),
-		term__apply_substitution_to_list(SubVars1, 
-			RenameSubst, SubVars),
-		term__apply_substitution_to_list(SuperVars0,
-			RenameSubst, SuperVars),
-
-			% Work out what the (renamed) vars from the
-			% typeclass declaration are bound to here
-		map__init(Empty),
-		(
-			type_unify_list(SuperVars, SuperClassTypes, [],
-				Empty, Bindings)
-		->
-			SubID = class_id(SubName, _SubArity),
-			term__apply_substitution_to_list(SubVars, Bindings,
-				SubClassTypes),
-			SubC = constraint(SubName, SubClassTypes)
-		;
-			error("eliminate_constraint_by_class_rules: type_unify_list failed")
-		)
-	),
-	list__map(SubDetailsToConstraint, SubClasses, SubClassConstraints),
+	list__map(subclass_details_to_constraint(TVarSet, SuperClassTypes),
+		SubClasses, SubClassConstraints),
 
 	(
 			% Do the first level of search. We search for
 			% an assumed constraint which unifies with any
 			% of the subclass constraints.
-		FindSub = (pred(TheConstraint::in) is semidet :-
-			some [SubClassConstraint] (
-				TheConstraint = constraint(TheConstraintClass,
-					TheConstraintTypes),
-				list__member(SubClassConstraint, 
-					SubClassConstraints),
-				SubClassConstraint = 
-					constraint(TheConstraintClass, 
-					SubClassConstraintTypes),
-				map__init(EmptySub),
-				type_unify_list(SubClassConstraintTypes, 
-					TheConstraintTypes,
-					ConstVars, EmptySub, _)
-			)
-		),
-		find_first_match(FindSub, AssumedConstraints, Sub)
+		find_first(
+			match_assumed_constraint(ConstVars,
+				SubClassConstraints),
+			AssumedConstraints, SubClass - SubClassSubst0)
 	->
-		map__set(Proofs0, C, superclass(Sub), Proofs)
+		SubClassSubst = SubClassSubst0,
+		apply_rec_subst_to_constraint(SubClassSubst, C, SubstC),
+		map__set(Proofs0, SubstC, superclass(SubClass), Proofs)
 	;
 		NewParentConstraints = [C|ParentConstraints],
 
@@ -4598,18 +4560,43 @@
 		SubClassSearch = (pred(Constraint::in, CnstrtAndProof::out) 
 				is semidet :-
 			eliminate_constraint_by_class_rules(Constraint, 
+				SubstConstraint, SubClassSubst0,
 				ConstVars, AssumedConstraints, SuperClassTable,
 				TVarSet, NewParentConstraints,
 				Proofs0, SubProofs),
-			CnstrtAndProof = Constraint - SubProofs
+			CnstrtAndProof = {SubstConstraint,
+				SubClassSubst0, SubProofs}
 		),
 			% XXX this could (and should) be more efficient. 
 			% (ie. by manually doing a "cut").
 		find_first(SubClassSearch, SubClassConstraints,
-			NewSub - NewProofs),
-		map__set(NewProofs, C, superclass(NewSub), Proofs)
+			{NewSubClass, SubClassSubst, NewProofs}),
+		apply_rec_subst_to_constraint(SubClassSubst, C, SubstC),
+		map__set(NewProofs, SubstC, superclass(NewSubClass), Proofs)
 	).
 
+:- pred match_assumed_constraint(list(tvar)::in, list(class_constraint)::in,
+	class_constraint::in, pair(class_constraint, tsubst)::out) is semidet.
+
+match_assumed_constraint(ConstVars, SubClassConstraints,
+		AssumedConstraint, Match) :-
+	find_first(match_assumed_constraint_2(ConstVars, AssumedConstraint), 
+		SubClassConstraints, Match).
+
+:- pred match_assumed_constraint_2(list(tvar)::in, class_constraint::in,
+	class_constraint::in, pair(class_constraint, tsubst)::out) is semidet.
+
+match_assumed_constraint_2(ConstVars, AssumedConstraint,
+		SubClassConstraint, Match) :-
+	AssumedConstraint = constraint(AssumedConstraintClass,
+		AssumedConstraintTypes),
+	SubClassConstraint = constraint(AssumedConstraintClass,
+		SubClassConstraintTypes),
+	map__init(EmptySub),
+	type_unify_list(SubClassConstraintTypes, AssumedConstraintTypes,
+		ConstVars, EmptySub, AssumedConstraintSub),
+	Match = AssumedConstraint - AssumedConstraintSub.
+
 	% XXX this should probably work its way into the library.
 	% This is just like list__filter_map except that it only returns
 	% the first match:
@@ -4638,6 +4625,39 @@
 		Result = X
 	;
 		find_first_match(Pred, Xs, Result)
+	).
+
+:- pred subclass_details_to_constraint(tvarset::in, list(type)::in,
+		subclass_details::in, class_constraint::out) is det.
+
+subclass_details_to_constraint(TVarSet, SuperClassTypes,
+			SubClassDetails, SubC) :-
+	SubClassDetails = subclass_details(SuperVars0, SubID,
+		SubVars0, SuperVarset),
+
+		% Rename the variables from the typeclass
+		% declaration into those of the current pred
+	varset__merge_subst(TVarSet, SuperVarset, _NewTVarSet, 
+		RenameSubst),
+	term__var_list_to_term_list(SubVars0, SubVars1),
+	term__apply_substitution_to_list(SubVars1, 
+		RenameSubst, SubVars),
+	term__apply_substitution_to_list(SuperVars0,
+		RenameSubst, SuperVars),
+
+		% Work out what the (renamed) vars from the
+		% typeclass declaration are bound to here
+	map__init(Empty),
+	(
+		type_unify_list(SuperVars, SuperClassTypes, [],
+			Empty, Bindings)
+	->
+		SubID = class_id(SubName, _SubArity),
+		term__apply_substitution_to_list(SubVars, Bindings,
+			SubClassTypes),
+		SubC = constraint(SubName, SubClassTypes)
+	;
+		error("eliminate_constraint_by_class_rules: type_unify_list failed")
 	).
 
 	%
Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.45
diff -u -u -r1.45 Mmakefile
--- tests/hard_coded/typeclasses/Mmakefile	26 Jul 2002 06:33:18 -0000	1.45
+++ tests/hard_coded/typeclasses/Mmakefile	26 Jul 2002 06:36:29 -0000
@@ -49,6 +49,7 @@
 	reordered_existential_constraint \
 	superclass_bug \
 	superclass_bug2 \
+	superclass_bug3 \
 	superclass_call \
 	test_default_func_mode \
 	tuple_instance \
Index: tests/hard_coded/typeclasses/superclass_bug3.exp
===================================================================
RCS file: tests/hard_coded/typeclasses/superclass_bug3.exp
diff -N tests/hard_coded/typeclasses/superclass_bug3.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/superclass_bug3.exp	26 Jul 2002 05:00:14 -0000
@@ -0,0 +1 @@
+1
Index: tests/hard_coded/typeclasses/superclass_bug3.m
===================================================================
RCS file: tests/hard_coded/typeclasses/superclass_bug3.m
diff -N tests/hard_coded/typeclasses/superclass_bug3.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/superclass_bug3.m	26 Jul 2002 04:59:37 -0000
@@ -0,0 +1,42 @@
+:- module superclass_bug3.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state::di, io__state::uo) is det.
+
+:- implementation.
+
+:- import_module string, std_util.
+
+main -->
+	{ parse_result_entry(unit, 1, unit, String) },
+	io__write_string(String),
+	io__nl.
+
+:- typeclass analysis(FuncInfo, Call, Answer)
+		<= call_pattern(FuncInfo, Call) where [].
+
+:- typeclass call_pattern(FuncInfo, Call) <= to_string(Call) where [].
+
+:- typeclass to_string(S) where [
+		func to_string(S) = string
+	].
+
+:- instance analysis(unit, int, unit) where [].
+:- instance call_pattern(unit, int) where [].
+:- instance to_string(int) where [
+		to_string(S) = string__int_to_string(S)
+].
+
+:- pred parse_result_entry(FuncInfo::in, Call::in,
+	Answer::in, string::out) is det <= analysis(FuncInfo, Call, Answer).
+
+:- implementation.
+
+:- import_module list.
+
+parse_result_entry(_FuncInfo, Call, _Answer, String) :-
+	String = to_string(Call).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------