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

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


Estimated hours taken: 240
Branches: main

Implement functional dependencies for the typeclass system.  The implementation
has two major parts.  First, some of the basic checks of constraints are
relaxed.  These used to occur in make_hlds but that functionality has now been
moved to check_typeclass.  We also add a range of new tests to ensure that
the FDs are used correctly.  Second, an "improvement" pass to context
reduction is added.  This looks for constraints which match certain rules,
and when it finds them updates the current bindings.  The general rule is
that type variables become more instantiated, but only in a way which provably
does not affect the satisfiability of the constraints.

XXX The plan for this change is to put the context reduction into a new
module check_hlds.typeclasses.m, but I have left the code in typecheck.m
for the moment because the diff will be easier to review that way.  Moving
to the new module will also remove the problem of one particular function
being implemented in both typecheck and hlds_data, which is flagged by an XXX
below.

XXX the check for consistency of instances is not yet complete.  We check all
visible instances, but not instances that are only present at link time.  We
could check these in a similar way to the check for overlapping instances
(that is, by defining a symbol that will conflict and cause a link error
if there are overlapping instances), but in the long run a better solution
will be required.  Producing this is left for a later change.

compiler/check_typeclass.m:
	Check for ambiguities in typeclass constraints here, rather than
	make_hlds.  We check by calculating the closure of the bound type
	variables under the induced functional dependencies.  This pass
	is merged in with the already existing pass that checks the
	quantifiers on constrained type variables.

	Check instances for range-restrictedness and for consistency.

	When checking for cycles in the typeclass hierarchy, build up the
	set of ancestors of a class which have FDs on them.  This set is
	used when searching for opportunities to apply improvement rules
	during type checking.

compiler/hlds_data.m:
	Define hlds_class_fundeps and add it to to hlds_class_defn.

	Add a field to hlds_class_defn to store the ancestors which have
	functional dependencies.

	Define the type 'instance_id', which is just an integer.  This is
	what is used in proofs to identify instances.

	In hlds_constraints and in constraint_ids, use the terms 'assumed'
	and 'unproven' rather than 'existential' and 'universal'.  The latter
	are confusing to use since the treatment of constraints differs
	depending on whether the constraint is on the head or the body of a
	clause.

	Add a field to the hlds_constraints for redundant constraints.  These
	are constraints that have either already been reduced or don't need to
	be reduced, which may contribute to improvement of types.

	Define some new predicates for initialising and updating the
	hlds_constraints.

compiler/type_util.m:
	Accommodate the change to hlds_constraints.

compiler/hlds_out.m:
	Output the functional dependencies.

compiler/intermod.m:
	Reconstruct a functional dependency from the HLDS, for outputting.

compiler/make_hlds.m:
	Convert functional dependencies from parse tree form and add them
	to the HLDS.

	Check that functional dependencies are identical in subsequent
	definitions of the same typeclass.

	Don't check for ambiguity here.  That is now done in check_typeclass.

compiler/mercury_to_mercury.m:
	Output functional dependencies in typeclass declarations.

compiler/prog_data.m:
	Define prog_fundeps and add them to the parse tree.

compiler/prog_io_typeclass.m:
	Parse functional dependencies on typeclass declarations.

compiler/typecheck.m:
	Require the class_table to be passed to
	reduce_context_by_rule_application, since the functional dependencies
	are stored here.  Also thread the bindings argument through, since the
	bindings may be improved by context reduction.  Save the resulting
	bindings in the type_assign.

	Instead of passing a list of assumed constraints and threading the
	unproven constraints through context reduction, thread through a
	hlds_constraints structure.  This contains more information about
	redundant constraints than just the two lists.

	Extend context reduction with two new passes.  The first applies the
	"class" FD rule, which tries to find two constraints which are
	identical on the domain of some FD, and then unifies the range
	arguments.  The pair of constraints are either both redundant
	constraints, or one redundant constraint and one assumed constraint.
	The second applies the "instance" FD rule, which for each constraint
	tries to find an instance which is more general on the domain
	arguments.  It then binds the instance arguments and unifies the
	range arguments of the instance with those of the constraint.

	When calculating the head_type_params for a predicate, include all
	variables that occur in universal constraints, since these may not
	necessarily occur in the arguments.

	Rename some variables: use variable prefixes "Pred" and "Parent" for
	types that are from the callee or that have been renamed apart
	respectively.  This follows the same naming scheme used in
	polymorphism.

	Remove the headtypes/0 type, and use head_type_params/0 throughout.

	Add a new kind of cons_error for using "new" on a constructor that is
	not existentially typed.  We check for this situation in
	convert_cons_defn, and report it in report_cons_error.

	Pass a value to convert_cons_defn indicating whether the constraints
	should be flipped or not, and whether the context is a constructor
	that uses 'new'.  We flip the constraints here rather than after the
	fact, since creating the constraints now requires some extra
	processing to be done, and we don't want to have to redo that
	processing.

	Add a constant function that specifies whether variable numbers should
	be displayed as part of the debugging output.  This is currently set
	to 'yes' but the previous behaviour can be achieved by changing the
	value to 'no'.

doc/reference_manual.texi:
	Document the new feature.

NEWS:
	Announce the new feature.

