From a108644461b2182d7380154f6b4e87e4d5167b7d Mon Sep 17 00:00:00 2001
From: TomasPuverle <TomasPuverle@users.noreply.github.com>
Date: Mon, 23 Sep 2024 20:27:23 -0700
Subject: [PATCH] feat: implement `To/FromJSON Empty` (#5421)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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
https://github.com/leanprover/lean4/pull/5415, as suggested by
@eric-wieser. It expands on the original suggestion by also handling
`FromJSON`.

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
---
 src/Lean/Data/Json/FromToJson.lean |  6 ++++
 tests/lean/run/json_empty.lean     | 53 ++++++++++++++++++++++++++++++
 2 files changed, 59 insertions(+)
 create mode 100644 tests/lean/run/json_empty.lean

diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index 1cfbe06ffa09..a6774aff3ddd 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/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⟩
diff --git a/tests/lean/run/json_empty.lean b/tests/lean/run/json_empty.lean
new file mode 100644
index 000000000000..806234255a21
--- /dev/null
+++ 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}