From c06d8191d35836230717df093950238bb1a4690f Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 27 Dec 2025 12:34:31 -0500 Subject: [PATCH 1/6] Add a 'highInferredUniverse' error explanation. --- Manual/ErrorExplanations.lean | 3 + .../HighInferredUniverse.lean | 128 ++++++++++++++++++ Manual/Types.lean | 3 + 3 files changed, 134 insertions(+) create mode 100644 Manual/ErrorExplanations/HighInferredUniverse.lean diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean index 7ecf948d2..97d740e0b 100644 --- a/Manual/ErrorExplanations.lean +++ b/Manual/ErrorExplanations.lean @@ -7,6 +7,7 @@ Author: Joseph Rotella, Rob Simmons import Manual.Meta.ErrorExplanation import Manual.ErrorExplanations.CtorResultingTypeMismatch import Manual.ErrorExplanations.DependsOnNoncomputable +import Manual.ErrorExplanations.HighInferredUniverse import Manual.ErrorExplanations.InductionWithNoAlts import Manual.ErrorExplanations.InductiveParamMismatch import Manual.ErrorExplanations.InductiveParamMissing @@ -85,6 +86,8 @@ by Lean when processing a source file. All error names listed below have the {include 0 Manual.ErrorExplanations.InductionWithNoAlts} +{include 0 Manual.ErrorExplanations.HighInferredUniverse} + {include 0 Manual.ErrorExplanations.InductiveParamMismatch} {include 0 Manual.ErrorExplanations.InductiveParamMissing} diff --git a/Manual/ErrorExplanations/HighInferredUniverse.lean b/Manual/ErrorExplanations/HighInferredUniverse.lean new file mode 100644 index 000000000..d562a2f08 --- /dev/null +++ b/Manual/ErrorExplanations/HighInferredUniverse.lean @@ -0,0 +1,128 @@ +/- +Copyright (c) 2025 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Rob Simmons, Kyle Miller +-/ + +import VersoManual +import Manual.Meta.ErrorExplanation + +open Lean +open Verso.Genre Manual InlineLean + +#doc (Manual) "About: `highInferredUniverse`" => +%%% +shortTitle := "highInferredUniverse" +%%% + +{errorExplanationHeader lean.highInferredUniverse} + +This error message appears when Lean's elaboration algorithm is about to assign a new type to a +higher universe than may be necessary. + +::::paragraph +Constructor argument universe levels must be no greater than the resulting universe level, so given +this definition: +:::keepEnv +```lean +inductive MaybeTwo (α : Type u) + | none + | some (fst snd : α) +``` +```lean -show +variable (α : Type u) +``` +Lean must classify {lean}`MaybeTwo α` as a {lean}`Type u`, or, equivalently, as a +{lean}`Sort (u + 1)`. (See the reference guide to {ref "universes-sorts"}[Universes] for more +details on the relationship between {lean}`Prop`, {lean}`Sort`, and {lean}`Type`.) +::: +:::: + +Lean chooses to avoid silently assigning a new type to a universe that might cause confusion later. +This error often indicates that the universe annotations need to be in a slightly different form, +or that more specific annotations are required. + +# Examples +:::errorExample "Use of `Type` May Force Universe Too High" +```broken +structure MyPair (α β : Sort u) : Type _ where + (a : α) + (b : β) +``` + +```output +Resulting type is of the form + Type ?u.6 +but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using + Sort (max 1 u) +if the resulting universe level should be at the above universe level or higher. + +Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u.6+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): + u ≤ ?u.6+1 +However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. +``` + +```fixed "remove annotation" +structure MyPair (α β : Sort u) where + (a : α) + (b : β) +``` + +```fixed "accept suggestion" +structure MyPair (α β : Sort u) : Sort (max 1 u) where + (a : α) + (b : β) +``` + +```fixed "restrict arguments" +structure MyPair (α β : Type u) : Type _ where + (a : α) + (b : β) +``` + +```fixed "make large type explicit" +structure MyPair (α β : Sort u) : Type u where + (a : α) + (b : β) +``` + +```lean -show +variable (α : Type u) +``` + +The initial type annotation {lean}`Type _` forces `MyPair` into a universe that looks like +{lean}`Sort (_ + 1)`, but the best universe for `MyPair` is {lean}`Sort (max u 1)`. (See the section +on {ref "prop-vs-type"}[Prop vs Type] for why it is {lean}`Sort (max u 1)` and not just +{lean}`Sort u`.) + +The first three fixes are all equivalent, and allow `MyPair` to have any non-zero universe that +is larger than `u`. The last two fixes make `MyPair` less general, but also silence the error. +::: + +:::errorExample "Inductive Definition Needs Sort Annotations" +```broken +inductive Bar +| foobar {Foo} : Foo → Bar +| barbar : Option Bar → Bar +``` +```output +Resulting type is of the form + Type ?u.16 +but the universes of constructor arguments suggest that this could accidentally be a higher universe than necessary. Explicitly providing a resulting type will silence this error. Universe inference suggests using + Type u_1 +if the resulting universe level should be at the above universe level or higher. + +Explanation: At this point in elaboration, universe level unification has committed to using a resulting universe level of the form `?u.16+1`. Constructor argument universe levels must be no greater than the resulting universe level, and this condition implies the following constraint(s): + u_1 ≤ ?u.16+1 +However, such constraint(s) usually indicate that the resulting universe level should have been in a different form. For example, if the resulting type is of the form `Sort (_ + 1)` and a constructor argument is in universe `Sort u`, then universe inference would yield `Sort (u + 1)`, but the resulting type `Sort (max 1 u)` would avoid being in a higher universe than necessary. +``` +```fixed +inductive Bar : Type u +| foobar {Foo : Sort u} : Foo → Bar +| barbar : Option Bar → Bar +``` + +In this case, the error message is a false positive, but the issue can be easily fixed with +clarifying annotations. After annotating Foo with a universe `u`, the overall type can be assigned +type that the error message suggests, which silences the error. +::: diff --git a/Manual/Types.lean b/Manual/Types.lean index 1c1b49ccb..011fb1992 100644 --- a/Manual/Types.lean +++ b/Manual/Types.lean @@ -170,6 +170,9 @@ Propositions have the following properties: {docstring propext} # Universes +%%% +tag := "universes-sorts" +%%% Types are classified by {deftech}_universes_. {index}[universe]{margin}[Universes are also referred to as {deftech}_sorts_.] Each universe has a {deftech (key:="universe level")}_level_, {index (subterm := "of universe")}[level] which is a natural number. From e6c08a4238421745fcb04643da467f6841a127fd Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 27 Dec 2025 12:38:16 -0500 Subject: [PATCH 2/6] Reorder --- Manual/ErrorExplanations.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean index 97d740e0b..b71be1ad3 100644 --- a/Manual/ErrorExplanations.lean +++ b/Manual/ErrorExplanations.lean @@ -84,10 +84,10 @@ by Lean when processing a source file. All error names listed below have the {include 0 Manual.ErrorExplanations.DependsOnNoncomputable} -{include 0 Manual.ErrorExplanations.InductionWithNoAlts} - {include 0 Manual.ErrorExplanations.HighInferredUniverse} +{include 0 Manual.ErrorExplanations.InductionWithNoAlts} + {include 0 Manual.ErrorExplanations.InductiveParamMismatch} {include 0 Manual.ErrorExplanations.InductiveParamMissing} From f9528407c6ef80230f19f34882c67e99a9afde2f Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 27 Dec 2025 12:39:38 -0500 Subject: [PATCH 3/6] correct number --- Manual/ErrorExplanations/HighInferredUniverse.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Manual/ErrorExplanations/HighInferredUniverse.lean b/Manual/ErrorExplanations/HighInferredUniverse.lean index d562a2f08..04708aef0 100644 --- a/Manual/ErrorExplanations/HighInferredUniverse.lean +++ b/Manual/ErrorExplanations/HighInferredUniverse.lean @@ -95,7 +95,7 @@ The initial type annotation {lean}`Type _` forces `MyPair` into a universe that on {ref "prop-vs-type"}[Prop vs Type] for why it is {lean}`Sort (max u 1)` and not just {lean}`Sort u`.) -The first three fixes are all equivalent, and allow `MyPair` to have any non-zero universe that +The first two fixes are all equivalent, and allow `MyPair` to have any non-zero universe that is larger than `u`. The last two fixes make `MyPair` less general, but also silence the error. ::: From b1731cc72d60c2f9c8d8110cc477b3ad8e6dd156 Mon Sep 17 00:00:00 2001 From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com> Date: Sun, 11 Jan 2026 18:54:48 -0500 Subject: [PATCH 4/6] Update Manual/ErrorExplanations/HighInferredUniverse.lean Co-authored-by: Kyle Miller --- Manual/ErrorExplanations/HighInferredUniverse.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Manual/ErrorExplanations/HighInferredUniverse.lean b/Manual/ErrorExplanations/HighInferredUniverse.lean index 04708aef0..3c44bedda 100644 --- a/Manual/ErrorExplanations/HighInferredUniverse.lean +++ b/Manual/ErrorExplanations/HighInferredUniverse.lean @@ -32,7 +32,8 @@ inductive MaybeTwo (α : Type u) ```lean -show variable (α : Type u) ``` -Lean must classify {lean}`MaybeTwo α` as a {lean}`Type u`, or, equivalently, as a +then the universe for {lean}`MaybeTwo α` must be {lean}`Type u` or higher. +Lean automatically infers the universe to be the least universe, hence it chooses {lean}`Type u`, or, equivalently, {lean}`Sort (u + 1)`. (See the reference guide to {ref "universes-sorts"}[Universes] for more details on the relationship between {lean}`Prop`, {lean}`Sort`, and {lean}`Type`.) ::: From 401f221d9279ed35592b5e5e8e2d19c81c14d9e7 Mon Sep 17 00:00:00 2001 From: "Robert J. Simmons" <442315+robsimmons@users.noreply.github.com> Date: Sun, 11 Jan 2026 18:55:45 -0500 Subject: [PATCH 5/6] Update Manual/ErrorExplanations/HighInferredUniverse.lean Co-authored-by: Kyle Miller --- Manual/ErrorExplanations/HighInferredUniverse.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Manual/ErrorExplanations/HighInferredUniverse.lean b/Manual/ErrorExplanations/HighInferredUniverse.lean index 3c44bedda..640478fa0 100644 --- a/Manual/ErrorExplanations/HighInferredUniverse.lean +++ b/Manual/ErrorExplanations/HighInferredUniverse.lean @@ -39,9 +39,13 @@ details on the relationship between {lean}`Prop`, {lean}`Sort`, and {lean}`Type` ::: :::: -Lean chooses to avoid silently assigning a new type to a universe that might cause confusion later. -This error often indicates that the universe annotations need to be in a slightly different form, -or that more specific annotations are required. +There are certain situations where universe inference yields +a universe level that may be higher than it could be. +In these situations, Lean chooses to avoid silently accepting +this unnecessarily high universe level, which might cause hard-to-diagnose errors later. +Avoiding these situations requires an explicitly provided universe for the inductive type +using a universe level in a slightly different form; +this cannot be corrected by the elaborator on its own and requires user intervention. # Examples :::errorExample "Use of `Type` May Force Universe Too High" From 3b93aa9e317d75129e2be522914ba093cca0eb2e Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sun, 11 Jan 2026 18:57:38 -0500 Subject: [PATCH 6/6] Additional revisions --- .../ErrorExplanations/HighInferredUniverse.lean | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/Manual/ErrorExplanations/HighInferredUniverse.lean b/Manual/ErrorExplanations/HighInferredUniverse.lean index 640478fa0..786f5d340 100644 --- a/Manual/ErrorExplanations/HighInferredUniverse.lean +++ b/Manual/ErrorExplanations/HighInferredUniverse.lean @@ -39,13 +39,14 @@ details on the relationship between {lean}`Prop`, {lean}`Sort`, and {lean}`Type` ::: :::: -There are certain situations where universe inference yields -a universe level that may be higher than it could be. -In these situations, Lean chooses to avoid silently accepting -this unnecessarily high universe level, which might cause hard-to-diagnose errors later. -Avoiding these situations requires an explicitly provided universe for the inductive type -using a universe level in a slightly different form; -this cannot be corrected by the elaborator on its own and requires user intervention. +There are certain situations where universe inference yields a universe level that may be higher +than it could be. +In these situations, Lean chooses to avoid silently accepting this unnecessarily high universe +level, because unnecessarily high universe levels can cause hard-to-diagnose errors in later +definitions. +Avoiding these situations requires an explicitly provided universe for the inductive type using a +universe level in a slightly different form. +This can't currently be done automatically, so fixing it requires user intervention. # Examples :::errorExample "Use of `Type` May Force Universe Too High"