fix: def _root_ and dotted notation in recursive definitions

closes #1289

doc/examples/bintree.lean

@@ -92,7 +92,7 @@ where
   go (t : Tree β) (acc : List (Nat × β)) : List (Nat × β) :=
     match t with
     | leaf => acc
-    | node l k v r => l.go ((k, v) :: r.go acc)
+    | node l k v r => go l ((k, v) :: go r acc)
 
 /-!
 We now prove that `t.toList` and `t.toListTR` return the same list.

src/Lean/Elab/App.lean

@@ -718,17 +718,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
     -- search local context first, then environment
     let searchCtx : Unit → TermElabM LValResolution := fun _ => do
       let fullName := Name.mkStr structName fieldName
-      let currNamespace ← getCurrNamespace
-      let localName := fullName.replacePrefix currNamespace Name.anonymous
-      let lctx ← getLCtx
-      match lctx.findFromUserName? localName with
-      | some localDecl =>
+      for localDecl in (← getLCtx) do
         if localDecl.binderInfo == BinderInfo.auxDecl then
-          /- LVal notation is being used to make a "local" recursive call. -/
-          return LValResolution.localRec structName fullName localDecl.toExpr
-        else
-          searchEnv ()
-      | none => searchEnv ()
+          if let some localDeclFullName := (← read).auxDeclToFullName.find? localDecl.fvarId then
+            if fullName == (privateToUserName? localDeclFullName).getD localDeclFullName then
+              /- LVal notation is being used to make a "local" recursive call. -/
+              return LValResolution.localRec structName fullName localDecl.toExpr
+      searchEnv ()
     if isStructure env structName then
       match findField? env structName (Name.mkSimple fieldName) with
       | some baseStructName => return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName)

src/Lean/Elab/Inductive.lean

