[m-dev.] for review: polymorphic ground insts

David Overton dmo at ender.cs.mu.oz.au
Mon Mar 6 17:41:40 AEDT 2000


On Sat, Feb 26, 2000 at 04:36:29PM +1100, Fergus Henderson wrote:
> On 21-Feb-2000, David Overton <dmo at ender.cs.mu.oz.au> wrote:
> > |inst_matches_final_3(ground(UniqA, _), bound(UniqB, ListB), MaybeType,
> > |		ModuleInfo, _Exps) :-
> >  	unique_matches_final(UniqA, UniqB),
> >  	bound_inst_list_is_ground(ListB, ModuleInfo),
> > |	uniq_matches_bound_inst_list(UniqA, ListB, ModuleInfo),
> > |	(
> > |		MaybeType = yes(Type),
> > |		% We can only do this check if the type is known.
> > |		bound_inst_list_is_complete_for_type(set__init, ModuleInfo,
> > |			ListB, Type)
> > |	;
> > |		true
> > |		% XXX enabling this check makes the mode checker too
> > |		% conservative in the absence of alias tracking.
> > |	).
> 
> It's not clear from the XXX comment what code ought to be put
> there when alias tracking is enabled.
> 
> Also, won't the lack of alias tracking cause problems even
> in the case where the type is known?

I've improved the comment here.

> 
> > +inst_matches_binding_3(ground(_UniqA, _), bound(_UniqB, ListB), MaybeType,
> > +		ModuleInfo, _Exps) :-
> > +	bound_inst_list_is_ground(ListB, ModuleInfo),
> > +	(
> > +		MaybeType = yes(Type),
> > +		% We can only do this check if the type is known.
> > +		bound_inst_list_is_complete_for_type(set__init, ModuleInfo,
> > +			ListB, Type)
> > +	;
> > +		true
> > +		% XXX enabling this check makes the mode checker too
> > +		% conservative in the absence of alias tracking.
> > +	).
> 
> Likewise here.

And here.

> 
> > --- ./mercury/compiler/inst_util.m	Fri Feb 11 10:45:01 2000
> > +++ .././mercury/compiler/inst_util.m	Wed Feb 16 14:36:39 2000
> > @@ -297,7 +297,9 @@
> >  abstractly_unify_inst_3(live, ground(UniqX, constrained_inst_var(Var)),
> >  		any(UniqY), Real, M, ground(Uniq, constrained_inst_var(Var)),
> >  		semidet, M) :-
> > -	Real = fake_unify, % AAA
> > +	Real = fake_unify, 
> > +		% If Real \= fake_unify then we must fail because the inst vars
> > +		% may represent higher order insts.
> >  	unify_uniq(live, Real, det, UniqX, UniqY, Uniq).
> 
> Hmm, I don't think failing is the right thing to do there.
> 
> If I write
> 
> 	:- pred p(T, T).
> 	:- mode p(in(I), in(I)) is semidet.
> 	p(X, Y) :- X = Y.
> 
> then that should be allowed, even though `I' might be a higher-order inst.
> The situation is very similar to
> 
> 	:- pred p(T, T).
> 	:- mode p(in, in) is semidet.
> 	p(X, Y) :- X = Y.
> 
> which is allowed, but which will throw an exception at runtime if T is a
> higher-order type.  I think the treatment of these two situations should
> be the same.

I've removed the `Real = fake_unify' line.

> 
> > +++ .././mercury/compiler/mercury_to_mercury.m	Fri Feb 11 11:20:12 2000
> > @@ -688,7 +688,6 @@
> >  		mercury_output_tabs(Indent),
> >  		mercury_output_var(Var, VarSet, no),
> >  		io__write_string("\n")
> > -		% AAA
> >  	;
> >  		{ GroundInstInfo = none},
> >  		mercury_output_uniqueness(Uniq, "ground"),
> > @@ -761,7 +760,6 @@
> >  	;
> >  		{ GroundInstInfo = constrained_inst_var(Var) },
> >  		mercury_output_var(Var, VarSet, no)
> > -		% AAA
> 
> Are you using the right VarSet there?

Yes.

