[m-rev.] for review: Fix check of existentially typed args in subtype definitions.

[Peter Wang]

We did not correctly enforce the rule that requires a one-to-one mapping
between the existentially quantified type variables for subtype
constructor, and the variables for the same constructor in the supertype
definition, e.g. this was inadvertently allowed:

    :- type pear2
	--->	some [T, U] pear(T, U).

    :- type pear1 =< pear2
	--->	some [A] pear(A, A).  % should be rejected

compiler/add_type.m:
    Use a bimap to represent the correspondence between existentially
    quantified type variables in the subtype and supertype.

    Improve check_is_subtype_var_var with an extra check and comments.

tests/invalid/subtype_exist_vars.err_exp:
tests/invalid/subtype_exist_vars.m:
    Extend test case.

(diff with -b)

diff --git a/compiler/add_type.m b/compiler/add_type.m
index f65050d55..3cc665754 100644
--- a/compiler/add_type.m
+++ b/compiler/add_type.m
@@ -2,7 +2,7 @@
 % vim: ft=mercury ts=4 sw=4 et
 %---------------------------------------------------------------------------%
 % Copyright (C) 1993-2011 The University of Melbourne.
-% Copyright (C) 2013-2021 The Mercury team.
+% Copyright (C) 2013-2024 The Mercury team.
 % This file may only be copied under the terms of the GNU General
 % Public License - see the file COPYING in the Mercury distribution.
 %---------------------------------------------------------------------------%
@@ -75,6 +75,7 @@
 :- import_module parse_tree.prog_type_subst.
 :- import_module parse_tree.prog_type_test.
 
+:- import_module bimap.
 :- import_module bool.
 :- import_module edit_seq.
 :- import_module int.
