Fix stack overflow

hazelgrove · Oct 15, 2024 · e018126 · e018126
1 parent 01f84c5
commit e018126
Show file tree

Hide file tree

Showing 2 changed files with 72 additions and 16 deletions.
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
@@ -819,29 +819,59 @@ and uexp_to_info_map =
     switch (Typ.weak_head_normalize(ctx, ty).term) {
     | Prod([{term: TupLabel({term: Label(l1), _}, ana_ty), _}]) =>
       let (e, m) = go(~mode=Mode.Syn, uexp, m);
+
       switch (Typ.weak_head_normalize(ctx, e.ty).term) {
       | _ when Typ.is_consistent(ctx, ana_ty, e.ty) =>
-        uexp_to_info_map(
-          ~ctx,
-          ~mode=Mode.Ana(ty),
-          ~is_in_filter,
-          ~ancestors,
+        let (e, m) =
+          uexp_to_info_map(
+            ~ctx,
+            ~mode=Mode.Ana(ana_ty),
+            ~is_in_filter,
+            ~ancestors,
+            uexp,
+            m,
+          );
+        let fake_uexp =
           Tuple([TupLabel(Label(l1) |> Exp.fresh, uexp) |> Exp.fresh])
-          |> Exp.fresh,
-          m,
-        )
+          |> Exp.fresh;
+        let info =
+          Info.derived_exp(
+            ~uexp=fake_uexp,
+            ~ctx,
+            ~mode,
+            ~ancestors,
+            ~self=Common(Just(ty)),
+            ~co_ctx=e.co_ctx,
+          );
+
+        (info, add_info(fake_uexp.ids, InfoExp(info), m));
       | Prod([{term: TupLabel({term: Label(l2), _}, _), _}]) when l1 == l2 =>
         default_case()
       | _ =>
-        uexp_to_info_map(
-          ~ctx,
-          ~mode=Mode.Ana(ty),
-          ~is_in_filter,
-          ~ancestors,
+        // TODO Deduplicate
+        let (e, m) =
+          uexp_to_info_map(
+            ~ctx,
+            ~mode=Mode.Ana(ana_ty),
+            ~is_in_filter,
+            ~ancestors,
+            uexp,
+            m,
+          );
+        let fake_uexp =
           Tuple([TupLabel(Label(l1) |> Exp.fresh, uexp) |> Exp.fresh])
-          |> Exp.fresh,
-          m,
-        )
+          |> Exp.fresh;
+        let info =
+          Info.derived_exp(
+            ~uexp=fake_uexp,
+            ~ctx,
+            ~mode,
+            ~ancestors,
+            ~self=Common(Just(ty)),
+            ~co_ctx=e.co_ctx,
+          );
+
+        (info, add_info(fake_uexp.ids, InfoExp(info), m));
       };
     | _ => default_case()
     }

diff --git a/test/Test_Statics.re b/test/Test_Statics.re
@@ -584,4 +584,30 @@ let tests =
       )
       |> Exp.fresh,
     ),
+    fully_consistent_typecheck(
+      "Reconstructed labeled tuple without values",
+      {|let x : (l=|},
+      Some(Unknown(Internal) |> Typ.fresh),
+      Let(
+        Cast(
+          Var("x") |> Pat.fresh,
+          Parens(
+            Prod([
+              TupLabel(
+                Label("l") |> Typ.fresh,
+                Unknown(Hole(EmptyHole)) |> Typ.fresh,
+              )
+              |> Typ.fresh,
+            ])
+            |> Typ.fresh,
+          )
+          |> Typ.fresh,
+          Unknown(Internal) |> Typ.fresh,
+        )
+        |> Pat.fresh,
+        EmptyHole |> Exp.fresh,
+        EmptyHole |> Exp.fresh,
+      )
+      |> Exp.fresh,
+    ),
   ];