Fix Deferral in first position throws exception #1446 (#1474)

hazelgrove · Jan 25, 2025 · c33b369 · c33b369
2 parents 5272a50 + 12f279a
commit c33b369
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/src/haz3lcore/statics/Elaborator.re b/src/haz3lcore/statics/Elaborator.re
@@ -329,12 +329,12 @@ let rec elaborate = (m: Statics.Map.t, uexp: Exp.t): (DHExp.t, Typ.t) => {
       let (args', tys) = List.map(elaborate(m), args) |> ListUtil.unzip;
       let (tyf1, tyf2) = Typ.matched_arrow(ctx, tyf);
       let ty_fargs = Typ.matched_prod(ctx, List.length(args), tyf1);
-      let f'' =
-        fresh_cast(
-          f',
-          tyf,
-          Arrow(Prod(ty_fargs) |> Typ.temp, tyf2) |> Typ.temp,
-        );
+      let prod_args =
+        switch (ty_fargs) {
+        | [ty] => ty
+        | _ => Prod(ty_fargs) |> Typ.temp
+        };
+      let f'' = fresh_cast(f', tyf, Arrow(prod_args, tyf2) |> Typ.temp);
       let args'' = ListUtil.map3(fresh_cast, args', tys, ty_fargs);
       let remaining_args =
         List.filter(