From 2db0a98b7ca7c724298ce4e75aec972b1e201597 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 18 Dec 2025 10:31:48 +0100
Subject: [PATCH] fix: internalize all arguments to Quot.lift during LCNF
 conversion (#11729)

This PR internalizes all arguments of Quot.lift during LCNF conversion,
preventing panics in certain
non trivial programs that use quotients.

Fixes #11719.
---
 src/Lean/Compiler/LCNF/ToLCNF.lean |  6 ++---
 tests/lean/run/11719.lean          | 39 ++++++++++++++++++++++++++++++
 2 files changed, 42 insertions(+), 3 deletions(-)
 create mode 100644 tests/lean/run/11719.lean

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index e23cca919d..ad4d50c986 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -613,12 +613,12 @@ where
     let arity := 6
     etaIfUnderApplied e arity do
       let mut args := e.getAppArgs
-      let α := args[0]!
-      let r := args[1]!
+      let α ← visitAppArg args[0]!
+      let r ← visitAppArg args[1]!
       let f ← visitAppArg args[3]!
       let q ← visitAppArg args[5]!
       let .const _ [u, _] := e.getAppFn | unreachable!
-      let invq ← mkAuxLetDecl (.const ``Quot.lcInv [u] #[.type α, .type r, q])
+      let invq ← mkAuxLetDecl (.const ``Quot.lcInv [u] #[α, r, q])
       match f with
       | .erased => return .erased
       | .type _ => unreachable!
diff --git a/tests/lean/run/11719.lean b/tests/lean/run/11719.lean
new file mode 100644
index 0000000000..04d7539d5d
--- /dev/null
+++ b/tests/lean/run/11719.lean
@@ -0,0 +1,39 @@
+/-! Regression test for Quot handling during LCNF conversion -/
+
+namespace A
+
+variable (α : Type)
+
+def space : Type :=
+  Quot (α := α × α) fun ⟨_, _⟩ ⟨_, _⟩ ↦ True
+
+def subspace := { x : space α // True }
+
+/--
+warning: declaration uses `sorry`
+---
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+def foo : subspace α → subspace α :=
+  fun ⟨x, h⟩ ↦ x.lift sorry sorry
+
+end A
+
+namespace B
+
+def space : Type :=
+  Quot (α := Bool × Bool) fun ⟨_, _⟩ ⟨_, _⟩ ↦ True
+
+def subspace := { x : space // True }
+
+/--
+warning: declaration uses `sorry`
+---
+warning: declaration uses `sorry`
+-/
+#guard_msgs in
+def foo : subspace → subspace :=
+  fun ⟨x, _⟩ ↦ x.lift sorry sorry
+
+end B