fix: handle optParam at consumeImplicits

`consumeImplicits` is used during LVal resolution.

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)

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

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