[m-rev.] for review: "fix" the bug Julien reported yesterday

Zoltan Somogyi zs at csse.unimelb.edu.au
Wed Jan 28 13:48:08 AEDT 2009


For review by anyone.

Zoltan.

"Fix" a problem whose workaround by Julien was committed recently.
The immediate symptom was a code generator abort caused by a model_non goal
in a model_det context: a det procedure whose body was multi. The reason
why the body was multi was that a disjunction with no outputs was not
recognized as having no outputs, because instmap_delta_no_output_vars_2
does not succeed if the old and new insts of a variable specify non-overlapping
sets of function symbols.

This diff does not fix the actual problem (though it does document it),
but it does make it much less likely to occur by making the mishandled
situation much less likely to occur.

compiler/instmap.m:
	Document the problem with instmap_delta_no_output_vars_2.
	Simplify the code of instmap_delta_no_output_vars_2.

compiler/mode_util.m:
	When recomputing instmap_deltas of deconstruction unifications,
	abstractly unify the inst of the LHS variable before and after
	the deconstruction. If the cons_id does not appear among the possible
	cons_ids in the old inst, this will make the final inst not_reached,
	and avoid the problem situation for later.

compiler/Mercury.options:
	Remove Julien's workaround, since it is not needed anymore.

doc/user_guide.texi:
	Document the --dump-hlds-options a bit better. This helped in tracking
	down the problem.

tests/hard_coded/Mmakefile:
	Reenable an old test that this change now enables us to pass.

The following are style fixes only.

compiler/compile_target_code.m:
	Fix formatting in the code affected by the workaround.

compiler/handle_options.m:
	Add a dump alias to help diagnose determinism problems.

compiler/inlining.m:
compiler/inst_util.m:
	Minor style fixes.

compiler/inst_match.m:
	Put the predicates into more logical groups.

	Move documentation of exported predicates from the implementation
	section to the interface section.

	Add a prefix to field names, to avoid ambiguity.

	Avoid the use of with_type and with_inst.

	Avoid the use of faux field accesses when it makes the actual
	steps harder to understand.

	Make the initial values of inst_match_info explicit.

	Abort when the lists of a cons_id's argument variables and argument
	modes are of different lengths.

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/include
cvs diff: Diffing boehm_gc/include/private
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/src/atomic_ops/sysdeps/gcc
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src/atomic_ops/sysdeps/hpc
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src/atomic_ops/sysdeps/ibmc
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src/atomic_ops/sysdeps/icc
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src/atomic_ops/sysdeps/msftc
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/src/atomic_ops/sysdeps/sunc
cvs diff: Diffing boehm_gc/libatomic_ops-1.2/tests
cvs diff: Diffing boehm_gc/tests
cvs diff: Diffing boehm_gc/windows-untested
cvs diff: Diffing boehm_gc/windows-untested/vc60
cvs diff: Diffing boehm_gc/windows-untested/vc70
cvs diff: Diffing boehm_gc/windows-untested/vc71
cvs diff: Diffing browser
cvs diff: Diffing bytecode
cvs diff: Diffing compiler
Index: compiler/Mercury.options
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/Mercury.options,v
retrieving revision 1.41
diff -u -b -r1.41 Mercury.options
--- compiler/Mercury.options	27 Jan 2009 06:44:29 -0000	1.41
+++ compiler/Mercury.options	28 Jan 2009 02:35:08 -0000
@@ -70,12 +70,6 @@
 # Work around a problem in the HiPE compiler (as of Erlang R11B5).
 MCFLAGS-libs.options += --erlang-switch-on-strings-as-atoms
 
-# Work around a problem first observed in rotd-2009-01-26.  Compiling
-# revision 1.135 of the module below results in an abort in the LLDS
-# code generator at -O5 or above.  The problem occurs when 
-# --inline-compound-threshold is set to 100 (as it is at -O5). 
-MCFLAGS-backend_libs.compile_target_code = --inline-compound-threshold 20 --no-local-constraint-propagation
-
 # The c_code in the module gcc.m needs the header files from the GNU C
 # distribution.  Note that we need to compile these with
 # -DMR_NO_BACKWARDS_COMPAT, because otherwise there are name
Index: compiler/compile_target_code.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/compile_target_code.m,v
retrieving revision 1.135
diff -u -b -r1.135 compile_target_code.m
--- compiler/compile_target_code.m	20 Jan 2009 06:24:02 -0000	1.135
+++ compiler/compile_target_code.m	27 Jan 2009 06:42:18 -0000
@@ -2061,7 +2061,8 @@
     option::in(bound(shlib_linker_rpath_separator ; linker_rpath_separator)),
     string::out, io::di, io::uo) is det.
 
-get_runtime_library_path_opts(LinkTargetType, RpathFlagOpt, RpathSepOpt, RpathOpts, !IO) :-
+get_runtime_library_path_opts(LinkTargetType, RpathFlagOpt, RpathSepOpt,
+        RpathOpts, !IO) :-
     globals.io_lookup_bool_option(shlib_linker_use_install_name,
         UseInstallName, !IO),
     shared_libraries_supported(SharedLibsSupported, !IO),
@@ -2073,8 +2074,8 @@
         ; LinkTargetType = shared_library
         )
     ->
-        globals.io_lookup_accumulating_option(
-            runtime_link_library_directories, RpathDirs0, !IO),
+        globals.io_lookup_accumulating_option(runtime_link_library_directories,
+            RpathDirs0, !IO),
         RpathDirs = list.map(quote_arg, RpathDirs0),
         ( 
             RpathDirs = [],
Index: compiler/handle_options.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/handle_options.m,v
retrieving revision 1.329
diff -u -b -r1.329 handle_options.m
--- compiler/handle_options.m	20 Jan 2009 06:35:12 -0000	1.329
+++ compiler/handle_options.m	27 Jan 2009 10:29:53 -0000
@@ -2923,6 +2923,7 @@
 convert_dump_alias("min", "ilv").
 convert_dump_alias("paths", "cP").
 convert_dump_alias("petdr", "din").
+convert_dump_alias("detism", "divM").
 convert_dump_alias("mm", "bdgvP").      % for debugging minimal model
 convert_dump_alias("osv", "bcdglmnpruvP").  % for debugging
                                             % --optimize-saved-vars-cell
Index: compiler/inlining.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/inlining.m,v
retrieving revision 1.161
diff -u -b -r1.161 inlining.m
--- compiler/inlining.m	23 Dec 2008 01:37:34 -0000	1.161
+++ compiler/inlining.m	27 Jan 2009 07:44:33 -0000
@@ -191,7 +191,6 @@
                 any_tracing             :: bool
                                         % Is any procedure being traced
                                         % in the module?
-
             ).
 
 inlining(!ModuleInfo) :-
@@ -220,11 +219,8 @@
     Params = params(Simple, SingleUse, CallCost, CompoundThreshold,
         SimpleThreshold, VarThreshold, HighLevelCode, AnyTracing),
 
-    %
-    % Get the usage counts for predicates
-    % (but only if needed, i.e. only if --inline-single-use
-    % or --inline-compound-threshold has been specified)
-    %
+    % Get the usage counts for predicates (but only if needed, i.e. only if
+    % --inline-single-use or --inline-compound-threshold has been specified).
     (
         ( SingleUse = yes
         ; CompoundThreshold > 0
@@ -234,7 +230,7 @@
     ;
         map.init(NeededMap)
     ),
-    %
+
     % Build the call graph and extract the topological sort.
     % NOTE: the topological sort returns a list of SCCs. Clearly, we want to
     % process the SCCs bottom to top (which is the order that they are
@@ -244,7 +240,7 @@
     % sophisticated approach would be to break the cycle so that
     % the procedure(s) that are called by higher SCCs are processed last,
     % but we do not implement that yet.
-    %
+
     module_info_ensure_dependency_info(!ModuleInfo),
     module_info_dependency_info(!.ModuleInfo, DepInfo),
     hlds_dependency_info_get_dependency_ordering(DepInfo, SCCs),
@@ -261,7 +257,7 @@
 
 do_inlining([], _Needed, _Params, _Inlined, !Module).
 do_inlining([PPId | PPIds], Needed, Params, !.Inlined, !Module) :-
-    in_predproc(PPId, !.Inlined, Params, !Module),
+    inline_in_proc(PPId, !.Inlined, Params, !Module),
     mark_predproc(PPId, Needed, Params, !.Module, !Inlined),
     do_inlining(PPIds, Needed, Params, !.Inlined, !Module).
 
@@ -321,12 +317,12 @@
     ;
         Clauses = [clause(_, Goal, _, _)],
         Size < SimpleThreshold * 3,
-        %
+
         % For flat goals, we are more likely to be able to optimize stuff away,
         % so we use a higher threshold.
         % XXX This should be a separate option, we shouldn't hardcode
         % the number `3' (which is just a guess).
-        %
+
         is_flat_simple_goal(Goal)
     ).
 
@@ -335,12 +331,11 @@
     (
         Size < SimpleThreshold
     ;
-        %
         % For flat goals, we are more likely to be able to optimize stuff away,
         % so we use a higher threshold.
         % XXX this should be a separate option, we shouldn't hardcode
         % the number `3' (which is just a guess).
-        %
+
         Size < SimpleThreshold * 3,
         is_flat_simple_goal(CalledGoal)
     ).
@@ -454,10 +449,10 @@
                                     % any subgoal.
             ).
 
