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}