From a6f4e9156effbea23106b31d81987c13ae501d79 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Sat, 15 Nov 2025 17:31:24 +0100
Subject: [PATCH] fix: avoid unknown free variables in match error message
 (#11190)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR avoids running into an “unknown free variable” when printing the
“Failed to compile pattern matching” error. Fixes #11186.
---
 src/Lean/Meta/Match/Match.lean | 17 ++++++------
 tests/lean/run/issue11186.lean | 51 ++++++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/issue11186.lean

diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 5601532bdf..3356a0d5fa 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -819,14 +819,15 @@ private def checkNextPatternTypes (p : Problem) : MetaM Unit := do
   | x::_ => withGoalOf p do
     for alt in p.alts do
       withRef alt.ref do
-        match alt.patterns with
-        | []   => return ()
-        | p::_ =>
-          let e ← p.toExpr
-          let xType ← inferType x
-          let eType ← inferType e
-          unless (← isDefEq xType eType) do
-            throwError "Type mismatch in pattern: Pattern{indentExpr e}\n{← mkHasTypeButIsExpectedMsg eType xType}"
+        withExistingLocalDecls alt.fvarDecls do
+          match alt.patterns with
+          | []   => return ()
+          | p::_ =>
+            let e ← p.toExpr
+            let xType ← inferType x
+            let eType ← inferType e
+            unless (← isDefEq xType eType) do
+              throwError "Type mismatch in pattern: Pattern{indentExpr e}\n{← mkHasTypeButIsExpectedMsg eType xType}"
 
 private def List.moveToFront [Inhabited α] (as : List α) (i : Nat) : List α :=
   let rec loop : (as : List α) → (i : Nat) → α × List α
diff --git a/tests/lean/run/issue11186.lean b/tests/lean/run/issue11186.lean
new file mode 100644
index 0000000000..63fa92e989
--- /dev/null
+++ b/tests/lean/run/issue11186.lean
@@ -0,0 +1,51 @@
+-- set_option trace.Meta.Match.match true
+-- set_option trace.Meta.Match.debug true
+
+/--
+error: Failed to compile pattern matching: Stuck at
+  remaining variables: [x✝:(String)]
+  alternatives:
+    [bytes✝:(ByteArray),
+     isValidUTF8✝:(bytes✝.IsValidUTF8)] |- [(String.ofByteArray bytes✝ isValidUTF8✝)] => h_1 bytes✝ isValidUTF8✝
+    [] |- ["Eek"] => h_2 ()
+    [x✝:(String)] |- [x✝] => h_3 x✝
+  examples:_
+-/
+#guard_msgs in
+def stringMatch : Option Nat :=
+  match "Bad" with
+  | String.ofByteArray _ _ => some 1
+  | "Eek" => some 2
+  | _ => none -- used to be: unknown free variable `_fvar.149`
+
+/--
+error: Failed to compile pattern matching: Stuck at
+  remaining variables: [x✝:(Char)]
+  alternatives:
+    [valid✝:(UInt32.isValidChar 5)] |- [(Char.mk 5 valid✝)] => h_1 valid✝
+    [] |- ['A'] => h_2 ()
+    [x✝:(Char)] |- [x✝] => h_3 x✝
+  examples:_
+-/
+#guard_msgs in
+def charMatch :=
+  match 'X' with
+  | Char.mk 5 _ => some 1
+  | 'A' => some 2
+  | _ => none -- used to be: unknown free variable `_fvar.836`
+
+/--
+error: Failed to compile pattern matching: Stuck at
+  remaining variables: [x✝:(UInt8)]
+  alternatives:
+    [] |- [(UInt8.ofBitVec (BitVec.ofFin 3))] => h_1 ()
+    [] |- [5] => h_2 ()
+    [x✝:(UInt8)] |- [x✝] => h_3 x✝
+  examples:_
+-/
+#guard_msgs in
+def uInt8Match :=
+  match (5: UInt8) with
+  | UInt8.ofBitVec (BitVec.ofFin 3) => some 1
+  | 5 => some 2
+  | _ => none -- used to be: unknown free variable `_fvar.1026`