From 376c541e9a4570ac118d1b200bb9bd012f5749c3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 15 Oct 2022 08:50:30 -0700
Subject: [PATCH] feat: do not generate code for declarations that will be
 specialized

---
 src/Lean/Compiler/LCNF/ToMono.lean  | 13 ++++++++++++-
 tests/lean/shadow.lean.expected.out |  2 +-
 2 files changed, 13 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean
index a987a87694..32c7b60b98 100644
--- a/src/Lean/Compiler/LCNF/ToMono.lean
+++ b/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
 
diff --git a/tests/lean/shadow.lean.expected.out b/tests/lean/shadow.lean.expected.out
index f98bfc46c2..b75cd4a6e3 100644
--- a/tests/lean/shadow.lean.expected.out
+++ b/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