[m-rev.] for review: functional dependencies (3/3)

Mark Brown mark at cs.mu.OZ.AU
Wed Apr 20 17:23:57 AEST 2005


Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.312
diff -u -r1.312 reference_manual.texi
--- doc/reference_manual.texi	15 Apr 2005 15:14:33 -0000	1.312
+++ doc/reference_manual.texi	17 Apr 2005 17:49:19 -0000
@@ -51,6 +51,7 @@
 @author Chris Speirs
 @author Tyson Dowd
 @author Ralph Becket
+ at author Mark Brown
 @page
 @vskip 0pt plus 1filll
 Copyright @copyright{} 1995--2005 The University of Melbourne.
@@ -4559,6 +4560,7 @@
 * Type class constraints on predicates and functions::
 * Type class constraints on type class declarations::
 * Type class constraints on instance declarations::
+* Functional dependencies::
 @end menu
 
 @node Typeclass declarations
@@ -4576,6 +4578,12 @@
 it is defining, the
 names of the type variables which are parameters to the type class, and the
 operations (i.e.@: methods) which form the interface of the type class.
+For each method, all parameters of the typeclass must be determined by
+the type variables appearing in the type signature of the method.
+A variable is determined by a type signature if it appears in the
+type signature, but if functional dependencies are present
+then it may also be determined from other variables
+(@pxref{Functional dependencies}).
 
 For example,
 
@@ -4898,8 +4906,12 @@
 @noindent
 where @var{Typeclass} is the name of a type class and @var{Type} is 
 a type.
-Any variable that appears in @var{Type} must also appear in
+Any variable that appears in @var{Type} must be determined by
 the predicate's or function's type signature.
+A variable is determined by a type signature if it appears in the
+type signature, but if functional dependencies are present
+then it may also be determined from other variables
+(@pxref{Functional dependencies}).
 Each type class constraint in a predicate or function declaration must contain
 at least one variable.
 
@@ -5024,6 +5036,146 @@
 constraints on the corresponding non-abstract instance declaration that
 defines that instance.
 @c XXX The current implementation does not enforce that rule.
+
+ at node Functional dependencies
+ at section Functional dependencies
+
+Type classes may be defined to have functional dependencies between arguments.
+There may be any number of functional dependencies on one typeclass.
+Each constraint is expressed with the same syntax as typeclass constraints
+on typeclass declarations, using a special constraint of the form
+ at code{(@var{Domain} -> @var{Range})}.
+
+The @var{Domain} and @var{Range} arguments are either single type variables,
+or conjunctions of type variables separated by commas.
+
+ at example
+	:- typeclass @var{Typeclass}(@var{Var}, @dots{})@
+<= ((@var{D} -> @var{R}), @dots{}) @dots{}
+
+	:- typeclass @var{Typeclass}(@var{Var}, @dots{})@
+<= (@var{D1}, @var{D2}, @dots{} -> @var{R1}, @var{R2}, @dots{}), @dots{}
+ at end example
+
+Each type variable must appear in the parameter list of the typeclass.
+Abstract typeclass declarations must have exactly the same functional
+dependencies as in the implementation.
+
+Mutually recursive functional dependencies are allowed,
+so the following examples are legal:
+
+ at example
+	:- typeclass foo(A, B) <= ((A -> B), (B -> A)).
+	:- typeclass bar(A, B, C, D)@
+<= ((A, B -> C), (B, C -> D), (D -> A, C)).
+ at end example
+
+A functional dependency on a typeclass places an additional requirement
+on the set of instances which are allowed for that type class.
+The requirement is that all types bound to variables in the range of the
+functional dependency must be able to be uniquely determined by the types
+bound to variables in the domain of the functional dependency.
+If more than one functional dependency is present,
+then the requirement for each one must be satisfied.
+
+For example, given the typeclass declaration
+
+ at example
+	:- typeclass baz(A, B) <= (A -> B) where @dots{}
+ at end example
+
+ at noindent
+it would be illegal to have both of the instances
+
+ at example
+	:- instance baz(int, int) where @dots{}
+	:- instance baz(int, string) where @dots{}
+ at end example
+
+ at noindent
+although either one would be acceptable on its own.
+
+The following instance would also be illegal
+
+ at example
+	:- instance baz(string, list(T)) where @dots{}
+ at end example
+
+ at noindent
+since the variable @samp{T} may not always be bound to the same type.
+
+The extra requirements that result from the use of functional dependencies
+allow the bindings of some variables to be determined from the bindings
+of others.  This in turn relaxes some of the requirements on typeclass
+constraints on predicate and function signatures.
+
+Without any functional dependencies, all variables in constraints must
+appear in the signature of the predicate or function being declared.
+However, variables which are in the range of a functional dependency need
+not appear in the signature, since it is known that their bindings will
+be determined from the bindings of the variables in the domain.
+
+More formally, the constraints on a predicate or function signature
+ at emph{induce} a set of functional dependencies on the variables appearing
+in those constraints.  A functional dependency
+ at samp{(A1, @dots{} -> B1, @dots{})} is induced from a constraint
+ at samp{@var{Typeclass}(@var{Type1}, @dots{})} if and only if the typeclass
+ at samp{@var{Typeclass}} has a functional dependency
+ at samp{(D1, @dots{} -> R1, @dots{})},
+and for each typeclass parameter @samp{Di} there exists an @samp{Aj}
+every type variable appearing in the @samp{@var{Typek}}
+corresponding to @samp{Di},
+and each @samp{Bi} appears in the @samp{@var{Typej}} bound to the typeclass
+parameter @samp{Rk} for some @var{k}.
+
+For example, with the definition of @code{baz} above, the constraint
+ at code{baz(map(X, Y), list(Z))} induces the constraint @code{(X, Y -> Z)},
+since @var{X} and @var{Y} appear in the domain argument, and @var{Z} appears
+in the range argument.
+
+The set of type variables determined from a signature is
+the @emph{closure} of the set appearing in the signature
+under the functional dependencies induced from the constraints.
+The closure is defined as the smallest set of variables which includes
+all of the variables appearing in the signature,
+and is such that, for each induced functional dependency
+ at samp{@var{Domain} -> @var{Range}},
+if the closure includes all of the variables in @var{Domain} then it
+includes all of the variables in @var{Range}.
+
+For example, the declaration
+
+ at example
+	:- pred p(X, Y) <= baz(map(X, Y), list(Z)).
+ at end example
+
+ at noindent
+is acceptable since the closure of @{@var{X}, @var{Y}@} under the
+induced functional dependency must include @var{Z}.
+Moreover, the typeclass @code{baz/2} would be allowed to have a method
+that only uses the first parameter, @var{A}, since the second parameter,
+ at var{B}, would always be determined from the first.
+
+The presence of functional dependencies also allows ``improvement'' to
+occur during type inference.  This can occur in two ways.
+First, if two constraints of a given class match on all of the domain
+arguments of a functional dependency on that class,
+then it can be inferred that they also match on the range arguments.
+For example, given the constraints @code{baz(A, B1)} and @code{baz(A, B2)},
+it will be inferred that @code{B1 = B2}.
+
+Similarly, if a constraint of a given class is subsumed by a known instance
+of that class in the domain arguments, then its range arguments can be
+unified with the corresponding instance range arguments.
+For example, given the instance:
+
+ at example
+	:- instance baz(list(T), string) where @dots{}
+ at end example
+
+ at noindent
+then the constraint @code{baz(list(int), X)} can be improved with the
+inference that @code{X = string}.
 
 @node Existential types
 @chapter Existential types
