Skip to content

Commit

Permalink
fix: refine how named arguments suppress explicit arguments (#5283)
Browse files Browse the repository at this point in the history
Recall that currently named arguments suppress all explicit parameters
that are dependencies. This PR limits this feature to only apply to true
structure projections, except in the case where it is triggered when
there are no more positional arguments. This preserves the primary
reason for generalizing this feature (issue #1851), while removing the
generalized feature, which has led to numerous confusions (issue #1867).
This also fixes a bug pointed out [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.40foo.20.28A.20.3A.3D.20bar.29.20_.20_/near/468564862)
where in `@` mode, instance implicit parameter dependencies to named
arguments would be suppressed unless the next positional argument was
`_`.

More detail:
* The `NamedArg` structure now has a `suppressDeps : Bool` field. It is
set to `true` for the `self` argument in structure projections. If there
is such a `NamedArg`, explicit parameters that are dependencies to the
named argument are turned into implicit arguments. The consequence is
that *all* structure projections are treated as if their type parameters
are implicit, even for class projections. This flag is *not* used for
generalized field notation.
* We preserve the suppression feature when there are no positional
arguments remaining. This feature pre-dates the fix to issue #1851, and
it is useful when combining named arguments and the eta expansion
feature, since dependencies of named arguments cannot be turned into eta
arguments. Plus, there are examples of the form `rw [lem (h := foo)]`
where `lem` has explicit arguments that `h` depends on.
* For instance implicit parameters in explicit mode, now `_` arguments
register terminfo and are hoverable.
* Now `..` is respected in explicit mode.

This implements RFC #5397. The `suppressDeps` flag suggests a future
possibility of a named argument syntax that can suppress dependencies.
  • Loading branch information
kmill authored Sep 27, 2024
1 parent 1b65727 commit 9f4075b
Show file tree
Hide file tree
Showing 4 changed files with 79 additions and 10 deletions.
48 changes: 38 additions & 10 deletions src/Lean/Elab/App.lean
Original file line number Diff line number Diff line change
Expand Up @@ -433,11 +433,13 @@ private def hasArgsToProcess : M Bool := do
let s ← get
return !s.args.isEmpty || !s.namedArgs.isEmpty

/-- Return `true` if the next argument at `args` is of the form `_` -/
private def isNextArgHole : M Bool := do
/--
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 (Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure true
| _ => pure false
| Arg.stx stx@(Syntax.node _ ``Lean.Parser.Term.hole _) :: _ => pure stx
| _ => pure none

/--
Return `true` if the next argument to be processed is the outparam of a local instance, and it the result type
Expand Down Expand Up @@ -649,20 +651,46 @@ mutual
This method assume `fType` is a function type -/
private partial def processInstImplicitArg (argName : Name) : M Expr := do
if (← read).explicit then
if (← isNextArgHole) then
if (← anyNamedArgDependsOnCurrent) then
/-
See the note in processExplicitArg about `anyNamedArgDependsOnCurrent`.
For consistency, instance implicit arguments should always become implicit if a named argument depends on them.
If we do not do this check here, then the `nextArgHole?` branch being before `processExplicitArg`
would result in counterintuitive behavior.
For example, without this block of code, in the following the `_` is optional.
When it is omitted, `processExplicitArg` sees that `h` depends on the `Decidable` instance
so makes the `Decidable` instance argument become implicit.
When it is `_`, the `nextArgHole?` branch allows it to be present.
The third example counterintuitively yields a "function expected" error.
```lean
theorem foo {p : Prop} [Decidable p] (h : ite p x y = x) : p := sorry
variable {p : Prop} [Decidable p] {α : Type} (x y : α) (h : ite p x y = x)
example : p := @foo (h := h)
example : p := @foo (h := h) _
example : p := @foo (h := h) inferInstance
```
-/
addImplicitArg argName
else if let some stx ← nextArgHole? then
/- Recall that if '@' has been used, and the argument is '_', then we still use type class resolution -/
let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
let ty ← getArgExpectedType
let arg ← mkInstMVar ty
addTermInfo' stx arg ty (← getLCtx)
modify fun s => { s with args := s.args.tail! }
addInstMVar arg.mvarId!
addNewArg argName arg
main
else
processExplicitArg argName
else
let arg ← mkFreshExprMVar (← getArgExpectedType) MetavarKind.synthetic
discard <| mkInstMVar (← getArgExpectedType)
main
where
mkInstMVar (ty : Expr) : M Expr := do
let arg ← mkFreshExprMVar ty MetavarKind.synthetic
addInstMVar arg.mvarId!
addNewArg argName arg
main
return arg

/-- Elaborate function application arguments. -/
partial def main : M Expr := do
Expand Down
6 changes: 6 additions & 0 deletions tests/lean/interactive/explicitAppInstHole.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
/-!
# Make sure there is type information on `_` for inst parameters in explicit mode
-/

example : Nat := @ite _ True _ 1 2
--^ textDocument/hover
8 changes: 8 additions & 0 deletions tests/lean/interactive/explicitAppInstHole.lean.expected.out
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
{"textDocument": {"uri": "file:///explicitAppInstHole.lean"},
"position": {"line": 4, "character": 29}}
{"range":
{"start": {"line": 4, "character": 29}, "end": {"line": 4, "character": 30}},
"contents":
{"value":
"```lean\ninstDecidableTrue : Decidable True\n```\n***\nA placeholder term, to be synthesized by unification. \n***\n*import Init.Core*",
"kind": "markdown"}}
27 changes: 27 additions & 0 deletions tests/lean/run/explicitApp.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
/-!
# Tests for app elaborator in explicit mode
-/

namespace Test1

/-!
Named arguments in explicit mode cause arguments it depends on to become implicit.
However, inst implicit arguments had odd behavior with `_`, since supplying `_` would override
the fact that it should be implicit.
-/

theorem foo {p : Prop} [Decidable p] (h : ite p x y = x) : p := sorry

variable {p : Prop} [Decidable p] {α : Type} (x y : α) (h : ite p x y = x)

example : p := @foo (h := h)
/--
error: function expected at
foo h
term has type
p
-/
#guard_msgs in
example : p := @foo (h := h) _

end Test1

0 comments on commit 9f4075b

Please sign in to comment.