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

Ralph Becket rafe at cs.mu.OZ.AU
Wed Aug 18 11:43:39 AEST 2004


Zoltan Somogyi, Monday, 16 August 2004:
> 
> Since the rest of the diff is full of stuff dependent on this design
> decision, I will finish the review once you and I agree on the types
> here; there is not much point until then.

I agree with you.  The special_type_details idea made sense when the
solver types design allowed any type to be a solver type (i.e. all of
them up to the last one), but now does not.  I have stripped out the
special_type_details type and reverted to maybe(unify_compare); the
solver_type_details now only reside in the solver_type data constructor.

Here's the new diff.

-- Ralph

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	17 Aug 2004 23:47:45 -0000
@@ -399,9 +399,22 @@
 		_, 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, EqPred),
+		du_type(TBody, EqPred), no, !VarSet, !Info) :-
 	equiv_type__replace_in_ctors(EqvMap, TBody0, TBody, !VarSet, !Info).
+
+equiv_type__replace_in_type_defn(EqvMap, TypeCtor,
+		solver_type(SolverTypeDetails0, MaybeUserEqComp),
+		solver_type(SolverTypeDetails,  MaybeUserEqComp),
+		ContainsCirc, !VarSet, !Info) :-
+	RepresentationType0 =
+		SolverTypeDetails0 ^ representation_type,
+	equiv_type__replace_in_type_2(EqvMap, [TypeCtor], 
+		RepresentationType0, RepresentationType,
+		_, ContainsCirc, !VarSet, !Info),
+	SolverTypeDetails =
+		SolverTypeDetails0 ^ representation_type :=
+			RepresentationType.
 
 %-----------------------------------------------------------------------------%
 
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	17 Aug 2004 03:50:10 -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,19 @@
 			TVarSet0, TVarSet, EquivTypeInfo0, EquivTypeInfo),
 		Body = eqv_type(Type)
 	;
-		Body0 = foreign_type(_, _),
+		Body0 = foreign_type(_),
 		EquivTypeInfo = EquivTypeInfo0,
 		Body = Body0,
 		TVarSet = TVarSet0
 	;
+		Body0 = solver_type(SolverTypeDetails0, UserEq),
+		RepnType0 = SolverTypeDetails0 ^ representation_type,
+		equiv_type__replace_in_type(EqvMap, RepnType0, RepnType, _,
+			TVarSet0, TVarSet, EquivTypeInfo0, EquivTypeInfo),
+		SolverTypeDetails =
+			SolverTypeDetails0 ^ representation_type := RepnType,
+		Body = solver_type(SolverTypeDetails, UserEq)
+	;
 		Body0 = abstract_type(_),
 		EquivTypeInfo = EquivTypeInfo0,
 		Body = Body0,
@@ -919,4 +927,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	17 Aug 2004 04:19:18 -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
@@ -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),
@@ -714,7 +714,8 @@
 			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,
@@ -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	17 Aug 2004 04:20:51 -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(
@@ -150,16 +150,13 @@
 					% 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)
+	;	foreign_type(foreign_type_body)
+	;	solver_type(solver_type_details, maybe(unify_compare))
 	;	abstract_type(is_solver_type).
 
 :- type foreign_type_body
@@ -171,6 +168,9 @@
 
 :- 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,
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.337
diff -u -r1.337 hlds_out.m
--- hlds_out.m	20 Jul 2004 04:40:59 -0000	1.337
+++ hlds_out.m	18 Aug 2004 01:05:43 -0000
@@ -436,10 +436,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 ++ "'"
 	).
 
@@ -471,7 +471,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).
@@ -554,7 +554,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"
 		;
@@ -2232,7 +2233,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),
@@ -3068,9 +3069,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)
@@ -3090,32 +3090,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,
+			MaybeUserEqComp, ReservedTag, Foreign),
 		!IO) :-
 	io__write_string(" --->\n", !IO),
 	(
@@ -3132,33 +3132,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_where_attributes(TVarSet, no, MaybeUserEqComp, !IO),
 	(
 		Foreign = yes(_),
 		hlds_out__write_indent(Indent, !IO),
@@ -3168,57 +3143,64 @@
 	),
 	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(SolverTypeDetails, MaybeUserEqComp), !IO) :-
