feat: allow explicit mode with field notation

Now one can write `@x.f`, `@(x).f`, `@x.1`, `@(x).1`, and so on.

This fixes an issue where structure instance update notation (like `{x with a := a'}`) could fail if the field `a` had a type with implicit, optional, or auto parameters.

Closes leanprover#5406.

src/Lean/Elab/App.lean

@@ -1394,8 +1394,6 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
 
 private def elabAppLVals (f : Expr) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg)
     (expectedType? : Option Expr) (explicit ellipsis : Bool) : TermElabM Expr := do
-  if !lvals.isEmpty && explicit then
-    throwError "invalid use of field notation with `@` modifier"
   elabAppLValsAux namedArgs args expectedType? explicit ellipsis f lvals
 
 def elabExplicitUnivs (lvls : Array Syntax) : TermElabM (List Level) := do
@@ -1494,19 +1492,21 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     withReader (fun ctx => { ctx with errToSorry := false }) do
       f.getArgs.foldlM (init := acc) fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc
   else
-    let elabFieldName (e field : Syntax) := do
+    let elabFieldName (e field : Syntax) (explicit : Bool) := do
       let newLVals := field.identComponents.map fun comp =>
         -- We use `none` in `suffix?` since `field` can't be part of a composite name
         LVal.fieldName comp comp.getId.getString! none f
       elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
-    let elabFieldIdx (e idxStx : Syntax) := do
+    let elabFieldIdx (e idxStx : Syntax) (explicit : Bool) := do
       let some idx := idxStx.isFieldIdx? | throwError "invalid field index"
       elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
     match f with
-    | `($(e).$idx:fieldIdx) => elabFieldIdx e idx
-    | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx
-    | `($(e).$field:ident) => elabFieldName e field
-    | `($e |>.$field:ident) => elabFieldName e field
+    | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit
+    | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit
+    | `($(e).$field:ident) => elabFieldName e field explicit
+    | `($e |>.$field:ident) => elabFieldName e field explicit
+    | `(@$(e).$idx:fieldIdx) => elabFieldIdx e idx (explicit := true)
+    | `(@$(e).$field:ident) => elabFieldName e field (explicit := true)
     | `($_:ident@$_:term) =>
       throwError "unexpected occurrence of named pattern"
     | `($id:ident) => do
@@ -1663,8 +1663,10 @@ 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)          => 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

src/Lean/Elab/StructInst.lean

@@ -473,7 +473,10 @@ private def getFieldIdx (structName : Name) (fieldNames : Array Name) (fieldName
 def mkProjStx? (s : Syntax) (structName : Name) (fieldName : Name) : TermElabM (Option Syntax) := do
   if (findField? (← getEnv) structName fieldName).isNone then
     return none
-  return some <| mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]
+  return some <|
+    mkNode ``Parser.Term.explicit
+      #[mkAtomFrom s "@",
+        mkNode ``Parser.Term.proj #[s, mkAtomFrom s ".", mkIdentFrom s fieldName]]
 
 def findField? (fields : Fields) (fieldName : Name) : Option (Field Struct) :=
   fields.find? fun field =>

tests/lean/run/5406.lean

@@ -0,0 +1,99 @@
+/-!
+# Add explicit mode projections
+
+This is to fix a bug where structure instance notation was not working when there were opt params.
+-/
+
+/-!
+Motivating issue from https://github.com/leanprover/lean4/issues/5406
+The `example` had an elaboration error because the structure instance was expanding to `{b := m.b}`.
+Now it expands to `{b := @m.b}`.
+-/
+structure Methods where
+  b : Nat → (opt : Nat := 42) → Nat
+
+example (m : Methods) : Methods := { m with }
+
+/-- info: fun m => { b := @Methods.b m } : Methods → Methods -/
+#guard_msgs in #check fun (m : Methods) => { m with }
+
+
+/-!
+Tests of explicit mode, with and without arguments.
+-/
+
+/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @m.b
+
+/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @(m).b
+
+/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @m.1
+
+/-- info: fun m => @Methods.b m : Methods → Nat → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @(m).1
+
+/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @m.b 1
+
+/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @(m).b 1
+
+/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @m.1 1
+
+/-- info: fun m => @Methods.b m 1 : Methods → optParam Nat 42 → Nat -/
+#guard_msgs in #check fun (m : Methods) => @(m).1 1
+
+
+/-!
+Tests of explicit mode with class instances. The type parameter remains implicit.
+We need this so that structure instances work properly.
+-/
+
+class C (α : Type) [Inhabited α] where
+  f (x : α := default) : α
+
+/-- info: fun inst => C.f : C Nat → Nat -/
+#guard_msgs in #check fun (inst : C Nat) => inst.f
+
+/-- info: fun inst => @C.f Nat instInhabitedNat inst : C Nat → optParam Nat default → Nat -/
+#guard_msgs in #check fun (inst : C Nat) => @inst.f
+
+/-- info: fun inst => @C.f Nat instInhabitedNat inst : C Nat → optParam Nat default → Nat -/
+#guard_msgs in #check fun (inst : C Nat) => @C.f _ _ inst
+
+/-- info: fun inst => { f := @C.f Nat instInhabitedNat inst } : C Nat → C Nat -/
+#guard_msgs in #check fun (inst : C Nat) => { inst with }
+
+
+/-!
+Tests of deeper updates and accesses.
+-/
+
+structure A (α : Type) where
+  x : α
+structure B (α β : Type) extends A α where
+  y : β
+
+/-- info: fun α β x' b => { x := x', y := b.y } : (α β : Type) → α → B α β → B α β -/
+#guard_msgs in #check fun (α β) (x' : α) (b : B α β) => {b with x := x'}
+
+/-- info: fun α β b => b.x : (α β : Type) → B α β → α -/
+#guard_msgs in #check fun (α β) (b : B α β) => @b.toA.x
+
+/-- info: fun α β b => b.x : (α β : Type) → B α β → α -/
+#guard_msgs in #check fun (α β) (b : B α β) => @b.x
+
+
+/-!
+Tests of implicit arguments in updates.
+-/
+
+structure I where
+  f : {_ : Nat} → Nat
+
+-- used to give `fun i ↦ ?m.369 i : I → I`
+/-- info: fun i => { f := @I.f i } : I → I -/
+#guard_msgs in #check fun (i : I) => {i with}