chore: update stage0

stage0/src/Lean/Elab/App.lean

@@ -282,16 +282,6 @@ private def propagateExpectedType (arg : Arg) : M Unit := do
                   /- Note that we only set `propagateExpected := false` when propagation has succeeded. -/
                   modify fun s => { s with propagateExpected := false }
 
-/-
-  Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
-  and then execute the continuation `k`.-/
-private def addEtaArg (k : M Expr) : M Expr := do
-  let n    ← getBindingName
-  let type ← getArgExpectedType
-  withLocalDeclD n type fun x => do
-    modify fun s => { s with etaArgs := s.etaArgs.push x }
-    addNewArg x
-    k
 
 /- This method execute after all application arguments have been processed. -/
 private def finalize : M Expr := do
@@ -320,13 +310,6 @@ private def finalize : M Expr := do
   synthesizeAppInstMVars
   pure e
 
-private def addImplicitArg (k : M Expr) : M Expr := do
-  let argType ← getArgExpectedType
-  let arg ← mkFreshExprMVar argType
-  modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! }
-  addNewArg arg
-  k
-
 /- Return true if there is a named argument that depends on the next argument. -/
 private def anyNamedArgDependsOnCurrent : M Bool := do
   let s ← get
@@ -342,60 +325,11 @@ private def anyNamedArgDependsOnCurrent : M Bool := do
             return true
       return false
 