Index: tests/hard_coded/typeclasses/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/typeclasses/Mercury.options,v
retrieving revision 1.1
diff -u -r1.1 Mercury.options
--- tests/hard_coded/typeclasses/Mercury.options	17 Aug 2002 13:52:18 -0000	1.1
+++ tests/hard_coded/typeclasses/Mercury.options	16 Apr 2005 15:09:12 -0000
@@ -8,6 +8,7 @@
 MCFLAGS-intermod_typeclass_bug = --intermodule-optimization
 MCFLAGS-intermod_typeclass_bug2 = --intermodule-optimization
 MCFLAGS-lambda_multi_constraint_same_tvar = --infer-all
+MCFLAGS-no_fundep_infer = --infer-all
 
 	# Check that the exported specialized versions are still created.
 MCFLAGS-type_spec_2 = --no-user-guided-type-specialization
Index: tests/hard_coded/typeclasses/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/hard_coded/typeclasses/Mmakefile,v
retrieving revision 1.53
diff -u -r1.53 Mmakefile
--- tests/hard_coded/typeclasses/Mmakefile	4 Mar 2005 05:55:52 -0000	1.53
+++ tests/hard_coded/typeclasses/Mmakefile	17 Apr 2005 15:39:54 -0000
@@ -9,6 +9,7 @@
 	arbitrary_constraint_pred_2 \
 	arbitrary_constraint_pred_1 \
 	complicated_constraint \
+	complicated_fundeps \
 	constrained_lambda \
 	extract_typeinfo \
 	exist_disjunction \
@@ -19,6 +20,9 @@
 	existential_type_switch \
 	extra_typeinfo \
 	func_default_mode_bug \
+	fundeps_1 \
+	fundeps_2 \
+	fundeps_3 \
 	ground_constraint \
 	ground_constraint_2 \
 	ho_map \
@@ -42,6 +46,7 @@
 	multi_moded \
 	multi_parameter \
 	multi_parameter_bug \
+	no_fundep_infer \
 	nondet_class_method \
 	operator_classname \
 	record_syntax \
Index: tests/hard_coded/typeclasses/complicated_fundeps.exp
===================================================================
RCS file: tests/hard_coded/typeclasses/complicated_fundeps.exp
diff -N tests/hard_coded/typeclasses/complicated_fundeps.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/complicated_fundeps.exp	17 Apr 2005 15:41:09 -0000
@@ -0,0 +1,2 @@
+test(1): yes
+test(2): no
Index: tests/hard_coded/typeclasses/complicated_fundeps.m
===================================================================
RCS file: tests/hard_coded/typeclasses/complicated_fundeps.m
diff -N tests/hard_coded/typeclasses/complicated_fundeps.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/complicated_fundeps.m	17 Apr 2005 15:40:33 -0000
@@ -0,0 +1,60 @@
+:- module complicated_fundeps.
+:- interface.
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+:- import_module int, string.
+
+main(!IO) :-
+	write_string("test(1): ", !IO),
+	(
+		test(1)
+	->
+		write_string("yes\n", !IO)
+	;
+		write_string("no\n", !IO)
+	),
+	write_string("test(2): ", !IO),
+	(
+		test(2)
+	->
+		write_string("yes\n", !IO)
+	;
+		write_string("no\n", !IO)
+	).
+
+:- typeclass a(A, B, C, D) <= ((A -> B), (C -> D)) where [
+	func f(A, C) = B,
+	func g(A) = C
+].
+
+:- typeclass b(A, B) <= (A -> B) where [
+	func h(B) = A,
+	func ii = A
+].
+
+:- pred test(A) <= (a(A, B, C, D), b(B, C)).
+:- mode test(in) is semidet.
+
+test(A) :-
+	C = g(A),
+	B = h(C),
+	f(A, C) = B.
+
+:- instance a(int, int, int, int) where [
+	(f(M, N) = M + N),
+	(g(M) = M)
+].
+
+:- instance a(int, int, string, int) where [
+	(f(M, S) = M + length(S)),
+	(g(_) = "7")
+].
+
+:- instance b(int, int) where [
+	(h(N) = N + 1),
+	(ii = 2)
+].
+
Index: tests/hard_coded/typeclasses/fundeps_1.exp
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_1.exp
diff -N tests/hard_coded/typeclasses/fundeps_1.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_1.exp	17 Apr 2005 08:35:28 -0000
@@ -0,0 +1 @@
+yes
Index: tests/hard_coded/typeclasses/fundeps_1.m
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_1.m
diff -N tests/hard_coded/typeclasses/fundeps_1.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_1.m	17 Apr 2005 08:34:22 -0000
@@ -0,0 +1,37 @@
+:- module fundeps_1.
+:- interface.
+:- import_module io.
+:- pred main(io::di, io::uo) is det.
+:- implementation.
+:- import_module list.
+
+main(!S) :-
+	(
+		test([0], 1)
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	).
+
+:- typeclass coll(C, E) <= (C -> E) where [
+	func e = C,
+	func i(C, E) = C,
+	pred m(E::in, C::in) is semidet
+].
+
+:- type intcoll == list(int).
+
+:- instance coll(intcoll, int) where [
+	(e = []),
+	(i(Ns, N) = [N | Ns]),
+	m(N, [N | _]),
+	m(N, [_ | Ns]) :- m(N, Ns)
+].
+
+:- pred test(C, E) <= coll(C, E).
+:- mode test(in, in) is semidet.
+
+test(C, E) :-
+	m(E, i(C, E)).
+
Index: tests/hard_coded/typeclasses/fundeps_2.exp
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_2.exp
diff -N tests/hard_coded/typeclasses/fundeps_2.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_2.exp	17 Apr 2005 08:37:44 -0000
@@ -0,0 +1,2 @@
+yes
+no
Index: tests/hard_coded/typeclasses/fundeps_2.m
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_2.m
diff -N tests/hard_coded/typeclasses/fundeps_2.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_2.m	17 Apr 2005 08:37:17 -0000
@@ -0,0 +1,47 @@
+:- module fundeps_2.
+:- interface.
+:- import_module io.
+:- pred main(io::di, io::uo) is det.
+:- implementation.
+:- import_module list.
+
+main(!S) :-
+	(
+		test([0], 1)
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	),
+	(
+		e = [1]
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	).
+
+:- typeclass foo(T) where [].
+:- instance foo(int) where [].
+
+:- typeclass coll(C, E) <= ((C -> E), foo(E)) where [
+	func e = C,
+	func i(C, E) = C,
+	pred m(E::in, C::in) is semidet
+].
+
+:- type intcoll == list(int).
+
+:- instance coll(intcoll, int) where [
+	(e = []),
+	(i(Ns, N) = [N | Ns]),
+	m(N, [N | _]),
+	m(N, [_ | Ns]) :- m(N, Ns)
+].
+
+:- pred test(C, E) <= coll(C, E).
+:- mode test(in, in) is semidet.
+
+test(C, E) :-
+	m(E, i(C, E)).
+
Index: tests/hard_coded/typeclasses/fundeps_3.exp
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_3.exp
diff -N tests/hard_coded/typeclasses/fundeps_3.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_3.exp	17 Apr 2005 15:34:36 -0000
@@ -0,0 +1 @@
+yes
Index: tests/hard_coded/typeclasses/fundeps_3.m
===================================================================
RCS file: tests/hard_coded/typeclasses/fundeps_3.m
diff -N tests/hard_coded/typeclasses/fundeps_3.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/fundeps_3.m	17 Apr 2005 15:33:56 -0000
@@ -0,0 +1,24 @@
+:- module fundeps_3.
+:- interface.
+:- import_module io.
+:- pred main(io::di, io::uo) is det.
+:- implementation.
+:- import_module list.
+
+main(!S) :-
+	(
+		e = 1
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	).
+
+:- typeclass coll(C, E) <= (C -> E) where [
+	func e = C
+].
+
+:- instance coll(int, int) where [
+	(e = 1)
+].
+
Index: tests/hard_coded/typeclasses/no_fundep_infer.exp
===================================================================
RCS file: tests/hard_coded/typeclasses/no_fundep_infer.exp
diff -N tests/hard_coded/typeclasses/no_fundep_infer.exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/no_fundep_infer.exp	16 Apr 2005 15:10:43 -0000
@@ -0,0 +1 @@
+[1, 2]
Index: tests/hard_coded/typeclasses/no_fundep_infer.m
===================================================================
RCS file: tests/hard_coded/typeclasses/no_fundep_infer.m
diff -N tests/hard_coded/typeclasses/no_fundep_infer.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/hard_coded/typeclasses/no_fundep_infer.m	16 Apr 2005 15:09:29 -0000
@@ -0,0 +1,31 @@
+% Compile with '--infer-all'
+
+:- module no_fundep_infer.
+:- interface.
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+
+main(!IO) :-
+	io.write(g([]), !IO),
+	io.nl(!IO).
+
+:- typeclass coll(E, C) where [
+	func i(E, C) = C
+].
+
+:- type intlist ---> [] ; [int | intlist].
+:- type stringlist ---> [] ; [string | stringlist].
+
+:- instance coll(string, intlist) where [ (i(_S, L) = [1 | L]) ].
+:- instance coll(int, intlist) where [ (i(N, L) = [N | L]) ].
+:- instance coll(string, stringlist) where [ (i(S, L) = [S | L]) ].
+
+:- func g(intlist) = intlist.
+
+g(L) = f("foo", 2, L).
+
+f(A, B, C) = i(A, i(B, C)).
+
Index: tests/invalid/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mercury.options,v
retrieving revision 1.9
diff -u -r1.9 Mercury.options
--- tests/invalid/Mercury.options	20 Feb 2004 03:00:14 -0000	1.9
+++ tests/invalid/Mercury.options	17 Apr 2005 16:04:34 -0000
@@ -57,8 +57,9 @@
 				--no-automatic-intermodule-optimization
 MCFLAGS-missing_parent_import = --no-intermodule-optimization \
 				--no-automatic-intermodule-optimization
