feat: improve implicit lambdas

src/Init/Lean/Elab/App.lean

@@ -494,17 +494,8 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na
     -- Remark: `id.<namedPattern>` should already have been expanded
     us ← if us.isEmpty then pure [] else elabExplicitUniv (us.get! 0);
     elabAppFnId ref id us lvals namedArgs args expectedType? explicit acc
-  | `(@($f:fun)) => do
-    s ← observing $ do {
-      if lvals.isEmpty && namedArgs.isEmpty && args.isEmpty then
-        elabFunCore f expectedType? true
-      else do
-        f ← elabFunCore f none true;
-        elabAppLVals ref f lvals namedArgs args expectedType? true
-    };
-    pure $ acc.push s
-  | `(@$f) =>
-    elabAppFn f lvals namedArgs args expectedType? true acc
+  | `(@$id:id) =>
+    elabAppFn id lvals namedArgs args expectedType? true acc
   | _ => do
     s ← observing $ do {
       f ← elabTerm f none;
@@ -580,7 +571,18 @@ def elabAtom : TermElab :=
 fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?
 
 @[builtinTermElab «id»] def elabId : TermElab := elabAtom
-@[builtinTermElab explicit] def elabExplicit : TermElab := elabAtom
+
+@[builtinTermElab explicit] def elabExplicit : TermElab :=
+fun stx expectedType? => match_syntax stx with
+  | `(@$f:fun)           => elabFunCore f expectedType? true
+  | `(@($f:fun))         => elabFunCore f expectedType? true
+  | `(@($f:fun : $type)) => do
+    type ← elabType type;
+    f ← elabFunCore f type true;
+    ensureHasType stx type f
+  | `(@$id:id)          => elabAtom stx expectedType?
+  | _                   => throwUnsupportedSyntax
+
 @[builtinTermElab choice] def elabChoice : TermElab := elabAtom
 @[builtinTermElab proj] def elabProj : TermElab := elabAtom
 @[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom
@@ -588,11 +590,6 @@ fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType?
    but it is nice to have a handler for them because it allows `macros` to insert them into terms. -/
 @[builtinTermElab ident] def elabRawIdent : TermElab := elabAtom
 
-@[builtinTermElab «fun»] def elabFun : TermElab :=
-fun stx expectedType? => do
-  f ← elabFunCore stx expectedType? false;
-  elabAppArgs stx f #[] #[] none false
-
 @[builtinTermElab sortApp] def elabSortApp : TermElab :=
 fun stx _ => do
   u ← elabLevel (stx.getArg 1);

src/Init/Lean/Elab/Binders.lean

@@ -243,7 +243,6 @@ expandFunBindersAux binders body 0 #[]
 namespace FunBinders
 
 structure State :=
-(implicitArgs  : Array Expr := #[])
 (fvars         : Array Expr := #[])
 (lctx          : LocalContext)
 (localInsts    : LocalInstances)
@@ -267,20 +266,29 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat
   if h : i < binderViews.size then
     let binderView := binderViews.get ⟨i, h⟩;
     withLCtx s.lctx s.localInsts $ do
+      let s     := if binderView.bi.isExplicit then { explicit := true, .. s } else s;
       type       ← elabType binderView.type;
-      fvarId     ← mkFreshFVarId;
+      fvarId ← mkFreshFVarId;
       let fvar  := mkFVar fvarId;
-      let fvars := s.fvars.push fvar;
-      -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
-      let lctx  := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
-      s ← propagateExpectedType binderView.id fvar type s;
-      className? ← isClass binderView.type type;
-      match className? with
-      | none           => elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, .. s }
-      | some className => do
-        resetSynthInstanceCache;
-        let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId };
-        elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, localInsts := localInsts, .. s }
+      let s     := { fvars := s.fvars.push fvar, .. s };
+      let continue (s : State) : TermElabM State := do {
+        className? ← isClass binderView.type type;
+        match className? with
+        | none           => elabFunBinderViews (i+1) s
+        | some className => do
+          resetSynthInstanceCache;
+          let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId };
+          elabFunBinderViews (i+1) { localInsts := localInsts, .. s }
+      };
+      if s.explicit then do
+        -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type);
+        let lctx  := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi;
+        s ← propagateExpectedType binderView.id fvar type s;
+        continue { lctx := lctx, .. s }
+      else do
+        mvar ← mkFreshExprMVar binderView.id type;
+        let lctx := s.lctx.mkLetDecl fvarId binderView.id.getId type mvar;
+        continue { lctx := lctx, .. s }
   else
     pure s
 
@@ -314,6 +322,9 @@ elabFunBinders binders expectedType? explicit $ fun xs expectedType? => do {
   mkLambda stx xs e
 }
 
+@[builtinTermElab «fun»] def elabFun : TermElab :=
+fun stx expectedType? => elabFunCore stx expectedType? false
+
 /-
   Recall that
   ```

tests/lean/run/newfrontend5.lean

@@ -0,0 +1,52 @@
+def foo {α} (f : forall {β}, β → β) (a : α) : α :=
+f a
+
+new_frontend
+
+#check_failure let g := id; foo g true -- fails
+/-
+Expands to
+```
+let g : ?γ → ?γ := @id ?γ;
+@foo ?α (fun (β : Sort ?u) => g) true
+```
+
+Unification constraint
+```
+  ?γ → ?γ =?= β → β
+```
+fails because `β` is not in the scope of `?γ`
+
+Error message can be improved because it doesn't make it clear
+the issue is the scope of the metavariable. Not sure yet how to improve it.
+-/
+#check_failure (fun g => foo g 2) id -- fails for the same reason the previous one fail.
+
+#check let g := @id; foo @g true -- works
+/-
+Expands into
+```
+let g : {γ : Sort ?v} → γ → γ := @id;
+@foo ?α @g true
+```
+Note that `@g` also disables implicit lambdas.
+The unification constraint is easily solved
+```
+{γ : Sort ?v} → γ → γ =?= {β : Sort ?u} → β → β
+```
+-/
+
+#check foo id true  -- works
+#check foo @id true -- works
+#check foo (fun b => b) true -- works
+#check foo (fun {β} b => b) true -- works
+#check_failure foo @(fun b => b) true     -- fails as expected, and error message is clear
+#check foo @(fun β b => b) true   -- works (implicit lambdas were disabled)
+#check foo @(fun {β} b => b) true -- works (implicit lambdas were disabled)
+
+
+set_option pp.all true
+
+#check let x := (fun f => (f, f)) @id; (x.1 (), x.2 true) -- works
+#check_failure let x := (fun f => (f, f)) id; (x.1 (), x.2 true) -- fails as expected
+#check let x := (fun (f : {α : Type} → α → α) => (f, f)) @id; (x.1 (), x.2 true) -- works