StateM and Result not universe polymorphic

Stream: lean4

[Jakob von Raumer]

Is there a reason that lots of the monads, e.g. StateM and EStateM are not fully universe polymorphic?

[Markus Himmel]

Cf. lean4#3010; I believe the status of the PR is basically "increasing universe polymorphism is a double-edged sword because it can cause elaboration problems at some unknown time in the future, and there is no need for this within the Lean repository, so the FRO has been hesitant to pull the trigger and doesn't plan to invest time into this at the moment"

[Jakob von Raumer]

Thanks, at least I'm not the only one with the issue :sweat_smile:

[Eric Wieser]

I thought the status of the PR was just "the benchmark looks too good to be true"?

[Eric Wieser]

Though unfortunately now that Batteries is proving stuff about EStateM, things are starting to rot

[Kim Morrison]

I think Markus has just updated the status..:-)

[Eric Wieser]

increasing universe polymorphism is a double-edged sword because it can cause elaboration problems at some unknown time in the future,

Do we have any reason to believe this?

[Eric Wieser]

And there is no need for this within the Lean repository

Doesn't lake make its own universe-polymorphic copy?

[Ruben Van de Velde]

We had that weird issue with the enormous slowdowns in mathlib recently, didn't we? Not sure if that counts as "elaboration problems"

[Eric Wieser]

All the mathlib cases were I believe ones where the universe variables were instantiated with max u v or similar, lean4#3010 in practice is only going to instantiate with free variables. Of course someone can write crazy code that does otherwise, but even then EStateM is a low level metaprogramming tool that is pretty far away from the kind of problem mathlib has.