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

David Overton dmo at cs.mu.OZ.AU
Thu Mar 7 12:37:07 AEDT 2002


Here is a relative diff which addresses Fergus's coments.

On Thu, Feb 21, 2002 at 06:40:38PM +1100, Fergus Henderson wrote:
> On 21-Feb-2002, David Overton <dmo at cs.mu.OZ.AU> wrote:
> > Index: doc/reference_manual.texi
> ...
> > + 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.
> 
> It's not clear from these words what kind of construct InstParam =< Inst is,
> or where in the syntax it is allowed to appear.  From the example below,
> I can guess that this construct is actually an inst, but this should be
> stated explicitly.

I have clarified the documentation here.

> 
> > +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))).
> 
> Wouldn't it be more consistent to use a syntax similar to the
> one that we use for type class constraints, e.g.
> 
> 	:- mode append(in(list_skel(I)), in(list_skel(I)),
> 	        out(list_skel(I))) <= I =< ground.

This syntax is now allowed.  I still allow the previously proposed
syntax also, since it is easier to support for writing insts in error
messages, hlds dumps, etc and also for specify modes in clause heads of
mode-specific clauses, pragma foreign proc, etc.

> 
> ?
> 
> Also, is it permitted to constrain one inst parameter as being
> compatible with another?
> 
> 	:- mode foo(in(I =< ground), in(J =< I)).

This is no longer permitted since it is not useful and only likely to
cause confusion.

On Thu, Feb 21, 2002 at 08:48:34PM +1100, Fergus Henderson wrote:
> The main problem I can see is that it doesn't handle uniqueness correctly.
> 
> On 21-Feb-2002, David Overton <dmo at cs.mu.OZ.AU> wrote:
> > Index: compiler/inst_match.m
> ...
> > +:- 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.
> 
> The difference between these two predicates should be documented.
> 
> (Also, the meaning of the inst_var_sub parameters in inst_matches_initial
> should be documented.)

Done.

> 
> > @@ -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)
> > +	).
> 
> Some comments here would help.

Done.

> 
> The if-then-else would probably be clearer if the `then' and the `else'
> parts were swapped.
> 
> The line `Inst = Inst0' throws away information; the compiler knows that
> Inst is at least as ground as InstVar, and is a subtype of InstVar,
> but these facts are not recorded in the inst returned.
> Is this going to cause trouble?
> Maybe there should be an XXX comment there.

I don't think this is likely to be a problem in practice because

	a) I don't think it's likely to occur very often with the
	   sorts of things I'm expecting this feature to be used for; and
	b) Even if the information is retained somehow, I can't see what
	   sort of situations it would actually be useful for.
	   Can you think of an example?

> 
> > +:- 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)
> > +	).
> 
> This seems a bit assymetrical.
> I'm concerned that the results may be different depending on
> whether unifications are written as `X = Y' or `Y = X'.

The intended (although not well documented) semantics was that 
constrained_inst_var(I, constrained_inst_var(J, Inst))
would be equivalent to
constrained_inst_var(J, constrained_inst_var(I, Inst)).
I've made this more explicit by changing the inst type to 

	constrained_inst_vars(set(inst_var), inst).

> 
> > +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 on `X =< clobbered' will give `X =< clobbered',
> which is wrong in the case where the inst parameter X happens to be `unique'.

There is no problem with this.  As I explained in a previous email, X
cannot be `unique' in this case.  I have fixed the comment on the
definition of the inst type.

> 
> > +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)
> > +	).
> 
> Likewise.

Likewise.

> 
> > @@ -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)
> > +			)
> 
> The call to inst_merge is the same in both branches of this if-then-else,
> so it should be hoisted out:

Done.

> 
> > @@ -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).
> 
> This might be wrong too.

There should be no problem here.

> 
> > +++ compiler/mercury_to_mercury.m	20 Feb 2002 04:58:22 -0000
> > +mercury_format_inst(constrained_inst_var(Var, Inst), VarSet) -->
> > +	mercury_format_var(Var, VarSet, no),
> > +	add_string(" =< "),
> > +	mercury_format_inst(Inst, VarSet).
> 
> You need to output parentheses around that.

Done.

> > +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)
> > +	).
> 
> Don't you need to apply substitutions recursively to Inst0?
> 
> E.g. what if you have an inst `X =< (Y =< ground)'?

Done.  

> 
> > Index: compiler/prog_io.m
> ...
> > +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
> > +	),
> 
> Please s/V/InstVar/g
> 
> (In connection with `map', my first guess at what `V' stands for
> is "value", not "variable".)

Done.

> 
> Otherwise that looks fine.


diff -u compiler/hlds_out.m compiler/hlds_out.m
--- compiler/hlds_out.m	20 Feb 2002 04:58:19 -0000
+++ compiler/hlds_out.m	5 Mar 2002 03:26:20 -0000
@@ -3378,6 +3378,7 @@
 inst_to_term(Inst) = inst_to_term(Inst, term__context_init).
 
 :- func inst_to_term(inst, prog_context) = prog_term.
+
 inst_to_term(any(Uniq), Context) =
 	make_atom(any_inst_uniqueness(Uniq), Context).
 inst_to_term(free, Context) =
@@ -3415,9 +3416,12 @@
 	).
 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(constrained_inst_vars(Vars, Inst), Context) =
