diff: typeclasses (final) [5/6]

David Glen JEFFERY dgj at cs.mu.oz.au
Fri Dec 19 14:02:08 AEDT 1997


 
 polymorphism__set_module_info(ModuleInfo, PolyInfo0, PolyInfo) :-
-	PolyInfo0 = poly_info(A, B, C, D, E, _),
-	PolyInfo = poly_info(A, B, C, D, E, ModuleInfo).
+	PolyInfo0 = poly_info(A, B, C, D, E, F, G, _),
+	PolyInfo = poly_info(A, B, C, D, E, F, G, ModuleInfo).
 
 %---------------------------------------------------------------------------%
 %---------------------------------------------------------------------------%
Index: compiler/prog_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_data.m,v
retrieving revision 1.27
diff -u -r1.27 prog_data.m
--- prog_data.m	1997/12/09 04:01:17	1.27
+++ prog_data.m	1997/12/15 06:21:23
@@ -18,8 +18,8 @@
 
 :- interface.
 
-:- import_module hlds_data, hlds_pred, (inst), purity.
-:- import_module term_util, list, map, varset, term, std_util.
+:- import_module hlds_data, hlds_pred, (inst), purity, term_util.
+:- import_module list, map, varset, term, std_util.
 
 %-----------------------------------------------------------------------------%
 
@@ -52,11 +52,13 @@
 	; 	module_defn(varset, module_defn)
 
 	; 	pred(varset, sym_name, list(type_and_mode),
-			maybe(determinism), condition, purity)
+			maybe(determinism), condition, purity,
+			list(class_constraint))
 		%     VarNames, PredName, ArgTypes, Deterministicness, Cond
 
 	; 	func(varset, sym_name, list(type_and_mode), type_and_mode,
-			maybe(determinism), condition, purity)
+			maybe(determinism), condition, purity,
+			list(class_constraint))
 		%       VarNames, PredName, ArgTypes, ReturnType,
 		%       Deterministicness, Cond
 
@@ -72,6 +74,16 @@
 
 	;	pragma(pragma_type)
 
+	;	typeclass(list(class_constraint), class_name, list(var),
+			class_interface, varset)
+		%	Constraints, ClassName, ClassParams, 
+		%	ClassMethods, VarNames
+
+	;	instance(list(class_constraint), class_name, list(type),
+			instance_interface, varset)
+		%	DerivingClass, ClassName, Types, 
+		%	MethodInstances, VarNames
+
 	;	nothing.
 		% used for items that should be ignored (currently only
 		% NU-Prolog `when' declarations, which are silently ignored
@@ -154,6 +166,51 @@
 
 	;	check_termination(sym_name, arity).
 			% Predname, Arity
+
+:- type class_constraint	---> constraint(class_name, list(type)).
+
+:- type class_name == sym_name.
+
+:- type class_interface  == list(class_method).	
+
+:- type class_method	--->	pred(varset, sym_name, list(type_and_mode),
+					maybe(determinism), condition,
+					list(class_constraint), term__context)
+				%       VarNames, PredName, ArgTypes,
+				%	Determinism, Cond
+				%	ClassContext, Context
+
+			; 	func(varset, sym_name, list(type_and_mode),
+					type_and_mode,
+					maybe(determinism), condition,
+					list(class_constraint), term__context)
+				%       VarNames, PredName, ArgTypes,
+				%	ReturnType,
+				%	Determinism, Cond
+				%	ClassContext, Context
+
+			; 	pred_mode(varset, sym_name, list(mode),
+					maybe(determinism), condition,
+					term__context)
+				%       VarNames, PredName, ArgModes,
+				%	Determinism, Cond
+				%	Context
+
+			; 	func_mode(varset, sym_name, list(mode), mode,
+					maybe(determinism), condition,
+					term__context)
+				%       VarNames, PredName, ArgModes,
+				%	ReturnValueMode,
+				%	Determinism, Cond
+				%	Context
+			.
+
+:- type instance_method	--->	func_instance(sym_name, sym_name, arity)
+			;	pred_instance(sym_name, sym_name, arity)
+				% Method, Instance, Arity
+			.
+
+:- type instance_interface ==	list(instance_method).
 
 	% For pragma c_code, there are two different calling conventions,
 	% one for C code that may recursively call Mercury code, and another
Index: compiler/prog_io.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_io.m,v
retrieving revision 1.166
diff -u -r1.166 prog_io.m
--- prog_io.m	1997/12/09 04:01:20	1.166
+++ prog_io.m	1997/12/15 06:23:32
@@ -55,8 +55,8 @@
 
 :- interface.
 
-:- import_module prog_data.
-:- import_module list, io.
+:- import_module prog_data, prog_io_util.
+:- import_module list, io. 
 
 %-----------------------------------------------------------------------------%
 
@@ -93,12 +93,22 @@
 :- pred search_for_file(list(string), string, bool, io__state, io__state).
 :- mode search_for_file(in, in, out, di, uo) is det.
 
+	% parse_item(ModuleName, VarSet, Term, MaybeItem)
+	%
+	% parse Term. If successful, MaybeItem is bound to the parsed item,
+	% otherwise it is bound to an appropriate error message.
+	% Qualify appropriate parts of the item, with ModuleName as the
+	% module name.
+:- pred parse_item(string, varset, term, maybe_item_and_context). 
+:- mode parse_item(in, in, in, out) is det.
+
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
 :- implementation.
 
 :- import_module prog_io_goal, prog_io_dcg, prog_io_pragma, prog_io_util.
+:- import_module prog_io_typeclass.
 :- import_module hlds_data, hlds_pred, prog_util, globals, options, (inst).
 :- import_module purity.
 :- import_module bool, int, string, std_util, parser, term_io, dir, require.
@@ -415,9 +425,6 @@
 convert_item(ok(Item, Context), ok(Item, Context)).
 convert_item(error(M, T), error(M, T)).
 
-:- pred parse_item(string, varset, term, maybe_item_and_context). 
-:- mode parse_item(in, in, in, out) is det.
-
 parse_item(ModuleName, VarSet, Term, Result) :-
  	( %%% some [Decl, DeclContext]
 		Term = term__functor(term__atom(":-"), [Decl], DeclContext)
@@ -522,6 +529,29 @@
 process_decl(ModuleName, VarSet, "func", [FuncDecl], Result) :-
 	parse_type_decl_func(ModuleName, VarSet, FuncDecl, pure, Result).
 
+	% Because "<=" has a higher precedence than "pred" or "func", we
+	% we need to handle preds and funcs with class contexts specially.
+process_decl(ModuleName, VarSet, "<=", [Decl, ClassContext], Result) :-
+	(
+		Decl = term__functor(term__atom("pred"), [PredDecl], Context)
+	->
+		NewTerm = term__functor(term__atom("<="), 
+			[PredDecl, ClassContext], Context),
+		parse_type_decl_pred(ModuleName, VarSet, NewTerm, pure,
+			Result)
+	;
+		Decl = term__functor(term__atom("func"), [FuncDecl], Context)
+	->
+		NewTerm = term__functor(term__atom("<="), 
+			[FuncDecl, ClassContext], Context),
+		parse_type_decl_func(ModuleName, VarSet, NewTerm, pure,
+			Result)
+	;
+		Result = error(
+		"Class contexts only allowed on pred or func declarations", 
+		    Decl)
+	).
+
 process_decl(ModuleName, VarSet, "mode", [ModeDecl], Result) :-
 	parse_mode_decl(ModuleName, VarSet, ModeDecl, Result).
 
@@ -663,6 +693,12 @@
 process_decl(ModuleName, VarSet, "pragma", Pragma, Result):-
 	parse_pragma(ModuleName, VarSet, Pragma, Result).
 
+process_decl(ModuleName, VarSet, "typeclass", Args, Result):-
+	parse_typeclass(ModuleName, VarSet, Args, Result).
+
+process_decl(ModuleName, VarSet, "instance", Args, Result):-
+	parse_instance(ModuleName, VarSet, Args, Result).
+
 	%  XXX I'm not very happy with this.  I believe this should
 	%  recursively call process_decl in order to process the pred or func
 	%  declaration.  The information that the pred/func decl is preceeded
@@ -1115,15 +1151,35 @@
 			purity, maybe1(item)).
 :- mode process_pred(in, in, in, in, in, in, out) is det.
 
-process_pred(ModuleName, VarSet, PredType, Cond, MaybeDet, Purity, Result) :-
-	parse_qualified_term(ModuleName, PredType, PredType,
-		"`:- pred' declaration", R),
-	process_pred_2(R, PredType, VarSet, MaybeDet, Cond, Purity, Result).
+process_pred(ModuleName, VarSet, PredType0, Cond, MaybeDet, Purity, Result) :-
+	(
+		maybe_get_class_context(ModuleName, PredType0, PredType,
+			MaybeContext)
+	->
+		(
+			MaybeContext = ok(Constraints),
+			parse_qualified_term(ModuleName, PredType, PredType,
+				"`:- pred' declaration", R),
+			process_pred_2(R, PredType, VarSet, MaybeDet, Cond,
+				Purity, Constraints, Result)
+		;
+			MaybeContext = error(String, Term),
+			Result = error(String, Term)
+		)
+	;
+		parse_qualified_term(ModuleName, PredType0, PredType0,
+			"`:- pred' declaration", R),
+		process_pred_2(R, PredType0, VarSet, MaybeDet, Cond, Purity, 
+			[], Result)
+	).
 
 :- pred process_pred_2(maybe_functor, term, varset, maybe(determinism),
-			condition, purity, maybe1(item)).
-:- mode process_pred_2(in, in, in, in, in, in, out) is det.
-process_pred_2(ok(F, As0), PredType, VarSet, MaybeDet, Cond, Purity, Result) :-
+			condition, purity, list(class_constraint), 
+			maybe1(item)).
+:- mode process_pred_2(in, in, in, in, in, in, in, out) is det.
+
+process_pred_2(ok(F, As0), PredType, VarSet, MaybeDet, Cond, Purity,
+		ClassContext, Result) :-
 	(
 		convert_type_and_mode_list(As0, As)
 	->
@@ -1131,7 +1187,7 @@
 			verify_type_and_mode_list(As)
 		->
 			Result = ok(pred(VarSet, F, As, MaybeDet, Cond,
-					 Purity))
+				Purity, ClassContext))
 		;
 			Result = error("some but not all arguments have modes", PredType)
 		)
@@ -1139,7 +1195,24 @@
 		Result = error("syntax error in `:- pred' declaration",
 				PredType)
 	).
