[m-rev.] for review: constrained polymorphic insts

David Overton dmo at cs.mu.OZ.AU
Thu Feb 21 17:43:30 AEDT 2002


Hi everyone,

This change is for Fergus to review.  It could probably do with a few
more test cases, but I wanted to post what I've done so far before I go
home tonight.

Also, if anyone is looking for a new syntax war, perhaps you would like
to comment on the syntax I've chosen for constraining inst parameters
(i.e. `InstParameter =< Inst').


David

Estimated hours taken: 60
Branches: main

Extend constrained polymorphic modes to allow inst parameters to be
constrained to insts other than `ground'.  The main motivation for this
is that for HAL we want inst parameters constrained to `any', however
this change is more general and allows inst parameters to be constrained
to any valid inst.

Introduce the syntax `InstParam =< Inst' to constrain an inst parameter
`InstParam' to an inst `Inst' in a predicate or function mode
declaration.

compiler/inst.m:
	Add a new alternative `constrained_inst_var(inst_var, inst)' to
	the `inst' type.
	Remove `constrained_inst_var(inst_var)' alternative from the
	`ground_inst_info' type.

compiler/inst_match.m:
compiler/inst_util.m:
compiler/modecheck_unify.m:
	Make changes required to the core mode checking algorithms to
	handle the change.

compiler/prog_io.m:
compiler/prog_io_util.m:
compiler/prog_io_goal.m:
compiler/prog_io_pragma.m:
compiler/make_hlds.m:
	Add support for `=<'/2 insts, but only when parsing predicate
	and function mode declarations, lambda argument modes, and
	pragmas.
	Make sure any unconstrained inst parameters in these
	declarations are constrained to be `ground'.
	Check that all constraints for a declaration are consistent,
	i.e. the same constraint for every occurrence of an inst
	parameter.

compiler/hlds_out.m:
compiler/mercury_to_mercury.m:
	Support printing of `=<'/2 insts.

compiler/mode_util.m:
compiler/module_qual.m:
compiler/pd_util.m:
compiler/recompilation_usage.m:
	Handle the changes to the definition of the `inst' type.

doc/reference_manual.texi:
	Document the change.

tests/valid/Mmakefile:
tests/valid/constrained_poly_insts.m:
tests/invalid/Mmakefile:
tests/invalid/constrained_poly_insts.m:
	Add some test cases.

Index: compiler/hlds_out.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/hlds_out.m,v
retrieving revision 1.273
diff -u -r1.273 hlds_out.m
--- compiler/hlds_out.m	20 Feb 2002 03:14:02 -0000	1.273
+++ compiler/hlds_out.m	20 Feb 2002 04:58:19 -0000
@@ -3410,14 +3410,14 @@
 		construct_qualified_term(unqualified("is"), [
 			ModesTerm, det_to_term(Det, Context)], Context, Term)
 	;
-		GroundInstInfo = constrained_inst_var(Var),
-		Term = term__coerce(term__variable(Var))
-	;
 		GroundInstInfo = none,
 		Term = make_atom(inst_uniqueness(Uniq, "ground"), Context)
 	).
 inst_to_term(inst_var(Var), _) =
 	term__coerce(term__variable(Var)).
+inst_to_term(constrained_inst_var(Var, Inst), Context) =
+	term__functor(term__atom("=<"), [term__coerce(term__variable(Var)),
+			inst_to_term(Inst, Context)], Context).
 inst_to_term(abstract_inst(Name, Args), Context) =
 	inst_name_to_term(user_inst(Name, Args), Context).
 inst_to_term(defined_inst(InstName), Context) =
Index: compiler/inst.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst.m,v
retrieving revision 1.7
diff -u -r1.7 inst.m
--- compiler/inst.m	13 Oct 2000 13:55:28 -0000	1.7
+++ compiler/inst.m	21 Feb 2002 05:35:08 -0000
@@ -39,6 +39,10 @@
 				% about the ground inst.
 	;		not_reached
 	;		inst_var(inst_var)
+				% A constrained_inst_var is an inst variable
+				% that is constrained to match_final the
+				% specified inst.
+	;		constrained_inst_var(inst_var, inst)
 				% A defined_inst is possibly recursive
 				% inst whose value is stored in the
 				% inst_table.  This is used both for
@@ -69,9 +73,6 @@
 :- type ground_inst_info
 	--->	higher_order(pred_inst_info)
 			% The ground inst is higher-order.
-	;	constrained_inst_var(inst_var)
-			% The ground inst is an inst variable that is
-			% constrained to be ground.
 	;	none.
 			% No extra information is available.
 
Index: compiler/inst_match.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_match.m,v
retrieving revision 1.48
diff -u -r1.48 inst_match.m
--- compiler/inst_match.m	12 Oct 2001 05:23:41 -0000	1.48
+++ compiler/inst_match.m	19 Feb 2002 22:31:30 -0000
@@ -51,6 +51,13 @@
 	% part of the inst is a defined inst, and if so replaces it
 	% with the definition.
 
+:- pred inst_expand_and_remove_constrained_inst_vars(module_info, inst, inst).
+:- mode inst_expand_and_remove_constrained_inst_vars(in, in, out) is det.
+
+	% inst_expand_and_remove_constrained_inst_vars is the same as
+	% inst_expand except that it also removes constrained_inst_vars from the
+	% top level, replacing them with the constraining inst.
+
 %-----------------------------------------------------------------------------%
 
 :- pred inst_matches_initial(inst, inst, type, module_info).
@@ -60,6 +67,9 @@
 		inst_var_sub, inst_var_sub).
 :- mode inst_matches_initial(in, in, in, in, out, in, out) is semidet.
 
+:- pred inst_matches_final(inst, inst, module_info).
+:- mode inst_matches_final(in, in, in) is semidet.
+
 :- pred inst_matches_final(inst, inst, type, module_info).
 :- mode inst_matches_final(in, in, in, in) is semidet.
 
@@ -327,89 +337,100 @@
 		inst_match_info, inst_match_info).
 :- mode inst_matches_initial_3(in, in, in, in, out) is semidet.
 
+inst_matches_initial_3(InstA, InstB, Type, Info0, Info) :-
+	( InstB = constrained_inst_var(InstVarB, InstB1) ->
+		% InstB is a constrained_inst_var with upper bound InstB1.
+		% We need to check that InstA matches_initial InstB1 and add the
+		% appropriate inst_var substitution.
+
+		inst_matches_initial_2(InstA, InstB1, Type, Info0, Info1),
+
+		ModuleInfo0 = Info1^module_info,
+		Sub0 = Info1^sub,
+
+		% Call abstractly_unify_inst to calculate the uniqueness of the
+		% inst represented by the constrained_inst_var.
+		% We pass `Live = dead' because we want
+		% abstractly_unify(unique, unique) = unique, not shared.
+		Live = dead,
+		abstractly_unify_inst(Live, InstA, InstB1, fake_unify,
+			ModuleInfo0, Inst, _Det, ModuleInfo1),
+		update_inst_var_sub(InstVarB, Inst, Type,
+			ModuleInfo1, ModuleInfo, Sub0, Sub),
+		Info = (Info1^module_info := ModuleInfo)
+			^sub := Sub
+	; InstA = constrained_inst_var(_InstVarA, InstA1) ->
+		inst_matches_initial_2(InstA1, InstB, Type, Info0, Info)
+	;
+		inst_matches_initial_4(InstA, InstB, Type, Info0, Info)
+	).
+
+:- pred inst_matches_initial_4(inst, inst, maybe(type), 
+		inst_match_info, inst_match_info).
+:- mode inst_matches_initial_4(in, in, in, in, out) is semidet.
+
 	% To avoid infinite regress, we assume that
 	% inst_matches_initial is true for any pairs of insts which
 	% occur in `Expansions'.
 
-inst_matches_initial_3(any(UniqA), any(UniqB), _, I, I) :-
+inst_matches_initial_4(any(UniqA), any(UniqB), _, I, I) :-
 	unique_matches_initial(UniqA, UniqB).
-inst_matches_initial_3(any(_), free, _, I, I).
-inst_matches_initial_3(free, any(_), _, I, I).
-inst_matches_initial_3(free, free, _, I, I).
-inst_matches_initial_3(bound(UniqA, ListA), any(UniqB), _, Info, Info) :-
+inst_matches_initial_4(any(_), free, _, I, I).
+inst_matches_initial_4(free, any(_), _, I, I).
+inst_matches_initial_4(free, free, _, I, I).
+inst_matches_initial_4(bound(UniqA, ListA), any(UniqB), _, Info, Info) :-
 	unique_matches_initial(UniqA, UniqB),
 	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info).