+	set__fold(func(Var, Term) =
+			term__functor(term__atom("=<"),
+				[term__coerce(term__variable(Var)), Term],
+				Context),
+		Vars, inst_to_term(Inst, 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) =
diff -u compiler/inst.m compiler/inst.m
--- compiler/inst.m	21 Feb 2002 05:35:08 -0000
+++ compiler/inst.m	5 Mar 2002 03:20:13 -0000
@@ -23,7 +23,7 @@
 %     `abstract_cons_id' and use that here instead of `cons_id'.
 
 :- import_module prog_data, hlds_data.
-:- import_module list, map.
+:- import_module list, map, set.
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
@@ -39,10 +39,11 @@
 				% 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
+				% constrained_inst_vars is a set of inst
+				% variables that are constrained to have the
+				% same uniqueness as and to match_final the
 				% specified inst.
-	;		constrained_inst_var(inst_var, inst)
+	;		constrained_inst_vars(set(inst_var), inst)
 				% A defined_inst is possibly recursive
 				% inst whose value is stored in the
 				% inst_table.  This is used both for
diff -u compiler/inst_match.m compiler/inst_match.m
--- compiler/inst_match.m	19 Feb 2002 22:31:30 -0000
+++ compiler/inst_match.m	5 Mar 2002 03:27:54 -0000
@@ -60,20 +60,7 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred inst_matches_initial(inst, inst, type, module_info).
-:- mode inst_matches_initial(in, in, in, in) is semidet.
-
-:- pred inst_matches_initial(inst, inst, type, module_info, module_info,
-		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.
-
-	% inst_matches_initial(InstA, InstB, ModuleInfo):
+	% inst_matches_initial(InstA, InstB, Type, ModuleInfo):
 	%	Succeed iff `InstA' specifies at least as much
 	%	information as `InstB', and in those parts where they
 	%	specify the same information, `InstA' is at least as
@@ -84,6 +71,17 @@
 	%	inst_matches_initial(bound(a), bound(a;b), _) should
 	%	succeed, but not vice versa.
 
+:- pred inst_matches_initial(inst, inst, type, module_info).
+:- mode inst_matches_initial(in, in, in, in) is semidet.
+
+	% This version of inst_matches_initial builds up a substitution map
+	% (inst_var_sub).  For each inst_var which occurs in InstA there will be
+	% a substitution to the corresponding inst in InstB.
+
+:- pred inst_matches_initial(inst, inst, type, module_info, module_info,
+		inst_var_sub, inst_var_sub).
+:- mode inst_matches_initial(in, in, in, in, out, in, out) is semidet.
+
 	% inst_matches_final(InstA, InstB, ModuleInfo):
 	%	Succeed iff InstA is compatible with InstB,
 	%	i.e. iff InstA will satisfy the final inst
@@ -92,7 +90,19 @@
 	%	great as that specified by InstB, and where the information
 	%	is the same and both insts specify a binding, the binding
 	%	must be identical.
-	%
+
+:- pred inst_matches_final(inst, inst, module_info).
+:- mode inst_matches_final(in, in, in) is semidet.
+
+	% This version of inst_matches_final allows you to pass in the type of
+	% the variables being compared.  This allows it to be more precise (i.e.
+	% less conservative) for cases such as
+	%	inst_matches_final(ground(...), bound(...), ...).
+	% This version is to be preferred when the type is available.
+
+:- pred inst_matches_final(inst, inst, type, module_info).
+:- mode inst_matches_final(in, in, in, in) is semidet.
+
 	%	The difference between inst_matches_initial and
 	%	inst_matches_final is that inst_matches_initial requires
 	%	only something which is at least as instantiated,
@@ -297,10 +307,10 @@
 
 inst_matches_initial_1(InstA, InstB, Type, ModuleInfo0, ModuleInfo,
 		MaybeSub0, MaybeSub) :-
-	Info0 = init_inst_match_info(ModuleInfo0)^sub := MaybeSub0,
+	Info0 = init_inst_match_info(ModuleInfo0) ^ maybe_sub := MaybeSub0,
 	inst_matches_initial_2(InstA, InstB, yes(Type), Info0, Info),
 	ModuleInfo = Info^module_info,
-	MaybeSub = Info^sub.
+	MaybeSub = Info ^ maybe_sub.
 
 :- type expansions == set(pair(inst)).
 
@@ -308,9 +318,19 @@
 	--->	inst_match_info(
 			module_info	:: module_info,
 			expansions	:: expansions,
-			sub		:: maybe(inst_var_sub)
+			maybe_sub	:: maybe(inst_var_sub)
 		).
 
+:- func sub(inst_match_info) = inst_var_sub is semidet.
+
+sub(Info) = Sub :-
+	Info ^ maybe_sub = yes(Sub).
+
+:- func 'sub :='(inst_match_info, inst_var_sub) = inst_match_info.
+
+'sub :='(Info, Sub) =
+	Info ^ maybe_sub := yes(Sub).
+
 :- func init_inst_match_info(module_info) = inst_match_info.
 
 init_inst_match_info(ModuleInfo) = inst_match_info(ModuleInfo, Exp, no) :-
@@ -338,7 +358,7 @@
 :- 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 = constrained_inst_vars(InstVarsB, 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.
@@ -346,7 +366,6 @@
 		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.
@@ -355,11 +374,9 @@
 		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) ->
+		Info2 = Info1 ^ module_info := ModuleInfo1,
+		update_inst_var_sub(InstVarsB, Inst, Type, Info2, Info)
+	; InstA = constrained_inst_vars(_InstVarsA, InstA1) ->
 		inst_matches_initial_2(InstA1, InstB, Type, Info0, Info)
 	;
 		inst_matches_initial_4(InstA, InstB, Type, Info0, Info)
@@ -537,23 +554,27 @@
 	% Update the inst_var_sub that is computed by inst_matches_initial.
 	% The inst_var_sub records what inst should be substituted for each
 	% inst_var that occurs in the called procedure's argument modes.
-:- pred update_inst_var_sub(inst_var, inst, maybe(type), module_info,
-		module_info, maybe(inst_var_sub), maybe(inst_var_sub)).
-:- mode update_inst_var_sub(in, in, in, in, out, in, out) is semidet.
-
-update_inst_var_sub(_, _, _, ModuleInfo, ModuleInfo, no, no).
-update_inst_var_sub(InstVar, InstA, MaybeType, ModuleInfo0, ModuleInfo,
-		yes(Sub0), yes(Sub)) :-
-	( map__search(Sub0, InstVar, InstB) ->
-		% If InstVar already has an inst associated with it,
-		% merge the old inst and the new inst.  Fail if this merge
-		% is not possible.
-		inst_merge(InstA, InstB, MaybeType, ModuleInfo0, Inst,
-			ModuleInfo),
-		map__det_update(Sub0, InstVar, Inst, Sub)
+:- pred update_inst_var_sub(set(inst_var), inst, maybe(type), inst_match_info,
+		inst_match_info).
+:- mode update_inst_var_sub(in, in, in, in, out) is semidet.
+
+update_inst_var_sub(InstVars, InstA, MaybeType) -->
+	( yes(_) =^ maybe_sub ->
+		set__fold((pred(InstVar::in, in, out) is semidet -->
+			( InstB =^ sub ^ elem(InstVar) ->
+				% If InstVar already has an inst associated with
+				% it, merge the old inst and the new inst.  Fail
+				% if this merge is not possible.
+				M0 =^ module_info,
+				{ inst_merge(InstA, InstB, MaybeType, M0,
+					Inst, M) },
+				^ module_info := M,
+				^ sub ^ elem(InstVar) := Inst
+			;
+				^ sub ^ elem(InstVar) := InstA
+			)), InstVars)
 	;
-		ModuleInfo = ModuleInfo0,
-		map__det_insert(Sub0, InstVar, InstA, Sub)
+		[]
 	).
 
 %-----------------------------------------------------------------------------%
@@ -586,16 +607,15 @@
 	{ maybe_get_higher_order_arg_types(MaybeType, length(ModesA),
 		MaybeTypes) },
 	pred_inst_argmodes_matches_initial(ModesA, ModesB, MaybeTypes),
-	MaybeSub =^ sub,
-	{ 
-		MaybeSub = yes(Sub)
+	( 
+		Sub =^ sub
 	->
-		mode_list_apply_substitution(ModesA, Sub, ModesASub),
-		mode_list_apply_substitution(ModesB, Sub, ModesBSub)
+		{ mode_list_apply_substitution(ModesA, Sub, ModesASub) },
+		{ mode_list_apply_substitution(ModesB, Sub, ModesBSub) }
 	;
-		ModesASub = ModesA,
-		ModesBSub = ModesB
-	},
+		{ ModesASub = ModesA },
+		{ ModesBSub = ModesB }
+	),
 	pred_inst_argmodes_matches(ModesASub, ModesBSub, MaybeTypes).
 
 :- pred pred_inst_argmodes_matches_initial(list(mode), list(mode),
@@ -765,7 +785,7 @@
 	( Inst0 = defined_inst(InstName) ->
 		inst_lookup(ModuleInfo, InstName, Inst1),
 		inst_expand(ModuleInfo, Inst1, Inst)
-	; Inst0 = constrained_inst_var(_, Inst1) ->
+	; Inst0 = constrained_inst_vars(_, Inst1) ->
 		inst_expand(ModuleInfo, Inst1, Inst)
 	;
 		Inst = Inst0
@@ -864,9 +884,9 @@
 		% 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,
+inst_matches_final_3(constrained_inst_vars(InstVarA, InstA), InstB, MaybeType,
 		Info0, Info) :-
-	( InstB = constrained_inst_var(InstVarB, InstB1) ->
+	( InstB = constrained_inst_vars(InstVarB, InstB1) ->
 		% Constrained_inst_vars match_final only if they are the same
 		% variable.
 		InstVarA = InstVarB,
@@ -1067,7 +1087,7 @@
 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, constrained_inst_vars(_, Inst)) :-
 	inst_is_clobbered(ModuleInfo, Inst).
 inst_is_clobbered(ModuleInfo, defined_inst(InstName)) :-
         inst_lookup(ModuleInfo, InstName, Inst),
@@ -1081,7 +1101,7 @@
 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, constrained_inst_vars(_, Inst)) :-
 	inst_is_free(ModuleInfo, Inst).
 inst_is_free(ModuleInfo, defined_inst(InstName)) :-
         inst_lookup(ModuleInfo, InstName, Inst),
@@ -1097,7 +1117,7 @@
 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, constrained_inst_vars(_, Inst)) :-
 	inst_is_bound(ModuleInfo, Inst).
 inst_is_bound(ModuleInfo, defined_inst(InstName)) :-
         inst_lookup(ModuleInfo, InstName, Inst),
@@ -1111,8 +1131,8 @@
 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, constrained_inst_vars(_, 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),
@@ -1141,7 +1161,7 @@
 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 = constrained_inst_vars(_, Inst2),
 	inst_is_ground_2(ModuleInfo, Inst2, Expansions0, Expansions).
 inst_is_ground_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
@@ -1176,7 +1196,7 @@
 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 = constrained_inst_vars(_, 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),
@@ -1212,7 +1232,7 @@
 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 = constrained_inst_vars(_, Inst2),
 	inst_is_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).
 inst_is_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
@@ -1255,7 +1275,7 @@
 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 = constrained_inst_vars(_, Inst2),
 	inst_is_mostly_unique_2(ModuleInfo, Inst2, Expansions0, Expansions).
 inst_is_mostly_unique_2(ModuleInfo, Inst, Expansions0, Expansions) :-
 	Inst = defined_inst(InstName),
@@ -1294,7 +1314,7 @@
 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 = constrained_inst_vars(_, 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),
@@ -1340,7 +1360,7 @@
 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 = constrained_inst_vars(_, 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),
@@ -1609,7 +1629,7 @@
 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,
+inst_contains_instname_2(constrained_inst_vars(_, Inst), ModuleInfo, InstName,
 		Result, Expansions0, Expansions) :-
 	inst_contains_instname_2(Inst, ModuleInfo, InstName, Result,
 		Expansions0, Expansions).
diff -u compiler/inst_util.m compiler/inst_util.m
--- compiler/inst_util.m	19 Feb 2002 22:36:17 -0000
+++ compiler/inst_util.m	5 Mar 2002 03:29:00 -0000
@@ -203,12 +203,12 @@
 		Inst = not_reached,
 		Det = det,
 		ModuleInfo = ModuleInfo0
-	; InstA = constrained_inst_var(InstVar, InstA1) ->
-		abstractly_unify_constrained_inst_var(IsLive, InstVar, InstA1,
+	; InstA = constrained_inst_vars(InstVars, InstA1) ->
+		abstractly_unify_constrained_inst_vars(IsLive, InstVars, InstA1,
 			InstB, UnifyIsReal, ModuleInfo0, Inst, Det,
 			ModuleInfo)
-	; InstB = constrained_inst_var(InstVar, InstB1) ->
-		abstractly_unify_constrained_inst_var(IsLive, InstVar, InstB1,
+	; InstB = constrained_inst_vars(InstVars, InstB1) ->
+		abstractly_unify_constrained_inst_vars(IsLive, InstVars, InstB1,
 			InstA, UnifyIsReal, ModuleInfo0, Inst, Det,
 			ModuleInfo)
 	;
@@ -476,15 +476,18 @@
 abstractly_unify_inst_functor(Live, InstA, ConsId, ArgInsts, ArgLives,
 		Real, ModuleInfo0, Inst, Det, ModuleInfo) :-
 	inst_expand(ModuleInfo0, InstA, InstA2),
-	( InstA2 = constrained_inst_var(InstVar, InstA3) ->
+	( InstA2 = constrained_inst_vars(InstVar, InstA3) ->
 		abstractly_unify_inst_functor(Live, InstA3, ConsId, ArgInsts,
 			ArgLives, Real, ModuleInfo0, Inst0, Det, ModuleInfo),
 		(
-			\+ inst_matches_final(Inst0, InstA3, ModuleInfo)
+			inst_matches_final(Inst0, InstA3, ModuleInfo)
 		->
-			Inst = Inst0
+			% We can keep the constrained_inst_vars.
+			Inst = constrained_inst_vars(InstVar, Inst0)
 		;
-			Inst = constrained_inst_var(InstVar, Inst0)
+			% The inst has become too instantiated so we must remove
+			% the constrained_inst_var.
+			Inst = Inst0
 		)
 	;
 		abstractly_unify_inst_functor_2(Live, InstA2, ConsId, ArgInsts,
@@ -670,29 +673,30 @@
 
 %-----------------------------------------------------------------------------%
 
-:- 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.
+:- pred abstractly_unify_constrained_inst_vars(is_live, set(inst_var), inst,
+	inst, unify_is_real, module_info, inst, determinism, module_info).
+:- mode abstractly_unify_constrained_inst_vars(in, in, in, in, in, in, out,
+	out, out) is semidet.
 
-abstractly_unify_constrained_inst_var(IsLive, InstVar, InstConstraint, InstB,
+abstractly_unify_constrained_inst_vars(IsLive, InstVars, 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.
+		% constrained_inst_vars must be removed.
 		Inst = Inst0
 	;
-		% We can keep the constrained_inst_var.
-		Inst = constrained_inst_var(InstVar, Inst0)
+		Inst0 = constrained_inst_vars(InstVars0, Inst1)
+	->
+		% Avoid nested constrained_inst_vars.
+		Inst = constrained_inst_vars(set__union(InstVars0, InstVars),
+				Inst1)
+	;
+		% We can keep the constrained_inst_vars.
+		Inst = constrained_inst_vars(InstVars, Inst0)
 	).
 
 %-----------------------------------------------------------------------------%
@@ -1102,7 +1106,7 @@
 	make_shared(Uniq0, Uniq).
 make_shared_inst(inst_var(_), _, _, _) :-
 	error("free inst var").
-make_shared_inst(constrained_inst_var(InstVar, Inst0), ModuleInfo0, Inst,
+make_shared_inst(constrained_inst_vars(InstVar, Inst0), ModuleInfo0, Inst,
 		ModuleInfo) :-
 	make_shared_inst(Inst0, ModuleInfo0, Inst1, ModuleInfo),
 	(
@@ -1110,7 +1114,7 @@
 	->
 		Inst = Inst1
 	;
-		Inst = constrained_inst_var(InstVar, Inst1)
+		Inst = constrained_inst_vars(InstVar, Inst1)
 	).
 make_shared_inst(abstract_inst(_,_), M, _, M) :-
 	error("make_shared_inst(abstract_inst)").
@@ -1203,7 +1207,7 @@
 	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,
+make_mostly_uniq_inst(constrained_inst_vars(InstVar, Inst0), ModuleInfo0, Inst,
 		ModuleInfo) :-
 	make_mostly_uniq_inst(Inst0, ModuleInfo0, Inst1, ModuleInfo),
 	(
@@ -1211,7 +1215,7 @@
 	->
 		Inst = Inst1
 	;
-		Inst = constrained_inst_var(InstVar, Inst1)
+		Inst = constrained_inst_vars(InstVar, Inst1)
 	).
 make_mostly_uniq_inst(abstract_inst(_,_), M, _, M) :-
 	error("make_mostly_uniq_inst(abstract_inst)").
@@ -1384,20 +1388,20 @@
 :- 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
+	( InstA = constrained_inst_vars(InstVarsA, InstA1) ->
+		( InstB = constrained_inst_vars(InstVarsB, InstB1) ->
+			inst_merge(InstA1, InstB1, MaybeType,
+				ModuleInfo0, Inst0, ModuleInfo),
+			InstVars = InstVarsA `set__intersect` InstVarsB,
+			( set__non_empty(InstVars) ->
+				Inst = constrained_inst_vars(InstVars, Inst0)
+				% We can keep the constrained_inst_vars here
 				% since Inst0 = InstA1 `lub` InstB1 and the
-				% original constraint on InstVarA, InstC,
+				% original constraint on the InstVars, InstC,
 				% must have been such that
 				% InstA1 `lub` InstB1 =< InstC
 			;
-				inst_merge(InstA1, InstB1, MaybeType,
-					ModuleInfo0, Inst, ModuleInfo)
+				Inst = Inst0
 			)
 		;
 			inst_merge(InstA1, InstB, MaybeType, ModuleInfo0,
@@ -1595,7 +1599,7 @@
 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,
+merge_inst_uniq(constrained_inst_vars(_InstVar, Inst0), UniqB, ModuleInfo,
 		Expansions0, Expansions, Uniq) :-
 	merge_inst_uniq(Inst0, UniqB, ModuleInfo, Expansions0, Expansions,
 		Uniq).
diff -u compiler/mercury_to_mercury.m compiler/mercury_to_mercury.m
--- compiler/mercury_to_mercury.m	20 Feb 2002 04:58:22 -0000
+++ compiler/mercury_to_mercury.m	7 Mar 2002 00:25:25 -0000
@@ -1006,13 +1006,10 @@
 	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_structured_inst(constrained_inst_vars(Vars, 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_constrained_inst_vars(Vars, Inst, VarSet).
 mercury_format_structured_inst(abstract_inst(Name, Args), Indent, VarSet) -->
 	mercury_format_structured_inst_name(user_inst(Name, Args), Indent,
 		VarSet).
@@ -1088,10 +1085,8 @@
 	).
 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(constrained_inst_vars(Vars, Inst), VarSet) -->
+	mercury_format_constrained_inst_vars(Vars, 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) -->
@@ -1447,6 +1442,20 @@
 	add_string("<deep_profiling_proc_static>").
 mercury_format_cons_id(table_io_decl(_), _) -->
 	add_string("<table_io_decl>").
+
+:- pred mercury_format_constrained_inst_vars(set(inst_var)::in, (inst)::in,
+		inst_varset::in, U::di, U::uo) is det <= output(U).
+
+mercury_format_constrained_inst_vars(Vars0, Inst, VarSet) -->
+	( { set__remove_least(Vars0, Var, Vars1) } ->
+		add_string("("),
+		mercury_format_var(Var, VarSet, no),
+		add_string(" =< "),
+		mercury_format_constrained_inst_vars(Vars1, Inst, VarSet),
+		add_string(")")
+	;
+		mercury_format_inst(Inst, VarSet)
+	).
 
 :- pred mercury_format_mode_defn(inst_varset::in, sym_name::in,
 	list(inst_var)::in, mode_defn::in, prog_context::in,
diff -u compiler/mode_util.m compiler/mode_util.m
--- compiler/mode_util.m	18 Feb 2002 06:05:49 -0000
+++ compiler/mode_util.m	5 Mar 2002 03:59:48 -0000
@@ -414,7 +414,7 @@
 	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,
+get_single_arg_inst(constrained_inst_vars(_, Inst), ModuleInfo, ConsId,
 		ArgInst) :-
 	get_single_arg_inst(Inst, ModuleInfo, ConsId, ArgInst).
 	
@@ -718,8 +718,8 @@
 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(constrained_inst_vars(V, Inst0), Type, Constructors,
+		ModuleInfo, constrained_inst_vars(V, Inst)) :-
 	propagate_ctor_info(Inst0, Type, Constructors, ModuleInfo, Inst).
 propagate_ctor_info(abstract_inst(Name, Args), _, _, _,
 		abstract_inst(Name, Args)).	% XXX loses info
@@ -786,8 +786,8 @@
 	).
 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(constrained_inst_vars(V, Inst0), Type, Constructors,
+		ModuleInfo, constrained_inst_vars(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
@@ -1072,7 +1072,12 @@
 	;
 		Result = inst_var(Var)
 	).
-inst_apply_substitution(constrained_inst_var(Var, Inst0), Subst, Result) :-
+inst_apply_substitution(constrained_inst_vars(Vars, Inst0), Subst, Result) :-
+	( set__singleton_set(Vars, Var0) ->
+		Var = Var0
+	;
+		error("inst_apply_substitution: multiple inst_vars found")
+	),
 	(
 		map__search(Subst, Var, Replacement)
 	->
@@ -1080,7 +1085,8 @@
 		% XXX Should probably have a sanity check here that
 		% Replacement =< Inst0
 	;
-		Result = constrained_inst_var(Var, Inst0)
+		inst_apply_substitution(Inst0, Subst, Result0),
+		Result = constrained_inst_vars(Vars, Result0)
 	).
 inst_apply_substitution(defined_inst(InstName0), Subst,
 		    defined_inst(InstName)) :-
@@ -1183,20 +1189,21 @@
 		GI = none
 	).
 rename_apart_inst_vars_in_inst(_, not_reached, not_reached).
-rename_apart_inst_vars_in_inst(Sub, inst_var(V0), inst_var(V)) :-
-	( map__search(Sub, V0, term__variable(V1)) ->
-		V = V1
+rename_apart_inst_vars_in_inst(Sub, inst_var(Var0), inst_var(Var)) :-
+	( map__search(Sub, Var0, term__variable(Var1)) ->
+		Var = Var1
 	;
-		V = V0
+		Var = Var0
 	).
-rename_apart_inst_vars_in_inst(Sub, constrained_inst_var(V0, Inst0),
-		constrained_inst_var(V, Inst)) :-
+rename_apart_inst_vars_in_inst(Sub, constrained_inst_vars(Vars0, Inst0),
+		constrained_inst_vars(Vars, Inst)) :-
 	rename_apart_inst_vars_in_inst(Sub, Inst0, Inst),
-	( map__search(Sub, V0, term__variable(V1)) ->
-		V = V1
-	;
-		V = V0
-	).
+	Vars = set__map(func(Var0) =
+		( map__search(Sub, Var0, term__variable(Var)) ->
+			Var
+		;
+			Var0
+		), Vars0).
 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
@@ -1712,8 +1719,8 @@
 	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(constrained_inst_vars(Vars, Inst0),
+		constrained_inst_vars(Vars, Inst)) :-
 	strip_builtin_qualifiers_from_inst(Inst0, Inst).
 strip_builtin_qualifiers_from_inst(not_reached, not_reached).
 strip_builtin_qualifiers_from_inst(free, free).
diff -u compiler/modecheck_unify.m compiler/modecheck_unify.m
--- compiler/modecheck_unify.m	20 Feb 2002 05:31:58 -0000
+++ compiler/modecheck_unify.m	5 Mar 2002 03:30:25 -0000
@@ -1194,7 +1194,7 @@
 		{ List = [functor(_, InstList)] },
 		bind_args_2(Args, InstList)
 	).
-bind_args(constrained_inst_var(_, Inst), Args) -->
+bind_args(constrained_inst_vars(_, Inst), Args) -->
 	bind_args(Inst, Args).
 
 :- pred bind_args_2(list(prog_var), list(inst), mode_info, mode_info).
@@ -1238,7 +1238,7 @@
 		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(constrained_inst_vars(_, Inst), ArgInsts, ArgModes) :-
 	get_mode_of_args(Inst, ArgInsts, ArgModes).
 
 :- pred get_mode_of_args_2(list(inst), list(inst), list(mode)).
diff -u compiler/module_qual.m compiler/module_qual.m
--- compiler/module_qual.m	18 Feb 2002 00:48:24 -0000
+++ compiler/module_qual.m	5 Mar 2002 03:55:33 -0000
@@ -760,8 +760,8 @@
 		{ 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(constrained_inst_vars(Vars, Inst0),
+		constrained_inst_vars(Vars, 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).
diff -u compiler/pd_util.m compiler/pd_util.m
--- compiler/pd_util.m	8 Feb 2002 00:32:18 -0000
+++ compiler/pd_util.m	5 Mar 2002 03:30:51 -0000
@@ -918,7 +918,7 @@
 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,
+pd_util__inst_size_2(ModuleInfo, constrained_inst_vars(_, Inst), Expansions,
 		Size) :-
 	pd_util__inst_size_2(ModuleInfo, Inst, Expansions, Size).
 pd_util__inst_size_2(_, abstract_inst(_, _), _, 0).
diff -u compiler/prog_io.m compiler/prog_io.m
--- compiler/prog_io.m	20 Feb 2002 05:41:11 -0000
+++ compiler/prog_io.m	6 Mar 2002 22:16:12 -0000
@@ -55,7 +55,7 @@
 
 :- interface.
 
-:- import_module prog_data, prog_io_util, timestamp.
+:- import_module prog_data, prog_io_util, timestamp, (inst).
 :- import_module bool, varset, term, list, io, std_util. 
 
 %-----------------------------------------------------------------------------%
@@ -194,6 +194,12 @@
 :- pred constrain_inst_vars_in_mode(mode, mode).
 :- mode constrain_inst_vars_in_mode(in, out) is det.
 
+	% Replace all occurrences of inst_var(I) with
+	% constrained_inst_var(I, Inst) where I -> Inst is in the inst_var_sub.
+	% If I is not in the inst_var_sub, default to ground(shared, none).
+:- pred constrain_inst_vars_in_mode(inst_var_sub, mode, mode).
+:- mode constrain_inst_vars_in_mode(in, in, out) is det.
+
 %-----------------------------------------------------------------------------%
 
 	% Check that for each constrained_inst_var all occurrences have the
@@ -209,11 +215,11 @@
 :- import_module prog_io_goal, prog_io_dcg, prog_io_pragma, prog_io_util.
 :- import_module prog_io_typeclass.
 :- import_module hlds_data, hlds_pred, prog_util, prog_out.
-:- import_module globals, options, (inst).
+:- import_module globals, options.
 :- import_module recompilation, recompilation_version.
 
 :- import_module int, string, std_util, parser, term_io, dir, require.
-:- import_module assoc_list, map, time.
+:- import_module assoc_list, map, time, set.
 
 %-----------------------------------------------------------------------------%
 
@@ -940,8 +946,7 @@
 	parse_type_decl_func(ModuleName, VarSet, FuncDecl, Attributes, Result).
 
 process_decl(ModuleName, VarSet, "mode", [ModeDecl], Attributes, Result) :-
-	parse_mode_decl(ModuleName, VarSet, ModeDecl, Result0),
-	check_no_attributes(Result0, Attributes, Result).
+	parse_mode_decl(ModuleName, VarSet, ModeDecl, Attributes, Result).
 
 process_decl(ModuleName, VarSet, "inst", [InstDecl], Attributes, Result) :-
 	parse_inst_decl(ModuleName, VarSet, InstDecl, Result0),
@@ -1410,14 +1415,15 @@
 	% if Pred is a predicate mode declaration, and binds Condition
 	% to the condition for that declaration (if any), and Result to
 	% a representation of the declaration.
-:- pred parse_mode_decl_pred(module_name, varset, term, maybe1(item)).
-:- mode parse_mode_decl_pred(in, in, in, out) is det.
+:- pred parse_mode_decl_pred(module_name, varset, term, decl_attrs,
+		maybe1(item)).
+:- mode parse_mode_decl_pred(in, in, in, in, out) is det.
 
-parse_mode_decl_pred(ModuleName, VarSet, Pred, Result) :-
+parse_mode_decl_pred(ModuleName, VarSet, Pred, Attributes, Result) :-
 	get_condition(Pred, Body, Condition),
 	get_determinism(Body, Body2, MaybeDeterminism),
-	process_maybe1_to_t(process_mode(ModuleName, VarSet, Body2, Condition),
-			MaybeDeterminism, Result).
+	process_maybe1_to_t(process_mode(ModuleName, VarSet, Body2, Condition,
+			Attributes), MaybeDeterminism, Result).
 
 %-----------------------------------------------------------------------------%
 
@@ -1815,27 +1821,28 @@
 
 process_pred(ModuleName, VarSet, PredType, Cond, MaybeDet, Attributes0,
 		Result) :-
-	get_class_context(ModuleName, Attributes0, Attributes, MaybeContext),
+	get_class_context_and_inst_constraints(ModuleName, Attributes0,
+		Attributes, MaybeContext),
 	(
-		MaybeContext = ok(ExistQVars, Constraints),
+		MaybeContext = ok(ExistQVars, Constraints, InstConstraints),
 		parse_implicitly_qualified_term(ModuleName,
 			PredType, PredType, "`:- pred' declaration",
 			R),
-		process_pred_2(R, PredType, VarSet, MaybeDet, Cond,
-			ExistQVars, Constraints, Attributes, Result)
+		process_pred_2(R, PredType, VarSet, MaybeDet, Cond, ExistQVars,
+			Constraints, InstConstraints, Attributes, Result)
 	;
 		MaybeContext = error(String, Term),
 		Result = error(String, Term)
 	).
 
 :- pred process_pred_2(maybe_functor, term, varset, maybe(determinism),
-			condition, existq_tvars, class_constraints, decl_attrs,
-			maybe1(item)).
-:- mode process_pred_2(in, in, in, in, in, in, in, in, out) is det.
+			condition, existq_tvars, class_constraints,
+			inst_var_sub, decl_attrs, maybe1(item)).
+:- mode process_pred_2(in, in, in, in, in, in, in, in, in, out) is det.
 
 process_pred_2(ok(F, As0), PredType, VarSet0, MaybeDet, Cond, ExistQVars,
-		ClassContext, Attributes0, Result) :-
-	( convert_type_and_mode_list(As0, As) ->
+		ClassContext, InstConstraints, Attributes0, Result) :-
+	( convert_type_and_mode_list(InstConstraints, As0, As) ->
 	    ( verify_type_and_mode_list(As) ->
 		get_purity(Attributes0, Purity, Attributes),
 		varset__coerce(VarSet0, TVarSet),
@@ -1860,7 +1867,7 @@
 	    Result = error("syntax error in `:- pred' declaration",
 				PredType)
 	).
-process_pred_2(error(M, T), _, _, _, _, _, _, _, error(M, T)).
+process_pred_2(error(M, T), _, _, _, _, _, _, _, _, error(M, T)).
 
 :- pred get_purity(decl_attrs, purity, decl_attrs).
 :- mode get_purity(in, out, out) is det.
@@ -1879,18 +1886,23 @@
 	% We could perhaps get rid of some code duplication between here and
 	% prog_io_typeclass.m?
 
-	% get_class_context(ModuleName, Attributes0, Attributes, MaybeContext):
-	% Parse type quantifiers and type class constraints from the
-	% declaration attributes in Attributes0.
+	% get_class_context_and_inst_constraints(ModuleName, Attributes0,
+	%	Attributes, MaybeContext, MaybeInstConstraints):
+	% Parse type quantifiers, type class constraints and inst constraints
+	% from the declaration attributes in Attributes0.
 	% MaybeContext is either bound to the correctly parsed context, or
 	% an appropriate error message (if there was a syntax error).
+	% MaybeInstConstraints is either bound to a map containing the inst
+	% constraints or an appropriate error message (if there was a syntax
+	% error).
 	% Attributes is bound to the remaining attributes.
 
-:- pred get_class_context(module_name, decl_attrs, decl_attrs,
-			maybe2(existq_tvars, class_constraints)).
-:- mode get_class_context(in, in, out, out) is det.
+:- pred get_class_context_and_inst_constraints(module_name, decl_attrs,
+	decl_attrs, maybe3(existq_tvars, class_constraints, inst_var_sub)).
+:- mode get_class_context_and_inst_constraints(in, in, out, out) is det.
 
-get_class_context(ModuleName, RevAttributes0, RevAttributes, MaybeContext) :-
+get_class_context_and_inst_constraints(ModuleName, RevAttributes0,
+		RevAttributes, MaybeContext) :-
 	%
 	% constraints and quantifiers should occur in the following
 	% order (outermost to innermost):
@@ -1940,16 +1952,17 @@
 	combine_quantifier_results(MaybeUnivConstraints, MaybeExistConstraints,
 			ExistQVars, MaybeContext).
 
-:- pred combine_quantifier_results(maybe1(list(class_constraint)),
-		maybe1(list(class_constraint)), existq_tvars,
-		maybe2(existq_tvars, class_constraints)).
+:- pred combine_quantifier_results(maybe_class_and_inst_constraints,
+		maybe_class_and_inst_constraints, existq_tvars,
+		maybe3(existq_tvars, class_constraints, inst_var_sub)).
 :- mode combine_quantifier_results(in, in, in, out) is det.
 
 combine_quantifier_results(error(Msg, Term), _, _, error(Msg, Term)).
-combine_quantifier_results(ok(_), error(Msg, Term), _, error(Msg, Term)).
-combine_quantifier_results(
-	ok(UnivConstraints), ok(ExistConstraints), ExistQVars,
-	ok(ExistQVars, constraints(UnivConstraints, ExistConstraints))).
+combine_quantifier_results(ok(_, _), error(Msg, Term), _, error(Msg, Term)).
+combine_quantifier_results(ok(UnivConstraints, InstConstraints0),
+	ok(ExistConstraints, InstConstraints1), ExistQVars,
+	ok(ExistQVars, constraints(UnivConstraints, ExistConstraints),
+		InstConstraints0 `map__merge` InstConstraints1)).
 
 :- pred get_quant_vars(quantifier_type, module_name, decl_attrs, list(var),
 		decl_attrs, list(var)).
@@ -1969,7 +1982,7 @@
 	).
 
 :- pred get_constraints(quantifier_type, module_name, decl_attrs, decl_attrs, 
-			maybe1(list(class_constraint))).
+			maybe_class_and_inst_constraints).
 :- mode get_constraints(in, in, in, out, out) is det.
 
 get_constraints(QuantType, ModuleName, Attributes0, Attributes,
@@ -1978,7 +1991,7 @@
 		Attributes0 = [constraints(QuantType, ConstraintsTerm) - _Term
 				| Attributes1]
 	->
-		parse_class_constraints(ModuleName, ConstraintsTerm,
+		parse_class_and_inst_constraints(ModuleName, ConstraintsTerm,
 			MaybeConstraints0),
 		% there may be more constraints of the same type --
 		% collect them all and combine them
@@ -1988,18 +2001,17 @@
 			MaybeConstraints0, MaybeConstraints)
 	;
 		Attributes = Attributes0,
-		MaybeConstraints = ok([])
+		MaybeConstraints = ok([], map__init)
 	).
 
