[m-rev.] for review: try_and_insert

Zoltan Somogyi zs at unimelb.edu.au
Thu Mar 29 18:35:40 AEDT 2012


I have already discussed with Ian the name of the predicate, try_and_insert,
that implements the new operation. Does anyone have any better ideas?

Zoltan.

compiler/inst_match.m:
	Instead of first testing whether an inst exists in a set
	and then inserting it if does not, use a single predicate
	that does both the membership test and the insertion (if
	the membership test failed) in one pass.

	This speeds up compilation of one version of the rcpsp_cpx
	stress test by about 9%, with negligible effect on tools/speedtest.

library/*set*.m:
	Implement this try_and_insert predicate for all the implementations
	of sets we have. The code in each case is copied from the code
	of insert, with code to return a set unchanged replaced with `fail'.

cvs diff: Diffing .
cvs diff: Diffing analysis
cvs diff: Diffing bindist
cvs diff: Diffing boehm_gc
cvs diff: Diffing boehm_gc/Mac_files
cvs diff: Diffing boehm_gc/cord
cvs diff: Diffing boehm_gc/cord/private
cvs diff: Diffing boehm_gc/doc
cvs diff: Diffing boehm_gc/extra
cvs diff: Diffing boehm_gc/include
cvs diff: Diffing boehm_gc/include/extra
cvs diff: Diffing boehm_gc/include/private
cvs diff: Diffing boehm_gc/libatomic_ops
cvs diff: Diffing boehm_gc/libatomic_ops/doc
cvs diff: Diffing boehm_gc/libatomic_ops/src
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps/armcc
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps/gcc
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps/hpc
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps/ibmc
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps/icc
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps/msftc
cvs diff: Diffing boehm_gc/libatomic_ops/src/atomic_ops/sysdeps/sunc
cvs diff: Diffing boehm_gc/libatomic_ops/tests
cvs diff: Diffing boehm_gc/libatomic_ops-1.2
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/doc
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src/atomic_ops
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src/atomic_ops/sysdeps
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/tests
cvs diff: Diffing boehm_gc/m4
cvs diff: Diffing boehm_gc/tests
cvs diff: Diffing browser
cvs diff: Diffing bytecode
cvs diff: Diffing compiler
Index: compiler/inst_match.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/inst_match.m,v
retrieving revision 1.96
diff -u -b -r1.96 inst_match.m
--- compiler/inst_match.m	27 Mar 2012 23:21:27 -0000	1.96
+++ compiler/inst_match.m	29 Mar 2012 07:16:39 -0000
@@ -15,12 +15,12 @@
 % rafe: XXX The following comment needs revising in the light of
 % the new solver types design.
 %
-% The handling of `any' insts is not complete. (See also inst_util.m) It would
-% be nice to allow `free' to match `any', but right now we only allow a few
-% special cases of that. The reason is that although the mode analysis would be
-% pretty straight-forward, generating the correct code is quite a bit trickier.
-% modes.m would have to be changed to handle the implicit conversions from
-% `free'/`bound'/`ground' to `any' at
+% The handling of `any' insts is not complete. (See also inst_util.m).
+% It would be nice to allow `free' to match `any', but right now we only allow
+% a few special cases of that. The reason is that although the mode analysis
+% would be pretty straight-forward, generating the correct code is quite a bit
+% trickier. modes.m would have to be changed to handle the implicit conversions
+% from `free'/`bound'/`ground' to `any' at
 %
 %   (1) procedure calls (this is just an extension of implied modes)
 %       currently we support only the easy cases of this
@@ -49,9 +49,8 @@
 
 %-----------------------------------------------------------------------------%
 
-    % inst_expand(ModuleInfo, Inst0, Inst) checks if the top-level
-    % part of the inst is a defined inst, and if so replaces it
-    % with the definition.
+    % inst_expand(ModuleInfo, Inst0, Inst) checks if the top-level part
+    % of the inst is a defined inst, and if so replaces it with the definition.
     %
 :- pred inst_expand(module_info::in, mer_inst::in, mer_inst::out) is det.
 
@@ -152,7 +151,7 @@
     %
 :- pred unique_matches_final(uniqueness::in, uniqueness::in) is semidet.
 
-    % inst_matches_binding(InstA, InstB, ModuleInfo):
+    % inst_matches_binding(InstA, InstB, Type, ModuleInfo):
     %
     % Succeed iff the binding of InstA is definitely exactly the same as
     % that of InstB. This is the same as inst_matches_final except that it
@@ -182,13 +181,13 @@
 
 %-----------------------------------------------------------------------------%
 %
-% Predicates to test various properties of insts
+% Predicates to test various properties of insts.
 %
 % NOTE: `not_reached' insts are considered to satisfy all of these predicates
 % except inst_is_clobbered.
 %
 
-    % succeed if the inst is fully ground (i.e. contains only `ground',
+    % Succeed if the inst is fully ground (i.e. contains only `ground',
     % `bound', and `not_reached' insts, with no `free' or `any' insts).
     % This predicate succeeds for non-standard function insts so some care
     % needs to be taken since these insts may not be replaced by a less
@@ -196,7 +195,7 @@
     %
 :- pred inst_is_ground(module_info::in, mer_inst::in) is semidet.
 
-    % succeed if the inst is not partly free (i.e. contains only `any',
+    % Succeed if the inst is not partly free (i.e. contains only `any',
     % `ground', `bound', and `not_reached' insts, with no `free' insts).
     % This predicate succeeds for non-standard function insts so some care
     % needs to be taken since these insts may not be replaced by a less
@@ -389,10 +388,10 @@
     % comparing two uniqueness annotations.
 
 :- type uniqueness_comparison
-    --->    match
+    --->    uc_match
             % We are doing a "matches" comparison, e.g. at a predicate call
             % or the end of a procedure body.
-    ;       instantiated.
+    ;       uc_instantiated.
             % We are comparing two insts for how "instantiated" they are.
             % The uniqueness order here should be the reverse of the order
             % used for matching.
@@ -410,17 +409,17 @@
     % The calculate_sub type determines how the inst var substitution
     % should be calculated.
 :- type calculate_sub
-    --->    forward
+    --->    cs_forward
             % Calculate in the (normal) forward direction
             % (used by inst_matches_initial).
 
-    ;       reverse
+    ;       cs_reverse
             % Calculate in the reverse direction. Used by the call
             % to inst_matches_final from pred_inst_argmodes_match
             % to ensure contravariance of the initial argument
             % insts of higher order pred insts.
 
-    ;       none.
+    ;       cs_none.
             % Do not calculate inst var substitions.
 
 :- func init_inst_match_info(module_info, maybe(inst_var_sub),
@@ -448,9 +447,9 @@
 
 :- func swap_calculate_sub(calculate_sub) = calculate_sub.
 
-swap_calculate_sub(forward) = reverse.
-swap_calculate_sub(reverse) = forward.
-swap_calculate_sub(none) = none.
+swap_calculate_sub(cs_forward) = cs_reverse.
+swap_calculate_sub(cs_reverse) = cs_forward.
+swap_calculate_sub(cs_none) = cs_none.
 
 :- pred swap_args(inst_matches_pred::in(inst_matches_pred),
     mer_inst::in, mer_inst::in, maybe(mer_type)::in,
@@ -470,15 +469,15 @@
 handle_inst_var_subs(Recurse, Continue, InstA, InstB, Type, !Info) :-
     CalculateSub = !.Info ^ imi_calculate_sub,
     (
-        CalculateSub = forward,
+        CalculateSub = cs_forward,
         handle_inst_var_subs_2(Recurse, Continue, InstA, InstB,
             Type, !Info)
     ;
-        CalculateSub = reverse,
+        CalculateSub = cs_reverse,
         handle_inst_var_subs_2(swap_args(Recurse), swap_args(Continue),
             InstB, InstA, Type, !Info)
     ;
-        CalculateSub = none,
+        CalculateSub = cs_none,
         Continue(InstA, InstB, Type, !Info)
     ).
 
@@ -568,14 +567,14 @@
     ).
 
 inst_matches_initial_no_implied_modes(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo, no, forward, match, yes),
-    inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
+    Info0 = init_inst_match_info(ModuleInfo, no, cs_forward, uc_match, yes),
+    inst_matches_final_mt(InstA, InstB, yes(Type), Info0, _).
 
 inst_matches_initial_no_implied_modes_sub(InstA, InstB, Type,
         !ModuleInfo, !Sub) :-
-    Info0 = init_inst_match_info(!.ModuleInfo, yes(!.Sub), forward,
-        match, yes),
-    inst_matches_final_2(InstA, InstB, yes(Type), Info0, Info),
+    Info0 = init_inst_match_info(!.ModuleInfo, yes(!.Sub), cs_forward,
+        uc_match, yes),
+    inst_matches_final_mt(InstA, InstB, yes(Type), Info0, Info),
     !:ModuleInfo = Info ^ imi_module_info,
     yes(!:Sub) = Info ^ imi_maybe_sub.
 
@@ -584,105 +583,140 @@
     maybe(inst_var_sub)::in, maybe(inst_var_sub)::out) is semidet.
 
 inst_matches_initial_1(InstA, InstB, Type, !ModuleInfo, !MaybeSub) :-
-    Info0 = init_inst_match_info(!.ModuleInfo, !.MaybeSub, forward,
-        match, yes),
-    inst_matches_initial_2(InstA, InstB, yes(Type), Info0, Info),
+    Info0 = init_inst_match_info(!.ModuleInfo, !.MaybeSub, cs_forward,
+        uc_match, yes),
+    inst_matches_initial_mt(InstA, InstB, yes(Type), Info0, Info),
     !:ModuleInfo = Info ^ imi_module_info,
     !:MaybeSub = Info ^ imi_maybe_sub.
 
-:- pred inst_matches_initial_2(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
-    inst_match_info::in, inst_match_info::out) is semidet.
+:- pred inst_matches_initial_mt(mer_inst::in, mer_inst::in,
+    maybe(mer_type)::in, inst_match_info::in, inst_match_info::out) is semidet.
 
-inst_matches_initial_2(InstA, InstB, MaybeType, !Info) :-
+inst_matches_initial_mt(InstA, InstB, MaybeType, !Info) :-
     ThisExpansion = inst_match_inputs(InstA, InstB, MaybeType),
     Expansions0 = !.Info ^ imi_expansions,
     ( expansion_member(ThisExpansion, Expansions0) ->
         true
     ;
-        inst_expand(!.Info ^ imi_module_info, InstA, InstA2),
-        inst_expand(!.Info ^ imi_module_info, InstB, InstB2),
+        inst_expand(!.Info ^ imi_module_info, InstA, ExpandedInstA),
+        inst_expand(!.Info ^ imi_module_info, InstB, ExpandedInstB),
         expansion_insert(ThisExpansion, Expansions0, Expansions),
         !Info ^ imi_expansions := Expansions,
-        handle_inst_var_subs(inst_matches_initial_2, inst_matches_initial_4,
-            InstA2, InstB2, MaybeType, !Info)
+        handle_inst_var_subs(inst_matches_initial_mt, inst_matches_initial_4,
+            ExpandedInstA, ExpandedInstB, MaybeType, !Info)
     ).
 
 :- pred inst_matches_initial_4(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
     inst_match_info::in, inst_match_info::out) is semidet.
 
+inst_matches_initial_4(InstA, InstB, MaybeType, !Info) :-
     % To avoid infinite regress, we assume that inst_matches_initial is true
     % for any pairs of insts which occur in `Expansions'.
-inst_matches_initial_4(any(UniqA, HOInstInfoA), any(UniqB, HOInstInfoB), Type,
-        !Info) :-
+    (
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = any(UniqB, HOInstInfoB),
     !.Info ^ imi_any_matches_any = yes,
     compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
-    ho_inst_info_matches_initial(HOInstInfoA, HOInstInfoB, UniqB, Type, !Info).
-inst_matches_initial_4(any(_, _), free, _, !Info).
-inst_matches_initial_4(any(UniqA, HOInstInfoA), ground(_, _)@InstB, Type,
-        !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA,
+        ho_inst_info_matches_initial(HOInstInfoA, HOInstInfoB, MaybeType,
+            !Info)
+    ;
+        InstA = any(_, _),
+        InstB = free
+    ;
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = ground(_, _),
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqA,
         HOInstInfoA, InstA),
-    inst_matches_initial_2(InstA, InstB, Type, !Info).
-inst_matches_initial_4(any(UniqA, HOInstInfoA), bound(_, _)@InstB, Type,
-        !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA,
+        inst_matches_initial_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = bound(_, _),
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqA,
         HOInstInfoA, InstA),
-    inst_matches_initial_2(InstA, InstB, Type, !Info).
-inst_matches_initial_4(free, free, _, !Info).
-inst_matches_initial_4(bound(UniqA, ListA), any(UniqB, none), _, !Info) :-
+        inst_matches_initial_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = free,
+        InstB = free
+    ;
+        InstA = bound(UniqA, ListA),
+        InstB = any(UniqB, none),
     compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
     compare_bound_inst_list_uniq(!.Info ^ imi_uniqueness_comparison,
-        ListA, UniqB, !.Info ^ imi_module_info).
-inst_matches_initial_4(bound(_Uniq, _List), free, _, !Info).
-inst_matches_initial_4(bound(UniqA, ListA), bound(UniqB, ListB), Type,
-        !Info) :-
+            ListA, UniqB, !.Info ^ imi_module_info)
+    ;
+        InstA = bound(_Uniq, _List),
+        InstB = free
+    ;
+        InstA = bound(UniqA, ListA),
+        InstB = bound(UniqB, ListB),
     compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
-    bound_inst_list_matches_initial(ListA, ListB, Type, !Info).
-inst_matches_initial_4(bound(UniqA, ListA), ground(UniqB, none), Type,
-        !Info) :-
+        bound_inst_list_matches_initial(ListA, ListB, MaybeType, !Info)
+    ;
+        InstA = bound(UniqA, ListA),
+        InstB = ground(UniqB, none),
     compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
-    bound_inst_list_is_ground(ListA, Type, !.Info ^ imi_module_info),
+        bound_inst_list_is_ground(ListA, MaybeType, !.Info ^ imi_module_info),
     compare_bound_inst_list_uniq(!.Info ^ imi_uniqueness_comparison,
-        ListA, UniqB, !.Info ^ imi_module_info).
-inst_matches_initial_4(bound(Uniq, List), abstract_inst(_,_), _, !Info) :-
+            ListA, UniqB, !.Info ^ imi_module_info)
+    ;
+        InstA = bound(Uniq, List),
+        InstB = abstract_inst(_,_),
     Uniq = unique,
     bound_inst_list_is_ground(List, !.Info ^ imi_module_info),
-    bound_inst_list_is_unique(List, !.Info ^ imi_module_info).
-inst_matches_initial_4(bound(Uniq, List), abstract_inst(_,_), _, !Info) :-
+        bound_inst_list_is_unique(List, !.Info ^ imi_module_info)
+    ;
+        InstA = bound(Uniq, List),
+        InstB = abstract_inst(_,_),
     Uniq = mostly_unique,
     bound_inst_list_is_ground(List, !.Info ^ imi_module_info),
-    bound_inst_list_is_mostly_unique(List, !.Info ^ imi_module_info).
-inst_matches_initial_4(ground(UniqA, HOInstInfoA), any(UniqB, HOInstInfoB),
-        Type, !Info) :-
+        bound_inst_list_is_mostly_unique(List, !.Info ^ imi_module_info)
+    ;
+        InstA = ground(UniqA, HOInstInfoA),
+        InstB = any(UniqB, HOInstInfoB),
     compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
-    ho_inst_info_matches_initial(HOInstInfoA, HOInstInfoB, UniqB, Type, !Info).
-inst_matches_initial_4(ground(_Uniq, _PredInst), free, _, !Info).
-inst_matches_initial_4(ground(UniqA, _GII_A), bound(UniqB, ListB), MaybeType,
-        !Info) :-
+        ho_inst_info_matches_initial(HOInstInfoA, HOInstInfoB, MaybeType,
+            !Info)
+    ;
+        InstA = ground(_Uniq, _PredInst),
+        InstB = free
+    ;
+        InstA = ground(UniqA, _GII_A),
+        InstB = bound(UniqB, ListB),
     MaybeType = yes(Type),
     % We can only check this case properly if the type is known.
     compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
-    bound_inst_list_is_complete_for_type(set.init, !.Info ^ imi_module_info,
-        ListB, Type),
+        bound_inst_list_is_complete_for_type(set.init,
+            !.Info ^ imi_module_info, ListB, Type),
     ground_matches_initial_bound_inst_list(UniqA, ListB, yes(Type),
-        !Info).
-inst_matches_initial_4(ground(UniqA, HOInstInfoA),
-        ground(UniqB, HOInstInfoB), Type, !Info) :-
+            !Info)
+    ;
+        InstA = ground(UniqA, HOInstInfoA),
+        InstB = ground(UniqB, HOInstInfoB),
     compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
-    ho_inst_info_matches_initial(HOInstInfoA, HOInstInfoB, UniqB, Type, !Info).
-inst_matches_initial_4(ground(_UniqA, none), abstract_inst(_,_), _, !Info) :-
+        ho_inst_info_matches_initial(HOInstInfoA, HOInstInfoB, MaybeType,
+            !Info)
+    ;
+        InstA = ground(_UniqA, none),
+        InstB = abstract_inst(_,_),
     % I don't know what this should do.
     % Abstract insts aren't really supported.
     unexpected($module, $pred,
-        "inst_matches_initial(ground, abstract_inst) == ??").
-inst_matches_initial_4(abstract_inst(_,_), any(shared, none), _, !Info).
-inst_matches_initial_4(abstract_inst(_,_), free, _, !Info).
-inst_matches_initial_4(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
-        _Type, !Info) :-
+            "inst_matches_initial(ground, abstract_inst) == ??")
+    ;
+        InstA = abstract_inst(_,_),
+        InstB = any(shared, none)
+    ;
+        InstA = abstract_inst(_,_),
+        InstB = free
+    ;
+        InstA = abstract_inst(Name, ArgsA),
+        InstB = abstract_inst(Name, ArgsB),
     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, !Info).
-inst_matches_initial_4(not_reached, _, _, !Info).
+        inst_list_matches_initial(ArgsA, ArgsB, MaybeTypes, !Info)
+    ;
+        InstA = not_reached
+    ).
 
 %-----------------------------------------------------------------------------%
 
@@ -694,22 +728,23 @@
     inst_match_info::in, inst_match_info::out) is semidet.
 
 ground_matches_initial_bound_inst_list(_, [], _, !Info).
-ground_matches_initial_bound_inst_list(Uniq,
-        [bound_functor(ConsId, Args) | List], MaybeType, !Info) :-
+ground_matches_initial_bound_inst_list(Uniq, [BoundInst | BoundInsts],
+        MaybeType, !Info) :-
+    BoundInst = bound_functor(ConsId, Args),
     maybe_get_cons_id_arg_types(!.Info ^ imi_module_info, MaybeType, ConsId,
         list.length(Args), MaybeTypes),
     ground_matches_initial_inst_list(Uniq, Args, MaybeTypes, !Info),
-    ground_matches_initial_bound_inst_list(Uniq, List, MaybeType, !Info).
+    ground_matches_initial_bound_inst_list(Uniq, BoundInsts, MaybeType, !Info).
 
 :- pred ground_matches_initial_inst_list(uniqueness::in, list(mer_inst)::in,
     list(maybe(mer_type))::in, inst_match_info::in, inst_match_info::out)
     is semidet.
 
 ground_matches_initial_inst_list(_, [], [], !Info).
-ground_matches_initial_inst_list(Uniq, [Inst | Insts], [Type | Types],
-        !Info) :-
-    inst_matches_initial_2(ground(Uniq, none), Inst, Type, !Info),
-    ground_matches_initial_inst_list(Uniq, Insts, Types, !Info).
+ground_matches_initial_inst_list(Uniq, [Inst | Insts],
+        [MaybeType | MaybeTypes], !Info) :-
+    inst_matches_initial_mt(ground(Uniq, none), Inst, MaybeType, !Info),
+    ground_matches_initial_inst_list(Uniq, Insts, MaybeTypes, !Info).
 
 %-----------------------------------------------------------------------------%
 
@@ -726,6 +761,11 @@
     type_util.cons_id_arg_types(ModuleInfo, Type, _, _),
 
     % Is there a bound_inst for each cons_id in the type_table?
+    % XXX This code has a potential performance problem. If the type has
+    % N cons_ids, then this code can do N invocations of list.member,
+    % each of which has O(N) complexity, for an overall complexity of O(N^2).
+    % We should fix this by taking advantage of the fact that BoundInsts
+    % should be sorted.
     all [ConsId, ArgTypes] (
         type_util.cons_id_arg_types(ModuleInfo, Type, ConsId, ArgTypes)
     =>
@@ -744,12 +784,13 @@
     mer_inst::in, mer_type::in) is semidet.
 
 inst_is_complete_for_type(Expansions, ModuleInfo, Inst, Type) :-
+    % XXX This should be a switch on Inst.
     ( Inst = defined_inst(Name) ->
         ( set.member(Name, Expansions) ->
             true
         ;
             inst_lookup(ModuleInfo, Name, ExpandedInst),
-            inst_is_complete_for_type(Expansions `set.insert` Name,
+            inst_is_complete_for_type(set.insert(Expansions, Name),
                 ModuleInfo, ExpandedInst, Type)
         )
     ; Inst = bound(_, List) ->
@@ -792,30 +833,35 @@
     % This predicate checks if two ho_inst_infos match_initial.
     % It does not check uniqueness.
     %
-:- pred ho_inst_info_matches_initial(ho_inst_info::in,
-    ho_inst_info::in, uniqueness::in, maybe(mer_type)::in,
-    inst_match_info::in, inst_match_info::out) is semidet.
+:- pred ho_inst_info_matches_initial(ho_inst_info::in, ho_inst_info::in,
+    maybe(mer_type)::in, inst_match_info::in, inst_match_info::out) is semidet.
 
-ho_inst_info_matches_initial(HOInstInfoA, none, _, _, !Info) :-
+ho_inst_info_matches_initial(HOInstInfoA, HOInstInfoB, MaybeType, !Info) :-
+    (
+        HOInstInfoB = none,
     \+ ho_inst_info_is_nonstandard_func_mode(!.Info ^ imi_module_info,
-        HOInstInfoA).
-ho_inst_info_matches_initial(none, higher_order(PredInstB), _, Type, !Info) :-
+            HOInstInfoA)
+    ;
+        HOInstInfoA = none,
+        HOInstInfoB = higher_order(PredInstB),
     PredInstB = pred_inst_info(pf_function, ArgModes, _, _Det),
     Arity = list.length(ArgModes),
     PredInstA = pred_inst_info_standard_func_mode(Arity),
-    pred_inst_matches_2(PredInstA, PredInstB, Type, !Info).
-ho_inst_info_matches_initial(higher_order(PredInstA), higher_order(PredInstB),
-        _, MaybeType, !Info) :-
-    pred_inst_matches_2(PredInstA, PredInstB, MaybeType, !Info).
+        pred_inst_matches_2(PredInstA, PredInstB, MaybeType, !Info)
+    ;
+        HOInstInfoA = higher_order(PredInstA),
+        HOInstInfoB = higher_order(PredInstB),
+        pred_inst_matches_2(PredInstA, PredInstB, MaybeType, !Info)
+    ).
 
 pred_inst_matches(PredInstA, PredInstB, ModuleInfo) :-
-    pred_inst_matches_1(PredInstA, PredInstB, no, ModuleInfo).
+    pred_inst_matches_mt(PredInstA, PredInstB, no, ModuleInfo).
 
-:- pred pred_inst_matches_1(pred_inst_info::in, pred_inst_info::in,
+:- pred pred_inst_matches_mt(pred_inst_info::in, pred_inst_info::in,
     maybe(mer_type)::in, module_info::in) is semidet.
 
-pred_inst_matches_1(PredInstA, PredInstB, MaybeType, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
+pred_inst_matches_mt(PredInstA, PredInstB, MaybeType, ModuleInfo) :-
+    Info0 = init_inst_match_info(ModuleInfo, no, cs_none, uc_match, yes),
     pred_inst_matches_2(PredInstA, PredInstB, MaybeType, Info0, _).
 
     % pred_inst_matches_2(PredInstA, PredInstB, !Info)
@@ -837,14 +883,13 @@
     maybe_get_higher_order_arg_types(MaybeType, length(ModesA), MaybeTypes),
     pred_inst_argmodes_matches(ModesA, ModesB, MaybeTypes, !Info).
 
-    % pred_inst_argmodes_matches(ModesA, ModesB, !Info):
+    % pred_inst_argmodes_matches(ModesA, ModesB, MaybeTypes, !Info):
     %
-    % 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 Inst0 ^ expansions
-    % are assumed to match_final each other.
+    % 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 Inst0 ^ expansions are assumed to match_final each other.
     %
     % (In other words, as far as subtyping goes it is contravariant in
     % the initial insts, and covariant in the final insts;
@@ -860,8 +905,8 @@
     ModuleInfo = !.Info ^ imi_module_info,
     mode_get_insts(ModuleInfo, ModeA, InitialA, FinalA),
     mode_get_insts(ModuleInfo, ModeB, InitialB, FinalB),
-    swap_sub(inst_matches_final_2(InitialB, InitialA, MaybeType), !Info),
-    inst_matches_final_2(FinalA, FinalB, MaybeType, !Info),
+    swap_sub(inst_matches_final_mt(InitialB, InitialA, MaybeType), !Info),
+    inst_matches_final_mt(FinalA, FinalB, MaybeType, !Info),
     pred_inst_argmodes_matches(ModeAs, ModeBs, MaybeTypes, !Info).
 
 %-----------------------------------------------------------------------------%
@@ -875,9 +920,9 @@
 :- pred compare_uniqueness(uniqueness_comparison::in,
     uniqueness::in, uniqueness::in) is semidet.
 
-compare_uniqueness(match, InstA, InstB) :-
+compare_uniqueness(uc_match, InstA, InstB) :-
     unique_matches_initial(InstA, InstB).
-compare_uniqueness(instantiated, InstA, InstB) :-
+compare_uniqueness(uc_instantiated, InstA, InstB) :-
     unique_matches_initial(InstB, InstA).
 
 unique_matches_initial(unique, _).
@@ -900,9 +945,9 @@
 :- pred compare_bound_inst_list_uniq(uniqueness_comparison::in,
     list(bound_inst)::in, uniqueness::in, module_info::in) is semidet.
 
-compare_bound_inst_list_uniq(match, List, Uniq, ModuleInfo) :-
+compare_bound_inst_list_uniq(uc_match, List, Uniq, ModuleInfo) :-
     bound_inst_list_matches_uniq(List, Uniq, ModuleInfo).
-compare_bound_inst_list_uniq(instantiated, List, Uniq, ModuleInfo) :-
+compare_bound_inst_list_uniq(uc_instantiated, List, Uniq, ModuleInfo) :-
     uniq_matches_bound_inst_list(Uniq, List, ModuleInfo).
 
 :- pred bound_inst_list_matches_uniq(list(bound_inst)::in, uniqueness::in,
@@ -964,24 +1009,25 @@
     is semidet.
 
 inst_list_matches_initial([], [], [], !Info).
-inst_list_matches_initial([X | Xs], [Y | Ys], [Type | Types], !Info) :-
-    inst_matches_initial_2(X, Y, Type, !Info),
-    inst_list_matches_initial(Xs, Ys, Types, !Info).
+inst_list_matches_initial([X | Xs], [Y | Ys], [MaybeType | MaybeTypes],
+        !Info) :-
+    inst_matches_initial_mt(X, Y, MaybeType, !Info),
+    inst_list_matches_initial(Xs, Ys, MaybeTypes, !Info).
 
 %-----------------------------------------------------------------------------%
 
 inst_matches_final(InstA, InstB, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
-    inst_matches_final_2(InstA, InstB, no, Info0, _).
+    Info0 = init_inst_match_info(ModuleInfo, no, cs_none, uc_match, yes),
+    inst_matches_final_mt(InstA, InstB, no, Info0, _).
 
 inst_matches_final_typed(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
-    inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
+    Info0 = init_inst_match_info(ModuleInfo, no, cs_none, uc_match, yes),
+    inst_matches_final_mt(InstA, InstB, yes(Type), Info0, _).
 
-:- pred inst_matches_final_2(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
+:- pred inst_matches_final_mt(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
     inst_match_info::in, inst_match_info::out) is semidet.
 
-inst_matches_final_2(InstA, InstB, MaybeType, !Info) :-
+inst_matches_final_mt(InstA, InstB, MaybeType, !Info) :-
     ThisExpansion = inst_match_inputs(InstA, InstB, MaybeType),
     Expansions0 = !.Info ^ imi_expansions,
     ( expansion_member(ThisExpansion, Expansions0) ->
@@ -989,59 +1035,74 @@
     ; InstA = InstB ->
         true
     ;
-        inst_expand(!.Info ^ imi_module_info, InstA, InstA2),
-        inst_expand(!.Info ^ imi_module_info, InstB, InstB2),
+        inst_expand(!.Info ^ imi_module_info, InstA, ExpandedInstA),
+        inst_expand(!.Info ^ imi_module_info, InstB, ExpandedInstB),
         expansion_insert(ThisExpansion, Expansions0, Expansions),
         !Info ^ imi_expansions := Expansions,
-        handle_inst_var_subs(inst_matches_final_2, inst_matches_final_3,
-            InstA2, InstB2, MaybeType, !Info)
+        handle_inst_var_subs(inst_matches_final_mt, inst_matches_final_3,
+            ExpandedInstA, ExpandedInstB, MaybeType, !Info)
     ).
 
 :- pred inst_matches_final_3(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
     inst_match_info::in, inst_match_info::out) is semidet.
 
-inst_matches_final_3(any(UniqA, HOInstInfoA), any(UniqB, HOInstInfoB), Type,
-        !Info) :-
-    ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, Type, !Info),
-    unique_matches_final(UniqA, UniqB).
-inst_matches_final_3(any(UniqA, HOInstInfoA), ground(_, _)@InstB, Type,
-        !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA,
+inst_matches_final_3(InstA, InstB, MaybeType, !Info) :-
+    (
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = any(UniqB, HOInstInfoB),
+        ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, MaybeType, !Info),
+        unique_matches_final(UniqA, UniqB)
+    ;
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = ground(_, _)@InstB,
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqA,
         HOInstInfoA, InstA),
-    inst_matches_final_2(InstA, InstB, Type, !Info).
-inst_matches_final_3(any(UniqA, HOInstInfoA), bound(_, _)@InstB, Type, !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA,
+        inst_matches_final_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = bound(_, _),
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqA,
         HOInstInfoA, InstA),
-    inst_matches_final_2(InstA, InstB, Type, !Info).
-inst_matches_final_3(free, any(Uniq, _), _, !Info) :-
+        inst_matches_final_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = free,
+        InstB = any(Uniq, _),
     % 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, _, !Info).
-inst_matches_final_3(bound(UniqA, ListA), any(UniqB, none), _, !Info) :-
+        ( Uniq = clobbered ; Uniq = mostly_clobbered )
+    ;
+        InstA = free,
+        InstB = free
+    ;
+        InstA = bound(UniqA, ListA),
+        InstB = any(UniqB, none),
     unique_matches_final(UniqA, UniqB),
     bound_inst_list_matches_uniq(ListA, UniqB, !.Info ^ imi_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, !.Info ^ imi_module_info).
-inst_matches_final_3(bound(UniqA, ListA), bound(UniqB, ListB), MaybeType,
-        !Info) :-
+        bound_inst_list_is_ground_or_any(ListA, !.Info ^ imi_module_info)
+    ;
+        InstA = bound(UniqA, ListA),
+        InstB = bound(UniqB, ListB),
     unique_matches_final(UniqA, UniqB),
-    bound_inst_list_matches_final(ListA, ListB, MaybeType, !Info).
-inst_matches_final_3(bound(UniqA, ListA), ground(UniqB, none), Type,
-        !Info) :-
+        bound_inst_list_matches_final(ListA, ListB, MaybeType, !Info)
+    ;
+        InstA = bound(UniqA, ListA),
+        InstB = ground(UniqB, none),
     unique_matches_final(UniqA, UniqB),
-    bound_inst_list_is_ground(ListA, Type, !.Info ^ imi_module_info),
-    bound_inst_list_matches_uniq(ListA, UniqB, !.Info ^ imi_module_info).
-inst_matches_final_3(ground(UniqA, HOInstInfoA), any(UniqB, HOInstInfoB),
-        MaybeType, !Info) :-
+        bound_inst_list_is_ground(ListA, MaybeType, !.Info ^ imi_module_info),
+        bound_inst_list_matches_uniq(ListA, UniqB, !.Info ^ imi_module_info)
+    ;
+        InstA = ground(UniqA, HOInstInfoA),
+        InstB = any(UniqB, HOInstInfoB),
     ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, MaybeType, !Info),
-    unique_matches_final(UniqA, UniqB).
-inst_matches_final_3(ground(UniqA, HOInstInfoA), bound(UniqB, ListB),
-        MaybeType, !Info) :-
+        unique_matches_final(UniqA, UniqB)
+    ;
+        InstA = ground(UniqA, HOInstInfoA),
+        InstB = bound(UniqB, ListB),
     ModuleInfo = !.Info ^ imi_module_info,
     \+ ho_inst_info_is_nonstandard_func_mode(ModuleInfo, HOInstInfoA),
     unique_matches_final(UniqA, UniqB),
@@ -1050,60 +1111,73 @@
     (
         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)
+            bound_inst_list_is_complete_for_type(set.init, ModuleInfo, 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, HOInstInfoA), ground(UniqB, HOInstInfoB),
-        MaybeType, !Info) :-
+        )
+    ;
+        InstA = ground(UniqA, HOInstInfoA),
+        InstB = ground(UniqB, HOInstInfoB),
     ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, MaybeType, !Info),
-    unique_matches_final(UniqA, UniqB).
-inst_matches_final_3(abstract_inst(_, _), any(shared, none), _, !Info).
-inst_matches_final_3(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
-        _MaybeType, !Info) :-
+        unique_matches_final(UniqA, UniqB)
+    ;
+        InstA = abstract_inst(_, _),
+        InstB = any(shared, none)
+    ;
+        InstA = abstract_inst(Name, ArgsA),
+        InstB = abstract_inst(Name, ArgsB),
     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, !Info).
-inst_matches_final_3(not_reached, _, _, !Info).
-inst_matches_final_3(constrained_inst_vars(InstVarsA, InstA), InstB, MaybeType,
-        !Info) :-
+        inst_list_matches_final(ArgsA, ArgsB, MaybeTypes, !Info)
+    ;
+        InstA = not_reached
+    ;
+        InstA = constrained_inst_vars(InstVarsA, InstA),
     ( InstB = constrained_inst_vars(InstVarsB, InstB1) ->
         % Constrained_inst_vars match_final only if InstVarsA contains
         % all the variables in InstVarsB.
-        InstVarsB `set.subset` InstVarsA,
-        inst_matches_final_2(InstA, InstB1, MaybeType, !Info)
+            set.subset(InstVarsB, InstVarsA),
+            inst_matches_final_mt(InstA, InstB1, MaybeType, !Info)
     ;
-        inst_matches_final_2(InstA, InstB, MaybeType, !Info)
+            inst_matches_final_mt(InstA, InstB, MaybeType, !Info)
+        )
     ).
 
 :- pred ho_inst_info_matches_final(ho_inst_info::in, ho_inst_info::in,
     maybe(mer_type)::in, inst_match_info::in, inst_match_info::out) is semidet.
 
-ho_inst_info_matches_final(HOInstInfoA, none, _, !Info) :-
+ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, MaybeType, !Info) :-
+    (
+        HOInstInfoB = none,
     \+ ho_inst_info_is_nonstandard_func_mode(!.Info ^ imi_module_info,
-        HOInstInfoA).
-ho_inst_info_matches_final(none, higher_order(PredInstB), Type, !Info) :-
+            HOInstInfoA)
+    ;
+        HOInstInfoA = none,
+        HOInstInfoB = higher_order(PredInstB),
     PredInstB = pred_inst_info(pf_function, ArgModes, _, _Det),
     Arity = list.length(ArgModes),
     PredInstA = pred_inst_info_standard_func_mode(Arity),
-    pred_inst_matches_2(PredInstA, PredInstB, Type, !Info).
-ho_inst_info_matches_final(higher_order(PredInstA),
-        higher_order(PredInstB), MaybeType, !Info) :-
-    pred_inst_matches_2(PredInstA, PredInstB, MaybeType, !Info).
+        pred_inst_matches_2(PredInstA, PredInstB, MaybeType, !Info)
+    ;
+        HOInstInfoA = higher_order(PredInstA),
+        HOInstInfoB = higher_order(PredInstB),
+        pred_inst_matches_2(PredInstA, PredInstB, MaybeType, !Info)
+    ).
 
 :- pred inst_list_matches_final(list(mer_inst)::in, list(mer_inst)::in,
     list(maybe(mer_type))::in, inst_match_info::in, inst_match_info::out)
     is semidet.
 
 inst_list_matches_final([], [], [], !Info).
-inst_list_matches_final([ArgA | ArgsA], [ArgB | ArgsB], [Type | Types],
-        !Info) :-
-    inst_matches_final_2(ArgA, ArgB, Type, !Info),
-    inst_list_matches_final(ArgsA, ArgsB, Types, !Info).
+inst_list_matches_final([ArgA | ArgsA], [ArgB | ArgsB],
+        [MaybeType | MaybeTypes], !Info) :-
+    inst_matches_final_mt(ArgA, ArgB, MaybeType, !Info),
+    inst_list_matches_final(ArgsA, ArgsB, MaybeTypes, !Info).
 
     % Here we check that the functors in the first list are a subset of the
     % functors in the second list. (If a bound(...) inst only specifies
@@ -1135,84 +1209,96 @@
     ).
 
 inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo) :-
-    Info = init_inst_match_info(ModuleInfo, no, none, instantiated, no),
-    inst_matches_initial_2(InstA, InstB, yes(Type), Info, _).
+    Info0 = init_inst_match_info(ModuleInfo, no, cs_none, uc_instantiated, no),
+    inst_matches_initial_mt(InstA, InstB, yes(Type), Info0, _).
 
 inst_matches_binding(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo, no, none, match, no),
-    inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
+    Info0 = init_inst_match_info(ModuleInfo, no, cs_none, uc_match, no),
+    inst_matches_binding_mt(InstA, InstB, yes(Type), Info0, _).
 
 inst_matches_binding_allow_any_any(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
-    inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
+    Info0 = init_inst_match_info(ModuleInfo, no, cs_none, uc_match, yes),
+    inst_matches_binding_mt(InstA, InstB, yes(Type), Info0, _).
 
-:- pred inst_matches_binding_2(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
+:- pred inst_matches_binding_mt(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
     inst_match_info::in, inst_match_info::out) is semidet.
 
-inst_matches_binding_2(InstA, InstB, MaybeType, !Info) :-
+inst_matches_binding_mt(InstA, InstB, MaybeType, !Info) :-
     ThisExpansion = inst_match_inputs(InstA, InstB, MaybeType),
     Expansions0 = !.Info ^ imi_expansions,
     ( expansion_member(ThisExpansion, Expansions0) ->
         true
     ;
         inst_expand_and_remove_constrained_inst_vars(!.Info ^ imi_module_info,
-            InstA, InstA2),
+            InstA, ExpandedInstA),
         inst_expand_and_remove_constrained_inst_vars(!.Info ^ imi_module_info,
-            InstB, InstB2),
+            InstB, ExpandedInstB),
         expansion_insert(ThisExpansion, Expansions0, Expansions),
         !Info ^ imi_expansions := Expansions,
-        inst_matches_binding_3(InstA2, InstB2, MaybeType, !Info)
+        inst_matches_binding_3(ExpandedInstA, ExpandedInstB, MaybeType, !Info)
     ).
 
 :- pred inst_matches_binding_3(mer_inst::in, mer_inst::in, maybe(mer_type)::in,
     inst_match_info::in, inst_match_info::out) is semidet.
 
-% Note that `any' is *not* considered to match `any' unless
-% Info ^ any_matches_any = yes or the type is not a solver type (and does not
-% contain any solver types).
-inst_matches_binding_3(free, free, _, !Info).
-inst_matches_binding_3(any(UniqA, HOInstInfoA), any(UniqB, HOInstInfoB), Type,
-        !Info) :-
+inst_matches_binding_3(InstA, InstB, MaybeType, !Info) :-
+    (
+        InstA = free,
+        InstB = free
+    ;
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = any(UniqB, HOInstInfoB),
+        % Note that `any' is *not* considered to match `any' unless
+        % Info ^ any_matches_any = yes or the type is not a solver type
+        % (and does not contain any solver types).
     AnyMatchesAny = !.Info ^ imi_any_matches_any,
     (
         AnyMatchesAny = yes,
-        ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, Type, !Info)
+            ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, MaybeType,
+                !Info)
     ;
         AnyMatchesAny = no,
-        maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA, HOInstInfoA,
-            InstA),
-        maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqB, HOInstInfoB,
-            InstB),
-        inst_matches_binding_2(InstA, InstB, Type, !Info)
-    ).
-inst_matches_binding_3(any(UniqA, HOInstInfoA), ground(_, _)@InstB, Type,
-        !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA,
+            maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqA,
         HOInstInfoA, InstA),
-    inst_matches_binding_2(InstA, InstB, Type, !Info).
-inst_matches_binding_3(any(UniqA, HOInstInfoA), bound(_, _)@InstB, Type,
-        !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA,
+            maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqB,
+                HOInstInfoB, InstB),
+            inst_matches_binding_mt(InstA, InstB, MaybeType, !Info)
+        )
+    ;
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = ground(_, _),
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqA,
         HOInstInfoA, InstA),
-    inst_matches_binding_2(InstA, InstB, Type, !Info).
-inst_matches_binding_3(ground(_, _)@InstA, any(UniqB, HOInstInfoB), Type,
-        !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqB,
+        inst_matches_binding_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = any(UniqA, HOInstInfoA),
+        InstB = bound(_, _),
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqA,
+            HOInstInfoA, InstA),
+        inst_matches_binding_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = ground(_, _),
+        InstB = any(UniqB, HOInstInfoB),
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqB,
         HOInstInfoB, InstB),
-    inst_matches_binding_2(InstA, InstB, Type, !Info).
-inst_matches_binding_3(bound(_, _)@InstA, any(UniqB, HOInstInfoB), Type,
-        !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqB,
+        inst_matches_binding_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = bound(_, _),
+        InstB = any(UniqB, HOInstInfoB),
+        maybe_any_to_bound(MaybeType, !.Info ^ imi_module_info, UniqB,
         HOInstInfoB, InstB),
-    inst_matches_binding_2(InstA, InstB, Type, !Info).
-inst_matches_binding_3(bound(_UniqA, ListA), bound(_UniqB, ListB), MaybeType,
-        !Info) :-
-    bound_inst_list_matches_binding(ListA, ListB, MaybeType, !Info).
-inst_matches_binding_3(bound(_UniqA, ListA), ground(_UniqB, none), Type,
-        !Info) :-
-    bound_inst_list_is_ground(ListA, Type, !.Info ^ imi_module_info).
-inst_matches_binding_3(ground(_UniqA, _), bound(_UniqB, ListB), MaybeType,
-        !Info) :-
+        inst_matches_binding_mt(InstA, InstB, MaybeType, !Info)
+    ;
+        InstA = bound(_UniqA, ListA),
+        InstB = bound(_UniqB, ListB),
+        bound_inst_list_matches_binding(ListA, ListB, MaybeType, !Info)
+    ;
+        InstA = bound(_UniqA, ListA),
+        InstB = ground(_UniqB, none),
+        bound_inst_list_is_ground(ListA, MaybeType, !.Info ^ imi_module_info)
+    ;
+        InstA = ground(_UniqA, _),
+        InstB = bound(_UniqB, ListB),
     bound_inst_list_is_ground(ListB, MaybeType, !.Info ^ imi_module_info),
     (
         MaybeType = yes(Type),
@@ -1221,35 +1307,45 @@
             !.Info ^ imi_module_info, ListB, Type)
     ;
         true
-        % XXX enabling the check for bound_inst_list_is_complete
+            % 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, HOInstInfoA),
-        ground(_UniqB, HOInstInfoB), MaybeType, !Info) :-
+        )
+    ;
+        InstA = ground(_UniqA, HOInstInfoA),
+        InstB = ground(_UniqB, HOInstInfoB),
     ho_inst_info_matches_binding(HOInstInfoA, HOInstInfoB, MaybeType,
-        !.Info ^ imi_module_info).
-inst_matches_binding_3(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
-        _MaybeType, !Info) :-
+            !.Info ^ imi_module_info)
+    ;
+        InstA = abstract_inst(Name, ArgsA),
+        InstB = abstract_inst(Name, ArgsB),
     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, !Info).
-inst_matches_binding_3(not_reached, _, _, !Info).
+        inst_list_matches_binding(ArgsA, ArgsB, MaybeTypes, !Info)
+    ;
+        InstA = not_reached
+    ).
 
 :- pred ho_inst_info_matches_binding(ho_inst_info::in, ho_inst_info::in,
     maybe(mer_type)::in, module_info::in) is semidet.
 
-ho_inst_info_matches_binding(_, none, _, _).
-ho_inst_info_matches_binding(none, higher_order(PredInstB), MaybeType,
+ho_inst_info_matches_binding(HOInstInfoA, HOInstInfoB, MaybeType,
         ModuleInfo) :-
+    (
+        HOInstInfoB = none
+    ;
+        HOInstInfoA = none,
+        HOInstInfoB = higher_order(PredInstB),
     PredInstB = pred_inst_info(pf_function, ArgModes, _, _Det),
     Arity = list.length(ArgModes),
     PredInstA = pred_inst_info_standard_func_mode(Arity),
-    pred_inst_matches_1(PredInstA, PredInstB, MaybeType, ModuleInfo).
-ho_inst_info_matches_binding(higher_order(PredInstA),
-        higher_order(PredInstB), MaybeType, ModuleInfo) :-
-    pred_inst_matches_1(PredInstA, PredInstB, MaybeType, ModuleInfo).
+        pred_inst_matches_mt(PredInstA, PredInstB, MaybeType, ModuleInfo)
+    ;
+        HOInstInfoA = higher_order(PredInstA),
+        HOInstInfoB = higher_order(PredInstB),
+        pred_inst_matches_mt(PredInstA, PredInstB, MaybeType, ModuleInfo)
+    ).
 
 :- pred inst_list_matches_binding(list(mer_inst)::in, list(mer_inst)::in,
     list(maybe(mer_type))::in, inst_match_info::in, inst_match_info::out)
@@ -1258,7 +1354,7 @@
 inst_list_matches_binding([], [], [], !Info).
 inst_list_matches_binding([ArgA | ArgsA], [ArgB | ArgsB],
         [MaybeType | MaybeTypes], !Info) :-
-    inst_matches_binding_2(ArgA, ArgB, MaybeType, !Info),
+    inst_matches_binding_mt(ArgA, ArgB, MaybeType, !Info),
     inst_list_matches_binding(ArgsA, ArgsB, MaybeTypes, !Info).
 
     % Here we check that the functors in the first list are a subset of the
@@ -1292,66 +1388,140 @@
 
 %-----------------------------------------------------------------------------%
 
-inst_is_clobbered(_, not_reached) :- fail.
-inst_is_clobbered(_, any(mostly_clobbered, _)).
-inst_is_clobbered(_, any(clobbered, _)).
-inst_is_clobbered(_, ground(clobbered, _)).
-inst_is_clobbered(_, ground(mostly_clobbered, _)).
-inst_is_clobbered(_, bound(clobbered, _)).
-inst_is_clobbered(_, bound(mostly_clobbered, _)).
-inst_is_clobbered(_, inst_var(_)) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-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),
-    inst_is_clobbered(ModuleInfo, Inst).
-
-inst_is_free(_, free).
-inst_is_free(_, free(_Type)).
-inst_is_free(_, inst_var(_)) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-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),
-    inst_is_free(ModuleInfo, Inst).
-
-inst_is_any(_, any(_, _)).
-inst_is_any(_, inst_var(_)) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-inst_is_any(ModuleInfo, constrained_inst_vars(_, Inst)) :-
-    inst_is_any(ModuleInfo, Inst).
-inst_is_any(ModuleInfo, defined_inst(InstName)) :-
-    inst_lookup(ModuleInfo, InstName, Inst),
-    inst_is_any(ModuleInfo, Inst).
-
-inst_is_bound(_, not_reached).
-inst_is_bound(_, any(_, _)).
-inst_is_bound(_, ground(_, _)).
-inst_is_bound(_, bound(_, _)).
-inst_is_bound(_, inst_var(_)) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-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),
-    inst_is_bound(ModuleInfo, Inst).
-inst_is_bound(_, abstract_inst(_, _)).
+inst_is_clobbered(ModuleInfo, Inst) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = free
+        ; Inst = free(_)
+        ; Inst = not_reached
+        ; Inst = abstract_inst(_, _)    % XXX is this right?
+        ),
+        fail
+    ;
+        ( Inst = any(mostly_clobbered, _)
+        ; Inst = any(clobbered, _)
+        ; Inst = ground(clobbered, _)
+        ; Inst = ground(mostly_clobbered, _)
+        ; Inst = bound(clobbered, _)
+        ; Inst = bound(mostly_clobbered, _)
+        )
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_clobbered(ModuleInfo, SubInst)
+    ;
+        Inst = defined_inst(InstName),
+        inst_lookup(ModuleInfo, InstName, NextInst),
+        inst_is_clobbered(ModuleInfo, NextInst)
+    ).
+
+inst_is_free(ModuleInfo, Inst) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = free
+        ; Inst = free(_)
+        )
+    ;
+        ( Inst = ground(_, _)
+        ; Inst = bound(_, _)
+        ; Inst = any(_, _)
+        ; Inst = not_reached
+        ; Inst = abstract_inst(_, _)    % XXX is this right?
+        ),
+        fail
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_free(ModuleInfo, SubInst)
+    ;
+        Inst = defined_inst(InstName),
+        inst_lookup(ModuleInfo, InstName, NextInst),
+        inst_is_free(ModuleInfo, NextInst)
+    ).
+
+inst_is_any(ModuleInfo, Inst) :-
+    require_complete_switch [Inst]
+    (
+        Inst = any(_, _)
+    ;
+        ( Inst = free
+        ; Inst = free(_)
+        ; Inst = ground(_, _)
+        ; Inst = bound(_, _)
+        ; Inst = not_reached
+        ; Inst = abstract_inst(_, _)    % XXX is this right?
+        ),
+        fail
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_any(ModuleInfo, SubInst)
+    ;
+        Inst = defined_inst(InstName),
+        inst_lookup(ModuleInfo, InstName, NextInst),
+        inst_is_any(ModuleInfo, NextInst)
+    ).
+
+inst_is_bound(ModuleInfo, Inst) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = ground(_, _)
+        ; Inst = bound(_, _)
+        ; Inst = any(_, _)
+        ; Inst = abstract_inst(_, _)    % XXX is this right?
+        ; Inst = not_reached
+        )
+    ;
+        ( Inst = free
+        ; Inst = free(_)
+        ),
+        fail
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_bound(ModuleInfo, SubInst)
+    ;
+        Inst = defined_inst(InstName),
+        inst_lookup(ModuleInfo, InstName, NextInst),
+        inst_is_bound(ModuleInfo, NextInst)
+    ).
 
+inst_is_bound_to_functors(ModuleInfo, Inst, Functors) :-
     % inst_is_bound_to_functors succeeds iff the inst passed is
     % `bound(_Uniq, Functors)' or is a user-defined inst which expands to
     % `bound(_Uniq, Functors)'.
     %
-inst_is_bound_to_functors(_, bound(_Uniq, Functors), Functors).
-inst_is_bound_to_functors(_, inst_var(_), _) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-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),
-    inst_is_bound_to_functors(ModuleInfo, Inst, Functors).
+    require_complete_switch [Inst]
+    (
+        Inst = bound(_Uniq, Functors)
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_bound_to_functors(ModuleInfo, SubInst, Functors)
+    ;
+        Inst = defined_inst(InstName),
+        inst_lookup(ModuleInfo, InstName, NextInst),
+        inst_is_bound_to_functors(ModuleInfo, NextInst, Functors)
+    ;
+        ( Inst = free
+        ; Inst = free(_)
+        ; Inst = any(_, _)
+        ; Inst = ground(_, _)
+        ; Inst = abstract_inst(_, _)
+        ; Inst = not_reached
+        ),
+        fail
+    ).
 
 %-----------------------------------------------------------------------------%
 
@@ -1373,7 +1543,7 @@
             trace [compiletime(flag("inst-is-ground-perf")), io(!IO)] (
                 io.write_string("inst_is_ground miss\n", !IO)
             ),
-            ( inst_is_ground(ModuleInfo, no, Inst) ->
+            ( inst_is_ground_mt(ModuleInfo, no, Inst) ->
                 impure record_inst_is_ground(Inst, yes)
                 % Succeed.
             ;
@@ -1481,50 +1651,74 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred inst_is_ground(module_info::in, maybe(mer_type)::in, mer_inst::in)
+:- pred inst_is_ground_mt(module_info::in, maybe(mer_type)::in, mer_inst::in)
     is semidet.
 
-inst_is_ground(ModuleInfo, MaybeType, Inst) :-
+inst_is_ground_mt(ModuleInfo, MaybeType, Inst) :-
     Expansions0 = set_tree234.init,
-    inst_is_ground_1(ModuleInfo, MaybeType, Inst, Expansions0, _Expansions).
+    inst_is_ground_mt_1(ModuleInfo, MaybeType, Inst, Expansions0, _Expansions).
 
     % The third arg is the set of insts which have already been expanded;
     % we use this to avoid going into an infinite loop.
     %
-:- pred inst_is_ground_1(module_info::in, maybe(mer_type)::in, mer_inst::in,
+:- pred inst_is_ground_mt_1(module_info::in, maybe(mer_type)::in, mer_inst::in,
     set_tree234(mer_inst)::in, set_tree234(mer_inst)::out) is semidet.
 
-inst_is_ground_1(ModuleInfo, MaybeType, Inst, !Expansions) :-
-    ( set_tree234.contains(!.Expansions, Inst) ->
-        true
-    ;
-        ( Inst \= any(_, _) ->
-            set_tree234.insert(Inst, !Expansions)
+inst_is_ground_mt_1(ModuleInfo, MaybeType, Inst, !Expansions) :-
+    % XXX This special casing of any/2 was introduced in version 1.65
+    % of this file. The log message for that version gives a reason why
+    % this special casing is required, but I (zs) don't believe it.
+    ( Inst = any(_, _) ->
+        inst_is_ground_mt_2(ModuleInfo, MaybeType, Inst, !Expansions)
+    ;
+        % ZZZ make this work on Inst's *address*.
+        ( set_tree234.try_and_insert(Inst, !Expansions) ->
+            inst_is_ground_mt_2(ModuleInfo, MaybeType, Inst, !Expansions)
         ;
+            % Inst was already in !.Expansions.
             true
-        ),
-        inst_is_ground_2(ModuleInfo, MaybeType, Inst, !Expansions)
+        )
     ).
 
-:- pred inst_is_ground_2(module_info::in, maybe(mer_type)::in, mer_inst::in,
+:- pred inst_is_ground_mt_2(module_info::in, maybe(mer_type)::in, mer_inst::in,
     set_tree234(mer_inst)::in, set_tree234(mer_inst)::out) is semidet.
 
-inst_is_ground_2(_, _, not_reached, !Expansions).
-inst_is_ground_2(ModuleInfo, MaybeType, bound(_, List), !Expansions) :-
-    bound_inst_list_is_ground_2(List, MaybeType, ModuleInfo, !Expansions).
-inst_is_ground_2(_, _, ground(_, _), !Expansions).
-inst_is_ground_2(_, _, inst_var(_), !Expansions) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-inst_is_ground_2(ModuleInfo, MaybeType, Inst, !Expansions) :-
-    Inst = constrained_inst_vars(_, Inst2),
-    inst_is_ground_1(ModuleInfo, MaybeType, Inst2, !Expansions).
-inst_is_ground_2(ModuleInfo, MaybeType, Inst, !Expansions) :-
+inst_is_ground_mt_2(ModuleInfo, MaybeType, Inst, !Expansions) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = free
+        ; Inst = free(_)
+        ),
+        fail
+    ;
+        ( Inst = not_reached
+        ; Inst = ground(_, _)
+        )
+    ;
+        Inst = bound(_, List),
+        bound_inst_list_is_ground_mt_2(List, MaybeType, ModuleInfo,
+            !Expansions)
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_ground_mt_1(ModuleInfo, MaybeType, SubInst, !Expansions)
+    ;
     Inst = defined_inst(InstName),
-    inst_lookup(ModuleInfo, InstName, Inst2),
-    inst_is_ground_1(ModuleInfo, MaybeType, Inst2, !Expansions).
-inst_is_ground_2(ModuleInfo, MaybeType, any(Uniq, HOInstInfo), !Expansions) :-
-    maybe_any_to_bound(MaybeType, ModuleInfo, Uniq, HOInstInfo, Inst),
-    inst_is_ground_1(ModuleInfo, MaybeType, Inst, !Expansions).
+        inst_lookup(ModuleInfo, InstName, NextInst),
+        inst_is_ground_mt_1(ModuleInfo, MaybeType, NextInst, !Expansions)
+    ;
+        Inst = any(Uniq, HOInstInfo),
+        maybe_any_to_bound(MaybeType, ModuleInfo, Uniq, HOInstInfo, NextInst),
+        inst_is_ground_mt_1(ModuleInfo, MaybeType, NextInst, !Expansions)
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = abstract_inst(_, _),
+        % XXX I (zs) am not sure this is the right thing to do here.
+        % The original code of this predicate simply did not consider
+        % this kind of Inst.
+        fail
+    ).
 
     % inst_is_ground_or_any succeeds iff the inst passed is `ground', `any',
     % or the equivalent. Fails for abstract insts.
@@ -1539,24 +1733,37 @@
 :- pred inst_is_ground_or_any_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
-inst_is_ground_or_any_2(_, not_reached, !Expansions).
-inst_is_ground_or_any_2(ModuleInfo, bound(_, List), !Expansions) :-
-    bound_inst_list_is_ground_or_any_2(List, ModuleInfo, !Expansions).
-inst_is_ground_or_any_2(_, ground(_, _), !Expansions).
-inst_is_ground_or_any_2(_, any(_, _), !Expansions).
-inst_is_ground_or_any_2(_, inst_var(_), !Expansions) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-inst_is_ground_or_any_2(ModuleInfo, Inst, !Expansions) :-
-    Inst = constrained_inst_vars(_, Inst2),
-    inst_is_ground_or_any_2(ModuleInfo, Inst2, !Expansions).
 inst_is_ground_or_any_2(ModuleInfo, Inst, !Expansions) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = ground(_, _)
+        ; Inst = any(_, _)
+        ; Inst = not_reached
+        )
+    ;
+        Inst = bound(_, BoundInsts),
+        bound_inst_list_is_ground_or_any_2(BoundInsts, ModuleInfo, !Expansions)
+    ;
+        ( Inst = free
+        ; Inst = free(_)
+        ; Inst = abstract_inst(_, _)   % XXX is this right?
+        ),
+        fail
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_ground_or_any_2(ModuleInfo, SubInst, !Expansions)
+    ;
     Inst = defined_inst(InstName),
     ( set.member(Inst, !.Expansions) ->
         true
     ;
         set.insert(Inst, !Expansions),
-        inst_lookup(ModuleInfo, InstName, Inst2),
-        inst_is_ground_or_any_2(ModuleInfo, Inst2, !Expansions)
+            inst_lookup(ModuleInfo, InstName, NextInst),
+            inst_is_ground_or_any_2(ModuleInfo, NextInst, !Expansions)
+        )
     ).
 
     % inst_is_unique succeeds iff the inst passed is unique or free.
@@ -1572,25 +1779,37 @@
 :- pred inst_is_unique_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
-inst_is_unique_2(_, not_reached, !Expansions).
-inst_is_unique_2(ModuleInfo, bound(unique, List), !Expansions) :-
-    bound_inst_list_is_unique_2(List, ModuleInfo, !Expansions).
-inst_is_unique_2(_, any(unique, _), !Expansions).
-inst_is_unique_2(_, free, !Expansions).
-inst_is_unique_2(_, ground(unique, _), !Expansions).
-inst_is_unique_2(_, inst_var(_), !Expansions) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-inst_is_unique_2(ModuleInfo, Inst, !Expansions) :-
-    Inst = constrained_inst_vars(_, Inst2),
-    inst_is_unique_2(ModuleInfo, Inst2, !Expansions).
 inst_is_unique_2(ModuleInfo, Inst, !Expansions) :-
+    (
+        ( Inst = ground(unique, _)
+        ; Inst = any(unique, _)
+        ; Inst = not_reached
+        ; Inst = free               % XXX I don't think this is right [zs].
+        )
+    ;
+        ( Inst = ground(shared, _)
+        ; Inst = bound(shared, _)
+        ; Inst = any(shared, _)
+        ),
+        fail
+    ;
+        Inst = bound(unique, BoundInsts),
+        bound_inst_list_is_unique_2(BoundInsts, ModuleInfo, !Expansions)
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_unique_2(ModuleInfo, SubInst, !Expansions)
+    ;
     Inst = defined_inst(InstName),
     ( set.member(Inst, !.Expansions) ->
         true
     ;
         set.insert(Inst, !Expansions),
-        inst_lookup(ModuleInfo, InstName, Inst2),
-        inst_is_unique_2(ModuleInfo, Inst2, !Expansions)
+            inst_lookup(ModuleInfo, InstName, NextInst),
+            inst_is_unique_2(ModuleInfo, NextInst, !Expansions)
+        )
     ).
 
     % inst_is_mostly_unique succeeds iff the inst passed is unique,
@@ -1606,29 +1825,44 @@
 :- pred inst_is_mostly_unique_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
-inst_is_mostly_unique_2(_, not_reached, !Expansions).
-inst_is_mostly_unique_2(ModuleInfo, bound(unique, List), !Expansions) :-
-    bound_inst_list_is_mostly_unique_2(List, ModuleInfo, !Expansions).
-inst_is_mostly_unique_2(ModuleInfo, bound(mostly_unique, List), !Expansions) :-
-    bound_inst_list_is_mostly_unique_2(List, ModuleInfo, !Expansions).
-inst_is_mostly_unique_2(_, any(unique, _), !Expansions).
-inst_is_mostly_unique_2(_, any(mostly_unique, _), !Expansions).
-inst_is_mostly_unique_2(_, free, !Expansions).
-inst_is_mostly_unique_2(_, ground(unique, _), !Expansions).
-inst_is_mostly_unique_2(_, ground(mostly_unique, _), !Expansions).
-inst_is_mostly_unique_2(_, inst_var(_), !Expansions) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-inst_is_mostly_unique_2(ModuleInfo, Inst, !Expansions) :-
-    Inst = constrained_inst_vars(_, Inst2),
-    inst_is_mostly_unique_2(ModuleInfo, Inst2, !Expansions).
 inst_is_mostly_unique_2(ModuleInfo, Inst, !Expansions) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = not_reached
+        ; Inst = free
+        ; Inst = free(_)
+        ; Inst = ground(unique, _)
+        ; Inst = ground(mostly_unique, _)
+        ; Inst = any(unique, _)
+        ; Inst = any(mostly_unique, _)
+        )
+    ;
+        Inst = bound(unique, List),
+        bound_inst_list_is_mostly_unique_2(List, ModuleInfo, !Expansions)
+    ;
+        Inst = bound(mostly_unique, SubjList),
+        bound_inst_list_is_mostly_unique_2(SubjList, ModuleInfo, !Expansions)
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, NextInst),
+        inst_is_mostly_unique_2(ModuleInfo, NextInst, !Expansions)
+    ;
     Inst = defined_inst(InstName),
     ( set.member(Inst, !.Expansions) ->
         true
     ;
         set.insert(Inst, !Expansions),
-        inst_lookup(ModuleInfo, InstName, Inst2),
-        inst_is_mostly_unique_2(ModuleInfo, Inst2, !Expansions)
+            inst_lookup(ModuleInfo, InstName, NextInst),
+            inst_is_mostly_unique_2(ModuleInfo, NextInst, !Expansions)
+        )
+    ;
+        Inst = abstract_inst(_, _),
+        % XXX I (zs) am not sure this is the right thing to do here.
+        % The original code of this predicate simply did not consider
+        % this kind of Inst.
+        fail
     ).
 
     % inst_is_not_partly_unique succeeds iff the inst passed is not unique
@@ -1644,25 +1878,39 @@
 :- pred inst_is_not_partly_unique_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
-inst_is_not_partly_unique_2(_, not_reached, !Expansions).
-inst_is_not_partly_unique_2(ModuleInfo, bound(shared, List), !Expansions) :-
-    bound_inst_list_is_not_partly_unique_2(List, ModuleInfo, !Expansions).
-inst_is_not_partly_unique_2(_, free, !Expansions).
-inst_is_not_partly_unique_2(_, any(shared, _), !Expansions).
-inst_is_not_partly_unique_2(_, ground(shared, _), !Expansions).
-inst_is_not_partly_unique_2(_, inst_var(_), !Expansions) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-inst_is_not_partly_unique_2(ModuleInfo, Inst, !Expansions) :-
-    Inst = constrained_inst_vars(_, Inst2),
-    inst_is_not_partly_unique_2(ModuleInfo, Inst2, !Expansions).
 inst_is_not_partly_unique_2(ModuleInfo, Inst, !Expansions) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = not_reached
+        ; Inst = free
+        ; Inst = free(_)
+        ; Inst = any(shared, _)
+        ; Inst = ground(shared, _)
+        )
+    ;
+        Inst = bound(shared, List),
+        bound_inst_list_is_not_partly_unique_2(List, ModuleInfo, !Expansions)
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_not_partly_unique_2(ModuleInfo, SubInst, !Expansions)
+    ;
     Inst = defined_inst(InstName),
     ( set.member(Inst, !.Expansions) ->
         true
     ;
         set.insert(Inst, !Expansions),
-        inst_lookup(ModuleInfo, InstName, Inst2),
-        inst_is_not_partly_unique_2(ModuleInfo, Inst2, !Expansions)
+            inst_lookup(ModuleInfo, InstName, NextInst),
+            inst_is_not_partly_unique_2(ModuleInfo, NextInst, !Expansions)
+        )
+    ;
+        Inst = abstract_inst(_, _),
+        % XXX I (zs) am not sure this is the right thing to do here.
+        % The original code of this predicate simply did not consider
+        % this kind of Inst.
+        fail
     ).
 
     % inst_is_not_fully_unique succeeds iff the inst passed is not unique,
@@ -1679,33 +1927,44 @@
 :- pred inst_is_not_fully_unique_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
-inst_is_not_fully_unique_2(_, not_reached, !Expansions).
-inst_is_not_fully_unique_2(ModuleInfo, bound(shared, List),
-        !Expansions) :-
-    bound_inst_list_is_not_fully_unique_2(List, ModuleInfo,
-        !Expansions).
-inst_is_not_fully_unique_2(ModuleInfo, bound(mostly_unique, List),
-        !Expansions) :-
-    bound_inst_list_is_not_fully_unique_2(List, ModuleInfo,
-        !Expansions).
-inst_is_not_fully_unique_2(_, any(shared, _), !Expansions).
-inst_is_not_fully_unique_2(_, any(mostly_unique, _), !Expansions).
-inst_is_not_fully_unique_2(_, free, !Expansions).
-inst_is_not_fully_unique_2(_, ground(shared, _), !Expansions).
-inst_is_not_fully_unique_2(_, ground(mostly_unique, _), !Expansions).
-inst_is_not_fully_unique_2(_, inst_var(_), _, _) :-
-    unexpected($module, $pred, "uninstantiated inst parameter").
-inst_is_not_fully_unique_2(ModuleInfo, Inst, !Expansions) :-
-    Inst = constrained_inst_vars(_, Inst2),
-    inst_is_not_fully_unique_2(ModuleInfo, Inst2, !Expansions).
 inst_is_not_fully_unique_2(ModuleInfo, Inst, !Expansions) :-
+    require_complete_switch [Inst]
+    (
+        ( Inst = not_reached
+        ; Inst = free
+        ; Inst = free(_)
+        ; Inst = ground(shared, _)
+        ; Inst = ground(mostly_unique, _)
+        ; Inst = any(shared, _)
+        ; Inst = any(mostly_unique, _)
+        )
+    ;
+        Inst = bound(shared, List),
+        bound_inst_list_is_not_fully_unique_2(List, ModuleInfo, !Expansions)
+    ;
+        Inst = bound(mostly_unique, List),
+        bound_inst_list_is_not_fully_unique_2(List, ModuleInfo, !Expansions)
+    ;
+        Inst = inst_var(_),
+        unexpected($module, $pred, "uninstantiated inst parameter")
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_is_not_fully_unique_2(ModuleInfo, SubInst, !Expansions)
+    ;
     Inst = defined_inst(InstName),
     ( set.member(Inst, !.Expansions) ->
         true
     ;
         set.insert(Inst, !Expansions),
-        inst_lookup(ModuleInfo, InstName, Inst2),
-        inst_is_not_fully_unique_2(ModuleInfo, Inst2, !Expansions)
+            inst_lookup(ModuleInfo, InstName, NextInst),
+            inst_is_not_fully_unique_2(ModuleInfo, NextInst, !Expansions)
+        )
+    ;
+        Inst = abstract_inst(_, _),
+        % XXX I (zs) am not sure this is the right thing to do here.
+        % The original code of this predicate simply did not consider
+        % this kind of Inst.
+        fail
     ).
 
 %-----------------------------------------------------------------------------%
@@ -1717,64 +1976,66 @@
     module_info::in) is semidet.
 
 bound_inst_list_is_ground([], _, _).
-bound_inst_list_is_ground([bound_functor(Name, Args) | BoundInsts], MaybeType,
-        ModuleInfo) :-
+bound_inst_list_is_ground([BoundInst | BoundInsts], MaybeType, ModuleInfo) :-
+    BoundInst = bound_functor(Name, Args),
     maybe_get_cons_id_arg_types(ModuleInfo, MaybeType, Name,
         list.length(Args), MaybeTypes),
-    inst_list_is_ground(Args, MaybeTypes, ModuleInfo),
+    inst_list_is_ground_mt(Args, MaybeTypes, ModuleInfo),
     bound_inst_list_is_ground(BoundInsts, MaybeType, ModuleInfo).
 
 bound_inst_list_is_ground_or_any([], _).
-bound_inst_list_is_ground_or_any([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo) :-
+bound_inst_list_is_ground_or_any([BoundInst | BoundInsts], ModuleInfo) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_ground_or_any(Args, ModuleInfo),
     bound_inst_list_is_ground_or_any(BoundInsts, ModuleInfo).
 
 bound_inst_list_is_unique([], _).
-bound_inst_list_is_unique([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo) :-
+bound_inst_list_is_unique([BoundInst | BoundInsts], ModuleInfo) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_unique(Args, ModuleInfo),
     bound_inst_list_is_unique(BoundInsts, ModuleInfo).
 
 bound_inst_list_is_mostly_unique([], _).
-bound_inst_list_is_mostly_unique([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo) :-
+bound_inst_list_is_mostly_unique([BoundInst | BoundInsts], ModuleInfo) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_mostly_unique(Args, ModuleInfo),
     bound_inst_list_is_mostly_unique(BoundInsts, ModuleInfo).
 
 bound_inst_list_is_not_partly_unique([], _).
-bound_inst_list_is_not_partly_unique([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo) :-
+bound_inst_list_is_not_partly_unique([BoundInst | BoundInsts], ModuleInfo) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_not_partly_unique(Args, ModuleInfo),
     bound_inst_list_is_not_partly_unique(BoundInsts, ModuleInfo).
 
 bound_inst_list_is_not_fully_unique([], _).
-bound_inst_list_is_not_fully_unique([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo) :-
+bound_inst_list_is_not_fully_unique([BoundInst | BoundInsts], ModuleInfo) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_not_fully_unique(Args, ModuleInfo),
     bound_inst_list_is_not_fully_unique(BoundInsts, ModuleInfo).
 
 %-----------------------------------------------------------------------------%
 
-:- pred bound_inst_list_is_ground_2(list(bound_inst)::in, maybe(mer_type)::in,
-    module_info::in, set_tree234(mer_inst)::in, set_tree234(mer_inst)::out)
-    is semidet.
+:- pred bound_inst_list_is_ground_mt_2(list(bound_inst)::in,
+    maybe(mer_type)::in, module_info::in,
+    set_tree234(mer_inst)::in, set_tree234(mer_inst)::out) is semidet.
 
-bound_inst_list_is_ground_2([], _, _, !Expansions).
-bound_inst_list_is_ground_2([bound_functor(Name, Args) | BoundInsts],
-        MaybeType, ModuleInfo, !Expansions) :-
+bound_inst_list_is_ground_mt_2([], _, _, !Expansions).
+bound_inst_list_is_ground_mt_2([BoundInst | BoundInsts], MaybeType, ModuleInfo,
+        !Expansions) :-
+    BoundInst = bound_functor(Name, Args),
     maybe_get_cons_id_arg_types(ModuleInfo, MaybeType, Name,
         list.length(Args), MaybeTypes),
-    inst_list_is_ground_2(Args, MaybeTypes, ModuleInfo, !Expansions),
-    bound_inst_list_is_ground_2(BoundInsts, MaybeType, ModuleInfo,
+    inst_list_is_ground_mt_2(Args, MaybeTypes, ModuleInfo, !Expansions),
+    bound_inst_list_is_ground_mt_2(BoundInsts, MaybeType, ModuleInfo,
         !Expansions).
 
 :- pred bound_inst_list_is_ground_or_any_2(list(bound_inst)::in,
     module_info::in, set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 bound_inst_list_is_ground_or_any_2([], _, !Expansions).
-bound_inst_list_is_ground_or_any_2([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo, !Expansions) :-
+bound_inst_list_is_ground_or_any_2([BoundInst | BoundInsts], ModuleInfo,
+        !Expansions) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_ground_or_any_2(Args, ModuleInfo, !Expansions),
     bound_inst_list_is_ground_or_any_2(BoundInsts, ModuleInfo, !Expansions).
 
@@ -1782,8 +2043,9 @@
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 bound_inst_list_is_unique_2([], _, !Expansions).
-bound_inst_list_is_unique_2([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo, !Expansions) :-
+bound_inst_list_is_unique_2([BoundInst | BoundInsts], ModuleInfo,
+        !Expansions) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_unique_2(Args, ModuleInfo, !Expansions),
     bound_inst_list_is_unique_2(BoundInsts, ModuleInfo, !Expansions).
 
@@ -1791,18 +2053,19 @@
     module_info::in, set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 bound_inst_list_is_mostly_unique_2([], _, !Expansions).
-bound_inst_list_is_mostly_unique_2([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo, !Expansions) :-
+bound_inst_list_is_mostly_unique_2([BoundInst | BoundInsts], ModuleInfo,
+        !Expansions) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_mostly_unique_2(Args, ModuleInfo, !Expansions),
-    bound_inst_list_is_mostly_unique_2(BoundInsts, ModuleInfo,
-        !Expansions).
+    bound_inst_list_is_mostly_unique_2(BoundInsts, ModuleInfo, !Expansions).
 
 :- pred bound_inst_list_is_not_partly_unique_2(list(bound_inst)::in,
     module_info::in, set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 bound_inst_list_is_not_partly_unique_2([], _, !Expansions).
-bound_inst_list_is_not_partly_unique_2(
-        [bound_functor(_Name, Args) | BoundInsts], ModuleInfo, !Expansions) :-
+bound_inst_list_is_not_partly_unique_2([BoundInst | BoundInsts], ModuleInfo,
+        !Expansions) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_not_partly_unique_2(Args, ModuleInfo, !Expansions),
     bound_inst_list_is_not_partly_unique_2(BoundInsts, ModuleInfo,
         !Expansions).
@@ -1811,25 +2074,27 @@
     module_info::in, set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 bound_inst_list_is_not_fully_unique_2([], _, !Expansions).
-bound_inst_list_is_not_fully_unique_2(
-        [bound_functor(_Name, Args) | BoundInsts], ModuleInfo, !Expansions) :-
+bound_inst_list_is_not_fully_unique_2([BoundInst | BoundInsts], ModuleInfo,
+        !Expansions) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_not_fully_unique_2(Args, ModuleInfo, !Expansions),
     bound_inst_list_is_not_fully_unique_2(BoundInsts, ModuleInfo,
         !Expansions).
 
 %-----------------------------------------------------------------------------%
 
-inst_list_is_ground(Insts, ModuleInfo) :-
-    MaybeTypes = list.duplicate(list.length(Insts), no),
-    inst_list_is_ground(Insts, MaybeTypes, ModuleInfo).
-
-:- pred inst_list_is_ground(list(mer_inst)::in, list(maybe(mer_type))::in,
+:- pred inst_list_is_ground_mt(list(mer_inst)::in, list(maybe(mer_type))::in,
     module_info::in) is semidet.
 
-inst_list_is_ground([], [], _).
-inst_list_is_ground([Inst | Insts], [MaybeType | MaybeTypes], ModuleInfo) :-
-    inst_is_ground(ModuleInfo, MaybeType, Inst),
-    inst_list_is_ground(Insts, MaybeTypes, ModuleInfo).
+inst_list_is_ground_mt([], [], _).
+inst_list_is_ground_mt([Inst | Insts], [MaybeType | MaybeTypes], ModuleInfo) :-
+    inst_is_ground_mt(ModuleInfo, MaybeType, Inst),
+    inst_list_is_ground_mt(Insts, MaybeTypes, ModuleInfo).
+
+inst_list_is_ground([], _).
+inst_list_is_ground([Inst | Insts], ModuleInfo) :-
+    inst_is_ground(ModuleInfo, Inst),
+    inst_list_is_ground(Insts, ModuleInfo).
 
 inst_list_is_ground_or_any([], _).
 inst_list_is_ground_or_any([Inst | Insts], ModuleInfo) :-
@@ -1858,19 +2123,19 @@
 
 %-----------------------------------------------------------------------------%
 
-:- pred inst_list_is_ground_2(list(mer_inst)::in, list(maybe(mer_type))::in,
+:- pred inst_list_is_ground_mt_2(list(mer_inst)::in, list(maybe(mer_type))::in,
     module_info::in, set_tree234(mer_inst)::in, set_tree234(mer_inst)::out)
     is semidet.
 
-inst_list_is_ground_2([], [], _, !Expansions).
-inst_list_is_ground_2([], [_ | _], _, !Expansions) :-
+inst_list_is_ground_mt_2([], [], _, !Expansions).
+inst_list_is_ground_mt_2([], [_ | _], _, !Expansions) :-
     unexpected($module, $pred, "length mismatch").
-inst_list_is_ground_2([_ | _], [], _, !Expansions) :-
+inst_list_is_ground_mt_2([_ | _], [], _, !Expansions) :-
     unexpected($module, $pred, "length mismatch").
-inst_list_is_ground_2([Inst | Insts], [MaybeType | MaybeTypes], ModuleInfo,
+inst_list_is_ground_mt_2([Inst | Insts], [MaybeType | MaybeTypes], ModuleInfo,
         !Expansions) :-
-    inst_is_ground_1(ModuleInfo, MaybeType, Inst, !Expansions),
-    inst_list_is_ground_2(Insts, MaybeTypes, ModuleInfo, !Expansions).
+    inst_is_ground_mt_1(ModuleInfo, MaybeType, Inst, !Expansions),
+    inst_list_is_ground_mt_2(Insts, MaybeTypes, ModuleInfo, !Expansions).
 
 :- pred inst_list_is_ground_or_any_2(list(mer_inst)::in, module_info::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
@@ -1915,8 +2180,8 @@
 %-----------------------------------------------------------------------------%
 
 bound_inst_list_is_free([], _).
-bound_inst_list_is_free([bound_functor(_Name, Args) | BoundInsts],
-        ModuleInfo) :-
+bound_inst_list_is_free([BoundInst | BoundInsts], ModuleInfo) :-
+    BoundInst = bound_functor(_Name, Args),
     inst_list_is_free(Args, ModuleInfo),
     bound_inst_list_is_free(BoundInsts, ModuleInfo).
 
@@ -1961,49 +2226,57 @@
 :- pred inst_contains_instname_2(mer_inst::in, module_info::in, inst_name::in,
     bool::out, inst_names::in, inst_names::out) is det.
 
-inst_contains_instname_2(abstract_inst(_, _), _, _, no, !Expansions).
-inst_contains_instname_2(any(_, _), _, _, no, !Expansions).
-inst_contains_instname_2(free, _, _, no, !Expansions).
-inst_contains_instname_2(free(_T), _, _, no, !Expansions).
-inst_contains_instname_2(ground(_Uniq, _), _, _, no, !Expansions).
-inst_contains_instname_2(inst_var(_), _, _, no, !Expansions).
-inst_contains_instname_2(not_reached, _, _, no, !Expansions).
-inst_contains_instname_2(constrained_inst_vars(_, Inst), ModuleInfo, InstName,
-        Result, !Expansions) :-
-    inst_contains_instname_2(Inst, ModuleInfo, InstName, Result,
-        !Expansions).
-inst_contains_instname_2(defined_inst(InstName1), ModuleInfo, InstName,
-        Result, !Expansions) :-
-    ( InstName = InstName1 ->
-        Result = yes
-    ;
-        ( set.member(InstName1, !.Expansions) ->
-            Result = no
-        ;
-            inst_lookup(ModuleInfo, InstName1, Inst1),
-            set.insert(InstName1, !Expansions),
-            inst_contains_instname_2(Inst1, ModuleInfo, InstName, Result,
+inst_contains_instname_2(Inst, ModuleInfo, InstName, Contains, !Expansions) :-
+    (
+        ( Inst = abstract_inst(_, _)
+        ; Inst = any(_, _)
+        ; Inst = free
+        ; Inst = free(_)
+        ; Inst = ground(_, _)
+        ; Inst = inst_var(_)
+        ; Inst = not_reached
+        ),
+        Contains = no
+    ;
+        Inst = constrained_inst_vars(_, SubInst),
+        inst_contains_instname_2(SubInst, ModuleInfo, InstName, Contains,
                 !Expansions)
+    ;
+        Inst = defined_inst(ThisInstName),
+        ( InstName = ThisInstName ->
+            Contains = yes
+        ;
+            ( set.member(ThisInstName, !.Expansions) ->
+                Contains = no
+            ;
+                inst_lookup(ModuleInfo, ThisInstName, ThisInst),
+                set.insert(ThisInstName, !Expansions),
+                inst_contains_instname_2(ThisInst, ModuleInfo, InstName,
+                    Contains, !Expansions)
         )
-    ).
-inst_contains_instname_2(bound(_Uniq, ArgInsts), ModuleInfo,
-        InstName, Result, !Expansions) :-
+        )
+    ;
+        Inst = bound(_Uniq, ArgInsts),
     % XXX This code has a performance problem.
     %
-    % The problem is that e.g. in a list of length N, you'll have N variables
-    % for the skeletons whose insts contain an average of N/2 occurences of
-    % `bound' each, so the complexity of running inst_contains_instname_2
-    % on all their insts is quadratic in N.
+        % The problem is that e.g. in a list of length N, you will have N
+        % variables for the skeletons whose insts contain an average of N/2
+        % occurences of `bound' each, so the complexity of running
+        % inst_contains_instname_2 on all their insts is quadratic in N.
     %
     % One solution to this would be to add an extra argument to bound/2
-    % that gives the set of included inst_names, or simply asserts that this
-    % set is empty. This field can be set at the time of the construction
-    % of the inst, avoiding quadratic behavior in inst_contains_instname_2.
-    % The complexity of constructing all the insts will remain quadratic in N,
-    % of course.
+        % that gives the set of included inst_names, or simply asserts that
+        % this set is empty. This field can be set at the time of the
+        % construction of the inst, avoiding quadratic behavior in
+        % inst_contains_instname_2. The complexity of constructing may be
+        % quadratic in N, of course.
+        %
+        % We could try to solve this performance problem with a cache
+        % of the results of recent invocations of inst_contains_instname.
 
     bound_inst_list_contains_instname(ArgInsts, ModuleInfo,
-        InstName, Result, !Expansions).
+            InstName, Contains, !Expansions)
+    ).
 
 :- pred bound_inst_list_contains_instname(list(bound_inst)::in,
     module_info::in, inst_name::in, bool::out,
@@ -2011,32 +2284,33 @@
 
 bound_inst_list_contains_instname([], _ModuleInfo, _InstName, no, !Expansions).
 bound_inst_list_contains_instname([BoundInst | BoundInsts], ModuleInfo,
-        InstName, Result, !Expansions) :-
+        InstName, Contains, !Expansions) :-
     BoundInst = bound_functor(_Functor, ArgInsts),
-    inst_list_contains_instname(ArgInsts, ModuleInfo, InstName, Result1,
+    inst_list_contains_instname(ArgInsts, ModuleInfo, InstName, Contains1,
         !Expansions),
     (
-        Result1 = yes,
-        Result = yes
+        Contains1 = yes,
+        Contains = yes
     ;
-        Result1 = no,
+        Contains1 = no,
         bound_inst_list_contains_instname(BoundInsts, ModuleInfo,
-            InstName, Result, !Expansions)
+            InstName, Contains, !Expansions)
     ).
 
 :- pred inst_list_contains_instname(list(mer_inst)::in, module_info::in,
     inst_name::in, bool::out, inst_names::in, inst_names::out) is det.
 
 inst_list_contains_instname([], _ModuleInfo, _InstName, no, !Expansions).
-inst_list_contains_instname([Inst | Insts], ModuleInfo, InstName, Result,
+inst_list_contains_instname([Inst | Insts], ModuleInfo, InstName, Contains,
         !Expansions) :-
-    inst_contains_instname_2(Inst, ModuleInfo, InstName, Result1, !Expansions),
+    inst_contains_instname_2(Inst, ModuleInfo, InstName, Contains1,
+        !Expansions),
     (
-        Result1 = yes,
-        Result = yes
+        Contains1 = yes,
+        Contains = yes
     ;
-        Result1 = no,
-        inst_list_contains_instname(Insts, ModuleInfo, InstName, Result,
+        Contains1 = no,
+        inst_list_contains_instname(Insts, ModuleInfo, InstName, Contains,
             !Expansions)
     ).
 
@@ -2044,42 +2318,60 @@
 
 :- pred inst_name_contains_inst_var(inst_name::in, inst_var::out) is nondet.
 
-inst_name_contains_inst_var(user_inst(_Name, ArgInsts), InstVar) :-
-    inst_list_contains_inst_var(ArgInsts, InstVar).
-inst_name_contains_inst_var(merge_inst(InstA, InstB), InstVar) :-
+inst_name_contains_inst_var(InstName, InstVar) :-
+    require_complete_switch [InstName]
+    (
+        InstName = user_inst(_Name, ArgInsts),
+        inst_list_contains_inst_var(ArgInsts, InstVar)
+    ;
+        InstName = merge_inst(InstA, InstB),
     ( inst_contains_inst_var(InstA, InstVar)
     ; inst_contains_inst_var(InstB, InstVar)
-    ).
-inst_name_contains_inst_var(unify_inst(_Live, InstA, InstB, _Real), InstVar) :-
+        )
+    ;
+        InstName = unify_inst(_Live, InstA, InstB, _Real),
     ( inst_contains_inst_var(InstA, InstVar)
     ; inst_contains_inst_var(InstB, InstVar)
+        )
+    ;
+        InstName = ground_inst(SubInstName, _Live, _Uniq, _Real),
+        inst_name_contains_inst_var(SubInstName, InstVar)
+    ;
+        InstName = any_inst(SubInstName, _Live, _Uniq, _Real),
+        inst_name_contains_inst_var(SubInstName, InstVar)
+    ;
+        InstName = shared_inst(SubInstName),
+        inst_name_contains_inst_var(SubInstName, InstVar)
+    ;
+        InstName = mostly_uniq_inst(SubInstName),
+        inst_name_contains_inst_var(SubInstName, InstVar)
+    ;
+        InstName = typed_ground(_Uniq, _Type),
+        fail
+    ;
+        InstName = typed_inst(_Type, SubInstName),
+        inst_name_contains_inst_var(SubInstName, InstVar)
     ).
-inst_name_contains_inst_var(ground_inst(InstName, _Live, _Uniq, _Real),
-        InstVar) :-
-    inst_name_contains_inst_var(InstName, InstVar).
-inst_name_contains_inst_var(any_inst(InstName, _Live, _Uniq, _Real),
-        InstVar) :-
-    inst_name_contains_inst_var(InstName, InstVar).
-inst_name_contains_inst_var(shared_inst(InstName), InstVar) :-
-    inst_name_contains_inst_var(InstName, InstVar).
-inst_name_contains_inst_var(mostly_uniq_inst(InstName), InstVar) :-
-    inst_name_contains_inst_var(InstName, InstVar).
-inst_name_contains_inst_var(typed_ground(_Uniq, _Type), _InstVar) :- fail.
-inst_name_contains_inst_var(typed_inst(_Type, InstName), InstVar) :-
-    inst_name_contains_inst_var(InstName, InstVar).
 
 :- pred inst_contains_inst_var(mer_inst::in, inst_var::out) is nondet.
 
-inst_contains_inst_var(inst_var(InstVar), InstVar).
-inst_contains_inst_var(defined_inst(InstName), InstVar) :-
-    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, HOInstInfo), InstVar) :-
+inst_contains_inst_var(Inst, InstVar) :-
+    (
+        Inst = inst_var(InstVar)
+    ;
+        Inst = defined_inst(InstName),
+        inst_name_contains_inst_var(InstName, InstVar)
+    ;
+        Inst = bound(_Uniq, ArgInsts),
+        bound_inst_list_contains_inst_var(ArgInsts, InstVar)
+    ;
+        Inst = ground(_Uniq, HOInstInfo),
     HOInstInfo = 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).
+        mode_list_contains_inst_var(Modes, InstVar)
+    ;
+        Inst = abstract_inst(_Name, ArgInsts),
+        inst_list_contains_inst_var(ArgInsts, InstVar)
+    ).
 
 :- pred bound_inst_list_contains_inst_var(list(bound_inst)::in, inst_var::out)
     is nondet.
@@ -2108,10 +2400,12 @@
 :- pred mode_list_contains_inst_var(list(mer_mode)::in, inst_var::out)
     is nondet.
 
-mode_list_contains_inst_var([Mode | _Modes], InstVar) :-
-    mode_contains_inst_var(Mode, InstVar).
-mode_list_contains_inst_var([_ | Modes], InstVar) :-
-    mode_list_contains_inst_var(Modes, InstVar).
+mode_list_contains_inst_var([Mode | Modes], InstVar) :-
+    (
+        mode_contains_inst_var(Mode, InstVar)
+    ;
+        mode_list_contains_inst_var(Modes, InstVar)
+    ).
 
 :- pred mode_contains_inst_var(mer_mode::in, inst_var::out) is nondet.
 
@@ -2159,7 +2453,8 @@
 :- pred type_may_contain_solver_type(module_info::in, mer_type::in) is semidet.
 
 type_may_contain_solver_type(ModuleInfo, Type) :-
-    type_may_contain_solver_type_2(classify_type(ModuleInfo, Type)) = yes.
+    TypeCtorCat = classify_type(ModuleInfo, Type),
+    type_may_contain_solver_type_2(TypeCtorCat) = yes.
 
 :- func type_may_contain_solver_type_2(type_ctor_category) = bool.
 
cvs diff: Diffing compiler/notes
cvs diff: Diffing deep_profiler
cvs diff: Diffing deep_profiler/notes
cvs diff: Diffing doc
cvs diff: Diffing extras
cvs diff: Diffing extras/base64
cvs diff: Diffing extras/cgi
cvs diff: Diffing extras/complex_numbers
cvs diff: Diffing extras/complex_numbers/samples
cvs diff: Diffing extras/complex_numbers/tests
cvs diff: Diffing extras/curs
cvs diff: Diffing extras/curs/samples
cvs diff: Diffing extras/curses
cvs diff: Diffing extras/curses/sample
cvs diff: Diffing extras/dynamic_linking
cvs diff: Diffing extras/error
cvs diff: Diffing extras/fixed
cvs diff: Diffing extras/gator
cvs diff: Diffing extras/gator/generations
cvs diff: Diffing extras/gator/generations/1
cvs diff: Diffing extras/graphics
cvs diff: Diffing extras/graphics/easyx
cvs diff: Diffing extras/graphics/easyx/samples
cvs diff: Diffing extras/graphics/mercury_allegro
cvs diff: Diffing extras/graphics/mercury_allegro/examples
cvs diff: Diffing extras/graphics/mercury_allegro/samples
cvs diff: Diffing extras/graphics/mercury_allegro/samples/demo
cvs diff: Diffing extras/graphics/mercury_allegro/samples/mandel
cvs diff: Diffing extras/graphics/mercury_allegro/samples/pendulum2
cvs diff: Diffing extras/graphics/mercury_allegro/samples/speed
cvs diff: Diffing extras/graphics/mercury_cairo
cvs diff: Diffing extras/graphics/mercury_cairo/samples
cvs diff: Diffing extras/graphics/mercury_cairo/samples/data
cvs diff: Diffing extras/graphics/mercury_cairo/tutorial
cvs diff: Diffing extras/graphics/mercury_glfw
cvs diff: Diffing extras/graphics/mercury_glfw/samples
cvs diff: Diffing extras/graphics/mercury_glut
cvs diff: Diffing extras/graphics/mercury_opengl
cvs diff: Diffing extras/graphics/mercury_tcltk
cvs diff: Diffing extras/graphics/samples
cvs diff: Diffing extras/graphics/samples/calc
cvs diff: Diffing extras/graphics/samples/gears
cvs diff: Diffing extras/graphics/samples/maze
cvs diff: Diffing extras/graphics/samples/pent
cvs diff: Diffing extras/lazy_evaluation
cvs diff: Diffing extras/lex
cvs diff: Diffing extras/lex/samples
cvs diff: Diffing extras/lex/tests
cvs diff: Diffing extras/log4m
cvs diff: Diffing extras/logged_output
cvs diff: Diffing extras/monte
cvs diff: Diffing extras/moose
cvs diff: Diffing extras/moose/samples
cvs diff: Diffing extras/moose/tests
cvs diff: Diffing extras/mopenssl
cvs diff: Diffing extras/morphine
cvs diff: Diffing extras/morphine/non-regression-tests
cvs diff: Diffing extras/morphine/scripts
cvs diff: Diffing extras/morphine/source
cvs diff: Diffing extras/net
cvs diff: Diffing extras/odbc
cvs diff: Diffing extras/posix
cvs diff: Diffing extras/posix/samples
cvs diff: Diffing extras/quickcheck
cvs diff: Diffing extras/quickcheck/tutes
cvs diff: Diffing extras/references
cvs diff: Diffing extras/references/samples
cvs diff: Diffing extras/references/tests
cvs diff: Diffing extras/solver_types
cvs diff: Diffing extras/solver_types/library
cvs diff: Diffing extras/trailed_update
cvs diff: Diffing extras/trailed_update/samples
cvs diff: Diffing extras/trailed_update/tests
cvs diff: Diffing extras/windows_installer_generator
cvs diff: Diffing extras/windows_installer_generator/sample
cvs diff: Diffing extras/windows_installer_generator/sample/images
cvs diff: Diffing extras/xml
cvs diff: Diffing extras/xml/samples
cvs diff: Diffing extras/xml_stylesheets
cvs diff: Diffing java
cvs diff: Diffing java/runtime
cvs diff: Diffing library
Index: library/fat_sparse_bitset.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/fat_sparse_bitset.m,v
retrieving revision 1.1
diff -u -b -r1.1 fat_sparse_bitset.m
--- library/fat_sparse_bitset.m	22 Aug 2011 06:33:02 -0000	1.1
+++ library/fat_sparse_bitset.m	29 Mar 2012 07:00:30 -0000
@@ -123,6 +123,13 @@
 :- pred insert(T::in, fat_sparse_bitset(T)::in, fat_sparse_bitset(T)::out)
     is det <= enum(T).
 
+    % `try_and_insert(X, Set0, Set)' returns the union of `Set0' and the set
+    % containing only `X' if `Set0' does not already contain `X'; if it does,
+    % it fails. Takes O(rep_size(Set)) time and space.
+    %
+:- pred try_and_insert(T::in,
+    fat_sparse_bitset(T)::in, fat_sparse_bitset(T)::out) is semidet <= enum(T).
+
     % `insert_list(Set, X)' returns the union of `Set' and the set containing
     % only the members of `X'. Same as `union(Set, list_to_set(X))', but may be
     % more efficient.
@@ -744,18 +751,20 @@
 
 %-----------------------------------------------------------------------------%
 
-insert(E, !Set) :-
-    !:Set = insert(!.Set, E).
+insert(Set0, E) = Set :-
+    insert(E, Set0, Set).
 
-insert(fat_sparse_bitset(Set), Elem) =
-    fat_sparse_bitset(insert_2(Set, enum.to_int(Elem))).
+insert(E, !Set) :-
+    !.Set = fat_sparse_bitset(Set0),
+    insert_2(Set0, enum.to_int(E), Set),
+    !:Set = fat_sparse_bitset(Set).
 
-:- func insert_2(fat_bitset_impl, int) = fat_bitset_impl.
+:- pred insert_2(fat_bitset_impl::in, int::in, fat_bitset_impl::out) is det.
 
-insert_2(empty, Index) = Set :-
+insert_2(empty, Index, Set) :-
     bits_for_index(Index, Offset, Bits),
     Set = node(Offset, Bits, empty).
-insert_2(Set0 @ node(Offset0, Bits0, Rest0), Index) = Set :-
+insert_2(Set0 @ node(Offset0, Bits0, Rest0), Index, Set) :-
     % Set0 = [Data0 | Rest],
     % Offset0 = Data0 ^ offset,
     ( Index < Offset0 ->
@@ -769,9 +778,43 @@
             Set = Set0
         )
     ;
-        Set = node(Offset0, Bits0, insert_2(Rest0, Index))
+        insert_2(Rest0, Index, Set1),
+        Set = node(Offset0, Bits0, Set1)
     ).
 
+%-----------------------------------------------------------------------------%
+
+try_and_insert(E, !Set) :-
+    !.Set = fat_sparse_bitset(Set0),
+    try_and_insert_2(Set0, enum.to_int(E), Set),
+    !:Set = fat_sparse_bitset(Set).
+
+:- pred try_and_insert_2(fat_bitset_impl::in, int::in, fat_bitset_impl::out)
+    is semidet.
+
+try_and_insert_2(empty, Index, Set) :-
+    bits_for_index(Index, Offset, Bits),
+    Set = node(Offset, Bits, empty).
+try_and_insert_2(Set0 @ node(Offset0, Bits0, Rest0), Index, Set) :-
+    % Set0 = [Data0 | Rest],
+    % Offset0 = Data0 ^ offset,
+    ( Index < Offset0 ->
+        bits_for_index(Index, Offset, Bits),
+        Set = node(Offset, Bits, Set0)
+    ; BitToSet = Index - Offset0, BitToSet < bits_per_int ->
+        ( get_bit(Bits0, BitToSet) = 0 ->
+            Bits = set_bit(Bits0, BitToSet),
+            Set = node(Offset0, Bits, Rest0)
+        ;
+            fail
+        )
+    ;
+        try_and_insert_2(Rest0, Index, Set1),
+        Set = node(Offset0, Bits0, Set1)
+    ).
+
+%-----------------------------------------------------------------------------%
+
 insert_list(List, !Set) :-
     !:Set = insert_list(!.Set, List).
 
Index: library/set.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/set.m,v
retrieving revision 1.97
diff -u -b -r1.97 set.m
--- library/set.m	26 Mar 2012 23:36:15 -0000	1.97
+++ library/set.m	29 Mar 2012 04:59:55 -0000
@@ -115,6 +115,11 @@
 :- func set.insert(set(T), T) = set(T).
 :- pred set.insert(T::in, set(T)::in, set(T)::out) is det.
 
+    % `set.try_and_insert(X, Set0, Set)' is true iff `Set0' does not contain
+    % `X', and `Set' is the union of `Set0' and the set containing only `X'.
+    %
+:- pred set.try_and_insert(T::in, set(T)::in, set(T)::out) is semidet.
+
     % `set.insert_list(Xs, Set0, Set)' is true iff `Set' is the union of
     % `Set0' and the set containing only the members of `Xs'.
     %
@@ -474,6 +479,9 @@
 set.insert(X, !Set) :-
     set_ordlist.insert(X, !Set).
 
+set.try_and_insert(X, !Set) :-
+    set_ordlist.try_and_insert(X, !Set).
+
 set.equal(SetA, SetB) :-
     set_ordlist.equal(SetA, SetB).
 
Index: library/set_bbbtree.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/set_bbbtree.m,v
retrieving revision 1.40
diff -u -b -r1.40 set_bbbtree.m
--- library/set_bbbtree.m	17 Jan 2012 15:49:45 -0000	1.40
+++ library/set_bbbtree.m	29 Mar 2012 06:21:47 -0000
@@ -103,6 +103,13 @@
 
 :- func set_bbbtree.insert(set_bbbtree(T), T) = set_bbbtree(T).
 
+    % `set_bbbtree.try_and_insert(X, Set0, Set)' is true iff `Set0' does not
+    % contain `X', and `Set' is the union of `Set0' and the set containing
+    % only `X'.
+    %
+:- pred set_bbbtree.try_and_insert(T::in,
+    set_bbbtree(T)::in, set_bbbtree(T)::out) is semidet.
+
     % `set_bbbtree.insert_list(Xs, Set0, Set)' is true iff `Set' is
     % the union of `Set0' and the set containing only the members of `Xs'.
     %
@@ -553,23 +560,19 @@
 set_bbbtree.insert(!.S, T) = !:S :-
     set_bbbtree.insert(T, !S).
 
-% This is a hack to handle the bugs with unique and destructive input modes.
 set_bbbtree.insert(X, !Set) :-
+    % This is a hack to handle the bugs with unique and destructive
+    % input modes.
     set_bbbtree.def_ratio(Ratio),
     set_bbbtree.insert_r(!.Set, X, !:Set, Ratio),
+    % When destructive input and unique modes are fixed, remove this.
     unsafe_promise_unique(!Set).
 
-% Uncomment this once destructive input and unique modes are fixed and delete
-% the one above.
-% set_bbbtree.insert(Set0, X, Set) :-
-%   set_bbbtree.def_ratio(Ratio),
-%   set_bbbtree.insert_r(Set0, X, Set, Ratio).
-
 :- pred set_bbbtree.insert_r(set_bbbtree(T)::in, T::in, set_bbbtree(T)::out,
     int::in) is det.
 
-    % X was not in the set so make new node with X as the value
 set_bbbtree.insert_r(empty, X, tree(X, 1, empty, empty), _Ratio).
+    % X was not in the set so make new node with X as the value.
 set_bbbtree.insert_r(tree(V, N, L, R), X, Set, Ratio) :-
     compare(Result, X, V),
     (
@@ -588,6 +591,35 @@
         Set = tree(V, N, L, R)
     ).
 
+set_bbbtree.try_and_insert(X, !Set) :-
+    % This is a hack to handle the bugs with unique and destructive
+    % input modes.
+    set_bbbtree.def_ratio(Ratio),
+    set_bbbtree.try_and_insert_r(!.Set, X, !:Set, Ratio).
+
+:- pred set_bbbtree.try_and_insert_r(
+    set_bbbtree(T)::in, T::in, set_bbbtree(T)::out, int::in) is semidet.
+
+set_bbbtree.try_and_insert_r(empty, X, tree(X, 1, empty, empty), _Ratio).
+    % X was not in the set so make new node with X as the value.
+set_bbbtree.try_and_insert_r(tree(V, _N, L, R), X, Set, Ratio) :-
+    compare(Result, X, V),
+    (
+        % Insert X into left subtree and re-balance it.
+        Result = (<),
+        set_bbbtree.try_and_insert_r(L, X, NewL, Ratio),
+        set_bbbtree.balance(V, NewL, R, Set, Ratio)
+    ;
+        % Insert X into right subtree and re-balance it.
+        Result = (>),
+        set_bbbtree.try_and_insert_r(R, X, NewR, Ratio),
+        set_bbbtree.balance(V, L, NewR, Set, Ratio)
+    ;
+        % X already in tree.
+        Result = (=),
+        fail
+    ).
+
 %------------------------------------------------------------------------------%
 
 set_bbbtree.insert_list(!.S, Xs) = !:S :-
Index: library/set_ctree234.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/set_ctree234.m,v
retrieving revision 1.17
diff -u -b -r1.17 set_ctree234.m
--- library/set_ctree234.m	17 Jan 2012 15:49:45 -0000	1.17
+++ library/set_ctree234.m	29 Mar 2012 06:39:14 -0000
@@ -119,6 +119,13 @@
 :- pred set_ctree234.insert(T::in, set_ctree234(T)::in, set_ctree234(T)::out)
     is det.
 
+    % `set_ctree234.try_and_insert(X, Set0, Set)' is true iff `Set0' does
+    % not contain `X', and `Set' is the union of `Set0' and the set containing
+    % only `X'.
+    %
+:- pred set_ctree234.try_and_insert(T::in,
+    set_ctree234(T)::in, set_ctree234(T)::out) is semidet.
+
     % `set_ctree234.insert_list(Xs, Set0, Set)' is true iff `Set' is the
     % union of `Set0' and the set containing only the members of `Xs'.
     %
@@ -789,8 +796,8 @@
     set_ctree234.do_insert(E, Incr, Tin, Tout),
     Sizeout = Sizein + Incr.
 
-:- pred set_ctree234.do_insert(T::in, int::out, set_tree234(T)::in,
-    set_tree234(T)::out) is det.
+:- pred set_ctree234.do_insert(T::in, int::out,
+    set_tree234(T)::in, set_tree234(T)::out) is det.
 
 set_ctree234.do_insert(E, Incr, Tin, Tout) :-
     (
@@ -863,6 +870,8 @@
                 ;
                     Result1 = (=),
                     Incr = 0,
+                    % The Tout we are returning does not have the same
+                    % shape as Tin, but it contains the same elements.
                     Tout = three(MT0E, E0, T00, T01, T1)
                 ;
                     Result1 = (>),
@@ -899,6 +908,8 @@
                     Tout = three(E0, MT1E, T0, NewT10, T11)
                 ;
                     Result1 = (=),
+                    % The Tout we are returning does not have the same
+                    % shape as Tin, but it contains the same elements.
                     Incr = 0,
                     Tout = three(E0, MT1E, T0, T10, T11)
                 ;
@@ -973,6 +984,8 @@
                     Tout = four(MT0E, E0, E1, NewT00, T01, T1, T2)
                 ;
                     ResultM = (=),
+                    % The Tout we are returning does not have the same
+                    % shape as Tin, but it contains the same elements.
                     Incr = 0,
                     Tout = four(MT0E, E0, E1, T00, T01, T1, T2)
                 ;
@@ -1013,6 +1026,8 @@
                         Tout = four(E0, MT1E, E1, T0, NewT10, T11, T2)
                     ;
                         ResultM = (=),
+                        % The Tout we are returning does not have the same
+                        % shape as Tin, but it contains the same elements.
                         Incr = 0,
                         Tout = four(E0, MT1E, E1, T0, T10, T11, T2)
                     ;
@@ -1050,6 +1065,8 @@
                         Tout = four(E0, E1, MT2E, T0, T1, NewT20, T21)
                     ;
                         ResultM = (=),
+                        % The Tout we are returning does not have the same
+                        % shape as Tin, but it contains the same elements.
                         Incr = 0,
                         Tout = four(E0, E1, MT2E, T0, T1, T20, T21)
                     ;
@@ -1075,6 +1092,277 @@
         )
     ).
 
+%------------------------------------------------------------------------------%
+
+set_ctree234.try_and_insert(E, ct(Sizein, Tin), ct(Sizeout, Tout)) :-
+    set_ctree234.do_try_and_insert(E, Tin, Tout),
+    Sizeout = Sizein + 1.
+
+:- pred set_ctree234.do_try_and_insert(T::in,
+    set_tree234(T)::in, set_tree234(T)::out) is semidet.
+
+set_ctree234.do_try_and_insert(E, Tin, Tout) :-
+    (
+        Tin = empty,
+        Tout = two(E, empty, empty)
+    ;
+        Tin = two(_, _, _),
+        set_ctree234.try_and_insert2(E, Tin, Tout)
+    ;
+        Tin = three(_, _, _, _, _),
+        set_ctree234.try_and_insert3(E, Tin, Tout)
+    ;
+        Tin = four(E0, E1, E2, T0, T1, T2, T3),
+        compare(Result1, E, E1),
+        (
+            Result1 = (<),
+            Sub0 = two(E0, T0, T1),
+            Sub1 = two(E2, T2, T3),
+            set_ctree234.try_and_insert2(E, Sub0, NewSub0),
+            Tout = two(E1, NewSub0, Sub1)
+        ;
+            Result1 = (=),
+            fail
+        ;
+            Result1 = (>),
+            Sub0 = two(E0, T0, T1),
+            Sub1 = two(E2, T2, T3),
+            set_ctree234.try_and_insert2(E, Sub1, NewSub1),
+            Tout = two(E1, Sub0, NewSub1)
+        )
+    ).
+
+:- pred set_ctree234.try_and_insert2(T::in,
+    set_tree234(T)::in_two, set_tree234(T)::out) is semidet.
+
+set_ctree234.try_and_insert2(E, Tin, Tout) :-
+    Tin = two(E0, T0, T1),
+    (
+        T0 = empty
+        % T1 = empty implied by T0 = empty
+    ->
+        compare(Result, E, E0),
+        (
+            Result = (<),
+            Tout = three(E, E0, empty, empty, empty)
+        ;
+            Result = (=),
+            fail
+        ;
+            Result = (>),
+            Tout = three(E0, E, empty, empty, empty)
+        )
+    ;
+        compare(Result, E, E0),
+        (
+            Result = (<),
+            (
+                T0 = four(_, _, _, _, _, _, _),
+                set_ctree234.split_four(T0, MT0E, T00, T01),
+                compare(Result1, E, MT0E),
+                (
+                    Result1 = (<),
+                    set_ctree234.try_and_insert2(E, T00, NewT00),
+                    Tout = three(MT0E, E0, NewT00, T01, T1)
+                ;
+                    Result1 = (=),
+                    fail
+                ;
+                    Result1 = (>),
+                    set_ctree234.try_and_insert2(E, T01, NewT01),
+                    Tout = three(MT0E, E0, T00, NewT01, T1)
+                )
+            ;
+                T0 = three(_, _, _, _, _),
+                set_ctree234.try_and_insert3(E, T0, NewT0),
+                Tout = two(E0, NewT0, T1)
+            ;
+                T0 = two(_, _, _),
+                set_ctree234.try_and_insert2(E, T0, NewT0),
+                Tout = two(E0, NewT0, T1)
+            ;
+                T0 = empty,
+                NewT0 = two(E, empty, empty),
+                Tout = two(E0, NewT0, T1)
+            )
+        ;
+            Result = (=),
+            fail
+        ;
+            Result = (>),
+            (
+                T1 = four(_, _, _, _, _, _, _),
+                set_ctree234.split_four(T1, MT1E, T10, T11),
+                compare(Result1, E, MT1E),
+                (
+                    Result1 = (<),
+                    set_ctree234.try_and_insert2(E, T10, NewT10),
+                    Tout = three(E0, MT1E, T0, NewT10, T11)
+                ;
+                    Result1 = (=),
+                    fail
+                ;
+                    Result1 = (>),
+                    set_ctree234.try_and_insert2(E, T11, NewT11),
+                    Tout = three(E0, MT1E, T0, T10, NewT11)
+                )
+            ;
+                T1 = three(_, _, _, _, _),
+                set_ctree234.try_and_insert3(E, T1, NewT1),
+                Tout = two(E0, T0, NewT1)
+            ;
+                T1 = two(_, _, _),
+                set_ctree234.try_and_insert2(E, T1, NewT1),
+                Tout = two(E0, T0, NewT1)
+            ;
+                T1 = empty,
+                NewT1 = two(E, empty, empty),
+                Tout = two(E0, T0, NewT1)
+            )
+        )
+    ).
+
+:- pred set_ctree234.try_and_insert3(T::in,
+    set_tree234(T)::in_three, set_tree234(T)::out) is semidet.
+
+set_ctree234.try_and_insert3(E, Tin, Tout) :-
+    Tin = three(E0, E1, T0, T1, T2),
+    (
+        T0 = empty
+        % T1 = empty implied by T0 = empty
+        % T2 = empty implied by T0 = empty
+    ->
+        compare(Result0, E, E0),
+        (
+            Result0 = (<),
+            Tout = four(E, E0, E1, empty, empty, empty, empty)
+        ;
+            Result0 = (=),
+            fail
+        ;
+            Result0 = (>),
+            compare(Result1, E, E1),
+            (
+                Result1 = (<),
+                Tout = four(E0, E, E1, empty, empty, empty, empty)
+            ;
+                Result1 = (=),
+                fail
+            ;
+                Result1 = (>),
+                Tout = four(E0, E1, E, empty, empty, empty, empty)
+            )
+        )
+    ;
+        compare(Result0, E, E0),
+        (
+            Result0 = (<),
+            (
+                T0 = four(_, _, _, _, _, _, _),
+                set_ctree234.split_four(T0, MT0E, T00, T01),
+                compare(ResultM, E, MT0E),
+                (
+                    ResultM = (<),
+                    set_ctree234.try_and_insert2(E, T00, NewT00),
+                    Tout = four(MT0E, E0, E1, NewT00, T01, T1, T2)
+                ;
+                    ResultM = (=),
+                    fail
+                ;
+                    ResultM = (>),
+                    set_ctree234.try_and_insert2(E, T01, NewT01),
+                    Tout = four(MT0E, E0, E1, T00, NewT01, T1, T2)
+                )
+            ;
+                T0 = three(_, _, _, _, _),
+                set_ctree234.try_and_insert3(E, T0, NewT0),
+                Tout = three(E0, E1, NewT0, T1, T2)
+            ;
+                T0 = two(_, _, _),
+                set_ctree234.try_and_insert2(E, T0, NewT0),
+                Tout = three(E0, E1, NewT0, T1, T2)
+            ;
+                T0 = empty,
+                NewT0 = two(E, empty, empty),
+                Tout = three(E0, E1, NewT0, T1, T2)
+            )
+        ;
+            Result0 = (=),
+            fail
+        ;
+            Result0 = (>),
+            compare(Result1, E, E1),
+            (
+                Result1 = (<),
+                (
+                    T1 = four(_, _, _, _, _, _, _),
+                    set_ctree234.split_four(T1, MT1E, T10, T11),
+                    compare(ResultM, E, MT1E),
+                    (
+                        ResultM = (<),
+                        set_ctree234.try_and_insert2(E, T10, NewT10),
+                        Tout = four(E0, MT1E, E1, T0, NewT10, T11, T2)
+                    ;
+                        ResultM = (=),
+                        fail
+                    ;
+                        ResultM = (>),
+                        set_ctree234.try_and_insert2(E, T11, NewT11),
+                        Tout = four(E0, MT1E, E1, T0, T10, NewT11, T2)
+                    )
+                ;
+                    T1 = three(_, _, _, _, _),
+                    set_ctree234.try_and_insert3(E, T1, NewT1),
+                    Tout = three(E0, E1, T0, NewT1, T2)
+                ;
+                    T1 = two(_, _, _),
+                    set_ctree234.try_and_insert2(E, T1, NewT1),
+                    Tout = three(E0, E1, T0, NewT1, T2)
+                ;
+                    T1 = empty,
+                    NewT1 = two(E, empty, empty),
+                    Tout = three(E0, E1, T0, NewT1, T2)
+                )
+            ;
+                Result1 = (=),
+                fail
+            ;
+                Result1 = (>),
+                (
+                    T2 = four(_, _, _, _, _, _, _),
+                    set_ctree234.split_four(T2, MT2E, T20, T21),
+                    compare(ResultM, E, MT2E),
+                    (
+                        ResultM = (<),
+                        set_ctree234.try_and_insert2(E, T20, NewT20),
+                        Tout = four(E0, E1, MT2E, T0, T1, NewT20, T21)
+                    ;
+                        ResultM = (=),
+                        fail
+                    ;
+                        ResultM = (>),
+                        set_ctree234.try_and_insert2(E, T21, NewT21),
+                        Tout = four(E0, E1, MT2E, T0, T1, T20, NewT21)
+                    )
+                ;
+                    T2 = three(_, _, _, _, _),
+                    set_ctree234.try_and_insert3(E, T2, NewT2),
+                    Tout = three(E0, E1, T0, T1, NewT2)
+                ;
+                    T2 = two(_, _, _),
+                    set_ctree234.try_and_insert2(E, T2, NewT2),
+                    Tout = three(E0, E1, T0, T1, NewT2)
+                ;
+                    T2 = empty,
+                    NewT2 = two(E, empty, empty),
+                    Tout = three(E0, E1, T0, T1, NewT2)
+                )
+            )
+        )
+    ).
+
+%------------------------------------------------------------------------------%
+
 set_ctree234.insert_list(Es, Set0) = Set :-
     set_ctree234.insert_list(Es, Set0, Set).
 
Index: library/set_ordlist.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/set_ordlist.m,v
retrieving revision 1.43
diff -u -b -r1.43 set_ordlist.m
--- library/set_ordlist.m	26 Mar 2012 23:36:15 -0000	1.43
+++ library/set_ordlist.m	29 Mar 2012 05:00:11 -0000
@@ -112,9 +112,15 @@
     %
 :- pred set_ordlist.insert(T::in, set_ordlist(T)::in, set_ordlist(T)::out)
     is det.
-
 :- func set_ordlist.insert(set_ordlist(T), T) = set_ordlist(T).
 
+    % `set_ordlist.try_and_insert(X, Set0, Set)' is true iff
+    % `Set0' does not contain `X', while `Set' is the union of `Set0'
+    % and the set containing only `X'.
+    %
+:- pred set_ordlist.try_and_insert(T::in,
+    set_ordlist(T)::in, set_ordlist(T)::out) is semidet.
+
     % `set_ordlist.insert_list(Xs, Set0, Set)' is true iff `Set' is the
     % union of `Set0' and the set containing only the members of `Xs'.
     %
@@ -460,25 +466,46 @@
 set_ordlist.insert(!.S, T) = !:S :-
     set_ordlist.insert(T, !S).
 
-set_ordlist.insert(E, sol(List0), sol(List)) :-
-    set_ordlist.insert_2(List0, E, List).
+set_ordlist.insert(NewItem, sol(List0), sol(List)) :-
+    set_ordlist.insert_2(List0, NewItem, List).
 
 :- pred set_ordlist.insert_2(list(T)::in, T::in, list(T)::out)
     is det.
 
-set_ordlist.insert_2([], E, [E]).
-set_ordlist.insert_2([I | Is], E, Js) :-
-    compare(R, I, E),
+set_ordlist.insert_2([], NewItem, [NewItem]).
+set_ordlist.insert_2([Head | Tail], NewItem, UpdatedList) :-
+    compare(R, Head, NewItem),
+    (
+        R = (<),
+        set_ordlist.insert_2(Tail, NewItem, UpdatedTail),
+        UpdatedList = [Head | UpdatedTail]
+    ;
+        R = (=),
+        UpdatedList = [Head | Tail]
+    ;
+        R = (>),
+        UpdatedList = [NewItem, Head | Tail]
+    ).
+
+set_ordlist.try_and_insert(NewItem, sol(List0), sol(List)) :-
+    set_ordlist.try_and_insert_2(List0, NewItem, List).
+
+:- pred set_ordlist.try_and_insert_2(list(T)::in, T::in, list(T)::out)
+    is semidet.
+
+set_ordlist.try_and_insert_2([], NewItem, [NewItem]).
+set_ordlist.try_and_insert_2([Head | Tail], NewItem, UpdatedList) :-
+    compare(R, Head, NewItem),
     (
         R = (<),
-        set_ordlist.insert_2(Is, E, Ks),
-        Js = [I | Ks]
+        set_ordlist.try_and_insert_2(Tail, NewItem, UpdatedTail),
+        UpdatedList = [Head | UpdatedTail]
     ;
         R = (=),
-        Js = [I | Is]
+        fail
     ;
         R = (>),
-        Js = [E, I | Is]
+        UpdatedList = [NewItem, Head | Tail]
     ).
 
 set_ordlist.insert_list(!.S, Xs) = !:S :-
Index: library/set_tree234.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/set_tree234.m,v
retrieving revision 1.20
diff -u -b -r1.20 set_tree234.m
--- library/set_tree234.m	25 Aug 2011 11:08:15 -0000	1.20
+++ library/set_tree234.m	29 Mar 2012 06:32:36 -0000
@@ -122,6 +122,13 @@
 :- pred set_tree234.insert(T::in, set_tree234(T)::in, set_tree234(T)::out)
     is det.
 
+    % `set_tree234.try_and_insert(X, Set0, Set)' is true iff
+    % `Set0' does not contain `X', while `Set' is the union of `Set0'
+    % and the set containing only `X'.
+    %
+:- pred set_tree234.try_and_insert(T::in,
+    set_tree234(T)::in, set_tree234(T)::out) is semidet.
+
     % `set_tree234.insert_list(Xs, Set0, Set)' is true iff `Set' is the
     % union of `Set0' and the set containing only the members of `Xs'.
     %
@@ -733,8 +740,8 @@
 
 :- pragma type_spec(set_tree234.insert2(in, in_two, out), T = var(_)).
 
-:- pred set_tree234.insert2(T::in, set_tree234(T)::in_two,
-    set_tree234(T)::out) is det.
+:- pred set_tree234.insert2(T::in,
+    set_tree234(T)::in_two, set_tree234(T)::out) is det.
 
 set_tree234.insert2(E, Tin, Tout) :-
     Tin = two(E0, T0, T1),
@@ -767,6 +774,8 @@
                     Tout = three(MT0E, E0, NewT00, T01, T1)
                 ;
                     Result1 = (=),
+                    % The Tout we are returning does not have the same
+                    % shape as Tin, but it contains the same elements.
                     Tout = three(MT0E, E0, T00, T01, T1)
                 ;
                     Result1 = (>),
@@ -801,6 +810,8 @@
                     Tout = three(E0, MT1E, T0, NewT10, T11)
                 ;
                     Result1 = (=),
+                    % The Tout we are returning does not have the same
+                    % shape as Tin, but it contains the same elements.
                     Tout = three(E0, MT1E, T0, T10, T11)
                 ;
                     Result1 = (>),
@@ -825,8 +836,8 @@
 
 :- pragma type_spec(set_tree234.insert3(in, in_three, out), T = var(_)).
 
-:- pred set_tree234.insert3(T::in, set_tree234(T)::in_three,
-    set_tree234(T)::out) is det.
+:- pred set_tree234.insert3(T::in,
+    set_tree234(T)::in_three, set_tree234(T)::out) is det.
 
 set_tree234.insert3(E, Tin, Tout) :-
     Tin = three(E0, E1, T0, T1, T2),
@@ -870,6 +881,8 @@
                     Tout = four(MT0E, E0, E1, NewT00, T01, T1, T2)
                 ;
                     ResultM = (=),
+                    % The Tout we are returning does not have the same
+                    % shape as Tin, but it contains the same elements.
                     Tout = four(MT0E, E0, E1, T00, T01, T1, T2)
                 ;
                     ResultM = (>),
@@ -907,6 +920,8 @@
                         Tout = four(E0, MT1E, E1, T0, NewT10, T11, T2)
                     ;
                         ResultM = (=),
+                        % The Tout we are returning does not have the same
+                        % shape as Tin, but it contains the same elements.
                         Tout = four(E0, MT1E, E1, T0, T10, T11, T2)
                     ;
                         ResultM = (>),
@@ -941,6 +956,8 @@
                         Tout = four(E0, E1, MT2E, T0, T1, NewT20, T21)
                     ;
                         ResultM = (=),
+                        % The Tout we are returning does not have the same
+                        % shape as Tin, but it contains the same elements.
                         Tout = four(E0, E1, MT2E, T0, T1, T20, T21)
                     ;
                         ResultM = (>),
@@ -964,6 +981,274 @@
         )
     ).
 
+%------------------------------------------------------------------------------%
+
+set_tree234.try_and_insert(E, Tin, Tout) :-
+    (
+        Tin = empty,
+        Tout = two(E, empty, empty)
+    ;
+        Tin = two(_, _, _),
+        set_tree234.try_and_insert2(E, Tin, Tout)
+    ;
+        Tin = three(_, _, _, _, _),
+        set_tree234.try_and_insert3(E, Tin, Tout)
+    ;
+        Tin = four(E0, E1, E2, T0, T1, T2, T3),
+        compare(Result1, E, E1),
+        (
+            Result1 = (<),
+            Sub0 = two(E0, T0, T1),
+            Sub1 = two(E2, T2, T3),
+            set_tree234.try_and_insert2(E, Sub0, NewSub0),
+            Tout = two(E1, NewSub0, Sub1)
+        ;
+            Result1 = (=),
+            fail
+        ;
+            Result1 = (>),
+            Sub0 = two(E0, T0, T1),
+            Sub1 = two(E2, T2, T3),
+            set_tree234.try_and_insert2(E, Sub1, NewSub1),
+            Tout = two(E1, Sub0, NewSub1)
+        )
+    ).
+
+:- pragma type_spec(set_tree234.try_and_insert2(in, in_two, out), T = var(_)).
+
+:- pred set_tree234.try_and_insert2(T::in,
+    set_tree234(T)::in_two, set_tree234(T)::out) is semidet.
+
+set_tree234.try_and_insert2(E, Tin, Tout) :-
+    Tin = two(E0, T0, T1),
+    (
+        T0 = empty
+        % T1 = empty implied by T0 = empty
+    ->
+        compare(Result, E, E0),
+        (
+            Result = (<),
+            Tout = three(E, E0, empty, empty, empty)
+        ;
+            Result = (=),
+            fail
+        ;
+            Result = (>),
+            Tout = three(E0, E, empty, empty, empty)
+        )
+    ;
+        compare(Result, E, E0),
+        (
+            Result = (<),
+            (
+                T0 = four(_, _, _, _, _, _, _),
+                set_tree234.split_four(T0, MT0E, T00, T01),
+                compare(Result1, E, MT0E),
+                (
+                    Result1 = (<),
+                    set_tree234.try_and_insert2(E, T00, NewT00),
+                    Tout = three(MT0E, E0, NewT00, T01, T1)
+                ;
+                    Result1 = (=),
+                    fail
+                ;
+                    Result1 = (>),
+                    set_tree234.try_and_insert2(E, T01, NewT01),
+                    Tout = three(MT0E, E0, T00, NewT01, T1)
+                )
+            ;
+                T0 = three(_, _, _, _, _),
+                set_tree234.try_and_insert3(E, T0, NewT0),
+                Tout = two(E0, NewT0, T1)
+            ;
+                T0 = two(_, _, _),
+                set_tree234.try_and_insert2(E, T0, NewT0),
+                Tout = two(E0, NewT0, T1)
+            ;
+                T0 = empty,
+                NewT0 = two(E, empty, empty),
+                Tout = two(E0, NewT0, T1)
+            )
+        ;
+            Result = (=),
+            fail
+        ;
+            Result = (>),
+            (
+                T1 = four(_, _, _, _, _, _, _),
+                set_tree234.split_four(T1, MT1E, T10, T11),
+                compare(Result1, E, MT1E),
+                (
+                    Result1 = (<),
+                    set_tree234.try_and_insert2(E, T10, NewT10),
+                    Tout = three(E0, MT1E, T0, NewT10, T11)
+                ;
+                    Result1 = (=),
+                    fail
+                ;
+                    Result1 = (>),
+                    set_tree234.try_and_insert2(E, T11, NewT11),
+                    Tout = three(E0, MT1E, T0, T10, NewT11)
+                )
+            ;
+                T1 = three(_, _, _, _, _),
+                set_tree234.try_and_insert3(E, T1, NewT1),
+                Tout = two(E0, T0, NewT1)
+            ;
+                T1 = two(_, _, _),
+                set_tree234.try_and_insert2(E, T1, NewT1),
+                Tout = two(E0, T0, NewT1)
+            ;
+                T1 = empty,
+                NewT1 = two(E, empty, empty),
+                Tout = two(E0, T0, NewT1)
+            )
+        )
+    ).
+
+:- pragma type_spec(set_tree234.try_and_insert3(in, in_three, out), T = var(_)).
+
+:- pred set_tree234.try_and_insert3(T::in,
+    set_tree234(T)::in_three, set_tree234(T)::out) is semidet.
+
+set_tree234.try_and_insert3(E, Tin, Tout) :-
+    Tin = three(E0, E1, T0, T1, T2),
+    (
+        T0 = empty
+        % T1 = empty implied by T0 = empty
+        % T2 = empty implied by T0 = empty
+    ->
+        compare(Result0, E, E0),
+        (
+            Result0 = (<),
+            Tout = four(E, E0, E1, empty, empty, empty, empty)
+        ;
+            Result0 = (=),
+            fail
+        ;
+            Result0 = (>),
+            compare(Result1, E, E1),
+            (
+                Result1 = (<),
+                Tout = four(E0, E, E1, empty, empty, empty, empty)
+            ;
+                Result1 = (=),
+                fail
+            ;
+                Result1 = (>),
+                Tout = four(E0, E1, E, empty, empty, empty, empty)
+            )
+        )
+    ;
+        compare(Result0, E, E0),
+        (
+            Result0 = (<),
+            (
+                T0 = four(_, _, _, _, _, _, _),
+                set_tree234.split_four(T0, MT0E, T00, T01),
+                compare(ResultM, E, MT0E),
+                (
+                    ResultM = (<),
+                    set_tree234.try_and_insert2(E, T00, NewT00),
+                    Tout = four(MT0E, E0, E1, NewT00, T01, T1, T2)
+                ;
+                    ResultM = (=),
+                    fail
+                ;
+                    ResultM = (>),
+                    set_tree234.try_and_insert2(E, T01, NewT01),
+                    Tout = four(MT0E, E0, E1, T00, NewT01, T1, T2)
+                )
+            ;
+                T0 = three(_, _, _, _, _),
+                set_tree234.try_and_insert3(E, T0, NewT0),
+                Tout = three(E0, E1, NewT0, T1, T2)
+            ;
+                T0 = two(_, _, _),
+                set_tree234.try_and_insert2(E, T0, NewT0),
+                Tout = three(E0, E1, NewT0, T1, T2)
+            ;
+                T0 = empty,
+                NewT0 = two(E, empty, empty),
+                Tout = three(E0, E1, NewT0, T1, T2)
+            )
+        ;
+            Result0 = (=),
+            fail
+        ;
+            Result0 = (>),
+            compare(Result1, E, E1),
+            (
+                Result1 = (<),
+                (
+                    T1 = four(_, _, _, _, _, _, _),
+                    set_tree234.split_four(T1, MT1E, T10, T11),
+                    compare(ResultM, E, MT1E),
+                    (
+                        ResultM = (<),
+                        set_tree234.try_and_insert2(E, T10, NewT10),
+                        Tout = four(E0, MT1E, E1, T0, NewT10, T11, T2)
+                    ;
+                        ResultM = (=),
+                        fail
+                    ;
+                        ResultM = (>),
+                        set_tree234.try_and_insert2(E, T11, NewT11),
+                        Tout = four(E0, MT1E, E1, T0, T10, NewT11, T2)
+                    )
+                ;
+                    T1 = three(_, _, _, _, _),
+                    set_tree234.try_and_insert3(E, T1, NewT1),
+                    Tout = three(E0, E1, T0, NewT1, T2)
+                ;
+                    T1 = two(_, _, _),
+                    set_tree234.try_and_insert2(E, T1, NewT1),
+                    Tout = three(E0, E1, T0, NewT1, T2)
+                ;
+                    T1 = empty,
+                    NewT1 = two(E, empty, empty),
+                    Tout = three(E0, E1, T0, NewT1, T2)
+                )
+            ;
+                Result1 = (=),
+                fail
+            ;
+                Result1 = (>),
+                (
+                    T2 = four(_, _, _, _, _, _, _),
+                    set_tree234.split_four(T2, MT2E, T20, T21),
+                    compare(ResultM, E, MT2E),
+                    (
+                        ResultM = (<),
+                        set_tree234.try_and_insert2(E, T20, NewT20),
+                        Tout = four(E0, E1, MT2E, T0, T1, NewT20, T21)
+                    ;
+                        ResultM = (=),
+                        fail
+                    ;
+                        ResultM = (>),
+                        set_tree234.try_and_insert2(E, T21, NewT21),
+                        Tout = four(E0, E1, MT2E, T0, T1, T20, NewT21)
+                    )
+                ;
+                    T2 = three(_, _, _, _, _),
+                    set_tree234.try_and_insert3(E, T2, NewT2),
+                    Tout = three(E0, E1, T0, T1, NewT2)
+                ;
+                    T2 = two(_, _, _),
+                    set_tree234.try_and_insert2(E, T2, NewT2),
+                    Tout = three(E0, E1, T0, T1, NewT2)
+                ;
+                    T2 = empty,
+                    NewT2 = two(E, empty, empty),
+                    Tout = three(E0, E1, T0, T1, NewT2)
+                )
+            )
+        )
+    ).
+
+%------------------------------------------------------------------------------%
+
 set_tree234.insert_list(Es, Set0) = Set :-
     set_tree234.insert_list(Es, Set0, Set).
 
Index: library/set_unordlist.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/set_unordlist.m,v
retrieving revision 1.39
diff -u -b -r1.39 set_unordlist.m
--- library/set_unordlist.m	26 Mar 2012 23:36:15 -0000	1.39
+++ library/set_unordlist.m	29 Mar 2012 06:24:18 -0000
@@ -123,6 +123,13 @@
 
 :- func set_unordlist.insert(set_unordlist(T), T) = set_unordlist(T).
 
+    % `set_unordlist.try_and_insert(X, Set0, Set)' is true iff `Set0' does
+    % not contain `X', and `Set' is the union of `Set0' and the set containing
+    % only `X'.
+    %
+:- pred set_unordlist.try_and_insert(T::in,
+    set_unordlist(T)::in, set_unordlist(T)::out) is semidet.
+
     % `set_unordlist.insert_list(Xs, Set0, Set)' is true iff `Set' is the
     % union of `Set0' and the set containing only the members of `Xs'.
     %
@@ -396,6 +403,13 @@
 
 set_unordlist.insert(E, sul(S0), sul([E | S0])).
 
+set_unordlist.try_and_insert(E, sul(S0), sul(S)) :-
+    ( list.member(E, S0) ->
+        fail
+    ;
+        S = [E | S0]
+    ).
+
 set_unordlist.init(sul([])).
 
 :- pragma promise_equivalent_clauses(set_unordlist.singleton_set/2).
Index: library/sparse_bitset.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/sparse_bitset.m,v
retrieving revision 1.42
diff -u -b -r1.42 sparse_bitset.m
--- library/sparse_bitset.m	22 Aug 2011 06:33:02 -0000	1.42
+++ library/sparse_bitset.m	29 Mar 2012 06:56:36 -0000
@@ -146,6 +146,13 @@
 :- pred insert(T::in, sparse_bitset(T)::in, sparse_bitset(T)::out)
     is det <= enum(T).
 
+    % `try_and_insert(X, Set0, Set)' returns the union of `Set' and the set
+    % containing only `X' if `Set0' does not already contain `X'; if it does,
+    % it fails. Takes O(rep_size(Set)) time and space.
+    %
+:- pred try_and_insert(T::in, sparse_bitset(T)::in, sparse_bitset(T)::out)
+    is semidet <= enum(T).
+
     % `insert_list(Set, X)' returns the union of `Set' and the set containing
     % only the members of `X'. Same as `union(Set, list_to_set(X))', but may be
     % more efficient.
@@ -761,18 +768,20 @@
 
 %-----------------------------------------------------------------------------%
 
-insert(E, !Set) :-
-    !:Set = insert(!.Set, E).
+insert(Set0, Elem) = Set :-
+    insert(Elem, Set0, Set).
 
-insert(sparse_bitset(Set), Elem) =
-    sparse_bitset(insert_2(Set, enum.to_int(Elem))).
+insert(E, !Set) :-
+    !.Set = sparse_bitset(Set0),
+    insert_2(Set0, enum.to_int(E), Set),
+    !:Set = sparse_bitset(Set).
 
-:- func insert_2(bitset_impl, int) = bitset_impl.
+:- pred insert_2(bitset_impl::in, int::in, bitset_impl::out) is det.
 
-insert_2([], Index) = [make_bitset_elem(Offset, Bits)] :-
+insert_2([], Index, [make_bitset_elem(Offset, Bits)]) :-
     bits_for_index(Index, Offset, Bits).
-insert_2(Set0, Index) = Set :-
-    Set0 = [Data0 | Rest],
+insert_2(Set0, Index, Set) :-
+    Set0 = [Data0 | Rest0],
     Offset0 = Data0 ^ offset,
     ( Index < Offset0 ->
         bits_for_index(Index, Offset, Bits),
@@ -783,12 +792,46 @@
             Set = Set0
         ;
             Bits = set_bit(Bits0, BitToSet),
-            Set = [make_bitset_elem(Offset0, Bits) | Rest]
+            Set = [make_bitset_elem(Offset0, Bits) | Rest0]
         )
     ;
-        Set = [Data0 | insert_2(Rest, Index)]
+        insert_2(Rest0, Index, Set1),
+        Set = [Data0 | Set1]
     ).
 
+%-----------------------------------------------------------------------------%
+
+try_and_insert(E, !Set) :-
+    !.Set = sparse_bitset(Set0),
+    try_and_insert_2(enum.to_int(E), Set0, Set),
+    !:Set = sparse_bitset(Set).
+
+:- pred try_and_insert_2(int::in, bitset_impl::in, bitset_impl::out)
+    is semidet.
+
+try_and_insert_2(Index, [], [make_bitset_elem(Offset, Bits)]) :-
+    bits_for_index(Index, Offset, Bits).
+try_and_insert_2(Index, Set0, Set) :-
+    Set0 = [Data0 | Rest0],
+    Offset0 = Data0 ^ offset,
+    ( Index < Offset0 ->
+        bits_for_index(Index, Offset, Bits),
+        Set = [make_bitset_elem(Offset, Bits) | Set0]
+    ; BitToSet = Index - Offset0, BitToSet < bits_per_int ->
+        Bits0 = Data0 ^ bits,
+        ( get_bit(Bits0, BitToSet) \= 0 ->
+            fail
+        ;
+            Bits = set_bit(Bits0, BitToSet),
+            Set = [make_bitset_elem(Offset0, Bits) | Rest0]
+        )
+    ;
+        try_and_insert_2(Index, Rest0, Set1),
+        Set = [Data0 | Set1]
+    ).
+
+%-----------------------------------------------------------------------------%
+
 insert_list(List, !Set) :-
     !:Set = insert_list(!.Set, List).
 
Index: library/test_bitset.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/test_bitset.m,v
retrieving revision 1.1
diff -u -b -r1.1 test_bitset.m
--- library/test_bitset.m	29 Mar 2012 04:03:11 -0000	1.1
+++ library/test_bitset.m	29 Mar 2012 06:41:59 -0000
@@ -77,6 +77,8 @@
 
 :- pred insert(T::in, test_bitset(T)::in, test_bitset(T)::out)
     is det <= enum(T).
+:- pred try_and_insert(T::in, test_bitset(T)::in, test_bitset(T)::out)
+    is semidet <= enum(T).
 :- pred insert_list(list(T)::in, test_bitset(T)::in, test_bitset(T)::out)
     is det <= enum(T).
 :- pred delete(T::in, test_bitset(T)::in, test_bitset(T)::out)
@@ -312,6 +314,24 @@
     set_ordlist.insert(E, SetB0, SetB),
     check1("insert", SetA0 - SetB0, SetA - SetB, Result).
 
+try_and_insert(E, SetA0 - SetB0, Result) :-
+    ( tree_bitset.try_and_insert(E, SetA0, SetA) ->
+        ( set_ordlist.try_and_insert(E, SetB0, SetB) ->
+            check1("insert", SetA0 - SetB0, SetA - SetB, Result)
+        ;
+            unexpected($module, $pred,
+                "success/fail in tree_bitset/set_ordlist")
+        )
+    ;
+        ( set_ordlist.try_and_insert(E, SetB0, _SetB) ->
+            unexpected($module, $pred,
+                "fail/success in tree_bitset/set_ordlist")
+        ;
+            % try_and_insert failed in both tree_bitset and set_ordlist.
+            fail
+        )
+    ).
+
 insert_list(Es, SetA0 - SetB0, Result) :-
     tree_bitset.insert_list(Es, SetA0, SetA),
     set_ordlist.insert_list(Es, SetB0, SetB),
Index: library/tree_bitset.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/library/tree_bitset.m,v
retrieving revision 1.17
diff -u -b -r1.17 tree_bitset.m
--- library/tree_bitset.m	29 Mar 2012 04:03:11 -0000	1.17
+++ library/tree_bitset.m	29 Mar 2012 06:46:56 -0000
@@ -129,6 +129,13 @@
 :- pred insert(T::in, tree_bitset(T)::in, tree_bitset(T)::out)
     is det <= enum(T).
 
+    % `try_and_insert(X, Set0, Set)' returns the union of `Set' and the set
+    % containing only `X' is `Set0' does not contain 'X'; if it does, it fails.
+    % Takes O(log(card(Set))) time and space.
+    %
+:- pred try_and_insert(T::in, tree_bitset(T)::in, tree_bitset(T)::out)
+    is semidet <= enum(T).
+
     % `insert_list(Set, X)' returns the union of `Set' and the set containing
     % only the members of `X'. Same as `union(Set, list_to_set(X))', but may be
     % more efficient.
@@ -1094,6 +1101,132 @@
 
 %-----------------------------------------------------------------------------%
 
+try_and_insert(Elem, Set0, Set) :-
+    Set0 = tree_bitset(List0),
+    Index = enum_to_index(Elem),
+    (
+        List0 = leaf_list(LeafList0),
+        (
+            LeafList0 = [],
+            bits_for_index(Index, Offset, Bits),
+            Set = wrap_tree_bitset(leaf_list([make_leaf_node(Offset, Bits)]))
+        ;
+            LeafList0 = [Leaf0 | _],
+            range_of_parent_node(Leaf0 ^ leaf_offset, 0,
+                ParentInitOffset, ParentLimitOffset),
+            (
+                ParentInitOffset =< Index,
+                Index < ParentLimitOffset
+            ->
+                leaflist_try_and_insert(Index, LeafList0, LeafList),
+                Set = wrap_tree_bitset(leaf_list(LeafList))
+            ;
+                expand_range(Index, List0, 1,
+                    ParentInitOffset, ParentLimitOffset,
+                    InteriorNode1, InteriorLevel1),
+                interiorlist_try_and_insert(Index, InteriorLevel1,
+                    [InteriorNode1], InteriorList),
+                Set = wrap_tree_bitset(
+                    interior_list(InteriorLevel1, InteriorList))
+            )
+        )
+    ;
+        List0 = interior_list(InteriorLevel, InteriorList0),
+        (
+            InteriorList0 = [],
+            % This is a violation of our invariants.
+            unexpected($module, $pred,
+                "try_and_insert into empty list of interior nodes")
+        ;
+            InteriorList0 = [InteriorNode0 | _],
+            range_of_parent_node(InteriorNode0 ^ init_offset, InteriorLevel,
+                ParentInitOffset, ParentLimitOffset),
+            (
+                ParentInitOffset =< Index,
+                Index < ParentLimitOffset
+            ->
+                interiorlist_try_and_insert(Index, InteriorLevel,
+                    InteriorList0, InteriorList),
+                Set = wrap_tree_bitset(
+                    interior_list(InteriorLevel, InteriorList))
+            ;
+                expand_range(Index, List0, InteriorLevel + 1,
+                    ParentInitOffset, ParentLimitOffset,
+                    InteriorNode1, InteriorLevel1),
+                interiorlist_try_and_insert(Index, InteriorLevel1,
+                    [InteriorNode1], InteriorList),
+                Set = wrap_tree_bitset(
+                    interior_list(InteriorLevel1, InteriorList))
+            )
+        )
+    ).
+
+:- pred leaflist_try_and_insert(int::in,
+    list(leaf_node)::in, list(leaf_node)::out) is semidet.
+
+leaflist_try_and_insert(Index, [], Leaves) :-
+    bits_for_index(Index, Offset, Bits),
+    Leaves = [make_leaf_node(Offset, Bits)].
+leaflist_try_and_insert(Index, Leaves0 @ [Head0 | Tail0], Leaves) :-
+    Offset0 = Head0 ^ leaf_offset,
+    ( Index < Offset0 ->
+        bits_for_index(Index, Offset, Bits),
+        Leaves = [make_leaf_node(Offset, Bits) | Leaves0]
+    ; BitToSet = Index - Offset0, BitToSet < bits_per_int ->
+        Bits0 = Head0 ^ leaf_bits,
+        ( get_bit(Bits0, BitToSet) \= 0 ->
+            fail
+        ;
+            Bits = set_bit(Bits0, BitToSet),
+            Leaves = [make_leaf_node(Offset0, Bits) | Tail0]
+        )
+    ;
+        leaflist_try_and_insert(Index, Tail0, Tail),
+        Leaves = [Head0 | Tail]
+    ).
+
+:- pred interiorlist_try_and_insert(int::in, int::in,
+    list(interior_node)::in, list(interior_node)::out) is semidet.
+
+interiorlist_try_and_insert(Index, Level, [], Nodes) :-
+    bits_for_index(Index, Offset, Bits),
+    raise_leaf_to_level(Level, make_leaf_node(Offset, Bits), Node),
+    Nodes = [Node].
+interiorlist_try_and_insert(Index, Level, Nodes0 @ [Head0 | Tail0], Nodes) :-
+    Offset0 = Head0 ^ init_offset,
+    ( Index < Offset0 ->
+        bits_for_index(Index, Offset, Bits),
+        raise_leaf_to_level(Level, make_leaf_node(Offset, Bits), Node),
+        Nodes = [Node | Nodes0]
+    ; Head0 ^ init_offset =< Index, Index < Head0 ^ limit_offset ->
+        Components0 = Head0 ^ components,
+        (
+            Components0 = leaf_list(LeafList0),
+            trace [compile_time(flag("tree-bitset-checks"))] (
+                expect(unify(Level, 1), $module, $pred,
+                    "bad component list (leaf)")
+            ),
+            leaflist_try_and_insert(Index, LeafList0, LeafList),
+            Components = leaf_list(LeafList)
+        ;
+            Components0 = interior_list(InteriorLevel, InteriorList0),
+            trace [compile_time(flag("tree-bitset-checks"))] (
+                expect(unify(InteriorLevel, Level - 1), $module, $pred,
+                    "bad component list (interior)")
+            ),
+            interiorlist_try_and_insert(Index, InteriorLevel,
+                InteriorList0, InteriorList),
+            Components = interior_list(InteriorLevel, InteriorList)
+        ),
+        Head = Head0 ^ components := Components,
+        Nodes = [Head | Tail0]
+    ;
+        interiorlist_try_and_insert(Index, Level, Tail0, Tail),
+        Nodes = [Head0 | Tail]
+    ).
+
+%-----------------------------------------------------------------------------%
+
 insert_list(Set, List) = union(list_to_set(List), Set).
 
 delete(Set, Elem) = difference(Set, insert(init, Elem)).
cvs diff: Diffing m4
cvs diff: Diffing mdbcomp
cvs diff: Diffing profiler
cvs diff: Diffing robdd
cvs diff: Diffing runtime
cvs diff: Diffing runtime/GETOPT
cvs diff: Diffing runtime/machdeps
cvs diff: Diffing samples
cvs diff: Diffing samples/appengine
cvs diff: Diffing samples/appengine/war
cvs diff: Diffing samples/appengine/war/WEB-INF
cvs diff: Diffing samples/c_interface
cvs diff: Diffing samples/c_interface/c_calls_mercury
cvs diff: Diffing samples/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/c_interface/mercury_calls_c
cvs diff: Diffing samples/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/c_interface/standalone_c
cvs diff: Diffing samples/concurrency
cvs diff: Diffing samples/concurrency/dining_philosophers
cvs diff: Diffing samples/concurrency/midimon
cvs diff: Diffing samples/diff
cvs diff: Diffing samples/java_interface
cvs diff: Diffing samples/java_interface/java_calls_mercury
cvs diff: Diffing samples/java_interface/mercury_calls_java
cvs diff: Diffing samples/lazy_list
cvs diff: Diffing samples/muz
cvs diff: Diffing samples/rot13
cvs diff: Diffing samples/solutions
cvs diff: Diffing samples/solver_types
cvs diff: Diffing samples/tests
cvs diff: Diffing samples/tests/c_interface
cvs diff: Diffing samples/tests/c_interface/c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/cplusplus_calls_mercury
cvs diff: Diffing samples/tests/c_interface/mercury_calls_c
cvs diff: Diffing samples/tests/c_interface/mercury_calls_cplusplus
cvs diff: Diffing samples/tests/c_interface/mercury_calls_fortran
cvs diff: Diffing samples/tests/c_interface/simpler_c_calls_mercury
cvs diff: Diffing samples/tests/c_interface/simpler_cplusplus_calls_mercury
cvs diff: Diffing samples/tests/diff
cvs diff: Diffing samples/tests/muz
cvs diff: Diffing samples/tests/rot13
cvs diff: Diffing samples/tests/solutions
cvs diff: Diffing samples/tests/toplevel
cvs diff: Diffing scripts
cvs diff: Diffing slice
cvs diff: Diffing ssdb
cvs diff: Diffing tests
cvs diff: Diffing tests/analysis
cvs diff: Diffing tests/analysis/ctgc
cvs diff: Diffing tests/analysis/excp
cvs diff: Diffing tests/analysis/ext
cvs diff: Diffing tests/analysis/sharing
cvs diff: Diffing tests/analysis/table
cvs diff: Diffing tests/analysis/trail
cvs diff: Diffing tests/analysis/unused_args
cvs diff: Diffing tests/benchmarks
cvs diff: Diffing tests/debugger
cvs diff: Diffing tests/debugger/declarative
cvs diff: Diffing tests/dppd
cvs diff: Diffing tests/feedback
cvs diff: Diffing tests/feedback/mandelbrot
cvs diff: Diffing tests/feedback/mmc
cvs diff: Diffing tests/general
cvs diff: Diffing tests/general/accumulator
cvs diff: Diffing tests/general/string_format
cvs diff: Diffing tests/general/structure_reuse
cvs diff: Diffing tests/grade_subdirs
cvs diff: Diffing tests/hard_coded
cvs diff: Diffing tests/hard_coded/exceptions
cvs diff: Diffing tests/hard_coded/purity
cvs diff: Diffing tests/hard_coded/sub-modules
cvs diff: Diffing tests/hard_coded/typeclasses
cvs diff: Diffing tests/invalid
cvs diff: Diffing tests/invalid/purity
cvs diff: Diffing tests/misc_tests
cvs diff: Diffing tests/mmc_make
cvs diff: Diffing tests/mmc_make/lib
cvs diff: Diffing tests/par_conj
cvs diff: Diffing tests/recompilation
cvs diff: Diffing tests/stm
cvs diff: Diffing tests/stm/orig
cvs diff: Diffing tests/stm/orig/stm-compiler
cvs diff: Diffing tests/stm/orig/stm-compiler/test1
cvs diff: Diffing tests/stm/orig/stm-compiler/test10
cvs diff: Diffing tests/stm/orig/stm-compiler/test2
cvs diff: Diffing tests/stm/orig/stm-compiler/test3
cvs diff: Diffing tests/stm/orig/stm-compiler/test4
cvs diff: Diffing tests/stm/orig/stm-compiler/test5
cvs diff: Diffing tests/stm/orig/stm-compiler/test6
cvs diff: Diffing tests/stm/orig/stm-compiler/test7
cvs diff: Diffing tests/stm/orig/stm-compiler/test8
cvs diff: Diffing tests/stm/orig/stm-compiler/test9
cvs diff: Diffing tests/stm/orig/stm-compiler-par
cvs diff: Diffing tests/stm/orig/stm-compiler-par/bm1
cvs diff: Diffing tests/stm/orig/stm-compiler-par/bm2
cvs diff: Diffing tests/stm/orig/stm-compiler-par/stmqueue
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test1
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test10
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test11
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test2
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test3
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test4
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test5
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test6
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test7
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test8
cvs diff: Diffing tests/stm/orig/stm-compiler-par/test9
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test1
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test2
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test3
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test4
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test5
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test6
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test7
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test8
cvs diff: Diffing tests/stm/orig/stm-compiler-par-asm_fast/test9
cvs diff: Diffing tests/tabling
cvs diff: Diffing tests/term
cvs diff: Diffing tests/trailing
cvs diff: Diffing tests/valid
cvs diff: Diffing tests/warnings
cvs diff: Diffing tools
cvs diff: Diffing trace
cvs diff: Diffing util
cvs diff: Diffing vim
cvs diff: Diffing vim/after
cvs diff: Diffing vim/ftplugin
cvs diff: Diffing vim/syntax
--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------



More information about the reviews mailing list