> 
> > @@ -1445,28 +1445,37 @@
> >  			ArgModes0, ArgModes1) },
> >  		{ mode_list_get_initial_insts(ArgModes1, ModuleInfo,
> >  			InitialInsts) },
> > +
> > +		% Compute the inst_var substitution from the initial insts
> > +		% of the called procedure and the insts of the argument
> > +		% variables.
> >  		{ map__init(InstVarSub0) },
> > -		lift(recompute_instmap_delta_call_1(Args, VarTypes, InstMap,
> > +		lift(compute_inst_var_sub(Args, VarTypes, InstMap,
> >  			InitialInsts, InstVarSub0), InstVarSub),
> >  
> > +		% Apply the inst_var substitution to the argument modes.
> >  		{ mode_list_apply_substitution(ArgModes1, InstVarSub,
> >  			ArgModes2) },
> > +
> > +		% Calculate the final insts of the argument variables
> > +		% from their initial insts and the final insts of called
> > +		% procedure (with inst_var substitutions applied.
> 
> That comment is missing a ')'.
> 

Fixed.

> 
> Apart from that, this relative diff looks fine.
> 

Here's another relative diff.  I'll commit this as soon as it passes a
bootcheck.

--- /home/ender/dmo/poly/prev/cvslog	Mon Mar  6 14:44:05 2000
+++ ./cvslog	Mon Mar  6 17:07:22 2000
@@ -103,3 +103,11 @@
 compiler/unused_args.m:
 	Pass inst_varsets and types where needed.
 	Changes to reflect change in definition of the inst data type.
+
+tests/invalid/Mmakefile:
+tests/invalid/unbound_inst_var.m:
+tests/invalid/unbound_inst_var.err_exp:
+tests/valid/Mmakefile:
+tests/valid/unbound_inst_var.m:
+	Move the `unbound_inst_var' test case from `invalid' to `valid'
+	and extend its coverage a bit.

--- accumulator.m	Mon Mar  6 14:31:19 2000
+++ ../mercury/compiler/accumulator.m	Wed Feb 23 12:03:03 2000
@@ -146,25 +146,31 @@
 
 :- type assoc_info
 	--->	assoc_info(
-			set(prog_var),	% Static set
+			static_set :: set(prog_var),
+					% Static set
 					% A static variable is one whose
 					% value is set before the
 					% recursive call.
 
-			set(prog_var),	% Dynamic set
+			dynamic_set :: set(prog_var),
+					% Dynamic set
 					% The dynamic set is initialised
 					% to Y0s.  At the end of the
 					% process it will contain all
 					% the variables that are
 					% constructed using another
 					% dynamic variable.
-			module_info,
-			prev_call_map,
-			orig_dynvar_map,
-			subst,		% Y0s -> As
-			subst,		% Hs -> As
-			set(prog_var),	% Ys
-			warnings
+			module_info :: module_info,
+			prev_call_map :: prev_call_map,
+			orig_dynvar_map :: orig_dynvar_map,
+			subst_Y0s_to_As :: subst,
+					% Y0s -> As
+			subst_Hs_to_As :: subst,
+					% Hs -> As
+			set_Ys :: set(prog_var),
+					% Ys
+			vartypes :: vartypes,
+			warnings :: warnings
 		).
 
 :- type warning 
@@ -1207,7 +1213,7 @@
 	assoc_info_init(ModuleInfo, HeadVars, VarTypes, DP, C, R0,
 		Y0stoYs_Subst, HstoAs_Subst, AssocInfo0),
 	accumulator__check_assoc(Compose, InstMapBeforeCompose, ModuleInfo,
-			VarTypes, FullyStrict, PreRecGoal0, PostRecGoal0,
+			FullyStrict, PreRecGoal0, PostRecGoal0,
 			AssocInfo0, AssocInfo),
 
 	(
@@ -1380,20 +1386,21 @@
 	% that goal into AGs.
 	%
 :- pred accumulator__check_assoc(hlds_goals::in, instmap::in,
-		module_info::in, vartypes::in, bool::in, hlds_goals::out,
+		module_info::in, bool::in, hlds_goals::out,
 		hlds_goals::out, assoc_info::in, assoc_info::out) is semidet.
 
-accumulator__check_assoc([], _InstMap, _MI, _VT, _FullyStrict, [], []) --> [].
+accumulator__check_assoc([], _InstMap, _MI, _FullyStrict, [], []) --> [].
 accumulator__check_assoc([Goal0 | Goal0s], InstMapBeforeGoal0,
-		ModuleInfo, VarTypes, FullyStrict, MovedGoals, AfterGoals) -->
+		ModuleInfo, FullyStrict, MovedGoals, AfterGoals) -->
 	(
 		{ goal_is_construction_unification(Goal0) }
 	->
+		VarTypes =^ vartypes,
 		{ move_goals(Goal0, InstMapBeforeGoal0, ModuleInfo, VarTypes,
 			FullyStrict, Goal0s, PreGoal0s, PostGoal0s) },
 		accumulator__check_assoc(PreGoal0s, InstMapBeforeGoal0,
-				ModuleInfo, VarTypes, FullyStrict,
-				MovedGoals, AfterGoal0s),
+				ModuleInfo, FullyStrict, MovedGoals,
+				AfterGoal0s),
 		{ list__append(AfterGoal0s, [Goal0 | PostGoal0s], AfterGoals) }
 	;
 		{ Goal0 = _ - GoalInfo0 },
@@ -1404,8 +1411,8 @@
 
 		accumulator__check_goal(Goal0, Goal),
 		accumulator__check_assoc(Goal0s, InstMapBeforeGoal0s,
-				ModuleInfo, VarTypes, FullyStrict,
-				MovedGoal0s, AfterGoals),
+				ModuleInfo, FullyStrict, MovedGoal0s,
+				AfterGoals),
 		{ MovedGoals = [Goal | MovedGoal0s] }
 	).
 
@@ -1755,7 +1762,8 @@
 
 	proc_info_argmodes(ProcInfo, Modes),
 	pred_info_get_assertions(PredInfo, Assertions),
-	proc_info_vartypes(ProcInfo, VarTypes),
+
+	VarTypes = AssocInfo0^vartypes,
 
 	(
 		commutativity_assertion(set__to_sorted_list(Assertions),
@@ -1981,87 +1989,72 @@
 
 	AssocInfo = assoc_info(StaticSet, DynamicSet,
 			ModuleInfo, PrevCallMap, OrigDynVarMap,
-			Y0stoAs_Subst, HstoAs_Subst, YsSet,
+			Y0stoAs_Subst, HstoAs_Subst, YsSet, VarTypes,
 			ErrorMessages).
 
 :- pred assoc_info_static_set(set(prog_var)::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_static_set(StaticSet, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(StaticSet, _, _, _, _, _, _, _, _).
+assoc_info_static_set(StaticSet) --> StaticSet =^ static_set.
 
 :- pred assoc_info_dynamic_set(set(prog_var)::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_dynamic_set(DynamicSet, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, DynamicSet, _, _, _, _, _, _, _).
+assoc_info_dynamic_set(DynamicSet) --> DynamicSet =^ dynamic_set.
 
 :- pred assoc_info_module_info(module_info::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_module_info(ModuleInfo, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, _, ModuleInfo, _, _, _, _, _, _).
+assoc_info_module_info(ModuleInfo) --> ModuleInfo =^ module_info.
 
 :- pred assoc_info_prev_call_map(prev_call_map::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_prev_call_map(PrevCallMap, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, _, _, PrevCallMap, _, _, _, _, _).
+assoc_info_prev_call_map(PrevCallMap) --> PrevCallMap =^ prev_call_map.
 
 :- pred assoc_info_orig_dynvar_map(orig_dynvar_map::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_orig_dynvar_map(OrigDynVarMap, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, _, _, _, OrigDynVarMap, _, _, _, _).
+assoc_info_orig_dynvar_map(OrigDynVarMap) --> OrigDynVarMap =^ orig_dynvar_map.
 
 :- pred assoc_info_Y0stoAs(subst::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_Y0stoAs(Y0stoAs_Subst, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, _, _, _, _, Y0stoAs_Subst, _, _, _).
+assoc_info_Y0stoAs(Y0stoAs_Subst) --> Y0stoAs_Subst =^ subst_Y0s_to_As.
 
 :- pred assoc_info_HstoAs(subst::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_HstoAs(HstoAs_Subst, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, _, _, _, _, _, HstoAs_Subst, _, _).
+assoc_info_HstoAs(HstoAs_Subst) --> HstoAs_Subst =^ subst_Hs_to_As.
 
 :- pred assoc_info_Ys(set(prog_var)::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_Ys(Ys, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, _, _, _, _, _, _, Ys, _).
+assoc_info_Ys(Ys) --> Ys =^ set_Ys.
 
 :- pred assoc_info_warnings(warnings::out,
 		assoc_info::in, assoc_info::out) is det.
-assoc_info_warnings(Warnings, AssocInfo, AssocInfo) :-
-	AssocInfo = assoc_info(_, _, _, _, _, _, _, _, Warnings).
+assoc_info_warnings(Warnings) --> Warnings =^ warnings.
 
 /*
 :- pred assoc_info_set_static_set(set(prog_var)::in, assoc_info::in,
 		assoc_info::out) is det.
-assoc_info_set_static_set(StaticSet, assoc_info(_, B, C, D, E, F, G, H, I),
-		assoc_info(StaticSet, B, C, D, E, F, G, H, I)).
+assoc_info_set_static_set(StaticSet) --> ^static_set := StaticSet.
 */
 
 :- pred assoc_info_set_dynamic_set(set(prog_var)::in, assoc_info::in,
 		assoc_info::out) is det.
-assoc_info_set_dynamic_set(DynamicSet, assoc_info(A, _, C, D, E, F, G, H, I),
-		assoc_info(A, DynamicSet, C, D, E, F, G, H, I)).
+assoc_info_set_dynamic_set(DynamicSet) --> ^dynamic_set := DynamicSet.
 
 :- pred assoc_info_set_prev_call_map(prev_call_map::in, assoc_info::in,
 		assoc_info::out) is det.
-assoc_info_set_prev_call_map(PrevCallMap, assoc_info(A, B, C, _, E, F, G, H, I),
-		assoc_info(A, B, C, PrevCallMap, E, F, G, H, I)).
+assoc_info_set_prev_call_map(PrevCallMap) --> ^prev_call_map := PrevCallMap.
 
 :- pred assoc_info_set_orig_dynvar_map(orig_dynvar_map::in, assoc_info::in,
 		assoc_info::out) is det.
-assoc_info_set_orig_dynvar_map(OrigDynMap,
-		assoc_info(A, B, C, D, _, F, G, H, I),
-		assoc_info(A, B, C, D, OrigDynMap, F, G, H, I)).
+assoc_info_set_orig_dynvar_map(OrigDynMap) --> ^orig_dynvar_map := OrigDynMap.
 
 :- pred assoc_info_set_Y0stoAs(subst::in, assoc_info::in,
 		assoc_info::out) is det.
-assoc_info_set_Y0stoAs(Y0stoAs_Subst, assoc_info(A, B, C, D, E, _, G, H, I),
-		assoc_info(A, B, C, D, E, Y0stoAs_Subst, G, H, I)).
+assoc_info_set_Y0stoAs(Y0stoAs_Subst) --> ^subst_Y0s_to_As := Y0stoAs_Subst.
 
 :- pred assoc_info_add_warning(warning::in, assoc_info::in,
 		assoc_info::out) is det.
-assoc_info_add_warning(Warning,
-		assoc_info(A, B, C, D, E, F, G, H, Warnings),
-		assoc_info(A, B, C, D, E, F, G, H, [Warning | Warnings])).
+assoc_info_add_warning(Warning) -->
+	Warnings =^ warnings,
+	^warnings := [Warning | Warnings].
 
 %-----------------------------------------------------------------------------%
 %-----------------------------------------------------------------------------%
--- hlds_pred.m	Mon Mar  6 14:31:19 2000
+++ ../mercury/compiler/hlds_pred.m	Mon Mar  6 13:32:41 2000
@@ -1441,13 +1441,11 @@
 
 :- type proc_info
 	--->	procedure(
-			declared_detism	:: maybe(determinism),
-					% _declared_ determinism
-					% or `no' if there was no detism decl
 			prog_varset	:: prog_varset,
 			var_types	:: vartypes,
 			head_vars	:: list(prog_var),
 			actual_head_modes :: list(mode),
+			inst_varset :: inst_varset,
 			head_var_caller_liveness :: maybe(list(is_live)),
 					% Liveness (in the mode analysis sense)
 					% of the arguments in the caller; says
@@ -1460,6 +1458,9 @@
 					% if there was no mode declaration).
 			stack_slots	:: stack_slots,
 					% stack allocations
+			declared_detism	:: maybe(determinism),
+					% _declared_ determinism
+					% or `no' if there was no detism decl
 			inferred_detism	:: determinism,
 			can_process	:: bool,
 					% no if we must not process this
@@ -1540,33 +1541,36 @@
 	map__init(TCVarsMap),
 	RLExprn = no,
 	NewProc = procedure(
-		MaybeDet, BodyVarSet, BodyTypes, HeadVars, Modes, MaybeArgLives,
-		ClauseBody, MContext, StackSlots, InferredDet, CanProcess,
-		ArgInfo, InitialLiveness, TVarsMap, TCVarsMap, eval_normal,
-		no, no, DeclaredModes, IsAddressTaken, RLExprn
+		BodyVarSet, BodyTypes, HeadVars, Modes, InstVarSet,
+		MaybeArgLives, ClauseBody, MContext, StackSlots, MaybeDet,
+		InferredDet, CanProcess, ArgInfo, InitialLiveness,
+		TVarsMap, TCVarsMap, eval_normal, no, no, DeclaredModes,
+		IsAddressTaken, RLExprn
 	).
 
 proc_info_set(DeclaredDetism, BodyVarSet, BodyTypes, HeadVars, HeadModes,
-		HeadLives, Goal, Context, StackSlots, InferredDetism,
-		CanProcess, ArgInfo, Liveness, TVarMap, TCVarsMap, ArgSizes,
-		Termination, IsAddressTaken, ProcInfo) :-
+		InstVarSet, HeadLives, Goal, Context, StackSlots, 
+		InferredDetism, CanProcess, ArgInfo, Liveness, TVarMap,
+		TCVarsMap, ArgSizes, Termination, IsAddressTaken,
+		ProcInfo) :-
 	RLExprn = no,
 	ProcInfo = procedure(
-		DeclaredDetism, BodyVarSet, BodyTypes, HeadVars, HeadModes,
-		HeadLives, Goal, Context, StackSlots, InferredDetism,
-		CanProcess, ArgInfo, Liveness, TVarMap, TCVarsMap, eval_normal, 
-		ArgSizes, Termination, no, IsAddressTaken, RLExprn).
+		BodyVarSet, BodyTypes, HeadVars,
+		HeadModes, InstVarSet, HeadLives, Goal, Context,
+		StackSlots, DeclaredDetism, InferredDetism, CanProcess, ArgInfo,
+		Liveness, TVarMap, TCVarsMap, eval_normal, ArgSizes,
+		Termination, no, IsAddressTaken, RLExprn).
 
-proc_info_create(VarSet, VarTypes, HeadVars, HeadModes, Detism, Goal,
-		Context, TVarMap, TCVarsMap, IsAddressTaken, ProcInfo) :-
+proc_info_create(VarSet, VarTypes, HeadVars, HeadModes, InstVarSet, Detism,
+		Goal, Context, TVarMap, TCVarsMap, IsAddressTaken, ProcInfo) :-
 	map__init(StackSlots),
 	set__init(Liveness),
 	MaybeHeadLives = no,
 	RLExprn = no,
-	ProcInfo = procedure(yes(Detism), VarSet, VarTypes, HeadVars, HeadModes,
-		MaybeHeadLives, Goal, Context, StackSlots, Detism, yes, [],
-		Liveness, TVarMap, TCVarsMap, eval_normal, no, no, no, 
-		IsAddressTaken, RLExprn).
+	ProcInfo = procedure(VarSet, VarTypes, HeadVars, HeadModes,
+		InstVarSet, MaybeHeadLives, Goal, Context, StackSlots,
+		yes(Detism), Detism, yes, [], Liveness, TVarMap, TCVarsMap,
+		eval_normal, no, no, no, IsAddressTaken, RLExprn).
 
 proc_info_set_body(ProcInfo0, VarSet, VarTypes, HeadVars, Goal,
 		TI_VarMap, TCI_VarMap, ProcInfo) :-
@@ -1636,6 +1640,7 @@
 proc_info_vartypes(ProcInfo, ProcInfo^var_types).
 proc_info_headvars(ProcInfo, ProcInfo^head_vars).
 proc_info_argmodes(ProcInfo, ProcInfo^actual_head_modes).
+proc_info_inst_varset(ProcInfo, ProcInfo^inst_varset).
 proc_info_maybe_arglives(ProcInfo, ProcInfo^head_var_caller_liveness).
 proc_info_goal(ProcInfo, ProcInfo^body).
 proc_info_context(ProcInfo, ProcInfo^proc_context).
@@ -1657,6 +1662,7 @@
 proc_info_set_vartypes(ProcInfo, VT, ProcInfo^var_types := VT).
 proc_info_set_headvars(ProcInfo, HV, ProcInfo^head_vars := HV).
 proc_info_set_argmodes(ProcInfo, AM, ProcInfo^actual_head_modes := AM).
+proc_info_set_inst_varset(ProcInfo, IV, ProcInfo^inst_varset := IV).
 proc_info_set_maybe_arglives(ProcInfo, CL,
 	ProcInfo^head_var_caller_liveness := CL).
 proc_info_set_goal(ProcInfo, G, ProcInfo^body := G).
--- inst_match.m	Mon Mar  6 14:31:45 2000
+++ ../mercury/compiler/inst_match.m	Mon Mar  6 14:39:37 2000
@@ -259,120 +259,324 @@
 %-----------------------------------------------------------------------------%
 
 :- implementation.
-:- import_module hlds_data, mode_util, prog_data, inst_util.
+:- import_module hlds_data, mode_util, prog_data, inst_util, type_util.
 :- import_module list, set, map, term, std_util, require, bool.
 
-inst_matches_initial(InstA, InstB, ModuleInfo) :-
-	set__init(Expansions0),
-	inst_matches_initial_2(InstA, InstB, ModuleInfo,
-		Expansions0, _Expansions).
+inst_matches_initial(InstA, InstB, Type, ModuleInfo) :-
+	map__init(Sub0),
+	inst_matches_initial(InstA, InstB, Type, ModuleInfo, _, Sub0, _).
+
+inst_matches_initial(InstA, InstB, Type, ModuleInfo0, ModuleInfo, Sub0, Sub) :-
+	Info0 = init_inst_match_info(ModuleInfo0)^sub := Sub0,
+	inst_matches_initial_2(InstA, InstB, yes(Type), Info0, Info),
+	ModuleInfo = Info^module_info,
+	Sub = Info^sub.
 
 :- type expansions == set(pair(inst)).
 
-:- pred inst_matches_initial_2(inst, inst, module_info,
-		expansions, expansions).
+:- type inst_match_info
+	--->	inst_match_info(
+			module_info	:: module_info,
+			expansions	:: expansions,
+			sub		:: inst_var_sub
+		).
+
+:- func init_inst_match_info(module_info) = inst_match_info.
+
+init_inst_match_info(ModuleInfo) = inst_match_info(ModuleInfo, Exp, Sub) :-
+	set__init(Exp),
+	map__init(Sub).
+
+:- pred inst_matches_initial_2(inst, inst, maybe(type), 
+		inst_match_info, inst_match_info).
 :- mode inst_matches_initial_2(in, in, in, in, out) is semidet.
 
-inst_matches_initial_2(InstA, InstB, ModuleInfo, Expansions0, Expansions) :-
+inst_matches_initial_2(InstA, InstB, Type, Info0, Info) :-
 	ThisExpansion = InstA - InstB,
-	( set__member(ThisExpansion, Expansions0) ->
-		Expansions = Expansions0
-/********* 
-		% does this test improve efficiency??
-	; InstA = InstB ->
-		Expansions = Expansions0
-**********/
+	( set__member(ThisExpansion, Info0^expansions) ->
+		Info = Info0
+
 	;
-		inst_expand(ModuleInfo, InstA, InstA2),
-		inst_expand(ModuleInfo, InstB, InstB2),
-		set__insert(Expansions0, ThisExpansion, Expansions1),
-		inst_matches_initial_3(InstA2, InstB2, ModuleInfo,
-			Expansions1, Expansions)
+		inst_expand(Info0^module_info, InstA, InstA2),
+		inst_expand(Info0^module_info, InstB, InstB2),
+		set__insert(Info0^expansions, ThisExpansion, Expansions1),
+		inst_matches_initial_3(InstA2, InstB2, Type, 
+			Info0^expansions := Expansions1, Info)
 	).
 
-:- pred inst_matches_initial_3(inst, inst, module_info, expansions, expansions).
+:- pred inst_matches_initial_3(inst, inst, maybe(type), 
+		inst_match_info, inst_match_info).
 :- mode inst_matches_initial_3(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), _, Expansions, Expansions) :-
+inst_matches_initial_3(any(UniqA), any(UniqB), _, I, I) :-
 	unique_matches_initial(UniqA, UniqB).
-inst_matches_initial_3(any(_), free, _, Expansions, Expansions).
-inst_matches_initial_3(free, any(_), _, Expansions, Expansions).
-inst_matches_initial_3(free, free, _, Expansions, Expansions).
-inst_matches_initial_3(bound(UniqA, ListA), any(UniqB), ModuleInfo,
-		Expansions, Expansions) :-
+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) :-
 	unique_matches_initial(UniqA, UniqB),
-	bound_inst_list_matches_uniq(ListA, UniqB, ModuleInfo).
-inst_matches_initial_3(bound(_Uniq, _List), free, _, Expansions, Expansions).
-inst_matches_initial_3(bound(UniqA, ListA), bound(UniqB, ListB), ModuleInfo,
-		Expansions0, Expansions) :-
+	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,
+		Info0, Info) :-
 	unique_matches_initial(UniqA, UniqB),
-	bound_inst_list_matches_initial(ListA, ListB, ModuleInfo,
-		Expansions0, Expansions).
-inst_matches_initial_3(bound(UniqA, ListA), ground(UniqB, no), ModuleInfo,
-		Expansions, Expansions) :-
+	bound_inst_list_matches_initial(ListA, ListB, Type, Info0, Info).
+inst_matches_initial_3(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)), _,
+		Info0, Info) :-
 	unique_matches_initial(UniqA, UniqB),
-	bound_inst_list_is_ground(ListA, ModuleInfo),
-	bound_inst_list_matches_uniq(ListA, UniqB, ModuleInfo).
-inst_matches_initial_3(bound(Uniq, List), abstract_inst(_,_), ModuleInfo,
-		Expansions, Expansions) :-
+	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, ModuleInfo1, ModuleInfo, Sub0, Sub),
+	Info = (Info0^module_info := ModuleInfo)
+		^sub := Sub.
+inst_matches_initial_3(bound(Uniq, List), abstract_inst(_,_), _, Info, Info) :-
 	Uniq = unique,
-	bound_inst_list_is_ground(List, ModuleInfo),
-	bound_inst_list_is_unique(List, ModuleInfo).
-inst_matches_initial_3(bound(Uniq, List), abstract_inst(_,_), ModuleInfo,
-		Expansions, Expansions) :-
+	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) :-
 	Uniq = mostly_unique,
-	bound_inst_list_is_ground(List, ModuleInfo),
-	bound_inst_list_is_mostly_unique(List, ModuleInfo).
-inst_matches_initial_3(ground(UniqA, _PredInst), any(UniqB), _,
-		Expansions, Expansions) :-
+	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, _PredInst), any(UniqB), _, I, I) :-
 	unique_matches_initial(UniqA, UniqB).
-inst_matches_initial_3(ground(_Uniq, _PredInst), free, _,
-		Expansions, Expansions).
-inst_matches_initial_3(ground(UniqA, _), bound(UniqB, List), ModuleInfo,
-		Expansions, Expansions) :-
+inst_matches_initial_3(ground(_Uniq, _PredInst), free, _, I, I).
+inst_matches_initial_3(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),
-	uniq_matches_bound_inst_list(UniqA, List, ModuleInfo),
-	fail.	% XXX BUG! should fail only if 
-		% List does not include all the constructors for the type,
-		% or if List contains some not_reached insts.
-		% Should succeed if List contains all the constructors
-		% for the type.  Problem is we don't know what the type was :-(
-inst_matches_initial_3(ground(UniqA, PredInstA), ground(UniqB, PredInstB),
-		ModuleInfo, Expansions, Expansions) :-
-	maybe_pred_inst_matches_initial(PredInstA, PredInstB, ModuleInfo),
-	unique_matches_initial(UniqA, UniqB).
-inst_matches_initial_3(ground(_UniqA, no), abstract_inst(_,_), _, _, _) :-
+	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),
+		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(_,_),_,_,_) :-
 		% 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), _,