-:- pred combine_constraint_list_results(maybe1(list(class_constraint)),
-	maybe1(list(class_constraint)), maybe1(list(class_constraint))).
+:- pred combine_constraint_list_results(maybe_class_and_inst_constraints,
+	maybe_class_and_inst_constraints, maybe_class_and_inst_constraints).
 :- mode combine_constraint_list_results(in, in, out) is det.
 
 combine_constraint_list_results(error(Msg, Term), _, error(Msg, Term)).
-combine_constraint_list_results(ok(_), error(Msg, Term), error(Msg, Term)).
-combine_constraint_list_results(ok(Constraints0), ok(Constraints1),
-		ok(Constraints)) :-
-	list__append(Constraints0, Constraints1, Constraints).
+combine_constraint_list_results(ok(_, _), error(Msg, Term), error(Msg, Term)).
+combine_constraint_list_results(ok(CC0, IC0), ok(CC1, IC1),
+		ok(CC0 ++ CC1, IC0 `map__merge` IC1)).
 
 :- pred get_existential_constraints_from_term(module_name, term, term,
 			maybe1(list(class_constraint))).
@@ -2054,24 +2066,25 @@
 :- mode process_func(in, in, in, in, in, in, out) is det.
 
 process_func(ModuleName, VarSet, Term, Cond, Attributes0, MaybeDet, Result) :-
