From db12e64845ceebd6f8f705368cd6d7814b564fdf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 12 Feb 2026 13:34:49 +0100 Subject: [PATCH] chore: mitigate noncomputable section issues in the code generator (#12453) This is a mitigation for the fact that the upfront noncomputable checker currently doesn't error out early enough in certain situations so we violate invariants later on. --- src/Lean/Compiler/LCNF/InferBorrow.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Compiler/LCNF/InferBorrow.lean b/src/Lean/Compiler/LCNF/InferBorrow.lean index 7a2a53a3d8..ec1a25eb7e 100644 --- a/src/Lean/Compiler/LCNF/InferBorrow.lean +++ b/src/Lean/Compiler/LCNF/InferBorrow.lean @@ -213,7 +213,7 @@ where | some ps => return ps | none => let .decl fn := k | unreachable! - let some sig ← getImpureSignature? fn | unreachable! + let some sig ← getImpureSignature? fn | throwError "Failed to find LCNF signature for {fn}" return sig.params /-- For each ps[i], if ps[i] is owned, then mark args[i] as owned. -/