+	mercury_output_where_attributes(TVarSet, yes(SolverTypeDetails),
+		MaybeUserEqComp, !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	18 Aug 2004 01:01:07 -0000
@@ -993,8 +993,7 @@
 		hlds_data__get_type_defn_body(TypeDefn0, TypeBody0),
 		(
 			TypeBody0 = du_type(Ctors, Tags, Enum,
-				MaybeUserEqComp0, ReservedTag, IsSolverType,
-				MaybeForeign0)
+				MaybeUserEqComp0, ReservedTag, MaybeForeign0)
 		->
 			module_info_globals(ModuleInfo, Globals),
 			globals__get_target(Globals, Target),
@@ -1024,17 +1023,17 @@
 				MaybeUserEqComp = MaybeUserEqComp0
 			;
 				intermod__resolve_unify_compare_overloading(
-					ModuleInfo, TypeCtor, MaybeUserEqComp0,
-					MaybeUserEqComp, !Info),
+					ModuleInfo, TypeCtor,
+					MaybeUserEqComp0, MaybeUserEqComp,
+					!Info),
 				MaybeForeign = MaybeForeign0
 			),
-			TypeBody = du_type(Ctors, Tags, Enum, MaybeUserEqComp,
-				ReservedTag, IsSolverType, MaybeForeign),
+			TypeBody = du_type(Ctors, Tags, Enum,
+				MaybeUserEqComp, 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 +1041,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,11 +1099,13 @@
 
 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, MaybeUserEqComp0,
+			Assertions)),
+		yes(foreign_type_lang_data(Body, MaybeUserEqComp,
+			Assertions)),
 		!Info) :-
 	intermod__resolve_unify_compare_overloading(ModuleInfo, TypeCtor,
-		MaybeEqComp0, MaybeEqComp, !Info).
+		MaybeUserEqComp0, MaybeUserEqComp, !Info).
 
 :- pred intermod__resolve_unify_compare_overloading(module_info::in,
 	type_ctor::in, maybe(unify_compare)::in, maybe(unify_compare)::out,
@@ -1112,8 +1113,8 @@
 
 intermod__resolve_unify_compare_overloading(_, _, no, no, !Info).
 intermod__resolve_unify_compare_overloading(_, _,
-		yes(abstract_noncanonical_type),
-		yes(abstract_noncanonical_type),
+		yes(abstract_noncanonical_type(IsSolverType)),
+		yes(abstract_noncanonical_type(IsSolverType)),
 		!Info).
 intermod__resolve_unify_compare_overloading(ModuleInfo, TypeCtor,
 		yes(unify_compare(MaybeUserEq0, MaybeUserCompare0)),
@@ -1273,9 +1274,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)
+		MaybeUserEqComp = Body ^ du_type_usereq,
+		TypeBody = du_type(Ctors, MaybeUserEqComp)
 	;
 		Body = eqv_type(EqvType),
 		TypeBody = eqv_type(EqvType)
@@ -1283,15 +1283,17 @@
 		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, MaybeUserEqComp),
+		TypeBody = solver_type(SolverTypeDetails, MaybeUserEqComp)
 	),
 	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 +1302,12 @@
 		(
 			MaybeIL = yes(DataIL),
 			DataIL = foreign_type_lang_data(ILForeignType,
-				ILUserEqComp, AssertionsIL),
+				ILMaybeUserEqComp, AssertionsIL),
 			mercury_output_item(
 				type_defn(VarSet, Name, Args,
 					foreign_type(il(ILForeignType),
-						ILUserEqComp, AssertionsIL),
+						ILMaybeUserEqComp,
+						AssertionsIL),
 				true),
 				Context, !IO)
 		;
@@ -1313,11 +1316,12 @@
 		(
 			MaybeC = yes(DataC),
 			DataC = foreign_type_lang_data(CForeignType,
-				CUserEqComp, AssertionsC),
+				CMaybeUserEqComp, AssertionsC),
 			mercury_output_item(
 				type_defn(VarSet, Name, Args,
 					foreign_type(c(CForeignType),
-						CUserEqComp, AssertionsC),
+						CMaybeUserEqComp,
+						AssertionsC),
 					true),
 				Context, !IO)
 		;
