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

[David Overton]

On Wed, Mar 12, 2003 at 07:37:14PM +1100, Fergus Henderson wrote:
> On 12-Mar-2003, David Overton <dmo at cs.mu.OZ.AU> wrote:
> > 
> > compiler/typecheck.m:
> > 	In `eliminate_constraint_by_class_rules', if `type_unify_list'
> > 	fails for a subclass, remove that subclass from the list of
> > 	constraints being examined rather than aborting.
> > 	`type_unify_list' may fail if one of the arguments to the
> > 	superclass constraint is not a type variable and does not unify
> > 	with the corresponding argument of the subclass.
> > 	In such cases, this particular superclass-subclass relationship
> > 	is not relevant to the constraint we are trying to prove so it is safe
> > 	to remove it.
> 
> Could you explain in more detail?  Perhaps with an example?
> I'm not yet completely convinced that removing such constraints is safe.

Okay.  See the modified test case below as an example.  When doing
context reduction on the call to unify_oo from graph_unify_oo (in
`typecheck__reduce_context_by_rule_application_2'), the compiler needs to
prove that the constraint `eq(list(arc))' is satisfied.  The first thing
it does is use the instance declaration

	:- instance eq(list(T)) <= eq(T).

to reduce the constraint that needs to be proven to `eq(arc)'.  Then,
before looking for an instance declaration to prove this constraint
(which it would obviously find if it looked for it) it calls
`apply_class_rules' to try to reduce the constraint using superclass
relations.

Eventually it finds the class declaration

	:- class lin_int_solver(T) <= lin_arith_solver(int, T).

which causes it to call `type_unify_list' with the two lists of types
being `[int, T]' and `[T, arc]'.  It does not expect the unification to
fail since in the past all elements of the first list have been distinct
variables, but now that we allow nonvariable arguments in the constraint
on a class declaration this is not the case so the unification does
fail.  However, it should be safe to remove a failing type unification
because it is clearly not going to contribute to our proof of `eq(arc)'.

I'm not sure why the algorithm doesn't try to reduce `eq(arc)' through
instance declarations before looking at subclasses (which would avoid
getting this particular error), but I assume there is some good reason
for it.  If there isn't, I could just change `apply_instance_rules' to
immediately operate on any new constraints it generates, which I think
would fix the problem.  Can someone with more knowledge of typeclasses
comment on what the best approach is?

> 
> > tests/valid/Mmakefile:
> > tests/valid/typeclass_constraint_nonvar_bug.m:
> > 	Test case.
> 
> The test case does not seem to be a proper regression test, since this
> test passes with the existing compiler (I tested with rotd-2003-03-08).

