feat: actual implementation for #5283 (#5512)

I did a bad git rebase before merging #5283, which reverted it to an
earlier version. This PR has the actual implementation of RFC #5397.

src/Init/Data/NeZero.lean

@@ -35,4 +35,4 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 :=
   ⟨fun h ↦ h.out, NeZero.mk⟩
 
 @[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False :=
-  ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩
+  ⟨fun _ ↦ NeZero.ne (0 : α) rfl, fun h ↦ h.elim⟩

src/Lean/Elab/App.lean

@@ -411,21 +411,23 @@ private def finalize : M Expr := do
   synthesizeAppInstMVars
   return e
 
-/-- Return `true` if there is a named argument that depends on the next argument. -/
-private def anyNamedArgDependsOnCurrent : M Bool := do
+/--
+Returns a named argument that depends on the next argument, otherwise `none`.
+-/
+private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do
   let s ← get
   if s.namedArgs.isEmpty then
-    return false
+    return none
   else
     forallTelescopeReducing s.fType fun xs _ => do
       let curr := xs[0]!
       for i in [1:xs.size] do
         let xDecl ← xs[i]!.fvarId!.getDecl
-        if s.namedArgs.any fun arg => arg.name == xDecl.userName then
+        if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then
           /- Remark: a default value at `optParam` does not count as a dependency -/
           if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then
-            return true
-      return false
+            return arg
+      return none
 
 
 /-- Return `true` if there are regular or named arguments to be processed. -/
@@ -514,8 +516,9 @@ where
 
 mutual
   /--
-    Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
-    and then execute the main loop.-/
+  Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
+  and then execute the main loop.
+  -/
   private partial def addEtaArg (argName : Name) : M Expr := do
     let n    ← getBindingName
     let type ← getArgExpectedType
@@ -524,6 +527,9 @@ mutual
       addNewArg argName x
       main
 
+  /--
+  Create a fresh metavariable for the implicit argument, add it to `f`, and thn execute the main loop.
+  -/
   private partial def addImplicitArg (argName : Name) : M Expr := do
     let argType ← getArgExpectedType
     let arg ← if (← isNextOutParamOfLocalInstanceAndResult) then
@@ -541,35 +547,47 @@ mutual
     main
 
   /--
-    Process a `fType` of the form `(x : A) → B x`.
-    This method assume `fType` is a function type -/
+  Process a `fType` of the form `(x : A) → B x`.
+  This method assume `fType` is a function type.
+  -/
   private partial def processExplicitArg (argName : Name) : M Expr := do
     match (← get).args with
     | arg::args =>
-      if (← anyNamedArgDependsOnCurrent) then
+      -- Note: currently the following test never succeeds in explicit mode since `@x.f` notation does not exist.
+      if let some true := NamedArg.suppressDeps <$> (← findNamedArgDependsOnCurrent?) then
         /-
-        We treat the explicit argument `argName` as implicit if we have named arguments that depend on it.
-        The idea is that this explicit argument can be inferred using the type of the named argument one.
-        Note that we also use this approach in the branch where there are no explicit arguments left.
-        This is important to make sure the system behaves in a uniform way.
-        Moreover, users rely on this behavior. For example, consider the example on issue #1851
+        We treat the explicit argument `argName` as implicit
+        if we have a named arguments that depends on it whose `suppressDeps` flag set to `true`.
+        The motivation for this is class projections (issue #1851).
+        In some cases, class projections can have explicit parameters. For example, in
         ```
         class Approx {α : Type} (a : α) (X : Type) : Type where
           val : X
+        ```
+        the type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X`.
+        Note that the parameter `a` is explicit since there is no way to infer it from the expected
+        type or from the types of other explicit parameters.
+        Being a parameter of the class, `a` is determined by the type of `self`.
 
-        variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] [x : Approx x' X]
-
-        #check f.val
-        #check f.val x.val
+        Consider
+        ```
+        variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)]
         ```
-        The type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X`
-        Note that the argument `a` is explicit since there is no way to infer it from the expected
-        type or the type of other explicit arguments.
-        Recall that `f.val` is sugar for `Approx.val (self := f)`. In both `#check` commands above
-        the user assumed that `a` does not need to be provided since it can be inferred from the type
-        of `self`.
-        We used to that only in the branch where `(← get).args` was empty, but it created an asymmetry
-        because `#check f.val` worked as expected, but one would have to write `#check f.val _ x.val`
+        Recall that `f.val` is, to first approximation, sugar for `Approx.val (self := f)`.
+        Without further refinement, this would expand to `fun f'' : α → β => Approx.val f'' f`,
+        which is a type error, since `f''` must be defeq to `f'`.
+        Furthermore, with projection notation, users expect all structure parameters
+        to be uniformly implicit; after all, they are determined by `self`.
+        To handle this, the `(self := f)` named argument is annotated with the `suppressDeps` flag.
+        This causes the `a` parameter to become implicit, and `f.val` instead expands to `Approx.val f' f`.
+
+        This feature previously was enabled for *all* explicit arguments, which confused users
+        and was frequently reported as a bug (issue #1867).
+        Now it is only enabled for the `self` argument in structure projections.
+
+        We used to do this only when `(← get).args` was empty,
+        but it created an asymmetry because `f.val` worked as expected,
+        yet one would have to write `f.val _ x` when there are further arguments.
         -/
         return (← addImplicitArg argName)
       propagateExpectedType arg
@@ -609,17 +627,20 @@ mutual
       | false, _, some _ =>
         throwError "invalid autoParam, argument must be a constant"
       | _, _, _ =>
-        if !(← get).namedArgs.isEmpty then
-          if (← anyNamedArgDependsOnCurrent) then
-            addImplicitArg argName
-          else if (← read).ellipsis then
+        if (← read).ellipsis then
+          addImplicitArg argName
+        else if !(← get).namedArgs.isEmpty then
+          if let some _ ← findNamedArgDependsOnCurrent? then
+            /-
+            Dependencies of named arguments cannot be turned into eta arguments
+            since they are determined by the named arguments.
+            Instead we can turn them into implicit arguments.
+            -/
             addImplicitArg argName
           else
             addEtaArg argName
         else if !(← read).explicit then
-          if (← read).ellipsis then
-            addImplicitArg argName
-          else if (← fTypeHasOptAutoParams) then
+          if (← fTypeHasOptAutoParams) then
             addEtaArg argName
           else
             finalize
@@ -647,37 +668,17 @@ mutual
       finalize
 
   /--
-    Process a `fType` of the form `[x : A] → B x`.
-    This method assume `fType` is a function type -/
+  Process a `fType` of the form `[x : A] → B x`.
+  This method assume `fType` is a function type.
+  -/
   private partial def processInstImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      if (← anyNamedArgDependsOnCurrent) then
-        /-
-        See the note in processExplicitArg about `anyNamedArgDependsOnCurrent`.
-        For consistency, instance implicit arguments should always become implicit if a named argument depends on them.
-        If we do not do this check here, then the `nextArgHole?` branch being before `processExplicitArg`
-        would result in counterintuitive behavior.
-        For example, without this block of code, in the following the `_` is optional.
-        When it is omitted, `processExplicitArg` sees that `h` depends on the `Decidable` instance
-        so makes the `Decidable` instance argument become implicit.
-        When it is `_`, the `nextArgHole?` branch allows it to be present.
-        The third example counterintuitively yields a "function expected" error.
-        ```lean
-        theorem foo {p : Prop} [Decidable p] (h : ite p x y = x) : p := sorry
-
-        variable {p : Prop} [Decidable p] {α : Type} (x y : α) (h : ite p x y = x)
-
-        example : p := @foo (h := h)
-        example : p := @foo (h := h) _
-        example : p := @foo (h := h) inferInstance
-        ```
-        -/
-        addImplicitArg argName
-      else if let some stx ← nextArgHole? then
-        /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
+      if let some stx ← nextArgHole? then
+        -- We still use typeclass resolution for `_` arguments.
+        -- This behavior can be suppressed with `(_)`.
         let ty ← getArgExpectedType
         let arg ← mkInstMVar ty
-        addTermInfo' stx arg ty (← getLCtx)
+        addTermInfo' stx arg ty
         modify fun s => { s with args := s.args.tail! }
         main
       else
@@ -1278,7 +1279,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name
     let mut e := e
     for projFunName in path do
       let projFn ← mkConst projFunName
-      e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false)
+      e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e, suppressDeps := true }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false)
     return e
 
 private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