@@ -172,14 +172,14 @@ private def elabHeader (views : Array InductiveView) : TermElabM (Array ElabHead
 private partial def withInductiveLocalDecls (rs : Array ElabHeaderResult) (x : Array Expr → Array Expr → TermElabM α) : TermElabM α := do
   let namesAndTypes ← rs.mapM fun r => do
     let type ← mkTypeFor r
-    pure (r.view.shortDeclName, type)
+    pure (r.view.declName, r.view.shortDeclName, type)
   let r0     := rs[0]!
   let params := r0.params
   withLCtx r0.lctx r0.localInsts <| withRef r0.view.ref do
     let rec loop (i : Nat) (indFVars : Array Expr) := do
       if h : i < namesAndTypes.size then
-        let (id, type) := namesAndTypes.get ⟨i, h⟩
-        withLocalDecl id BinderInfo.auxDecl type fun indFVar => loop (i+1) (indFVars.push indFVar)
+        let (declName, shortDeclName, type) := namesAndTypes.get ⟨i, h⟩
+        Term.withAuxDecl shortDeclName type declName fun indFVar => loop (i+1) (indFVars.push indFVar)
       else
         x params indFVars
     loop 0 #[]

src/Lean/Elab/LetRec.lean

@@ -66,7 +66,7 @@ private partial def withAuxLocalDecls {α} (views : Array LetRecDeclView) (k : A
   let rec loop (i : Nat) (fvars : Array Expr) : TermElabM α :=
     if h : i < views.size then
       let view := views.get ⟨i, h⟩
-      withLocalDecl view.shortDeclName BinderInfo.auxDecl view.type fun fvar => loop (i+1) (fvars.push fvar)
+      withAuxDecl view.shortDeclName view.type view.declName fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars
   loop 0 #[]

src/Lean/Elab/MutualDef.lean

@@ -156,7 +156,7 @@ private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (
       if header.modifiers.isNonrec then
         loop (i+1) fvars
       else
-        withLocalDecl header.shortDeclName BinderInfo.auxDecl header.type fun fvar => loop (i+1) (fvars.push fvar)
+        withAuxDecl header.shortDeclName header.type header.declName fun fvar => loop (i+1) (fvars.push fvar)
     else
       k fvars
   loop 0 #[]

src/Lean/Elab/Term.lean

@@ -166,13 +166,17 @@ end Tactic
 namespace Term
 
 structure Context where
-  declName?       : Option Name     := none
-  macroStack      : MacroStack      := []
+  declName? : Option Name := none
+  /--
+    Map `.auxDecl` local declarations used to encode recursive declarations to their full-names.
+  -/
+  auxDeclToFullName : FVarIdMap Name  := {}
+  macroStack        : MacroStack      := []
   /--
      When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
      The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
      the list of pending synthetic metavariables, and returns `?m`. -/
-  mayPostpone     : Bool            := true
+  mayPostpone : Bool := true
   /--
      When `errToSorry` is set to true, the method `elabTerm` catches
      exceptions and converts them into synthetic `sorry`s.
@@ -181,7 +185,7 @@ structure Context where
      `errToSorry` remains `false` for all elaboration functions invoked by `F`.
      That is, it is safe to transition `errToSorry` from `true` to `false`, but
      we must not set `errToSorry` to `true` when it is currently set to `false`. -/
-  errToSorry      : Bool            := true
+  errToSorry : Bool := true
   /--
      When `autoBoundImplicit` is set to true, instead of producing
      an "unknown identifier" error for unbound variables, we generate an
@@ -432,6 +436,15 @@ def withLevelNames (levelNames : List Name) (x : TermElabM α) : TermElabM α :=
   setLevelNames levelNames
   try x finally setLevelNames levelNamesSaved
 
+/--
+  Declare an auxiliary local declaration `shortDeclName : type` for elaborating recursive declaration `declName`,
+  update the mapping `auxDeclToFullName`, and then execute `k`.
+-/
+def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → TermElabM α) : TermElabM α :=
+  withLocalDecl shortDeclName BinderInfo.auxDecl type fun x =>
+    withReader (fun ctx => { ctx with auxDeclToFullName := ctx.auxDeclToFullName.insert x.fvarId! declName }) do
+      k x
+
 /--
   Execute `x` without converting errors (i.e., exceptions) to `sorry` applications.
   Recall that when `errToSorry = true`, the method `elabTerm` catches exceptions and convert them into `sorry` applications.

tests/lean/run/1289.lean

@@ -0,0 +1,43 @@
+def _root_.Nat.mod2 : Nat → Nat
+  | n+2 => n.mod2
+  | n => n
+
+protected def _root_.Nat.mod3 : Nat → Nat
+  | n+2 => n.mod3
+  | n => n
+
+private def _root_.Nat.mod4 : Nat → Nat
+  | n+2 => n.mod4
+  | n => n
+
+#exit
+
+inductive Foo.Bla.T where
+  | s : T → T
+  | z
+
+namespace AAA.BBB.CCC
+
+def _root_.Foo.Bla.T.toNat₁ : Foo.Bla.T → Nat
+  | .s a => a.toNat₁ + 1
+  | .z => 0
+
+protected def _root_.Foo.Bla.T.toNat₂ : Foo.Bla.T → Nat
+  | .s a => a.toNat₂ + 1
+  | .z => 0
+
+private def _root_.Foo.Bla.T.toNat₃ : Foo.Bla.T → Nat
+  | .s a => a.toNat₃ + 1
+  | .z => 0
+
+def _root_.Foo.Bla.T.toNat₄ : Foo.Bla.T → Nat
+  | .s a => toNat₄ a + 1
+  | .z => 0
+
+protected def _root_.Foo.Bla.T.toNat₅ : Foo.Bla.T → Nat
+  | .s a => T.toNat₅ a + 1
+  | .z => 0
+
+private def _root_.Foo.Bla.T.toNat₆ : Foo.Bla.T → Nat
+  | .s a => toNat₆ a + 1
+  | .z => 0