diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index c5445241ef..1fa0cfaa12 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -39,7 +39,7 @@ structure CommandInfo where
 
 inductive CompletionInfo where
   | dot (termInfo : TermInfo) (field? : Option Syntax) (expectedType? : Option Expr)
-  | id (stx : Syntax) (lctx : LocalContext) (expectedType? : Option Expr)
+  | id (stx : Syntax) (id : Name) (danglingDot : Bool) (lctx : LocalContext) (expectedType? : Option Expr)
   | namespaceId (stx : Syntax)
   | option (stx : Syntax)
   | endSection (stx : Syntax) (scopeNames : List String)
@@ -161,7 +161,7 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
 def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
   match info with
   | CompletionInfo.dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
-  | CompletionInfo.id stx lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
+  | CompletionInfo.id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
   | _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
 
 def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index f9efbf05f4..fd6f4c1f32 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -103,7 +103,7 @@ structure Context where
   /-- Map from internal name to fvar -/
   sectionFVars       : NameMap Expr    := {}
   /-- Enable/disable implicit lambdas feature. -/
-  implicitLambda     : Bool             := true
+  implicitLambda     : Bool            := true
 
 /-- Saved context for postponed terms and tactics to be executed. -/
 structure SavedContext where
@@ -1243,20 +1243,34 @@ private def elabOptLevel (stx : Syntax) : TermElabM Level :=
 @[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ =>
   return mkSort (mkLevelSucc (← elabOptLevel stx[1]))
 
-@[builtinTermElab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
-  /-
-    `ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field".
-    If the identifier `ident`, the method `resolveName` adds a completion point for it using the given
+/-
+ the method `resolveName` adds a completion point for it using the given
     expected type. Thus, we propagate the expected type if `stx[0]` is an identifier.
     It doesn't "hurt" if the identifier can be resolved because the expected type is not used in this case.
     Recall that if the name resolution fails a synthetic sorry is returned.-/
-  let e ← elabTerm stx[0] (if stx[0].isIdent then expectedType? else none)
+
+@[builtinTermElab «pipeCompletion»] def elabPipeCompletion : TermElab := fun stx expectedType? => do
+  let e ← elabTerm stx[0] none
   unless e.isSorry do
     addDotCompletionInfo stx e expectedType?
   throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
 
-@[builtinTermElab «pipeCompletion»] def elabPipeCompletion : TermElab :=
-  elabCompletion
+@[builtinTermElab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
+  /- `ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field". -/
+  if stx[0].isIdent then
+    /- If we can elaborate the identifier successfully, we assume it a dot-completion. Otherwise, we treat it as
+       identifier completion with a dangling `.`.
+       Recall that the server falls back to identifier completion when dot-completion fails. -/
+    let s ← saveState
+    try
+      let e ← elabTerm stx[0] none
+      addDotCompletionInfo stx e expectedType?
+    catch _ =>
+      s.restore
+      addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) (← getLCtx) expectedType?
+    throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
+  else
+    elabPipeCompletion stx expectedType?
 
 @[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do
   let mvar ← mkFreshExprMVar expectedType?
@@ -1354,7 +1368,7 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
    let const ← mkConst constName explicitLevels
    return (const, projs) :: result
 
-def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none): TermElabM (List (Expr × List String)) := do
+def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
   try
     if let some (e, projs) ← resolveLocalName n then
       unless explicitLevels.isEmpty do
@@ -1369,7 +1383,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
       process preresolved
   catch ex =>
     if preresolved.isEmpty && explicitLevels.isEmpty then
-      addCompletionInfo <| CompletionInfo.id stx (← getLCtx) expectedType?
+      addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
     throw ex
 where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
   if candidates.isEmpty then
@@ -1377,6 +1391,8 @@ where process (candidates : List (Name × List String)) : TermElabM (List (Expr
       throwAutoBoundImplicitLocal n
     else
       throwError "unknown identifier '{Lean.mkConst n}'"
+  if preresolved.isEmpty && explicitLevels.isEmpty then
+    addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
   mkConsts candidates explicitLevels
 
 /--
diff --git a/src/Lean/Server/Completion.lean b/src/Lean/Server/Completion.lean
index 758fe8e5bb..1ff495962a 100644
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -55,7 +55,7 @@ private def isTypeApplicable (type : Expr) (expectedType? : Option Expr) : MetaM
       -- TODO take coercions into account
       -- We use `withReducible` to make sure we don't spend too much time unfolding definitions
       -- Alternative: use default and small number of heartbeats
-      withReducible <| isDefEq type expectedType
+      withReducible <| withoutModifyingState <| isDefEq type expectedType
   catch _ =>
     return false
 
@@ -98,19 +98,22 @@ private def matchAtomic (id: Name) (declName : Name) : Bool :=
 /--
   Return the auto-completion label if `id` can be auto completed using `declName` assuming namespace `ns` is open.
   This function only succeeds with atomic labels. BTW, it seems most clients only use the last part.
+
+  Remark: `danglingDot == true` when the completion point is an identifier followed by `.`.
 -/
-private def matchDecl? (ns : Name) (id : Name) (declName : Name) : Option Name :=
+private def matchDecl? (ns : Name) (id : Name) (danglingDot : Bool) (declName : Name) : Option Name :=
+  -- dbg_trace "{ns}, {id}, {declName}, {danglingDot}"
   if !ns.isPrefixOf declName then
     none
   else
     let declName := declName.replacePrefix ns Name.anonymous
-    if id.isPrefixOf declName then
+    if id.isPrefixOf declName && danglingDot then
       let declName := declName.replacePrefix id Name.anonymous
       if declName.isAtomic && !declName.isAnonymous then
         some declName
       else
         none
-    else
+    else if !danglingDot then
       match id, declName with
       | Name.str p₁ s₁ _, Name.str p₂ s₂ _ =>
         if p₁ == p₂ && s₁.isPrefixOf s₂ then
@@ -118,9 +121,11 @@ private def matchDecl? (ns : Name) (id : Name) (declName : Name) : Option Name :
         else
           none
       | _, _ => none
+    else
+      none
 
-private def idCompletionCore (ctx : ContextInfo) (stx : Syntax) (expectedType? : Option Expr) : M Unit := do
-  let id := stx.getId.eraseMacroScopes
+private def idCompletionCore (ctx : ContextInfo) (id : Name) (danglingDot : Bool) (expectedType? : Option Expr) : M Unit := do
+  let id := id.eraseMacroScopes
   -- dbg_trace ">> id {id} : {expectedType?}"
   if id.isAtomic then
     -- search for matches in the local context
@@ -132,7 +137,7 @@ private def idCompletionCore (ctx : ContextInfo) (stx : Syntax) (expectedType? :
   env.constants.forM fun declName c => do
     unless (← isBlackListed declName) do
       let matchUsingNamespace (ns : Name): M Bool := do
-        if let some label := matchDecl? ns id declName then
+        if let some label := matchDecl? ns id danglingDot declName then
           -- dbg_trace "matched with {id}, {declName}, {label}"
           addCompletionItem label c.type expectedType?
           return true
@@ -172,9 +177,9 @@ private def idCompletionCore (ctx : ContextInfo) (stx : Syntax) (expectedType? :
   -- TODO search macros
   -- TODO search namespaces
 
-private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (stx : Syntax) (expectedType? : Option Expr) : IO (Option CompletionList) :=
+private def idCompletion (ctx : ContextInfo) (lctx : LocalContext) (id : Name) (danglingDot : Bool) (expectedType? : Option Expr) : IO (Option CompletionList) :=
   runM ctx lctx do
-    idCompletionCore ctx stx expectedType?
+    idCompletionCore ctx id danglingDot expectedType?
 
 private def isDotCompletionMethod (info : ConstantInfo) : MetaM Bool :=
   forallTelescopeReducing info.type fun xs _ => do
@@ -214,9 +219,9 @@ private def dotCompletion (ctx : ContextInfo) (info : TermInfo) (expectedType? :
         pure {}
     if nameSet.isEmpty then
       if info.stx.isIdent then
-        idCompletionCore ctx info.stx expectedType?
-      else if info.stx.getKind == ``Lean.Parser.Term.completion then
-        idCompletionCore ctx info.stx[0] expectedType?
+        idCompletionCore ctx info.stx.getId (danglingDot := false) expectedType?
+      else if info.stx.getKind == ``Lean.Parser.Term.completion && info.stx[0].isIdent then
+        idCompletionCore ctx info.stx[0].getId (danglingDot := true) expectedType?
       else
         failure
     else
@@ -249,7 +254,7 @@ partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTr
   | some (ctx, Info.ofCompletionInfo info) =>
     match info with
     | CompletionInfo.dot info (expectedType? := expectedType?) .. => dotCompletion ctx info expectedType?
-    | CompletionInfo.id stx lctx expectedType? => idCompletion ctx lctx stx expectedType?
+    | CompletionInfo.id stx id danglingDot lctx expectedType? => idCompletion ctx lctx id danglingDot expectedType?
     | CompletionInfo.option .. => optionCompletion ctx
     | CompletionInfo.tactic .. => tacticCompletion ctx
     | _ => return none
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index 654b8b9446..f7cd67aa8d 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -1,5 +1,6 @@
 [Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩
   Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
+    [.] `Nat : some Sort.{?_uniq.237} @ ⟨13, 11⟩-⟨13, 14⟩
     Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
   x : Nat @ ⟨13, 7⟩-⟨13, 8⟩
   Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩
@@ -9,8 +10,10 @@
     Prod✝ Nat Nat
       Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 22⟩†
       Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
+        [.] `Nat : some Type.{?_uniq.241} @ ⟨13, 18⟩-⟨13, 21⟩
         Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
       Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
+        [.] `Nat : some Type.{?_uniq.240} @ ⟨13, 24⟩-⟨13, 27⟩
         Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
   let y : Nat × Nat := (x, x);
   id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩
@@ -28,19 +31,23 @@
             x : Nat @ ⟨14, 15⟩-⟨14, 16⟩
     y : Nat × Nat @ ⟨14, 6⟩-⟨14, 7⟩
     id y : Nat × Nat @ ⟨15, 2⟩-⟨15, 6⟩
+      [.] `id : some Prod.{0 0} Nat Nat @ ⟨15, 2⟩-⟨15, 4⟩
       id : {α : Type} → α → α @ ⟨15, 2⟩-⟨15, 4⟩
       y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩
         y : Nat × Nat @ ⟨15, 5⟩-⟨15, 6⟩
 [Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩
   ∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩
     Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
+      [.] `Nat : some Sort.{?_uniq.270} @ ⟨17, 15⟩-⟨17, 18⟩
       Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
     x : Nat @ ⟨17, 9⟩-⟨17, 10⟩
     Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
+      [.] `Nat : some Sort.{?_uniq.272} @ ⟨17, 15⟩-⟨17, 18⟩
       Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
     y : Nat @ ⟨17, 11⟩-⟨17, 12⟩
     Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩
       Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
+        [.] `Bool : some Sort.{?_uniq.275} @ ⟨17, 27⟩-⟨17, 31⟩
         Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
       b : Bool @ ⟨17, 23⟩-⟨17, 24⟩
       x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩
@@ -90,16 +97,20 @@
 [Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩
   Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩
     Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
+      [.] `Nat : some Sort.{?_uniq.592} @ ⟨21, 16⟩-⟨21, 19⟩
       Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
     x : Nat @ ⟨21, 10⟩-⟨21, 11⟩
     Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
+      [.] `Nat : some Sort.{?_uniq.594} @ ⟨21, 16⟩-⟨21, 19⟩
       Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
     y : Nat @ ⟨21, 12⟩-⟨21, 13⟩
     Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩
       Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
+        [.] `Bool : some Sort.{?_uniq.597} @ ⟨21, 28⟩-⟨21, 32⟩
         Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
       b : Bool @ ⟨21, 24⟩-⟨21, 25⟩
       Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
+        [.] `Nat : some Sort.{?_uniq.599} @ ⟨21, 36⟩-⟨21, 39⟩
         Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
   fun (x y : Nat) (b : Bool) =>
     let x : Nat × Nat := (x + y, x - y);
@@ -211,18 +222,24 @@
     Prod✝ Nat (Array (Array Nat))
       Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 16⟩†
       Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
+        [.] `Nat : some Type.{?_uniq.1452} @ ⟨27, 12⟩-⟨27, 15⟩
         Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
       Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩
+        [.] `Array : some Type.{?_uniq.1451} @ ⟨27, 18⟩-⟨27, 23⟩
         Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
         Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩
           Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩
+            [.] `Array : some Type.{?_uniq.1453} @ ⟨27, 25⟩-⟨27, 30⟩
             Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
             Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
+              [.] `Nat : some Type.{?_uniq.1454} @ ⟨27, 31⟩-⟨27, 34⟩
               Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
   s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
   Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩
+    [.] `Array : some Sort.{?_uniq.1456} @ ⟨27, 39⟩-⟨27, 44⟩
     Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
     Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
+      [.] `Nat : some Type.{?_uniq.1457} @ ⟨27, 45⟩-⟨27, 48⟩
       Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
   Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩
     s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
@@ -236,9 +253,11 @@
       Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
 [Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩
   B : Type @ ⟨30, 14⟩-⟨30, 15⟩
+    [.] `B : some Sort.{?_uniq.1498} @ ⟨30, 14⟩-⟨30, 15⟩
     B : Type @ ⟨30, 14⟩-⟨30, 15⟩
   arg : B @ ⟨30, 8⟩-⟨30, 11⟩
   Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
+    [.] `Nat : some Sort.{?_uniq.1500} @ ⟨30, 19⟩-⟨30, 22⟩
     Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
   A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩
     arg : B @ ⟨31, 2⟩-⟨31, 5⟩
@@ -251,9 +270,11 @@
     0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩
 [Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩
   Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
+    [.] `Nat : some Sort.{?_uniq.1520} @ ⟨33, 12⟩-⟨33, 15⟩
     Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
   x : Nat @ ⟨33, 8⟩-⟨33, 9⟩
   B : Type @ ⟨33, 19⟩-⟨33, 20⟩
+    [.] `B : some Sort.{?_uniq.1522} @ ⟨33, 19⟩-⟨33, 20⟩
     B : Type @ ⟨33, 19⟩-⟨33, 20⟩
   { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩
     ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩
@@ -265,10 +286,12 @@
           Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 17⟩†
           { val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩
             id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩
+              [.] `id : some Nat -> Nat @ ⟨34, 20⟩-⟨34, 22⟩
               id : {α : Type} → α → α @ ⟨34, 20⟩-⟨34, 22⟩
             val : Nat → Nat := id @ ⟨34, 13⟩-⟨34, 16⟩
           { val := id } : A @ ⟨34, 26⟩-⟨34, 39⟩
             id : Nat → Nat @ ⟨34, 35⟩-⟨34, 37⟩
+              [.] `id : some Nat -> Nat @ ⟨34, 35⟩-⟨34, 37⟩
               id : {α : Type} → α → α @ ⟨34, 35⟩-⟨34, 37⟩
             val : Nat → Nat := id @ ⟨34, 28⟩-⟨34, 31⟩
     pair : A × A := ({ val := id }, { val := id }) @ ⟨34, 2⟩-⟨34, 6⟩