[m-rev.] For review: solver-types

Ralph Becket rafe at cs.mu.OZ.AU
Fri Jul 16 16:26:55 AEST 2004


Because of its size, I would like to commit this change as soon as
possible before the compiler changes much more.

(1) There are a few parts of this change (about a dozen) marked
`rafe: XXX' in comments about which I would appreciate advice from
reviewers.

(2) I've successfully compiled and tested a simple Church numerals
solver-type using this version of the compiler.

(3) Developer and user documentation to follow.

(4) There are still a number of problems to fix, including
- adding calls to init where necessary at the end of disjuncts;
- improving scheduling of solver-type goals to minimise the introduction
  of initialisation calls (currently it's pretty bad...);
- compilation with sub-modules doesn't yet work;
- it needs much more extensive testing.

-- Ralph



Estimated hours taken: 100s
Branches: main

Implement the solver-types design.


SOLVER TYPES

Solver types provide the means for adding constrained types to Mercury
programs.  A variable of a constrained type may have constraints placed
on it, limiting the values it may be bound to, *before* the variable is
actually bound to a particular value (cf. CLP(Z), CLP(R), CLP(FD) etc.)


SYNTAX

An abstract solver-type is introduced using the syntax

:- solver type t(T1, ..., Tn).

A solver-type is defined using the following syntax (all four attributes
are mandatory):

:- solver type t(T1, ..., Tn)
	where	representation is <type>,
		initialisation is <pred>,
		ground         is <inst>,
		any            is <inst>.

(The `where' attributes may also include `equality is <pred>' and/or
`comparison is <pred>' at the end.)

(Note that neither foreign types nor du-types can be solver types,
although they can of course be used to represent them.)

(As with user-defined equality, if a solver type is exported then so
must its initialisation predicate and representation type.)

The `representation is <type>' attribute specifies the type used to
implement the solver-type.

The `initialisation is <pred>' attribute specifies the predicate used to
initialise solver-type variables (more on this below.)

The `ground is <inst>' attribute specifies the representation type inst
corresponding to inst `ground' variables of the solver-type (this is
necessary because a solver-type variable may be semantically ground, but
have a non-ground representation - e.g.  if X, Y and Z are constrained
integers and we have the constraints X = Y - Z and Y = Z + 3 then X must
be 3 regardless of whether Y and Z are `ground'.)

The `any is <inst>' attribute specifies the representation type inst
corresponding to inst `any' variables of the solver-type (again, this is
necessary for similar reasons.)


THE `any' INST

The inst `any' applies to non-free variables that may or may not be
semantically ground.  A variable is semantically ground if the set of
values with which it unifies forms an equivalence class (i.e. if X is
semantically ground then if X can unify with Y and Z, then Y and Z must
also unify with each other.)  A variable is semantically non-ground if
the set of values with which it unifies do not form an equivalence class
(i.e. if X is semantically non-ground then there exist Y and Z that each
unify with X, but which do not unify with each other.)

Both `free' and `ground' are considered sub-insts of `any', but not the
other way round.


THE INITIALISATION PREDICATE

The implementation of a solver type will typically involve impure code.
At the very least impure code will be necessary to update the constraint
store for a solver type (i.e. the structure used to keep track of
constraints placed on variables of the solver type.)

Calls to the initialisation predicate are introduced by the compiler
during mode analysis when the subgoals of a procedure are being
scheduled.  Such calls are inserted when the compiler needs to turn a
solver-type argument variable inst from `free' to `any'.  The
initialisation predicate for a solver-type is responsible for adding a
new, unconstrained, variable to the corresponding constraint store.


COMPILER GENERATED CONVERSION FUNCTIONS

The compiler generates three impure functions from the solver-type
definition.  The first provides the means for the solver-type
implementer to convert solver-type values into the representation-type.

:- impure func 'representation of t/n'(<solver type>) = <repn type>.
:-        mode 'representation of t/n'(in           ) = out(<ground inst>)
			is det.
:-        mode 'representation of t/n'(in(any)      ) = out(<any inst>)
			is det.

The other two provide a translation in the other direction:

:- impure func 'representation to ground t/n'(<repn type>) = <solver type>.
:-        mode 'representation to ground t/n'(in)        ) = out
			is det.

:- impure func 'representation to any t/n'(<repn type>   ) = <solver type>.
:-        mode 'representation to any t/n'(in(<any inst>)) = out(any)
			is det.

(Two are necessary because a single bi-moded function would have
ambiguous modes in the case the <ground inst> = <any inst>.)

These functions are impure because they can potentially convert a
semantically ground value into a semantically non-ground value and vice
versa (e.g. constrained variables for a particular solver type might be
represented using indices into an array or pointers into the heap,
either of which are certainly ground, but may denote non-ground values
in the context of the constraint store.)  Such conversions are obviously
not logically sound; guaranteeing denotational soundness is the
solver-type implementor's responsibility.


OTHER ASPECTS OF THIS CHANGE

I have moved all HLDS details concerning solver-type details and
user-defined equality and comparison into a single special_type_details
structure defined in prog_data.m.  A large part of this change involves
propagating this change throughout the compiler.

I have made some small, opportunistic cosmetic changes.  This
implementation has evolved through several design changes, during which
some functionality was added then later removed - I elected to preserve
any cleaned-up replacement code if removing the no-longer-needed-by-the-
solver-types-design functionality was easy to do.


compiler/hlds_data.m:
	Changed the du_type and foreign_type constructors appropriately
	and added a new solver_type constructor.

compiler/hlds_out.m:
	Improved and moved the code to write out the `where ...' part of
	a type definition to mercury_output.m.

compiler/inst_match.m:
	Added the pred inst_is_any/1.

compiler/inst_util.m:
	Added the pred inst_contains_unconstrained_var/1.

compiler/make_hlds.m:
	Added processing for solver types, in particular adding the
	compiler generated declarations and implementations of the
	conversion functions.

	"Neutered" combine_is_solver_type (see `rafe: XXX' comment):
	I don't think foreign types should be solver types.

compiler/maybe_mlds_to_gcc.pp:
	Added an import of hlds__passes_aux which the compiler was
	complaining about not having.

compiler/mercury_to_mercury.m:
	Added predicate mercury_output_special_type_details.

compiler/mode_errors.m:
compiler/modecheck_call.m:
compiler/modecheck_unify.m:
compiler/modes.m:
	The compiler now inserts calls to initialisation preds, where
	necessary, before calls and at the end of procedures.  It does
	not yet do this at the end of disjuncts and its scheduling
	policy is naive (i.e. it performs terribly.)

compiler/modules.m:
	XXX Reviewers: please look at the `rafe: XXX' comments and
	advise!

compiler/prog_data.m:
	Added the solver_type constructor and the special_type_details
	and solver_type_details types.

compiler/prog_io.m:
compiler/prog_io_pragma.m:
	Parse the new syntax.
	Replaced get_maybe_equality_compare_preds with
	parse_type_decl_where_part_if_present.

compiler/prog_mode.m:
	Added funcs in_mode/1, out_mode/1, in_any_mode/0,
	out_any_mode/0, and any_inst/0.

compiler/special_pred.m:
	Added `initialise' constructor to special_pred_id.
	Changed special_pred_name to include the type name and arity
	with `__Unify__', `__Inex__' etc.

compiler/type_util.m:
	Added some more utility funcs/preds.

compiler/unify_proc.m:
	Generate the forwarding predicates for initialisation preds.

compiler/equiv_type.m:
compiler/equiv_type_hlds.m:
compiler/foreign.m:
compiler/hlds_module.m:
compiler/intermod.m:
compiler/magic_util.m:
compiler/ml_code_gen.m:
compiler/ml_type_gen.m:
compiler/ml_unify_gen.m:
compiler/mlds.m:
compiler/module_qual.m:
compiler/post_typecheck.m:
compiler/pragma_c_gen.m:
compiler/prog_util.m:
compiler/purity.m:
compiler/recompilation.check.m:
compiler/recompilation.usage.m:
compiler/recompilation.version.m:
compiler/rl_key.m:
compiler/table_gen.m:
compiler/term_norm.m:
compiler/termination.m:
compiler/type_ctor_info.m:
compiler/typecheck.m:
	Propagate the change to use special_type_details.
	Some minor cosmetic changes.


Index: equiv_type.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/equiv_type.m,v
retrieving revision 1.39
diff -u -r1.39 equiv_type.m
--- equiv_type.m	14 Jun 2004 04:49:07 -0000	1.39
+++ equiv_type.m	15 Jul 2004 06:29:43 -0000
@@ -389,6 +389,11 @@
 		ExpandedItems = yes(_ - ItemIds)
 	).
 
+	% rafe: XXX Should this handle the representation type of
+	% solver types as well?  I already have something in
+	% equiv_type_hlds.replace_in_type_defn that appears to
+	% do the right thing.
+	%
 :- pred equiv_type__replace_in_type_defn(eqv_map::in, type_ctor::in,
 	type_defn::in, type_defn::out, bool::out, tvarset::in, tvarset::out,
 	equiv_type_info::in, equiv_type_info::out) is semidet.
@@ -399,8 +404,8 @@
 		_, ContainsCirc, !VarSet, !Info).
 
 equiv_type__replace_in_type_defn(EqvMap, _,
-		du_type(TBody0, IsSolverType, EqPred),
-		du_type(TBody, IsSolverType, EqPred), no, !VarSet, !Info) :-
+		du_type(TBody0, SpecialTypeDetails),
+		du_type(TBody, SpecialTypeDetails), no, !VarSet, !Info) :-
 	equiv_type__replace_in_ctors(EqvMap, TBody0, TBody, !VarSet, !Info).
 
 %-----------------------------------------------------------------------------%
Index: equiv_type_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/equiv_type_hlds.m,v
retrieving revision 1.6
diff -u -r1.6 equiv_type_hlds.m
--- equiv_type_hlds.m	14 Jun 2004 04:16:02 -0000	1.6
+++ equiv_type_hlds.m	1 Jul 2004 02:23:18 -0000
@@ -36,7 +36,7 @@
 :- import_module parse_tree__prog_data.
 :- import_module recompilation.
 
-:- import_module bool, list, set, map, require, std_util, term, varset.
+:- import_module bool, list, set, map, require, std_util, string, term, varset.
 
 replace_in_hlds(!ModuleInfo) :-
 	module_info_types(!.ModuleInfo, Types0),
@@ -119,7 +119,7 @@
 	equiv_type__maybe_record_expanded_items(ModuleName, fst(TypeCtor),
 		!.MaybeRecompInfo, EquivTypeInfo0),
 	(
-		Body0 = du_type(Ctors0, _, _, _, _, _, _),
+		Body0 = du_type(Ctors0, _, _, _, _, _),
 		equiv_type__replace_in_ctors(EqvMap, Ctors0, Ctors,
 			TVarSet0, TVarSet, EquivTypeInfo0, EquivTypeInfo),
 		Body = Body0 ^ du_type_ctors := Ctors
@@ -129,11 +129,35 @@
 			TVarSet0, TVarSet, EquivTypeInfo0, EquivTypeInfo),
 		Body = eqv_type(Type)
 	;
-		Body0 = foreign_type(_, _),
+		Body0 = foreign_type(_),
 		EquivTypeInfo = EquivTypeInfo0,
 		Body = Body0,
 		TVarSet = TVarSet0
 	;
+		Body0 = solver_type(SpecialTypeDetails0),
+		(
+			SpecialTypeDetails0 ^ solver_type_details =
+				yes(SolverTypeDetails0)
+		->
+			RepnType0 = SolverTypeDetails0 ^ representation_type,
+			equiv_type__replace_in_type(EqvMap,
+				RepnType0, RepnType, _,
+				TVarSet0, TVarSet1,
+				EquivTypeInfo0, EquivTypeInfo1),
+			SolverTypeDetails =
+				SolverTypeDetails0 ^ representation_type :=
+					RepnType,
+			SpecialTypeDetails =
+				SpecialTypeDetails0 ^ solver_type_details :=
+					yes(SolverTypeDetails)
+		;
+			error("replace_in_type_defn: solver type" ++
+				"with no solver_type_details")
+		),
+		EquivTypeInfo = EquivTypeInfo1,
+		Body = solver_type(SpecialTypeDetails),
+		TVarSet = TVarSet1
+	;
 		Body0 = abstract_type(_),
 		EquivTypeInfo = EquivTypeInfo0,
 		Body = Body0,
@@ -919,4 +943,5 @@
 		List = List0
 	).
 
+%-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
Index: foreign.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/foreign.m,v
retrieving revision 1.41
diff -u -r1.41 foreign.m
--- foreign.m	28 Jun 2004 04:49:42 -0000	1.41
+++ foreign.m	14 Jul 2004 06:44:17 -0000
@@ -24,7 +24,7 @@
 :- import_module libs__globals.
 :- import_module parse_tree__prog_data.
 
-:- import_module bool, std_util, list, string, term.
+:- import_module bool, list, std_util, string, term.
 
 :- type foreign_decl_info 		== list(foreign_decl_code).
 					% in reverse order
@@ -94,14 +94,14 @@
 	% Does the implementation of the given foreign type body on
 	% the current backend use a user-defined comparison predicate.
 :- func foreign_type_body_has_user_defined_eq_comp_pred(module_info,
-	foreign_type_body) = unify_compare is semidet.
+	foreign_type_body) = special_type_details is semidet.
 
 	% Find the current target backend from the module_info, and given
 	% a foreign_type_body, return the name of the foreign language type
 	% the identity of any user-defined unify/compare predicates, and the
 	% assertions applicable to that backend.
 :- pred foreign_type_body_to_exported_type(module_info::in,
-	foreign_type_body::in, sym_name::out, maybe(unify_compare)::out,
+	foreign_type_body::in, sym_name::out, special_type_details::out,
 	list(foreign_type_assertion)::out) is det.
 
 	% Given the exported_type representation for a type, determine
@@ -133,8 +133,8 @@
 	% returns the module name needed to refer to ForeignImport from the
 	% CurrentModule.
 	%
-:- func foreign_import_module_name(foreign_import_module, module_name)
-	= module_name.
+:- func foreign_import_module_name(foreign_import_module, module_name) =
+		module_name.
 
 	% Filter the decls for the given foreign language.
 	% The first return value is the list of matches, the second is
@@ -145,9 +145,9 @@
 	% Filter the module imports for the given foreign language.
 	% The first return value is the list of matches, the second is
 	% the list of mis-matches.
-:- pred filter_imports(foreign_language::in, foreign_import_module_info::in,
-	foreign_import_module_info::out, foreign_import_module_info::out)
-	is det.
+:- pred filter_imports(foreign_language::in,
+	foreign_import_module_info::in, foreign_import_module_info::out,
+	foreign_import_module_info::out) is det.
 
 	% Filter the bodys for the given foreign language.
 	% The first return value is the list of matches, the second is
@@ -661,7 +661,7 @@
 		map__search(Types, TypeCtor, TypeDefn)
 	->
 		hlds_data__get_type_defn_body(TypeDefn, Body),
-		( Body = foreign_type(ForeignTypeBody, _IsSolverType) ->
+		( Body = foreign_type(ForeignTypeBody) ->
 			foreign_type_body_to_exported_type(ModuleInfo,
 				ForeignTypeBody, ForeignTypeName, _,
 				Assertions),
@@ -674,13 +674,13 @@
 	).
 
 foreign_type_body_has_user_defined_eq_comp_pred(ModuleInfo, Body) =
-		UserEqComp :-
+		SpecialTypeDetails :-
 	foreign_type_body_to_exported_type(ModuleInfo, Body, _,
-		MaybeUserEqComp, _),
-	MaybeUserEqComp = yes(UserEqComp).
+		SpecialTypeDetails, _),
+	prog_data__has_user_defined_equality(SpecialTypeDetails).
 
 foreign_type_body_to_exported_type(ModuleInfo, ForeignTypeBody, Name,
-		MaybeUserEqComp, Assertions) :-
+		SpecialTypeDetails, Assertions) :-
 	ForeignTypeBody = foreign_type_body(MaybeIL, MaybeC, MaybeJava),
 	module_info_globals(ModuleInfo, Globals),
 	globals__get_target(Globals, Target),
@@ -689,7 +689,7 @@
 		(
 			MaybeC = yes(Data),
 			Data = foreign_type_lang_data(c(NameStr),
-				MaybeUserEqComp, Assertions),
+				SpecialTypeDetails, Assertions),
 			Name = unqualified(NameStr)
 		;
 			MaybeC = no,
@@ -700,7 +700,7 @@
 		(
 			MaybeIL = yes(Data),
 			Data = foreign_type_lang_data(il(_, _, Name),
-				MaybeUserEqComp, Assertions)
+				SpecialTypeDetails, Assertions)
 		;
 			MaybeIL = no,
 			unexpected(this_file, "to_exported_type: no IL type")
@@ -710,18 +710,19 @@
 		(
 			MaybeJava = yes(Data),
 			Data = foreign_type_lang_data(java(NameStr),
-				MaybeUserEqComp, Assertions),
+				SpecialTypeDetails, Assertions),
 			Name = unqualified(NameStr)
 		;
 			MaybeJava = no,
-			unexpected(this_file, "to_exported_type: no Java type")
+			unexpected(this_file,
+				"to_exported_type: no Java type")
 		)
 	;
 		Target = asm,
 		(
 			MaybeC = yes(Data),
 			Data = foreign_type_lang_data(c(NameStr),
-				MaybeUserEqComp, Assertions),
+				SpecialTypeDetails, Assertions),
 			Name = unqualified(NameStr)
 		;
 			MaybeC = no,
@@ -743,7 +744,7 @@
 	).
 to_type_string(csharp, foreign(ForeignType, _)) = Result :-
 	sym_name_to_string(ForeignType, ".", Result).
-to_type_string(managed_cplusplus, foreign(ForeignType, _)) = Result ++ " *":-
+to_type_string(managed_cplusplus, foreign(ForeignType, _)) = Result ++ " *" :-
 	sym_name_to_string(ForeignType, "::", Result).
 to_type_string(il, foreign(ForeignType, _)) = Result :-
 	sym_name_to_string(ForeignType, ".", Result).
@@ -793,16 +794,21 @@
 foreign_import_module_name(
 		foreign_import_module(Lang, ForeignImportModule, _)) =
 		ModuleName :-
-	( Lang = c,
+	(
+		Lang = c,
 		ModuleName = ForeignImportModule
-	; Lang = il,
+	;
+		Lang = il,
 		ModuleName = ForeignImportModule
-	; Lang = java,
+	;
+		Lang = java,
 		ModuleName = ForeignImportModule
-	; Lang = managed_cplusplus,
+	;
+		Lang = managed_cplusplus,
 		ModuleName = foreign_language_module_name(ForeignImportModule,
 				Lang)
-	; Lang = csharp,
+	;
+		Lang = csharp,
 		ModuleName = foreign_language_module_name(ForeignImportModule,
 				Lang)
 	).
Index: hlds_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_data.m,v
retrieving revision 1.87
diff -u -r1.87 hlds_data.m
--- hlds_data.m	14 Jun 2004 04:16:06 -0000	1.87
+++ hlds_data.m	14 Jul 2004 06:20:48 -0000
@@ -129,7 +129,7 @@
 	% An `hlds_type_body' holds the body of a type definition:
 	% du = discriminated union, uu = undiscriminated union,
 	% eqv_type = equivalence type (a type defined to be equivalent
-	% to some other type)
+	% to some other type), and solver_type.
 
 :- type hlds_type_body
 	--->	du_type(
@@ -142,24 +142,26 @@
 					% is this type an enumeration?
 			du_type_is_enum		:: bool,
 
-					% user-defined equality and
-					% comparison preds
-			du_type_usereq		:: maybe(unify_compare),
+					% Optional user-defined equality and
+					% comparison preds, but no
+					% solver_type_details.
+			du_type_special_type_details :: special_type_details,
 
 					% is there a `:- pragma reserve_tag'
 					% pragma for this type?
 			du_type_reserved_tag	:: bool,
 
-					% should the `any' inst be considered
-					% `bound' for this type?
-			du_type_is_solver_type	:: is_solver_type,
-
 					% are there `:- pragma foreign' type
 					% declarations for this type?
 			du_type_is_foreign_type	:: maybe(foreign_type_body)
 		)
 	;	eqv_type(type)
-	;	foreign_type(foreign_type_body, is_solver_type)
+			% Optional user-defined equality and comparison preds,
+			% but no solver_type_details.
+	;	foreign_type(foreign_type_body)
+			% Optional user-defined equality and comparison preds,
+			% and must have solver_type_details.
+	;	solver_type(special_type_details)
 	;	abstract_type(is_solver_type).
 
 :- type foreign_type_body
@@ -171,10 +173,13 @@
 
 :- type foreign_type_lang_body(T) == maybe(foreign_type_lang_data(T)).
 
+	% Foreign types may have user-defined equality and comparison
+	% preds, but not solver_type_details.
+	%
 :- type foreign_type_lang_data(T)
 	--->	foreign_type_lang_data(
 			T,
-			maybe(unify_compare),
+			special_type_details,
 			list(foreign_type_assertion)
 		).
 
Index: hlds_module.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_module.m,v
retrieving revision 1.101
diff -u -r1.101 hlds_module.m
--- hlds_module.m	14 Jun 2004 04:16:07 -0000	1.101
+++ hlds_module.m	30 Jun 2004 06:47:33 -0000
@@ -1942,7 +1942,7 @@
                 % Undefined/invalid pred or func.
 		% the type-checker should ensure that this never happens
 		list__length(ArgTypes, Arity),
-		PredOrFuncStr = pred_or_func_to_str(PredOrFunc),
+		PredOrFuncStr = prog_out__pred_or_func_to_str(PredOrFunc),
 		prog_out__sym_name_to_string(SymName, Name2),
 		string__int_to_string(Arity, ArityString),
 		string__append_list(["get_pred_id_and_proc_id: ",
@@ -1962,7 +1962,7 @@
 		Name = pred_info_name(PredInfo),
 		PredOrFunc = pred_info_is_pred_or_func(PredInfo),
 		Arity = pred_info_arity(PredInfo),
-		PredOrFuncStr = pred_or_func_to_str(PredOrFunc),
+		PredOrFuncStr = prog_out__pred_or_func_to_str(PredOrFunc),
 		string__int_to_string(Arity, ArityString),
 		( ProcIds = [] ->
 			string__append_list([
Index: hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.336
diff -u -r1.336 hlds_out.m
--- hlds_out.m	30 Jun 2004 02:48:00 -0000	1.336
+++ hlds_out.m	14 Jul 2004 05:41:38 -0000
@@ -435,10 +435,10 @@
 		Str = "`" ++ PromiseStr ++ "' declaration"
 	;
 		Promise = none,
-		PredOrFuncStr = pred_or_func_to_full_str(PredOrFunc),
+		PredOrFuncStr = prog_out__pred_or_func_to_full_str(PredOrFunc),
 		hlds_out__simple_call_id_to_sym_name_and_arity(
 			PredOrFunc - Name/Arity, SymArity),
-		sym_name_and_arity_to_string(SymArity, SymArityStr),
+		SymArityStr = prog_out__sym_name_and_arity_to_string(SymArity),
 		Str = PredOrFuncStr ++ " `" ++ SymArityStr ++ "'"
 	).
 
@@ -470,7 +470,7 @@
 hlds_out__generic_call_id_to_string(higher_order(Purity, PredOrFunc, _)) =
 	purity_prefix_to_string(Purity)
 		++ "higher-order "
-		++ pred_or_func_to_full_str(PredOrFunc)
+		++ prog_out__pred_or_func_to_full_str(PredOrFunc)
 		++ " call".
 hlds_out__generic_call_id_to_string(class_method(_ClassId, MethodId)) =
 	hlds_out__simple_call_id_to_string(MethodId).