-		Expansions, Expansions).
-inst_matches_initial_3(abstract_inst(_,_), free, _, Expansions, Expansions).
+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),
-				ModuleInfo, Expansions0, Expansions) :-
-	inst_list_matches_initial(ArgsA, ArgsB, ModuleInfo,
-		Expansions0, Expansions).
-inst_matches_initial_3(not_reached, _, _, Expansions, Expansions).
+		_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).
 
 %-----------------------------------------------------------------------------%
 
-:- pred maybe_pred_inst_matches_initial(maybe(pred_inst_info),
-		maybe(pred_inst_info), module_info).
-:- mode maybe_pred_inst_matches_initial(in, in, in) is semidet.
-
-maybe_pred_inst_matches_initial(no, no, _).
-maybe_pred_inst_matches_initial(yes(_), no, _).
-maybe_pred_inst_matches_initial(yes(PredInstA), yes(PredInstB), ModuleInfo) :-
-	pred_inst_matches(PredInstA, PredInstB, ModuleInfo).
+	% This predicate assumes that the check of
+	% `bound_inst_list_is_complete_for_type' is done by the caller.
+:- pred ground_matches_initial_bound_inst_list(uniqueness, list(bound_inst),
+	maybe(type), inst_match_info, inst_match_info).
+:- mode ground_matches_initial_bound_inst_list(in, in, in, in, out) is semidet.
+
+ground_matches_initial_bound_inst_list(_, [], _) --> [].
+ground_matches_initial_bound_inst_list(Uniq, [functor(ConsId, Args) | List],
+		MaybeType) -->
+	ModuleInfo0 =^ module_info,
+	{ maybe_get_cons_id_arg_types(ModuleInfo0, MaybeType, ConsId,
+		MaybeTypes) },
+	ground_matches_initial_inst_list(Uniq, Args, MaybeTypes),
+	ground_matches_initial_bound_inst_list(Uniq, List, MaybeType).
+
+:- pred ground_matches_initial_inst_list(uniqueness, list(inst),
+	list(maybe(type)), inst_match_info, inst_match_info).
+:- mode ground_matches_initial_inst_list(in, in, in, in, out) is semidet.
+
+ground_matches_initial_inst_list(_, [], []) --> [].
+ground_matches_initial_inst_list(Uniq, [Inst | Insts], [Type | Types]) -->
+	inst_matches_initial_2(ground(Uniq, none), Inst, Type),
+	ground_matches_initial_inst_list(Uniq, Insts, Types).
+
+%-----------------------------------------------------------------------------%
+
+	% A list(bound_inst) is ``complete'' for a given type iff it
+	% includes each functor of the type and each argument of each
+	% functor is also ``complete'' for the type.
+:- pred bound_inst_list_is_complete_for_type(set(inst_name), module_info,
+		list(bound_inst), type).
+:- mode bound_inst_list_is_complete_for_type(in, in, in, in) is semidet.
+
+bound_inst_list_is_complete_for_type(Expansions, ModuleInfo, BoundInsts, Type)
+		:-
+	% Is this a type for which cons_ids are recorded in the type_table?
+	type_util__cons_id_arg_types(ModuleInfo, Type, _, _),
+
+	% Is there a bound_inst for each cons_id in the type_table?
+	all [ConsId, ArgTypes] (
+		type_util__cons_id_arg_types(ModuleInfo, Type, ConsId,
+			ArgTypes)
+	=>
+		(
+			list__member(functor(ConsId0, ArgInsts), BoundInsts),
+			% Cons_ids returned from type_util__cons_id_arg_types
+			% are not module-qualified so we need to call
+			% equivalent_cons_ids instead of just using `=/2'.
+			equivalent_cons_ids(ConsId0, ConsId),
+			list__map(inst_is_complete_for_type(Expansions,
+				ModuleInfo), ArgInsts, ArgTypes)
+		)
+	).
+
+:- pred inst_is_complete_for_type(set(inst_name), module_info, inst, type).
+:- mode inst_is_complete_for_type(in, in, in, in) is semidet.
+
+inst_is_complete_for_type(Expansions, ModuleInfo, Inst, Type) :-
+	( Inst = defined_inst(Name) ->
+		( set__member(Name, Expansions) ->
+			true
+		;
+			inst_lookup(ModuleInfo, Name, ExpandedInst),
+			inst_is_complete_for_type(Expansions `set__insert` Name,
+				ModuleInfo, ExpandedInst, Type)
+		)
+	; Inst = bound(_, List) ->
+		bound_inst_list_is_complete_for_type(Expansions, ModuleInfo,
+			List, Type)
+	;
+		Inst \= not_reached
+	).
+
+	% Check that two cons_ids are the same, except that one may be less
+	% module qualified than the other.
+:- pred equivalent_cons_ids(cons_id, cons_id).
+:- mode equivalent_cons_ids(in, in) is semidet.
+
+equivalent_cons_ids(ConsIdA, ConsIdB) :-
+	(
+		ConsIdA = cons(NameA, ArityA),
+		ConsIdB = cons(NameB, ArityB)
+	->
+		ArityA = ArityB,
+		equivalent_sym_names(NameA, NameB)
+	;
+		ConsIdA = ConsIdB
+	).
+
+:- pred equivalent_sym_names(sym_name, sym_name).
+:- mode equivalent_sym_names(in, in) is semidet.
+
+equivalent_sym_names(unqualified(S), unqualified(S)).
+equivalent_sym_names(qualified(_, S), unqualified(S)).
+equivalent_sym_names(unqualified(S), qualified(_, S)).
+equivalent_sym_names(qualified(QualA, S), qualified(QualB, S)) :-
+	equivalent_sym_names(QualA, QualB).
+
+%-----------------------------------------------------------------------------%
+
+	% 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, module_info, module_info,
+		inst_var_sub, inst_var_sub).
+:- mode update_inst_var_sub(in, in, in, out, in, out) is semidet.
+
+update_inst_var_sub(InstVar, InstA, ModuleInfo0, ModuleInfo, Sub0, Sub) :-
+	( map__search(Sub0, InstVar, InstB) ->
+		% If InstVar already has an inst associated with it,
+		% merge the old inst and the new inst.  Fail is this merge
+		% is not possible.
+		inst_merge(InstA, InstB, ModuleInfo0, Inst, ModuleInfo),
+		map__det_update(Sub0, InstVar, Inst, Sub)
+	;
+		ModuleInfo = ModuleInfo0,
+		map__det_insert(Sub0, InstVar, InstA, Sub)
+	).
+
+%-----------------------------------------------------------------------------%
+
+	% This predicate checks if two ground_inst_infos match_initial.
+	% It does not check uniqueness.
+:- pred ground_inst_info_matches_initial(ground_inst_info, ground_inst_info,
+		uniqueness, maybe(type), inst_match_info, inst_match_info).
+:- mode ground_inst_info_matches_initial(in, in, in, in, in, out) is semidet.
+
+ground_inst_info_matches_initial(_, none, _, _) --> [].
+ground_inst_info_matches_initial(higher_order(PredInstA),
+		higher_order(PredInstB), _, Type) -->
+	pred_inst_matches_initial(PredInstA, PredInstB, Type).
+ground_inst_info_matches_initial(GroundInstInfoA,
+		constrained_inst_var(InstVarB), UniqB, _) -->
+	{ Inst = ground(UniqB, GroundInstInfoA) },
+	ModuleInfo0 =^ module_info,
+	Sub0 =^ sub,
+	{ update_inst_var_sub(InstVarB, Inst, 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).
+:- mode pred_inst_matches_initial(in, in, in, in, out) is semidet.
+
+pred_inst_matches_initial(pred_inst_info(PredOrFunc, ModesA, Det),
+		pred_inst_info(PredOrFunc, ModesB, Det), MaybeType) -->
+	{ maybe_get_higher_order_arg_types(MaybeType, length(ModesA),
+		MaybeTypes) },
+	pred_inst_argmodes_matches_initial(ModesA, ModesB, MaybeTypes),
+	Sub =^ sub,
+	{ mode_list_apply_substitution(ModesA, Sub, ModesASub) },
+	{ mode_list_apply_substitution(ModesB, Sub, ModesBSub) },
+	pred_inst_argmodes_matches(ModesASub, ModesBSub, MaybeTypes).
+
+	% pred_inst_matches_argmodes(ModesA, ModesB, ModuleInfo, Expansions):
+	% succeeds if the initial insts of ModesB specify at least as
+	% much information as, and the same binding as, the initial
+	% insts of ModesA; and the final insts of ModesA specify at
+	% least as much information as, and the same binding as, the
+	% final insts of ModesB.  Any inst pairs in Expansions are assumed
+	% to match_final each other.
+	%
+:- pred pred_inst_argmodes_matches_initial(list(mode), list(mode),
+	list(maybe(type)), inst_match_info, inst_match_info).
+:- mode pred_inst_argmodes_matches_initial(in, in, in, in, out) is semidet.
+
+pred_inst_argmodes_matches_initial([], [], []) --> [].
+pred_inst_argmodes_matches_initial([ModeA|ModeAs], [ModeB|ModeBs],
+		[Type|Types]) -->
+	ModuleInfo0 =^ module_info,
+	{ mode_get_insts(ModuleInfo0, ModeA, InitialA, FinalA) },
+	{ mode_get_insts(ModuleInfo0, ModeB, InitialB, FinalB) },
+	inst_matches_initial_2(InitialA, InitialB, Type),
+	inst_matches_initial_2(FinalA, FinalB, Type),
+	pred_inst_argmodes_matches_initial(ModeAs, ModeBs, Types).
 
 pred_inst_matches(PredInstA, PredInstB, ModuleInfo) :-
-	set__init(Expansions0),
-	pred_inst_matches_2(PredInstA, PredInstB, ModuleInfo,
-		Expansions0, _).
+	pred_inst_matches_1(PredInstA, PredInstB, no, ModuleInfo).
+
+:- pred pred_inst_matches_1(pred_inst_info, pred_inst_info, maybe(type),
+		module_info).
+:- mode pred_inst_matches_1(in, in, in, in) is semidet.
+
+pred_inst_matches_1(PredInstA, PredInstB, MaybeType, ModuleInfo) :-
+	Info0 = init_inst_match_info(ModuleInfo),
+	pred_inst_matches_2(PredInstA, PredInstB, MaybeType, Info0, _).
 
 	% pred_inst_matches_2(PredInstA, PredInstB, ModuleInfo, Expansions)
 	%	Same as pred_inst_matches/3, except that inst pairs in
@@ -380,32 +584,17 @@
 	%	(This avoids infinite loops when calling inst_matches_final
 	%	on higher-order recursive insts.)
 	%
-:- pred pred_inst_matches_2(pred_inst_info, pred_inst_info, module_info,
-			expansions, expansions).
+:- pred pred_inst_matches_2(pred_inst_info, pred_inst_info, maybe(type),
+		inst_match_info, inst_match_info).
 :- mode pred_inst_matches_2(in, in, in, in, out) is semidet.
 
 pred_inst_matches_2(pred_inst_info(PredOrFunc, ModesA, Det),
 		pred_inst_info(PredOrFunc, ModesB, Det),
-		ModuleInfo, Expansions0, Expansions) :-
-	pred_inst_argmodes_matches(ModesA, ModesB, ModuleInfo, Expansions0,
-		Expansions).
-
-:- pred pred_inst_matches_2(pred_inst_info, pred_inst_info,
-				module_info, expansions).
-:- mode pred_inst_matches_2(in, in, in, in) is semidet.
-
-pred_inst_matches_2(PredInstInfoA, PredInstInfoB, ModuleInfo, Expansions) :-
-	pred_inst_matches_2(PredInstInfoA, PredInstInfoB, ModuleInfo,
-		Expansions, _).
-	
-:- pred pred_inst_argmodes_matches(list(mode), list(mode),
-				module_info, expansions).
-:- mode pred_inst_argmodes_matches(in, in, in, in) is semidet.
-
-pred_inst_argmodes_matches(ModesA, ModesB, ModuleInfo, Expansions) :-
-	pred_inst_argmodes_matches(ModesA, ModesB, ModuleInfo,
-		Expansions, _).
-	
+		MaybeType) -->
+	{ maybe_get_higher_order_arg_types(MaybeType, length(ModesA),
+		MaybeTypes) },
+	pred_inst_argmodes_matches(ModesA, ModesB, MaybeTypes).
+
 	% pred_inst_matches_argmodes(ModesA, ModesB, ModuleInfo, Expansions):
 	% succeeds if the initial insts of ModesB specify at least as
 	% much information as, and the same binding as, the initial