-	get_class_context(ModuleName, Attributes0, Attributes, MaybeContext),
+	get_class_context_and_inst_constraints(ModuleName, Attributes0,
+		Attributes, MaybeContext),
 	(
-		MaybeContext = ok(ExistQVars, Constraints),
+		MaybeContext = ok(ExistQVars, Constraints, InstConstraints),
 		process_func_2(ModuleName, VarSet, Term,
-			Cond, MaybeDet, ExistQVars, Constraints, Attributes,
-			Result) 
+			Cond, MaybeDet, ExistQVars, Constraints,
+			InstConstraints, Attributes, Result) 
 	;
 		MaybeContext = error(String, ErrorTerm),
 		Result = error(String, ErrorTerm)
 	).
 
 :- pred process_func_2(module_name, varset, term, condition,
-	maybe(determinism), existq_tvars, class_constraints, decl_attrs,
-	maybe1(item)).
-:- mode process_func_2(in, in, in, in, in, in, in, in, out) is det.
+	maybe(determinism), existq_tvars, class_constraints, inst_var_sub,
+	decl_attrs, maybe1(item)).
+:- mode process_func_2(in, in, in, in, in, in, in, in, in, out) is det.
 
 process_func_2(ModuleName, VarSet, Term, Cond, MaybeDet, 
-		ExistQVars, Constraints, Attributes, Result) :-
+		ExistQVars, Constraints, InstConstraints, Attributes, Result) :-
 	(
 		Term = term__functor(term__atom("="),
 				[FuncTerm, ReturnTypeTerm], _Context)
@@ -2079,8 +2092,8 @@
 		parse_implicitly_qualified_term(ModuleName, FuncTerm, Term,
 			"`:- func' declaration", R),
 		process_func_3(R, FuncTerm, ReturnTypeTerm, Term, VarSet,
-			MaybeDet, Cond, ExistQVars, Constraints, Attributes,
-			Result)
+			MaybeDet, Cond, ExistQVars, Constraints,
+			InstConstraints, Attributes, Result)
 	;
 		Result = error("`=' expected in `:- func' declaration", Term)
 	).
