From 5d22886aff90967fc684700c7f42fbf9850f9cb6 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Mon, 18 May 2026 07:41:09 -0700 Subject: [PATCH] refactor: app elaborator refactoring and improvements (#13762) This PR does some refactoring of the function application elaborator, and it improves `trace.Elab.app` tracing. It also improves asymptotic complexity by more carefully substituting arguments into the function's type and by changing how named argument dependency suppression is implemented. For dot notation, it now constructs base projections directly rather than using the app elaborator. It fixes a bug in the eta args feature where more explicit arguments would be turned into implicit arguments than expected, and it improves expected type propagation by following the rules from the main app elaborator. --- src/Lean/Elab/App.lean | 599 +++++++++++++++++++++++++---------------- src/Lean/Elab/Arg.lean | 28 +- 2 files changed, 390 insertions(+), 237 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 19da5d0ba6..59274eea48 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -31,14 +31,6 @@ builtin_initialize elabWithoutExpectedTypeAttr : TagAttribute ← def hasElabWithoutExpectedType (env : Environment) (declName : Name) : Bool := elabWithoutExpectedTypeAttr.hasTag env declName -instance : ToString Arg where - toString - | .stx val => toString val - | .expr val => toString val - -instance : ToString NamedArg where - toString s := "(" ++ toString s.name ++ " := " ++ toString s.val ++ ")" - def throwInvalidNamedArg (namedArg : NamedArg) (fn? : Option Name) (validNames : Array Name) : TermElabM α := do let hint ← do if validNames.size > 0 then @@ -87,7 +79,7 @@ def synthesizeAppInstMVars (instMVars : Array MVarId) (app : Expr) : TermElabM U registerMVarErrorImplicitArgInfo mvarId (← getRef) app /-- Return `some namedArg` if `namedArgs` contains an entry for `binderName`. -/ -private def findBinderName? (namedArgs : List NamedArg) (binderName : Name) : Option NamedArg := +private def findNamedArg? (namedArgs : List NamedArg) (binderName : Name) : Option NamedArg := namedArgs.find? fun namedArg => namedArg.name == binderName /-- @@ -131,7 +123,7 @@ private def hasOptAutoParams (type : Expr) : MetaM Bool := do forallTelescopeReducing type fun xs _ => xs.anyM fun x => do let xType ← inferType x - return xType.getOptParamDefault?.isSome || xType.getAutoParamTactic?.isSome + return xType.isOptParam || xType.isAutoParam /-! # Default application elaborator -/ @@ -178,14 +170,22 @@ structure Context where but it did not work well in practice. For example, it failed in the example above. -/ resultIsOutParamSupport : Bool + /-- Cached from `NamedArg.numImplicitParams`. This is the prefix of parameters whose explicitness + should be overridden to become implicit. -/ + numImplicitParams : Nat /-- Auxiliary structure for elaborating the application `f args namedArgs`. -/ structure State where + /-- The elaborated application so far, with applied arguments. -/ f : Expr + /-- The type of `f` once loose bvars are instantiated with `fArgs`, reduced to WHNF if it is a forall + after `fTypeIsForall` is called. -/ fType : Expr - /-- Remaining regular arguments. -/ + /-- Elaborated arguments. -/ + fArgs : Array Expr := #[] + /-- Remaining positional arguments to be elaborated. -/ args : List Arg - /-- remaining named arguments to be processed. -/ + /-- Remaining named arguments to be elaborated. -/ namedArgs : List NamedArg expectedType? : Option Expr /-- @@ -200,11 +200,13 @@ structure State where Each pair records the name to use for the binding and the fvar for the argument. When `..` is used, eta-expansion is disabled, and missing arguments are treated as `_`. + When there are named arguments that depend on a missing argument, the missing arguments + are treated as `_` as well. -/ etaArgs : Array (Name × Expr) := #[] /-- Metavariables that we need to set the error context using the application being built. -/ toSetErrorCtx : Array MVarId := #[] - /-- Metavariables for the instance implicit arguments that have already been processed. -/ + /-- Metavariables for the instance implicit arguments that have already been processed but not yet synthesized.. -/ instMVars : Array MVarId := #[] /-- The following field is used to implement the `propagateExpectedType` heuristic. @@ -219,11 +221,129 @@ structure State where /-- Valid named arguments found while traversing the function's type. -/ foundNamedArgs : Array Name := #[] +/-- The index of the parameter currently being worked on -/ +@[inline] private def State.paramIdx (s : State) : Nat := s.fArgs.size + +/-- Gets `s.fType` with all loose bvars instantiated. -/ +@[inline] private def State.getFType (s : State) : Expr := + s.fType.instantiateRevRange 0 s.fArgs.size s.fArgs + abbrev M := ReaderT Context (StateRefT State TermElabM) -/-- Add the given metavariable to the collection of metavariables associated with instance-implicit arguments. -/ -private def addInstMVar (mvarId : MVarId) : M Unit := - modify fun s => { s with instMVars := s.instMVars.push mvarId } +/-- +Returns `true` if `fType` is a function type, possibly after applying `whnf` and updating `fType` if necessary. +It does not modify `fType` if it doesn't reduce to a function type, except to instantiate bvars. +Guarantees that the domain of the function type has no loose bvars. +-/ +private def fTypeIsForall : M Bool := do + let s ← get + if let Expr.forallE n d b bi := s.fType then + -- Ensure the domain is instantiated, to ensure validity of `getParamType` + if d.hasLooseBVars then + let d := d.instantiateRevRange 0 s.fArgs.size s.fArgs + set { s with fType := Expr.forallE n d b bi } + return true + else + let fType ← whnfForall s.getFType + set { s with fType } + return fType.isForall + +/-- +Returns the current parameter's name. +Only valid if `fTypeIsForall` has returned `true`. +-/ +@[inline] private def getParamName : M Name := return (← get).fType.bindingName! + +/-- +Returns the current parameter's type. +Only valid if `fTypeIsForall` has returned `true`. +-/ +@[inline] private def getParamType : M Expr := return (← get).fType.bindingDomain! + +/-- +Returns the current parameter's binder info. +Only valid if `fTypeIsForall` has returned `true`. +-/ +@[inline] private def getParamInfo : M BinderInfo := return (← get).fType.bindingInfo! + +/-- +Returns the expected type to use for the argument for the current parameter. +Only valid if `fTypeIsForall` has returned `true`. +-/ +@[inline] private def getArgExpectedType : M Expr := return (← getParamType).consumeTypeAnnotations + +/-- +Returns `fType` with loose bvars instantiated. +Like `State.getFType` but caches the result. +-/ +private def getFType : M Expr := do + modify fun s => { s with fType := s.getFType } + return (← get).fType + +/-- +Returns `fType` with loose bvars instantiated and metavariables instantiated. +Caches the result. +-/ +private def getFType' : M Expr := do + let fType ← getFType >>= instantiateMVars + modify fun s => { s with fType } + return (← get).fType + +/-- Returns `true` if there are positional or named arguments to be processed. -/ +private def hasArgsToProcess : M Bool := do + let s ← get + return !s.args.isEmpty || !s.namedArgs.isEmpty + +/-- +Returns the argument syntax if the next positional argument is of the form `_`. +-/ +private def nextArgHole? : M (Option Syntax) := do + match (← get).args with + | Arg.stx stx@(Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure stx + | _ => pure none + +/-- Remove named argument with name `binderName` from `namedArgs`. -/ +def eraseNamedArg (binderName : Name) : M Unit := + modify fun s => { s with namedArgs := Term.eraseNamedArg s.namedArgs binderName } + +/-- Record a valid named argument for the function. -/ +private def pushFoundNamedArg (name : Name) : M Unit := do + modify fun s => { s with foundNamedArgs := s.foundNamedArgs.push name } + +/-- Get the function's named arguments (which were found during elaboration). -/ +private def getFoundNamedArgs : M (Array Name) := + return (← get).foundNamedArgs + +/-- +Returns a named argument that depends on the next argument, otherwise `none`. +-/ +private def findNamedArgDependsOn? (fType : Expr) (namedArgs : List NamedArg) : MetaM (Option NamedArg) := do + if fType.isArrow then + return none + else + forallTelescopeReducing fType fun xs _ => do + let curr := xs[0]! + let mut namedArgs := namedArgs + for h : i in 1...xs.size do + let xDecl ← xs[i].fvarId!.getDecl + if let some arg := namedArgs.find? fun arg => arg.name == xDecl.userName then + /- Remark: a default value at `optParam` does not count as a dependency -/ + if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then + return arg + -- Erase, since `xDecl.userName` can be repeated, and we can otherwise get false dependencies + namedArgs := Term.eraseNamedArg namedArgs xDecl.userName + return none + +/-- +Returns a named argument that depends on the next argument, otherwise `none`. +-/ +private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do + if (← get).namedArgs.isEmpty then + return none + else if (← get).fType.isArrow then + return none + else + findNamedArgDependsOn? (← getFType) (← get).namedArgs /-- Try to synthesize metavariables are `instMVars` using type class resolution. @@ -249,23 +369,12 @@ def synthesizeAppInstMVars : M Unit := do Term.synthesizeAppInstMVars (← get).instMVars (← get).f modify ({ · with instMVars := #[] }) -/-- Record a valid named argument for the function. -/ -private def pushFoundNamedArg (name : Name) : M Unit := do - modify fun s => { s with foundNamedArgs := s.foundNamedArgs.push name } - -/-- Get the function's named arguments (which were found during elaboration). -/ -private def getFoundNamedArgs : M (Array Name) := - return (← get).foundNamedArgs - /-- fType may become a forallE after we synthesize pending metavariables. -/ private def synthesizePendingAndNormalizeFunType : M Unit := do trySynthesizeAppInstMVars synthesizeSyntheticMVars - let s ← get - let fType ← whnfForall s.fType - if fType.isForall then - modify fun s => { s with fType } - else + unless ← fTypeIsForall do + let s ← get if let some f ← coerceToFunction? s.f then let fType ← inferType f modify fun s => { s with f, fType } @@ -297,32 +406,24 @@ private def synthesizePendingAndNormalizeFunType : M Unit := do .note m!"Expected a function because this term is being applied to the argument\ {indentD <| toMessageData arg}" else .nil - throwError "Function expected at{indentExpr s.f}\nbut this term has type{indentExpr fType}\ + throwError "Function expected at{indentExpr s.f}\nbut this term has type{indentExpr (← inferType s.f)}\ {extra}\ {← hintAutoImplicitFailure s.f}" -/-- Normalize and return the function type. -/ -private def normalizeFunType : M Expr := do - let s ← get - let fType ← whnfForall s.fType - modify fun s => { s with fType } - return fType - -/-- Return the binder name at `fType`. This method assumes `fType` is a function type. -/ -private def getBindingName : M Name := return (← get).fType.bindingName! - -/-- Return the next argument expected type. This method assumes `fType` is a function type. -/ -private def getArgExpectedType : M Expr := return (← get).fType.bindingDomain! - -/-- Remove named argument with name `binderName` from `namedArgs`. -/ -def eraseNamedArg (binderName : Name) : M Unit := - modify fun s => { s with namedArgs := Term.eraseNamedArg s.namedArgs binderName } +/-- Add the given metavariable to the collection of metavariables associated with instance-implicit arguments. -/ +private def addInstMVar (mvarId : MVarId) : M Unit := + modify fun s => { s with instMVars := s.instMVars.push mvarId } /-- Add a new argument to the result. That is, `f := f arg`, update `fType`. This method assumes `fType` is a function type. -/ private def addNewArg (argName : Name) (arg : Expr) : M Unit := do - modify fun s => { s with f := mkApp s.f arg, fType := s.fType.bindingBody!.instantiate1 arg } + let s ← get + trace[Elab.app.args] "arg {s.paramIdx+1}{if argName.hasMacroScopes then m!"" else m!" ({argName})"}: {arg}" + modify fun s => { s with + f := mkApp s.f arg, + fArgs := s.fArgs.push arg, + fType := s.fType.bindingBody! } if arg.isMVar then registerMVarArgName arg.mvarId! argName @@ -331,7 +432,7 @@ private def addNewArg (argName : Name) (arg : Expr) : M Unit := do Recall that, `Arg` may be wrapping an already elaborated `Expr`. -/ private def elabAndAddNewArg (argName : Name) (arg : Arg) : M Unit := do let s ← get - let expectedType := (← getArgExpectedType).consumeTypeAnnotations + let expectedType ← getArgExpectedType match arg with | Arg.expr val => let arg ← ensureArgType s.f val expectedType @@ -341,29 +442,76 @@ private def elabAndAddNewArg (argName : Name) (arg : Arg) : M Unit := do let arg ← withRef stx <| ensureArgType s.f val expectedType addNewArg argName arg -/-- Return true if `fType` contains `OptParam` or `AutoParams` -/ -private def fTypeHasOptAutoParams : M Bool := do - hasOptAutoParams (← get).fType +/-- +Auxiliary function for computing the resulting type of a function application. +Simulates `ElabAppArgs.main` without elaborating anything. +-/ +private partial def getResultingTypeCore? (explicit ellipsis : Bool) (numImplicitParams : Nat) + (paramIdx : Nat) (numArgs : Nat) (namedArgs : List NamedArg) (fType : Expr) : TermElabM (Option Expr) := do + trace[Elab.app.propagateExpectedType] "numArgs: {numArgs}, namedArgs.length: {namedArgs.length}" + trace[Elab.app.propagateExpectedType] "fType: {fType}" + main' paramIdx numArgs namedArgs fType +where + main' (paramIdx : Nat) (numArgs : Nat) (namedArgs : List NamedArg) (fType : Expr) : TermElabM (Option Expr) := do + -- Note that we want to return an `fType` that's *not* in WHNF, so we keep the original `fType` + -- and compute a separate `fType'`. + let fType' ← if fType.isForall || fType.hasLooseBVars then pure fType else whnfForall fType + if let .forallE binderName paramType fTypeBody bi := fType' then + match Term.findNamedArg? namedArgs binderName with + | some _ => main' (paramIdx + 1) numArgs (Term.eraseNamedArg namedArgs binderName) fTypeBody + | none => + let processImplicit' (_ : Unit) := main' (paramIdx + 1) numArgs namedArgs fTypeBody + if !explicit && bi.isStrictImplicit && numArgs == 0 && namedArgs.isEmpty then + finalize' fType + else if !explicit && !bi.isExplicit then + processImplicit' () + else if paramIdx < numImplicitParams then -- Simulates `processExplicitArg` from this point onward + processImplicit' () + else if numArgs > 0 then + main' (paramIdx + 1) (numArgs - 1) namedArgs fTypeBody + else if ellipsis || !explicit && (paramType.isAutoParam || paramType.isOptParam) then + processImplicit' () + else if fType'.hasLooseBVars then + trace[Elab.app.propagateExpectedType] "propogation postponed, resulting type depends on arguments that have not yet been elaborated: {fType'}" + return none + else if !namedArgs.isEmpty then + if (← findNamedArgDependsOn? fType' namedArgs).isSome then + processImplicit' () + else + trace[Elab.app.propagateExpectedType] "propogation postponed, there are still named arguments, and need to use eta arguments" + return none + else if !explicit then + if (← hasOptAutoParams fType') then + trace[Elab.app.propagateExpectedType] "propagation postponed, resulting type has opt-params or auto-params: {fType'}" + return none + else + finalize' fType + else + finalize' fType + else if numArgs > 0 || !namedArgs.isEmpty then + trace[Elab.app.propagateExpectedType] "propogation postponed, currently more arguments than parameters" + return none + else + finalize' fType + finalize' (fType : Expr) : MetaM (Option Expr) := do + if fType.hasLooseBVars then + trace[Elab.app.propagateExpectedType] "propagation postponed, resulting type depends on arguments that have not yet been elaborated: {fType}" + return none + else + return fType /-- - Auxiliary function for retrieving the resulting type of a function application. - See `propagateExpectedType`. - Remark: `(explicit : Bool) == true` when `@` modifier is used. -/ -private partial def getForallBody (explicit : Bool) : Nat → List NamedArg → Expr → Option Expr - | i, namedArgs, type@(.forallE n d b bi) => - match findBinderName? namedArgs n with - | some _ => getForallBody explicit i (Term.eraseNamedArg namedArgs n) b - | none => - if !explicit && !bi.isExplicit then - getForallBody explicit i namedArgs b - else if i > 0 then - getForallBody explicit (i-1) namedArgs b - else if d.isAutoParam || d.isOptParam then - getForallBody explicit i namedArgs b - else - some type - | 0, [], type => some type - | _, _, _ => none +Auxiliary function for `propagateExpectedType`. Returns the inferred type of the function +application, if enough information is currently known. +-/ +private partial def getResultingType? : M (Option Expr) := do + withTraceNode `Elab.app.propagateExpectedType + (fun + | .ok resultingType => return m!"resulting type: {resultingType}" + | .error ex => return m!"resulting type failed: {ex.toMessageData}") do + let fType ← getFType' + getResultingTypeCore? (← read).explicit (← read).ellipsis (← read).numImplicitParams + (← get).paramIdx (← get).args.length (← get).namedArgs fType private def shouldPropagateExpectedTypeFor (nextArg : Arg) : Bool := match nextArg with @@ -431,7 +579,7 @@ private def propagateExpectedType (arg : Arg) : M Unit := do ``` They would all fail for the same reason. So, let's focus on the first one. We would elaborate `s.2` with `expectedType == Prop`. - Before we elaborate `s`, this method would be invoked, and `s.fType` is `?α × ?β → ?β` and after + Before we elaborate `s`, this method would be invoked, and `fType` is `?α × ?β → ?β` and after propagation we would have `?α × Prop → Prop`. Then, when we would try to elaborate `s`, and get a type error because `?α × Prop` cannot be unified with `Nat × Bool`. Most users would have a hard time trying to understand why these examples failed. @@ -442,97 +590,71 @@ private def propagateExpectedType (arg : Arg) : M Unit := do This may not be that bad since the developers and users don't seem to care about constructivism. We currently use a different workaround, we just don't propagate the expected type when it is `Prop`. -/ + let expectedType ← instantiateMVars expectedType if expectedType.isProp then modify fun s => { s with propagateExpected := false } - else - let numRemainingArgs := s.args.length - trace[Elab.app.propagateExpectedType] "etaArgs.size: {s.etaArgs.size}, numRemainingArgs: {numRemainingArgs}, fType: {s.fType}" - match getForallBody (← read).explicit numRemainingArgs s.namedArgs s.fType with - | none => pure () - | some fTypeBody => - unless fTypeBody.hasLooseBVars do - unless (← hasOptAutoParams fTypeBody) do - trySynthesizeAppInstMVars - trace[Elab.app.propagateExpectedType] "{expectedType} =?= {fTypeBody}" - if (← isDefEq expectedType fTypeBody) then - /- Note that we only set `propagateExpected := false` when propagation has succeeded. -/ - modify fun s => { s with propagateExpected := false } + trace[Elab.app.propagateExpectedType] "expected type is Prop, propagation disabled" + else if let some fTypeBody ← getResultingType? then + trySynthesizeAppInstMVars + discard <| withTraceNodeBefore `Elab.app.propagateExpectedType (fun _ => return m!"{expectedType} =?= {fTypeBody}") do + if (← isDefEq expectedType fTypeBody) then + /- Note that we only set `propagateExpected := false` when propagation has succeeded. -/ + modify fun s => { s with propagateExpected := false } + trace[Elab.app.propagateExpectedType] "propagated: {expectedType} =?= {fTypeBody}" + return true + else + trace[Elab.app.propagateExpectedType] "propagation pending, unification of expected type and resulting type failed" + return false /-- This method executes after all application arguments have been processed. -/ private def finalize : M Expr := do - let s ← get - let mut e := s.f - -- all user explicit arguments have been consumed - trace[Elab.app.finalize] e - let ref ← getRef - -- Register the error context of implicits - for mvarId in s.toSetErrorCtx do - registerMVarErrorImplicitArgInfo mvarId ref e - if !s.etaArgs.isEmpty then - e ← mkLambdaFVars (s.etaArgs.map (·.2)) e - e := e.updateBinderNames (s.etaArgs.map (some <| ·.1)).toList - /- - Remark: we should not use `s.fType` as `eType` even when - `s.etaArgs.isEmpty`. Reason: it may have been unfolded. - -/ - let eType ← inferType e - trace[Elab.app.finalize] "after etaArgs, {e} : {eType}" - /- Recall that `resultTypeOutParam? = some mvarId` if the function result type is the output parameter - of a local instance. The value of this parameter may be inferable using other arguments. For example, - suppose we have - ```lean - def add_one {X} [Trait X] [One (Trait.R X)] [HAdd X (Trait.R X) X] (x : X) : X := x + (One.one : (Trait.R X)) - ``` - from test `948.lean`. There are multiple ways to infer `X`, and we don't want to mark it as `syntheticOpaque`. - -/ - if let some outParamMVarId := s.resultTypeOutParam? then + withTraceNode `Elab.app.finalize (fun + | .ok e => return m!"{e} : {← inferType e}" + | .error ex => return m!"error finalizing{indentD (← get).f}\n{ex.toMessageData}") do + let s ← get + let mut e := s.f + trace[Elab.app.finalize] "initial: {e}" + let ref ← getRef + -- Register the error context of implicits + for mvarId in s.toSetErrorCtx do + registerMVarErrorImplicitArgInfo mvarId ref e + unless s.etaArgs.isEmpty do + e ← mkLambdaFVars (s.etaArgs.map (·.2)) e + e := e.updateBinderNames (s.etaArgs.map (some <| ·.1)).toList + trace[Elab.app.finalize] "after etaArgs, {e}" + /- + Remark: we should not use `s.fType` as `eType` even when + `s.etaArgs.isEmpty`. Reason: it may have been unfolded. + -/ + let eType ← inferType e + /- Recall that `resultTypeOutParam? = some mvarId` if the function result type is the output parameter + of a local instance. The value of this parameter may be inferable using other arguments. For example, + suppose we have + ```lean + def add_one {X} [Trait X] [One (Trait.R X)] [HAdd X (Trait.R X) X] (x : X) : X := x + (One.one : (Trait.R X)) + ``` + from test `948.lean`. There are multiple ways to infer `X`, and we don't want to mark it as `syntheticOpaque`. + -/ + if let some outParamMVarId := s.resultTypeOutParam? then + synthesizeAppInstMVars + /- If `eType != mkMVar outParamMVarId`, then the + function is partially applied, and we do not apply default instances. -/ + if !(← outParamMVarId.isAssigned) && eType.isMVar && eType.mvarId! == outParamMVarId then + synthesizeSyntheticMVarsUsingDefault + return e + else + return e + if let some expectedType := s.expectedType? then + trySynthesizeAppInstMVars + -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it. + discard <| withTraceNodeBefore `Elab.app.finalize (fun _ => return m!"propagating expected type: {expectedType} =?= {eType}") do + if (← isDefEq expectedType eType) then + trace[Elab.app.finalize] "propagated: {expectedType} =?= {eType}" + return true + else + return false synthesizeAppInstMVars - /- If `eType != mkMVar outParamMVarId`, then the - function is partially applied, and we do not apply default instances. -/ - if !(← outParamMVarId.isAssigned) && eType.isMVar && eType.mvarId! == outParamMVarId then - synthesizeSyntheticMVarsUsingDefault - return e - else - return e - if let some expectedType := s.expectedType? then - trySynthesizeAppInstMVars - -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it. - trace[Elab.app.finalize] "expected type: {expectedType}" - discard <| isDefEq expectedType eType - synthesizeAppInstMVars - return e - -/-- -Returns a named argument that depends on the next argument, otherwise `none`. --/ -private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do - let s ← get - if s.namedArgs.isEmpty then - return none - else - forallTelescopeReducing s.fType fun xs _ => do - let curr := xs[0]! - for h : i in 1...xs.size do - let xDecl ← xs[i].fvarId!.getDecl - if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then - /- Remark: a default value at `optParam` does not count as a dependency -/ - if (← exprDependsOn xDecl.type.cleanupAnnotations curr.fvarId!) then - return arg - return none - - -/-- 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 - -/-- -Returns the argument syntax if the next argument at `args` is of the form `_`. --/ -private def nextArgHole? : M (Option Syntax) := do - match (← get).args with - | Arg.stx stx@(Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure stx - | _ => pure none + return e /-- Return `true` if the next argument to be processed is the outparam of a local instance, and it the result type @@ -557,12 +679,12 @@ private def nextArgHole? : M (Option Syntax) := do Remark: if `resultIsOutParamSupport` is `false`, this method returns `false`. -/ private partial def isNextOutParamOfLocalInstanceAndResult : M Bool := do - if !(← read).resultIsOutParamSupport then + unless (← read).resultIsOutParamSupport && (← get).resultTypeOutParam?.isNone do return false let type := (← get).fType.bindingBody! unless isResultType type 0 do return false - if (← hasLocalInstanceWithOutParams type) then + if hasLocalInstanceWithOutParams (← getEnv) type then let x := mkFVar (← mkFreshFVarId) isOutParamOfLocalInstance x (type.instantiate1 x) else @@ -575,20 +697,20 @@ where | _ => false /-- (quick filter) Return true if `type` contains a binder `[C ...]` where `C` is a class containing outparams. -/ - hasLocalInstanceWithOutParams (type : Expr) : CoreM Bool := do + hasLocalInstanceWithOutParams (env : Environment) (type : Expr) : Bool := Id.run do let .forallE _ d b bi := type | return false if bi.isInstImplicit then if let .const declName .. := d.getAppFn then - if hasOutParams (← getEnv) declName then + if hasOutParams env declName then return true - hasLocalInstanceWithOutParams b + hasLocalInstanceWithOutParams env b isOutParamOfLocalInstance (x : Expr) (type : Expr) : MetaM Bool := do let .forallE _ d b bi := type | return false if bi.isInstImplicit then - if let .const declName .. := d.getAppFn then + if let c@(.const declName ..) := d.getAppFn then if hasOutParams (← getEnv) declName then - let cType ← inferType d.getAppFn + let cType ← inferType c if (← isOutParamOf x 0 d.getAppArgs cType) then return true isOutParamOfLocalInstance x b @@ -610,11 +732,10 @@ mutual and then execute the main loop. -/ private partial def addEtaArg (argName : Name) : M Expr := do - let n ← getBindingName let type ← getArgExpectedType -- Use a fresh name to ensure that the remaining arguments can't capture this parameter's name. - withLocalDeclD (← Core.mkFreshUserName n) type fun x => do - modify fun s => { s with etaArgs := s.etaArgs.push (n, x) } + withLocalDeclD (← Core.mkFreshUserName argName) type fun x => do + modify fun s => { s with etaArgs := s.etaArgs.push (argName, x) } addNewArg argName x main @@ -630,6 +751,7 @@ mutual At `finalize`, we check whether `arg` is still unassigned, if it is, we apply default instances, and try to synthesize pending mvars. -/ modify fun s => { s with resultTypeOutParam? := some arg.mvarId!, propagateExpected := false } + trace[Elab.app.propagateExpectedType] "result type is an output parameter, propagation disabled" pure arg else mkFreshExprMVar argType @@ -642,45 +764,44 @@ mutual This method assume `fType` is a function type. -/ private partial def processExplicitArg (argName : Name) : M Expr := do + if (← get).paramIdx < (← read).numImplicitParams then + /- + We treat the explicit argument `argName` as implicit if + it's among the first `numImplicitParams` parameters. + The motivation for this is class projections (issue #1851). + In some cases, class projections can have explicit parameters. For example, in + ``` + class Approx {α : Type} (a : α) (X : Type) : Type where + val : X + ``` + the type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X`. + Note that the parameter `a` is explicit since there is no way to infer it from the expected + type or from the types of other explicit parameters. + Being a parameter of the class, `a` is determined by the type of `self`. + + Consider + ``` + variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] + ``` + Recall that `f.val` is, to first approximation, sugar for `Approx.val (self := f)`. + Without further refinement, this would expand to `fun f'' : α → β => Approx.val f'' f`, + which is a type error, since `f''` must be defeq to `f'`. + Furthermore, with projection notation, users expect all structure parameters + to be uniformly implicit; after all, they are determined by `self`. + To handle this, the `(self := f)` named argument is annotated with the `suppressDeps` flag. + This causes the `a` parameter to become implicit, and `f.val` instead expands to `Approx.val f' f`. + + This feature previously was enabled for *all* explicit arguments, which confused users + and was frequently reported as a bug (issue #1867). + Now it is only enabled for the `self` argument in structure projections. + + We used to do this only when `(← get).args` was empty, + but it created an asymmetry because `f.val` worked as expected, + yet one would have to write `f.val _ x` when there are further arguments. + -/ + return (← addImplicitArg argName) match (← get).args with | arg::args => - -- Note: currently the following test never succeeds in explicit mode since `@x.f` notation does not exist. - if let some true := NamedArg.suppressDeps <$> (← findNamedArgDependsOnCurrent?) then - /- - We treat the explicit argument `argName` as implicit - if we have a named arguments that depends on it whose `suppressDeps` flag set to `true`. - The motivation for this is class projections (issue #1851). - In some cases, class projections can have explicit parameters. For example, in - ``` - class Approx {α : Type} (a : α) (X : Type) : Type where - val : X - ``` - the type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X`. - Note that the parameter `a` is explicit since there is no way to infer it from the expected - type or from the types of other explicit parameters. - Being a parameter of the class, `a` is determined by the type of `self`. - - Consider - ``` - variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] - ``` - Recall that `f.val` is, to first approximation, sugar for `Approx.val (self := f)`. - Without further refinement, this would expand to `fun f'' : α → β => Approx.val f'' f`, - which is a type error, since `f''` must be defeq to `f'`. - Furthermore, with projection notation, users expect all structure parameters - to be uniformly implicit; after all, they are determined by `self`. - To handle this, the `(self := f)` named argument is annotated with the `suppressDeps` flag. - This causes the `a` parameter to become implicit, and `f.val` instead expands to `Approx.val f' f`. - - This feature previously was enabled for *all* explicit arguments, which confused users - and was frequently reported as a bug (issue #1867). - Now it is only enabled for the `self` argument in structure projections. - - We used to do this only when `(← get).args` was empty, - but it created an asymmetry because `f.val` worked as expected, - yet one would have to write `f.val _ x` when there are further arguments. - -/ - return (← addImplicitArg argName) propagateExpectedType arg modify fun s => { s with args } elabAndAddNewArg argName arg @@ -702,8 +823,8 @@ mutual but it's not possible to opt-in. -/ return ← addImplicitArg argName - let argType ← getArgExpectedType - match (← read).explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with + let paramType ← getParamType + match (← read).explicit, paramType.getOptParamDefault?, paramType.getAutoParamTactic? with | false, some defVal, _ => addNewArg argName defVal; main | false, _, some (.const tacticDecl _) => let env ← getEnv @@ -722,14 +843,12 @@ mutual -/ let info := (← getRef).getHeadInfo.nonCanonicalSynthetic let tacticBlock := tacticBlock.raw.rewriteBottomUp (·.setInfo info) - let mvar ← mkTacticMVar argType.consumeTypeAnnotations tacticBlock (.autoParam argName) + let mvar ← mkTacticMVar (← getArgExpectedType) tacticBlock (.autoParam argName) -- Note(kmill): We are adding terminfo to simulate a previous implementation that elaborated `tacticBlock`. -- We should look into removing this since terminfo for synthetic syntax is suspect, -- but we noted it was necessary to preserve the behavior of the unused variable linter. addTermInfo' tacticBlock mvar - let argNew := Arg.expr mvar - propagateExpectedType argNew - elabAndAddNewArg argName argNew + addNewArg argName mvar main | false, _, some _ => throwError "Internal error when elaborating function application: autoParam `{argName}` is not a constant" @@ -737,17 +856,20 @@ mutual if (← read).ellipsis then addImplicitArg argName else if !(← get).namedArgs.isEmpty then - if let some _ ← findNamedArgDependsOnCurrent? then + if let some depNamedArg ← findNamedArgDependsOnCurrent? then /- Dependencies of named arguments cannot be turned into eta arguments since they are determined by the named arguments. Instead we can turn them into implicit arguments. -/ + trace[Elab.app.args] "named arg `{depNamedArg.name}` depends on this one, adding implicit" addImplicitArg argName else + trace[Elab.app.args] "using eta arg since there are still named arguments" addEtaArg argName else if !(← read).explicit then - if (← fTypeHasOptAutoParams) then + if (← hasOptAutoParams (← getFType)) then + trace[Elab.app.args] "using eta arg since there are still optParams or autoParams" addEtaArg argName else finalize @@ -802,12 +924,10 @@ mutual /-- Elaborate function application arguments. -/ partial def main : M Expr := do - let fType ← normalizeFunType - if fType.isForall then - let binderName := fType.bindingName! - let binfo := fType.bindingInfo! + if (← fTypeIsForall) then + let binderName ← getParamName let s ← get - let namedArg? ← match findBinderName? s.namedArgs binderName with + let namedArg? ← match findNamedArg? s.namedArgs binderName with | some namedArg => pure (some namedArg) | none => findDeprecatedBinderName? s.namedArgs s.f binderName match namedArg? with @@ -819,11 +939,11 @@ mutual | none => unless binderName.hasMacroScopes do pushFoundNamedArg binderName - match binfo with + match (← getParamInfo) with | .implicit => processImplicitArg binderName | .instImplicit => processInstImplicitArg binderName | .strictImplicit => processStrictImplicitArg binderName - | _ => processExplicitArg binderName + | .default => processExplicitArg binderName else if (← hasArgsToProcess) then synthesizePendingAndNormalizeFunType main @@ -1125,7 +1245,7 @@ The result is `.none` if it is an implicit argument which was not provided using The result is `.undef` if `args` is empty and `namedArgs` does contain an entry for `binderName`. -/ def getNextArg? (binderName : Name) (binderInfo : BinderInfo) : M (LOption Arg) := do - match findBinderName? (← get).namedArgs binderName with + match findNamedArg? (← get).namedArgs binderName with | some namedArg => modify fun s => { s with namedArgs := eraseNamedArg s.namedArgs binderName } return .some namedArg.val @@ -1235,13 +1355,24 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg) let resultIsOutParamSupport := ((← getEnv).contains ``Lean.Internal.coeM) && resultIsOutParamSupport && !explicit let fType ← inferType f let fType ← instantiateMVars fType + withTraceNodeBefore `Elab.app.args + (fun _ => do + let mut msgs := #[] + if explicit then msgs := msgs.push m!"explicit" + if ellipsis then msgs := msgs.push m!"ellipsis" + if args.size > 0 then msgs := msgs.push m!"({args.size} args)" + if namedArgs.size > 0 then msgs := msgs.push m!"({namedArgs.size} namedArgs)" + return m!"elabAppArgs {MessageData.joinSep msgs.toList " "}{inlineExprTrailing f}") do unless namedArgs.isEmpty && args.isEmpty do tryPostponeIfMVar fType - trace[Elab.app.args] "explicit: {explicit}, ellipsis: {ellipsis}, {f} : {fType}" + trace[Elab.app.args] "fType: {fType}" + trace[Elab.app.args] "expectedType: {expectedType?}" trace[Elab.app.args] "namedArgs: {namedArgs}" trace[Elab.app.args] "args: {args}" + trace[Elab.app.args] "explicit: {explicit}, ellipsis: {ellipsis}, resultIsOutParamSupport: {resultIsOutParamSupport}" if let some elimInfo ← elabAsElim? then tryPostponeIfNoneOrMVar expectedType? + trace[Elab.app.args] "Using ElabAsElim procedure. motivePos: {elimInfo.motivePos}, majorPos: {elimInfo.majorsPos}" let some expectedType := expectedType? | throwError "failed to elaborate eliminator, expected type is not available" let expectedType ← instantiateMVars expectedType if expectedType.getAppFn.isMVar then throwError "failed to elaborate eliminator, expected type is not available" @@ -1251,7 +1382,11 @@ def elabAppArgs (f : Expr) (namedArgs : Array NamedArg) (args : Array Arg) namedArgs := namedArgs.toList } else - ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport } |>.run' { + -- Note: we only expect one `numImplicitParams` to be set. + let numImplicitParams := namedArgs.foldl (init := 0) (max · ·.numImplicitParams) + if numImplicitParams > 0 then + trace[Elab.app.args] "the first {numImplicitParams} parameters are overridden to be implicit" + ElabAppArgs.main.run { explicit, ellipsis, resultIsOutParamSupport, numImplicitParams } |>.run' { args := args.toList expectedType?, f, fType namedArgs := namedArgs.toList @@ -1273,13 +1408,13 @@ where let mut namedArgs := namedArgs.toList for x in xs[*...elimInfo.motivePos] do let localDecl ← x.fvarId!.getDecl - match findBinderName? namedArgs localDecl.userName with + match findNamedArg? namedArgs localDecl.userName with | some _ => namedArgs := eraseNamedArg namedArgs localDecl.userName | none => if localDecl.binderInfo.isExplicit then args := args.tailD [] -- Invariant: `elimInfo.motivePos < xs.size` due to construction of `elimInfo`. let some x := xs[elimInfo.motivePos]? | unreachable! let localDecl ← x.fvarId!.getDecl - if findBinderName? namedArgs localDecl.userName matches some _ then + if findNamedArg? namedArgs localDecl.userName matches some _ then -- motive has been explicitly provided, so we should use standard app elaborator return none else @@ -1560,13 +1695,14 @@ private def resolveLVal (e : Expr) (lval : LVal) (hasArgs : Bool) : TermElabM (E private partial def mkBaseProjections (baseStructName : Name) (structName : Name) (e : Expr) : TermElabM Expr := do let env ← getEnv match getPathToBaseStructure? env baseStructName structName with - | none => throwError "Internal error: Failed to access field in parent structure" + | none => panic! "Internal error: Failed to access field in parent structure" | some path => - let mut e := e - for projFunName in path do - let projFn ← mkConst projFunName - e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e, suppressDeps := true }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false) - return e + path.foldlM (init := e) fun e projFn => do + let ty ← whnf (← inferType e) + let .const _ us := ty.getAppFn + | panic! "Type of structure value cannot be reduced to a constant application" + let params := ty.getAppArgs + pure <| mkApp (mkAppN (.const projFn us) params) e private partial def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := withReducibleAndInstances do @@ -1720,11 +1856,14 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp throwError "Field `{fieldName}` from structure `{structName}` is private" let projFn ← withRef lval.getRef <| mkConst info.projFn levels let projFn ← addProjTermInfo lval.getRef projFn + let baseStructInfo ← getConstInfoInduct baseStructName + let namedArg : NamedArg := + { name := `self, val := Arg.expr f, numImplicitParams := baseStructInfo.numParams } if lvals.isEmpty then - let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true } + let namedArgs ← addNamedArg namedArgs namedArg elabAppArgs projFn namedArgs args expectedType? explicit ellipsis else - let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false) + let f ← elabAppArgs projFn #[namedArg] #[] (expectedType? := none) (explicit := false) (ellipsis := false) loop f lvals | LValResolution.const baseStructName structName constName levels => let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f diff --git a/src/Lean/Elab/Arg.lean b/src/Lean/Elab/Arg.lean index 3ea3335244..cf6dd286fd 100644 --- a/src/Lean/Elab/Arg.lean +++ b/src/Lean/Elab/Arg.lean @@ -21,20 +21,34 @@ inductive Arg where | expr (val : Expr) deriving Inhabited +instance : ToString Arg where + toString + | .stx stx => toString stx + | .expr e => toString e + +instance : ToMessageData Arg where + toMessageData + | .stx stx => toMessageData stx + | .expr e => toMessageData e + /-- Named arguments created using the notation `(x := val)`. -/ structure NamedArg where ref : Syntax := Syntax.missing name : Name val : Arg - /-- If `true`, then make all parameters that depend on this one become implicit. - This is used for projection notation, since structure parameters might be explicit for classes. -/ - suppressDeps : Bool := false + /-- Overrides the binder infos for the first `numImplicitParams` parameters + to make them be implicit if they were explicit. + This is used for expanding projection notation. The primary motivation for this field + is that class projections may feature explicit structure parameters. + See the note at `Lean.Elab.Term.ElabAppArgs.processExplicitArg`. -/ + numImplicitParams : Nat := 0 deriving Inhabited -instance : ToMessageData Arg where - toMessageData - | .stx stx => toMessageData stx - | .expr e => toMessageData e +instance : ToString NamedArg where + toString s := s!"({s.name} := {s.val})" + +instance : ToMessageData NamedArg where + toMessageData s := m!"({s.name} := {s.val})" /-- Add a new named argument to `namedArgs`, and throw an error if it already contains a named argument