-process_pred_2(error(M, T), _, _, _, _, _, error(M, T)).
+process_pred_2(error(M, T), _, _, _, _, _, _, error(M, T)).
+
+%-----------------------------------------------------------------------------%
+	% We could probably get rid of some code duplication between here and
+	% prog_io_typeclass.m
+	% The last argument is `no' if no context was given, and yes(Result) if
+	% there was. Result is either bound to the correctly parsed context, or
+	% an appropriate error message (if a syntactically invalid class 
+	% context was given).
+
+:- pred maybe_get_class_context(string, term, term,
+	maybe1(list(class_constraint))).
+:- mode maybe_get_class_context(in, in, out, out) is semidet.
+
+maybe_get_class_context(ModuleName, PredType0, PredType, MaybeContext) :-
+	PredType0 = term__functor(term__atom("<="), 
+		[PredType, Constraints], _),
+	parse_class_constraints(ModuleName, Constraints, MaybeContext).
 
 %-----------------------------------------------------------------------------%
 
@@ -1175,7 +1248,30 @@
 			maybe(determinism), maybe1(item)).
 :- mode process_func(in, in, in, in, in, in, out) is det.
 
-process_func(ModuleName, VarSet, Term, Cond, Purity, MaybeDet, Result) :-
+process_func(ModuleName, VarSet, Term0, Cond, Purity, MaybeDet, Result) :-
+	(
+		maybe_get_class_context(ModuleName, Term0, Term,
+			MaybeContext)
+	->
+		(
+			MaybeContext = ok(Constraints),
+			process_unconstrained_func(ModuleName, VarSet, Term,
+				Cond, MaybeDet, Purity, Constraints, Result) 
+		;
+			MaybeContext = error(String, ErrorTerm),
+			Result = error(String, ErrorTerm)
+		)
+	;
+		process_unconstrained_func(ModuleName, VarSet, Term0, 
+			Cond, MaybeDet, Purity, [], Result) 
+	).
+
+:- pred process_unconstrained_func(string, varset, term, condition,
+	maybe(determinism), purity, list(class_constraint), maybe1(item)).
+:- mode process_unconstrained_func(in, in, in, in, in, in, in, out) is det.
+
+process_unconstrained_func(ModuleName, VarSet, Term, Cond, MaybeDet, 
+		Purity, Constraints, Result) :-
 	(
 		Term = term__functor(term__atom("="),
 				[FuncTerm, ReturnTypeTerm], _Context)
@@ -1183,16 +1279,19 @@
 		parse_qualified_term(ModuleName, FuncTerm, Term,
 			"`:- func' declaration", R),
 		process_func_2(R, FuncTerm, ReturnTypeTerm, VarSet, MaybeDet,
-				Cond, Purity, Result)
+				Cond, Purity, Constraints, Result)
 	;
 		Result = error("`=' expected in `:- func' declaration", Term)
 	).
 
+
 :- pred process_func_2(maybe_functor, term, term, varset, maybe(determinism),
-			condition, purity, maybe1(item)).
-:- mode process_func_2(in, in, in, in, in, in, in, out) is det.
+			condition, purity, list(class_constraint),
+			maybe1(item)).
+:- mode process_func_2(in, in, in, in, in, in, in, in, out) is det.
+
 process_func_2(ok(F, As0), FuncTerm, ReturnTypeTerm, VarSet, MaybeDet, Cond,
-		Purity, Result) :-
+		Purity, ClassContext, Result) :-
 	( convert_type_and_mode_list(As0, As) ->
 		( \+ verify_type_and_mode_list(As) ->
 			Result = error("some but not all arguments have modes",
@@ -1221,7 +1320,7 @@
 					FuncTerm)
 			;
 				Result = ok(func(VarSet, F, As, ReturnType,
-					MaybeDet, Cond, Purity))
+					MaybeDet, Cond, Purity, ClassContext))
 			)
 		;
 			Result = error(
@@ -1233,7 +1332,7 @@
 			"syntax error in arguments of `:- func' declaration",
 					FuncTerm)
 	).
-process_func_2(error(M, T), _, _, _, _, _, _, error(M, T)).
+process_func_2(error(M, T), _, _, _, _, _, _, _, error(M, T)).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/prog_out.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_out.m,v
retrieving revision 1.33
diff -u -r1.33 prog_out.m
--- prog_out.m	1997/07/27 15:16:38	1.33
+++ prog_out.m	1997/12/18 00:31:02
@@ -26,6 +26,13 @@
 :- pred prog_out__write_context(term__context, io__state, io__state).
 :- mode prog_out__write_context(in, di, uo) is det.
 
+	% XXX This pred should be deleted, and all uses replaced with
+	% XXX error_util:write_error_pieces, once zs has committed that
+	% XXX error_util.m.
+:- pred prog_out__write_strings_with_context(term__context, list(string),
+	io__state, io__state).
+:- mode prog_out__write_strings_with_context(in, in, di, uo) is det.
+
 :- pred prog_out__write_sym_name(sym_name, io__state, io__state).
 :- mode prog_out__write_sym_name(in, di, uo) is det.
 
@@ -39,7 +46,7 @@
 %-----------------------------------------------------------------------------%
 
 :- implementation.
-:- import_module require, string, list, varset, std_util, term_io.
+:- import_module require, string, list, varset, std_util, term_io, int.
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -81,15 +88,62 @@
 	% error message.
 
 prog_out__write_context(Context) -->
+	prog_out__write_context_2(Context, _).
+
+:- pred prog_out__write_context_2(term__context, int, io__state, io__state).
+:- mode prog_out__write_context_2(in, out, di, uo) is det.
+
+prog_out__write_context_2(Context, Length) -->
 	{ term__context_file(Context, FileName) },
 	{ term__context_line(Context, LineNumber) },
 	( { FileName = "" } ->
-		[]
+		{ Length = 0 }
 	;
 		{ string__format("%s:%03d: ", [s(FileName), i(LineNumber)],
 			ContextMessage) }, 
-		io__write_string(ContextMessage)
+		io__write_string(ContextMessage),
+		{ string__length(ContextMessage, Length) }
 	).
+
+%-----------------------------------------------------------------------------%
+
+prog_out__write_strings_with_context(Context, Strings) -->
+	prog_out__write_strings_with_context_2(Context, Strings, 0).
+
+:- pred prog_out__write_strings_with_context_2(term__context, list(string), int,
+	io__state, io__state).
+:- mode prog_out__write_strings_with_context_2(in, in, in, di, uo) is det.
+
+prog_out__write_strings_with_context_2(_Context, [], _) --> [].
+prog_out__write_strings_with_context_2(Context, [S|Ss], N0) -->
+	{ string__length(S, MessageLength) },
+	(
+		{ N0 = 0 }
+	->
+		prog_out__write_context_2(Context, ContextLength),
+		io__write_string("  "),
+		io__write_string(S),
+		{ N is ContextLength + MessageLength },
+		{ Rest = Ss }
+	;
+		{ N1 is MessageLength + N0 },
+		{ num_columns(NumColumns) },
+		{ N1 < NumColumns }
+	->
+		io__write_string(S),
+		{ N = N1 },
+		{ Rest = Ss }
+	;
+		io__write_char('\n'),
+		{ N = 0 },
+		{ Rest = [S|Ss] }
+	),
+	prog_out__write_strings_with_context_2(Context, Rest, N).
+
+
+:- pred num_columns(int::out) is det.
+
+num_columns(80).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/purity.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/purity.m,v
retrieving revision 1.2
diff -u -r1.2 purity.m
--- purity.m	1997/12/11 10:31:08	1.2
+++ purity.m	1997/12/18 07:37:45
@@ -366,6 +366,11 @@
 	{ HOCall = higher_order_call(_,_,_,_,_,_) },
 	error_if_body_purity_indicated(GoalInfo, NumErrors0, NumErrors,
 				       InClosure, "higher order goal").
+compute_expr_purity(CMCall, CMCall, GoalInfo, _, _, InClosure, pure,
+		NumErrors0, NumErrors) -->
+	{ CMCall = class_method_call(_,_,_,_,_,_) },
+	error_if_body_purity_indicated(GoalInfo, NumErrors0, NumErrors,
+				       InClosure, "class method goal").
 compute_expr_purity(switch(Var,Canfail,Cases0,Storemap),
 		switch(Var,Canfail,Cases,Storemap), GoalInfo, PredInfo,
 		ModuleInfo, InClosure, Purity, NumErrors0, NumErrors) -->
Index: compiler/quantification.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/quantification.m,v
retrieving revision 1.53
diff -u -r1.53 quantification.m
--- quantification.m	1997/09/01 14:04:33	1.53
+++ quantification.m	1997/09/08 05:19:36
@@ -297,6 +297,10 @@
 		higher_order_call(PredVar, ArgVars, C, D, E, F)) -->
 	implicitly_quantify_atomic_goal([PredVar|ArgVars]).
 
+implicitly_quantify_goal_2(class_method_call(TCVar, B, ArgVars, D, E, F), _,
+		class_method_call(TCVar, B, ArgVars, D, E, F)) -->
+	implicitly_quantify_atomic_goal([TCVar|ArgVars]).
+
 implicitly_quantify_goal_2(
 		unify(Var, UnifyRHS0, Mode, Unification0, UnifyContext),
 		Context,
@@ -589,6 +593,10 @@
 quantification__goal_vars_2(higher_order_call(PredVar, ArgVars, _, _, _, _),
 		Set0, LambdaSet, Set, LambdaSet) :-
 	set__insert_list(Set0, [PredVar | ArgVars], Set).
+
+quantification__goal_vars_2(class_method_call(TCVar, _, ArgVars, _, _, _),
+		Set0, LambdaSet, Set, LambdaSet) :-
+	set__insert_list(Set0, [TCVar | ArgVars], Set).
 
 quantification__goal_vars_2(call(_, _, ArgVars, _, _, _), Set0, LambdaSet,
 		Set, LambdaSet) :-
Index: compiler/saved_vars.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/saved_vars.m,v
retrieving revision 1.11
diff -u -r1.11 saved_vars.m
--- saved_vars.m	1997/09/01 14:04:35	1.11
+++ saved_vars.m	1997/10/21 05:03:55
@@ -110,6 +110,10 @@
 		Goal = GoalExpr0 - GoalInfo0,
 		SlotInfo = SlotInfo0
 	;
+		GoalExpr0 = class_method_call(_, _, _, _, _, _),
+		Goal = GoalExpr0 - GoalInfo0,
+		SlotInfo = SlotInfo0
+	;
 		GoalExpr0 = call(_, _, _, _, _, _),
 		Goal = GoalExpr0 - GoalInfo0,
 		SlotInfo = SlotInfo0
@@ -266,6 +270,15 @@
 			Goals = [NewConstruct, Goal1 | Goals1]
 		;
 			Goal0Expr = higher_order_call(_, _, _, _, _, _),
+			rename_var(SlotInfo0, Var, _NewVar, Subst, SlotInfo1),
+			goal_util__rename_vars_in_goal(Construct, Subst,
+				NewConstruct),
+			goal_util__rename_vars_in_goal(Goal0, Subst, Goal1),
+			saved_vars_delay_goal(Goals0, Construct, Var,
+				IsNonLocal, SlotInfo1, Goals1, SlotInfo),
+			Goals = [NewConstruct, Goal1 | Goals1]
+		;
+			Goal0Expr = class_method_call(_, _, _, _, _, _),
 			rename_var(SlotInfo0, Var, _NewVar, Subst, SlotInfo1),
 			goal_util__rename_vars_in_goal(Construct, Subst,
 				NewConstruct),
Index: compiler/simplify.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/simplify.m,v
retrieving revision 1.48
diff -u -r1.48 simplify.m
--- simplify.m	1997/12/09 04:01:35	1.48
+++ simplify.m	1997/12/10 07:20:54
@@ -424,6 +424,11 @@
 		Info = Info0
 	).
 
