squashed 3fb427e

src/Lean/Elab/App.lean

@@ -145,6 +145,8 @@ structure State where
     When `..` is used, eta-expansion is disabled, and missing arguments are treated as `_`.
   -/
   etaArgs              : Array Expr   := #[]
+  /-- Missing explicit arguments, from dependencies of named arguments. These cannot be eta arguments. -/
+  missingExplicits     : Array Expr   := #[]
   /-- Metavariables that we need to set the error context using the application being built. -/
   toSetErrorCtx        : Array MVarId := #[]
   /-- Metavariables for the instance implicit arguments that have already been processed. -/
@@ -378,6 +380,13 @@ private def finalize : M Expr := do
   -- Register the error context of implicits
   for mvarId in s.toSetErrorCtx do
     registerMVarErrorImplicitArgInfo mvarId ref e
+  unless s.missingExplicits.isEmpty do
+    let mes := s.missingExplicits.map fun e => m!"{indentExpr e}"
+    logError m!"insufficient number of arguments, \
+      missing {s.missingExplicits.size} explicit argument(s) that are dependencies of a named argument.\n\n\
+      Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. \
+      These are the inferred missing arguments:\
+      {MessageData.joinSep mes.toList ""}"
   if !s.etaArgs.isEmpty then
     e ← mkLambdaFVars s.etaArgs e
   /-
@@ -411,33 +420,38 @@ 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`.
+If `onlySuppressDeps` is true, then only returns such a named argument with `suppressDeps` true.
+-/
+private def anyNamedArgDependsOnCurrent? (onlySuppressDeps := true) : M (Option NamedArg) := do
   let s ← get
-  if s.namedArgs.isEmpty then
-    return false
-  else
+  if s.namedArgs.any (·.suppressDeps || !onlySuppressDeps) then
     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.suppressDeps || !onlySuppressDeps) && 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
+  else
+    return none
 
 
 /-- Return `true` if there are regular or named arguments to be processed. -/
 private def hasArgsToProcess : M Bool := do
   let s ← get
   return !s.args.isEmpty || !s.namedArgs.isEmpty
 
-/-- Return `true` if the next argument at `args` is of the form `_` -/
-private def isNextArgHole : M Bool := do
+/--
+Returns the argument syntax if the next argument at `args` is of the form `_`.
+-/
+private def nextArgHole? : M (Option Syntax) := do
   match (← get).args with
-  | Arg.stx (Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure true
-  | _ => pure false
+  | Arg.stx stx@(Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure stx
+  | _ => pure none
 
 /--
   Return `true` if the next argument to be processed is the outparam of a local instance, and it the result type
@@ -522,7 +536,7 @@ mutual
       addNewArg argName x
       main
 
-  private partial def addImplicitArg (argName : Name) : M Expr := do
+  private partial def addImplicitArg (argName : Name) (missingExplicit : Bool := false) : M Expr := do
     let argType ← getArgExpectedType
     let arg ← if (← isNextOutParamOfLocalInstanceAndResult) then
       let arg ← mkFreshExprMVar argType
@@ -535,6 +549,8 @@ mutual
     else
       mkFreshExprMVar argType
     modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! }
+    if missingExplicit then
+      modify fun s => { s with missingExplicits := s.missingExplicits.push arg }
     addNewArg argName arg
     main
 
@@ -544,13 +560,16 @@ mutual
   private partial def processExplicitArg (argName : Name) : M Expr := do
     match (← get).args with
     | arg::args =>
-      if (← anyNamedArgDependsOnCurrent) then
+      if ← pure !(← read).explicit <&&> Option.isSome <$> anyNamedArgDependsOnCurrent? 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.
+        We treat the explicit argument `argName` as implicit if we have a named arguments that depends on it
+        that has the `suppressDeps` flag set to `true`.
+        The idea is that this explicit argument can be inferred using the type of the named argument.
         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
+
+        The motivation is that class projections can have explicit type parameters.
+        For example, consider the example on issue #1851
         ```
         class Approx {α : Type} (a : α) (X : Type) : Type where
           val : X
@@ -566,8 +585,9 @@ mutual
         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`.
+        Setting `suppressDeps` for this `self` argument enables this feature.
         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`
+        because `#check f.val` worked as expected, but one would have to write `#check f.val _ x.val`.
         -/
         return (← addImplicitArg argName)
       propagateExpectedType arg