-/-
-  Process a `fType` of the form `(x : A) → B x`.
-  This method assume `fType` is a function type -/
-private def processExplictArg (k : M Expr) : M Expr := do
-  let s ← get
-  match s.args with
-  | arg::args =>
-    propagateExpectedType arg
-    modify fun s => { s with args := args }
-    elabAndAddNewArg arg
-    k
-  | _ =>
-    let argType ← getArgExpectedType
-    match s.explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
-    | false, some defVal, _  => addNewArg defVal; k
-    | false, _, some (Expr.const tacticDecl _ _) =>
-      let env ← getEnv
-      let opts ← getOptions
-      match evalSyntaxConstant env opts tacticDecl with
-      | Except.error err       => throwError err
-      | Except.ok tacticSyntax =>
-        -- TODO(Leo): does this work correctly for tactic sequences?
-        let tacticBlock ← `(by $tacticSyntax)
-        let argType     := argType.getArg! 0 -- `autoParam type := by tactic` ==> `type`
-        let argNew := Arg.stx tacticBlock
-        propagateExpectedType argNew
-        elabAndAddNewArg argNew
-        k
-    | false, _, some _ =>
-      throwError "invalid autoParam, argument must be a constant"
-    | _, _, _ =>
-      if !s.namedArgs.isEmpty then
-        if (← anyNamedArgDependsOnCurrent) then
-          addImplicitArg k
-        else
-          addEtaArg k
-      else if !s.explicit then
-        if (← fTypeHasOptAutoParams) then
-          addEtaArg k
-        else if (← get).ellipsis then
-          addImplicitArg k
-        else
-          finalize
-      else
-        finalize
 
-/-
-  Process a `fType` of the form `{x : A} → B x`.
-  This method assume `fType` is a function type -/
-private def processImplicitArg (k : M Expr) : M Expr := do
-  if (← get).explicit then
-    processExplictArg k
-  else
-    addImplicitArg k
+/- Return true if there are regular or named arguments to be processed. -/
+private def hasArgsToProcess : M Bool := do
+  let s ← get
+  return !s.args.isEmpty || !s.namedArgs.isEmpty
 
 /- Return true if the next argument at `args` is of the form `_` -/
 private def isNextArgHole : M Bool := do
@@ -403,55 +337,139 @@ private def isNextArgHole : M Bool := do
   | Arg.stx (Syntax.node ``Lean.Parser.Term.hole _) :: _ => pure true
   | _ => pure false
 
-/-
-  Process a `fType` of the form `[x : A] → B x`.
-  This method assume `fType` is a function type -/
-private def processInstImplicitArg (k : M Expr) : M Expr := do
-  if (← get).explicit then
-    if (← isNextArgHole) then
-      /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
+
+mutual
+  /-
+    Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`,
+    and then execute the main loop.-/
+  private partial def addEtaArg : M Expr := do
+    let n    ← getBindingName
+    let type ← getArgExpectedType
+    withLocalDeclD n type fun x => do
+      modify fun s => { s with etaArgs := s.etaArgs.push x }
+      addNewArg x
+      main
+
+  private partial def addImplicitArg : M Expr := do
+    let argType ← getArgExpectedType
+    let arg ← mkFreshExprMVar argType
+    modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! }
+    addNewArg arg
+    main
+
+  /-
+    Process a `fType` of the form `(x : A) → B x`.
+    This method assume `fType` is a function type -/
+  private partial def processExplictArg : M Expr := do
+    let s ← get
+    match s.args with
+    | arg::args =>
+      propagateExpectedType arg
+      modify fun s => { s with args := args }
+      elabAndAddNewArg arg
+      main
+    | _ =>
+      let argType ← getArgExpectedType
+      match s.explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
+      | false, some defVal, _  => addNewArg defVal; main
+      | false, _, some (Expr.const tacticDecl _ _) =>
+        let env ← getEnv
+        let opts ← getOptions
+        match evalSyntaxConstant env opts tacticDecl with
+        | Except.error err       => throwError err
+        | Except.ok tacticSyntax =>
+          -- TODO(Leo): does this work correctly for tactic sequences?
+          let tacticBlock ← `(by $tacticSyntax)
+          let argType     := argType.getArg! 0 -- `autoParam type := by tactic` ==> `type`
+          let argNew := Arg.stx tacticBlock
+          propagateExpectedType argNew
+          elabAndAddNewArg argNew
+          main
+      | false, _, some _ =>
+        throwError "invalid autoParam, argument must be a constant"
+      | _, _, _ =>
+        if !s.namedArgs.isEmpty then
+          if (← anyNamedArgDependsOnCurrent) then
+            addImplicitArg
+          else
+            addEtaArg
+        else if !s.explicit then
+          if (← fTypeHasOptAutoParams) then
+            addEtaArg
+          else if (← get).ellipsis then
+            addImplicitArg
+          else
+            finalize
+        else
+          finalize
+
+  /-
+    Process a `fType` of the form `{x : A} → B x`.
+    This method assume `fType` is a function type -/
+  private partial def processImplicitArg : M Expr := do
+    if (← get).explicit then
+      processExplictArg
+    else
+      addImplicitArg
+
+  /-
+    Process a `fType` of the form `{{x : A}} → B x`.
+    This method assume `fType` is a function type -/
+  private partial def processStrictImplicitArg : M Expr := do
+    if (← get).explicit then
+      processExplictArg
+    else if (← hasArgsToProcess) then
+      addImplicitArg
+    else
+      finalize
+
+  /-
+    Process a `fType` of the form `[x : A] → B x`.
+    This method assume `fType` is a function type -/
+  private partial def processInstImplicitArg : M Expr := do
+    if (← get).explicit then
+      if (← isNextArgHole) then
+        /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
+        let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
+        modify fun s => { s with args := s.args.tail! }
+        addInstMVar arg.mvarId!
+        addNewArg arg
+        main
+      else
+        processExplictArg
+    else
       let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
-      modify fun s => { s with args := s.args.tail! }
       addInstMVar arg.mvarId!
       addNewArg arg
-      k
-    else
-      processExplictArg k
-  else
-    let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
-    addInstMVar arg.mvarId!
-    addNewArg arg
-    k
-
-/- Return true if there are regular or named arguments to be processed. -/
-private def hasArgsToProcess : M Bool := do
-  let s ← get
-  pure $ !s.args.isEmpty || !s.namedArgs.isEmpty
-
-/- Elaborate function application arguments. -/
-partial def main : M Expr := do
-  let s ← get
-  let fType ← normalizeFunType
-  if fType.isForall then
-    let binderName := fType.bindingName!
-    let binfo := fType.bindingInfo!
-    let s ← get
-    match s.namedArgs.find? fun (namedArg : NamedArg) => namedArg.name == binderName with
-    | some namedArg =>
-      propagateExpectedType namedArg.val
-      eraseNamedArg binderName
-      elabAndAddNewArg namedArg.val
       main
-    | none          =>
-      match binfo with
-      | BinderInfo.implicit     => processImplicitArg main
-      | BinderInfo.instImplicit => processInstImplicitArg main
-      | _                       => processExplictArg main
-  else if (← hasArgsToProcess) then
-    synthesizePendingAndNormalizeFunType
-    main
-  else
-    finalize
+
+  /- Elaborate function application arguments. -/
+  partial def main : M Expr := do
+    let s ← get
+    let fType ← normalizeFunType
+    if fType.isForall then
+      let binderName := fType.bindingName!
+      let binfo := fType.bindingInfo!
+      let s ← get
+      match s.namedArgs.find? fun (namedArg : NamedArg) => namedArg.name == binderName with
+      | some namedArg =>
+        propagateExpectedType namedArg.val
+        eraseNamedArg binderName
+        elabAndAddNewArg namedArg.val
+        main
+      | none          =>
+        match binfo with
+        | BinderInfo.implicit       => processImplicitArg
+        | BinderInfo.instImplicit   => processInstImplicitArg
+        | BinderInfo.strictImplicit => processStrictImplicitArg
+        | _                         => processExplictArg
+    else if (← hasArgsToProcess) then
+      synthesizePendingAndNormalizeFunType
+      main
+    else
+      finalize
+
+end
 
 end ElabAppArgs
 
@@ -572,25 +590,25 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
 
 /- whnfCore + implicit consumption.
    Example: given `e` with `eType := {α : Type} → (fun β => List β) α `, it produces `(e ?m, List ?m)` where `?m` is fresh metavariable. -/
-private partial def consumeImplicits (stx : Syntax) (e eType : Expr) : TermElabM (Expr × Expr) := do
+private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs : Bool) : TermElabM (Expr × Expr) := do
   let eType ← whnfCore eType
   match eType with
   | Expr.forallE n d b c =>
-    if c.binderInfo.isImplicit then
+    if c.binderInfo.isImplicit || (hasArgs && c.binderInfo.isStrictImplicit) then
       let mvar ← mkFreshExprMVar d
       registerMVarErrorHoleInfo mvar.mvarId! stx
-      consumeImplicits stx (mkApp e mvar) (b.instantiate1 mvar)
+      consumeImplicits stx (mkApp e mvar) (b.instantiate1 mvar) hasArgs
     else if c.binderInfo.isInstImplicit then
       let mvar ← mkInstMVar d
-      consumeImplicits stx (mkApp e mvar) (b.instantiate1 mvar)
+      consumeImplicits stx (mkApp e mvar) (b.instantiate1 mvar) hasArgs
     else match d.getOptParamDefault? with
-      | some defVal => consumeImplicits stx (mkApp e defVal) (b.instantiate1 defVal)
+      | some defVal => consumeImplicits stx (mkApp e defVal) (b.instantiate1 defVal) hasArgs
       -- TODO: we do not handle autoParams here.
       | _ => pure (e, eType)
   | _ => pure (e, eType)
 
-private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExceptions : Array Exception) : TermElabM (Expr × LValResolution) := do
-  let (e, eType) ← consumeImplicits lval.getRef e eType
+private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExceptions : Array Exception) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do
+  let (e, eType) ← consumeImplicits lval.getRef e eType hasArgs
   tryPostponeIfMVar eType
   try
     let lvalRes ← resolveLValAux e eType lval
@@ -599,15 +617,15 @@ private partial def resolveLValLoop (lval : LVal) (e eType : Expr) (previousExce
     | ex@(Exception.error _ _) =>
       let eType? ← unfoldDefinition? eType
       match eType? with
-      | some eType => resolveLValLoop lval e eType (previousExceptions.push ex)
+      | some eType => resolveLValLoop lval e eType (previousExceptions.push ex) hasArgs
       | none       =>
         previousExceptions.forM fun ex => logException ex
         throw ex
     | ex@(Exception.internal _ _) => throw ex
 
-private def resolveLVal (e : Expr) (lval : LVal) : TermElabM (Expr × LValResolution) := do
+private def resolveLVal (e : Expr) (lval : LVal) (hasArgs : Bool) : TermElabM (Expr × LValResolution) := do
   let eType ← inferType e
-  resolveLValLoop lval e eType #[]
+  resolveLValLoop lval e eType #[] hasArgs
 
 private partial def mkBaseProjections (baseStructName : Name) (structName : Name) (e : Expr) : TermElabM Expr := do
   let env ← getEnv
@@ -675,7 +693,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
   | f, lval::lvals => do
     if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then
       addDotCompletionInfo targetStx f expectedType? fieldStx
-    let (f, lvalRes) ← resolveLVal f lval
+    let hasArgs := !namedArgs.isEmpty || !args.isEmpty
+    let (f, lvalRes) ← resolveLVal f lval hasArgs
     match lvalRes with
     | LValResolution.projIdx structName idx =>
       let f := mkProj structName idx f

stage0/src/Lean/Elab/Binders.lean

@@ -104,24 +104,29 @@ private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
 
 private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := do
   let k := stx.getKind
-  if k == `Lean.Parser.Term.simpleBinder then
+  if k == ``Lean.Parser.Term.simpleBinder then
     -- binderIdent+ >> optType
     let ids ← getBinderIds stx[0]
     let type := expandOptType (mkNullNode ids) stx[1]
     ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.default }
