From ce523506e027b5d3907d4885289ab875c78429fe Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 8 Sep 2024 11:23:54 -0700 Subject: [PATCH] squashed 3fb427ecb112bb80b85c63f995db7f1b0510d131 --- src/Lean/Elab/App.lean | 88 +++++++++++++------ src/Lean/Elab/Arg.lean | 3 + .../lean/interactive/explicitAppInstHole.lean | 6 ++ .../explicitAppInstHole.lean.expected.out | 8 ++ .../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 | 41 +++++++++ .../missingExplicitWithForwardNamedDep.lean | 48 ++++++++++ tests/lean/run/structuralMutual.lean | 6 +- 11 files changed, 171 insertions(+), 71 deletions(-) create mode 100644 tests/lean/interactive/explicitAppInstHole.lean create mode 100644 tests/lean/interactive/explicitAppInstHole.lean.expected.out delete mode 100644 tests/lean/missingExplicitWithForwardNamedDep.lean delete mode 100644 tests/lean/missingExplicitWithForwardNamedDep.lean.expected.out create mode 100644 tests/lean/run/explicitApp.lean create mode 100644 tests/lean/run/missingExplicitWithForwardNamedDep.lean diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 373e029f9876..38853659ab94 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -145,6 +145,8 @@ structure State where When `..` is used, eta-expansion is disabled, and missing arguments are treated as `_`. -/ etaArgs : Array Expr := #[] + /-- Missing explicit arguments, from dependencies of named arguments. These cannot be eta arguments. -/ + missingExplicits : Array 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. -/ @@ -378,6 +380,13 @@ private def finalize : M Expr := do -- Register the error context of implicits for mvarId in s.toSetErrorCtx do registerMVarErrorImplicitArgInfo mvarId ref e + 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. \ + These are the inferred missing arguments:\ + {MessageData.joinSep mes.toList ""}" if !s.etaArgs.isEmpty then e ← mkLambdaFVars s.etaArgs e /- @@ -411,21 +420,24 @@ 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`. +If `onlySuppressDeps` is true, then only returns such a named argument with `suppressDeps` true. +-/ +private def anyNamedArgDependsOnCurrent? (onlySuppressDeps := true) : M (Option NamedArg) := do let s ← get - if s.namedArgs.isEmpty then - return false - else + if s.namedArgs.any (·.suppressDeps || !onlySuppressDeps) 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 s.namedArgs.any fun arg => arg.name == xDecl.userName then + if let some arg := s.namedArgs.find? fun arg => (arg.suppressDeps || !onlySuppressDeps) && 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 + else + return none /-- Return `true` if there are regular or named arguments to be processed. -/ @@ -433,11 +445,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 @@ -522,7 +536,7 @@ mutual addNewArg argName x main - private partial def addImplicitArg (argName : Name) : M Expr := do + private partial def addImplicitArg (argName : Name) (missingExplicit : Bool := false) : M Expr := do let argType ← getArgExpectedType let arg ← if (← isNextOutParamOfLocalInstanceAndResult) then let arg ← mkFreshExprMVar argType @@ -535,6 +549,8 @@ mutual else mkFreshExprMVar argType modify fun s => { s with toSetErrorCtx := s.toSetErrorCtx.push arg.mvarId! } + if missingExplicit then + modify fun s => { s with missingExplicits := s.missingExplicits.push arg } addNewArg argName arg main @@ -544,13 +560,16 @@ mutual private partial def processExplicitArg (argName : Name) : M Expr := do match (← get).args with | arg::args => - if (← anyNamedArgDependsOnCurrent) then + if ← pure !(← read).explicit <&&> Option.isSome <$> anyNamedArgDependsOnCurrent? 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. + 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. - Moreover, users rely on this behavior. For example, consider the example on issue #1851 + + The motivation is that class projections can have explicit type parameters. + For example, consider the example on issue #1851 ``` class Approx {α : Type} (a : α) (X : Type) : Type where val : X @@ -566,8 +585,9 @@ mutual 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` + because `#check f.val` worked as expected, but one would have to write `#check f.val _ x.val`. -/ return (← addImplicitArg argName) propagateExpectedType arg @@ -604,8 +624,14 @@ mutual throwError "invalid autoParam, argument must be a constant" | _, _, _ => if !(← get).namedArgs.isEmpty then - if (← anyNamedArgDependsOnCurrent) then - addImplicitArg argName + if let some arg ← anyNamedArgDependsOnCurrent? (onlySuppressDeps := false) 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. + This is an error unless the named argument is meant to suppress dependencies. + -/ + addImplicitArg argName (missingExplicit := (← read).explicit || !arg.suppressDeps) else if (← read).ellipsis then addImplicitArg argName else @@ -645,20 +671,24 @@ 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 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 @@ -1221,7 +1251,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 @@ -1305,10 +1335,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..6ad2bac201c0 100644 --- a/src/Lean/Elab/Arg.lean +++ b/src/Lean/Elab/Arg.lean @@ -21,6 +21,9 @@ 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. -/ + suppressDeps : Bool := false deriving Inhabited /-- diff --git a/tests/lean/interactive/explicitAppInstHole.lean b/tests/lean/interactive/explicitAppInstHole.lean new file mode 100644 index 000000000000..96f5abb08db6 --- /dev/null +++ b/tests/lean/interactive/explicitAppInstHole.lean @@ -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 diff --git a/tests/lean/interactive/explicitAppInstHole.lean.expected.out b/tests/lean/interactive/explicitAppInstHole.lean.expected.out new file mode 100644 index 000000000000..5b8f04d000f9 --- /dev/null +++ b/tests/lean/interactive/explicitAppInstHole.lean.expected.out @@ -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"}} 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 new file mode 100644 index 000000000000..566258b5dc53 --- /dev/null +++ b/tests/lean/run/explicitApp.lean @@ -0,0 +1,41 @@ +/-! +# Tests for app elaborator in explicit mode +-/ + +namespace Test1 + +/-! +Named arguments in explicit mode should not cause arguments they depend on to become implicit, +except when doing error recovery. +-/ + +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) + + +/-- +error: insufficient number of arguments, missing 5 explicit argument(s) that are dependencies of a named argument. + +Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. +These are the inferred missing arguments: + α + x + y + p + inst✝ +-/ +#guard_msgs in example : p := @foo (h := h) + +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 diff --git a/tests/lean/run/missingExplicitWithForwardNamedDep.lean b/tests/lean/run/missingExplicitWithForwardNamedDep.lean new file mode 100644 index 000000000000..c632cff690e2 --- /dev/null +++ b/tests/lean/run/missingExplicitWithForwardNamedDep.lean @@ -0,0 +1,48 @@ +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 + +/-- +error: insufficient number of arguments, missing 2 explicit argument(s) that are dependencies of a named argument. + +Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. These are the inferred missing arguments: + Bool + Bool +--- +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 +/-- +error: insufficient number of arguments, missing 1 explicit argument(s) that are dependencies of a named argument. + +Such arguments can be filled in with '_', or '(_)' if it is a non-canonical instance argument. These are the inferred missing arguments: + Bool +--- +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