From 15e6ad70928e7d7a353ec4009e7c2200f1e4c320 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Mon, 29 Apr 2024 16:58:57 +0200
Subject: [PATCH] feat(engine/fstar): do not mark refinement type with `unfold`

---
 engine/backends/fstar/fstar_backend.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
index ec4d247d4..bf239c330 100644
--- a/engine/backends/fstar/fstar_backend.ml
+++ b/engine/backends/fstar/fstar_backend.ml
@@ -914,18 +914,21 @@ struct
           @@ F.AST.PatVar
                (F.id @@ U.Concrete_ident_view.to_definition_name name, None, [])
         in
-        let ty =
+        let ty, quals =
           (* Adds a refinement if a refinement attribute is detected *)
           match Attrs.associated_expr ~keep_last_args:1 Ensures e.attrs with
           | Some { e = Closure { params = [ binder ]; body; _ }; _ } ->
               let binder, _ =
                 U.Expect.pbinding_simple binder |> Option.value_exn
               in
-              F.mk_refined (plocal_ident_str binder) (pty e.span ty) (fun ~x ->
-                  pexpr body)
-          | _ -> pty e.span ty
+              let ty =
+                F.mk_refined (plocal_ident_str binder) (pty e.span ty)
+                  (fun ~x -> pexpr body)
+              in
+              (ty, [])
+          | _ -> (pty e.span ty, [ F.AST.Unfold_for_unification_and_vcgen ])
         in
-        F.decls ~quals:[ F.AST.Unfold_for_unification_and_vcgen ]
+        F.decls ~quals
         @@ F.AST.TopLevelLet
              ( NoLetQualifier,
                [