Zulip Chat Archive

Stream: general

Topic: crazy universe

Patrick Massot (Aug 13 2021 at 22:10):

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 (Aug 13 2021 at 22:12):

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

Patrick Massot (Aug 13 2021 at 22:16):

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

Kyle Miller (Aug 13 2021 at 22:27):

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 (Aug 13 2021 at 22:42):

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 (Aug 13 2021 at 22:49):

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 (Aug 13 2021 at 23:03):

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 (Aug 14 2021 at 07:12):

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 (Aug 14 2021 at 07:13):

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 (Aug 14 2021 at 10:27):

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

Floris van Doorn (Aug 14 2021 at 17:58):

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 (Aug 15 2021 at 03:59):

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 (Aug 15 2021 at 04:03):

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 (Aug 15 2021 at 04:17):

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 (Aug 15 2021 at 06:16):

@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 (Aug 15 2021 at 06:43):

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

Floris van Doorn (Aug 15 2021 at 06:53):

Ok, I've added it to #8677

Simon Hudon (Aug 15 2021 at 06:54):

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

Floris van Doorn (Aug 15 2021 at 06:59):

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 (Aug 15 2021 at 09:19):

Great! Thank you very much Floris!

Last updated: Aug 03 2023 at 10:10 UTC