@@ -1326,11 +1330,12 @@
 		(
 			MaybeJava = yes(DataJava),
 			DataJava = foreign_type_lang_data(JavaForeignType,
-				JavaUserEqComp, AssertionsJava),
+				JavaMaybeUserEqComp, AssertionsJava),
 			mercury_output_item(
 				type_defn(VarSet, Name, Args,
 					foreign_type(java(JavaForeignType),
-						JavaUserEqComp, AssertionsJava),
+						JavaMaybeUserEqComp,
+						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	12 Aug 2004 06:54:32 -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.476
diff -u -r1.476 make_hlds.m
--- make_hlds.m	20 Jul 2004 16:06:37 -0000	1.476
+++ make_hlds.m	18 Aug 2004 01:05:45 -0000
@@ -323,7 +323,28 @@
 	% 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(SolverTypeDetails, _MaybeUserEqComp)
+	->
+		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 +453,203 @@
 
 %-----------------------------------------------------------------------------%
 
+	% 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,24 @@
 		!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(SolverTypeDetails, _MaybeUserEqComp)
+	->
+		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 +1102,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 +1383,7 @@
 
 		;
 			TypeBody0 = du_type(Body, _CtorTags0, _IsEnum0,
-				EqualityPred, ReservedTag0, IsSolverType,
-				IsForeign)
+				MaybeUserEqComp, ReservedTag0, IsForeign)
 		->
 			(
 				ReservedTag0 = yes,
@@ -1038,8 +1414,7 @@
 			assign_constructor_tags(Body, TypeCtor, ReservedTag,
 				Globals, CtorTags, IsEnum),
 			TypeBody = du_type(Body, CtorTags, IsEnum,
-				EqualityPred, ReservedTag, IsSolverType,
-				IsForeign),
+				MaybeUserEqComp, ReservedTag, IsForeign),
 			hlds_data__set_type_defn_body(TypeBody,
 				TypeDefn0, TypeDefn),
 			map__set(Types0, TypeCtor, TypeDefn, Types),
@@ -2099,7 +2474,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 +2523,7 @@
 		NeedQual, Context, T),
 	(
 		MaybeOldDefn = no,
-		Body = foreign_type(_, _)
+		Body = foreign_type(_)
 	->
 		TypeStr = error_util__describe_sym_name_and_arity(
 				Name / Arity),
@@ -2161,7 +2536,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 +2570,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 +2670,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 +2691,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 +2759,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 +2868,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 +2882,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 +2997,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, MaybeUserEqComp), TypeCtor, Globals,
+		du_type(Body, CtorTags, IsEnum, MaybeUserEqComp,
+			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 +3011,26 @@
 		CtorTags, IsEnum),
 	IsForeign = no.
 convert_type_defn(eqv_type(Body), _, _, eqv_type(Body)).
+convert_type_defn(solver_type(SolverTypeDetails, MaybeUserEqComp), _, _,
+		solver_type(SolverTypeDetails, MaybeUserEqComp)).
 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, MaybeUserEqComp, Assertions),
+		_, _, foreign_type(Body)) :-
 	(
 		ForeignType = il(ILForeignType),
-		Data = foreign_type_lang_data(ILForeignType, UserEqComp,
-			Assertions),
+		Data = foreign_type_lang_data(ILForeignType,
+				MaybeUserEqComp, 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,
+				MaybeUserEqComp, 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,
+				MaybeUserEqComp, Assertions),
 		Body = foreign_type_body(no, no, yes(Data))
 	).
 
@@ -3629,9 +3995,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)
 	).
@@ -3687,6 +4067,19 @@
 					TVarSet, Type, TypeCtor, TypeBody,
 					Context, Status0, !Module)
 			;
+				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
 			)
 		)
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	18 Aug 2004 00:28:21 -0000
@@ -297,6 +297,10 @@
 :- pred write_maybe_termination_info(maybe(generic_termination_info(T))::in,
 	bool::in, io::di, io::uo) is det.
 
+:- pred mercury_output_where_attributes(tvarset::in,
+		maybe(solver_type_details)::in, maybe(unify_compare)::in,
+		io::di, io::uo) is det.
+
 %-----------------------------------------------------------------------------%
 
 % This is the typeclass mentioned in the long comment at the top of the module.
@@ -1565,38 +1569,42 @@
 	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, MaybeUserEqComp), 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_where_attributes(TVarSet, no, MaybeUserEqComp),
