From a00cf6330f78cdc793fa8f75e72a5bbc96c4b149 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 19 Nov 2024 13:27:00 -0800 Subject: [PATCH] fix: add a missing case to `Level.geq` (#2689) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds a case to `Level.geq` that is present in the kernel's level `is_geq` procedure, making them consistent with one another. This came up during testing of `lean4lean`. Currently `Level.geq` differs from `level::is_geq` in the case of `max u v >= imax u v`. The elaborator function is overly pessimistic and yields `false` on this while the kernel function yields true. This comes up concretely in the `Trans` class: ```lean class Trans (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) where trans : r a b → s b c → t a c ``` The type of this class is `Sort (max (max (max (max (max (max 1 u) u_1) u_2) u_3) v) w)` (where `u_1 u_2 u_3` are the levels of `α β γ`), but if you try writing that type explicitly then the `class` command fails. Omitting the type leaves the `class` to infer the universe level (the command assumes the level is correct, and the kernel agrees it is), but including the type then the elaborator checks the level inequality with `Level.geq` and fails. --------- Co-authored-by: Kyle Miller --- src/Lean/Level.lean | 23 +++++++++++++---------- tests/lean/run/2689.lean | 36 ++++++++++++++++++++++++++++++++++++ tests/lean/run/level.lean | 1 + 3 files changed, 50 insertions(+), 10 deletions(-) create mode 100644 tests/lean/run/2689.lean diff --git a/src/Lean/Level.lean b/src/Lean/Level.lean index b27cb5249c..dd3be8a93b 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -599,17 +599,20 @@ def geq (u v : Level) : Bool := where go (u v : Level) : Bool := u == v || + let k := fun () => + match v with + | imax v₁ v₂ => go u v₁ && go u v₂ + | _ => + let v' := v.getLevelOffset + (u.getLevelOffset == v' || v'.isZero) + && u.getOffset ≥ v.getOffset match u, v with - | _, zero => true - | u, max v₁ v₂ => go u v₁ && go u v₂ - | max u₁ u₂, v => go u₁ v || go u₂ v - | u, imax v₁ v₂ => go u v₁ && go u v₂ - | imax _ u₂, v => go u₂ v - | succ u, succ v => go u v - | _, _ => - let v' := v.getLevelOffset - (u.getLevelOffset == v' || v'.isZero) - && u.getOffset ≥ v.getOffset + | _, zero => true + | u, max v₁ v₂ => go u v₁ && go u v₂ + | max u₁ u₂, v => go u₁ v || go u₂ v || k () + | imax _ u₂, v => go u₂ v + | succ u, succ v => go u v + | _, _ => k () termination_by (u, v) end Level diff --git a/tests/lean/run/2689.lean b/tests/lean/run/2689.lean new file mode 100644 index 0000000000..12a2775c56 --- /dev/null +++ b/tests/lean/run/2689.lean @@ -0,0 +1,36 @@ +/-! +# Tests of universe constraints for inductive types + +https://github.com/leanprover/lean4/pull/2689 corrected the elaborator's `Level.geq`, +which was missing cases that the kernel `is_geq` could handle. +-/ + +/-! +This always worked. The universe level of `Trans₁` is inferred from the fields. +-/ +structure Trans₁ {α : Sort a} {β : Sort b} {γ : Sort c} + (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) where + trans : r a b → s b c → t a c + +/-! +Regression test: This was failing. An explicit universe invokes `Level.geq`. +-/ +structure Trans₂ {α : Sort a} {β : Sort b} {γ : Sort c} + (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) : + Sort (max 1 a b c u v w) where + trans : r a b → s b c → t a c + +/-! +Regression test: This was failing. An explicit universe invokes `Level.geq`. +-/ +inductive Trans₃ {α : Sort a} {β : Sort b} {γ : Sort c} + (r : α → β → Sort u) (s : β → γ → Sort v) (t : outParam (α → γ → Sort w)) : + Sort (max 1 a b c u v w) where + | mk : (∀ a b c, r a b → s b c → t a c) → Trans₃ r s t + +/-! +Regression test: This was failing due to the included `Type (max u v)` +even though this is the inferred universe. +-/ +inductive I (α : Type u) (Hom : α → α → Sort v) : Type (max u v) where + | mk (id : ∀ X : α, Hom X X) diff --git a/tests/lean/run/level.lean b/tests/lean/run/level.lean index ecf7d3b263..fe9d340edc 100644 --- a/tests/lean/run/level.lean +++ b/tests/lean/run/level.lean @@ -6,3 +6,4 @@ open Lean #guard levelZero != mkLevelSucc levelZero #guard mkLevelMax (mkLevelSucc levelZero) levelZero != mkLevelSucc levelZero #guard mkLevelMax (mkLevelSucc levelZero) levelZero == mkLevelMax (mkLevelSucc levelZero) levelZero +#guard Level.geq (.max (.param `u) (.param `v)) (.imax (.param `u) (.param `v))