-inst_matches_initial_3(bound(_Uniq, _List), free, _, I, I).
-inst_matches_initial_3(bound(UniqA, ListA), bound(UniqB, ListB), Type,
+inst_matches_initial_4(bound(_Uniq, _List), free, _, I, I).
+inst_matches_initial_4(bound(UniqA, ListA), bound(UniqB, ListB), Type,
 		Info0, Info) :-
 	unique_matches_initial(UniqA, UniqB),
 	bound_inst_list_matches_initial(ListA, ListB, Type, Info0, Info).
-inst_matches_initial_3(bound(UniqA, ListA), ground(UniqB, none), _,
+inst_matches_initial_4(bound(UniqA, ListA), ground(UniqB, none), _,
 		Info, Info) :-
 	unique_matches_initial(UniqA, UniqB),
 	bound_inst_list_is_ground(ListA, Info^module_info),
 	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info).
-inst_matches_initial_3(bound(UniqA, ListA),
-		ground(UniqB, constrained_inst_var(InstVarB)), MaybeType,
-		Info0, Info) :-
-	unique_matches_initial(UniqA, UniqB),
-	ModuleInfo0 = Info0^module_info,
-	Sub0 = Info0^sub,
-	bound_inst_list_is_ground(ListA, ModuleInfo0),
-	bound_inst_list_matches_uniq(ListA, UniqB, ModuleInfo0),
-
-	% Call abstractly_unify_inst to calculate the uniqueness of the 
-	% bound_inst arguments.  We pass `Live = dead' because we want
-	% abstractly_unify(unique, unique) = unique, not shared.
-	Live = dead,
-	abstractly_unify_inst(Live, bound(UniqA, ListA), ground(UniqB, none),
-		fake_unify, ModuleInfo0, Inst, _Det, ModuleInfo1),
-	update_inst_var_sub(InstVarB, Inst, MaybeType, ModuleInfo1, ModuleInfo,
-		Sub0, Sub),
-	Info = (Info0^module_info := ModuleInfo)
-		^sub := Sub.
-inst_matches_initial_3(bound(Uniq, List), abstract_inst(_,_), _, Info, Info) :-
+inst_matches_initial_4(bound(Uniq, List), abstract_inst(_,_), _, Info, Info) :-
 	Uniq = unique,
 	bound_inst_list_is_ground(List, Info^module_info),
 	bound_inst_list_is_unique(List, Info^module_info).
-inst_matches_initial_3(bound(Uniq, List), abstract_inst(_,_), _, Info, Info) :-
+inst_matches_initial_4(bound(Uniq, List), abstract_inst(_,_), _, Info, Info) :-
 	Uniq = mostly_unique,
 	bound_inst_list_is_ground(List, Info^module_info),
 	bound_inst_list_is_mostly_unique(List, Info^module_info).
-inst_matches_initial_3(ground(UniqA, GroundInstInfoA), any(UniqB), _,
+inst_matches_initial_4(ground(UniqA, GroundInstInfoA), any(UniqB), _,
 		Info, Info) :-
 	\+ ground_inst_info_is_nonstandard_func_mode(GroundInstInfoA,
 		Info^module_info),
 	unique_matches_initial(UniqA, UniqB).
-inst_matches_initial_3(ground(_Uniq, _PredInst), free, _, I, I).
-inst_matches_initial_3(ground(UniqA, GII_A), bound(UniqB, ListB), MaybeType,
+inst_matches_initial_4(ground(_Uniq, _PredInst), free, _, I, I).
+inst_matches_initial_4(ground(UniqA, _GII_A), bound(UniqB, ListB), MaybeType,
 		Info0, Info) :-
 	MaybeType = yes(Type),
 		% We can only check this case properly if the type is known.
-	GII_A \= constrained_inst_var(_),
-		% Don't overly constrain the inst_var.
 	unique_matches_initial(UniqA, UniqB),
 	bound_inst_list_is_complete_for_type(set__init, Info0^module_info,
 		ListB, Type),
 	ground_matches_initial_bound_inst_list(UniqA, ListB, yes(Type),
 		Info0, Info).
-inst_matches_initial_3(ground(UniqA, GroundInstInfoA),
+inst_matches_initial_4(ground(UniqA, GroundInstInfoA),
 		ground(UniqB, GroundInstInfoB), Type, Info0, Info) :-
 	unique_matches_initial(UniqA, UniqB),
 	ground_inst_info_matches_initial(GroundInstInfoA, GroundInstInfoB,
 		UniqB, Type, Info0, Info).
-inst_matches_initial_3(ground(_UniqA, none), abstract_inst(_,_),_,_,_) :-
+inst_matches_initial_4(ground(_UniqA, none), abstract_inst(_,_),_,_,_) :-
 		% I don't know what this should do.
 		% Abstract insts aren't really supported.
 	error("inst_matches_initial(ground, abstract_inst) == ??").
-inst_matches_initial_3(abstract_inst(_,_), any(shared), _, I, I).
-inst_matches_initial_3(abstract_inst(_,_), free, _, I, I).
-inst_matches_initial_3(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
+inst_matches_initial_4(abstract_inst(_,_), any(shared), _, I, I).
+inst_matches_initial_4(abstract_inst(_,_), free, _, I, I).
+inst_matches_initial_4(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
 		_Type, Info0, Info) :-
 	list__duplicate(length(ArgsA), no, MaybeTypes),
 		% XXX how do we get the argument types for an abstract inst?
 	inst_list_matches_initial(ArgsA, ArgsB, MaybeTypes, Info0, Info).
-inst_matches_initial_3(not_reached, _, _, I, I).
+inst_matches_initial_4(not_reached, _, _, I, I).
 
 %-----------------------------------------------------------------------------%
 
@@ -555,15 +576,6 @@
 ground_inst_info_matches_initial(higher_order(PredInstA),
 		higher_order(PredInstB), _, MaybeType) -->
 	pred_inst_matches_initial(PredInstA, PredInstB, MaybeType).
-ground_inst_info_matches_initial(GroundInstInfoA,
-		constrained_inst_var(InstVarB), UniqB, MaybeType) -->
-	{ Inst = ground(UniqB, GroundInstInfoA) },
-	ModuleInfo0 =^ module_info,
-	Sub0 =^ sub,
-	{ update_inst_var_sub(InstVarB, Inst, MaybeType, ModuleInfo0,
-		ModuleInfo, Sub0, Sub) },
-	^module_info := ModuleInfo,
-	^sub := Sub.
 
 :- pred pred_inst_matches_initial(pred_inst_info, pred_inst_info, maybe(type),
 	inst_match_info, inst_match_info).
@@ -749,8 +761,22 @@
 		Inst = Inst0
 	).
 
+inst_expand_and_remove_constrained_inst_vars(ModuleInfo, Inst0, Inst) :-
+	( Inst0 = defined_inst(InstName) ->
+		inst_lookup(ModuleInfo, InstName, Inst1),
+		inst_expand(ModuleInfo, Inst1, Inst)
+	; Inst0 = constrained_inst_var(_, Inst1) ->
+		inst_expand(ModuleInfo, Inst1, Inst)
+	;
+		Inst = Inst0
+	).
+
 %-----------------------------------------------------------------------------%
 
+inst_matches_final(InstA, InstB, ModuleInfo) :-
+	Info0 = init_inst_match_info(ModuleInfo),
+	inst_matches_final_2(InstA, InstB, no, Info0, _).
+
 inst_matches_final(InstA, InstB, Type, ModuleInfo) :-
 	Info0 = init_inst_match_info(ModuleInfo),
 	inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
@@ -838,6 +864,16 @@
 		% XXX how do we get the argument types for an abstract inst?
 	inst_list_matches_final(ArgsA, ArgsB, MaybeTypes, Info0, Info).
 inst_matches_final_3(not_reached, _, _, I, I).
+inst_matches_final_3(constrained_inst_var(InstVarA, InstA), InstB, MaybeType,
+		Info0, Info) :-
+	( InstB = constrained_inst_var(InstVarB, InstB1) ->
+		% Constrained_inst_vars match_final only if they are the same
+		% variable.
+		InstVarA = InstVarB,
+		inst_matches_final_2(InstA, InstB1, MaybeType, Info0, Info)
+	;
+		inst_matches_final_2(InstA, InstB, MaybeType, Info0, Info)
+	).
 
 :- pred ground_inst_info_matches_final(ground_inst_info, ground_inst_info,
 		maybe(type), inst_match_info, inst_match_info).
@@ -855,8 +891,6 @@
 ground_inst_info_matches_final(higher_order(PredInstA),
 		higher_order(PredInstB), MaybeType) -->
 	pred_inst_matches_2(PredInstA, PredInstB, MaybeType).
-ground_inst_info_matches_final(constrained_inst_var(InstVar),
-		constrained_inst_var(InstVar), _) --> [].
 
 :- pred inst_list_matches_final(list(inst), list(inst), list(maybe(type)),
 		inst_match_info, inst_match_info).
@@ -913,8 +947,10 @@
 	( set__member(ThisExpansion, Info0^expansions) ->
 		Info = Info0
 	;
-		inst_expand(Info0^module_info, InstA, InstA2),
-		inst_expand(Info0^module_info, InstB, InstB2),
+		inst_expand_and_remove_constrained_inst_vars(Info0^module_info,
+			InstA, InstA2),
+		inst_expand_and_remove_constrained_inst_vars(Info0^module_info,
+			InstB, InstB2),
 		set__insert(Info0^expansions, ThisExpansion, Expansions1),
 		inst_matches_binding_3(InstA2, InstB2, MaybeType,
 			Info0^expansions := Expansions1, Info)
@@ -932,9 +968,6 @@
 inst_matches_binding_3(bound(_UniqA, ListA), ground(_UniqB, none), _,
 		Info, Info) :-
 	bound_inst_list_is_ground(ListA, Info^module_info).
-inst_matches_binding_3(bound(_UniqA, ListA),
-		ground(_UniqB, constrained_inst_var(_)), _, Info, Info) :-
-	bound_inst_list_is_ground(ListA, Info^module_info).
 inst_matches_binding_3(ground(_UniqA, _), bound(_UniqB, ListB), MaybeType,
 		Info, Info) :-
 	bound_inst_list_is_ground(ListB, Info^module_info),
@@ -975,8 +1008,6 @@
 ground_inst_info_matches_binding(higher_order(PredInstA),
 		higher_order(PredInstB), MaybeType, ModuleInfo) :-
 	pred_inst_matches_1(PredInstA, PredInstB, MaybeType, ModuleInfo).
-ground_inst_info_matches_binding(constrained_inst_var(InstVar),
-		constrained_inst_var(InstVar), _, _).
 
 :- pred inst_list_matches_binding(list(inst), list(inst), list(maybe(type)),
 		inst_match_info, inst_match_info).
@@ -1036,6 +1067,8 @@
 inst_is_clobbered(_, bound(mostly_clobbered, _)).
 inst_is_clobbered(_, inst_var(_)) :-
         error("internal error: uninstantiated inst parameter").
+inst_is_clobbered(ModuleInfo, constrained_inst_var(_, Inst)) :-
+	inst_is_clobbered(ModuleInfo, Inst).
 inst_is_clobbered(ModuleInfo, defined_inst(InstName)) :-
         inst_lookup(ModuleInfo, InstName, Inst),
         inst_is_clobbered(ModuleInfo, Inst).
@@ -1048,6 +1081,8 @@
 inst_is_free(_, free(_Type)).
 inst_is_free(_, inst_var(_)) :-
         error("internal error: uninstantiated inst parameter").
+inst_is_free(ModuleInfo, constrained_inst_var(_, Inst)) :-
+	inst_is_free(ModuleInfo, Inst).
 inst_is_free(ModuleInfo, defined_inst(InstName)) :-
         inst_lookup(ModuleInfo, InstName, Inst),
         inst_is_free(ModuleInfo, Inst).
@@ -1062,6 +1097,8 @@
 inst_is_bound(_, bound(_, _)).
 inst_is_bound(_, inst_var(_)) :-
         error("internal error: uninstantiated inst parameter").
+inst_is_bound(ModuleInfo, constrained_inst_var(_, Inst)) :-
+	inst_is_bound(ModuleInfo, Inst).
 inst_is_bound(ModuleInfo, defined_inst(InstName)) :-
         inst_lookup(ModuleInfo, InstName, Inst),
         inst_is_bound(ModuleInfo, Inst).
@@ -1074,6 +1111,9 @@
 inst_is_bound_to_functors(_, bound(_Uniq, Functors), Functors).
 inst_is_bound_to_functors(_, inst_var(_), _) :-
         error("internal error: uninstantiated inst parameter").
+inst_is_bound_to_functors(ModuleInfo, constrained_inst_var(_, Inst), Functors)
+		:-
+	inst_is_bound_to_functors(ModuleInfo, Inst, Functors).
 inst_is_bound_to_functors(ModuleInfo, defined_inst(InstName), Functors) :-
         inst_lookup(ModuleInfo, InstName, Inst),
         inst_is_bound_to_functors(ModuleInfo, Inst, Functors).
@@ -1101,6 +1141,9 @@
 inst_is_ground_2(_, inst_var(_), Expansions, Expansions) :-
         error("internal error: uninstantiated inst parameter").
 inst_is_ground_2(ModuleInfo, Inst, Expansions0, Expansions) :-
+	Inst = constrained_inst_var(_, Inst2),
+	inst_is_ground_2(ModuleInfo, Inst2, Expansions0, Expansions).
+inst_is_ground_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
         ( set__member(Inst, Expansions0) ->
                 Expansions = Expansions0
@@ -1133,6 +1176,9 @@
 inst_is_ground_or_any_2(_, inst_var(_), _, _) :-
         error("internal error: uninstantiated inst parameter").
 inst_is_ground_or_any_2(ModuleInfo, Inst, Expansions0, Expansions) :-
+	Inst = constrained_inst_var(_, Inst2),
+	inst_is_ground_or_any_2(ModuleInfo, Inst2, Expansions0, Expansions).
+inst_is_ground_or_any_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
         ( set__member(Inst, Expansions0) ->
                 Expansions = Expansions0
@@ -1166,6 +1212,9 @@
 inst_is_unique_2(_, inst_var(_), _, _) :-
         error("internal error: uninstantiated inst parameter").
 inst_is_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
+	Inst = constrained_inst_var(_, Inst2),
+	inst_is_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).
+inst_is_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
         ( set__member(Inst, Expansions0) ->
                 Expansions = Expansions0
@@ -1206,6 +1255,9 @@
 inst_is_mostly_unique_2(_, inst_var(_), _, _) :-
         error("internal error: uninstantiated inst parameter").
 inst_is_mostly_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
+	Inst = constrained_inst_var(_, Inst2),
+	inst_is_mostly_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).
+inst_is_mostly_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
         ( set__member(Inst, Expansions0) ->
                 Expansions = Expansions0
@@ -1242,6 +1294,9 @@
 inst_is_not_partly_unique_2(_, inst_var(_), _, _) :-
         error("internal error: uninstantiated inst parameter").
 inst_is_not_partly_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
+	Inst = constrained_inst_var(_, Inst2),
+	inst_is_not_partly_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).
+inst_is_not_partly_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
         ( set__member(Inst, Expansions0) ->
                 Expansions = Expansions0
@@ -1285,6 +1340,9 @@
 inst_is_not_fully_unique_2(_, inst_var(_), _, _) :-
         error("internal error: uninstantiated inst parameter").
 inst_is_not_fully_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
+	Inst = constrained_inst_var(_, Inst2),
+	inst_is_not_fully_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).
+inst_is_not_fully_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
         ( set__member(Inst, Expansions0) ->
                 Expansions = Expansions0
@@ -1551,6 +1609,10 @@
 inst_contains_instname_2(ground(_Uniq, _), _, _, no, Expns, Expns).
 inst_contains_instname_2(inst_var(_), _, _, no, Expns, Expns).
 inst_contains_instname_2(not_reached, _, _, no, Expns, Expns).
+inst_contains_instname_2(constrained_inst_var(_, Inst), ModuleInfo, InstName,
+		Result, Expansions0, Expansions) :-
+	inst_contains_instname_2(Inst, ModuleInfo, InstName, Result,
+		Expansions0, Expansions).
 inst_contains_instname_2(defined_inst(InstName1), ModuleInfo, InstName,
 		Result, Expansions0, Expansions) :-
 	( InstName = InstName1 ->
Index: compiler/inst_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/inst_util.m,v
retrieving revision 1.18
diff -u -r1.18 inst_util.m
--- compiler/inst_util.m	12 Oct 2001 05:23:42 -0000	1.18
+++ compiler/inst_util.m	19 Feb 2002 22:36:17 -0000
@@ -203,6 +203,14 @@
 		Inst = not_reached,
 		Det = det,
 		ModuleInfo = ModuleInfo0
+	; InstA = constrained_inst_var(InstVar, InstA1) ->
+		abstractly_unify_constrained_inst_var(IsLive, InstVar, InstA1,
+			InstB, UnifyIsReal, ModuleInfo0, Inst, Det,
+			ModuleInfo)
+	; InstB = constrained_inst_var(InstVar, InstB1) ->
+		abstractly_unify_constrained_inst_var(IsLive, InstVar, InstB1,
+			InstA, UnifyIsReal, ModuleInfo0, Inst, Det,
+			ModuleInfo)
 	;
 		abstractly_unify_inst_3(IsLive, InstA, InstB, UnifyIsReal,
 			ModuleInfo0, Inst, Det, ModuleInfo)
@@ -322,27 +330,6 @@
 				Inst, Det, M) :-
 	make_ground_inst(Inst0, live, Uniq, Real, M0, Inst, Det, M).
 
-abstractly_unify_inst_3(live, ground(UniqX, constrained_inst_var(Var)),
-		any(UniqY), Real, M, ground(Uniq, constrained_inst_var(Var)),
-		semidet, M) :-
-	unify_uniq(live, Real, det, UniqX, UniqY, Uniq).
-
-abstractly_unify_inst_3(live, ground(Uniq0, constrained_inst_var(Var)), free,
-		Real, M, ground(Uniq, constrained_inst_var(Var)), det, M) :-
-	unify_uniq(live, Real, det, unique, Uniq0, Uniq).
-
-abstractly_unify_inst_3(live, ground(UniqX, constrained_inst_var(_)),
-		bound(UniqY, BoundInsts0), Real, M0, bound(Uniq, BoundInsts),
-		Det, M) :-
-	unify_uniq(live, Real, semidet, UniqX, UniqY, Uniq),
-	make_ground_bound_inst_list(BoundInsts0, live, UniqX, Real, M0,
-			BoundInsts, Det1, M),
-	det_par_conjunction_detism(Det1, semidet, Det).
-
-abstractly_unify_inst_3(live, ground(UniqA, constrained_inst_var(_V)),
-		ground(UniqB, GII), Real, M, ground(Uniq, GII), semidet, M) :-
-	unify_uniq(live, Real, semidet, UniqA, UniqB, Uniq).
-
 % abstractly_unify_inst_3(live, abstract_inst(_,_), free,       _, _, _, _, _)
 %       :- fail.
 
@@ -437,28 +424,6 @@
 				Inst, Det, M) :-
 	make_ground_inst(Inst0, dead, Uniq, Real, M0, Inst, Det, M).
 
-abstractly_unify_inst_3(dead, ground(UniqX, constrained_inst_var(Var)),
-		any(UniqY), Real, M, ground(Uniq, constrained_inst_var(Var)),
-		semidet, M) :-
-	allow_unify_bound_any(Real),
-	unify_uniq(dead, Real, semidet, UniqX, UniqY, Uniq).
-
-abstractly_unify_inst_3(dead, ground(Uniq, constrained_inst_var(Var)), free,
-		_Real, M, ground(Uniq, constrained_inst_var(Var)), det, M).
-
-abstractly_unify_inst_3(dead, ground(UniqA, constrained_inst_var(_)),
-		bound(UniqB, BoundInsts0), Real, M0, bound(Uniq, BoundInsts),
-		Det, M) :-
-	unify_uniq(dead, Real, semidet, UniqA, UniqB, Uniq),
-	make_ground_bound_inst_list(BoundInsts0, dead, UniqA, Real, M0,
-					BoundInsts, Det1, M),
-	det_par_conjunction_detism(Det1, semidet, Det).
-
-abstractly_unify_inst_3(dead, ground(UniqA, constrained_inst_var(_Var)),
-				ground(UniqB, GroundInstInfo), Real, M,
-				ground(Uniq, GroundInstInfo), det, M) :-
-	unify_uniq(dead, Real, det, UniqA, UniqB, Uniq).
-
 /***** abstract insts aren't really supported
 abstractly_unify_inst_3(dead, abstract_inst(N,As), bound(List), Real,
 			ModuleInfo, Result, Det, ModuleInfo) :-
@@ -511,8 +476,20 @@
 abstractly_unify_inst_functor(Live, InstA, ConsId, ArgInsts, ArgLives,
 		Real, ModuleInfo0, Inst, Det, ModuleInfo) :-
 	inst_expand(ModuleInfo0, InstA, InstA2),
-	abstractly_unify_inst_functor_2(Live, InstA2, ConsId, ArgInsts,
-			ArgLives, Real, ModuleInfo0, Inst, Det, ModuleInfo).
+	( InstA2 = constrained_inst_var(InstVar, InstA3) ->
+		abstractly_unify_inst_functor(Live, InstA3, ConsId, ArgInsts,
+			ArgLives, Real, ModuleInfo0, Inst0, Det, ModuleInfo),
+		(
+			\+ inst_matches_final(Inst0, InstA3, ModuleInfo)
+		->
+			Inst = Inst0
+		;
+			Inst = constrained_inst_var(InstVar, Inst0)
+		)
+	;
+		abstractly_unify_inst_functor_2(Live, InstA2, ConsId, ArgInsts,
+			ArgLives, Real, ModuleInfo0, Inst, Det, ModuleInfo)
+	).
 
 :- pred abstractly_unify_inst_functor_2(is_live, inst, cons_id, list(inst),
 			list(is_live), unify_is_real, module_info,
@@ -692,6 +669,33 @@
 	det_par_conjunction_detism(Det1, Det2, Det).
 
 %-----------------------------------------------------------------------------%
+
+:- pred abstractly_unify_constrained_inst_var(is_live, inst_var, inst, inst,
+		unify_is_real, module_info, inst, determinism, module_info).
+:- mode abstractly_unify_constrained_inst_var(in, in, in, in, in, in, out,
+		out, out) is semidet.
+
+abstractly_unify_constrained_inst_var(IsLive, InstVar, InstConstraint, InstB,
+		UnifyIsReal, ModuleInfo0, Inst, Det, ModuleInfo) :-
+	abstractly_unify_inst(IsLive, InstConstraint, InstB, UnifyIsReal,
+		ModuleInfo0, Inst0, Det, ModuleInfo),
+	( 
+		Inst0 = constrained_inst_var(InstVar, _)
+	->
+		% Avoid adding the same constrained_inst_var twice.
+		Inst = Inst0
+	;
+		\+ inst_matches_final(Inst0, InstConstraint, ModuleInfo)
+	->
+		% The inst has become too instantiated so the
+		% constrained_inst_var must be removed.
+		Inst = Inst0
+	;
+		% We can keep the constrained_inst_var.
+		Inst = constrained_inst_var(InstVar, Inst0)
+	).
+
+%-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
 :- pred unify_uniq(is_live, unify_is_real, determinism, uniqueness, uniqueness,
@@ -1098,6 +1102,16 @@
 	make_shared(Uniq0, Uniq).
 make_shared_inst(inst_var(_), _, _, _) :-
 	error("free inst var").
+make_shared_inst(constrained_inst_var(InstVar, Inst0), ModuleInfo0, Inst,
+		ModuleInfo) :-
+	make_shared_inst(Inst0, ModuleInfo0, Inst1, ModuleInfo),
+	(
+		\+ inst_matches_final(Inst1, Inst0, ModuleInfo)
+	->
+		Inst = Inst1
+	;
+		Inst = constrained_inst_var(InstVar, Inst1)
+	).
 make_shared_inst(abstract_inst(_,_), M, _, M) :-
 	error("make_shared_inst(abstract_inst)").
 make_shared_inst(defined_inst(InstName), ModuleInfo0, Inst, ModuleInfo) :-
@@ -1189,6 +1203,16 @@
 	make_mostly_uniq(Uniq0, Uniq).
 make_mostly_uniq_inst(inst_var(_), _, _, _) :-
 	error("free inst var").
+make_mostly_uniq_inst(constrained_inst_var(InstVar, Inst0), ModuleInfo0, Inst,
+		ModuleInfo) :-
+	make_mostly_uniq_inst(Inst0, ModuleInfo0, Inst1, ModuleInfo),
+	(
+		\+ inst_matches_final(Inst1, Inst0, ModuleInfo)
+	->
+		Inst = Inst1
+	;
+		Inst = constrained_inst_var(InstVar, Inst1)
+	).
 make_mostly_uniq_inst(abstract_inst(_,_), M, _, M) :-
 	error("make_mostly_uniq_inst(abstract_inst)").
 make_mostly_uniq_inst(defined_inst(InstName), ModuleInfo0, Inst, ModuleInfo) :-
@@ -1359,6 +1383,34 @@
 :- pred inst_merge_3(inst, inst, maybe(type), module_info, inst, module_info).
 :- mode inst_merge_3(in, in, in, in, out, out) is semidet.
 
+inst_merge_3(InstA, InstB, MaybeType, ModuleInfo0, Inst, ModuleInfo) :-
+	( InstA = constrained_inst_var(InstVarA, InstA1) ->
+		( InstB = constrained_inst_var(InstVarB, InstB1) ->
+			( InstVarA = InstVarB ->
+				inst_merge(InstA1, InstB1, MaybeType,
+					ModuleInfo0, Inst0, ModuleInfo),
+				Inst = constrained_inst_var(InstVarA, Inst0)
+				% We can keep the constrained_inst_var here
+				% since Inst0 = InstA1 `lub` InstB1 and the
+				% original constraint on InstVarA, InstC,
+				% must have been such that
+				% InstA1 `lub` InstB1 =< InstC
+			;
+				inst_merge(InstA1, InstB1, MaybeType,
+					ModuleInfo0, Inst, ModuleInfo)
+			)
+		;
+			inst_merge(InstA1, InstB, MaybeType, ModuleInfo0,
+				Inst, ModuleInfo)
+		)
+	;
+		inst_merge_4(InstA, InstB, MaybeType, ModuleInfo0, Inst,
+			ModuleInfo)
+	).
+
+:- pred inst_merge_4(inst, inst, maybe(type), module_info, inst, module_info).
+:- mode inst_merge_4(in, in, in, in, out, out) is semidet.
+
 % We do not yet allow merging of `free' and `any',
 % except in the case where the any is `mostly_clobbered_any'
 % or `clobbered_any', because that would require inserting
@@ -1371,12 +1423,12 @@
 % too weak -- it might not be able to detect bugs as well
 % as it can currently.
 
-inst_merge_3(any(UniqA), any(UniqB), _, M, any(Uniq), M) :-
+inst_merge_4(any(UniqA), any(UniqB), _, M, any(Uniq), M) :-
 	merge_uniq(UniqA, UniqB, Uniq).
-inst_merge_3(any(Uniq), free, _, M, any(Uniq), M) :-
+inst_merge_4(any(Uniq), free, _, M, any(Uniq), M) :-
 	% we do not yet allow merge of any with free, except for clobbered anys
 	( Uniq = clobbered ; Uniq = mostly_clobbered ).
-inst_merge_3(any(UniqA), bound(UniqB, ListB), _, ModInfo, any(Uniq), ModInfo) :-
+inst_merge_4(any(UniqA), bound(UniqB, ListB), _, ModInfo, any(Uniq), ModInfo) :-
 	merge_uniq_bound(UniqA, UniqB, ListB, ModInfo, Uniq),
 	% we do not yet allow merge of any with free, except for clobbered anys
 	( ( Uniq = clobbered ; Uniq = mostly_clobbered ) ->
@@ -1384,16 +1436,16 @@
 	;
 		bound_inst_list_is_ground_or_any(ListB, ModInfo)
 	).
-inst_merge_3(any(UniqA), ground(UniqB, _), _, M, any(Uniq), M) :-
+inst_merge_4(any(UniqA), ground(UniqB, _), _, M, any(Uniq), M) :-
 	merge_uniq(UniqA, UniqB, Uniq).
-inst_merge_3(any(UniqA), abstract_inst(_, _), _, M, any(Uniq), M) :-
+inst_merge_4(any(UniqA), abstract_inst(_, _), _, M, any(Uniq), M) :-
 	merge_uniq(UniqA, shared, Uniq),
 	% we do not yet allow merge of any with free, except for clobbered anys
 	( Uniq = clobbered ; Uniq = mostly_clobbered ).
-inst_merge_3(free, any(Uniq), _, M, any(Uniq), M) :-
+inst_merge_4(free, any(Uniq), _, M, any(Uniq), M) :-
 	% we do not yet allow merge of any with free, except for clobbered anys
 	( Uniq = clobbered ; Uniq = mostly_clobbered ).
-inst_merge_3(bound(UniqA, ListA), any(UniqB), _, ModInfo, any(Uniq), ModInfo) :-
+inst_merge_4(bound(UniqA, ListA), any(UniqB), _, ModInfo, any(Uniq), ModInfo) :-
 	merge_uniq_bound(UniqB, UniqA, ListA, ModInfo, Uniq),
 	% we do not yet allow merge of any with free, except for clobbered anys
 	( ( Uniq = clobbered ; Uniq = mostly_clobbered ) ->
@@ -1401,27 +1453,27 @@
 	;
 		bound_inst_list_is_ground_or_any(ListA, ModInfo)
 	).
-inst_merge_3(ground(UniqA, _), any(UniqB), _, M, any(Uniq), M) :-
+inst_merge_4(ground(UniqA, _), any(UniqB), _, M, any(Uniq), M) :-
 	merge_uniq(UniqA, UniqB, Uniq).
-inst_merge_3(abstract_inst(_, _), any(UniqB), _, M, any(Uniq), M) :-
+inst_merge_4(abstract_inst(_, _), any(UniqB), _, M, any(Uniq), M) :-
 	merge_uniq(shared, UniqB, Uniq),
 	% we do not yet allow merge of any with free, except for clobbered anys
 	( Uniq = clobbered ; Uniq = mostly_clobbered ).
-inst_merge_3(free, free, _, M, free, M).
-inst_merge_3(bound(UniqA, ListA), bound(UniqB, ListB), MaybeType, ModuleInfo0,
+inst_merge_4(free, free, _, M, free, M).
+inst_merge_4(bound(UniqA, ListA), bound(UniqB, ListB), MaybeType, ModuleInfo0,
 		bound(Uniq, List), ModuleInfo) :-
 	merge_uniq(UniqA, UniqB, Uniq),
 	bound_inst_list_merge(ListA, ListB, MaybeType, ModuleInfo0, List,
 		ModuleInfo).
-inst_merge_3(bound(UniqA, ListA), ground(UniqB, _), MaybeType, ModuleInfo0,
+inst_merge_4(bound(UniqA, ListA), ground(UniqB, _), MaybeType, ModuleInfo0,
 		Result, ModuleInfo) :-
 	inst_merge_bound_ground(UniqA, ListA, UniqB, MaybeType,
 		ModuleInfo0, Result, ModuleInfo).
-inst_merge_3(ground(UniqA, _), bound(UniqB, ListB), MaybeType, ModuleInfo0,
+inst_merge_4(ground(UniqA, _), bound(UniqB, ListB), MaybeType, ModuleInfo0,
 		Result, ModuleInfo) :-
 	inst_merge_bound_ground(UniqB, ListB, UniqA, MaybeType,
 		ModuleInfo0, Result, ModuleInfo).
-inst_merge_3(ground(UniqA, GroundInstInfoA), ground(UniqB, GroundInstInfoB),
+inst_merge_4(ground(UniqA, GroundInstInfoA), ground(UniqB, GroundInstInfoB),
 		_, ModuleInfo, ground(Uniq, GroundInstInfo), ModuleInfo) :-
 	(
 		GroundInstInfoA = higher_order(PredA),
@@ -1445,11 +1497,6 @@
 			GroundInstInfo = none
 		)
 	;       
-		GroundInstInfoA = constrained_inst_var(V),
-		GroundInstInfoB = constrained_inst_var(V)
-	->
-		GroundInstInfo = constrained_inst_var(V)
-	;
 		\+ ground_inst_info_is_nonstandard_func_mode(GroundInstInfoA,
 			ModuleInfo),
 		\+ ground_inst_info_is_nonstandard_func_mode(GroundInstInfoB,
@@ -1457,13 +1504,13 @@
 		GroundInstInfo = none
 	),
 	merge_uniq(UniqA, UniqB, Uniq).
-inst_merge_3(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
+inst_merge_4(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
 		_, ModuleInfo0, abstract_inst(Name, Args), ModuleInfo) :-
 	% We don't know the arguments types of an abstract inst.
 	MaybeTypes = list__duplicate(list__length(ArgsA), no),
 	inst_list_merge(ArgsA, ArgsB, MaybeTypes, ModuleInfo0, Args,
 		ModuleInfo).
-inst_merge_3(not_reached, Inst, _, M, Inst, M).
+inst_merge_4(not_reached, Inst, _, M, Inst, M).
 
 :- pred merge_uniq(uniqueness, uniqueness, uniqueness).
 :- mode merge_uniq(in, in, out) is det.
@@ -1548,6 +1595,10 @@
 merge_inst_uniq(not_reached, Uniq, _, Expansions, Expansions, Uniq).
 merge_inst_uniq(inst_var(_), _, _, Expansions, Expansions, _) :-
 	error("merge_inst_uniq: unexpected inst_var").
+merge_inst_uniq(constrained_inst_var(_InstVar, Inst0), UniqB, ModuleInfo,
+		Expansions0, Expansions, Uniq) :-
+	merge_inst_uniq(Inst0, UniqB, ModuleInfo, Expansions0, Expansions,
+		Uniq).
 
 %-----------------------------------------------------------------------------%
 
@@ -1571,7 +1622,7 @@
 			constructors_to_bound_insts(Constructors, UniqB,
 				ModuleInfo0, ListB0),
 			list__sort_and_remove_dups(ListB0, ListB),
-			inst_merge_3(bound(UniqA, ListA),
+			inst_merge_4(bound(UniqA, ListA),
 				bound(UniqB, ListB), MaybeType,
 				ModuleInfo0, Result, ModuleInfo)
 		;
Index: compiler/make_hlds.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/make_hlds.m,v
retrieving revision 1.399
diff -u -r1.399 make_hlds.m
--- compiler/make_hlds.m	8 Feb 2002 02:26:45 -0000	1.399
+++ compiler/make_hlds.m	18 Feb 2002 00:48:16 -0000
@@ -3915,7 +3915,8 @@
 get_mode_annotation(Arg0, Arg, MaybeAnnotation) :-
 	(
 		Arg0 = term__functor(term__atom("::"), [Arg1, ModeTerm], _),
-		convert_mode(term__coerce(ModeTerm), Mode)
+		convert_mode(allow_constrained_inst_var, term__coerce(ModeTerm),
+			Mode)
 	->
 		Arg = Arg1,
 		MaybeAnnotation = yes(Mode)
@@ -4641,13 +4642,22 @@
 :- pred get_procedure_matching_argmodes(assoc_list(proc_id, proc_info),
 		list(mode), module_info, proc_id).
 :- mode get_procedure_matching_argmodes(in, in, in, out) is semidet.
-get_procedure_matching_argmodes([P|Procs], Modes, ModuleInfo, OurProcId) :-
+
+get_procedure_matching_argmodes(Procs, Modes0, ModuleInfo, ProcId) :-
+	list__map(constrain_inst_vars_in_mode, Modes0, Modes),
+	get_procedure_matching_argmodes_2(Procs, Modes, ModuleInfo, ProcId).
+
+:- pred get_procedure_matching_argmodes_2(assoc_list(proc_id, proc_info),
+		list(mode), module_info, proc_id).
+:- mode get_procedure_matching_argmodes_2(in, in, in, out) is semidet.
+
+get_procedure_matching_argmodes_2([P|Procs], Modes, ModuleInfo, OurProcId) :-
 	P = ProcId - ProcInfo,
 	proc_info_argmodes(ProcInfo, ArgModes),
 	( mode_list_matches(Modes, ArgModes, ModuleInfo) ->
 		OurProcId = ProcId
 	;
-		get_procedure_matching_argmodes(Procs, Modes, ModuleInfo, 
+		get_procedure_matching_argmodes_2(Procs, Modes, ModuleInfo, 
 			OurProcId)
 	).
 
@@ -4657,13 +4667,22 @@
 :- pred get_procedure_matching_declmodes(assoc_list(proc_id, proc_info),
 		list(mode), module_info, proc_id).
 :- mode get_procedure_matching_declmodes(in, in, in, out) is semidet.
-get_procedure_matching_declmodes([P|Procs], Modes, ModuleInfo, OurProcId) :-
+
+get_procedure_matching_declmodes(Procs, Modes0, ModuleInfo, ProcId) :-
+	list__map(constrain_inst_vars_in_mode, Modes0, Modes),
+	get_procedure_matching_declmodes_2(Procs, Modes, ModuleInfo, ProcId).
+
+:- pred get_procedure_matching_declmodes_2(assoc_list(proc_id, proc_info),
+		list(mode), module_info, proc_id).
+:- mode get_procedure_matching_declmodes_2(in, in, in, out) is semidet.
+
+get_procedure_matching_declmodes_2([P|Procs], Modes, ModuleInfo, OurProcId) :-
 	P = ProcId - ProcInfo,
 	proc_info_declared_argmodes(ProcInfo, ArgModes),
 	( mode_list_matches(Modes, ArgModes, ModuleInfo) ->
 		OurProcId = ProcId
 	;
-		get_procedure_matching_declmodes(Procs, Modes, ModuleInfo, 
+		get_procedure_matching_declmodes_2(Procs, Modes, ModuleInfo, 
 			OurProcId)
 	).
 
Index: compiler/mercury_to_mercury.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mercury_to_mercury.m,v
retrieving revision 1.205
diff -u -r1.205 mercury_to_mercury.m
--- compiler/mercury_to_mercury.m	20 Feb 2002 03:14:10 -0000	1.205
+++ compiler/mercury_to_mercury.m	20 Feb 2002 04:58:22 -0000
@@ -998,11 +998,6 @@
 			add_string(")\n")
 		)
 	;
-		{ GroundInstInfo = constrained_inst_var(Var) },
-		mercury_format_tabs(Indent),
-		mercury_format_var(Var, VarSet, no),
-		add_string("\n")
-	;
 		{ GroundInstInfo = none},
 		mercury_format_uniqueness(Uniq, "ground"),
 		add_string("\n")
@@ -1011,6 +1006,13 @@
 	mercury_format_tabs(Indent),
 	mercury_format_var(Var, VarSet, no),
 	add_string("\n").
+mercury_format_structured_inst(constrained_inst_var(Var, Inst), Indent, VarSet)
+		-->
+	mercury_format_tabs(Indent),
+	mercury_format_var(Var, VarSet, no),
+	add_string(" =< "),
+	mercury_format_inst(Inst, VarSet),
+	add_string("\n").
 mercury_format_structured_inst(abstract_inst(Name, Args), Indent, VarSet) -->
 	mercury_format_structured_inst_name(user_inst(Name, Args), Indent,
 		VarSet).
@@ -1081,14 +1083,15 @@
 			add_string(")")
 		)
 	;
-		{ GroundInstInfo = constrained_inst_var(Var) },
-		mercury_format_var(Var, VarSet, no)
-	;
 		{ GroundInstInfo = none },
 		mercury_format_uniqueness(Uniq, "ground")
 	).
 mercury_format_inst(inst_var(Var), VarSet) -->
 	mercury_format_var(Var, VarSet, no).
+mercury_format_inst(constrained_inst_var(Var, Inst), VarSet) -->
+	mercury_format_var(Var, VarSet, no),
+	add_string(" =< "),
+	mercury_format_inst(Inst, VarSet).
 mercury_format_inst(abstract_inst(Name, Args), VarSet) -->
 	mercury_format_inst_name(user_inst(Name, Args), VarSet).
 mercury_format_inst(defined_inst(InstName), VarSet) -->
Index: compiler/mode_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/mode_util.m,v
retrieving revision 1.139
diff -u -r1.139 mode_util.m
--- compiler/mode_util.m	8 Nov 2001 05:56:01 -0000	1.139
+++ compiler/mode_util.m	18 Feb 2002 06:05:49 -0000
@@ -414,6 +414,10 @@
 	error("get_single_arg_inst: abstract insts not supported").
 get_single_arg_inst(inst_var(_), _, _, _) :-
 	error("get_single_arg_inst: inst_var").
+get_single_arg_inst(constrained_inst_var(_, Inst), ModuleInfo, ConsId,
+		ArgInst) :-
+	get_single_arg_inst(Inst, ModuleInfo, ConsId, ArgInst).
+	
 
 :- pred get_single_arg_inst_2(list(bound_inst), cons_id, inst).
 :- mode get_single_arg_inst_2(in, in, out) is semidet.
@@ -711,12 +715,12 @@
 		% be reported if anything tries to match with the inst.
 		Modes = Modes0
 	).
-
-propagate_ctor_info(ground(Uniq, constrained_inst_var(Var)), _, _, _,
-		ground(Uniq, constrained_inst_var(Var))).
 propagate_ctor_info(not_reached, _Type, _Constructors, _ModuleInfo,
 		not_reached).
 propagate_ctor_info(inst_var(V), _, _, _, inst_var(V)).
+propagate_ctor_info(constrained_inst_var(V, Inst0), Type, Constructors,
+		ModuleInfo, constrained_inst_var(V, Inst)) :-
+	propagate_ctor_info(Inst0, Type, Constructors, ModuleInfo, Inst).
 propagate_ctor_info(abstract_inst(Name, Args), _, _, _,
 		abstract_inst(Name, Args)).	% XXX loses info
 propagate_ctor_info(defined_inst(InstName), Type, Ctors, ModuleInfo, Inst) :-
@@ -780,10 +784,11 @@
 		% be reported if anything tries to match with the inst.
 		Modes = Modes0
 	).
-propagate_ctor_info_lazily(ground(Uniq, constrained_inst_var(Var)), _, _, _,
-		ground(Uniq, constrained_inst_var(Var))).
 propagate_ctor_info_lazily(not_reached, _Type, _, _ModuleInfo, not_reached).
 propagate_ctor_info_lazily(inst_var(Var), _, _, _, inst_var(Var)).
+propagate_ctor_info_lazily(constrained_inst_var(V, Inst0), Type, Constructors,
+		ModuleInfo, constrained_inst_var(V, Inst)) :-
+	propagate_ctor_info_lazily(Inst0, Type, Constructors, ModuleInfo, Inst).
 propagate_ctor_info_lazily(abstract_inst(Name, Args), _, _, _,
 		abstract_inst(Name, Args)).	% XXX loses info
 propagate_ctor_info_lazily(defined_inst(InstName0), Type0, Subst, _,
@@ -1067,6 +1072,16 @@
 	;
 		Result = inst_var(Var)
 	).
+inst_apply_substitution(constrained_inst_var(Var, Inst0), Subst, Result) :-
+	(
+		map__search(Subst, Var, Replacement)
+	->
+		Result = Replacement
+		% XXX Should probably have a sanity check here that
+		% Replacement =< Inst0
+	;
+		Result = constrained_inst_var(Var, Inst0)
+	).
 inst_apply_substitution(defined_inst(InstName0), Subst,
 		    defined_inst(InstName)) :-
 	( inst_name_apply_substitution(InstName0, Subst, InstName1) ->
@@ -1113,15 +1128,6 @@
 	GII0 = higher_order(pred_inst_info(PredOrFunc, Modes0, Det)),
 	mode_list_apply_substitution(Modes0, Subst, Modes),
 	GII = higher_order(pred_inst_info(PredOrFunc, Modes, Det)).
-ground_inst_info_apply_substitution(constrained_inst_var(Var), Subst, Uniq,
-		Inst) :-
-	(
-		map__search(Subst, Var, Inst0)
-	->
-		Inst = Inst0
-	;
-		Inst = ground(Uniq, constrained_inst_var(Var))
-	).
 
 	% mode_list_apply_substitution(Modes0, Subst, Modes) is true
 	% iff Mode is the mode that results from applying Subst to Modes0.
@@ -1173,13 +1179,6 @@
 		list__map(rename_apart_inst_vars_in_mode(Sub), Modes0, Modes),
 		GI = higher_order(pred_inst_info(PoF, Modes, Det))
 	;
-		GI0 = constrained_inst_var(V0),
-		( map__search(Sub, V0, term__variable(V)) ->
-			GI = constrained_inst_var(V)
-		;
-			GI = GI0
-		)
-	;
 		GI0 = none,
 		GI = none
 	).
@@ -1190,6 +1189,14 @@
 	;
 		V = V0
 	).
+rename_apart_inst_vars_in_inst(Sub, constrained_inst_var(V0, Inst0),
+		constrained_inst_var(V, Inst)) :-
+	rename_apart_inst_vars_in_inst(Sub, Inst0, Inst),
+	( map__search(Sub, V0, term__variable(V1)) ->
+		V = V1
+	;
+		V = V0
+	).
 rename_apart_inst_vars_in_inst(Sub, defined_inst(Name0), defined_inst(Name)) :-
 	( rename_apart_inst_vars_in_inst_name(Sub, Name0, Name1) ->
 		Name = Name1
@@ -1705,6 +1712,9 @@
 	list__map(strip_builtin_qualifiers_from_inst, Insts0, Insts).
 
 strip_builtin_qualifiers_from_inst(inst_var(V), inst_var(V)).
+strip_builtin_qualifiers_from_inst(constrained_inst_var(V, Inst0),
+		constrained_inst_var(V, Inst)) :-
+	strip_builtin_qualifiers_from_inst(Inst0, Inst).
 strip_builtin_qualifiers_from_inst(not_reached, not_reached).
 strip_builtin_qualifiers_from_inst(free, free).
 strip_builtin_qualifiers_from_inst(free(Type), free(Type)).
@@ -1764,8 +1774,6 @@
 	Pred0 = pred_inst_info(Uniq, Modes0, Det),
 	Pred = pred_inst_info(Uniq, Modes, Det),
 	strip_builtin_qualifiers_from_mode_list(Modes0, Modes).
-strip_builtin_qualifiers_from_ground_inst_info(constrained_inst_var(Var),
-		constrained_inst_var(Var)).
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
Index: compiler/modecheck_unify.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/modecheck_unify.m,v
retrieving revision 1.47
diff -u -r1.47 modecheck_unify.m
--- compiler/modecheck_unify.m	31 Jul 2001 18:37:18 -0000	1.47
+++ compiler/modecheck_unify.m	20 Feb 2002 05:31:58 -0000
@@ -492,7 +492,8 @@
 			error("get_mode_of_args failed")
 		),
 		(
-			inst_expand(ModuleInfo1, InstOfX, InstOfX1),
+			inst_expand_and_remove_constrained_inst_vars(
+				ModuleInfo1, InstOfX, InstOfX1),
 			list__length(ArgVars0, Arity),
 			get_arg_insts(InstOfX1, InstConsId, Arity, InstOfXArgs),
 			get_mode_of_args(Inst, InstOfXArgs, ModeOfXArgs0)
@@ -1193,6 +1194,8 @@
 		{ List = [functor(_, InstList)] },
 		bind_args_2(Args, InstList)
 	).
+bind_args(constrained_inst_var(_, Inst), Args) -->
+	bind_args(Inst, Args).
 
 :- pred bind_args_2(list(prog_var), list(inst), mode_info, mode_info).
 :- mode bind_args_2(in, in, mode_info_di, mode_info_uo) is semidet.
@@ -1235,6 +1238,8 @@
 		List = [functor(_Name, ArgInstsB)],
 		get_mode_of_args_2(ArgInstsA, ArgInstsB, ArgModes)
 	).
+get_mode_of_args(constrained_inst_var(_, Inst), ArgInsts, ArgModes) :-
+	get_mode_of_args(Inst, ArgInsts, ArgModes).
 
 :- pred get_mode_of_args_2(list(inst), list(inst), list(mode)).
 :- mode get_mode_of_args_2(in, in, out) is semidet.
Index: compiler/module_qual.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/module_qual.m,v
retrieving revision 1.72
diff -u -r1.72 module_qual.m
--- compiler/module_qual.m	8 Feb 2002 02:26:52 -0000	1.72
+++ compiler/module_qual.m	18 Feb 2002 00:48:24 -0000
@@ -755,15 +755,14 @@
 		qualify_mode_list(Modes0, Modes, Info0, Info),
 		{ GroundInstInfo = higher_order(pred_inst_info(A, Modes, Det)) }
 	;
-		{ GroundInstInfo0 = constrained_inst_var(Var) },
-		{ GroundInstInfo = constrained_inst_var(Var) },
-		{ Info = Info0 }
-	;
 		{ GroundInstInfo0 = none },
 		{ GroundInstInfo = none },
 		{ Info = Info0 }
 	).
 qualify_inst(inst_var(Var), inst_var(Var), Info, Info) --> [].
+qualify_inst(constrained_inst_var(Var, Inst0), constrained_inst_var(Var, Inst),
+		Info0, Info) -->
+	qualify_inst(Inst0, Inst, Info0, Info).
 qualify_inst(defined_inst(InstName0), defined_inst(InstName), Info0, Info) -->
 	qualify_inst_name(InstName0, InstName, Info0, Info).
 qualify_inst(abstract_inst(Name, Args0), abstract_inst(Name, Args),
Index: compiler/pd_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/pd_util.m,v
retrieving revision 1.16
diff -u -r1.16 pd_util.m
--- compiler/pd_util.m	12 Oct 2001 05:23:45 -0000	1.16
+++ compiler/pd_util.m	8 Feb 2002 00:32:18 -0000
@@ -918,6 +918,9 @@
 pd_util__inst_size_2(_, free(_), _, 0).
 pd_util__inst_size_2(_, ground(_, _), _, 0).
 pd_util__inst_size_2(_, inst_var(_), _, 0).
+pd_util__inst_size_2(ModuleInfo, constrained_inst_var(_, Inst), Expansions,
+		Size) :-
+	pd_util__inst_size_2(ModuleInfo, Inst, Expansions, Size).
 pd_util__inst_size_2(_, abstract_inst(_, _), _, 0).
 pd_util__inst_size_2(ModuleInfo, defined_inst(InstName), Expansions0, Size) :-
 	( set__member(InstName, Expansions0) ->
Index: compiler/prog_io.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io.m,v
retrieving revision 1.200
diff -u -r1.200 prog_io.m
--- compiler/prog_io.m	12 Feb 2002 04:59:01 -0000	1.200
+++ compiler/prog_io.m	20 Feb 2002 05:41:11 -0000
@@ -188,6 +188,20 @@
 :- mode parse_implicitly_qualified_term(in, in, in, in, out) is det.
 
 %-----------------------------------------------------------------------------%
+
+	% Replace all occurrences of inst_var(I) with
+	% constrained_inst_var(I, ground(shared, none)).
+:- pred constrain_inst_vars_in_mode(mode, mode).
+:- mode constrain_inst_vars_in_mode(in, out) is det.
+
+%-----------------------------------------------------------------------------%
+
+	% Check that for each constrained_inst_var all occurrences have the
+	% same constraint.
+:- pred inst_var_constraints_are_consistent_in_modes(list(mode)).
+:- mode inst_var_constraints_are_consistent_in_modes(in) is semidet.
+
+%-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
 
 :- implementation.
@@ -1822,20 +1836,28 @@
 process_pred_2(ok(F, As0), PredType, VarSet0, MaybeDet, Cond, ExistQVars,
 		ClassContext, Attributes0, Result) :-
 	( convert_type_and_mode_list(As0, As) ->
-		( verify_type_and_mode_list(As) ->
-	        	get_purity(Attributes0, Purity, Attributes),
-			varset__coerce(VarSet0, TVarSet),
-			varset__coerce(VarSet0, IVarSet),
-			Result0 = ok(pred_or_func(TVarSet, IVarSet, ExistQVars,
-				predicate, F, As, MaybeDet, Cond, Purity,
-				ClassContext)),
-			check_no_attributes(Result0, Attributes, Result)
-		;
-			Result = error("some but not all arguments have modes",
-				PredType)
+	    ( verify_type_and_mode_list(As) ->
+		get_purity(Attributes0, Purity, Attributes),
+		varset__coerce(VarSet0, TVarSet),
+		varset__coerce(VarSet0, IVarSet),
+		(
+		    inst_var_constraints_are_consistent_in_type_and_modes(As)
+		->
+		    Result0 = ok(pred_or_func(TVarSet, IVarSet, ExistQVars,
+			predicate, F, As, MaybeDet, Cond, Purity,
+			ClassContext)),
+		    check_no_attributes(Result0, Attributes, Result)
+		;
+		    Result = error(
+	"inconsistent constraints on inst variables in predicate declaration",
+			    PredType)
 		)
+	    ;
+		Result = error("some but not all arguments have modes",
+		    PredType)
+	    )
 	;
-		Result = error("syntax error in `:- pred' declaration",
+	    Result = error("syntax error in `:- pred' declaration",
 				PredType)
 	).
 process_pred_2(error(M, T), _, _, _, _, _, _, _, error(M, T)).
@@ -2056,62 +2078,71 @@
 	->
 		parse_implicitly_qualified_term(ModuleName, FuncTerm, Term,
 			"`:- func' declaration", R),
-		process_func_3(R, FuncTerm, ReturnTypeTerm, VarSet, MaybeDet,
-				Cond, ExistQVars, Constraints, Attributes,
-				Result)
+		process_func_3(R, FuncTerm, ReturnTypeTerm, Term, VarSet,
+			MaybeDet, Cond, ExistQVars, Constraints, Attributes,
+			Result)
 	;
 		Result = error("`=' expected in `:- func' declaration", Term)
 	).
 
 
-:- pred process_func_3(maybe_functor, term, term, varset, maybe(determinism),
-			condition, existq_tvars, class_constraints, decl_attrs,
-			maybe1(item)).
-:- mode process_func_3(in, in, in, in, in, in, in, in, in, out) is det.
-
-process_func_3(ok(F, As0), FuncTerm, ReturnTypeTerm, VarSet0, MaybeDet, Cond,
-		ExistQVars, ClassContext, Attributes0, Result) :-
+:- pred process_func_3(maybe_functor, term, term, term, varset,
+	maybe(determinism), condition, existq_tvars, class_constraints,
+	decl_attrs, maybe1(item)).
+:- mode process_func_3(in, in, in, in, in, in, in, in, in, in, out) is det.
+
+process_func_3(ok(F, As0), FuncTerm, ReturnTypeTerm, FullTerm, VarSet0,
+		MaybeDet, Cond, ExistQVars, ClassContext, Attributes0, Result)
+		:-
 	( convert_type_and_mode_list(As0, As) ->
-		( \+ verify_type_and_mode_list(As) ->
-			Result = error("some but not all arguments have modes",
-					FuncTerm)
-		; convert_type_and_mode(ReturnTypeTerm, ReturnType) ->
-			(
-				As = [type_and_mode(_, _) | _],
-				ReturnType = type_only(_)
-			->
-				Result = error(
+	    ( \+ verify_type_and_mode_list(As) ->
+		Result = error("some but not all arguments have modes",
+		    FuncTerm)
+	    ; convert_type_and_mode(ReturnTypeTerm, ReturnType) ->
+		(
+		    As = [type_and_mode(_, _) | _],
+		    ReturnType = type_only(_)
+		->
+		    Result = error(
 		"function arguments have modes, but function result doesn't",
-					FuncTerm)
-			;
-				As = [type_only(_) | _],
-				ReturnType = type_and_mode(_, _)
-			->
-				Result = error(
+				    FuncTerm)
+		;
+		    As = [type_only(_) | _],
+		    ReturnType = type_and_mode(_, _)
+		->
+		    Result = error(
 		"function result has mode, but function arguments don't",
-					FuncTerm)
-			;
-				get_purity(Attributes0, Purity, Attributes),
-				varset__coerce(VarSet0, TVarSet),
-				varset__coerce(VarSet0, IVarSet),
-				list__append(As, [ReturnType], Args),
-				Result0 = ok(pred_or_func(TVarSet, IVarSet,
-					ExistQVars, function, F, Args,
-					MaybeDet, Cond, Purity, ClassContext)),
-				check_no_attributes(Result0, Attributes,
-					Result)
-			)
+				    FuncTerm)
 		;
+		    get_purity(Attributes0, Purity, Attributes),
+		    varset__coerce(VarSet0, TVarSet),
+		    varset__coerce(VarSet0, IVarSet),
+		    list__append(As, [ReturnType], Args),
+		    (
+			inst_var_constraints_are_consistent_in_type_and_modes(
+			    Args)
+		    ->
+				
+			Result0 = ok(pred_or_func(TVarSet, IVarSet, ExistQVars,
+			    function, F, Args, MaybeDet, Cond, Purity,
+			    ClassContext)),
+			check_no_attributes(Result0, Attributes, Result)
+		    ;
 			Result = error(
-			"syntax error in return type of `:- func' declaration",
-					ReturnTypeTerm)
+	"inconsistent constraints on inst variables in function declaration",
+			    FullTerm)
+		    )
 		)
-	;
+	    ;
 		Result = error(
-			"syntax error in arguments of `:- func' declaration",
+		    "syntax error in return type of `:- func' declaration",
+					ReturnTypeTerm)
+	    )
+	;
+	    Result = error("syntax error in arguments of `:- func' declaration",
 					FuncTerm)
 	).
-process_func_3(error(M, T), _, _, _, _, _, _, _, _, error(M, T)).
+process_func_3(error(M, T), _, _, _, _, _, _, _, _, _, error(M, T)).
 
 %-----------------------------------------------------------------------------%
 
@@ -2128,8 +2159,8 @@
 	->
 		parse_implicitly_qualified_term(ModuleName, FuncTerm, Term,
 				"function `:- mode' declaration", R),
-		process_func_mode(R, FuncTerm, ReturnTypeTerm, VarSet, MaybeDet,
-				Cond, Result)
+		process_func_mode(R, FuncTerm, ReturnTypeTerm, Term, VarSet,
+			MaybeDet, Cond, Result)
 	;
 		parse_implicitly_qualified_term(ModuleName, Term, Term,
 				"predicate `:- mode' declaration", R),
@@ -2142,54 +2173,62 @@
 
 process_pred_mode(ok(F, As0), PredMode, VarSet0, MaybeDet, Cond, Result) :-
 	(
-		convert_mode_list(As0, As1)
+		convert_mode_list(allow_constrained_inst_var, As0, As1)
 	->
 		list__map(constrain_inst_vars_in_mode, As1, As),
 		varset__coerce(VarSet0, VarSet),
-		Result = ok(pred_or_func_mode(VarSet, predicate, F, As,
+		( inst_var_constraints_are_consistent_in_modes(As) ->
+			Result = ok(pred_or_func_mode(VarSet, predicate, F, As,
 				MaybeDet, Cond))
+		;
+			Result = error(
+    "inconsistent constraints on inst variables in predicate mode declaration",
+				PredMode)
+		)
 	;
 		Result = error("syntax error in predicate mode declaration",
 				PredMode)
 	).
 process_pred_mode(error(M, T), _, _, _, _, error(M, T)).
 
-:- pred process_func_mode(maybe_functor, term, term, varset, maybe(determinism),
-			condition, maybe1(item)).
-:- mode process_func_mode(in, in, in, in, in, in, out) is det.
+:- pred process_func_mode(maybe_functor, term, term, term, varset,
+		maybe(determinism), condition, maybe1(item)).
+:- mode process_func_mode(in, in, in, in, in, in, in, out) is det.
 
-process_func_mode(ok(F, As0), FuncMode, RetMode0, VarSet0, MaybeDet, Cond,
-		Result) :-
+process_func_mode(ok(F, As0), FuncMode, RetMode0, FullTerm, VarSet0, MaybeDet,
+		Cond, Result) :-
 	(
-		convert_mode_list(As0, As1)
+	    convert_mode_list(allow_constrained_inst_var, As0, As1)
 	->
-		list__map(constrain_inst_vars_in_mode, As1, As),
-		( convert_mode(RetMode0, RetMode1) ->
-			constrain_inst_vars_in_mode(RetMode1, RetMode),
-			varset__coerce(VarSet0, VarSet),
-			list__append(As, [RetMode], ArgModes),
-			Result = ok(pred_or_func_mode(VarSet, function, F,
-					ArgModes, MaybeDet, Cond))
-		;
-			Result = error(
-		"syntax error in return mode of function mode declaration",
-					RetMode0)
+	    list__map(constrain_inst_vars_in_mode, As1, As),
+	    (
+		convert_mode(allow_constrained_inst_var, RetMode0, RetMode1)
+	    ->
+		constrain_inst_vars_in_mode(RetMode1, RetMode),
+		varset__coerce(VarSet0, VarSet),
+		list__append(As, [RetMode], ArgModes),
+		( inst_var_constraints_are_consistent_in_modes(ArgModes) ->
+		    Result = ok(pred_or_func_mode(VarSet, function,
+			F, ArgModes, MaybeDet, Cond))
+		;
+		    Result = error(
+    "inconsistent constraints on inst variables in function mode declaration",
+			FullTerm)
 		)
-	;
+	    ;
 		Result = error(
+		    "syntax error in return mode of function mode declaration",
+		    RetMode0)
+	    )
+	;
+	    Result = error(
 		"syntax error in arguments of function mode declaration",
-				FuncMode)
+		FuncMode)
 	).
-process_func_mode(error(M, T), _, _, _, _, _, error(M, T)).
+process_func_mode(error(M, T), _, _, _, _, _, _, error(M, T)).
 
 %-----------------------------------------------------------------------------%
 
-% Replace all occurrences of inst_var(I) with
-% ground(shared, constrained_inst_var(I)).
-
-:- pred constrain_inst_vars_in_mode(mode, mode).
-:- mode constrain_inst_vars_in_mode(in, out) is det.
-
 constrain_inst_vars_in_mode(I0 -> F0, I -> F) :-
 	constrain_inst_vars_in_inst(I0, I),
 	constrain_inst_vars_in_inst(F0, F).
@@ -2210,11 +2249,12 @@
 constrain_inst_vars_in_inst(ground(U, higher_order(PredInstInfo0)),
 		ground(U, higher_order(PredInstInfo))) :-
 	constrain_inst_vars_in_pred_inst_info(PredInstInfo0, PredInstInfo).
-constrain_inst_vars_in_inst(ground(U, constrained_inst_var(V)),
-		ground(U, constrained_inst_var(V))).
+constrain_inst_vars_in_inst(constrained_inst_var(V, Inst0),
+		constrained_inst_var(V, Inst)) :-
+	constrain_inst_vars_in_inst(Inst0, Inst).
 constrain_inst_vars_in_inst(not_reached, not_reached).
 constrain_inst_vars_in_inst(inst_var(V),
-		ground(shared, constrained_inst_var(V))).
+		constrained_inst_var(V, ground(shared, none))).
 constrain_inst_vars_in_inst(defined_inst(Name0), defined_inst(Name)) :-
 	constrain_inst_vars_in_inst_name(Name0, Name).
 constrain_inst_vars_in_inst(abstract_inst(N, Is0), abstract_inst(N, Is)) :-
@@ -2241,6 +2281,83 @@
 
 %-----------------------------------------------------------------------------%
 
+inst_var_constraints_are_consistent_in_modes(Modes) :-
+	inst_var_constraints_are_consistent_in_modes(Modes, map__init, _).
+
+:- pred inst_var_constraints_are_consistent_in_modes(list(mode),
+		inst_var_sub, inst_var_sub).
+:- mode inst_var_constraints_are_consistent_in_modes(in, in, out) is semidet.
+
+inst_var_constraints_are_consistent_in_modes(Modes) -->
+	list__foldl(inst_var_constraints_are_consistent_in_mode, Modes).
+
+:- pred inst_var_constraints_are_consistent_in_type_and_modes(
+		list(type_and_mode)).
+:- mode inst_var_constraints_are_consistent_in_type_and_modes(in) is semidet.
+
+inst_var_constraints_are_consistent_in_type_and_modes(TypeAndModes) :-
+	list__foldl((pred(TypeAndMode::in, in, out) is semidet -->
+		( { TypeAndMode = type_only(_) }
+		; { TypeAndMode = type_and_mode(_, Mode) },
+			inst_var_constraints_are_consistent_in_mode(Mode)
+		)), TypeAndModes, map__init, _).
+
+:- pred inst_var_constraints_are_consistent_in_mode(mode, inst_var_sub,
+		inst_var_sub).
+:- mode inst_var_constraints_are_consistent_in_mode(in, in, out) is semidet.
+
+inst_var_constraints_are_consistent_in_mode(InitialInst -> FinalInst) -->
+	inst_var_constraints_are_consistent_in_inst(InitialInst),
+	inst_var_constraints_are_consistent_in_inst(FinalInst).
+inst_var_constraints_are_consistent_in_mode(user_defined_mode(_, ArgInsts)) -->
+	inst_var_constraints_are_consistent_in_insts(ArgInsts).
+
+:- pred inst_var_constraints_are_consistent_in_insts(list(inst), inst_var_sub,
+		inst_var_sub).
+:- mode inst_var_constraints_are_consistent_in_insts(in, in, out) is semidet.
+
+inst_var_constraints_are_consistent_in_insts(Insts) -->
+	list__foldl(inst_var_constraints_are_consistent_in_inst, Insts).
+
+:- pred inst_var_constraints_are_consistent_in_inst(inst, inst_var_sub,
+		inst_var_sub).
+:- mode inst_var_constraints_are_consistent_in_inst(in, in, out) is semidet.
+
+inst_var_constraints_are_consistent_in_inst(any(_)) --> [].
+inst_var_constraints_are_consistent_in_inst(free) --> [].
+inst_var_constraints_are_consistent_in_inst(free(_)) --> [].
+inst_var_constraints_are_consistent_in_inst(bound(_, BoundInsts)) -->
+	list__foldl((pred(functor(_, Insts)::in, in, out) is semidet -->
+		inst_var_constraints_are_consistent_in_insts(Insts)),
+		BoundInsts).
+inst_var_constraints_are_consistent_in_inst(ground(_, GroundInstInfo)) -->
+	( { GroundInstInfo = none }
+	; { GroundInstInfo = higher_order(pred_inst_info(_, Modes, _)) },
+		inst_var_constraints_are_consistent_in_modes(Modes)
+	).
+inst_var_constraints_are_consistent_in_inst(not_reached) --> [].
+inst_var_constraints_are_consistent_in_inst(inst_var(_)) -->
+	{ error("inst_var_constraints_are_consistent_in_inst: unconstrained inst_var") }.
+inst_var_constraints_are_consistent_in_inst(defined_inst(InstName)) -->
+	( { InstName = user_inst(_, Insts) } ->
+		inst_var_constraints_are_consistent_in_insts(Insts)
+	;
+		[]
+	).
+inst_var_constraints_are_consistent_in_inst(abstract_inst(_, Insts)) -->
+	inst_var_constraints_are_consistent_in_insts(Insts).
+inst_var_constraints_are_consistent_in_inst(constrained_inst_var(V, Inst)) -->
+	( Inst0 =^ map__elem(V) ->
+		% Check that the inst_var constraint is consistent with the
+		% previous constraint on this inst_var.
+		{ Inst = Inst0 }
+	;
+		^ map__elem(V) := Inst
+	),
+	inst_var_constraints_are_consistent_in_inst(Inst).
+
+%-----------------------------------------------------------------------------%
+
 	% Parse a `:- inst <InstDefn>.' declaration.
 	%
 	% `==' is the correct operator to use, although we accept
@@ -2323,7 +2440,8 @@
 			% inst, i.e. that it does not have the form of
 			% one of the builtin insts
 			\+ (
-				convert_inst(Head, UserInst),
+				convert_inst(no_allow_constrained_inst_var,
+					Head, UserInst),
 				UserInst = defined_inst(user_inst(_, _))
 			)
 		->
@@ -2331,7 +2449,8 @@
 		;
 			% should improve the error message here
 			(
-				convert_inst(Body, ConvertedBody)
+				convert_inst(no_allow_constrained_inst_var,
+					Body, ConvertedBody)
 			->
 				list__map(term__coerce_var, Args, InstArgs),
 				Result = ok(
@@ -2481,7 +2600,8 @@
 		;
 			% should improve the error message here
 			(
-				convert_mode(Body, ConvertedBody)
+				convert_mode(no_allow_constrained_inst_var,
+					Body, ConvertedBody)
 			->
 				list__map(term__coerce_var, Args, InstArgs),
 				Result = ok(processed_mode_body(Name,
@@ -2513,7 +2633,7 @@
 				_Context)
 	->
 		convert_type(TypeTerm, Type),
-		convert_mode(ModeTerm, Mode0),
+		convert_mode(allow_constrained_inst_var, ModeTerm, Mode0),
 		constrain_inst_vars_in_mode(Mode0, Mode),
 		Result = type_and_mode(Type, Mode)
 	;
Index: compiler/prog_io_goal.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_goal.m,v
retrieving revision 1.20
diff -u -r1.20 prog_io_goal.m
--- compiler/prog_io_goal.m	25 Sep 2001 09:36:54 -0000	1.20
+++ compiler/prog_io_goal.m	13 Feb 2002 00:21:53 -0000
@@ -277,7 +277,8 @@
 				[LambdaArgsTerm, DetTerm], _),
 	DetTerm = term__functor(term__atom(DetString), [], _),
 	standard_det(DetString, Det),
-	parse_lambda_args(LambdaArgsTerm, Args, Modes).
+	parse_lambda_args(LambdaArgsTerm, Args, Modes),
+	inst_var_constraints_are_consistent_in_modes(Modes).
 
 :- pred parse_lambda_args(term, list(prog_term), list(mode)).
 :- mode parse_lambda_args(in, out, out) is semidet.
@@ -303,7 +304,8 @@
 parse_lambda_arg(Term, ArgTerm, Mode) :-
 	Term = term__functor(term__atom("::"), [ArgTerm0, ModeTerm], _),
 	term__coerce(ArgTerm0, ArgTerm),
-	convert_mode(ModeTerm, Mode).
+	convert_mode(allow_constrained_inst_var, ModeTerm, Mode0),
+	constrain_inst_vars_in_mode(Mode0, Mode).
 
 %-----------------------------------------------------------------------------%
 
@@ -314,7 +316,8 @@
 	standard_det(DetString, Det),
 	parse_lambda_eval_method(PredEvalArgsTerm, EvalMethod, PredArgsTerm),
 	PredArgsTerm = term__functor(term__atom("pred"), PredArgsList, _),
-	parse_pred_expr_args(PredArgsList, Args, Modes).
+	parse_pred_expr_args(PredArgsList, Args, Modes),
+	inst_var_constraints_are_consistent_in_modes(Modes).
 
 parse_dcg_pred_expression(PredTerm, EvalMethod, Args, Modes, Det) :-
 	PredTerm = term__functor(term__atom("is"),
@@ -323,7 +326,8 @@
 	standard_det(DetString, Det),
 	parse_lambda_eval_method(PredEvalArgsTerm, EvalMethod, PredArgsTerm),
 	PredArgsTerm = term__functor(term__atom("pred"), PredArgsList, _),
-	parse_dcg_pred_expr_args(PredArgsList, Args, Modes).
+	parse_dcg_pred_expr_args(PredArgsList, Args, Modes),
+	inst_var_constraints_are_consistent_in_modes(Modes).
 
 parse_func_expression(FuncTerm, EvalMethod, Args, Modes, Det) :-
 	%
@@ -340,7 +344,8 @@
 	( parse_pred_expr_args(FuncArgsList, Args0, Modes0) ->
 		parse_lambda_arg(RetTerm, RetArg, RetMode),
 		list__append(Args0, [RetArg], Args),
-		list__append(Modes0, [RetMode], Modes)
+		list__append(Modes0, [RetMode], Modes),
+		inst_var_constraints_are_consistent_in_modes(Modes)
 	;
 		%
 		% the argument modes default to `in',
@@ -377,6 +382,7 @@
 	RetMode = OutMode,
 	Det = det,
 	list__append(Modes0, [RetMode], Modes),
+	inst_var_constraints_are_consistent_in_modes(Modes),
 	list__append(Args0, [RetTerm], Args1),
 	list__map(term__coerce, Args1, Args).
 
@@ -412,10 +418,12 @@
 		list(mode)).
 :- mode parse_dcg_pred_expr_args(in, out, out) is semidet.
 
-parse_dcg_pred_expr_args([DCGModeTerm0, DCGModeTerm1], [],
-		[DCGMode0, DCGMode1]) :-
-	convert_mode(DCGModeTerm0, DCGMode0),
-	convert_mode(DCGModeTerm1, DCGMode1).
+parse_dcg_pred_expr_args([DCGModeTermA, DCGModeTermB], [],
+		[DCGModeA, DCGModeB]) :-
+	convert_mode(allow_constrained_inst_var, DCGModeTermA, DCGModeA0),
+	convert_mode(allow_constrained_inst_var, DCGModeTermB, DCGModeB0),
+	constrain_inst_vars_in_mode(DCGModeA0, DCGModeA),
+	constrain_inst_vars_in_mode(DCGModeB0, DCGModeB).
 parse_dcg_pred_expr_args([Term|Terms], [Arg|Args], [Mode|Modes]) :-
 	Terms = [_, _|_],
 	parse_lambda_arg(Term, Arg, Mode),
Index: compiler/prog_io_pragma.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_pragma.m,v
retrieving revision 1.47
diff -u -r1.47 prog_io_pragma.m
--- compiler/prog_io_pragma.m	19 Feb 2002 09:48:21 -0000	1.47
+++ compiler/prog_io_pragma.m	19 Feb 2002 22:44:01 -0000
@@ -1355,8 +1355,10 @@
 			varset__search_name(VarSet, Var, VarName)
 		->
 			(
-				convert_mode(ModeTerm, Mode)
+				convert_mode(allow_constrained_inst_var,
+					ModeTerm, Mode0)
 			->
+				constrain_inst_vars_in_mode(Mode0, Mode),
 				term__coerce_var(Var, ProgVar),
 				P = (pragma_var(ProgVar, VarName, Mode)),
 				parse_pragma_c_code_varlist(VarSet, 
@@ -1466,11 +1468,19 @@
 	(
 	    PredAndArgsResult =
 		ok(PredName, ArgModeTerms - MaybeRetModeTerm),
-	    ( convert_mode_list(ArgModeTerms, ArgModes0) ->
+	    (
+	    	convert_mode_list(allow_constrained_inst_var, ArgModeTerms,
+	    		ArgModes0)
+	    ->
 		(
 		    MaybeRetModeTerm = yes(RetModeTerm),
-		    ( convert_mode(RetModeTerm, RetMode) ->
-			list__append(ArgModes0, [RetMode], ArgModes),
+		    (
+		    	convert_mode(allow_constrained_inst_var, RetModeTerm,
+				RetMode)
+		    ->
+			list__append(ArgModes0, [RetMode], ArgModes1),
+			list__map(constrain_inst_vars_in_mode, ArgModes1,
+			    ArgModes),
 			Result = ok(PredName - function, ArgModes)
 		    ;
 			string__append("error in return mode in ",
Index: compiler/prog_io_util.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/prog_io_util.m,v
retrieving revision 1.21
diff -u -r1.21 prog_io_util.m
--- compiler/prog_io_util.m	25 Sep 2001 09:36:55 -0000	1.21
+++ compiler/prog_io_util.m	12 Feb 2002 04:10:39 -0000
@@ -87,17 +87,21 @@
 :- pred convert_type(term(T), type).
 :- mode convert_type(in, out) is det.
 
-:- pred convert_mode_list(list(term), list(mode)).
-:- mode convert_mode_list(in, out) is semidet.
+:- type allow_constrained_inst_var
+	--->	allow_constrained_inst_var
+	;	no_allow_constrained_inst_var.
 
-:- pred convert_mode(term, mode).
-:- mode convert_mode(in, out) is semidet.
+:- pred convert_mode_list(allow_constrained_inst_var, list(term), list(mode)).
+:- mode convert_mode_list(in, in, out) is semidet.
 
-:- pred convert_inst_list(list(term), list(inst)).
-:- mode convert_inst_list(in, out) is semidet.
+:- pred convert_mode(allow_constrained_inst_var, term, mode).
+:- mode convert_mode(in, in, out) is semidet.
 
-:- pred convert_inst(term, inst).
-:- mode convert_inst(in, out) is semidet.
+:- pred convert_inst_list(allow_constrained_inst_var, list(term), list(inst)).
+:- mode convert_inst_list(in, in, out) is semidet.
+
+:- pred convert_inst(allow_constrained_inst_var, term, inst).
+:- mode convert_inst(in, in, out) is semidet.
 
 :- pred standard_det(string, determinism).
 :- mode standard_det(in, out) is semidet.
@@ -257,10 +261,10 @@
 			list__map(strip_prog_context, As),
 			term__context_init).
 
-convert_mode_list([], []).
-convert_mode_list([H0|T0], [H|T]) :-
-	convert_mode(H0, H),
-	convert_mode_list(T0, T).
+convert_mode_list(_, [], []).
+convert_mode_list(AllowConstrainedInstVar, [H0|T0], [H|T]) :-
+	convert_mode(AllowConstrainedInstVar, H0, H),
+	convert_mode_list(AllowConstrainedInstVar, T0, T).
 
 
 	% 
@@ -273,7 +277,7 @@
 	% Eventually we can stop supporting :: and -> in :- mode
 	% declarations altogether.
 	%
-convert_mode(Term, Mode) :-
+convert_mode(AllowConstrainedInstVar, Term, Mode) :-
 	(
 		( 
 			Term = term__functor(term__atom(">>"), 
@@ -283,8 +287,8 @@
 				[InstA, InstB], _)
 		)
 	->
-		convert_inst(InstA, ConvertedInstA),
-		convert_inst(InstB, ConvertedInstB),
+		convert_inst(AllowConstrainedInstVar, InstA, ConvertedInstA),
+		convert_inst(AllowConstrainedInstVar, InstB, ConvertedInstB),
 		Mode = (ConvertedInstA -> ConvertedInstB)
 	;
 		% Handle higher-order predicate modes:
@@ -300,7 +304,8 @@
 	->
 		DetTerm = term__functor(term__atom(DetString), [], _),
 		standard_det(DetString, Detism),
-		convert_mode_list(ArgModesTerms, ArgModes),
+		convert_mode_list(AllowConstrainedInstVar, ArgModesTerms,
+			ArgModes),
 		PredInstInfo = pred_inst_info(predicate, ArgModes, Detism),
 		Inst = ground(shared, higher_order(PredInstInfo)),
 		Mode = (Inst -> Inst)
@@ -320,8 +325,9 @@
 	->
 		DetTerm = term__functor(term__atom(DetString), [], _),
 		standard_det(DetString, Detism),
-		convert_mode_list(ArgModesTerms, ArgModes0),
-		convert_mode(RetModeTerm, RetMode),
+		convert_mode_list(AllowConstrainedInstVar, ArgModesTerms,
+			ArgModes0),
+		convert_mode(AllowConstrainedInstVar, RetModeTerm, RetMode),
 		list__append(ArgModes0, [RetMode], ArgModes),
 		FuncInstInfo = pred_inst_info(function, ArgModes, Detism),
 		Inst = ground(shared, higher_order(FuncInstInfo)),
@@ -329,18 +335,18 @@
 	;
 		parse_qualified_term(Term, Term, "mode definition", R),
 		R = ok(Name, Args),	% should improve error reporting
-		convert_inst_list(Args, ConvertedArgs),
+		convert_inst_list(AllowConstrainedInstVar, Args, ConvertedArgs),
 		Mode = user_defined_mode(Name, ConvertedArgs)
 	).
 
-convert_inst_list([], []).
-convert_inst_list([H0|T0], [H|T]) :-
-	convert_inst(H0, H),
-	convert_inst_list(T0, T).
+convert_inst_list(_, [], []).
+convert_inst_list(AllowConstrainedInstVar, [H0|T0], [H|T]) :-
+	convert_inst(AllowConstrainedInstVar, H0, H),
+	convert_inst_list(AllowConstrainedInstVar, T0, T).
 
-convert_inst(term__variable(V0), inst_var(V)) :-
+convert_inst(_, term__variable(V0), inst_var(V)) :-
 	term__coerce_var(V0, V).
-convert_inst(Term, Result) :-
+convert_inst(AllowConstrainedInstVar, Term, Result) :-
 	Term = term__functor(Name, Args0, _Context),
 	% `free' insts
 	( Name = term__atom("free"), Args0 = [] ->
@@ -382,7 +388,8 @@
 	->
 		DetTerm = term__functor(term__atom(DetString), [], _),
 		standard_det(DetString, Detism),
-		convert_mode_list(ArgModesTerm, ArgModes),
+		convert_mode_list(AllowConstrainedInstVar, ArgModesTerm,
+			ArgModes),
 		PredInst = pred_inst_info(predicate, ArgModes, Detism),
 		Result = ground(shared, higher_order(PredInst))
 	;
@@ -401,8 +408,9 @@
 	->
 		DetTerm = term__functor(term__atom(DetString), [], _),
 		standard_det(DetString, Detism),
-		convert_mode_list(ArgModesTerm, ArgModes0),
-		convert_mode(RetModeTerm, RetMode),
+		convert_mode_list(AllowConstrainedInstVar, ArgModesTerm,
+			ArgModes0),
+		convert_mode(AllowConstrainedInstVar, RetModeTerm, RetMode),
 		list__append(ArgModes0, [RetMode], ArgModes),
 		FuncInst = pred_inst_info(function, ArgModes, Detism),
 		Result = ground(shared, higher_order(FuncInst))
@@ -413,20 +421,29 @@
 
 	% `bound' insts
 	; Name = term__atom("bound"), Args0 = [Disj] ->
-		parse_bound_inst_list(Disj, shared, Result)
+		parse_bound_inst_list(AllowConstrainedInstVar, Disj, shared,
+			Result)
 /* `bound_unique' is for backwards compatibility - use `unique' instead */
 	; Name = term__atom("bound_unique"), Args0 = [Disj] ->
-		parse_bound_inst_list(Disj, unique, Result)
+		parse_bound_inst_list(AllowConstrainedInstVar, Disj, unique,
+			Result)
 	; Name = term__atom("unique"), Args0 = [Disj] ->
-		parse_bound_inst_list(Disj, unique, Result)
+		parse_bound_inst_list(AllowConstrainedInstVar, Disj, unique,
+			Result)
 	; Name = term__atom("mostly_unique"), Args0 = [Disj] ->
-		parse_bound_inst_list(Disj, mostly_unique, Result)
+		parse_bound_inst_list(AllowConstrainedInstVar, Disj,
+			mostly_unique, Result)
+	; Name = term__atom("=<"), Args0 = [VarTerm, InstTerm] ->
+		AllowConstrainedInstVar = allow_constrained_inst_var,
+		VarTerm = term__variable(Var),
+		convert_inst(AllowConstrainedInstVar, InstTerm, Inst),
+		Result = constrained_inst_var(term__coerce_var(Var), Inst)
 
 	% anything else must be a user-defined inst
 	;
 		parse_qualified_term(Term, Term, "inst",
 			ok(QualifiedName, Args1)),
-		convert_inst_list(Args1, Args),
+		convert_inst_list(AllowConstrainedInstVar, Args1, Args),
 		Result = defined_inst(user_inst(QualifiedName, Args))
 	).
 
@@ -440,11 +457,13 @@
 standard_det("erroneous", erroneous).
 standard_det("failure", failure).
 
-:- pred parse_bound_inst_list(term::in, uniqueness::in, (inst)::out) is semidet.
+:- pred parse_bound_inst_list(allow_constrained_inst_var::in, term::in,
+		uniqueness::in, (inst)::out) is semidet.
 
-parse_bound_inst_list(Disj, Uniqueness, bound(Uniqueness, Functors)) :-
+parse_bound_inst_list(AllowConstrainedInstVar, Disj, Uniqueness,
+		bound(Uniqueness, Functors)) :-
 	disjunction_to_list(Disj, List),
-	convert_bound_inst_list(List, Functors0),
+	convert_bound_inst_list(AllowConstrainedInstVar, List, Functors0),
 	list__sort(Functors0, Functors),
 	% check that the list doesn't specify the same functor twice
 	\+ (
@@ -454,18 +473,19 @@
 		F2 = functor(ConsId, _)
 	).
 
-:- pred convert_bound_inst_list(list(term), list(bound_inst)).
-:- mode convert_bound_inst_list(in, out) is semidet.
-
-convert_bound_inst_list([], []).
-convert_bound_inst_list([H0|T0], [H|T]) :-
-	convert_bound_inst(H0, H),
-	convert_bound_inst_list(T0, T).
+:- pred convert_bound_inst_list(allow_constrained_inst_var, list(term),
+		list(bound_inst)).
+:- mode convert_bound_inst_list(in, in, out) is semidet.
+
+convert_bound_inst_list(_, [], []).
+convert_bound_inst_list(AllowConstrainedInstVar, [H0|T0], [H|T]) :-
+	convert_bound_inst(AllowConstrainedInstVar, H0, H),
+	convert_bound_inst_list(AllowConstrainedInstVar, T0, T).
 
-:- pred convert_bound_inst(term, bound_inst).
-:- mode convert_bound_inst(in, out) is semidet.
+:- pred convert_bound_inst(allow_constrained_inst_var, term, bound_inst).
+:- mode convert_bound_inst(in, in, out) is semidet.
 
-convert_bound_inst(InstTerm, functor(ConsId, Args)) :-
+convert_bound_inst(AllowConstrainedInstVar, InstTerm, functor(ConsId, Args)) :-
 	InstTerm = term__functor(Functor, Args0, _),
 	( Functor = term__atom(_) ->
 		parse_qualified_term(InstTerm, InstTerm, "inst",
@@ -477,7 +497,7 @@
 		list__length(Args1, Arity),
 		make_functor_cons_id(Functor, Arity, ConsId)
 	),
-	convert_inst_list(Args1, Args).
+	convert_inst_list(AllowConstrainedInstVar, Args1, Args).
 
 disjunction_to_list(Term, List) :-
 	binop_term_to_list(";", Term, List).
Index: compiler/recompilation_usage.m
===================================================================
RCS file: /home/mercury1/repository/mercury/compiler/recompilation_usage.m,v
retrieving revision 1.4
diff -u -r1.4 recompilation_usage.m
--- compiler/recompilation_usage.m	16 Jan 2002 01:13:41 -0000	1.4
+++ compiler/recompilation_usage.m	18 Feb 2002 06:10:51 -0000
@@ -1277,12 +1277,12 @@
 		{ GroundInstInfo = higher_order(pred_inst_info(_, Modes, _)) },
 		recompilation_usage__find_items_used_by_modes(Modes)
 	;
-		{ GroundInstInfo = constrained_inst_var(_) }
-	;
 		{ GroundInstInfo = none }
 	).
 recompilation_usage__find_items_used_by_inst(not_reached) --> [].
 recompilation_usage__find_items_used_by_inst(inst_var(_)) --> [].
+recompilation_usage__find_items_used_by_inst(constrained_inst_var(_, Inst)) -->
+	recompilation_usage__find_items_used_by_inst(Inst).
 recompilation_usage__find_items_used_by_inst(defined_inst(InstName)) -->
 	recompilation_usage__find_items_used_by_inst_name(InstName).
 recompilation_usage__find_items_used_by_inst(
Index: doc/reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.241
diff -u -r1.241 reference_manual.texi
--- doc/reference_manual.texi	18 Feb 2002 06:34:44 -0000	1.241
+++ doc/reference_manual.texi	20 Feb 2002 04:12:07 -0000
@@ -1821,6 +1821,7 @@
 @menu
 * Insts modes and mode definitions::
 * Predicate and function mode declarations::
+* Constrained polymorphic modes::
 * Different clauses for different modes::
 @end menu
 
@@ -2139,6 +2140,57 @@
 is the same as the one given by the procedure's declaration.
 
 The mode analysis algorithm annotates each call with the mode used.
+
+ at node Constrained polymorphic modes
+ at section Constrained polymorphic modes
+
+Mode declarations for predicates and functions may also have inst parameters.
+However, such parameters must be constrained to be @emph{compatible} with some
+other inst.
+The construct @samp{@var{InstParam} =< @var{Inst}},
+where @var{InstParam} is a variable and @var{Inst} is an inst,
+states that 
+ at var{InstParam} is constrained to be @emph{compatible} with @var{Inst},
+that is,
+ at var{InstParam} represents some inst that can be used anywhere where
+ at var{Inst} is required.
+If an inst parameter occurs more than once in a declaration, it must have the
+same constraint on each occurrence.
+
+For example, in the mode declaration
+ at example
+	:- mode append(in(list_skel(I =< ground)), in(list_skel(I =< ground)),
+	        out(list_skel(I =< ground))).
+ at end example
+ at noindent
+ at code{I} is an inst parameter which is constrained to be ground.  
+If @samp{append} is called with the first two arguments having an inst of, say,
+ at samp{list_skel(bound(f))} then after @samp{append} returns, all three arguments
+will have inst @samp{list_skel(bound(f))}.
+If the mode of append had been simply
+ at example
+	:- mode append(in(list_skel(ground)), in(list_skel(ground)),
+	        out(list_skel(ground))).
+ at end example
+ at noindent
+then we would only have been able to infer an inst of @samp{list_skel(ground)}
+for the third argument, not the more specific inst.
+
+Note that attempting to call @samp{append} when the first two arguments do not
+have ground insts (e.g. @samp{list_skel(bound(g(free)))}) is a mode error
+because it violates the constraint on the inst parameter.
+
+As a shortcut, if the constraint on an inst parameter is @samp{ground} then it
+is not necessary to give the constraint in the declaration.
+E.g. the above example could have been written as
+ at example
+	:- mode append(in(list_skel(I)), in(list_skel(I)), out(list_skel(I))).
+ at end example
+
+Constrained polymorphic modes are particularly useful when passing
+objects with higher-order types to polymorphic predicates
+since they allow the higher-order mode information to be retained
+(@pxref{Higher-order}).
 
 @node Different clauses for different modes
 @section Different clauses for different modes
Index: tests/invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.102
diff -u -r1.102 Mmakefile
--- tests/invalid/Mmakefile	11 Feb 2002 10:29:08 -0000	1.102
+++ tests/invalid/Mmakefile	21 Feb 2002 03:56:22 -0000
@@ -37,6 +37,7 @@
 	builtin_int.m \
 	builtin_proc.m \
 	circ_type.m \
+	constrained_poly_insts.m \
 	constructor_warning.m \
 	det_errors.m \
 	duplicate_modes.m \
Index: tests/invalid/constrained_poly_insts.err_exp
===================================================================
RCS file: tests/invalid/constrained_poly_insts.err_exp
diff -N tests/invalid/constrained_poly_insts.err_exp
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/constrained_poly_insts.err_exp	21 Feb 2002 03:55:33 -0000
@@ -0,0 +1,14 @@
+constrained_poly_insts.m:005: Error: inconsistent constraints on inst variables in predicate mode declaration: p(in(_1), out(_1 =< any)).
+constrained_poly_insts.m:007: Error: inconsistent constraints on inst variables in predicate declaration: q(_1 :: in(_2 =< free), _1 :: out(_2 =< bound(c))).
+constrained_poly_insts.m:010: Error: inconsistent constraints on inst variables in function mode declaration: r(in(_1)) = out(_1 =< free).
+constrained_poly_insts.m:012: Error: inconsistent constraints on inst variables in function declaration: s(_1 :: in(_2 =< ground)) = (_1 :: out(_2 =< unique)).
+constrained_poly_insts.m:017: Error: clause for predicate `constrained_poly_insts:q/2'
+constrained_poly_insts.m:017:   without preceding `pred' declaration.
+constrained_poly_insts.m:019: Error: clause for function `constrained_poly_insts:s/1'
+constrained_poly_insts.m:019:   without preceding `func' declaration.
+constrained_poly_insts.m:017: Inferred :- pred q(T1, T1).
+constrained_poly_insts.m:019: Inferred :- func s(T1) = T1.
+constrained_poly_insts.m:004: Error: no mode declaration for exported
+constrained_poly_insts.m:004:   predicate `constrained_poly_insts:p/2'.
+constrained_poly_insts.m:017: Error: no mode declaration for predicate `constrained_poly_insts:q/2'.
+For more information, try recompiling with `-E'.
Index: tests/invalid/constrained_poly_insts.m
===================================================================
RCS file: tests/invalid/constrained_poly_insts.m
diff -N tests/invalid/constrained_poly_insts.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/invalid/constrained_poly_insts.m	21 Feb 2002 04:25:24 -0000
@@ -0,0 +1,27 @@
+:- module constrained_poly_insts.
+:- interface.
+
+% Test that inconsistent declarations are not allowed.
+
+:- pred p(T, T).
+:- mode p(in(I), out(I =< any)) is det.
+
+:- pred q(T::in(I =< free), T::out(I =< bound(c))) is det.
+
+:- func r(T) = T.
+:- mode r(in(I)) = out(I =< free) is det.
+
+:- func s(T::in(I =< ground)) = (T::out(I =< unique)) is det.
+
+% Test that mode errors are detected correctly.
+
+:- pred t(int::in(I), int::out(I)) is det.
+
+:- implementation.
+
+p(X, X).
+q(X, X).
+r(X) = X.
+s(X) = X.
+
+t(_, 42).
Index: tests/valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.95
diff -u -r1.95 Mmakefile
--- tests/valid/Mmakefile	4 Jan 2002 05:56:40 -0000	1.95
+++ tests/valid/Mmakefile	21 Feb 2002 04:28:46 -0000
@@ -51,6 +51,7 @@
 	common_struct_bug.m \
 	compl_unify_bug.m \
 	complicated_unify.m \
+	constrained_poly_insts.m \
 	constructor_arg_names.m \
 	dcg_test.m \
 	deforest_bug.m \
Index: tests/valid/constrained_poly_insts.m
===================================================================
RCS file: tests/valid/constrained_poly_insts.m
diff -N tests/valid/constrained_poly_insts.m
--- /dev/null	1 Jan 1970 00:00:00 -0000
+++ tests/valid/constrained_poly_insts.m	21 Feb 2002 05:00:58 -0000
@@ -0,0 +1,39 @@
+:- module constrained_poly_insts.
+:- interface.
+
+:- pred search(tree(K, V), K, V).
+:- mode search(in(tree(K, V =< any)), in(K), out(V =< any)) is semidet.
+
+:- inst k == bound(a ; b ; c).
+:- inst v == (pred(in, out) is det).
+
+:- func call_search(tree(K, V), K) = V.
+:- mode call_search(in(tree(k, v)), in(k)) = out(v) is semidet.
+
+:- type tree(K, V) ---> empty ; node(tree(K, V), K, V, tree(K, V)).
+:- inst tree(K, V) ---> empty ; node(tree(K, V), K, V, tree(K, V)).
+
+:- inst b == bound(42 ; 43 ; 44).
+
+:- pred p(int::in(I =< b), int::out(I =< b)) is semidet.
+
+:- implementation.
+
+call_search(T, K) = V :- search(T, K, V).
+
+search(node(L, K0, V0, R), K, V) :-
+	compare(Res, K0, K),
+	(
+		Res = (<),
+		search(R, K, V)
+	;
+		Res = (=),
+		V = V0
+	;
+		Res = (>),
+		search(L, K, V)
+	).
+
+p(X, Y) :-
+	X = 42,
+	Y = X.
-- 
David Overton      Computer Science and Software Engineering
PhD Student        The University of Melbourne   +61 3 8344 9159
Research Fellow    Monash University (Clayton)   +61 3 9905 5779
--------------------------------------------------------------------------
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