+	io__write_string(".\n").
+
+mercury_output_type_defn(TVarSet, Name, Args,
+		solver_type(SolverTypeDetails, MaybeUserEqComp), Context) -->
+	mercury_output_begin_type_decl(solver_type),
+	{ construct_qualified_term(Name, Args, Context, TypeTerm) },
+	mercury_output_term(TypeTerm, TVarSet, no),
+	mercury_output_where_attributes(TVarSet, yes(SolverTypeDetails),
+		MaybeUserEqComp),
+	io__write_string(".\n").
 
 mercury_output_type_defn(TVarSet, Name, Args,
-		foreign_type(ForeignType, MaybeEqCompare, Assertions),
+		foreign_type(ForeignType, MaybeUserEqComp, Assertions),
 		_Context) -->
 	io__write_string(":- pragma foreign_type("),
 	( { ForeignType = il(_) }, io__write_string("il, ")
@@ -1628,12 +1636,7 @@
 		io__write_string("]")
 	),
 	io__write_string(")"),
-	( { MaybeEqCompare = yes(_) } ->
-		io__write_string(" ")
-	;
-		[]
-	),
-	mercury_output_equality_compare_preds(MaybeEqCompare),
+	mercury_output_where_attributes(TVarSet, no, MaybeUserEqComp),
 	io__write_string(".\n").
 
 :- pred mercury_output_foreign_type_assertion(foreign_type_assertion::in,
@@ -1652,32 +1655,89 @@
 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_where_attributes(TVarSet,
+		MaybeSolverTypeDetails, MaybeUserEqComp) -->
+	(
+		{ MaybeSolverTypeDetails = no },
+		{ MaybeUserEqComp        = no }
+	->
+		[]
+	;
+		{ if
+			MaybeUserEqComp = yes(unify_compare(MaybeUnifyPred0,
+							    MaybeComparePred0))
+		  then
+			MaybeUnifyPred   = MaybeUnifyPred0,
+			MaybeComparePred = MaybeComparePred0
+		  else
+			MaybeUnifyPred   = no,
+			MaybeComparePred = no
+		},
+		io__write_string("\n\twhere\t"),
+		(
+			{ MaybeUserEqComp =
+				yes(abstract_noncanonical_type(_)) }
+		->
+			io__write_string("type_is_abstract_noncanonical")
+		;
+			{ 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").
+
+
+:- 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.144
diff -u -r1.144 ml_code_gen.m
--- ml_code_gen.m	2 Aug 2004 08:30:06 -0000	1.144
+++ ml_code_gen.m	18 Aug 2004 01:05:46 -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.37
diff -u -r1.37 ml_type_gen.m
--- ml_type_gen.m	2 Aug 2004 08:30:07 -0000	1.37
+++ ml_type_gen.m	18 Aug 2004 01:05:46 -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, MaybeUserEqComp,
+		_ReservedTag, _), ModuleInfo, TypeCtor, TypeDefn, !Defns) :-
 	% XXX we probably shouldn't ignore _ReservedTag
-	ml_gen_equality_members(MaybeUserEqCompare, MaybeEqualityMembers),
+	ml_gen_equality_members(MaybeUserEqComp, 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).
 
 %-----------------------------------------------------------------------------%
 %
Index: ml_unify_gen.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/ml_unify_gen.m,v
retrieving revision 1.77
diff -u -r1.77 ml_unify_gen.m
--- ml_unify_gen.m	2 Aug 2004 08:30:07 -0000	1.77
+++ ml_unify_gen.m	18 Aug 2004 01:05:47 -0000
@@ -1876,7 +1876,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.114
diff -u -r1.114 mlds.m
--- mlds.m	2 Aug 2004 08:30:07 -0000	1.114
+++ mlds.m	18 Aug 2004 01:05:47 -0000
@@ -1780,7 +1780,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	17 Aug 2004 05:08:08 -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, MaybeUserEqComp0),
+		du_type(Ctors, MaybeUserEqComp),
 		Info0, Info) -->
 	qualify_constructors(Ctors0, Ctors, Info0, Info),
 
@@ -738,11 +738,25 @@
 	% 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 }.
+	{ MaybeUserEqComp = MaybeUserEqComp0 }.
 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(SolverTypeDetails0, MaybeUserEqComp),