-  else if k == `Lean.Parser.Term.explicitBinder then
+  else if k == ``Lean.Parser.Term.explicitBinder then
     -- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
     let ids ← getBinderIds stx[1]
     let type        := expandBinderType (mkNullNode ids) stx[2]
     let optModifier := stx[3]
     let type ← expandBinderModifier type optModifier
     ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.default }
-  else if k == `Lean.Parser.Term.implicitBinder then
+  else if k == ``Lean.Parser.Term.implicitBinder then
     -- `{` binderIdent+ binderType `}`
     let ids ← getBinderIds stx[1]
     let type := expandBinderType (mkNullNode ids) stx[2]
     ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.implicit }
-  else if k == `Lean.Parser.Term.instBinder then
+  else if k == ``Lean.Parser.Term.strictImplicitBinder then
+    -- `⦃` binderIdent+ binderType `⦄`
+    let ids ← getBinderIds stx[1]
+    let type := expandBinderType (mkNullNode ids) stx[2]
+    ids.mapM fun id => do pure { id := (← expandBinderIdent id), type := type, bi := BinderInfo.strictImplicit }
+  else if k == ``Lean.Parser.Term.instBinder then
     -- `[` optIdent type `]`
     let id ← expandOptIdent stx[1]
     let type := stx[2]
@@ -256,15 +261,16 @@ partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (
         let newBody ← `(match $major:ident with | $pattern => $newBody)
         pure (binders, newBody, true)
       match binder with
