Upstreaming `ToExpr` derive handler

Stream: lean4 dev

[Alex Keizer]

I'd like to upstream a derive handler for ToExpr into core. I figured I'd get the ball rolling by working on a PR (lean4#5906) to do just that, but @Kyle Miller responded:

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).

I'd be curious if people have thought on how to address these issues? It's quite painful not having ToExpr handlers available in LNSym.

[Kyle Miller]

I've been thinking about addressing this issue, and it's one of the reasons I haven't yet begun upstreaming that ToExpr derive handler myself yet :-)

The universe issue is tracked in lean4#2116

[Kyle Miller]

There's also the matter that core hasn't decide it wants this handler. If you could create an issue explaining that you want it and why, that would help me with the process of getting it in.

[Alex Keizer]

(That should be lean4#2116, I assume)

Interestingly, I tried to work around the universe bump issue by referring to the universe in an existential, like so:

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 : Prop := ∃ x, PUnit.{u} = x

Unfortunately, this still complains that u is unused

[Kyle Miller]

The issue doesn't have to be too detailed, but the question is "why core, why not another library, or why can't you embed it into LNSym"

[Kyle Miller]

One "why put it in core" reason for me is "it'll support #eval automatically pretty printing results"

[Kyle Miller]

There's also the added complexity that if the point is to support a Qq-lite library like you mentioned, should ToExpr be dropped in favor of a richer type that supports that sort of thing better?

This is where upstreaming the ToExpr deriving handler to Batteries got stuck, because some think it should be a ToQExpr deriving handler instead.

[Kyle Miller]

Here's a Qq version of ToExpr and a deriving handler by the way: mathlib4#5952

[Alex Keizer]

I guess for me the main reason for having the ToExpr derive handler in core is that ToExpr itself lives in core, and is used. That usage today could be nicer by having the derive handler available (even in projects that don't want to depend on Mathlib/Std4/Quote4).

Having a ToQExpr typeclass and derive handler certainly would be nice, but that's not entirely the same discussion; then we're talking about deprecating ToExpr entirely. I'd be happy with either having the ToExpr derive handler or having ToExprQ and a handler, but currently we have neither (in core)

[Alex Keizer]

I created an issue: https://github.com/leanprover/lean4/issues/5909

[Alex Keizer]

Alex Keizer said:

(That should be lean4#2116, I assume)

Interestingly, I tried to work around the universe bump issue by referring to the universe in an existential, like so:
...

I was being a bit silly there, the default value of a field is not actually part of the structure's definition so the error is correct (even if it looks a bit funny at first glance).

The following, does work: :tada:

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

#check ToLevel -- Lean.ToLevel.{u} : Type

[Eric Wieser]

I think lean4#2116 has a simpler workaround in the comments via a let?