@@ -553,7 +553,8 @@
 		% Make error messages for higher-order calls
 		% such as `P(A, B)' clearer.
 		Main = "argument " ++ int_to_string(ArgNum),
-		PredOrFuncStr = pred_or_func_to_full_str(PredOrFunc),
+		PredOrFuncStr =
+			prog_out__pred_or_func_to_full_str(PredOrFunc),
 		( ArgNum = 1 ->
 			Expl = "the " ++ PredOrFuncStr ++ " term"
 		;
@@ -2223,7 +2224,7 @@
 	io__write_string(UpdateName, !IO),
 	io__write_string("(", !IO),
 	CallId = PredOrFunc - _,
-	PredOrFuncStr = pred_or_func_to_str(PredOrFunc),
+	PredOrFuncStr = prog_out__pred_or_func_to_str(PredOrFunc),
 	io__write_string(PredOrFuncStr, !IO),
 	io__write_string(" ", !IO),
 	hlds_out__simple_call_id_to_sym_name_and_arity(CallId, SymArity),
@@ -3059,9 +3060,8 @@
 
 	hlds_out__write_indent(Indent, !IO),
 	(
-		( TypeBody ^ du_type_is_solver_type = solver_type
+		( TypeBody = solver_type(_)
 		; TypeBody = abstract_type(solver_type)
-		; TypeBody = foreign_type(_, solver_type)
 		)
 	->
 		io__write_string(":- solver type ", !IO)
@@ -3081,32 +3081,32 @@
 :- pred hlds_out__write_type_params(tvarset::in, list(type_param)::in,
 	io::di, io::uo) is det.
 
-hlds_out__write_type_params(_Tvarset, [], !IO).
-hlds_out__write_type_params(Tvarset, [P], !IO) :-
+hlds_out__write_type_params(_TVarSet, [], !IO).
+hlds_out__write_type_params(TVarSet, [P], !IO) :-
 	io__write_string("(", !IO),
-	term_io__write_term(Tvarset, P, !IO),
+	term_io__write_term(TVarSet, P, !IO),
 	io__write_string(")", !IO).
-hlds_out__write_type_params(Tvarset, [P | Ps], !IO) :-
+hlds_out__write_type_params(TVarSet, [P | Ps], !IO) :-
 	Ps = [_ | _],
 	io__write_string("(", !IO),
-	term_io__write_term(Tvarset, P, !IO),
-	hlds_out__write_type_params_2(Tvarset, Ps, !IO).
+	term_io__write_term(TVarSet, P, !IO),
+	hlds_out__write_type_params_2(TVarSet, Ps, !IO).
 
 :- pred hlds_out__write_type_params_2(tvarset::in, list(type_param)::in,
 	io::di, io::uo) is det.
 
-hlds_out__write_type_params_2(_Tvarset, [], !IO) :-
+hlds_out__write_type_params_2(_TVarSet, [], !IO) :-
 	io__write_string(")", !IO).
-hlds_out__write_type_params_2(Tvarset, [P | Ps], !IO) :-
+hlds_out__write_type_params_2(TVarSet, [P | Ps], !IO) :-
 	io__write_string(", ", !IO),
-	term_io__write_term(Tvarset, P, !IO),
-	hlds_out__write_type_params_2(Tvarset, Ps, !IO).
+	term_io__write_term(TVarSet, P, !IO),
+	hlds_out__write_type_params_2(TVarSet, Ps, !IO).
 
 :- pred hlds_out__write_type_body(int::in, tvarset::in, hlds_type_body::in,
 	io::di, io::uo) is det.
 
-hlds_out__write_type_body(Indent, Tvarset, du_type(Ctors, Tags, Enum,
-		MaybeEqualityPred, ReservedTag, _IsSolverType, Foreign),
+hlds_out__write_type_body(Indent, TVarSet, du_type(Ctors, Tags, Enum,
+			SpecialTypeDetails, ReservedTag, Foreign),
 		!IO) :-
 	io__write_string(" --->\n", !IO),
 	(
@@ -3123,33 +3123,8 @@
 	;
 		ReservedTag = no
 	),
-	hlds_out__write_constructors(Indent, Tvarset, Ctors, Tags, !IO),
-	( MaybeEqualityPred = yes(unify_compare(MaybeEq, MaybeCompare)) ->
-		io__write_string("\n", !IO),
-		hlds_out__write_indent(Indent + 1, !IO),
-		io__write_string("where ", !IO),
-		(
-			MaybeEq = yes(Eq),
-			io__write_string("equality is ", !IO),
-			prog_out__write_sym_name(Eq, !IO),
-			( MaybeCompare = yes(_) ->
-				io__write_string(", ", !IO)
-			;
-				true
-			)
-		;
-			MaybeEq = no
-		),
-		(
-			MaybeCompare = yes(Compare),
-			io__write_string("comparison is ", !IO),
-			prog_out__write_sym_name(Compare, !IO)
-		;
-			MaybeCompare = no
-		)
-	;
-		true
-	),
+	hlds_out__write_constructors(Indent, TVarSet, Ctors, Tags, !IO),
+	mercury_output_special_type_details(TVarSet, SpecialTypeDetails, !IO),
 	(
 		Foreign = yes(_),
 		hlds_out__write_indent(Indent, !IO),
@@ -3159,57 +3134,63 @@
 	),
 	io__write_string(".\n", !IO).
 
-hlds_out__write_type_body(_Indent, Tvarset, eqv_type(Type), !IO) :-
+hlds_out__write_type_body(_Indent, TVarSet, eqv_type(Type), !IO) :-
 	io__write_string(" == ", !IO),
-	term_io__write_term(Tvarset, Type, !IO),
+	term_io__write_term(TVarSet, Type, !IO),
 	io__write_string(".\n", !IO).
 
-hlds_out__write_type_body(_Indent, _Tvarset, abstract_type(_IsSolverType),
+hlds_out__write_type_body(_Indent, _TVarSet, abstract_type(_IsSolverType),
 		!IO) :-
 	io__write_string(".\n", !IO).
 
-hlds_out__write_type_body(_Indent, _Tvarset, foreign_type(_, _), !IO) :-
+hlds_out__write_type_body(_Indent, _TVarSet, foreign_type(_), !IO) :-
 	% XXX
 	io__write_string(" == $foreign_type.\n", !IO).
 
+hlds_out__write_type_body(_Indent, TVarSet, solver_type(SpecialTypeDetails),
+		!IO) :-
+	mercury_output_special_type_details(TVarSet, SpecialTypeDetails, !IO),
+	io__write_string(".\n", !IO).
+
+
 :- pred hlds_out__write_constructors(int::in, tvarset::in,
 	list(constructor)::in, cons_tag_values::in, io::di, io::uo) is det.
 
-hlds_out__write_constructors(_Indent, _Tvarset, [], _, !IO) :-
+hlds_out__write_constructors(_Indent, _TVarSet, [], _, !IO) :-
 	error("hlds_out__write_constructors: empty constructor list?").
-hlds_out__write_constructors(Indent, Tvarset, [C], TagValues, !IO) :-
+hlds_out__write_constructors(Indent, TVarSet, [C], TagValues, !IO) :-
 	hlds_out__write_indent(Indent, !IO),
 	io__write_char('\t', !IO),
-	hlds_out__write_ctor(C, Tvarset, TagValues, !IO).
-hlds_out__write_constructors(Indent, Tvarset, [C | Cs], TagValues, !IO) :-
+	hlds_out__write_ctor(C, TVarSet, TagValues, !IO).
+hlds_out__write_constructors(Indent, TVarSet, [C | Cs], TagValues, !IO) :-
 	Cs = [_ | _],
 	hlds_out__write_indent(Indent, !IO),
 	io__write_char('\t', !IO),
-	hlds_out__write_ctor(C, Tvarset, TagValues, !IO),
+	hlds_out__write_ctor(C, TVarSet, TagValues, !IO),
 	io__write_string("\n", !IO),
-	hlds_out__write_constructors_2(Indent, Tvarset, Cs, TagValues, !IO).
+	hlds_out__write_constructors_2(Indent, TVarSet, Cs, TagValues, !IO).
 
 :- pred hlds_out__write_constructors_2(int::in, tvarset::in,
 	list(constructor)::in, cons_tag_values::in, io::di, io::uo) is det.
 
-hlds_out__write_constructors_2(_Indent, _Tvarset, [], _, !IO).
-hlds_out__write_constructors_2(Indent, Tvarset, [C | Cs], TagValues, !IO) :-
+hlds_out__write_constructors_2(_Indent, _TVarSet, [], _, !IO).
+hlds_out__write_constructors_2(Indent, TVarSet, [C | Cs], TagValues, !IO) :-
 	hlds_out__write_indent(Indent, !IO),
 	io__write_string(";\t", !IO),
-	hlds_out__write_ctor(C, Tvarset, TagValues, !IO),
+	hlds_out__write_ctor(C, TVarSet, TagValues, !IO),
 	( Cs = [] ->
 		true
 	;
 		io__write_string("\n", !IO),
-		hlds_out__write_constructors_2(Indent, Tvarset, Cs, TagValues,
+		hlds_out__write_constructors_2(Indent, TVarSet, Cs, TagValues,
 			!IO)
 	).
 
 :- pred hlds_out__write_ctor(constructor::in, tvarset::in,
 	cons_tag_values::in, io::di, io::uo) is det.
 
-hlds_out__write_ctor(C, Tvarset, TagValues, !IO) :-
-	mercury_output_ctor(C, Tvarset, !IO),
+hlds_out__write_ctor(C, TVarSet, TagValues, !IO) :-
+	mercury_output_ctor(C, TVarSet, !IO),
 	C = ctor(_, _, Name, Args),
 	ConsId = make_cons_id_from_qualified_sym_name(Name, Args),
 	( map__search(TagValues, ConsId, TagValue) ->
Index: inst_match.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_match.m,v
retrieving revision 1.58
diff -u -r1.58 inst_match.m
--- inst_match.m	14 Jun 2004 04:16:09 -0000	1.58
+++ inst_match.m	2 Jul 2004 03:44:59 -0000
@@ -10,6 +10,9 @@
 % This module defines some utility routines for comparing insts
 % that are used by modes.m and det_analysis.m.
 %
+% rafe: XXX The following comment needs revising in the light of
+% the new solver types design.
+%
 % The handling of `any' insts is not complete.  (See also inst_util.m)
 % It would be nice to allow `free' to match `any', but right now we
 % only allow a few special cases of that.
@@ -269,6 +272,9 @@
 :- pred inst_is_free(module_info, inst).
 :- mode inst_is_free(in, in) is semidet.
 
+:- pred inst_is_any(module_info, inst).
+:- mode inst_is_any(in, in) is semidet.
+
 :- pred inst_list_is_free(list(inst), module_info).
 :- mode inst_list_is_free(in, in) is semidet.
 
@@ -1281,6 +1287,15 @@
 inst_is_free(ModuleInfo, defined_inst(InstName)) :-
         inst_lookup(ModuleInfo, InstName, Inst),
         inst_is_free(ModuleInfo, Inst).
+
+inst_is_any(_, any(_)).
+inst_is_any(_, inst_var(_)) :-
+        error("internal error: uninstantiated inst parameter").
+inst_is_any(ModuleInfo, constrained_inst_vars(_, Inst)) :-
+	inst_is_any(ModuleInfo, Inst).
+inst_is_any(ModuleInfo, defined_inst(InstName)) :-
+        inst_lookup(ModuleInfo, InstName, Inst),
+        inst_is_any(ModuleInfo, Inst).
 
         % inst_is_bound succeeds iff the inst passed is not `free'
         % or is a user-defined inst which is not defined as `free'.
Index: inst_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_util.m,v
retrieving revision 1.29
diff -u -r1.29 inst_util.m
--- inst_util.m	14 Jun 2004 04:16:10 -0000	1.29
+++ inst_util.m	28 Jun 2004 06:59:42 -0000
@@ -33,7 +33,6 @@
 % `bound', `ground', and `any' are all represented the same way.
 % That works fine for the CLP(R) interface but might not be ideal
 % in the general case.
-
 %-----------------------------------------------------------------------------%
 
 :- module check_hlds__inst_util.
@@ -128,6 +127,13 @@
 
 %-----------------------------------------------------------------------------%
 
+	% inst_contains_unconstrained_var(Inst) iff Inst includes an
+	% unconstrained inst variable.
+	%
+:- pred inst_contains_unconstrained_var((inst)::in) is semidet.
+
+%-----------------------------------------------------------------------------%
+
 :- implementation.
 
 :- import_module check_hlds__det_analysis.
@@ -1140,6 +1146,7 @@
 maybe_make_shared_inst_list([_|_], [], _, _, _) :-
 	error("maybe_make_shared_inst_list: length mismatch").
 
+
 make_shared_inst_list([], ModuleInfo, [], ModuleInfo).
 make_shared_inst_list([Inst0 | Insts0], ModuleInfo0,
 		[Inst | Insts], ModuleInfo) :-
@@ -1408,6 +1415,7 @@
 		inst_merge_2(InstA, InstB, MaybeType, ModuleInfo1, Inst0,
 			ModuleInfo2),
 
+
 			% now update the value associated with ThisInstPair
 		module_info_insts(ModuleInfo2, InstTable2),
 		inst_table_get_merge_insts(InstTable2, MergeInstTable2),
@@ -1798,5 +1806,67 @@
 	in_mode(InMode),
 	out_mode(OutMode),
 	ArgModes = list__duplicate(Arity - 1, InMode) ++ [OutMode].
+
+%-----------------------------------------------------------------------------%
+
+inst_contains_unconstrained_var(bound(_Uniqueness, BoundInsts)) :-
+	member(BoundInst, BoundInsts),
+	BoundInst = functor(_ConsId, ArgInsts),
+	member(ArgInst, ArgInsts),
+	inst_contains_unconstrained_var(ArgInst).
+
+inst_contains_unconstrained_var(ground(_Uniqueness, GroundInstInfo)) :-
+	GroundInstInfo = higher_order(PredInstInfo),
+	PredInstInfo = pred_inst_info(_PredOrFunc, Modes, _Detism),
+	member(Mode, Modes),
+	(
+		Mode = (Inst -> _)
+	;
+		Mode = (_ -> Inst)
+	;
+		Mode = user_defined_mode(_SymName, Insts),
+		member(Inst, Insts)
+	),
+	inst_contains_unconstrained_var(Inst).
+
+inst_contains_unconstrained_var(inst_var(_InstVar)).
+
+inst_contains_unconstrained_var(defined_inst(InstName)) :-
+	(
+		InstName = user_inst(_, Insts),
+		member(Inst, Insts),
+		inst_contains_unconstrained_var(Inst)
+	;
+		InstName = merge_inst(Inst, _),
+		inst_contains_unconstrained_var(Inst)
+	;
+		InstName = merge_inst(_, Inst),
+		inst_contains_unconstrained_var(Inst)
+	;
+		InstName = unify_inst(_, Inst, _, _),
+		inst_contains_unconstrained_var(Inst)
+	;
+		InstName = unify_inst(_, _, Inst, _),
+		inst_contains_unconstrained_var(Inst)
+	;
+		InstName = ground_inst(InstName1, _, _, _),
+		inst_contains_unconstrained_var(defined_inst(InstName1))
+	;
+		InstName = any_inst(InstName1, _, _, _),
+		inst_contains_unconstrained_var(defined_inst(InstName1))
+	;
+		InstName = shared_inst(InstName1),
+		inst_contains_unconstrained_var(defined_inst(InstName1))
+	;
+		InstName = mostly_uniq_inst(InstName1),
+		inst_contains_unconstrained_var(defined_inst(InstName1))
+	;
+		InstName = typed_inst(_, InstName1),
+		inst_contains_unconstrained_var(defined_inst(InstName1))
+	).
+
+inst_contains_unconstrained_var(abstract_inst(_SymName, Insts)) :-
+	member(Inst, Insts),
+	inst_contains_unconstrained_var(Inst).
 
 %-----------------------------------------------------------------------------%
Index: intermod.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/intermod.m,v
retrieving revision 1.161
diff -u -r1.161 intermod.m
--- intermod.m	14 Jun 2004 04:16:10 -0000	1.161
+++ intermod.m	1 Jul 2004 02:42:54 -0000
@@ -993,7 +993,7 @@
 		hlds_data__get_type_defn_body(TypeDefn0, TypeBody0),
 		(
 			TypeBody0 = du_type(Ctors, Tags, Enum,
-				MaybeUserEqComp0, ReservedTag, IsSolverType,
+				SpecialTypeDetails0, ReservedTag,
 				MaybeForeign0)
 		->
 			module_info_globals(ModuleInfo, Globals),
@@ -1021,20 +1021,21 @@
 					ModuleInfo, TypeCtor, ForeignTypeBody0,
 					ForeignTypeBody, !Info),
 				MaybeForeign = yes(ForeignTypeBody),
-				MaybeUserEqComp = MaybeUserEqComp0
+				SpecialTypeDetails = SpecialTypeDetails0
 			;
 				intermod__resolve_unify_compare_overloading(
-					ModuleInfo, TypeCtor, MaybeUserEqComp0,
-					MaybeUserEqComp, !Info),
+					ModuleInfo, TypeCtor,
+					SpecialTypeDetails0,
+					SpecialTypeDetails, !Info),
 				MaybeForeign = MaybeForeign0
 			),
-			TypeBody = du_type(Ctors, Tags, Enum, MaybeUserEqComp,
-				ReservedTag, IsSolverType, MaybeForeign),
+			TypeBody = du_type(Ctors, Tags, Enum,
+				SpecialTypeDetails, ReservedTag,
+				MaybeForeign),
 			hlds_data__set_type_defn_body(TypeBody,
 				TypeDefn0, TypeDefn)
 		;
-			TypeBody0 = foreign_type(ForeignTypeBody0,
-				IsSolverType)
+			TypeBody0 = foreign_type(ForeignTypeBody0)
 		->
 			% The header code must be written since
 			% it could be used by the foreign type.
@@ -1042,7 +1043,7 @@
 			intermod__resolve_foreign_type_body_overloading(
 				ModuleInfo, TypeCtor,
 				ForeignTypeBody0, ForeignTypeBody, !Info),
-			TypeBody = foreign_type(ForeignTypeBody, IsSolverType),
+			TypeBody = foreign_type(ForeignTypeBody),
 			hlds_data__set_type_defn_body(TypeBody,
 				TypeDefn0, TypeDefn)
 		;
@@ -1100,29 +1101,34 @@
 
 intermod__resolve_foreign_type_body_overloading_2(_, _, no, no, !Info).
 intermod__resolve_foreign_type_body_overloading_2(ModuleInfo, TypeCtor,
-		yes(foreign_type_lang_data(Body, MaybeEqComp0, Assertions)),
-		yes(foreign_type_lang_data(Body, MaybeEqComp, Assertions)),
+		yes(foreign_type_lang_data(Body, SpecialTypeDetails0,
+			Assertions)),
+		yes(foreign_type_lang_data(Body, SpecialTypeDetails,
+			Assertions)),
 		!Info) :-
 	intermod__resolve_unify_compare_overloading(ModuleInfo, TypeCtor,
-		MaybeEqComp0, MaybeEqComp, !Info).
+		SpecialTypeDetails0, SpecialTypeDetails, !Info).
 
 :- pred intermod__resolve_unify_compare_overloading(module_info::in,
-	type_ctor::in, maybe(unify_compare)::in, maybe(unify_compare)::out,
+	type_ctor::in, special_type_details::in, special_type_details::out,
 	intermod_info::in, intermod_info::out) is det.
 
-intermod__resolve_unify_compare_overloading(_, _, no, no, !Info).
-intermod__resolve_unify_compare_overloading(_, _,
-		yes(abstract_noncanonical_type),
-		yes(abstract_noncanonical_type),
-		!Info).
 intermod__resolve_unify_compare_overloading(ModuleInfo, TypeCtor,
-		yes(unify_compare(MaybeUserEq0, MaybeUserCompare0)),
-		yes(unify_compare(MaybeUserEq, MaybeUserCompare)),
-		!Info) :-
-	intermod__resolve_user_special_pred_overloading(ModuleInfo,
-		unify, TypeCtor, MaybeUserEq0, MaybeUserEq, !Info),
-	intermod__resolve_user_special_pred_overloading(ModuleInfo,
-		compare, TypeCtor, MaybeUserCompare0, MaybeUserCompare, !Info).
+		SpecialTypeDetails0, SpecialTypeDetails, !Info) :-
+	(
+		MaybeUnify0 = SpecialTypeDetails0 ^ unify,
+		MaybeCompare0 = SpecialTypeDetails0 ^ unify
+	->
+		intermod__resolve_user_special_pred_overloading(ModuleInfo,
+			unify, TypeCtor, MaybeUnify0, MaybeUnify, !Info),
+		intermod__resolve_user_special_pred_overloading(ModuleInfo,
+			compare, TypeCtor, MaybeCompare0, MaybeCompare, !Info),
+		SpecialTypeDetails =
+			((SpecialTypeDetails0 ^ unify   := MaybeUnify  )
+					      ^ compare := MaybeCompare)
+	;
+		SpecialTypeDetails = SpecialTypeDetails0
+	).
 
 :- pred intermod__resolve_user_special_pred_overloading(module_info::in,
 	special_pred_id::in, type_ctor::in, maybe(sym_name)::in,
@@ -1273,9 +1279,8 @@
 	TypeCtor = Name - Arity,
 	(
 		Ctors = Body ^ du_type_ctors,
-		IsSolverType = Body ^ du_type_is_solver_type,
-		MaybeEqualityPred = Body ^ du_type_usereq,
-		TypeBody = du_type(Ctors, IsSolverType, MaybeEqualityPred)
+		SpecialTypeDetails = Body ^ du_type_special_type_details,
+		TypeBody = du_type(Ctors, SpecialTypeDetails)
 	;
 		Body = eqv_type(EqvType),
 		TypeBody = eqv_type(EqvType)
@@ -1283,15 +1288,18 @@
 		Body = abstract_type(IsSolverType),
 		TypeBody = abstract_type(IsSolverType)
 	;
-		Body = foreign_type(_, IsSolverType),
-		TypeBody = abstract_type(IsSolverType)
+		Body = foreign_type(_),
+		TypeBody = abstract_type(non_solver_type)
+	;
+		Body = solver_type(SolverTypeDetails),
+		TypeBody = solver_type(SolverTypeDetails)
 	),
 	mercury_output_item(
 		type_defn(VarSet, Name, Args, TypeBody, true),
 		Context, !IO),
 
 	(
-		( Body = foreign_type(ForeignTypeBody, _)
+		( Body = foreign_type(ForeignTypeBody)
 		; Body ^ du_type_is_foreign_type = yes(ForeignTypeBody)
 		),
 		ForeignTypeBody = foreign_type_body(MaybeIL, MaybeC,
@@ -1300,11 +1308,12 @@
 		(
 			MaybeIL = yes(DataIL),
 			DataIL = foreign_type_lang_data(ILForeignType,
-				ILUserEqComp, AssertionsIL),
+				ILSpecialTypeDetails, AssertionsIL),
 			mercury_output_item(
 				type_defn(VarSet, Name, Args,
 					foreign_type(il(ILForeignType),
-						ILUserEqComp, AssertionsIL),
+						ILSpecialTypeDetails,
+						AssertionsIL),
 				true),
 				Context, !IO)
 		;
@@ -1313,11 +1322,12 @@
 		(
 			MaybeC = yes(DataC),
 			DataC = foreign_type_lang_data(CForeignType,
-				CUserEqComp, AssertionsC),
+				CSpecialTypeDetails, AssertionsC),
 			mercury_output_item(
 				type_defn(VarSet, Name, Args,
 					foreign_type(c(CForeignType),
-						CUserEqComp, AssertionsC),
+						CSpecialTypeDetails,
+						AssertionsC),
 					true),
 				Context, !IO)
 		;
@@ -1326,11 +1336,12 @@
 		(
 			MaybeJava = yes(DataJava),
 			DataJava = foreign_type_lang_data(JavaForeignType,
-				JavaUserEqComp, AssertionsJava),
+				JavaSpecialTypeDetails, AssertionsJava),
 			mercury_output_item(
 				type_defn(VarSet, Name, Args,
 					foreign_type(java(JavaForeignType),
-						JavaUserEqComp, AssertionsJava),
+						JavaSpecialTypeDetails,
+						AssertionsJava),
 					true),
 				Context, !IO)
 		;
Index: magic_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/magic_util.m,v
retrieving revision 1.40
diff -u -r1.40 magic_util.m
--- magic_util.m	30 Jun 2004 02:48:03 -0000	1.40
+++ magic_util.m	14 Jul 2004 05:41:39 -0000
@@ -1384,15 +1384,17 @@
 	set(argument_error)::in, set(argument_error)::out,
 	magic_info::in, magic_info::out) is det.
 
