yet another universe issue

Stream: general

[Kevin Buzzard]

I cannot believe it. I just spent several hours porting 350 lines of mathlib over to get a mathlib-independent MWE of a time-out issue (file available here) and after I was done I was just setting up the question to post, and I managed to solve it. It's another universe issue. See the last few lines of the gist.

@Gabriel Ebner @Mario Carneiro I was going to ask you a question but I solved it myself, however maybe you are interested in a mathlib-free universe issue. If I say {R : Type u} then my lemma typechecks no problem, but with {R : Type*} I get excessive memory consumption errors -- and even if things do work they clearly take much much longer. Is this evidence that {R : Type*} should be avoided? I think Reid told me he avoided it years ago, but now I am beginning to think that replacing all Type*s by Type u's in mathlib (when they occur in a def or lemma statement) might result in a speed-up: one could make the definition with Type, see what Lean thinks Type should be, and then replace it with its conclusion.

[Mario Carneiro]

I still think it is better not to bother folks with universe management in 99% of cases

[Mario Carneiro]

If you say always use Type u then you are likely to make lemmas which have (A : Type u) (B : Type u) which will cause problems later

[Mario Carneiro]

It would be nice if there was a variant on Type* which was Type <fresh universe variable> instead of Type <fresh metavariable> since it is the metavariables that cause the problem here

[Eric Wieser]

The other way to solve this problem is to try and put types in variables statements instead of in definitions

[Eric Wieser]

Which means we get to keep Type*

[Eric Wieser]

Also, a fun fact - if you write variables {a b c d e f g h i j : Type*} then u_10 becomes a universe variable you can reference by name.

[Eric Wieser]

Also, regarding Kevin's repro - from what I remember set_option profiler true does not measure any of this universe variable unification time, which in the case of this lemma was almost all of the time.

[Eric Wieser]

Mario Carneiro said:

It would be nice if there was a variant on Type* which was Type <fresh universe variable> instead of Type <fresh metavariable> since it is the metavariables that cause the problem here

How much would break if Type* _became_ that meaning, and Type _ continues to mean "fresh metavariable"?

[Kevin Buzzard]

The point of Type* within a theorem statement is "OK so maybe R will end up having type imax (max u v) w", right?

[Eric Wieser]

That's certainly the effect, I can't comment on whether it was the intent

[Eric Wieser]

I managed to solve it. It's another universe issue. See the last few lines of the gist.

As far as I can tell, that universe issue is only present in your MWE, not in the original

[Mario Carneiro]

Eric Wieser said:

Also, a fun fact - if you write variables {a b c d e f g h i j : Type*} then u_10 becomes a universe variable you can reference by name.

Indeed, Type* in variable actually means Type <fresh universe variable>, to add to the confusion

[Yaël Dillies]

And is the <fresh universe variable> common to the newly declared variables? Is using variables {X Y : Type*} implying that X and Y have the same type?

[Kevin Buzzard]

No (it used to mean this, it changed a year or so ago)

[Yaël Dillies]

Ah okay great. I am overly using it and was getting worried.