-:- pred in_predproc(pred_proc_id::in, set(pred_proc_id)::in, inline_params::in,
-    module_info::in, module_info::out) is det.
+:- pred inline_in_proc(pred_proc_id::in, set(pred_proc_id)::in,
+    inline_params::in, module_info::in, module_info::out) is det.
 
-in_predproc(PredProcId, InlinedProcs, Params, !ModuleInfo) :-
+inline_in_proc(PredProcId, InlinedProcs, Params, !ModuleInfo) :-
     VarThresh = Params ^ var_threshold,
     HighLevelCode = Params ^ highlevel_code,
     AnyTracing = Params ^ any_tracing,
@@ -538,8 +533,7 @@
         ),
 
         map.det_update(PredTable0, PredId, !.PredInfo, PredTable),
-        module_info_set_preds(PredTable, !ModuleInfo)
-    ),
+        module_info_set_preds(PredTable, !ModuleInfo),
 
     % If the determinism of some sub-goals has changed, then we re-run
     % determinism analysis, because propagating the determinism information
@@ -549,6 +543,7 @@
         det_infer_proc(PredId, ProcId, !ModuleInfo, _, _, _)
     ;
         DetChanged = no
+        )
     ).
 
 %-----------------------------------------------------------------------------%
Index: compiler/inst_match.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/inst_match.m,v
retrieving revision 1.85
diff -u -b -r1.85 inst_match.m
--- compiler/inst_match.m	11 Feb 2008 21:25:56 -0000	1.85
+++ compiler/inst_match.m	27 Jan 2009 13:21:15 -0000
@@ -65,30 +65,29 @@
 %-----------------------------------------------------------------------------%
 
     % inst_matches_initial(InstA, InstB, Type, ModuleInfo):
-    %   Succeed iff `InstA' specifies at least as much
-    %   information as `InstB', and in those parts where they
-    %   specify the same information, `InstA' is at least as
-    %   instantiated as `InstB'.
-    %   Thus, inst_matches_initial(not_reached, ground, _)
-    %   succeeds, since not_reached contains more information
-    %   than ground - but not vice versa.  Similarly,
-    %   inst_matches_initial(bound(a), bound(a;b), _) should
+    %
+    % Succeed iff `InstA' specifies at least as much information as `InstB',
+    % and in those parts where they specify the same information, `InstA'
+    % is at least as instantiated as `InstB'. Thus, the call
+    % inst_matches_initial(not_reached, ground, _) succeeds, since
+    % not_reached contains more information than ground - but not vice versa.
+    % Similarly, inst_matches_initial(bound(a), bound(a;b), _) should
     %   succeed, but not vice versa.
     %
 :- pred inst_matches_initial(mer_inst::in, mer_inst::in, mer_type::in,
     module_info::in) is semidet.
 
     % This version of inst_matches_initial builds up a substitution map
-    % (inst_var_sub).  For each inst_var which occurs in InstA there will be a
-    % substitution to the corresponding inst in InstB.
+    % (inst_var_sub). For each inst_var which occurs in InstA there will be
+    % a substitution to the corresponding inst in InstB.
     %
 :- pred inst_matches_initial(mer_inst::in, mer_inst::in, mer_type::in,
     module_info::in, module_info::out, inst_var_sub::in, inst_var_sub::out)
     is semidet.
 
-    % This version of inst_matches_initial does not allow implied modes.  This
-    % makes it almost the same as inst_matches_final.  The only difference is
-    % in the way it handles constrained_inst_vars.
+    % This version of inst_matches_initial does not allow implied modes.
+    % This makes it almost the same as inst_matches_final. The only difference
+    % is in the way it handles constrained_inst_vars.
     %
 :- pred inst_matches_initial_no_implied_modes(mer_inst::in, mer_inst::in,
     mer_type::in, module_info::in) is semidet.
@@ -100,11 +99,12 @@
     inst_var_sub::in, inst_var_sub::out) is semidet.
 
     % inst_matches_final(InstA, InstB, ModuleInfo):
-    %   Succeed iff InstA is compatible with InstB, i.e. iff InstA will
-    %   satisfy the final inst requirement InstB.  This is true if the
-    %   information specified by InstA is at least as great as that specified
-    %   by InstB, and where the information is the same and both insts specify
-    %   a binding, the binding must be identical.
+    %
+    % Succeed iff InstA is compatible with InstB, i.e. iff InstA will satisfy
+    % the final inst requirement InstB.  This is true if the information
+    % specified by InstA is at least as great as that specified by InstB,
+    % and where the information is the same and both insts specify a binding,
+    % the binding must be identical.
     %
 :- pred inst_matches_final(mer_inst::in, mer_inst::in, module_info::in)
     is semidet.