-MCFLAGS-multisoln_func	=	--infer-types
 MCFLAGS-mode_inf	=	--infer-all
+MCFLAGS-mpj1		=	--infer-all
+MCFLAGS-multisoln_func	=	--infer-types
 MCFLAGS-no_exports = 		--halt-at-warn
 MCFLAGS-nonexistent_import =    --no-verbose-make --make nonexistent_import
 MCFLAGS-overloading = 		--no-intermodule-optimization \
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.164
diff -u -r1.164 Mmakefile
--- tests/invalid/Mmakefile	15 Apr 2005 15:14:42 -0000	1.164
+++ tests/invalid/Mmakefile	17 Apr 2005 16:08:25 -0000
@@ -32,6 +32,8 @@
 
 SINGLEMODULE= \
 	after_end_module \
+	ambiguous_method \
+	ambiguous_method_2 \
 	any_mode \
 	any_should_not_match_bound \
 	assert_in_interface \
@@ -53,6 +55,7 @@
 	circ_type2 \
 	circ_type3 \
 	circ_type5 \
+	complex_constraint_err \
 	conflicting_tabling_pragmas \
 	constrained_poly_insts \
 	constructor_warning \
@@ -77,18 +80,21 @@
 	freefree \
 	func_errors \
 	funcs_as_preds \
+	fundeps_vars \
 	ho_default_func_1 \
 	ho_default_func_3 \
 	ho_type_mode_bug \
 	ho_unique_error \
 	illtyped_compare \
 	impure_method_impl \
+	inconsistent_instances \
 	inline_conflict \
 	inst_list_dup \
 	instance_bug \
 	invalid_export_detism \
 	invalid_import_detism \
 	invalid_main \
+	invalid_new \
 	invalid_typeclass \
 	io_in_ite_cond \
 	lambda_syntax_error \
@@ -105,6 +111,9 @@
 	modes_erroneous \
 	mostly_uniq1 \
 	mostly_uniq2 \
+	mpj1 \
+	mpj3 \
+	mpj4 \
 	multimode_dcg \
 	multimode_missing_impure \
 	multimode_syntax \
@@ -125,6 +134,7 @@
 	qualified_cons_id2 \
 	quant_constraint_1 \
 	quant_constraint_2 \
+	range_restrict \
 	record_syntax_errors \
 	some \
 	spurious_mode_error \
@@ -147,6 +157,7 @@
 	typeclass_test_1 \
 	typeclass_test_10 \
 	typeclass_test_11 \
+	typeclass_test_12 \
 	typeclass_test_2 \
 	typeclass_test_3 \
 	typeclass_test_4 \
@@ -170,6 +181,7 @@
 	unify_mode_error \
 	uniq_modes \
 	uniq_neg \
+	unsatisfiable_constraint \
 	uu_type \
 	vars_in_wrong_places \
 	with_type