@@ -414,21 +603,19 @@
 	% final insts of ModesB.  Any inst pairs in Expansions are assumed
 	% to match_final each other.
 	%
-:- pred pred_inst_argmodes_matches(list(mode), list(mode),
-				module_info, expansions, expansions).
+:- pred pred_inst_argmodes_matches(list(mode), list(mode), list(maybe(type)),
+				inst_match_info, inst_match_info).
 :- mode pred_inst_argmodes_matches(in, in, in, in, out) is semidet.
 
-pred_inst_argmodes_matches([], [], _, Expansions, Expansions).
+pred_inst_argmodes_matches([], [], []) --> [].
 pred_inst_argmodes_matches([ModeA|ModeAs], [ModeB|ModeBs],
-		ModuleInfo, Expansions0, Expansions) :-
-	mode_get_insts(ModuleInfo, ModeA, InitialA, FinalA),
-	mode_get_insts(ModuleInfo, ModeB, InitialB, FinalB),
-	inst_matches_final_2(InitialB, InitialA, ModuleInfo,
-		Expansions0, Expansions1),
-	inst_matches_final_2(FinalA, FinalB, ModuleInfo,
-		Expansions1, Expansions2),
-	pred_inst_argmodes_matches(ModeAs, ModeBs, ModuleInfo,
-		Expansions2, Expansions).
+		[MaybeType | MaybeTypes]) -->
+	ModuleInfo =^ module_info,
+	{ mode_get_insts(ModuleInfo, ModeA, InitialA, FinalA) },
+	{ mode_get_insts(ModuleInfo, ModeB, InitialB, FinalB) },
+	inst_matches_final_2(InitialB, InitialA, MaybeType),
+	inst_matches_final_2(FinalA, FinalB, MaybeType),
+	pred_inst_argmodes_matches(ModeAs, ModeBs, MaybeTypes).
 
 %-----------------------------------------------------------------------------%
 
