feat: implement Repr Empty (#5415)

Given the derived `Repr` instance for types with parameters, the absence
of `Repr Empty` can cause `Repr` instance synthesis to fail. For
example, given
```lean
inductive Prim (special : Type) where
  | plus
  | other : special → Prim special
deriving Repr
```
this works:
```lean
#eval (Prim.plus : Prim Int)
```
but this fails:
```lean
#eval (Prim.plus : Prim Empty)
```

---------

Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

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"

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)