feat: allow dotted function notation to use @ and explicit universes (#13245)

This PR extends Lean syntax for dotted function notation (`.f`) to add
support for explicit mode (`@.f`), explicit universes (`.f.{u,v}`), and
both simultaneously (`@.f.{u,v}`). This also includes a fix for a bug
involving overloaded functions, where it used to give erroneous
deprecation warnings about declarations that the function did not
elaborate to.

Closes #10984

src/Lean/Elab/App.lean

@@ -1832,13 +1832,15 @@ To infer a namespace from the expected type, we do the following operations:
 - if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace,
   and if that doesn't work, try unfolding the expression and continuing.
 -/
-private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
+private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do
   unless id.isAtomic do
     throwError "Invalid dotted identifier notation: The name `{id}` must be atomic"
   tryPostponeIfNoneOrMVar expectedType?
   let some expectedType := expectedType?
     | throwNoExpectedType
   addCompletionInfo <| CompletionInfo.dotId idRef id (← getLCtx) expectedType?
+  -- We will check deprecations in `elabAppFnResolutions`.
+  withoutCheckDeprecated do
   withForallBody expectedType fun resultType => do
     go resultType expectedType #[]
 where
@@ -1878,8 +1880,10 @@ where
           |>.filter (fun (_, fieldList) => fieldList.isEmpty)
           |>.map Prod.fst
         if !candidates.isEmpty then
-          candidates.mapM fun resolvedName => return (← mkConst resolvedName, ← getRef, [])
+          candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, [])
         else if let some (fvar, []) ← resolveLocalName fullName then
+          unless explicitUnivs.isEmpty do
+            throwInvalidExplicitUniversesForLocal fvar
           return [(fvar, ← getRef, [])]
         else
           throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`"
@@ -1919,6 +1923,10 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
       let some idx := idxStx.isFieldIdx?
         | throwError "Internal error: Unexpected field index syntax `{idxStx}`"
       elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
+    let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do
+      let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType?
+      -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
+      elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     match f with
     | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
     | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
@@ -1934,16 +1942,17 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     | `($id:ident.{$us,*}) => do
       let us ← elabExplicitUnivs us
       elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
-    | `(@$id:ident) =>
-      elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
-    | `(@$_:ident.{$_us,*}) =>
+    | `(.$id:ident) => elabDottedIdent id [] explicit
+    | `(.$id:ident.{$us,*}) =>
+      let us ← elabExplicitUnivs us
+      elabDottedIdent id us explicit
+    | `(@$_:ident)
+    | `(@$_:ident.{$_us,*})
+    | `(@.$_:ident)
+    | `(@.$_:ident.{$_us,*}) =>
       elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
     | `(@$_)     => throwUnsupportedSyntax -- invalid occurrence of `@`
     | `(_)       => throwError "A placeholder `_` cannot be used where a function is expected"
-    | `(.$id:ident) =>
-        let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes expectedType?
-        -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns
-        elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true)
     | _ => do
       let catchPostpone := !overloaded
       /- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms.
@@ -2086,13 +2095,15 @@ private def elabAtom : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$_:ident)          => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$_:ident.{$_us,*}) => elabAtom stx expectedType?
-  | `(@$(_).$_:fieldIdx)  => elabAtom stx expectedType?
-  | `(@$(_).$_:ident)     => elabAtom stx expectedType?
-  | `(@($t))             => elabTerm t expectedType? (implicitLambda := false)    -- `@` is being used just to disable implicit lambdas
-  | `(@$t)               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
-  | _                    => throwUnsupportedSyntax
+  | `(@$_:ident)           => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$_:ident.{$_us,*})  => elabAtom stx expectedType?
+  | `(@$(_).$_:fieldIdx)   => elabAtom stx expectedType?
+  | `(@$(_).$_:ident)      => elabAtom stx expectedType?
+  | `(@.$_:ident)          => elabAtom stx expectedType?
+  | `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType?
+  | `(@($t))               => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | `(@$t)                 => elabTerm t expectedType? (implicitLambda := false)   -- `@` is being used just to disable implicit lambdas
+  | _                      => throwUnsupportedSyntax
 
 @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom
 @[builtin_term_elab proj] def elabProj : TermElab := elabAtom

src/Lean/Elab/Term/TermElabM.lean

@@ -2124,11 +2124,14 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels :
     let const ← withoutCheckDeprecated <| mkConst declName explicitLevels
     return (const, projs) :: result
 
+def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α :=
+  throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
+
 def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do
   addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType?
   if let some (e, projs) ← resolveLocalName n then
     unless explicitLevels.isEmpty do
-      throwError "invalid use of explicit universe parameters, `{e}` is a local variable"
+      throwInvalidExplicitUniversesForLocal e
     return [(e, projs)]
   let preresolved := preresolved.filterMap fun
     | .decl n projs => some (n, projs)