+		solver_type(SolverTypeDetails, MaybeUserEqComp),
+		Info0, Info) -->
+	{ 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    ) }.
 
 :- 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.304
diff -u -r1.304 modules.m
--- modules.m	20 Jul 2004 04:41:03 -0000	1.304
+++ modules.m	18 Aug 2004 01:05:49 -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)]
 				;
@@ -6953,7 +6952,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
@@ -6962,7 +6962,16 @@
 	;
 		TypeDefn = abstract_type(IsSolverType)
 	;
+		TypeDefn = solver_type(_, _),
+		% rafe: 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
@@ -6971,8 +6980,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
@@ -6991,14 +6999,20 @@
 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, yes(_UserEqComp)),
+		TypeDefn  = du_type(Constructors, yes(
+				abstract_noncanonical_type(non_solver_type)))
+	;
+		TypeDefn0 = foreign_type(ForeignType, yes(_UserEqComp),
+				Assertions),
+		TypeDefn  = foreign_type(ForeignType,
+				yes(abstract_noncanonical_type(
+					non_solver_type)),
+				Assertions)
+	;
+		TypeDefn0 = solver_type(SolverTypeDetails, yes(_UserEqComp)),
+		TypeDefn  = solver_type(SolverTypeDetails,
+				yes(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.113
diff -u -r1.113 prog_data.m
--- prog_data.m	20 Jul 2004 04:41:05 -0000	1.113
+++ prog_data.m	18 Aug 2004 01:05:50 -0000
@@ -1144,7 +1144,6 @@
 :- type type_defn
 	--->	du_type(
 			list(constructor),
-			is_solver_type,
 			maybe(unify_compare)
 		)
 	;	eqv_type(
@@ -1153,6 +1152,10 @@
 	;	abstract_type(
 			is_solver_type
 		)
+	;	solver_type(
+			solver_type_details,
+			maybe(unify_compare)
+		)
 	;	foreign_type(
 			foreign_language_type,
 			maybe(unify_compare),
@@ -1181,19 +1184,41 @@
 :- 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
-	% representation, but we don't know what the unification/comparison
-	% predicates are.
+	% predicates for a noncanonical type, if they are known.  The value
+	% `abstract_noncanonical_type' represents a 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 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)
 		)
-	;	abstract_noncanonical_type.
+	;	abstract_noncanonical_type(is_solver_type).
+
+	% The `where' attributes of a solver type definition must begin
+	% with
+	% 	representation is <<representation type>>,
+	% 	initialisation is <<init pred name>>,
+	% 	ground         is <<ground inst>>,
+	% 	any            is <<any inst>>
+	% 
+:- 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
@@ -1599,6 +1624,7 @@
 	attributes(Language, may_call_mercury, not_thread_safe,
 		not_tabled_for_io, impure, depends_on_mercury_calls,
 		no, no, []).
+
 
 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	18 Aug 2004 00:58:55 -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,19 @@
 :- 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.
+	%
+:- pred parse_type_decl_where_part_if_present(is_solver_type::in,
+		module_name::in, term::in, term::out,
+		maybe2(maybe(solver_type_details), maybe(unify_compare))::out)
+			is det.
 
 %-----------------------------------------------------------------------------%
 
@@ -262,6 +262,7 @@
 
 :- implementation.
 
+:- import_module check_hlds__inst_util.
 :- import_module libs__globals.
 :- import_module libs__options.
 :- import_module parse_tree__modules.
@@ -1519,19 +1520,84 @@
 		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(_NoSolverTypeDetails,
+						 MaybeUserEqComp),
+				process_du_type(ModuleName, H, Body, Ctors,
+					MaybeUserEqComp, 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(MaybeSolverTypeDetails, MaybeUserEqComp),
+			process_solver_type(ModuleName, H,
+				MaybeSolverTypeDetails, MaybeUserEqComp, R1),
+			check_no_attributes(R1, Attributes, R)
+		)
+	).
+
+
+:- 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 +1719,362 @@
 
 %-----------------------------------------------------------------------------%
 
-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) :-
 	(
-		B = term__functor(term__atom("where"), Args, _Context1),
-		Args = [Body1, EqCompTerm]
+		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, no)
+	).
+
+
+:- func parse_type_decl_where_term(is_solver_type, module_name, maybe(term)) =
+		maybe2(maybe(solver_type_details), maybe(unify_compare)).
+
+parse_type_decl_where_term(_IsSolverType, _ModuleName, no) =
+	ok(no, no).
+
+parse_type_decl_where_term(IsSolverType, ModuleName, MaybeTerm0 @ yes(Term)) =
+		MaybeWhereDetails :-
+	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)
+	),
+	MaybeWhereDetails =
+		make_maybe_where_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) :-
+	(
+		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(
+			LHS = term__functor(term__atom(Name), [], _Context2)
+		->
+			Result0 = Parser(RHS),
+			(
+				Result0 = ok(X),
+				Result  = ok(yes(X))
+			;
+				Result0 = error(Msg, ProblemTerm),
+				Result  = error(Msg, ProblemTerm)
+			)
+		;
+			Result = 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"),
-				[], _Context2)
+				[],
+				_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_where_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
+	) = maybe2(maybe(solver_type_details), maybe(unify_compare)).
+
+make_maybe_where_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(_))
+	->
+			% rafe: XXX I think this is wrong.  There isn't
+			% a problem with having the solver_type_details
+			% and type_is_abstract_noncanonical.
+		(
+			RepresentationIsResult = ok(no),
+			InitialisationIsResult = ok(no),
+			GroundIsResult         = ok(no),
+			AnyIsResult            = ok(no),
+			EqualityIsResult       = ok(no),
+			ComparisonIsResult     = ok(no)
 		->
-			MaybeEqComp = ok(yes(abstract_noncanonical_type))
+			ok(no, yes(abstract_noncanonical_type(IsSolverType)))
 		;
-			parse_equality_or_comparison_pred_term("equality",
-				EqCompTerm, PredName)
+			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)
 		->
