No subject

Fergus Henderson fjh at cs.mu.OZ.AU
Mon Jun 22 21:21:03 AEST 1998
Previous message: for review: improvement to typeclass error reporting
Next message: your mail
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
Message-ID: <19980622184334.24810 at murlibobo.cs.mu.OZ.AU>
Date: Mon, 22 Jun 1998 18:43:34 +1000
From: Fergus Henderson <fjh at cs.mu.OZ.AU>
To: Mercury Developers <mercury-developers at cs.mu.OZ.AU>
Subject: for review: improvement to typeclass error reporting
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Length: 7749
Lines: 202

DJ, can you please review this one?

Estimated hours taken: 1

compiler/typecheck.m:
	Improve error reporting by checking type class constraints for
	satisfiability as we go and thus reporting unsatisfiable constraints
	as soon as possible, rather than only at the end of the clause.
	Previously we already did that for the case of ground constraints,
	but they are not the only unsatsfiable constraints: constraints
	on head type params (type variables which cannot be bound) are
	also unsatisfiable if they can't be eliminated straight away
	by context reduction.

tests/invalid/Mmakefile:
tests/invalid/typeclass_test_7.m:
tests/invalid/typeclass_test_7.err_exp:
	Regression test for the above change.

Index: compiler/typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.240.2.6
diff -u -r1.240.2.6 typecheck.m
--- typecheck.m	1998/06/20 19:55:50	1.240.2.6
+++ typecheck.m	1998/06/22 07:56:44
@@ -152,7 +152,7 @@
 	map(class_constraint, constraint_proof),
 	list(class_constraint), list(class_constraint)).
 :- mode typecheck__reduce_context_by_rule_application(in, in, in, in, in, out, 
-	in, out, in, out) is semidet.
+	in, out, in, out) is det.
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -3209,8 +3209,9 @@
 
 reduce_type_assign_context(SuperClassTable, InstanceTable, 
 		TypeAssign0, TypeAssign) :-
-	type_assign_get_typeclass_constraints(TypeAssign0, Constraints0),
+	type_assign_get_head_type_params(TypeAssign0, HeadTypeParams),
 	type_assign_get_type_bindings(TypeAssign0, Bindings),
+	type_assign_get_typeclass_constraints(TypeAssign0, Constraints0),
 	type_assign_get_typevarset(TypeAssign0, Tvarset0),
 	type_assign_get_constraint_proofs(TypeAssign0, Proofs0),
 
@@ -3221,6 +3222,8 @@
 		Bindings, Tvarset0, Tvarset, Proofs0, Proofs,
 		UnprovenConstraints0, UnprovenConstraints),
 
+	check_satisfiability(UnprovenConstraints, HeadTypeParams),
+
 	Constraints = constraints(AssumedConstraints, UnprovenConstraints),
 
 	type_assign_set_typeclass_constraints(TypeAssign0, Constraints,
@@ -3274,7 +3277,7 @@
 :- pred apply_instance_rules(list(class_constraint), instance_table,
 	tvarset, tvarset, map(class_constraint, constraint_proof),
 	map(class_constraint, constraint_proof), list(class_constraint), bool).
-:- mode apply_instance_rules(in, in, in, out, in, out, out, out) is semidet.
+:- mode apply_instance_rules(in, in, in, out, in, out, out, out) is det.
 
 apply_instance_rules([], _, Names, Names, Proofs, Proofs, [], no).
 apply_instance_rules([C|Cs], InstanceTable, TVarSet, NewTVarSet,
@@ -3293,24 +3296,6 @@
 		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,
@@ -3506,6 +3491,50 @@
 		Result = Result0
 	;
 		find_first(Pred, Xs, Result)
+	).
+
+	%
+	% check_satisfiability(Constraints, HeadTypeParams):
+	% 	Check that all of the constraints are satisfiable.
+	%	Fail if any are definitely not satisfiable.
+	%
+	% 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 satisfiability.
+	%
+	% Similarly, for constraints on head type params
+	% (universally quantified type vars in the head of this pred,
+	% or existentially quantified type vars in callees),
+	% we know that the head type params can never get bound.
+	% This means that if the constraint wasn't an assumed constraint
+	% and can't be eliminated by instance rule or class rule
+	% application, then we can report an error now, rather than
+	% later.  (For non-head-type-param type variables,
+	% we need to wait, in case the type variable gets bound
+	% to a type for which there is a valid instance declaration.)
+	%
+	% So a constraint is considered satisfiable iff it
+	% contains at least one type variable that is not in the
+	% head type params.
+	%
+:- pred check_satisfiability(list(class_constraint), head_type_params).
+:- mode check_satisfiability(in, in) is semidet.
+
+check_satisfiability(Constraints, HeadTypeParams) :-
+	all [C] list__member(C, Constraints) => (
+		C = constraint(_ClassName, Types),
+		term__contains_var_list(Types, TVar),
+		not list__member(TVar, HeadTypeParams)
 	).
 
 %-----------------------------------------------------------------------------%
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.18
diff -u -r1.18 Mmakefile
--- Mmakefile	1998/06/06 11:09:57	1.18
+++ Mmakefile	1998/06/22 08:41:21
@@ -46,6 +46,7 @@
 	typeclass_test_2.m \
 	typeclass_test_3.m \
 	typeclass_test_4.m \
+	typeclass_test_7.m \
 	unbound_inst_var.m \
 	undef_lambda_mode.m \
 	undef_mode.m \
Index: tests/invalid/typeclass_test_7.err_exp
===================================================================
RCS file: typeclass_test_7.err_exp
diff -N typeclass_test_7.err_exp
--- /dev/null	Mon Jun 22 18:42:22 1998
+++ typeclass_test_7.err_exp	Mon Jun 22 18:40:31 1998
@@ -0,0 +1,4 @@
+typeclass_test_7.m:010: In clause for predicate `typeclass_test_7:p/2':
+typeclass_test_7.m:010:   unsatisfied typeclass constraint(s):
+typeclass_test_7.m:010:   typeclass_test_7:numbered_type(T).
+For more information, try recompiling with `-E'.
Index: tests/invalid/typeclass_test_7.m
===================================================================
RCS file: typeclass_test_7.m
diff -N typeclass_test_7.m
--- /dev/null	Mon Jun 22 18:42:22 1998
+++ typeclass_test_7.m	Mon Jun 22 18:15:50 1998
@@ -0,0 +1,24 @@
+:- module typeclass_test_7.
+:- interface.
+:- import_module int.
+:- pred p(T::in, int::out) is det.
+
+:- implementation.
+
+p(X, Y) :-
+	F = 42,
+	N = type_num(X),	% error should be reported on *this* line
+	N2 is N * 2,
+	Y = N2 + F.
+
+:- typeclass numbered_type(T) where [
+	func type_num(T) = int
+].
+
+:- instance numbered_type(int) where [
+	func(type_num/1) is foo_type_num
+].
+
+:- func foo_type_num(T) = int.
+foo_type_num(_) = 42.
+
-- 
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.
Previous message: for review: improvement to typeclass error reporting
Next message: your mail
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]
More information about the developers mailing list