@@ -153,6 +153,7 @@
 :- pred unique_matches_final(uniqueness::in, uniqueness::in) is semidet.
 
     % inst_matches_binding(InstA, InstB, 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
     %   ignores uniqueness, and that `any' does not match itself.  It is used
@@ -170,10 +171,11 @@
 %-----------------------------------------------------------------------------%
 
     % pred_inst_matches(PredInstA, PredInstB, ModuleInfo)
+    %
     %   Succeeds if PredInstA specifies a pred that can be used wherever and
     %   whenever PredInstB could be used.  This is true if they both have the
-    %   same PredOrFunc indicator and the same determinism, and if the
-    %   arguments match using pred_inst_argmodes_match.
+    % same PredOrFunc indicator and the same determinism, and if the arguments
+    % match using pred_inst_argmodes_match.
     %
 :- pred pred_inst_matches(pred_inst_info::in, pred_inst_info::in,
     module_info::in) is semidet.
@@ -218,6 +220,10 @@
     %
 :- pred inst_is_not_fully_unique(module_info::in, mer_inst::in) is semidet.
 
+    % inst_is_clobbered succeeds iff the inst passed is `clobbered'
+    % or `mostly_clobbered' or if it is a user-defined inst which
+    % is defined as one of those.
+    %
 :- pred inst_is_clobbered(module_info::in, mer_inst::in) is semidet.
 
 :- pred inst_list_is_ground(list(mer_inst)::in, module_info::in) is semidet.
@@ -254,6 +260,10 @@
 :- pred bound_inst_list_is_not_fully_unique(list(bound_inst)::in,
     module_info::in) is semidet.
 
+    % inst_is_free succeeds iff the inst passed is `free'
+    % or is a user-defined inst which is defined as `free'.
+    % Abstract insts must not be free.
+    %
 :- pred inst_is_free(module_info::in, mer_inst::in) is semidet.
 
 :- pred inst_is_any(module_info::in, mer_inst::in) is semidet.
@@ -263,6 +273,10 @@
 :- pred bound_inst_list_is_free(list(bound_inst)::in, module_info::in)
     is semidet.
 
+    % inst_is_bound succeeds iff the inst passed is not `free'
+    % or is a user-defined inst which is not defined as `free'.
+    % Abstract insts must be bound.
+    %
 :- pred inst_is_bound(module_info::in, mer_inst::in) is semidet.
 
 :- pred inst_is_bound_to_functors(module_info::in, mer_inst::in,
@@ -324,43 +338,6 @@
 
 %-----------------------------------------------------------------------------%
 
-inst_matches_initial(InstA, InstB, Type, ModuleInfo) :-
-    inst_matches_initial_1(InstA, InstB, Type, ModuleInfo, _, no, _).
-
-inst_matches_initial(InstA, InstB, Type, !ModuleInfo, !Sub) :-
-    inst_matches_initial_1(InstA, InstB, Type, !ModuleInfo,
-        yes(!.Sub), MaybeSub),
-    (
-        MaybeSub = yes(!:Sub)
-    ;
-        MaybeSub = no,
-        unexpected(this_file, "inst_matches_initial: missing inst_var_sub")
-    ).
-
-inst_matches_initial_no_implied_modes(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo) ^ calculate_sub := forward,
-    inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
-
-inst_matches_initial_no_implied_modes(InstA, InstB, Type, !ModuleInfo, !Sub) :-
-    Info0 = (init_inst_match_info(!.ModuleInfo)
-        ^ calculate_sub := forward)
-        ^ maybe_sub := yes(!.Sub),
-    inst_matches_final_2(InstA, InstB, yes(Type), Info0, Info),
-    !:ModuleInfo = Info ^ module_info,
-    yes(!:Sub) = Info ^ maybe_sub.
-
-:- pred inst_matches_initial_1(mer_inst::in, mer_inst::in, mer_type::in,
-    module_info::in, module_info::out,
-    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)
-        ^ maybe_sub := !.MaybeSub)
-        ^ calculate_sub := forward,
-    inst_matches_initial_2(InstA, InstB, yes(Type), Info0, Info),
-    !:ModuleInfo = Info ^ module_info,
-    !:MaybeSub = Info ^ maybe_sub.
-
 :- type inst_match_inputs
     --->    inst_match_inputs(
                 mer_inst,
@@ -388,6 +365,26 @@
 expansion_insert(E, S0, S) :-
     set_tree234.insert(E, S0, S).
 
+inst_expand(ModuleInfo, !Inst) :-
+    ( !.Inst = defined_inst(InstName) ->
+        inst_lookup(ModuleInfo, InstName, !:Inst),
+        inst_expand(ModuleInfo, !Inst)
+    ;
+        true
+    ).
+
+inst_expand_and_remove_constrained_inst_vars(ModuleInfo, !Inst) :-
+    ( !.Inst = defined_inst(InstName) ->
+        inst_lookup(ModuleInfo, InstName, !:Inst),
+        inst_expand(ModuleInfo, !Inst)
+    ; !.Inst = constrained_inst_vars(_, !:Inst) ->
+        inst_expand(ModuleInfo, !Inst)
+    ;
+        true
+    ).
+
+%-----------------------------------------------------------------------------%
+
     % The uniqueness_comparison type is used by the predicate
     % compare_uniqueness to determine what order should be used for
     % comparing two uniqueness annotations.
@@ -403,12 +400,12 @@
 
 :- type inst_match_info
     --->    inst_match_info(
-                module_info             :: module_info,
-                expansions              :: expansions,
-                maybe_sub               :: maybe(inst_var_sub),
-                calculate_sub           :: calculate_sub,
-                uniqueness_comparison   :: uniqueness_comparison,
-                any_matches_any         :: bool
+                imi_module_info             :: module_info,
+                imi_expansions              :: expansions,
+                imi_maybe_sub               :: maybe(inst_var_sub),
+                imi_calculate_sub           :: calculate_sub,
+                imi_uniqueness_comparison   :: uniqueness_comparison,
+                imi_any_matches_any         :: bool
             ).
 
     % The calculate_sub type determines how the inst var substitution
@@ -427,30 +424,28 @@
     ;       none.
             % Do not calculate inst var substitions.
 
-:- func sub(inst_match_info) = inst_var_sub is semidet.
+:- func init_inst_match_info(module_info, maybe(inst_var_sub),
+    calculate_sub, uniqueness_comparison, bool) = inst_match_info.
 
-sub(Info) = Sub :-
-    Info ^ maybe_sub = yes(Sub).
+init_inst_match_info(ModuleInfo, MaybeSub, CalculateSub, Comparison,
+        AnyMatchesAny) =
+    inst_match_info(ModuleInfo, expansion_init, MaybeSub, CalculateSub,
+        Comparison, AnyMatchesAny).
 
-:- func 'sub :='(inst_match_info, inst_var_sub) = inst_match_info.
-
-'sub :='(Info, Sub) =
-    Info ^ maybe_sub := yes(Sub).
-
-:- func init_inst_match_info(module_info) = inst_match_info.
-
-init_inst_match_info(ModuleInfo) =
-    inst_match_info(ModuleInfo, expansion_init, no, none, match, yes).
+:- type inst_matches_pred ==
+    pred(mer_inst, mer_inst, maybe(mer_type),
+        inst_match_info, inst_match_info).
+:- inst inst_matches_pred == (pred(in, in, in, in, out) is semidet).
 
 :- pred swap_sub(
     pred(inst_match_info, inst_match_info)::in(pred(in, out) is semidet),
     inst_match_info::in, inst_match_info::out) is semidet.
 
 swap_sub(P, !Info) :-
-    CalculateSub = !.Info ^ calculate_sub,
-    !:Info = !.Info ^ calculate_sub := swap_calculate_sub(CalculateSub),
+    CalculateSub = !.Info ^ imi_calculate_sub,
+    !Info ^ imi_calculate_sub := swap_calculate_sub(CalculateSub),
     P(!Info),
-    !:Info = !.Info ^ calculate_sub := CalculateSub.
+    !Info ^ imi_calculate_sub := CalculateSub.
 
 :- func swap_calculate_sub(calculate_sub) = calculate_sub.
 
@@ -458,35 +453,23 @@
 swap_calculate_sub(reverse) = forward.
 swap_calculate_sub(none) = none.
 
-:- type inst_matches_pred ==
-    pred(mer_inst, mer_inst, maybe(mer_type),
-        inst_match_info, inst_match_info).
-:- inst inst_matches_pred ==
-    (pred(in, in, in, in, out) is semidet).
+:- pred swap_args(inst_matches_pred::in(inst_matches_pred),
+    mer_inst::in, mer_inst::in, maybe(mer_type)::in,
+    inst_match_info::in, inst_match_info::out) is semidet.
 
-:- pred inst_matches_initial_2 `with_type` inst_matches_pred.
-:- mode inst_matches_initial_2 `with_inst` inst_matches_pred.
+swap_args(P, InstA, InstB, Type, !Info) :-
+    P(InstB, InstA, Type, !Info).
 
-inst_matches_initial_2(InstA, InstB, MaybeType, !Info) :-
-    ThisExpansion = inst_match_inputs(InstA, InstB, MaybeType),
-    ( expansion_member(ThisExpansion, !.Info ^ expansions) ->
-        true
-    ;
-        inst_expand(!.Info ^ module_info, InstA, InstA2),
-        inst_expand(!.Info ^ module_info, InstB, InstB2),
-        expansion_insert(ThisExpansion, !.Info ^ expansions, Expansions1),
-        handle_inst_var_subs(inst_matches_initial_2,
-            inst_matches_initial_4, InstA2, InstB2, MaybeType,
-            !.Info ^ expansions := Expansions1, !:Info)
-    ).
+%-----------------------------------------------------------------------------%
 
-:- pred handle_inst_var_subs(inst_matches_pred, inst_matches_pred) `with_type`
-    inst_matches_pred.
-:- mode handle_inst_var_subs(in(inst_matches_pred), in(inst_matches_pred))
-    `with_inst` inst_matches_pred.
+:- pred handle_inst_var_subs(
+    inst_matches_pred::in(inst_matches_pred),
+    inst_matches_pred::in(inst_matches_pred),
+    mer_inst::in, mer_inst::in, maybe(mer_type)::in,
+    inst_match_info::in, inst_match_info::out) is semidet.
 
 handle_inst_var_subs(Recurse, Continue, InstA, InstB, Type, !Info) :-
-    CalculateSub = !.Info ^ calculate_sub,
+    CalculateSub = !.Info ^ imi_calculate_sub,
     (
         CalculateSub = forward,
         handle_inst_var_subs_2(Recurse, Continue, InstA, InstB,
@@ -500,29 +483,28 @@
         Continue(InstA, InstB, Type, !Info)
     ).
 
-:- pred handle_inst_var_subs_2(inst_matches_pred, inst_matches_pred)
-    `with_type` inst_matches_pred.
-:- mode handle_inst_var_subs_2(in(inst_matches_pred), in(inst_matches_pred))
-    `with_inst` inst_matches_pred.
+:- pred handle_inst_var_subs_2(
+    inst_matches_pred::in(inst_matches_pred),
+    inst_matches_pred::in(inst_matches_pred),
+    mer_inst::in, mer_inst::in, maybe(mer_type)::in,
+    inst_match_info::in, inst_match_info::out) is semidet.
 
 handle_inst_var_subs_2(Recurse, Continue, InstA, InstB, Type, !Info) :-
     ( InstB = constrained_inst_vars(InstVarsB, InstB1) ->
         % InstB is a constrained_inst_var with upper bound InstB1.
         % We need to check that InstA matches_initial InstB1 and add the
         % appropriate inst_var substitution.
-
         Recurse(InstA, InstB1, Type, !Info),
 
-        ModuleInfo0 = !.Info ^ module_info,
-
         % Call abstractly_unify_inst to calculate the uniqueness of the
         % inst represented by the constrained_inst_var.
         % We pass `Live = is_dead' because we want
         % abstractly_unify(unique, unique) = unique, not shared.
         Live = is_dead,
+        ModuleInfo0 = !.Info ^ imi_module_info,
         abstractly_unify_inst(Live, InstA, InstB1, fake_unify,
             Inst, _Det, ModuleInfo0, ModuleInfo),
-        !:Info = !.Info ^ module_info := ModuleInfo,
+        !Info ^ imi_module_info := ModuleInfo,
         update_inst_var_sub(InstVarsB, Inst, Type, !Info)
     ; InstA = constrained_inst_vars(_InstVarsA, InstA1) ->
         Recurse(InstA1, InstB, Type, !Info)
@@ -530,74 +512,163 @@
         Continue(InstA, InstB, Type, !Info)
     ).
 
