From 573ca7dcadef1ba93a98fc447692fd9cc9372007 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 27 Oct 2020 12:40:43 -0700
Subject: [PATCH] chore: remove workarounds

---
 src/Lean/Elab/Command.lean   | 2 +-
 src/Lean/MetavarContext.lean | 2 +-
 tests/lean/run/stateRef.lean | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 12a3c046be..59b4488fe1 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -50,7 +50,7 @@ structure Context :=
   (currMacroScope : MacroScope := firstFrontendMacroScope)
   (ref            : Syntax := Syntax.missing)
 
-abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State (EIO ε)
+abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
 abbrev Linter := Syntax → CommandElabM Unit
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index fdf9e4cd17..e3ac69ac60 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -594,7 +594,7 @@ def instantiateMVars (mctx : MetavarContext) (e : Expr) : Expr × MetavarContext
   if !e.hasMVar then
     (e, mctx)
   else
-    let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext (ST ω)) Expr :=
+    let instantiate {ω} (e : Expr) : (MonadCacheT Expr Expr $ StateRefT MetavarContext $ ST ω) Expr :=
       instantiateExprMVars e
     runST fun _ => instantiate e $.run $.run mctx
 
diff --git a/tests/lean/run/stateRef.lean b/tests/lean/run/stateRef.lean
index fdaae76ea0..30d6e9d105 100644
--- a/tests/lean/run/stateRef.lean
+++ b/tests/lean/run/stateRef.lean
@@ -39,7 +39,7 @@ instance monadState.hasGetAt (β : Type) (v : β) (α : Type) (m : Type → Type
 
 export HasGetAt (getAt)
 
-abbrev M := StateRefT (Label 0 Nat) (StateRefT (Label 1 Nat) (StateRefT (Label 2 Nat) IO))
+abbrev M := StateRefT (Label 0 Nat) $ StateRefT (Label 1 Nat) $ StateRefT (Label 2 Nat) IO
 
 def f4 : M Nat := do
 let a0 : Nat ← getAt 0
@@ -52,7 +52,7 @@ pure (a0 + a1 + a2)
 
 #eval f4.run' ⟨10⟩ $.run' ⟨20⟩ $.run' ⟨30⟩
 
-abbrev S (ω : Type) := StateRefT Nat (StateRefT String (ST ω))
+abbrev S (ω : Type) := StateRefT Nat $ StateRefT String $ ST ω
 
 def f5 {ω} : S ω Unit := do
 let s ← getThe String