Sorry, I reduced the test case too much.  The test case given aborts
with this error if you leave out the `:- instance eq(cint)...'
declaration, but when you add that in it works.

I have modified it slightly so that the error occurs in a type correct
program.

> 
> > Index: compiler/typecheck.m
> > ===================================================================
> > RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
> > retrieving revision 1.331
> > diff -u -r1.331 typecheck.m
> > --- compiler/typecheck.m	28 Feb 2003 06:40:43 -0000	1.331
> > +++ compiler/typecheck.m	12 Mar 2003 03:50:54 -0000
> > @@ -4629,7 +4629,8 @@
> >  		% Convert all the subclass_details into class_constraints by
> >  		% doing the appropriate variable renaming and applying the
> >  		% type variable bindings.
> > -	list__map(subclass_details_to_constraint(TVarSet, SuperClassTypes),
> > +	list__filter_map(subclass_details_to_constraint(TVarSet,
> > +			SuperClassTypes),
> 
> Please update the comment here.  This is now doing more than just
> converting things, it is also removing some contraints.
> (E.g. with text similar to that in the log message.)

Done.

> 
> >  		SubClasses, SubClassConstraints),
> >  
> >  	(
> > @@ -4720,7 +4721,7 @@
> >  	).
> >  
> >  :- pred subclass_details_to_constraint(tvarset::in, list(type)::in,
> > -		subclass_details::in, class_constraint::out) is det.
> > +		subclass_details::in, class_constraint::out) is semidet.
> 
> Please add some comments here indicating when the procedure will succeed
> and when it will fail.

Done.

New full diff (Interdiff wouldn't work for some reason.  I hope the
change is not too big for a full new diff.):


Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.331
diff -u -r1.331 typecheck.m
--- compiler/typecheck.m	28 Feb 2003 06:40:43 -0000	1.331
+++ compiler/typecheck.m	13 Mar 2003 01:26:50 -0000
@@ -4629,7 +4629,12 @@
 		% Convert all the subclass_details into class_constraints by
 		% doing the appropriate variable renaming and applying the
 		% type variable bindings.
-	list__map(subclass_details_to_constraint(TVarSet, SuperClassTypes),
+		% If the unification of the type variables for a particular
+		% constraint fails then that constraint is eliminated because it
+		% cannot contribute to proving the constraint we are trying to
+		% prove.
+	list__filter_map(subclass_details_to_constraint(TVarSet,
+			SuperClassTypes),
 		SubClasses, SubClassConstraints),
 
 	(
@@ -4719,8 +4724,11 @@
 		find_first_match(Pred, Xs, Result)
 	).
 
+	% subclass_details_to_constraint will fail iff the call to
+	% type_unify_list fails.
+
 :- pred subclass_details_to_constraint(tvarset::in, list(type)::in,
-		subclass_details::in, class_constraint::out) is det.
+		subclass_details::in, class_constraint::out) is semidet.
 
 subclass_details_to_constraint(TVarSet, SuperClassTypes,
 			SubClassDetails, SubC) :-
@@ -4740,17 +4748,11 @@
 		% 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("subclass_details_to_constraint: type_unify_list failed")
-	).
+	type_unify_list(SuperVars, SuperClassTypes, [], Empty, Bindings),
+	SubID = class_id(SubName, _SubArity),
+	term__apply_substitution_to_list(SubVars, Bindings,
+		SubClassTypes),
+	SubC = constraint(SubName, SubClassTypes).
 
 	%
 	% check_satisfiability(Constraints, HeadTypeParams):
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.126
diff -u -r1.126 Mmakefile
--- tests/valid/Mmakefile	22 Feb 2003 13:18:33 -0000	1.126
+++ tests/valid/Mmakefile	13 Mar 2003 01:26:50 -0000
@@ -25,6 +25,7 @@
 	instance_unconstrained_tvar \
 	repeated_class_constraint \
 	typeclass_constraint_no_var \
+	typeclass_constraint_nonvar_bug \
 	typeclass_det_warning
 
 ADITI_PROGS= \
Index: tests/valid/typeclass_constraint_nonvar_bug.m
===================================================================
RCS file: tests/valid/typeclass_constraint_nonvar_bug.m
diff -N tests/valid/typeclass_constraint_nonvar_bug.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/typeclass_constraint_nonvar_bug.m	13 Mar 2003 01:26:50 -0000
@@ -0,0 +1,107 @@
+:- module typeclass_constraint_nonvar_bug.
+
+:- interface.
+
+:- typeclass eq(T) where [
+	pred unify_oo(T::in, T::in) is semidet
+].
+
+:- typeclass add(T) <= eq(T) where [].
+:- typeclass neq(T) <= eq(T) where [].
+:- typeclass ord(T) <= eq(T) where [].
+:- typeclass mult(T) <= add(T) where [].
+:- typeclass sord(T) <= ord(T) where [].
+:- typeclass strict(T) <= (neq(T),sord(T)) where [].
+:- typeclass arith(T) <= (mult(T),strict(T)) where [].
+
+:- typeclass solver(T) <= eq(T) where [].
+
+:- typeclass solver_for(B, S) <= solver(S) where [].
+:- typeclass lin_mult(B, S) <= arith(B) where [].
+:- typeclass lin_arith_solver(B, S) <=
+	(add(S), ord(S), solver(S), lin_mult(B, S), solver_for(B, S)) where [].
+:- typeclass arith_solver(B, S) <= (arith(S), lin_arith_solver(B, S)) where [].
+
+:- typeclass lin_int_solver(T) <= lin_arith_solver(int, T) where [].
+:- typeclass int_solver(T) <= (arith(T), lin_int_solver(T)) where [].
+
+:- instance eq(int) where [
+	pred(unify_oo/2) is int_unify_oo
+].
+
+:- instance add(int) where [].
+:- instance neq(int) where [].
+:- instance ord(int) where [].
+:- instance mult(int) where [].
+:- instance sord(int) where [].
+:- instance strict(int) where [].
+:- instance arith(int) where [].
+
+:- type cint ---> a ; b.
+
+:- instance eq(cint) where [
+	pred(unify_oo/2) is cint_unify_oo
+].
+
+:- instance add(cint) where [].
+:- instance neq(cint) where [].
+:- instance ord(cint) where [].
+:- instance mult(cint) where [].
+:- instance sord(cint) where [].
+:- instance strict(cint) where [].
+:- instance arith(cint) where [].
+
+:- instance solver(cint) where [].
+
+:- instance solver_for(int, cint) where [].
+:- instance lin_mult(int, cint) where [].
+:- instance lin_arith_solver(int, cint) where [].
+:- instance arith_solver(int, cint) where [].
+
+:- instance lin_int_solver(cint) where [].
+:- instance int_solver(cint) where [].
+
+
+:- type list(T) ---> [] ; [T | list(T)].
+:- instance eq(list(T)) <= eq(T) where [
+	pred(unify_oo/2) is list_unify_oo
+].
+
+:- type arc ---> arc(int, int).
+:- instance eq(arc) where [
+	pred(unify_oo/2) is arc_unify_oo
+].
+
+:- type graph ---> graph(list(arc)).
+:- instance eq(graph) where [
+	pred(unify_oo/2) is graph_unify_oo
+].
+
+
+:- pred int_unify_oo(int::in, int::in) is semidet.
+
+:- pred cint_unify_oo(cint::in, cint::in) is semidet.
+
+:- pred list_unify_oo(list(T)::in, list(T)::in) is semidet <= eq(T).
+
+:- pred arc_unify_oo(arc::in, arc::in) is semidet.
+
+:- pred graph_unify_oo(graph::in, graph::in) is semidet.
+
+:- implementation.
+
+int_unify_oo(X, X).
+
+cint_unify_oo(X, X).
+
+list_unify_oo([], []).
+list_unify_oo([X | Xs], [Y | Ys]) :-
+	unify_oo(X, Y),
+	list_unify_oo(Xs, Ys).
+
+arc_unify_oo(arc(X1, Y1), arc(X2, Y2)) :-
+	unify_oo(X1, X2),
+	unify_oo(Y1, Y2).
+
+graph_unify_oo(graph(As1), graph(As2)) :-
+	unify_oo(As1, As2).

-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------