src/Lean/Parser/Term.lean

@@ -882,13 +882,19 @@ the available context).
 -/
 def identProjKind := `Lean.Parser.Term.identProj
 
+@[builtin_term_parser] def dotIdent := leading_parser
+  "." >> checkNoWsBefore >> rawIdent
+
 def isIdent (stx : Syntax) : Bool :=
   -- antiquotations should also be allowed where an identifier is expected
   stx.isAntiquot || stx.isIdent
 
+def isIdentOrDotIdent (stx : Syntax) : Bool :=
+  isIdent stx || stx.isOfKind ``dotIdent
+
 /-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/
 @[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser
-  checkStackTop isIdent "expected preceding identifier" >>
+  checkStackTop isIdentOrDotIdent "expected preceding identifier" >>
   checkNoWsBefore "no space before '.{'" >> ".{" >>
   sepBy1 levelParser ", " >> "}"
 /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`.
@@ -976,9 +982,6 @@ appropriate parameter for the underlying monad's `ST` effects, then passes it to
 @[builtin_term_parser] def dynamicQuot := withoutPosition <| leading_parser
   "`(" >> ident >> "| " >> incQuotDepth (parserOfStack 1) >> ")"
 
-@[builtin_term_parser] def dotIdent := leading_parser
-  "." >> checkNoWsBefore >> rawIdent
-
 /--
 Implementation of the `show_term` term elaborator.
 -/

tests/elab/10984.lean

@@ -0,0 +1,115 @@
+/-!
+# Dotted function notation can handle `@` and universe levels
+-/
+
+set_option warn.sorry false
+set_option linter.deprecated true
+set_option pp.mvars.anonymous false
+
+/-!
+Explicit `@`
+-/
+/-- info: [] : List Nat -/
+#guard_msgs in #check (@.nil Nat : List _)
+
+/-!
+Explicit `@` disables implicit lambda
+-/
+/--
+error: Type mismatch
+  @List.nil
+has type
+  {α : Type _} → List α
+but is expected to have type
+  List ?_
+-/
+#guard_msgs in #check (@.nil : List _)
+
+/-!
+Universe levels.
+-/
+example : List Nat := .nil.{0}
+
+/--
+error: Type mismatch
+  []
+has type
+  List.{1} ?_
+of sort `Type 1` but is expected to have type
+  List.{0} Nat
+of sort `Type`
+-/
+#guard_msgs in
+example : List Nat := .nil.{1}
+
+/-- error: too many explicit universe levels for `List.nil` -/
+#guard_msgs in
+example : List Nat := .nil.{0,0}
+
+/-!
+Explicit plus universe levels also disables implicit lambda
+-/
+/--
+error: Type mismatch
+  @List.nil
+has type
+  {α : Type} → List α
+of sort `Type 1` but is expected to have type
+  List Nat
+of sort `Type`
+-/
+#guard_msgs in example : List Nat := @.nil.{0}
+
+/-!
+Example of `@` from Floris van Doorn at https://github.com/leanprover/lean4/issues/10984
+-/
+example {α : Type} (f : ∀ {α}, List α → List α) : f (@.nil α) = .nil := sorry
+
+/-!
+Example of `@` plus universe levels adapated from https://github.com/leanprover/lean4/issues/10984
+-/
+example {α : Type u} (f : ∀ {α}, List α → List α) : f (@.nil.{u} α) = .nil := sorry
+
+/-!
+Example from Arthur Adjedj at https://github.com/leanprover/lean4/issues/8743
+-/
+/-- info: [2] : List Nat -/
+#guard_msgs in #check (List.cons.{0} 2 [] : List Nat)
+/-- info: [2] : List Nat -/
+#guard_msgs in #check (.cons.{0} 2 [] : List Nat)
+
+/--
+error: Type mismatch
+  [2]
+has type
+  List.{1} ?_
+of sort `Type 1` but is expected to have type
+  List.{0} Nat
+of sort `Type`
+-/
+#guard_msgs in #check (.cons.{1} 2 [] : List Nat)
+
+/-!
+Regression test: This used to give a deprecation warning on the first `#check`.
+-/
+def MyNS1.List.nil' : List Nat := []
+@[deprecated MyNS1.List.nil' (since := "forever")] def MyNS2.List.nil' : List Int := []
+
+/-- info: MyNS1.List.nil' : List Nat -/
+#guard_msgs in
+open MyNS1 MyNS2 in #check (.nil' : List Nat)
+
+/--
+warning: `MyNS2.List.nil'` has been deprecated: Use `MyNS1.List.nil'` instead
+
+Note: The updated constant has a different type:
+  List Nat
+instead of
+  List Int
+
+Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.nil'` to `MyNS1.List.nil' x`).
+---
+info: MyNS2.List.nil' : List Int
+-/
+#guard_msgs in
+open MyNS1 MyNS2 in #check (.nil' : List Int)