diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean
index 4b5f10ce7a..06ab57e956 100644
--- a/library/init/lean/elaborator/basic.lean
+++ b/library/init/lean/elaborator/basic.lean
@@ -40,6 +40,8 @@ end ElabException
 
 abbrev Elab := ReaderT ElabContext (EState ElabException ElabState)
 
+instance str2ElabException : HasCoe String ElabException := ⟨ElabException.other⟩
+
 abbrev TermElab    := SyntaxNode → Elab Expr
 abbrev CommandElab := SyntaxNode → Elab Unit
 
@@ -207,7 +209,7 @@ do pos ← getPos stx;
 
 def logErrorAndThrow {α : Type} (stx : Syntax) (errorMsg : String) : Elab α :=
 do logError stx errorMsg;
-   throw (ElabException.other errorMsg)
+   throw errorMsg
 
 def elabTerm (stx : Syntax) : Elab Expr :=
 stx.ifNode
@@ -218,7 +220,7 @@ stx.ifNode
     match tables.find k with
     | some elab => elab n
     | none      => logErrorAndThrow stx ("term elaborator failed, no support for syntax '" ++ toString k ++ "'"))
-  (fun _ => throw $ ElabException.other "term elaborator failed, unexpected syntax")
+  (fun _ => throw "term elaborator failed, unexpected syntax")
 
 def elabCommand (stx : Syntax) : Elab Unit :=
 stx.ifNode
diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index 8cb5cb3f63..dfee88254f 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -99,9 +99,9 @@ def isIdent {α} : Syntax α → Bool
 | (ident _ _ _ _) := true
 | _               := false
 
-def getIdentVal {α} : Syntax α → Option Name
-| (ident _ _ val _) := val
-| _                 := none
+@[inline] def getIdentVal {α ε m} [MonadExcept ε m] [HasLiftT String ε] [Monad m] : Syntax α → m Name
+| (ident _ _ val _) := pure val
+| _                 := throw (coe "ill-formed syntax")
 
 def isOfKind {α} : Syntax α → SyntaxNodeKind → Bool
 | (node kind _) k := k == kind