-magic_util__check_type_defn(du_type(Ctors, _, _, _, _, _, _),
+magic_util__check_type_defn(du_type(Ctors, _, _, _, _, _),
 		Parents, Errors0, Errors) -->
 	list__foldl2(magic_util__check_ctor(Parents), Ctors, Errors0, Errors).
 magic_util__check_type_defn(eqv_type(_), _, _, _) -->
 	{ error("magic_util__check_type_defn: eqv_type") }.
 magic_util__check_type_defn(abstract_type(_), _, Errors0, Errors) -->
 	{ set__insert(Errors0, abstract, Errors) }.
-magic_util__check_type_defn(foreign_type(_, _), _, _, _) -->
+magic_util__check_type_defn(foreign_type(_), _, _, _) -->
 	{ error("magic_util__check_type_defn: foreign_type") }.
+magic_util__check_type_defn(solver_type(_), _, _, _) -->
+	{ error("magic_util__check_type_defn: solver_type") }.
 
 :- pred magic_util__check_ctor(set(type_ctor)::in, constructor::in,
 	set(argument_error)::in, set(argument_error)::out,
Index: make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.474
diff -u -r1.474 make_hlds.m
--- make_hlds.m	14 Jul 2004 05:37:03 -0000	1.474
+++ make_hlds.m	16 Jul 2004 06:01:31 -0000
@@ -323,7 +323,29 @@
 	% skip clauses
 add_item_decl_pass_1(clause(_, _, _, _, _), _, !Status, !Module, no, !IO).
 
-add_item_decl_pass_1(type_defn(_, _, _, _, _), _, !Status, !Module, no, !IO).
+	% If this is a solver type then we need to also add the declarations
+	% for the compiler generated construction function and deconstruction
+	% predicate for the special constrained data constructor.
+	%
+	% In pass 3 we add the corresponding clauses.
+	%
+	% Before switch detection, we turn calls to these functions/predicates
+	% into ordinary constructions/deconstructions, but preserve the
+	% corresponding impurity annotations.
+	%
+add_item_decl_pass_1(
+		type_defn(TVarSet, SymName, TypeParams, TypeDefn, _Cond),
+		Context, !Status, !Module, no, !IO) :-
+	(
+		TypeDefn = solver_type(SpecialTypeDetails),
+		SpecialTypeDetails ^ solver_type_details =
+			yes(SolverTypeDetails)
+	->
+		add_solver_type_decl_items(TVarSet, SymName, TypeParams,
+			SolverTypeDetails, Context, !Status, !Module, !IO)
+	;
+		true
+	).
 
 add_item_decl_pass_1(inst_defn(VarSet, Name, Params, InstDefn, Cond), Context,
 		!Status, !Module, InvalidMode, !IO) :-
@@ -432,6 +454,202 @@
 
 %-----------------------------------------------------------------------------%
 
+	% A solver type t defined with
+	%
+	% :- solver type st
+	% 	where representation is rt,		% type
+	% 	      initialisation is ip,		% pred
+	% 	      ground         is gi,		% inst
+	% 	      any            is ai, ...		% inst
+	%
+	% causes the following to be introduced:
+	%
+	% :- impure func 'representation of st'(st)      = rt.
+	% :-        mode 'representation of st'(in)      = out(gi) is det.
+	% :-        mode 'representation of st'(in(any)) = out(ai) is det.
+	%
+	% :- impure func 'representation to ground st'(rt::in(gi)) =
+	% 			(st::out) is det.
+	% :- impure func 'representation to any st'(rt::in(ai)) =
+	% 			(st::out(any)) is det.
+	%
+	% We need two 'representation to ...' functions because
+	% having a single, two-moded conversion function would
+	% lead to the compiler issuing a `duplicate mode declaration'
+	% error in the case that gi = ai.
+	%
+:- pred add_solver_type_decl_items(
+		tvarset::in, sym_name::in, list(type_param)::in,
+		solver_type_details::in, prog_context::in,
+		item_status::in, item_status::out,
+		module_info::in, module_info::out, io::di, io::uo) is det.
+
+add_solver_type_decl_items(TVarSet, TypeSymName, TypeParams,
+		SolverTypeDetails, Context, !Status, !Module, !IO) :-
+
+	SolverType        = sym_name_and_args_to_term(TypeSymName,
+				TypeParams, Context),
+	Arity             = length(TypeParams),
+
+	RepnType          = SolverTypeDetails ^ representation_type,
+	AnyInst           = SolverTypeDetails ^ any_inst,
+	GroundInst        = SolverTypeDetails ^ ground_inst,
+
+	InAnyMode         = in_mode(AnyInst),
+	InGroundMode      = in_mode(GroundInst),
+
+	OutAnyMode        = out_mode(AnyInst),
+	OutGroundMode     = out_mode(GroundInst),
+
+	InstVarSet        = varset__init,
+	ExistQTVars       = [],
+
+	% Insert the conversion function declarations.
+
+		% The `:- impure func 'representation of st'(st) = rt'
+		% declaration.
+		%
+	ToRepnSymName     = solver_to_repn_symname(TypeSymName, Arity),
+	ToRepnArgTypes    = [type_only(SolverType), type_only(RepnType)],
+	ToRepnTypeSigItem =
+		pred_or_func(TVarSet, InstVarSet, ExistQTVars,
+			function,
+			ToRepnSymName,
+			ToRepnArgTypes,
+			no,	/* no `with_type` ... */
+			no,	/* no `with_inst` ... */
+			no,	/* no determinism */
+			true,	/* no `where ...' */
+			(impure), 
+			constraints([], []) /* no type class constraints */
+		),
+	add_item_decl_pass_1(ToRepnTypeSigItem, Context,
+		!Status, !Module, _, !IO),
+
+		% The `:- mode 'representation of st'(in) = out(gi) is det'
+		% declaration.
+		%
+	ToGroundRepnArgModes  = [in_mode, OutGroundMode],
+	ToGroundRepnModeItem =
+		pred_or_func_mode(InstVarSet,
+			yes(function),
+			ToRepnSymName,
+			ToGroundRepnArgModes,
+			no,	/* no `with_inst` ... */
+			yes(det),
+			true	/* no `where ...' */
+		),
+	add_item_decl_pass_1(ToGroundRepnModeItem, Context,
+		!Status, !Module, _, !IO),
+
+		% The `:- mode 'representation of st'(in(any)) =
+		% 			out(ai) is det' declaration.
+		%
+	ToAnyRepnArgModes  = [in_any_mode, OutAnyMode],
+	ToAnyRepnModeItem =
+		pred_or_func_mode(InstVarSet,
+			yes(function),
+			ToRepnSymName,
+			ToAnyRepnArgModes,
+			no,	/* no `with_inst` ... */
+			yes(det),
+			true	/* no `where ...' */
+		),
+	add_item_decl_pass_1(ToAnyRepnModeItem, Context,
+		!Status, !Module, _, !IO),
+
+		% The `:- impure
+		%	func 'representation to ground st'(rt::in(gi)) =
+		% 			(st::out) is det' declaration.
+		%
+	FromGroundRepnSymName     =
+		repn_to_ground_solver_symname(TypeSymName, Arity),
+	FromGroundRepnArgTypes    =
+		[type_and_mode(RepnType,   InGroundMode   ),
+		 type_and_mode(SolverType, out_mode       )],
+	FromGroundRepnTypeSigItem =
+		pred_or_func(TVarSet, InstVarSet, ExistQTVars,
+			function,
+			FromGroundRepnSymName,
+			FromGroundRepnArgTypes,
+			no,	/* no `with_type` ... */
+			no,	/* no `with_inst` ... */
+			yes(det),
+			true,	/* no `where ...' */
+			(impure), 
+			constraints([], []) /* no type class constraints */
+		),
+	add_item_decl_pass_1(FromGroundRepnTypeSigItem, Context,
+		!Status, !Module, _, !IO),
+
+		% The `:- impure
+		%	func 'representation to any st'(rt::in(ai)) =
+		% 			(st::out(any)) is det' declaration.
+		%
+	FromAnyRepnSymName     =
+		repn_to_any_solver_symname(TypeSymName, Arity),
+	FromAnyRepnArgTypes    =
+		[type_and_mode(RepnType,   InAnyMode   ),
+		 type_and_mode(SolverType, out_any_mode)],
+	FromAnyRepnTypeSigItem =
+		pred_or_func(TVarSet, InstVarSet, ExistQTVars,
+			function,
+			FromAnyRepnSymName,
+			FromAnyRepnArgTypes,
+			no,	/* no `with_type` ... */
+			no,	/* no `with_inst` ... */
+			yes(det),
+			true,	/* no `where ...' */
+			(impure), 
+			constraints([], []) /* no type class constraints */
+		),
+	add_item_decl_pass_1(FromAnyRepnTypeSigItem, Context,
+		!Status, !Module, _, !IO).
+
+%-----------------------------------------------------------------------------%
+
+	% Obtain the solver type conversion function sym_names from
+	% the solver type sym_name.
+	%
+:- func solver_to_repn_symname(sym_name, arity) = sym_name.
+
+solver_to_repn_symname(unqualified(Name), Arity) =
+	unqualified(
+		"representation of " ++ Name ++ "/" ++ int_to_string(Arity)
+	).
+solver_to_repn_symname(qualified(ModuleNames, Name), Arity) =
+	qualified(ModuleNames,
+		"representation of " ++ Name ++ "/" ++ int_to_string(Arity)
+	).
+
+
+:- func repn_to_any_solver_symname(sym_name, arity) = sym_name.
+
+repn_to_any_solver_symname(SymName, Arity) =
+	repn_to_solver_symname("any", SymName, Arity).
+
+
+:- func repn_to_ground_solver_symname(sym_name, arity) = sym_name.
+
+repn_to_ground_solver_symname(SymName, Arity) =
+	repn_to_solver_symname("ground", SymName, Arity).
+
+
+:- func repn_to_solver_symname(string, sym_name, arity) = sym_name.
+
+repn_to_solver_symname(AnyOrGround, unqualified(Name), Arity) =
+	unqualified(
+		string.format("representation to %s %s/%d",
+			[s(AnyOrGround), s(Name), i(Arity)])
+	).
+repn_to_solver_symname(AnyOrGround, qualified(ModuleNames, Name), Arity) =
+	qualified(ModuleNames,
+		string.format("representation to %s %s/%d",
+			[s(AnyOrGround), s(Name), i(Arity)])
+	).
+
+%-----------------------------------------------------------------------------%
+
 	% dispatch on the different types of items
 
 :- pred add_item_decl_pass_2(item::in, prog_context::in, item_status::in,
@@ -723,10 +941,26 @@
 		!Status, Context, !Module, !Info, !IO) :-
 	check_not_exported(!.Status, Context, "clause", !IO),
 	GoalType = none,
-	% at this stage we only need know that it's not % a promise declaration
+	% at this stage we only need know that it's not a promise declaration
 	module_add_clause(VarSet, PredOrFunc, PredName, Args, Body, !.Status,
 		Context, GoalType, !Module, !Info, !IO).
-add_item_clause(type_defn(_, _, _, _, _), !Status, _, !Module, !Info, !IO).
+
+add_item_clause(type_defn(_TVarSet, SymName, TypeParams, TypeDefn, _Cond),
+		!Status, Context, !Module, !Info, !IO) :-
+	% If this is a solver type then we need to also add clauses
+	% the compiler generated inst cast predicate (the declaration
+	% for which was added in pass 1).
+	(
+		TypeDefn = solver_type(SpecialTypeDetails),
+		SpecialTypeDetails ^ solver_type_details =
+			yes(SolverTypeDetails)
+	->
+		add_solver_type_clause_items(SymName, TypeParams,
+			SolverTypeDetails, !Status, Context, !Module, !Info,
+			!IO)
+	;
+		true
+	).
 add_item_clause(inst_defn(_, _, _, _, _), !Status, _, !Module, !Info, !IO).
 add_item_clause(mode_defn(_, _, _, _, _), !Status, _, !Module, !Info, !IO).
 add_item_clause(pred_or_func(_, _, _, PredOrFunc, SymName, TypesAndModes,
@@ -870,6 +1104,151 @@
 add_item_clause(typeclass(_, _, _, _, _), !Status, _, !Module, !Info, !IO).
 add_item_clause(instance(_, _, _, _, _, _), !Status, _, !Module, !Info, !IO).
 
+
+:- pred add_solver_type_clause_items(sym_name::in, list(type_param)::in,
+		solver_type_details::in,
+		import_status::in, import_status::out, prog_context::in,
+		module_info::in, module_info::out,
+		qual_info::in, qual_info::out, io::di, io::uo) is det.
+
+add_solver_type_clause_items(TypeSymName, TypeParams, SolverTypeDetails,
+		!Status, Context, !Module, !Info, !IO) :-
+
+	Arity             = length(TypeParams),
+	ToRepnSymName     = solver_to_repn_symname(TypeSymName, Arity),
+	FromAnyRepnSymName =
+		repn_to_any_solver_symname(TypeSymName, Arity),
+	FromGroundRepnSymName =
+		repn_to_ground_solver_symname(TypeSymName, Arity),
+
+	AnyInst           = SolverTypeDetails ^ any_inst,
+	GroundInst        = SolverTypeDetails ^ ground_inst,
+
+	InAnyMode         = in_mode(AnyInst),
+	InGroundMode      = in_mode(GroundInst),
+
+	OutAnyMode        = out_mode(AnyInst),
+	OutGroundMode     = out_mode(GroundInst),
+
+	VarSet0           = varset__init,
+	varset__new_var(VarSet0, X, VarSet1),
+	varset__new_var(VarSet1, Y, VarSet),
+
+	Attrs0            = default_attributes(c),
+	set_may_call_mercury(will_not_call_mercury, Attrs0, Attrs1),
+	set_thread_safe(thread_safe,                Attrs1, Attrs2),
+	set_terminates(terminates,                  Attrs2, Attrs),
+
+	Impl              = ordinary("Y = X;", yes(Context)),
+
+		% The `func(in) = out(<i_ground>) is det' mode.
+		%
+	ToGroundRepnArgs = [ pragma_var(X, "X", in_mode      ),
+                             pragma_var(Y, "Y", OutGroundMode) ],
+	ToGroundRepnForeignProc =
+		foreign_proc(
+			Attrs,
+			ToRepnSymName,
+			function,
+			ToGroundRepnArgs,
+			VarSet,
+			Impl
+		),
+	ToGroundRepnItem = pragma(ToGroundRepnForeignProc),
+	add_item_clause(ToGroundRepnItem, !Status, Context, !Module, !Info,
+		!IO),
+
+		% The `func(in(any)) = out(<i_any>) is det' mode.
+		%
+	ToAnyRepnArgs = [ pragma_var(X, "X", in_any_mode),
+                          pragma_var(Y, "Y", OutAnyMode ) ],
+	ToAnyRepnForeignProc =
+		foreign_proc(
+			Attrs,
+			ToRepnSymName,
+			function,
+			ToAnyRepnArgs,
+			VarSet,
+			Impl
+		),
+	ToAnyRepnItem = pragma(ToAnyRepnForeignProc),
+	add_item_clause(ToAnyRepnItem, !Status, Context, !Module, !Info, !IO),
+
+		% The `func(in(<i_ground>)) = out is det' mode.
+		%
+	FromGroundRepnArgs        = [ pragma_var(X, "X", InGroundMode),
+			              pragma_var(Y, "Y", out_mode) ],
+	FromGroundRepnForeignProc =
+		foreign_proc(
+			Attrs,
+			FromGroundRepnSymName,
+			function,
+			FromGroundRepnArgs,
+			VarSet,
+			Impl
+		),
+	FromGroundRepnItem = pragma(FromGroundRepnForeignProc),
+	add_item_clause(FromGroundRepnItem, !Status, Context, !Module, !Info,
+		!IO),
+
+		% The `func(in(<i_any>)) = out(any) is det' mode.
+		%
+	FromAnyRepnArgs        = [ pragma_var(X, "X", InAnyMode   ),
+			           pragma_var(Y, "Y", out_any_mode) ],
+	FromAnyRepnForeignProc =
+		foreign_proc(
+			Attrs,
+			FromAnyRepnSymName,
+			function,
+			FromAnyRepnArgs,
+			VarSet,
+			Impl
+		),
+	FromAnyRepnItem = pragma(FromAnyRepnForeignProc),
+	add_item_clause(FromAnyRepnItem, !Status, Context, !Module, !Info,
+		!IO).
+
+%-----------------------------------------------------------------------------%
+
+	% We need to "unparse" the sym_name to construct the properly
+	% module qualified term.
+	%
+:- func sym_name_and_args_to_term(sym_name, list(term(T)), prog_context) =
+		term(T).
+
+sym_name_and_args_to_term(unqualified(Name), Xs, Context) =
+	term__functor(term__atom(Name), Xs, Context).
+
+sym_name_and_args_to_term(qualified(ModuleNames, Name), Xs, Context) =
+	sym_name_and_term_to_term(ModuleNames,
+		term__functor(term__atom(Name), Xs, Context), Context).
+
+
+:- func sym_name_and_term_to_term(module_specifier, term(T),
+		prog_context) = term(T).
+
+sym_name_and_term_to_term(unqualified(ModuleName), Term, Context) =
+	term__functor(
+		term__atom("."),
+		[ term__functor(term__atom(ModuleName), [], Context),
+		  Term ],
+		Context
+	).
+
+sym_name_and_term_to_term(qualified(ModuleNames, ModuleName), Term,
+		Context) =
+	term__functor(
+		term__atom("."),
+		[ sym_name_and_term_to_term(
+			ModuleNames,
+			term__functor(term__atom(ModuleName), [], Context),
+			Context
+		  ),
+		  Term ],
+		Context
+	).
+
+
 :- pred add_promise_clause(promise_type::in, list(term(prog_var_type))::in,
 	prog_varset::in, goal::in, prog_context::in, import_status::in,
 	module_info::in, module_info::out, qual_info::in, qual_info::out,
@@ -1006,8 +1385,7 @@
 
 		;
 			TypeBody0 = du_type(Body, _CtorTags0, _IsEnum0,
-				EqualityPred, ReservedTag0, IsSolverType,
-				IsForeign)
+				SpecialTypeDetails, ReservedTag0, IsForeign)
 		->
 			(
 				ReservedTag0 = yes,
@@ -1038,8 +1416,7 @@
 			assign_constructor_tags(Body, TypeCtor, ReservedTag,
 				Globals, CtorTags, IsEnum),
 			TypeBody = du_type(Body, CtorTags, IsEnum,
-				EqualityPred, ReservedTag, IsSolverType,
-				IsForeign),
+				SpecialTypeDetails, ReservedTag, IsForeign),
 			hlds_data__set_type_defn_body(TypeBody,
 				TypeDefn0, TypeDefn),
 			map__set(Types0, TypeCtor, TypeDefn, Types),
@@ -2099,7 +2476,7 @@
 		(
 			Body0 = abstract_type(_)
 		;
-			Body0 = du_type(_, _, _, _, _, _, _),
+			Body0 = du_type(_, _, _, _, _, _),
 			string__suffix(term__context_file(Context), ".int2")
 			% If the type definition comes from a .int2 file then
 			% we need to treat it as abstract.  The constructors
@@ -2148,7 +2525,7 @@
 		NeedQual, Context, T),
 	(
 		MaybeOldDefn = no,
-		Body = foreign_type(_, _)
+		Body = foreign_type(_)
 	->
 		TypeStr = error_util__describe_sym_name_and_arity(
 				Name / Arity),
@@ -2161,7 +2538,7 @@
 		module_info_incr_errors(!Module)
 	;
 		MaybeOldDefn = yes(OldDefn1),
-		Body = foreign_type(_, _),
+		Body = foreign_type(_),
 		hlds_data__get_type_defn_status(OldDefn1, OldStatus1),
 		hlds_data__get_type_defn_body(OldDefn1, OldBody1),
 		OldBody1 = abstract_type(_),
@@ -2195,7 +2572,7 @@
 		globals__io_get_target(Target, !IO),
 		globals__io_lookup_bool_option(make_optimization_interface,
 			MakeOptInt, !IO),
-		( Body = foreign_type(_, _) ->
+		( Body = foreign_type(_) ->
 			module_info_contains_foreign_type(!Module)
 		;
 			true
@@ -2295,26 +2672,13 @@
 	% default to having an is_solver_type field of `non_solver_type'.
 	% If another declaration for the type has a `solver' annotation then
 	% we must update the foreign_type body to reflect this.
+	%
+	% rafe: XXX think it should be an error for foreign types to
+	% be solver types.
+	%
 :- pred combine_is_solver_type(hlds_type_body::in, hlds_type_body::out,
-	hlds_type_body::in, hlds_type_body::out) is det.
-
-combine_is_solver_type(OldBody0, OldBody, Body0, Body) :-
-	(
-		OldBody0 = foreign_type(OldForeignTypeBody, non_solver_type),
-		maybe_get_body_is_solver_type(Body0, solver_type)
-	->
-		OldBody = foreign_type(OldForeignTypeBody, solver_type),
-		Body = Body0
-	;
-		maybe_get_body_is_solver_type(OldBody0, solver_type),
-		Body0 = foreign_type(ForeignTypeBody, non_solver_type)
-	->
-		OldBody = OldBody0,
-		Body = foreign_type(ForeignTypeBody, solver_type)
-	;
-		OldBody = OldBody0,
-		Body = Body0
-	).
+		hlds_type_body::in, hlds_type_body::out) is det.
+combine_is_solver_type(OldBody, OldBody, Body, Body).
 
 	% Succeed iff the two type bodies have inconsistent is_solver_type
 	% annotations.
@@ -2329,9 +2693,8 @@
 :- pred maybe_get_body_is_solver_type(hlds_type_body::in, is_solver_type::out)
 	is semidet.
 
-maybe_get_body_is_solver_type(Body, Body ^ du_type_is_solver_type).
 maybe_get_body_is_solver_type(abstract_type(IsSolverType), IsSolverType).
-maybe_get_body_is_solver_type(foreign_type(_, IsSolverType), IsSolverType).
+maybe_get_body_is_solver_type(solver_type(_), solver_type).
 
 	% check_foreign_type_visibility(OldStatus, NewDefnStatus).
 	%
@@ -2398,10 +2761,13 @@
 		Body = abstract_type(_),
 		NewFoundError = no
 	;
+		Body = solver_type(_),
+		NewFoundError = no
+	;
 		Body = eqv_type(_),
 		NewFoundError = no
 	;
-		Body = foreign_type(ForeignTypeBody, _),
+		Body = foreign_type(ForeignTypeBody),
 		check_foreign_type(TypeCtor, ForeignTypeBody, Context,
 			NewFoundError, !Module, !IO)
 	),
@@ -2504,7 +2870,7 @@
 	% if we are making the optimization interface so that it gets
 	% output in the .opt file.
 merge_foreign_type_bodies(Target, MakeOptInterface,
-		foreign_type(ForeignTypeBody0, IsSolverType), Body1, Body) :-
+		foreign_type(ForeignTypeBody0), Body1, Body) :-
 	MaybeForeignTypeBody1 = Body1 ^ du_type_is_foreign_type,
 	(
 		MaybeForeignTypeBody1 = yes(ForeignTypeBody1)
@@ -2518,17 +2884,17 @@
 		have_foreign_type_for_backend(Target, ForeignTypeBody, yes),
 		MakeOptInterface = no
 	->
-		Body = foreign_type(ForeignTypeBody, IsSolverType)
+		Body = foreign_type(ForeignTypeBody)
 	;
 		Body = Body1 ^ du_type_is_foreign_type := yes(ForeignTypeBody)
 	).
 merge_foreign_type_bodies(Target, MakeOptInterface,
-		Body0 @ du_type(_, _, _, _, _, _, _),
-		Body1 @ foreign_type(_, _), Body) :-
+		Body0 @ du_type(_, _, _, _, _, _),
+		Body1 @ foreign_type(_), Body) :-
 	merge_foreign_type_bodies(Target, MakeOptInterface, Body1, Body0, Body).
-merge_foreign_type_bodies(_, _, foreign_type(Body0, _IsSolverType0),
-		foreign_type(Body1, IsSolverType),
-		foreign_type(Body, IsSolverType)) :-
+merge_foreign_type_bodies(_, _, foreign_type(Body0),
+		foreign_type(Body1),
+		foreign_type(Body)) :-
 	merge_foreign_type_bodies_2(Body0, Body1, Body).
 
 :- pred merge_foreign_type_bodies_2(foreign_type_body::in,
@@ -2633,9 +2999,9 @@
 :- pred convert_type_defn(type_defn::in, type_ctor::in, globals::in,
 	hlds_type_body::out) is det.
 
-convert_type_defn(du_type(Body, IsSolverType, EqualityPred), TypeCtor, Globals,
-		du_type(Body, CtorTags, IsEnum, EqualityPred,
-			ReservedTagPragma, IsSolverType, IsForeign)) :-
+convert_type_defn(du_type(Body, SpecialTypeDetails), TypeCtor, Globals,
+		du_type(Body, CtorTags, IsEnum, SpecialTypeDetails,
+			ReservedTagPragma, IsForeign)) :-
 	% Initially, when we first see the `:- type' definition,
 	% we assign the constructor tags assuming that there is no
 	% `:- pragma reserve_tag' declaration for this type.
@@ -2647,24 +3013,26 @@
 		CtorTags, IsEnum),
 	IsForeign = no.
 convert_type_defn(eqv_type(Body), _, _, eqv_type(Body)).
+convert_type_defn(solver_type(SolverTypeDetails), _, _,
+		solver_type(SolverTypeDetails)).
 convert_type_defn(abstract_type(IsSolverType), _, _,
 		abstract_type(IsSolverType)).
-convert_type_defn(foreign_type(ForeignType, UserEqComp, Assertions), _, _,
-		foreign_type(Body, non_solver_type)) :-
+convert_type_defn(foreign_type(ForeignType, SpecialTypeDetails, Assertions),
+		_, _, foreign_type(Body)) :-
 	(
 		ForeignType = il(ILForeignType),
-		Data = foreign_type_lang_data(ILForeignType, UserEqComp,
-			Assertions),
+		Data = foreign_type_lang_data(ILForeignType,
+				SpecialTypeDetails, Assertions),
 		Body = foreign_type_body(yes(Data), no, no)
 	;
 		ForeignType = c(CForeignType),
-		Data = foreign_type_lang_data(CForeignType, UserEqComp,
-			Assertions),
+		Data = foreign_type_lang_data(CForeignType,
+				SpecialTypeDetails, Assertions),
 		Body = foreign_type_body(no, yes(Data), no)
 	;
 		ForeignType = java(JavaForeignType),
-		Data = foreign_type_lang_data(JavaForeignType, UserEqComp,
-			Assertions),
+		Data = foreign_type_lang_data(JavaForeignType,
+				SpecialTypeDetails, Assertions),
 		Body = foreign_type_body(no, no, yes(Data))
 	).
 
@@ -3604,7 +3972,8 @@
 			(
 				Ctors = Body ^ du_type_ctors,
 				Body ^ du_type_is_enum = no,
-				Body ^ du_type_usereq = no,
+				not has_user_defined_equality(
+					Body ^ du_type_special_type_details),
 				module_info_globals(!.Module, Globals),
 				globals__lookup_int_option(Globals,
 					compare_specialization, CompareSpec),
@@ -3629,9 +3998,23 @@
 					TypeCtor, Body, Context, Status,
 					!Module)
 			)
-		)
+		),
+		(
+			type_util__type_body_is_solver_type(!.Module, Body)
+		->
+			add_special_pred(initialise, TVarSet, Type,
+				TypeCtor, Body, Context, Status, !Module)
+		;
+			true
+ 		)
 	;
-		SpecialPredIds = [unify, compare],
+		(
+			type_util__type_body_is_solver_type(!.Module, Body)
+		->
+			SpecialPredIds = [unify, compare, initialise]
+		;
+			SpecialPredIds = [unify, compare]
+		),
 		add_special_pred_decl_list(SpecialPredIds, TVarSet, Type,
 			TypeCtor, Body, Context, Status, !Module)
 	).
@@ -3672,7 +4055,10 @@
 			SpecialPredId = index
 		;
 			SpecialPredId = compare,
-			( TypeBody ^ du_type_usereq = yes(_) ->
+			(
+				has_user_defined_equality(TypeBody ^
+					du_type_special_type_details)
+			->
 					% The compiler generated comparison
 					% procedure prints an error message,
 					% since comparisons of types with
@@ -3689,6 +4075,19 @@
 			;
 				true
 			)
+		;
+			SpecialPredId = initialise,
+			(
+				type_is_solver_type(!.Module, Type)
+			->
+				add_special_pred_for_real(SpecialPredId,
+					TVarSet, Type, TypeCtor, TypeBody,
+					Context, Status0, !Module)
+			;
+				% rafe: XXX Should this be an error?
+				%
+				true
+			)
 		)
 	).
 
@@ -3714,7 +4113,8 @@
 	->
 		pred_info_set_import_status(Status, PredInfo0, PredInfo1)
 	;
-		TypeBody ^ du_type_usereq = yes(_),
+		has_user_defined_equality(
+			TypeBody ^ du_type_special_type_details),
 		pred_info_import_status(PredInfo0, OldStatus),
 		OldStatus = pseudo_imported,
 		status_is_imported(Status, no)
@@ -3834,7 +4234,10 @@
 	import_status::out) is det.
 
 add_special_pred_unify_status(TypeBody, Status0, Status) :-
