Make Equality Check Pattern Asciptions (#2059)

Author: cyrus-

src/language/term/Equality.re

@@ -403,6 +403,7 @@ let equality =
       (alphas_exp: Alphas.t, alphas_typ: Alphas.t, p1: Pat.t, p2: Pat.t)
       : option(Alphas.t) => {
     let pat' = pat(alphas_exp, alphas_typ);
+    let typ' = typ(alphas_exp, alphas_typ);
     let any' = any(alphas_exp, alphas_typ);
     switch (p1 |> Grammar.Annotated.term_of, p2 |> Grammar.Annotated.term_of) {
     // Wrappers when ignored: unwrap.
@@ -414,7 +415,12 @@ let equality =
     // Wrappers otherwise: compare.
     | (Parens(x), Parens(y)) => pat'(x, y)
     | (Parens(_), _) => None
-    | (Asc(x, _), Asc(y, _)) => pat'(x, y)
+    | (Asc(x, t1), Asc(y, t2)) =>
+      if (typ'(t1, t2)) {
+        pat'(x, y);
+      } else {
+        None;
+      }
     | (Asc(_), _) => None
 
     // Variables: special case depending on alpha equivalence.

test/Test_Equality.re

@@ -20,5 +20,35 @@ let tests = (
         );
       },
     ),
+    test_case(
+      "forall type inequality",
+      `Quick,
+      () => {
+        let forall_string =
+          Exp.forall(
+          Pat.asc(Pat.var("x"), Typ.string()),
+          Exp.bin_op(
+              Operators.Poly(Operators.Equals),
+              Exp.var("x"),
+              Exp.var("x"),
+            ),
+          );
+        let forall_int =
+          Exp.forall(
+            Pat.asc(Pat.var("x"), Typ.int()),
+            Exp.bin_op(
+              Operators.Poly(Operators.Equals),
+              Exp.var("x"),
+              Exp.var("x"),
+            ),
+          );
+        check(
+          bool,
+          "forall x : String -> x == x !== forall x : Int -> x == x",
+          false,
+          Equality.semantic.exp(forall_string, forall_int),
+        );
+      },
+    ),
   ],
 );