feat: LCNF local context dead variable checker

This commit also fixes a few local declaration leaks.

src/Lean/Compiler/LCNF/Check.lean

@@ -180,4 +180,41 @@ end Check
 def Decl.check (decl : Decl) : CompilerM Unit := do
   Check.run do Check.checkFunDeclCore decl.name decl.type decl.params decl.value
 
+/--
+Check whether every local declaration in the local context is used in one of given `decls`.
+-/
+partial def checkDeadLocalDecls (decls : Array Decl) : CompilerM Unit := do
+  let (_, s) := visitDecls decls |>.run {}
+  (← get).lctx.localDecls.forM fun fvarId decl =>
+    unless s.contains fvarId do
+      throwError "LCNF local context contains unused local variable declaration `{decl.userName}`"
+where
+  visitFVar (fvarId : FVarId) : StateM FVarIdHashSet Unit :=
+    modify (·.insert fvarId)
+
+  visitParam (param : Param) : StateM FVarIdHashSet Unit := do
+    visitFVar param.fvarId
+
+  visitParams (params : Array Param) : StateM FVarIdHashSet Unit := do
+    params.forM visitParam
+
+  visitCode (code : Code) : StateM FVarIdHashSet Unit := do
+    match code with
+    | .jmp .. | .return .. | .unreach .. => return ()
+    | .let decl k => visitFVar decl.fvarId; visitCode k
+    | .fun decl k | .jp decl k =>
+      visitFVar decl.fvarId; visitParams decl.params; visitCode decl.value
+      visitCode k
+    | .cases c => c.alts.forM fun alt => do
+      match alt with
+      | .default k => visitCode k
+      | .alt _ ps k => visitParams ps; visitCode k
+
+  visitDecl (decl : Decl) : StateM FVarIdHashSet Unit := do
+    visitParams decl.params
+    visitCode decl.value
+
+  visitDecls (decls : Array Decl) : StateM FVarIdHashSet Unit :=
+    decls.forM visitDecl
+
 end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/CompilerM.lean

@@ -48,6 +48,9 @@ def getFunDecl (fvarId : FVarId) : CompilerM FunDecl := do
 def eraseFVar (fvarId : FVarId) (recursive := true) : CompilerM Unit := do
   modifyLCtx fun lctx => lctx.erase fvarId recursive
 
+def eraseFVarsAt (code : Code) : CompilerM Unit := do
+  modifyLCtx fun lctx => lctx.eraseFVarsAt code
+
 /--
 A free variable substitution.
 We use these substitutions when inlining definitions and "internalizing" LCNF code into `CompilerM`.

src/Lean/Compiler/LCNF/LCtx.lean

@@ -50,12 +50,22 @@ where
   goParams (params : Array Param) (lctx : LCtx) : LCtx :=
     params.foldl (init := lctx) fun lctx p => lctx.erase p.fvarId
 
+  goAlts (alts : Array Alt) (lctx : LCtx) : LCtx :=
+    alts.foldl (init := lctx) fun lctx alt =>
+      match alt with
+      | .default k => go k lctx
+      | .alt _ ps k => go k <| goParams ps lctx
+
   go (code : Code) (lctx : LCtx) : LCtx :=
     match code with
     | .let decl k => go k <| lctx.eraseLocal decl.fvarId
     | .jp decl k | .fun decl k => go k <| lctx.erase decl.fvarId
+    | .cases c => goAlts c.alts lctx
     | _ => lctx
 
+def LCtx.eraseFVarsAt (c : Code) (lctx : LCtx) : LCtx :=
+  LCtx.erase.go c lctx
+
 /--
 Convert a LCNF local context into a regular Lean local context.
 -/

src/Lean/Compiler/LCNF/Main.lean

@@ -49,6 +49,7 @@ def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
         Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl decl}"
       if compiler.check.get (← getOptions) then
         decl.check
+  checkDeadLocalDecls decls
 
 namespace PassManager
 

src/Lean/Compiler/LCNF/ToLCNF.lean

@@ -33,7 +33,7 @@ inductive Element where
   | fun (decl : FunDecl)
   | let (decl : LetDecl)
   | cases (fvarId : FVarId) (cases : Cases)
-  | unreach
+  | unreach (fvarId : FVarId)
   deriving Inhabited
 
 def seqToCode (seq : Array Element) (e : Expr) : CompilerM Code := do
@@ -50,7 +50,14 @@ where
       | .jp decl => go seq (i - 1) (.jp decl c)
       | .fun decl => go seq (i - 1) (.fun decl c)
       | .let decl => go seq (i - 1) (.let decl c)
-      | .unreach => return .unreach (← c.inferType)
+      | .unreach _ =>
+        let type ← c.inferType
+        eraseFVarsAt c
+        seq[:i].forM fun
+          | .let decl | .jp decl | .fun decl => eraseFVar decl.fvarId
+          | .cases _ cs => eraseFVarsAt (.cases cs)
+          | .unreach fvarId => eraseFVar fvarId
+        return .unreach type
       | .cases fvarId cases =>
         if let .return fvarId' := c then
           if fvarId == fvarId' then
@@ -93,8 +100,9 @@ def pushElement (elem : Element) : M Unit := do
   modify fun s => { s with seq := s.seq.push elem }
 
 def mkUnreachable (type : Expr) : M Expr := do
-  pushElement .unreach
-  return .fvar (← mkAuxParam type).fvarId
+  let p ← mkAuxParam type
+  pushElement (.unreach p.fvarId)
+  return .fvar p.fvarId
 
 def mkAuxLetDecl (e : Expr) (prefixName := `_x) : M Expr := do
   if e.isFVar then