possible bug re: universe level count due to type ambiguity

Stream: lean4

[Matt Diamond]

I ran into a weird too many explicit universe levels error recently and thought I would share here:

import Mathlib.ModelTheory.Basic
import Mathlib.Computability.Language

universe u v

open FirstOrder

variable (L1 : Language)

#check L1 -- L1 : FirstOrder.Language

variable (L2 : Language.{u, v}) -- "too many explicit universe levels"

The universe level error does not occur if you comment out the Mathlib.Computability.Language import, so it seems likely that Lean is confusing docs#FirstOrder.Language and docs#Language when calculating the correct number of universe levels, despite the fact that it otherwise interprets the type as FirstOrder.Language.

[François G. Dorais]

I found this (unsatisfactory) workaround:

import Mathlib.ModelTheory.Basic
import Mathlib.Computability.Language

example (L2 : (FirstOrder.Language.{u, v} : Type (max u v + 1))) : True := trivial

[Matt Diamond]

Oh, I should have mentioned that the bug doesn't occur if you use namespace instead of open, which is potentially relevant

[Matt Diamond]

so there's another workaround for the time being

[Matt Diamond]

should I open an issue on GitHub? this seems like a legitimate bug (not a high priority one but still worth fixing at some point)

[François G. Dorais]

Probably since this is unexpected behavior for sure. But you need a mwe first: remove the imports.

[François G. Dorais]

That's not an easy task.

[Matt Diamond]

Sorry, I'm a bit unclear on what you mean... aren't the imports necessary for this example? Or are you saying that we need a mwe which doesn't rely on Mathlib?

[François G. Dorais]

The imports include a lot of things that are not relevant to the issue, which makes diagnosis nearly impossible.

One mwe path is to have a file with no imports. Replace FirstOrder.Language with a structure with the same fields but filled with sorries. Tren add more and more details until you can reproduce the bug.

[Matt Diamond]

Gotcha, will try that.

[Matt Diamond]

To be fair, I feel like diagnosis should be relatively easy given that the universe level count is determined by docs#Lean.Elab.Term.mkConst which appears to rely on docs#Lean.getConstVal ... I'm guessing that getConstVal has access to namespaces but not open declarations. However, I'll see if I can come up with a minimal example anyway. (Also, I have very little knowledge of Lean internals so it's possible that my assumptions here are completely off.)