@@ -2088,17 +2101,22 @@
 
 :- 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.
+	inst_var_sub, decl_attrs, maybe1(item)).
+:- mode process_func_3(in, 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) ->
+		MaybeDet, Cond, ExistQVars, ClassContext, InstConstraints,
+		Attributes0, Result) :-
+	( convert_type_and_mode_list(InstConstraints, As0, As) ->
+	    (
+		\+ verify_type_and_mode_list(As)
+	    ->
 		Result = error("some but not all arguments have modes",
 		    FuncTerm)
-	    ; convert_type_and_mode(ReturnTypeTerm, ReturnType) ->
+	    ;
+		convert_type_and_mode(InstConstraints, ReturnTypeTerm,
+		    ReturnType)
+	    ->
 		(
 		    As = [type_and_mode(_, _) | _],
 		    ReturnType = type_only(_)
@@ -2142,138 +2160,183 @@
 	    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)).
 
 %-----------------------------------------------------------------------------%
 
 	% parse a `:- mode p(...)' declaration
 
-:- pred process_mode(module_name, varset, term, condition, maybe(determinism),
-		maybe1(item)).
-:- mode process_mode(in, in, in, in, in, out) is det.
+:- pred process_mode(module_name, varset, term, condition, decl_attrs,
+		maybe(determinism), maybe1(item)).
+:- mode process_mode(in, in, in, in, in, in, out) is det.
 
-process_mode(ModuleName, VarSet, Term, Cond, MaybeDet, Result) :-
+process_mode(ModuleName, VarSet, Term, Cond, Attributes, MaybeDet, Result) :-
 	(
 		Term = term__functor(term__atom("="),
 				[FuncTerm, ReturnTypeTerm], _Context)
 	->
 		parse_implicitly_qualified_term(ModuleName, FuncTerm, Term,
 				"function `:- mode' declaration", R),
-		process_func_mode(R, FuncTerm, ReturnTypeTerm, Term, VarSet,
-			MaybeDet, Cond, Result)
+		process_func_mode(R, ModuleName, FuncTerm, ReturnTypeTerm,
+		    Term, VarSet, MaybeDet, Cond, Attributes, Result)
 	;
 		parse_implicitly_qualified_term(ModuleName, Term, Term,
 				"predicate `:- mode' declaration", R),
-		process_pred_mode(R, Term, VarSet, MaybeDet, Cond, Result)
+		process_pred_mode(R, ModuleName, Term, VarSet, MaybeDet, Cond,
+		    Attributes, Result)
 	).
 