-	( TypeBody ^ du_type_usereq = yes(_) ->
+	(
+		has_user_defined_equality(
+			TypeBody ^ du_type_special_type_details)
+	->
 			% If the type has user-defined equality,
 			% then we create a real unify predicate
 			% for it, whose body calls the user-specified
Index: maybe_mlds_to_gcc.pp
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/maybe_mlds_to_gcc.pp,v
retrieving revision 1.8
diff -u -r1.8 maybe_mlds_to_gcc.pp
--- maybe_mlds_to_gcc.pp	14 Jun 2004 04:16:16 -0000	1.8
+++ maybe_mlds_to_gcc.pp	14 Jul 2004 07:30:38 -0000
@@ -58,6 +58,7 @@
 
 #else
 
+:- import_module hlds__passes_aux.
 :- import_module parse_tree__prog_out.
 :- import_module string.
 
Index: mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.245
diff -u -r1.245 mercury_to_mercury.m
--- mercury_to_mercury.m	14 Jul 2004 05:37:05 -0000	1.245
+++ mercury_to_mercury.m	14 Jul 2004 05:41:40 -0000
@@ -297,6 +297,9 @@
 :- pred write_maybe_termination_info(maybe(generic_termination_info(T))::in,
 	bool::in, io::di, io::uo) is det.
 
+:- pred mercury_output_special_type_details(tvarset::in,
+		special_type_details::in, io::di, io::uo) is det.
+
 %-----------------------------------------------------------------------------%
 
 % This is the typeclass mentioned in the long comment at the top of the module.
@@ -1565,38 +1568,41 @@
 	list(type_param), type_defn, prog_context, io__state, io__state).
 :- mode mercury_output_type_defn(in, in, in, in, in, di, uo) is det.
 
-mercury_output_type_defn(VarSet, Name, Args,
+mercury_output_type_defn(TVarSet, Name, Args,
 		abstract_type(IsSolverType), Context) -->
 	mercury_output_begin_type_decl(IsSolverType),
 	{ construct_qualified_term(Name, Args, Context, TypeTerm) },
-	mercury_output_term(TypeTerm, VarSet, no, next_to_graphic_token),
+	mercury_output_term(TypeTerm, TVarSet, no, next_to_graphic_token),
 	io__write_string(".\n").
 
-mercury_output_type_defn(VarSet, Name, Args, eqv_type(Body), Context) -->
+mercury_output_type_defn(TVarSet, Name, Args, eqv_type(Body), Context) -->
 	mercury_output_begin_type_decl(non_solver_type),
 	{ construct_qualified_term(Name, Args, Context, TypeTerm) },
-	mercury_output_term(TypeTerm, VarSet, no),
+	mercury_output_term(TypeTerm, TVarSet, no),
 	io__write_string(" == "),
-	mercury_output_term(Body, VarSet, no, next_to_graphic_token),
+	mercury_output_term(Body, TVarSet, no, next_to_graphic_token),
 	io__write_string(".\n").
 
-mercury_output_type_defn(VarSet, Name, Args,
-		du_type(Ctors, IsSolverType, MaybeEqCompare), Context) -->
-	mercury_output_begin_type_decl(IsSolverType),
+mercury_output_type_defn(TVarSet, Name, Args,
+		du_type(Ctors, SpecialTypeDetails), Context) -->
+	mercury_output_begin_type_decl(non_solver_type),
 	{ construct_qualified_term(Name, Args, Context, TypeTerm) },
-	mercury_output_term(TypeTerm, VarSet, no),
+	mercury_output_term(TypeTerm, TVarSet, no),
 	io__write_string("\n\t--->\t"),
-	mercury_output_ctors(Ctors, VarSet),
-	( { MaybeEqCompare = yes(_) } ->
-		io__write_string("\n\t")
-	;
-		[]
-	),
-	mercury_output_equality_compare_preds(MaybeEqCompare),
-	io__write_string("\n\t.\n").
+	mercury_output_ctors(Ctors, TVarSet),
+	mercury_output_special_type_details(TVarSet, SpecialTypeDetails),
+	io__write_string(".\n").
+
+mercury_output_type_defn(TVarSet, Name, Args, solver_type(SpecialTypeDetails),
+		Context) -->
+	mercury_output_begin_type_decl(solver_type),
+	{ construct_qualified_term(Name, Args, Context, TypeTerm) },
+	mercury_output_term(TypeTerm, TVarSet, no),
+	mercury_output_special_type_details(TVarSet, SpecialTypeDetails),
+	io__write_string(".\n").
 
 mercury_output_type_defn(TVarSet, Name, Args,
-		foreign_type(ForeignType, MaybeEqCompare, Assertions),
+		foreign_type(ForeignType, SpecialTypeDetails, Assertions),
 		_Context) -->
 	io__write_string(":- pragma foreign_type("),
 	( { ForeignType = il(_) }, io__write_string("il, ")
@@ -1628,12 +1634,7 @@
 		io__write_string("]")
 	),
 	io__write_string(")"),
-	( { MaybeEqCompare = yes(_) } ->
-		io__write_string(" ")
-	;
-		[]
-	),
-	mercury_output_equality_compare_preds(MaybeEqCompare),
+	mercury_output_special_type_details(TVarSet, SpecialTypeDetails),
 	io__write_string(".\n").
 
 :- pred mercury_output_foreign_type_assertion(foreign_type_assertion::in,
@@ -1652,32 +1653,82 @@
 mercury_output_begin_type_decl(non_solver_type) -->
 	io__write_string(":- type ").
 
-:- pred mercury_output_equality_compare_preds(maybe(unify_compare)::in,
-	io::di, io::uo) is det.
-
-mercury_output_equality_compare_preds(no) --> [].
-mercury_output_equality_compare_preds(
-		yes(unify_compare(MaybeEqualityPred, MaybeComparisonPred))) -->
-	io__write_string("where "),
-	( { MaybeEqualityPred = yes(EqualityPredName) } ->
-		io__write_string("equality is "),
-		mercury_output_bracketed_sym_name(EqualityPredName),
-		( { MaybeComparisonPred = yes(_) } ->
-			io__write_string(", ")
+mercury_output_special_type_details(TVarSet,
+		special_type_details(
+			MaybeSolverTypeDetails,
+			MaybeUnifyPred,
+			MaybeComparePred)) -->
+	(
+		{ MaybeSolverTypeDetails = no },
+		{ MaybeUnifyPred         = no },
+		{ MaybeComparePred       = no }
+	->
+		[]
+	;
+		io__write_string("\n\twhere\t"),
+		(
+			{ MaybeSolverTypeDetails = yes(SolverTypeDetails) }
+		->
+			mercury_output_solver_type_details(TVarSet,
+				SolverTypeDetails),
+			(
+				{	MaybeUnifyPred = yes(_)
+				;	MaybeComparePred = yes(_)
+				}
+			->
+				io__write_string(",\n\t\t")
+			;
+				[]
+			)
+		;
+			[]
+		),
+		(
+			{ MaybeUnifyPred = yes(UnifyPredName) }
+		->
+			io__write_string("equality is "),
+			mercury_output_bracketed_sym_name(UnifyPredName),
+			(
+				{	MaybeComparePred = yes(_)	}
+			->
+				io__write_string(",\n\t\t")
+			;
+				[]
+			)
+		;
+			[]
+		),
+		(
+			{ MaybeComparePred = yes(ComparePredName) }
+		->
+			io__write_string("comparison is "),
+			mercury_output_bracketed_sym_name(ComparePredName)
 		;
 			[]
 		)
-	;
-		[]
-	),
-	( { MaybeComparisonPred = yes(ComparisonPredName) } ->
-		io__write_string("comparison is "),
-		mercury_output_bracketed_sym_name(ComparisonPredName)
-	;
-		[]
 	).
-mercury_output_equality_compare_preds(yes(abstract_noncanonical_type)) -->
-	io__write_string("where type_is_abstract_noncanonical").
+
+mercury_output_special_type_details(_TVarSet,
+		abstract_noncanonical_type(_)) -->
+	io__write_string("\n\twhere type_is_abstract_noncanonical").
+
+
+:- pred mercury_output_solver_type_details(tvarset::in,
+		solver_type_details::in, io::di, io::uo) is det.
+
+mercury_output_solver_type_details(TVarSet,
+		solver_type_details(RepresentationType, InitPred,
+			GroundInst, AnyInst)) -->
+	io__write_string("representation is "),
+	mercury_output_term(RepresentationType, TVarSet, no),
+	io__write_string(",\n\t\tinitialisation is "),
+	mercury_output_bracketed_sym_name(InitPred),
+	{ varset__init(EmptyInstVarSet) },
+	io__write_string(",\n\t\tground is "),
+	mercury_output_inst(GroundInst, EmptyInstVarSet),
+	io__write_string(",\n\t\tany is "),
+	mercury_output_inst(AnyInst, EmptyInstVarSet).
+
 
 :- pred mercury_output_ctors(list(constructor), tvarset,
 				io__state, io__state).
Index: ml_code_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/ml_code_gen.m,v
retrieving revision 1.143
diff -u -r1.143 ml_code_gen.m
--- ml_code_gen.m	6 Jul 2004 04:18:49 -0000	1.143
+++ ml_code_gen.m	14 Jul 2004 05:41:40 -0000
@@ -894,8 +894,8 @@
 foreign_type_required_imports(il, TypeDefn) = Imports :-
 	hlds_data__get_type_defn_body(TypeDefn, Body),
 	(
-		Body = foreign_type(foreign_type_body(MaybeIL,
-			_MaybeC, _MaybeJava), _)
+		Body = foreign_type(foreign_type_body(MaybeIL, _MaybeC,
+				_MaybeJava))
 	->
 		(
 			MaybeIL = yes(Data),
Index: ml_type_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/ml_type_gen.m,v
retrieving revision 1.36
diff -u -r1.36 ml_type_gen.m
--- ml_type_gen.m	19 Mar 2004 10:19:22 -0000	1.36
+++ ml_type_gen.m	1 Jul 2004 01:19:50 -0000
@@ -128,11 +128,10 @@
 	% XXX Fixme!
 	% For a description of the problems with equivalence types,
 	% see our BABEL'01 paper "Compiling Mercury to the .NET CLR".
-ml_gen_type_2(du_type(Ctors, TagValues, IsEnum, MaybeUserEqCompare,
-		_ReservedTag, _IsSolverType, _), ModuleInfo, TypeCtor,
-		TypeDefn, !Defns) :-
+ml_gen_type_2(du_type(Ctors, TagValues, IsEnum, SpecialTypeDetails,
+		_ReservedTag, _), ModuleInfo, TypeCtor, TypeDefn, !Defns) :-
 	% XXX we probably shouldn't ignore _ReservedTag
-	ml_gen_equality_members(MaybeUserEqCompare, MaybeEqualityMembers),
+	ml_gen_equality_members(SpecialTypeDetails, MaybeEqualityMembers),
 	( IsEnum = yes ->
 		ml_gen_enum_type(TypeCtor, TypeDefn, Ctors, TagValues,
 			MaybeEqualityMembers, !Defns)
@@ -141,7 +140,8 @@
 			Ctors, TagValues, MaybeEqualityMembers, !Defns)
 	).
 	% XXX Fixme!  Same issues here as for eqv_type/1.
-ml_gen_type_2(foreign_type(_, _), _, _, _, !Defns).
+ml_gen_type_2(foreign_type(_), _, _, _, !Defns).
+ml_gen_type_2(solver_type(_), _, _, _, !Defns).
 
 %-----------------------------------------------------------------------------%
 %
@@ -951,7 +951,7 @@
 	% For interoperability, we ought to generate an `==' member
 	% for types which have a user-defined equality, if the target
 	% language supports it (as do e.g. C++, Java).
-:- pred ml_gen_equality_members(maybe(unify_compare)::in,
+:- pred ml_gen_equality_members(special_type_details::in,
 	list(mlds__defn)::out) is det.
 
 ml_gen_equality_members(_, []).  % XXX generation of `==' members
Index: ml_unify_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/ml_unify_gen.m,v
retrieving revision 1.76
diff -u -r1.76 ml_unify_gen.m
--- ml_unify_gen.m	14 Jun 2004 04:16:18 -0000	1.76
+++ ml_unify_gen.m	1 Jul 2004 01:23:32 -0000
@@ -1870,7 +1870,7 @@
 	module_info_types(ModuleInfo, TypeTable),
 	TypeDefn = map__lookup(TypeTable, TypeCtor),
 	hlds_data__get_type_defn_body(TypeDefn, TypeDefnBody),
-	( TypeDefnBody = du_type(Ctors, TagValues, _, _, _ReservedTag, _, _) ->
+	( TypeDefnBody = du_type(Ctors, TagValues, _, _, _ReservedTag, _) ->
 		% XXX we probably shouldn't ignore ReservedTag here
 		(
 			(some [Ctor] (
Index: mlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mlds.m,v
retrieving revision 1.113
diff -u -r1.113 mlds.m
--- mlds.m	14 Jun 2004 04:16:19 -0000	1.113
+++ mlds.m	30 Jun 2004 17:54:58 -0000
@@ -1757,7 +1757,7 @@
 		map__search(Types, TypeCtor, TypeDefn),
 		hlds_data__get_type_defn_body(TypeDefn, Body),
 		Body = foreign_type(foreign_type_body(MaybeIL, MaybeC,
-			MaybeJava), _)
+				MaybeJava))
 	->
 		module_info_globals(ModuleInfo, Globals),
 		globals__get_target(Globals, Target),
Index: mode_errors.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_errors.m,v
retrieving revision 1.79
diff -u -r1.79 mode_errors.m
--- mode_errors.m	14 Jun 2004 04:16:21 -0000	1.79
+++ mode_errors.m	30 Jun 2004 05:40:39 -0000
@@ -197,7 +197,7 @@
 :- import_module parse_tree__prog_util.
 
 :- import_module int, map, term_io, varset, term.
-:- import_module std_util, require.
+:- import_module std_util, string, require.
 
 	% just dispatch on the diffferent sorts of mode errors
 
@@ -444,7 +444,7 @@
 		prog_out__write_context(Context),
 		io__write_string("  inside the condition of an if-then-else.\n")
 	; { Reason = lambda(PredOrFunc) },
-		{ PredOrFuncS = pred_or_func_to_str(PredOrFunc) },
+		{ PredOrFuncS = prog_out__pred_or_func_to_str(PredOrFunc) },
 		io__write_string("attempt to bind a non-local variable inside\n"),
 		prog_out__write_context(Context),
 		io__write_strings(["  a ", PredOrFuncS, " lambda goal.\n"])
@@ -753,11 +753,12 @@
 	globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
 	( { VerboseErrors = yes } ->
 		io__write_string("\tYour code is trying to test whether two "),
-		write_pred_or_func(PredOrFunc),
+		prog_out__write_pred_or_func(PredOrFunc),
 		io__write_string("s are equal,\n"),
-		io__write_string("\tby unifying them.  In the general case, testing equivalence\n"),
+		io__write_string("\tby unifying them.  In the general " ++
+					"case, testing equivalence\n"),
 		io__write_string("\tof "),
-		write_pred_or_func(PredOrFunc),
+		prog_out__write_pred_or_func(PredOrFunc),
 		io__write_string("s is an undecidable problem,\n"),
 		io__write_string("\tand so this is not allowed by the Mercury mode system.\n"),
 		io__write_string("\tIn some cases, you can achieve the same effect by\n"),
Index: modecheck_call.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_call.m,v
retrieving revision 1.50
diff -u -r1.50 modecheck_call.m
--- modecheck_call.m	14 Jun 2004 04:16:22 -0000	1.50
+++ modecheck_call.m	2 Jul 2004 04:00:18 -0000
@@ -874,13 +874,12 @@
 	; A_mi_B = no,  B_mi_A = yes, Result = worse
 	; A_mi_B = no,  B_mi_A = no,  Result = incomparable
 	; A_mi_B = yes, B_mi_A = yes,
-		%
-		% We need to further disambiguate the cases involving
-		% `any' and `free', since `any' matches_initial `free'
-		% and vice versa.  For these cases, we want to take
-		% the actual inst of the argument into account:
-		% if the argument is `free', we should prefer `free',
-		% but otherwise, we should prefer `any'.
+		% Otherwise, we need to further disambiguate the cases
+		% involving `any' and `free', since `any' matches_initial
+		% `free' and vice versa.  For these cases, we want to take
+		% the actual inst of the argument into account: if the
+		% argument is `free', we should prefer `free', but otherwise,
+		% we should prefer `any'.
 		%
 		(
 			MaybeArgInst = no,
Index: modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.68
diff -u -r1.68 modecheck_unify.m
--- modecheck_unify.m	14 Jun 2004 04:16:23 -0000	1.68
+++ modecheck_unify.m	30 Jun 2004 05:53:32 -0000
@@ -314,12 +314,13 @@
 		(
 			HowToCheckGoal = check_unique_modes
 		->
-			unique_modes__check_goal(Goal0, Goal, !ModeInfo, !IO)
+			unique_modes__check_goal(Goal0, Goal1, !ModeInfo, !IO)
 		;
-			modecheck_goal(Goal0, Goal, !ModeInfo, !IO)
+			modecheck_goal(Goal0, Goal1, !ModeInfo, !IO)
 		),
 		mode_list_get_final_insts(Modes, ModuleInfo0, FinalInsts),
-		modecheck_final_insts(Vars, FinalInsts, !ModeInfo),
+		modecheck_final_insts(Vars, FinalInsts, Goal1, Goal,
+			!ModeInfo),
 		mode_checkpoint(exit, "lambda goal", !ModeInfo, !IO),
 
 		mode_info_remove_live_vars(LiveVars, !ModeInfo),
Index: modes.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modes.m,v
retrieving revision 1.279
diff -u -r1.279 modes.m
--- modes.m	14 Jun 2004 04:16:23 -0000	1.279
+++ modes.m	7 Jul 2004 06:48:46 -0000
@@ -53,7 +53,7 @@
 % 	        record the newly inferred normalised final insts
 % 		in the proc_info, and check whether they changed
 % 		(so that we know when we've reached the fixpoint).
-% 
+%
 % To mode-analyse a goal:
 % If goal is
 % 	(a) a disjunction
@@ -100,14 +100,14 @@
 % 		insts match.  (Perhaps also think about expanding
 % 		if-then-elses so that they can be run backwards,
 % 		if the condition can't be scheduled?)
-% 
+%
 % To attempt to schedule a goal, first mode-check the goal.  If mode-checking
 % succeeds, then scheduling succeeds.  If mode-checking would report
 % an error due to the binding of a local variable, then scheduling
 % fails.  (If mode-checking would report an error due to the binding of
 % a *local* variable, we could report the error right away --
 % but this idea has not yet been implemented.)
-% 
+%
 % Note that the notion of liveness used here is different to that
 % used in liveness.m and the code generator.  Here, we consider
 % a variable live if its value will be used later on in the computation.
@@ -242,10 +242,10 @@
 	mode_info::in, mode_info::out) is det.
 
 	% check that the final insts of the head vars of a lambda
-	% goal matches their expected insts
+	% goal matches their expected insts.
 	%
 :- pred modecheck_final_insts(list(prog_var)::in, list(inst)::in,
-	mode_info::in, mode_info::out) is det.
+	hlds_goal::in, hlds_goal::out, mode_info::in, mode_info::out) is det.
 
 :- pred mode_info_add_goals_live_vars(list(hlds_goal)::in,
 	mode_info::in, mode_info::out) is det.
@@ -777,13 +777,13 @@
 
 		% modecheck the procedure body
 	( WhatToCheck = check_unique_modes ->
-		unique_modes__check_goal(Body0, Body, ModeInfo1, ModeInfo2,
+		unique_modes__check_goal(Body0, Body1, ModeInfo1, ModeInfo2,
 			!IO)
 	;
-		modecheck_goal(Body0, Body, ModeInfo1, ModeInfo2, !IO)
+		modecheck_goal(Body0, Body1, ModeInfo1, ModeInfo2, !IO)
 	),
 
-		% check that final insts match those specified in the
+		% Check that final insts match those specified in the
 		% mode declaration
 	mode_list_get_final_insts(ArgModes0, !.ModuleInfo, ArgFinalInsts0),
 	pred_info_get_markers(PredInfo, Markers),
@@ -793,7 +793,7 @@
 		InferModes = no
 	),
 	modecheck_final_insts_2(HeadVars, ArgFinalInsts0, InferModes,
-		ArgFinalInsts, ModeInfo2, ModeInfo3),
+		ArgFinalInsts, Body1, Body, ModeInfo2, ModeInfo3),
 
 	( InferModes = yes ->
 		% For inferred predicates, we don't report the
@@ -822,21 +822,22 @@
 	proc_info_set_argmodes(ArgModes, !ProcInfo).
 
 	% modecheck_final_insts for a lambda expression
-modecheck_final_insts(HeadVars, ArgFinalInsts, !ModeInfo) :-
+modecheck_final_insts(HeadVars, ArgFinalInsts, !Goal, !ModeInfo) :-
 		% for lambda expressions, modes must always be
 		% declared, we never infer them.
 	InferModes = no,
 	modecheck_final_insts_2(HeadVars, ArgFinalInsts, InferModes,
-		_NewFinalInsts, !ModeInfo).
+		_NewFinalInsts, !Goal, !ModeInfo).
 
 :- pred modecheck_final_insts_2(list(prog_var)::in, list(inst)::in, bool::in,
-	list(inst)::out, mode_info::in, mode_info::out) is det.
+	list(inst)::out, hlds_goal::in, hlds_goal::out,
+	mode_info::in, mode_info::out) is det.
 
 	% check that the final insts of the head vars matches their
 	% expected insts
 	%
 modecheck_final_insts_2(HeadVars, FinalInsts0, InferModes, FinalInsts,
-		!ModeInfo) :-
+		Body0, Body, !ModeInfo) :-
 	mode_info_get_module_info(!.ModeInfo, ModuleInfo),
 	mode_info_get_errors(!.ModeInfo, Errors),
 	% If there were any mode errors, use an unreachable instmap.
@@ -876,13 +877,15 @@
 		proc_info_arglives(ProcInfo, ModuleInfo, ArgLives),
 		maybe_clobber_insts(VarFinalInsts2, ArgLives, FinalInsts),
 		check_final_insts(HeadVars, FinalInsts0, FinalInsts,
-			InferModes, 1, ModuleInfo, no, Changed1, !ModeInfo),
+			InferModes, 1, ModuleInfo, Body0, Body, no, Changed1,
+			!ModeInfo),
 		mode_info_get_changed_flag(!.ModeInfo, Changed2),
 		bool__or_list([Changed0, Changed1, Changed2], Changed),
 		mode_info_set_changed_flag(Changed, !ModeInfo)
 	;
 		check_final_insts(HeadVars, FinalInsts0, VarFinalInsts1,
-			InferModes, 1, ModuleInfo, no, _Changed1, !ModeInfo),
+			InferModes, 1, ModuleInfo, Body0, Body, no, _Changed1,
+			!ModeInfo),
 		FinalInsts = FinalInsts0
 	).
 
@@ -903,11 +906,11 @@
 	maybe_clobber_insts(Insts0, IsLives, Insts).
 
 :- pred check_final_insts(list(prog_var)::in, list(inst)::in, list(inst)::in,
-	bool::in, int::in, module_info::in, bool::in, bool::out,
-	mode_info::in, mode_info::out) is det.
+	bool::in, int::in, module_info::in, hlds_goal::in, hlds_goal::out,
+	bool::in, bool::out, mode_info::in, mode_info::out) is det.
 
 check_final_insts(Vars, Insts, VarInsts, InferModes, ArgNum, ModuleInfo,
-		!Changed, !ModeInfo) :-
+		!Goal, !Changed, !ModeInfo) :-
 	(
 		Vars = [],
 		Insts = [],
@@ -921,18 +924,34 @@
 	->
 		mode_info_get_var_types(!.ModeInfo, VarTypes),
 		map__lookup(VarTypes, Var, Type),
-		( inst_matches_final(VarInst, Inst, Type, ModuleInfo) ->
+		(
+			inst_matches_final(VarInst, Inst, Type, ModuleInfo)
+		->
 			true
 		;
 			!:Changed = yes,
 			(
+				% If this is a solver type with inst `free'
+				% that should have inst `any' then insert
+				% a call to the appropriate initialisation
+				% predicate.
+				%
+				inst_match__inst_is_free(ModuleInfo, VarInst),
+				inst_match__inst_is_any(ModuleInfo, Inst),
+				type_util__type_is_solver_type(ModuleInfo,
+					Type)
+			->
+				prepend_initialisation_call(ModuleInfo, Var,
+					Type, VarInst, !Goal)
+			;
 				% If we're inferring the mode, then don't
 				% report an error, just set changed to yes
 				% to make sure that we will do another
 				% fixpoint pass.
 				InferModes = yes
+			->
+				true
 			;
-				InferModes = no,
 				% XXX this might need to be reconsidered now
 				% we have unique modes
 				(
@@ -959,12 +978,27 @@
 		),
 		check_final_insts(VarsTail, InstsTail, VarInstsTail,
 			InferModes, ArgNum + 1, ModuleInfo,
-			!Changed, !ModeInfo)
+			!Goal, !Changed, !ModeInfo)
 	;
 		error("check_final_insts: length mismatch")
 	).
 
 %-----------------------------------------------------------------------------%
+
+:- pred prepend_initialisation_call(module_info::in,
+		prog_var::in, (type)::in, (inst)::in,
+		hlds_goal::in, hlds_goal::out) is det.
+
+prepend_initialisation_call(ModuleInfo, Var, VarType, InitialInst,
+		Goal0, Goal) :-
+	Goal0   = _GoalExpr0 - GoalInfo0,
+	hlds_goal__goal_info_get_context(GoalInfo0, Context),
+	construct_initialisation_call(ModuleInfo, Var, VarType, InitialInst,
+		Context, no /* CallUnifyContext */, InitVarGoal),
+	goal_to_conj_list(Goal0, ConjList0),
+	conj_list_to_goal([InitVarGoal | ConjList0], GoalInfo0, Goal).
+
+%-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
 % Modecheck a goal by abstractly interpreteting it, as explained
@@ -2070,101 +2104,129 @@
 		% instantiated vars, since that would require
 		% doing a partially instantiated deep copy, and we
 		% don't know how to do that yet.
-		(
-			InitialInst = any(_),
-			inst_is_free(ModuleInfo0, VarInst1)
-		->
-			% This is the simple case of implied `any' modes,
-			% where the declared mode was `any -> ...'
-			% and the argument passed was `free'
 
-			Var = Var0,
+		InitialInst = any(_),
+		inst_is_free(ModuleInfo0, VarInst1)
+	->
+		% This is the simple case of implied `any' modes,
+		% where the declared mode was `any -> ...'
+		% and the argument passed was `free'
+
+		Var = Var0,
+
+		% If the variable's type is not a solver type (in
+		% which case inst `any' means the same as inst
+		% `ground') then this is an implied mode that we
+		% don't yet know how to handle.
+		%
+		% If the variable's type is a solver type then
+		% we need to insert a call to the solver type's
+		% initialisation predicate.
 
-			% Create code to initialize the variable to
-			% inst `any', by calling <mod>:<type>_init_any/1,
-			% where <mod>:<type> is the type of the variable.
-			% XXX We ought to use a more elegant method
-			% XXX than hard-coding the name `<foo>_init_any'.
+		mode_info_get_context(!.ModeInfo, Context),
+		mode_info_get_mode_context(!.ModeInfo, ModeContext),
+		mode_context_to_unify_context(!.ModeInfo, ModeContext,
+			UnifyContext),
+		CallUnifyContext = yes(call_unify_context(Var, var(Var),
+						UnifyContext)),
 
-			mode_info_get_context(!.ModeInfo, Context),
-			mode_info_get_mode_context(!.ModeInfo, ModeContext),
-			mode_context_to_unify_context(!.ModeInfo,
-				ModeContext, UnifyContext),
-			CallUnifyContext = yes(call_unify_context(
-				Var, var(Var), UnifyContext)),
-			(
-				type_to_ctor_and_args(VarType, TypeCtor,
-					_TypeArgs),
-				TypeCtor = qualified(TypeModule, TypeName) -
-					_TypeArity,
-				string__append(TypeName, "_init_any", PredName),
-				modes__build_call(TypeModule, PredName, [Var],
-					Context, CallUnifyContext, ModuleInfo0,
-					BeforeGoal - GoalInfo0)
-			->
-				set__singleton_set(NonLocals, Var),
-				goal_info_set_nonlocals(GoalInfo0,
-					NonLocals, GoalInfo1),
-				InstmapDeltaAL = [Var - InitialInst],
-				instmap_delta_from_assoc_list(InstmapDeltaAL,
-					InstmapDelta),
-				goal_info_set_instmap_delta(GoalInfo1,
-					InstmapDelta, GoalInfo),
-				NewExtraGoal = extra_goals(
-					[BeforeGoal - GoalInfo], []),
-				append_extra_goals(!.ExtraGoals, NewExtraGoal,
-					!:ExtraGoals)
-			;
-				% If the type is a type variable,
-				% or there isn't any <mod>:<type>_init_any/1
-				% predicate, then give up.
-				set__singleton_set(WaitingVars, Var0),
-				mode_info_error(WaitingVars,
-					mode_error_implied_mode(Var0, VarInst0,
-						InitialInst),
-					!ModeInfo
-				)
-			)
-		;
-			inst_is_bound(ModuleInfo0, InitialInst)
+		(
+			type_util__type_is_solver_type(ModuleInfo0, VarType)
 		->
-			% This is the case we can't handle
-			Var = Var0,
+			% Create code to initialize the variable to
+			% inst `any', by calling the solver type's
+			% initialisation predicate.
+			insert_extra_initialisation_call(ModuleInfo0, Var,
+				VarType, InitialInst, Context,
+				CallUnifyContext, !ExtraGoals)
+		;
+			% If the type is a type variable,
+			% or isn't a solver type then give up.
 			set__singleton_set(WaitingVars, Var0),
 			mode_info_error(WaitingVars,
 				mode_error_implied_mode(Var0, VarInst0,
 					InitialInst),
-				!ModeInfo
-			)
-		;
-			% This is the simple case of implied modes,
-			% where the declared mode was free -> ...
-
-			% Introduce a new variable
-			mode_info_get_varset(!.ModeInfo, VarSet0),
-			varset__new_var(VarSet0, Var, VarSet),
-			map__set(VarTypes0, Var, VarType, VarTypes),
-			mode_info_set_varset(VarSet, !ModeInfo),
-			mode_info_set_var_types(VarTypes, !ModeInfo),
-
-			% Construct the code to do the unification
-			modecheck_unify__create_var_var_unification(Var0, Var,
-				VarType, !.ModeInfo, ExtraGoal),
-
-			% append the goals together in the appropriate order:
-			% ExtraGoals0, then NewUnify
-			NewUnifyExtraGoal = extra_goals([], [ExtraGoal]),
-			append_extra_goals(!.ExtraGoals, NewUnifyExtraGoal,
-				!:ExtraGoals)
+				!ModeInfo)
 		)
+	;
+		inst_is_bound(ModuleInfo0, InitialInst)
+	->
+		% This is the case we can't handle
+		Var = Var0,
+		set__singleton_set(WaitingVars, Var0),
+		mode_info_error(WaitingVars,
+			mode_error_implied_mode(Var0, VarInst0, InitialInst),
+			!ModeInfo)
+	;
+		% This is the simple case of implied modes,
+		% where the declared mode was free -> ...
+
+		% Introduce a new variable
+		mode_info_get_varset(!.ModeInfo, VarSet0),
+		varset__new_var(VarSet0, Var, VarSet),
+		map__set(VarTypes0, Var, VarType, VarTypes),
+		mode_info_set_varset(VarSet, !ModeInfo),
+		mode_info_set_var_types(VarTypes, !ModeInfo),
+
+		% Construct the code to do the unification
+		modecheck_unify__create_var_var_unification(Var0, Var,
+			VarType, !.ModeInfo, ExtraGoal),
+
+		% append the goals together in the appropriate order:
+		% ExtraGoals0, then NewUnify
+		NewUnifyExtraGoal = extra_goals([], [ExtraGoal]),
+		append_extra_goals(!.ExtraGoals, NewUnifyExtraGoal,
+			!:ExtraGoals)
 	).
 
+
+:- pred insert_extra_initialisation_call(module_info::in, prog_var::in,
+		(type)::in, (inst)::in,
+		prog_context::in, maybe(call_unify_context)::in,
+		extra_goals::in, extra_goals::out) is det.
+
+insert_extra_initialisation_call(ModuleInfo, Var, VarType, InitialInst,
+		Context, CallUnifyContext, !ExtraGoals) :-
+
+	construct_initialisation_call(ModuleInfo, Var, VarType, InitialInst,
+		Context, CallUnifyContext, InitVarGoal),
+	NewExtraGoal = extra_goals([InitVarGoal], []),
+	append_extra_goals(!.ExtraGoals, NewExtraGoal, !:ExtraGoals).
+
+
+:- pred construct_initialisation_call(module_info::in, prog_var::in,
+		(type)::in, (inst)::in, prog_context::in,
+		maybe(call_unify_context)::in, hlds_goal::out) is det.
+
+construct_initialisation_call(ModuleInfo, Var, VarType, InitialInst, Context,
+		MaybeCallUnifyContext, InitVarGoal) :-
+	(
+		type_to_ctor_and_args(VarType, TypeCtor, _TypeArgs),
+		PredName = special_pred__special_pred_name(initialise,
+				TypeCtor),
+		hlds_module__module_info_name(ModuleInfo, ThisModule),
+		modes__build_call(ThisModule, PredName, [Var],
+			Context, MaybeCallUnifyContext, ModuleInfo,
+			GoalExpr - GoalInfo0)
+	->
+		set__singleton_set(NonLocals, Var),
+		goal_info_set_nonlocals(GoalInfo0, NonLocals, GoalInfo1),
+		InstmapDeltaAL = [Var - InitialInst],
+		instmap_delta_from_assoc_list(InstmapDeltaAL, InstmapDelta),
+		goal_info_set_instmap_delta(GoalInfo1, InstmapDelta, GoalInfo),
+		InitVarGoal = GoalExpr - GoalInfo
+	;
+		error("modes.insert_extra_initialisation_call: " ++
+			"modes.construct_initialisation_call failed")
+	).
+
+
 :- pred modes__build_call(module_name::in, string::in, list(prog_var)::in,
-	prog_context::in, maybe(call_unify_context)::in, module_info::in,
-	hlds_goal::out) is semidet.
+	prog_context::in, maybe(call_unify_context)::in,
+	module_info::in, hlds_goal::out) is semidet.
 
-modes__build_call(Module, Name, ArgVars, Context, CallUnifyContext, ModuleInfo,
-		Goal) :-
+modes__build_call(Module, Name, ArgVars, Context, CallUnifyContext,
+		ModuleInfo, Goal) :-
 	module_info_get_predicate_table(ModuleInfo, PredicateTable),
 	list__length(ArgVars, Arity),
 	predicate_table_search_pred_m_n_a(PredicateTable, is_fully_qualified,
Index: module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.92
diff -u -r1.92 module_qual.m
--- module_qual.m	14 Jun 2004 04:16:24 -0000	1.92
+++ module_qual.m	16 Jul 2004 06:09:32 -0000
@@ -729,8 +729,8 @@
 :- pred qualify_type_defn(type_defn::in, type_defn::out, mq_info::in,
 	mq_info::out, io__state::di, io__state::uo) is det.
 
-qualify_type_defn(du_type(Ctors0, IsSolverType, MaybeEqualityPred0),
-		du_type(Ctors, IsSolverType, MaybeEqualityPred),
+qualify_type_defn(du_type(Ctors0, SpecialTypeDetails0),
+		du_type(Ctors, SpecialTypeDetails),
 		Info0, Info) -->
 	qualify_constructors(Ctors0, Ctors, Info0, Info),
 
@@ -738,11 +738,36 @@
 	% 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 }.
+	{ SpecialTypeDetails = SpecialTypeDetails0 }.
 qualify_type_defn(eqv_type(Type0), eqv_type(Type), Info0, Info) -->
 	qualify_type(Type0, Type, Info0, Info).
 qualify_type_defn(abstract_type(_) @ Defn, Defn, Info, Info) --> [].
 qualify_type_defn(foreign_type(_, _, _) @ Defn, Defn, Info, Info) --> [].
+qualify_type_defn(solver_type(SpecialTypeDetails0),
+		solver_type(SpecialTypeDetails),
+		Info0, Info) -->
+	(
+		{ SpecialTypeDetails0 ^ solver_type_details =
+			yes(SolverTypeDetails0) }
+	->
+		{ RepnType0   = SolverTypeDetails0 ^ representation_type },
+		{ GroundInst0 = SolverTypeDetails0 ^ ground_inst },
+		{ AnyInst0    = SolverTypeDetails0 ^ any_inst },
+		qualify_type(RepnType0, RepnType,     Info0, Info1),
+		qualify_inst(GroundInst0, GroundInst, Info1, Info2),
+		qualify_inst(AnyInst0, AnyInst,       Info2, Info ),
+		{ SolverTypeDetails =
+			(((SolverTypeDetails0
+				^ representation_type := RepnType   )
+				^ ground_inst         := GroundInst )
+				^ any_inst            := AnyInst    ) },
+		{ SpecialTypeDetails =
+			SpecialTypeDetails0 ^ solver_type_details :=
+				yes(SolverTypeDetails) }
+	;
+		{ error("module_qual.qualify_type_defn: solver type " ++
+			"with no solver_type_details") }
+	).
 
 :- pred qualify_constructors(list(constructor)::in, list(constructor)::out,
 		mq_info::in, mq_info::out, io__state::di, io__state::uo) is det.
Index: modules.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modules.m,v
retrieving revision 1.303
diff -u -r1.303 modules.m
--- modules.m	14 Jun 2004 04:16:24 -0000	1.303
+++ modules.m	7 Jul 2004 04:53:17 -0000
@@ -15,11 +15,11 @@
 % The interface system works as follows:
 %
 % 1. a .int3 file is written, which contains all the types, typeclasses, insts
-% and modes defined in the interface. Equivalence types, insts and
-% modes are written in full, others are written in abstract form.
-% These are module qualified as far as possible given the information
-% present in the current module. The datestamp on the .date3 file
-% gives the last time the .int3 file was checked for consistency.
+% and modes defined in the interface. Equivalence types, solver types, insts
+% and modes are written in full, others are written in abstract form.  These
+% are module qualified as far as possible given the information present in the
+% current module. The datestamp on the .date3 file gives the last time the
+% .int3 file was checked for consistency.
 %
 % 2. The .int and .int2 files are created, using the .int3 files
 % of imported modules to fully module qualify all items.
@@ -1478,10 +1478,9 @@
 	map__map_values(
 		(pred(_::in, Defns0::in, Defns::out) is det :-
 			(
-				Defns0 = [du_type(_, IsSolverType, _) -
-					(Item0 - Context)]
+				Defns0 = [du_type(_, _) - (Item0 - Context)]
 			->
-				Defn = abstract_type(IsSolverType),
+				Defn = abstract_type(non_solver_type),
 				( Item = Item0 ^ td_ctor_defn := Defn ->
 					Defns = [Defn - (Item - Context)]
 				;
@@ -6950,7 +6949,8 @@
 		type_defn(VarSet, Name, Args, abstract_type(IsSolverType),
 			Cond)) :-
 	(
-		TypeDefn = du_type(_, IsSolverType, _),
+		TypeDefn = du_type(_, _),
+		IsSolverType = non_solver_type,
 		% For the `.int2' files, we need the full definitions of
 		% discriminated union types.  Even if the functors for a type
 		% are not used within a module, we may need to know them for
@@ -6959,7 +6959,16 @@
 	;
 		TypeDefn = abstract_type(IsSolverType)
 	;
+		TypeDefn = solver_type(_),
+		% rafe: XXX XXX we need to also export the details of the
+		% forwarding type for the representation and the forwarding
+		% pred for initialization.
+		IsSolverType = solver_type
+	;
 		TypeDefn = eqv_type(_),
+		% rafe: XXX what *should* IsSolverType be here?  We need
+		% to know properly.
+		IsSolverType = non_solver_type,
 		% For the `.int2' files, we need the full definitions of
 		% equivalence types. They are needed to ensure that
 		% non-abstract equivalence types always get fully expanded
@@ -6968,8 +6977,7 @@
 		% But the full definitions are not needed for the `.int3'
 		% files. So we convert equivalence types into abstract
 		% types only for the `.int3' files.
-		ShortInterfaceKind = int3,
-		IsSolverType = non_solver_type
+		ShortInterfaceKind = int3
 	;
 		TypeDefn = foreign_type(_, _, _),
 		% We always need the definitions of foreign types
@@ -6988,14 +6996,22 @@
 make_abstract_unify_compare(type_defn(VarSet, Name, Args, TypeDefn0, Cond),
 		int2, type_defn(VarSet, Name, Args, TypeDefn, Cond)) :-
 	(
-		TypeDefn0 = du_type(Constructors, IsSolverType,
-			yes(_UnifyCompare)),
-		TypeDefn  = du_type(Constructors, IsSolverType,
-			yes(abstract_noncanonical_type))
-	;
-		TypeDefn0 = foreign_type(ForeignType, yes(_), Assertions),
-		TypeDefn = foreign_type(ForeignType,
-			yes(abstract_noncanonical_type), Assertions)
+		TypeDefn0 = du_type(Constructors, SpecialTypeDetails),
+		prog_data__has_user_defined_equality(SpecialTypeDetails),
+		TypeDefn  = du_type(Constructors,
+				abstract_noncanonical_type(non_solver_type))
+	;
+		TypeDefn0 = foreign_type(ForeignType, SpecialTypeDetails,
+				Assertions),
+		prog_data__has_user_defined_equality(SpecialTypeDetails),
+		TypeDefn  = foreign_type(ForeignType,
+				abstract_noncanonical_type(non_solver_type),
+				Assertions)
+	;
+		TypeDefn0 = solver_type(SpecialTypeDetails),
+		prog_data__has_user_defined_equality(SpecialTypeDetails),
+		TypeDefn  = solver_type(
+				abstract_noncanonical_type(solver_type))
 	).
 
 	% All instance declarations must be written
Index: post_typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/post_typecheck.m,v
retrieving revision 1.64
diff -u -r1.64 post_typecheck.m
--- post_typecheck.m	14 Jun 2004 04:16:28 -0000	1.64
+++ post_typecheck.m	30 Jun 2004 06:08:50 -0000
@@ -645,7 +645,7 @@
 	prog_out__write_context(Context),
 	io__write_string("  error: the modified "),
 	{ CallId = PredOrFunc - _ },
-	write_pred_or_func(PredOrFunc),
+	prog_out__write_pred_or_func(PredOrFunc),
 	io__write_string(" is not a base relation.\n").
 
 %-----------------------------------------------------------------------------%
Index: pragma_c_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/pragma_c_gen.m,v
retrieving revision 1.69
diff -u -r1.69 pragma_c_gen.m
--- pragma_c_gen.m	7 Jun 2004 09:07:03 -0000	1.69
+++ pragma_c_gen.m	30 Jun 2004 17:51:52 -0000
@@ -1262,7 +1262,7 @@
 		map__search(Types, TypeId, Defn),
 		hlds_data__get_type_defn_body(Defn, Body),
 		Body = foreign_type(foreign_type_body(_MaybeIL, MaybeC,
-			_MaybeJava), _)
+				_MaybeJava))
 	->
 		(
 			MaybeC = yes(Data),
Index: prog_data.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_data.m,v
retrieving revision 1.112
diff -u -r1.112 prog_data.m
--- prog_data.m	6 Jul 2004 04:18:50 -0000	1.112
+++ prog_data.m	15 Jul 2004 06:46:47 -0000
@@ -1139,8 +1139,7 @@
 :- type type_defn
 	--->	du_type(
 			list(constructor),
-			is_solver_type,
-			maybe(unify_compare)
+			special_type_details
 		)
 	;	eqv_type(
 			type
@@ -1148,9 +1147,12 @@
 	;	abstract_type(
 			is_solver_type
 		)
+	;	solver_type(
+			special_type_details
+		)
 	;	foreign_type(
 			foreign_language_type,
-			maybe(unify_compare),
+			special_type_details,
 			list(foreign_type_assertion)
 		).
 
@@ -1175,20 +1177,67 @@
 
 :- type ctor_field_name == sym_name.
 
-	% unify_compare gives the user-defined unification and/or comparison
-	% predicates for a noncanonical type, if they are known.
-	% The value `abstract_noncanonical_type' represents a discriminated
-	% union type whose definition uses the syntax
-	% `where type_is_abstract_noncanonical' and has been read from a .int2
-	% file.  This means we know that the type has a noncanonical
+	% special_type_details captures information from the optional
+	% `where ...' part of a type definition.
+	%
+	% special_type_details/3 applies to a concrete type definition,
+	% which may include solver_type_details (iff the type is a solver
+	% type) and/or the name of a user-defined equality predicate
+	% and/or the name of a user-defined comparison predicate.
+	%
+	% If no `where ...' part is supplied in a type definition then
+	% the corresponding special_type_details value is
+	% `special_type_details(no, no, no)'.
+	%
+	% abstract_noncanonical_type/1 applies to
+	% `where type_is_abstract_noncanonical', which may only be read from
+	% a .int2 file.  This means we know that the type has a noncanonical
 	% representation, but we don't know what the unification/comparison
 	% predicates are.
-:- type unify_compare
-	--->	unify_compare(
-			unify		:: maybe(equality_pred),
-			compare		:: maybe(comparison_pred)
+	%
+:- type special_type_details
+	--->	special_type_details(
+			solver_type_details  :: maybe(solver_type_details),
+			unify                :: maybe(equality_pred),
+			compare              :: maybe(comparison_pred)
 		)
-	;	abstract_noncanonical_type.
+	;	abstract_noncanonical_type(is_solver_type).
+
+	% no_special_type_details = special_type_details(no, no, no).
+	%
+:- func no_special_type_details = special_type_details.
+
+:- func special_type_details ^ is_solver_type = is_solver_type.
+
+:- pred has_user_defined_equality(special_type_details::in) is semidet.
+
+
+	% A concrete solver type definition's `where part' must begin
+	% with
+	% 	representation is <<representation type>>,
+	% 	initialisation is <<init pred name>>,
+	% 	ground         is <<ground inst>>,
+	% 	any            is <<any inst>>
+	%
+	% rafe: XXX Do we need to change the insts if any constructor
+	% includes existentially typed arguments (meaning typeinfos
+	% and so forth must also be included at some point) or does
+	% all that sort of thing happen after mode checking?
+	% 
+:- type solver_type_details
+	--->	solver_type_details(
+			representation_type :: (type),
+			init_pred           :: init_pred,
+			ground_inst         :: (inst),
+			any_inst            :: (inst)
+		).
+
+	% An init_pred specifies the name of an impure user-defined predicate
+	% used to initialise solver type values (the compiler will insert
+	% calls to this predicate to convert free solver type variables to
+	% inst any variables where necessary.)
+	%
+:- type init_pred	==	sym_name.
 
 	% An equality_pred specifies the name of a user-defined predicate
 	% used for equality on a type.  See the chapter on them in the
@@ -1594,6 +1643,19 @@
 	attributes(Language, may_call_mercury, not_thread_safe,
 		not_tabled_for_io, impure, depends_on_mercury_calls,
 		no, no, []).
+
+
+no_special_type_details = special_type_details(no, no, no).
+
+
+special_type_details(no,     _, _)       ^ is_solver_type = non_solver_type.
+special_type_details(yes(_), _, _)       ^ is_solver_type = solver_type.
+abstract_noncanonical_type(IsSolverType) ^ is_solver_type = IsSolverType.
+
+
+has_user_defined_equality(special_type_details(_, yes(_), _)).
+has_user_defined_equality(special_type_details(_, _, yes(_))).
+
 
 set_may_call_mercury(MayCallMercury, Attrs0, Attrs) :-
 	Attrs = Attrs0 ^ may_call_mercury := MayCallMercury.
Index: prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.227
diff -u -r1.227 prog_io.m
--- prog_io.m	30 Jun 2004 02:48:08 -0000	1.227
+++ prog_io.m	16 Jul 2004 03:21:23 -0000
@@ -1,4 +1,4 @@
-%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------e
 % Copyright (C) 1993-2004 The University of Melbourne.
 % This file may only be copied under the terms of the GNU General
 % Public License - see the file COPYING in the Mercury distribution.
@@ -176,19 +176,18 @@
 :- pred parse_type_defn_head(module_name::in, term::in, term::in,
 	maybe_functor::out) is det.
 
-	% get_maybe_equality_compare_preds(ModuleName,
-	%		Body0, Body, MaybeEqualPred):
-	%	Checks if `Body0' is a term of the form
-	%		`<body> where equality is <symname>'
-	%		`<body> where comparison is <symname>'
-	%		or `<body> where equality is <symname>,
-	%			comparison is <sym_name>'
-	%	If so, returns the `<body>' in Body and the <symname>s in
-	%	MaybeEqualPred.  If not, returns Body = Body0
-	%	and `no' in MaybeEqualPred.
-
-:- pred get_maybe_equality_compare_preds(module_name::in, term::in, term::out,
-	maybe1(maybe(unify_compare))::out) is det.
+	% parse_type_decl_where_part_if_present(TypeSymName, Arity,
+	% 		IsSolverType, Inst, ModuleName,	Term0, Term, Result):
+	%	Checks if Term0 is a term of the form
+	%		`<body> where <attributes>'
+	%	If so, returns the `<body>' in Term and the parsed
+	%	`<attributes>' in Result.
+	%	If not, returns Term = Term0 and
+	%	Result = no_special_type_details.
+	%
+:- pred parse_type_decl_where_part_if_present(is_solver_type::in,
+		module_name::in, term::in, term::out,
+		maybe1(special_type_details)::out) is det.
 
 %-----------------------------------------------------------------------------%
 
@@ -262,6 +261,7 @@
 
 :- implementation.
 
+:- import_module check_hlds__inst_util.
 :- import_module libs__globals.
 :- import_module libs__options.
 :- import_module parse_tree__modules.
@@ -1519,19 +1519,99 @@
 		condition, maybe1(processed_type_body)).
 :- mode parse_type_decl_type(in, in, in, in, out, out) is semidet.
 
-parse_type_decl_type(ModuleName, "--->", [H, B], Attributes0, Condition, R) :-
-	/* get_condition(...), */
-	Condition = true,
-	get_maybe_equality_compare_preds(ModuleName, B, Body, EqCompare),
+parse_type_decl_type(ModuleName, "--->", [H, B], Attributes0, Condition,
+		Result) :-
+	get_condition(B, Body, Condition),
 	get_is_solver_type(Attributes0, IsSolverType, Attributes),
-	process_du_type(ModuleName, H, Body, IsSolverType, EqCompare, R0),
-	check_no_attributes(R0, Attributes, R).
+	(
+		IsSolverType = solver_type,
+		Result = error("a solver type cannot have data constructors",
+				H)
+	;
+		IsSolverType = non_solver_type,
+		du_type_rhs_ctors_and_where_terms(Body, CtorsTerm,
+			MaybeWhereTerm),
+		CtorsResult = convert_constructors(ModuleName, CtorsTerm),
+		(
+			CtorsResult = error(String, Term),
+			Result      = error(String, Term)
+		;
+			CtorsResult = ok(Ctors),
+			WhereResult = parse_type_decl_where_term(
+					non_solver_type, ModuleName,
+					MaybeWhereTerm),
+			(
+				WhereResult = error(String, Term),
+				Result      = error(String, Term)
+			;
+				WhereResult = ok(SpecialTypeDetails),
+				process_du_type(ModuleName, H, Body, Ctors,
+					SpecialTypeDetails, Result0),
+				check_no_attributes(Result0, Attributes,
+					Result)
+			)
+		)
+	).
 
 parse_type_decl_type(ModuleName, "==", [H, B], Attributes, Condition, R) :-
 	get_condition(B, Body, Condition),
 	process_eqv_type(ModuleName, H, Body, R0),
 	check_no_attributes(R0, Attributes, R).
 
+parse_type_decl_type(ModuleName, "where", [H, B], Attributes0, Condition,
+		R) :-
+	get_condition(B, Body, Condition),
+	get_is_solver_type(Attributes0, IsSolverType, Attributes),
+	(
+		IsSolverType = non_solver_type,
+		R = error("only solver types can be defined " ++
+				"by a `where' block alone", H)
+	;
+		IsSolverType = solver_type,
+		R0 = parse_type_decl_where_term(solver_type, ModuleName,
+			yes(Body)),
+		(
+			R0 = error(String, Term),
+			R  = error(String, Term)
+		;
+			R0 = ok(SpecialTypeDetails),
+			process_solver_type(ModuleName, H, SpecialTypeDetails,
+				R1),
+			check_no_attributes(R1, Attributes, R)
+		)
+	).
+
+
+:- pred term_to_sym_name_and_arity(term::in, module_name::in,
+		sym_name::out, arity::out) is det.
+
+	% A malformed type head error is caught elsewhere in
+	% parse_type_decl_type.
+	%
+term_to_sym_name_and_arity(Term, ModuleName, SymName, Arity) :-
+	( if Term = term__functor(term__atom(Name), Args, _Context) then
+		SymName = qualified(ModuleName, Name),
+		Arity   = length(Args)
+	  else
+	  	SymName = unqualified("shouldn't see this"),
+		Arity   = -1
+	).
+
+
+:- pred du_type_rhs_ctors_and_where_terms(term::in,
+		term::out, maybe(term)::out) is det.
+
+du_type_rhs_ctors_and_where_terms(Term, CtorsTerm, MaybeWhereTerm) :-
+	( if Term = term__functor(term__atom("where"),
+			[CtorsTerm0, WhereTerm], _Context)
+	  then
+	  	CtorsTerm      = CtorsTerm0,
+		MaybeWhereTerm = yes(WhereTerm)
+	  else
+	  	CtorsTerm      = Term,
+		MaybeWhereTerm = no
+	).
+
 %-----------------------------------------------------------------------------%
 
 	% parse_type_decl_pred(ModuleName, VarSet, Pred, Attributes, Result)
@@ -1653,81 +1733,361 @@
 
 %-----------------------------------------------------------------------------%
 
-get_maybe_equality_compare_preds(ModuleName, B, Body, MaybeEqComp) :-
+	% The optional `where ...' part of the type definition syntax 
+	% is a comma separated list of special type `attributes'.
+	%
+	% The possible attributes (in this order) are either
+	% - `type_is_abstract_noncanonical' on its own appears only in .int2
+	%   files and indicates that the type has user-defined equality and/or
+	%   comparison, but that what these predicates are is not known at
+	%   this point
+	% or
+	% - `representation is <<type name>>' (required for solver types)
+	% - `initialisation is <<pred name>>' (required for solver types)
+	% - `ground is <<inst>>' (required for solver types)
+	% - `any is <<inst>>' (required for solver types)
+	% - `equality is <<pred name>>' (optional)
+	% - `comparison is <<pred name>>' (optional).
+	%
+parse_type_decl_where_part_if_present(IsSolverType, ModuleName, Term0, Term,
+		Result) :-
+	(
+		Term0  = term__functor(term__atom("where"), [Term1, WhereTerm],
+				_Context)
+	->
+		Term   = Term1,
+		Result = parse_type_decl_where_term(IsSolverType, ModuleName,
+				yes(WhereTerm))
+	;
+		Term   = Term0,
+		Result = ok(no_special_type_details)
+	).
+
+
+:- func parse_type_decl_where_term(is_solver_type, module_name, maybe(term)) =
+		maybe1(special_type_details).
+
+parse_type_decl_where_term(_IsSolverType, _ModuleName, no) =
+	ok(no_special_type_details).
+
+parse_type_decl_where_term(IsSolverType, ModuleName, MaybeTerm0 @ yes(Term)) =
+		MaybeSpecialTypeDetails :-
+	some [!MaybeTerm] (
+		!:MaybeTerm = MaybeTerm0,
+		parse_where_attribute(
+			parse_where_type_is_abstract_noncanonical,
+			TypeIsAbstractNoncanonicalResult, !MaybeTerm),
+		parse_where_attribute(
+			parse_where_is("representation",
+				parse_where_type_is(ModuleName)),
+			RepresentationIsResult, !MaybeTerm),
+		parse_where_attribute(
+			parse_where_initialisation_is(ModuleName),
+			InitialisationIsResult, !MaybeTerm),
+		parse_where_attribute(
+			parse_where_is("ground",
+				parse_where_inst_is(ModuleName)),
+			GroundIsResult, !MaybeTerm),
+		parse_where_attribute(
+			parse_where_is("any",
+				parse_where_inst_is(ModuleName)),
+			AnyIsResult, !MaybeTerm),
+		parse_where_attribute(
+			parse_where_is("equality",
+				parse_where_pred_is(ModuleName)),
+			EqualityIsResult, !MaybeTerm),
+		parse_where_attribute(
+			parse_where_is("comparison",
+				parse_where_pred_is(ModuleName)),
+			ComparisonIsResult, !MaybeTerm),
+		parse_where_end(!.MaybeTerm, WhereEndResult)
+	),
+	MaybeSpecialTypeDetails =
+		make_maybe_special_type_details(
+			IsSolverType,
+			TypeIsAbstractNoncanonicalResult,
+			RepresentationIsResult,
+			InitialisationIsResult,
+			GroundIsResult,
+			AnyIsResult,
+			EqualityIsResult,
+			ComparisonIsResult,
+			WhereEndResult,
+			Term
+		).
+
+
+	% parse_where_attribute(Parser, Result, MaybeTerm0, MaybeTerm)
+	% handles
+	% - where MaybeTerm0 may contain nothing
+	% - where MaybeTerm0 may be a comma-separated pair
+	% - applies Parser to the appropriate (sub)term to obtain Result
+	% - sets MaybeTerm depending upon whether the Result is an error
+	% or not and whether there is more to parse because MaybeTerm0
+	% was a comma-separated pair.
+	%
+:- pred parse_where_attribute((func(term) = maybe1(maybe(T)))::in,
+		maybe1(maybe(T))::out, maybe(term)::in, maybe(term)::out)
+			is det.
+
+parse_where_attribute(_Parser, ok(no), no,         no       ).
+
+parse_where_attribute( Parser, Result, yes(Term0), MaybeRest) :-
 	(
-		B = term__functor(term__atom("where"), Args, _Context1),
-		Args = [Body1, EqCompTerm]
+		Term0 = term__functor(term__atom(","), [Term1, Term], _Context)
+	->
+		Result         = Parser(Term1),
+		MaybeRestIfYes = yes(Term)
+	;
+		Result         = Parser(Term0),
+		MaybeRestIfYes = no
+	),
+	(
+		Result = error(_, _),
+		MaybeRest = no
+	;
+		Result = ok(no),
+		MaybeRest = yes(Term0)
+	;
+		Result = ok(yes(_)),
+		MaybeRest = MaybeRestIfYes
+	).
+
+
+	% Parser for `where ...' attributes of the form
+	% `attributename is attributevalue'.
+	%
+:- func parse_where_is(string, func(term) = maybe1(T), term) =
+		maybe1(maybe(T)).
+
+parse_where_is(Name, Parser, Term) = Result :-
+	(
+		Term = term__functor(term__atom("is"), [LHS, RHS], _Context1)
 	->
-		Body = Body1,
 		(
-			EqCompTerm = term__functor(
-				term__atom("type_is_abstract_noncanonical"),
-				[], _Context2)
+			LHS = term__functor(term__atom(Name), [], _Context2)
 		->
-			MaybeEqComp = ok(yes(abstract_noncanonical_type))
-		;
-			parse_equality_or_comparison_pred_term("equality",
-				EqCompTerm, PredName)
-		->
-			parse_implicitly_qualified_symbol_name(ModuleName,
-				PredName, MaybeEqComp0),
-			process_maybe1(make_equality, MaybeEqComp0,
-				MaybeEqComp)
-		;
-			parse_equality_or_comparison_pred_term("comparison",
-				EqCompTerm, PredName)
-		->
-			parse_implicitly_qualified_symbol_name(ModuleName,
-				PredName, MaybeEqComp0),
-			process_maybe1(make_comparison, MaybeEqComp0,
-				MaybeEqComp)
-		;
-			EqCompTerm = term__functor(term__atom(","),
-					[EqTerm, CompTerm], _),
-			parse_equality_or_comparison_pred_term("equality",
-				EqTerm, EqPredNameTerm),
-			parse_equality_or_comparison_pred_term("comparison",
-				CompTerm, CompPredNameTerm)
-		->
-			parse_implicitly_qualified_symbol_name(ModuleName,
-				EqPredNameTerm, EqPredNameResult),
-			parse_implicitly_qualified_symbol_name(ModuleName,
-				CompPredNameTerm, CompPredNameResult),
+			Result0 = Parser(RHS),
 			(
-				EqPredNameResult = ok(EqPredName),
-				CompPredNameResult = ok(CompPredName),
-				MaybeEqComp = ok(yes(
-					unify_compare(yes(EqPredName),
-						yes(CompPredName))))
-			;
-				EqPredNameResult = ok(_),
-				CompPredNameResult = error(M, T),
-				MaybeEqComp = error(M, T)
+				Result0 = ok(X),
+				Result  = ok(yes(X))
 			;
-				EqPredNameResult = error(M, T),
-				MaybeEqComp = error(M, T)
+				Result0 = error(Msg, ProblemTerm),
+				Result  = error(Msg, ProblemTerm)
 			)
 		;
-			MaybeEqComp = error("syntax error after `where'",
-				Body)
+			Result = ok(no)
 		)
 	;
-		Body = B,
-		MaybeEqComp = ok(no)
+		Result = error("expected is/2", Term)
+	).
+
+
+:- func parse_where_type_is_abstract_noncanonical(term) = maybe1(maybe(unit)).
+
+parse_where_type_is_abstract_noncanonical(Term) =
+	(
+		Term = term__functor(
+				term__atom("type_is_abstract_noncanonical"),
+				[],
+				_Context)
+	->
+		ok(yes(unit))
+	;
+		ok(no)
+	).
+
+
+:- func parse_where_initialisation_is(module_name, term) =
+		maybe1(maybe(sym_name)).
+
+parse_where_initialisation_is(ModuleName, Term) = Result :-
+	Result0 = parse_where_is("initialisation",
+			parse_where_pred_is(ModuleName), Term),
+	(
+		Result0 = ok(no)
+	->
+		Result  = parse_where_is("initialization",
+				parse_where_pred_is(ModuleName), Term)
+	;
+		Result  = Result0
+	).
+
+
+:- func parse_where_pred_is(module_name, term) = maybe1(sym_name).
+
+parse_where_pred_is(ModuleName, Term) = Result :-
+	parse_implicitly_qualified_symbol_name(ModuleName, Term, Result).
+
+
+:- func parse_where_inst_is(module_name, term) = maybe1(inst).
+
+parse_where_inst_is(_ModuleName, Term) =
+	( if
+		prog_io_util__convert_inst(no_allow_constrained_inst_var,
+			Term, Inst),
+		not inst_util__inst_contains_unconstrained_var(Inst)
+	  then ok(Inst)
+	  else error("expected a ground, unconstrained inst", Term)
+	).
+
+
+:- func parse_where_type_is(module_name, term) = maybe1(type).
+
+parse_where_type_is(_ModuleName, Term) = ok(Type) :-
+	prog_io_util__convert_type(Term, Type).
+
+
+:- pred parse_where_end(maybe(term)::in, maybe1(maybe(unit))::out) is det.
+
+parse_where_end(no,        ok(yes(unit))).
+
+parse_where_end(yes(Term), error("attributes are either badly ordered or " ++
+				"contain an unrecognised attribute", Term)).
+
+
+:- func make_maybe_special_type_details(
+		is_solver_type,
+		maybe1(maybe(unit)),
+		maybe1(maybe(type)),
+		maybe1(maybe(init_pred)),
+		maybe1(maybe(inst)),
+		maybe1(maybe(inst)),
+		maybe1(maybe(equality_pred)),
+		maybe1(maybe(comparison_pred)),
+		maybe1(maybe(unit)),
+		term
+	) = maybe1(special_type_details).
+
+make_maybe_special_type_details(
+		IsSolverType,
+		TypeIsAbstractNoncanonicalResult,
+		RepresentationIsResult,
+		InitialisationIsResult,
+		GroundIsResult,
+		AnyIsResult,
+		EqualityIsResult,
+		ComparisonIsResult,
+		WhereEndResult,
+		WhereTerm) =
+	(
+		TypeIsAbstractNoncanonicalResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		RepresentationIsResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		InitialisationIsResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		GroundIsResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		AnyIsResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		EqualityIsResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		ComparisonIsResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		WhereEndResult = error(String, Term)
+	->
+		error(String, Term)
+	;
+		TypeIsAbstractNoncanonicalResult = ok(yes(_))
+	->
+		(
+			RepresentationIsResult = ok(no),
+			InitialisationIsResult = ok(no),
+			GroundIsResult         = ok(no),
+			AnyIsResult            = ok(no),
+			EqualityIsResult       = ok(no),
+			ComparisonIsResult     = ok(no)
+		->
+			ok(abstract_noncanonical_type(IsSolverType))
+		;
+			error("`where type_is_abstract_noncanonical' " ++
+				" excludes other `where ...' attributes",
+				WhereTerm)
+		)
+	;
+		IsSolverType = solver_type
+	->
+		(
+			RepresentationIsResult = ok(yes(RepnType)),
+			InitialisationIsResult = ok(yes(InitPred)),
+			GroundIsResult         = ok(yes(GroundInst)),
+			AnyIsResult            = ok(yes(AnyInst)),
+			EqualityIsResult       = ok(MaybeEqPred),
+			ComparisonIsResult     = ok(MaybeCmpPred)
+		->
+			ok(special_type_details(
+				yes(solver_type_details(RepnType, InitPred,
+					GroundInst, AnyInst)),
+				MaybeEqPred,
+				MaybeCmpPred
+			))
+		;
+			error("missing solver type attribute: " ++
+				"required solver type attributes are " ++
+				"`representation', `initialisation', " ++
+				"`ground', and `any'", WhereTerm)
+		)
+	;
+		% Here we know IsSolverType = non_solver_type, so...
+
+		(	RepresentationIsResult = ok(yes(_))
+		;	InitialisationIsResult = ok(yes(_))
+		;	GroundIsResult         = ok(yes(_))
+		;	AnyIsResult            = ok(yes(_))
+		)
+	->
+		error("solver type attribute given for non-solver type",
+			WhereTerm)
+	;
+		EqualityIsResult = ok(MaybeEqPred),
+		ComparisonIsResult = ok(MaybeCmpPred)
+	->
+		ok(special_type_details(no, MaybeEqPred, MaybeCmpPred))
+	;
+		error("prog_io__make_maybe_special_type_details: " ++
+			"shouldn't have reached this point!", WhereTerm)
 	).
 
-:- pred parse_equality_or_comparison_pred_term(string::in, term::in,
-		term::out) is semidet.
 
-parse_equality_or_comparison_pred_term(EqOrComp, Term, PredNameTerm) :-
-	Term = term__functor(term__atom("is"),
-		[term__functor(term__atom(EqOrComp), [], _), PredNameTerm], _).
+:- func solver_inst_cast_sym_name(sym_name, arity) = sym_name.
+
+solver_inst_cast_sym_name(TypeSymName, TypeArity) =
+	unqualified_sym_name_with_prefix_suffix("inst cast ", TypeSymName,
+		"/" ++ int_to_string(TypeArity)).
+
+
+:- func solver_inst_sym_name(sym_name, arity) = sym_name.
+
+solver_inst_sym_name(TypeSymName, TypeArity) =
+	unqualified_sym_name_with_prefix_suffix("", TypeSymName,
+		"/" ++ int_to_string(TypeArity) ++ " inst").
 
-:- pred make_equality(sym_name::in, maybe(unify_compare)::out) is det.
-make_equality(Pred, yes(unify_compare(yes(Pred), no))).
 
-:- pred make_comparison(sym_name::in, maybe(unify_compare)::out) is det.
-make_comparison(Pred, yes(unify_compare(no, yes(Pred)))).
+:- func unqualified_sym_name_with_prefix_suffix(string, sym_name, string) =
+		sym_name.
+
+unqualified_sym_name_with_prefix_suffix(Prefix, unqualified(Name), Suffix) =
+	unqualified(Prefix ++ Name ++ Suffix).
+
+unqualified_sym_name_with_prefix_suffix(Prefix, 
+		qualified(ModuleSpecifier, Name), Suffix) =
+	qualified(ModuleSpecifier, Prefix ++ Name ++ Suffix).
+
 
 	% get_determinism(Term0, Term, Determinism) binds Determinism
 	% to a representation of the determinism condition of Term0, if any,
@@ -1842,6 +2202,37 @@
 
 %-----------------------------------------------------------------------------%
 
+:- pred process_solver_type(module_name::in, term::in,
+		special_type_details::in, maybe1(processed_type_body)::out)
+			is det.
+
+process_solver_type(ModuleName, Head, SpecialTypeDetails, Result) :-
+	dummy_term(Body),
+	parse_type_defn_head(ModuleName, Head, Body, Result0),
+	(
+		Result0 = error(String, Term),
+		Result  = error(String, Term)
+	;
+		Result0 = ok(Name, Args0),
+		(
+			SpecialTypeDetails ^ solver_type_details =
+				yes(SolverTypeDetails),
+			RepnType = SolverTypeDetails ^ representation_type,
+			term__contains_var(RepnType, Var),
+			not term__contains_var_list(Args0,
+				term__coerce_var(Var))
+		->
+			Result = error("free type variable in " ++
+					"representation type", Head)
+		;
+			list__map(term__coerce, Args0, Args),
+			Result = ok(processed_type_body(Name, Args,
+					solver_type(SpecialTypeDetails)))
+		)
+	).
+
+%-----------------------------------------------------------------------------%
+
 	% This is for "Head == Body" (equivalence) definitions.
 :- pred process_eqv_type(module_name, term, term, maybe1(processed_type_body)).
 :- mode process_eqv_type(in, in, in, out) is det.
@@ -1849,8 +2240,8 @@
 	parse_type_defn_head(ModuleName, Head, Body, Result0),
 	process_eqv_type_2(Result0, Body, Result).
 
-:- pred process_eqv_type_2(maybe_functor, term, maybe1(processed_type_body)).
-:- mode process_eqv_type_2(in, in, out) is det.
+:- pred process_eqv_type_2(maybe_functor::in, term::in,
+		maybe1(processed_type_body)::out) is det.
 process_eqv_type_2(error(Error, Term), _, error(Error, Term)).
 process_eqv_type_2(ok(Name, Args0), Body0, Result) :-
 	% check that all the variables in the body occur in the head
@@ -1860,8 +2251,8 @@
 			\+ term__contains_var_list(Args0, Var2)
 		)
 	->
-		Result = error("free type parameter in RHS of type definition",
-				Body0)
+		Result = error("free type parameter in RHS of " ++
+				"type definition", Body0)
 	;
 		list__map(term__coerce, Args0, Args),
 		convert_type(Body0, Body),
@@ -1870,104 +2261,106 @@
 
 %-----------------------------------------------------------------------------%
 
-	% process_du_type(ModuleName, TypeHead, TypeBody, Result)
+	% process_du_type(ModuleName, TypeHead, TypeBody,
+	% 	MaybeSpecialTypeDetails, Result)
 	% checks that its arguments are well formed, and if they are,
 	% binds Result to a representation of the type information about the
 	% TypeHead.
-	% This is for "Head ---> Body" (constructor) definitions.
-:- pred process_du_type(module_name, term, term, is_solver_type,
-		maybe1(maybe(unify_compare)), maybe1(processed_type_body)).
-:- mode process_du_type(in, in, in, in, in, out) is det.
-process_du_type(ModuleName, Head, Body, IsSolverType, EqualityPred, Result) :-
+	% This is for "Head ---> Body [where ...]" (constructor) definitions.
+
+:- pred process_du_type(module_name::in, term::in, term::in,
+		list(constructor)::in, special_type_details::in,
+		maybe1(processed_type_body)::out) is det.
+
+process_du_type(ModuleName, Head, Body, Ctors, SpecialTypeDetails, Result) :-
 	parse_type_defn_head(ModuleName, Head, Body, Result0),
-	process_du_type_2(ModuleName, Result0, Body, IsSolverType,
-		EqualityPred, Result).
+	(
+		Result0 = error(String, Term),
+		Result  = error(String, Term)
+	;
+		Result0 = ok(Functor, Args),
+		process_du_type_2(Functor, Args, Body, Ctors,
+			SpecialTypeDetails, Result)
+	).
+
+
+:- pred process_du_type_2(sym_name::in, list(term)::in, term::in,
+		list(constructor)::in, special_type_details::in,
+		maybe1(processed_type_body)::out) is det.
+
+process_du_type_2(Functor, Args0, Body, Ctors, SpecialTypeDetails, Result) :-
 
-:- pred process_du_type_2(module_name, maybe_functor, term, is_solver_type,
-		maybe1(maybe(unify_compare)), maybe1(processed_type_body)).
-:- mode process_du_type_2(in, in, in, in, in, out) is det.
-process_du_type_2(_, error(Error, Term), _, _, _, error(Error, Term)).
-process_du_type_2(ModuleName, ok(Functor, Args0), Body, IsSolverType,
-		MaybeEqualityPred, Result) :-
 	% check that body is a disjunction of constructors
 	list__map(term__coerce, Args0, Args),
-	(
-		convert_constructors(ModuleName, Body, Constrs)
-	->
-		% check that all type variables in the body
-		% are either explicitly existentially quantified
-		% or occur in the head.
-		(
-			list__member(Ctor, Constrs),
-			Ctor = ctor(ExistQVars, _Constraints, _CtorName,
-					CtorArgs),
-			assoc_list__values(CtorArgs, CtorArgTypes),
-			term__contains_var_list(CtorArgTypes, Var),
-			\+ list__member(Var, ExistQVars),
-			\+ term__contains_var_list(Args, Var)
-		->
-			Result = error(
-			"free type parameter in RHS of type definition",
-					Body)
 
-		% check that all type variables in existential quantifiers
-		% do not occur in the head
-		% (maybe this should just be a warning, not an error?
-		% If we were to allow it, we would need to rename them apart.)
-		;
-			list__member(Ctor, Constrs),
-			Ctor = ctor(ExistQVars, _Constraints, _CtorName,
-					_CtorArgs),
-			list__member(Var, ExistQVars),
-			term__contains_var_list(Args, Var)
-		->
-			Result = error( "type variable has overlapping scopes (explicit type quantifier shadows argument type)", Body)
-
-		% check that all type variables in existential quantifiers
-		% occur somewhere in the constructor argument types
-		% (not just the constraints)
-		;
-			list__member(Ctor, Constrs),
-			Ctor = ctor(ExistQVars, _Constraints, _CtorName,
-					CtorArgs),
-			list__member(Var, ExistQVars),
-			assoc_list__values(CtorArgs, CtorArgTypes),
-			\+ term__contains_var_list(CtorArgTypes, Var)
-		->
-			Result = error(
-"type variable in existential quantifier does not occur in arguments of constructor",
-					Body)
-		% check that all type variables in existential constraints
-		% occur in the existential quantifiers
-		% (XXX is this check overly conservative? Perhaps we should
-		% allow existential constraints so long as they contain
-		% at least one type variable which is existentially quantified,
-		% rather than requiring all variables in them to be
-		% existentially quantified.)
-		;
-			list__member(Ctor, Constrs),
-			Ctor = ctor(ExistQVars, Constraints, _CtorName,
-					_CtorArgs),
-			list__member(Constraint, Constraints),
-			Constraint = constraint(_Name, ConstraintArgs),
-			term__contains_var_list(ConstraintArgs, Var),
-			\+ list__member(Var, ExistQVars)
-		->
-			Result = error("type variables in class constraints introduced with `=>' must be explicitly existentially quantified using `some'",
-					Body)
-		;
-			(
-				MaybeEqualityPred = ok(EqualityPred),
-				Result = ok(processed_type_body(Functor, Args,
-					du_type(Constrs, IsSolverType,
-						EqualityPred)))
-			;
-				MaybeEqualityPred = error(Error, Term),
-				Result = error(Error, Term)
-			)
-		)
+	% check that all type variables in the body
+	% are either explicitly existentially quantified
+	% or occur in the head.
+	(
+		list__member(Ctor, Ctors),
+		Ctor = ctor(ExistQVars, _Constraints, _CtorName,
+				CtorArgs),
+		assoc_list__values(CtorArgs, CtorArgTypes),
+		term__contains_var_list(CtorArgTypes, Var),
+		\+ list__member(Var, ExistQVars),
+		\+ term__contains_var_list(Args, Var)
+	->
+		Result = error("free type parameter in RHS of " ++
+				"type definition", Body)
+
+	% check that all type variables in existential quantifiers
+	% do not occur in the head
+	% (maybe this should just be a warning, not an error?
+	% If we were to allow it, we would need to rename them apart.)
+	;
+		list__member(Ctor, Ctors),
+		Ctor = ctor(ExistQVars, _Constraints, _CtorName,
+				_CtorArgs),
+		list__member(Var, ExistQVars),
+		term__contains_var_list(Args, Var)
+	->
+		Result = error( "type variable has overlapping " ++
+				"scopes (explicit type quantifier " ++
+				"shadows argument type)", Body)
+
+	% check that all type variables in existential quantifiers
+	% occur somewhere in the constructor argument types
+	% (not just the constraints)
+	;
+		list__member(Ctor, Ctors),
+		Ctor = ctor(ExistQVars, _Constraints, _CtorName,
+				CtorArgs),
+		list__member(Var, ExistQVars),
+		assoc_list__values(CtorArgs, CtorArgTypes),
+		\+ term__contains_var_list(CtorArgTypes, Var)
+	->
+		Result = error("type variable in existential " ++
+				"quantifier does not occur in " ++
+				"arguments of constructor", Body)
+	% check that all type variables in existential constraints
+	% occur in the existential quantifiers
+	% (XXX is this check overly conservative? Perhaps we should
+	% allow existential constraints so long as they contain
+	% at least one type variable which is existentially quantified,
+	% rather than requiring all variables in them to be
+	% existentially quantified.)
+	;
+		list__member(Ctor, Ctors),
+		Ctor = ctor(ExistQVars, Constraints, _CtorName,
+				_CtorArgs),
+		list__member(Constraint, Constraints),
+		Constraint = constraint(_Name, ConstraintArgs),
+		term__contains_var_list(ConstraintArgs, Var),
+		\+ list__member(Var, ExistQVars)
+	->
+		Result = error("type variables in class " ++
+				"constraints introduced " ++
+				"with `=>' must be explicitly " ++
+				"existentially quantified " ++
+				"using `some'", Body)
 	;
-		Result = error("invalid RHS of type definition", Body)
+		Result = ok(processed_type_body(Functor, Args,
+				du_type(Ctors, SpecialTypeDetails)))
 	).
 
 %-----------------------------------------------------------------------------%
@@ -2013,18 +2406,18 @@
 	;
 		parse_implicitly_qualified_term(ModuleName,
 			Head, Head, "type definition", R),
-		parse_type_defn_head_2(R, Body, Head, Result)
+		parse_type_defn_head_2(R, Head, Result)
 	).
 
-:- pred parse_type_defn_head_2(maybe_functor, term, term, maybe_functor).
-:- mode parse_type_defn_head_2(in, in, in, out) is det.
-parse_type_defn_head_2(error(Msg, Term), _, _, error(Msg, Term)).
-parse_type_defn_head_2(ok(Name, Args), Body, Head, Result) :-
-	parse_type_defn_head_3(Name, Args, Body, Head, Result).
-
-:- pred parse_type_defn_head_3(sym_name, list(term), term, term, maybe_functor).
-:- mode parse_type_defn_head_3(in, in, in, in, out) is det.
-parse_type_defn_head_3(Name, Args, _Body, Head, Result) :-
+:- pred parse_type_defn_head_2(maybe_functor, term, maybe_functor).
+:- mode parse_type_defn_head_2(in, in, out) is det.
+parse_type_defn_head_2(error(Msg, Term), _, error(Msg, Term)).
+parse_type_defn_head_2(ok(Name, Args), Head, Result) :-
+	parse_type_defn_head_3(Name, Args, Head, Result).
+
+:- pred parse_type_defn_head_3(sym_name, list(term), term, maybe_functor).
+:- mode parse_type_defn_head_3(in, in, in, out) is det.
+parse_type_defn_head_3(Name, Args, Head, Result) :-
 	% check that all the head args are variables
 	( %%%	some [Arg]
 		(
@@ -2051,55 +2444,120 @@
 
 	% Convert a list of terms separated by semi-colons
 	% (known as a "disjunction", even thought the terms aren't goals
-	% in this case) into a list of constructors
+	% in this case) into a list of constructors.
 
-:- pred convert_constructors(module_name, term, list(constructor)).
-:- mode convert_constructors(in, in, out) is semidet.
-convert_constructors(ModuleName, Body, Constrs) :-
+:- func convert_constructors(module_name, term) = maybe1(list(constructor)).
+
+convert_constructors(ModuleName, Body) = Result :-
 	disjunction_to_list(Body, List),
-	convert_constructors_2(ModuleName, List, Constrs).
+	Result0 = convert_constructors_2(ModuleName, List),
+	(
+		Result0 = ok(Constructors),
+		Result  = ok(Constructors)
+	;
+		Result0 = error(String, Term),
+		Result  = error(String, Term)
+	).
 
 	% true if input argument is a valid list of constructors
 
-:- pred convert_constructors_2(module_name, list(term), list(constructor)).
-:- mode convert_constructors_2(in, in, out) is semidet.
-convert_constructors_2(_, [], []).
-convert_constructors_2(ModuleName, [Term | Terms], [Constr | Constrs]) :-
-	convert_constructor(ModuleName, Term, Constr),
-	convert_constructors_2(ModuleName, Terms, Constrs).
-
-	% true if input argument is a valid constructor.
-
-:- pred convert_constructor(module_name, term, constructor).
-:- mode convert_constructor(in, in, out) is semidet.
-convert_constructor(ModuleName, Term0, Result) :-
-	(
-		Term0 = term__functor(term__atom("some"), [Vars, Term1], _)
-	->
-		parse_list_of_vars(Vars, ExistQVars0),
-		list__map(term__coerce_var, ExistQVars0, ExistQVars),
-		Term2 = Term1
+
+:- func convert_constructors_2(module_name, list(term)) =
+		maybe1(list(constructor)).
+
+convert_constructors_2(_ModuleName, []) = ok([]).
+
+convert_constructors_2( ModuleName, [Term | Terms]) = Result :-
+	Result0 = convert_constructor(ModuleName, Term),
+	(
+		Result0 = error(String0, Term0),
+		Result  = error(String0, Term0)
 	;
-		ExistQVars = [],
-		Term2 = Term0
-	),
-	get_existential_constraints_from_term(ModuleName, Term2, Term3,
-		ok(Constraints)),
+		Result0 = ok(Constructor),
+		Result1 = convert_constructors_2(ModuleName, Terms),
+		(
+			Result1 = error(String1, Term1),
+			Result  = error(String1, Term1)
+		;
+			Result1 = ok(Constructors),
+			Result  = ok([Constructor | Constructors])
+		)
+	).
+
+
+:- func convert_constructor(module_name, term) =
+		maybe1(constructor).
+
+convert_constructor(ModuleName, Term0) = Result :-
 	(
-		% Note that as a special case, one level of
-		% curly braces around the constructor are ignored.
-		% This is to allow you to define ';'/2 and 'some'/2
-		% constructors.
-		Term3 = term__functor(term__atom("{}"), [Term4], _Context)
+		Term0 = term__functor(term__atom("some"), [Vars, Term1], 
+				_Context)
 	->
-		Term5 = Term4
+		(
+			parse_list_of_vars(Vars, ExistQVars0)
+		->
+			list__map(term__coerce_var, ExistQVars0, ExistQVars),
+			Result = convert_constructor_2(ModuleName, ExistQVars,
+					Term0, Term1)
+		;
+			Result = error("syntax error in variable list", Term0)
+		)
 	;
-		Term5 = Term3
-	),
+		ExistQVars = [],
+		Result = convert_constructor_2(ModuleName, ExistQVars,
+				Term0, Term0)
+	).
+
+
+:- func convert_constructor_2(module_name, list(tvar), term, term) =
+		maybe1(constructor).
+
+convert_constructor_2(ModuleName, ExistQVars, Term0, Term1) = Result :-
+	get_existential_constraints_from_term(ModuleName, Term1, Term2,
+		Result0),
+	(
+		Result0 = error(String, Term),
+		Result  = error(String, Term)
+	;
+		Result0 = ok(Constraints),
+		(
+			% Note that as a special case, one level of
+			% curly braces around the constructor are ignored.
+			% This is to allow you to define ';'/2 and 'some'/2
+			% constructors.
+			Term2 = term__functor(term__atom("{}"), [Term3],
+					_Context)
+		->
+			Term4 = Term3
+		;
+			Term4 = Term2
+		),
+		Result  = convert_constructor_3(ModuleName, ExistQVars,
+				Constraints, Term0, Term4)
+	).
+
+
+:- func convert_constructor_3(module_name, list(tvar),
+		list(class_constraint), term, term) = maybe1(constructor).
+
+convert_constructor_3(ModuleName, ExistQVars, Constraints, Term0, Term1) =
+		Result :-
 	parse_implicitly_qualified_term(ModuleName,
-		Term5, Term0, "constructor definition", ok(F, As)),
-	convert_constructor_arg_list(ModuleName, As, Args),
-	Result = ctor(ExistQVars, Constraints, F, Args).
+		Term1, Term0, "constructor definition", Result0),
+	(
+		Result0 = error(String, Term),
+		Result  = error(String, Term)
+	;
+		Result0 = ok(F, As),
+		Result1 = convert_constructor_arg_list(ModuleName, As),
+		(
+			Result1 = error(String, Term),
+			Result  = error(String, Term)
+		;
+			Result1 = ok(Args),
+			Result  = ok(ctor(ExistQVars, Constraints, F, Args))
+		)
+	).
 
 %-----------------------------------------------------------------------------%
 
@@ -3672,25 +4130,56 @@
 parse_type(T0, ok(T)) :-
 	convert_type(T0, T).
 
-:- pred convert_constructor_arg_list(module_name,
-		list(term), list(constructor_arg)).
-:- mode convert_constructor_arg_list(in, in, out) is semidet.
+:- func convert_constructor_arg_list(module_name, list(term)) =
+		maybe1(list(constructor_arg)).
+
+convert_constructor_arg_list(_ModuleName, []) = ok([]).
 
-convert_constructor_arg_list(_, [], []).
-convert_constructor_arg_list(ModuleName, [Term | Terms], [Arg | Args]) :-
+convert_constructor_arg_list( ModuleName, [Term | Terms]) = Result :-
 	(
-		Term = term__functor(term__atom("::"), [NameTerm, TypeTerm], _)
+		Term = term__functor(term__atom("::"), [NameTerm, TypeTerm],
+				_)
 	->
 		parse_implicitly_qualified_term(ModuleName, NameTerm, Term,
 			"field name", NameResult),
-		NameResult = ok(SymName, []),
-		convert_type(TypeTerm, Type),
-		Arg = yes(SymName) - Type
+		(
+			NameResult = error(String1, Term1),
+			Result     = error(String1, Term1)
+		;
+			NameResult = ok(_SymName, [_ | _]),
+			Result     = error("syntax error in " ++
+					   "constructor name", Term)
+		;
+			NameResult = ok(SymName, []),
+			MaybeFieldName = yes(SymName),
+			Result     = convert_constructor_arg_list_2(
+					ModuleName, MaybeFieldName,
+					TypeTerm, Terms)
+		)
 	;
-		convert_type(Term, Type),
-		Arg = no - Type
-	),
-	convert_constructor_arg_list(ModuleName, Terms, Args).
+		MaybeFieldName = no,
+		TypeTerm       = Term,
+		Result         = convert_constructor_arg_list_2(
+					ModuleName, MaybeFieldName,
+					TypeTerm, Terms)
+	).
+
+
+:- func convert_constructor_arg_list_2(module_name, maybe(sym_name), term,
+		list(term)) = maybe1(list(constructor_arg)).
+
+convert_constructor_arg_list_2(ModuleName, MaybeFieldName, TypeTerm, Terms) =
+		Result :-
+	convert_type(TypeTerm, Type),
+	Arg     = MaybeFieldName - Type,
+	Result0 = convert_constructor_arg_list(ModuleName, Terms),
+	(
+		Result0 = error(String, Term),
+		Result  = error(String, Term)
+	;
+		Result0 = ok(Args),
+		Result  = ok([Arg | Args])
+	).
 
 %-----------------------------------------------------------------------------%
 
Index: prog_io_pragma.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.70
diff -u -r1.70 prog_io_pragma.m
--- prog_io_pragma.m	6 Jul 2004 04:18:50 -0000	1.70
+++ prog_io_pragma.m	16 Jul 2004 03:19:55 -0000
@@ -35,18 +35,19 @@
 	(
 		% new syntax: `:- pragma foo(...).'
 		PragmaTerms = [SinglePragmaTerm0],
-		get_maybe_equality_compare_preds(ModuleName,
-			SinglePragmaTerm0, SinglePragmaTerm,
-			UnifyCompareResult),
+		parse_type_decl_where_part_if_present(
+			non_solver_type, ModuleName, SinglePragmaTerm0,
+			SinglePragmaTerm, WherePartResult),
 		SinglePragmaTerm = term__functor(term__atom(PragmaType),
-			PragmaArgs, _),
+					PragmaArgs, _),
 		parse_pragma_type(ModuleName, PragmaType, PragmaArgs,
-			SinglePragmaTerm, VarSet, Result0)
+				SinglePragmaTerm, VarSet, Result0)
 	->
 		(
-			UnifyCompareResult = ok(MaybeUserEqCompare),
+			WherePartResult = ok(SpecialTypeDetails),
 			(
-				MaybeUserEqCompare = yes(_),
+				prog_data__has_user_defined_equality(
+					SpecialTypeDetails),
 				Result0 = ok(Item0)
 			->
 				(
@@ -56,7 +57,7 @@
 				->
 					Result = ok(Item0 ^ td_ctor_defn :=
 						foreign_type(Type,
-							MaybeUserEqCompare,
+							SpecialTypeDetails,
 							Assertions))
 				;
 					Result = error(
@@ -67,8 +68,8 @@
 				Result = Result0
 			)
 		;
-			UnifyCompareResult = error(Msg, Term),
-			Result = error(Msg, Term)
+			WherePartResult = error(String, Term),
+			Result          = error(String, Term)
 		)
 	;
 		% old syntax: `:- pragma(foo, ...).'
@@ -115,7 +116,9 @@
 			MaybeAssertionTerm = yes(AssertionTerm)
 		)
 	->
-		( parse_foreign_language(LangTerm, Language) ->
+		(
+			parse_foreign_language(LangTerm, Language)
+		->
 			parse_foreign_language_type(ForeignTypeTerm, Language,
 				MaybeForeignType),
 			(
@@ -133,12 +136,18 @@
 					( parse_maybe_foreign_type_assertions(
 						MaybeAssertionTerm, Assertions)
 					->
+							% rafe: XXX I'm not
+							% sure that
+							% no_special_type_dtls
+							% here is right - we
+							% might need some more
+							% parsing...
 						Result = ok(type_defn(TVarSet,
 							MercuryTypeSymName,
 							MercuryArgs,
 							foreign_type(
 								ForeignType,
-								no,
+								no_special_type_details,
 								Assertions),
 							true))
 					; MaybeAssertionTerm =
@@ -473,8 +482,7 @@
 			)
 		;
 			ErrMsg = "-- invalid language parameter",
-			Result = error(string__append(InvalidDeclStr, ErrMsg),
-				LangTerm)
+			Result = error(InvalidDeclStr ++ ErrMsg, LangTerm)
 		)
 	;
 		string__format("invalid `:- pragma %s' declaration ",
Index: prog_mode.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_mode.m,v
retrieving revision 1.1
diff -u -r1.1 prog_mode.m
--- prog_mode.m	14 Jun 2004 04:16:31 -0000	1.1
+++ prog_mode.m	1 Jul 2004 02:17:59 -0000
@@ -21,15 +21,20 @@
 	% `in', `out', `uo' or `unused' mode.
 :- pred in_mode((mode)::out) is det.
 :- func in_mode = (mode).
+:- func in_mode(inst) = (mode).
 :- pred out_mode((mode)::out) is det.
 :- func out_mode = (mode).
+:- func out_mode(inst) = (mode).
 :- pred uo_mode((mode)::out) is det.
 :- func uo_mode = (mode).
 :- pred unused_mode((mode)::out) is det.
 :- func unused_mode = (mode).
+:- func in_any_mode = (mode).
+:- func out_any_mode = (mode).
 
 :- func ground_inst = (inst).
 :- func free_inst = (inst).
+:- func any_inst = (inst).
 
 	% Construct the modes used for `aditi__state' arguments.
 	% XXX These should be unique, but are not yet because that
@@ -127,9 +132,13 @@
 unused_mode(unused_mode).
 
 in_mode = make_std_mode("in", []).
+in_mode(I) = make_std_mode("in", [I]).
 out_mode = make_std_mode("out", []).
+out_mode(I) = make_std_mode("out", [I]).
 uo_mode = make_std_mode("uo", []).
 unused_mode = make_std_mode("unused", []).
+in_any_mode = make_std_mode("in", [any_inst]).
+out_any_mode = make_std_mode("out", [any_inst]).
 
 aditi_mui_mode = Mode :- in_mode(Mode).
 aditi_ui_mode = Mode :- in_mode(Mode).
@@ -138,6 +147,7 @@
 
 ground_inst = ground(shared, none).
 free_inst = free.
+any_inst = any(shared).
 
 make_std_mode(Name, Args, make_std_mode(Name, Args)).
 
Index: prog_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_util.m,v
retrieving revision 1.67
diff -u -r1.67 prog_util.m
--- prog_util.m	14 Jun 2004 04:16:31 -0000	1.67
+++ prog_util.m	28 Jun 2004 05:27:11 -0000
@@ -711,3 +711,6 @@
 	;
 		error("hlds_pred__get_state_args_det")
 	).
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
Index: purity.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/purity.m,v
retrieving revision 1.66
diff -u -r1.66 purity.m
--- purity.m	14 Jun 2004 04:16:31 -0000	1.66
+++ purity.m	30 Jun 2004 06:13:21 -0000
@@ -937,14 +937,14 @@
 	write_context_and_pred_id(ModuleInfo, PredInfo, PredId),
 	prog_out__write_context(Context),
 	report_warning("  warning: declared `"),
-	write_purity(Purity),
+	prog_out__write_purity(Purity),
 	io__write_string("' but promised pure.\n"),
 	globals__io_lookup_bool_option(verbose_errors, VerboseErrors),
 	( { VerboseErrors = yes } ->
 		{ PredOrFunc = pred_info_is_pred_or_func(PredInfo) },
 		prog_out__write_context(Context),
 		io__write_string("  A pure "),
-		write_pred_or_func(PredOrFunc),
+		prog_out__write_pred_or_func(PredOrFunc),
 		io__write_string(" that invokes impure or semipure code should\n"),
 		prog_out__write_context(Context),
 		io__write_string(
@@ -997,7 +997,7 @@
 		prog_out__write_context(Context),
 		{ PredOrFunc = pred_info_is_pred_or_func(PredInfo) },
 		io__write_string("  This "),
-		write_pred_or_func(PredOrFunc),
+		prog_out__write_pred_or_func(PredOrFunc),
 		io__write_string(" does not invoke any "),
 		io__write_string(CodeStr),
 		io__write_string(" code,\n"),
@@ -1018,9 +1018,9 @@
 	write_context_and_pred_id(ModuleInfo, PredInfo, PredId),
 	prog_out__write_context(Context),
 	io__write_string("  purity error: "),
-	write_pred_or_func(PredOrFunc),
+	prog_out__write_pred_or_func(PredOrFunc),
 	io__write_string(" is "),
-	write_purity(Purity),
+	prog_out__write_purity(Purity),
 	io__write_string(".\n"),
 	prog_out__write_context(Context),
 	{ pred_info_get_purity(PredInfo, DeclaredPurity) },
@@ -1028,9 +1028,9 @@
 		io__write_string("  It must be pure.\n")
 	;
 		io__write_string("  It must be declared `"),
-		write_purity(Purity),
+		prog_out__write_purity(Purity),
 		io__write_string("' or promised "),
-		write_purity(DeclaredPurity),
+		prog_out__write_purity(DeclaredPurity),
 		io__write_string(".\n")
 	).
 
Index: recompilation.check.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation.check.m,v
retrieving revision 1.8
diff -u -r1.8 recompilation.check.m
--- recompilation.check.m	14 Jun 2004 04:16:32 -0000	1.8
+++ recompilation.check.m	1 Jul 2004 01:38:48 -0000
@@ -1133,10 +1133,11 @@
 check_type_defn_ambiguity_with_functor(_, _, abstract_type(_)) --> [].
 check_type_defn_ambiguity_with_functor(_, _, eqv_type(_)) --> [].
 check_type_defn_ambiguity_with_functor(NeedQualifier,
-			TypeCtor, du_type(Ctors, _, _)) -->
+			TypeCtor, du_type(Ctors, _)) -->
 	list__foldl(check_functor_ambiguities(NeedQualifier, TypeCtor),
 		Ctors).
 check_type_defn_ambiguity_with_functor(_, _, foreign_type(_, _, _)) --> [].
+check_type_defn_ambiguity_with_functor(_, _, solver_type(_)) --> [].
 
 :- pred check_functor_ambiguities(need_qualifier::in, type_ctor::in,
 		constructor::in, recompilation_check_info::in,
Index: recompilation.usage.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation.usage.m,v
retrieving revision 1.11
diff -u -r1.11 recompilation.usage.m
--- recompilation.usage.m	14 Jun 2004 04:16:32 -0000	1.11
+++ recompilation.usage.m	30 Jun 2004 17:56:00 -0000
@@ -1060,7 +1060,9 @@
 recompilation__usage__find_items_used_by_type_body(eqv_type(Type)) -->
 	recompilation__usage__find_items_used_by_type(Type).
 recompilation__usage__find_items_used_by_type_body(abstract_type(_)) --> [].
-recompilation__usage__find_items_used_by_type_body(foreign_type(_, _)) --> [].
+recompilation__usage__find_items_used_by_type_body(foreign_type(_)) --> [].
+	% rafe: XXX Should we trace the representation type?
+recompilation__usage__find_items_used_by_type_body(solver_type(_)) --> [].
 
 :- pred recompilation__usage__find_items_used_by_mode_defn(hlds_mode_defn::in,
 	recompilation_usage_info::in, recompilation_usage_info::out) is det.
Index: recompilation.version.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation.version.m,v
retrieving revision 1.10
diff -u -r1.10 recompilation.version.m
--- recompilation.version.m	14 Jun 2004 04:16:33 -0000	1.10
+++ recompilation.version.m	1 Jul 2004 01:40:01 -0000
@@ -272,7 +272,9 @@
 			% generated unification procedure.
 			{ BodyItem = Item }
 		;
-			{ Body = du_type(_, IsSolverType, _) },
+			{ Body = du_type(_, SpecialTypeDetails) },
+			{ IsSolverType =
+				SpecialTypeDetails ^ is_solver_type },
 			{ NameItem = type_defn(VarSet, Name, Args,
 				abstract_type(IsSolverType), Cond) },
 			{ BodyItem = Item }
@@ -280,6 +282,10 @@
 			{ Body = eqv_type(_) },
 			% When we use an equivalence type we
 			% always use the body.
+			{ NameItem = Item },
+			{ BodyItem = Item }
+		;
+			{ Body = solver_type(_) },
 			{ NameItem = Item },
 			{ BodyItem = Item }
 		;
Index: rl_key.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/rl_key.m,v
retrieving revision 1.18
diff -u -r1.18 rl_key.m
--- rl_key.m	14 Jun 2004 04:16:34 -0000	1.18
+++ rl_key.m	30 Jun 2004 04:09:10 -0000
@@ -1041,7 +1041,8 @@
 		map__search(Types, TypeCtor, TypeDefn),
 		hlds_data__get_type_defn_body(TypeDefn, Body),
 		% If there's a user defined equality pred we're in trouble.
-		Body ^ du_type_usereq = no,
+		not has_user_defined_equality(Body ^
+				du_type_special_type_details),
 		rl_key__choose_cons_id_2(Body ^ du_type_ctors,
 			UpperLower, ConsId1, ConsId2, ConsId)
 	;
Index: special_pred.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/special_pred.m,v
retrieving revision 1.45
diff -u -r1.45 special_pred.m
--- special_pred.m	14 Jun 2004 04:16:36 -0000	1.45
+++ special_pred.m	7 Jul 2004 07:57:43 -0000
@@ -30,7 +30,8 @@
 :- type special_pred_id
 	--->	unify
 	;	index
-	;	compare.
+	;	compare
+	;	initialise.
 
 	% Return the predicate name we should use for the given special_pred
 	% for the given type constructor.
@@ -90,7 +91,8 @@
 	% A compiler-generated predicate only needs type checking if
 	%	(a) it is a user-defined equality pred
 	% or	(b) it is the unification or comparison predicate for an
-	%           existially quantified type.
+	%           existially quantified type
+	% or    (c) it is the initialisation predicate for a solver type.
 	%
 :- pred special_pred_for_type_needs_typecheck(module_info::in,
 	hlds_type_body::in) is semidet.
@@ -117,22 +119,33 @@
 :- import_module libs__globals.
 :- import_module libs__options.
 :- import_module parse_tree__prog_mode.
+:- import_module parse_tree__prog_out.
 :- import_module parse_tree__prog_util.
 
-:- import_module bool, require.
+:- import_module bool, require, string.
 
 special_pred_list([unify, index, compare]).
 
 special_pred_name_arity(unify, "unify", 2).
 special_pred_name_arity(index, "index", 2).
 special_pred_name_arity(compare, "compare", 3).
+special_pred_name_arity(initialise, "initialise", 1).
 
 	% mode num for special procs is always 0 (the first mode)
 special_pred_mode_num(_, 0).
 
-special_pred_name(unify, _TypeCtor) = "__Unify__".
-special_pred_name(index, _TypeCtor) = "__Index__".
-special_pred_name(compare, _TypeCtor) = "__Compare__".
+special_pred_name(unify,      SymName - Arity) =
+	string__format("__Unify__%s/%d",
+		[s(sym_name_to_string(SymName)), i(Arity)]).
+special_pred_name(index,      SymName - Arity) =
+	string__format("__Index__%s/%d",
+		[s(sym_name_to_string(SymName)), i(Arity)]).
+special_pred_name(compare,    SymName - Arity) =
+	string__format("__Compare__%s/%d",
+		[s(sym_name_to_string(SymName)), i(Arity)]).
+special_pred_name(initialise, SymName - Arity) =
+	string__format("__Initialise__%s/%d",
+		[s(sym_name_to_string(SymName)), i(Arity)]).
 
 special_pred_interface(unify, Type, [Type, Type], [In, In], semidet) :-
 	in_mode(In).
@@ -143,6 +156,8 @@
 		[Uo, In, In], det) :-
 	in_mode(In),
 	uo_mode(Uo).
+special_pred_interface(initialise, Type, [Type], [InAny], det) :-
+	InAny = out_any_mode.
 
 special_pred_get_type(unify, Types, T) :-
 	list__reverse(Types, [T | _]).
@@ -150,6 +165,8 @@
 	list__reverse(Types, [_, T | _]).
 special_pred_get_type(compare, Types, T) :-
 	list__reverse(Types, [T | _]).
+special_pred_get_type(initialise, Types, T) :-
+	list__reverse(Types, [T | _]).
 
 special_pred_get_type_det(SpecialId, ArgTypes, Type) :-
 	( special_pred_get_type(SpecialId, ArgTypes, TypePrime) ->
@@ -161,6 +178,7 @@
 special_pred_description(unify, "unification predicate").
 special_pred_description(compare, "comparison predicate").
 special_pred_description(index, "indexing predicate").
+special_pred_description(initialise, "initialisation predicate").
 
 special_pred_is_generated_lazily(ModuleInfo, TypeCtor) :-
 	TypeCategory = classify_type_ctor(ModuleInfo, TypeCtor),
@@ -180,6 +198,15 @@
 	).
 
 special_pred_is_generated_lazily(ModuleInfo, TypeCtor, Body, Status) :-
+	% rafe: XXX Is there a cleaner way of doing this?  I don't
+	% want special preds for solver types to be generated lazily
+	% because I have to insert calls to their initialisation preds
+	% during mode analysis and I therefore require the appropriate
+	% names to appear in the symbol table.
+	%
+	Body \= solver_type(_),
+	Body \= abstract_type(solver_type),
+
 	TypeCategory = classify_type_ctor(ModuleInfo, TypeCtor),
 	(
 		TypeCategory = tuple_type
@@ -210,7 +237,7 @@
 	% polymorphism__process_generated_pred can't handle calls to
 	% polymorphic procedures after the initial polymorphism pass.
 	%
-	Body \= foreign_type(_, _),
+	Body \= foreign_type(_),
 
 	% The special predicates for types with user-defined
 	% equality or existentially typed constructors are always
@@ -220,7 +247,7 @@
 special_pred_for_type_needs_typecheck(ModuleInfo, Body) :-
 	(
 		type_body_has_user_defined_equality_pred(ModuleInfo, Body,
-			unify_compare(_, _))
+			_SpecialTypeDetails)
 	;
 		Ctors = Body ^ du_type_ctors,
 		list__member(Ctor, Ctors),
@@ -239,7 +266,7 @@
 	),
 	\+ type_ctor_has_hand_defined_rtti(TypeCtor, Body),
 	\+ type_body_has_user_defined_equality_pred(ModuleInfo, Body,
-		abstract_noncanonical_type).
+		abstract_noncanonical_type(_IsSolverType)).
 
 is_builtin_types_special_preds_defined_in_mercury(TypeCtor, TypeName) :-
 	Builtin = mercury_public_builtin_module,
Index: table_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/table_gen.m,v
retrieving revision 1.64
diff -u -r1.64 table_gen.m
--- table_gen.m	21 Jun 2004 03:31:55 -0000	1.64
+++ table_gen.m	1 Jul 2004 01:41:30 -0000
@@ -1470,7 +1470,8 @@
 			(
 				Ctors = TypeBody ^ du_type_ctors,
 				TypeBody ^ du_type_is_enum = yes,
-				TypeBody ^ du_type_usereq = no
+				not has_user_defined_equality(TypeBody ^
+					du_type_special_type_details)
 			->
 				list__length(Ctors, EnumRange)
 			;
Index: term_norm.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/term_norm.m,v
retrieving revision 1.4
diff -u -r1.4 term_norm.m
--- term_norm.m	14 Jun 2004 04:16:39 -0000	1.4
+++ term_norm.m	30 Jun 2004 17:56:34 -0000
@@ -140,7 +140,10 @@
 		TypeBody = abstract_type(_)
 	;
 		% This type does not introduce any functors
-		TypeBody = foreign_type(_, _)
+		TypeBody = foreign_type(_)
+	;
+		% This type does not introduce any functors
+		TypeBody = solver_type(_)
 	).
 
 :- pred find_weights_for_cons(type_ctor::in, list(type_param)::in,
Index: termination.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/termination.m,v
retrieving revision 1.43
diff -u -r1.43 termination.m
--- termination.m	14 Jun 2004 04:16:39 -0000	1.43
+++ termination.m	1 Jul 2004 02:48:24 -0000
@@ -704,6 +704,12 @@
 	term_util__make_bool_list(HeadVars, [no, no], OutList),
 	ArgSize = finite(0, OutList),
 	Termination = cannot_loop.
+		% rafe: XXX I think the [yes] here is correct.
+		%
+special_pred_id_to_termination(initialise, HeadVars, ArgSize, Termination) :-
+	term_util__make_bool_list(HeadVars, [yes], OutList),
+	ArgSize = finite(0, OutList),
+	Termination = cannot_loop.
 
 % The list of proc_ids must refer to builtin predicates.  This predicate
 % sets the termination information of builtin predicates.
Index: type_ctor_info.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_ctor_info.m,v
retrieving revision 1.58
diff -u -r1.58 type_ctor_info.m
--- type_ctor_info.m	30 Jun 2004 02:48:17 -0000	1.58
+++ type_ctor_info.m	14 Jul 2004 05:41:42 -0000
@@ -224,7 +224,8 @@
 		;
 			SpecialPreds = no,
 			hlds_data__get_type_defn_body(TypeDefn, Body),
-			Body ^ du_type_usereq = yes(_UserDefinedEquality)
+			has_user_defined_equality(Body ^
+				du_type_special_type_details)
 		)
 	->
 		map__lookup(SpecMap, unify - TypeCtor, UnifyPredId),
@@ -327,7 +328,36 @@
 			error("type_ctor_info__gen_type_ctor_data: " ++
 				"abstract_type")
 		;
-			TypeBody = foreign_type(ForeignBody, _),
+				% We treat solver_types as being
+				% equivalent to their representation
+				% types for RTTI purposes.
+				%
+				% rafe: XXX Won't this cause trouble
+				% with construct etc?
+				%
+			TypeBody = solver_type(SpecialTypeDetails),
+			(
+				SpecialTypeDetails ^ solver_type_details =
+					yes(SolverTypeDetails)
+			->
+				RepnType =
+					SolverTypeDetails ^
+						representation_type,
+				% There can be no existentially typed args to
+				% an equivalence.
+				UnivTvars = TypeArity,
+				ExistTvars = [],
+			pseudo_type_info__construct_maybe_pseudo_type_info(
+					RepnType, UnivTvars, ExistTvars,
+					MaybePseudoTypeInfo),
+				Details = eqv(MaybePseudoTypeInfo)
+			;
+				error("type_ctor_info__gen_type_ctor_data:" ++
+					" solver_type with no" ++
+					" solver_type_details")
+			)
+		;
+			TypeBody = foreign_type(ForeignBody),
 			foreign_type_body_to_exported_type(ModuleInfo, 
 				ForeignBody, _, _, Assertions),
 			(
@@ -351,12 +381,10 @@
 			Details = eqv(MaybePseudoTypeInfo)
 		;
 			TypeBody = du_type(Ctors, ConsTagMap, Enum,
-				EqualityPred, ReservedTag, _, _),
-			(
-				EqualityPred = yes(_),
+				SpecialTypeDetails, ReservedTag, _),
+			( has_user_defined_equality(SpecialTypeDetails) ->
 				EqualityAxioms = user_defined
 			;
-				EqualityPred = no,
 				EqualityAxioms = standard
 			),
 			(
@@ -385,7 +413,7 @@
 		)
 	),
 	Flags0 = set__init,
-	( TypeBody = du_type(_, _, _, _, _, _, _) ->
+	( TypeBody = du_type(_, _, _, _, _, _) ->
 		Flags1 = set__insert(Flags0, kind_of_du_flag),
 		( TypeBody ^ du_type_reserved_tag = yes ->
 			Flags2 = set__insert(Flags1, reserve_tag_flag)
Index: type_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/type_util.m,v
retrieving revision 1.139
diff -u -r1.139 type_util.m
--- type_util.m	14 Jun 2004 04:16:40 -0000	1.139
+++ type_util.m	16 Jul 2004 06:18:40 -0000
@@ -67,6 +67,16 @@
 	% hlds_type_defn.
 :- func builtin_type_ctors_with_no_hlds_type_defn = list(type_ctor).
 
+	% Obtain the type definition and type definition body respectively,
+	% if known, for the principal type constructor of the given type.
+	%
+	% Fail if the given type is a type variable.
+:- pred type_util__type_to_type_defn(module_info::in, (type)::in,
+		hlds_type_defn::out) is semidet.
+
+:- pred type_util__type_to_type_defn_body(module_info::in, (type)::in,
+		hlds_type_body::out) is semidet.
+
 	% Succeed iff there was either a `where equality is <predname>' or a
 	% `where comparison is <predname>' declaration for the principal type
 	% constructor of the specified type, and return the ids of the declared
@@ -78,17 +88,28 @@
 	% If the type is a type variable and thus has no principal type
 	% constructor, fail.
 :- pred type_has_user_defined_equality_pred(module_info::in, (type)::in,
-	unify_compare::out) is semidet.
+	special_type_details::out) is semidet.
 
 :- pred type_body_has_user_defined_equality_pred(module_info::in,
-	hlds_type_body::in, unify_compare::out) is semidet.
+	hlds_type_body::in, special_type_details::out) is semidet.
+
+	% Succeed iff the principal type constructor for the given type
+	% is a solver type.
+	%
+	% If the type is a type variable and thus has no principal type
+	% constructor, fail.
+:- pred type_util__type_is_solver_type(module_info::in, (type)::in) is semidet.
+
+:- pred type_util__type_has_solver_type_details(module_info::in, (type)::in,
+		solver_type_details::out) is semidet.
+
+:- pred type_util__type_body_has_solver_type_details(module_info::in,
+		hlds_type_body::in, solver_type_details::out) is semidet.
 
-	% Succeed if the inst `any' can be considered `bound' for this type.
 :- pred type_util__is_solver_type(module_info::in, (type)::in) is semidet.
 
 :- pred type_body_is_solver_type(module_info::in, hlds_type_body::in)
-	is semidet.
-
+		is semidet.
 
 	% Certain types, e.g. io__state and store__store(S),
 	% are just dummy types used to ensure logical semantics;
@@ -581,8 +602,10 @@
 	; Name = "typeclass_info"
 	; Name = "base_typeclass_info"
 	),
-	\+ ( Body = du_type(_, _, _, _, _, _, yes(_))
-		; Body = foreign_type(_, _) ).
+	\+ (	Body = du_type(_, _, _, _, _, yes(_))
+	   ;	Body = foreign_type(_)
+	   ;	Body = solver_type(_)
+	   ).
 
 is_introduced_type_info_type(Type) :-
 	type_to_ctor_and_args(Type, TypeCtor, _),
@@ -724,7 +747,7 @@
 			TypeArgs0)
 	->
 		TypeArgs = TypeArgs0,
-		PredOrFuncStr = pred_or_func_to_str(PredOrFunc),
+		PredOrFuncStr = prog_out__pred_or_func_to_str(PredOrFunc),
 		TypeCtor = unqualified(PredOrFuncStr) - 0
 	;
 		type_is_tuple(Type, TypeArgs1)
@@ -776,63 +799,98 @@
 
 type_ctor_is_tuple(unqualified("{}") - _).
 
-type_has_user_defined_equality_pred(ModuleInfo, Type, UserEqComp) :-
-	module_info_types(ModuleInfo, TypeTable),
-	type_to_ctor_and_args(Type, TypeCtor, _TypeArgs),
-	map__search(TypeTable, TypeCtor, TypeDefn),
-	hlds_data__get_type_defn_body(TypeDefn, TypeBody),
+type_has_user_defined_equality_pred(ModuleInfo, Type, SpecialTypeDetails) :-
+	type_to_type_defn_body(ModuleInfo, Type, TypeBody),
 	type_body_has_user_defined_equality_pred(ModuleInfo, TypeBody,
-		UserEqComp).
+		SpecialTypeDetails).
 
-type_body_has_user_defined_equality_pred(ModuleInfo, TypeBody, UserEqComp) :-
+type_body_has_user_defined_equality_pred(ModuleInfo, TypeBody,
+		SpecialTypeDetails) :-
 	module_info_globals(ModuleInfo, Globals),
 	globals__get_target(Globals, Target),
 	(
-		TypeBody = du_type(_, _, _, _, _, _, _),
+		TypeBody = du_type(_, _, _, _, _, _),
 		(
 			TypeBody ^ du_type_is_foreign_type =
 				yes(ForeignTypeBody),
 			have_foreign_type_for_backend(Target, ForeignTypeBody,
 				yes)
 		->
-			UserEqComp =
+			SpecialTypeDetails =
 				foreign_type_body_has_user_defined_eq_comp_pred(
 					ModuleInfo, ForeignTypeBody)
 		;
-			TypeBody ^ du_type_usereq = yes(UserEqComp)
+			SpecialTypeDetails =
+				TypeBody ^ du_type_special_type_details,
+			prog_data__has_user_defined_equality(
+				SpecialTypeDetails)
 		)
 	;
-		TypeBody = foreign_type(ForeignTypeBody, _),
-		UserEqComp = foreign_type_body_has_user_defined_eq_comp_pred(
-			ModuleInfo, ForeignTypeBody)
+		TypeBody = foreign_type(ForeignTypeBody),
+		SpecialTypeDetails =
+			foreign_type_body_has_user_defined_eq_comp_pred(
+				ModuleInfo, ForeignTypeBody)
+	;
+		TypeBody = solver_type(SpecialTypeDetails),
+		prog_data__has_user_defined_equality(SpecialTypeDetails)
 	).
 
-type_util__is_solver_type(ModuleInfo, Type) :-
-	module_info_types(ModuleInfo, TypeTable),
-	( type_to_ctor_and_args(Type, TypeCtor, _TypeArgs) ->
-		map__search(TypeTable, TypeCtor, TypeDefn),
-			% Type table search will fail for builtin types such as
-			% `int/0'.  Such types are not solver types so
-			% type_util__is_solver_type fails too.
-		hlds_data__get_type_defn_body(TypeDefn, TypeBody),
-		type_body_is_solver_type(ModuleInfo, TypeBody)
-	;
-		% type_to_ctor_and_args will fail for type variables.  In that
-		% case we assume that the type may be a solver type.
-		true
+
+type_util__type_is_solver_type(ModuleInfo, Type) :-
+	type_to_type_defn_body(ModuleInfo, Type, TypeBody),
+	(
+		TypeBody = solver_type(_)
+	;
+		TypeBody = abstract_type(solver_type)
 	).
 
-	% Return the `is_solver_type' field for the type body.
-type_body_is_solver_type(ModuleInfo, TypeBody) :-
+
+type_util__type_has_solver_type_details(ModuleInfo, Type, SolverTypeDetails) :-
+	type_to_type_defn_body(ModuleInfo, Type, TypeBody),
+	type_util__type_body_has_solver_type_details(ModuleInfo, TypeBody,
+		SolverTypeDetails).
+
+
+type_util__type_body_has_solver_type_details(_ModuleInfo,
+		solver_type(SpecialTypeDetails), SolverTypeDetails) :-
+	SpecialTypeDetails ^ solver_type_details = yes(SolverTypeDetails).
+type_util__type_body_has_solver_type_details( ModuleInfo,
+		eqv_type(Type), SolverTypeDetails) :-
+	type_util__type_has_solver_type_details(ModuleInfo, Type,
+		SolverTypeDetails).
+
+
+type_util__type_to_type_defn(ModuleInfo, Type, TypeDefn) :-
+	module_info_types(ModuleInfo, TypeTable),
+	type_to_ctor_and_args(Type, TypeCtor, _TypeArgs),
+	map__search(TypeTable, TypeCtor, TypeDefn).
+
+
+type_util__type_to_type_defn_body(ModuleInfo, Type, TypeBody) :-
+	type_to_type_defn(ModuleInfo, Type, TypeDefn),
+	hlds_data__get_type_defn_body(TypeDefn, TypeBody).
+
+
+	% We assume that type variables may refer to solver types.
+type_util__is_solver_type(_ModuleInfo, term__variable(_)).
+
+type_util__is_solver_type( ModuleInfo, Type) :-
+		% type_to_type_defn_body will fail for builtin types such
+		% as `int/0'.  Such types are not solver types so
+		% type_util__is_solver_type fails too.
+	type_util__type_to_type_defn_body(ModuleInfo, Type, TypeBody),
+	type_util__type_body_is_solver_type(ModuleInfo, TypeBody).
+
+
+	% Succeed if the type body is for a solver type.
+type_util__type_body_is_solver_type(ModuleInfo, TypeBody) :-
 	(
-		TypeBody ^ du_type_is_solver_type = solver_type
+		TypeBody = solver_type(_)
+	;
+		TypeBody = abstract_type(solver_type)
 	;
 		TypeBody = eqv_type(Type),
 		type_util__is_solver_type(ModuleInfo, Type)
-	;
-		TypeBody = foreign_type(_, solver_type)
-	;
-		TypeBody = abstract_type(solver_type)
 	).
 
 	% Certain types, e.g. io__state and store__store(S),
Index: typecheck.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/typecheck.m,v
retrieving revision 1.355
diff -u -r1.355 typecheck.m
--- typecheck.m	14 Jun 2004 04:16:41 -0000	1.355
+++ typecheck.m	30 Jun 2004 06:24:25 -0000
@@ -5689,7 +5689,7 @@
 	{ typecheck_info_get_context(Info, Context) },
 	prog_out__write_context(Context),
 	io__write_string("  (There is a *"),
-	write_pred_or_func(PredOrFunc),
+	prog_out__write_pred_or_func(PredOrFunc),
 	io__write_string("* with that name, however."),
 	( { PredOrFunc = function } ->
 		io__nl,
@@ -5750,7 +5750,7 @@
 	io__nl,
 	prog_out__write_context(Context),
 	io__write_string("  in call to "),
-	write_pred_or_func(PredOrFunc),
+	prog_out__write_pred_or_func(PredOrFunc),
 	io__write_string(" `"),
 	prog_out__write_sym_name(SymName),
 	io__write_string("'.\n").
Index: unify_proc.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/unify_proc.m,v
retrieving revision 1.138
diff -u -r1.138 unify_proc.m
--- unify_proc.m	30 Jun 2004 02:48:18 -0000	1.138
+++ unify_proc.m	16 Jul 2004 02:32:40 -0000
@@ -135,6 +135,7 @@
 :- import_module check_hlds__cse_detection.
 :- import_module check_hlds__det_analysis.
 :- import_module check_hlds__inst_match.
+:- import_module check_hlds__mode_util.
 :- import_module check_hlds__modes.
 :- import_module check_hlds__polymorphism.
 :- import_module check_hlds__post_typecheck.
@@ -546,13 +547,12 @@
 		ConsId = cons(CtorSymName, TupleArity),
 		map__from_assoc_list([ConsId - single_functor],
 			ConsTagValues),
-		TypeBody = du_type([Ctor], ConsTagValues, IsEnum,
-			UnifyPred, ReservedTag, IsSolverType, IsForeign),
-		UnifyPred = no,
 		IsEnum = no,
-		IsForeign = no,
+		SpecialTypeDetails = no_special_type_details,
 		ReservedTag = no,
-		IsSolverType = non_solver_type,
+		IsForeign = no,
+		TypeBody = du_type([Ctor], ConsTagValues, IsEnum,
+				SpecialTypeDetails, ReservedTag, IsForeign),
 		construct_type(TypeCtor, TupleArgTypes, Type),
 
 		term__context_init(Context)
@@ -691,6 +691,10 @@
 	; SpecialPredId = compare, Args = [Res, X, Y] ->
 		unify_proc__generate_compare_clauses(ModuleInfo, Type,
 			TypeBody, Res, X, Y, Context, Clauses, Info1, Info)
+	; SpecialPredId = initialise, Args = [X] ->
+		unify_proc__generate_initialise_clauses(ModuleInfo, Type,
+			TypeBody, X, Context, Clauses, Info1, Info)
+
 	;
 		error("unknown special pred")
 	),
@@ -702,6 +706,37 @@
 	ClauseInfo = clauses_info(VarSet, Types, TVarNameMap, Types, Args,
 		Clauses, TI_VarMap, TCI_VarMap, HasForeignClauses).
 
+
+:- pred unify_proc__generate_initialise_clauses(module_info::in, (type)::in,
+	hlds_type_body::in, prog_var::in, prog_context::in,
+	list(clause)::out, unify_proc_info::in, unify_proc_info::out) is det.
+
+unify_proc__generate_initialise_clauses(ModuleInfo, _Type, TypeBody,
+		X, Context, Clauses, !Info) :-
+	(
+		type_util__type_body_has_solver_type_details(ModuleInfo,
+			TypeBody, SolverTypeDetails)
+	->
+		% 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.)
+		%
+		InitPred = SolverTypeDetails ^ init_pred,
+		PredId = invalid_pred_id,
+		ModeId = invalid_proc_id,
+		Call = call(PredId, ModeId, [X], not_builtin, no, InitPred),
+		goal_info_init(Context, GoalInfo),
+		Goal = Call - GoalInfo,
+		unify_proc__quantify_clauses_body([X], Goal, Context, Clauses,
+			!Info)
+	;
+		error("trying to create initialisation proc for type " ++
+			"that has no solver_type_details")
+	).
+
+
 :- pred unify_proc__generate_unify_clauses(module_info::in, (type)::in,
 	hlds_type_body::in, prog_var::in, prog_var::in, prog_context::in,
 	list(clause)::out, unify_proc_info::in, unify_proc_info::out) is det.
@@ -710,9 +745,10 @@
 		H1, H2, Context, Clauses, !Info) :-
 	(
 		type_body_has_user_defined_equality_pred(ModuleInfo,
-			TypeBody, UserEqCompare)
+			TypeBody, SpecialTypeDetails)
 	->
-		unify_proc__generate_user_defined_unify_clauses(UserEqCompare,
+		unify_proc__generate_user_defined_unify_clauses(
+			SpecialTypeDetails,
 			H1, H2, Context, Clauses, !Info)
 	;
 		(
@@ -740,7 +776,14 @@
 			generate_unify_clauses_eqv_type(EqvType, H1, H2,
 				Context, Clauses, !Info)
 		;
-			TypeBody = foreign_type(_, _),
+			TypeBody = solver_type(_),
+			% If no user defined equality predicate is given,
+			% we treat solver types as if they were an equivalent
+			% to the builtin type c_pointer.
+			generate_unify_clauses_eqv_type(c_pointer_type,
+				H1, H2, Context, Clauses, !Info)
+		;
+			TypeBody = foreign_type(_),
 			% If no user defined equality predicate is given,
 			% we treat foreign_type as if they were an equivalent
 			% to the builtin type c_pointer.
@@ -820,16 +863,18 @@
 	unify_proc__build_call(Name, ArgVars, Context, UnifyGoal, !Info),
 	quantify_clauses_body(ArgVars, UnifyGoal, Context, Clauses, !Info).
 
-:- pred unify_proc__generate_user_defined_unify_clauses(unify_compare::in,
+:- pred unify_proc__generate_user_defined_unify_clauses(
+	special_type_details::in,
 	prog_var::in, prog_var::in, prog_context::in, list(clause)::out,
 	unify_proc_info::in, unify_proc_info::out) is det.
 
-unify_proc__generate_user_defined_unify_clauses(abstract_noncanonical_type,
+unify_proc__generate_user_defined_unify_clauses(
+		abstract_noncanonical_type(_IsSolverType),
 		_, _, _, _, !Info) :-
 	error("trying to create unify proc for abstract noncanonical type").
-unify_proc__generate_user_defined_unify_clauses(UserEqCompare, H1, H2,
-		Context, Clauses, !Info) :-
-	UserEqCompare = unify_compare(MaybeUnify, MaybeCompare),
+unify_proc__generate_user_defined_unify_clauses(
+		special_type_details(_MaybeSolver, MaybeUnify, MaybeCompare),
+		H1, H2, Context, Clauses, !Info) :-
 	( MaybeUnify = yes(UnifyPredName) ->
 		%
 		% Just generate a call to the specified predicate,
@@ -952,9 +997,12 @@
 			% we are generating should never be invoked.
 			error("trying to create index proc for eqv type")
 		;
-			TypeBody = foreign_type(_, _),
+			TypeBody = foreign_type(_),
 			error("trying to create index proc for a foreign type")
 		;
+			TypeBody = solver_type(_),
+			error("trying to create index proc for a solver type")
+		;
 			TypeBody = abstract_type(_),
 			error("trying to create index proc for abstract type")
 		)
@@ -969,9 +1017,9 @@
 		H1, H2, Context, Clauses, !Info) :-
 	(
 		type_body_has_user_defined_equality_pred(ModuleInfo,
-			TypeBody, UserEqComp)
+			TypeBody, SpecialTypeDetails)
 	->
-		generate_user_defined_compare_clauses(UserEqComp,
+		generate_user_defined_compare_clauses(SpecialTypeDetails,
 			Res, H1, H2, Context, Clauses, !Info)
 	;
 		(
@@ -1013,7 +1061,11 @@
 			generate_compare_clauses_eqv_type(EqvType,
 				Res, H1, H2, Context, Clauses, !Info)
 		;
-			TypeBody = foreign_type(_, _),
+			TypeBody = foreign_type(_),
+			generate_compare_clauses_eqv_type(c_pointer_type,
+				Res, H1, H2, Context, Clauses, !Info)
+		;
+			TypeBody = solver_type(_),
 			generate_compare_clauses_eqv_type(c_pointer_type,
 				Res, H1, H2, Context, Clauses, !Info)
 		;
@@ -1091,15 +1143,17 @@
 	unify_proc__build_call(Name, ArgVars, Context, CompareGoal, !Info),
 	quantify_clauses_body(ArgVars, CompareGoal, Context, Clauses, !Info).
 
-:- pred generate_user_defined_compare_clauses(unify_compare::in,
+:- pred generate_user_defined_compare_clauses(special_type_details::in,
 	prog_var::in, prog_var::in, prog_var::in,
 	prog_context::in, list(clause)::out,
 	unify_proc_info::in, unify_proc_info::out) is det.
 
-generate_user_defined_compare_clauses(abstract_noncanonical_type,
+generate_user_defined_compare_clauses(
+		abstract_noncanonical_type(_IsSolverType),
 		_, _, _, _, _, !Info) :-
 	error("trying to create compare proc for abstract noncanonical type").
-generate_user_defined_compare_clauses(unify_compare(_, MaybeCompare),
+generate_user_defined_compare_clauses(
+		special_type_details(_MaybeSolver, _MaybeUnify, MaybeCompare),
 		Res, H1, H2, Context, Clauses, !Info) :-
 	ArgVars = [Res, H1, H2],
 	(
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------



More information about the reviews mailing list