support for non-canonical types (user-defined equality preds)

Fergus Henderson fjh at cs.mu.oz.au
Thu Jul 17 06:10:14 AEST 1997


Hi,

I've finished implementing support for types with user-defined equality
predicates.  Anyone want to review this one?

Any opinions on whether this should be included in Mercury 0.7?

As it stands, there are just a couple of things standing in the way
of it being generally useful and easy-to-use:

	* the only mechanism for promising that things are
	  unique is via the C interface

	* since we haven't implemented type classes,
	  there is no way for the user to override
	  compare/3, arg/3, functor/3, write/3, etc.
	  for non-canonical types.  Instead calls to
	  all these for such types are runtime errors.

--------------------

Implement support for types with user-defined equality predicates.

Types with user-defined equality predicates are called "non-canonical types";
they may have more than one representation for the same abstract value.
That means that any attempt to deconstruct a value of a non-canonical
type, i.e. any attempt to peek at the representation, must be cc_multi.

This also implies that conceptually speaking, non-canonical types are not
members of the type classes `comparable' (compare/3) or `deconstructible'
(index/2, argument/3, functor/3, deconstruct/5).  Since we don't support
type classes yet, that just means that the type-class checking is done
at runtime, i.e. any call to one of those functions for a non-canonical
type will call error/1 or fatal_error().

To make non-canonical types useful, we really need type classes,
so that the user can provide instance definitions for `comparable'
and `deconstructible' for such types.  It might also be a good idea
to have a type-class `canonicalizable' which provides a function
to convert its argument to some canonical type (that would
require existential types to do nicely, but alternatively we could
just use `univ').

cvs diff: Diffing .
cvs diff: Diffing bindist
cvs diff: Diffing boehm_gc
cvs diff: Diffing boehm_gc/Mac_files
cvs diff: Diffing boehm_gc/cord
cvs diff: Diffing boehm_gc/cord/private
cvs diff: Diffing boehm_gc/include
cvs diff: Diffing boehm_gc/include/private
cvs diff: Diffing bytecode
cvs diff: Diffing compiler
Index: compiler/base_type_layout.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/base_type_layout.m,v
retrieving revision 1.19
diff -u -r1.19 base_type_layout.m
--- base_type_layout.m	1997/05/23 06:16:15	1.19
+++ base_type_layout.m	1997/06/30 06:49:49
@@ -350,7 +350,7 @@
 		LayoutTypeData = [],
 		FunctorsTypeData = []
 	;
-		TypeBody = du_type(Ctors, ConsTagMap, Enum),
+		TypeBody = du_type(Ctors, ConsTagMap, Enum, _EqualityPred),
 
 			% sort list on tags, so that 
 			% enums, complicated constants and
Index: compiler/code_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/code_util.m,v
retrieving revision 1.86
diff -u -r1.86 code_util.m
--- code_util.m	1997/05/20 01:51:38	1.86
+++ code_util.m	1997/07/16 13:21:55
@@ -527,10 +527,7 @@
 code_util__compiler_generated(PredInfo) :-
 	pred_info_name(PredInfo, PredName),
 	pred_info_arity(PredInfo, PredArity),
-	( PredName = "__Unify__", PredArity = 2
-	; PredName = "__Compare__", PredArity = 3
-	; PredName = "__Index__", PredArity = 2
-	).
+	special_pred_name_arity(_, _, PredName, PredArity).
 
 %-----------------------------------------------------------------------------%
 
@@ -671,7 +668,7 @@
 		map__lookup(TypeTable, TypeId, TypeDefn),
 		hlds_data__get_type_defn_body(TypeDefn, TypeBody),
 		(
-			TypeBody = du_type(_, ConsTable0, _)
+			TypeBody = du_type(_, ConsTable0, _, _)
 		->
 			ConsTable = ConsTable0
 		;
Index: compiler/dense_switch.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/dense_switch.m,v
retrieving revision 1.26
diff -u -r1.26 dense_switch.m
--- dense_switch.m	1997/06/29 23:10:24	1.26
+++ dense_switch.m	1997/06/30 06:49:49
@@ -128,7 +128,7 @@
 	{ module_info_types(ModuleInfo, TypeTable) },
 	{ map__lookup(TypeTable, TypeId, TypeDefn) },
 	{ hlds_data__get_type_defn_body(TypeDefn, TypeBody) },
-	{ TypeBody = du_type(_, ConsTable, _) ->
+	{ TypeBody = du_type(_, ConsTable, _, _) ->
 		map__count(ConsTable, TypeRange)
 	;
 		error("dense_switch__type_range: enum type is not d.u. type?")
Index: compiler/det_analysis.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/det_analysis.m,v
retrieving revision 1.118
diff -u -r1.118 det_analysis.m
--- det_analysis.m	1997/07/09 05:44:05	1.118
+++ det_analysis.m	1997/07/16 17:29:04
@@ -99,7 +99,7 @@
 :- implementation.
 
 :- import_module hlds_goal, prog_data, det_report, det_util.
-:- import_module mode_util, globals, options, passes_aux.
+:- import_module type_util, mode_util, globals, options, passes_aux.
 :- import_module hlds_out, mercury_to_mercury, instmap.
 :- import_module bool, list, map, set, std_util, require, term.
 
@@ -385,14 +385,30 @@
 	% then it is semideterministic or worse - this is determined
 	% in switch_detection.m and handled via the SwitchCanFail field.
 
-det_infer_goal_2(switch(Var, SwitchCanFail, Cases0, SM), _,
+det_infer_goal_2(switch(Var, SwitchCanFail, Cases0, SM), GoalInfo,
 		InstMap0, SolnContext, DetInfo, _, _,
 		switch(Var, SwitchCanFail, Cases, SM), Detism, Msgs) :-
 	det_infer_switch(Cases0, InstMap0, SolnContext, DetInfo,
-		cannot_fail, at_most_zero, Cases, CasesDetism, Msgs),
+		cannot_fail, at_most_zero, Cases, CasesDetism, Msgs0),
 	determinism_components(CasesDetism, CasesCanFail, CasesSolns),
+	% The switch variable tests are in a first_soln context if and only
+	% if the switch goal as a whole was in a first_soln context and the
+	% cases cannot fail.
+	(
+		CasesCanFail = cannot_fail,
+		SolnContext = first_soln
+	->
+		SwitchSolnContext = first_soln
+	;
+		SwitchSolnContext = all_solns
+	),
+	ExaminesRep = yes,
+	det_check_for_noncanonical_type(Var, ExaminesRep, SwitchCanFail,
+		SwitchSolnContext, GoalInfo, switch, DetInfo, Msgs0,
+		SwitchSolns, Msgs),
 	det_conjunction_canfail(SwitchCanFail, CasesCanFail, CanFail),
-	determinism_components(Detism, CanFail, CasesSolns).
+	det_conjunction_maxsoln(SwitchSolns, CasesSolns, NumSolns),
+	determinism_components(Detism, CanFail, NumSolns).
 
 	% For calls, just look up the determinism entry associated with
 	% the called predicate.
@@ -435,7 +451,7 @@
 
 	% unifications are either deterministic or semideterministic.
 	% (see det_infer_unify).
-det_infer_goal_2(unify(LT, RT0, M, U, C), GoalInfo, InstMap0, _SolnContext,
+det_infer_goal_2(unify(LT, RT0, M, U, C), GoalInfo, InstMap0, SolnContext,
 		DetInfo, _, _, unify(LT, RT, M, U, C), UnifyDet, Msgs) :-
 	(
 		RT0 = lambda_goal(PredOrFunc, Vars, Modes, LambdaDeclaredDet,
@@ -456,14 +472,19 @@
 				Goal, LambdaInferredDet, Msgs1),
 		det_check_lambda(LambdaDeclaredDet, LambdaInferredDet,
 				Goal, GoalInfo, DetInfo, Msgs2),
-		list__append(Msgs1, Msgs2, Msgs),
+		list__append(Msgs1, Msgs2, Msgs3),
 		RT = lambda_goal(PredOrFunc, Vars, Modes, LambdaDeclaredDet,
 				Goal)
 	;
 		RT = RT0,
-		Msgs = []
+		Msgs3 = []
 	),
-	det_infer_unify(U, UnifyDet).
+	det_infer_unify_canfail(U, UnifyCanFail),
+	det_infer_unify_examines_rep(U, ExaminesRepresentation),
+	det_check_for_noncanonical_type(LT, ExaminesRepresentation,
+		UnifyCanFail, SolnContext, GoalInfo, unify(C), DetInfo, Msgs3,
+		UnifyNumSolns, Msgs),
+	determinism_components(UnifyDet, UnifyCanFail, UnifyNumSolns).
 
 det_infer_goal_2(if_then_else(Vars, Cond0, Then0, Else0, SM), _GoalInfo0,
 		InstMap0, SolnContext, DetInfo, _NonLocalVars, _DeltaInstMap,
@@ -677,26 +698,96 @@
 		MaxSolns2, Cases, Detism, Msgs2),
 	list__append(Msgs1, Msgs2, Msgs).
 
-	% Deconstruction unifications are deterministic if the type
+%-----------------------------------------------------------------------------%
+
+:- pred det_check_for_noncanonical_type(var, bool, can_fail, soln_context,
+		hlds_goal_info, cc_unify_context, det_info, list(det_msg),
+		soln_count, list(det_msg)).
+:- mode det_check_for_noncanonical_type(in, in, in, in,
+		in, in, in, in, out, out) is det.
+
+det_check_for_noncanonical_type(Var, ExaminesRepresentation, CanFail,
+		SolnContext, GoalInfo, GoalContext, DetInfo, Msgs0,
+		NumSolns, Msgs) :-
+	(
+		%
+		% check for unifications that attempt to examine
+		% the representation of a type that does not have
+		% a single representation for each abstract value
+		%
+		ExaminesRepresentation = yes,
+		det_get_proc_info(DetInfo, ProcInfo),
+		proc_info_vartypes(ProcInfo, VarTypes),
+		map__lookup(VarTypes, Var, Type),
+		det_type_has_user_defined_equality_pred(DetInfo, Type,
+			_TypeContext)
+	->
+		( CanFail = can_fail ->
+			proc_info_variables(ProcInfo, VarSet),
+			Msgs = [cc_unify_can_fail(GoalInfo, Var, Type,
+				VarSet, GoalContext) | Msgs0]
+		; SolnContext \= first_soln ->
+			proc_info_variables(ProcInfo, VarSet),
+			Msgs = [cc_unify_in_wrong_context(GoalInfo, Var,
+				Type, VarSet, GoalContext) | Msgs0]
+		;
+			Msgs = Msgs0
+		),
+		( SolnContext = first_soln ->
+			NumSolns = at_most_many_cc
+		;
+			NumSolns = at_most_many
+		)
+	;
+		NumSolns = at_most_one,
+		Msgs = Msgs0
+	).
+
+% return true iff there was a `where equality is <predname>' declaration
+% for the specified type.
+:- pred det_type_has_user_defined_equality_pred(det_info::in, (type)::in,
+		term__context::out) is semidet.
+det_type_has_user_defined_equality_pred(DetInfo, Type, TypeContext) :-
+	det_info_get_module_info(DetInfo, ModuleInfo),
+	module_info_types(ModuleInfo, TypeTable),
+	type_to_type_id(Type, TypeId, _TypeArgs),
+	map__search(TypeTable, TypeId, TypeDefn),
+	hlds_data__get_type_defn_body(TypeDefn, TypeBody),
+	TypeBody = du_type(_, _, _, yes(_)),
+	hlds_data__get_type_defn_context(TypeDefn, TypeContext).
+
+% return yes iff the results of the specified unification might depend on
+% the concrete representation of the abstract values involved.
+:- pred det_infer_unify_examines_rep(unification::in, bool::out) is det.
+det_infer_unify_examines_rep(assign(_, _), no).
+det_infer_unify_examines_rep(construct(_, _, _, _), no).
+det_infer_unify_examines_rep(deconstruct(_, _, _, _, _), yes).
+det_infer_unify_examines_rep(simple_test(_, _), yes).
+det_infer_unify_examines_rep(complicated_unify(_, _), no).
+	% Some complicated modes of complicated unifications _do_
+	% examine the representation...
+	% but we will catch those by reporting errors in the
+	% compiler-generated code for the complicated unification.
+
+
+	% Deconstruction unifications cannot fail if the type
 	% only has one constructor, or if the variable is known to be
 	% already bound to the appropriate functor.
 	% 
 	% This is handled (modulo bugs) by modes.m, which sets
-	% the determinism field in the deconstruct(...) to semidet for
+	% the appropriate field in the deconstruct(...) to can_fail for
 	% those deconstruction unifications which might fail.
-	% But switch_detection.m may set it back to det again, if it moves
-	% the functor test into a switch instead.
+	% But switch_detection.m may set it back to cannot_fail again,
+	% if it moves the functor test into a switch instead.
 
-:- pred det_infer_unify(unification, determinism).
-:- mode det_infer_unify(in, out) is det.
+:- pred det_infer_unify_canfail(unification, can_fail).
+:- mode det_infer_unify_canfail(in, out) is det.
 
-det_infer_unify(deconstruct(_, _, _, _, CanFail), Detism) :-
-	determinism_components(Detism, CanFail, at_most_one).
-det_infer_unify(assign(_, _), det).
-det_infer_unify(construct(_, _, _, _), det).
-det_infer_unify(simple_test(_, _), semidet).
-det_infer_unify(complicated_unify(_, CanFail), Detism) :-
-	determinism_components(Detism, CanFail, at_most_one).
+det_infer_unify_canfail(deconstruct(_, _, _, _, CanFail), CanFail).
+det_infer_unify_canfail(assign(_, _), cannot_fail).
+det_infer_unify_canfail(construct(_, _, _, _), cannot_fail).
+det_infer_unify_canfail(simple_test(_, _), can_fail).
+det_infer_unify_canfail(complicated_unify(_, CanFail), CanFail).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/det_report.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/det_report.m,v
retrieving revision 1.37
diff -u -r1.37 det_report.m
--- det_report.m	1997/07/03 14:38:20	1.37
+++ det_report.m	1997/07/16 17:30:51
@@ -14,7 +14,7 @@
 
 :- interface.
 
-:- import_module hlds_module, hlds_pred, hlds_goal, det_util.
+:- import_module hlds_module, hlds_pred, hlds_goal, det_util, prog_data.
 :- import_module io.
 
 :- type det_msg	--->
@@ -39,6 +39,10 @@
 				term__context)
 				% multiple calls with the same input args.
 			% errors
+		;	cc_unify_can_fail(hlds_goal_info, var, type, varset,
+				cc_unify_context)
+		;	cc_unify_in_wrong_context(hlds_goal_info, var, type,
+				varset, cc_unify_context)
 		;	cc_pred_in_wrong_context(hlds_goal_info, determinism,
 				pred_id, proc_id)
 		;	higher_order_cc_pred_in_wrong_context(hlds_goal_info,
@@ -51,6 +55,10 @@
 	--->	seen_call(pred_id, proc_id)
 	;	higher_order_call.
 
+:- type cc_unify_context
+	--->	unify(unify_context)
+	;	switch.
+
 %-----------------------------------------------------------------------------%
 
 	% Check all the determinism declarations in this module.
@@ -96,23 +104,33 @@
 
 global_checking_pass([], ModuleInfo, ModuleInfo) --> [].
 global_checking_pass([proc(PredId, ProcId) | Rest], ModuleInfo0, ModuleInfo) -->
-	{
-		module_info_preds(ModuleInfo0, PredTable),
-		map__lookup(PredTable, PredId, PredInfo),
-		pred_info_procedures(PredInfo, ProcTable),
-		map__lookup(ProcTable, ProcId, ProcInfo),
-		proc_info_declared_determinism(ProcInfo, MaybeDetism),
-		proc_info_inferred_determinism(ProcInfo, InferredDetism)
-	},
+	{ module_info_pred_proc_info(ModuleInfo0, PredId, ProcId,
+		PredInfo, ProcInfo) },
+	check_determinism(PredId, ProcId, PredInfo, ProcInfo,
+		ModuleInfo0, ModuleInfo1),
+	check_if_main_can_fail(PredId, ProcId, PredInfo, ProcInfo,
+		ModuleInfo1, ModuleInfo2),
+	check_for_multisoln_func(PredId, ProcId, PredInfo, ProcInfo,
+		ModuleInfo2, ModuleInfo3),
+	global_checking_pass(Rest, ModuleInfo3, ModuleInfo).
+
+:- pred check_determinism(pred_id, proc_id, pred_info, proc_info,
+		module_info, module_info, io__state, io__state).
+:- mode check_determinism(in, in, in, in, in, out, di, uo) is det.
+
+check_determinism(PredId, ProcId, _PredInfo, ProcInfo,
+		ModuleInfo0, ModuleInfo) -->
+	{ proc_info_declared_determinism(ProcInfo, MaybeDetism) },
+	{ proc_info_inferred_determinism(ProcInfo, InferredDetism) },
 	(
 		{ MaybeDetism = no },
-		{ ModuleInfo1 = ModuleInfo0 }
+		{ ModuleInfo = ModuleInfo0 }
 	;
 		{ MaybeDetism = yes(DeclaredDetism) },
 		{ compare_determinisms(DeclaredDetism, InferredDetism, Cmp) },
 		(
 			{ Cmp = sameas },
-			{ ModuleInfo1 = ModuleInfo0 }
+			{ ModuleInfo = ModuleInfo0 }
 		;
 			{ Cmp = looser },
 			globals__io_lookup_bool_option(
@@ -126,24 +144,33 @@
 			;
 				[]
 			),
-			{ ModuleInfo1 = ModuleInfo0 }
+			{ ModuleInfo = ModuleInfo0 }
 		;
 			{ Cmp = tighter },
-			{ module_info_incr_errors(ModuleInfo0, ModuleInfo1) },
+			{ module_info_incr_errors(ModuleInfo0, ModuleInfo) },
 			{ Message = "  error: determinism declaration not satisfied.\n" },
 			report_determinism_problem(PredId,
-				ProcId, ModuleInfo1, Message,
+				ProcId, ModuleInfo, Message,
 				DeclaredDetism, InferredDetism),
 			{ proc_info_goal(ProcInfo, Goal) },
 			globals__io_get_globals(Globals),
-			{ det_info_init(ModuleInfo1, PredId, ProcId, Globals,
+			{ det_info_init(ModuleInfo, PredId, ProcId, Globals,
 				DetInfo) },
 			det_diagnose_goal(Goal, DeclaredDetism, [], DetInfo, _)
 			% XXX with the right verbosity options, we want to
 			% call report_determinism_problem only if diagnose
 			% returns false, i.e. it didn't print a message.
 		)
-	),
+	).
+
+:- pred check_if_main_can_fail(pred_id, proc_id, pred_info, proc_info,
+		module_info, module_info, io__state, io__state).
+:- mode check_if_main_can_fail(in, in, in, in, in, out, di, uo) is det.
+
+check_if_main_can_fail(_PredId, _ProcId, PredInfo, ProcInfo,
+		ModuleInfo0, ModuleInfo) -->
+	{ proc_info_declared_determinism(ProcInfo, MaybeDetism) },
+	{ proc_info_inferred_determinism(ProcInfo, InferredDetism) },
 	% check that `main/2' cannot fail
 	( 
 		{ pred_info_name(PredInfo, "main") },
@@ -163,11 +190,19 @@
 			% that would probably just confuse people.
 		io__write_string(
 			"Error: main/2 must be `det' or `cc_multi'.\n"),
-		{ module_info_incr_errors(ModuleInfo1,
-			ModuleInfo2) }
+		{ module_info_incr_errors(ModuleInfo0, ModuleInfo) }
 	;
-		{ ModuleInfo2 = ModuleInfo1 }
-	),
+		{ ModuleInfo = ModuleInfo0 }
+	).
+
+:- pred check_for_multisoln_func(pred_id, proc_id, pred_info, proc_info,
+		module_info, module_info, io__state, io__state).
+:- mode check_for_multisoln_func(in, in, in, in, in, out, di, uo) is det.
+
+check_for_multisoln_func(_PredId, _ProcId, PredInfo, ProcInfo,
+		ModuleInfo0, ModuleInfo) -->
+	{ proc_info_inferred_determinism(ProcInfo, InferredDetism) },
+
 	% Functions can only have more than one solution if it is a
 	% non-standard mode.  Otherwise, they would not be referentially
 	% transparent.  (Nondeterministic "functions" like C's `rand()'
@@ -185,7 +220,7 @@
 			FuncArgModes, _FuncResultMode) },
 		{ \+ (
 			list__member(FuncArgMode, FuncArgModes),
-			\+ mode_is_fully_input(ModuleInfo2, FuncArgMode)
+			\+ mode_is_fully_input(ModuleInfo0, FuncArgMode)
 		  )
 	 	} 
 	->
@@ -193,7 +228,9 @@
 		{ pred_info_name(PredInfo, PredName) },
 		{ proc_info_context(ProcInfo, FuncContext) },
 		prog_out__write_context(FuncContext),
-		io__write_string("Error: invalid determinism for `"),
+		io__write_string("Error: invalid determinism for function\n"),
+		prog_out__write_context(FuncContext),
+		io__write_string("  `"),
 		report_pred_name_mode(function, PredName, PredArgModes),
 		io__write_string("':\n"),
 		prog_out__write_context(FuncContext),
@@ -215,13 +252,10 @@
 		;
 			[]
 		),
-		{ module_info_incr_errors(ModuleInfo2,
-			ModuleInfo3) }
-		
+		{ module_info_incr_errors(ModuleInfo0, ModuleInfo) }
 	;
-		{ ModuleInfo3 = ModuleInfo2 }
-	),
-	global_checking_pass(Rest, ModuleInfo3, ModuleInfo).
+		{ ModuleInfo = ModuleInfo0 }
+	).
 
 det_check_lambda(DeclaredDetism, InferredDetism, Goal, GoalInfo, DetInfo,
 		Msgs) :-
