From b3d706262bad3be2812931477527754229ea35fe Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 24 Sep 2026 04:32:22 +0000
Subject: [PATCH] Rel: quasi-pattern solutions keep RHS uvars abstracted over
 the pattern vars

When a non-pattern flex term `?u e1..en` was solved against a rigid RHS by
the quasi-pattern rule, the uvars in the RHS were restricted to ctx(?u)
alone, so they could no longer mention the variables the solution
abstracts over. Restrict them over those binders instead, as the pattern
case already does (skipping uvars whose context is already included in
ctx(?u)).

Also make restrict_ctx drop abstracted binders whose sort mentions a
variable that is not in scope (e.g. one bound to a non-variable argument
of the quasi-pattern), which would otherwise yield an ill-scoped arrow.

Fixes #4587.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 pulse/test/bug-reports/Bug4587.fst         | 50 ++++++++++++++++++++++
 src/typechecker/FStarC.TypeChecker.Rel.fst | 25 ++++++++++-
 2 files changed, 74 insertions(+), 1 deletion(-)
 create mode 100644 pulse/test/bug-reports/Bug4587.fst

diff --git a/pulse/test/bug-reports/Bug4587.fst b/pulse/test/bug-reports/Bug4587.fst
new file mode 100644
index 00000000000..ddbb784326f
--- /dev/null
+++ b/pulse/test/bug-reports/Bug4587.fst
@@ -0,0 +1,50 @@
+module Bug4587
+
+(* FStarLang/FStar#4587: when the unifier solves a non-pattern flex term by
+   the quasi-pattern rule, the uvars on the RHS must stay abstracted over the
+   pattern variables (here, the existential [_v7] opened by [havoc]). *)
+#lang-pulse
+open Pulse
+module R = Pulse.Lib.Reference
+
+let eta_expanded (#[@@@mkey] t: Type0) (x: t) : slprop = emp
+
+[@@pulse_eager_intro]
+ghost fn eta_expanded_leaf (#t: Type0) (x: t)
+  ensures eta_expanded x
+{ fold eta_expanded x }
+
+[@@pulse_eager_intro]
+ghost fn eta_expanded_unit ()
+  ensures eta_expanded ()
+{ fold eta_expanded () }
+
+[@@pulse_eager_intro]
+ghost fn eta_expanded_erased (#t: Type0) (x: erased t)
+  requires eta_expanded (reveal x)
+  ensures eta_expanded x
+{ unfold eta_expanded (reveal x); fold eta_expanded x }
+
+[@@pulse_eager_intro]
+ghost fn eta_expanded_pair (#t #s: Type0) (x: t) (y: s)
+  requires eta_expanded x
+  requires eta_expanded y
+  ensures eta_expanded (x, y)
+{ unfold eta_expanded x; unfold eta_expanded y; fold eta_expanded (x, y) }
+
+assume val call (x: R.ref int) (w: erased (unit & int))
+  : stt unit (eta_expanded w ** (let (_, v) = reveal w in R.pts_to x v))
+             (fun _ -> R.pts_to x (snd (reveal w)))
+
+assume val havoc (n: int) (x: R.ref int) :
+  stt unit (R.pts_to x 0) (fun _ -> exists* v. R.pts_to x v)
+
+fn test (a: R.ref int)
+  requires R.pts_to a 0
+  ensures exists* v. R.pts_to a v
+{
+  let mut n = 0;
+  let n1 = !n;
+  havoc n1 a;
+  call a _;
+}
diff --git a/src/typechecker/FStarC.TypeChecker.Rel.fst b/src/typechecker/FStarC.TypeChecker.Rel.fst
index 6dd38980be7..a34ef772ac9 100644
--- a/src/typechecker/FStarC.TypeChecker.Rel.fst
+++ b/src/typechecker/FStarC.TypeChecker.Rel.fst
@@ -1261,6 +1261,21 @@ let restrict_ctx env (tgt:ctx_uvar) (bs:binders) (src:ctx_uvar) wl : ML worklist
     let bs = bs |> List.filter (fun ({binder_bv=bv1}) ->
     (src.ctx_uvar_binders |> List.existsb (fun ({binder_bv=bv2}) -> S.bv_eq bv1 bv2)) &&  //binder exists in G_t
     (not (pfx |> List.existsb (fun ({binder_bv=bv2}) -> S.bv_eq bv1 bv2)))) in  //but not in the maximal prefix
+    (* Also drop any binder whose sort mentions a variable that is neither in
+       the maximal prefix nor an earlier kept binder: abstracting over it would
+       produce an ill-scoped arrow type. *)
+    let bs =
+      let _, kept =
+        List.fold_left
+          (fun (scope, kept) (b:binder) ->
+            if subset (Free.names b.binder_bv.sort) scope
+            then add b.binder_bv scope, b::kept
+            else scope, kept)
+          (binders_as_bv_set pfx, [])
+          bs
+      in
+      List.rev kept
+    in
 
   if Nil? bs then aux (U.ctx_uvar_typ src) (fun src' -> src')  //no abstraction over bs
   else begin
@@ -3037,7 +3052,15 @@ let rec solve_t_flex_rigid_eq (orig:prob) (wl:worklist) (lhs:(flex_t & (subst_ts
                let fvs_rhs = Free.names rhs in
                if not (subset fvs_rhs fvs_lhs)
                then Inl ("quasi-pattern, free names on the RHS are not included in the LHS"), wl
-               else Inr (mk_solution env lhs bs rhs), restrict_all_uvars env ctx_u [] uvars wl
+               (* Restrict the RHS uvars *over* bs (as in the pattern case), so
+                  that they can still depend on the variables that
+                  the solution abstracts over. Uvars whose context is already
+                  included in the LHS's context need no restriction. *)
+               else
+                 let ctx_lhs = binders_as_bv_set ctx_u.ctx_uvar_binders in
+                 let uvars = uvars |> List.filter (fun (src:ctx_uvar) ->
+                   not (subset (binders_as_bv_set src.ctx_uvar_binders) ctx_lhs)) in
+                 Inr (mk_solution env lhs bs rhs), restrict_all_uvars env ctx_u bs uvars wl
     in
 
     (*