Imports change inferred universe

Stream: general

[Violeta Hernández]

@Jayde Massmann just came across some really weird behavior which I've minimized here

import Mathlib.SetTheory.ZFC.Basic
import Mathlib.Logic.UnivLE -- Code only works without this import!

universe u

theorem foo (x : ℕ -> ZFSet) : ZFSet.range x = ∅ := sorry
example (x : ℕ -> ZFSet.{u}) : ZFSet.range x = ∅ := foo x

Without the second import, foo infers a dummy argument u_1 for ZFSet, and the example works. With the second import, foo instead infers ZFSet.{0}, and the example does not typecheck.

[Violeta Hernández]

Is this a bug, an example of non-determinism, or is there some other explanation for this?

[Violeta Hernández]

Edit: Mathlib.Logic.UnivLE seems to be the minimal import that reproduces this bug. Suspicious.

[Violeta Hernández]

I imagine this isn't really a bug, and is rather some weird interaction between UnivLE and the Small instance argument in ZFSet.range. I'd still love to see an explanation for what's going on, though.

[Aaron Liu]

Should typeclass be allowed to unify universe metavariables like this? I'm not sure what the answer is.

[Eric Wieser]

import Lean

#eval Lean.ToLevel.toLevel.toNat -- some 127

is a very simple example of this

[Jovan Gerbscheid]

I agree that assigning universe metavariables is the issue here. But the source code contains a motivating example for why to allow universe metavairable assignments during type class search

"The example in the issue lean#796 exposed this issue.

structure A
class B (a : outParam A) (α : Sort u)
class C {a : A} (α : Sort u) [B a α]
class D {a : A} (α : Sort u) [B a α] [c : C α]
class E (a : A) where [c (α : Sort u) [B a α] : C α]
instance c {a : A} [e : E a] (α : Sort u) [B a α] : C α := e.c α

def d {a : A} [e : E a] (α : Sort u) [b : B a α] : D α := ⟨⟩

The term D α has two instance implicit arguments. The second one has type C α, and TC
resolution produces the result @c.{u} a e α b.
Note that the e has type E.{?v} a, and E is universe polymorphic,
but the universe does not occur in the parameter a. We have that ?v := u is implied by @c.{u} a e α b,
but this assignment is lost."

[Kyle Miller]

This is reminding me of an idea to have a concept of universe level outparams, which seems to be what u is for E.

[Jovan Gerbscheid]

It doesn't really look like a universe outParam in this example. I don't think there is a way to infer the universe level of E at the point of elaborating [e : E a].

[Kyle Miller]

Correct, it can't be inferred from E a. It's a universe level that's determined by the inferred instance, and is intended to be provided by that instance, rather than a universe level that is given to constrain typeclass inference. (That's my reading, but maybe it's meant to be a constraint. I'm thinking of some examples in category theory where some levels are meant to be determined by the instances.)