@@ -387,7 +421,7 @@
 			{ det_lookup_var_type(ModuleInfo, ProcInfo, Var,
 				TypeDefn) },
 			{ hlds_data__get_type_defn_body(TypeDefn, TypeBody) },
-			{ TypeBody = du_type(_, ConsTable, _) }
+			{ TypeBody = du_type(_, ConsTable, _, _) }
 		->
 			{ map__keys(ConsTable, ConsIds) },
 			{ det_diagnose_missing_consids(ConsIds, Cases,
@@ -413,110 +447,25 @@
 det_diagnose_goal_2(call(PredId, ModeId, _, _, CallContext, _), GoalInfo,
 		Desired, Actual, _, DetInfo, yes) -->
 	{ goal_info_get_context(GoalInfo, Context) },
-	{ determinism_components(Desired, DesiredCanFail, DesiredSolns) },
-	{ determinism_components(Actual, ActualCanFail, ActualSolns) },
-	{ compare_canfails(DesiredCanFail, ActualCanFail, CmpCanFail) },
-	( { CmpCanFail = tighter } ->
-		det_report_call_context(Context, CallContext, DetInfo,
-			PredId, ModeId),
-		io__write_string("can fail.\n"),
-		{ Diagnosed1 = yes }
-	;
-		{ Diagnosed1 = no }
-	),
-	{ compare_solncounts(DesiredSolns, ActualSolns, CmpSolns) },
-	( { CmpSolns = tighter } ->
-		det_report_call_context(Context, CallContext, DetInfo,
-			PredId, ModeId),
-		io__write_string("can succeed"),
-		( { DesiredSolns = at_most_one } ->
-			io__write_string(" more than once.\n")
-		;
-			io__write_string(".\n")
-		),
-		{ Diagnosed2 = yes }
-	;
-		{ Diagnosed2 = no }
-	),
-	{ bool__or(Diagnosed1, Diagnosed2, Diagnosed) },
-	(
-		{ Diagnosed = yes }
-	;
-		{ Diagnosed = no },
+	det_diagnose_atomic_goal(Desired, Actual,
 		det_report_call_context(Context, CallContext, DetInfo,
 			PredId, ModeId),
-		io__write_string("has unknown determinism problem;\n"),
-		prog_out__write_context(Context),
-		io__write_string("  desired determinism is "),
-		hlds_out__write_determinism(Desired),
-		io__write_string(", while actual determinism is "),
-		hlds_out__write_determinism(Actual),
-		io__write_string(".\n")
-	).
+		Context).
 
 det_diagnose_goal_2(higher_order_call(_, _, _, _, _), GoalInfo,
-		Desired, Actual, _, _MiscInfo, yes) -->
+		Desired, Actual, _, _DetInfo, yes) -->
 	{ goal_info_get_context(GoalInfo, Context) },
-	{ determinism_components(Desired, DesiredCanFail, DesiredSolns) },
-	{ determinism_components(Actual, ActualCanFail, ActualSolns) },
-	{ compare_canfails(DesiredCanFail, ActualCanFail, CmpCanFail) },
-	( { CmpCanFail = tighter } ->
-		prog_out__write_context(Context),
-		io__write_string("  Higher-order predicate call can fail.\n"),
-		{ Diagnosed1 = yes }
-	;
-		{ Diagnosed1 = no }
-	),
-	{ compare_solncounts(DesiredSolns, ActualSolns, CmpSolns) },
-	( { CmpSolns = tighter } ->
-		prog_out__write_context(Context),
-		io__write_string("  Higher-order predicate call can succeed"),
-		( { DesiredSolns = at_most_one } ->
-			io__write_string(" more than once.\n")
-		;
-			io__write_string(".\n")
-		),
-		{ Diagnosed2 = yes }
-	;
-		{ Diagnosed2 = no }
-	),
-	{ bool__or(Diagnosed1, Diagnosed2, Diagnosed) },
-	(
-		{ Diagnosed = yes }
-	;
-		{ Diagnosed = no },
-		prog_out__write_context(Context),
-		io__write_string("  Higher-order predicate call has unknown determinism problem;\n"),
-		prog_out__write_context(Context),
-		io__write_string("  desired determinism is "),
-		hlds_out__write_determinism(Desired),
-		io__write_string(", while actual determinism is "),
-		hlds_out__write_determinism(Actual),
-		io__write_string(".\n")
-	).
+	prog_out__write_context(Context),
+	det_diagnose_atomic_goal(Desired, Actual,
+		report_higher_order_call_context(Context), Context).
 
 det_diagnose_goal_2(unify(LT, RT, _, _, UnifyContext), GoalInfo,
 		Desired, Actual, _, DetInfo, yes) -->
 	{ goal_info_get_context(GoalInfo, Context) },
-	{ determinism_components(Desired, DesiredCanFail, _DesiredSolns) },
-	{ determinism_components(Actual, ActualCanFail, _ActualSolns) },
 	{ First = yes, Last = yes },
-	det_report_unify_context(First, Last, Context, UnifyContext, DetInfo,
-				LT, RT),
-	(
-		{ DesiredCanFail = cannot_fail },
-		{ ActualCanFail = can_fail }
-	->
-		io__write_string(" can fail.\n")
-	;
-		io__write_string(" has unknown determinism problem;\n"),
-		prog_out__write_context(Context),
-		io__write_string("  desired determinism is "),
-		hlds_out__write_determinism(Desired),
-		io__write_string(", while actual determinism is "),
-		hlds_out__write_determinism(Actual),
-		io__write_string(".\n")
-	).
+	det_diagnose_atomic_goal(Desired, Actual,
+		det_report_unify_context(First, Last, Context, UnifyContext,
+			DetInfo, LT, RT), Context).
 
 det_diagnose_goal_2(if_then_else(_Vars, Cond, Then, Else, _), _GoalInfo,
 		Desired, _Actual, SwitchContext, DetInfo, Diagnosed) -->
@@ -594,6 +543,59 @@
 
 %-----------------------------------------------------------------------------%
 
+:- pred report_higher_order_call_context(term__context::in,
+		io__state::di, io__state::uo) is det.
+report_higher_order_call_context(Context) -->
+	prog_out__write_context(Context),
+	io__write_string("  Higher-order call").
+
+%-----------------------------------------------------------------------------%
+
+:- pred det_diagnose_atomic_goal(determinism, determinism, 
+		pred(io__state, io__state), term__context,
+		io__state, io__state).
+:- mode det_diagnose_atomic_goal(in, in, pred(di, uo) is det, in,
+		di, uo) is det.
+
+det_diagnose_atomic_goal(Desired, Actual, WriteContext, Context) -->
+	{ determinism_components(Desired, DesiredCanFail, DesiredSolns) },
+	{ determinism_components(Actual, ActualCanFail, ActualSolns) },
+	{ compare_canfails(DesiredCanFail, ActualCanFail, CmpCanFail) },
+	( { CmpCanFail = tighter } ->
+		call(WriteContext),
+		io__write_string(" can fail.\n"),
+		{ Diagnosed1 = yes }
+	;
+		{ Diagnosed1 = no }
+	),
+	{ compare_solncounts(DesiredSolns, ActualSolns, CmpSolns) },
+	( { CmpSolns = tighter } ->
+		call(WriteContext),
+		io__write_string(" can succeed"),
+		( { DesiredSolns = at_most_one } ->
+			io__write_string(" more than once.\n")
+		;
+			io__write_string(".\n")
+		),
+		{ Diagnosed2 = yes }
+	;
+		{ Diagnosed2 = no }
+	),
+	{ bool__or(Diagnosed1, Diagnosed2, Diagnosed) },
+	(
+		{ Diagnosed = yes }
+	;
+		{ Diagnosed = no },
+		call(WriteContext),
+		io__write_string(" has unknown determinism problem;\n"),
+		prog_out__write_context(Context),
+		io__write_string("  desired determinism is "),
+		hlds_out__write_determinism(Desired),
+		io__write_string(", while actual determinism is "),
+		hlds_out__write_determinism(Actual),
+		io__write_string(".\n")
+	).
+
 :- pred det_diagnose_conj(list(hlds_goal), determinism,
 	list(switch_context), det_info, bool, io__state, io__state).
 :- mode det_diagnose_conj(in, in, in, in, out, di, uo) is det.
@@ -727,15 +729,14 @@
 					call_unify_context(LT, RT, UC)) },
 			{ First = yes, Last = yes },
 			det_report_unify_context(First, Last,
-				Context, UC, DetInfo, LT, RT),
-			io__write_string(" ")
+				Context, UC, DetInfo, LT, RT)
 		;
 			% this shouldn't happen; every call to __Unify__
 			% should have a unify_context
 			{ CallUnifyContext = no },
 			prog_out__write_context(Context),
 			io__write_string(
-	"  Some weird unification (or explicit call to `__Unify__'?) ")
+	"  Some weird unification (or explicit call to `__Unify__'?)")
 		)
 	;
 		(
@@ -754,7 +755,7 @@
 		prog_out__write_context(Context),
 		io__write_string("  call to `"),
 		report_pred_name_mode(PredOrFunc, PredName, ArgModes),
-		io__write_string("' ")
+		io__write_string("'")
 	).
 
 %-----------------------------------------------------------------------------%
