max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: improve universe level contraint checks in inductive datatype constructors

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-03 09:18:38 -07:00
parent 3ee8ceafb4
commit 61ae72330f
3 changed files with 86 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

49
src/Lean/Elab/Inductive.lean
View file

@ -403,26 +403,45 @@ def withCtorRef (views : Array InductiveView) (ctorName : Name) (k : TermElabM
k
private def checkResultingUniverses (views : Array InductiveView) (numParams : Nat) (indTypes : List InductiveType) : TermElabM Unit := do
let u ← instantiateLevelMVars (← getResultingUniverse indTypes)
let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize
checkResultingUniverse u
unless u.isZero do
indTypes.forM fun indType => indType.ctors.forM fun ctor =>
forallTelescopeReducing ctor.type fun ctorArgs type =>
forallTelescopeReducing ctor.type fun ctorArgs type => do
for ctorArg in ctorArgs[numParams:] do
let type ← inferType ctorArg
let v ← instantiateLevelMVars (← getLevel type)
if v.hasMVar then
-- TODO
trace[Meta.debug] "checkCtorArgLevel, {v} <= {u}"
else unless u.geq v do
let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"
let localDecl ← getFVarLocalDecl ctorArg
unless localDecl.userName.hasMacroScopes do
msg := msg ++ m!" '{ctorArg}'"
msg := msg ++ m!" has type{indentExpr type}"
msg := msg ++ m!"\nat universe level{indentD v}"
msg := msg ++ m!"\nit must be smaller than or equal to the inductive datatype universe level{indentD u}"
withCtorRef views ctor.name <| throwError msg
let v := (← instantiateLevelMVars (← getLevel type)).normalize
let rec check (v' : Level) (u' : Level) : TermElabM Unit :=
match v', u' with
| .succ v' _, .succ u' _ => check v' u'
| .mvar id _, .param .. =>
/- Special case:
The constructor parameter `v` is at unverse level `?v+k` and
the resulting inductive universe level is `u'+k`, where `u'` is a parameter (or zero).
Thus, `?v := u'` is the only choice for satisfying the universe contraint `?v+k <= u'+k`.
Note that, we still generate an error for cases where there is more than one of satisfying the constraint.
Examples:
-----------------------------------------------------------
| ctor universe level | inductive datatype universe level |
-----------------------------------------------------------
| ?v | max u w |
-----------------------------------------------------------
| ?v | u + 1 |
-----------------------------------------------------------
-/
assignLevelMVar id u'
| .mvar id _, .zero _ => assignLevelMVar id u' -- TODO: merge with previous case
| _, _ =>
unless u.geq v do
let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"
let localDecl ← getFVarLocalDecl ctorArg
unless localDecl.userName.hasMacroScopes do
msg := msg ++ m!" '{ctorArg}'"
msg := msg ++ m!" has type{indentExpr type}"
msg := msg ++ m!"\nat universe level{indentD v}"
msg := msg ++ m!"\nit must be smaller than or equal to the inductive datatype universe level{indentD u}"
withCtorRef views ctor.name <| throwError msg
check v u
private def collectUsed (indTypes : List InductiveType) : StateRefT CollectFVars.State MetaM Unit := do
indTypes.forM fun indType => do

36
tests/lean/ctorUnivTooBig.lean
View file

@ -1,17 +1,47 @@
inductive Bla : Type u where
| nil : Bla
| cons : (α : Type u) → (a : α) → Bla → Bla
| cons : (α : Type u) → (a : α) → Bla → Bla -- Error
inductive Foo : Type where
| leaf
| mk (α : Type) (a : α)
| mk (α : Type) (a : α) -- Error
| mk₂
inductive Foo' : Type u where
| leaf
| mk : Sort (max u v) → a → Foo'
| mk : Sort (max u v) → a → Foo' -- Error
| mk₂
inductive Boo : Type u where
| nil : Boo
| cons : (α : Sort u) → (a : α) → Boo → Boo
namespace Ex1
inductive Member : α → List α → Type u
| head : Member a (a::as)
| tail : Member a bs → Member a (b::bs)
end Ex1
namespace Ex2
inductive Member : α → List α → Type
| head : Member a (a::as)
| tail : Member a bs → Member a (b::bs)
end Ex2
namespace Ex3
inductive Member : α → List α → Type (max u v)
| head : Member a (a::as) -- Error
| tail : Member a bs → Member a (b::bs)
end Ex3
namespace Ex4
inductive Member : α → List α → Type (u+1)
| head : Member a (a::as) -- Error
| tail : Member a bs → Member a (b::bs)
end Ex4
namespace Ex5
inductive Member : α → List α → Type 1
| head : Member a (a::as) -- Error
| tail : Member a bs → Member a (b::bs)
end Ex5

20
tests/lean/ctorUnivTooBig.lean.expected.out
View file

@ -13,6 +13,24 @@ it must be smaller than or equal to the inductive datatype universe level
ctorUnivTooBig.lean:12:2-12:34: error: invalid universe level in constructor 'Foo'.mk', parameter has type
Sort (max u v)
at universe level
(max u v)+1
max (u+1) (v+1)
it must be smaller than or equal to the inductive datatype universe level
u+1
ctorUnivTooBig.lean:33:2-33:27: error: invalid universe level in constructor 'Ex3.Member.head', parameter 'a' has type
x✝
at universe level
?u+1
it must be smaller than or equal to the inductive datatype universe level
max (u+1) (v+1)
ctorUnivTooBig.lean:39:2-39:27: error: invalid universe level in constructor 'Ex4.Member.head', parameter 'a' has type
x✝
at universe level
?u+1
it must be smaller than or equal to the inductive datatype universe level
u+2
ctorUnivTooBig.lean:45:2-45:27: error: invalid universe level in constructor 'Ex5.Member.head', parameter 'a' has type
x✝
at universe level
?u+1
it must be smaller than or equal to the inductive datatype universe level
2