tests/*:
	New test cases.

compler/*.m:
	Minor changes related to the above.

compiler/error_util.m:
	Fix comment grammar.

compiler/prog_type.m:
	Fix an incorrect comment.

Index: NEWS
===================================================================
RCS file: /home/mercury1/repository/mercury/NEWS,v
retrieving revision 1.377
diff -u -r1.377 NEWS
--- NEWS	30 Mar 2005 10:52:03 -0000	1.377
+++ NEWS	19 Apr 2005 14:32:41 -0000
@@ -1,6 +1,10 @@
 NEWS since the 0.12.0 fork:
 ----------------------------------
 
+Changes to the Mercury language:
+* We have added support for functional dependencies to the typeclass system.
+
+Changes to the Mercury standard library:
 * We have added string.word_wrap/2.
 
 NEWS since Mercury release 0.11.0:
Index: compiler/base_typeclass_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/base_typeclass_info.m,v
retrieving revision 1.34
diff -u -r1.34 base_typeclass_info.m
--- compiler/base_typeclass_info.m	1 Apr 2005 14:28:54 -0000	1.34
+++ compiler/base_typeclass_info.m	2 Apr 2005 08:31:25 -0000
@@ -159,9 +159,7 @@
 		NumSuperClasses, ClassArity) :-
 	module_info_classes(ModuleInfo, ClassTable),
 	map__lookup(ClassTable, ClassId, ClassDefn),
-	ClassDefn = hlds_class_defn(_, SuperClassConstraints, ClassVars,
-		_, _, _, _),
-	list__length(SuperClassConstraints, NumSuperClasses),
-	list__length(ClassVars, ClassArity).
+	list__length(ClassDefn ^ class_supers, NumSuperClasses),
+	list__length(ClassDefn ^ class_vars, ClassArity).
 
 %----------------------------------------------------------------------------%
Index: compiler/check_typeclass.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/check_typeclass.m,v
retrieving revision 1.69
diff -u -r1.69 check_typeclass.m
--- compiler/check_typeclass.m	15 Apr 2005 15:14:26 -0000	1.69
+++ compiler/check_typeclass.m	19 Apr 2005 15:12:48 -0000
@@ -5,9 +5,9 @@
 %---------------------------------------------------------------------------%
 %
 % This module checks conformance of instance declarations to the typeclass
-% declaration.
+% declaration.  It takes various steps to do this.
 %
-% It does so by, for every method of every instance, generating a new pred
+% First, for every method of every instance it generates a new pred
 % whose types and modes are as expected by the typeclass declaration and
 % whose body just calls the implementation provided by the instance
 % declaration.
@@ -34,13 +34,28 @@
 % determinism and uniqueness correctness since the generated pred is checked
 % in each of those passes too.
 %
-% In addition, this pass checks that all superclass constraints are satisfied
-% by the instance declaration.
+% Second, this pass checks that all superclass constraints are satisfied
+% by the instance declaration.  To do this it attempts to perform context
+% reduction on the typeclass constraints, using the instance constraints
+% as assumptions.
+%
+% Third, typeclass constraints on predicate and function declarations are
+% checked for ambiguity, taking into consideration the information
+% provided by functional depencies.
+%
+% Fourth, all visible instances are checked for range-restrictedness and
+% mutual consistency, with respect to any functional dependencies.  This
+% doesn't necessarily catch all cases of inconsistent instances, however,
+% since in general that cannot be done until link time.  We try to catch
+% as many cases as possible here, though, since we can give better error
+% messages.
 %
-% This pass also checks for cycles in the typeclass hierarchy.
+% This module also checks for cycles in the typeclass hierarchy, and checks
+% that each abstract instance has a corresponding concrete instance.
 %
 % This pass fills in the super class proofs and instance method pred/proc ids
-% in the instance table of the HLDS.
+% in the instance table of the HLDS, and fills in the fundeps_ancestors in
+% the class table.
 %
 % Author: dgj.
 %
@@ -74,6 +89,7 @@
 :- import_module hlds__hlds_goal.
 :- import_module hlds__hlds_out.
 :- import_module hlds__hlds_pred.
+:- import_module hlds__passes_aux.
 :- import_module libs__globals.
 :- import_module libs__options.
 :- import_module mdbcomp__prim_data.
@@ -93,6 +109,7 @@
 :- import_module set.
 :- import_module std_util.
 :- import_module string.
+:- import_module svmap.
 :- import_module svmulti_map.
 :- import_module svset.
 :- import_module term.
@@ -101,15 +118,29 @@
 %---------------------------------------------------------------------------%
 
 check_typeclass__check_typeclasses(!QualInfo, !ModuleInfo, FoundError, !IO) :-
+	globals__io_lookup_bool_option(verbose, Verbose, !IO),
+	maybe_write_string(Verbose, "% Checking typeclass instances...\n", !IO),
 	check_typeclass__check_instance_decls(!QualInfo, !ModuleInfo,
 		FoundInstanceError, !IO),
+
+	maybe_write_string(Verbose, "% Checking for cyclic classes...\n", !IO),
+	check_for_cyclic_classes(!ModuleInfo, FoundCycleError, !IO),
+
+	maybe_write_string(Verbose,
+		"% Checking for missing concrete instances...\n", !IO),
  	check_for_missing_concrete_instances(!ModuleInfo, FoundMissingError,
 		!IO),
-	module_info_classes(!.ModuleInfo, ClassTable),
-	check_for_cyclic_classes(ClassTable, FoundCycleError, !IO),
-	check_constraint_quant(!ModuleInfo, FoundQuantError, !IO),
-	FoundError = bool.or_list([FoundInstanceError, FoundMissingError,
-		FoundCycleError, FoundQuantError]).
+
+	maybe_write_string(Verbose,
+		"% Checking functional dependencies on instances...\n", !IO),
+	check_functional_dependencies(!ModuleInfo, FoundFunDepError, !IO),
+
+	maybe_write_string(Verbose,
+		"% Checking typeclass constraints...\n", !IO),
+	check_constraints(!ModuleInfo, FoundConstraintsError, !IO),
+
+	FoundError = bool.or_list([FoundInstanceError, FoundCycleError,
+		FoundMissingError, FoundFunDepError, FoundConstraintsError]).
 
 %---------------------------------------------------------------------------%
 
@@ -164,9 +195,9 @@
 	ClassId - InstanceDefns, !CheckTCInfo, !IO) :-
 
 	map__lookup(ClassTable, ClassId, ClassDefn),
-	ClassDefn = hlds_class_defn(ImportStatus, SuperClasses, ClassVars,
-		Interface, ClassInterface, ClassVarSet, TermContext),
-
+	ClassDefn = hlds_class_defn(ImportStatus, SuperClasses, _FunDeps,
+		_Ancestors, ClassVars, Interface, ClassInterface, ClassVarSet,
+		TermContext),
 	(
 		status_defined_in_this_module(ImportStatus, yes),
 		Interface = abstract
@@ -843,14 +874,14 @@
 		InstanceProgConstraints, InstanceTypes, F, G, InstanceVarSet0,
 		Proofs0),
 	varset__merge_subst(InstanceVarSet0, ClassVarSet, InstanceVarSet1,
-		Subst),
+		RenameSubst),
 
 		% Make the constraints in terms of the instance variables
-	apply_subst_to_prog_constraint_list(Subst, ProgSuperClasses0,
+	apply_subst_to_prog_constraint_list(RenameSubst, ProgSuperClasses0,
 		ProgSuperClasses),
 
 		% Now handle the class variables
-	map__apply_to_list(ClassVars0, Subst, ClassVarTerms),
+	map__apply_to_list(ClassVars0, RenameSubst, ClassVarTerms),
 	( term__var_list_to_term_list(ClassVars1, ClassVarTerms) ->
 		ClassVars = ClassVars1
 	;
@@ -860,26 +891,36 @@
 		% Calculate the bindings
 	map__from_corresponding_lists(ClassVars, InstanceTypes, TypeSubst),
 
+	module_info_classes(ModuleInfo, ClassTable),
 	module_info_instances(ModuleInfo, InstanceTable),
 	module_info_superclasses(ModuleInfo, SuperClassTable),
 
-		% These constraints are not required to be put into the
-		% final constraint_map, so we initialise them with no
-		% constraint_id and throw away the constraint_map that
-		% results.
-	map__init(ConstraintMap0),
+		% Build a suitable constraint context for checking the
+		% instance.  To do this, we assume any constraints on the
+		% instance declaration (that is, treat them as universal
+		% constraints on a predicate) and try to prove the constraints
+		% on the class declaration (that is, treat them as existential
+		% constraints on a predicate).
+		%
+		% We don't bother assigning ids to these constraints, since
+		% the resulting constraint map is not used anyway.
+		%
+	init_hlds_constraint_list(ProgSuperClasses, SuperClasses),
 	init_hlds_constraint_list(InstanceProgConstraints,
 		InstanceConstraints),
-	init_hlds_constraint_list(ProgSuperClasses, SuperClasses),
-
-		% Try to reduce the superclass constraints,
-		% using the declared instance constraints
-		% and the usual context reduction rules.
-	typecheck__reduce_context_by_rule_application(InstanceTable,
-		SuperClassTable, InstanceConstraints, TypeSubst,
-		InstanceVarSet1, InstanceVarSet2, Proofs0, Proofs1,
-		ConstraintMap0, _,
-		SuperClasses, UnprovenConstraints),
+	make_hlds_constraints(ClassTable, InstanceVarSet1, SuperClasses,
+		InstanceConstraints, Constraints0),
+		
+		% Try to reduce the superclass constraints, using the declared
+		% instance constraints and the usual context reduction rules.
+		%
+	map__init(ConstraintMap0),
+	typecheck__reduce_context_by_rule_application(ClassTable,
+		InstanceTable, SuperClassTable, ClassVars, TypeSubst, _,
+		InstanceVarSet1, InstanceVarSet2,
+		Proofs0, Proofs1, ConstraintMap0, _,
+		Constraints0, Constraints),
+	UnprovenConstraints = Constraints ^ unproven,
 
 	(
 		UnprovenConstraints = [],
@@ -1067,13 +1108,21 @@
 	).
 
 %-----------------------------------------------------------------------------%
+%
+% Check for cyclic classes in the class table by traversing the
+% class hierarchy for each class.  While we are doing this, calculate
+% the set of ancestors with functional dependencies for each class,
+% and enter this information in the class table.
+%
 
-:- pred check_for_cyclic_classes(class_table::in, bool::out, io::di, io::uo)
-	is det.
+:- pred check_for_cyclic_classes(module_info::in, module_info::out, bool::out,
+	io::di, io::uo) is det.
 
-check_for_cyclic_classes(ClassTable, Errors, !IO) :-
-	ClassIds = map__keys(ClassTable),
-	foldl2(find_cycles(ClassTable, []), ClassIds, set.init, _, [], Cycles),
+check_for_cyclic_classes(!ModuleInfo, Errors, !IO) :-
+	module_info_classes(!.ModuleInfo, ClassTable0),
+	ClassIds = map__keys(ClassTable0),
+	foldl3(find_cycles([]), ClassIds, ClassTable0, ClassTable, set.init, _,
+		[], Cycles),
 	(
 		Cycles = [],
 		Errors = no
@@ -1081,22 +1130,37 @@
 		Cycles = [_ | _],
 		Errors = yes,
 		foldl(report_cyclic_classes(ClassTable), Cycles, !IO)
-	).
+	),
+	module_info_set_classes(ClassTable, !ModuleInfo).
 
 :- type class_path == list(class_id).
 
-	% find_cycles(ClassTable, Path, ClassId, !Visited, !Cycles)
+	% find_cycles(Path, ClassId, !ClassTable, !Visited, !Cycles)
 	%
 	% Perform a depth first traversal of the class hierarchy, starting
 	% from ClassId.  Path contains a list of nodes joining the current
 	% node to the root.  When we reach a node that has already been
 	% visited, check whether there is a cycle in the Path.
 	%
-:- pred find_cycles(class_table::in, class_path::in, class_id::in,
+:- pred find_cycles(class_path::in, class_id::in,
+	class_table::in, class_table::out,
+	set(class_id)::in, set(class_id)::out,
+	list(class_path)::in, list(class_path)::out) is det.
+
+find_cycles(Path, ClassId, !ClassTable, !Visited, !Cycles) :-
+	find_cycles_2(Path, ClassId, _, _, !ClassTable, !Visited, !Cycles).
+
+	% As above, but also return this class's parameters and ancestor list.
+	%
+:- pred find_cycles_2(class_path::in, class_id::in, list(tvar)::out,
+	list(prog_constraint)::out, class_table::in, class_table::out,
 	set(class_id)::in, set(class_id)::out,
 	list(class_path)::in, list(class_path)::out) is det.
 
-find_cycles(ClassTable, Path, ClassId, !Visited, !Cycles) :-
+find_cycles_2(Path, ClassId, Params, Ancestors, !ClassTable, !Visited,
+		!Cycles) :-
+	ClassDefn0 = map.lookup(!.ClassTable, ClassId),
+	Params = ClassDefn0 ^ class_vars,
 	( set.member(ClassId, !.Visited) ->
 		(
 			find_cycle(ClassId, Path, [ClassId], Cycle)
@@ -1104,14 +1168,54 @@
 			!:Cycles = [Cycle | !.Cycles]
 		;
 			true
-		)
+		),
+		Ancestors = ClassDefn0 ^ class_fundep_ancestors
 	;
 		svset.insert(ClassId, !Visited),
-		ClassIds = get_superclass_ids(ClassTable, ClassId),
-		foldl2(find_cycles(ClassTable, [ClassId | Path]), ClassIds,
-			!Visited, !Cycles)
+
+			%
+			% Make this class its own ancestor, but only if it
+			% has fundeps on it.
+			%
+		FunDeps = ClassDefn0 ^ class_fundeps,
+		(
+			FunDeps = [],
+			Ancestors0 = []
+		;
+			FunDeps = [_ | _],
+			ClassId = class_id(ClassName, _),
+			term.var_list_to_term_list(Params, ParamTerms),
+			Ancestors0 = [constraint(ClassName, ParamTerms)]
+		),
+		Superclasses = ClassDefn0 ^ class_supers,
+		foldl4(find_cycles_3([ClassId | Path]), Superclasses,
+			!ClassTable, !Visited, !Cycles, Ancestors0, Ancestors),
+		ClassDefn = ClassDefn0 ^ class_fundep_ancestors := Ancestors,
+		svmap.det_update(ClassId, ClassDefn, !ClassTable)
 	).
 
+	% As we go, accumulate the ancestors from all the superclasses,
+	% with the class parameters bound to the corresponding arguments.
+	% Note that we don't need to merge varsets because typeclass
+	% parameters are guaranteed to be distinct variables.
+	%
+:- pred find_cycles_3(class_path::in, prog_constraint::in,
+	class_table::in, class_table::out,
+	set(class_id)::in, set(class_id)::out,
+	list(class_path)::in, list(class_path)::out,
+	list(prog_constraint)::in, list(prog_constraint)::out) is det.
+
+find_cycles_3(Path, Constraint, !ClassTable, !Visited, !Cycles, !Ancestors) :-
+	Constraint = constraint(Name, Args),
+	list.length(Args, Arity),
+	ClassId = class_id(Name, Arity),
+	find_cycles_2(Path, ClassId, Params, NewAncestors0, !ClassTable,
+		!Visited, !Cycles),
+	map.from_corresponding_lists(Params, Args, Binding),
+	apply_subst_to_prog_constraint_list(Binding, NewAncestors0,
+		NewAncestors),
+	list.append(NewAncestors, !Ancestors).
+
 	% find_cycle(ClassId, PathRemaining, PathSoFar, Cycle)
 	%
 	% Check if ClassId is present in PathRemaining, and if so then make
@@ -1130,17 +1234,6 @@
 		find_cycle(ClassId, Tail, Path, Cycle)
 	).
 
-:- func get_superclass_ids(class_table, class_id) = list(class_id).
-
-get_superclass_ids(ClassTable, ClassId) = SuperclassIds :-
-	ClassDefn = map.lookup(ClassTable, ClassId),
-	SuperclassIds = list.map(get_constraint_class_id,
-		ClassDefn ^ class_supers).
-
-:- func get_constraint_class_id(prog_constraint) = class_id.
-
-get_constraint_class_id(constraint(Name, Args)) = class_id(Name, length(Args)).
-
 	% Report an error using the format
 	%
 	%	module.m:NNN: Error: cyclic superclass relation detected:
@@ -1173,27 +1266,446 @@
 add_path_element(class_id(Name, Arity), RevPieces0) =
 	[sym_name_and_arity(Name/Arity), words("<=") | RevPieces0].
 
-
 %---------------------------------------------------------------------------%
-%
-% Check that all types appearing in universal (existential) constraints are
-% universally (existentially) quantified.
-%
 
-:- pred check_constraint_quant(module_info::in, module_info::out,
+	% Check that all instances are range restricted with respect to the
+	% functional dependencies.  This means that, for each functional
+	% dependency, the set of tvars in the range arguments must be a
+	% subset of the set of tvars in the domain arguments.
+	% (Note that with the requirement of distinct variables as arguments,
+	% this implies that all range arguments must be ground.  However,
+	% this code should work even if that requirement is lifted in future.)
+	%
+	% Also, check that all pairs of visible instances are mutually
+	% consistent with respect to the functional dependencies.  This is
+	% true iff the most general unifier of corresponding domain arguments
+	% (if it exists) is also a unifier of the corresponding range
+	% arguments.
+	%
+:- pred check_functional_dependencies(module_info::in, module_info::out,
 	bool::out, io::di, io::uo) is det.
 
-check_constraint_quant(!ModuleInfo, FoundError, !IO) :-
+check_functional_dependencies(!ModuleInfo, FoundError, !IO) :-
+	module_info_instances(!.ModuleInfo, InstanceTable),
+	map.keys(InstanceTable, ClassIds),
+	list.foldl3(check_fundeps_class, ClassIds, !ModuleInfo, no, FoundError,
+		!IO).
+
+:- pred check_fundeps_class(class_id::in, module_info::in, module_info::out,
+	bool::in, bool::out, io::di, io::uo) is det.
+
+check_fundeps_class(ClassId, !ModuleInfo, !FoundError, !IO) :-
+	module_info_classes(!.ModuleInfo, ClassTable),
+	map.lookup(ClassTable, ClassId, ClassDefn),
+	module_info_instances(!.ModuleInfo, InstanceTable),
+	map.lookup(InstanceTable, ClassId, InstanceDefns),
+	FunDeps = ClassDefn ^ class_fundeps,
+	check_range_restrictedness(ClassId, InstanceDefns, FunDeps,
+		!ModuleInfo, !FoundError, !IO),
+	check_consistency(ClassId, ClassDefn, InstanceDefns, FunDeps,
+		!ModuleInfo, !FoundError, !IO).
+
+:- pred check_range_restrictedness(class_id::in, list(hlds_instance_defn)::in,
+	hlds_class_fundeps::in, module_info::in, module_info::out,
+	bool::in, bool::out, io::di, io::uo) is det.
+
+check_range_restrictedness(_, [], _, !ModuleInfo, !FoundError, !IO).
+check_range_restrictedness(ClassId, [InstanceDefn | InstanceDefns], FunDeps,
+		!ModuleInfo, !FoundError, !IO) :-
+	list.foldl3(check_range_restrictedness_2(ClassId, InstanceDefn),
+		FunDeps, !ModuleInfo, !FoundError, !IO),
+	check_range_restrictedness(ClassId, InstanceDefns, FunDeps,
+		!ModuleInfo, !FoundError, !IO).
+
+:- pred check_range_restrictedness_2(class_id::in, hlds_instance_defn::in,
+	hlds_class_fundep::in, module_info::in, module_info::out,
+	bool::in, bool::out, io::di, io::uo) is det.
+
+check_range_restrictedness_2(ClassId, InstanceDefn, FunDep, !ModuleInfo,
+		!FoundError, !IO) :-
+	Types = InstanceDefn ^ instance_types,
+	FunDep = fundep(Domain, Range),
+	DomainTypes = restrict_list_elements(Domain, Types),
+	DomainVars = term.vars_list(DomainTypes),
+	RangeTypes = restrict_list_elements(Range, Types),
+	RangeVars = term.vars_list(RangeTypes),
+	solutions((pred(V::out) is nondet :-
+			member(V, RangeVars),
+			\+ member(V, DomainVars)
+		), UnboundVars),
+	(
+		UnboundVars = []
+	;
+		UnboundVars = [_ | _],
+		report_range_restriction_error(ClassId, InstanceDefn,
+			UnboundVars, !IO),
+		!:FoundError = yes,
+		module_info_incr_errors(!ModuleInfo)
+	).
+
+% The error message is intended to look like this:
+%
+% very_long_module_name:001: In instance for typeclass `long_class/2':
+% very_long_module_name:001:   functional dependency not satisfied: type
+% very_long_module_name:001:   variables T1, T2 and T3 occur in the range of a
+% very_long_module_name:001:   functional dependency, but are not in the
+% very_long_module_name:001:   domain.
+
+:- pred report_range_restriction_error(class_id::in, hlds_instance_defn::in,
+	list(tvar)::in, io::di, io::uo) is det.
+
+report_range_restriction_error(ClassId, InstanceDefn, Vars, !IO) :-
+	ClassId = class_id(SymName, Arity),
+	TVarSet = InstanceDefn ^ instance_tvarset,
+	Context = InstanceDefn ^ instance_context,
+
+	VarsStrs = list.map(
+			(func(Var) = mercury_var_to_string(Var, TVarSet, no)),
+			Vars),
+
+	Msg = [ words("In instance for typeclass"),
+		sym_name_and_arity(SymName / Arity),
+		suffix(":"), nl,
+		words("functional dependency not satisfied:"),
+		words(choose_number(Vars, "type variable", "type variables"))]
+		++ list_to_pieces(VarsStrs) ++
+		[words(choose_number(Vars, "occurs", "occur")),
+		words("in the range of the functional dependency, but"),
+		words(choose_number(Vars, "is", "are")),
+		words("not in the domain.")],
+	write_error_pieces(Context, 0, Msg, !IO),
+	io__set_exit_status(1, !IO).
+
+	% Check the consistency of each (unordered) pair of instances.
+	%
+:- pred check_consistency(class_id::in, hlds_class_defn::in,
+	list(hlds_instance_defn)::in, hlds_class_fundeps::in,
+	module_info::in, module_info::out, bool::in, bool::out,
+	io::di, io::uo) is det.
+
+check_consistency(_, _, [], _, !ModuleInfo, !FoundError, !IO).
+check_consistency(ClassId, ClassDefn, [Instance | Instances], FunDeps,
+		!ModuleInfo, !FoundError, !IO) :-
+	list.foldl3(
+		check_consistency_pair(ClassId, ClassDefn, FunDeps, Instance),
+		Instances, !ModuleInfo, !FoundError, !IO),
+	check_consistency(ClassId, ClassDefn, Instances, FunDeps, !ModuleInfo,
+		!FoundError, !IO).
+
+:- pred check_consistency_pair(class_id::in, hlds_class_defn::in,
+	hlds_class_fundeps::in, hlds_instance_defn::in, hlds_instance_defn::in,
+	module_info::in, module_info::out, bool::in, bool::out, io::di, io::uo)
+	is det.
+
+check_consistency_pair(ClassId, ClassDefn, FunDeps, InstanceA, InstanceB,
+		!ModuleInfo, !FoundError, !IO) :-
+	list.foldl3(
+		check_consistency_pair_2(ClassId, ClassDefn, InstanceA,
+			InstanceB),
+		FunDeps, !ModuleInfo, !FoundError, !IO).
+
+:- pred check_consistency_pair_2(class_id::in, hlds_class_defn::in,
+	hlds_instance_defn::in, hlds_instance_defn::in, hlds_class_fundep::in,
+	module_info::in, module_info::out, bool::in, bool::out, io::di, io::uo)
+	is det.
+
+check_consistency_pair_2(ClassId, ClassDefn, InstanceA, InstanceB, FunDep,
+		!ModuleInfo, !FoundError, !IO) :-
+	TVarSetA = InstanceA ^ instance_tvarset,
+	TVarSetB = InstanceB ^ instance_tvarset,
+	varset.merge_subst(TVarSetA, TVarSetB, _, RenameSubst),
+
+	TypesA = InstanceA ^ instance_types,
+	TypesB0 = InstanceB ^ instance_types,
+	TypesB = term.apply_substitution_to_list(TypesB0, RenameSubst),
+
+	FunDep = fundep(Domain, Range),
+	DomainA = restrict_list_elements(Domain, TypesA),
+	DomainB = restrict_list_elements(Domain, TypesB),
+
+	(
+		type_unify_list(DomainA, DomainB, [], map.init, Subst)
+	->
+		RangeA0 = restrict_list_elements(Range, TypesA),
+		RangeB0 = restrict_list_elements(Range, TypesB),
+		term.apply_rec_substitution_to_list(RangeA0, Subst, RangeA),
+		term.apply_rec_substitution_to_list(RangeB0, Subst, RangeB),
+		(
+			RangeA = RangeB
+		->
+			true
+		;
+			report_consistency_error(ClassId, ClassDefn, InstanceA,
+				InstanceB, FunDep, !IO),
+			!:FoundError = yes,
+			module_info_incr_errors(!ModuleInfo)
+		)
+	;
+		true
+	).
+
+:- pred report_consistency_error(class_id::in, hlds_class_defn::in,
+	hlds_instance_defn::in, hlds_instance_defn::in, hlds_class_fundep::in,
+	io::di, io::uo) is det.
+
+report_consistency_error(ClassId, ClassDefn, InstanceA, InstanceB, FunDep,
+		!IO) :-
+	ClassId = class_id(SymName, Arity),
+	Params = ClassDefn ^ class_vars,
+	TVarSet = ClassDefn ^ class_tvarset,
+	ContextA = InstanceA ^ instance_context,
+	ContextB = InstanceB ^ instance_context,
+
+	FunDep = fundep(Domain, Range),
+	DomainParams = restrict_list_elements(Domain, Params),
+	RangeParams = restrict_list_elements(Range, Params),
+	DomainList = mercury_vars_to_string(DomainParams, TVarSet, no),
+	RangeList = mercury_vars_to_string(RangeParams, TVarSet, no),
+	FunDepStr = "`(" ++ DomainList ++ " -> " ++ RangeList ++ ")'",
+
+	ErrorPiecesA = [
+		words("Inconsistent instance declaration for typeclass"),
+		sym_name_and_arity(SymName / Arity),
+		words("with functional dependency"),
+		fixed(FunDepStr),
+		suffix(".")
+	],
+	ErrorPiecesB = [
+		words("Here is the conflicting instance.")
+	],
+		
+	write_error_pieces(ContextA, 0, ErrorPiecesA, !IO),
+	write_error_pieces(ContextB, 0, ErrorPiecesB, !IO),
+	io__set_exit_status(1, !IO).
+
+	% XXX this is duplicated in typecheck
+:- func restrict_list_elements(set(int), list(T)) = list(T).
+
+restrict_list_elements(Elements, List) =
+        restrict_list_elements_2(Elements, 1, List).
+
+:- func restrict_list_elements_2(set(int), int, list(T)) = list(T).
+
+restrict_list_elements_2(_, _, []) = [].
+restrict_list_elements_2(Elements, Index, [X | Xs]) =
+        (
+                set__member(Index, Elements)
+        ->
+                [X | restrict_list_elements_2(Elements, Index + 1, Xs)]
+        ;
+                restrict_list_elements_2(Elements, Index + 1, Xs)
+        ).
+
+%---------------------------------------------------------------------------%
+
+	% Look for pred or func declarations for which the type variables in
+	% the constraints are not all determined by the type variables in the
+	% type and the functional dependencies.
+	%
+:- pred check_typeclass.check_constraints(module_info::in,
+	module_info::out, bool::out, io::di, io::uo) is det.
+
+check_typeclass.check_constraints(!ModuleInfo, FoundError, !IO) :-
 	module_info_predids(!.ModuleInfo, PredIds),
-	list.foldl3(check_constraint_quant_2, PredIds, !ModuleInfo,
+	list.foldl3(check_pred_constraints, PredIds, !ModuleInfo,
 		no, FoundError, !IO).
 
-:- pred check_constraint_quant_2(pred_id::in,
+:- pred check_pred_constraints(pred_id::in, module_info::in,
+	module_info::out, bool::in, bool::out, io::di, io::uo) is det.
+
+check_pred_constraints(PredId, !ModuleInfo, !FoundError, !IO) :-
+	module_info_pred_info(!.ModuleInfo, PredId, PredInfo),
+	(
+		pred_info_import_status(PredInfo, ImportStatus),
+		needs_no_ambiguity_check(ImportStatus)
+	->
+		true
+	;
+		write_pred_progress_message(
+			"% Checking typeclass constraints on ",
+			PredId, !.ModuleInfo, !IO),
+		check_pred_type_ambiguities(PredInfo, !ModuleInfo, !FoundError,
+			!IO),
+		check_constraint_quant(PredInfo, !ModuleInfo, !FoundError, !IO)
+	).
+
+:- pred needs_no_ambiguity_check(import_status::in) is semidet.
+
+needs_no_ambiguity_check(imported(_)).
+needs_no_ambiguity_check(opt_imported).
+needs_no_ambiguity_check(abstract_imported).
+needs_no_ambiguity_check(pseudo_imported).
+
+:- pred check_pred_type_ambiguities(pred_info::in, module_info::in,
+	module_info::out, bool::in, bool::out, io::di, io::uo) is det.
+
+check_pred_type_ambiguities(PredInfo, !ModuleInfo, !FoundError, !IO) :-
+	pred_info_arg_types(PredInfo, ArgTypes),
+	TVars = list_to_set(term.vars_list(ArgTypes)),
+	pred_info_get_class_context(PredInfo, Constraints),
+	module_info_classes(!.ModuleInfo, ClassTable),
+	InducedFunDeps = induced_fundeps(ClassTable, Constraints),
+	FunDepsClosure = fundeps_closure(InducedFunDeps, TVars),
+	solutions(constrained_var_not_in_closure(Constraints, FunDepsClosure),
+		UnboundTVars),
+	(
+		UnboundTVars = []
+	->
+		true
+	;
+		report_unbound_tvars_in_class_context(UnboundTVars, PredInfo,
+			!IO),
+		!:FoundError = yes,
+		module_info_incr_errors(!ModuleInfo)
+	).
+
+:- pred constrained_var_not_in_closure(prog_constraints::in, set(tvar)::in,
+	tvar::out) is nondet.
+
+constrained_var_not_in_closure(ClassContext, Closure, UnboundTVar) :-
+	ClassContext = constraints(UnivCs, ExistCs),
+	(
+		Constraints = UnivCs
+	;
+		Constraints = ExistCs
+	),
+	prog_type.constraint_list_get_tvars(Constraints, TVars),
+	list.member(UnboundTVar, TVars),
+	\+ set.member(UnboundTVar, Closure).
+
+:- type induced_fundeps == list(induced_fundep).
+:- type induced_fundep
+	--->	fundep(
+			domain		:: set(tvar),
+			range		:: set(tvar)
+		).
+
+:- func induced_fundeps(class_table, prog_constraints) = induced_fundeps.
+
+induced_fundeps(ClassTable, constraints(UnivCs, ExistCs))
+	= foldl(induced_fundeps_2(ClassTable), UnivCs,
+		foldl(induced_fundeps_2(ClassTable), ExistCs, [])).
+
+:- func induced_fundeps_2(class_table, prog_constraint, induced_fundeps)
+	= induced_fundeps.
+
+induced_fundeps_2(ClassTable, constraint(Name, Args), FunDeps0) = FunDeps :-
+	Arity = length(Args),
+	ClassDefn = map.lookup(ClassTable, class_id(Name, Arity)),
+	FunDeps = foldl(induced_fundep(Args), ClassDefn ^ class_fundeps,
+		FunDeps0).
+
+:- func induced_fundep(list(type), hlds_class_fundep, induced_fundeps)
+	= induced_fundeps.
+
+induced_fundep(Args, fundep(Domain0, Range0), FunDeps)
+		= [fundep(Domain, Range) | FunDeps] :-
+	Domain = set.fold(induced_vars(Args), Domain0, set.init),
+	Range = set.fold(induced_vars(Args), Range0, set.init).
+
+:- func induced_vars(list(type), int, set(tvar)) = set(tvar).
+
+induced_vars(Args, ArgNum, Vars) = union(Vars, NewVars) :-
+	Arg = list.index1_det(Args, ArgNum),
+	NewVars = set.list_to_set(term.vars(Arg)).
+
+:- func fundeps_closure(induced_fundeps, set(tvar)) = set(tvar).
+
+fundeps_closure(FunDeps, TVars) = fundeps_closure_2(FunDeps, TVars, set.init).
+
+:- func fundeps_closure_2(induced_fundeps, set(tvar), set(tvar)) = set(tvar).
+
+fundeps_closure_2(FunDeps0, NewVars0, Result0) = Result :-
+	(
+		set.empty(NewVars0)
+	->
+		Result = Result0
+	;
+		Result1 = set.union(Result0, NewVars0),
+		FunDeps1 = list.map(remove_vars(NewVars0), FunDeps0),
+		list.foldl2(collect_determined_vars, FunDeps1, [], FunDeps,
+			set.init, NewVars),
+		Result = fundeps_closure_2(FunDeps, NewVars, Result1)
+	).
+
+:- func remove_vars(set(tvar), induced_fundep) = induced_fundep.
+
+remove_vars(Vars, fundep(Domain0, Range0)) = fundep(Domain, Range) :-
+	Domain = set.difference(Domain0, Vars),
+	Range = set.difference(Range0, Vars).
+
+:- pred collect_determined_vars(induced_fundep::in, induced_fundeps::in,
+	induced_fundeps::out, set(tvar)::in, set(tvar)::out) is det.
+
+collect_determined_vars(FunDep @ fundep(Domain, Range), !FunDeps, !Vars) :-
+	(
+		set.empty(Domain)
+	->
+		!:Vars = set.union(Range, !.Vars)
+	;
+		!:FunDeps = [FunDep | !.FunDeps]
+	).
+
+% The error message is intended to look like this:
+%
+% very_long_module_name:001: In declaration for function `long_function/2':
+% very_long_module_name:001:   error in type class constraints: type variables
+% very_long_module_name:001:   T1, T2 and T3 occur in the constraints, but are
+% very_long_module_name:001:   not determined by the function's argument or
+% very_long_module_name:001:   result types.
+%
+% very_long_module_name:002: In declaration for predicate `long_predicate/3':
+% very_long_module_name:002:   error in type class constraints: type variable
+% very_long_module_name:002:   T occurs in the constraints, but is not
+% very_long_module_name:002:   determined by the predicate's argument types.
+
+:- pred report_unbound_tvars_in_class_context(list(tvar)::in, pred_info::in,
+	io::di, io::uo) is det.
+
+report_unbound_tvars_in_class_context(Vars, PredInfo, !IO) :-
+	pred_info_context(PredInfo, Context),
+	pred_info_arg_types(PredInfo, TVarSet, _, ArgTypes),
+	PredName = pred_info_name(PredInfo),
+	Module = pred_info_module(PredInfo),
+	SymName = qualified(Module, PredName),
+	Arity = length(ArgTypes),
+	PredOrFunc = pred_info_is_pred_or_func(PredInfo),
+
+	VarsStrs = list.map(
+			(func(Var) = mercury_var_to_string(Var, TVarSet, no)),
+			Vars),
+
+	Msg0 = [words("In declaration for"),
+		words(simple_call_id_to_string(PredOrFunc, SymName, Arity)),
+		suffix(":"), nl,
+		words("error in type class constraints:"),
+		words(choose_number(Vars, "type variable", "type variables"))]
+		++ list_to_pieces(VarsStrs) ++
+		[words(choose_number(Vars, "occurs", "occur")),
+		words("in the constraints, but"),
+		words(choose_number(Vars, "is", "are")),
+		words("not determined by the")],
+	(
+		PredOrFunc = predicate,
+		Msg = Msg0 ++ [words("predicate's argument types.")]
+	;
+		PredOrFunc = function,
+		Msg = Msg0 ++ [words("function's argument or result types.")]
+	),
+	write_error_pieces(Context, 0, Msg, !IO),
+	io__set_exit_status(1, !IO).
+
+%---------------------------------------------------------------------------%
+%
+% Check that all types appearing in universal (existential) constraints are
+% universally (existentially) quantified.
+%
+
+:- pred check_constraint_quant(pred_info::in,
 	module_info::in, module_info::out, bool::in, bool::out,
 	io::di, io::uo) is det.
 
-check_constraint_quant_2(PredId, !ModuleInfo, !FoundError, !IO) :-
-	module_info_pred_info(!.ModuleInfo, PredId, PredInfo),
+check_constraint_quant(PredInfo, !ModuleInfo, !FoundError, !IO) :-
 	pred_info_get_exist_quant_tvars(PredInfo, ExistQVars),
 	pred_info_get_class_context(PredInfo, Constraints),
 	Constraints = constraints(UnivCs, ExistCs),
Index: compiler/dead_proc_elim.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/dead_proc_elim.m,v
retrieving revision 1.98
diff -u -r1.98 dead_proc_elim.m
--- compiler/dead_proc_elim.m	30 Mar 2005 00:50:19 -0000	1.98
+++ compiler/dead_proc_elim.m	2 Apr 2005 08:29:26 -0000
@@ -267,7 +267,7 @@
 	is det.
 
 get_class_pred_procs(Class, !Queue, !Needed) :-
-	Class = hlds_class_defn(_, _, _, _, Methods, _, _),
+	Methods = Class ^ class_hlds_interface,
 	list__foldl2(get_class_interface_pred_proc, Methods, !Queue, !Needed).
 
 :- pred get_class_interface_pred_proc(hlds_class_proc::in,
Index: compiler/equiv_type.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/equiv_type.m,v
retrieving revision 1.45
diff -u -r1.45 equiv_type.m
--- compiler/equiv_type.m	1 Apr 2005 14:28:54 -0000	1.45
+++ compiler/equiv_type.m	2 Apr 2005 10:56:33 -0000
@@ -328,11 +328,11 @@
 	).
 
 equiv_type__replace_in_item(ModuleName,
-		typeclass(Constraints0, ClassName, Vars, ClassInterface0,
-			VarSet0),
+		typeclass(Constraints0, FunDeps, ClassName, Vars,
+			ClassInterface0, VarSet0),
 		_Context, EqvMap, EqvInstMap,
-		typeclass(Constraints, ClassName, Vars, ClassInterface,
-			VarSet),
+		typeclass(Constraints, FunDeps, ClassName, Vars,
+			ClassInterface, VarSet),
 		Errors, !Info) :-
 	list__length(Vars, Arity),
 	equiv_type__maybe_record_expanded_items(ModuleName, ClassName,
Index: compiler/error_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/error_util.m,v
retrieving revision 1.37
diff -u -r1.37 error_util.m
--- compiler/error_util.m	15 Apr 2005 15:14:27 -0000	1.37
+++ compiler/error_util.m	19 Apr 2005 14:50:07 -0000
@@ -49,7 +49,7 @@
 				% in one piece, as it is.
 
 	;	suffix(string)	% This string should appear in the output
-				% in one pieces, as it is, appended directly
+				% in one piece, as it is, appended directly
 				% after the previous format_component, without
 				% any intervening space.
 
Index: compiler/hlds_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_data.m,v
retrieving revision 1.92
diff -u -r1.92 hlds_data.m
--- compiler/hlds_data.m	13 Apr 2005 07:41:27 -0000	1.92
+++ compiler/hlds_data.m	13 Apr 2005 08:44:55 -0000
@@ -26,7 +26,12 @@
 
 :- implementation.
 
+:- import_module check_hlds__type_util.
+
 :- import_module int.
+:- import_module svmulti_map.
+:- import_module term.
+:- import_module varset.
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -786,14 +791,22 @@
 
 :- interface.
 
+:- import_module set.
+
 :- type class_table == map(class_id, hlds_class_defn).
 
 	% Information about a single `typeclass' declaration
+	%
 :- type hlds_class_defn --->
 	hlds_class_defn(
 		class_status		:: import_status,
 		class_supers		:: list(prog_constraint),
 					% SuperClasses
+		class_fundeps		:: hlds_class_fundeps,
+					% Functional dependencies
+		class_fundep_ancestors	:: list(prog_constraint),
+					% All ancestors which have fundeps
+					% on them.
 		class_vars		:: list(tvar),
 					% ClassVars
 		class_interface		:: class_interface,
@@ -811,6 +824,19 @@
 					% Location of declaration
 	).
 
+	% In the HLDS, functional dependencies are represented using
+	% argument positions (counting from 1) rather than type variables.
+	% We know that there will be a one-one correspondence since
+	% typeclass parameters must be distinct variables, and using
+	% argument positions is more efficient.
+	%
+:- type hlds_class_fundeps == list(hlds_class_fundep).
+:- type hlds_class_fundep
+	--->	fundep(
+			domain		:: set(int),
+			range		:: set(int)
+		).
+
 :- type hlds_class_interface	==	list(hlds_class_proc).
 :- type hlds_class_proc
 	---> 	hlds_class_proc(
@@ -819,11 +845,16 @@
 		).
 
 	% For each class, we keep track of a list of its instances, since there
-	% can be more than one instance of each class.
+	% can be more than one instance of each class.  Each visible instance
+	% is assigned a unique identifier (integers beginning from one).
+	% The position in the list of instances corresponds to the instance_id.
 	%
-:- type instance_table == multi_map(class_id, hlds_instance_defn).
+:- type instance_table == map(class_id, list(hlds_instance_defn)).
+
+:- type instance_id == int.
 
 	% Information about a single `instance' declaration
+	%
 :- type hlds_instance_defn --->
 	hlds_instance_defn(
 		instance_module		:: module_name,
@@ -869,7 +900,7 @@
 :- type constraint_id
 	--->	constraint_id(
 			constraint_type,
-				% Existential or universal.
+				% Assumed or unproven.
 
 			goal_path,
 				% The location of the atomic goal which is
@@ -879,8 +910,8 @@
 		).
 
 :- type constraint_type
-	--->	existential
-	;	universal.
+	--->	unproven
+	;	assumed.
 
 	% The identifier of a constraint is stored along with the constraint.
 	% Each value of this type may have more than one identifier because
@@ -896,13 +927,37 @@
 
 :- type hlds_constraints
 	--->	constraints(
-			universal	:: list(hlds_constraint),
-						% Universal constraints.
-
-			existential	:: list(hlds_constraint)
-						% Existential constraints.
+			unproven	:: list(hlds_constraint),
+					% Unproven constraints.  These are
+					% the constraints that we must prove
+					% (that is, universal constraints from
+					% the goal being checked, or
+					% existential constraints on the head).
+
+			assumed		:: list(hlds_constraint),
+					% Assumed constraints.  These are
+					% constraints we can use in proofs
+					% (that is, existential constraints
+					% from the goal being checked, or
+					% universal constraints on the head).
+
+			redundant	:: redundant_constraints
+					% Constraints that are known to be
+					% redundant.  This includes constraints
+					% that have already been proved as well
+					% as constraints that are ancestors of
+					% other unproven or redundant
+					% constraints.  Not all such
+					% constraints are included, only those
+					% which may be used for the purposes
+					% of improvement.
 		).
 
+	% Redundant constraints are partitioned by class, which helps us
+	% process them more efficiently.
+	%
+:- type redundant_constraints == multi_map(class_id, hlds_constraint).
+
 	% During type checking we fill in a constraint_map which gives
 	% the constraint that corresponds to each identifier.  This is used
 	% by the polymorphism translation to retrieve details of constraints.
@@ -911,7 +966,7 @@
 
 	% `Proof' of why a constraint is redundant
 :- type constraint_proof
-			% Apply the instance decl with the given number.
+			% Apply the instance decl with the given identifier.
 			% Note that we don't store the actual
 			% hlds_instance_defn for two reasons:
 			% - That would require storing a renamed version of
@@ -925,23 +980,52 @@
 			%   would require the class relation to be
 			%   topologically sorted before checking the
 			%   instance declarations.
-	--->	apply_instance(int)
+	--->	apply_instance(instance_id)
 
 			% The constraint is redundant because of the
 			% following class's superclass declaration
 	;	superclass(prog_constraint).
 
+	% The constraint_proof_map is a map which for each type class
+	% constraint records how/why that constraint was satisfied.
+	% This information is used to determine how to construct the
+	% typeclass_info for that constraint.
+	%
 :- type constraint_proof_map == map(prog_constraint, constraint_proof).
 
+:- pred empty_hlds_constraints(hlds_constraints::out) is det.
+
 :- pred init_hlds_constraint_list(list(prog_constraint)::in,
 	list(hlds_constraint)::out) is det.
 
-:- pred make_hlds_constraints(prog_constraints::in, goal_path::in,
+:- pred make_head_hlds_constraints(class_table::in, tvarset::in,
+	prog_constraints::in, hlds_constraints::out) is det.
+
+:- pred make_body_hlds_constraints(class_table::in, tvarset::in, goal_path::in,
+	prog_constraints::in, hlds_constraints::out) is det.
+
+	% make_hlds_constraints(ClassTable, TVarSet, UnprovenConstraints,
+	% 	AssumedConstraints, Constraints)
+	%
+	% ClassTable is the class_table for the module.  TVarSet is the
+	% tvarset for the predicate this class context is for.
+	% UnprovenConstraints is a list of constraints which will need to
+	% be proven (that is, universal constraints in the body or
+	% existential constraints in the head).  AssumedConstraints is a
+	% list of constraints that may be used in proofs (that is,
+	% existential constraints in the body or universal constraints in
+	% the head).
+	%
+:- pred make_hlds_constraints(class_table::in, tvarset::in,
+	list(hlds_constraint)::in, list(hlds_constraint)::in,
 	hlds_constraints::out) is det.
 
 :- pred make_hlds_constraint_list(list(prog_constraint)::in,
 	constraint_type::in, goal_path::in, list(hlds_constraint)::out) is det.
 
+:- pred merge_hlds_constraints(hlds_constraints::in, hlds_constraints::in,
+	hlds_constraints::out) is det.
+
 :- pred retrieve_prog_constraints(hlds_constraints::in, prog_constraints::out)
 	is det.
 
@@ -960,6 +1044,10 @@
 :- pred update_constraint_map(hlds_constraint::in, constraint_map::in,
 	constraint_map::out) is det.
 
+:- pred update_redundant_constraints(class_table::in, tvarset::in,
+	list(hlds_constraint)::in,
+	redundant_constraints::in, redundant_constraints::out) is det.
+
 :- pred lookup_hlds_constraint_list(constraint_map::in, constraint_type::in,
 	goal_path::in, int::in, list(prog_constraint)::out) is det.
 
@@ -967,6 +1055,9 @@
 
 :- implementation.
 
+empty_hlds_constraints(Constraints) :-
+	Constraints = constraints([], [], multi_map.init).
+
 init_hlds_constraint_list(ProgConstraints, Constraints) :-
 	list.map(init_hlds_constraint, ProgConstraints, Constraints).
 
@@ -974,14 +1065,31 @@
 
 init_hlds_constraint(constraint(Name, Types), constraint([], Name, Types)).
 
-make_hlds_constraints(ProgConstraints, GoalPath, Constraints) :-
-	ProgConstraints = constraints(UnivProgConstraints,
-		ExistProgConstraints),
-	make_hlds_constraint_list(UnivProgConstraints, universal, GoalPath,
-		UnivConstraints),
-	make_hlds_constraint_list(ExistProgConstraints, existential, GoalPath,
-		ExistConstraints),
-	Constraints = constraints(UnivConstraints, ExistConstraints).
+make_head_hlds_constraints(ClassTable, TVarSet, ProgConstraints,
+		Constraints) :-
+	ProgConstraints = constraints(UnivConstraints, ExistConstraints),
+	GoalPath = [],
+	make_hlds_constraint_list(UnivConstraints, assumed, GoalPath,
+		AssumedConstraints),
+	make_hlds_constraint_list(ExistConstraints, unproven, GoalPath,
+		UnprovenConstraints),
+	make_hlds_constraints(ClassTable, TVarSet, UnprovenConstraints,
+		AssumedConstraints, Constraints).
+
+make_body_hlds_constraints(ClassTable, TVarSet, GoalPath, ProgConstraints,
+		Constraints) :-
+	ProgConstraints = constraints(UnivConstraints, ExistConstraints),
+	make_hlds_constraint_list(UnivConstraints, unproven, GoalPath,
+		UnprovenConstraints),
+	make_hlds_constraint_list(ExistConstraints, assumed, GoalPath,
+		AssumedConstraints),
+	make_hlds_constraints(ClassTable, TVarSet, UnprovenConstraints,
+		AssumedConstraints, Constraints).
+
+make_hlds_constraints(ClassTable, TVarSet, Unproven, Assumed, Constraints) :-
+	list.foldl(update_redundant_constraints_2(ClassTable, TVarSet),
+		Unproven, multi_map.init, Redundant),
+	Constraints = constraints(Unproven, Assumed, Redundant).
 
 make_hlds_constraint_list(ProgConstraints, ConstraintType, GoalPath,
 		Constraints) :-
@@ -999,10 +1107,18 @@
 	H = constraint([Id], Name, Types),
 	make_hlds_constraint_list_2(Ps, T, G, N + 1, Hs).
 
+merge_hlds_constraints(ConstraintsA, ConstraintsB, Constraints) :-
+	ConstraintsA = constraints(UnprovenA, AssumedA, RedundantA),
+	ConstraintsB = constraints(UnprovenB, AssumedB, RedundantB),
+	list.append(UnprovenA, UnprovenB, Unproven),
+	list.append(AssumedA, AssumedB, Assumed),
+	multi_map.merge(RedundantA, RedundantB, Redundant),
+	Constraints = constraints(Unproven, Assumed, Redundant).
+
 retrieve_prog_constraints(Constraints, ProgConstraints) :-
-	Constraints = constraints(UnivConstraints, ExistConstraints),
-	retrieve_prog_constraint_list(UnivConstraints, UnivProgConstraints),
-	retrieve_prog_constraint_list(ExistConstraints, ExistProgConstraints),
+	Constraints = constraints(Unproven, Assumed, _),
+	retrieve_prog_constraint_list(Unproven, UnivProgConstraints),
+	retrieve_prog_constraint_list(Assumed, ExistProgConstraints),
 	ProgConstraints = constraints(UnivProgConstraints,
 		ExistProgConstraints).
 
@@ -1035,6 +1151,58 @@
 update_constraint_map_2(ProgConstraint, ConstraintId, ConstraintMap0,
 		ConstraintMap) :-
 	map.set(ConstraintMap0, ConstraintId, ProgConstraint, ConstraintMap).
+
+update_redundant_constraints(ClassTable, TVarSet, Constraints, !Redundant) :-
+	list.foldl(update_redundant_constraints_2(ClassTable, TVarSet),
+		Constraints, !Redundant).
+
+:- pred update_redundant_constraints_2(class_table::in, tvarset::in,
+	hlds_constraint::in, redundant_constraints::in,
+	redundant_constraints::out) is det.
+
+update_redundant_constraints_2(ClassTable, TVarSet, Constraint, !Redundant) :-
+	Constraint = constraint(_, Name, Args),
+	list.length(Args, Arity),
+	ClassId = class_id(Name, Arity),
+	map.lookup(ClassTable, ClassId, ClassDefn),
+	ClassAncestors0 = ClassDefn ^ class_fundep_ancestors,
+	list.map(init_hlds_constraint, ClassAncestors0, ClassAncestors),
+	(
+		% Optimize the simple case.
+		ClassAncestors = []
+	;
+		ClassAncestors = [_ | _],
+		ClassTVarSet = ClassDefn ^ class_tvarset,
+		ClassParams = ClassDefn ^ class_vars,
+
+			%
+			% We can ignore the resulting tvarset, since any new
+			% variables will become bound when the arguments are
+			% bound.  (This follows from the fact that constraints
+			% on class declarations can only use variables that
+			% appear in the head of the declaration.)
+			%
+		varset.merge_subst(TVarSet, ClassTVarSet, _, RenameSubst),
+		apply_subst_to_constraint_list(RenameSubst, ClassAncestors,
+			RenamedAncestors),
+		term.var_list_to_term_list(ClassParams, ClassParamTerms),
+		term.apply_substitution_to_list(ClassParamTerms, RenameSubst,
+			RenamedParamTerms),
+		term.term_list_to_var_list(RenamedParamTerms, RenamedParams),
+		map.from_corresponding_lists(RenamedParams, Args, Subst),
+		apply_subst_to_constraint_list(Subst, RenamedAncestors,
+			Ancestors),
+		list.foldl(add_redundant_constraint, Ancestors, !Redundant)
+	).
+
+:- pred add_redundant_constraint(hlds_constraint::in,
+	redundant_constraints::in, redundant_constraints::out) is det.
+
+add_redundant_constraint(Constraint, !Redundant) :-
+	Constraint = constraint(_, Name, Args),
+	list.length(Args, Arity),
+	ClassId = class_id(Name, Arity),
+	svmulti_map.add(ClassId, Constraint, !Redundant).
 
 lookup_hlds_constraint_list(ConstraintMap, ConstraintType, GoalPath, Count,
 		Constraints) :-
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.353
diff -u -r1.353 hlds_out.m
--- compiler/hlds_out.m	7 Apr 2005 06:32:08 -0000	1.353
+++ compiler/hlds_out.m	11 Apr 2005 12:33:21 -0000
@@ -3420,8 +3420,8 @@
 	hlds_out__write_class_id(ClassId, !IO),
 	io__write_string(":\n", !IO),
 
-	ClassDefn = hlds_class_defn(_, Constraints, Vars, _, Interface,
-		VarSet, Context),
+	ClassDefn = hlds_class_defn(_, Constraints, FunDeps, _, Vars, _,
+		Interface, VarSet, Context),
 
 	term__context_file(Context, FileName),
 	term__context_line(Context, LineNumber),
@@ -3449,6 +3449,11 @@
 	io__nl(!IO),
 
 	hlds_out__write_indent(Indent, !IO),
+	io__write_string("% Functional dependencies: ", !IO),
+	io__write_list(FunDeps, ", ", hlds_output_fundep, !IO),
+	io__nl(!IO),
+
+	hlds_out__write_indent(Indent, !IO),
 	io__write_string("% Constraints: ", !IO),
 	io__write_list(Constraints, ", ",
 		mercury_output_constraint(VarSet, AppendVarNums), !IO),
@@ -3459,6 +3464,27 @@
 	io__write_list(Interface, ", ", hlds_out__write_class_proc, !IO),
 	io__nl(!IO).
 
+:- pred hlds_output_fundep(hlds_class_fundep::in, io::di, io::uo) is det.
+
+hlds_output_fundep(fundep(Domain, Range), !IO) :-
+	hlds_output_fundep_2(Domain, !IO),
+	io.write_string(" >> ", !IO),
+	hlds_output_fundep_2(Range, !IO).
+
+:- pred hlds_output_fundep_2(set(int)::in, io::di, io::uo) is det.
+
+hlds_output_fundep_2(ArgNumSet, !IO) :-
+	ArgNumList = set.to_sorted_list(ArgNumSet),
+	(
+		ArgNumList = [ArgNum]
+	->
+		io.write_int(ArgNum, !IO)
+	;
+		io.write_char('{', !IO),
+		io.write_list(ArgNumList, ", ", io.write_int, !IO),
+		io.write_char('}', !IO)
+	).
+
 	% Just output the class methods as pred_ids and proc_ids because
 	% its probably not that useful to have the names. If that information
 	% is needed, it shouldn't be a very difficult fix.
@@ -3999,10 +4025,10 @@
 hlds_out__write_constraint_id(ConstraintId, !IO) :-
 	ConstraintId = constraint_id(ConstraintType, GoalPath, N),
 	(
-		ConstraintType = existential,
+		ConstraintType = assumed,
 		io__write_string("(E, ", !IO)
 	;
-		ConstraintType = universal,
+		ConstraintType = unproven,
 		io__write_string("(A, ", !IO)
 	),
 	goal_path_to_string(GoalPath, GoalPathStr),
Index: compiler/intermod.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/intermod.m,v
retrieving revision 1.169
diff -u -r1.169 intermod.m
--- compiler/intermod.m	24 Mar 2005 05:34:05 -0000	1.169
+++ compiler/intermod.m	10 Apr 2005 15:17:56 -0000
@@ -1440,21 +1440,38 @@
 	hlds_class_defn::in, io::di, io::uo) is det.
 
 intermod__write_class(ModuleName, ClassId, ClassDefn, !IO) :-
-	ClassDefn = hlds_class_defn(ImportStatus, Constraints,
-		TVars, Interface, _HLDSClassInterface,
+	ClassDefn = hlds_class_defn(ImportStatus, Constraints, HLDSFunDeps,
+		_Ancestors, TVars, Interface, _HLDSClassInterface,
 		TVarSet, Context),
 	ClassId = class_id(QualifiedClassName, _),
 	(
 		QualifiedClassName = qualified(ModuleName, _),
 		import_status_to_write(ImportStatus)
 	->
-		Item = typeclass(Constraints, QualifiedClassName, TVars,
-			Interface, TVarSet),
+		FunDeps = list.map(unmake_hlds_class_fundep(TVars),
+			HLDSFunDeps),
+		Item = typeclass(Constraints, FunDeps, QualifiedClassName,
+			TVars, Interface, TVarSet),
 		mercury_output_item(Item, Context, !IO)
 	;
 		true
 	).
 
+:- func unmake_hlds_class_fundep(list(tvar), hlds_class_fundep) = prog_fundep.
+
+unmake_hlds_class_fundep(TVars, fundep(Domain0, Range0))
+		= fundep(Domain, Range) :-
+	Domain = unmake_hlds_class_fundep_2(TVars, Domain0),
+	Range = unmake_hlds_class_fundep_2(TVars, Range0).
+
+:- func unmake_hlds_class_fundep_2(list(tvar), set(int)) = list(tvar).
+
+unmake_hlds_class_fundep_2(TVars, Set) = solutions(P) :-
+	P = (pred(TVar::out) is nondet :-
+		set.member(N, Set),
+		TVar = list.index1_det(TVars, N)
+	).
+
 :- pred intermod__write_instances(assoc_list(class_id, hlds_instance_defn)::in,
 	io::di, io::uo) is det.
 
@@ -2076,22 +2093,16 @@
 	pair(class_id, hlds_class_defn)::out,
 	module_info::in, module_info::out) is det.
 
-adjust_class_status_2(ClassId - ClassDefn0, ClassId - ClassDefn,
-			ModuleInfo0, ModuleInfo) :-
+adjust_class_status_2(ClassId - ClassDefn0, ClassId - ClassDefn, !ModuleInfo) :-
 	(
-		ClassDefn0 = hlds_class_defn(Status0, Constraints, TVars,
-				Interface, HLDSClassInterface,
-				TVarSet, Context),
-		import_status_to_write(Status0)
+		import_status_to_write(ClassDefn0 ^ class_status)
 	->
-		ClassDefn = hlds_class_defn(exported, Constraints, TVars,
-				Interface, HLDSClassInterface,
-				TVarSet, Context),
-		class_procs_to_pred_ids(HLDSClassInterface, PredIds),
-		set_list_of_preds_exported(PredIds, ModuleInfo0, ModuleInfo)
+		ClassDefn = ClassDefn0 ^ class_status := exported,
+		class_procs_to_pred_ids(ClassDefn ^ class_hlds_interface,
+			PredIds),
+		set_list_of_preds_exported(PredIds, !ModuleInfo)
 	;
-		ClassDefn = ClassDefn0,
-		ModuleInfo = ModuleInfo0
+		ClassDefn = ClassDefn0
 	).
 
 :- pred class_procs_to_pred_ids(list(hlds_class_proc)::in, list(pred_id)::out)
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.511
diff -u -r1.511 make_hlds.m
--- compiler/make_hlds.m	14 Apr 2005 06:50:57 -0000	1.511
+++ compiler/make_hlds.m	15 Apr 2005 15:46:09 -0000
@@ -484,9 +484,9 @@
     Item = nothing(_).
 
 add_item_decl_pass_1(Item, Context, !Status, !ModuleInfo, no, !IO) :-
-    Item = typeclass(Constraints, Name, Vars, Interface, VarSet),
-    module_add_class_defn(Constraints, Name, Vars, Interface, VarSet, Context,
-        !.Status, !ModuleInfo, !IO).
+    Item = typeclass(Constraints, FunDeps, Name, Vars, Interface, VarSet),
+	module_add_class_defn(Constraints, FunDeps, Name, Vars, Interface,
+		VarSet, Context, !.Status, !ModuleInfo, !IO).
 
     % We add instance declarations on the second pass so that we don't add
     % an instance declaration before its class declaration.
@@ -927,7 +927,7 @@
 add_item_decl_pass_2(Item, _, !Status, !ModuleInfo, !IO) :-
     Item = nothing(_).
 add_item_decl_pass_2(Item, _, !Status, !ModuleInfo, !IO) :-
-    Item = typeclass(_, _, _, _, _).
+    Item = typeclass(_, _, _, _, _, _).
 add_item_decl_pass_2(Item, Context, !Status, !ModuleInfo, !IO) :-
     Item = instance(Constraints, Name, Types, Body, VarSet,
         InstanceModuleName),
@@ -1170,8 +1170,8 @@
         !.Status, !ModuleInfo, !QualInfo, !IO).
 
 add_item_clause(nothing(_), !Status, _, !ModuleInfo, !QualInfo, !IO).
-add_item_clause(typeclass(_, _, _, _, _), !Status, _, !ModuleInfo, !QualInfo,
-    !IO).
+add_item_clause(typeclass(_, _, _, _, _, _), !Status, _, !ModuleInfo,
+    !QualInfo, !IO).
 add_item_clause(instance(_, _, _, _, _, _), !Status, _, !ModuleInfo, !QualInfo,
     !IO).
 
@@ -3427,13 +3427,13 @@
         MaybePredProcId = no
     ).
 
-:- pred module_add_class_defn(list(prog_constraint)::in, sym_name::in,
-    list(tvar)::in, class_interface::in, tvarset::in, prog_context::in,
-    item_status::in, module_info::in, module_info::out,
-    io::di, io::uo) is det.
+:- pred module_add_class_defn(list(prog_constraint)::in,
+    list(prog_fundep)::in, sym_name::in, list(tvar)::in, class_interface::in,
+    tvarset::in, prog_context::in, item_status::in,
+    module_info::in, module_info::out, io::di, io::uo) is det.
 
-module_add_class_defn(Constraints, Name, Vars, Interface, VarSet, Context,
-        Status, !ModuleInfo, !IO) :-
+module_add_class_defn(Constraints, FunDeps, Name, Vars, Interface, VarSet,
+        Context, Status, !ModuleInfo, !IO) :-
     module_info_classes(!.ModuleInfo, Classes0),
     module_info_superclasses(!.ModuleInfo, SuperClasses0),
     list__length(Vars, ClassArity),
@@ -3444,13 +3444,15 @@
     ;
         ImportStatus1 = ImportStatus0
     ),
+    HLDSFunDeps = list__map(make_hlds_fundep(Vars), FunDeps),
     (
         % the typeclass is exported if *any* occurrence is exported,
         % even a previous abstract occurrence
         map__search(Classes0, ClassId, OldDefn)
     ->
-        OldDefn = hlds_class_defn(OldStatus, OldConstraints, OldVars,
-            OldInterface, OldMethods, OldVarSet, OldContext),
+        OldDefn = hlds_class_defn(OldStatus, OldConstraints, OldFunDeps,
+            _OldAncestors, OldVars, OldInterface, OldMethods, OldVarSet,
+            OldContext),
         combine_status(ImportStatus1, OldStatus, ImportStatus),
         (
             OldInterface = concrete(_),
@@ -3467,14 +3469,26 @@
         ->
             % Always report the error, even in `.opt' files.
             DummyStatus = local,
-            multiple_def_error(DummyStatus, Name, ClassArity,
-                "typeclass", Context, OldContext, _, !IO),
+            multiple_def_error(DummyStatus, Name, ClassArity, "typeclass",
+                Context, OldContext, _, !IO),
             prog_out__write_context(Context, !IO),
             io__write_string("  The superclass constraints do not match.\n",
                 !IO),
             io__set_exit_status(1, !IO),
             ErrorOrPrevDef = yes
         ;
+            \+ class_fundeps_are_identical(OldFunDeps, HLDSFunDeps)
+        ->
+            % Always report the error, even in `.opt' files.
+            DummyStatus = local,
+            multiple_def_error(DummyStatus, Name, ClassArity, "typeclass",
+                Context, OldContext, _, !IO),
+            prog_out__write_context(Context, !IO),
+            io__write_string("  The functional dependencies do not match.\n",
+                !IO),
+            io__set_exit_status(1, !IO),
+            ErrorOrPrevDef = yes
+        ;
             Interface = concrete(_),
             OldInterface = concrete(_)
         ->
@@ -3517,8 +3531,10 @@
             ClassMethods = ClassMethods0
         ),
 
-        Defn = hlds_class_defn(ImportStatus, Constraints, Vars,
-            ClassInterface, ClassMethods, VarSet, Context),
+        % Ancestors is not set until check_typeclass.
+        Ancestors = [],
+        Defn = hlds_class_defn(ImportStatus, Constraints, HLDSFunDeps,
+            Ancestors, Vars, ClassInterface, ClassMethods, VarSet, Context),
         map__set(Classes0, ClassId, Defn, Classes),
         module_info_set_classes(Classes, !ModuleInfo),
 
@@ -3540,6 +3556,32 @@
         true
     ).
 
+:- func make_hlds_fundep(list(tvar), prog_fundep) = hlds_class_fundep.
+
+make_hlds_fundep(TVars, fundep(Domain0, Range0)) = fundep(Domain, Range) :-
+	Domain = make_hlds_fundep_2(TVars, Domain0),
+	Range = make_hlds_fundep_2(TVars, Range0).
+
+:- func make_hlds_fundep_2(list(tvar), list(tvar)) = set(int).
+
+make_hlds_fundep_2(TVars, List) = list.foldl(Func, List, set.init) :-
+	Func = (func(TVar, Set0) = set.insert(Set0, N) :-
+		N = get_list_index(TVars, 1, TVar)
+	).
+
+:- func get_list_index(list(T), int, T) = int.
+
+get_list_index([], _, _) = _ :-
+	error("get_list_index: element not found").
+get_list_index([E | Es], N, X) =
+	(
+		X = E
+	->
+		N
+	;
+		get_list_index(Es, N + 1, X)
+	).
+
 :- pred superclass_constraints_are_identical(list(tvar)::in, tvarset::in,
     list(prog_constraint)::in, list(tvar)::in, tvarset::in,
     list(prog_constraint)::in) is semidet.
@@ -3556,6 +3598,17 @@
         OldConstraints1, OldConstraints),
     OldConstraints = Constraints.
 
+:- pred class_fundeps_are_identical(hlds_class_fundeps::in,
+	hlds_class_fundeps::in) is semidet.
+
+class_fundeps_are_identical(OldFunDeps0, FunDeps0) :-
+	% Allow for the functional dependencies to be in a different order.
+	% we rely on the fact that sets (ordered lists) have a canonical
+	% representation.
+	sort_and_remove_dups(OldFunDeps0, OldFunDeps),
+	sort_and_remove_dups(FunDeps0, FunDeps),
+	OldFunDeps = FunDeps.
+
 :- pred module_add_class_interface(sym_name::in, list(tvar)::in,
     list(class_method)::in, item_status::in,
     list(maybe(pair(pred_id, proc_id)))::out,
@@ -3786,8 +3839,6 @@
     ;
         Status = ItemStatus
     ),
-    check_tvars_in_constraints(ClassContext, Types, TVarSet, PredOrFunc,
-        PredName, Context, !ModuleInfo, !IO),
     module_info_name(!.ModuleInfo, ModuleName),
     list__length(Types, Arity),
     (
@@ -3842,88 +3893,6 @@
             module_info_set_predicate_table(PredTable, !ModuleInfo)
         )
     ).
-
-%-----------------------------------------------------------------------------%
-
-    %
-    % check for type variables which occur in the the class constraints,
-    % but which don't occur in the predicate argument types
-    %
-:- pred check_tvars_in_constraints(prog_constraints::in, list(type)::in,
-    tvarset::in, pred_or_func::in, sym_name::in, prog_context::in,
-    module_info::in, module_info::out, io::di, io::uo) is det.
-
-check_tvars_in_constraints(ClassContext, ArgTypes, TVarSet,
-        PredOrFunc, PredName, Context, !ModuleInfo, !IO) :-
-    solutions(constrained_tvar_not_in_arg_types(ClassContext, ArgTypes),
-        UnboundTVars),
-    (
-        UnboundTVars = []
-    ;
-        UnboundTVars = [_ | _],
-        module_info_incr_errors(!ModuleInfo),
-        report_unbound_tvars_in_class_context(UnboundTVars, ArgTypes,
-            TVarSet, PredOrFunc, PredName, Context, !IO)
-    ).
-
-:- pred constrained_tvar_not_in_arg_types(prog_constraints::in, list(type)::in,
-    tvar::out) is nondet.
-
-constrained_tvar_not_in_arg_types(ClassContext, ArgTypes, TVar) :-
-    ClassContext = constraints(UnivCs, ExistCs),
-    ( Constraints = UnivCs ; Constraints = ExistCs ),
-    prog_type__constraint_list_get_tvars(Constraints, TVars),
-    list__member(TVar, TVars),
-    \+ term__contains_var_list(ArgTypes, TVar).
-
-:- pred report_unbound_tvars_in_class_context(list(tvar)::in, list(type)::in,
-    tvarset::in, pred_or_func::in, sym_name::in, prog_context::in,
-    io::di, io::uo) is det.
-
-% The error message is intended to look like this:
-%
-% very_long_module_name:001: In declaration for function `long_function/2':
-% very_long_module_name:001:   error in type class constraints: type variables
-% very_long_module_name:001:   `T1, T2, T3' occur only in the constraints,
-% very_long_module_name:001:   not in the function's argument or result types.
-%
-% very_long_module_name:002: In declaration for predicate `long_predicate/3':
-% very_long_module_name:002:   error in type class constraints: type variable
-% very_long_module_name:002:   `T' occurs only in the constraints,
-% very_long_module_name:002:   not in the predicate's argument types.
-
-report_unbound_tvars_in_class_context(UnboundTVars, ArgTypes, TVarSet,
-        PredOrFunc, PredName, Context, !IO) :-
-    list__length(ArgTypes, Arity),
-    Part1 = [words("In declaration for"),
-        words(simple_call_id_to_string(PredOrFunc, PredName, Arity)),
-        suffix(":"), nl,
-        words("error in type class constraints:")],
-    (
-        UnboundTVars = [],
-        error("report_unbound_tvars_in_class_context: no type vars")
-    ;
-        UnboundTVars = [TVar],
-        Part2 = [words("type variable"),
-            words("`" ++ mercury_var_to_string(TVar, TVarSet, no) ++ "'"),
-            words("occurs")]
-    ;
-        UnboundTVars = [_, _ | _],
-        Part2 = [words("type variable"),
-            words("`" ++ mercury_vars_to_string(UnboundTVars, TVarSet, no)
-                ++ "'"),
-            words("occur")]
-    ),
-    Part3 = [words("only in the constraints, not in the")],
-    (
-        PredOrFunc = predicate,
-        Part4 = [words("predicate's argument types.")]
-    ;
-        PredOrFunc = function,
-        Part4 = [words("function's argument or result types.")]
-    ),
-    write_error_pieces(Context, 0, Part1 ++ Part2 ++ Part3 ++ Part4, !IO),
-    io__set_exit_status(1, !IO).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.257
diff -u -r1.257 mercury_to_mercury.m
--- compiler/mercury_to_mercury.m	14 Apr 2005 06:50:59 -0000	1.257
+++ compiler/mercury_to_mercury.m	19 Apr 2005 16:20:44 -0000
@@ -370,6 +370,7 @@
 :- import_module libs__globals.
 :- import_module libs__options.
 :- import_module libs__rat.
+:- import_module parse_tree__error_util.
 :- import_module parse_tree__prog_io_util.
 :- import_module parse_tree__prog_out.
 :- import_module parse_tree__prog_util.
@@ -695,7 +696,8 @@
     io__write_string(".\n", !IO).
 mercury_output_item(_, nothing(_), _, !IO).
 mercury_output_item(UnqualifiedItemNames,
-        typeclass(Constraints, ClassName0, Vars, Interface, VarSet), _, !IO) :-
+        typeclass(Constraints, FunDeps, ClassName0, Vars, Interface, VarSet),
+        _, !IO) :-
     maybe_unqualify_sym_name(UnqualifiedItemNames, ClassName0, ClassName),
     io__write_string(":- typeclass ", !IO),
 
@@ -710,8 +712,8 @@
         ), !IO),
     io__write_char(')', !IO),
     AppendVarnums = no,
-    mercury_format_prog_constraint_list(Constraints, VarSet, "<=",
-        AppendVarnums, !IO),
+    mercury_format_fundeps_and_prog_constraint_list(FunDeps, Constraints,
+        VarSet, AppendVarnums, !IO),
     (
         Interface = abstract,
         io__write_string(".\n", !IO)
@@ -2115,9 +2117,40 @@
     ;
         add_string(")", !U)
     ),
-    mercury_format_prog_constraint_list(UnivCs, VarSet, "<=",
+    mercury_format_prog_constraint_list(UnivCs, VarSet, "<=", AppendVarnums,
+        !U).
+
+:- pred mercury_format_fundeps_and_prog_constraint_list(list(prog_fundep)::in,
+    list(prog_constraint)::in, tvarset::in, bool::in, U::di, U::uo) is det
+    <= output(U).
+
+mercury_format_fundeps_and_prog_constraint_list(FunDeps, Constraints, VarSet,
+        AppendVarnums, !U) :-
+    list.map(make_fundep_constraint, FunDeps, FunDepConstraints),
+    AllConstraints = FunDepConstraints ++ Constraints,
+    mercury_format_prog_constraint_list(AllConstraints, VarSet, "<=",
         AppendVarnums, !U).
 
+:- pred make_fundep_constraint(prog_fundep::in, prog_constraint::out) is det.
+
+make_fundep_constraint(fundep(Domain, Range), Constraint) :-
+    make_fundep_constraint_arg(Domain, DomainArg),
+    make_fundep_constraint_arg(Range, RangeArg),
+    Constraint = constraint(unqualified("->"), [DomainArg, RangeArg]).
+
+:- pred make_fundep_constraint_arg(list(tvar)::in, (type)::out) is det.
+
+make_fundep_constraint_arg(TVars, Arg) :-
+    var_list_to_term_list(TVars, TVarTerms),
+    (
+        TVarTerms = [],
+        unexpected(this_file, "make_fundep_constraint_arg: empty list")
+    ;
+        TVarTerms = [First | Rest],
+        term.context_init(Context),
+        list_to_conjunction(Context, First, Rest, Arg)
+    ).
+
 :- pred mercury_format_prog_constraint_list(list(prog_constraint)::in,
     tvarset::in, string::in, bool::in, U::di, U::uo) is det <= output(U).
 
@@ -2133,13 +2166,11 @@
         add_string(")", !U)
     ).
 
-mercury_output_constraint(VarSet, AppendVarnums, constraint(Name, Types),
-        !IO) :-
-    mercury_format_constraint(VarSet, AppendVarnums,
-        constraint(Name, Types), !IO).
+mercury_output_constraint(VarSet, AppendVarnums, Constraint, !IO) :-
+    mercury_format_constraint(VarSet, AppendVarnums, Constraint, !IO).
 
-mercury_constraint_to_string(VarSet, constraint(Name, Types)) = String :-
-    mercury_format_constraint(VarSet, no, constraint(Name, Types), "", String).
+mercury_constraint_to_string(VarSet, Constraint) = String :-
+    mercury_format_constraint(VarSet, no, Constraint, "", String).
 
 :- pred mercury_format_constraint(tvarset::in, bool::in, prog_constraint::in,
     U::di, U::uo) is det <= output(U).
@@ -4217,6 +4248,12 @@
 		TerminationStr = "cannot_loop"
 	),
 	io.write_string(TerminationStr, !IO).	
+
+%---------------------------------------------------------------------------%
+
+:- func this_file = string.
+
+this_file = "mercury_to_mercury.m".
 
 %-----------------------------------------------------------------------------%
 :- end_module mercury_to_mercury.
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.103
diff -u -r1.103 module_qual.m
--- compiler/module_qual.m	14 Apr 2005 06:50:59 -0000	1.103
+++ compiler/module_qual.m	15 Apr 2005 15:46:10 -0000
@@ -302,7 +302,7 @@
 			!Info)
 	).
 collect_mq_info_2(nothing(_), !Info).
-collect_mq_info_2(typeclass(_, SymName, Params, _, _), !Info) :-
+collect_mq_info_2(typeclass(_, _, SymName, Params, _, _), !Info) :-
 	% This item is not visible in the current module.
 	( mq_info_get_import_status(!.Info, abstract_imported) ->
 		true
@@ -660,10 +660,10 @@
 		promise(T, G, V, U) - Context, !Info, yes, !IO).
 module_qualify_item(nothing(A) - Context, nothing(A) - Context,
 		!Info, yes, !IO).
-module_qualify_item(typeclass(Constraints0, Name, Vars, Interface0, VarSet) -
-			Context,
-		typeclass(Constraints, Name, Vars, Interface, VarSet) -
-			Context,
+module_qualify_item(typeclass(Constraints0, FunDeps, Name, Vars, Interface0,
+			VarSet) - Context,
+		typeclass(Constraints, FunDeps, Name, Vars, Interface, VarSet)
+			- Context,
 		!Info, yes, !IO) :-
 	list.length(Vars, Arity),
 	mq_info_set_error_context(class(Name - Arity) - Context, !Info),
--------------------------------------------------------------------------
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