Index: tests/invalid/ambiguous_method.err_exp
===================================================================
RCS file: tests/invalid/ambiguous_method.err_exp
diff -N tests/invalid/ambiguous_method.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/ambiguous_method.err_exp	20 Apr 2005 06:49:41 -0000
@@ -0,0 +1,5 @@
+ambiguous_method.m:018: In declaration for function `ambiguous_method.e/0':
+ambiguous_method.m:018:   error in type class constraints: type variable E
+ambiguous_method.m:018:   occurs in the constraints, but is not determined by
+ambiguous_method.m:018:   the function's argument or result types.
+For more information, try recompiling with `-E'.
Index: tests/invalid/ambiguous_method.m
===================================================================
RCS file: tests/invalid/ambiguous_method.m
diff -N tests/invalid/ambiguous_method.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/ambiguous_method.m	16 Apr 2005 15:02:10 -0000
@@ -0,0 +1,37 @@
+:- module ambiguous_method.
+:- interface.
+:- import_module io.
+:- pred main(io::di, io::uo) is det.
+:- implementation.
+:- import_module list.
+
+main(!S) :-
+	(
+		test([0], 1)
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	).
+
+:- typeclass coll(C, E) where [
+	func e = C,
+	func i(C, E) = C,
+	pred m(E::in, C::in) is semidet
+].
+
+:- type intcoll == list(int).
+
+:- instance coll(intcoll, int) where [
+	(e = []),
+	(i(Ns, N) = [N | Ns]),
+	m(N, [N | _]),
+	m(N, [_ | Ns]) :- m(N, Ns)
+].
+
+:- pred test(C, E) <= coll(C, E).
+:- mode test(in, in) is semidet.
+
+test(C, E) :-
+	m(E, i(C, E)).
+
Index: tests/invalid/ambiguous_method_2.err_exp
===================================================================
RCS file: tests/invalid/ambiguous_method_2.err_exp
diff -N tests/invalid/ambiguous_method_2.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/ambiguous_method_2.err_exp	20 Apr 2005 06:50:15 -0000
@@ -0,0 +1,5 @@
+ambiguous_method_2.m:028: In declaration for function `ambiguous_method_2.e/0':
+ambiguous_method_2.m:028:   error in type class constraints: type variable E
+ambiguous_method_2.m:028:   occurs in the constraints, but is not determined by
+ambiguous_method_2.m:028:   the function's argument or result types.
+For more information, try recompiling with `-E'.
Index: tests/invalid/ambiguous_method_2.m
===================================================================
RCS file: tests/invalid/ambiguous_method_2.m
diff -N tests/invalid/ambiguous_method_2.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/ambiguous_method_2.m	17 Apr 2005 08:44:22 -0000
@@ -0,0 +1,47 @@
+:- module ambiguous_method_2.
+:- interface.
+:- import_module io.
+:- pred main(io::di, io::uo) is det.
+:- implementation.
+:- import_module list.
+
+main(!S) :-
+	(
+		test([0], 1)
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	),
+	(
+		e = [1]
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	).
+
+:- typeclass foo(T) where [].
+:- instance foo(int) where [].
+
+:- typeclass coll(C, E) <= foo(E) where [
+	func e = C,
+	func i(C, E) = C,
+	pred m(E::in, C::in) is semidet
+].
+
+:- type intcoll == list(int).
+
+:- instance coll(intcoll, int) where [
+	(e = []),
+	(i(Ns, N) = [N | Ns]),
+	m(N, [N | _]),
+	m(N, [_ | Ns]) :- m(N, Ns)
+].
+
+:- pred test(C, E) <= coll(C, E).
+:- mode test(in, in) is semidet.
+
+test(C, E) :-
+	m(E, i(C, E)).
+
Index: tests/invalid/complex_constraint_err.err_exp
===================================================================
RCS file: tests/invalid/complex_constraint_err.err_exp
diff -N tests/invalid/complex_constraint_err.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/complex_constraint_err.err_exp	20 Apr 2005 06:51:00 -0000
@@ -0,0 +1,11 @@
+complex_constraint_err.m:009: In declaration for predicate
+complex_constraint_err.m:009:   `complex_constraint_err.t/1':
+complex_constraint_err.m:009:   error in type class constraints: type variable
+complex_constraint_err.m:009:   C occurs in the constraints, but is not
+complex_constraint_err.m:009:   determined by the predicate's argument types.
+complex_constraint_err.m:013: In declaration for predicate
+complex_constraint_err.m:013:   `complex_constraint_err.u/1':
+complex_constraint_err.m:013:   error in type class constraints: type variables
+complex_constraint_err.m:013:   Z and X occur in the constraints, but are not
+complex_constraint_err.m:013:   determined by the predicate's argument types.
+For more information, try recompiling with `-E'.
Index: tests/invalid/complex_constraint_err.m
===================================================================
RCS file: tests/invalid/complex_constraint_err.m
diff -N tests/invalid/complex_constraint_err.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/complex_constraint_err.m	17 Apr 2005 15:28:29 -0000
@@ -0,0 +1,20 @@
+:- module complex_constraint_err.
+:- interface.
+:- import_module std_util, map, list.
+
+:- typeclass foo(A, B, C) <= (A -> B) where [].
+:- typeclass bar(B, C) <= (B -> C) where [].
+
+	% Error: C is not determined.
+:- pred t(A) <= (foo(A, B, C), bar(B, C1)).
+:- mode t(in) is semidet.
+
+	% Error: X and Z are not determined.
+:- pred u(A) <= (foo(A, pair(W, X1), map(Y, Z)), bar(W, Y), bar(X, list(Z))).
+:- mode u(in) is semidet.
+
+:- implementation.
+
+t(_) :- semidet_succeed.
+u(_) :- semidet_succeed.
+
Index: tests/invalid/foreign_type_2.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/foreign_type_2.err_exp,v
retrieving revision 1.2
diff -u -r1.2 foreign_type_2.err_exp
--- tests/invalid/foreign_type_2.err_exp	17 Jan 2003 05:57:08 -0000	1.2
+++ tests/invalid/foreign_type_2.err_exp	18 Apr 2005 05:00:03 -0000
@@ -2,7 +2,7 @@
 foreign_type_2.m:018:   in argument 1 of clause head:
 foreign_type_2.m:018:   error: undefined symbol `foreign/1'.
 foreign_type_2.m:018:   There are `:- pragma foreign_type' declarations for
-foreign_type_2.m:018:   type `foreign_type_2.foreign/0', so it is treated as an
+foreign_type_2.m:018:   type `foreign_type_2.foreign'/0, so it is treated as an
 foreign_type_2.m:018:   abstract type in all predicates and functions which are
 foreign_type_2.m:018:   not implemented for those foreign types.
 For more information, try recompiling with `-E'.
