From a5ab59a413df6b2fca2c6909aea878d19c3ad8af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Nov 2022 07:01:02 -0800
Subject: [PATCH] fix: fixes #1851

---
 src/Lean/Elab/App.lean     | 27 +++++++++++++++++++++++++++
 tests/lean/elabAsElim.lean |  3 +--
 tests/lean/run/1851.lean   | 12 ++++++++++++
 3 files changed, 40 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/1851.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 81409cf25d..619feaf989 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -527,6 +527,33 @@ mutual
   private partial def processExplictArg (argName : Name) : M Expr := do
     match (← get).args with
     | arg::args =>
+      unless (← get).namedArgs.isEmpty do
+        if (← 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.
+          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
+          ```
+          class Approx {α : Type} (a : α) (X : Type) : Type where
+            val : X
+
+          variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] [x : Approx x' X]
+
+          #check f.val 
+          #check f.val x.val
+          ```
+          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`
+          -/
+          return (← addImplicitArg argName)
       propagateExpectedType arg
       modify fun s => { s with args }
       elabAndAddNewArg argName arg
diff --git a/tests/lean/elabAsElim.lean b/tests/lean/elabAsElim.lean
index 2582321b69..1b1352bd97 100644
--- a/tests/lean/elabAsElim.lean
+++ b/tests/lean/elabAsElim.lean
@@ -26,7 +26,7 @@ def f7 (xs : Vec α n) : Nat :=
   xs.casesOn (a := 10) 0 -- Error unused named args
 
 def f8 (xs : List Nat) : xs ≠ [] → xs.length > 0 :=
-  @List.casesOn _ (motive := fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
+  @List.casesOn _ (fun xs => xs ≠ [] → xs.length > 0) xs (by dsimp; intros; contradiction) (by dsimp; intros; simp_arith)
 
 def f5' (xs : List Nat) (h : xs ≠ []) : xs.length > 0 :=
   xs.casesOn (fun h => absurd rfl h) (fun _ _ _ => Nat.zero_lt_succ ..) h
@@ -87,4 +87,3 @@ noncomputable def f : Nat → Nat :=
 
 example : ∀ x, x ≥ 0 :=
   Nat.rec (Nat.le_refl 0) (fun _ ih => Nat.le_succ_of_le ih)
-
diff --git a/tests/lean/run/1851.lean b/tests/lean/run/1851.lean
new file mode 100644
index 0000000000..467833032b
--- /dev/null
+++ b/tests/lean/run/1851.lean
@@ -0,0 +1,12 @@
+class Approx {α : Type} (a : α) (X : Type) : Type where
+  val : X
+
+variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] [x : Approx x' X]
+
+-- fails
+#check f.val x.val
+
+-- works
+#check let f'' := f.val
+       let x'' := x.val
+       f'' x''