diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean
index 67c0d27488..be65fe1d62 100644
--- a/src/Lean/Meta/DiscrTree.lean
+++ b/src/Lean/Meta/DiscrTree.lean
@@ -483,15 +483,20 @@ partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α 
     let (k, args) ← getMatchKeyArgs e (root := true)
     match k with
     | Key.star => return result
-    | _        => process k args 0 result
+    | _        => process k args.toSubarray 0 result
 where
-  process (k : Key) (args : Array Expr) (numExtraArgs : Nat) (result : Array (α × Nat)) : MetaM (Array (α × Nat)) := do
-    let result := result ++ ((← getMatchRoot d k args #[]).map (., numExtraArgs))
+  process (k : Key) (args : Subarray Expr) (numExtraArgs : Nat) (result : Array (α × Nat)) : MetaM (Array (α × Nat)) := do
+    -- Remark: the args are stored in reverse order
+    let result :=
+      if d.root.find? k |>.isSome then
+        result ++ ((← getMatchRoot d k args.toArray #[]).map (., numExtraArgs))
+      else
+        result
     match k with
     | Key.const f 0     => return result
-    | Key.const f (n+1) => process (Key.const f n) args.pop (numExtraArgs + 1) result
+    | Key.const f (n+1) => process (Key.const f n) args.popFront (numExtraArgs + 1) result
     | Key.fvar f 0      => return result
-    | Key.fvar f (n+1)  => process (Key.fvar f n) args.pop (numExtraArgs + 1) result
+    | Key.fvar f (n+1)  => process (Key.fvar f n) args.popFront (numExtraArgs + 1) result
     | _                 => return result
 
 partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
diff --git a/tests/lean/run/simpPartialApp.lean b/tests/lean/run/simpPartialApp.lean
new file mode 100644
index 0000000000..12a8be78a0
--- /dev/null
+++ b/tests/lean/run/simpPartialApp.lean
@@ -0,0 +1,9 @@
+variable {U V}
+
+def f : (U → V) → (U → U) := sorry
+def add  {U} : U → U → U := sorry
+
+@[simp] theorem foo  (u : U) : f (add u) = id := sorry
+
+def bar (u v : U) : f (add u) v =  id v := by
+  simp