Index: tests/invalid/fundeps_vars.err_exp
===================================================================
RCS file: tests/invalid/fundeps_vars.err_exp
diff -N tests/invalid/fundeps_vars.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/fundeps_vars.err_exp	17 Apr 2005 08:40:22 -0000
@@ -0,0 +1,9 @@
+fundeps_vars.m:020: Error: domain and range of functional dependency must be comma-separated lists of variables: c -> e.
+fundeps_vars.m:027: Error: type variable in functional dependency is not a parameter of this type class: (_1 -> _2, _3), foo(_2).
+fundeps_vars.m:035: In declaration of instance of typeclass `coll'/2:
+fundeps_vars.m:035:   error: undefined typeclass `coll'/2.
+fundeps_vars.m:042: In definition of predicate `fundeps_vars.test'/2:
+fundeps_vars.m:042:   error: undefined typeclass `coll'/2.
+fundeps_vars.m:035: Error: instance declaration for `coll'/2 without preceding
+fundeps_vars.m:035:   typeclass declaration.
+For more information, try recompiling with `-E'.
Index: tests/invalid/fundeps_vars.m
===================================================================
RCS file: tests/invalid/fundeps_vars.m
diff -N tests/invalid/fundeps_vars.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/fundeps_vars.m	17 Apr 2005 08:39:44 -0000
@@ -0,0 +1,47 @@
+:- module fundeps_vars.
+:- interface.
+:- import_module io.
+:- pred main(io::di, io::uo) is det.
+:- implementation.
+:- import_module list.
+
+main(!S) :-
+	(
+		test([0], 1)
+	->
+		write_string("yes\n", !S)
+	;
+		write_string("no\n", !S)
+	).
+
+:- typeclass foo(T) where [].
+
+% Syntax error: fundeps not variables.
+:- typeclass coll(C, E) <= ((c -> e), foo(E)) where [
+	func e = C,
+	func i(C, E) = C,
+	pred m(E::in, C::in) is semidet
+].
+
+% Syntax error: fundep variables not in head.
+:- typeclass coll(C, E) <= ((C -> E, F), foo(E)) where [
+	func e = C,
+	func i(C, E) = C,
+	pred m(E::in, C::in) is semidet
+].
+
+:- type intcoll == list(int).
+
+:- instance coll(intcoll, int) where [
+	(e = []),
+	(i(Ns, N) = [N | Ns]),
+	m(N, [N | _]),
+	m(N, [_ | Ns]) :- m(N, Ns)
+].
+
+:- pred test(C, E) <= coll(C, E).
+:- mode test(in, in) is semidet.
+
+test(C, E) :-
+	m(E, i(C, E)).
+
Index: tests/invalid/inconsistent_instances.err_exp
===================================================================
RCS file: tests/invalid/inconsistent_instances.err_exp
diff -N tests/invalid/inconsistent_instances.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/inconsistent_instances.err_exp	18 Apr 2005 07:05:45 -0000
@@ -0,0 +1,5 @@
+inconsistent_instances.m:012: Inconsistent instance declaration for typeclass
+inconsistent_instances.m:012:   `inconsistent_instances.foo'/2 with functional
+inconsistent_instances.m:012:   dependency `(A -> B)'.
+inconsistent_instances.m:011: Here is the conflicting instance.
+For more information, try recompiling with `-E'.
Index: tests/invalid/inconsistent_instances.m
===================================================================
RCS file: tests/invalid/inconsistent_instances.m
diff -N tests/invalid/inconsistent_instances.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/inconsistent_instances.m	17 Apr 2005 15:45:10 -0000
@@ -0,0 +1,13 @@
+:- module inconsistent_instances.
+:- interface.
+
+:- typeclass foo(A, B) <= (A -> B) where [].
+
+:- implementation.
+:- import_module list.
+
+	% Inconsistent.
+
+:- instance foo(list(T), int) where [].
+:- instance foo(list(X), string) where [].
+
Index: tests/invalid/invalid_new.err_exp
===================================================================
RCS file: tests/invalid/invalid_new.err_exp
diff -N tests/invalid/invalid_new.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/invalid_new.err_exp	17 Apr 2005 15:48:10 -0000
@@ -0,0 +1,6 @@
+invalid_new.m:020: In clause for function `invalid_new.nc/1':
+invalid_new.m:020:   in function result term of clause head:
+invalid_new.m:020:   error: undefined symbol `new c/1'.
+invalid_new.m:020:   Invalid use of `new' on a constructor of type
+invalid_new.m:020:   `invalid_new.c'/1 which is not existentially typed.
+For more information, try recompiling with `-E'.
Index: tests/invalid/invalid_new.m
===================================================================
RCS file: tests/invalid/invalid_new.m
diff -N tests/invalid/invalid_new.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/invalid_new.m	17 Apr 2005 15:47:54 -0000
@@ -0,0 +1,21 @@
+:- module invalid_new.
+:- interface.
+
+:- typeclass foo(T) where [].
+
+:- type a ---> some [T] (a(T) => foo(T)).
+:- type b ---> some [T] b(T).
+:- type c(T) ---> c(T).
+
+:- func na(T) = a <= foo(T).
+:- func nb(T) = b.
+:- func nc(T) = c(T).
+
+:- implementation.
+
+na(T) = 'new a'(T).
+nb(T) = 'new b'(T).
+
+	% Error: using 'new' where not required.
+nc(T) = 'new c'(T).
+
Index: tests/invalid/mpj1.err_exp
===================================================================
RCS file: tests/invalid/mpj1.err_exp
diff -N tests/invalid/mpj1.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/mpj1.err_exp	17 Apr 2005 16:04:53 -0000
@@ -0,0 +1,9 @@
+mpj1.m:014: In clause for function `mpj1.g/1':
+mpj1.m:014:   in function result term of clause head:
+mpj1.m:014:   in argument 2 of functor `f/3':
+mpj1.m:014:   type error in unification of argument
+mpj1.m:014:   and constant `2'.
+mpj1.m:014:   argument has type `string',
+mpj1.m:014:   constant `2' has type `int'.
+mpj1.m:012: Inferred :- func f(E, E, T4) = T4 <= (mpj1.coll(E, T4)).
+For more information, try recompiling with `-E'.
Index: tests/invalid/mpj1.m
===================================================================
RCS file: tests/invalid/mpj1.m
diff -N tests/invalid/mpj1.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/mpj1.m	17 Apr 2005 16:03:22 -0000
@@ -0,0 +1,15 @@
+% Compile with '--infer-all'
+
+:- module mpj1.
+:- interface.
+
+:- typeclass coll(E, C) <= (C -> E) where [
+	func insert(E, C) = C
+].
+
+:- implementation.
+
+f(A, B, C) = insert(A, insert(B, C)).
+
+g(L) = f("foo", 2, L).
+
Index: tests/invalid/mpj3.err_exp
===================================================================
RCS file: tests/invalid/mpj3.err_exp
diff -N tests/invalid/mpj3.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/mpj3.err_exp	18 Apr 2005 07:06:33 -0000
@@ -0,0 +1,4 @@
+mpj3.m:019: Inconsistent instance declaration for typeclass `mpj3.coll'/2 with
+mpj3.m:019:   functional dependency `(C -> E)'.
+mpj3.m:017: Here is the conflicting instance.
+For more information, try recompiling with `-E'.
Index: tests/invalid/mpj3.m
===================================================================
RCS file: tests/invalid/mpj3.m
diff -N tests/invalid/mpj3.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/mpj3.m	17 Apr 2005 16:07:02 -0000
@@ -0,0 +1,31 @@
+:- module mpj3.
+:- interface.
+
+:- typeclass coll(E, C) <= (C -> E) where [
+	func i(E, C) = C
+].
+
+:- type intlist ---> [] ; [int | intlist].
+:- type stringlist ---> [] ; [string | stringlist].
+
+:- func g(intlist) = intlist.
+
+:- implementation.
+
+	% Error: overlapping instances:
+
+:- instance coll(int, intlist) where [ (i(N, L) = [N | L]) ].
+:- instance coll(string, stringlist) where [ (i(S, L) = [S | L]) ].
+:- instance coll(string, intlist) where [ (i(_S, L) = [1 | L]) ].
+
+	% Error: conflicting types for args 1 and 2, both of which are
+	% determined by the type of L.
+
+g(L) = f(1, "foo", L).
+
+% This probably should be an error, or at least a warning, since the
+% constraints could be tighter.
+:- func f(A, B, C) = C <= (coll(A, C), coll(B, C)).
+
+f(A, B, C) = i(A, i(B, C)).
+
Index: tests/invalid/mpj4.err_exp
===================================================================
RCS file: tests/invalid/mpj4.err_exp
diff -N tests/invalid/mpj4.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/mpj4.err_exp	17 Apr 2005 16:09:13 -0000
@@ -0,0 +1,8 @@
+mpj4.m:020: In clause for function `mpj4.g/1':
+mpj4.m:020:   in function result term of clause head:
+mpj4.m:020:   in argument 2 of functor `f/3':
+mpj4.m:020:   type error in unification of argument
+mpj4.m:020:   and constant `"foo"'.
+mpj4.m:020:   argument has type `int',
+mpj4.m:020:   constant `"foo"' has type `string'.
+For more information, try recompiling with `-E'.
Index: tests/invalid/mpj4.m
===================================================================
RCS file: tests/invalid/mpj4.m
diff -N tests/invalid/mpj4.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/mpj4.m	17 Apr 2005 16:08:08 -0000
@@ -0,0 +1,27 @@
+:- module mpj4.
+:- interface.
+
+:- typeclass coll(E, C) <= (C -> E) where [
+	func i(E, C) = C
+].
+
+:- type intlist ---> [] ; [int | intlist].
+:- type stringlist ---> [] ; [string | stringlist].
+
+:- func g(intlist) = intlist.
+
+:- implementation.
+
+:- instance coll(int, intlist) where [ (i(N, L) = [N | L]) ].
+:- instance coll(string, stringlist) where [ (i(S, L) = [S | L]) ].
+
+	% Error: call to f/3 has unsatisfiable constraints
+
+g(L) = f(1, "foo", L).
+
+% This probably should be an error, or at least a warning, since the
+% constraints could be tighter.
+:- func f(A, B, C) = C <= (coll(A, C), coll(B, C)).
+
+f(A, B, C) = i(A, i(B, C)).
+
Index: tests/invalid/range_restrict.err_exp
===================================================================
RCS file: tests/invalid/range_restrict.err_exp
diff -N tests/invalid/range_restrict.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/range_restrict.err_exp	20 Apr 2005 06:52:25 -0000
@@ -0,0 +1,9 @@
+range_restrict.m:012: In instance for typeclass `range_restrict.foo'/2:
+range_restrict.m:012:   functional dependency not satisfied: type variables Y
+range_restrict.m:012:   and Z occur in the range of the functional dependency,
+range_restrict.m:012:   but are not in the domain.
+range_restrict.m:011: In instance for typeclass `range_restrict.foo'/2:
+range_restrict.m:011:   functional dependency not satisfied: type variable Y
+range_restrict.m:011:   occurs in the range of the functional dependency, but
+range_restrict.m:011:   is not in the domain.
+For more information, try recompiling with `-E'.
Index: tests/invalid/range_restrict.m
===================================================================
RCS file: tests/invalid/range_restrict.m
diff -N tests/invalid/range_restrict.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/range_restrict.m	17 Apr 2005 15:43:14 -0000
@@ -0,0 +1,13 @@
+:- module range_restrict.
+:- interface.
+
+:- typeclass foo(A, B) <= (A -> B) where [].
+
+:- implementation.
+:- import_module list, map.
+
+	% Errors: range-restrictedness
+
+:- instance foo(list(X), map(X, Y)) where [].
+:- instance foo(map(W, X), map(Y, Z)) where [].
+
Index: tests/invalid/typeclass_constraint_extra_var.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/typeclass_constraint_extra_var.err_exp,v
retrieving revision 1.4
diff -u -r1.4 typeclass_constraint_extra_var.err_exp
--- tests/invalid/typeclass_constraint_extra_var.err_exp	12 Apr 2005 07:58:20 -0000	1.4
+++ tests/invalid/typeclass_constraint_extra_var.err_exp	20 Apr 2005 06:53:01 -0000
@@ -1,10 +1,7 @@
 typeclass_constraint_extra_var.m:011: In declaration for predicate
 typeclass_constraint_extra_var.m:011:   `typeclass_constraint_extra_var.mg/2':
 typeclass_constraint_extra_var.m:011:   error in type class constraints: type
-typeclass_constraint_extra_var.m:011:   variable `U' occurs only in the
-typeclass_constraint_extra_var.m:011:   constraints, not in the predicate's
-typeclass_constraint_extra_var.m:011:   argument types.
-typeclass_constraint_extra_var.m:025: In clause for predicate `typeclass_constraint_extra_var.mg/2':
-typeclass_constraint_extra_var.m:025:   unsatisfiable typeclass constraint(s):
-typeclass_constraint_extra_var.m:025:   `typeclass_constraint_extra_var.solver_for((list.list(T)), T)'.
+typeclass_constraint_extra_var.m:011:   variable U occurs in the constraints,
+typeclass_constraint_extra_var.m:011:   but is not determined by the
+typeclass_constraint_extra_var.m:011:   predicate's argument types.
 For more information, try recompiling with `-E'.
Index: tests/invalid/typeclass_test_12.err_exp
===================================================================
RCS file: tests/invalid/typeclass_test_12.err_exp
diff -N tests/invalid/typeclass_test_12.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/typeclass_test_12.err_exp	20 Apr 2005 06:53:38 -0000
@@ -0,0 +1,9 @@
+typeclass_test_12.m:003: In declaration for predicate `typeclass_test_12.p/0':
+typeclass_test_12.m:003:   error in type class constraints: type variable T
+typeclass_test_12.m:003:   occurs in the constraints, but is not determined by
+typeclass_test_12.m:003:   the predicate's argument types.
+typeclass_test_12.m:005: In declaration for function `typeclass_test_12.q/0':
+typeclass_test_12.m:005:   error in type class constraints: type variable T
+typeclass_test_12.m:005:   occurs in the constraints, but is not determined by
+typeclass_test_12.m:005:   the function's argument or result types.
+For more information, try recompiling with `-E'.
Index: tests/invalid/typeclass_test_12.m
===================================================================
RCS file: tests/invalid/typeclass_test_12.m
diff -N tests/invalid/typeclass_test_12.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/typeclass_test_12.m	6 Apr 2005 13:39:18 -0000
@@ -0,0 +1,5 @@
+:- module typeclass_test_12.
+:- interface.
+:- typeclass foo(T) where [pred p is semidet].
+:- typeclass bar(T) where [].
+:- typeclass baz(T) where [func q = int].
Index: tests/invalid/typeclass_test_9.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/typeclass_test_9.err_exp,v
retrieving revision 1.8
diff -u -r1.8 typeclass_test_9.err_exp
--- tests/invalid/typeclass_test_9.err_exp	12 Apr 2005 07:58:21 -0000	1.8
+++ tests/invalid/typeclass_test_9.err_exp	12 Apr 2005 16:30:16 -0000
@@ -1,11 +1,3 @@
-typeclass_test_9.m:003: In declaration for predicate `typeclass_test_9.p/0':
-typeclass_test_9.m:003:   error in type class constraints: type variable `T'
-typeclass_test_9.m:003:   occurs only in the constraints, not in the
-typeclass_test_9.m:003:   predicate's argument types.
-typeclass_test_9.m:005: In declaration for predicate `typeclass_test_9.q/0':
-typeclass_test_9.m:005:   error in type class constraints: type variable `T'
-typeclass_test_9.m:005:   occurs only in the constraints, not in the
-typeclass_test_9.m:005:   predicate's argument types.
 typeclass_test_9.m:018: Error: multiply defined (or overlapping) instance
 typeclass_test_9.m:018:   declarations for class `typeclass_test_9.foo'/1.
 typeclass_test_9.m:015: Previous instance declaration was here.
Index: tests/invalid/unbound_type_vars.err_exp
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/unbound_type_vars.err_exp,v
retrieving revision 1.4
diff -u -r1.4 unbound_type_vars.err_exp
--- tests/invalid/unbound_type_vars.err_exp	15 Apr 2005 15:14:44 -0000	1.4
+++ tests/invalid/unbound_type_vars.err_exp	20 Apr 2005 06:54:28 -0000
@@ -1,25 +1,25 @@
 unbound_type_vars.m:014: Error: type variable in superclass constraint is not a parameter of this type class: c1(_1, _2).
 unbound_type_vars.m:018: Error: unbound type variable(s) in constraints on instance declaration: c1(int, float) <= c3(_1).
 unbound_type_vars.m:021: In declaration for predicate `unbound_type_vars.p1/1':
