diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 3ecd61a814..3ca700c106 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1832,13 +1832,15 @@ To infer a namespace from the expected type, we do the following operations: - if the type is of the form `c x₁ ... xₙ` with `c` a constant, then try using `c` as the namespace, and if that doesn't work, try unfolding the expression and continuing. -/ -private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do +private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitUnivs : List Level) (expectedType? : Option Expr) : TermElabM (List (Expr × Syntax × List Syntax)) := do unless id.isAtomic do throwError "Invalid dotted identifier notation: The name `{id}` must be atomic" tryPostponeIfNoneOrMVar expectedType? let some expectedType := expectedType? | throwNoExpectedType addCompletionInfo <| CompletionInfo.dotId idRef id (← getLCtx) expectedType? + -- We will check deprecations in `elabAppFnResolutions`. + withoutCheckDeprecated do withForallBody expectedType fun resultType => do go resultType expectedType #[] where @@ -1878,8 +1880,10 @@ where |>.filter (fun (_, fieldList) => fieldList.isEmpty) |>.map Prod.fst if !candidates.isEmpty then - candidates.mapM fun resolvedName => return (← mkConst resolvedName, ← getRef, []) + candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← getRef, []) else if let some (fvar, []) ← resolveLocalName fullName then + unless explicitUnivs.isEmpty do + throwInvalidExplicitUniversesForLocal fvar return [(fvar, ← getRef, [])] else throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`" @@ -1919,6 +1923,10 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra let some idx := idxStx.isFieldIdx? | throwError "Internal error: Unexpected field index syntax `{idxStx}`" elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc + let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) (explicit : Bool) : TermElabM (Array (TermElabResult Expr)) := do + let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes explicitUnivs expectedType? + -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns + elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true) match f with | `($(e).$idx:fieldIdx) => elabFieldIdx e idx explicit | `($e |>.$idx:fieldIdx) => elabFieldIdx e idx explicit @@ -1934,16 +1942,17 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra | `($id:ident.{$us,*}) => do let us ← elabExplicitUnivs us elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc - | `(@$id:ident) => - elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc - | `(@$_:ident.{$_us,*}) => + | `(.$id:ident) => elabDottedIdent id [] explicit + | `(.$id:ident.{$us,*}) => + let us ← elabExplicitUnivs us + elabDottedIdent id us explicit + | `(@$_:ident) + | `(@$_:ident.{$_us,*}) + | `(@.$_:ident) + | `(@.$_:ident.{$_us,*}) => elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc | `(@$_) => throwUnsupportedSyntax -- invalid occurrence of `@` | `(_) => throwError "A placeholder `_` cannot be used where a function is expected" - | `(.$id:ident) => - let res ← withRef f <| resolveDottedIdentFn id id.getId.eraseMacroScopes expectedType? - -- Use (forceTermInfo := true) because we want to record the result of .ident resolution even in patterns - elabAppFnResolutions f res lvals namedArgs args expectedType? explicit ellipsis overloaded acc (forceTermInfo := true) | _ => do let catchPostpone := !overloaded /- If we are processing a choice node, then we should use `catchPostpone == false` when elaborating terms. @@ -2086,13 +2095,15 @@ private def elabAtom : TermElab := fun stx expectedType? => do @[builtin_term_elab explicit] def elabExplicit : TermElab := fun stx expectedType? => match stx with - | `(@$_:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@` - | `(@$_:ident.{$_us,*}) => elabAtom stx expectedType? - | `(@$(_).$_:fieldIdx) => elabAtom stx expectedType? - | `(@$(_).$_:ident) => elabAtom stx expectedType? - | `(@($t)) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas - | `(@$t) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas - | _ => throwUnsupportedSyntax + | `(@$_:ident) => elabAtom stx expectedType? -- Recall that `elabApp` also has support for `@` + | `(@$_:ident.{$_us,*}) => elabAtom stx expectedType? + | `(@$(_).$_:fieldIdx) => elabAtom stx expectedType? + | `(@$(_).$_:ident) => elabAtom stx expectedType? + | `(@.$_:ident) => elabAtom stx expectedType? + | `(@.$_:ident.{$_us,*}) => elabAtom stx expectedType? + | `(@($t)) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas + | `(@$t) => elabTerm t expectedType? (implicitLambda := false) -- `@` is being used just to disable implicit lambdas + | _ => throwUnsupportedSyntax @[builtin_term_elab choice] def elabChoice : TermElab := elabAtom @[builtin_term_elab proj] def elabProj : TermElab := elabAtom diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index 0cfdb29f7b..555f15179b 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -2124,11 +2124,14 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels : let const ← withoutCheckDeprecated <| mkConst declName explicitLevels return (const, projs) :: result +def throwInvalidExplicitUniversesForLocal {α} (e : Expr) : TermElabM α := + throwError "invalid use of explicit universe parameters, `{e}` is a local variable" + def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String)) := do addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType? if let some (e, projs) ← resolveLocalName n then unless explicitLevels.isEmpty do - throwError "invalid use of explicit universe parameters, `{e}` is a local variable" + throwInvalidExplicitUniversesForLocal e return [(e, projs)] let preresolved := preresolved.filterMap fun | .decl n projs => some (n, projs) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 16b73a52ad..9e4abd0ed1 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -882,13 +882,19 @@ the available context). -/ def identProjKind := `Lean.Parser.Term.identProj +@[builtin_term_parser] def dotIdent := leading_parser + "." >> checkNoWsBefore >> rawIdent + def isIdent (stx : Syntax) : Bool := -- antiquotations should also be allowed where an identifier is expected stx.isAntiquot || stx.isIdent +def isIdentOrDotIdent (stx : Syntax) : Bool := + isIdent stx || stx.isOfKind ``dotIdent + /-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/ @[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser - checkStackTop isIdent "expected preceding identifier" >> + checkStackTop isIdentOrDotIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}" /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`. @@ -976,9 +982,6 @@ appropriate parameter for the underlying monad's `ST` effects, then passes it to @[builtin_term_parser] def dynamicQuot := withoutPosition <| leading_parser "`(" >> ident >> "| " >> incQuotDepth (parserOfStack 1) >> ")" -@[builtin_term_parser] def dotIdent := leading_parser - "." >> checkNoWsBefore >> rawIdent - /-- Implementation of the `show_term` term elaborator. -/ diff --git a/tests/elab/10984.lean b/tests/elab/10984.lean new file mode 100644 index 0000000000..48f16cfe6f --- /dev/null +++ b/tests/elab/10984.lean @@ -0,0 +1,115 @@ +/-! +# Dotted function notation can handle `@` and universe levels +-/ + +set_option warn.sorry false +set_option linter.deprecated true +set_option pp.mvars.anonymous false + +/-! +Explicit `@` +-/ +/-- info: [] : List Nat -/ +#guard_msgs in #check (@.nil Nat : List _) + +/-! +Explicit `@` disables implicit lambda +-/ +/-- +error: Type mismatch + @List.nil +has type + {α : Type _} → List α +but is expected to have type + List ?_ +-/ +#guard_msgs in #check (@.nil : List _) + +/-! +Universe levels. +-/ +example : List Nat := .nil.{0} + +/-- +error: Type mismatch + [] +has type + List.{1} ?_ +of sort `Type 1` but is expected to have type + List.{0} Nat +of sort `Type` +-/ +#guard_msgs in +example : List Nat := .nil.{1} + +/-- error: too many explicit universe levels for `List.nil` -/ +#guard_msgs in +example : List Nat := .nil.{0,0} + +/-! +Explicit plus universe levels also disables implicit lambda +-/ +/-- +error: Type mismatch + @List.nil +has type + {α : Type} → List α +of sort `Type 1` but is expected to have type + List Nat +of sort `Type` +-/ +#guard_msgs in example : List Nat := @.nil.{0} + +/-! +Example of `@` from Floris van Doorn at https://github.com/leanprover/lean4/issues/10984 +-/ +example {α : Type} (f : ∀ {α}, List α → List α) : f (@.nil α) = .nil := sorry + +/-! +Example of `@` plus universe levels adapated from https://github.com/leanprover/lean4/issues/10984 +-/ +example {α : Type u} (f : ∀ {α}, List α → List α) : f (@.nil.{u} α) = .nil := sorry + +/-! +Example from Arthur Adjedj at https://github.com/leanprover/lean4/issues/8743 +-/ +/-- info: [2] : List Nat -/ +#guard_msgs in #check (List.cons.{0} 2 [] : List Nat) +/-- info: [2] : List Nat -/ +#guard_msgs in #check (.cons.{0} 2 [] : List Nat) + +/-- +error: Type mismatch + [2] +has type + List.{1} ?_ +of sort `Type 1` but is expected to have type + List.{0} Nat +of sort `Type` +-/ +#guard_msgs in #check (.cons.{1} 2 [] : List Nat) + +/-! +Regression test: This used to give a deprecation warning on the first `#check`. +-/ +def MyNS1.List.nil' : List Nat := [] +@[deprecated MyNS1.List.nil' (since := "forever")] def MyNS2.List.nil' : List Int := [] + +/-- info: MyNS1.List.nil' : List Nat -/ +#guard_msgs in +open MyNS1 MyNS2 in #check (.nil' : List Nat) + +/-- +warning: `MyNS2.List.nil'` has been deprecated: Use `MyNS1.List.nil'` instead + +Note: The updated constant has a different type: + List Nat +instead of + List Int + +Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.nil'` to `MyNS1.List.nil' x`). +--- +info: MyNS2.List.nil' : List Int +-/ +#guard_msgs in +open MyNS1 MyNS2 in #check (.nil' : List Int)