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