-unbound_type_vars.m:021:   error in type class constraints: type variable `T2'
-unbound_type_vars.m:021:   occurs only in the constraints, not in the
-unbound_type_vars.m:021:   predicate's argument types.
+unbound_type_vars.m:021:   error in type class constraints: type variable T2
+unbound_type_vars.m:021:   occurs in the constraints, but is not determined by
+unbound_type_vars.m:021:   the predicate's argument types.
 unbound_type_vars.m:024: In declaration for predicate `unbound_type_vars.p2/2':
-unbound_type_vars.m:024:   error in type class constraints: type variable `T3'
-unbound_type_vars.m:024:   occurs only in the constraints, not in the
-unbound_type_vars.m:024:   predicate's argument types.
+unbound_type_vars.m:024:   error in type class constraints: type variable T3
+unbound_type_vars.m:024:   occurs in the constraints, but is not determined by
+unbound_type_vars.m:024:   the predicate's argument types.
 unbound_type_vars.m:028: In declaration for predicate `unbound_type_vars.p3/1':
-unbound_type_vars.m:028:   error in type class constraints: type variable `T2'
-unbound_type_vars.m:028:   occurs only in the constraints, not in the
-unbound_type_vars.m:028:   predicate's argument types.
+unbound_type_vars.m:028:   error in type class constraints: type variable T2
+unbound_type_vars.m:028:   occurs in the constraints, but is not determined by
+unbound_type_vars.m:028:   the predicate's argument types.
 unbound_type_vars.m:031: In declaration for predicate `unbound_type_vars.p4/1':