@@ -1362,10 +1363,10 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
         let projFn ← mkConst info.projFn
         let projFn ← addProjTermInfo lval.getRef projFn
         if lvals.isEmpty then
-          let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f }
+          let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true }
           elabAppArgs projFn namedArgs args expectedType? explicit ellipsis
         else
-          let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
+          let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false)
           loop f lvals
       else
         unreachable!

src/Lean/Elab/Arg.lean

@@ -9,18 +9,22 @@ import Lean.Elab.Term
 namespace Lean.Elab.Term
 
 /--
-  Auxiliary inductive datatype for combining unelaborated syntax
-  and already elaborated expressions. It is used to elaborate applications. -/
+Auxiliary inductive datatype for combining unelaborated syntax
+and already elaborated expressions. It is used to elaborate applications.
+-/
 inductive Arg where
   | stx  (val : Syntax)
   | expr (val : Expr)
   deriving Inhabited
 
-/-- Named arguments created using the notation `(x := val)` -/
+/-- Named arguments created using the notation `(x := val)`. -/
 structure NamedArg where
   ref  : Syntax := Syntax.missing
   name : Name
   val  : Arg
+  /-- If `true`, then make all parameters that depend on this one become implicit.
+  This is used for projection notation, since structure parameters might be explicit for classes. -/
+  suppressDeps : Bool := false
   deriving Inhabited
 
 /--

