From 1883c9b7ebb68c18980f5b17b59f6d77bc401b99 Mon Sep 17 00:00:00 2001 From: TomasPuverle Date: Sun, 22 Sep 2024 18:11:36 -0700 Subject: [PATCH] feat: implement `Repr Empty` (#5415) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 Co-authored-by: Eric Wieser --- src/Init/Data/Repr.lean | 6 ++++++ tests/lean/run/repr_empty.lean | 29 +++++++++++++++++++++++++++++ 2 files changed, 35 insertions(+) create mode 100644 tests/lean/run/repr_empty.lean 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)