Skip to content

Commit

Permalink
fix: don't filter out local instances in LCNF toMono pass (#6664)
Browse files Browse the repository at this point in the history
This PR changes the toMono pass to longer filter out type class
instances, because they may actually be needed for later compilation.
  • Loading branch information
zwarich authored Jan 17, 2025
1 parent 35a4da2 commit 7f0ae22
Showing 1 changed file with 1 addition and 12 deletions.
13 changes: 1 addition & 12 deletions src/Lean/Compiler/LCNF/ToMono.lean
Original file line number Diff line number Diff line change
Expand Up @@ -150,18 +150,7 @@ where

def toMono : Pass where
name := `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)
run := (·.mapM (·.toMono))
phase := .base
phaseOut := .mono

Expand Down

0 comments on commit 7f0ae22

Please sign in to comment.