-			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),
-			(
-				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)
-			;
-				EqPredNameResult = error(M, T),
-				MaybeEqComp = error(M, T)
+			ok(yes(solver_type_details(RepnType, InitPred,
+					GroundInst, AnyInst)),
+			   yes(unify_compare(MaybeEqPred, MaybeCmpPred))
 			)
 		;
-			MaybeEqComp = error("syntax error after `where'",
-				Body)
+			error("missing solver type attribute: " ++
+				"required solver type attributes are " ++
+				"`representation', `initialisation', " ++
+				"`ground', and `any'", WhereTerm)
 		)
 	;
-		Body = B,
-		MaybeEqComp = ok(no)
+		% 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(no, yes(unify_compare(MaybeEqPred, MaybeCmpPred)))
+	;
+		func_error("prog_io__make_maybe_where_details: " ++
+			"shouldn't have reached this point!")
 	).
 
-:- 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.
 
-:- pred make_equality(sym_name::in, maybe(unify_compare)::out) is det.
-make_equality(Pred, yes(unify_compare(yes(Pred), no))).
+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").
+
+
+:- 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).
 
-:- pred make_comparison(sym_name::in, maybe(unify_compare)::out) is det.
-make_comparison(Pred, yes(unify_compare(no, yes(Pred)))).
 
 	% get_determinism(Term0, Term, Determinism) binds Determinism
 	% to a representation of the determinism condition of Term0, if any,
@@ -1842,6 +2189,45 @@
 
 %-----------------------------------------------------------------------------%
 
+:- pred process_solver_type(module_name::in, term::in,
+		maybe(solver_type_details)::in, maybe(unify_compare)::in,
+		maybe1(processed_type_body)::out) is det.
+
+process_solver_type(ModuleName, Head, MaybeSolverTypeDetails, MaybeUserEqComp,
+		Result) :-
+	(
+		MaybeSolverTypeDetails = yes(SolverTypeDetails),
+		dummy_term(Body),
+		parse_type_defn_head(ModuleName, Head, Body, Result0),
+		(
+			Result0 = error(String, Term),
+			Result  = error(String, Term)
+		;
+			Result0 = ok(Name, Args0),
+			(
+				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(SolverTypeDetails,
+					     	MaybeUserEqComp)))
+			)
+		)
+	;
+		MaybeSolverTypeDetails = no,
+		Result = error("solver type with no solver_type_details",
+				Head)
+	).
+
+%-----------------------------------------------------------------------------%
+
 	% 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 +2235,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 +2246,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 +2256,106 @@
 
 %-----------------------------------------------------------------------------%
 
