From 7b36b9d8d3d3af4dd534551ba58b5a09154da949 Mon Sep 17 00:00:00 2001
From: Crazycolorz5 <Crazycolorz5@gmail.com>
Date: Sat, 20 Apr 2024 01:13:50 -0400
Subject: [PATCH 1/3] Change mode of the closing typefunap mold to be static,
 thus only allowing it to close.

---
 src/haz3lcore/lang/Form.re | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/haz3lcore/lang/Form.re b/src/haz3lcore/lang/Form.re
index 65a8dcd292..b400c97ed0 100644
--- a/src/haz3lcore/lang/Form.re
+++ b/src/haz3lcore/lang/Form.re
@@ -302,7 +302,10 @@ let forms: list((string, t)) = [
   ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))),
   ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))),
   ("ap_typ", mk(ii, ["(", ")"], mk_post(P.ap, Typ, [Typ]))),
-  ("ap_exp_typ", mk(ii, ["@<", ">"], mk_post(P.ap, Exp, [Typ]))),
+  (
+    "ap_exp_typ",
+    mk((Instant, Static), ["@<", ">"], mk_post(P.ap, Exp, [Typ])),
+  ),
   ("at_sign", mk_nul_infix("@", P.eqs)), // HACK: SUBSTRING REQ
   ("case", mk(ds, ["case", "end"], mk_op(Exp, [Rul]))),
   ("test", mk(ds, ["test", "end"], mk_op(Exp, [Exp]))),

From 2bc7dd022798e6071192873f63a579035de79799 Mon Sep 17 00:00:00 2001
From: Crazycolorz5 <Crazycolorz5@gmail.com>
Date: Sun, 28 Apr 2024 19:41:51 -0400
Subject: [PATCH 2/3] Make forall types be considered for recursion.

---
 src/haz3lcore/statics/Statics.re | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 7e7bb1952c..08518137e2 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -64,21 +64,23 @@ let map_m = (f, xs, m: Map.t) =>
 let add_info = (ids: list(Id.t), info: Info.t, m: Map.t): Map.t =>
   ids |> List.fold_left((m, id) => Id.Map.add(id, info, m), m);
 
+let rec is_arrow_like = (t: Typ.t) => {
+  switch (t) {
+  | Unknown(_) => true
+  | Arrow(_) => true
+  | Forall(_, t) => is_arrow_like(t)
+  | _ => false
+  };
+};
+
 let is_recursive = (ctx, p, def, syn: Typ.t) => {
   switch (Term.UPat.get_num_of_vars(p), Term.UExp.get_num_of_functions(def)) {
   | (Some(num_vars), Some(num_fns))
       when num_vars != 0 && num_vars == num_fns =>
     switch (Typ.normalize(ctx, syn)) {
-    | Unknown(_)
-    | Arrow(_) => num_vars == 1
     | Prod(syns) when List.length(syns) == num_vars =>
-      syns
-      |> List.for_all(
-           fun
-           | Typ.Unknown(_)
-           | Arrow(_) => true
-           | _ => false,
-         )
+      syns |> List.for_all(is_arrow_like)
+    | t when is_arrow_like(t) => num_vars == 1
     | _ => false
     }
   | _ => false

From 9249bfee86c36c0a0194fca6846f8775ec0f458b Mon Sep 17 00:00:00 2001
From: Matt Keenan <negabinary@gmail.com>
Date: Wed, 1 May 2024 15:49:38 -0400
Subject: [PATCH 3/3] Fix #1298

---
 src/haz3lcore/statics/Statics.re | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index 08518137e2..29f4c27ce9 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -239,6 +239,7 @@ and uexp_to_info_map =
       m,
     );
   | ListConcat(e1, e2) =>
+    let mode = Mode.of_list_concat(ctx, mode);
     let ids = List.map(Term.UExp.rep_id, [e1, e2]);
     let (e1, m) = go(~mode, e1, m);
     let (e2, m) = go(~mode, e2, m);