From fe12c58216725dbd8002d9415fe2785349972087 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 24 Sep 2024 14:32:41 -0700 Subject: [PATCH] improve docs, errors, and implementation --- src/Lean/Elab/App.lean | 87 +++++++++++-------- src/Lean/Elab/Arg.lean | 11 +-- tests/lean/run/explicitApp.lean | 5 +- .../missingExplicitWithForwardNamedDep.lean | 12 ++- 4 files changed, 67 insertions(+), 48 deletions(-) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 38853659ab94..7d54dfa689d7 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -383,8 +383,9 @@ private def finalize : M Expr := do unless s.missingExplicits.isEmpty do let mes := s.missingExplicits.map fun e => m!"{indentExpr e}" logError m!"insufficient number of arguments, \ - missing {s.missingExplicits.size} explicit argument(s) that are dependencies of a named argument.\n\n\ - Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. \ + {s.missingExplicits.size} missing explicit argument(s) are dependencies of a named argument and must be provided. \ + Typically each missing argument can be filled in with '_' or `(_)`. \ + In explicit mode, `_` for an instance argument triggers typeclass synthesis and `(_)` does not.\n\n\ These are the inferred missing arguments:\ {MessageData.joinSep mes.toList ""}" if !s.etaArgs.isEmpty then @@ -421,17 +422,16 @@ private def finalize : M Expr := do return e /-- -Returns a named argument that depends on the next argument, otherwise `none`. -If `onlySuppressDeps` is true, then only returns such a named argument with `suppressDeps` true. +Returns a named argument satisfying the predicate `p` that depends on the next argument, otherwise `none`. -/ -private def anyNamedArgDependsOnCurrent? (onlySuppressDeps := true) : M (Option NamedArg) := do +private def findNamedArgDependsOnCurrent? (p : NamedArg → Bool) : M (Option NamedArg) := do let s ← get - if s.namedArgs.any (·.suppressDeps || !onlySuppressDeps) then + if s.namedArgs.any p then forallTelescopeReducing s.fType fun xs _ => do let curr := xs[0]! for i in [1:xs.size] do let xDecl ← xs[i]!.fvarId!.getDecl - if let some arg := s.namedArgs.find? fun arg => (arg.suppressDeps || !onlySuppressDeps) && arg.name == xDecl.userName then + if let some arg := s.namedArgs.find? fun arg => p 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 @@ -536,6 +536,10 @@ mutual addNewArg argName x main + /-- + Create a fresh metavariable for the implicit argument. + - If `missingExplicit` is true, then it is added to the `missingExplicits` array. + -/ private partial def addImplicitArg (argName : Name) (missingExplicit : Bool := false) : M Expr := do let argType ← getArgExpectedType let arg ← if (← isNextOutParamOfLocalInstanceAndResult) then @@ -560,34 +564,41 @@ mutual private partial def processExplicitArg (argName : Name) : M Expr := do match (← get).args with | arg::args => - if ← pure !(← read).explicit <&&> Option.isSome <$> anyNamedArgDependsOnCurrent? then + -- Note: currently the following test never succeeds in explicit mode since `@x.f` notation does not exist. + if (← findNamedArgDependsOnCurrent? (·.suppressDeps)).isSome then /- - We treat the explicit argument `argName` as implicit if we have a named arguments that depends on it - that has the `suppressDeps` flag set to `true`. - The idea is that this explicit argument can be inferred using the type of the named argument. - Note that we also use this approach in the branch where there are no explicit arguments left. - This is important to make sure the system behaves in a uniform way. - - The motivation is that class projections can have explicit type parameters. - For example, consider the example on issue #1851 + 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`. - variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] [x : Approx x' X] - - #check f.val - #check f.val x.val + Consider ``` - The type of `Approx.val` is `{α : Type} → (a : α) → {X : Type} → [self : Approx a X] → X` - Note that the argument `a` is explicit since there is no way to infer it from the expected - type or the type of other explicit arguments. - Recall that `f.val` is sugar for `Approx.val (self := f)`. In both `#check` commands above - the user assumed that `a` does not need to be provided since it can be inferred from the type - of `self`. - Setting `suppressDeps` for this `self` argument enables this feature. - We used to that only in the branch where `(← get).args` was empty, but it created an asymmetry - because `#check f.val` worked as expected, but one would have to write `#check f.val _ x.val`. + 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 uniformly be 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`. + + We used to have this feature 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 also used to do this in case `(← 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 @@ -624,14 +635,14 @@ mutual throwError "invalid autoParam, argument must be a constant" | _, _, _ => if !(← get).namedArgs.isEmpty then - if let some arg ← anyNamedArgDependsOnCurrent? (onlySuppressDeps := false) then + if let some arg ← findNamedArgDependsOnCurrent? (fun _ => true) then /- Dependencies of named arguments cannot be turned into eta arguments. - Doing so leads to confusing type errors. - However, they can safely be turned into implicit arguments for elaboration. + Doing so leads to confusing type errors due to the eta arguments not being defeq to the inferred arguments. + However, they can safely be turned into implicit arguments for error recovery. This is an error unless the named argument is meant to suppress dependencies. -/ - addImplicitArg argName (missingExplicit := (← read).explicit || !arg.suppressDeps) + addImplicitArg argName (missingExplicit := !arg.suppressDeps) else if (← read).ellipsis then addImplicitArg argName else @@ -667,15 +678,17 @@ mutual finalize /-- - Process a `fType` of the form `[x : A] → B x`. - This method assume `fType` is a function type -/ + Process a `fType` of the form `[x : A] → B x`. + This method assume `fType` is a function type. + -/ private partial def processInstImplicitArg (argName : Name) : M Expr := do if (← read).explicit then if let some stx ← nextArgHole? then - /- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/ + -- We still use typeclass resolution for `_` arguments. + -- This behavior can be suppressed with `(_)`. let ty ← getArgExpectedType let arg ← mkInstMVar ty - addTermInfo' stx arg ty (← getLCtx) + addTermInfo' stx arg ty (← getLCtx) (elaborator := `Lean.Elab.Term.elabHole) modify fun s => { s with args := s.args.tail! } main else diff --git a/src/Lean/Elab/Arg.lean b/src/Lean/Elab/Arg.lean index 6ad2bac201c0..79057d7ac3ad 100644 --- a/src/Lean/Elab/Arg.lean +++ b/src/Lean/Elab/Arg.lean @@ -9,20 +9,21 @@ import Lean.Elab.Term namespace Lean.Elab.Term /-- - Auxiliary inductive datatype for combining unelaborated syntax - and already elaborated expressions. It is used to elaborate applications. -/ +Auxiliary inductive datatype for combining unelaborated syntax +and already elaborated expressions. It is used to elaborate applications. +-/ inductive Arg where | stx (val : Syntax) | expr (val : Expr) deriving Inhabited -/-- Named arguments created using the notation `(x := val)` -/ +/-- 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 the corresponding named parameter depends on - become implicit. This is used for projection notation to suppress explicit type parameters. -/ + /-- 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 deriving Inhabited diff --git a/tests/lean/run/explicitApp.lean b/tests/lean/run/explicitApp.lean index 566258b5dc53..7a615d19d14c 100644 --- a/tests/lean/run/explicitApp.lean +++ b/tests/lean/run/explicitApp.lean @@ -15,9 +15,10 @@ variable {p : Prop} [Decidable p] {α : Type} (x y : α) (h : ite p x y = x) /-- -error: insufficient number of arguments, missing 5 explicit argument(s) that are dependencies of a named argument. +error: insufficient number of arguments, 5 missing explicit argument(s) are dependencies of +a named argument and must be provided. Typically each missing argument can be filled in with '_' or `(_)`. +In explicit mode, `_` for an instance argument triggers typeclass synthesis and `(_)` does not. -Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. These are the inferred missing arguments: α x diff --git a/tests/lean/run/missingExplicitWithForwardNamedDep.lean b/tests/lean/run/missingExplicitWithForwardNamedDep.lean index c632cff690e2..1ac68fcfa328 100644 --- a/tests/lean/run/missingExplicitWithForwardNamedDep.lean +++ b/tests/lean/run/missingExplicitWithForwardNamedDep.lean @@ -16,9 +16,11 @@ def valOf2 (α β : Type) [s : Foo α β] : Nat := s.val /-- -error: insufficient number of arguments, missing 2 explicit argument(s) that are dependencies of a named argument. +error: insufficient number of arguments, 2 missing explicit argument(s) are dependencies of +a named argument and must be provided. Typically each missing argument can be filled in with '_' or `(_)`. +In explicit mode, `_` for an instance argument triggers typeclass synthesis and `(_)` does not. -Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. These are the inferred missing arguments: +These are the inferred missing arguments: Bool Bool --- @@ -38,9 +40,11 @@ def g {α : Type} (a b : α) := b def h (α : Type) (a b : α) := b /-- -error: insufficient number of arguments, missing 1 explicit argument(s) that are dependencies of a named argument. +error: insufficient number of arguments, 1 missing explicit argument(s) are dependencies of +a named argument and must be provided. Typically each missing argument can be filled in with '_' or `(_)`. +In explicit mode, `_` for an instance argument triggers typeclass synthesis and `(_)` does not. -Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. These are the inferred missing arguments: +These are the inferred missing arguments: Bool --- info: fun a => h Bool a true : Bool → Bool