@@ -487,39 +674,78 @@
 	% are sorted.
 
 :- pred bound_inst_list_matches_initial(list(bound_inst), list(bound_inst),
-					module_info, expansions, expansions).
+	maybe(type), inst_match_info, inst_match_info).
 :- mode bound_inst_list_matches_initial(in, in, in, in, out) is semidet.
 
-bound_inst_list_matches_initial([], _, _, Expansions, Expansions).
-bound_inst_list_matches_initial([X|Xs], [Y|Ys], ModuleInfo,
-		Expansions0, Expansions) :-
-	X = functor(ConsIdX, ArgsX),
-	Y = functor(ConsIdY, ArgsY),
-	( ConsIdX = ConsIdY ->
-		inst_list_matches_initial(ArgsX, ArgsY, ModuleInfo,
-			Expansions0, Expansions1),
-		bound_inst_list_matches_initial(Xs, Ys, ModuleInfo,
-			Expansions1, Expansions)
+bound_inst_list_matches_initial([], _, _) --> [].
+bound_inst_list_matches_initial([X|Xs], [Y|Ys], MaybeType) -->
+	{ X = functor(ConsIdX, ArgsX) },
+	{ Y = functor(ConsIdY, ArgsY) },
+	( { ConsIdX = ConsIdY } ->
+		ModuleInfo =^ module_info,
+		{ maybe_get_cons_id_arg_types(ModuleInfo, MaybeType, ConsIdX,
+			MaybeTypes) },
+		inst_list_matches_initial(ArgsX, ArgsY, MaybeTypes),
+		bound_inst_list_matches_initial(Xs, Ys, MaybeType)
 	;
-		compare(>, ConsIdX, ConsIdY),
+		{ compare(>, ConsIdX, ConsIdY) },
 			% ConsIdY does not occur in [X|Xs].
 			% Hence [X|Xs] implicitly specifies `not_reached'
 			% for the args of ConsIdY, and hence 
 			% automatically matches_initial Y.  We just need to
 			% check that [X|Xs] matches_initial Ys.
-		bound_inst_list_matches_initial([X|Xs], Ys, ModuleInfo,
-					Expansions0, Expansions)
+		bound_inst_list_matches_initial([X|Xs], Ys, MaybeType)
 	).
 
-:- pred inst_list_matches_initial(list(inst), list(inst), module_info,
-				expansions, expansions).
+:- pred inst_list_matches_initial(list(inst), list(inst), list(maybe(type)),
+	inst_match_info, inst_match_info).
 :- mode inst_list_matches_initial(in, in, in, in, out) is semidet.
 
-inst_list_matches_initial([], [], _, Expansions, Expansions).
-inst_list_matches_initial([X|Xs], [Y|Ys], ModuleInfo,
-		Expansions0, Expansions) :-
-	inst_matches_initial_2(X, Y, ModuleInfo, Expansions0, Expansions1),
-	inst_list_matches_initial(Xs, Ys, ModuleInfo, Expansions1, Expansions).
+inst_list_matches_initial([], [], []) --> [].
+inst_list_matches_initial([X|Xs], [Y|Ys], [Type | Types]) -->
+	inst_matches_initial_2(X, Y, Type),
+	inst_list_matches_initial(Xs, Ys, Types).
+
+:- pred maybe_get_cons_id_arg_types(module_info, maybe(type), cons_id,
+		list(maybe(type))).
+:- mode maybe_get_cons_id_arg_types(in, in, in, out) is det.
+
+maybe_get_cons_id_arg_types(ModuleInfo, MaybeType, ConsId0, MaybeTypes) :-
+	( ConsId0 = cons(SymName, Arity) ->
+		( SymName = qualified(_, Name) ->
+			% type_util__get_cons_id_arg_types expects an 
+			% unqualified cons_id.
+			ConsId = cons(unqualified(Name), Arity)
+		;
+			ConsId = ConsId0
+		),
+		(
+			MaybeType = yes(Type),
+			type_util__get_cons_id_arg_types(ModuleInfo, Type,
+				ConsId, Types),
+			list__length(Types, Arity)
+		->
+			list__map(pred(T::in, yes(T)::out) is det, Types,
+				MaybeTypes)
+		;
+			list__duplicate(Arity, no, MaybeTypes)
+		)
+	;
+		MaybeTypes = []
+	).
+
+:- pred maybe_get_higher_order_arg_types(maybe(type), arity, list(maybe(type))).
+:- mode maybe_get_higher_order_arg_types(in, in, out) is det.
+
+maybe_get_higher_order_arg_types(MaybeType, Arity, MaybeTypes) :-
+	(
+		MaybeType = yes(Type),
+		type_is_higher_order(Type, _, _, Types)
+	->
+		list__map(pred(T::in, yes(T)::out) is det, Types, MaybeTypes)
+	;
+		list__duplicate(Arity, no, MaybeTypes)
+	).
 
 %-----------------------------------------------------------------------------%
 
@@ -533,105 +759,108 @@
 
 %-----------------------------------------------------------------------------%
 
-inst_matches_final(InstA, InstB, ModuleInfo) :-
-	set__init(Expansions0),
-	inst_matches_final_2(InstA, InstB, ModuleInfo,
-		Expansions0, _Expansions).
+inst_matches_final(InstA, InstB, Type, ModuleInfo) :-
+	Info0 = init_inst_match_info(ModuleInfo),
+	inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
 
-:- pred inst_matches_final_2(inst, inst, module_info, expansions, expansions).
+:- pred inst_matches_final_2(inst, inst, maybe(type),
+		inst_match_info, inst_match_info).
 :- mode inst_matches_final_2(in, in, in, in, out) is semidet.
 
-inst_matches_final_2(InstA, InstB, ModuleInfo, Expansions0, Expansions) :-
+inst_matches_final_2(InstA, InstB, MaybeType, Info0, Info) :-
 	ThisExpansion = InstA - InstB,
-	( set__member(ThisExpansion, Expansions0) ->
-		Expansions = Expansions0
+	( set__member(ThisExpansion, Info0^expansions) ->
+		Info = Info0
 	; InstA = InstB ->
-		Expansions = Expansions0
+		Info = Info0
 	;
-		inst_expand(ModuleInfo, InstA, InstA2),
-		inst_expand(ModuleInfo, InstB, InstB2),
-		set__insert(Expansions0, ThisExpansion, Expansions1),
-		inst_matches_final_3(InstA2, InstB2, ModuleInfo,
-			Expansions1, Expansions)
+		inst_expand(Info0^module_info, InstA, InstA2),
+		inst_expand(Info0^module_info, InstB, InstB2),
+		set__insert(Info0^expansions, ThisExpansion, Expansions1),
+		inst_matches_final_3(InstA2, InstB2, MaybeType,
+			Info0^expansions := Expansions1, Info)
 	).
 
-:- pred inst_matches_final_3(inst, inst, module_info, expansions, expansions).
+:- pred inst_matches_final_3(inst, inst, maybe(type),
+		inst_match_info, inst_match_info).
 :- mode inst_matches_final_3(in, in, in, in, out) is semidet.
 
-inst_matches_final_3(any(UniqA), any(UniqB), _, Expansions, Expansions) :-
+inst_matches_final_3(any(UniqA), any(UniqB), _, I, I) :-
 	unique_matches_final(UniqA, UniqB).
-inst_matches_final_3(free, any(Uniq), _, Expansions, Expansions) :-
+inst_matches_final_3(free, any(Uniq), _, I, I) :-
 	% We do not yet allow `free' to match `any',
 	% unless the `any' is `clobbered_any' or `mostly_clobbered_any'.
 	% Among other things, changing this would break compare_inst
 	% in modecheck_call.m.
 	( Uniq = clobbered ; Uniq = mostly_clobbered ).
-inst_matches_final_3(free, free, _, Expansions, Expansions).
-inst_matches_final_3(bound(UniqA, ListA), any(UniqB), ModuleInfo,
-		Expansions, Expansions) :-
+inst_matches_final_3(free, free, _, I, I).
+inst_matches_final_3(bound(UniqA, ListA), any(UniqB), _, Info, Info) :-
 	unique_matches_final(UniqA, UniqB),
-	bound_inst_list_matches_uniq(ListA, UniqB, ModuleInfo),
+	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info),
 	% We do not yet allow `free' to match `any'.
 	% Among other things, changing this would break compare_inst
 	% in modecheck_call.m.
-	bound_inst_list_is_ground_or_any(ListA, ModuleInfo).
-inst_matches_final_3(bound(UniqA, ListA), bound(UniqB, ListB), ModuleInfo,
-		Expansions0, Expansions) :-
+	bound_inst_list_is_ground_or_any(ListA, Info^module_info).
+inst_matches_final_3(bound(UniqA, ListA), bound(UniqB, ListB), MaybeType,
+		Info0, Info) :-
 	unique_matches_final(UniqA, UniqB),
-	bound_inst_list_matches_final(ListA, ListB, ModuleInfo,
-		Expansions0, Expansions).
-inst_matches_final_3(bound(UniqA, ListA), ground(UniqB, no), ModuleInfo,
-		Expansions, Expansions) :-
+	bound_inst_list_matches_final(ListA, ListB, MaybeType, Info0, Info).
+inst_matches_final_3(bound(UniqA, ListA), ground(UniqB, none), _,
+		Info, Info) :-
 	unique_matches_final(UniqA, UniqB),
-	bound_inst_list_is_ground(ListA, ModuleInfo),
-	bound_inst_list_matches_uniq(ListA, UniqB, ModuleInfo).
-inst_matches_final_3(ground(UniqA, _), any(UniqB), _ModuleInfo,
-		Expansions, Expansions) :-
+	bound_inst_list_is_ground(ListA, Info^module_info),
+	bound_inst_list_matches_uniq(ListA, UniqB, Info^module_info).
+inst_matches_final_3(ground(UniqA, _), any(UniqB), _, I, I) :-
 	unique_matches_final(UniqA, UniqB).
-inst_matches_final_3(ground(UniqA, _), bound(UniqB, ListB), ModuleInfo,
-		Expansions, Expansions) :-
+inst_matches_final_3(ground(UniqA, _), bound(UniqB, ListB), MaybeType,
+		Info, Info) :-
 	unique_matches_final(UniqA, UniqB),
-	bound_inst_list_is_ground(ListB, ModuleInfo),
-	uniq_matches_bound_inst_list(UniqA, ListB, ModuleInfo).
-		% XXX BUG! Should fail if there are not_reached
-		% insts in ListB, or if ListB does not contain a complete list
-		% of all the constructors for the type in question.
-	%%% error("not implemented: `ground' matches_final `bound(...)'").
-inst_matches_final_3(ground(UniqA, PredInstA), ground(UniqB, PredInstB),
-		ModuleInfo, Expansions0, Expansions) :-
-	maybe_pred_inst_matches_final(PredInstA, PredInstB,
-		ModuleInfo, Expansions0, Expansions),
+	bound_inst_list_is_ground(ListB, Info^module_info),
+	uniq_matches_bound_inst_list(UniqA, ListB, Info^module_info),
+	(
+		MaybeType = yes(Type),
+		% We can only do this check if the type is known.
+		bound_inst_list_is_complete_for_type(set__init,
+			Info^module_info, ListB, Type)
+	;
+		true
+		% XXX enabling the check for bound_inst_list_is_complete
+		% for type makes the mode checker too conservative in
+		% the absence of alias tracking, so we currently always
+		% succeed, even if this check fails.
+	).
+inst_matches_final_3(ground(UniqA, GroundInstInfoA),
+		ground(UniqB, GroundInstInfoB), MaybeType, Info0, Info) :-
+	ground_inst_info_matches_final(GroundInstInfoA, GroundInstInfoB,
+		MaybeType, Info0, Info),
 	unique_matches_final(UniqA, UniqB).
-inst_matches_final_3(abstract_inst(_, _), any(shared), _,
-		Expansions, Expansions).
+inst_matches_final_3(abstract_inst(_, _), any(shared), _, I, I).
 inst_matches_final_3(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
-		ModuleInfo, Expansions0, Expansions) :-
-	inst_list_matches_final(ArgsA, ArgsB, ModuleInfo,
-		Expansions0, Expansions).
-inst_matches_final_3(not_reached, _, _, Expansions, Expansions).
+		_MaybeType, Info0, Info) :-
+	list__duplicate(length(ArgsA), no, MaybeTypes),
+		% 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).
+
+:- pred ground_inst_info_matches_final(ground_inst_info, ground_inst_info,
+		maybe(type), inst_match_info, inst_match_info).
+:- mode ground_inst_info_matches_final(in, in, in, in, out) is semidet.
+
+ground_inst_info_matches_final(_, none, _) --> [].
+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 maybe_pred_inst_matches_final(maybe(pred_inst_info),
-		maybe(pred_inst_info), module_info, expansions, expansions).
-:- mode maybe_pred_inst_matches_final(in, in, in, in, out) is semidet.
-
-maybe_pred_inst_matches_final(no, no, _, Expansions, Expansions).
-maybe_pred_inst_matches_final(yes(_), no, _, Expansions, Expansions).
-maybe_pred_inst_matches_final(yes(PredInstA), yes(PredInstB),
-		ModuleInfo, Expansions0, Expansions) :-
-	pred_inst_matches_2(PredInstA, PredInstB, ModuleInfo,
-		Expansions0, Expansions).
-
-:- pred inst_list_matches_final(list(inst), list(inst), module_info,
-				expansions, expansions).
+:- pred inst_list_matches_final(list(inst), list(inst), list(maybe(type)),
+		inst_match_info, inst_match_info).
 :- mode inst_list_matches_final(in, in, in, in, out) is semidet.
 
