From dc670bfd5dc6194ed91f168e9ad59f05dc2bd59e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 11 Oct 2020 15:24:55 -0700
Subject: [PATCH] fix: handle `optParam` at `consumeImplicits`

`consumeImplicits` is used during LVal resolution.
---
 src/Lean/Elab/App.lean       |  6 ++++--
 tests/compiler/lazylist.lean |  4 ++--
 tests/lean/run/optParam.lean | 19 +++++++++++++++++++
 3 files changed, 25 insertions(+), 4 deletions(-)
 create mode 100644 tests/lean/run/optParam.lean

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index e9978d5664..62a621c575 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -534,8 +534,10 @@ private partial def consumeImplicits : Expr → Expr → TermElabM (Expr × Expr
     if !c.binderInfo.isExplicit then do
       mvar ← mkFreshExprMVar d;
       consumeImplicits (mkApp e mvar) (b.instantiate1 mvar)
-    else
-      pure (e, eType)
+    else match d.getOptParamDefault? with
+      | some defVal => consumeImplicits (mkApp e defVal) (b.instantiate1 defVal)
+      -- TODO: we do not handle autoParams here.
+      | _ => pure (e, eType)
   | _ => pure (e, eType)
 
 private partial def resolveLValLoop (lval : LVal) : Expr → Expr → Array Exception → TermElabM (Expr × LValResolution)
diff --git a/tests/compiler/lazylist.lean b/tests/compiler/lazylist.lean
index 17df476cbe..33730b802c 100644
--- a/tests/compiler/lazylist.lean
+++ b/tests/compiler/lazylist.lean
@@ -124,5 +124,5 @@ def main : IO Unit := do
 let n := 40;
 IO.println tst.isEmpty;
 IO.println tst.head;
-IO.println $ fib.interleave ((iota 0).map (· + 100)) $.approx n;
-IO.println $ (iota 0).map (· + 10) $.filter (· % 2 == 0) $.approx n
+IO.println $ fib.interleave (iota.map (· + 100)) $.approx n;
+IO.println $ iota.map (· + 10) $.filter (· % 2 == 0) $.approx n
diff --git a/tests/lean/run/optParam.lean b/tests/lean/run/optParam.lean
new file mode 100644
index 0000000000..fe7b4e65e1
--- /dev/null
+++ b/tests/lean/run/optParam.lean
@@ -0,0 +1,19 @@
+new_frontend
+
+def p (x : Nat := 0) : Nat × Nat :=
+(x, x)
+
+theorem ex1 : p.1 = 0 :=
+rfl
+
+theorem ex2 : p (x := 1) $.2 = 1 :=
+rfl
+
+def c {α : Type} [Inhabited α] : α × α :=
+(arbitrary _, arbitrary _)
+
+theorem ex3 {α} [Inhabited α] : c.1 = arbitrary α :=
+rfl
+
+theorem ex4 {α} [Inhabited α] : c.2 = arbitrary α :=
+rfl