fix: allow dot idents to resolve to local names (#6602)

This PR allows the dot ident notation to resolve to the current
definition, or to any of the other definitions in the same mutual block.
Existing code that uses dot ident notation may need to have `nonrec`
added if the ident has the same name as the definition.

Closes #6601

src/Lean/Elab/App.lean

@@ -1474,7 +1474,7 @@ where
     | field::fields, false => .fieldName field field.getId.getString! none fIdent :: toLVals fields false
 
 /-- Resolve `(.$id:ident)` using the expected type to infer namespace. -/
-private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Name := do
+private partial def resolveDotName (id : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
   tryPostponeIfNoneOrMVar expectedType?
   let some expectedType := expectedType?
     | throwError "invalid dotted identifier notation, expected type must be known"
@@ -1489,17 +1489,20 @@ where
         withForallBody body k
       else
         k body
-  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Name := do
+  go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM Expr := do
     let resultType ← instantiateMVars resultType
     let resultTypeFn := resultType.cleanupAnnotations.getAppFn
     try
       tryPostponeIfMVar resultTypeFn
       let .const declName .. := resultTypeFn.cleanupAnnotations
         | throwError "invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant{indentExpr expectedType}"
       let idNew := declName ++ id.getId.eraseMacroScopes
-      unless (← getEnv).contains idNew do
+      if (← getEnv).contains idNew then
+        mkConst idNew
+      else if let some (fvar, []) ← resolveLocalName idNew then
+        return fvar
+      else
         throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
-      return idNew
     catch
       | ex@(.error ..) =>
         match (← unfoldDefinition? resultType) with
@@ -1548,7 +1551,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
     | `(.$id:ident) =>
         addCompletionInfo <| CompletionInfo.dotId f id.getId (← getLCtx) expectedType?
-        let fConst ← mkConst (← resolveDotName id expectedType?)
+        let fConst ← resolveDotName id expectedType?
         let s ← observing do
           -- Use (force := true) because we want to record the result of .ident resolution even in patterns
           let fConst ← addTermInfo f fConst expectedType? (force := true)

tests/lean/6601.lean

@@ -0,0 +1,26 @@
+/-! Dot ident notation should resolve mutual definitions -/
+
+mutual
+
+inductive Even
+  | zero
+  | succ (n : Odd)
+  deriving Inhabited
+
+inductive Odd
+  | succ (n : Even)
+  deriving Inhabited
+
+end
+
+mutual
+
+def Even.ofNat : Nat → Even
+  | 0 => .zero
+  | n + 1 => .succ (.ofNat n)
+
+def Odd.ofNat : Nat → Odd
+  | 0 => panic! "invalid input"
+  | n + 1 => .succ (.ofNat n)
+
+end