Fix IH not appearing with pattern cast mismatch

Author: Negabinary

src/language/proof/MatchExp.re

@@ -71,7 +71,10 @@ let rec match_exp =
             ctx,
           ),
         )
-      | Some(e) => Equality.semantic.exp(e, exp) ? Some(ctx) : None
+      | Some(e) =>
+        print_endline("ASSIGNED");
+        print_endline("assigned exp: " ++ Exp.show(e));
+        Equality.ignoring_ascriptions.exp(e, exp) ? Some(ctx) : None;
       }
     };
   | (Var(x), Var(y)) when are_alpha_equiv(alphas, x, y) => Some(ctx)
@@ -265,6 +268,8 @@ and match_pat = (pat_r: Pat.t, pat: Pat.t): option(alphas) =>
   | (Projector(_, p1), _) => match_pat(p1, pat)
   | (_, Parens(p2))
   | (_, Projector(_, p2)) => match_pat(pat_r, p2)
+  | (Asc(p1, _), _) => match_pat(p1, pat)
+  | (_, Asc(p2, _)) => match_pat(pat_r, p2)
   | (Invalid(x), Invalid(y)) when x == y => Some([])
   | (Invalid(_), _) => None
   | (EmptyHole, EmptyHole) => Some([])
@@ -319,11 +324,6 @@ and match_pat = (pat_r: Pat.t, pat: Pat.t): option(alphas) =>
     let* alphas2 = match_pat(x2, y2);
     Some(alphas1 @ alphas2);
   | (Ap(_, _), _) => None
-  | (Asc(x, t1), Asc(y, t2)) =>
-    let* alphas1 = match_pat(x, y);
-    let* () = match_typ(t1, t2);
-    Some(alphas1);
-  | (Asc(_, _), _) => None
   | (Label(l1), Label(l2)) when l1 == l2 => Some([])
   | (Label(_), _) => None
   | (TupLabel({term: ExplicitNonlabel, _}, pat_r), _) =>

src/language/proof/ProofHacks.re

@@ -32,7 +32,7 @@ let exp_idx = (e1: Exp.t, e2: Exp.t) => {
         (cont, exp) =>
           if (Exp.rep_id(exp) == Exp.rep_id(e1)) {
             raise(Found(exp));
-          } else if (DHExp.fast_equal(exp, e1)) {
+          } else if (Equality.ignoring_ascriptions.exp(exp, e1)) {
             n := n^ + 1;
             exp;
           } else {
@@ -58,7 +58,7 @@ let nth_exp = (e1: Exp.t, n: int, e2: Exp.t) => {
     Exp.map_term(
       ~f_exp=
         (cont, exp) =>
-          if (DHExp.fast_equal(exp, e1)) {
+          if (Equality.ignoring_ascriptions.exp(exp, e1)) {
             if (count^ == n) {
               raise(Found(exp));
             } else {
@@ -349,7 +349,7 @@ let rec replace_exp =
         switch (term) {
         /* Note[Matt]: We are not currently checking alpha-equivalence here because it's unlikely
            to come up, but we could. */
-        | _ when Exp.fast_equal(exp, replace) =>
+        | _ when Equality.ignoring_ascriptions.exp(exp, replace) =>
           with_exp |> Exp.replace_all_ids
         /* Forms with binders: check if any bound variables are in the coctx,
            if so, stop. */

src/language/term/Equality.re

@@ -776,3 +776,9 @@ let semantic_settings = {
 };
 
 let semantic = equality(semantic_settings);
+
+let ignoring_ascriptions =
+  equality({
+    ...semantic_settings,
+    ignore_ascriptions: true,
+  });

src/util/StringUtil.re

@@ -180,14 +180,5 @@ let subseq_search = (s: string, sub: string): bool => {
       );
     };
 
-  print_endline(
-    "Subseq search: "
-    ++ sub
-    ++ " in "
-    ++ s
-    ++ "returns"
-    ++ string_of_bool(search(0, 0)),
-  );
-
   search(0, 0);
 };