From 7b292090ceb97f67a648f2216f87d1f2186a1188 Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Thu, 17 Apr 2025 16:01:56 -0700 Subject: [PATCH] fix: restrict lifting outside of cases expressions on Decidable (#8009) This PR restricts lifting outside of cases expressions on values of a Decidable type, since we can't correctly represent the dependency on the erased proposition in the later stages of the compiler. --- src/Lean/Compiler/LCNF/PullLetDecls.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/Lean/Compiler/LCNF/PullLetDecls.lean b/src/Lean/Compiler/LCNF/PullLetDecls.lean index cb07a1bcfa..ec48511a69 100644 --- a/src/Lean/Compiler/LCNF/PullLetDecls.lean +++ b/src/Lean/Compiler/LCNF/PullLetDecls.lean @@ -69,9 +69,14 @@ mutual partial def pullDecls (code : Code) : PullM Code := do match code with | .cases c => - withCheckpoint do - let alts ← c.alts.mapMonoM pullAlt - return code.updateAlts! alts + -- At the present time, we can't correctly enforce the dependencies required for lifting + -- out of a cases expression on Decidable, so we disable this optimization. + if c.typeName == ``Decidable then + return code + else + withCheckpoint do + let alts ← c.alts.mapMonoM pullAlt + return code.updateAlts! alts | .let decl k => if (← shouldPull decl) then pullDecls k