-:- pred process_pred_mode(maybe_functor, term, varset, maybe(determinism),
-			condition, maybe1(item)).
-:- mode process_pred_mode(in, in, in, in, in, out) is det.
+:- pred process_pred_mode(maybe_functor, module_name, term, varset,
+		maybe(determinism), condition, decl_attrs, maybe1(item)).
+:- mode process_pred_mode(in, in, in, in, in, in, in, out) is det.
 
-process_pred_mode(ok(F, As0), PredMode, VarSet0, MaybeDet, Cond, Result) :-
+process_pred_mode(ok(F, As0), ModuleName, PredMode, VarSet0, MaybeDet, Cond,
+		Attributes0, Result) :-
 	(
-		convert_mode_list(allow_constrained_inst_var, As0, As1)
+	    convert_mode_list(allow_constrained_inst_var, As0, As1)
 	->
-		list__map(constrain_inst_vars_in_mode, As1, As),
+	    get_class_context_and_inst_constraints(ModuleName, Attributes0,
+		Attributes, MaybeConstraints),
+	    (
+		MaybeConstraints = ok(_, _, InstConstraints),
+		list__map(constrain_inst_vars_in_mode(InstConstraints),
+			As1, As),
 		varset__coerce(VarSet0, VarSet),
 		( inst_var_constraints_are_consistent_in_modes(As) ->
-			Result = ok(pred_or_func_mode(VarSet, predicate, F, As,
-				MaybeDet, Cond))
+		    Result0 = ok(pred_or_func_mode(VarSet, predicate, F, As,
+				    MaybeDet, Cond))
 		;
-			Result = error(
-    "inconsistent constraints on inst variables in predicate mode declaration",
-				PredMode)
+		    Result0 = error("inconsistent constraints on inst variables in predicate mode declaration",
+			PredMode)
 		)
+	    ;
+		MaybeConstraints = error(String, Term),
+		Result0 = error(String, Term)
+	    ),
+	    check_no_attributes(Result0, Attributes, Result)
 	;
 		Result = error("syntax error in predicate mode declaration",
 				PredMode)
 	).
-process_pred_mode(error(M, T), _, _, _, _, error(M, T)).
+process_pred_mode(error(M, T), _, _, _, _, _, _, error(M, T)).
 
-:- 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.
+:- pred process_func_mode(maybe_functor, module_name, term, term, term, varset,
+		maybe(determinism), condition, decl_attrs, maybe1(item)).
+:- mode process_func_mode(in, in, in, in, in, in, in, in, in, out) is det.
 
-process_func_mode(ok(F, As0), FuncMode, RetMode0, FullTerm, VarSet0, MaybeDet,
-		Cond, Result) :-
+process_func_mode(ok(F, As0), ModuleName, FuncMode, RetMode0, FullTerm,
+		VarSet0, MaybeDet, Cond, Attributes0, Result) :-
 	(
 	    convert_mode_list(allow_constrained_inst_var, As0, As1)
 	->
-	    list__map(constrain_inst_vars_in_mode, As1, As),
+	    get_class_context_and_inst_constraints(ModuleName, Attributes0,
+		Attributes, MaybeConstraints),
 	    (
-		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))
+		MaybeConstraints = ok(_, _, InstConstraints),
+		list__map(constrain_inst_vars_in_mode(InstConstraints),
+		    As1, As),
+		(
+		    convert_mode(allow_constrained_inst_var, RetMode0, RetMode1)
+		->
+		    constrain_inst_vars_in_mode(InstConstraints, RetMode1,
+			RetMode),
+		    varset__coerce(VarSet0, VarSet),
+		    list__append(As, [RetMode], ArgModes),
+		    ( inst_var_constraints_are_consistent_in_modes(ArgModes) ->
+			Result0 = ok(pred_or_func_mode(VarSet, function,
+			    F, ArgModes, MaybeDet, Cond))
+		    ;
+			Result0 = error(
+	"inconsistent constraints on inst variables in function mode declaration",
+			    FullTerm)
+		    )
 		;
-		    Result = error(
-    "inconsistent constraints on inst variables in function mode declaration",
-			FullTerm)
+		    Result0 = error(
+		    "syntax error in return mode of function mode declaration",
+			RetMode0)
 		)
 	    ;
-		Result = error(
-		    "syntax error in return mode of function mode declaration",
-		    RetMode0)
-	    )
+		MaybeConstraints = error(String, Term),
+		Result0 = error(String, Term)
+	    ),
+	    check_no_attributes(Result0, Attributes, Result)
 	;
 	    Result = error(
 		"syntax error in arguments of function mode declaration",
 		FuncMode)
 	).
-process_func_mode(error(M, T), _, _, _, _, _, _, error(M, T)).
+process_func_mode(error(M, T), _, _, _, _, _, _, _, _, error(M, T)).
 
 %-----------------------------------------------------------------------------%
 
-constrain_inst_vars_in_mode(I0 -> F0, I -> F) :-
-	constrain_inst_vars_in_inst(I0, I),
-	constrain_inst_vars_in_inst(F0, F).
-constrain_inst_vars_in_mode(user_defined_mode(Name, Args0),
+constrain_inst_vars_in_mode(Mode0, Mode) :-
+	constrain_inst_vars_in_mode(map__init, Mode0, Mode).
+
+constrain_inst_vars_in_mode(InstConstraints, I0 -> F0, I -> F) :-
+	constrain_inst_vars_in_inst(InstConstraints, I0, I),
+	constrain_inst_vars_in_inst(InstConstraints, F0, F).
+constrain_inst_vars_in_mode(InstConstraints, user_defined_mode(Name, Args0),
 		user_defined_mode(Name, Args)) :-
-	list__map(constrain_inst_vars_in_inst, Args0, Args).
+	list__map(constrain_inst_vars_in_inst(InstConstraints), Args0, Args).
 
-:- pred constrain_inst_vars_in_inst(inst, inst).
-:- mode constrain_inst_vars_in_inst(in, out) is det.
+:- pred constrain_inst_vars_in_inst(inst_var_sub, inst, inst).
+:- mode constrain_inst_vars_in_inst(in, in, out) is det.
 
-constrain_inst_vars_in_inst(any(U), any(U)).
-constrain_inst_vars_in_inst(free, free).
-constrain_inst_vars_in_inst(free(T), free(T)).
-constrain_inst_vars_in_inst(bound(U, BIs0), bound(U, BIs)) :-
+constrain_inst_vars_in_inst(_, any(U), any(U)).
+constrain_inst_vars_in_inst(_, free, free).
+constrain_inst_vars_in_inst(_, free(T), free(T)).
+constrain_inst_vars_in_inst(InstConstraints, bound(U, BIs0), bound(U, BIs)) :-
 	list__map((pred(functor(C, Is0)::in, functor(C, Is)::out) is det :-
-		list__map(constrain_inst_vars_in_inst, Is0, Is)), BIs0, BIs).
-constrain_inst_vars_in_inst(ground(U, none), ground(U, none)).
-constrain_inst_vars_in_inst(ground(U, higher_order(PredInstInfo0)),
+	    list__map(constrain_inst_vars_in_inst(InstConstraints), Is0, Is)),
+	    BIs0, BIs).
+constrain_inst_vars_in_inst(_, ground(U, none), ground(U, none)).
+constrain_inst_vars_in_inst(InstConstraints,
+		ground(U, higher_order(PredInstInfo0)),
 		ground(U, higher_order(PredInstInfo))) :-
-	constrain_inst_vars_in_pred_inst_info(PredInstInfo0, PredInstInfo).
-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),
-		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)) :-
-	list__map(constrain_inst_vars_in_inst, Is0, Is).
-
-:- pred constrain_inst_vars_in_pred_inst_info(pred_inst_info, pred_inst_info).
-:- mode constrain_inst_vars_in_pred_inst_info(in, out) is det.
+	constrain_inst_vars_in_pred_inst_info(InstConstraints, PredInstInfo0,
+		PredInstInfo).
+constrain_inst_vars_in_inst(InstConstraints,
+		constrained_inst_vars(Vars0, Inst0),
+		constrained_inst_vars(Vars, Inst)) :-
+	constrain_inst_vars_in_inst(InstConstraints, Inst0, Inst1),
+	( Inst1 = constrained_inst_vars(Vars2, Inst2) ->
+		Vars = Vars0 `set__union` Vars2,
+		Inst = Inst2
+	;
+		Vars = Vars0,
+		Inst = Inst1
+	).
+constrain_inst_vars_in_inst(_, not_reached, not_reached).
+constrain_inst_vars_in_inst(InstConstraints, inst_var(Var),
+		constrained_inst_vars(set__make_singleton_set(Var), Inst)) :-
+	Inst = ( map__search(InstConstraints, Var, Inst0) -> 
+	    	Inst0
+	;
+		ground(shared, none)
+	).
+constrain_inst_vars_in_inst(InstConstraints, defined_inst(Name0),
+		defined_inst(Name)) :-
+	constrain_inst_vars_in_inst_name(InstConstraints, Name0, Name).
+constrain_inst_vars_in_inst(InstConstraints, abstract_inst(N, Is0),
+		abstract_inst(N, Is)) :-
+	list__map(constrain_inst_vars_in_inst(InstConstraints), Is0, Is).
+
+:- pred constrain_inst_vars_in_pred_inst_info(inst_var_sub, pred_inst_info,
+		pred_inst_info).
+:- mode constrain_inst_vars_in_pred_inst_info(in, in, out) is det.
 