-unbound_type_vars.m:031:   error in type class constraints: type variable `T2'
-unbound_type_vars.m:031:   occurs only in the constraints, not in the
-unbound_type_vars.m:031:   predicate's argument types.
+unbound_type_vars.m:031:   error in type class constraints: type variable T2
+unbound_type_vars.m:031:   occurs in the constraints, but is not determined by
+unbound_type_vars.m:031:   the predicate's argument types.
 unbound_type_vars.m:034: In declaration for predicate `unbound_type_vars.p5/1':
-unbound_type_vars.m:034:   error in type class constraints: type variable `T2'
-unbound_type_vars.m:034:   occurs only in the constraints, not in the
-unbound_type_vars.m:034:   predicate's argument types.
+unbound_type_vars.m:034:   error in type class constraints: type variable T2
+unbound_type_vars.m:034:   occurs in the constraints, but is not determined by
+unbound_type_vars.m:034:   the predicate's argument types.
 unbound_type_vars.m:034: In declaration of predicate `unbound_type_vars.p5/1':
 unbound_type_vars.m:034:   type variable T2 is universally constrained, but is
 unbound_type_vars.m:034:   existentially quantified.
Index: tests/invalid/unsatisfiable_constraint.err_exp
===================================================================
RCS file: tests/invalid/unsatisfiable_constraint.err_exp
diff -N tests/invalid/unsatisfiable_constraint.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/unsatisfiable_constraint.err_exp	17 Apr 2005 15:31:16 -0000
@@ -0,0 +1,11 @@
+unsatisfiable_constraint.m:038: In predicate `unsatisfiable_constraint.test/1':
+unsatisfiable_constraint.m:038:   type error: unsatisfied typeclass constraint(s):
+unsatisfiable_constraint.m:038:   unsatisfiable_constraint.a(A, B, A, V_8), unsatisfiable_constraint.a(A, B, C, V_14), unsatisfiable_constraint.b(A, C).
+unsatisfiable_constraint.m:038: In predicate `unsatisfiable_constraint.test/1':
+unsatisfiable_constraint.m:038:   warning: unresolved polymorphism.
+unsatisfiable_constraint.m:038:   The variables with unbound types were:
+unsatisfiable_constraint.m:038:       C: C
+unsatisfiable_constraint.m:038:       B: A
+unsatisfiable_constraint.m:038:   The unbound type variable(s) will be implicitly
+unsatisfiable_constraint.m:038:   bound to the builtin type `void'.
+For more information, try recompiling with `-E'.
Index: tests/invalid/unsatisfiable_constraint.m
===================================================================
RCS file: tests/invalid/unsatisfiable_constraint.m
diff -N tests/invalid/unsatisfiable_constraint.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/unsatisfiable_constraint.m	17 Apr 2005 15:30:56 -0000
@@ -0,0 +1,60 @@
+:- module unsatisfiable_constraint.
+:- interface.
+:- import_module io.
+
+:- pred main(io::di, io::uo) is det.
+
+:- implementation.
+:- import_module int, string.
+
+main(!IO) :-
+	write_string("test(1): ", !IO),
+	(
+		test(1)
+	->
+		write_string("yes\n", !IO)
+	;
+		write_string("no\n", !IO)
+	),
+	write_string("test(2): ", !IO),
+	(
+		test(2)
+	->
+		write_string("yes\n", !IO)
+	;
+		write_string("no\n", !IO)
+	).
+
+:- typeclass a(A, B, C, D) <= ((A -> B), (C -> D)) where [
+	func f(A, C) = B,
+	func g(A) = C
+].
+
+:- typeclass b(A, B) <= (A -> B) where [
+	func h(A) = B,
+	func ii = A
+].
+
+:- pred test(A) <= (a(A, B, C, D), b(B, C)).
+:- mode test(in) is semidet.
+
+test(A) :-
+	B = g(A),
+	C = h(B),		% unsatisfiable!
+	f(A, C) = ii.
+
+:- instance a(int, int, int, int) where [
+	(f(M, N) = M + N),
+	(g(M) = -M)
+].
+
+:- instance a(int, int, string, int) where [
+	(f(M, S) = M + length(S)),
+	(g(_) = "")
+].
+
+:- instance b(int, int) where [
+	(h(N) = -N),
+	(ii = 2)
+].
+
Index: tests/valid/Mercury.options
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mercury.options,v
retrieving revision 1.18
diff -u -r1.18 Mercury.options
--- tests/valid/Mercury.options	21 Feb 2005 00:13:39 -0000	1.18
+++ tests/valid/Mercury.options	18 Apr 2005 05:00:03 -0000
@@ -81,6 +81,7 @@
 MCFLAGS-loop_inv_bug		= --common-struct --loop-invariants
 MCFLAGS-middle_rec_labels	= --middle-rec
 MCFLAGS-mostly_uniq_mode_inf	= --infer-all
+MCFLAGS-mpj6			= --infer-all
 MCFLAGS-pred_with_no_modes	= --infer-all
 MCFLAGS-quantifier_warning	= --halt-at-warn
 MCFLAGS-simplify_bug2		= -O3
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.150
diff -u -r1.150 Mmakefile
--- tests/valid/Mmakefile	21 Feb 2005 00:13:39 -0000	1.150
+++ tests/valid/Mmakefile	17 Apr 2005 16:12:10 -0000
@@ -19,11 +19,17 @@
 
 TYPECLASS_PROGS= \
 	abstract_typeclass \