-inst_list_matches_final([], [], _ModuleInfo, Expansions, Expansions).
-inst_list_matches_final([ArgA | ArgsA], [ArgB | ArgsB], ModuleInfo,
-			Expansions0, Expansions) :-
-	inst_matches_final_2(ArgA, ArgB, ModuleInfo,
-		Expansions0, Expansions1),
-	inst_list_matches_final(ArgsA, ArgsB, ModuleInfo,
-		Expansions1, Expansions).
+inst_list_matches_final([], [], []) --> [].
+inst_list_matches_final([ArgA | ArgsA], [ArgB | ArgsB], [Type | Types]) -->
+	inst_matches_final_2(ArgA, ArgB, Type),
+	inst_list_matches_final(ArgsA, ArgsB, Types).
 
 	% Here we check that the functors in the first list are a
 	% subset of the functors in the second list. 
@@ -643,98 +872,110 @@
 	% are sorted.
 
 :- pred bound_inst_list_matches_final(list(bound_inst), list(bound_inst),
-				module_info, expansions, expansions).
+				maybe(type), inst_match_info, inst_match_info).
 :- mode bound_inst_list_matches_final(in, in, in, in, out) is semidet.
 
-bound_inst_list_matches_final([], _, _, Expansions, Expansions).
-bound_inst_list_matches_final([X|Xs], [Y|Ys], ModuleInfo,
-		Expansions0, Expansions) :-
-	X = functor(ConsIdX, ArgsX),
-	Y = functor(ConsIdY, ArgsY),
-	( ConsIdX = ConsIdY ->
-		inst_list_matches_final(ArgsX, ArgsY, ModuleInfo,
-			Expansions0, Expansions1),
-		bound_inst_list_matches_final(Xs, Ys, ModuleInfo,
-			Expansions1, Expansions)
+bound_inst_list_matches_final([], _, _) --> [].
+bound_inst_list_matches_final([X|Xs], [Y|Ys], MaybeType) -->
+	{ X = functor(ConsIdX, ArgsX) },
+	{ Y = functor(ConsIdY, ArgsY) },
+	( { ConsIdX = ConsIdY } ->
+		ModuleInfo =^ module_info,
+		{ maybe_get_cons_id_arg_types(ModuleInfo, MaybeType, ConsIdX,
+			MaybeTypes) },
+		inst_list_matches_final(ArgsX, ArgsY, MaybeTypes),
+		bound_inst_list_matches_final(Xs, Ys, MaybeType)
 	;
-		compare(>, ConsIdX, ConsIdY),
+		{ compare(>, ConsIdX, ConsIdY) },
 			% ConsIdY does not occur in [X|Xs].
 			% Hence [X|Xs] implicitly specifies `not_reached'
 			% for the args of ConsIdY, and hence 
 			% automatically matches_final Y.  We just need to
 			% check that [X|Xs] matches_final Ys.
-		bound_inst_list_matches_final([X|Xs], Ys, ModuleInfo,
-			Expansions0, Expansions)
+		bound_inst_list_matches_final([X|Xs], Ys, MaybeType)
 	).
 
-inst_matches_binding(InstA, InstB, ModuleInfo) :-
-	set__init(Expansions0),
-	inst_matches_binding_2(InstA, InstB, ModuleInfo,
-		Expansions0, _Expansions).
+inst_matches_binding(InstA, InstB, Type, ModuleInfo) :-
+	Info0 = init_inst_match_info(ModuleInfo),
+	inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
 
-:- pred inst_matches_binding_2(inst, inst, module_info, expansions, expansions).
+:- pred inst_matches_binding_2(inst, inst, maybe(type), inst_match_info,
+		inst_match_info).
 :- mode inst_matches_binding_2(in, in, in, in, out) is semidet.
 
-inst_matches_binding_2(InstA, InstB, ModuleInfo, Expansions0, Expansions) :-
+inst_matches_binding_2(InstA, InstB, MaybeType, Info0, Info) :-
 	ThisExpansion = InstA - InstB,
-	( set__member(ThisExpansion, Expansions0) ->
-		Expansions = Expansions0
+	( set__member(ThisExpansion, Info0^expansions) ->
+		Info = Info0
 	;
-		inst_expand(ModuleInfo, InstA, InstA2),
-		inst_expand(ModuleInfo, InstB, InstB2),
-		set__insert(Expansions0, ThisExpansion, Expansions1),
-		inst_matches_binding_3(InstA2, InstB2, ModuleInfo,
-			Expansions1, Expansions)
+		inst_expand(Info0^module_info, InstA, InstA2),
+		inst_expand(Info0^module_info, InstB, InstB2),
+		set__insert(Info0^expansions, ThisExpansion, Expansions1),
+		inst_matches_binding_3(InstA2, InstB2, MaybeType,
+			Info0^expansions := Expansions1, Info)
 	).
 
-:- pred inst_matches_binding_3(inst, inst, module_info, expansions, expansions).
+:- pred inst_matches_binding_3(inst, inst, maybe(type), inst_match_info,
+		inst_match_info).
 :- mode inst_matches_binding_3(in, in, in, in, out) is semidet.
 
 % Note that `any' is *not* considered to match `any'.
-inst_matches_binding_3(free, free, _, Expansions, Expansions).
-inst_matches_binding_3(bound(_UniqA, ListA), bound(_UniqB, ListB), ModuleInfo,
-		Expansions0, Expansions) :-
-	bound_inst_list_matches_binding(ListA, ListB, ModuleInfo,
-		Expansions0, Expansions).
-inst_matches_binding_3(bound(_UniqA, ListA), ground(_UniqB, no), ModuleInfo,
-		Expansions, Expansions) :-
-	bound_inst_list_is_ground(ListA, ModuleInfo).
-inst_matches_binding_3(ground(_UniqA, _), bound(_UniqB, ListB), ModuleInfo,
-		Expansions, Expansions) :-
-	bound_inst_list_is_ground(ListB, ModuleInfo).
-		% XXX BUG! Should fail if there are not_reached
-		% insts in ListB, or if ListB does not contain a complete list
-		% of all the constructors for the type in question.
-	%%% error("not implemented: `ground' matches_binding `bound(...)'").
-inst_matches_binding_3(ground(_UniqA, PredInstA), ground(_UniqB, PredInstB),
-		ModuleInfo, Expansions, Expansions) :-
-	pred_inst_matches_binding(PredInstA, PredInstB, ModuleInfo).
+inst_matches_binding_3(free, free, _, I, I).
+inst_matches_binding_3(bound(_UniqA, ListA), bound(_UniqB, ListB), MaybeType,
+		Info0, Info) :-
+	bound_inst_list_matches_binding(ListA, ListB, MaybeType, Info0, Info).
+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),
+	(
+		MaybeType = yes(Type),
+		% We can only do this check if the type is known.
+		bound_inst_list_is_complete_for_type(set__init,
+			Info^module_info, ListB, Type)
+	;
+		true
+		% XXX enabling the check for bound_inst_list_is_complete
+		% for type makes the mode checker too conservative in
+		% the absence of alias tracking, so we currently always
+		% succeed, even if this check fails.
+	).
+inst_matches_binding_3(ground(_UniqA, GroundInstInfoA),
+		ground(_UniqB, GroundInstInfoB), MaybeType, Info, Info) :-
+	ground_inst_info_matches_binding(GroundInstInfoA, GroundInstInfoB,
+		MaybeType, Info^module_info).
 inst_matches_binding_3(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
-		ModuleInfo, Expansions0, Expansions) :-
-	inst_list_matches_binding(ArgsA, ArgsB, ModuleInfo,
-		Expansions0, Expansions).
-inst_matches_binding_3(not_reached, _, _, Expansions, Expansions).
+		_MaybeType, Info0, Info) :-
+	list__duplicate(length(ArgsA), no, MaybeTypes),
+		% XXX how do we get the argument types for an abstract inst?
+	inst_list_matches_binding(ArgsA, ArgsB, MaybeTypes, Info0, Info).
+inst_matches_binding_3(not_reached, _, _, I, I).
+
+:- pred ground_inst_info_matches_binding(ground_inst_info, ground_inst_info,
+		maybe(type), module_info).
+:- mode ground_inst_info_matches_binding(in, in, in, in) is semidet.
+
+ground_inst_info_matches_binding(_, none, _, _).
+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 pred_inst_matches_binding(maybe(pred_inst_info), maybe(pred_inst_info),
-		module_info).
-:- mode pred_inst_matches_binding(in, in, in) is semidet.
-
-pred_inst_matches_binding(no, no, _).
-pred_inst_matches_binding(yes(_), no, _).
-pred_inst_matches_binding(yes(PredInstA), yes(PredInstB), ModuleInfo) :-
-	pred_inst_matches(PredInstA, PredInstB, ModuleInfo).
-
-:- pred inst_list_matches_binding(list(inst), list(inst), module_info,
-				expansions, expansions).
+:- pred inst_list_matches_binding(list(inst), list(inst), list(maybe(type)),
+		inst_match_info, inst_match_info).
 :- mode inst_list_matches_binding(in, in, in, in, out) is semidet.
 
