feat: generalize inferred namespace notation to functions

RELEASES.md

@@ -27,6 +27,12 @@ example (a : Nat) (h : n = 1) : [a].length = n := by
 * Extend dot-notation `x.field` for arrow types. If type of `x` is an arrow, we look up for `Function.field`.
 For example, given `f : Nat → Nat` and `g : Nat → Nat`, `f.comp g` is now notation for `Function.comp f g`.
 
+* The new `.<identifier>` notation is now also accepted where a function type is expected.
+```lean
+example (xs : List Nat) : List Nat := .map .succ xs
+example (xs : List α) : Std.RBTree α ord := xs.foldl .insert ∅
+```
+
 * [Add code folding support to the language server](https://github.com/leanprover/lean4/pull/1014).
 
 * Support notation `let <pattern> := <expr> | <else-case>` in `do` blocks.

src/Lean/Elab/App.lean

@@ -862,22 +862,23 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `(@$t)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
     | `(.$id:ident) =>
-       tryPostponeIfNoneOrMVar expectedType?
-       match expectedType? with
-       | none => throwError "invalid dotted identifier notation, expected type must be known"
-       | some expectedType =>
-         if let .const declName .. := (← instantiateMVars expectedType).getAppFn then
-           let idNew := declName ++ id.getId.eraseMacroScopes
-           unless (← getEnv).contains idNew do
-             throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
-           let fConst ← mkConst idNew
-           addTermInfo f fConst
-           let s ← observing do
-             let e ← elabAppLVals fConst lvals namedArgs args expectedType? explicit ellipsis
-             if overloaded then ensureHasType expectedType? e else pure e
-           return acc.push s
-         else
-           throwError "invalid dotted identifier notation, expected type is not of the form (C ...) where C is a constant{indentExpr expectedType}"
+      tryPostponeIfNoneOrMVar expectedType?
+      let some expectedType := expectedType?
+        | throwError "invalid dotted identifier notation, expected type must be known"
+      forallTelescopeReducing expectedType fun _ resultType => do
+        let resultTypeFn := (← instantiateMVars resultType).getAppFn
+        tryPostponeIfMVar resultTypeFn
+        let .const declName .. := resultTypeFn
+          | 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
+          throwError "invalid dotted identifier notation, unknown identifier `{idNew}` from expected type{indentExpr expectedType}"
+        let fConst ← mkConst idNew
+        addTermInfo f fConst
+        let s ← observing do
+          let e ← elabAppLVals fConst lvals namedArgs args expectedType? explicit ellipsis
+          if overloaded then ensureHasType expectedType? e else pure e
+        return acc.push s
     | _ => do
       let catchPostpone := !overloaded
       /- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms.

tests/lean/run/944.lean

@@ -28,8 +28,14 @@ end Lean.Elab
 def f2 (xs : List Nat) : List Nat :=
   .map (· + 1) xs
 
+def f2' (xs : List Nat) : List Nat :=
+  .map .succ xs
+
 def f3 : Nat :=
   .zero
 
 def f4 (x : Nat) : Nat :=
   .succ x
+
+example (xs : List α) : Std.RBTree α ord :=
+  xs.foldl .insert ∅