invalid occurrence of universe level 'u_1'

Stream: new members

[Shanghe Chen]

Hi I got an error like invalid occurrence of universe level 'u_1' in the following code snippet:

import Mathlib.CategoryTheory.Functor.Basic
import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.Yoneda
import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
import Mathlib.CategoryTheory.Limits.Shapes.CommSq
import Mathlib.CategoryTheory.Limits.Shapes.Diagonal
import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
import Mathlib.CategoryTheory.Limits.HasLimits
import Mathlib.CategoryTheory.Limits.IsLimit
import Mathlib.CategoryTheory.Limits.Types
import Mathlib.CategoryTheory.Limits.Yoneda
import Mathlib.CategoryTheory.Limits.Presheaf
import Mathlib.CategoryTheory.Limits.Preserves.Limits

noncomputable section
universe v u

set_option autoImplicit false

open CategoryTheory Category Functor Limits IsLimit

variable {C: Type u} [Category.{v} C] [HasFiniteLimits C]
variable {Y Z : C}
variable (g: Y ⟶ Z)
#check pullback.diagonal (yoneda.map g)
/--
 the diagonal morphism Y -> Y ×Z Y
-/
def d := pullback.diagonal g
#check d (yoneda.map g)
lemma test_d : True := by
  have := (d (yoneda.map g))
  sorry

The detailed error is:

invalid occurrence of universe level 'u_1' at 'test_d', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  hasFiniteLimits_of_hasLimitsOfSize.{u_1, v, max u v, max u (v + 1)}
    (CategoryTheory.Functor.{v, v, u, v + 1} (Opposite.{u + 1} C) (Type v))
at declaration body
  fun {C : Type u} [Category.{v, u} C] {Y Z : C} (g : Y ⟶ Z) ↦
    let_fun this : yoneda.obj Y ⟶ pullback.diagonalObj (yoneda.map g) := d (yoneda.map g);
    sorryAx True

It seems there is some extra universe argument but I am not clear why

[Shanghe Chen]

I found similar error in https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60mkAppM.60.20fails.20with.20multiple.20universe.20metavariables but after quickly reading it I still have no direction on how to fix it. :smiling_face_with_tear:

[Kyle Miller]

On the most recent mathlib, I'm not seeing this error.

Could you set set_option pp.universes true to see a more detailed error?

[Shanghe Chen]

Sure! It seems reported by the HasFiniteLimits instance synthesized for the category CategoryTheory.Functor.{v, v, u, v + 1} (Opposite.{u + 1} C) (Type v)

[Shanghe Chen]

image.png

[Shanghe Chen]

my local copy for mathlib seems to be db651742f2 at tag v4.8.0-rc1

[Joël Riou]

As a temporary fix (if updating does not work), you may try to insert

instance : HasFiniteLimits (Cᵒᵖ ⥤ Type v) :=
  hasFiniteLimits_of_hasLimitsOfSize.{0, 0} _

[Kyle Miller]

I see the error in my v4.8.0-rc1 mathlib too. If you set set_option pp.all true, you can see the universe level metavariables that are inside the expression, like @CategoryTheory.Limits.functorCategoryHasLimitsOfSize.{?u.6523, v, v, u, v, v + 1}

[Kyle Miller]

If you see an invalid occurrence of universe level 'u_1' error (with a numeric suffix like that) it usually indicates that the body of the lemma has a universe level metavariable.

[Joël Riou]

The problem is with the instance hasFiniteLimits_of_hasLimitsOfSize C. It is a good lemma, but it should be made an instance only for universes that can be deduced from the category C (or for {0, 0}).

[Shanghe Chen]

Thank you Kyle and Joël for the kindly help and detailed explanation :smiling_face: I updated to the latest commit of master branch. It's taking some time for compilation now

[Shanghe Chen]

Update to master not working for me but instance : HasFiniteLimits (Cᵒᵖ ⥤ Type v) := hasFiniteLimits_of_hasLimitsOfSize.{0, 0} _ works:tada: To late in my timezone I will continue it tomorrow

[Kyle Miller]

Here's another way to fix this, using a local instance:

lemma test_d : True := by
  have := hasFiniteLimits_of_hasLimitsOfSize.{0} (Cᵒᵖ ⥤ Type v)
  have := (d (yoneda.map g))
  sorry

[Joël Riou]

This is fixed in PR #12797.

[Shanghe Chen]

Hi Joël it's awesome:tada: Is it now in the master branch? My local env checking out 945d7cf3cf seems still requiring the temp fix :blush:

[Joël Riou]

The fix on master was done a few hours ago: you need to update...

[Shanghe Chen]

Yeah after update it works!:tada:

[Mark Aagaard]

Hello,

I'm getting the error invalid occurrence of universe level 'u_1' when writing expressions that contain an empty list.
I'm able to prevent the error by writing a type assertion for the empty list, but I'd like to avoid this if possible.

variable (α : Type 0)

abbrev xs0 := List.length ([] : List α)  -- this works, because there is a type assertion

abbrev xs1 : ℕ := List.length [] + List.length []  -- this fails with: invalid occurrence of universe level 'u_1'

The larger context is I'm teaching an intro to logic course to computer engineers and am trying to keep the syntax as simple as possible. I'm happy to define my own length function that works only over Type 0 types, if that's a route toward a solution. (In this first offering of the course, I'm using Lean primarily for the students to write and typecheck logical expressions. I'm not yet having the students prove theorems in Lean, so it's ok if I lose access to the List tactics.)

I tried writing my own size function as:

abbrev size3 : List α → ℕ
  | [] => 0
  | x :: xs => 1 + size3 xs

abbrev xs3 := size3 [] = 0

and got the error: don't know how to synthesize implicit argument @size3 ?m.555 (@List.nil.{0} ?m.555)

-mark

[Edward van de Meent]

the point is that once again, lean can't figure out what α is. (i.e., lean is trying to figure out what the type of [] is, but gets stuck at List ?A)

[Edward van de Meent]

and btw, α : Type is a shortcut for α : Type 0, which you might find helpful in teaching.

[Edward van de Meent]

for teaching, it might be helpful if you use set_option autoImplicit false

[Edward van de Meent]

this way, it becomes more obvious when you introduce type polymorphism

[Kyle Miller]

If you use any mathlib from this month, the error message is less obscure:

abbrev xs1 : ℕ := List.length [] + List.length []
/-
don't know how to synthesize implicit argument 'α'
  @List.length ?m.4210 []
-/

The universe level issue was the less-strong reason why the definition failed. The proximal reason is what Edward says, the type argument to List.length isn't able to be solved for.

[Mark Aagaard]

Thanks for the quick and helpful replies.

-mark