feat: do not generate code for declarations that will be specialized

src/Lean/Compiler/LCNF/ToMono.lean

@@ -152,7 +152,18 @@ where
 
 def toMono : Pass where
   name     := `toMono
-  run      := fun decls => decls.mapM (·.toMono)
+  run      := fun decls => do
+    let decls ← decls.filterM fun decl => do
+      if hasLocalInst decl.type then
+        /-
+        Declaration is a "template" for the code specialization pass.
+        So, we should delete it before going to next phase.
+        -/
+        decl.erase
+        return false
+      else
+        return true
+    decls.mapM (·.toMono)
   phase    := .base
   phaseOut := .mono
 

tests/lean/shadow.lean.expected.out

@@ -19,7 +19,7 @@ inst✝ inst : α
 shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
 context:
 α : Type u_1
-inst.82 : Inhabited α
+inst.71 : Inhabited α
 inst inst : α
 ⊢ {β δ : Type} → α → β → δ → α × β × δ
 shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder