Autoderiving instances for `#eval`

Stream: lean4

[Eric Wieser]

Should the auto-derivation emit a warning recommending the user add deriving instance Repr for Tp?

[Eric Wieser]

In particular:

#eval ℕ ⇒ ℕ -- works
#eval (ℕ ⇒ ℕ, 0) -- fails

deriving instance Repr for Tp

#eval (ℕ ⇒ ℕ, 0) -- works

[Notification Bot]

2 messages were moved here from #lean4 > Prettyprinting the result of an #eval by Kyle Miller.

[Kyle Miller]

This was something I wasn't sure about. I expect autoderivation to be relatively quick, so it's not clear to me anyone needs to be told to add deriving commands themselves. On the other hand, it would be a shame if people didn't know they could speed up #eval a little bit by deriving the instances!

Recursive autoderivation is still something I am thinking about. The main change was to get #eval into a state where it was even possible to consider autoderivation at all, so the current form is a proof of the concept.

I'm also considering things like having #eval throw in "fake" Repr instances for unrepresentable objects, like

instance : Repr Type where
  reprPrec _ _ := "<type>"

possibly by having a namespace of scoped instances it can activate.

Eventually we may even see a ToExpr deriving handler in core. A neat thing for that would be that in truly unrepresentable situations (like functions Nat -> Nat), the pretty printed omissions could have hovers that explain why they are missing.