-:- pred swap_args(inst_matches_pred) `with_type` inst_matches_pred.
-:- mode swap_args(in(inst_matches_pred)) `with_inst` inst_matches_pred.
+    % Update the inst_var_sub that is computed by inst_matches_initial.
+    % The inst_var_sub records what inst should be substituted for each
+    % inst_var that occurs in the called procedure's argument modes.
+    %
+:- pred update_inst_var_sub(set(inst_var)::in, mer_inst::in,
+    maybe(mer_type)::in, inst_match_info::in, inst_match_info::out) is semidet.
 
-swap_args(P, InstA, InstB, Type, !Info) :-
-    P(InstB, InstA, Type, !Info).
+update_inst_var_sub(InstVars, InstA, MaybeType, !Info) :-
+    (
+        !.Info ^ imi_maybe_sub = yes(_),
+        set.fold(update_inst_var_sub_2(InstA, MaybeType), InstVars, !Info)
+    ;
+        !.Info ^ imi_maybe_sub = no
+    ).
 
-:- pred inst_matches_initial_4 `with_type` inst_matches_pred.
-:- mode inst_matches_initial_4 `with_inst` inst_matches_pred.
+:- pred update_inst_var_sub_2(mer_inst::in, maybe(mer_type)::in, inst_var::in,
+    inst_match_info::in, inst_match_info::out) is semidet.
 
-    % To avoid infinite regress, we assume that
-    % inst_matches_initial is true for any pairs of insts which
-    % occur in `Expansions'.
+update_inst_var_sub_2(InstA, MaybeType, InstVar, !Info) :-
+    (
+        !.Info ^ imi_maybe_sub = yes(InstVarSub0),
+        ( map.search(InstVarSub0, InstVar, InstB) ->
+            % If InstVar already has an inst associated with it, merge
+            % the old inst and the new inst. Fail if this merge is not
+            % possible.
+            ModuleInfo0 = !.Info ^ imi_module_info,
+            inst_merge(InstA, InstB, MaybeType, Inst,
+                ModuleInfo0, ModuleInfo),
+            !Info ^ imi_module_info := ModuleInfo,
+            map.det_update(InstVarSub0, InstVar, Inst, InstVarSub),
+            !Info ^ imi_maybe_sub := yes(InstVarSub)
+        ;
+            map.det_insert(InstVarSub0, InstVar, InstA, InstVarSub),
+            !Info ^ imi_maybe_sub := yes(InstVarSub)
+        )
+    ;
+        !.Info ^ imi_maybe_sub = no,
+        map.det_insert(map.init, InstVar, InstA, InstVarSub),
+        !Info ^ imi_maybe_sub := yes(InstVarSub)
+    ).
+
+%-----------------------------------------------------------------------------%
 
+inst_matches_initial(InstA, InstB, Type, ModuleInfo) :-
+    inst_matches_initial_1(InstA, InstB, Type, ModuleInfo, _, no, _).
+
+inst_matches_initial(InstA, InstB, Type, !ModuleInfo, !Sub) :-
+    inst_matches_initial_1(InstA, InstB, Type, !ModuleInfo,
+        yes(!.Sub), MaybeSub),
+    (
+        MaybeSub = yes(!:Sub)
+    ;
+        MaybeSub = no,
+        unexpected(this_file, "inst_matches_initial: missing inst_var_sub")
+    ).
+
+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, _).
+
+inst_matches_initial_no_implied_modes(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),
+    !:ModuleInfo = Info ^ imi_module_info,
+    yes(!:Sub) = Info ^ imi_maybe_sub.
+
+:- pred inst_matches_initial_1(mer_inst::in, mer_inst::in, mer_type::in,
+    module_info::in, module_info::out,
+    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),
+    !: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.
+
+inst_matches_initial_2(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),
+        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)
+    ).
+
+:- 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.
+
+    % 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) :-
-    !.Info ^ any_matches_any = yes,
-    compare_uniqueness(!.Info ^ uniqueness_comparison, UniqA, UniqB),
+    !.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 ^ module_info, UniqA, HOInstInfoA, InstA),
+    maybe_any_to_bound(Type, !.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 ^ module_info, UniqA, HOInstInfoA, InstA),
+    maybe_any_to_bound(Type, !.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) :-
-    compare_uniqueness(!.Info ^ uniqueness_comparison, UniqA, UniqB),
-    compare_bound_inst_list_uniq(!.Info ^ uniqueness_comparison,
-        ListA, UniqB, !.Info ^ module_info).
+    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) :-
-    compare_uniqueness(!.Info ^ uniqueness_comparison, UniqA, UniqB),
+    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) :-
-    compare_uniqueness(!.Info ^ uniqueness_comparison, UniqA, UniqB),
-    bound_inst_list_is_ground(ListA, Type, !.Info ^ module_info),
-    compare_bound_inst_list_uniq(!.Info ^ uniqueness_comparison,
-        ListA, UniqB, !.Info ^ module_info).
+    compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
+    bound_inst_list_is_ground(ListA, Type, !.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) :-
     Uniq = unique,
-    bound_inst_list_is_ground(List, !.Info ^ module_info),
-    bound_inst_list_is_unique(List, !.Info ^ module_info).
+    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) :-
     Uniq = mostly_unique,
-    bound_inst_list_is_ground(List, !.Info ^ module_info),
-    bound_inst_list_is_mostly_unique(List, !.Info ^ module_info).
+    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) :-
-    compare_uniqueness(!.Info ^ uniqueness_comparison, UniqA, UniqB),
+    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) :-
     MaybeType = yes(Type),
         % We can only check this case properly if the type is known.
-    compare_uniqueness(!.Info ^ uniqueness_comparison, UniqA, UniqB),
-    bound_inst_list_is_complete_for_type(set.init, !.Info ^ module_info,
+    compare_uniqueness(!.Info ^ imi_uniqueness_comparison, UniqA, UniqB),
+    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) :-
-    compare_uniqueness(!.Info ^ uniqueness_comparison, UniqA, UniqB),
+    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) :-
         % I don't know what this should do.
@@ -624,7 +695,7 @@
 ground_matches_initial_bound_inst_list(_, [], _, !Info).
 ground_matches_initial_bound_inst_list(Uniq,
         [bound_functor(ConsId, Args) | List], MaybeType, !Info) :-
-    maybe_get_cons_id_arg_types(!.Info ^ module_info, MaybeType, ConsId,
+    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).
@@ -641,9 +712,10 @@
 
 %-----------------------------------------------------------------------------%
 
-    % A list(bound_inst) is ``complete'' for a given type iff it
-    % includes each functor of the type and each argument of each
-    % functor is also ``complete'' for the type.
+    % A list(bound_inst) is ``complete'' for a given type iff it includes
+    % each functor of the type and each argument of each functor is also
+    % ``complete'' for its type.
+    %
 :- pred bound_inst_list_is_complete_for_type(set(inst_name)::in,
     module_info::in, list(bound_inst)::in, mer_type::in) is semidet.
 
@@ -659,7 +731,7 @@
         (
             list.member(bound_functor(ConsId0, ArgInsts), BoundInsts),
             % Cons_ids returned from type_util.cons_id_arg_types
-            % are not module-qualified so we need to call
+            % are not module-qualified, so we need to call
             % equivalent_cons_ids instead of just using `=/2'.
             equivalent_cons_ids(ConsId0, ConsId),
             list.map(inst_is_complete_for_type(Expansions, ModuleInfo),
@@ -740,40 +812,6 @@
 
 %-----------------------------------------------------------------------------%
 
-    % Update the inst_var_sub that is computed by inst_matches_initial.
-    % The inst_var_sub records what inst should be substituted for each
-    % inst_var that occurs in the called procedure's argument modes.
-    %
-:- pred update_inst_var_sub(set(inst_var)::in, mer_inst::in,
-    maybe(mer_type)::in, inst_match_info::in, inst_match_info::out) is semidet.
-
-update_inst_var_sub(InstVars, InstA, MaybeType, !Info) :-
-    (
-        !.Info ^ maybe_sub  = yes(_),
-        set.fold(update_inst_var_sub_2(InstA, MaybeType),
-            InstVars, !Info)
-    ;
-        !.Info ^ maybe_sub  = no
-    ).
-
-:- pred update_inst_var_sub_2(mer_inst::in, maybe(mer_type)::in, inst_var::in,
-    inst_match_info::in, inst_match_info::out) is semidet.
-
-update_inst_var_sub_2(InstA, MaybeType, InstVar, !Info) :-
-    ( InstB = !.Info ^ sub ^ elem(InstVar) ->
-        % If InstVar already has an inst associated with it, merge the old inst
-        % and the new inst.  Fail if this merge is not possible.
-        ModuleInfo0 = !.Info ^ module_info,
-        inst_merge(InstA, InstB, MaybeType, Inst,
-            ModuleInfo0, ModuleInfo),
-        !:Info = !.Info ^ module_info := ModuleInfo,
-        !:Info = !.Info ^ sub ^ elem(InstVar) := Inst
-    ;
-        !:Info = !.Info ^ sub ^ elem(InstVar) := InstA
-    ).
-
-%-----------------------------------------------------------------------------%
-
     % This predicate checks if two ho_inst_infos match_initial.
     % It does not check uniqueness.
     %
@@ -782,7 +820,7 @@
     inst_match_info::in, inst_match_info::out) is semidet.
 
 ho_inst_info_matches_initial(HOInstInfoA, none, _, _, !Info) :-