+	% XXX We ought to do duplicate call elimination for class 
+	% XXX method calls here.
+simplify__goal_2(Goal, GoalInfo, Goal, GoalInfo, Info, Info) :-
+	Goal = class_method_call(_, _, _, _, _, _).
+
 simplify__goal_2(Goal0, GoalInfo0, Goal, GoalInfo, Info0, Info) :-
 	Goal0 = call(PredId, ProcId, Args, IsBuiltin, _, _),
 
Index: compiler/store_alloc.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/store_alloc.m,v
retrieving revision 1.55
diff -u -r1.55 store_alloc.m
--- store_alloc.m	1997/09/01 14:04:44	1.55
+++ store_alloc.m	1997/09/08 05:53:33
@@ -168,6 +168,9 @@
 store_alloc_in_goal_2(higher_order_call(A, B, C, D, E, F), Liveness, _, _,
 		higher_order_call(A, B, C, D, E, F), Liveness).
 
+store_alloc_in_goal_2(class_method_call(A, B, C, D, E, F), Liveness, _, _,
+		class_method_call(A, B, C, D, E, F), Liveness).
+
 store_alloc_in_goal_2(call(A, B, C, D, E, F), Liveness, _, _,
 		call(A, B, C, D, E, F), Liveness).
 
Index: compiler/stratify.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/stratify.m,v
retrieving revision 1.11
diff -u -r1.11 stratify.m
--- stratify.m	1997/11/24 07:27:02	1.11
+++ stratify.m	1997/12/10 07:22:00
@@ -235,6 +235,15 @@
 		"higher order call may introduce a non-stratified loop",
 		Error, Module0, Module).
 
+	% XXX This is very conservative.
+first_order_check_goal(class_method_call(_Var, _Num, _Vars, _Types, _Modes, 
+	_Det), GInfo, _Negated, _WholeScc, ThisPredProcId, Error,  
+	Module0, Module) --> 
+	{ goal_info_get_context(GInfo, Context) },
+	emit_message(ThisPredProcId, Context,
+		"class method call may introduce a non-stratified loop",
+		Error, Module0, Module).
+
 :- pred first_order_check_goal_list(list(hlds_goal), bool, 
 	list(pred_proc_id), pred_proc_id, bool, module_info, 
 	module_info, io__state, io__state).
@@ -400,7 +409,22 @@
 	->
 		{ goal_info_get_context(GoalInfo, Context) },
 		emit_message(ThisPredProcId, Context, 
-			"higher order call may introduce a non-stratified loop", 
+			"higher order call may introduce a non-stratified loop",
+			Error, Module0, Module)		
+	;
+		{ Module = Module0 }
+	).
+
+higher_order_check_goal(class_method_call(_Var, _Num, _Vars, _Types, _Modes,
+		_Det), GoalInfo, Negated, _WholeScc, ThisPredProcId,
+		HighOrderLoops, Error, Module0, Module) -->
+	(
+		{ Negated = yes },
+		{ HighOrderLoops = yes }
+	->
+		{ goal_info_get_context(GoalInfo, Context) },
+		emit_message(ThisPredProcId, Context, 
+			"class method call may introduce a non-stratified loop",
 			Error, Module0, Module)		
 	;
 		{ Module = Module0 }
@@ -827,6 +851,11 @@
 check_goal1(higher_order_call(_Var, _Vars, _Types, _Modes, _Det, _PredOrFUnc),
 		Calls, Calls, HasAT, HasAT, _, yes).
 
+	% record that the higher order call was made. Well... a class method
+	% call is pretty similar to a higher order call...
+check_goal1(class_method_call(_Var, _Num, _Vars, _Types, _Modes, _Det), Calls,
+		Calls, HasAT, HasAT, _, yes).
+
 check_goal1(conj(Goals), Calls0, Calls, HasAT0, HasAT, CallsHO0, CallsHO) :-
 	check_goal_list(Goals, Calls0, Calls, HasAT0, HasAT, CallsHO0, CallsHO).
 check_goal1(disj(Goals, _Follow), Calls0, Calls, HasAT0, HasAT, CallsHO0, 
@@ -922,6 +951,9 @@
 
 get_called_procs(higher_order_call(_Var, _Vars, _Types, _Modes, _Det,
 		_PredOrFunc), Calls, Calls).
+
+get_called_procs(class_method_call(_Var, _Num,_Vars, _Types, _Modes, _Det),
+	Calls, Calls).
 
 
 get_called_procs(conj(Goals), Calls0, Calls) :-
Index: compiler/switch_detection.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/switch_detection.m,v
retrieving revision 1.76
diff -u -r1.76 switch_detection.m
--- switch_detection.m	1997/09/01 14:04:54	1.76
+++ switch_detection.m	1997/09/08 06:12:35
@@ -166,6 +166,9 @@
 detect_switches_in_goal_2(higher_order_call(A,B,C,D,E,F), _, _, _, _,
 		higher_order_call(A,B,C,D,E,F)).
 
+detect_switches_in_goal_2(class_method_call(A,B,C,D,E,F), _, _, _, _,
+		class_method_call(A,B,C,D,E,F)).
+
 detect_switches_in_goal_2(call(A,B,C,D,E,F), _, _, _, _,
 		call(A,B,C,D,E,F)).
 
Index: compiler/switch_gen.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/switch_gen.m,v
retrieving revision 1.61
diff -u -r1.61 switch_gen.m
--- switch_gen.m	1997/10/14 09:27:56	1.61
+++ switch_gen.m	1997/10/20 07:16:43
@@ -208,6 +208,7 @@
 switch_gen__priority(pred_closure_tag(_, _), 6).	% should never occur
 switch_gen__priority(code_addr_constant(_, _), 6).	% should never occur
 switch_gen__priority(base_type_info_constant(_, _, _), 6).% should never occur
+switch_gen__priority(base_typeclass_info_constant(_, _, _), 6).% shouldn't occur
 
 %---------------------------------------------------------------------------%
 %---------------------------------------------------------------------------%
Index: compiler/term_pass1.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/term_pass1.m,v
retrieving revision 1.3
diff -u -r1.3 term_pass1.m
--- term_pass1.m	1997/10/20 04:12:41	1.3
+++ term_pass1.m	1997/12/15 06:32:47
@@ -486,6 +486,13 @@
 		GoalInfo, _Module, _, _PPId, Error, Offs, Offs) :-
 	goal_info_get_context(GoalInfo, Context),
 	Error = error(Context - horder_call).
+	
+proc_inequalities_goal(class_method_call(_, _, _, _, _, _), 
+		GoalInfo, _Module, _, _PPId, Error, Offs, Offs) :-
+	goal_info_get_context(GoalInfo, Context),
+		% It would be better to use a new alternative
+		% `class_method_call' rather than than `horder_call' here.
+	Error = error(Context - horder_call).
 
 proc_inequalities_goal(switch(_SwitchVar, _CanFail, Cases, _StoreMap), GoalInfo,
 		Module, Info, PPId, Res, Offs0, Offs) :-
Index: compiler/term_pass2.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/term_pass2.m,v
retrieving revision 1.2
diff -u -r1.2 term_pass2.m
--- term_pass2.m	1997/10/09 09:39:18	1.2
+++ term_pass2.m	1997/10/17 05:33:30
@@ -607,6 +607,17 @@
 	Res = error(Context - horder_call),
 	Out = Out0.
 
+	% For now, we'll pretend that the class method call is a higher order
+	% call. In reality, we could probably analyse further than this, since
+	% we know that the method being called must come from one of the
+	% instance declarations, and we could potentially (globally) analyse
+	% these.
+termination_goal(class_method_call(_, _, _, _, _, _), 
+		GoalInfo, _Module, _UnifyInfo, _CallInfo, Res, Out0, Out) :-
+	goal_info_get_context(GoalInfo, Context),
+	Res = error(Context - horder_call),
+	Out = Out0.
+
 termination_goal(switch(_Var, _CanFail, Cases, _StoreMap),
 		_GoalInfo, Module, UnifyInfo, CallInfo, Res, Out0, Out) :-
 	termination_switch(Cases, Module, UnifyInfo, CallInfo, 
Index: compiler/type_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/type_util.m,v
retrieving revision 1.47
diff -u -r1.47 type_util.m
--- type_util.m	1997/10/14 09:27:58	1.47
+++ type_util.m	1997/12/15 06:42:57
@@ -135,6 +135,11 @@
 :- pred type_list_subsumes(list(type), list(type), tsubst).
 :- mode type_list_subsumes(in, in, out) is semidet.
 
+	% type_list_matches_exactly(TypesA, TypesB) succeeds iff TypesA and
+	% TypesB are exactly the same modulo variable renaming. 
+:- pred type_list_matches_exactly(list(type), list(type)).
+:- mode type_list_matches_exactly(in, in) is semidet.
+
 	% apply a type substitution (i.e. map from tvar -> type)
 	% to all the types in a variable typing (i.e. map from var -> type).
 
@@ -149,16 +154,32 @@
 						 map(var, type)).
 :- mode apply_rec_substitution_to_type_map(in, in, out) is det.
 
-	% Update a map from tvar to var, using the type substititon to
-	% rename tvars and a variable substition to rename vars.
+	% Update a map from tvar to type_info_locn, using the type substititon
+	% to rename tvars and a variable substition to rename vars.
 	%
 	% If tvar maps to a another type variable, we keep the new
 	% variable, if it maps to a type, we remove it from the map.
 
-:- pred apply_substitutions_to_var_map(map(tvar, var), tsubst, map(var, var), 
-		map(tvar, var)).
+:- pred apply_substitutions_to_var_map(map(tvar, type_info_locn), tsubst,
+	map(var, var), map(tvar, type_info_locn)).
 :- mode apply_substitutions_to_var_map(in, in, in, out) is det.
 
+:- pred apply_rec_subst_to_constraints(substitution, list(class_constraint),
+	list(class_constraint)).
+:- mode apply_rec_subst_to_constraints(in, in, out) is det.
+
+:- pred apply_rec_subst_to_constraint(substitution, class_constraint,
+	class_constraint).
+:- mode apply_rec_subst_to_constraint(in, in, out) is det.
+
+:- pred apply_subst_to_constraints(substitution, list(class_constraint),
+	list(class_constraint)).
+:- mode apply_subst_to_constraints(in, in, out) is det.
+
+:- pred apply_subst_to_constraint(substitution, class_constraint,
+	class_constraint).
+:- mode apply_subst_to_constraint(in, in, out) is det.
+
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
@@ -357,7 +378,11 @@
 	Ctor \= qualified("mercury_builtin", "type_info"),
 	Ctor \= qualified("mercury_builtin", "base_type_info"),
 	Ctor \= unqualified("type_info"),
-	Ctor \= unqualified("base_type_info").
+	Ctor \= unqualified("base_type_info"),
+	Ctor \= qualified("mercury_builtin", "typeclass_info"),
+	Ctor \= qualified("mercury_builtin", "base_typeclass_info"),
+	Ctor \= unqualified("typeclass_info"),
+	Ctor \= unqualified("base_typeclass_info").
 
 %-----------------------------------------------------------------------------%
 
@@ -414,6 +439,14 @@
 
 %-----------------------------------------------------------------------------%
 
+	% If this becomes a performance bottleneck, it can probably be coded
+	% more efficiently.
+type_list_matches_exactly(TypesA, TypesB) :-
+	type_list_subsumes(TypesA, TypesB, _),
+	type_list_subsumes(TypesB, TypesA, _).
+
+%-----------------------------------------------------------------------------%
+
 	% Types are represented as terms, but we can't just use term__unify
 	% because we need to avoid binding any of the "head type params"
 	% (the type variables that occur in the head of the clause),
@@ -639,14 +672,16 @@
 	).
 
 
