feat: Upstream derive handler for ToExpr from Mathlib

[alexkeizer]

This takes the derive handler for ToExpr from mathlib, and upstreams it into core.

The derive handler uses an auxiliary typeclass, ToLevel to ensure the derived ToExpr instances are properly universe polymorphic (when the original type is polymorphic), so we upstream this, too.

/-- A class to create `Level` expressions that denote particular universe levels in Lean.
`Lean.ToLevel.toLevel.{u}` evaluates to a `Lean.Level` term representing `u` -/
class ToLevel.{u} where
  /-- A `Level` that represents the universe level `u`. -/
  toLevel : Level
  /-- The universe itself. This is only here to avoid the "unused universe parameter" error. -/
  univ : Type u := Sort u

Credit goes to @kmill for originally developing the derive handler. We'll use this in a light-weight, basic QQ alternative that currently lives in a PR to LNSym, but we plan to upstream also.

[kmill]

Thanks for your interest Alex — upstreaming this has been on my radar for awhile, especially since #expr now uses ToExpr instances. However, for upstreaming, please be sure to run your plans by core developers ahead of time. It's still not clear how this ToExpr deriving handler will appear in core, and it has some issues that will likely need more core fixes (for example, ToLevel should not need to live in a universe above Type, yet it does).

[alexkeizer]

Thanks for your input, Kyle. For the record, I did mention, quite a while back, on the Zulip that I'd like to have ToExpr available in core, and got as response that this seemed like a good idea. Admittedly, I didn't follow up on that saying I would do it (since I wasn't planning to at the time), but recently figured I might as well get that ball rolling myself. I'll communicate this more clearly in the future.

[alexkeizer]

I've opened an issue to track the discussion at #5909

[kmill]

Great, the ToExpr RFC was just accepted — looking forward to seeing progress on this!

[alexkeizer]

Wonderful! I'm currently on vacation, but will push this forward when I'm back on the 25th!

By the way, where did this acceptance happen? I didn't see any activity on the issue.

[kmill]

It looks like there's a gap in FRO communication here — the triage team accepted it on Thursday and assigned to me seeing that it gets implemented.

I'd suggest that we do two PRs here. One would be adding ToLevel and fixing all the currently existing ToExpr handlers, and then the second would be this PR, upstreaming the ToExpr handler. Does that sound reasonable? (No need to respond until you get back!)

[alexkeizer]

@kmill Thanks for clarifying. Splitting it into 2 PRs makes sense to me!

For the first PR, should I upstream the ToLevel class as-is, or should I use the alternative definition I proposed in #5909 to avoid the universe bump?

[kmill]

We should use the improved ToLevel since we definitely don't want the universe bump.

[alexkeizer]

I've opened a PR to upstream ToLevel at #6285

[kmill]

There's a sort-of-bug that would be nice to fix. If you use these deriving handlers with set_option autoImplicit false, then the universe level variables cause errors.

Ideally we would use $(...):ident.{$levels,*} on this instance to insert levels, but that would prevent the automatic instance name generator from being used.

Alternatively, we could wrap the instance in three commands: section, universe $levels*, and end.

Would you mind adding a test that the deriving handler works when autoImplicit is false as well? (Take a look at lean/run/partialDelta.lean for an example of how test files are structured.)

[alexkeizer]

The "bug" is actually slightly trickier than that still: things also break if we explicitly add a universe u command, even if autoImplicits are enabled.

Alternatively, we could wrap the instance in three commands: section, universe $levels*, and end.

I implemented this, expect using universe $levels* in as an abbreviation for the section stuff.
Then, to prevent universe clashes, I check which universe names have been explicitly added to the Elaboration state, and remove those from the $levels list.

This fixes the tests that use exclusively explicit or implicit universes, but there is a final test that has both that still fails.

EDIT: turns out that failing test had a typo, and was in fact failing because it had an autoImplicit type parameter. I've fixed that typo, and added yet another testcase that tests the autoImplicit type parameter (and is currently still failing).

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b862e2d25163584322bcca54e5e56d671da1f258 --onto 8709ca35e9ddb977f7d050751e04981e2ab0d5c7. (2024-12-11 15:18:28)