crazy universe

Stream: general

[Patrick Massot]

Does anyone understands why Lean gets crazy with universes in docs#topological_add_group.of_comm_of_nhds_zero? I can fix this by replacing G : Type* by G : Type u but it would be nice to understand when this happens because it really causes a lot of confusion when it strikes.

[Eric Wieser]

You can also fix it by moving G to a variables statement

[Patrick Massot]

Could we have a linter for this? I can't imagine a situation where a parameter can have such a universe annotation.

[Kyle Miller]

It seems to not realize that once it's solved for the universe variables it can generalize max u_1 u_2 (or, rather, it found too specialized of a solution through whatever algorithm it uses). Here's the pp.universes output at the beginning of that lemma's proof:

G : Type (max u_1 u_2),
_inst_5 : comm_group.{(max u_1 u_2)} G,
_inst_6 : topological_space.{(max u_1 u_2)} G,
hmul :
  tendsto.{(max u_1 u_2) (max u_1 u_2)}
    (uncurry.{(max u_1 u_2) (max u_1 u_2) (max u_1 u_2)} has_mul.mul.{(max u_1 u_2)})
    (𝓝 1 ×ᶠ 𝓝 1)
    (𝓝 1),
hinv : tendsto.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x⁻¹) (𝓝 1) (𝓝 1),
hleft : ∀ (x₀ : G), 𝓝 x₀ = map.{(max u_1 u_2) (max u_1 u_2)} (λ (x : G), x₀ * x) (𝓝 1)
⊢ topological_group.{(max u_1 u_2)} G

[Kyle Miller]

In case it's helpful in figuring out what's going on, it's something to do with the hinv argument.

lemma crazy_universe {G : Type*} [topological_space G]
  (f : G → G → G) (a : G)
  (hinv : tendsto (uncurry f) ((𝓝 a) ×ᶠ 𝓝 a) (𝓝 a)) :
  true :=
sorry -- can see that G : Type (max u_1 u_2)

[Kyle Miller]

This reproduces it, too:

def crazy_universe {G : Type*} (F : filter G)
  (h : F ×ᶠ F = F ×ᶠ F) : true :=
sorry -- can see G : Type (max u_1 u_2)

Strangely, replacing filter with set doesn't show this behavior:

import order.filter.basic

def crazy_universe {G : Type*} (s : filter G)
  (h : s.prod s = s.prod s) : true :=
sorry -- can see G : Type (max u_1 u_2)

def ok_universe {G : Type*} (s : set G)
  (h : s.prod s = s.prod s) : true :=
sorry -- can see G : Type u_1

[Kyle Miller]

Changing the transparency of set to irreducible changes the inferred universe:

attribute [irreducible] set
def crazy_universe' {G : Type*} (s : set G)
  (h : s.prod s = s.prod s) : true :=
sorry -- can see G : Type (max u_1 u_2)

[Kevin Buzzard]

I've seen a few of these recently and I've always just figured that it's the fact that lean universe arithmetic is hardly its strong point and it's just easier to do it yourself sometimes

[Kevin Buzzard]

I agree with Patrick that it's confusing. It can often manifest itself in things taking much longer to typecheck than they should

[Reid Barton]

This sort of thing is why I largely stopped using Type* outside of variables.

[Floris van Doorn]

Yeah, we can definitely have a linter that catches this kind of behavior.
We can probably just check for an argument of the form Type (max _ _) or Sort (max _ _)(ignoring the conclusion). I think that doesn't give many false positives.

[Floris van Doorn]

I opened #8677, where I fix a bunch of current bad universes in the library.
The linter has a bunch of false positives in declarations, such as src#module.projective, where Type (max u v) is used as an arbitrary type larger than Type u.
There were also still a bunch of bad declarations that weren't caught by my linter, like src#algebraic_geometry.Spec.SheafedSpace_map, where CommRing means CommRing.{max u v}. In this case I was lucky, since an auxiliary declaration part of this one was caught by the linter.

I think we should make a linter where we properly test for declarations whether it has two universe variables u and v that only occur as max u v. This is a little trickier to test than my previous suggestion, but I'll take another stab.

[Mario Carneiro]

I don't think false positives are a problem here, since the few cases where they are used legitimately could use a small acknowledgment in the form of a @[nolint] and/or comment

[Floris van Doorn]

That's true, but note that we also need to apply nolint to all lemmas that use module.projective. But the current version doesn't catch much more false positives (there are ~5 rarely used declarations, for example src#uliftable.adapt_up in control/uliftable).

I hope that the proper version of the linter catches more declarations that are ignored by the current linter.

[Floris van Doorn]

@Simon Hudon Can you tell me how to fix the universe levels of src#uliftable.down_map?
Currently the universes u₀ and v₀ only occur in the declaration as max u₀ v₀. I suspect that G : Type → Type v₁ should be replaced by G : Type u₀ → Type v₁?

[Simon Hudon]

@Floris van Doorn you're right, that's what it should be. That's a simple fix

[Floris van Doorn]

Ok, I've added it to #8677

[Simon Hudon]

Oh you're a bit faster than me: #8684

[Floris van Doorn]

I've PR'd the linter in #8685. This version catches a lot more problematic declarations than the earlier version, and I don't think it gives any false positives.

[Patrick Massot]

Great! Thank you very much Floris!