tests/lean/run/270.lean

@@ -23,7 +23,7 @@ theorem addComm5 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := b
     have h' := congrArg (a + ·) h;
     simp at h';
     rw [←addAssoc] at h';
-    rw [←@addAssoc (a := a)] at h';
+    rw [←addAssoc (a := a)] at h';
     exact h';
 }
 

tests/lean/run/computedFields.lean

@@ -32,9 +32,9 @@ inductive B.C (α : Type u) : Nat → Type u
 with
   @[computed_field] hash : ∀ α i, C α i → UInt64
     | _, _, .a => 1
-    | _, _, .b c => 42 + c.hash
+    | _, _, .b c => 42 + c.hash _ _
 
-#guard (B.C.b (α := Nat) (.a) (d := .a)).hash == 43
+#guard (B.C.b (α := Nat) (.a) (d := .a)).hash _ _ == 43
 
 end WithIndices
 

tests/lean/run/explicitApp.lean

@@ -5,23 +5,26 @@
 namespace Test1
 
 /-!
-Named arguments in explicit mode cause arguments it depends on to become implicit.
-However, inst implicit arguments had odd behavior with `_`, since supplying `_` would override
-the fact that it should be implicit.
+Named arguments in explicit mode should not cause arguments they depend on to become implicit,
+unless there are no more positional arguments.
 -/
 
 theorem foo {p : Prop} [Decidable p] (h : ite p x y = x) : p := sorry
 
 variable {p : Prop} [Decidable p] {α : Type} (x y : α) (h : ite p x y = x)
 
+
 example : p := @foo (h := h)
+
+example : p := @foo (h := h) _ _ _ _ _
+
 /--
 error: function expected at
   foo h
 term has type
   p
 -/
 #guard_msgs in
-example : p := @foo (h := h) _
+example : p := @foo (h := h) _ _ _ _ _ _
 
 end Test1

tests/lean/run/missingExplicitWithForwardNamedDep.lean

@@ -0,0 +1,33 @@
+class Foo (α : Type) (β : Type)  where
+  val : Nat
+  a   : α
+  b   : β
+
+/-- info: Foo.val (α β : Type) [self : Foo α β] : Nat -/
+#guard_msgs in #check Foo.val
+
+def valOf [s : Foo α β] : Nat :=
+  s.val
+
+/-- info: 10 -/
+#guard_msgs in #eval valOf (s := { val := 10, a := true, b := false : Foo Bool Bool })
+
+def valOf2 (α β : Type) [s : Foo α β] : Nat :=
+  s.val
+
+/-- info: valOf2 Bool Bool : Nat -/
+#guard_msgs in #check valOf2 (s := { val := 10, a := true, b := false : Foo Bool Bool })
+
+def f (x y z : Nat) := x + y + z
+
+/-- info: fun x y => f x y 10 : Nat → Nat → Nat -/
+#guard_msgs in
+#check f (z := 10)
+
+def g {α : Type} (a b : α) := b
+/-- info: fun a => g a 10 : Nat → Nat -/
+#guard_msgs in #check g (b := 10)
+
+def h (α : Type) (a b : α) := b
+/-- info: fun a => h Bool a true : Bool → Bool -/
+#guard_msgs in #check h (b := true)

tests/lean/run/structuralMutual.lean

@@ -185,12 +185,12 @@ inductive B (m : Nat) : Nat → Type
 end
 
 mutual
-def A.size (m n : Nat) : A m n → Nat
+def A.size {m n : Nat} : A m n → Nat
   | .self a => a.size + m
   | .other b => b.size + m
   | .empty => 0
 termination_by structural x => x
-def B.size (m n : Nat): B m n → Nat
+def B.size {m n : Nat} : B m n → Nat
   | .self b => b.size + m
   | .other a => a.size + m
   | .empty => 0
@@ -470,7 +470,7 @@ error: cannot use specified parameter for structural recursion:
   which does not come before the varying parameters and before the indices of the recursion parameter.
 -/
 #guard_msgs in
-def T.a (n : Nat) : T n n → Nat
+def T.a {n : Nat} : T n n → Nat
   | .z => 0
   | .n t => t.a + 1
 termination_by structural t => t