+	complex_constraint \
 	constraint_proof_bug \
 	func_method \
 	instance_superclass \
 	instance_unconstrained_tvar \
+	mpj2 \
+	mpj5 \
+	mpj6 \
+	mpj7 \
 	repeated_class_constraint \
+	superclass_improvement \
 	typeclass_constraint_no_var \
 	typeclass_constraint_nonvar_bug \
 	typeclass_det_warning
Index: tests/valid/complex_constraint.m
===================================================================
RCS file: tests/valid/complex_constraint.m
diff -N tests/valid/complex_constraint.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/complex_constraint.m	17 Apr 2005 15:26:45 -0000
@@ -0,0 +1,18 @@
+:- module complex_constraint.
+:- interface.
+:- import_module std_util, map, list.
+
+:- typeclass foo(A, B, C) <= (A -> B) where [].
+:- typeclass bar(B, C) <= (B -> C) where [].
+
+:- pred t(A) <= (foo(A, B, C), bar(B, C)).
+:- mode t(in) is semidet.
+
+:- pred u(A) <= (foo(A, pair(W, X), map(Y, Z)), bar(W, Y), bar(X, list(Z))).
+:- mode u(in) is semidet.
+
+:- implementation.
+
+t(_) :- semidet_succeed.
+u(_) :- semidet_succeed.
+
Index: tests/valid/mpj2.m
===================================================================
RCS file: tests/valid/mpj2.m
diff -N tests/valid/mpj2.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/mpj2.m	17 Apr 2005 16:05:40 -0000
@@ -0,0 +1,25 @@
+:- module mpj2.
+:- interface.
+
+:- typeclass coll(E, C) <= (C -> E) where [
+	func i(E, C) = C
+].
+
+:- type intlist ---> [] ; [int | intlist].
+:- type stringlist ---> [] ; [string | stringlist].
+
+:- func g(intlist) = intlist.
+
+:- implementation.
+
+:- instance coll(int, intlist) where [ (i(N, L) = [N | L]) ].
+:- instance coll(string, stringlist) where [ (i(S, L) = [S | L]) ].
+
+g(L) = f(1, 2, L).
+
+% This probably should be an error, or at least a warning, since the
+% constraints could be tighter.
+:- func f(A, B, C) = C <= (coll(A, C), coll(B, C)).
+
+f(A, B, C) = i(A, i(B, C)).
+
Index: tests/valid/mpj5.m
===================================================================
RCS file: tests/valid/mpj5.m
diff -N tests/valid/mpj5.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/mpj5.m	17 Apr 2005 16:10:16 -0000
@@ -0,0 +1,38 @@
+:- module mpj5.
+:- interface.
+:- import_module list, bool.
+
+:- typeclass coll(E, C) <= (C -> E) where [
+	func e = C,
+	func i(E, C) = C,
+	pred m(E::in, C::in) is semidet
+].
+
+:- type w(T) ---> w(T).
+:- type cf(T) ---> cf(func(T) = bool).
+
+:- instance coll(w(T), list(T)).
+:- instance coll(w(T), cf(T)).
+:- instance coll(int, int).
+
+:- implementation.
+:- import_module int.
+
+:- instance coll(w(T), list(T)) where [
+	(e = []),
+	(i(w(E), L) = [E | L]),
+	(m(w(E), L) :- list__member(E, L))
+].
+
+:- instance coll(w(T), cf(T)) where [
+	(e = cf(func(_) = no)),
+	(i(w(E), cf(F)) = cf(func(X) = ( X = E -> yes ; F(X) ))),
+	(m(w(E), cf(F)) :- F(E) = yes)
+].
+
+:- instance coll(int, int) where [
+	(e = 0),
+	(i(N, B) = B \/ (1 << N)),
+	(m(N, B) :- B /\ (1 << N) \= 0)
+].
+
Index: tests/valid/mpj6.m
===================================================================
RCS file: tests/valid/mpj6.m
diff -N tests/valid/mpj6.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/mpj6.m	17 Apr 2005 16:11:08 -0000
@@ -0,0 +1,27 @@
+% Compile with '--infer-all'
+
+:- module mpj6.
+:- interface.
+
+:- typeclass coll(E, C) <= (C -> E) where [
+	func i(E, C) = C
+].
+
+:- type intlist ---> [] ; [int | intlist].
+:- type stringlist ---> [] ; [string | stringlist].
+
+:- func g(intlist) = intlist.
+
+:- implementation.
+
+:- instance coll(int, intlist) where [ (i(N, L) = [N | L]) ].
+:- instance coll(string, stringlist) where [ (i(S, L) = [S | L]) ].
+
+g(L) = h(f, 1, 2, L).
+
+:- func h(func(A, A, C) = C, A, A, C) = C <= coll(A, C).
+
+h(F, A1, A2, L) = F(A1, A2, L).
+
+f(A, B, C) = i(A, i(B, C)).
+
Index: tests/valid/mpj7.m
===================================================================
RCS file: tests/valid/mpj7.m
diff -N tests/valid/mpj7.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/mpj7.m	17 Apr 2005 16:12:01 -0000
@@ -0,0 +1,29 @@
+% Compile with '--infer-all'
+
+:- module mpj7.
+:- interface.
+
+:- typeclass coll(E, C) where [
+	func i(E, C) = C
+].
+
+:- type intlist ---> [] ; [int | intlist].
+:- type stringlist ---> [] ; [string | stringlist].
+
+:- func g(intlist) = intlist.
+
+:- implementation.
+
+:- instance coll(string, intlist) where [ (i(_S, L) = [1 | L]) ].
+:- instance coll(int, intlist) where [ (i(N, L) = [N | L]) ].
+:- instance coll(string, stringlist) where [ (i(S, L) = [S | L]) ].
+
+g(L) = h(f, 1, 2, L).
+
+:- func h(func(A, A, C) = C, A, A, C) = C <= coll(A, C).
+
+h(F, A1, A2, L) = F(A1, A2, L).
+
+:- func f(A, B, C) = C <= (coll(A, C), coll(B, C)).
+f(A, B, C) = i(A, i(B, C)).
+
Index: tests/valid/superclass_improvement.m
===================================================================
RCS file: tests/valid/superclass_improvement.m
diff -N tests/valid/superclass_improvement.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/superclass_improvement.m	17 Apr 2005 15:37:37 -0000
@@ -0,0 +1,22 @@
+:- module superclass_improvement.
+:- interface.
+
+:- typeclass z(A, B) <= (A -> B) where [].
+
+:- typeclass x(A, B) <= z(A, B) where [ func f(A) = B ].
+:- typeclass y(A, B) <= z(A, B) where [ func g(A) = B ].
+
+:- pred p(int::in) is semidet.
+
+:- implementation.
+
+:- instance z(int, int) where [].
+
+:- instance x(int, int) where [ (f(N) = N) ].
+:- instance y(int, int) where [ (g(_) = 1) ].
+
+p(N) :-
+	% The FD on z/2 is required in order to prove that these two
+	% function calls have the same return type.
+	f(N) = g(N).
+
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------



More information about the reviews mailing list