diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean
index 2c45dc14c2..c1f7e522df 100644
--- a/src/Init/Data/Repr.lean
+++ b/src/Init/Data/Repr.lean
@@ -51,6 +51,12 @@ instance [Repr α] : Repr (id α) :=
 instance [Repr α] : Repr (Id α) :=
   inferInstanceAs (Repr α)
 
+/-
+This instance allows us to use `Empty` as a type parameter without causing instance synthesis to fail.
+-/
+instance : Repr Empty where
+  reprPrec := nofun
+
 instance : Repr Bool where
   reprPrec
     | true, _  => "true"
diff --git a/tests/lean/run/repr_empty.lean b/tests/lean/run/repr_empty.lean
new file mode 100644
index 0000000000..8d917ce974
--- /dev/null
+++ b/tests/lean/run/repr_empty.lean
@@ -0,0 +1,29 @@
+/-!
+# Validation of `Repr Empty` instance
+
+While it may seem unnecessary to have Repr, it prevents the automatic derivation
+of Repr for other types when `Empty` is used as a type parameter.
+
+This is a simplified version of an example from the "Functional Programming in Lean" book.
+The Empty type is used to exlude the `other` constructor from the `Prim` type.
+-/
+
+inductive Prim (special : Type) where
+  | plus
+  | minus
+  | other : special → Prim special
+deriving Repr
+
+/-!
+Check that both Repr's work
+-/
+
+/-- info: Prim.plus -/
+#guard_msgs in
+open Prim in
+#eval (plus : Prim Int)
+
+/-- info: Prim.minus -/
+#guard_msgs in
+open Prim in
+#eval (minus : Prim Empty)