[m-rev.] diff: Revert a fix for constrained polymorphic modes.

[Peter Wang]

Commit 338b5cb98e8abd320aac6d3619f8ab98f773c846 changed a call in
handle_inst_var_subs_2, essentially from
	Recurse(InstA, SubInstB)
to
	Recurse(InstA, abstractly_unify_inst(InstA, SubInstB))

Unfortunately, it results in infinite recursion on some cases.

compiler/inst_match.m:
	Revert the change to handle_inst_var_subs_2.

tests/EXPECT_FAIL_TESTS.all_grades:
	Expect constrained_poly_insts2 to fail now.

tests/invalid/constrained_poly_insts3.err_exp:
tests/invalid/constrained_poly_insts3.m:
tests/invalid/constrained_poly_insts4.err_exp:
tests/invalid/constrained_poly_insts4.m:
	Add test cases.

diff --git a/compiler/inst_match.m b/compiler/inst_match.m
index 494df76..5cb8247 100644
--- a/compiler/inst_match.m
+++ b/compiler/inst_match.m
@@ -495,20 +495,35 @@ handle_inst_var_subs(Recurse, Continue, InstA, InstB, Type, !Info) :-
 
 handle_inst_var_subs_2(Recurse, Continue, InstA, InstB, Type, !Info) :-
     ( InstB = constrained_inst_vars(InstVarsB, SubInstB) ->
-        % Add the substitution InstVarsB => InstA `glb` SubInstB
-        % (see get_subst_inst in dmo's thesis, page 78).
-        %
+        % InstB is a constrained_inst_var with upper bound SubInstB.
+        % We need to check that InstA matches_initial SubInstB and add the
+        % appropriate inst_var substitution.
+        Recurse(InstA, SubInstB, Type, !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, SubInstB, fake_unify,
+            Inst, _Det, ModuleInfo0, ModuleInfo),
+        !Info ^ imi_module_info := ModuleInfo,
+        update_inst_var_sub(InstVarsB, Inst, Type, !Info)
+
+        % This accepts more code but some cases cause infinite recursion.
+        /*
+        % Add the substitution InstVarsB => InstA `glb` SubInstB
+        % (see get_subst_inst in dmo's thesis, page 78).
         ModuleInfo0 = !.Info ^ imi_module_info,
         abstractly_unify_inst(is_dead, InstA, SubInstB, fake_unify,
             Inst, _Det, ModuleInfo0, ModuleInfo),
         !Info ^ imi_module_info := ModuleInfo,
         update_inst_var_sub(InstVarsB, Inst, Type, !Info),
-
         % Check that InstA matches InstB after applying the substitution
         % to InstB.
         Recurse(InstA, Inst, Type, !Info)
+        */
     ; InstA = constrained_inst_vars(_InstVarsA, SubInstA) ->
         Recurse(SubInstA, InstB, Type, !Info)
     ;
diff --git a/tests/EXPECT_FAIL_TESTS.all_grades b/tests/EXPECT_FAIL_TESTS.all_grades
index febbde7..ebcf18d 100644
--- a/tests/EXPECT_FAIL_TESTS.all_grades
+++ b/tests/EXPECT_FAIL_TESTS.all_grades
@@ -4,3 +4,4 @@ valid/bug85
 valid/constraint_prop_bug
 valid/csharp_hello
 valid/ho_and_type_spec_bug2
+invalid/constrained_poly_insts2
diff --git a/tests/invalid/constrained_poly_insts3.err_exp b/tests/invalid/constrained_poly_insts3.err_exp
new file mode 100644
index 0000000..fb6d04f
--- /dev/null
+++ b/tests/invalid/constrained_poly_insts3.err_exp
@@ -0,0 +1,9 @@
+constrained_poly_insts3.m:020: In clause for `p1(in((I =< ground)), out((I =<
+constrained_poly_insts3.m:020:   ground)))':
+constrained_poly_insts3.m:020:   mode error: argument 2 became too
+constrained_poly_insts3.m:020:   instantiated.
+constrained_poly_insts3.m:020:   Final instantiatedness of `Y' was
+constrained_poly_insts3.m:020:   `bound((list.[]) ; list.'[|]'(ground,
+constrained_poly_insts3.m:020:   bound((list.[]) ; list.'[|]'(ground, ...))))',
+constrained_poly_insts3.m:020:   expected final instantiatedness was `(I =<
+constrained_poly_insts3.m:020:   ground)'.
diff --git a/tests/invalid/constrained_poly_insts3.m b/tests/invalid/constrained_poly_insts3.m
new file mode 100644
index 0000000..81118e2
--- /dev/null
+++ b/tests/invalid/constrained_poly_insts3.m
@@ -0,0 +1,28 @@
+%-----------------------------------------------------------------------------%
+
+:- module constrained_poly_insts3.
+:- interface.
+
+:- import_module list.
+
+:- type thing == list(list(int)).
+:- inst thing == list_skel(ground).
+
+:- pred p1(thing, thing).
+:- mode p1(in(I), out(I)) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+p1(X, Y) :-
+    q(X, Y).
+
+:- pred q(thing, thing).
+:- mode q(in(thing), out(thing)) is det.
+
+q(X, X).
+
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sts=4 sw=4 et
diff --git a/tests/invalid/constrained_poly_insts4.err_exp b/tests/invalid/constrained_poly_insts4.err_exp
new file mode 100644
index 0000000..f12d05f
--- /dev/null
+++ b/tests/invalid/constrained_poly_insts4.err_exp
@@ -0,0 +1,10 @@
+constrained_poly_insts4.m:020: In clause for `p2(in((I =<
+constrained_poly_insts4.m:020:   (constrained_poly_insts4.thing))), out((I =<
+constrained_poly_insts4.m:020:   (constrained_poly_insts4.thing))))':
+constrained_poly_insts4.m:020:   mode error: argument 2 became too
+constrained_poly_insts4.m:020:   instantiated.
+constrained_poly_insts4.m:020:   Final instantiatedness of `Y' was
+constrained_poly_insts4.m:020:   `bound((list.[]) ; list.'[|]'(ground,
+constrained_poly_insts4.m:020:   bound((list.[]) ; list.'[|]'(ground, ...))))',
+constrained_poly_insts4.m:020:   expected final instantiatedness was `(I =<
+constrained_poly_insts4.m:020:   bound((list.[]) ; list.'[|]'(ground, ...)))'.
diff --git a/tests/invalid/constrained_poly_insts4.m b/tests/invalid/constrained_poly_insts4.m
new file mode 100644
index 0000000..af0c2bf
--- /dev/null
+++ b/tests/invalid/constrained_poly_insts4.m
@@ -0,0 +1,28 @@
+%-----------------------------------------------------------------------------%
+
+:- module constrained_poly_insts4.
+:- interface.
+
+:- import_module list.
+
+:- type thing == list(list(int)).
+:- inst thing == list_skel(ground).
+
+:- pred p2(thing, thing).
+:- mode p2(in(I =< thing), out(I =< thing)) is det.
+
+%-----------------------------------------------------------------------------%
+%-----------------------------------------------------------------------------%
+
+:- implementation.
+
+p2(X, Y) :-
+    q(X, Y).
+
+:- pred q(thing, thing).
+:- mode q(in(thing), out(thing)) is det.
+
+q(X, X).
+
+%-----------------------------------------------------------------------------%
+% vim: ft=mercury ts=4 sts=4 sw=4 et