perf: eliminate cases with all branches unreachable (#11525)

This PR makes the LCNF simplifier eliminate cases where all alts are
`.unreach` to just an `.unreach`.
  an `.unreach`

We considered dropping a cases in a situation like this but decided
against it because it might hinder reuse.
```
def test x : Bool :=
  cases x : Bool
  | Except.error a.1 =>
    ⊥
  | Except.ok a.2 =>
    let _x.3 := true;
    return _x.3
```

Author: hargoniX

src/Lean/Compiler/LCNF/Simp/Main.lean

@@ -336,6 +336,18 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do
               params.forM (eraseParam ·)
               markSimplified
               return k
+        if alts.all (·.getCode matches .unreach ..) then
+          alts.forM (liftM <| ·.getParams.forM eraseParam)
+          markSimplified
+          return .unreach resultType
+        /-
+        We considered handling a case where we drop a cases if it only has one non-unreachable
+        branch and doesn't rely on the params of that branch here. However, this has the potential
+        to hinder reuse in later passes as we loose information about the shape of a variable. We
+        might be able to reintroduce this at a later point if we track this information different
+        from cases.
+        -/
+
         markUsedFVar discr
         return code.updateCases! resultType discr alts
 end