-inst_list_matches_binding([], [], _ModuleInfo, Expansions, Expansions).
-inst_list_matches_binding([ArgA | ArgsA], [ArgB | ArgsB], ModuleInfo,
-			Expansions0, Expansions) :-
-	inst_matches_binding_2(ArgA, ArgB, ModuleInfo,
-		Expansions0, Expansions1),
-	inst_list_matches_binding(ArgsA, ArgsB, ModuleInfo,
-		Expansions1, Expansions).
+inst_list_matches_binding([], [], []) --> [].
+inst_list_matches_binding([ArgA | ArgsA], [ArgB | ArgsB],
+		[MaybeType | MaybeTypes]) -->
+	inst_matches_binding_2(ArgA, ArgB, MaybeType),
+	inst_list_matches_binding(ArgsA, ArgsB, MaybeTypes).
 
 	% Here we check that the functors in the first list are a
 	% subset of the functors in the second list. 
@@ -746,28 +987,27 @@
 	% are sorted.
 
 :- pred bound_inst_list_matches_binding(list(bound_inst), list(bound_inst),
-					module_info, expansions, expansions).
+			maybe(type), inst_match_info, inst_match_info).
 :- mode bound_inst_list_matches_binding(in, in, in, in, out) is semidet.
 
-bound_inst_list_matches_binding([], _, _, Expansions, Expansions).
-bound_inst_list_matches_binding([X|Xs], [Y|Ys], ModuleInfo,
-		Expansions0, Expansions) :-
-	X = functor(ConsIdX, ArgsX),
-	Y = functor(ConsIdY, ArgsY),
-	( ConsIdX = ConsIdY ->
-		inst_list_matches_binding(ArgsX, ArgsY, ModuleInfo,
-			Expansions0, Expansions1),
-		bound_inst_list_matches_binding(Xs, Ys, ModuleInfo,
-			Expansions1, Expansions)
+bound_inst_list_matches_binding([], _, _) --> [].
+bound_inst_list_matches_binding([X|Xs], [Y|Ys], MaybeType) -->
+	{ X = functor(ConsIdX, ArgsX) },
+	{ Y = functor(ConsIdY, ArgsY) },
+	( { ConsIdX = ConsIdY } ->
+		ModuleInfo =^ module_info,
+		{ maybe_get_cons_id_arg_types(ModuleInfo, MaybeType, ConsIdX,
+			MaybeTypes) },
+		inst_list_matches_binding(ArgsX, ArgsY, MaybeTypes),
+		bound_inst_list_matches_binding(Xs, Ys, MaybeType)
 	;
-		compare(>, ConsIdX, ConsIdY),
+		{ compare(>, ConsIdX, ConsIdY) },
 			% ConsIdX does not occur in [X|Xs].
 			% Hence [X|Xs] implicitly specifies `not_reached'
 			% for the args of ConsIdY, and hence 
 			% automatically matches_binding Y.  We just need to
 			% check that [X|Xs] matches_binding Ys.
-		bound_inst_list_matches_binding([X|Xs], Ys, ModuleInfo,
-			Expansions0, Expansions)
+		bound_inst_list_matches_binding([X|Xs], Ys, MaybeType)
 	).
 
 %-----------------------------------------------------------------------------%
@@ -1392,8 +1632,8 @@
 	inst_name_contains_inst_var(InstName, InstVar).
 inst_contains_inst_var(bound(_Uniq, ArgInsts), InstVar) :-
 	bound_inst_list_contains_inst_var(ArgInsts, InstVar).
-inst_contains_inst_var(ground(_Uniq, PredInstInfo), InstVar) :-
-	PredInstInfo = yes(pred_inst_info(_PredOrFunc, Modes, _Det)),
+inst_contains_inst_var(ground(_Uniq, GroundInstInfo), InstVar) :-
+	GroundInstInfo = higher_order(pred_inst_info(_PredOrFunc, Modes, _Det)),
 	mode_list_contains_inst_var(Modes, InstVar).
 inst_contains_inst_var(abstract_inst(_Name, ArgInsts), InstVar) :-
 	inst_list_contains_inst_var(ArgInsts, InstVar).
--- inst_util.m	Mon Mar  6 14:31:45 2000
+++ ../mercury/compiler/inst_util.m	Mon Mar  6 14:41:58 2000
@@ -297,9 +297,6 @@
 abstractly_unify_inst_3(live, ground(UniqX, constrained_inst_var(Var)),
 		any(UniqY), Real, M, ground(Uniq, constrained_inst_var(Var)),
 		semidet, M) :-
-	Real = fake_unify, 
-		% If Real \= fake_unify then we must fail because the inst vars
-		% may represent higher order insts.
 	unify_uniq(live, Real, det, UniqX, UniqY, Uniq).
 
 abstractly_unify_inst_3(live, ground(Uniq0, constrained_inst_var(Var)), free,
@@ -432,7 +429,6 @@
 abstractly_unify_inst_3(dead, ground(UniqA, constrained_inst_var(_Var)),
 				ground(UniqB, GroundInstInfo), Real, M,
 				ground(Uniq, GroundInstInfo), det, M) :-
-	Real = fake_unify,
 	unify_uniq(dead, Real, det, UniqA, UniqB, Uniq).
 
 /***** abstract insts aren't really supported
--- mode_util.m	Mon Mar  6 14:31:45 2000
+++ ../mercury/compiler/mode_util.m	Mon Mar  6 14:43:25 2000
@@ -1458,8 +1458,8 @@
 			ArgModes2) },
 
 		% Calculate the final insts of the argument variables
-		% from their initial insts and the final insts of called
-		% procedure (with inst_var substitutions applied.
+		% from their initial insts and the final insts of the called
+		% procedure (with inst_var substitutions applied).
 		lift(recompute_instmap_delta_call_2(Args, InstMap,
 			ArgModes2), ArgModes),
 		{ instmap_delta_from_mode_list(Args, ArgModes,
--- modes.m	Mon Mar  6 14:31:45 2000
+++ ../mercury/compiler/modes.m	Mon Mar  6 10:12:34 2000
@@ -614,7 +614,8 @@
 					ModuleInfo0),
 			{ NumErrors0 = 0 }
 		;
-			{ special_pred_name_arity(unify, _, PredName, Arity) },
+			{ special_pred_name_arity(unify, _, PredName,
+				PredArity) },
 			{ pred_info_name(PredInfo0, PredName) },
 			{ pred_info_arity(PredInfo0, PredArity) }
 		->

Index: invalid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/invalid/Mmakefile,v
retrieving revision 1.57
diff -u -r1.57 Mmakefile
--- invalid/Mmakefile	2000/01/13 06:19:33	1.57
+++ invalid/Mmakefile	2000/03/06 05:43:52
@@ -69,7 +69,6 @@
 	typeclass_test_9.m \
 	types.m	\
 	type_spec.m \
-	unbound_inst_var.m \
 	undef_lambda_mode.m \
 	undef_mode.m \
 	undef_symbol.m \
Index: invalid/unbound_inst_var.err_exp
===================================================================
RCS file: unbound_inst_var.err_exp
diff -N unbound_inst_var.err_exp
--- /tmp/cvs03359baa	Mon Mar  6 17:25:02 2000
+++ /dev/null	Thu Mar  4 04:20:11 1999
@@ -1,5 +0,0 @@
-unbound_inst_var.m:019: In mode declaration for predicate `unbound_inst_var:test/1':
-unbound_inst_var.m:019:   error: unbound inst variable(s).
-unbound_inst_var.m:019:   (Sorry, polymorphic modes are not supported.)
-unbound_inst_var.m:018: Error: no mode declaration for predicate `unbound_inst_var:test/1'.
-For more information, try recompiling with `-E'.
Index: invalid/unbound_inst_var.m
===================================================================
RCS file: unbound_inst_var.m
diff -N unbound_inst_var.m
--- /tmp/cvs03359caa	Mon Mar  6 17:25:02 2000
+++ /dev/null	Thu Mar  4 04:20:11 1999
@@ -1,29 +0,0 @@
-:- module unbound_inst_var.
-
-:- interface.
-
-:- import_module io.
-
-:- pred main(io__state,io__state).
-:- mode main(di,uo) is det.
-
-:- implementation.
-
-:- import_module char.
-
-:- type all(X) ---> a(X) ; b ; c ; d.
-
-:- inst all(X) ---> a(X) ; ground.
-
-:- pred test(all(char)).
-:- mode test(in(all(_))) is det.
-
-test(_) :- true.
-
-%:- pred main(io__state,io__state).
-%:- mode main(di,uo) is det.
-
-main(IO,IO) :-
-  true.
-
-:- end_module unbound_inst_var.
Index: valid/Mmakefile
===================================================================
RCS file: /home/mercury1/repository/tests/valid/Mmakefile,v
retrieving revision 1.57
diff -u -r1.57 Mmakefile
--- valid/Mmakefile	2000/02/22 10:56:39	1.57
+++ valid/Mmakefile	2000/03/06 05:44:24
@@ -123,6 +123,7 @@
 	two_pragma_c_codes.m \
 	two_way_unif.m \
 	type_inf_ambig_test.m \
+	unbound_inst_var.m \
 	unbound_tvar_in_lambda.m \
 	undead_proc.m \
 	uniq_unify.m \
Index: valid/unbound_inst_var.m
===================================================================
RCS file: unbound_inst_var.m
diff -N unbound_inst_var.m
--- /dev/null	Thu Mar  4 04:20:11 1999
+++ unbound_inst_var.m	Mon Mar  6 17:02:24 2000
@@ -0,0 +1,36 @@
+:- module unbound_inst_var.
+
+:- interface.
+
+:- import_module io.
+
+:- pred main(io__state,io__state).
+:- mode main(di,uo) is det.
+
+:- implementation.
+
+:- import_module char.
+
+:- type all(X) ---> a(X).
+
+:- inst all(X) ---> a(X).
+
+:- pred test(all(char), all(char)).
+:- mode test(in(all(I)), out(all(I))) is det.
+
+:- pred try_test is det.
+
+test(X, X).
+
+%:- pred main(io__state,io__state).
+%:- mode main(di,uo) is det.
+
+main(IO,IO) :-
+	true.
+
+try_test :-
+  ( C = a ; C = b ; C = c),
+  test(a(C), a(D)),
+  ( D = a ; D = b ; D = c).
+
+:- end_module unbound_inst_var.

-- 
David Overton       Department of Computer Science & Software Engineering
PhD Student         The University of Melbourne, Victoria 3010, Australia
+61 3 8344 9159     http://www.cs.mu.oz.au/~dmo
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------



More information about the developers mailing list