-    \+ ho_inst_info_is_nonstandard_func_mode(!.Info ^ module_info,
+    \+ ho_inst_info_is_nonstandard_func_mode(!.Info ^ imi_module_info,
         HOInstInfoA).
 ho_inst_info_matches_initial(none, higher_order(PredInstB), _, Type, !Info) :-
     PredInstB = pred_inst_info(pf_function, ArgModes, _Det),
@@ -800,7 +838,7 @@
     maybe(mer_type)::in, module_info::in) is semidet.
 
 pred_inst_matches_1(PredInstA, PredInstB, MaybeType, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo),
+    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
     pred_inst_matches_2(PredInstA, PredInstB, MaybeType, Info0, _).
 
     % pred_inst_matches_2(PredInstA, PredInstB, !Info)
@@ -839,7 +877,7 @@
 pred_inst_argmodes_matches([], [], [], !Info).
 pred_inst_argmodes_matches([ModeA | ModeAs], [ModeB | ModeBs],
         [MaybeType | MaybeTypes], !Info) :-
-    ModuleInfo = !.Info ^ module_info,
+    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),
@@ -928,17 +966,16 @@
     X = bound_functor(ConsIdX, ArgsX),
     Y = bound_functor(ConsIdY, ArgsY),
     ( equivalent_cons_ids(ConsIdX, ConsIdY) ->
-        maybe_get_cons_id_arg_types(!.Info ^ module_info, MaybeType,
+        maybe_get_cons_id_arg_types(!.Info ^ imi_module_info, MaybeType,
             ConsIdX, list.length(ArgsX), MaybeTypes),
         inst_list_matches_initial(ArgsX, ArgsY, MaybeTypes, !Info),
         bound_inst_list_matches_initial(Xs, Ys, MaybeType, !Info)
     ;
         greater_than_disregard_module_qual(ConsIdX, ConsIdY),
             % ConsIdY does not occur in [X | Xs].
-            % Hence [X | Xs] implicitly specifies `not_reached'
-            % for the args of ConsIdY, and hence
-            % automatically matches_initial Y.  We just need to
-            % check that [X | Xs] matches_initial Ys.
+        % Hence [X | Xs] implicitly specifies `not_reached' for the args
+        % of ConsIdY, and hence automatically matches_initial Y. We just
+        % need to check that [X | Xs] matches_initial Ys.
         bound_inst_list_matches_initial([X | Xs], Ys, MaybeType, !Info)
     ).
 
@@ -953,54 +990,35 @@
 
 %-----------------------------------------------------------------------------%
 
-inst_expand(ModuleInfo, !Inst) :-
-    ( !.Inst = defined_inst(InstName) ->
-        inst_lookup(ModuleInfo, InstName, !:Inst),
-        inst_expand(ModuleInfo, !Inst)
-    ;
-        true
-    ).
-
-inst_expand_and_remove_constrained_inst_vars(ModuleInfo, !Inst) :-
-    ( !.Inst = defined_inst(InstName) ->
-        inst_lookup(ModuleInfo, InstName, !:Inst),
-        inst_expand(ModuleInfo, !Inst)
-    ; !.Inst = constrained_inst_vars(_, !:Inst) ->
-        inst_expand(ModuleInfo, !Inst)
-    ;
-        true
-    ).
-
-%-----------------------------------------------------------------------------%
-
 inst_matches_final(InstA, InstB, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo),
+    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
     inst_matches_final_2(InstA, InstB, no, Info0, _).
 
 inst_matches_final(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo),
+    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
     inst_matches_final_2(InstA, InstB, yes(Type), Info0, _).
 
-:- pred inst_matches_final_2 `with_type` inst_matches_pred.
-:- mode inst_matches_final_2 `with_inst` inst_matches_pred.
+:- pred inst_matches_final_2(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) :-
     ThisExpansion = inst_match_inputs(InstA, InstB, MaybeType),
-    ( expansion_member(ThisExpansion, !.Info ^ expansions) ->
+    Expansions0 = !.Info ^ imi_expansions,
+    ( expansion_member(ThisExpansion, Expansions0) ->
         true
     ; InstA = InstB ->
         true
     ;
-        inst_expand(!.Info ^ module_info, InstA, InstA2),
-        inst_expand(!.Info ^ module_info, InstB, InstB2),
-        expansion_insert(ThisExpansion, !.Info ^ expansions, Expansions1),
-        handle_inst_var_subs(inst_matches_final_2,
-            inst_matches_final_3, InstA2, InstB2, MaybeType,
-            !.Info ^ expansions := Expansions1, !:Info)
+        inst_expand(!.Info ^ imi_module_info, InstA, InstA2),
+        inst_expand(!.Info ^ imi_module_info, InstB, InstB2),
+        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)
     ).
 
-:- pred inst_matches_final_3 `with_type` inst_matches_pred.
-:- mode inst_matches_final_3 `with_inst` inst_matches_pred.
+:- 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) :-
@@ -1008,10 +1026,12 @@
     unique_matches_final(UniqA, UniqB).
 inst_matches_final_3(any(UniqA, HOInstInfoA), ground(_, _)@InstB, Type,
         !Info) :-
-    maybe_any_to_bound(Type, !.Info ^ module_info, UniqA, HOInstInfoA, InstA),
+    maybe_any_to_bound(Type, !.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 ^ module_info, UniqA, HOInstInfoA, InstA),
+    maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA,
+        HOInstInfoA, InstA),
     inst_matches_final_2(InstA, InstB, Type, !Info).
 inst_matches_final_3(free, any(Uniq, _), _, !Info) :-
     % We do not yet allow `free' to match `any',
@@ -1022,11 +1042,11 @@
 inst_matches_final_3(free, free, _, !Info).
 inst_matches_final_3(bound(UniqA, ListA), any(UniqB, none), _, !Info) :-
     unique_matches_final(UniqA, UniqB),
-    bound_inst_list_matches_uniq(ListA, UniqB, !.Info ^ module_info),
+    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 ^ module_info).
+    bound_inst_list_is_ground_or_any(ListA, !.Info ^ imi_module_info).
 inst_matches_final_3(bound(UniqA, ListA), bound(UniqB, ListB), MaybeType,
         !Info) :-
     unique_matches_final(UniqA, UniqB),
@@ -1034,24 +1054,23 @@
 inst_matches_final_3(bound(UniqA, ListA), ground(UniqB, none), Type,
         !Info) :-
     unique_matches_final(UniqA, UniqB),
-    bound_inst_list_is_ground(ListA, Type, !.Info ^ module_info),
-    bound_inst_list_matches_uniq(ListA, UniqB, !.Info ^ module_info).
+    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) :-
     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) :-
-    \+ ho_inst_info_is_nonstandard_func_mode(!.Info ^ module_info,
-        HOInstInfoA),
+    ModuleInfo = !.Info ^ imi_module_info,
+    \+ ho_inst_info_is_nonstandard_func_mode(ModuleInfo, HOInstInfoA),
     unique_matches_final(UniqA, UniqB),
