feat: implement To/FromJSON Empty

[TomasPuverle]

Resolve cases when the To/FromJSON type classes are used with Empty, e.g. in the following motivating example.

import Lean

structure Foo (α : Type) where
  y : Option α
deriving Lean.ToJson

#eval Lean.toJson (⟨none⟩ : Foo Empty) -- fails

This is a follow-up to this PR #5415, as suggested by @eric-wieser. It expands on the original suggestion by also handling FromJSON.

[TomasPuverle]

CC: @kmill in case interested/relevant.

[leanprover-community-mathlib4-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 738435b90aaa251a731cc463d6e49560f2037df9 --onto a6830f90ab365e14ccb7ca31201de37f8c1e978c. (2024-09-23 03:47:18)

[eric-wieser]

Perhaps it's not in core, but somewhere there's a json% elaborator which should avoid the quoting awkwardness here.

[david-christiansen]

There's also raw strings:

Suggested change

	#eval fromStrHelper (Foo Nat) "{\"y\": 1}"
	#eval fromStrHelper (Foo Nat) r#"{"y": 1}"#

[eric-wieser]

Suggested change

	#eval fromStrHelper (Foo Nat) "{\"y\": 1}"
	#eval Lean.fromJson? (α := Foo Nat) <| json% {"y": 1}

[david-christiansen]

As long as the string is a literal here, rather than something generated by deriving, it might save someone some debugging pain someday to write:

Suggested change

	fromJson? j := throw s!"no constructor matched JSON value '{j}'"
	fromJson? j := throw s!"type Empty has no constructor to match JSON value '{j}'"