From c60f97a3fa7f2ef1b5dec6d48b865baec305da89 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Thu, 9 Apr 2026 06:29:10 -0700 Subject: [PATCH] feat: allow field notation to use explicit universe levels (#13262) This PR extends Lean's syntax to allow explicit universe levels in expressions such as `e.f.{u,v}`, `(f e).g.{u}`, and `e |>.f.{u,v} x y z`. It fixes a bug where universe levels would be attributed to the wrong expression; for example `x.f.{u}` would be interpreted as `x.{u}.f`. It also changes the syntax of top-level declarations to not allow space between the identifier and the universe level list, and it fixes a bug in the `checkWsBefore` parser where it would not detect whitespace across `optional` parsers. Closes #8743 --- src/Lean/Elab/App.lean | 131 +++++++++-------- src/Lean/Elab/Quotation/Precheck.lean | 2 +- src/Lean/Elab/Term/TermElabM.lean | 57 +++++--- src/Lean/Parser/Basic.lean | 20 +-- src/Lean/Parser/Command.lean | 4 +- src/Lean/Parser/Term.lean | 19 ++- tests/elab/8743.lean | 195 ++++++++++++++++++++++++++ 7 files changed, 337 insertions(+), 91 deletions(-) create mode 100644 tests/elab/8743.lean diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 3ca700c106..19da5d0ba6 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -13,6 +13,7 @@ public import Lean.IdentifierSuggestion import all Lean.Elab.ErrorUtils import Lean.Elab.DeprecatedArg import Init.Omega +import Init.Data.List.MapIdx public section @@ -1299,13 +1300,13 @@ where inductive LValResolution where /-- When applied to `f`, effectively expands to `BaseStruct.fieldName (self := Struct.toBase f)`. This is a special named argument where it suppresses any explicit arguments depending on it so that type parameters don't need to be supplied. -/ - | projFn (baseStructName : Name) (structName : Name) (fieldName : Name) + | projFn (baseStructName : Name) (structName : Name) (fieldName : Name) (levels : List Level) /-- Similar to `projFn`, but for extracting field indexed by `idx`. Works for one-constructor inductive types in general. -/ | projIdx (structName : Name) (idx : Nat) /-- When applied to `f`, effectively expands to `constName ... (Struct.toBase f)`, with the argument placed in the correct positional argument if possible, or otherwise as a named argument. The `Struct.toBase` is not present if `baseStructName == structName`, in which case these do not need to be structures. Supports generalized field notation. -/ - | const (baseStructName : Name) (structName : Name) (constName : Name) + | const (baseStructName : Name) (structName : Name) (constName : Name) (levels : List Level) /-- Like `const`, but with `fvar` instead of `constName`. The `baseName` is the base name of the type to search for in the parameter list. -/ | localRec (baseName : Name) (fvar : Expr) @@ -1380,7 +1381,7 @@ private def reverseFieldLookup (env : Environment) (fieldName : String) := private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM LValResolution := do match eType.getAppFn, lval with - | .const structName _, LVal.fieldIdx ref idx => + | .const structName _, LVal.fieldIdx ref idx levels => if idx == 0 then throwError "Invalid projection: Index must be greater than 0" let env ← getEnv @@ -1393,10 +1394,14 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L if idx - 1 < numFields then if isStructure env structName then let fieldNames := getStructureFields env structName - return LValResolution.projFn structName structName fieldNames[idx - 1]! + return LValResolution.projFn structName structName fieldNames[idx - 1]! levels else /- `structName` was declared using `inductive` command. So, we don't projection functions for it. Thus, we use `Expr.proj` -/ + unless levels.isEmpty do + throwError "Invalid projection: Explicit universe levels are only supported for inductive types \ + defined using the `structure` command. \ + The expression{indentExpr e}\nhas type{inlineExpr eType}which is not a `structure`." return LValResolution.projIdx structName (idx - 1) else if numFields == 0 then @@ -1409,31 +1414,33 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L ++ MessageData.note m!"The expression{indentExpr e}\nhas type{inlineExpr eType}which has only \ {numFields} field{numFields.plural}" ++ tupleHint - | .const structName _, LVal.fieldName ref fieldName _ _ => withRef ref do + | .const structName _, LVal.fieldName ref fieldName levels _ _ => withRef ref do let env ← getEnv if isStructure env structName then if let some baseStructName := findField? env structName (Name.mkSimple fieldName) then - return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName) + return LValResolution.projFn baseStructName structName (Name.mkSimple fieldName) levels -- Search the local context first let fullName := Name.mkStr (privateToUserName structName) fieldName for localDecl in (← getLCtx) do if localDecl.isAuxDecl then if let some localDeclFullName := (← getLCtx).auxDeclToFullName.get? localDecl.fvarId then if fullName == privateToUserName localDeclFullName then + unless levels.isEmpty do + throwInvalidExplicitUniversesForLocal localDecl.toExpr /- LVal notation is being used to make a "local" recursive call. -/ return LValResolution.localRec structName localDecl.toExpr -- Then search the environment if let some (baseStructName, fullName) ← findMethod? structName (.mkSimple fieldName) then - return LValResolution.const baseStructName structName fullName + return LValResolution.const baseStructName structName fullName levels throwInvalidFieldAt ref fieldName fullName -- Suggest a potential unreachable private name as hint. This does not cover structure -- inheritance, nor `import all`. (declHint := (mkPrivateName env structName).mkStr fieldName) - | .forallE .., LVal.fieldName ref fieldName suffix? fullRef => + | .forallE .., LVal.fieldName ref fieldName levels suffix? fullRef => let fullName := Name.str `Function fieldName if (← getEnv).contains fullName then - return LValResolution.const `Function `Function fullName + return LValResolution.const `Function `Function fullName levels match e.getAppFn, suffix? with | Expr.const c _, some suffix => throwUnknownNameWithSuggestions (idOrConst := "constant") (ref? := fullRef) (c ++ suffix) @@ -1443,7 +1450,7 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L throwError "Invalid projection: Projections cannot be used on functions, and{indentExpr e}\n\ has function type{inlineExprTrailing eType}" - | .mvar .., .fieldName _ fieldName _ _ => + | .mvar .., .fieldName _ fieldName levels _ _ => let hint := match reverseFieldLookup (← getEnv) fieldName with | #[] => MessageData.nil | #[opt] => .hint' m!"Consider replacing the field projection `.{fieldName}` with a call to the function `{.ofConstName opt}`." @@ -1451,13 +1458,13 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L {MessageData.joinSep (opts.toList.map (indentD m!"• `{.ofConstName ·}`")) .nil}" throwNamedError lean.invalidField (m!"Invalid field notation: Type of{indentExpr e}\nis not \ known; cannot resolve field `{fieldName}`" ++ hint) - | .mvar .., .fieldIdx _ i => + | .mvar .., .fieldIdx _ i _ => throwError m!"Invalid projection: Type of{indentExpr e}\nis not known; cannot resolve \ projection `{i}`" | _, _ => match e.getAppFn, lval with - | Expr.const c _, .fieldName _ref _fieldName (some suffix) fullRef => + | Expr.const c _, .fieldName _ref _fieldName _levels (some suffix) fullRef => throwUnknownNameWithSuggestions (idOrConst := "constant") (ref? := fullRef) (c ++ suffix) | _, .fieldName .. => throwNamedError lean.invalidField m!"Invalid field notation: Field projection operates on \ @@ -1706,12 +1713,12 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp let f ← mkProjAndCheck structName idx f let f ← addTermInfo lval.getRef f loop f lvals - | LValResolution.projFn baseStructName structName fieldName => + | LValResolution.projFn baseStructName structName fieldName levels => let f ← mkBaseProjections baseStructName structName f let some info := getFieldInfo? (← getEnv) baseStructName fieldName | unreachable! if (← isInaccessiblePrivateName info.projFn) then throwError "Field `{fieldName}` from structure `{structName}` is private" - let projFn ← withRef lval.getRef <| mkConst info.projFn + let projFn ← withRef lval.getRef <| mkConst info.projFn levels let projFn ← addProjTermInfo lval.getRef projFn if lvals.isEmpty then let namedArgs ← addNamedArg namedArgs { name := `self, val := Arg.expr f, suppressDeps := true } @@ -1719,9 +1726,9 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp else let f ← elabAppArgs projFn #[{ name := `self, val := Arg.expr f, suppressDeps := true }] #[] (expectedType? := none) (explicit := false) (ellipsis := false) loop f lvals - | LValResolution.const baseStructName structName constName => + | LValResolution.const baseStructName structName constName levels => let f ← if baseStructName != structName then mkBaseProjections baseStructName structName f else pure f - let projFn ← withRef lval.getRef <| mkConst constName + let projFn ← withRef lval.getRef <| mkConst constName levels let projFn ← addProjTermInfo lval.getRef projFn if lvals.isEmpty then let (args, namedArgs) ← addLValArg baseStructName f args namedArgs projFn explicit @@ -1772,15 +1779,19 @@ false, no elaboration function executed by `x` will reset it to /-- Elaborates the resolutions of a function. The `fns` array is the output of `resolveName'`. -/ -private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax)) (lvals : List LVal) +private def elabAppFnResolutions (fRef : Syntax) (fns : List (Expr × Syntax × List Syntax × List Level)) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) (forceTermInfo : Bool := false) : TermElabM (Array (TermElabResult Expr)) := do let overloaded := overloaded || fns.length > 1 -- Set `errToSorry` to `false` if `fns` > 1. See comment above about the interaction between `errToSorry` and `observing`. withReader (fun ctx => { ctx with errToSorry := fns.length == 1 && ctx.errToSorry }) do - fns.foldlM (init := acc) fun acc (f, fIdent, fields) => do - let lvals' := toLVals fields (first := true) + fns.foldlM (init := acc) fun acc (f, fIdent, fields, projLevels) => do + let lastIdx := fields.length - 1 + let lvals' := fields.mapIdx fun idx field => + let suffix? := if idx == 0 then some <| toName fields else none + let levels := if idx == lastIdx then projLevels else [] + LVal.fieldName field field.getId.getString! levels suffix? fRef let s ← observing do checkDeprecated fIdent f let f ← addTermInfo fIdent f expectedType? (force := forceTermInfo) @@ -1794,11 +1805,6 @@ where | field :: fields => .mkStr (go fields) field.getId.toString go fields.reverse - toLVals : List Syntax → (first : Bool) → List LVal - | [], _ => [] - | field::fields, true => .fieldName field field.getId.getString! (toName (field::fields)) fRef :: toLVals fields false - | field::fields, false => .fieldName field field.getId.getString! none fRef :: toLVals fields false - private def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level) (lvals : List LVal) (namedArgs : Array NamedArg) (args : Array Arg) (expectedType? : Option Expr) (explicit ellipsis overloaded : Bool) (acc : Array (TermElabResult Expr)) : @@ -1832,7 +1838,7 @@ 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) (explicitUnivs : List Level) (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 × List Level)) := do unless id.isAtomic do throwError "Invalid dotted identifier notation: The name `{id}` must be atomic" tryPostponeIfNoneOrMVar expectedType? @@ -1844,7 +1850,7 @@ private partial def resolveDottedIdentFn (idRef : Syntax) (id : Name) (explicitU withForallBody expectedType fun resultType => do go resultType expectedType #[] where - throwNoExpectedType := do + throwNoExpectedType {α} : TermElabM α := do let hint ← match reverseFieldLookup (← getEnv) (id.getString!) with | #[] => pure MessageData.nil | suggestions => @@ -1863,7 +1869,7 @@ where withForallBody body k else k type - go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax)) := do + go (resultType : Expr) (expectedType : Expr) (previousExceptions : Array Exception) : TermElabM (List (Expr × Syntax × List Syntax × List Level)) := do let resultType ← instantiateMVars resultType let resultTypeFn := resultType.getAppFn try @@ -1880,11 +1886,11 @@ where |>.filter (fun (_, fieldList) => fieldList.isEmpty) |>.map Prod.fst if !candidates.isEmpty then - candidates.mapM fun resolvedName => return (← mkConst resolvedName explicitUnivs, ← 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, [])] + return [(fvar, ← getRef, [], [])] else throwUnknownIdentifierAt (← getRef) (declHint := fullName) <| m!"Unknown constant `{.ofConstName fullName}`" ++ .note m!"Inferred this name from the expected resulting type of `.{id}`:{indentExpr expectedType}" @@ -1914,26 +1920,37 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra withReader (fun ctx => { ctx with errToSorry := false }) do f.getArgs.foldlM (init := acc) fun acc f => elabAppFn f lvals namedArgs args expectedType? explicit ellipsis true acc else - let elabFieldName (e field : Syntax) (explicit : Bool) := do - let newLVals := field.identComponents.map fun comp => - -- We use `none` in `suffix?` since `field` can't be part of a composite name - LVal.fieldName comp comp.getId.getString! none f + let elabFieldName (e field : Syntax) (explicitUnivs : List Level) := do + let comps := field.identComponents + let lastIdx := comps.length - 1 + let newLVals := comps.mapIdx fun idx comp => + let levels := if idx = lastIdx then explicitUnivs else [] + let suffix? := none -- We use `none` since the field can't be part of a composite name + LVal.fieldName comp comp.getId.getString! levels suffix? f elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc - let elabFieldIdx (e idxStx : Syntax) (explicit : Bool) := do + let elabFieldIdx (e idxStx : Syntax) (explicitUnivs : List Level) := do 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 + elabAppFn e (LVal.fieldIdx idxStx idx explicitUnivs :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc + let elabDottedIdent (id : Syntax) (explicitUnivs : List Level) : 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 - | `($(e).$field:ident) => elabFieldName e field explicit - | `($e |>.$field:ident) => elabFieldName e field explicit - | `(@$(e).$idx:fieldIdx) => elabFieldIdx e idx (explicit := true) - | `(@$(e).$field:ident) => elabFieldName e field (explicit := true) + | `($(e).$idx:fieldIdx) + | `($e |>.$idx:fieldIdx) => + elabFieldIdx e idx [] + | `($(e).$idx:fieldIdx.{$us,*}) + | `($e |>.$idx:fieldIdx.{$us,*}) => + let us ← elabExplicitUnivs us + elabFieldIdx e idx us + | `($(e).$field:ident) + | `($e |>.$field:ident) => + elabFieldName e field [] + | `($(e).$field:ident.{$us,*}) + | `($e |>.$field:ident.{$us,*}) => + let us ← elabExplicitUnivs us + elabFieldName e field us | `($_:ident@$_:term) => throwError m!"Expected a function, but found the named pattern{indentD f}" ++ .note m!"Named patterns `@` can only be used when pattern-matching" @@ -1942,12 +1959,15 @@ 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) => elabDottedIdent id [] explicit + | `(.$id:ident) => elabDottedIdent id [] | `(.$id:ident.{$us,*}) => let us ← elabExplicitUnivs us - elabDottedIdent id us explicit + elabDottedIdent id us | `(@$_:ident) | `(@$_:ident.{$_us,*}) + | `(@$(_).$_:fieldIdx) + | `(@$(_).$_:ident) + | `(@$(_).$_:ident.{$_us,*}) | `(@.$_:ident) | `(@.$_:ident.{$_us,*}) => elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc @@ -2084,10 +2104,10 @@ private def elabAtom : TermElab := fun stx expectedType? => do @[builtin_term_elab dotIdent] def elabDotIdent : TermElab := elabAtom @[builtin_term_elab explicitUniv] def elabExplicitUniv : TermElab := elabAtom @[builtin_term_elab pipeProj] def elabPipeProj : TermElab - | `($e |>.%$tk$f $args*), expectedType? => + | `($e |>.%$tk$f$[.{$us?,*}]? $args*), expectedType? => universeConstraintsCheckpoint do let (namedArgs, args, ellipsis) ← expandArgs args - let mut stx ← `($e |>.%$tk$f) + let mut stx ← `($e |>.%$tk$f$[.{$us?,*}]?) if let (some startPos, some stopPos) := (e.raw.getPos?, f.raw.getTailPos?) then stx := ⟨stx.raw.setInfo <| .synthetic (canonical := true) startPos stopPos⟩ elabAppAux stx namedArgs args (ellipsis := ellipsis) expectedType? @@ -2095,15 +2115,16 @@ 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? - | `(@.$_: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 + | `(@$_: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.{$_us,*}) => 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/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean index ba0c42f0bd..0ae20abd95 100644 --- a/src/Lean/Elab/Quotation/Precheck.lean +++ b/src/Lean/Elab/Quotation/Precheck.lean @@ -113,7 +113,7 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do if (← read).quotLCtx.contains val then return let rs ← try resolveName stx val [] [] catch _ => pure [] - for (e, _) in rs do + for (e, _, _) in rs do match e with | Expr.fvar _ .. => if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then diff --git a/src/Lean/Elab/Term/TermElabM.lean b/src/Lean/Elab/Term/TermElabM.lean index 555f15179b..94aa9998b2 100644 --- a/src/Lean/Elab/Term/TermElabM.lean +++ b/src/Lean/Elab/Term/TermElabM.lean @@ -627,13 +627,13 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl `[LVal.fieldName "foo", LVal.fieldIdx 1]`. -/ inductive LVal where - | fieldIdx (ref : Syntax) (i : Nat) + | fieldIdx (ref : Syntax) (i : Nat) (levels : List Level) /-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name. `ref` is the syntax object representing the field. `fullRef` includes the LHS. -/ - | fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax) + | fieldName (ref : Syntax) (name : String) (levels : List Level) (suffix? : Option Name) (fullRef : Syntax) def LVal.getRef : LVal → Syntax - | .fieldIdx ref _ => ref + | .fieldIdx ref .. => ref | .fieldName ref .. => ref def LVal.isFieldName : LVal → Bool @@ -642,8 +642,11 @@ def LVal.isFieldName : LVal → Bool instance : ToString LVal where toString - | .fieldIdx _ i => toString i - | .fieldName _ n .. => n + | .fieldIdx _ i levels .. => toString i ++ levelsToString levels + | .fieldName _ n levels .. => n ++ levelsToString levels +where + levelsToString levels := + if levels.isEmpty then "" else ".{" ++ String.intercalate "," (levels.map toString) ++ "}" /-- Return the name of the declaration being elaborated if available. -/ def getDeclName? : TermElabM (Option Name) := return (← read).declName? @@ -2111,8 +2114,10 @@ def checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit := do @[inline] def withoutCheckDeprecated [MonadWithReaderOf Context m] : m α → m α := withTheReader Context (fun ctx => { ctx with checkDeprecated := false }) -private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do +private def mkConsts (candidates : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String × List Level)) := do candidates.foldlM (init := []) fun result (declName, projs) => do + -- levels apply to the last projection, not the constant + let (constLevels, projLevels) := if projs.isEmpty then (explicitLevels, []) else ([], explicitLevels) -- TODO: better support for `mkConst` failure. We may want to cache the failures, and report them if all candidates fail. /- We disable `checkDeprecated` here because there may be many overloaded symbols. @@ -2121,25 +2126,38 @@ private def mkConsts (candidates : List (Name × List String)) (explicitLevels : At `elabAppFnId`, we perform the check when converting the list returned by `resolveName'` into a list of `TermElabResult`s. -/ - let const ← withoutCheckDeprecated <| mkConst declName explicitLevels - return (const, projs) :: result + let const ← withoutCheckDeprecated <| mkConst declName constLevels + return (const, projs, projLevels) :: 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 +/-- + Gives all resolutions of the name `n`. + +- `explicitLevels` provides a prefix of level parameters to the constant. For resolutions with a projection + component, the levels are not used, since they must apply to the last projection, not the constant. + In that case, the third component of the tuple is `explicitLevels`. +-/ +def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String × List Level)) := do addCompletionInfo <| CompletionInfo.id stx stx.getId (danglingDot := false) (← getLCtx) expectedType? + let processLocal (e : Expr) (projs : List String) := do + if projs.isEmpty then + if explicitLevels.isEmpty then + return [(e, [], [])] + else + throwInvalidExplicitUniversesForLocal e + else + return [(e, projs, explicitLevels)] if let some (e, projs) ← resolveLocalName n then - unless explicitLevels.isEmpty do - throwInvalidExplicitUniversesForLocal e - return [(e, projs)] + return ← processLocal e projs let preresolved := preresolved.filterMap fun | .decl n projs => some (n, projs) | _ => none -- check for section variable capture by a quotation let ctx ← read if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then - return [(e, projs)] -- section variables should shadow global decls + return ← processLocal e projs -- section variables should shadow global decls if preresolved.isEmpty then mkConsts (← realizeGlobalName n) explicitLevels else @@ -2148,14 +2166,17 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved /-- Similar to `resolveName`, but creates identifiers for the main part and each projection with position information derived from `ident`. Example: Assume resolveName `v.head.bla.boo` produces `(v.head, ["bla", "boo"])`, then this method produces - `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. -/ -def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax)) := do + `(v.head, id, [f₁, f₂])` where `id` is an identifier for `v.head`, and `f₁` and `f₂` are identifiers for fields `"bla"` and `"boo"`. + + See the comment there about `explicitLevels` and the meaning of the `List Level` component of the returned tuple. +-/ +def resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (Name × List (Expr × Syntax × List Syntax × List Level)) := do let .ident _ _ n preresolved := ident | throwError "identifier expected" let r ← resolveName ident n preresolved explicitLevels expectedType? - let rc ← r.mapM fun (c, fields) => do + let rc ← r.mapM fun (c, fields, levels) => do let ids := ident.identComponents (nFields? := fields.length) - return (c, ids.head!, ids.tail!) + return (c, ids.head!, ids.tail!, levels) return (n, rc) @@ -2163,7 +2184,7 @@ def resolveId? (stx : Syntax) (kind := "term") (withInfo := false) : TermElabM ( match stx with | .ident _ _ val preresolved => let rs ← try resolveName stx val preresolved [] catch _ => pure [] - let rs := rs.filter fun ⟨_, projs⟩ => projs.isEmpty + let rs := rs.filter fun ⟨_, projs, _⟩ => projs.isEmpty let fs := rs.map fun (f, _) => f match fs with | [] => return none diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index 5b38ff62d8..46fc939638 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -1115,11 +1115,6 @@ def symbolNoAntiquot (sym : String) : Parser := { info := symbolInfo sym fn := symbolFn sym } -def checkTailNoWs (prev : Syntax) : Bool := - match prev.getTailInfo with - | .original _ _ trailing _ => trailing.stopPos == trailing.startPos - | _ => false - /-- Check if the following token is the symbol _or_ identifier `sym`. Useful for parsing local tokens that have not been added to the token table (but may have been so by some unrelated code). @@ -1168,13 +1163,18 @@ partial def strAux (sym : String) (errorMsg : String) (j : String.Pos.Raw) :Pars else parse (j.next' sym h₁) c (s.next' c i h₂) parse j +private def pickNonNone (stack : SyntaxStack) : Syntax := + match stack.toSubarray.findRev? fun stx => !stx.isNone with + | none => Syntax.missing + | some stx => stx + def checkTailWs (prev : Syntax) : Bool := match prev.getTailInfo with | .original _ _ trailing _ => trailing.stopPos > trailing.startPos | _ => false def checkWsBeforeFn (errorMsg : String) : ParserFn := fun _ s => - let prev := s.stxStack.back + let prev := pickNonNone s.stxStack if checkTailWs prev then s else s.mkError errorMsg /-- The `ws` parser requires that there is some whitespace at this location. @@ -1202,10 +1202,10 @@ This parser has arity 0 - it does not capture anything. -/ info := epsilonInfo fn := checkLinebreakBeforeFn errorMsg -private def pickNonNone (stack : SyntaxStack) : Syntax := - match stack.toSubarray.findRev? fun stx => !stx.isNone with - | none => Syntax.missing - | some stx => stx +def checkTailNoWs (prev : Syntax) : Bool := + match prev.getTailInfo with + | .original _ _ trailing _ => trailing.stopPos == trailing.startPos + | _ => false def checkNoWsBeforeFn (errorMsg : String) : ParserFn := fun _ s => let prev := pickNonNone s.stxStack diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index afeef0920f..2a830ef3a5 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -122,7 +122,9 @@ def declModifiers (inline : Bool) := leading_parser /-- `declId` matches `foo` or `foo.{u,v}`: an identifier possibly followed by a list of universe names -/ -- @[builtin_doc] -- FIXME: suppress the hover def declId := leading_parser - ident >> optional (".{" >> sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}") + ident >> + optional (checkNoWsBefore "no space before '.{'" >> ".{" >> + sepBy1 (recover ident (skipUntil (fun c => c.isWhitespace || c ∈ [',', '}']))) ", " >> "}") /-- `declSig` matches the signature of a declaration with required type: a list of binders and then `: type` -/ -- @[builtin_doc] -- FIXME: suppress the hover def declSig := leading_parser diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 9e4abd0ed1..a1905ae4e0 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -889,14 +889,21 @@ 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 +/-- Predicate for what `explicitUniv` can follow. It is only meant to be used on an identifier +that becomes the head constant of an application. -/ +def isIdentOrDotIdentOrProj (stx : Syntax) : Bool := + isIdent stx || stx.isOfKind ``dotIdent || stx.isOfKind ``proj -/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/ -@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser - checkStackTop isIdentOrDotIdent "expected preceding identifier" >> +/-- Syntax for `.{u, ...}` itself. Generally the `explicitUniv` trailing parser suffices. +However, for `e |>.x.{u} a1 a2 a3` notation we need to be able to express explicit universes in the +middle of the syntax. -/ +def explicitUnivSuffix : Parser := checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}" +/-- `x.{u, ...}` explicitly specifies the universes `u, ...` of the constant `x`. -/ +@[builtin_term_parser] def explicitUniv : TrailingParser := trailing_parser + checkStackTop isIdentOrDotIdentOrProj "expected preceding identifier" >> + explicitUnivSuffix /-- `x@e` or `x@h:e` matches the pattern `e` and binds its value to the identifier `x`. If present, the identifier `h` is bound to a proof of `x = e`. -/ @[builtin_term_parser] def namedPattern : TrailingParser := trailing_parser @@ -909,7 +916,7 @@ If present, the identifier `h` is bound to a proof of `x = e`. -/ It is especially useful for avoiding parentheses with repeated applications. -/ @[builtin_term_parser] def pipeProj := trailing_parser:minPrec - " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument + " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> optional explicitUnivSuffix >> many argument @[builtin_term_parser] def pipeCompletion := trailing_parser:minPrec " |>." diff --git a/tests/elab/8743.lean b/tests/elab/8743.lean new file mode 100644 index 0000000000..8066feaf4c --- /dev/null +++ b/tests/elab/8743.lean @@ -0,0 +1,195 @@ +/-! +# Generalized field notation allows explicit universes + +https://github.com/leanprover/lean4/issues/8743 +-/ + +set_option warn.sorry false +set_option pp.universes true +set_option pp.mvars.anonymous false + +/-! +Kenny Lau's example. This used to give "invalid use of explicit universe parameters, 'x' is a local variable" +since generalized field notation was improperly attributing the explicit universe to `x` itself, not the projection. +-/ +section +def Foo : Type u := sorry +def Foo.inv.{v,u} : Foo.{u} → Foo.{v} := sorry + +variable (x : Foo.{u}) +/-- info: Foo.inv.{2, u} x : Foo.{2} -/ +#guard_msgs in #check Foo.inv.{2} x +/-- info: Foo.inv.{2, u} x : Foo.{2} -/ +#guard_msgs in #check x.inv.{2} +/-- info: Foo.inv.{u, u} x : Foo.{u} -/ +#guard_msgs in #check x.inv.{u} +/-- info: Foo.inv.{2, u} x : Foo.{2} -/ +#guard_msgs in #check Foo.inv.{2,u} x +/-- info: Foo.inv.{2, u} x : Foo.{2} -/ +#guard_msgs in #check x.inv.{2,u} +/-- +error: Application type mismatch: The argument + x +has type + Foo.{u} +of sort `Type u` but is expected to have type + Foo.{2} +of sort `Type 2` in the application + Foo.inv.{u, 2} x +--- +info: Foo.inv.{u, 2} sorry : Foo.{u} +-/ +#guard_msgs in #check x.inv.{u,2} + +/-! +That example was an explicit universe applied to the identifier syntax `x.inv`. +New feature: it's possible to apply dot notation to expressions too: +-/ +/-- info: Foo.inv.{u, u} x : Foo.{u} -/ +#guard_msgs in #check (x).inv.{u} +/-- info: Foo.inv.{2, u} x : Foo.{2} -/ +#guard_msgs in #check (x).inv.{2} + +/-! +New feature: it's possible to chain field notations. +-/ +/-- info: Foo.inv.{4, 3} (Foo.inv.{3, u} x) : Foo.{4} -/ +#guard_msgs in #check Foo.inv.{4} (Foo.inv.{3} x) +/-- info: Foo.inv.{4, 3} (Foo.inv.{3, u} x) : Foo.{4} -/ +#guard_msgs in #check x.inv.{3}.inv.{4} +/-- info: Foo.inv.{4, u_1} (Foo.inv.{u_1, u} x) : Foo.{4} -/ +#guard_msgs in #check x.inv.inv.{4} +/-- info: Foo.inv.{u_1, 3} (Foo.inv.{3, u} x) : Foo.{u_1} -/ +#guard_msgs in #check x.inv.{3}.inv +/-- info: Foo.inv.{4, 3} (Foo.inv.{3, u} x) : Foo.{4} -/ +#guard_msgs in #check (x).inv.{3}.inv.{4} +/-- info: Foo.inv.{4, u_1} (Foo.inv.{u_1, u} x) : Foo.{4} -/ +#guard_msgs in #check (x).inv.inv.{4} +/-- info: Foo.inv.{u_1, 3} (Foo.inv.{3, u} x) : Foo.{u_1} -/ +#guard_msgs in #check (x).inv.{3}.inv + +end + + +/-! +Eric Wieser's example from the issue. +-/ +abbrev Nat.ulift.{u} (n : Nat) : ULift.{u} Nat := ULift.up.{u} n + +/-- info: Nat.ulift.{5} 1 : ULift.{5, 0} Nat -/ +#guard_msgs in #check Nat.ulift.{5} (1 : Nat) +/-- info: Nat.ulift.{5} 1 : ULift.{5, 0} Nat -/ +#guard_msgs in #check (1 : Nat).ulift.{5} + + +/-! +Mario Carneiro's example from the issue +-/ +/-- info: Nat.ulift.{5} 1 : ULift.{5, 0} Nat -/ +#guard_msgs in #check (1 : Nat) |>.ulift.{5} +/-- info: Nat.ulift.{u_1} 1 : ULift.{u_1, 0} Nat -/ +#guard_msgs in #check (1 : Nat) |>.ulift + +/-! +Check that `|>.` notation supports arguments, with and without universes. +-/ +section +def Foo.add.{u} : Foo.{u} → Nat → Foo.{u} := sorry + +variable (x : Foo.{3}) +/-- info: Foo.add.{3} x 2 : Foo.{3} -/ +#guard_msgs in #check x |>.add.{3} 2 +/-- info: Foo.add.{3} x 2 : Foo.{3} -/ +#guard_msgs in #check x |>.add 2 +/-- +error: Application type mismatch: The argument + x +has type + Foo.{3} +of sort `Type 3` but is expected to have type + Foo.{4} +of sort `Type 4` in the application + Foo.add.{4} x +--- +info: Foo.add.{4} sorry 2 : Foo.{4} +-/ +#guard_msgs in #check x |>.add.{4} 2 +/-- info: Foo.add.{3} x : Nat → Foo.{3} -/ +#guard_msgs in #check x |>.add +/-- info: Foo.add.{3} x : Nat → Foo.{3} -/ +#guard_msgs in #check x |>.add.{3} +/-- info: Foo.add.{3} (Foo.add.{3} x 2) : Nat → Foo.{3} -/ +#guard_msgs in #check x |>.add.{3} 2 |>.add.{3} + +end + +/-! +Named structure projections allow explicit universes. +These have a different code path from generalized field notation. +-/ +/-- info: fun p => Prod.fst.{u_1, u_2} p : Prod.{u_1, u_2} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p.fst +/-- info: fun p => Prod.fst.{u_1, u_2} p : Prod.{u_1, u_2} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p |>.fst +/-- info: fun p => Prod.fst.{1, u_1} p : Prod.{1, u_1} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p.fst.{1} +/-- info: fun p => Prod.fst.{1, u_1} p : Prod.{1, u_1} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p |>.fst.{1} +/-- info: fun p => Prod.fst.{1, 2} p : Prod.{1, 2} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p.fst.{1,2} +/-- info: fun p => Prod.fst.{1, 2} p : Prod.{1, 2} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p |>.fst.{1,2} + +/-! +Indexed projections allow explicit universes for `structure`s. +-/ +/-- info: fun p => Prod.fst.{1, u_1} p : Prod.{1, u_1} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p.1.{1} +/-- info: fun p => Prod.fst.{1, u_1} p : Prod.{1, u_1} ?_ ?_ → ?_ -/ +#guard_msgs in #check fun (p : _ × _) => p |>.1.{1} + +/-! +Indexed projections don't allow explicit universes for structures not defined using `inductive`. +-/ +inductive IPair (α : Type u) where + | mk (x y : α) +/-- info: fun p => p.1 : IPair.{u_1} ?_ → ?_ -/ +#guard_msgs in #check fun (p : IPair _) => p.1 +/-- +error: Invalid projection: Explicit universe levels are only supported for inductive types defined using the `structure` command. The expression + p +has type `IPair.{_} ?_` which is not a `structure`. +--- +info: fun p => sorry : (p : IPair.{u_1} ?_) → ?_ p +-/ +#guard_msgs in #check fun (p : IPair _) => p.1.{0} + +/-! +Inherited structure projections can be counterintuitive, since the universe levels apply to the +projection function *after* the base projection. +-/ +section +structure S1 (α : Type u) where + x : α +structure S2.{v,u} (α : Type u) (β : Type v) extends S1 α + +variable (s : S2.{5,6} PUnit PUnit) +/-- info: S1.x.{6} (S2.toS1.{5, 6} s) : PUnit.{7} -/ +#guard_msgs in #check s.x +-- Surprisingly, even though it's `S2.{5,6}`, `s.x.{5}` doesn't work ... +/-- +error: Application type mismatch: The argument + S2.toS1.{5, 6} s +has type + S1.{6} PUnit.{7} +of sort `Type 6` but is expected to have type + S1.{5} ?_ +of sort `Type 5` in the application + S1.x.{5} (S2.toS1.{5, 6} s) +-/ +#guard_msgs in #check s.x.{5} +-- ... but `s.x.{6}` does +/-- info: S1.x.{6} (S2.toS1.{5, 6} s) : PUnit.{7} -/ +#guard_msgs in #check s.x.{6} + +end