-    bound_inst_list_is_ground(ListB, MaybeType, !.Info ^ module_info),
-    uniq_matches_bound_inst_list(UniqA, ListB, !.Info ^ module_info),
+    bound_inst_list_is_ground(ListB, MaybeType, ModuleInfo),
+    uniq_matches_bound_inst_list(UniqA, ListB, ModuleInfo),
     (
         MaybeType = yes(Type),
         % We can only do this check if the type is known.
-        bound_inst_list_is_complete_for_type(set.init,
-            !.Info ^ module_info, 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
@@ -1074,7 +1093,7 @@
         !Info) :-
     ( InstB = constrained_inst_vars(InstVarsB, InstB1) ->
         % Constrained_inst_vars match_final only if InstVarsA contains
-        % all the variables in InstVarsB
+        % all the variables in InstVarsB.
         InstVarsB `set.subset` InstVarsA,
         inst_matches_final_2(InstA, InstB1, MaybeType, !Info)
     ;
@@ -1085,7 +1104,7 @@
     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_is_nonstandard_func_mode(!.Info ^ module_info,
+    \+ ho_inst_info_is_nonstandard_func_mode(!.Info ^ imi_module_info,
         HOInstInfoA).
 ho_inst_info_matches_final(none, higher_order(PredInstB), Type, !Info) :-
     PredInstB = pred_inst_info(pf_function, ArgModes, _Det),
@@ -1122,53 +1141,51 @@
     X = bound_functor(ConsIdX, ArgsX),
     Y = bound_functor(ConsIdY, ArgsY),
     ( equivalent_cons_ids(ConsIdX, ConsIdY) ->
-        maybe_get_cons_id_arg_types(!.Info ^ module_info, MaybeType,
+        maybe_get_cons_id_arg_types(!.Info ^ imi_module_info, MaybeType,
             ConsIdX, list.length(ArgsX), MaybeTypes),
         inst_list_matches_final(ArgsX, ArgsY, MaybeTypes, !Info),
         bound_inst_list_matches_final(Xs, Ys, MaybeType, !Info)
     ;
         greater_than_disregard_module_qual(ConsIdX, ConsIdY),
             % ConsIdY does not occur in [X | Xs].
-            % Hence [X | Xs] implicitly specifies `not_reached'
-            % for the args of ConsIdY, and hence
-            % automatically matches_final Y.  We just need to
-            % check that [X | Xs] matches_final Ys.
+        % Hence [X | Xs] implicitly specifies `not_reached' for the args
+        % of ConsIdY, and hence automatically matches_final Y. We just
+        % need to check that [X | Xs] matches_final Ys.
         bound_inst_list_matches_final([X | Xs], Ys, MaybeType, !Info)
     ).
 
 inst_is_at_least_as_instantiated(InstA, InstB, Type, ModuleInfo) :-
-    Info = (init_inst_match_info(ModuleInfo)
-        ^ uniqueness_comparison := instantiated)
-        ^ any_matches_any := no,
+    Info = init_inst_match_info(ModuleInfo, no, none, instantiated, no),
     inst_matches_initial_2(InstA, InstB, yes(Type), Info, _).
 
 inst_matches_binding(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo) ^ any_matches_any := no,
+    Info0 = init_inst_match_info(ModuleInfo, no, none, match, no),
     inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
 
 inst_matches_binding_allow_any_any(InstA, InstB, Type, ModuleInfo) :-
-    Info0 = init_inst_match_info(ModuleInfo),
+    Info0 = init_inst_match_info(ModuleInfo, no, none, match, yes),
     inst_matches_binding_2(InstA, InstB, yes(Type), Info0, _).
 
-:- pred inst_matches_binding_2 `with_type` inst_matches_pred.
-:- mode inst_matches_binding_2 `with_inst` inst_matches_pred.
+:- pred inst_matches_binding_2(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) :-
     ThisExpansion = inst_match_inputs(InstA, InstB, MaybeType),
-    ( expansion_member(ThisExpansion, !.Info ^ expansions) ->
+    Expansions0 = !.Info ^ imi_expansions,
+    ( expansion_member(ThisExpansion, Expansions0) ->
         true
     ;
-        inst_expand_and_remove_constrained_inst_vars(
-            !.Info ^ module_info, InstA, InstA2),
-        inst_expand_and_remove_constrained_inst_vars(
-            !.Info ^ module_info, InstB, InstB2),
-        expansion_insert(ThisExpansion, !.Info ^ expansions, Expansions1),
-        inst_matches_binding_3(InstA2, InstB2, MaybeType,
-            !.Info ^ expansions := Expansions1, !:Info)
+        inst_expand_and_remove_constrained_inst_vars(!.Info ^ imi_module_info,
+            InstA, InstA2),
+        inst_expand_and_remove_constrained_inst_vars(!.Info ^ imi_module_info,
+            InstB, InstB2),
+        expansion_insert(ThisExpansion, Expansions0, Expansions),
+        !Info ^ imi_expansions := Expansions,
+        inst_matches_binding_3(InstA2, InstB2, MaybeType, !Info)
     ).
 
-:- pred inst_matches_binding_3 `with_type` inst_matches_pred.
-:- mode inst_matches_binding_3 `with_inst` inst_matches_pred.
+:- 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
@@ -1176,45 +1193,52 @@
 inst_matches_binding_3(free, free, _, !Info).
 inst_matches_binding_3(any(UniqA, HOInstInfoA), any(UniqB, HOInstInfoB), Type,
         !Info) :-
-    ( !.Info ^ any_matches_any = yes ->
+    AnyMatchesAny = !.Info ^ imi_any_matches_any,
+    (
+        AnyMatchesAny = yes,
         ho_inst_info_matches_final(HOInstInfoA, HOInstInfoB, Type, !Info)
     ;
-        maybe_any_to_bound(Type, !.Info ^ module_info, UniqA, HOInstInfoA,
+        AnyMatchesAny = no,
+        maybe_any_to_bound(Type, !.Info ^ imi_module_info, UniqA, HOInstInfoA,
             InstA),
-        maybe_any_to_bound(Type, !.Info ^ module_info, UniqB, HOInstInfoB,
+        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 ^ module_info, UniqA, HOInstInfoA, InstA),
+    maybe_any_to_bound(Type, !.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 ^ module_info, UniqA, HOInstInfoA, InstA),
+    maybe_any_to_bound(Type, !.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 ^ module_info, UniqB, HOInstInfoB, InstB),
+    maybe_any_to_bound(Type, !.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 ^ module_info, UniqB, HOInstInfoB, InstB),
+    maybe_any_to_bound(Type, !.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 ^ module_info).
+    bound_inst_list_is_ground(ListA, Type, !.Info ^ imi_module_info).
 inst_matches_binding_3(ground(_UniqA, _), bound(_UniqB, ListB), MaybeType,
         !Info) :-
-    bound_inst_list_is_ground(ListB, MaybeType, !.Info ^ module_info),
+    bound_inst_list_is_ground(ListB, MaybeType, !.Info ^ imi_module_info),
     (
         MaybeType = yes(Type),
         % We can only do this check if the type is known.
         bound_inst_list_is_complete_for_type(set.init,
-            !.Info ^ module_info, ListB, Type)
+            !.Info ^ imi_module_info, ListB, Type)
     ;
         true
         % XXX enabling the check for bound_inst_list_is_complete
@@ -1225,7 +1249,7 @@
 inst_matches_binding_3(ground(_UniqA, HOInstInfoA),
         ground(_UniqB, HOInstInfoB), MaybeType, !Info) :-
     ho_inst_info_matches_binding(HOInstInfoA, HOInstInfoB, MaybeType,
-        !.Info ^ module_info).
+        !.Info ^ imi_module_info).
 inst_matches_binding_3(abstract_inst(Name, ArgsA), abstract_inst(Name, ArgsB),
         _MaybeType, !Info) :-
     list.duplicate(length(ArgsA), no, MaybeTypes),
@@ -1273,26 +1297,21 @@
     X = bound_functor(ConsIdX, ArgsX),
     Y = bound_functor(ConsIdY, ArgsY),
     ( equivalent_cons_ids(ConsIdX, ConsIdY) ->
-        maybe_get_cons_id_arg_types(!.Info ^ module_info, MaybeType,
+        maybe_get_cons_id_arg_types(!.Info ^ imi_module_info, MaybeType,
             ConsIdX, list.length(ArgsX), MaybeTypes),
         inst_list_matches_binding(ArgsX, ArgsY, MaybeTypes, !Info),
         bound_inst_list_matches_binding(Xs, Ys, MaybeType, !Info)
     ;
         greater_than_disregard_module_qual(ConsIdX, ConsIdY),
             % ConsIdX does not occur in [X | Xs].
-            % Hence [X | Xs] implicitly specifies `not_reached'
-            % for the args of ConsIdY, and hence
-            % automatically matches_binding Y.  We just need to
-            % check that [X | Xs] matches_binding Ys.
+        % Hence [X | Xs] implicitly specifies `not_reached' for the args
+        % of ConsIdY, and hence automatically matches_binding Y. We just
+        % need to check that [X | Xs] matches_binding Ys.
         bound_inst_list_matches_binding([X | Xs], Ys, MaybeType, !Info)
     ).
 
 %-----------------------------------------------------------------------------%
 
-    % inst_is_clobbered succeeds iff the inst passed is `clobbered'
-    % or `mostly_clobbered' or if it is a user-defined inst which
-    % is defined as one of those.
-
 inst_is_clobbered(_, not_reached) :- fail.
 inst_is_clobbered(_, any(mostly_clobbered, _)).
 inst_is_clobbered(_, any(clobbered, _)).
@@ -1308,10 +1327,6 @@
     inst_lookup(ModuleInfo, InstName, Inst),
     inst_is_clobbered(ModuleInfo, Inst).
 
-    % inst_is_free succeeds iff the inst passed is `free'
-    % or is a user-defined inst which is defined as `free'.
-    % Abstract insts must not be free.
-    %
 inst_is_free(_, free).
 inst_is_free(_, free(_Type)).
 inst_is_free(_, inst_var(_)) :-
@@ -1331,10 +1346,6 @@
     inst_lookup(ModuleInfo, InstName, Inst),
     inst_is_any(ModuleInfo, Inst).
 
-    % inst_is_bound succeeds iff the inst passed is not `free'
-    % or is a user-defined inst which is not defined as `free'.
-    % Abstract insts must be bound.
-    %
 inst_is_bound(_, not_reached).
 inst_is_bound(_, any(_, _)).
 inst_is_bound(_, ground(_, _)).
@@ -1364,8 +1375,8 @@
 
 %-----------------------------------------------------------------------------%
 
-    % inst_is_ground succeeds iff the inst passed is `ground'
-    % or the equivalent.  Abstract insts are not considered ground.
+    % inst_is_ground succeeds iff the inst passed is `ground' or the
+    % equivalent. Abstract insts are not considered ground.
     %
 inst_is_ground(ModuleInfo, Inst) :-
     inst_is_ground(ModuleInfo, no, Inst).
@@ -1377,8 +1388,8 @@
     set.init(Expansions0),
     inst_is_ground_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.
+    % 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,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
@@ -1422,16 +1433,15 @@
     set.init(Expansions0),
     inst_is_ground_or_any_2(ModuleInfo, 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.
+    % 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_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).
+    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) :-
@@ -1449,15 +1459,15 @@
         inst_is_ground_or_any_2(ModuleInfo, Inst2, !Expansions)
     ).
 
-    % inst_is_unique succeeds iff the inst passed is unique or free.  Abstract
-    % insts are not considered unique.
+    % inst_is_unique succeeds iff the inst passed is unique or free.
+    % Abstract insts are not considered unique.
     %
 inst_is_unique(ModuleInfo, Inst) :-
     set.init(Expansions0),
     inst_is_unique_2(ModuleInfo, 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.
+    % 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_unique_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
@@ -1490,8 +1500,8 @@
     set.init(Expansions0),
     inst_is_mostly_unique_2(ModuleInfo, 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.
+    % 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_mostly_unique_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
@@ -1521,17 +1531,15 @@
         inst_is_mostly_unique_2(ModuleInfo, Inst2, !Expansions)
     ).
 
-    % inst_is_not_partly_unique succeeds iff the inst passed is
-    % not unique or mostly_unique, i.e. if it is shared
-    % or free.  It fails for abstract insts.
+    % inst_is_not_partly_unique succeeds iff the inst passed is not unique
+    % or mostly_unique, i.e. if it is shared free. It fails for abstract insts.
     %
 inst_is_not_partly_unique(ModuleInfo, Inst) :-
     set.init(Expansions0),
     inst_is_not_partly_unique_2(ModuleInfo, 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.
+    % 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_not_partly_unique_2(module_info::in, mer_inst::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
@@ -1667,8 +1675,7 @@
 bound_inst_list_is_ground_or_any_2([bound_functor(_Name, Args) | BoundInsts],
         ModuleInfo, !Expansions) :-
     inst_list_is_ground_or_any_2(Args, ModuleInfo, !Expansions),
-    bound_inst_list_is_ground_or_any_2(BoundInsts, ModuleInfo,
-        !Expansions).
+    bound_inst_list_is_ground_or_any_2(BoundInsts, ModuleInfo, !Expansions).
 
 :- pred bound_inst_list_is_unique_2(list(bound_inst)::in, module_info::in,
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
@@ -1753,7 +1760,11 @@
 :- pred inst_list_is_ground_2(list(mer_inst)::in, list(maybe(mer_type))::in,
     module_info::in, set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
-inst_list_is_ground_2([], _, _, !Expansions).
+inst_list_is_ground_2([], [], _, !Expansions).
+inst_list_is_ground_2([], [_ | _], _, !Expansions) :-
+    unexpected(this_file, "inst_list_is_ground_2: list length mismatch").
+inst_list_is_ground_2([_ | _], [], _, !Expansions) :-
+    unexpected(this_file, "inst_list_is_ground_2: list length mismatch").
 inst_list_is_ground_2([Inst | Insts], [MaybeType | MaybeTypes], ModuleInfo,
         !Expansions) :-
     inst_is_ground_1(ModuleInfo, MaybeType, Inst, !Expansions),
@@ -1779,8 +1790,7 @@
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 inst_list_is_mostly_unique_2([], _, !Expansions).
-inst_list_is_mostly_unique_2([Inst | Insts], ModuleInfo,
-        !Expansions) :-
+inst_list_is_mostly_unique_2([Inst | Insts], ModuleInfo, !Expansions) :-
     inst_is_mostly_unique_2(ModuleInfo, Inst, !Expansions),
     inst_list_is_mostly_unique_2(Insts, ModuleInfo, !Expansions).
 
@@ -1788,8 +1798,7 @@
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 inst_list_is_not_partly_unique_2([], _, !Expansions).
-inst_list_is_not_partly_unique_2([Inst | Insts], ModuleInfo,
-        !Expansions) :-
+inst_list_is_not_partly_unique_2([Inst | Insts], ModuleInfo, !Expansions) :-
     inst_is_not_partly_unique_2(ModuleInfo, Inst, !Expansions),
     inst_list_is_not_partly_unique_2(Insts, ModuleInfo, !Expansions).
 
@@ -1797,8 +1806,7 @@
     set(mer_inst)::in, set(mer_inst)::out) is semidet.
 
 inst_list_is_not_fully_unique_2([], _, !Expansions).
-inst_list_is_not_fully_unique_2([Inst | Insts], ModuleInfo,
-        !Expansions) :-
+inst_list_is_not_fully_unique_2([Inst | Insts], ModuleInfo, !Expansions) :-
     inst_is_not_fully_unique_2(ModuleInfo, Inst, !Expansions),
     inst_list_is_not_fully_unique_2(Insts, ModuleInfo, !Expansions).
 
@@ -2032,8 +2040,8 @@
 maybe_any_to_bound(yes(Type), ModuleInfo, Uniq, none, Inst) :-
     \+ type_util.is_solver_type(ModuleInfo, Type),
     ( type_constructors(ModuleInfo, Type, Constructors) ->
-        constructors_to_bound_any_insts(ModuleInfo, Uniq,
-            Constructors, BoundInsts0),
+        constructors_to_bound_any_insts(ModuleInfo, Uniq, Constructors,
+            BoundInsts0),
         list.sort_and_remove_dups(BoundInsts0, BoundInsts),
         Inst = bound(Uniq, BoundInsts)
     ; type_may_contain_solver_type(ModuleInfo, Type) ->
Index: compiler/inst_util.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/inst_util.m,v
retrieving revision 1.57
diff -u -b -r1.57 inst_util.m
--- compiler/inst_util.m	23 Dec 2008 01:37:34 -0000	1.57
+++ compiler/inst_util.m	27 Jan 2009 13:23:38 -0000
@@ -386,7 +386,6 @@
         !ModuleInfo) :-
     make_any_inst(Inst0, is_live, Uniq, Real, Inst, Det, !ModuleInfo).
 
-
 % abstractly_unify_inst_3(is_live, abstract_inst(_,_), free, _, _, _, _, _)
 %       :- fail.
 
@@ -669,24 +668,21 @@
 
 abstractly_unify_bound_inst_list(Live, Xs, Ys, Real, L, Det, !ModuleInfo) :-
     ( ( Xs = [] ; Ys = [] ) ->
-        %
         % This probably shouldn't happen. If we get here, it means that
         % a previous goal had determinism `failure' or `erroneous',
         % but we should have optimized away the rest of the conjunction
         % after that goal.
-        %
+
         L = [],
         Det = detism_erroneous
     ;
         abstractly_unify_bound_inst_list_2(Live, Xs, Ys, Real,
             L, Det0, !ModuleInfo),
 
-        %
         % If there are multiple alternatives for either of the inputs,
         % or the constructor of the single alternative for each input
         % doesn't match, then the unification can fail, so adjust the
         % determinism.
-        %
         (
             Xs = [bound_functor(ConsIdX, _)],
             Ys = [bound_functor(ConsIdY, _)],
Index: compiler/instmap.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/instmap.m,v
retrieving revision 1.63
diff -u -b -r1.63 instmap.m
--- compiler/instmap.m	2 Jan 2009 03:12:07 -0000	1.63
+++ compiler/instmap.m	27 Jan 2009 15:14:54 -0000
@@ -1197,21 +1197,30 @@
 instmap_delta_no_output_vars_2([], _, _, _, _).
 instmap_delta_no_output_vars_2([Var | Vars], InstMap0, InstMapDelta, VarTypes,
         ModuleInfo) :-
+    instmap_lookup_var(InstMap0, Var, OldInst),
+    ( map.search(InstMapDelta, Var, NewInst) ->
     % We use `inst_matches_binding' to check that the new inst has only
     % added information or lost uniqueness, not bound anything.
     % If the instmap delta contains the variable, the variable may still
     % not be output, if the change is just an increase in information
-    % rather than an increase in instantiatedness. If the instmap delta
-    % doesn't contain the variable, it may still have been (partially) output,
-    % if its inst is (or contains) `any'.
-    instmap_lookup_var(InstMap0, Var, Inst0),
-    ( map.search(InstMapDelta, Var, Inst1) ->
-        Inst = Inst1
+        % rather than an increase in instantiatedness.
+        %
+        % XXX Inlining can result in cases where OldInst (from procedure 1)
+        % can decide that Var must be bound to one set of function symbols,
+        % while NewInst (from a later unification inlined into procedure 1
+        % from procedure 2) can say that it is bound to a different,
+        % non-overlapping set of function symbols. In such cases,
+        % inst_matches_binding will fail, even though we want to succeed.
+        % The right fix for this would be to generalize inst_matches_binding,
+        % to allow the caller to specify what kinds of deviations from an exact
+        % syntactic match are ok.
+        map.lookup(VarTypes, Var, Type),
+        inst_matches_binding(NewInst, OldInst, Type, ModuleInfo)
     ;
-        Inst = Inst0
+        % If the instmap delta doesn't contain the variable, it may still
+        % have been (partially) output, if its inst is (or contains) `any'.
+        not inst_contains_any(ModuleInfo, OldInst)
     ),
-    map.lookup(VarTypes, Var, Type),
-    inst_matches_binding(Inst, Inst0, Type, ModuleInfo),
     instmap_delta_no_output_vars_2(Vars, InstMap0, InstMapDelta, VarTypes,
         ModuleInfo).
 
Index: compiler/mode_util.m
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/compiler/mode_util.m,v
retrieving revision 1.207
diff -u -b -r1.207 mode_util.m
--- compiler/mode_util.m	23 Dec 2008 01:37:37 -0000	1.207
+++ compiler/mode_util.m	28 Jan 2009 02:37:28 -0000
@@ -208,6 +208,7 @@
 :- import_module maybe.
 :- import_module pair.
 :- import_module set.
+:- import_module string.
 :- import_module term.
 :- import_module varset.
 
@@ -1165,7 +1166,7 @@
         (
             RecomputeAtomic = recompute_atomic_instmap_deltas,
             recompute_instmap_delta_unify(Uni, UniMode0, UniMode,
-                GoalInfo, InstMap0, InstMapDelta, !.RI)
+                GoalInfo, InstMap0, InstMapDelta, !RI)
         ;
             RecomputeAtomic = do_not_recompute_atomic_instmap_deltas,
             UniMode = UniMode0,
@@ -1378,8 +1379,7 @@
             % XXX  We shouldn't ever get here, but unfortunately
             % the mode system currently has several problems (most
             % noticeably lack of alias tracking for unique modes)
-            % which mean inst_matches_initial can sometimes fail
-            % here.
+            % which mean inst_matches_initial can sometimes fail here.
             !:ModuleInfo = SaveModuleInfo,
             !:Sub = SaveSub
         )
@@ -1404,6 +1404,10 @@
         instmap_lookup_var(InstMap, Arg, ArgInst0),
         mode_get_insts(!.ModuleInfo, Mode0, _, FinalInst),
         (
+            % The is_dead allows abstractly_unify_inst to succeed when
+            % some parts of ArgInst0 and the corresponding parts of FinalInst
+            % are free.
+            % XXX There should be a better way to communicate that information.
             abstractly_unify_inst(is_dead, ArgInst0, FinalInst,
                 fake_unify, UnifyInst, _, !ModuleInfo)
         ->
@@ -1420,16 +1424,16 @@
 
 :- pred recompute_instmap_delta_unify(unification::in, unify_mode::in,
     unify_mode::out, hlds_goal_info::in, instmap::in, instmap_delta::out,
-    recompute_info::in) is det.
+    recompute_info::in, recompute_info::out) is det.
 
 recompute_instmap_delta_unify(Uni, UniMode0, UniMode, GoalInfo,
-        InstMap, InstMapDelta, RI) :-
+        InstMap, InstMapDelta, !RI) :-
     % Deconstructions are the only types of unifications that can require
     % updating of the instmap_delta after simplify.m has been run.
     % Type specialization may require constructions of type-infos, 
     % typeclass-infos or predicate constants to be added to the
     % instmap_delta.
-    ModuleInfo = RI ^ ri_module_info,
+    ModuleInfo0 = !.RI ^ ri_module_info,
     (
         Uni = deconstruct(Var, _ConsId, Vars, UniModes, _, _CanCGC),
 
@@ -1438,18 +1442,33 @@
 
         OldInstMapDelta = goal_info_get_instmap_delta(GoalInfo),
         instmap_lookup_var(InstMap, Var, InitialInst),
-        ( instmap_delta_search_var(OldInstMapDelta, Var, FinalInst1) ->
-            % XXX we need to merge the information in InitialInst
-            % and FinalInst1. In puzzle_detism_bug, InitialInst
-            % has a var bound to one function symbol (james), while
-            % FinalInst1 has it bound to another (katherine).
-            % The correct final inst is thus `unreachable', but
-            % we don't return that.
-            FinalInst = FinalInst1
-        ;
-            % It wasn't in the instmap_delta, so the inst didn't
-            % change.
-            FinalInst = InitialInst
+        ( instmap_delta_search_var(OldInstMapDelta, Var, DeltaInst) ->
+            % Inlining can result in situations where the initial inst
+            % (from procedure 1) can decide that a variable must be bound
+            % to one set of function symbols, while the instmap delta from
+            % a later unification (from procedure 2) can say that it is bound
+            % to a different, non-overlapping set of function symbols.
+            %
+            % The is_dead allows abstractly_unify_inst to succeed when some
+            % parts of InitialInst and the corresponding parts of DeltaInst
+            % are free.
+            % XXX There should be a better way to communicate that information.
+            (
+                abstractly_unify_inst(is_dead, InitialInst, DeltaInst,
+                    fake_unify, FinalInstPrime, _Detism,
+                    ModuleInfo0, ModuleInfo1)
+            ->
+                FinalInst = FinalInstPrime,
+                ModuleInfo = ModuleInfo1,
+                !RI ^ ri_module_info := ModuleInfo
+            ;
+                unexpected(this_file, "recompute_instmap_delta_unify: "
+                    ++ "abstractly_unify_inst failed")
+            )
+        ;
+            % It wasn't in the instmap_delta, so the inst didn't change.
+            FinalInst = InitialInst,
+            ModuleInfo = ModuleInfo0
         ),
         UniModeToRhsMode =
             (pred(UMode::in, Mode::out) is det :-
@@ -1468,7 +1487,7 @@
             set.member(Var, NonLocals),
             OldInstMapDelta = goal_info_get_instmap_delta(GoalInfo),
             \+ instmap_delta_search_var(OldInstMapDelta, Var, _),
-            MaybeInst = cons_id_to_shared_inst(ModuleInfo, ConsId,
+            MaybeInst = cons_id_to_shared_inst(ModuleInfo0, ConsId,
                 length(Args)),
             MaybeInst = yes(Inst)
         ->
cvs diff: Diffing compiler/notes
cvs diff: Diffing debian
cvs diff: Diffing debian/patches
cvs diff: Diffing deep_profiler
cvs diff: Diffing deep_profiler/notes
cvs diff: Diffing doc
Index: doc/user_guide.texi
===================================================================
RCS file: /home/mercury/mercury1/repository/mercury/doc/user_guide.texi,v
retrieving revision 1.581
diff -u -b -r1.581 user_guide.texi
--- doc/user_guide.texi	20 Jan 2009 06:24:04 -0000	1.581
+++ doc/user_guide.texi	27 Jan 2009 10:19:51 -0000
@@ -6844,7 +6844,7 @@
 A - argument passing information,
 B - mode constraint information,
 C - clause information,
-D - instmap deltas of goals,
+D - instmap deltas of goals (meaningful only with i),
 E - deep profiling information,
 G - compile-time garbage collection information,
 I - imported predicates,
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/concurrency
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_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/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
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/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/diff
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/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
Index: tests/hard_coded/Mmakefile
===================================================================
RCS file: /home/mercury/mercury1/repository/tests/hard_coded/Mmakefile,v
retrieving revision 1.362
diff -u -b -r1.362 Mmakefile
--- tests/hard_coded/Mmakefile	2 Jan 2009 03:12:09 -0000	1.362
+++ tests/hard_coded/Mmakefile	27 Jan 2009 14:47:25 -0000
@@ -180,6 +180,7 @@
 	promise_equivalent_clauses \
 	promise_equivalent_solutions_test \
 	pure_mutable \
+	puzzle_detism_bug \
 	qual_adv_test \
 	qual_basic_test \
 	qual_is_test \
@@ -495,8 +496,6 @@
 # XXX compare_rep_array doesn't work because MR_COMPARE_BY_RTTI is
 #     not yet implemented for arrays.
 #
-# XXX puzzle_detism_bug exposes a bug in mode analysis
-#
 # XXX we fail some of the commented-out tests in write_binary
 
 # The following tests are passed only in some grades.
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