-	% process_du_type(ModuleName, TypeHead, TypeBody, Result)
+	% process_du_type(ModuleName, TypeHead, TypeBody,
+	% 	MaybeUserEqComp, 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, maybe(unify_compare)::in,
+		maybe1(processed_type_body)::out) is det.
+
+process_du_type(ModuleName, Head, Body, Ctors, MaybeUserEqComp, 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,
+			MaybeUserEqComp, Result)
+	).
+
+
+:- pred process_du_type_2(sym_name::in, list(term)::in, term::in,
+		list(constructor)::in, maybe(unify_compare)::in,
+		maybe1(processed_type_body)::out) is det.
+
+process_du_type_2(Functor, Args0, Body, Ctors, MaybeUserEqComp, 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, MaybeUserEqComp)))
 	).
 
 %-----------------------------------------------------------------------------%
@@ -2013,18 +2401,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 +2439,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.
+
+:- func convert_constructors(module_name, term) = maybe1(list(constructor)).
 
-:- pred convert_constructors(module_name, term, list(constructor)).
-:- mode convert_constructors(in, in, out) is semidet.
-convert_constructors(ModuleName, Body, Constrs) :-
+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 +4125,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.71
diff -u -r1.71 prog_io_pragma.m
--- prog_io_pragma.m	20 Jul 2004 04:41:05 -0000	1.71
+++ prog_io_pragma.m	18 Aug 2004 01:05:50 -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(_NoSolverTypeDetails, MaybeUserEqComp),
 			(
-				MaybeUserEqCompare = yes(_),
+				MaybeUserEqComp = yes(_),
 				Result0 = ok(Item0)
 			->
 				(
@@ -56,7 +57,7 @@
 				->
 					Result = ok(Item0 ^ td_ctor_defn :=
 						foreign_type(Type,
-							MaybeUserEqCompare,
+							MaybeUserEqComp,
 							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,6 +136,12 @@
 					( parse_maybe_foreign_type_assertions(
 						MaybeAssertionTerm, Assertions)
 					->
+							% rafe: XXX I'm not
+							% sure that
+							% `no'
+							% here is right - we
+							% might need some more
+							% parsing...
 						Result = ok(type_defn(TVarSet,
 							MercuryTypeSymName,
 							MercuryArgs,
@@ -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.68
diff -u -r1.68 prog_util.m
--- prog_util.m	20 Jul 2004 04:41:06 -0000	1.68
+++ prog_util.m	18 Aug 2004 01:05:50 -0000
@@ -723,3 +723,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	17 Aug 2004 06:06:52 -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	12 Aug 2004 07:01:58 -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	18 Aug 2004 00:48:53 -0000
@@ -272,14 +272,19 @@
 			% generated unification procedure.
 			{ BodyItem = Item }
 		;
-			{ Body = du_type(_, IsSolverType, _) },
+			{ Body = du_type(_, _) },
 			{ NameItem = type_defn(VarSet, Name, Args,
-				abstract_type(IsSolverType), Cond) },
+					abstract_type(non_solver_type),
+					Cond) },
 			{ BodyItem = Item }
 		;
 			{ 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: 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	17 Aug 2004 06:18:21 -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
@@ -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.65
diff -u -r1.65 table_gen.m
--- table_gen.m	20 Jul 2004 04:41:06 -0000	1.65
+++ table_gen.m	18 Aug 2004 01:05:52 -0000
@@ -2096,7 +2096,7 @@
 			(
 				Ctors = TypeBody ^ du_type_ctors,
 				TypeBody ^ du_type_is_enum = yes,
-				TypeBody ^ du_type_usereq = no
+				TypeBody ^ du_type_usereq  = no
 			->
 				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	12 Aug 2004 07:02:42 -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	18 Aug 2004 00:55:31 -0000
@@ -327,7 +327,26 @@
 			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(SolverTypeDetails,
+					_MaybeUserEqComp),
+			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)
+		;
+			TypeBody = foreign_type(ForeignBody),
 			foreign_type_body_to_exported_type(ModuleInfo, 
 				ForeignBody, _, _, Assertions),
 			(
@@ -351,12 +370,12 @@
 			Details = eqv(MaybePseudoTypeInfo)
 		;
 			TypeBody = du_type(Ctors, ConsTagMap, Enum,
-				EqualityPred, ReservedTag, _, _),
+				MaybeUserEqComp, ReservedTag, _),
 			(
-				EqualityPred = yes(_),
+				MaybeUserEqComp = yes(_),
 				EqualityAxioms = user_defined
 			;
-				EqualityPred = no,
+				MaybeUserEqComp = no,
 				EqualityAxioms = standard
 			),
 			(
@@ -385,7 +404,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	18 Aug 2004 00:55:43 -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
@@ -83,12 +93,23 @@
 :- pred type_body_has_user_defined_equality_pred(module_info::in,
 	hlds_type_body::in, unify_compare::out) is semidet.
 
-	% Succeed if the inst `any' can be considered `bound' for this type.
+	% 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.
+
 :- 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)
@@ -777,10 +800,7 @@
 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_to_type_defn_body(ModuleInfo, Type, TypeBody),
 	type_body_has_user_defined_equality_pred(ModuleInfo, TypeBody,
 		UserEqComp).
 
@@ -788,7 +808,7 @@
 	module_info_globals(ModuleInfo, Globals),
 	globals__get_target(Globals, Target),
 	(
-		TypeBody = du_type(_, _, _, _, _, _, _),
+		TypeBody = du_type(_, _, _, _, _, _),
 		(
 			TypeBody ^ du_type_is_foreign_type =
 				yes(ForeignTypeBody),
@@ -796,43 +816,76 @@
 				yes)
 		->
 			UserEqComp =
-				foreign_type_body_has_user_defined_eq_comp_pred(
-					ModuleInfo, ForeignTypeBody)
+			    foreign_type_body_has_user_defined_eq_comp_pred(
+				ModuleInfo, ForeignTypeBody)
 		;
 			TypeBody ^ du_type_usereq = yes(UserEqComp)
 		)
 	;
-		TypeBody = foreign_type(ForeignTypeBody, _),
+		TypeBody = foreign_type(ForeignTypeBody),
 		UserEqComp = foreign_type_body_has_user_defined_eq_comp_pred(
-			ModuleInfo, ForeignTypeBody)
+					ModuleInfo, ForeignTypeBody)
+	;
+		TypeBody = solver_type(_SolverTypeDetails, yes(UserEqComp))
 	).
 
-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(SolverTypeDetails, _MaybeUserEqComp),
+		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.357
diff -u -r1.357 typecheck.m
--- typecheck.m	20 Jul 2004 16:06:40 -0000	1.357
+++ typecheck.m	18 Aug 2004 01:05:52 -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.139
diff -u -r1.139 unify_proc.m
--- unify_proc.m	20 Jul 2004 04:41:08 -0000	1.139
+++ unify_proc.m	18 Aug 2004 01:05:53 -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,13 @@
 		ConsId = cons(CtorSymName, TupleArity),
 		map__from_assoc_list([ConsId - single_functor],
 			ConsTagValues),
-		TypeBody = du_type([Ctor], ConsTagValues, IsEnum,
-			UnifyPred, ReservedTag, IsSolverType, IsForeign),
+		TypeBody = du_type([Ctor], ConsTagValues, IsEnum, UnifyPred,
+				ReservedTag, IsForeign),
 		UnifyPred = no,
 		IsEnum = no,
 		IsForeign = no,
 		ReservedTag = no,
-		IsSolverType = non_solver_type,
+		IsForeign = no,
 		construct_type(TypeCtor, TupleArgTypes, Type),
 
 		term__context_init(Context)
@@ -691,6 +692,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 +707,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 +746,9 @@
 		H1, H2, Context, Clauses, !Info) :-
 	(
 		type_body_has_user_defined_equality_pred(ModuleInfo,
-			TypeBody, UserEqCompare)
+			TypeBody, UserEqComp)
 	->
-		unify_proc__generate_user_defined_unify_clauses(UserEqCompare,
+		unify_proc__generate_user_defined_unify_clauses(UserEqComp,
 			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.
@@ -824,7 +867,8 @@
 	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,
@@ -952,9 +996,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")
 		)
@@ -1013,7 +1060,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)
 		;
@@ -1096,7 +1147,7 @@
 	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(_),
 		_, _, _, _, _, !Info) :-
 	error("trying to create compare proc for abstract noncanonical type").
 generate_user_defined_compare_clauses(unify_compare(_, MaybeCompare),
--------------------------------------------------------------------------
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