The Lean Language Reference

About: highInferredUniverse

Error code: lean.highInferredUniverse

Summary unavailable

Severity: ErrorSince: Metadata unavailable

This error message appears when Lean's elaboration algorithm is about to assign a new type to a higher universe than may be necessary.

Constructor argument universe levels must be no greater than the resulting universe level, so given this definition:

inductive MaybeTwo (α : Type u) | none | some (fst snd : α)

then the universe for MaybeTwo α must be Type u or higher. Lean automatically infers the universe to be the least universe, hence it chooses Type u, or, equivalently, Sort (u + 1). (See the reference guide to Universes for more details on the relationship between Prop, Sort, and 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, 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

Use of `Type` May Force Universe Too High
structure MyPair (α β : Sort u) : 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.Type _ where (a : α) (b : β) 
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.
structure MyPair (α β : Sort u) where (a : α) (b : β)
structure MyPair (α β : Sort u) : Sort (max 1 u) where (a : α) (b : β)
structure MyPair (α β : Type u) : Type _ where (a : α) (b : β)
structure MyPair (α β : Sort u) : Type u where (a : α) (b : β)

The initial type annotation Type _ forces MyPair into a universe that looks like Sort (_ + 1), but the best universe for MyPair is Sort (max u 1). (See the section on Prop vs Type for why it is Sort (max u 1) and not just Sort u.)

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.

Inductive Definition Needs Sort Annotations
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.inductive Bar | foobar {Foo} : Foo → Bar | barbar : Option Bar → Bar 
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.
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.