-constrain_inst_vars_in_pred_inst_info(PII0, PII) :-
+constrain_inst_vars_in_pred_inst_info(InstConstraints, PII0, PII) :-
 	PII0 = pred_inst_info(PredOrFunc, Modes0, Det),
-	list__map(constrain_inst_vars_in_mode, Modes0, Modes),
+	list__map(constrain_inst_vars_in_mode(InstConstraints), Modes0, Modes),
 	PII = pred_inst_info(PredOrFunc, Modes, Det).
 
-:- pred constrain_inst_vars_in_inst_name(inst_name, inst_name).
-:- mode constrain_inst_vars_in_inst_name(in, out) is det.
+:- pred constrain_inst_vars_in_inst_name(inst_var_sub, inst_name, inst_name).
+:- mode constrain_inst_vars_in_inst_name(in, in, out) is det.
 
-constrain_inst_vars_in_inst_name(Name0, Name) :-
+constrain_inst_vars_in_inst_name(InstConstraints, Name0, Name) :-
 	( Name0 = user_inst(SymName, Args0) ->
-		list__map(constrain_inst_vars_in_inst, Args0, Args),
+		list__map(constrain_inst_vars_in_inst(InstConstraints),
+			Args0, Args),
 		Name = user_inst(SymName, Args)
 	;
 		Name = Name0
@@ -2346,14 +2409,16 @@
 	).
 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(
+		constrained_inst_vars(InstVars, Inst)) -->
+	set__fold((pred(InstVar::in, in, out) is semidet -->
+		( Inst0 =^ map__elem(InstVar) ->
+			% Check that the inst_var constraint is consistent with
+			% the previous constraint on this inst_var.
+			{ Inst = Inst0 }
+		;
+			^ map__elem(InstVar) := Inst
+		)), InstVars),
 	inst_var_constraints_are_consistent_in_inst(Inst).
 
 %-----------------------------------------------------------------------------%
@@ -2517,9 +2582,10 @@
 
 	% parse a `:- mode foo :: ...' or `:- mode foo = ...' definition.
 
-:- pred parse_mode_decl(module_name, varset, term, maybe1(item)).
-:- mode parse_mode_decl(in, in, in, out) is det.
-parse_mode_decl(ModuleName, VarSet, ModeDefn, Result) :-
+:- pred parse_mode_decl(module_name, varset, term, decl_attrs, maybe1(item)).
+:- mode parse_mode_decl(in, in, in, in, out) is det.
+
+parse_mode_decl(ModuleName, VarSet, ModeDefn, Attributes, Result) :-
 	( %%% some [H, B]
 		mode_op(ModeDefn, H, B)
 	->
@@ -2527,7 +2593,8 @@
 		convert_mode_defn(ModuleName, H, Body, R),
 		process_maybe1(make_mode_defn(VarSet, Condition), R, Result)
 	;
-		parse_mode_decl_pred(ModuleName, VarSet, ModeDefn, Result)
+		parse_mode_decl_pred(ModuleName, VarSet, ModeDefn, Attributes,
+			Result)
 	).
 
 	% People never seemed to remember what the right operator to use
@@ -2618,23 +2685,24 @@
 		Result = error("mode parameters must be variables", Head)
 	).
 
-:- pred convert_type_and_mode_list(list(term), list(type_and_mode)).
-:- mode convert_type_and_mode_list(in, out) is semidet.
-convert_type_and_mode_list([], []).
-convert_type_and_mode_list([H0|T0], [H|T]) :-
-	convert_type_and_mode(H0, H),
-	convert_type_and_mode_list(T0, T).
-
-:- pred convert_type_and_mode(term, type_and_mode).
-:- mode convert_type_and_mode(in, out) is semidet.
-convert_type_and_mode(Term, Result) :-
+:- pred convert_type_and_mode_list(inst_var_sub, list(term),
+		list(type_and_mode)).
+:- mode convert_type_and_mode_list(in, in, out) is semidet.
+convert_type_and_mode_list(_, [], []).
+convert_type_and_mode_list(InstConstraints, [H0|T0], [H|T]) :-
+	convert_type_and_mode(InstConstraints, H0, H),
+	convert_type_and_mode_list(InstConstraints, T0, T).
+
+:- pred convert_type_and_mode(inst_var_sub, term, type_and_mode).
+:- mode convert_type_and_mode(in, in, out) is semidet.
+convert_type_and_mode(InstConstraints, Term, Result) :-
 	(
 		Term = term__functor(term__atom("::"), [TypeTerm, ModeTerm],
 				_Context)
 	->
 		convert_type(TypeTerm, Type),
 		convert_mode(allow_constrained_inst_var, ModeTerm, Mode0),
-		constrain_inst_vars_in_mode(Mode0, Mode),
+		constrain_inst_vars_in_mode(InstConstraints, Mode0, Mode),
 		Result = type_and_mode(Type, Mode)
 	;
 		convert_type(Term, Type),
diff -u compiler/prog_io_util.m compiler/prog_io_util.m
--- compiler/prog_io_util.m	12 Feb 2002 04:10:39 -0000
+++ compiler/prog_io_util.m	6 Mar 2002 01:05:16 -0000
@@ -31,6 +31,10 @@
 :- type maybe2(T1, T2)	--->	error(string, term)
 			;	ok(T1, T2).
 
+:- type maybe3(T1, T2, T3)
+	--->	error(string, term)
+	;	ok(T1, T2, T3).
+
 :- type maybe1(T)	== 	maybe1(T, generic).
 :- type maybe1(T, U)	--->	error(string, term(U))
 			;	ok(T).
@@ -164,7 +168,7 @@
 % that is used in insts.
 :- import_module hlds_data.
 
-:- import_module bool, string, std_util, term.
+:- import_module bool, string, std_util, term, set.
 
 add_context(error(M, T), _, error(M, T)).
 add_context(ok(Item), Context, ok(Item, Context)).
@@ -436,9 +440,10 @@
 	; 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)
-
+		% Do not allow nested constrained_inst_vars.
+		convert_inst(no_allow_constrained_inst_var, InstTerm, Inst),
+		Result = constrained_inst_vars(set__make_singleton_set(
+				term__coerce_var(Var)), Inst)
 	% anything else must be a user-defined inst
 	;
 		parse_qualified_term(Term, Term, "inst",
diff -u compiler/recompilation_usage.m compiler/recompilation_usage.m
--- compiler/recompilation_usage.m	18 Feb 2002 06:10:51 -0000
+++ compiler/recompilation_usage.m	5 Mar 2002 03:31:57 -0000
@@ -1281,7 +1281,7 @@
 	).
 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(constrained_inst_vars(_, 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).
diff -u doc/reference_manual.texi doc/reference_manual.texi
--- doc/reference_manual.texi	20 Feb 2002 04:12:07 -0000
+++ doc/reference_manual.texi	6 Mar 2002 22:38:51 -0000
@@ -2147,7 +2147,8 @@
 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}},
+In a predicate or function mode declaration,
+an inst of the form @samp{@var{InstParam} =< @var{Inst}},
 where @var{InstParam} is a variable and @var{Inst} is an inst,
 states that 
 @var{InstParam} is constrained to be @emph{compatible} with @var{Inst},
@@ -2180,12 +2181,22 @@
 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.
+To avoid having to repeat a constraint everywhere that an inst parameter occurs,
+it is possible to list the constraints after the rest of the mode declaration,
+following a @samp{<=}.
 E.g. the above example could have been written as
 @example
+	:- mode append(in(list_skel(I)), in(list_skel(I)), out(list_skel(I)))
+	              <= I =< ground.
+ at end example
+
+Also, if the constraint on an inst parameter is @samp{ground} then it
+is not necessary to give the constraint in the declaration.
+The example can be further shorted to
+ at example
 	:- mode append(in(list_skel(I)), in(list_skel(I)), out(list_skel(I))).
 @end example
+
 
 Constrained polymorphic modes are particularly useful when passing
 objects with higher-order types to polymorphic predicates
diff -u tests/valid/constrained_poly_insts.m tests/valid/constrained_poly_insts.m
--- tests/valid/constrained_poly_insts.m	21 Feb 2002 05:00:58 -0000
+++ tests/valid/constrained_poly_insts.m	6 Mar 2002 23:09:17 -0000
@@ -15,7 +15,7 @@
 
 :- inst b == bound(42 ; 43 ; 44).
 
-:- pred p(int::in(I =< b), int::out(I =< b)) is semidet.
+:- pred p(int::in(I), int::out(I)) is semidet <= I =< b.
 
 :- implementation.
 
