From 0db6daa8f125424f79b6a270d7c3777f7fb0f66e Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sat, 28 Sep 2024 18:22:12 -0700 Subject: [PATCH] feat: actual implementation for #5283 (#5512) I did a bad git rebase before merging #5283, which reverted it to an earlier version. This PR has the actual implementation of RFC #5397. --- src/Init/Data/NeZero.lean | 2 +- src/Lean/Elab/App.lean | 131 +++++++++--------- src/Lean/Elab/Arg.lean | 10 +- .../missingExplicitWithForwardNamedDep.lean | 30 ---- ...licitWithForwardNamedDep.lean.expected.out | 6 - tests/lean/run/270.lean | 2 +- tests/lean/run/computedFields.lean | 4 +- tests/lean/run/explicitApp.lean | 11 +- .../missingExplicitWithForwardNamedDep.lean | 33 +++++ tests/lean/run/structuralMutual.lean | 6 +- 10 files changed, 120 insertions(+), 115 deletions(-) delete mode 100644 tests/lean/missingExplicitWithForwardNamedDep.lean delete mode 100644 tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out create mode 100644 tests/lean/run/missingExplicitWithForwardNamedDep.lean diff --git a/src/Init/Data/NeZero.lean b/src/Init/Data/NeZero.lean index 4502ccbfee19..1961d0c4d0d6 100644 --- a/src/Init/Data/NeZero.lean +++ b/src/Init/Data/NeZero.lean @@ -35,4 +35,4 @@ theorem neZero_iff {n : R} : NeZero n ↔ n ≠ 0 := ⟨fun h ↦ h.out, NeZero.mk⟩ @[simp] theorem neZero_zero_iff_false {α : Type _} [Zero α] : NeZero (0 : α) ↔ False := - ⟨fun h ↦ h.ne rfl, fun h ↦ h.elim⟩ + ⟨fun _ ↦ NeZero.ne (0 : α) rfl, fun h ↦ h.elim⟩ diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index bf9f872e0568..5f9e18e95962 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -411,21 +411,23 @@ private def finalize : M Expr := do synthesizeAppInstMVars return e -/-- Return `true` if there is a named argument that depends on the next argument. -/ -private def anyNamedArgDependsOnCurrent : M Bool := do +/-- +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 false + return none else forallTelescopeReducing s.fType fun xs _ => do let curr := xs[0]! for i in [1:xs.size] do let xDecl ← xs[i]!.fvarId!.getDecl - if s.namedArgs.any fun arg => arg.name == xDecl.userName then + 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 true - return false + return arg + return none /-- Return `true` if there are regular or named arguments to be processed. -/ @@ -514,8 +516,9 @@ where mutual /-- - Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`, - and then execute the main loop.-/ + Create a fresh local variable with the current binder name and argument type, add it to `etaArgs` and `f`, + and then execute the main loop. + -/ private partial def addEtaArg (argName : Name) : M Expr := do let n ← getBindingName let type ← getArgExpectedType @@ -524,6 +527,9 @@ mutual addNewArg argName x main + /-- + Create a fresh metavariable for the implicit argument, add it to `f`, and thn execute the main loop. + -/ private partial def addImplicitArg (argName : Name) : M Expr := do let argType ← getArgExpectedType let arg ← if (← isNextOutParamOfLocalInstanceAndResult) then @@ -541,35 +547,47 @@ mutual main /-- - 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 processExplicitArg (argName : Name) : M Expr := do match (← get).args with | arg::args => - if (← anyNamedArgDependsOnCurrent) then + -- 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 named arguments that depend on it. - The idea is that this explicit argument can be inferred using the type of the named argument one. - 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. - Moreover, users rely on this behavior. 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 + ``` + variable {α β X Y : Type} {f' : α → β} {x' : α} [f : Approx f' (X → Y)] ``` - 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`. - 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` + 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 @@ -609,17 +627,20 @@ mutual | false, _, some _ => throwError "invalid autoParam, argument must be a constant" | _, _, _ => - if !(← get).namedArgs.isEmpty then - if (← anyNamedArgDependsOnCurrent) then - addImplicitArg argName - else if (← read).ellipsis then + if (← read).ellipsis then + addImplicitArg argName + else if !(← get).namedArgs.isEmpty then + if let some _ ← 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. + -/ addImplicitArg argName else addEtaArg argName else if !(← read).explicit then - if (← read).ellipsis then - addImplicitArg argName - else if (← fTypeHasOptAutoParams) then + if (← fTypeHasOptAutoParams) then addEtaArg argName else finalize @@ -647,37 +668,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 (← 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 -/ + if let some stx ← nextArgHole? then + -- 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 modify fun s => { s with args := s.args.tail! } main else @@ -1278,7 +1279,7 @@ private partial def mkBaseProjections (baseStructName : Name) (structName : Name let mut e := e for projFunName in path do let projFn ← mkConst projFunName - e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false) + e ← elabAppArgs projFn #[{ name := `self, val := Arg.expr e, suppressDeps := true }] (args := #[]) (expectedType? := none) (explicit := false) (ellipsis := false) return e private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do @@ -1362,10 +1363,10 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp let projFn ← mkConst info.projFn let projFn ← addProjTermInfo lval.getRef projFn if lvals.isEmpty then - let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f } + let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true } elabAppArgs projFn namedArgs args expectedType? explicit ellipsis else - let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f }] #[] (expectedType? := none) (explicit := false) (ellipsis := false) + let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false) loop f lvals else unreachable! diff --git a/src/Lean/Elab/Arg.lean b/src/Lean/Elab/Arg.lean index 81fd73ec9d55..79057d7ac3ad 100644 --- a/src/Lean/Elab/Arg.lean +++ b/src/Lean/Elab/Arg.lean @@ -9,18 +9,22 @@ 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 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/missingExplicitWithForwardNamedDep.lean b/tests/lean/missingExplicitWithForwardNamedDep.lean deleted file mode 100644 index 9633bb4acee7..000000000000 --- a/tests/lean/missingExplicitWithForwardNamedDep.lean +++ /dev/null @@ -1,30 +0,0 @@ -class Foo (α : Type) (β : Type) where - val : Nat - a : α - b : β - -#check Foo.val - -def valOf [s : Foo α β] : Nat := - s.val - -#eval valOf (s := { val := 10, a := true, b := false : Foo Bool Bool }) - -def valOf2 (α β : Type) [s : Foo α β] : Nat := - s.val - -#check valOf2 (s := { val := 10, a := true, b := false : Foo Bool Bool }) --- valOf2 Bool Bool - -def f (x y z : Nat) := x + y + z - -#check f (z := 10) --- fun (x y : Nat) => f x y 10 : Nat → Nat → Nat - -def g {α : Type} (a b : α) := b -#check g (b := 10) --- fun (a : Nat) => g a 10 - -def h (α : Type) (a b : α) := b -#check h (b := true) --- fun a => h Bool a true diff --git a/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out b/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out deleted file mode 100644 index b80d58fcc0f9..000000000000 --- a/tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out +++ /dev/null @@ -1,6 +0,0 @@ -Foo.val (α β : Type) [self : Foo α β] : Nat -10 -valOf2 Bool Bool : Nat -fun x y => f x y 10 : Nat → Nat → Nat -fun a => g a 10 : Nat → Nat -fun a => h Bool a true : Bool → Bool diff --git a/tests/lean/run/270.lean b/tests/lean/run/270.lean index de05864acb20..99a6bd8747fa 100644 --- a/tests/lean/run/270.lean +++ b/tests/lean/run/270.lean @@ -23,7 +23,7 @@ theorem addComm5 [CommAddSemigroup α] {a b c : α} : a + b + c = a + c + b := b have h' := congrArg (a + ·) h; simp at h'; rw [←addAssoc] at h'; - rw [←@addAssoc (a := a)] at h'; + rw [←addAssoc (a := a)] at h'; exact h'; } diff --git a/tests/lean/run/computedFields.lean b/tests/lean/run/computedFields.lean index 37420fd536e4..234a8fc79db9 100644 --- a/tests/lean/run/computedFields.lean +++ b/tests/lean/run/computedFields.lean @@ -32,9 +32,9 @@ inductive B.C (α : Type u) : Nat → Type u with @[computed_field] hash : ∀ α i, C α i → UInt64 | _, _, .a => 1 - | _, _, .b c => 42 + c.hash + | _, _, .b c => 42 + c.hash _ _ -#guard (B.C.b (α := Nat) (.a) (d := .a)).hash == 43 +#guard (B.C.b (α := Nat) (.a) (d := .a)).hash _ _ == 43 end WithIndices diff --git a/tests/lean/run/explicitApp.lean b/tests/lean/run/explicitApp.lean index 188575def36e..a31a2f4d6c0b 100644 --- a/tests/lean/run/explicitApp.lean +++ b/tests/lean/run/explicitApp.lean @@ -5,16 +5,19 @@ 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. +Named arguments in explicit mode should not cause arguments they depend on to become implicit, +unless there are no more positional arguments. -/ 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) _ _ _ _ _ + /-- error: function expected at foo h @@ -22,6 +25,6 @@ term has type p -/ #guard_msgs in -example : p := @foo (h := h) _ +example : p := @foo (h := h) _ _ _ _ _ _ end Test1 diff --git a/tests/lean/run/missingExplicitWithForwardNamedDep.lean b/tests/lean/run/missingExplicitWithForwardNamedDep.lean new file mode 100644 index 000000000000..11accad9b8b2 --- /dev/null +++ b/tests/lean/run/missingExplicitWithForwardNamedDep.lean @@ -0,0 +1,33 @@ +class Foo (α : Type) (β : Type) where + val : Nat + a : α + b : β + +/-- info: Foo.val (α β : Type) [self : Foo α β] : Nat -/ +#guard_msgs in #check Foo.val + +def valOf [s : Foo α β] : Nat := + s.val + +/-- info: 10 -/ +#guard_msgs in #eval valOf (s := { val := 10, a := true, b := false : Foo Bool Bool }) + +def valOf2 (α β : Type) [s : Foo α β] : Nat := + s.val + +/-- info: valOf2 Bool Bool : Nat -/ +#guard_msgs in #check valOf2 (s := { val := 10, a := true, b := false : Foo Bool Bool }) + +def f (x y z : Nat) := x + y + z + +/-- info: fun x y => f x y 10 : Nat → Nat → Nat -/ +#guard_msgs in +#check f (z := 10) + +def g {α : Type} (a b : α) := b +/-- info: fun a => g a 10 : Nat → Nat -/ +#guard_msgs in #check g (b := 10) + +def h (α : Type) (a b : α) := b +/-- info: fun a => h Bool a true : Bool → Bool -/ +#guard_msgs in #check h (b := true) diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index cae9891de1b5..63d7f0a4337c 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -185,12 +185,12 @@ inductive B (m : Nat) : Nat → Type end mutual -def A.size (m n : Nat) : A m n → Nat +def A.size {m n : Nat} : A m n → Nat | .self a => a.size + m | .other b => b.size + m | .empty => 0 termination_by structural x => x -def B.size (m n : Nat): B m n → Nat +def B.size {m n : Nat} : B m n → Nat | .self b => b.size + m | .other a => a.size + m | .empty => 0 @@ -470,7 +470,7 @@ error: cannot use specified parameter for structural recursion: which does not come before the varying parameters and before the indices of the recursion parameter. -/ #guard_msgs in -def T.a (n : Nat) : T n n → Nat +def T.a {n : Nat} : T n n → Nat | .z => 0 | .n t => t.a + 1 termination_by structural t => t