From 0d7e76ea889bacbe8a55af77b2c5841445ae3f64 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 13 Apr 2026 11:27:25 +0200
Subject: [PATCH] fix: include `ignoreNoncomputable` in LCNF cache key (#13384)

This PR fixes a compiler panic when a structure constructor receives a
noncomputable instance as an instance-implicit argument.

The LCNF translation first visits the instance in an irrelevant position
(type parameter) where `ignoreNoncomputable` is `true`, caches the
result, and then reuses that cached entry in a relevant position,
bypassing `checkComputable`. Adding `ignoreNoncomputable` to the cache
key ensures the two contexts do not share cache entries.

Fixes #13371
---
 src/Lean/Compiler/LCNF/ToLCNF.lean | 19 ++++++++++++++++---
 tests/elab/13371.lean              | 13 +++++++++++++
 2 files changed, 29 insertions(+), 3 deletions(-)
 create mode 100644 tests/elab/13371.lean

diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean
index fb7d10e253..3c630d1b03 100644
--- a/src/Lean/Compiler/LCNF/ToLCNF.lean
+++ b/src/Lean/Compiler/LCNF/ToLCNF.lean
@@ -213,11 +213,22 @@ structure Context where
   -/
   expectedType : Option Expr
 
+/--
+Key for the LCNF translation cache. `ignoreNoncomputable` is part of the key
+because entries cached in irrelevant positions skip the `checkComputable`
+check and must not be reused in relevant positions.
+-/
+structure CacheKey where
+  expr : Expr
+  expectedType? : Option Expr
+  ignoreNoncomputable : Bool
+  deriving BEq, Hashable
+
 structure State where
   /-- Local context containing the original Lean types (not LCNF ones). -/
   lctx : LocalContext := {}
   /-- Cache from Lean regular expression to LCNF argument. -/
-  cache : PHashMap (Expr × Option Expr) (Arg .pure) := {}
+  cache : PHashMap CacheKey (Arg .pure) := {}
   /--
   Determines whether caching has been disabled due to finding a use of
   a constant marked with `never_extract`.
@@ -473,7 +484,9 @@ partial def toLCNF (e : Expr) (eType : Expr) : CompilerM (Code .pure) := do
 where
   visitCore (e : Expr) : M (Arg .pure) := withIncRecDepth do
     let eType? := (← read).expectedType
-    if let some arg := (← get).cache.find? (e, eType?) then
+    let ignoreNoncomputable := (← read).ignoreNoncomputable
+    let key : CacheKey := { expr := e, expectedType? := eType?, ignoreNoncomputable }
+    if let some arg := (← get).cache.find? key then
       return arg
     let r : Arg .pure ← match e with
       | .app ..      => visitApp e
@@ -485,7 +498,7 @@ where
       | .lit lit     => visitLit lit
       | .fvar fvarId => if (← get).toAny.contains fvarId then pure .erased else pure (.fvar fvarId)
       | .forallE .. | .mvar .. | .bvar .. | .sort ..  => unreachable!
-    modify fun s => if s.shouldCache then { s with cache := s.cache.insert (e, eType?) r } else s
+    modify fun s => if s.shouldCache then { s with cache := s.cache.insert key r } else s
     return r
 
   visit (e : Expr) : M (Arg .pure) := withIncRecDepth do
diff --git a/tests/elab/13371.lean b/tests/elab/13371.lean
new file mode 100644
index 0000000000..1cf8a038fe
--- /dev/null
+++ b/tests/elab/13371.lean
@@ -0,0 +1,13 @@
+-- Regression test for https://github.com/leanprover/lean4/issues/13371
+-- The LCNF cache must distinguish entries cached in irrelevant positions
+-- (where noncomputable uses are tolerated) from those in relevant positions.
+structure Hom [Inhabited Unit] where
+  toFun : Unit
+
+noncomputable instance inst : Inhabited Unit := ⟨Classical.choice ⟨()⟩⟩
+
+/--
+error: failed to compile definition, consider marking it as 'noncomputable' because it depends on 'inst', which is 'noncomputable'
+-/
+#guard_msgs in
+def test : Hom := ⟨default⟩