only in patch2:
--- compiler/prog_io_typeclass.m	25 Sep 2001 09:36:54 -0000	1.21
+++ compiler/prog_io_typeclass.m	6 Mar 2002 06:24:10 -0000
@@ -14,7 +14,7 @@
 
 :- interface.
 
-:- import_module prog_data, prog_io_util.
+:- import_module prog_data, prog_io_util, (inst).
 :- import_module list, varset, term.
 
 	% parse a typeclass declaration. 
@@ -30,11 +30,19 @@
 		maybe1(list(class_constraint))).
 :- mode parse_class_constraints(in, in, out) is det.
 
+	% parse a list of class and inst constraints
+:- pred parse_class_and_inst_constraints(module_name, term,
+		maybe_class_and_inst_constraints).
+:- mode parse_class_and_inst_constraints(in, in, out) is det.
+
+:- type maybe_class_and_inst_constraints ==
+		maybe2(list(class_constraint), inst_var_sub).
+
 :- implementation.
 
 :- import_module prog_io, prog_io_goal, prog_util, hlds_pred.
 :- import_module term, varset.
-:- import_module int, string, std_util, require, type_util, set.
+:- import_module int, string, std_util, require, type_util, set, map.
 
 parse_typeclass(ModuleName, VarSet, TypeClassTerm, Result) :-
 		%XXX should return an error if we get more than one arg,
@@ -259,8 +267,12 @@
 % Parse constraints on a pred or func declaration,
 % or on an existentially quantified type definition.
 
-parse_class_constraints(ModuleName, Constraints, Result) :-
-	parse_simple_class_constraints(ModuleName, Constraints, 
+parse_class_constraints(ModuleName, ConstraintsTerm, Result) :-
+	parse_class_and_inst_constraints(ModuleName, ConstraintsTerm, Result0),
+	extract_class_constraints(Result0, Result).
+
+parse_class_and_inst_constraints(ModuleName, ConstraintsTerm, Result) :-
+	parse_simple_class_and_inst_constraints(ModuleName, ConstraintsTerm, 
 		"sorry, not implemented: constraints may only constrain type variables, not compound types",
 		Result).
 
@@ -270,77 +282,116 @@
 		maybe1(list(class_constraint))).
 :- mode parse_simple_class_constraints(in, in, in, out) is det.
 
-parse_simple_class_constraints(ModuleName, Constraints, ErrorMessage,
+parse_simple_class_constraints(ModuleName, ConstraintsTerm, ErrorMessage,
 		Result) :-
-	parse_arbitrary_class_constraints(ModuleName, Constraints,
-		ParsedConstraints),
+	parse_simple_class_and_inst_constraints(ModuleName, ConstraintsTerm,
+		ErrorMessage, Result0),
+	extract_class_constraints(Result0, Result).
+
+:- pred parse_simple_class_and_inst_constraints(module_name, term, string,
+		maybe_class_and_inst_constraints).
+:- mode parse_simple_class_and_inst_constraints(in, in, in, out) is det.
+
+parse_simple_class_and_inst_constraints(ModuleName, ConstraintsTerm,
+		ErrorMessage, Result) :-
+	parse_arbitrary_class_and_inst_constraints(ModuleName, ConstraintsTerm,
+		Result0),
 	(
-		ParsedConstraints = ok(ConstraintList),
+		Result0 = ok(ConstraintList, _),
 		(
 			list__member(Constraint, ConstraintList),
 			Constraint = constraint(_, Types),
 			list__member(Type, Types),
 			\+ type_util__var(Type, _)
 		->
-			Result = error(ErrorMessage, Constraints)
+			Result = error(ErrorMessage, ConstraintsTerm)
 		;
-			Result = ParsedConstraints
+			Result = Result0
 		)
 	;
-		ParsedConstraints = error(_, _),
-		Result = ParsedConstraints
+		Result0 = error(_, _),
+		Result = Result0
 	).
 
 % Parse constraints which can constrain arbitrary types
 
-:- pred parse_arbitrary_class_constraints(module_name, term,
-		maybe1(list(class_constraint))).
-:- mode parse_arbitrary_class_constraints(in, in, out) is det.
+:- pred parse_arbitrary_class_and_inst_constraints(module_name, term,
+		maybe_class_and_inst_constraints).
+:- mode parse_arbitrary_class_and_inst_constraints(in, in, out) is det.
 
-parse_arbitrary_class_constraints(ModuleName, Constraints, ParsedConstraints) :-
-	conjunction_to_list(Constraints, ConstraintList),
-	parse_class_constraint_list(ModuleName, ConstraintList, 
-		ParsedConstraints).
+parse_arbitrary_class_and_inst_constraints(ModuleName, ConstraintsTerm,
+		Result) :-
+	conjunction_to_list(ConstraintsTerm, ConstraintList),
+	parse_class_and_inst_constraint_list(ModuleName, ConstraintList, 
+		Result).
 
-:- pred parse_class_constraint_list(module_name, list(term),
-		maybe1(list(class_constraint))).
-:- mode parse_class_constraint_list(in, in, out) is det.
+:- pred parse_class_and_inst_constraint_list(module_name, list(term),
+		maybe_class_and_inst_constraints).
+:- mode parse_class_and_inst_constraint_list(in, in, out) is det.
+
+parse_class_and_inst_constraint_list(_, [], ok([], map__init)).
+parse_class_and_inst_constraint_list(ModuleName, [C0|C0s], Result) :-
+	parse_class_or_inst_constraint(ModuleName, C0, Result0),
+	parse_class_and_inst_constraint_list(ModuleName, C0s, Result1),
+	Result = combine_class_and_inst_constraints(Result0, Result1).
+
+:- func combine_class_and_inst_constraints(maybe1(class_or_inst_constraint),
+		maybe_class_and_inst_constraints) =
+		maybe_class_and_inst_constraints.
+
+combine_class_and_inst_constraints(error(String, Term), _) =
+		error(String, Term).
+combine_class_and_inst_constraints(ok(_), error(String, Term)) =
+		error(String, Term).
+combine_class_and_inst_constraints(ok(class_constraint(ClassConstraint)),
+			ok(ClassConstraints, InstConstraints)) =
+		ok([ClassConstraint | ClassConstraints], InstConstraints).
+combine_class_and_inst_constraints(ok(inst_constraint(InstVar, Inst)),
+			ok(ClassConstraints, InstConstraints)) =
+		ok(ClassConstraints, InstConstraints ^ elem(InstVar) := Inst).
+
+:- type class_or_inst_constraint
+	--->	class_constraint(class_constraint)
+	;	inst_constraint(inst_var, inst).
+
+:- pred parse_class_or_inst_constraint(module_name, term,
+		maybe1(class_or_inst_constraint)).
+:- mode parse_class_or_inst_constraint(in, in, out) is det.
 
-parse_class_constraint_list(_, [], ok([])).
-parse_class_constraint_list(ModuleName, [C0|C0s], Result) :-
-	parse_class_constraint(ModuleName, C0, Result0),
+parse_class_or_inst_constraint(_ModuleName, ConstraintTerm, Result) :-
 	(
-		Result0 = ok(C),
-		parse_class_constraint_list(ModuleName, C0s, Result1),
-		(
-			Result1 = ok(Cs),
-			Result = ok([C|Cs])
-		;
-			Result1 = error(_, _),
-			Result = Result1
-		)
+		parse_inst_constraint(ConstraintTerm, InstVar, Inst)
+	->
+		Result = ok(inst_constraint(InstVar, Inst))
 	;
-		Result0 = error(String, Term),
-		Result = error(String, Term)
-	).
-
-:- pred parse_class_constraint(module_name, term,
-		maybe1(class_constraint)).
-:- mode parse_class_constraint(in, in, out) is det.
-
-parse_class_constraint(_ModuleName, Constraint, Result) :-
-	(
-		parse_qualified_term(Constraint, Constraint,
+		parse_qualified_term(ConstraintTerm, ConstraintTerm,
 			"class constraint", ok(ClassName, Args0))
 	->
 		% we need to enforce the invariant that types in type class
 		% constraints do not contain any info in their prog_context
 		% fields
 		list__map(convert_type, Args0, Args),
-		Result = ok(constraint(ClassName, Args))
+		Result = ok(class_constraint(constraint(ClassName, Args)))
 	;
-		Result = error("expected atom as class name", Constraint)
+		Result = error("expected atom as class name or inst constraint",
+			ConstraintTerm)
 	).
+
+:- pred parse_inst_constraint(term, inst_var, inst).
+:- mode parse_inst_constraint(in, out, out) is semidet.
+
+parse_inst_constraint(Term, InstVar, Inst) :-
+	Term = term__functor(term__atom("=<"), [Arg1, Arg2], _),
+	Arg1 = term__variable(InstVar0),
+	term__coerce_var(InstVar0, InstVar),
+	convert_inst(no_allow_constrained_inst_var, Arg2, Inst).
+
+:- pred extract_class_constraints(maybe_class_and_inst_constraints,
+		maybe1(list(class_constraint))).
+:- mode extract_class_constraints(in, out) is det.
+
+extract_class_constraints(ok(ClassConstraints, _), ok(ClassConstraints)).
+extract_class_constraints(error(String, Term), error(String, Term)).
 
 %-----------------------------------------------------------------------------%
 

-- 
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