@@ -1699,7 +1700,7 @@ check_subtype_ctor(TypeTable, TVarSet, TypeStatus, Ctor, SuperCtor,
         check_subtype_ctor_arg(TypeTable, TVarSet, TypeStatus,
             CtorSymName, MaybeExistConstraints, MaybeSuperExistConstraints),
         Args, SuperArgs,
-        1, _, map.init, ExistQVarsMapping,
+        1, _, bimap.init, ExistQVarsMapping,
         did_not_find_invalid_type, FoundInvalidType, !Specs),
     (
         FoundInvalidType = did_not_find_invalid_type,
@@ -1732,7 +1733,7 @@ check_subtype_ctor(TypeTable, TVarSet, TypeStatus, Ctor, SuperCtor,
     % A map from existential type variable in the supertype constructor
     % to an existential type variable in the subtype constructor.
     %
-:- type existq_tvar_mapping == map(tvar, tvar).
+:- type existq_tvar_mapping == bimap(tvar, tvar).
 
 :- pred check_subtype_ctor_arg(type_table::in, tvarset::in, type_status::in,
     sym_name::in,
@@ -1890,16 +1891,25 @@ check_is_subtype(TypeTable, TVarSet0, OrigTypeStatus, TypeA, TypeB,
 check_is_subtype_var_var(VarA, VarB,
         MaybeExistConstraintsA, MaybeExistConstraintsB, !ExistQVarsMapping) :-
     ( if VarA = VarB then
-        true
-    else if map.search(!.ExistQVarsMapping, VarB, VarB1) then
-        VarB1 = VarA
+        % Double check that VarA (and VarB) are universally quantified.
+        is_univ_quantified(MaybeExistConstraintsA, VarA)
     else
+        % VarA and VarB should both be existentially quantified.
+        % There must be a one-to-one correspondence between existentially
+        % quantified type variables in the subtype and the supertype.
+        ( if bimap.forward_search(!.ExistQVarsMapping, VarB, PrevVar) then
+            % VarB was seen already; it should be mapped to VarA.
+            PrevVar = VarA
+        else
+            % VarB was not seen yet.
             MaybeExistConstraintsA = exist_constraints(ExistConstraintsA),
             MaybeExistConstraintsB = exist_constraints(ExistConstraintsB),
             ExistConstraintsA = cons_exist_constraints(_ExistQVarsA,
                 _ConstraintsA, UnconstrainedExistQVarsA, ConstrainedExistQVarsA),
             ExistConstraintsB = cons_exist_constraints(_ExistQVarsB,
                 _ConstraintsB, UnconstrainedExistQVarsB, ConstrainedExistQVarsB),
+            % VarA and VarB should both be unconstrained, or both be
+            % constrained.
             (
                 list.contains(UnconstrainedExistQVarsA, VarA),
                 list.contains(UnconstrainedExistQVarsB, VarB)
@@ -1907,7 +1917,22 @@ check_is_subtype_var_var(VarA, VarB,
                 list.contains(ConstrainedExistQVarsA, VarA),
                 list.contains(ConstrainedExistQVarsB, VarB)
             ),
-        map.insert(VarB, VarA, !ExistQVarsMapping)
+            % Record the correspondence between VarB and VarA.
+            % This fails if another type variable was mapped to VarA already.
+            bimap.insert(VarB, VarA, !ExistQVarsMapping)
+        )
+    ).
+
+:- pred is_univ_quantified(maybe_cons_exist_constraints::in, tvar::in)
+    is semidet.
+
+is_univ_quantified(MaybeExistConstraints, TVar) :-
+    (
+        MaybeExistConstraints = no_exist_constraints
+    ;
+        MaybeExistConstraints = exist_constraints(ExistConstraints),
+        ExistQVars = ExistConstraints ^ cons_existq_tvars,
+        not list.contains(ExistQVars, TVar)
     ).
 
 :- pred check_corresponding_args_are_subtype(type_table::in, tvarset::in,
@@ -1984,7 +2009,8 @@ check_subtype_ctor_exist_constraints(CtorSymNameArity,
         !FoundInvalidType, !Specs) :-
     ExistConstraints = cons_exist_constraints(_, Constraints, _, _),
     SuperExistConstraints = cons_exist_constraints(_, SuperConstraints0, _, _),
-    apply_variable_renaming_to_prog_constraint_list(ExistQVarsMapping,
+    ExistQVarsRenaming = bimap.forward_map(ExistQVarsMapping),
+    apply_variable_renaming_to_prog_constraint_list(ExistQVarsRenaming,
         SuperConstraints0, SuperConstraints),
     list.sort(Constraints, SortedConstraints),
     list.sort(SuperConstraints, SortedSuperConstraints),
diff --git a/tests/invalid/subtype_exist_vars.err_exp b/tests/invalid/subtype_exist_vars.err_exp
index fc4f73a8a..562efaf92 100644
--- a/tests/invalid/subtype_exist_vars.err_exp
+++ b/tests/invalid/subtype_exist_vars.err_exp
@@ -1,12 +1,15 @@
-subtype_exist_vars.m:019: Error: the first argument of `orange' has a type,
-subtype_exist_vars.m:019:   `T', which is not a subtype of the corresponding
-subtype_exist_vars.m:019:   argument type `O' in the supertype.
-subtype_exist_vars.m:022: Error: the first argument of `apple' has a type, `T',
-subtype_exist_vars.m:022:   which is not a subtype of the corresponding
-subtype_exist_vars.m:022:   argument type `int' in the supertype.
-subtype_exist_vars.m:028: Error: the second argument of `lemon' has a type,
-subtype_exist_vars.m:028:   `B', which is not a subtype of the corresponding
-subtype_exist_vars.m:028:   argument type `T' in the supertype.
-subtype_exist_vars.m:031: Error: the second argument of `lemon' has a type,
-subtype_exist_vars.m:031:   `A', which is not a subtype of the corresponding
-subtype_exist_vars.m:031:   argument type `T' in the supertype.
+subtype_exist_vars.m:020: Error: the first argument of `orange' has a type,
+subtype_exist_vars.m:020:   `T', which is not a subtype of the corresponding
+subtype_exist_vars.m:020:   argument type `O' in the supertype.
+subtype_exist_vars.m:023: Error: the first argument of `apple' has a type, `T',
+subtype_exist_vars.m:023:   which is not a subtype of the corresponding
+subtype_exist_vars.m:023:   argument type `int' in the supertype.
+subtype_exist_vars.m:029: Error: the second argument of `lemon' has a type,
+subtype_exist_vars.m:029:   `B', which is not a subtype of the corresponding
+subtype_exist_vars.m:029:   argument type `T' in the supertype.
+subtype_exist_vars.m:032: Error: the second argument of `lemon' has a type,
+subtype_exist_vars.m:032:   `A', which is not a subtype of the corresponding
+subtype_exist_vars.m:032:   argument type `T' in the supertype.
+subtype_exist_vars.m:035: Error: the second argument of `pear' has a type, `A',
+subtype_exist_vars.m:035:   which is not a subtype of the corresponding
+subtype_exist_vars.m:035:   argument type `U' in the supertype.
diff --git a/tests/invalid/subtype_exist_vars.m b/tests/invalid/subtype_exist_vars.m
index 43e2560ea..0f0084a0e 100644
--- a/tests/invalid/subtype_exist_vars.m
+++ b/tests/invalid/subtype_exist_vars.m
@@ -10,7 +10,8 @@
 :- type fruit(A)
     --->    apple(A)
     ;       some [O] orange(O)
-    ;       some [T, U] lemon(T, T, foo(U)).
+    ;       some [T, U] lemon(T, T, foo(U))
+    ;       some [T, U] pear(T, U).
 
 :- type foo(T)
     --->    foo(T).
@@ -29,3 +30,6 @@
 
 :- type exist_vars_mismatch2 =< fruit
     --->    some [A, B] lemon(B, A, foo(A)).
+
+:- type exist_vars_mismatch3 =< fruit
+    --->    some [A] pear(A, A).
-- 
2.44.0