-:- pred apply_substitutions_to_var_map_2(list(var)::in, map(tvar, var)::in,
-		tsubst::in, map(var, var)::in, map(tvar, var)::in, 
-		map(tvar, var)::out) is det.
+:- pred apply_substitutions_to_var_map_2(list(var)::in, map(tvar,
+		type_info_locn)::in, tsubst::in, map(var, var)::in, 
+		map(tvar, type_info_locn)::in, 
+		map(tvar, type_info_locn)::out) is det.
 
 apply_substitutions_to_var_map_2([], _VarMap0, _, _, NewVarMap, NewVarMap).
 apply_substitutions_to_var_map_2([TVar | TVars], VarMap0, TSubst, Subst, 
 		NewVarMap0, NewVarMap) :-
-	map__lookup(VarMap0, TVar, Var),
+	map__lookup(VarMap0, TVar, Locn),
+	type_info_locn_var(Locn, Var),
 
 		% find the new tvar, if there is one, otherwise just
 		% create the old var as a type variable.
@@ -662,16 +697,36 @@
 	;
 		NewVar = Var
 	),
+	type_info_locn_set_var(Locn, NewVar, NewLocn),
 
 		% if the tvar is still a variable, insert it into the
 		% map with the new var.
 	( type_util__var(NewTerm, NewTVar) ->
-		map__det_insert(NewVarMap0, NewTVar, NewVar, NewVarMap1)
+		map__det_insert(NewVarMap0, NewTVar, NewLocn, NewVarMap1)
 	;
 		NewVarMap1 = NewVarMap0
 	),
 	apply_substitutions_to_var_map_2(TVars, VarMap0, TSubst, Subst, 
 		NewVarMap1, NewVarMap).
+
+%-----------------------------------------------------------------------------%
+
+apply_rec_subst_to_constraints(Subst, Constraints0, Constraints) :-
+	list__map(apply_rec_subst_to_constraint(Subst), Constraints0,
+		Constraints).
+
+apply_rec_subst_to_constraint(Subst, Constraint0, Constraint) :-
+	Constraint0 = constraint(ClassName, Types0),
+	term__apply_rec_substitution_to_list(Types0, Subst, Types),
+	Constraint  = constraint(ClassName, Types).
+
+apply_subst_to_constraints(Subst, Constraints0, Constraints) :-
+	list__map(apply_subst_to_constraint(Subst), Constraints0, Constraints).
+
+apply_subst_to_constraint(Subst, Constraint0, Constraint) :-
+	Constraint0 = constraint(ClassName, Types0),
+	term__apply_substitution_to_list(Types0, Subst, Types),
+	Constraint  = constraint(ClassName, Types).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
Index: compiler/typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/typecheck.m,v
retrieving revision 1.222
diff -u -r1.222 typecheck.m
--- typecheck.m	1997/12/09 04:01:42	1.222
+++ typecheck.m	1997/12/19 00:48:57
@@ -155,6 +155,17 @@
 			tvarset, list(type), pred_id, sym_name).
 :- mode typecheck__find_matching_pred_id(in, in, in, in, out, out) is semidet.
 
+	% Apply context reduction to the list of class constraints by applying
+	% the instance rules or superclass rules, building up proofs for
+	% redundant constraints
+:- pred typecheck__reduce_context_by_rule_application(instance_table,
+	class_table, tsubst, tvarset, tvarset, 
+	map(class_constraint, constraint_proof), 
+	map(class_constraint, constraint_proof),
+	list(class_constraint), list(class_constraint)).
+:- mode typecheck__reduce_context_by_rule_application(in, in, in, in, out, 
+	in, out, in, out) is semidet.
+
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
@@ -416,17 +427,35 @@
 	    pred_info_typevarset(PredInfo0, TypeVarSet0),
 	    pred_info_clauses_info(PredInfo0, ClausesInfo0),
 	    pred_info_import_status(PredInfo0, Status),
