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

@@ -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!

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