feat: implement To/FromJSON Empty (#5421)

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

---------

Co-authored-by: Kyle Miller <[email protected]>

src/Lean/Data/Json/FromToJson.lean

@@ -28,6 +28,12 @@ instance : ToJson Json := ⟨id⟩
 instance : FromJson JsonNumber := ⟨Json.getNum?⟩
 instance : ToJson JsonNumber := ⟨Json.num⟩
 
+instance : FromJson Empty where
+  fromJson? j := throw (s!"type Empty has no constructor to match JSON value '{j}'. \
+                           This occurs when deserializing a value for type Empty, \
+                           e.g. at type Option Empty with code for the 'some' constructor.")
+
+instance : ToJson Empty := ⟨nofun⟩
 -- looks like id, but there are coercions happening
 instance : FromJson Bool := ⟨Json.getBool?⟩
 instance : ToJson Bool := ⟨fun b => b⟩

tests/lean/run/json_empty.lean

@@ -0,0 +1,53 @@
+import Lean
+
+/-!
+# Validation of `Json Empty` instance
+
+This test serves a similar purpose to the `Repr Empty` test in `repr_empty.lean`.
+-/
+
+structure Foo (α : Type) where
+  y : Option α
+deriving Lean.ToJson, Lean.FromJson, Repr
+
+/-! First, two basic examples with α not-Empty -/
+/-- info: {"y": 1} -/
+#guard_msgs in
+#eval Lean.toJson (⟨some 1⟩ : Foo Nat)
+
+/-! Ensure we can parse the type back -/
+/-- info: Except.ok { y := some 1 } -/
+#guard_msgs in
+#eval Lean.fromJson? (α := Foo Nat) <| json% {"y": 1}
+
+/-- info: {"y": null} -/
+#guard_msgs in
+#eval Lean.toJson (⟨none⟩ : Foo Nat)
+
+/-- info: Except.ok { y := none } -/
+#guard_msgs in
+#eval Lean.fromJson? (α := Foo Nat) <| json% {"y": null}
+
+/-! Examples with the `Empty` type -/
+/-- info: {"y": null} -/
+#guard_msgs in
+#eval Lean.toJson (⟨none⟩ : Foo Empty)
+
+/-! Show that we can round-trip from string  -/
+/-- info: Except.ok { y := none } -/
+#guard_msgs in
+#eval Lean.fromJson? (α := Foo Empty) <| json% {"y": null}
+
+/-! Show that parsing fails -/
+/-- info: Except.error "type Empty has no constructor to match JSON value '\"Yo!\"'.
+This occurs when deserializing a value for type Empty, e.g. at type Option Empty with code
+for the 'some' constructor." -/
+#guard_msgs in
+#eval Lean.fromJson? (α := Empty) <| json% "Yo!"
+
+/-! Show that parsing fails if we supply anything else but `null` -/
+/-- info: Except.error "Foo.y: type Empty has no constructor to match JSON value '1'.
+This occurs when deserializing a value for type Empty, e.g. at type Option Empty with code
+for the 'some' constructor." -/
+#guard_msgs in
+#eval Lean.fromJson? (α := Foo Empty) <| json% {"y": 1}