[m-rev.] for review: Fix problems with higher-order inst matching with polymorphic modes.

[Peter Wang]

On Mon, 18 Aug 2014 16:06:37 +1000, Peter Wang <novalazy at gmail.com> wrote:
> XXX contravariance_poly is broken but that may be due to a weakness
> elsewhere

This fixes the last known problem exposed by this patch series.

----

Fix problems with higher-order inst matching with polymorphic modes.

These changes allow the compiler to accept the contravariance_poly.m
test case, which requires that higher order pred insts are contravariant
in the initial argument insts.  Previously the compiler would have
rejected the test case, if not for the hack in inst_matches_final
that allows a ground inst to match a bound inst.

compiler/inst_match.m:
	pred_inst_argmodes_matches set the mode cs_reverse when matching
	initial insts, which causes handle_inst_var_subs to swap the
	insts for the inst var substitution calculation.  The insts are
	swapped back for inst matching, but cs_reverse remained.
	A recursive call to match two insts would swap the insts
	*again*, to the wrong order.  The fix is to invert cs_reverse to
	cs_forward when the insts are swapped back for matching.

	In pred_inst_argmodes_matches apply the incrementally calculated
	inst var substitution before matching.

compiler/modecheck_util.m:
	Make handle_implied_mode use
	inst_matches_initial_no_implied_modes_sub.  The non-sub variant
	does not compute inst var substitutions and fails where the
	higher-order argument inst has an inst variable, as in
	contravariance_poly.m, and handle_implied_mode incorrectly
	deduces that the call is to an implied mode.
---
 compiler/inst_match.m     | 43 +++++++++++++++++++++++++++++++++----------
 compiler/modecheck_util.m |  4 ++--
 2 files changed, 35 insertions(+), 12 deletions(-)

diff --git a/compiler/inst_match.m b/compiler/inst_match.m
index 7253d1b..f3c0ace 100644
--- a/compiler/inst_match.m
+++ b/compiler/inst_match.m
@@ -342,6 +342,7 @@
 :- import_module mdbcomp.prim_data.
 :- import_module mdbcomp.sym_name.
 :- import_module parse_tree.prog_data.
+:- import_module parse_tree.prog_mode.
 :- import_module parse_tree.prog_type.
 
 :- import_module bool.
@@ -438,7 +439,7 @@ inst_expand_and_remove_constrained_inst_vars(ModuleInfo, !Inst) :-
             % insts of higher order pred insts.
 
     ;       cs_none.
-            % Do not calculate inst var substitions.
+            % Do not calculate inst var substitution.
 
 :- func init_inst_match_info(module_info, maybe(inst_var_sub),
     calculate_sub, uniqueness_comparison, bool, trust_final_insts) =
@@ -464,19 +465,23 @@ swap_sub(P, !Info) :-
     P(!Info),
     !Info ^ imi_calculate_sub := CalculateSub.
 
+:- pred unswap(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.
+
+unswap(P, InstA, InstB, Type, !Info) :-
+    % Swap the arguments *and* undo swap_sub.
+    CalculateSub = !.Info ^ imi_calculate_sub,
+    !Info ^ imi_calculate_sub := swap_calculate_sub(CalculateSub),
+    P(InstB, InstA, Type, !Info),
+    !Info ^ imi_calculate_sub := CalculateSub.
+
 :- func swap_calculate_sub(calculate_sub) = calculate_sub.
 
 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,
-    inst_match_info::in, inst_match_info::out) is semidet.
-
-swap_args(P, InstA, InstB, Type, !Info) :-
-    P(InstB, InstA, Type, !Info).
-
 %-----------------------------------------------------------------------------%
 
 :- pred handle_inst_var_subs(
@@ -493,7 +498,9 @@ handle_inst_var_subs(Recurse, Continue, InstA, InstB, Type, !Info) :-
             Type, !Info)
     ;
         CalculateSub = cs_reverse,
-        handle_inst_var_subs_2(swap_args(Recurse), swap_args(Continue),
+        % Calculate the inst var substitution with arguments swapped,
+        % but swap back for inst matching.
+        handle_inst_var_subs_2(unswap(Recurse), unswap(Continue),
             InstB, InstA, Type, !Info)
     ;
         CalculateSub = cs_none,
@@ -937,12 +944,28 @@ pred_inst_argmodes_matches([], [], [], !Info).
 pred_inst_argmodes_matches([ModeA | ModeAs], [ModeB | ModeBs],
         [MaybeType | MaybeTypes], !Info) :-
     ModuleInfo = !.Info ^ imi_module_info,
-    mode_get_insts(ModuleInfo, ModeA, InitialA, FinalA),
+    mode_get_insts(ModuleInfo, ModeA, InitialA, FinalA0),
     mode_get_insts(ModuleInfo, ModeB, InitialB, FinalB),
+    % inst_matches_final_mt should probably just accept cs_reverse directly.
     swap_sub(inst_matches_final_mt(InitialB, InitialA, MaybeType), !Info),
+    % Apply the substitution computed so far (it may be necessary for InitialA
+    % as well).
+    maybe_apply_substitution(!.Info, FinalA0, FinalA),
     inst_matches_final_mt(FinalA, FinalB, MaybeType, !Info),
     pred_inst_argmodes_matches(ModeAs, ModeBs, MaybeTypes, !Info).
 
+:- pred maybe_apply_substitution(inst_match_info::in,
+    mer_inst::in, mer_inst::out) is det.
+
+maybe_apply_substitution(Info, Inst0, Inst) :-
+    (
+        Info ^ imi_maybe_sub = yes(Subst),
+        inst_apply_substitution(Subst, Inst0, Inst)
+    ;
+        Info ^ imi_maybe_sub = no,
+        Inst = Inst0
+    ).
+
 %-----------------------------------------------------------------------------%
 
     % Determine what kind of uniqueness comparison we are doing and then do it.
diff --git a/compiler/modecheck_util.m b/compiler/modecheck_util.m
index dbd760b..0dfe44f 100644
--- a/compiler/modecheck_util.m
+++ b/compiler/modecheck_util.m
@@ -780,8 +780,8 @@ handle_implied_mode(Var0, VarInst0, InitialInst0, Var, !ExtraGoals,
         % If the initial inst of the variable matches_final the initial inst
         % specified in the pred's mode declaration, then it's not a call
         % to an implied mode, it's an exact match with a genuine mode.
-        inst_matches_initial_no_implied_modes(VarInst1, InitialInst,
-            VarType, ModuleInfo0)
+        inst_matches_initial_no_implied_modes_sub(VarInst1, InitialInst,
+            VarType, ModuleInfo0, _ModuleInfo, map.init, _Sub)
     ->
         Var = Var0
     ;
-- 
1.8.4