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
This commit is contained in:
Kyle Miller
GitHub
parent
82bb27fd7d
commit
c60f97a3fa
7 changed files with 337 additions and 91 deletions
|
|
@ -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 `<identifier>@<term>` 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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
" |>."
|
||||
|
||||
|
|
|
|||
195
tests/elab/8743.lean
Normal file
195
tests/elab/8743.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue