[m-rev.] for review: Fix overly-conservative inst matching exposed by the previous change.

[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

When matching a constrained inst variable A =< SubInstA on the LHS,
we matched SubInstA with the inst on the RHS.  We can improve the
precision by unifying the insts.

In contravariance_poly.m, in the term `q(p)' the final inst of the first
argument of p must match_final the final inst of the first argument of
the higher-order argument of q, where

:- mode p((list(I) >> nonempty(I)), (free >> nonempty(I))) is semidet.

:- mode q(pred((nonempty(bit) >> nonempty(bit)), (free >> list(bit)))
    is semidet) is semidet.

We did not substitute I = bit so this rightfully fails:

	nonempty(I =< ground) match_final nonempty(bit)

compiler/inst_match.m:
	Add the unification to handle_inst_var_subs_2.

compiler/prog_data.m:
	Improve wording of a comment.

tests/invalid/Mmakefile:
tests/invalid/contravariance_poly2.err_exp:
tests/invalid/contravariance_poly2.m:
	Add an invalid test case based on contravariance_poly.m.
---
 compiler/inst_match.m                      | 15 ++++++++++----
 compiler/prog_data.m                       |  4 ++--
 tests/invalid/Mmakefile                    |  1 +
 tests/invalid/contravariance_poly2.err_exp | 22 ++++++++++++++++++++
 tests/invalid/contravariance_poly2.m       | 32 ++++++++++++++++++++++++++++++
 5 files changed, 68 insertions(+), 6 deletions(-)
 create mode 100644 tests/invalid/contravariance_poly2.err_exp
 create mode 100644 tests/invalid/contravariance_poly2.m

diff --git a/compiler/inst_match.m b/compiler/inst_match.m
index c475ce5..88c4371 100644
--- a/compiler/inst_match.m
+++ b/compiler/inst_match.m
@@ -516,14 +516,21 @@ handle_inst_var_subs_2(Recurse, Continue, InstA, InstB, Type, !Info) :-
         % 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,
+        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)
-    ; InstA = constrained_inst_vars(_InstVarsA, SubInstA) ->
-        Recurse(SubInstA, InstB, Type, !Info)
+    ; InstA = constrained_inst_vars(InstVarsA, _SubInstA) ->
+        % InstA is a constrained_inst_var with upper bound SubInstA.
+        % Unify the insts improve upon SubInstA.
+        ModuleInfo0 = !.Info ^ imi_module_info,
+        abstractly_unify_inst(is_dead, InstA, InstB, fake_unify,
+            Inst, _Det, ModuleInfo0, ModuleInfo),
+        !Info ^ imi_module_info := ModuleInfo,
+        update_inst_var_sub(InstVarsA, Inst, Type, !Info),
+
+        Recurse(Inst, InstB, Type, !Info)
     ;
         Continue(InstA, InstB, Type, !Info)
     ).
diff --git a/compiler/prog_data.m b/compiler/prog_data.m
index a9f04f2..ad65010 100644
--- a/compiler/prog_data.m
+++ b/compiler/prog_data.m
@@ -2234,8 +2234,8 @@ get_type_kind(kinded_type(_, Kind)) = Kind.
 
     ;           constrained_inst_vars(set(inst_var), mer_inst)
                 % Constrained_inst_vars is a set of inst variables that are
-                % constrained to have the same uniqueness as and to match_final
-                % the specified inst.
+                % constrained to have the same uniqueness as the specified
+                % inst, and to match_final the specified inst.
 
     ;           defined_inst(inst_name)
                 % A defined_inst is possibly recursive inst whose value is
diff --git a/tests/invalid/Mmakefile b/tests/invalid/Mmakefile
index 6341235..7b06e04 100644
--- a/tests/invalid/Mmakefile
+++ b/tests/invalid/Mmakefile
@@ -74,6 +74,7 @@ SINGLEMODULE= \
 	constrained_poly_insts \
 	constraint_proof_bug_lib \
 	constructor_warning \
+	contravariance_poly2 \
 	cyclic_typeclass \
 	cyclic_typeclass_2 \
 	cyclic_typeclass_3 \
diff --git a/tests/invalid/contravariance_poly2.err_exp b/tests/invalid/contravariance_poly2.err_exp
new file mode 100644
index 0000000..ac01a46
--- /dev/null
+++ b/tests/invalid/contravariance_poly2.err_exp
@@ -0,0 +1,22 @@
+Error: file `contravariance_poly2.m' contains the wrong module.
+  Expected module `contravariance_poly2', found module `contravariance_poly22'.
+contravariance_poly2.m:001: Error: source file `contravariance_poly2.m'
+contravariance_poly2.m:001:   contains module named `contravariance_poly22'.
+contravariance_poly2.m:011: In clause for `main(di, uo)':
+contravariance_poly2.m:011:   in argument 1 of call to predicate
+contravariance_poly2.m:011:   `contravariance_poly22.q'/1:
+contravariance_poly2.m:011:   mode error: variable `V_8' has instantiatedness
+contravariance_poly2.m:011:   `/* unique */(pred(($typed_inst(list.list(int),
+contravariance_poly2.m:011:   list.list((V_1 =< ground))) >>
+contravariance_poly2.m:011:   $typed_inst(list.list(int), list.list((V_1 =<
+contravariance_poly2.m:011:   ground)))), (free >> $typed_inst(list.list(int),
+contravariance_poly2.m:011:   contravariance_poly22.nonempty((V_1 =<
+contravariance_poly2.m:011:   ground))))) is semidet)',
+contravariance_poly2.m:011:   expected instantiatedness was
+contravariance_poly2.m:011:   `(pred(($typed_inst(list.list(int),
+contravariance_poly2.m:011:   contravariance_poly22.nonempty((contravariance_poly22.bit)))
+contravariance_poly2.m:011:   >> $typed_inst(list.list(int),
+contravariance_poly2.m:011:   contravariance_poly22.nonempty((contravariance_poly22.bit)))),
+contravariance_poly2.m:011:   (free >> $typed_inst(list.list(int),
+contravariance_poly2.m:011:   list.list((contravariance_poly22.bit))))) is
+contravariance_poly2.m:011:   semidet)'.
diff --git a/tests/invalid/contravariance_poly2.m b/tests/invalid/contravariance_poly2.m
new file mode 100644
index 0000000..977ebd7
--- /dev/null
+++ b/tests/invalid/contravariance_poly2.m
@@ -0,0 +1,32 @@
+:- module contravariance_poly22.
+:- interface.
+:- import_module io.
+ 
+:- pred main(io__state::di, io__state::uo) is det.
+ 
+:- implementation.
+:- import_module list, bool.
+ 
+main -->
+	( { q(r) } ->
+		print("yes"), nl
+	;
+		print("no"), nl
+	).
+ 
+:- inst nonempty(I) ---> [I | list(I)].
+
+:- type intlist == list(int).
+:- inst bit == bound(0 ; 1).
+ 
+:- pred r(intlist, intlist).
+:- mode r((list(I) >> list(I)), (free >> nonempty(I))) is semidet.
+ 
+r([X], [X]).
+r([X,Y|Zs], [Y,X|Zs]).
+ 
+:- pred q(pred(intlist, intlist)).
+:- mode q(pred((nonempty(bit) >> nonempty(bit)), (free >> list(bit)))
+		is semidet) is semidet.
+ 
+q(P) :- P([1], L), L \= [].
-- 
1.8.4