From 3f076fc83647cdbae05f6c8be07be75ded2dff86 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 14 Oct 2022 08:41:59 -0700
Subject: [PATCH] perf: missing annotations and helper instances

---
 src/Lean/Compiler/LCNF/CompilerM.lean  | 3 +++
 src/Lean/Compiler/LCNF/Simp/SimpM.lean | 3 +++
 src/Lean/CoreM.lean                    | 1 +
 src/Lean/Meta/Basic.lean               | 1 +
 4 files changed, 8 insertions(+)

diff --git a/src/Lean/Compiler/LCNF/CompilerM.lean b/src/Lean/Compiler/LCNF/CompilerM.lean
index c9d5ce2109..03426d29d2 100644
--- a/src/Lean/Compiler/LCNF/CompilerM.lean
+++ b/src/Lean/Compiler/LCNF/CompilerM.lean
@@ -42,6 +42,9 @@ structure CompilerM.Context where
 
 abbrev CompilerM := ReaderT CompilerM.Context $ StateRefT CompilerM.State CoreM
 
+@[alwaysInline]
+instance : Monad CompilerM := let i := inferInstanceAs (Monad CompilerM); { pure := i.pure, bind := i.bind }
+
 @[inline] def withPhase (phase : Phase) (x : CompilerM α) : CompilerM α :=
   withReader (fun ctx => { ctx with phase }) x
 
diff --git a/src/Lean/Compiler/LCNF/Simp/SimpM.lean b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
index e7a0a8e6cc..3200d13f23 100644
--- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean
+++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean
@@ -75,6 +75,9 @@ structure State where
 
 abbrev SimpM := ReaderT Context $ StateRefT State DiscrM
 
+@[alwaysInline]
+instance : Monad SimpM := let i := inferInstanceAs (Monad SimpM); { pure := i.pure, bind := i.bind }
+
 instance : MonadFVarSubst SimpM false where
   getSubst := return (← get).subst
 
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index ab84d1d1c1..735095ea80 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -76,6 +76,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`.
+@[alwaysInline]
 instance : Monad CoreM := let i := inferInstanceAs (Monad CoreM); { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (CoreM α) where
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 189736c17a..690b7324cb 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -300,6 +300,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`.
+@[alwaysInline]
 instance : Monad MetaM := let i := inferInstanceAs (Monad MetaM); { pure := i.pure, bind := i.bind }
 
 instance : Inhabited (MetaM α) where