RFC: Upstreaming the derive handler for ToExpr

[alexkeizer]

Proposal

Currently we have ToExpr in core, but it's derive handler lives in Mathlib.
This makes ToExpr unnecessarily painful to use for those projects (e.g., leanprover/LNSym) that do not want to depend on Mathlib.

Since ToExpr itself already lives in core, it seems within scope to also have the corresponding derive handler upstream.
Another benefit, brought up by @kmill, is that it'll support #eval automatically pretty printing results.

Maintaining this derive handler naturally has a cost, but having it will mean we no longer have to support the various hand-written instances we currently have in Lean.toExpr, and it enables us to easily add more instances we should have (e.g., ToExpr Expr) by reducing the maintenance burden for a specific instance.

Community Feedback

Previously, it has been tried to upstream this handler to batteries (batteries#221). The discussion then focussed on the merits of ToExprQ over ToExpr, ending with the following comment with the following comment by @kim-em:

We've decided not to do this for now. The long term plan is to migrate quote4 into std4 and then implement the ToExprQ derive handler instead.

(For what it's worth, I think "perfect is the enemy of good" applies here...)

This was August 2023, and this has not since moved forward. I believe that Kim's comment about "perfect is the enemy of good" applies even stronger today.

Regardless of an eventual move to ToExprQ or similar in the distant future, we can improve usage of ToExpr today.

A more recent Zulip discussion also brought up that ToLevel (a new typeclass used by the derive handler to support universe polymorphism) currently unnecessarily involves a universe bump --- in the sense that ToLevel.{u} should live in Type but currently lives in Type (u+1) to avoid an "unused universe variable" error. This issue is already being tracked in lean4#2116.

Regardless, I believe here, too, "perfect is the enemy of good" is applicable. Currently, core has an instance of ToExpr (List α) which is already broken when α lives in a higher universe:

import Lean
open Lean

instance : ToExpr (PUnit.{2}) where
  toTypeExpr := .const ``PUnit [2]
  toExpr _ := .const ``PUnit.unit [2]

#eval @id (MetaM _) <| do
  let u := PUnit.unit.{2}
  let x := [u]
  Meta.check (toExpr u) -- type checks
  Meta.check (toExpr x) -- does not type check

This is known, and Mathlib overrides these instances, using the derive handler, to circumvent this. If we upstream the handler, we can fix these instances in core itself, improving the status quo, even if the universe bump in ToLevel is not 100% perfect yet.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

[alexkeizer]

Regarding the issue with ToLevel, we can actually circumvent the universe bump by redefining the univ field as follows:

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.
    We'll remove this field once https://github.com/leanprover/lean4/issues/2116 gets fixed.
  -/
  univ : ∃ x, x = PUnit.unit.{u} := ⟨_, rfl⟩

With this version, ToLevel.{u} indeed lives in Type