@@ -883,6 +884,8 @@
 det_msg_get_type(warn_obsolete(_, _), warning).
 det_msg_get_type(warn_infinite_recursion(_), warning).
 det_msg_get_type(duplicate_call(_, _, _), warning).
+det_msg_get_type(cc_unify_can_fail(_, _, _, _, _), error).
+det_msg_get_type(cc_unify_in_wrong_context(_, _, _, _, _), error).
 det_msg_get_type(cc_pred_in_wrong_context(_, _, _, _), error).
 det_msg_get_type(higher_order_cc_pred_in_wrong_context(_, _), error).
 det_msg_get_type(error_in_lambda(_, _, _, _, _, _), error).
@@ -967,6 +970,101 @@
 	io__write_string("Here is the previous "),
 	det_report_seen_call_id(SeenCall, ModuleInfo),
 	io__write_string(".\n").
+det_report_msg(cc_unify_can_fail(GoalInfo, Var, Type, VarSet, GoalContext),
+		_ModuleInfo) -->
+	{ goal_info_get_context(GoalInfo, Context) },
+	{ First0 = yes },
+	( { GoalContext = switch },
+		prog_out__write_context(Context),
+		io__write_string("In switch on variable `"),
+		mercury_output_var(Var, VarSet, no),
+		io__write_string("':\n"),
+		{ First = no }
+	; { GoalContext = unify(UnifyContext) },
+		hlds_out__write_unify_context(First0, UnifyContext, Context,
+			First)
+	),
+	prog_out__write_context(Context),
+	( { First = yes } ->
+		io__write_string("Error: ")
+	;
+		io__write_string("  error: ")
+	),
+	io__write_string("unification for non-canonical type\n"),
+	prog_out__write_context(Context),
+	io__write_string("  `"),
+	( { type_to_type_id(Type, TypeId, _TypeArgs) } ->
+		hlds_out__write_type_id(TypeId)
+	;
+		{ error("det_report_message: type_to_type_id failed") }
+	),
+	io__write_string("'\n"),
+	prog_out__write_context(Context),
+	io__write_string("  is not guaranteed to succeed.\n"),
+	globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+	( { VerboseErrors = yes } ->
+		io__write_strings([
+"	Since the type has a user-defined equality predicate, I must\n",
+"	presume that there is more than one possible concrete\n",
+"	representation for each abstract value of this type.  The success\n",
+"	of this unification might depend on the choice of concrete\n",
+"	representation.  Figuring out whether there is a solution to\n",
+"	this unification would require backtracking over all possible\n",
+"	representations, but I'm not going to do that implicitly.\n",
+"	(If that's really what you want, you must do it explicitly.)\n"
+		])
+	;
+		[]
+	),
+	io__set_exit_status(1).
+det_report_msg(cc_unify_in_wrong_context(GoalInfo, Var, Type, VarSet,
+		GoalContext), _ModuleInfo) -->
+	{ goal_info_get_context(GoalInfo, Context) },
+	{ First0 = yes },
+	( { GoalContext = switch },
+		prog_out__write_context(Context),
+		io__write_string("In switch on variable `"),
+		mercury_output_var(Var, VarSet, no),
+		io__write_string("':\n"),
+		{ First = no }
+	; { GoalContext = unify(UnifyContext) },
+		hlds_out__write_unify_context(First0, UnifyContext, Context,
+			First)
+	),
+	prog_out__write_context(Context),
+	( { First = yes } ->
+		io__write_string("Error: ")
+	;
+		io__write_string("  error: ")
+	),
+	io__write_string("unification for non-canonical type\n"),
+	prog_out__write_context(Context),
+	io__write_string("  `"),
+	( { type_to_type_id(Type, TypeId, _TypeArgs) } ->
+		hlds_out__write_type_id(TypeId)
+	;
+		{ error("det_report_message: type_to_type_id failed") }
+	),
+	io__write_string("'\n"),
+	prog_out__write_context(Context),
+	io__write_string(
+		"  occurs in a context which requires all solutions.\n"),
+	globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
+	( { VerboseErrors = yes } ->
+		io__write_strings([
+"	Since the type has a user-defined equality predicate, I must\n",
+"	presume that there is more than one possible concrete\n",
+"	representation for each abstract value of this type.  The results\n",
+"	of this unification might depend on the choice of concrete\n",
+"	representation.  Finding all possible solutions to this\n",
+"	unification would require backtracking over all possible\n",
+"	representations, but I'm not going to do that implicitly.\n",
+"	(If that's really what you want, you must do it explicitly.)\n"
+		])
+	;
+		[]
+	),
+	io__set_exit_status(1).
 det_report_msg(cc_pred_in_wrong_context(GoalInfo, Detism, PredId, _ModeId),
 		ModuleInfo) -->
 	{ goal_info_get_context(GoalInfo, Context) },
Index: compiler/equiv_type.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/equiv_type.m,v
retrieving revision 1.7
diff -u -r1.7 equiv_type.m
--- equiv_type.m	1997/06/29 23:10:31	1.7
+++ equiv_type.m	1997/06/30 06:49:49
@@ -143,8 +143,9 @@
 		EqvMap, uu_type(TName, TArgs, TBody), VarSet, no) :-
 	equiv_type__replace_in_uu(TBody0, VarSet0, EqvMap, TBody, VarSet).
 
-equiv_type__replace_in_type_defn(du_type(TName, TArgs, TBody0), VarSet0,
-			EqvMap, du_type(TName, TArgs, TBody), VarSet, no) :-
+equiv_type__replace_in_type_defn(du_type(TName, TArgs, TBody0, EqPred), VarSet0,
+			EqvMap, du_type(TName, TArgs, TBody, EqPred), VarSet,
+			no) :-
 	equiv_type__replace_in_du(TBody0, VarSet0, EqvMap, TBody, VarSet).
 
 %-----------------------------------------------------------------------------%
Index: compiler/hlds_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_data.m,v
retrieving revision 1.13
diff -u -r1.13 hlds_data.m
--- hlds_data.m	1997/05/20 01:51:49	1.13
+++ hlds_data.m	1997/07/16 19:44:52
@@ -187,7 +187,8 @@
 	--->	du_type(
 			list(constructor), 	% the ctors for this type
 			cons_tag_values,	% their tag values
-			bool		% is this type an enumeration?
+			bool,		% is this type an enumeration?
+			maybe(sym_name) % user-defined equality pred
 		)
 	;	uu_type(list(type))	% not yet implemented!
 	;	eqv_type(type)
Index: compiler/hlds_out.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/hlds_out.m,v
retrieving revision 1.167
diff -u -r1.167 hlds_out.m
--- hlds_out.m	1997/07/09 06:16:33	1.167
+++ hlds_out.m	1997/07/16 19:56:43
@@ -1685,9 +1685,17 @@
 	io__state, io__state).
 :- mode hlds_out__write_type_body(in, in, in, di, uo) is det.
 
-hlds_out__write_type_body(Indent, Tvarset, du_type(Ctors, _Tags, _Enum)) -->
+hlds_out__write_type_body(Indent, Tvarset, du_type(Ctors, _Tags, _Enum,
+		MaybeEqualityPred)) -->
 	io__write_string(" --->\n"),
-	hlds_out__write_constructors(Indent, Tvarset, Ctors).
+	hlds_out__write_constructors(Indent, Tvarset, Ctors),
+	( { MaybeEqualityPred = yes(PredName) } ->
+		io__write_string("\n\twhere equality is "),
+		prog_out__write_sym_name(PredName)
+	;
+		[]
+	),
+	io__write_string(".\n").
 hlds_out__write_type_body(_Indent, _Tvarset, uu_type(_)) -->
 	{ error("hlds_out__write_type_body: undiscriminated union found") }.
 hlds_out__write_type_body(_Indent, Tvarset, eqv_type(Type)) -->
@@ -1706,8 +1714,7 @@
 hlds_out__write_constructors(Indent, Tvarset, [C]) -->
 	hlds_out__write_indent(Indent),
 	io__write_char('\t'),
-	hlds_out__write_constructor(Tvarset, C),
-	io__write_string(".\n").
+	hlds_out__write_constructor(Tvarset, C).
 hlds_out__write_constructors(Indent, Tvarset, [C | Cs]) -->
 	{ Cs = [_ | _] },
 	hlds_out__write_indent(Indent),
