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

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