+	    pred_info_get_markers(PredInfo0, Markers),
 	    ClausesInfo0 = clauses_info(VarSet, ExplicitVarTypes,
 				_OldInferredVarTypes, HeadVars, Clauses0),
 	    ( 
 		Clauses0 = [] 
 	    ->
-	        report_error_no_clauses(PredId, PredInfo0, ModuleInfo,
-		    IOState0, IOState),
-	        MaybePredInfo = no,
-		Changed = no
+			% There are no clauses for class methods.
+			% The clauses are generated later on,
+			% in polymorphism__expand_class_method_bodies
+		( check_marker(Markers, class_method) ->
+			IOState = IOState0,
+				% For the moment, we just insert the types
+				% of the head vars into the clauses_info
+			pred_info_arg_types(PredInfo0, _, ArgTypes),
+			map__from_corresponding_lists(HeadVars, ArgTypes,
+				VarTypes),
+			ClausesInfo = clauses_info(VarSet, VarTypes,
+				VarTypes, HeadVars, Clauses0),
+			pred_info_set_clauses_info(PredInfo0, ClausesInfo,
+				PredInfo),
+			MaybePredInfo = yes(PredInfo),
+			Changed = no
+		;
+			report_error_no_clauses(PredId, PredInfo0, ModuleInfo,
+			    IOState0, IOState),
+			MaybePredInfo = no,
+			Changed = no
+		)
 	    ;
-		pred_info_get_markers(PredInfo0, Markers),
 		( check_marker(Markers, infer_type) ->
 			% For a predicate whose type is inferred,
 			% the predicate is allowed to bind the type
@@ -436,37 +465,43 @@
 			% `pred foo(T1, T2, ..., TN)' by make_hlds.m.
 			Inferring = yes,
 			HeadTypeParams = [],
+			Constraints = [],
 			write_pred_progress_message("% Inferring type of ",
 				PredId, ModuleInfo, IOState0, IOState1)
 		;
 			Inferring = no,
 			term__vars_list(ArgTypes0, HeadTypeParams),
+			pred_info_get_class_context(PredInfo0, Constraints),
 			write_pred_progress_message("% Type-checking ",
 				PredId, ModuleInfo, IOState0, IOState1)
 		),
-		bool(Inferring), % dummy pred call to avoid type ambiguity
 
 		typecheck_info_init(IOState1, ModuleInfo, PredId,
 				TypeVarSet0, VarSet, ExplicitVarTypes,
-				HeadTypeParams, Status, TypeCheckInfo1),
+				HeadTypeParams, Constraints, Status,
+				TypeCheckInfo1),
 		typecheck_clause_list(Clauses0, HeadVars, ArgTypes0, Clauses,
 				TypeCheckInfo1, TypeCheckInfo2),
+		typecheck_constraints(Inferring, TypeCheckInfo2,
+				TypeCheckInfo3),
 		typecheck_check_for_ambiguity(whole_pred, HeadVars,
-				TypeCheckInfo2, TypeCheckInfo3),
-		typecheck_info_get_final_info(TypeCheckInfo3, TypeVarSet, 
+				TypeCheckInfo3, TypeCheckInfo4),
+		typecheck_info_get_final_info(TypeCheckInfo4, TypeVarSet, 
 				InferredVarTypes0),
 		map__optimize(InferredVarTypes0, InferredVarTypes),
 		ClausesInfo = clauses_info(VarSet, ExplicitVarTypes,
 				InferredVarTypes, HeadVars, Clauses),
 		pred_info_set_clauses_info(PredInfo0, ClausesInfo, PredInfo1),
 		pred_info_set_typevarset(PredInfo1, TypeVarSet, PredInfo2),
+		record_class_constraint_proofs(PredInfo2, TypeCheckInfo4,
+			PredInfo3),
 		( Inferring = no ->
-			PredInfo = PredInfo2,
+			PredInfo = PredInfo3,
 			Changed = no
 		;
 			map__apply_to_list(HeadVars, InferredVarTypes,
 				ArgTypes),
-			pred_info_set_arg_types(PredInfo2, TypeVarSet,
+			pred_info_set_arg_types(PredInfo3, TypeVarSet,
 				ArgTypes, PredInfo),
 			( identical_up_to_renaming(ArgTypes0, ArgTypes) ->
 				Changed = no
@@ -474,7 +509,7 @@
 				Changed = yes
 			)
 		),
-		typecheck_info_get_found_error(TypeCheckInfo3, Error),
+		typecheck_info_get_found_error(TypeCheckInfo4, Error),
 		(
 			Error = yes,
 			MaybePredInfo = no
@@ -482,14 +517,10 @@
 			Error = no,
 			MaybePredInfo = yes(PredInfo)
 		),
-		typecheck_info_get_io_state(TypeCheckInfo3, IOState)
+		typecheck_info_get_io_state(TypeCheckInfo4, IOState)
 	    )
 	).
 
-	% bool/1 is used to avoid a type ambiguity
-:- pred bool(bool::in) is det.
-bool(_).
-
 :- pred pred_is_user_defined_equality_pred(pred_info::in, module_info::in)
 	is semidet.
 
@@ -861,6 +892,9 @@
 		higher_order_call(PredVar, Args, C, D, E, F)) -->
 	checkpoint("higher-order call"),
 	typecheck_higher_order_call(PredVar, Args).
+typecheck_goal_2(class_method_call(A, B, C, D, E, F),
+		class_method_call(A, B, C, D, E, F)) -->
+	{ error("class_method_calls should be introduced after typechecking") }.
 typecheck_goal_2(unify(A, B0, Mode, Info, UnifyContext),
 		unify(A, B, Mode, Info, UnifyContext)) -->
 	checkpoint("unify"),
@@ -907,7 +941,7 @@
 			TypeVars, TypeVarSet) },
 		{ term__var_list_to_term_list(TypeVars, Types) },
 		typecheck_var_has_polymorphic_type_list(Vars,
-			TypeVarSet, Types)
+			TypeVarSet, Types, [])
 	).
 
 %-----------------------------------------------------------------------------%
@@ -923,8 +957,11 @@
 	{ Arity1 is Arity + 1 },
 	{ PredCallId = unqualified("call")/Arity1 },
 	typecheck_info_set_called_predid(PredCallId),
+		% The class context is empty because higher-order predicates
+		% are always monomorphic.
+	{ ClassContext = [] },
 	typecheck_var_has_polymorphic_type_list([PredVar|Args], TypeVarSet,
-		[PredVarType|ArgTypes]).
+		[PredVarType|ArgTypes], ClassContext).
 
 :- pred higher_order_pred_type(int, tvarset, type, list(type)).
 :- mode higher_order_pred_type(in, out, out, out) is det.
@@ -992,9 +1029,11 @@
 			map__lookup(Preds, PredId, PredInfo),
 			pred_info_arg_types(PredInfo, PredTypeVarSet,
 						PredArgTypes),
+			pred_info_get_class_context(PredInfo,
+						PredClassContext),
 
 				% rename apart the type variables in 
-				% called predicate's arg types and then
+				% called predicate's arg types and then 
 				% unify the types of the call arguments
 				% with the called predicates' arg types
 				% (optimize for the common case of
@@ -1002,12 +1041,27 @@
 			( varset__is_empty(PredTypeVarSet) ->
 			    typecheck_var_has_type_list(Args,
 				PredArgTypes, 0, TypeCheckInfo1,
-				TypeCheckInfo)
+				TypeCheckInfo2),
+			    ( 
+					% sanity check
+			        PredClassContext \= []
+			    ->
+			        error("non-polymorphic pred has class context")
+			    ;
+			    	true
+			    )
 			;
 			    typecheck_var_has_polymorphic_type_list(
 				Args, PredTypeVarSet, PredArgTypes,
-				TypeCheckInfo1, TypeCheckInfo)
-			)
+				PredClassContext,
+				TypeCheckInfo1, TypeCheckInfo2)
+			),
+				% Arguably, we could do context reduction at
+				% a different point. See the paper:
+				% "Type classes: an exploration of the design
+				% space", S.P. Jones, M. Jones 1997.
+				% for a discussion of some of the issues.
+			perform_context_reduction(TypeCheckInfo2, TypeCheckInfo)
 		;
 			typecheck_info_get_pred_import_status(TypeCheckInfo1,
 						CallingStatus),
@@ -1109,8 +1163,9 @@
 		TypeAssignSet0, ArgsTypeAssignSet0, ArgsTypeAssignSet) :-
 	map__lookup(Preds, PredId, PredInfo),
 	pred_info_arg_types(PredInfo, PredTypeVarSet, PredArgTypes),
+	pred_info_get_class_context(PredInfo, PredClassContext),
 	rename_apart(TypeAssignSet0, PredTypeVarSet, PredArgTypes,
-		ArgsTypeAssignSet0, ArgsTypeAssignSet1),
+		PredClassContext, ArgsTypeAssignSet0, ArgsTypeAssignSet1),
 	get_overloaded_pred_arg_types(PredIds, Preds, CallingPredStatus,
 		TypeAssignSet0, ArgsTypeAssignSet1, ArgsTypeAssignSet).
 
@@ -1142,7 +1197,7 @@
 	;
 		% if there is no matching predicate for this call,
 		% then this predicate must have a type error which
-		% should have been caught by in typechecking.
+		% should have been caught by typechecking.
 		error("type error in pred call: no matching pred")
 	).
 
@@ -1203,42 +1258,49 @@
 	% assignment set", and then for each arg type assignment in the
 	% arg type assignment set, check that the argument variables have
 	% the expected types.
+	% A set of class constraints are also passed in, which must have the
+	% types contained within renamed apart. 
 
 :- pred typecheck_var_has_polymorphic_type_list(list(var), tvarset, list(type),
-		typecheck_info, typecheck_info).
-:- mode typecheck_var_has_polymorphic_type_list(in, in, in,
+		list(class_constraint), typecheck_info, typecheck_info).
+:- mode typecheck_var_has_polymorphic_type_list(in, in, in, in,
 		typecheck_info_di, typecheck_info_uo) is det.
 
 typecheck_var_has_polymorphic_type_list(Args, PredTypeVarSet, PredArgTypes,
-		TypeCheckInfo0, TypeCheckInfo) :-
+		PredClassConstraints, TypeCheckInfo0, TypeCheckInfo) :-
 	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
 	rename_apart(TypeAssignSet0, PredTypeVarSet, PredArgTypes,
-				[], ArgsTypeAssignSet),
+				PredClassConstraints, [], ArgsTypeAssignSet),
 	typecheck_var_has_arg_type_list(Args, 0, ArgsTypeAssignSet,
 				TypeCheckInfo0, TypeCheckInfo).
 
 :- pred rename_apart(type_assign_set, tvarset, list(type),
+			list(class_constraint),
                         args_type_assign_set, args_type_assign_set).
-:- mode rename_apart(in, in, in, in, out) is det.
+:- mode rename_apart(in, in, in, in, in, out) is det.
 
-rename_apart([], _, _, ArgTypeAssigns, ArgTypeAssigns).
+rename_apart([], _, _, _, ArgTypeAssigns, ArgTypeAssigns).
 rename_apart([TypeAssign0 | TypeAssigns0], PredTypeVarSet, PredArgTypes0,
-		ArgTypeAssigns0, ArgTypeAssigns) :-
+		PredClassConstraints0, ArgTypeAssigns0, ArgTypeAssigns) :-
         type_assign_rename_apart(TypeAssign0, PredTypeVarSet, PredArgTypes0,
-                        TypeAssign, PredArgTypes),
-        ArgTypeAssigns1 = [TypeAssign - PredArgTypes | ArgTypeAssigns0],
+                        TypeAssign, PredArgTypes, Subst),
+	apply_subst_to_constraints(Subst, PredClassConstraints0,
+		PredClassConstraints),
+	NewArgTypeAssign = args(TypeAssign, PredArgTypes, PredClassConstraints),
+        ArgTypeAssigns1 = [NewArgTypeAssign | ArgTypeAssigns0],
         rename_apart(TypeAssigns0, PredTypeVarSet, PredArgTypes0,
-			ArgTypeAssigns1, ArgTypeAssigns).
+			PredClassConstraints0, ArgTypeAssigns1, ArgTypeAssigns).
 
 :- pred type_assign_rename_apart(type_assign, tvarset, list(type),
-			type_assign, list(type)).
-:- mode type_assign_rename_apart(in, in, in, out, out) is det.
+			type_assign, list(type), substitution).
+:- mode type_assign_rename_apart(in, in, in, out, out, out) is det.
 
 type_assign_rename_apart(TypeAssign0, PredTypeVarSet, PredArgTypes0,
-		TypeAssign, PredArgTypes) :-
+		TypeAssign, PredArgTypes, Subst) :-
 	type_assign_get_typevarset(TypeAssign0, TypeVarSet0),
-	varset__merge(TypeVarSet0, PredTypeVarSet, PredArgTypes0,
-			  TypeVarSet, PredArgTypes),
+	varset__merge_subst(TypeVarSet0, PredTypeVarSet, TypeVarSet, Subst),
+	term__apply_substitution_to_list(PredArgTypes0, Subst,
+		PredArgTypes),
 	type_assign_set_typevarset(TypeAssign0, TypeVarSet, TypeAssign).
 
 %-----------------------------------------------------------------------------%
@@ -1267,10 +1329,19 @@
 :- mode convert_args_type_assign_set(in, out) is det.
 
 convert_args_type_assign_set([], []).
-convert_args_type_assign_set([TypeAssign - Args | ArgTypeAssigns],
-				[TypeAssign | TypeAssigns]) :-
+convert_args_type_assign_set(
+			[args(TypeAssign0, Args, Constraints0)|ArgTypeAssigns],
+			[TypeAssign | TypeAssigns]) :-
 	( Args = [] ->
-		true
+		type_assign_get_typeclass_constraints(TypeAssign0,
+			OldConstraints),
+		type_assign_get_type_bindings(TypeAssign0, Bindings),
+		apply_rec_subst_to_constraints(Bindings, Constraints0,
+			Constraints),
+
+		list__append(Constraints, OldConstraints, NewConstraints),
+		type_assign_set_typeclass_constraints(TypeAssign0,
+			NewConstraints, TypeAssign)
 	;
 		% this should never happen, since the arguments should
 		% all have been processed at this point
@@ -1278,14 +1349,6 @@
 	),
 	convert_args_type_assign_set(ArgTypeAssigns, TypeAssigns).
 
-:- pred conv_args_type_assign_set(args_type_assign_set, type_assign_set).
-:- mode conv_args_type_assign_set(in, out) is det.
-
-conv_args_type_assign_set([], []).
-conv_args_type_assign_set([X|Xs], [Y|Ys]) :-
-	conv_args_type_assign(X, Y),
-	conv_args_type_assign_set(Xs, Ys).
-
 :- pred conv_args_type_assign(pair(type_assign, list(type)), type_assign).
 :- mode conv_args_type_assign(in, out) is det.
 
@@ -1323,8 +1386,8 @@
 :- mode skip_arg(in, out) is det.
 
 skip_arg([], []).
-skip_arg([TypeAssign - Args0 | ArgTypeAssigns0],
-				[TypeAssign - Args| ArgTypeAssigns]) :-
+skip_arg([args(TypeAssign, Args0, Constraints) | ArgTypeAssigns0],
+		[args(TypeAssign, Args, Constraints)| ArgTypeAssigns]) :-
 	( Args0 = [_ | Args1] ->
 		Args = Args1
 	;
@@ -1338,18 +1401,20 @@
 :- mode typecheck_var_has_arg_type_2(in, in, in, in, out) is det.
 
 typecheck_var_has_arg_type_2([], _, _) --> [].
-typecheck_var_has_arg_type_2([TypeAssign0 - ArgTypes0 | TypeAssignSet0],
-				HeadTypeParams, VarId) -->
+typecheck_var_has_arg_type_2(
+		[args(TypeAssign0, ArgTypes0, ClassContext) | TypeAssignSet0],
+		HeadTypeParams, VarId) -->
 	arg_type_assign_var_has_type(TypeAssign0, ArgTypes0,
-					HeadTypeParams, VarId),
+					HeadTypeParams, VarId, ClassContext),
 	typecheck_var_has_arg_type_2(TypeAssignSet0, HeadTypeParams, VarId).
 
 :- pred arg_type_assign_var_has_type(type_assign, list(type), headtypes, var,
+				list(class_constraint),
 				args_type_assign_set, args_type_assign_set).
-:- mode arg_type_assign_var_has_type(in, in, in, in, in, out) is det.
+:- mode arg_type_assign_var_has_type(in, in, in, in, in, in, out) is det.
 
 arg_type_assign_var_has_type(TypeAssign0, ArgTypes0, HeadTypeParams, VarId,
-		ArgTypeAssignSet0, ArgTypeAssignSet) :-
+		ClassContext, ArgTypeAssignSet0, ArgTypeAssignSet) :-
 	type_assign_get_var_types(TypeAssign0, VarTypes0),
 	( ArgTypes0 = [Type | ArgTypes] ->
 	    (
@@ -1359,15 +1424,17 @@
 		    type_assign_unify_type(TypeAssign0, HeadTypeParams,
 				VarType, Type, TypeAssign1)
 		->
-		    ArgTypeAssignSet = [TypeAssign1 - ArgTypes |
-					ArgTypeAssignSet0]
+		    ArgTypeAssignSet = 
+		    		[args(TypeAssign1, ArgTypes, ClassContext) |
+				ArgTypeAssignSet0]
 		;
 		    ArgTypeAssignSet = ArgTypeAssignSet0
 		)
 	    ;
 		map__det_insert(VarTypes0, VarId, Type, VarTypes),
 		type_assign_set_var_types(TypeAssign0, VarTypes, TypeAssign),
-		ArgTypeAssignSet = [TypeAssign - ArgTypes | ArgTypeAssignSet0]
+		ArgTypeAssignSet = [args(TypeAssign, ArgTypes, ClassContext)
+					| ArgTypeAssignSet0]
 	    )
 	;
 	    error("arg_type_assign_var_has_type")
@@ -1461,7 +1528,8 @@
 :- pred get_arg_type_stuff(args_type_assign_set, var, list(arg_type_stuff)).
 :- mode get_arg_type_stuff(in, in, out) is det.
 get_arg_type_stuff([], _VarId, []).
-get_arg_type_stuff([TypeAssign - ArgTypes | ArgTypeAssigns], VarId, L) :-
+get_arg_type_stuff([args(TypeAssign, ArgTypes, _) | ArgTypeAssigns], 
+			VarId, L) :-
 	get_arg_type_stuff(ArgTypeAssigns, VarId, L0),
 	type_assign_get_type_bindings(TypeAssign, TypeBindings),
 	type_assign_get_typevarset(TypeAssign, TVarSet),
@@ -1671,7 +1739,8 @@
 typecheck_unification(X, var(Y), var(Y)) -->
 	typecheck_unify_var_var(X, Y).
 typecheck_unification(X, functor(F, As), functor(F, As)) -->
-	typecheck_unify_var_functor(X, F, As).
+	typecheck_unify_var_functor(X, F, As),
+	perform_context_reduction.
 typecheck_unification(X, lambda_goal(PredOrFunc, Vars, Modes, Det, Goal0),
 			 lambda_goal(PredOrFunc, Vars, Modes, Det, Goal)) -->
  	typecheck_lambda_var_has_type(PredOrFunc, X, Vars),
@@ -1805,7 +1874,14 @@
 :- type cons_type ---> cons_type(type, list(type)).
 :- type cons_type_assign_set == list(pair(type_assign, cons_type)).
 
-:- type args_type_assign_set == list(pair(type_assign, list(type))).
+:- type args_type_assign_set == list(args_type_assign).
+
+:- type args_type_assign 
+	--->	args(
+			type_assign, 	% Type assignment, 
+			list(type), 	% types of callee,
+			list(class_constraint) % constraints from callee
+		).
 
 :- pred typecheck_unify_var_functor_get_ctors(type_assign_set,
 				typecheck_info, list(cons_type_info),
@@ -1869,7 +1945,7 @@
 	is det.
 
 typecheck_functor_arg_types([], _, _) --> [].
-typecheck_functor_arg_types([TypeAssign - ArgTypes | ConsTypeAssigns],
+typecheck_functor_arg_types([args(TypeAssign, ArgTypes, _) | ConsTypeAssigns],
 			Args, TypeCheckInfo) -->
 	type_assign_var_has_type_list(Args, ArgTypes, TypeAssign,
 		TypeCheckInfo),
@@ -1981,15 +2057,22 @@
 			type_assign_unify_type(TypeAssign1, HeadTypeParams,
 					ConsType, TypeY, TypeAssign2)
 		->
-			TypeAssignSet = [TypeAssign2 - ArgTypes |
+				% The constraints are empty here because
+				% none are added by unification with a
+				% functor
+			TypeAssignSet = [args(TypeAssign2, ArgTypes, []) |
 					TypeAssignSet0]
 		;
 			TypeAssignSet = TypeAssignSet0
 		)
 	;
+			% The constraints are empty here because
+			% none are added by unification with a
+			% functor
 		map__det_insert(VarTypes0, Y, ConsType, VarTypes),
 		type_assign_set_var_types(TypeAssign1, VarTypes, TypeAssign3),
-		TypeAssignSet = [TypeAssign3 - ArgTypes | TypeAssignSet0]
+		TypeAssignSet = [args(TypeAssign3, ArgTypes, []) | 
+				TypeAssignSet0]
 	).
 
 %-----------------------------------------------------------------------------%
@@ -2006,7 +2089,8 @@
 get_cons_stuff(ConsDefn, TypeAssign0, _TypeCheckInfo, ConsType, ArgTypes,
 			TypeAssign) :-
 
-	ConsDefn = cons_type_info(ConsTypeVarSet, ConsType0, ArgTypes0),
+	ConsDefn = cons_type_info(ConsTypeVarSet, ConsType0, ArgTypes0,
+			ClassConstraints0),
 
 	% Rename apart the type vars in the type of the constructor
 	% and the types of its arguments.
@@ -2019,11 +2103,18 @@
 	;
 		type_assign_rename_apart(TypeAssign0, ConsTypeVarSet,
 			[ConsType0 | ArgTypes0],
-			TypeAssign1, [ConsType1 | ArgTypes1])
+			TypeAssign1, [ConsType1 | ArgTypes1], Subst)
 	->
+		apply_subst_to_constraints(Subst, ClassConstraints0,
+			ClassConstraints2),
+		type_assign_get_typeclass_constraints(TypeAssign1,
+			OldConstraints),
+		list__append(OldConstraints, ClassConstraints2,
+			ClassConstraints),
+		type_assign_set_typeclass_constraints(TypeAssign1,
+			ClassConstraints, TypeAssign),
 		ConsType = ConsType1,
-		ArgTypes = ArgTypes1,
-		TypeAssign = TypeAssign1
+		ArgTypes = ArgTypes1
 	;
 		error("get_cons_stuff: type_assign_rename_apart failed")
 	).
@@ -2185,7 +2276,15 @@
 	make_pred_cons_info_list(TypeCheckInfo, PredIds, PredTable, Arity,
 				ModuleInfo, L1, L).
 
-:- type cons_type_info ---> cons_type_info(tvarset, type, list(type)).
+:- type cons_type_info 
+	---> cons_type_info(
+			tvarset, 		% Type variables
+			type, 			% Constructor type
+			list(type), 		% Types of the arguments
+			list(class_constraint)	% Constraints introduced by 
+						% this constructor (ie. if it
+						% is actually a function).
+		).
 
 :- pred make_pred_cons_info(typecheck_info, pred_id, pred_table, int,
 		module_info, list(cons_type_info), list(cons_type_info)).
@@ -2196,6 +2295,7 @@
 	map__lookup(PredTable, PredId, PredInfo),
 	pred_info_arity(PredInfo, PredArity),
 	pred_info_get_is_pred_or_func(PredInfo, IsPredOrFunc),
+	pred_info_get_class_context(PredInfo, ClassContext),
 	(
 		IsPredOrFunc = predicate,
 		PredArity >= FuncArity
@@ -2210,7 +2310,7 @@
 			PredType = term__functor(term__atom("pred"),
 					PredTypeParams, Context),
 			ConsInfo = cons_type_info(PredTypeVarSet,
-					PredType, ArgTypes),
+					PredType, ArgTypes, ClassContext),
 			L = [ConsInfo | L0]
 		;
 			error("make_pred_cons_info: split_list failed")
@@ -2243,7 +2343,7 @@
 					], Context)
 			),
 			ConsInfo = cons_type_info(PredTypeVarSet,
-					FuncType, FuncArgTypes),
+					FuncType, FuncArgTypes, ClassContext),
 			L = [ConsInfo | L0]
 		;
 			error("make_pred_cons_info: split_list or remove_suffix failed")
@@ -2268,7 +2368,7 @@
 	Arity1 is Arity - 1,
 	higher_order_func_type(Arity1, TypeVarSet, FuncType, ArgTypes, RetType),
 	ConsTypeInfos = [cons_type_info(TypeVarSet, RetType,
-					[FuncType | ArgTypes])].
+					[FuncType | ArgTypes], [])].
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -2307,6 +2407,9 @@
 
 			headtypes,	% Head type params
 
+			list(class_constraint),
+					% The declared typeclass constraints
+
 			bool,		% Have we already warned about
 					% highly ambiguous overloading?
 			import_status
@@ -2358,24 +2461,28 @@
 %-----------------------------------------------------------------------------%
 
 :- pred typecheck_info_init(io__state, module_info, pred_id, varset,
-	varset, map(var, type), headtypes, import_status, typecheck_info).
-:- mode typecheck_info_init(di, in, in, in, in, in, in, in, typecheck_info_uo)
+	varset, map(var, type), headtypes, list(class_constraint),
+	import_status, typecheck_info).
+:- mode typecheck_info_init(di, in, in, in, in, in, in, in, in,
+	typecheck_info_uo)
 	is det.
 
 typecheck_info_init(IOState0, ModuleInfo, PredId, TypeVarSet, VarSet,
-		VarTypes, HeadTypeParams, Status, TypeCheckInfo) :-
+		VarTypes, HeadTypeParams, Constraints, Status, TypeCheckInfo) :-
 	CallPredId = unqualified("") / 0,
 	term__context_init(Context),
 	map__init(TypeBindings),
+	map__init(Proofs),
 	FoundTypeError = no,
 	WarnedAboutOverloading = no,
 	unsafe_promise_unique(IOState0, IOState),	% XXX
 	TypeCheckInfo = typecheck_info(
 		IOState, ModuleInfo, CallPredId, 0, PredId, Context,
-		unify_context(explicit, []),
-		VarSet, [type_assign(VarTypes, TypeVarSet, TypeBindings)],
-		FoundTypeError, HeadTypeParams, WarnedAboutOverloading,
-		Status
+		unify_context(explicit, []), VarSet, 
+		[type_assign(VarTypes, TypeVarSet, TypeBindings, 
+			Constraints, Proofs)],
+		FoundTypeError, HeadTypeParams, Constraints,
+		WarnedAboutOverloading, Status
 	).
 
 %-----------------------------------------------------------------------------%
@@ -2383,7 +2490,7 @@
 :- pred typecheck_info_get_io_state(typecheck_info, io__state).
 :- mode typecheck_info_get_io_state(typecheck_info_get_io_state, uo) is det.
 
-typecheck_info_get_io_state(typecheck_info(IOState0,_,_,_,_,_,_,_,_,_,_,_,_), 
+typecheck_info_get_io_state(typecheck_info(IOState0,_,_,_,_,_,_,_,_,_,_,_,_,_), 
 		IOState) :-
 	unsafe_promise_unique(IOState0, IOState).	% XXX
 
@@ -2393,8 +2500,9 @@
 :- mode typecheck_info_set_io_state(typecheck_info_set_io_state, di, 
 				typecheck_info_uo) is det.
 
-typecheck_info_set_io_state(typecheck_info(_,B,C,D,E,F,G,H,I,J,K,L,M), IOState0,
-			typecheck_info(IOState,B,C,D,E,F,G,H,I,J,K,L,M)) :-
+typecheck_info_set_io_state(typecheck_info(_,B,C,D,E,F,G,H,I,J,K,L,M,N), 
+			IOState0,
+			typecheck_info(IOState,B,C,D,E,F,G,H,I,J,K,L,M,N)) :-
 	unsafe_promise_unique(IOState0, IOState).	% XXX
 
 %-----------------------------------------------------------------------------%
@@ -2403,7 +2511,7 @@
 :- mode typecheck_info_get_module_name(in, out) is det.
 
 typecheck_info_get_module_name(TypeCheckInfo, Name) :-
-	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_),
+	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_,_),
 	module_info_name(ModuleInfo, Name).
 
 %-----------------------------------------------------------------------------%
@@ -2412,7 +2520,7 @@
 :- mode typecheck_info_get_module_info(in, out) is det.
 
 typecheck_info_get_module_info(TypeCheckInfo, ModuleInfo) :-
-	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2420,7 +2528,7 @@
 :- mode typecheck_info_get_preds(in, out) is det.
 
 typecheck_info_get_preds(TypeCheckInfo, Preds) :-
-	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_), 
+	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_,_), 
 	module_info_get_predicate_table(ModuleInfo, Preds).
 
 %-----------------------------------------------------------------------------%
@@ -2429,7 +2537,7 @@
 :- mode typecheck_info_get_types(in, out) is det.
 
 typecheck_info_get_types(TypeCheckInfo, Types) :-
-	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_),
+	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_,_),
 	module_info_types(ModuleInfo, Types).
 
 %-----------------------------------------------------------------------------%
@@ -2438,7 +2546,7 @@
 :- mode typecheck_info_get_ctors(in, out) is det.
 
 typecheck_info_get_ctors(TypeCheckInfo, Ctors) :-
-	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_),
+	TypeCheckInfo = typecheck_info(_,ModuleInfo,_,_,_,_,_,_,_,_,_,_,_,_),
 	module_info_ctors(ModuleInfo, Ctors).
 
 %-----------------------------------------------------------------------------%
@@ -2447,7 +2555,7 @@
 :- mode typecheck_info_get_called_predid(in, out) is det.
 
 typecheck_info_get_called_predid(TypeCheckInfo, PredId) :-
-	TypeCheckInfo = typecheck_info(_,_,PredId,_,_,_,_,_,_,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,PredId,_,_,_,_,_,_,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2457,8 +2565,8 @@
 			typecheck_info_uo) is det.
 
 typecheck_info_set_called_predid(PredCallId, TypeCheckInfo0, TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,_,D,E,F,G,H,I,J,K,L,M),
-	TypeCheckInfo = typecheck_info(A,B,PredCallId,D,E,F,G,H,I,J,K,L,M).
+	TypeCheckInfo0 = typecheck_info(A,B,_,D,E,F,G,H,I,J,K,L,M,N),
+	TypeCheckInfo = typecheck_info(A,B,PredCallId,D,E,F,G,H,I,J,K,L,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2466,7 +2574,7 @@
 :- mode typecheck_info_get_arg_num(in, out) is det.
 
 typecheck_info_get_arg_num(TypeCheckInfo, ArgNum) :-
-	TypeCheckInfo = typecheck_info(_,_,_,ArgNum,_,_,_,_,_,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,_,ArgNum,_,_,_,_,_,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2475,8 +2583,8 @@
 		typecheck_info_uo) is det.
 
 typecheck_info_set_arg_num(ArgNum, TypeCheckInfo0, TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,_,E,F,G,H,I,J,K,L,M),
-	TypeCheckInfo = typecheck_info(A,B,C,ArgNum,E,F,G,H,I,J,K,L,M).
+	TypeCheckInfo0 = typecheck_info(A,B,C,_,E,F,G,H,I,J,K,L,M,N),
+	TypeCheckInfo = typecheck_info(A,B,C,ArgNum,E,F,G,H,I,J,K,L,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2484,7 +2592,7 @@
 :- mode typecheck_info_get_predid(in, out) is det.
 
 typecheck_info_get_predid(TypeCheckInfo, PredId) :- 
-	TypeCheckInfo = typecheck_info(_,_,_,_,PredId,_,_,_,_,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,_,_,PredId,_,_,_,_,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2492,7 +2600,7 @@
 :- mode typecheck_info_get_context(in, out) is det.
 
 typecheck_info_get_context(TypeCheckInfo, Context) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,Context,_,_,_,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,_,_,_,Context,_,_,_,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2502,8 +2610,8 @@
 			typecheck_info_uo) is det.
 
 typecheck_info_set_context(Context, TypeCheckInfo0, TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,_,G,H,I,J,K,L,M),
-	TypeCheckInfo = typecheck_info(A,B,C,D,E,Context,G,H,I,J,K,L,M).
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,_,G,H,I,J,K,L,M,N),
+	TypeCheckInfo = typecheck_info(A,B,C,D,E,Context,G,H,I,J,K,L,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2511,7 +2619,7 @@
 :- mode typecheck_info_get_unify_context(in, out) is det.
 
 typecheck_info_get_unify_context(TypeCheckInfo, UnifyContext) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,UnifyContext,_,_,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,UnifyContext,_,_,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2521,8 +2629,8 @@
 			typecheck_info_uo) is det.
 
 typecheck_info_set_unify_context(UnifyContext, TypeCheckInfo0, TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,_,H,I,J,K,L,M),
-	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,UnifyContext,H,I,J,K,L,M).
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,_,H,I,J,K,L,M,N),
+	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,UnifyContext,H,I,J,K,L,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2530,7 +2638,7 @@
 :- mode typecheck_info_get_varset(in, out) is det.
 
 typecheck_info_get_varset(TypeCheckInfo, VarSet) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,VarSet,_,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,VarSet,_,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2538,7 +2646,7 @@
 :- mode typecheck_info_get_type_assign_set(in, out) is det.
 
 typecheck_info_get_type_assign_set(TypeCheckInfo, TypeAssignSet) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,TypeAssignSet,_,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,TypeAssignSet,_,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2644,8 +2752,8 @@
 
 typecheck_info_set_type_assign_set(TypeCheckInfo0, TypeAssignSet, 
 					TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,_,J,K,L,M),
-	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,TypeAssignSet,J,K,L,M).
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,_,J,K,L,M,N),
+	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,TypeAssignSet,J,K,L,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2653,7 +2761,7 @@
 :- mode typecheck_info_get_found_error(typecheck_info_ui, out) is det.
 
 typecheck_info_get_found_error(TypeCheckInfo, FoundError) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,_,FoundError,_,_,_).
+	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,_,FoundError,_,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2662,8 +2770,8 @@
 			typecheck_info_uo) is det.
 
 typecheck_info_set_found_error(TypeCheckInfo0, FoundError, TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,_,K,L,M),
-	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,FoundError,K,L,M).
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,_,K,L,M,N),
+	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,FoundError,K,L,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2671,7 +2779,8 @@
 :- mode typecheck_info_get_head_type_params(typecheck_info_ui, out) is det.
 
 typecheck_info_get_head_type_params(TypeCheckInfo, HeadTypeParams) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,_,_,HeadTypeParams,_,_).
+	TypeCheckInfo =
+		typecheck_info(_,_,_,_,_,_,_,_,_,_,HeadTypeParams,_,_,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2682,8 +2791,31 @@
 
 typecheck_info_set_head_type_params(TypeCheckInfo0, HeadTypeParams,
 					TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,_,L,M),
-	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,J,HeadTypeParams,L,M).
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,_,L,M,N),
+	TypeCheckInfo =
+		typecheck_info(A,B,C,D,E,F,G,H,I,J,HeadTypeParams,L,M,N).
+
+%-----------------------------------------------------------------------------%
+
+:- pred typecheck_info_get_constraints(typecheck_info, list(class_constraint)).
+:- mode typecheck_info_get_constraints(typecheck_info_ui, out) is det.
+
+typecheck_info_get_constraints(TypeCheckInfo, Constraints) :-
+	TypeCheckInfo =
+		typecheck_info(_,_,_,_,_,_,_,_,_,_,_,Constraints,_,_).
+
+%-----------------------------------------------------------------------------%
+
+:- pred typecheck_info_set_constraints(typecheck_info,
+	list(class_constraint), typecheck_info).
+:- mode typecheck_info_set_constraints(typecheck_info_di, in, 
+			typecheck_info_uo) is det.
+
+typecheck_info_set_constraints(TypeCheckInfo0, Constraints,
+					TypeCheckInfo) :-
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,_,M,N),
+	TypeCheckInfo =
+		typecheck_info(A,B,C,D,E,F,G,H,I,J,K,Constraints,M,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2692,7 +2824,7 @@
 			is det.
 
 typecheck_info_get_warned_about_overloading(TypeCheckInfo, Warned) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,_,_,_,Warned,_).
+	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,_,_,_,_,Warned,_).
 
 %-----------------------------------------------------------------------------%
 
@@ -2703,8 +2835,8 @@
 
 typecheck_info_set_warned_about_overloading(TypeCheckInfo0, Warned,
 				TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,_,M),
-	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,Warned,M).
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,L,_,N),
+	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,L,Warned,N).
 
 %-----------------------------------------------------------------------------%
 
@@ -2712,7 +2844,7 @@
 :- mode typecheck_info_get_pred_import_status(typecheck_info_ui, out) is det.
 
 typecheck_info_get_pred_import_status(TypeCheckInfo, Status) :-
-	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,_,_,_,_,Status).
+	TypeCheckInfo = typecheck_info(_,_,_,_,_,_,_,_,_,_,_,_,_,Status).
 
 :- pred typecheck_info_set_pred_import_status(typecheck_info, import_status,
 			typecheck_info).
@@ -2720,8 +2852,8 @@
 			typecheck_info_uo) is det.
 
 typecheck_info_set_pred_import_status(TypeCheckInfo0, Status, TypeCheckInfo) :-
-	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,L,_),
-	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,L,Status).
+	TypeCheckInfo0 = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,L,M,_),
+	TypeCheckInfo = typecheck_info(A,B,C,D,E,F,G,H,I,J,K,L,M,Status).
 
 %-----------------------------------------------------------------------------%
 
@@ -2769,7 +2901,7 @@
 		ConsType = term__functor(term__atom(BuiltInTypeName), [],
 				Context),
 		varset__init(ConsTypeVarSet),
-		ConsInfo = cons_type_info(ConsTypeVarSet, ConsType, []),
+		ConsInfo = cons_type_info(ConsTypeVarSet, ConsType, [], []),
 		ConsInfoList1 = [ConsInfo | ConsInfoList0]
 	;
 		ConsInfoList1 = ConsInfoList0
@@ -2786,6 +2918,410 @@
 		ConsInfoList = ConsInfoList1
 	).
 
+	% Add  a set of constraints to each type_assign in the typecheck info.
+:- pred typecheck_info_add_type_assign_constraints(list(class_constraint),
+	typecheck_info, typecheck_info).
+:- mode typecheck_info_add_type_assign_constraints(in, typecheck_info_di, 
+	typecheck_info_uo) is det.
+
+typecheck_info_add_type_assign_constraints(NewConstraints, TypecheckInfo0,
+		TypecheckInfo) :-
+	typecheck_info_get_type_assign_set(TypecheckInfo0, TypeAssignSet0),
+	AddConstraints = lambda([TypeAssign0::in, TypeAssign::out] is det,
+		(
+		type_assign_get_typeclass_constraints(TypeAssign0,
+			OldConstraints), 
+		list__append(NewConstraints, OldConstraints, Constraints),
+		type_assign_set_typeclass_constraints(TypeAssign0,
+			Constraints, TypeAssign)
+		)),
+	list__map(AddConstraints, TypeAssignSet0, TypeAssignSet),
+	typecheck_info_set_type_assign_set(TypecheckInfo0, TypeAssignSet,
+		TypecheckInfo).
+
+%-----------------------------------------------------------------------------%
+
+	% typecheck_constraints(Inferring, TypeCheckInfo0, TypeCheckInfo)
+	%
+	% Produces TypeCheckInfo from TypeCheckInfo0 by rejecting any
+	% type_assign in TypeCheckInfo0 whose calculated typeclass constraints
+	% do not match the declared constraints.
+	%
+	% An appropriate error message is given if all type_assigns are 
+	% rejected.
+:- pred typecheck_constraints(bool, typecheck_info, typecheck_info).
+:- mode typecheck_constraints(in, typecheck_info_di, typecheck_info_uo) is det.
+
+	% XXX if we're inferring, don't bother checking the constraints at this
+	% XXX stage. Fix this up. Handling inference isn't actually that
+	% XXX difficult: you just collect the constraint set, perform context
+	% XXX reduction, and that is the class context of the pred.
+typecheck_constraints(yes, TypeCheckInfo, TypeCheckInfo).
+typecheck_constraints(no, TypeCheckInfo0, TypeCheckInfo) :-
+		%get the declared constraints
+	typecheck_info_get_constraints(TypeCheckInfo0, DeclaredConstraints),
+
+	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
+
+	ConstraintsMatch = lambda([TypeAssign::in] is semidet,
+		(
+			type_assign_get_typeclass_constraints(TypeAssign,
+				CalculatedConstraints0),
+			type_assign_get_type_bindings(TypeAssign, Bindings),
+			apply_rec_subst_to_constraints(Bindings,
+				CalculatedConstraints0, CalculatedConstraints1),
+			list__sort_and_remove_dups(CalculatedConstraints1, 
+				CalculatedConstraints),
+				% XXX. This needs thought. _When_ exactly
+				% do two constraint sets match? This is
+				% certainly too strict.
+			CalculatedConstraints = DeclaredConstraints
+		)),
+
+		% reject any type assignment whose constraints don't match the
+		% declared ones
+	list__filter(ConstraintsMatch, TypeAssignSet0, TypeAssignSet),
+	(
+			% Check that we haven't just eliminated
+			% all the type assignments. 
+		TypeAssignSet = [], 
+		TypeAssignSet0 \= []
+	->
+		report_unsatisfied_constraints(TypeAssignSet0,
+			TypeCheckInfo0, TypeCheckInfo)
+	;
+		typecheck_info_set_type_assign_set(TypeCheckInfo0,
+			TypeAssignSet, TypeCheckInfo)
+	).
+
+%-----------------------------------------------------------------------------%
+
+:- pred report_unsatisfied_constraints(type_assign_set,
+	typecheck_info, typecheck_info).
+:- mode report_unsatisfied_constraints(in,
+	typecheck_info_di, typecheck_info_uo) is det.
+
+report_unsatisfied_constraints(TypeAssignSet, TypeCheckInfo0, TypeCheckInfo) :-
+	typecheck_info_get_io_state(TypeCheckInfo0, IOState0),
+
+	typecheck_info_get_constraints(TypeCheckInfo0, DeclaredConstraints),
+
+	typecheck_info_get_context(TypeCheckInfo0, Context),
+	write_context_and_pred_id(TypeCheckInfo0, IOState0, IOState1),
+	prog_out__write_context(Context, IOState1, IOState2),
+	io__write_string("  unsatisfied typeclass constraint(s):\n",
+		IOState2, IOState3),
+
+	WriteConstraints = lambda([TheTypeAssign::in, IO0::di, IO::uo] is det,
+		(
+			type_assign_get_typeclass_constraints(
+				TheTypeAssign, TheConstraints0),
+			type_assign_get_typevarset(TheTypeAssign, TheVarSet),
+			type_assign_get_type_bindings(TheTypeAssign, Bindings),
+			apply_rec_subst_to_constraints(Bindings,
+				TheConstraints0, TheConstraints1),
+			list__sort_and_remove_dups(TheConstraints1,
+				TheConstraints),
+			list__delete_elems(TheConstraints, DeclaredConstraints,
+				Unsatisfied),
+			prog_out__write_context(Context, IO0, IO1),
+			io__write_list(Unsatisfied, ", ",
+				mercury_output_constraint(TheVarSet), IO1, IO2),
+			io__write_char('\n', IO2, IO)
+		)),
+
+		% XXX this won't be very pretty when there are
+		% XXX multiple type_assigns.
+	io__write_list(TypeAssignSet, "\n", WriteConstraints, 
+		IOState3, IOState),
+
+	typecheck_info_set_io_state(TypeCheckInfo0, IOState, TypeCheckInfo1),
+	typecheck_info_set_found_error(TypeCheckInfo1, yes, TypeCheckInfo).
+
+%-----------------------------------------------------------------------------%
+
+% perform_context_reduction(TypeCheckInfo0, TypeCheckInfo) is true iff
+% 	TypeCheckInfo is the typecheck_info that results from performing
+% 	context reduction on the type_assigns in TypeCheckInfo0.
+%
+% 	Context reduction is the process of eliminating redundant constraints
+% 	from the constraints in the type_assign and adding the proof of the
+% 	constraint's redundancy to the proofs in the same type_assign. There
+% 	are two ways in which a constraint may be redundant:
+% 		- if there is an instance declaration that may be applied, the
+% 		  constraint is replaced by the constraints from that instance
+% 		  declaration
+% 		- if a constraint is present in the set of constraints and all
+% 		  of the "superclass" constraints for the constraints are all
+% 		  present, then all the superclass constraints are eliminated
+%
+% 	In addition, context reduction removes repeated constraints.
+%
+% 	If context reduction fails on a type_assign, that type_assign is
+% 	removed from the type_assign_set. Context reduction fails if there is
+%	a constraint where the type of (at least) one of the arguments to
+%	the constraint has its top level functor bound, but there is no
+%	instance declaration for that type.
+%
+%	If all type_assigns from the typecheck_info are rejected, than an
+%	appropriate error message is given.
+
+:- pred perform_context_reduction(typecheck_info, typecheck_info).
+:- mode perform_context_reduction(typecheck_info_di, typecheck_info_uo) is det.
+
+perform_context_reduction(TypeCheckInfo0, TypeCheckInfo) :-
+	typecheck_info_get_module_info(TypeCheckInfo0, ModuleInfo),
+	module_info_classes(ModuleInfo, ClassTable),
+	module_info_instances(ModuleInfo, InstanceTable),
+	typecheck_info_get_type_assign_set(TypeCheckInfo0, TypeAssignSet0),
+	list__filter_map(reduce_type_assign_context(ClassTable, InstanceTable), 
+		TypeAssignSet0, TypeAssignSet),
+	(
+			% Check that this context reduction hasn't eliminated
+			% all the type assignments.
+		TypeAssignSet = [], 
+		TypeAssignSet0 \= []
+	->
+		report_unsatisfied_constraints(TypeAssignSet0,
+			TypeCheckInfo0, TypeCheckInfo)
+	;
+		typecheck_info_set_type_assign_set(TypeCheckInfo0,
+			TypeAssignSet, TypeCheckInfo)
+	).
+
+:- pred reduce_type_assign_context(class_table, instance_table, 
+	type_assign, type_assign).
+:- mode reduce_type_assign_context(in, in, in, out) is semidet.
+
+reduce_type_assign_context(ClassTable, InstanceTable, 
+		TypeAssign0, TypeAssign) :-
+	type_assign_get_typeclass_constraints(TypeAssign0, Constraints0),
+	type_assign_get_type_bindings(TypeAssign0, Bindings),
+	type_assign_get_typevarset(TypeAssign0, Tvarset0),
+	type_assign_get_constraint_proofs(TypeAssign0, Proofs0),
+
+	typecheck__reduce_context_by_rule_application(InstanceTable, 
+		ClassTable, Bindings, Tvarset0, Tvarset, Proofs0, Proofs,
+		Constraints0, Constraints),
+
+	type_assign_set_typeclass_constraints(TypeAssign0, Constraints,
+		TypeAssign1),
+	type_assign_set_typevarset(TypeAssign1, Tvarset, TypeAssign2),
+	type_assign_set_constraint_proofs(TypeAssign2, Proofs, TypeAssign).
+
+
+typecheck__reduce_context_by_rule_application(InstanceTable, ClassTable, 
+		Bindings, Tvarset0, Tvarset, Proofs0, Proofs, 
+		Constraints0, Constraints) :-
+	apply_instance_rules(Constraints0, InstanceTable, Bindings, 
+		Tvarset0, Tvarset1, Proofs0, Proofs1, Constraints1, Changed1),
+	apply_class_rules(Constraints1, ClassTable, Bindings, Tvarset1,
+		Proofs1, Proofs2, Constraints2, Changed2),
+	(
+		Changed1 = no, Changed2 = no
+	->
+			% We have reached fixpoint
+		list__sort_and_remove_dups(Constraints2, Constraints),
+		Tvarset = Tvarset1,
+		Proofs = Proofs2
+	;
+		typecheck__reduce_context_by_rule_application(InstanceTable,
+			ClassTable, Bindings, Tvarset1, Tvarset, Proofs2,
+			Proofs, Constraints2, Constraints)
+	).
+
+:- pred apply_instance_rules(list(class_constraint), instance_table,
+	tsubst, tvarset, tvarset, map(class_constraint, constraint_proof),
+	map(class_constraint, constraint_proof), list(class_constraint), bool).
+:- mode apply_instance_rules(in, in, in, in, out, in, out, out, out) is semidet.
+
+apply_instance_rules([], _, _, Names, Names, Proofs, Proofs, [], no).
+apply_instance_rules([C|Cs], InstanceTable, Bindings, 
+		TVarSet, NewTVarSet, Proofs0, Proofs, 
+		Constraints, Changed) :-
+	C = constraint(ClassName, Types0),
+	list__length(Types0, Arity),
+	map__lookup(InstanceTable, class_id(ClassName, Arity), Instances),
+	term__apply_rec_substitution_to_list(Types0, Bindings, Types),
+	(
+		find_matching_instance_rule(Instances, ClassName, Types,
+			TVarSet, NewTVarSet0, Proofs0, Proofs1,
+			NewConstraints0)
+	->
+			% Put the new constraints at the front of the list
+		NewConstraints = NewConstraints0,
+		NewTVarSet1 = NewTVarSet0,
+		Proofs2 = Proofs1,
+		Changed1 = yes
+	;
+			% Put the old constraint at the front of the list
+		NewConstraints = [C],
+		NewTVarSet1 = TVarSet,
+		Proofs2 = Proofs0,


love and cuddles,
dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) |  Marge: Did you just call everyone "chicken"?
MEngSc student,                 |  Homer: Noooo.  I swear on this Bible!
Department of Computer Science  |  Marge: That's not a Bible; that's a book of
University of Melbourne         |         carpet samples!
Australia                       |  Homer: Ooooh... Fuzzy.



More information about the developers mailing list