From 16026e9edd5268317c32f993d3cc16cd830f1095 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 12 Aug 2021 21:09:09 +0200
Subject: [PATCH] perf: restore monad instance specialization hack

---
 src/Lean/CoreM.lean             | 2 +-
 src/Lean/Elab/Command.lean      | 2 +-
 src/Lean/Elab/Tactic/Basic.lean | 2 +-
 src/Lean/Elab/Term.lean         | 2 +-
 src/Lean/Meta/Basic.lean        | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 9af0a13f9b..9ebfa3f326 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -45,7 +45,7 @@ abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception)
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
-instance : Monad CoreM := { inferInstanceAs (Monad CoreM) with }
+instance : Monad CoreM := let i := inferInstanceAs (Monad CoreM); { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (CoreM α) where
   default := fun _ _ => throw arbitrary
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 56862a3ded..0882e24175 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -56,7 +56,7 @@ abbrev Linter := Syntax → CommandElabM Unit
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
-instance : Monad CommandElabM := { inferInstanceAs (Monad CommandElabM) with }
+instance : Monad CommandElabM := let i := inferInstanceAs (Monad CommandElabM); { pure := i.pure, bind := i.bind }
 
 def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
   env         := env
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 2fdd00d44b..c559c9d732 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -53,7 +53,7 @@ abbrev Tactic  := Syntax → TacticM Unit
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
-instance : Monad TacticM := { inferInstanceAs (Monad TacticM) with }
+instance : Monad TacticM := let i := inferInstanceAs (Monad TacticM); { pure := i.pure, bind := i.bind }
 
 def getGoals : TacticM (List MVarId) :=
   return (← get).goals
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index effc34879f..9cc0d302f9 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -181,7 +181,7 @@ abbrev TermElab  := Syntax → Option Expr → TermElabM Expr
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
-instance : Monad TermElabM := { inferInstanceAs (Monad TermElabM) with }
+instance : Monad TermElabM := let i := inferInstanceAs (Monad TermElabM); { pure := i.pure, bind := i.bind }
 
 open Meta
 
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 512e6a5be7..d27ca62a79 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -174,7 +174,7 @@ abbrev MetaM  := ReaderT Context $ StateRefT State CoreM
 
 -- Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
 -- whole monad stack at every use site. May eventually be covered by `deriving`.
-instance : Monad MetaM := { inferInstanceAs (Monad MetaM) with }
+instance : Monad MetaM := let i := inferInstanceAs (Monad MetaM); { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (MetaM α) where
   default := fun _ _ => arbitrary