@@ -604,8 +624,14 @@ mutual
         throwError "invalid autoParam, argument must be a constant"
       | _, _, _ =>
         if !(← get).namedArgs.isEmpty then
-          if (← anyNamedArgDependsOnCurrent) then
-            addImplicitArg argName
+          if let some arg ← anyNamedArgDependsOnCurrent? (onlySuppressDeps := false) then
+            /-
+            Dependencies of named arguments cannot be turned into eta arguments.
+            Doing so leads to confusing type errors.
+            However, they can safely be turned into implicit arguments for elaboration.
+            This is an error unless the named argument is meant to suppress dependencies.
+            -/
+            addImplicitArg argName (missingExplicit := (← read).explicit || !arg.suppressDeps)
           else if (← read).ellipsis then
             addImplicitArg argName
           else
@@ -645,20 +671,24 @@ mutual
     This method assume `fType` is a function type -/
   private partial def processInstImplicitArg (argName : Name) : M Expr := do
     if (← read).explicit then
-      if (← isNextArgHole) then
+      if let some stx ← nextArgHole? then
         /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
-        let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+        let ty ← getArgExpectedType
+        let arg ← mkInstMVar ty
+        addTermInfo' stx arg ty (← getLCtx)
         modify fun s => { s with args := s.args.tail! }
-        addInstMVar arg.mvarId!
-        addNewArg argName arg
         main
       else
         processExplicitArg argName
     else
-      let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+      discard <| mkInstMVar (← getArgExpectedType)
+      main
+  where
+    mkInstMVar (ty : Expr) : M Expr := do
+      let arg ← mkFreshExprMVar ty MetavarKind.synthetic
       addInstMVar arg.mvarId!
       addNewArg argName arg
-      main
+      return arg
 
   /-- Elaborate function application arguments. -/
   partial def main : M Expr := do
@@ -1221,7 +1251,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
@@ -1305,10 +1335,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

@@ -21,6 +21,9 @@ structure NamedArg where
   ref  : Syntax := Syntax.missing
   name : Name
   val  : Arg
+  /-- If `true`, then make all parameters that the corresponding named parameter depends on
+  become implicit. This is used for projection notation to suppress explicit type parameters. -/
+  suppressDeps : Bool := false
   deriving Inhabited
 
 /--

tests/lean/interactive/explicitAppInstHole.lean

@@ -0,0 +1,6 @@
+/-!
+# Make sure there is type information on `_` for inst parameters in explicit mode
+-/
+
+example : Nat := @ite _ True _ 1 2
+                           --^ textDocument/hover

tests/lean/interactive/explicitAppInstHole.lean.expected.out

@@ -0,0 +1,8 @@
+{"textDocument": {"uri": "file:///explicitAppInstHole.lean"},
+ "position": {"line": 4, "character": 29}}
+{"range":
+ {"start": {"line": 4, "character": 29}, "end": {"line": 4, "character": 30}},
+ "contents":
+ {"value":
+  "```lean\ninstDecidableTrue : Decidable True\n```\n***\nA placeholder term, to be synthesized by unification. \n***\n*import Init.Core*",
+  "kind": "markdown"}}

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

@@ -0,0 +1,41 @@
+/-!
+# Tests for app elaborator in explicit mode
+-/
+
+namespace Test1
+
+/-!
+Named arguments in explicit mode should not cause arguments they depend on to become implicit,
+except when doing error recovery.
+-/
+
+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)
+
+
+/--
+error: insufficient number of arguments, missing 5 explicit argument(s) that are dependencies of a named argument.
+
+Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument.
+These are the inferred missing arguments:
+  α
+  x
+  y
+  p
+  inst✝
+-/
+#guard_msgs in 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) _ _ _ _ _ _
+
+end Test1

tests/lean/run/missingExplicitWithForwardNamedDep.lean

@@ -0,0 +1,48 @@
+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
+
+/--
+error: insufficient number of arguments, missing 2 explicit argument(s) that are dependencies of a named argument.
+
+Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. These are the inferred missing arguments:
+  Bool
+  Bool
+---
+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
+/--
+error: insufficient number of arguments, missing 1 explicit argument(s) that are dependencies of a named argument.
+
+Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. These are the inferred missing arguments:
+  Bool
+---
+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