Index: compiler/intermod.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/intermod.m,v
retrieving revision 1.27
diff -u -r1.27 intermod.m
--- intermod.m	1997/06/29 23:10:49	1.27
+++ intermod.m	1997/07/16 19:57:31
@@ -774,8 +774,9 @@
 	{ hlds_data__get_type_defn_body(TypeDefn, Body) },
 	{ hlds_data__get_type_defn_context(TypeDefn, Context) },
 	(
-		{ Body = du_type(Ctors, _, _) },
-		mercury_output_type_defn(VarSet, du_type(Name, Args, Ctors),
+		{ Body = du_type(Ctors, _, _, MaybeEqualityPred) },
+		mercury_output_type_defn(VarSet,
+				du_type(Name, Args, Ctors, MaybeEqualityPred),
 				Context)
 	;
 		{ Body = uu_type(_) },
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/make_hlds.m,v
retrieving revision 1.234
diff -u -r1.234 make_hlds.m
--- make_hlds.m	1997/06/29 23:10:57	1.234
+++ make_hlds.m	1997/07/16 19:48:53
@@ -788,7 +788,7 @@
 	;
 		{ map__set(Types0, TypeId, T, Types) },
 		(
-			{ Body = du_type(ConsList, _, _) }
+			{ Body = du_type(ConsList, _, _, _) }
 		->
 			{ module_info_ctors(Module0, Ctors0) },
 			ctors_add(ConsList, TypeId, NeedQual, 
@@ -907,8 +907,9 @@
 			sym_name, list(type_param), hlds_type_body).
 :- mode convert_type_defn(in, in, out, out, out) is det.
 
-convert_type_defn(du_type(Name, Args, Body), Globals, Name, Args,
-		du_type(Body, CtorTags, IsEnum)) :-
+convert_type_defn(du_type(Name, Args, Body, EqualityPred),
+		Globals, Name, Args,
+		du_type(Body, CtorTags, IsEnum, EqualityPred)) :-
 	assign_constructor_tags(Body, Globals, CtorTags, IsEnum).
 convert_type_defn(uu_type(Name, Args, Body), _, Name, Args, uu_type(Body)).
 convert_type_defn(eqv_type(Name, Args, Body), _, Name, Args, eqv_type(Body)).
@@ -1200,7 +1201,7 @@
 		PredInfo1 = PredInfo0
 	),
 	unify_proc__generate_clause_info(SpecialPredId, Type, TypeBody,
-				Module1, ClausesInfo),
+				Context, Module1, ClausesInfo),
 	pred_info_set_clauses_info(PredInfo1, ClausesInfo, PredInfo),
 	map__det_update(Preds0, PredId, PredInfo, Preds),
 	module_info_set_preds(Module1, Preds, Module).
@@ -2528,7 +2529,7 @@
 		;
 			% initialize some fields to junk
 			invalid_pred_id(PredId),
-			hlds_pred__initial_proc_id(ModeId),
+			invalid_proc_id(ModeId),
 			MaybeUnifyContext = no,
 			Call = call(PredId, ModeId, HeadVars, not_builtin,
 					MaybeUnifyContext, Name)
Index: compiler/mercury_to_goedel.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mercury_to_goedel.m,v
retrieving revision 1.58
diff -u -r1.58 mercury_to_goedel.m
--- mercury_to_goedel.m	1997/05/28 07:39:10	1.58
+++ mercury_to_goedel.m	1997/07/16 17:40:22
@@ -234,8 +234,17 @@
 	io__write_string("equivalence type unexpected.\n"),
 	io__set_output_stream(OldStream, _).
 
-goedel_output_type_defn_2(du_type(Name, Args, Ctors), VarSet, Context) -->
+goedel_output_type_defn_2(du_type(Name, Args, Ctors, EqualityPred),
+		VarSet, Context) -->
 	{ unqualify_name(Name, Name2) },
+	( { EqualityPred \= no } ->
+		io__write_string("% WARNING: ignored user-defined equality "),
+		io__write_string(" for type `"),
+		io__write_string(Name2),
+		io__write_string("'\n")
+	;
+		[]
+	),
 	{ convert_functor_name(Name2, Name3) },
 	( { option_handle_functor_overloading(Name2) } ->
 		{ string__append("Type__", Name3, TypeModule) },
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.108
diff -u -r1.108 mercury_to_mercury.m
--- mercury_to_mercury.m	1997/06/29 23:11:01	1.108
+++ mercury_to_mercury.m	1997/06/30 07:08:40
@@ -912,12 +912,19 @@
 	mercury_output_term(Body, VarSet, no),
 	io__write_string(".\n").
 
-mercury_output_type_defn_2(du_type(Name, Args, Ctors), VarSet, Context) -->
+mercury_output_type_defn_2(du_type(Name, Args, Ctors, MaybeEqualityPred),
+		VarSet, Context) -->
 	io__write_string(":- type "),
 	{ construct_qualified_term(Name, Args, Context, TypeTerm) },
 	mercury_output_term(TypeTerm, VarSet, no),
 	io__write_string("\n\t--->\t"),
 	mercury_output_ctors(Ctors, VarSet),
+	( { MaybeEqualityPred = yes(EqualityPredName) } ->
+		io__write_string("\n\twhere equality is "),
+		mercury_output_bracketed_sym_name(EqualityPredName)
+	;
+		[]
+	),
 	io__write_string(".\n").
 
 :- pred mercury_output_ctors(list(constructor), varset,
Index: compiler/mode_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/mode_util.m,v
retrieving revision 1.94
diff -u -r1.94 mode_util.m
--- mode_util.m	1997/06/16 08:58:01	1.94
+++ mode_util.m	1997/06/30 06:49:50
@@ -1336,7 +1336,7 @@
 		map__search(TypeTable, TypeId, TypeDefn),
 		hlds_data__get_type_defn_tparams(TypeDefn, TypeParams0),
 		hlds_data__get_type_defn_body(TypeDefn, TypeBody),
-		TypeBody = du_type(Constructors, _, _)
+		TypeBody = du_type(Constructors, _, _, _)
 	->
 		term__term_list_to_var_list(TypeParams0, TypeParams),
 		map__from_corresponding_lists(TypeParams, TypeArgs, ArgSubst),
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.17
diff -u -r1.17 modecheck_unify.m
--- modecheck_unify.m	1997/07/02 08:06:17	1.17
+++ modecheck_unify.m	1997/07/16 15:30:03
@@ -836,8 +836,9 @@
 			;
 				type_to_type_id(Type, TypeId, _)
 			->
-				unify_proc__request_unify(TypeId - UniMode, Det,
-					ModuleInfo0, ModuleInfo),
+				mode_info_get_context(ModeInfo0, Context),
+				unify_proc__request_unify(TypeId - UniMode,
+					Det, Context, ModuleInfo0, ModuleInfo),
 				mode_info_set_module_info(ModeInfo0, ModuleInfo,
 					ModeInfo)
 			;
Index: compiler/module_qual.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/module_qual.m,v
retrieving revision 1.19
diff -u -r1.19 module_qual.m
--- module_qual.m	1997/06/29 23:11:11	1.19
+++ module_qual.m	1997/07/16 18:39:32
@@ -143,7 +143,7 @@
 :- pred add_type_defn(type_defn::in, mq_info::in, mq_info::out) is det.
 
 add_type_defn(TypeDefn, Info0, Info) :-
-	(	TypeDefn = du_type(SymName, Params, _)
+	(	TypeDefn = du_type(SymName, Params, _, _EqualityPred)
 	;	TypeDefn = uu_type(SymName, Params, _)
 	;	TypeDefn = eqv_type(SymName, Params, _)
 	;	TypeDefn = abstract_type(SymName, Params)
@@ -319,12 +319,19 @@
 :- pred qualify_type_defn(type_defn::in, type_defn::out, mq_info::in,
 	mq_info::out, term__context::in, io__state::di, io__state::uo) is det.
 
-qualify_type_defn(du_type(SymName, Params, Ctors0),
-		du_type(SymName, Params, Ctors), Info0, Info, Context) -->
+qualify_type_defn(du_type(SymName, Params, Ctors0, MaybeEqualityPred0),
+		du_type(SymName, Params, Ctors, MaybeEqualityPred),
+		Info0, Info, Context) -->
 	{ list__length(Params, Arity) },
 	{ mq_info_set_error_context(Info0, type(SymName - Arity) - Context,
 								Info1) },
-	qualify_constructors(Ctors0, Ctors, Info1, Info).
+	qualify_constructors(Ctors0, Ctors, Info1, Info),
+
+	% User-defined equality pred names will be converted into
+	% predicate calls and then module-qualified after type analysis
+	% (during mode analysis).  That way they get full type overloading
+	% resolution, etc.  Thus we don't module-qualify them here.
+	{ MaybeEqualityPred = MaybeEqualityPred0 }.
 
 qualify_type_defn(uu_type(SymName, Params, Types0),
 		uu_type(SymName, Params, Types), Info0, Info, Context) -->
Index: compiler/modules.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/modules.m,v
retrieving revision 1.36
diff -u -r1.36 modules.m
--- modules.m	1997/07/15 09:12:01	1.36
+++ modules.m	1997/07/15 09:12:10
@@ -1564,7 +1564,7 @@
 :- pred make_abstract_type_defn(item, item).
 :- mode make_abstract_type_defn(in, out) is semidet.
 
-make_abstract_type_defn(type_defn(VarSet, du_type(Name, Args, _Ctors), Cond),
+make_abstract_type_defn(type_defn(VarSet, du_type(Name, Args, _, _), Cond),
 			type_defn(VarSet, abstract_type(Name, Args), Cond)).
 make_abstract_type_defn(type_defn(VarSet, abstract_type(Name, Args), Cond),
 			type_defn(VarSet, abstract_type(Name, Args), Cond)).
Index: compiler/prog_data.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_data.m,v
retrieving revision 1.21
diff -u -r1.21 prog_data.m
--- prog_data.m	1997/07/07 12:01:36	1.21
+++ prog_data.m	1997/07/12 17:03:56
@@ -184,7 +184,9 @@
 % type_defn/3 define above
 
 :- type type_defn	--->	du_type(sym_name, list(type_param),
-						list(constructor))
+					list(constructor),
+					maybe(equality_pred)
+				)
 			;	uu_type(sym_name, list(type_param), list(type))
 			;	eqv_type(sym_name, list(type_param), type)
 			;	abstract_type(sym_name, list(type_param)).
@@ -192,6 +194,11 @@
 :- type constructor	==	pair(sym_name, list(constructor_arg)).
 
 :- type constructor_arg	==	pair(string, type).
+
+	% An equality_pred specifies the name of a user-defined predicate
+	% used for equality on a type.  See the chapter on them in the
+	% Mercury Language Reference Manual.
+:- type equality_pred	==	sym_name.
 
 	% probably type parameters should be variables not terms.
 :- type type_param	==	term.
Index: compiler/prog_io.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/prog_io.m,v
retrieving revision 1.157
diff -u -r1.157 prog_io.m
--- prog_io.m	1997/07/08 05:49:44	1.157
+++ prog_io.m	1997/07/12 17:03:57
@@ -709,15 +709,17 @@
 	% to the condition for that declaration (if any), and Result to
 	% a representation of the declaration.
 
-:- pred parse_type_decl_type(string, string, list(term),
-				condition, maybe1(type_defn)).
+:- pred parse_type_decl_type(string, string, list(term), condition,
+				maybe1(type_defn)).
 :- mode parse_type_decl_type(in, in, in, out, out) is semidet.
 
 :- parse_type_decl_type(_, [A|B], _, _, _) when A and B.
 
 parse_type_decl_type(ModuleName, "--->", [H, B], Condition, R) :-
-	get_condition(B, Body, Condition),
-	process_du_type(ModuleName, H, Body, R).
+	/* get_condition(...), */
+	Condition = true,
+	get_maybe_equality_pred(B, Body, EqualityPred),
+	process_du_type(ModuleName, H, Body, EqualityPred, R).
 
 parse_type_decl_type(ModuleName, "=", [H, B], Condition, R) :-
 	get_condition(B, Body, Condition),
@@ -784,6 +786,42 @@
 
 %-----------------------------------------------------------------------------%
 
+	% get_maybe_equality_pred(Body0, Body, MaybeEqualPred):
+	%	Checks if `Body0' is a term of the form
+	%		`<body> where equality is <symname>'
+	%	If so, returns the `<body>' in Body and the <symname> in
+	%	MaybeEqualPred.  If not, returns Body = Body0 
+	%	and `no' in MaybeEqualPred.
+
+:- pred get_maybe_equality_pred(term, term, maybe1(maybe(sym_name))).
+:- mode get_maybe_equality_pred(in, out, out) is det.
+
+get_maybe_equality_pred(B, Body, MaybeEqualityPred) :-
+	( 
+		B = term__functor(term__atom("where"), Args, _Context1),
+		Args = [Body1, Equality_Is_PredName]
+	->
+		Body = Body1,
+		( 
+			Equality_Is_PredName = term__functor(term__atom("is"),
+				[Equality, PredName], _),
+			Equality = term__functor(term__atom("equality"), [], _)
+		->
+			parse_symbol_name(PredName, MaybeEqualityPred0),
+			process_maybe1(make_yes, MaybeEqualityPred0,
+				MaybeEqualityPred)
+		;
+			MaybeEqualityPred = error("syntax error after `where'",
+				Body)
+		)
+	;
+		Body = B,
+		MaybeEqualityPred = ok(no)
+	).
+
+:- pred make_yes(T::in, maybe(T)::out) is det.
+make_yes(T, yes(T)).
+
 	% get_determinism(Term0, Term, Determinism) binds Determinism
 	% to a representation of the determinism condition of Term0, if any,
 	% and binds Term to the other part of Term0. If Term0 does not
@@ -823,6 +861,20 @@
 
 :- pred get_condition(term, term, condition).
 :- mode get_condition(in, out, out) is det.
+
+get_condition(Body, Body, true).
+
+/********
+% NU-Prolog supported type declarations of the form
+%	:- pred p(T) where p(X) : sorted(X).
+% or
+%	:- type sorted_list(T) = list(T) where X : sorted(X).
+%	:- pred p(sorted_list(T).
+% There is some code here to support that sort of thing, but
+% probably we would now need to use a different syntax, since
+% Mercury now uses `where' for different purposes (e.g. specifying
+% user-defined equality predicates; also for type classes, eventually...)
+%
 get_condition(B, Body, Condition) :-
 	( 
 		B = term__functor(term__atom("where"), [Body1, Condition1],
@@ -834,6 +886,7 @@
 		Body = B,
 		Condition = true
 	).
+********/
 
 %-----------------------------------------------------------------------------%
 
@@ -871,21 +924,31 @@
 	% binds Result to a representation of the type information about the
 	% TypeHead.
 	% This is for "Head ---> Body" (constructor) definitions.
-:- pred process_du_type(string, term, term, maybe1(type_defn)).
-:- mode process_du_type(in, in, in, out) is det.
-process_du_type(ModuleName, Head, Body, Result) :-
+:- pred process_du_type(string, term, term, maybe1(maybe(equality_pred)),
+			maybe1(type_defn)).
+:- mode process_du_type(in, in, in, in, out) is det.
+process_du_type(ModuleName, Head, Body, EqualityPred, Result) :-
 	check_for_errors(ModuleName, Head, Body, Result0),
-	process_du_type_2(ModuleName, Result0, Body, Result).
+	process_du_type_2(ModuleName, Result0, Body, EqualityPred, Result).
 
-:- pred process_du_type_2(string, maybe_functor, term, maybe1(type_defn)).
-:- mode process_du_type_2(in, in, in, out) is det.
-process_du_type_2(_, error(Error, Term), _, error(Error, Term)).
-process_du_type_2(ModuleName, ok(Functor, Args), Body, Result) :-
+:- pred process_du_type_2(string, maybe_functor, term,
+			maybe1(maybe(equality_pred)), maybe1(type_defn)).
+:- mode process_du_type_2(in, in, in, in, out) is det.
+process_du_type_2(_, error(Error, Term), _, _, error(Error, Term)).
+process_du_type_2(ModuleName, ok(Functor, Args), Body, MaybeEqualityPred,
+		Result) :-
 	% check that body is a disjunction of constructors
 	( %%% some [Constrs] 
 		convert_constructors(ModuleName, Body, Constrs)
 	->
-		Result = ok(du_type(Functor, Args, Constrs))
+		(
+			MaybeEqualityPred = ok(EqualityPred),
+			Result = ok(du_type(Functor, Args, Constrs,
+						EqualityPred))
+		;
+			MaybeEqualityPred = error(Error, Term),
+			Result = error(Error, Term)
+		)
 	;
 		Result = error("invalid RHS of type definition", Body)
 	).
Index: compiler/switch_detection.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/switch_detection.m,v
retrieving revision 1.72
diff -u -r1.72 switch_detection.m
--- switch_detection.m	1997/07/08 05:46:01	1.72
+++ switch_detection.m	1997/07/12 17:03:59
@@ -522,7 +522,7 @@
 	module_info_types(ModuleInfo, TypeTable),
 	map__search(TypeTable, TypeId, TypeDefn),
 	hlds_data__get_type_defn_body(TypeDefn, TypeBody),
-	TypeBody = du_type(_, ConsTable, _),
+	TypeBody = du_type(_, ConsTable, _, _),
 	map__keys(ConsTable, Constructors),
 	list__same_length(CasesList, Constructors).
 
Index: compiler/tag_switch.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/tag_switch.m,v
retrieving revision 1.37
diff -u -r1.37 tag_switch.m
--- tag_switch.m	1997/06/29 23:11:33	1.37
+++ tag_switch.m	1997/06/30 06:49:50
@@ -818,7 +818,7 @@
 	module_info_types(ModuleInfo, TypeTable),
 	map__lookup(TypeTable, TypeId, TypeDefn),
 	hlds_data__get_type_defn_body(TypeDefn, Body),
-	( Body = du_type(_, ConsTable, _) ->
+	( Body = du_type(_, ConsTable, _, _) ->
 		map__to_assoc_list(ConsTable, ConsList),
 		tag_switch__cons_list_to_tag_list(ConsList, TagList)
 	;
Index: compiler/type_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/type_util.m,v
retrieving revision 1.43
diff -u -r1.43 type_util.m
--- type_util.m	1997/06/03 06:22:40	1.43
+++ type_util.m	1997/06/30 06:51:48
@@ -252,7 +252,7 @@
 	module_info_types(ModuleInfo, TypeDefnTable),
 	map__search(TypeDefnTable, TypeId, TypeDefn),
 	hlds_data__get_type_defn_body(TypeDefn, TypeBody),
-	TypeBody = du_type(_, _, IsEnum),
+	TypeBody = du_type(_, _, IsEnum, _),
 	IsEnum = yes.
 
 type_to_type_id(Type, SymName - Arity, Args) :-
@@ -315,7 +315,7 @@
 	map__search(TypeTable, TypeId, TypeDefn),
 	hlds_data__get_type_defn_tparams(TypeDefn, TypeParams),
 	hlds_data__get_type_defn_body(TypeDefn, TypeBody),
-	TypeBody = du_type(Constructors0, _, _),
+	TypeBody = du_type(Constructors0, _, _, _),
 	substitute_type_args(TypeParams, TypeArgs, Constructors0,
 		Constructors).
 
Index: compiler/typecheck.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/typecheck.m,v
retrieving revision 1.207
diff -u -r1.207 typecheck.m
--- typecheck.m	1997/06/29 23:11:36	1.207
+++ typecheck.m	1997/07/16 13:54:17
@@ -94,10 +94,6 @@
 %	then delete unused overloadings, and only then should we report
 %	ambiguity errors, if any overloading still remains.
 %
-% XXX	There seems to be a performance bug with the handling of
-%	typevarsets; during type inference, the typevarsets get bigger
-%	and bigger.
-%
 % Wish list:
 %
 %	we should handle equivalence types here
@@ -167,7 +163,7 @@
 :- import_module hlds_goal, hlds_data, prog_util, type_util, code_util.
 :- import_module prog_data, prog_io, prog_io_util, prog_out, hlds_out.
 :- import_module mercury_to_mercury, mode_util, options, getopt, globals.
-:- import_module passes_aux, clause_to_proc.
+:- import_module passes_aux, clause_to_proc, special_pred.
 
 :- import_module int, list, map, set, string, require, std_util, tree234.
 :- import_module assoc_list, varset, term, term_io.
@@ -340,7 +336,10 @@
 	(
 	    % Compiler-generated predicates are created already type-correct,
 	    % there's no need to typecheck them.  Same for builtins.
-	    ( code_util__compiler_generated(PredInfo0)
+	    % But, compiler-generated unify predicates are not guaranteed
+	    % to be type-correct if they call a user-defined equality pred.
+	    ( code_util__compiler_generated(PredInfo0),
+	      \+ pred_is_user_defined_equality_pred(PredInfo0, ModuleInfo)
 	    ; code_util__predinfo_is_builtin(PredInfo0)
 	    )
 	->
@@ -417,7 +416,7 @@
 				Changed = yes
 			)
 		),
-		typecheck_info_get_found_error(TypeCheckInfo2, Error),
+		typecheck_info_get_found_error(TypeCheckInfo3, Error),
 		(
 			Error = yes,
 			MaybePredInfo = no
@@ -425,13 +424,36 @@
 			Error = no,
 			MaybePredInfo = yes(PredInfo)
 		),
-		typecheck_info_get_io_state(TypeCheckInfo2, IOState)
+		typecheck_info_get_io_state(TypeCheckInfo3, 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.
+
+pred_is_user_defined_equality_pred(PredInfo, ModuleInfo) :-
+	%
+	% check if the predicate is a compiler-generated unification predicate
+	%
+	pred_info_name(PredInfo, PredName),
+	pred_info_arity(PredInfo, PredArity),
+	special_pred_name_arity(unify, _, PredName, PredArity),
+	%
+	% find out which type it is a unification predicate for,
+	% and check whether that type is a type for which there is
+	% a user-defined equality predicate.
+	%
+	pred_info_arg_types(PredInfo, _TypeVarSet, ArgTypes),
+	special_pred_get_type(PredName, ArgTypes, Type),
+	type_to_type_id(Type, TypeId, _TypeArgs),
+	module_info_types(ModuleInfo, TypeTable),
+	map__lookup(TypeTable, TypeId, TypeDefn),
+	hlds_data__get_type_defn_body(TypeDefn, Body),
+	Body = du_type(_, _, _, yes(_)).
 
 %-----------------------------------------------------------------------------%
 
Index: compiler/unify_gen.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/unify_gen.m,v
retrieving revision 1.80
diff -u -r1.80 unify_gen.m
--- unify_gen.m	1997/05/30 15:21:43	1.80
+++ unify_gen.m	1997/06/30 06:49:50
@@ -122,7 +122,7 @@
 		code_info__lookup_type_defn(Type, TypeDefn),
 		{ hlds_data__get_type_defn_body(TypeDefn, TypeBody) },
 		{
-			TypeBody = du_type(_, ConsTable, _)
+			TypeBody = du_type(_, ConsTable, _, _)
 		->  
 			map__to_assoc_list(ConsTable, ConsList),
 			(
Index: compiler/unify_proc.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/compiler/unify_proc.m,v
retrieving revision 1.58
diff -u -r1.58 unify_proc.m
--- unify_proc.m	1997/05/21 02:13:54	1.58
+++ unify_proc.m	1997/07/16 19:52:00
@@ -58,9 +58,9 @@
 
 	% Add a new request to the unify_requests table.
 
-:- pred unify_proc__request_unify(unify_proc_id, determinism,
+:- pred unify_proc__request_unify(unify_proc_id, determinism, term__context,
 				module_info, module_info).
-:- mode unify_proc__request_unify(in, in, in, out) is det.
+:- mode unify_proc__request_unify(in, in, in, in, out) is det.
 
 	% Modecheck the unification procedures which have been
 	% requested.  If the first argument is `unique_mode_check',
@@ -82,8 +82,9 @@
 	% special predicates (compare/3, index/3, unify, etc.)
 
 :- pred unify_proc__generate_clause_info(special_pred_id, type,
-			hlds_type_body, module_info, clauses_info).
-:- mode unify_proc__generate_clause_info(in, in, in, in, out) is det.
+			hlds_type_body, term__context, module_info,
+			clauses_info).
+:- mode unify_proc__generate_clause_info(in, in, in, in, in, out) is det.
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -191,7 +192,8 @@
 
 %-----------------------------------------------------------------------------%
 
-unify_proc__request_unify(UnifyId, Determinism, ModuleInfo0, ModuleInfo) :-
+unify_proc__request_unify(UnifyId, Determinism, Context, ModuleInfo0,
+		ModuleInfo) :-
 	%
 	% check if this unification has already been requested
 	%
@@ -219,7 +221,6 @@
 		UnifyMode = ((X_Initial - Y_Initial) -> (X_Final - Y_Final)),
 		ArgModes = [(X_Initial -> X_Final), (Y_Initial -> Y_Final)],
 		MaybeDet = yes(Determinism),
-		term__context_init(Context),
 		ArgLives = no,  % XXX ArgLives should be part of the UnifyId
 		add_new_proc(PredInfo0, Arity, ArgModes, no, ArgLives,
 				MaybeDet, Context, PredInfo1, ProcId),
@@ -340,29 +341,35 @@
 	% modecheck the procedure
 	%
 	modecheck_proc(ProcId, PredId, ModuleInfo1, ModuleInfo2, NumErrors),
-	{ NumErrors \= 0 ->
-		error("mode error in compiler-generated unification predicate")
-	;
-		true
-	},
-	( { HowToCheckGoal = check_unique_modes } ->
-		{ detect_switches_in_proc(ProcId, PredId,
-					ModuleInfo2, ModuleInfo3) },
-		detect_cse_in_proc(ProcId, PredId,
-					ModuleInfo3, ModuleInfo4),
-		determinism_check_proc(ProcId, PredId,
-					ModuleInfo4, ModuleInfo5),
-		unique_modes__check_proc(ProcId, PredId,
-					ModuleInfo5, ModuleInfo)
-	;	
+	(
+		{ NumErrors \= 0 }
+	->
+		% It _is_ possible for a compiler-generated unification
+		% predicate to get have mode error, in the case where it
+		% contains a unification for a type with a user-defined
+		% equality predicate.
+		io__set_exit_status(1),
 		{ ModuleInfo = ModuleInfo2 }
+	;
+		( { HowToCheckGoal = check_unique_modes } ->
+			{ detect_switches_in_proc(ProcId, PredId,
+						ModuleInfo2, ModuleInfo3) },
+			detect_cse_in_proc(ProcId, PredId,
+						ModuleInfo3, ModuleInfo4),
+			determinism_check_proc(ProcId, PredId,
+						ModuleInfo4, ModuleInfo5),
+			unique_modes__check_proc(ProcId, PredId,
+						ModuleInfo5, ModuleInfo)
+		;	
+			{ ModuleInfo = ModuleInfo2 }
+		)
 	).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
-unify_proc__generate_clause_info(SpecialPredId, Type, TypeBody, ModuleInfo,
-				ClauseInfo) :-
+unify_proc__generate_clause_info(SpecialPredId, Type, TypeBody, Context,
+		ModuleInfo, ClauseInfo) :-
 	unify_proc__info_init(ModuleInfo, VarTypeInfo0),
 	( TypeBody = eqv_type(EqvType) ->
 		HeadVarType = EqvType
@@ -374,13 +381,14 @@
 	unify_proc__make_fresh_vars_from_types(ArgTypes, Args,
 					VarTypeInfo0, VarTypeInfo1),
 	( SpecialPredId = unify, Args = [H1, H2] ->
-		unify_proc__generate_unify_clauses(TypeBody, H1, H2,
+		unify_proc__generate_unify_clauses(TypeBody, H1, H2, Context,
 					Clauses, VarTypeInfo1, VarTypeInfo)
 	; SpecialPredId = index, Args = [X, Index] ->
-		unify_proc__generate_index_clauses(TypeBody, X, Index,
+		unify_proc__generate_index_clauses(TypeBody, X, Index, Context,
 					Clauses, VarTypeInfo1, VarTypeInfo)
 	; SpecialPredId = compare, Args = [Res, X, Y] ->
 		unify_proc__generate_compare_clauses(TypeBody, Res, X, Y,
+					Context,
 					Clauses, VarTypeInfo1, VarTypeInfo)
 	;
 		error("unknown special pred")
@@ -389,68 +397,116 @@
 	ClauseInfo = clauses_info(VarSet, Types, Types, Args, Clauses).
 
 :- pred unify_proc__generate_unify_clauses(hlds_type_body, var, var,
-				list(clause), unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_unify_clauses(in, in, in, out, in, out) is det.
+				term__context, list(clause),
+				unify_proc_info, unify_proc_info).
+:- mode unify_proc__generate_unify_clauses(in, in, in, in, out, in, out)
+	is det.
 
-unify_proc__generate_unify_clauses(TypeBody, H1, H2, Clauses) -->
-	( { TypeBody = du_type(Ctors, _, IsEnum), IsEnum = no } ->
-		unify_proc__generate_du_unify_clauses(Ctors, H1, H2, Clauses)
+unify_proc__generate_unify_clauses(TypeBody, H1, H2, Context, Clauses) -->
+	( { TypeBody = du_type(Ctors, _, IsEnum, MaybeEqPred), IsEnum = no } ->
+		( { MaybeEqPred = yes(PredName) } ->
+			%
+			% Just generate a call to the specified predicate,
+			% which is the user-defined equality pred for this
+			% type.
+			% (The pred_id and proc_id will be figured
+			% out by type checking and mode analysis.)
+			%
+			{ invalid_pred_id(PredId) },
+			{ invalid_proc_id(ModeId) },
+			{ Call = call(PredId, ModeId, [H1, H2], not_builtin,
+					no, PredName) },
+			{ goal_info_init(GoalInfo0) },
+			{ goal_info_set_context(GoalInfo0, Context,
+				GoalInfo) },
+			{ Goal = Call - GoalInfo },
+			unify_proc__quantify_clause_body([H1, H2], Goal,
+				Context, Clauses)
+		;
+			unify_proc__generate_du_unify_clauses(Ctors, H1, H2,
+				Context, Clauses)
+		)
 	;
-		{ term__context_init(Context) },
 		{ create_atomic_unification(H1, var(H2), Context, explicit, [],
 			Goal) },
-		unify_proc__info_get_varset(Varset0),
-		unify_proc__info_get_types(Types0),
-		{ implicitly_quantify_clause_body([H1, H2], Goal,
-			Varset0, Types0, Body, Varset, Types, _Warnings) },
-		unify_proc__info_set_varset(Varset),
-		unify_proc__info_set_types(Types),
-		{ Clauses = [clause([], Body, Context)] }
+		unify_proc__quantify_clause_body([H1, H2], Goal, Context,
+			Clauses)
 	).
 
 :- pred unify_proc__generate_index_clauses(hlds_type_body, var, var,
-				list(clause), unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_index_clauses(in, in, in, out, in, out) is det.
+				term__context, list(clause),
+				unify_proc_info, unify_proc_info).
+:- mode unify_proc__generate_index_clauses(in, in, in, in, out, in, out)
+	is det.
 
-unify_proc__generate_index_clauses(TypeBody, X, Index, Clauses) -->
-	( { TypeBody = du_type(Ctors, _, IsEnum), IsEnum = no } ->
-		unify_proc__generate_du_index_clauses(Ctors, X, Index, 0,
-			Clauses)
+unify_proc__generate_index_clauses(TypeBody, X, Index, Context, Clauses) -->
+	( { TypeBody = du_type(Ctors, _, IsEnum, MaybeEqPred), IsEnum = no } ->
+		( { MaybeEqPred = yes(_) } ->
+			%
+			% For non-canonical types, we just give up and
+			% always return -1 (meaning "index not available")
+			% from index/1.
+			%
+			{ ArgVars = [X, Index] },
+			unify_proc__build_call(
+				"builtin_index_non_canonical_type",
+				ArgVars, Context, Goal),
+			unify_proc__quantify_clause_body(ArgVars, Goal,
+				Context, Clauses)
+		;
+			unify_proc__generate_du_index_clauses(Ctors, X, Index,
+				Context, 0, Clauses)
+		)
 	;
 		{ ArgVars = [X, Index] },
-		unify_proc__build_call("index", ArgVars, Goal),
-		unify_proc__info_get_varset(Varset0),
-		unify_proc__info_get_types(Types0),
-		{ implicitly_quantify_clause_body(ArgVars, Goal,
-			Varset0, Types0, Body, Varset, Types, _Warnings) },
-		unify_proc__info_set_varset(Varset),
-		unify_proc__info_set_types(Types),
-		{ term__context_init(Context) },
-		{ Clauses = [clause([], Body, Context)] }
+		unify_proc__build_call("index", ArgVars, Context, Goal),
+		unify_proc__quantify_clause_body(ArgVars, Goal, Context,
+			Clauses)
 	).
 
 :- pred unify_proc__generate_compare_clauses(hlds_type_body, var, var, var,
+				term__context,
 				list(clause), unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_compare_clauses(in, in, in, in, out, in, out)
+:- mode unify_proc__generate_compare_clauses(in, in, in, in, in, out, in, out)
 	is det.
 
-unify_proc__generate_compare_clauses(TypeBody, Res, H1, H2, Clauses) -->
-	( { TypeBody = du_type(Ctors, _, IsEnum), IsEnum = no } ->
-		unify_proc__generate_du_compare_clauses(Ctors, Res, H1, H2,
-			Clauses)
+unify_proc__generate_compare_clauses(TypeBody, Res, H1, H2, Context, Clauses)
+		-->
+	( { TypeBody = du_type(Ctors, _, IsEnum, MaybeEqPred), IsEnum = no } ->
+		( { MaybeEqPred = yes(_) } ->
+			%
+			% just generate code that will call error/1
+			%
+			{ ArgVars = [Res, H1, H2] },
+			unify_proc__build_call(
+				"builtin_compare_non_canonical_type",
+				ArgVars, Context, Goal),
+			unify_proc__quantify_clause_body(ArgVars, Goal,
+				Context, Clauses)
+		;
+			unify_proc__generate_du_compare_clauses(Ctors,
+				Res, H1, H2, Context, Clauses)
+		)
 	;
 		{ ArgVars = [Res, H1, H2] },
-		unify_proc__build_call("compare", ArgVars, Goal),
-		unify_proc__info_get_varset(Varset0),
-		unify_proc__info_get_types(Types0),
-		{ implicitly_quantify_clause_body(ArgVars, Goal,
-			Varset0, Types0, Body, Varset, Types, _Warnings) },
-		unify_proc__info_set_varset(Varset),
-		unify_proc__info_set_types(Types),
-		{ term__context_init(Context) },
-		{ Clauses = [clause([], Body, Context)] }
+		unify_proc__build_call("compare", ArgVars, Context, Goal),
+		unify_proc__quantify_clause_body(ArgVars, Goal, Context,
+			Clauses)
 	).
 
+:- pred unify_proc__quantify_clause_body(list(var), hlds_goal, term__context,
+			list(clause), unify_proc_info, unify_proc_info).
+:- mode unify_proc__quantify_clause_body(in, in, in, out, in, out) is det.
+
+unify_proc__quantify_clause_body(HeadVars, Goal, Context, Clauses) -->
+	unify_proc__info_get_varset(Varset0),
+	unify_proc__info_get_types(Types0),
+	{ implicitly_quantify_clause_body(HeadVars, Goal,
+		Varset0, Types0, Body, Varset, Types, _Warnings) },
+	unify_proc__info_set_varset(Varset),
+	unify_proc__info_set_types(Types),
+	{ Clauses = [clause([], Body, Context)] }.
+
 %-----------------------------------------------------------------------------%
 
 /*
@@ -482,16 +538,17 @@
 */
 
 :- pred unify_proc__generate_du_unify_clauses(list(constructor), var, var,
-				list(clause), unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_du_unify_clauses(in, in, in, out, in, out) is det.
+				term__context, list(clause),
+				unify_proc_info, unify_proc_info).
+:- mode unify_proc__generate_du_unify_clauses(in, in, in, in, out, in, out)
+	is det.
 
-unify_proc__generate_du_unify_clauses([], _H1, _H2, []) --> [].
-unify_proc__generate_du_unify_clauses([Ctor | Ctors], H1, H2,
+unify_proc__generate_du_unify_clauses([], _H1, _H2, _Context, []) --> [].
+unify_proc__generate_du_unify_clauses([Ctor | Ctors], H1, H2, Context,
 		[Clause | Clauses]) -->
 	{ Ctor = FunctorName - ArgTypes },
 	{ list__length(ArgTypes, FunctorArity) },
 	{ FunctorConsId = cons(FunctorName, FunctorArity) },
-	{ term__context_init(Context) },
 	unify_proc__make_fresh_vars(ArgTypes, Vars1),
 	unify_proc__make_fresh_vars(ArgTypes, Vars2),
 	{ create_atomic_unification(
@@ -502,7 +559,9 @@
 		UnifyH2_Goal) },
 	{ unify_proc__unify_var_lists(Vars1, Vars2, UnifyArgs_Goal) },
 	{ GoalList = [UnifyH1_Goal, UnifyH2_Goal | UnifyArgs_Goal] },
-	{ goal_info_init(GoalInfo) },
+	{ goal_info_init(GoalInfo0) },
+	{ goal_info_set_context(GoalInfo0, Context,
+		GoalInfo) },
 	{ conj_list_to_goal(GoalList, GoalInfo, Goal) },
 	unify_proc__info_get_varset(Varset0),
 	unify_proc__info_get_types(Types0),
@@ -511,7 +570,7 @@
 	unify_proc__info_set_varset(Varset),
 	unify_proc__info_set_types(Types),
 	{ Clause = clause([], Body, Context) },
-	unify_proc__generate_du_unify_clauses(Ctors, H1, H2, Clauses).
+	unify_proc__generate_du_unify_clauses(Ctors, H1, H2, Context, Clauses).
 
 %-----------------------------------------------------------------------------%
 
@@ -535,18 +594,18 @@
 			).
 */
 
-:- pred unify_proc__generate_du_index_clauses(list(constructor), var, var, int,
-				list(clause), unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_du_index_clauses(in, in, in, in, out, in, out)
+:- pred unify_proc__generate_du_index_clauses(list(constructor), var, var,
+				term__context, int, list(clause),
+				unify_proc_info, unify_proc_info).
+:- mode unify_proc__generate_du_index_clauses(in, in, in, in, in, out, in, out)
 	is det.
 
-unify_proc__generate_du_index_clauses([], _X, _Index, _N, []) --> [].
-unify_proc__generate_du_index_clauses([Ctor | Ctors], X, Index, N,
+unify_proc__generate_du_index_clauses([], _X, _Index, _Context, _N, []) --> [].
+unify_proc__generate_du_index_clauses([Ctor | Ctors], X, Index, Context, N,
 		[Clause | Clauses]) -->
 	{ Ctor = FunctorName - ArgTypes },
 	{ list__length(ArgTypes, FunctorArity) },
 	{ FunctorConsId = cons(FunctorName, FunctorArity) },
-	{ term__context_init(Context) },
 	unify_proc__make_fresh_vars(ArgTypes, ArgVars),
 	{ create_atomic_unification(
 		X, functor(FunctorConsId, ArgVars), Context, explicit, [], 
@@ -555,7 +614,9 @@
 		Index, functor(int_const(N), []), Context, explicit, [], 
 		UnifyIndex_Goal) },
 	{ GoalList = [UnifyX_Goal, UnifyIndex_Goal] },
-	{ goal_info_init(GoalInfo) },
+	{ goal_info_init(GoalInfo0) },
+	{ goal_info_set_context(GoalInfo0, Context,
+		GoalInfo) },
 	{ conj_list_to_goal(GoalList, GoalInfo, Goal) },
 	unify_proc__info_get_varset(Varset0),
 	unify_proc__info_get_types(Types0),
@@ -565,7 +626,8 @@
 	unify_proc__info_set_types(Types),
 	{ Clause = clause([], Body, Context) },
 	{ N1 is N + 1 },
-	unify_proc__generate_du_index_clauses(Ctors, X, Index, N1, Clauses).
+	unify_proc__generate_du_index_clauses(Ctors, X, Index, Context, N1,
+		Clauses).
 
 %-----------------------------------------------------------------------------%
 
@@ -607,17 +669,18 @@
 */
 
 :- pred unify_proc__generate_du_compare_clauses(
-			list(constructor), var, var, var,
+			list(constructor), var, var, var, term__context,
 			list(clause), unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_du_compare_clauses(in, in, in, in, out, in, out)
-	is det.
+:- mode unify_proc__generate_du_compare_clauses(in, in, in, in, in,
+			out, in, out) is det.
 
-unify_proc__generate_du_compare_clauses(Ctors, Res, X, Y, [Clause]) -->
+unify_proc__generate_du_compare_clauses(Ctors, Res, X, Y, Context, [Clause]) -->
 	( { Ctors = [SingleCtor] } ->
-		unify_proc__generate_compare_case(SingleCtor, Res, X, Y, Goal)
+		unify_proc__generate_compare_case(SingleCtor, Res, X, Y,
+			Context, Goal)
 	;
 		unify_proc__generate_du_compare_clauses_2(Ctors, Res, X, Y,
-			Goal)
+			Context, Goal)
 	),
 	{ ArgVars = [Res, X, Y] },
 	unify_proc__info_get_varset(Varset0),
@@ -626,17 +689,15 @@
 		Varset0, Types0, Body, Varset, Types, _Warnings) },
 	unify_proc__info_set_varset(Varset),
 	unify_proc__info_set_types(Types),
-	{ term__context_init(Context) },
 	{ Clause = clause([], Body, Context) }.
 
 :- pred unify_proc__generate_du_compare_clauses_2(
-			list(constructor), var, var, var,
+			list(constructor), var, var, var, term__context,
 			hlds_goal, unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_du_compare_clauses_2(in, in, in, in, out, in, out)
-	is det.
+:- mode unify_proc__generate_du_compare_clauses_2(in, in, in, in, in,
+			out, in, out) is det.
 
-unify_proc__generate_du_compare_clauses_2(Ctors, Res, X, Y, Goal) -->
-	{ term__context_init(Context) },
+unify_proc__generate_du_compare_clauses_2(Ctors, Res, X, Y, Context, Goal) -->
 	{ construct_type(unqualified("int") - 0, [], IntType) },
 	{ construct_type(qualified("mercury_builtin", "comparison_result") - 0,
 					[], ResType) },
@@ -644,16 +705,18 @@
 	unify_proc__info_new_var(IntType, Y_Index),
 	unify_proc__info_new_var(ResType, R),
 
-	{ goal_info_init(GoalInfo) },
+	{ goal_info_init(GoalInfo0) },
+	{ goal_info_set_context(GoalInfo0, Context,
+		GoalInfo) },
 
-	unify_proc__build_call("index", [X, X_Index], Call_X_Index),
+	unify_proc__build_call("index", [X, X_Index], Context, Call_X_Index),
 
-	unify_proc__build_call("index", [Y, Y_Index], Call_Y_Index),
+	unify_proc__build_call("index", [Y, Y_Index], Context, Call_Y_Index),
 
-	unify_proc__build_call("builtin_int_lt", [X_Index, Y_Index],
+	unify_proc__build_call("builtin_int_lt", [X_Index, Y_Index], Context,
 		Call_Less_Than),
 
-	unify_proc__build_call("builtin_int_gt", [X_Index, Y_Index],
+	unify_proc__build_call("builtin_int_gt", [X_Index, Y_Index], Context,
 		Call_Greater_Than),
 
 	{ create_atomic_unification(
@@ -669,11 +732,11 @@
 	{ create_atomic_unification(Res, var(R), Context, explicit, [],
 		Return_R) },
 
-	unify_proc__generate_compare_cases(Ctors, R, X, Y, Cases),
+	unify_proc__generate_compare_cases(Ctors, R, X, Y, Context, Cases),
 	{ map__init(Empty) },
 	{ CasesGoal = disj(Cases, Empty) - GoalInfo },
 
-	unify_proc__build_call("compare_error", [], Abort),
+	unify_proc__build_call("compare_error", [], Context, Abort),
 
 	{ Goal = conj([
 		Call_X_Index,
@@ -712,23 +775,27 @@
 */
 
 :- pred unify_proc__generate_compare_cases(list(constructor), var, var, var,
-			list(hlds_goal), unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_compare_cases(in, in, in, in, out, in, out) is det.
+			term__context, list(hlds_goal),
+			unify_proc_info, unify_proc_info).
+:- mode unify_proc__generate_compare_cases(in, in, in, in, in, out, in, out)
+	is det.
 
-unify_proc__generate_compare_cases([], _R, _X, _Y, []) --> [].
-unify_proc__generate_compare_cases([Ctor | Ctors], R, X, Y, [Case | Cases]) -->
-	unify_proc__generate_compare_case(Ctor, R, X, Y, Case),
-	unify_proc__generate_compare_cases(Ctors, R, X, Y, Cases).
+unify_proc__generate_compare_cases([], _R, _X, _Y, _Context, []) --> [].
+unify_proc__generate_compare_cases([Ctor | Ctors], R, X, Y, Context,
+		[Case | Cases]) -->
+	unify_proc__generate_compare_case(Ctor, R, X, Y, Context, Case),
+	unify_proc__generate_compare_cases(Ctors, R, X, Y, Context, Cases).
 
 :- pred unify_proc__generate_compare_case(constructor, var, var, var,
-			hlds_goal, unify_proc_info, unify_proc_info).
-:- mode unify_proc__generate_compare_case(in, in, in, in, out, in, out) is det.
+			term__context, hlds_goal,
+			unify_proc_info, unify_proc_info).
+:- mode unify_proc__generate_compare_case(in, in, in, in, in, out, in, out)
+	is det.
 
-unify_proc__generate_compare_case(Ctor, R, X, Y, Case) -->
+unify_proc__generate_compare_case(Ctor, R, X, Y, Context, Case) -->
 	{ Ctor = FunctorName - ArgTypes },
 	{ list__length(ArgTypes, FunctorArity) },
 	{ FunctorConsId = cons(FunctorName, FunctorArity) },
-	{ term__context_init(Context) },
 	unify_proc__make_fresh_vars(ArgTypes, Vars1),
 	unify_proc__make_fresh_vars(ArgTypes, Vars2),
 	{ create_atomic_unification(
@@ -737,9 +804,11 @@
 	{ create_atomic_unification(
 		Y, functor(FunctorConsId, Vars2), Context, explicit, [], 
 		UnifyY_Goal) },
-	unify_proc__compare_args(Vars1, Vars2, R, CompareArgs_Goal),
+	unify_proc__compare_args(Vars1, Vars2, R, Context, CompareArgs_Goal),
 	{ GoalList = [UnifyX_Goal, UnifyY_Goal, CompareArgs_Goal] },
-	{ goal_info_init(GoalInfo) },
+	{ goal_info_init(GoalInfo0) },
+	{ goal_info_set_context(GoalInfo0, Context,
+		GoalInfo) },
 	{ conj_list_to_goal(GoalList, GoalInfo, Case) }.
 
 /*	unify_proc__compare_args: for a constructor such as
@@ -768,28 +837,28 @@
 
 */
 
-:- pred unify_proc__compare_args(list(var), list(var), var, hlds_goal,
-				unify_proc_info, unify_proc_info).
-:- mode unify_proc__compare_args(in, in, in, out, in, out) is det.
+:- pred unify_proc__compare_args(list(var), list(var), var, term__context,
+				hlds_goal, unify_proc_info, unify_proc_info).
+:- mode unify_proc__compare_args(in, in, in, in, out, in, out) is det.
 
-unify_proc__compare_args([], [], R, Return_Equal) -->
-	{ term__context_init(Context) },
+unify_proc__compare_args([], [], R, Context, Return_Equal) -->
 	{ create_atomic_unification(
 		R, functor(cons(unqualified("="), 0), []),
 		Context, explicit, [], 
 		Return_Equal) }.
-unify_proc__compare_args([X|Xs], [Y|Ys], R, Goal) -->
-	{ goal_info_init(GoalInfo) },
+unify_proc__compare_args([X|Xs], [Y|Ys], R, Context, Goal) -->
+	{ goal_info_init(GoalInfo0) },
+	{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 	( { Xs = [], Ys = [] } ->
-		unify_proc__build_call("compare", [R, X, Y], Goal)
+		unify_proc__build_call("compare", [R, X, Y], Context, Goal)
 	;
-		{ term__context_init(Context) },
 		{ construct_type(
 			qualified("mercury_builtin", "comparison_result") - 0,
 			[], ResType) },
 		unify_proc__info_new_var(ResType, R1),
 
-		unify_proc__build_call("compare", [R1, X, Y], Do_Comparison),
+		unify_proc__build_call("compare", [R1, X, Y], Context,
+			Do_Comparison),
 
 		{ create_atomic_unification(
 			R1, functor(cons(unqualified("="), 0), []),
@@ -804,20 +873,20 @@
 		{ map__init(Empty) },
 		{ Goal = if_then_else([], Condition, Return_R1, ElseCase, Empty)
 					- GoalInfo},
-		unify_proc__compare_args(Xs, Ys, R, ElseCase)
+		unify_proc__compare_args(Xs, Ys, R, Context, ElseCase)
 	).
-unify_proc__compare_args([], [_|_], _, _) -->
+unify_proc__compare_args([], [_|_], _, _, _) -->
 	{ error("unify_proc__compare_args: length mismatch") }.
-unify_proc__compare_args([_|_], [], _, _) -->
+unify_proc__compare_args([_|_], [], _, _, _) -->
 	{ error("unify_proc__compare_args: length mismatch") }.
 
 %-----------------------------------------------------------------------------%
 
-:- pred unify_proc__build_call(string, list(var), hlds_goal,
+:- pred unify_proc__build_call(string, list(var), term__context, hlds_goal,
 			unify_proc_info, unify_proc_info).
-:- mode unify_proc__build_call(in, in, out, in, out) is det.
+:- mode unify_proc__build_call(in, in, in, out, in, out) is det.
 
-unify_proc__build_call(Name, ArgVars, Goal) -->
+unify_proc__build_call(Name, ArgVars, Context, Goal) -->
 	unify_proc__info_get_module_info(ModuleInfo),
 	{ module_info_get_predicate_table(ModuleInfo, PredicateTable) },
 	{ list__length(ArgVars, Arity) },
@@ -833,12 +902,10 @@
 		error(ErrorMessage)
 	},
 	{ hlds_pred__initial_proc_id(ModeId) },
-	% We cheat by not providing a context for the call.
-	% Since automatically generated procedures should not have errors,
-	% the absence of a context should not be a problem.
 	{ Call = call(IndexPredId, ModeId, ArgVars, not_builtin,
 			no, unqualified(Name)) },
-	{ goal_info_init(GoalInfo) },
+	{ goal_info_init(GoalInfo0) },
+	{ goal_info_set_context(GoalInfo0, Context, GoalInfo) },
 	{ Goal = Call - GoalInfo }.
 
 %-----------------------------------------------------------------------------%
cvs diff: Diffing compiler/notes
cvs diff: Diffing doc
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/staff/zs/imp/mercury/doc/reference_manual.texi,v
retrieving revision 1.55
diff -u -r1.55 reference_manual.texi
--- reference_manual.texi	1997/07/14 03:45:11	1.55
+++ reference_manual.texi	1997/07/16 19:28:18
@@ -82,6 +82,8 @@
                       safely use destructive update to modify that value
 * Determinism::       Determinism declarations let you specify that a predicate
                       should never fail or should never succeed more than once
+* Equality preds::    User-defined types can have user-defined equality
+                      predicates.
 * Higher-order::      Mercury supports higher-order predicates and functions,
                       with closures, lambda expressions, and currying
 * Modules::           Modules allow you to divide a program into smaller parts
@@ -286,7 +288,7 @@
 except that as an extension we permit higher-order terms, as described
 below.
 However, the meaning of some terms in Mercury is different to that
-in Prolog.  See @xref{Data-terms}.
+in Prolog.  @xref{Data-terms}.
 
 A term is either a variable or a functor.
 
@@ -467,7 +469,7 @@
 @samp{call(Closure)} just calls
 the specified closure.  The other forms append the specified
 arguments onto the argument list of the closure before calling it.
-See @xref{Higher-order}.
+ at xref{Higher-order}.
 
 @item @code{Var}
 @itemx @code{Var(Arg1)}
@@ -685,12 +687,12 @@
 
 @noindent
 where Var1, Var2, @dots{} are variables, Mode1, Mode2, @dots{} are
-modes [@xref{Modes}], Det is a determinism [@xref{Determinism}],
-and Goal is a goal [@xref{Goals}]. 
+modes (@pxref{Modes}), Det is a determinism (@pxref{Determinism}),
+and Goal is a goal (@pxref{Goals}). 
 It denotes a higher-order predicate or function term
 whose value is the predicate or function of the specified arguments
 determined by the specified goal.
-See @xref{Higher-order}.
+ at xref{Higher-order}.
 
 A higher-order function application is a compound term of one
 of the following two forms
@@ -708,14 +710,14 @@
 @samp{T1}, @samp{T2}, @dots{}, @samp{Tn}. 
 The type of the higher-order function application term is @var{T}.
 It denotes the result of applying the specified function to the
-specified arguments.  See @xref{Higher-order}.
+specified arguments.  @xref{Higher-order}.
 
 @node Implicit quantification
 @section Implicit quantification
 
 The rule for implicit quantification in Mercury
 is not the same as the usual one in mathematical logic.
-In Mercury variables that do not occur in the head of a clause
+In Mercury, variables that do not occur in the head of a clause
 are implicitly existentially quantified around their closest enclosing scope
 (in a sense to be made precise in the following paragraphs).
 This allows most existential quantifiers to be omitted,
@@ -768,7 +770,7 @@
 @item Predicate types: @code{pred}, @code{pred(T)}, @code{pred(T1, T2)}, @dots{}
 @itemx Function types: @code{func(T1) = T}, @code{func(T1, T2) = T}, @dots{}
 These higher-order function and predicate types are used to pass procedure
-addresses and closures to other predicates.  See @xref{Higher-order}.
+addresses and closures to other predicates.  @xref{Higher-order}.
 
 @item The universal type: @code{univ}.
 The type @code{univ} is defined in the standard library module @code{std_util},
@@ -1616,7 +1618,8 @@
 The determinism of the empty conjunction (the goal @samp{true})
 is @code{det}.
 The conjunction @samp{(@var{A}, @var{B})} can fail
-if either @var{A} or @var{B} can fail.
+if either @var{A} can fail, or if @var{A} can succeed at least once,
+and @var{B} can fail.
 The conjunction can succeed at most zero times
 if either @var{A} or @var{B} can succeed at most zero times.
 The conjunction can succeed more than once
@@ -1800,7 +1803,7 @@
 If you want all of them, you need to use the predicate
 @samp{solutions/2} in the standard library module @samp{std_util},
 which collects all of the solutions to a goal into a list --
-see @xref{Higher-order}.
+ at pxref{Higher-order}.
 
 If you just want one solution and don't care which,
 the calling predicate should be declared @code{nondet} or @code{multi}.
@@ -1824,11 +1827,12 @@
 The other situation in which you may want pruning
 and committed choice style nondeterminism
 is when you know that all the solutions returned will be equivalent.
-For example, you might want to count the elements in a set
-by removing them one at a time.
-Removing an unspecified element from a set is a nondeterministic operation,
+For example, you might want to find the maximum element in a set
+by iterating over the elements in the set.
+Iterating over the elements in a set in an unspecified order is a
+nondeterministic operation,
 but no matter which order you remove them,
-the computed size of the set should be the same.
+the maximum value in the set should be the same.
 
 We may eventually extend Mercury to allow users to write
 
@@ -1843,10 +1847,9 @@
 to prune alternative solutions for @samp{Goal}
 if @samp{X} was the only output variable of @samp{Goal}.  
 
-We would also like to allow users
-to specify a user-defined equivalence relation
-as the equality relation for user-defined types,
-so that the @samp{unique} quantifier
+Note that specifying a user-defined equivalence relation
+as the equality predicate for user-defined types (@pxref{Equality preds})
+means that the @samp{unique} quantifier
 could be used to express more general forms of equivalence.
 For example, if you define a set type which represents sets as unsorted lists,
 you would want to define a user-defined equivalence relation for that type,
@@ -1855,8 +1858,10 @@
 even though the lists used to represent the sets
 might not be in the same order in every solution.
 
-However, the current implementation does not yet support
-either the @samp{unique} quantifier or user-defined equivalence relations.
+The current version of Mercury does not support
+the @samp{unique} quantifier.  (However, it is possible
+to achieve a similar effect by using the C interface
+to type-cast a higher-order predicate term.)
 
 @node Committed choice nondeterminism
 @section Committed choice nondeterminism
@@ -1895,11 +1900,14 @@
 The compiler will check that all calls to a committed-choice
 mode of a predicate do indeed occur in a single-solution context.
 
-There are two reasons to use committed choice determinism annotations.
+There are several reasons to use committed choice determinism annotations.
 One reason is for efficiency: committed choice annotations allow
 the compiler to generate much more efficient code.
-The other reason is for doing I/O, which is allowed only in @samp{det}
+Another reason is for doing I/O, which is allowed only in @samp{det}
 or @samp{cc_multi} predicates, not in @samp{multi} predicates.
+Another is for dealing with types that use non-canonical representations
+(@pxref{Equality preds}).
+And there are a variety of other applications.
 
 It would be nice to be able to declare a mode of a predicate as
 both @samp{multi} and @samp{cc_multi}, and have the compiler call
@@ -1907,6 +1915,117 @@
 single-solution context or not.  However, the current implementation
 does not yet support this.
 
+ at node Equality preds
+ at chapter User-defined equality predicates
+
+When defining abstract data types, 
+often it is convenient to use a non-canonical representation ---
+that is, one for which a single abstract value may have more than
+one different possible concrete representations.
+For example, you may wish to implement an abstract type @samp{set}
+by representing a set as an (unsorted) list. 
+
+ at example
+:- module set_as_unsorted_list.
+:- interface.
+:- type set(T).
+
+:- implementation.
+:- import_module list.
+:- type set(T) ---> set(list(T)).
+ at end example
+
+ at noindent
+In this example, the concrete representations @samp{set([1,2])} and
+ at samp{set([2,1])} would both represent the same abstract value, namely
+the set containing the elements 1 and 2.
+
+For types such as this, which do not have a canonical representation,
+the standard definition of equality is the desired one; we want equality on
+sets to mean equality of the abstract values, not equality of their
+representations.  To support such types, Mercury allows programmers to
+specify a user-defined equality predicate for user-defined types:
+
+ at example
+:- type set(T) ---> set(list(T))
+	where equality is set_equals.
+ at end example
+
+ at noindent
+Here @samp{set_equals} is the name of a user-defined predicate that
+is used for equality on the type @samp{set(T)}.  It could for example
+be defined in terms of a @samp{subset} predicate.
+
+ at example
+:- pred set_equals(set(T)::in, set(T)::in) is semidet.
+set_equals(S1, S2) :-
+	subset(S1, S2),
+	subset(S2, S1).
+ at end example
+
+A type declaration for a type @var{T} may contain a
+ at samp{where equality is @var{equalitypred}} specification only
+if the following conditions are satisfied:
+
+ at itemize @bullet
+ at item
+ at var{T} must be a discriminated union type; it may not be an
+equivalence type
+
+ at item
+ at var{equalitypred} must be the name of a predicate with type
+ at samp{pred(T, T)} and mode @samp{(in, in) is semidet}.
+
+ at end itemize
+
+Types with user-defined equality can only be used in limited ways.
+Because there multiple representations for the same abstract
+value, any attempt to examine the representation of such a value
+is a conceptually non-deterministic operation.  
+In Mercury this is modelled using committed choice nondeterminism.
+
+The semantics of a specifying @samp{where equality is @var{equalitypred}} 
+on the type declaration for a type @var{T} are as follows:
+
+ at itemize @bullet
+ at item
+If the program contains any deconstruction unification or switch
+on a variable of type @var{T} that could fail, other than unifications
+with mode @samp{(in, in)}, then it is a compile-time error.
+
+ at item
+If the program contains any deconstruction unification or switch
+on a variable of type @var{T} that cannot fail, then that operation
+has determinism @samp{cc_multi}.
+
+ at item
+Any attempts to examine the representation of a variable of type @var{T}
+using facilities of the standard library (e.g. @samp{argument}/3
+and @samp{functor/3} in @samp{std_util}) that do not have determinism
+ at samp{cc_multi} or @samp{cc_nondet} will result in a run-time error.
+
+ at item
+In addition to the usual equality axioms,
+the declarative semantics of the program will contain the axiom
+ at samp{@var{X} = @var{Y} <=> @var{equalitypred}(X, Y)} for all
+ at var{X} and @var{Y} of type @samp{T}.
+
+ at item
+Any @samp{(in, in)} unifications for type @var{T} are computed using the
+specified predicate @var{equalitypred}.
+
+ at item
+ at var{equalitypred} should be an equivalence relation; that is, it must be
+symmetric, reflexive, and transitive.  However, the compiler is not required
+to check this at footnote{If @var{equalitypred} is not an equivalence relation,
+then the program is inconsistent: its declarative semantics 
+contains a contradiction, because the additional axioms for the user-defined
+equality contradict the standard equality axioms.  That implies that the
+implementation may compute any answer at all (@pxref{Semantics}),
+i.e. the behaviour of the program is undefined.}.
+
+ at end itemize
+
 @node Higher-order
 @chapter Higher-order programming
 
@@ -2206,7 +2325,7 @@
 @end example
 
 @noindent
-using the parametric inst @samp{in/1} mentioned in @xref{Modes}
+using the parametric inst @samp{in/1} mentioned in @ref{Modes}
 which maps an inst to itself.
 
 If you want to define a predicate which returns a higher-order predicate
@@ -2369,10 +2488,8 @@
 two underscores.  We have found this convention improves the
 readability and maintainability of our code, and so we recommend that
 you follow it in your code too. (Eventually, these names will be converted
-to names of the form @code{module:name}; this will allow you to omit the
-prefix in places where it does not improve readability. A tool for the
-automatic conversion of existing programs will be provided when this change
-occurs.)
+to names of the form @code{module.name}; this will allow you to omit the
+prefix in places where it does not improve readability.)
 
 @node Semantics
 @chapter Semantics
@@ -2719,9 +2836,9 @@
 
 The @samp{list_cons} macro should only be used in C code called
 using the @samp{will_not_call_mercury} calling convention.
-XXX I am not sure about this - zs
+ at c XXX I am not sure about this - zs
 
-XXX we need a more extensive discussion on memory allocation here
+ at c XXX we need a more extensive discussion on memory allocation here
 
 @node Using C pointers
 @subsection Using C pointers
cvs diff: Diffing extras
cvs diff: Diffing extras/cgi
cvs diff: Diffing extras/complex_numbers
cvs diff: Diffing extras/complex_numbers/samples
cvs diff: Diffing extras/complex_numbers/tests
cvs diff: Diffing library
Index: library/mercury_builtin.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/library/mercury_builtin.m,v
retrieving revision 1.77
diff -u -r1.77 mercury_builtin.m
--- mercury_builtin.m	1997/07/16 17:49:31	1.77
+++ mercury_builtin.m	1997/07/16 17:51:12
@@ -198,6 +198,13 @@
 :- pred builtin_compare_pred(comparison_result::out, (pred)::in, (pred)::in)
 	is det.
 
+% The following two preds are used for index/1 or compare/3 on
+% non-canonical types (types for which there is a `where equality is ...'
+% declaration).
+:- pred builtin_index_non_canonical_type(T::in, int::out) is det.
+:- pred builtin_compare_non_canonical_type(comparison_result::out,
+		T::in, T::in) is det.
+
 :- pred unused is det.
 
 	% compare_error is used in the code generated for compare/3 preds
@@ -231,7 +238,7 @@
 %-----------------------------------------------------------------------------%
 
 :- implementation.
-:- import_module require, std_util, int, float, char, string, list.
+:- import_module require, string, std_util, int, float, char, string, list.
 
 % Many of the predicates defined in this module are builtin -
 % the compiler generates code for them inline.
@@ -299,7 +306,7 @@
 builtin_compare_float(R, F1, F2) :-
 	( F1 < F2 ->
 		R = (<)
-	; F1 < F2 ->
+	; F1 > F2 ->
 		R = (>)
 	;
 		R = (=)
@@ -310,6 +317,22 @@
 
 :- pragma(c_code, builtin_strcmp(Res::out, S1::in, S2::in),
 	"Res = strcmp(S1, S2);").
+
+builtin_index_non_canonical_type(_, -1).
+
+builtin_compare_non_canonical_type(Res, X, _Y) :-
+	% suppress determinism warning
+	( semidet_succeed ->
+		string__append_list([
+			"call to compare/3 for non-canonical type `",
+			type_name(type_of(X)),
+			"'"],
+			Message),
+		error(Message)
+	;
+		% the following is never executed
+		Res = (<)
+	).
 
 :- external(builtin_unify_pred/2).
 :- external(builtin_index_pred/2).
Index: library/std_util.m
===================================================================
RCS file: /home/staff/zs/imp/mercury/library/std_util.m,v
retrieving revision 1.93
diff -u -r1.93 std_util.m
--- std_util.m	1997/06/04 09:59:37	1.93
+++ std_util.m	1997/07/16 13:05:45
@@ -1891,7 +1891,8 @@
 	 * non-zero). The arity will always be set.
 	 *
 	 * ML_expand will fill in the other fields (functor, arity,
-	 * argument_vector and type_info_vector) accordingly, but
+	 * argument_vector, type_info_vector, and non_canonical_type)
+	 * accordingly, but
 	 * the values of fields not asked for should be assumed to
 	 * contain random data when ML_expand returns.
 	 * (that is, they should not be relied on to remain unchanged).
@@ -1903,6 +1904,7 @@
 	int arity;
 	Word *argument_vector;
 	Word *type_info_vector;
+	bool non_canonical_type;
 	bool need_functor;
 	bool need_args;
 } ML_Expand_Info;
@@ -1929,6 +1931,9 @@
 static void ML_expand_complicated(Word data_value, Word entry_value, 
 	Word * type_info, ML_Expand_Info *info);
 
+Declare_entry(mercury__builtin_compare_pred_3_0);
+Declare_entry(mercury__builtin_compare_non_canonical_type_3_0);
+
 /*
 ** Expand the given data using its type_info, find its
 ** functor, arity, argument vector and type_info vector.
@@ -1956,12 +1961,20 @@
 void 
 ML_expand(Word* type_info, Word data_word, ML_Expand_Info *info)
 {
+	Code *compare_pred;
 	Word *base_type_info, *arg_type_info;
 	Word data_value, entry_value, base_type_layout_entry;
 	int entry_tag, data_tag; 
 
 	base_type_info = MR_TYPEINFO_GET_BASE_TYPEINFO(type_info);
 
+	compare_pred = (Code *) base_type_info[OFFSET_FOR_COMPARE_PRED];
+	info->non_canonical_type =
+		( compare_pred == ENTRY(mercury__builtin_compare_pred_3_0) ||
+		  compare_pred ==
+			ENTRY(mercury__builtin_compare_non_canonical_type_3_0)
+		);
+
 	data_tag = tag(data_word);
 	data_value = body(data_word, data_tag);
 	
@@ -2383,11 +2396,23 @@
 
 	restore_transient_registers();
 
+		/*
+		** Check for attempts to deconstruct a non-canonical type:
+		** such deconstructions must be cc_multi, and since
+		** functor/3 is det, we must treat violations of this
+		** as runtime errors.
+		** (There ought to be a cc_multi version of functor/3
+		** that allows this.)
+		*/
+	if (info.non_canonical_type) {
+		fatal_error(""called functor/3 for a type with a ""
+			""user-defined equality predicate"");
+	}
+
 		/* Copy functor onto the heap */
 	make_aligned_string(LVALUE_CAST(ConstString, Functor), info.functor);
 
 	Arity = info.arity;
-
 }").
 
 :- pragma c_code(argument(Type::in, ArgumentIndex::in) = (Argument::out),
@@ -2406,6 +2431,19 @@
 
 	restore_transient_registers();
 
+		/*
+		** Check for attempts to deconstruct a non-canonical type:
+		** such deconstructions must be cc_multi, and since
+		** argument/3 is det, we must treat violations of this
+		** as runtime errors.
+		** (There ought to be a cc_multi version of argument/3
+		** that allows this.)
+		*/
+	if (info.non_canonical_type) {
+		fatal_error(""called argument/3 for a type with a ""
+			""user-defined equality predicate"");
+	}
+
 		/* Check range */
 	success = (ArgumentIndex >= 0 && ArgumentIndex < info.arity);
 	if (success) {
@@ -2460,6 +2498,19 @@
 	ML_expand((Word *) TypeInfo_for_T, Type, &info);
 	
 	restore_transient_registers();
+
+		/*
+		** Check for attempts to deconstruct a non-canonical type:
+		** such deconstructions must be cc_multi, and since
+		** deconstruct/5 is det, we must treat violations of this
+		** as runtime errors.
+		** (There ought to be a cc_multi version of deconstruct/5
+		** that allows this.)
+		*/
+	if (info.non_canonical_type) {
+		fatal_error(""called deconstruct/5 for a type with a ""
+			""user-defined equality predicate"");
+	}
 
 		/* Get functor */
 	make_aligned_string(LVALUE_CAST(ConstString, Functor), info.functor);
cvs diff: Diffing lp_solve
cvs diff: Diffing lp_solve/lp_examples
cvs diff: Diffing profiler
cvs diff: Diffing runtime
cvs diff: Diffing runtime/machdeps
cvs diff: Diffing samples
cvs diff: Diffing samples/c_interface
cvs diff: Diffing samples/c_interface/c_calls_mercury
cvs diff: Diffing samples/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/c_interface/mercury_calls_c
cvs diff: Diffing samples/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/diff
cvs diff: Diffing scripts
cvs diff: Diffing tests
cvs diff: Diffing tests/benchmarks
cvs diff: Diffing tests/general
cvs diff: Diffing tests/hard_coded
cvs diff: Diffing tests/invalid
cvs diff: Diffing tests/misc_tests
cvs diff: Diffing tests/valid
cvs diff: Diffing tests/warnings
cvs diff: Diffing tools
cvs diff: Diffing trial
cvs diff: Diffing util

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.



More information about the developers mailing list