max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: app elaborator refactoring and improvements (#13762)

Browse source 
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.
This commit is contained in:
Kyle Miller 2026-05-18 07:41:09 -07:00 • committed by GitHub
parent 3f3a26c53c
commit 5d22886aff
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 390 additions and 237 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

599
src/Lean/Elab/App.lean
View file

@ -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

28
src/Lean/Elab/Arg.lean
View file

@ -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