-      | Syntax.node `Lean.Parser.Term.implicitBinder _ => loop body (i+1) (newBinders.push binder)
-      | Syntax.node `Lean.Parser.Term.instBinder _     => loop body (i+1) (newBinders.push binder)
-      | Syntax.node `Lean.Parser.Term.explicitBinder _ => loop body (i+1) (newBinders.push binder)
-      | Syntax.node `Lean.Parser.Term.simpleBinder _   => loop body (i+1) (newBinders.push binder)
-      | Syntax.node `Lean.Parser.Term.hole _ =>
+      | Syntax.node ``Lean.Parser.Term.implicitBinder _       => loop body (i+1) (newBinders.push binder)
+      | Syntax.node ``Lean.Parser.Term.strictImplicitBinder _ => loop body (i+1) (newBinders.push binder)
+      | Syntax.node ``Lean.Parser.Term.instBinder _           => loop body (i+1) (newBinders.push binder)
+      | Syntax.node ``Lean.Parser.Term.explicitBinder _       => loop body (i+1) (newBinders.push binder)
+      | Syntax.node ``Lean.Parser.Term.simpleBinder _         => loop body (i+1) (newBinders.push binder)
+      | Syntax.node ``Lean.Parser.Term.hole _ =>
         let ident ← mkFreshIdent binder
         let type := binder
         loop body (i+1) (newBinders.push <| mkExplicitBinder ident type)
-      | Syntax.node `Lean.Parser.Term.paren args =>
+      | Syntax.node ``Lean.Parser.Term.paren args =>
         -- `(` (termParser >> parenSpecial)? `)`
         -- parenSpecial := (tupleTail <|> typeAscription)?
         let binderBody := binder[1]

stage0/src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -506,10 +506,12 @@ def delabLam : Delab :=
             else
               pure $ curNames.get! 0;
           `(funBinder| ($stxCurNames : $stxT))
-        | BinderInfo.default,     false  => pure curNames.back  -- here `curNames.size == 1`
-        | BinderInfo.implicit,    true   => `(funBinder| {$curNames* : $stxT})
-        | BinderInfo.implicit,    false  => `(funBinder| {$curNames*})
-        | BinderInfo.instImplicit, _     =>
+        | BinderInfo.default,        false  => pure curNames.back  -- here `curNames.size == 1`
+        | BinderInfo.implicit,       true   => `(funBinder| {$curNames* : $stxT})
+        | BinderInfo.implicit,       false  => `(funBinder| {$curNames*})
+        | BinderInfo.strictImplicit, true   => `(funBinder| ⦃$curNames* : $stxT⦄)
+        | BinderInfo.strictImplicit, false  => `(funBinder| ⦃$curNames*⦄)
+        | BinderInfo.instImplicit,   _     =>
           if usedDownstream then `(funBinder| [$curNames.back : $stxT])  -- here `curNames.size == 1`
           else  `(funBinder| [$stxT])
         | _                      , _     => unreachable!;
@@ -524,10 +526,11 @@ def delabForall : Delab :=
     let prop ← try isProp e catch _ => false
     let stxT ← withBindingDomain delab
     let group ← match e.binderInfo with
-    | BinderInfo.implicit     => `(bracketedBinderF|{$curNames* : $stxT})
+    | BinderInfo.implicit       => `(bracketedBinderF|{$curNames* : $stxT})
+    | BinderInfo.strictImplicit => `(bracketedBinderF|⦃$curNames* : $stxT⦄)
     -- here `curNames.size == 1`
-    | BinderInfo.instImplicit => `(bracketedBinderF|[$curNames.back : $stxT])
-    | _                       =>
+    | BinderInfo.instImplicit   => `(bracketedBinderF|[$curNames.back : $stxT])
+    | _                         =>
       -- heuristic: use non-dependent arrows only if possible for whole group to avoid
       -- noisy mix like `(α : Type) → Type → (γ : Type) → ...`.
       let dependent := curNames.any $ fun n => hasIdent n.getId stxBody