CharToNat and NatToChar type families
@RyanGlScott’s work on `singletons` revealed that built-in type families added in 7f3524efcbd58ca6837ec0ffca6ddd121d64e4de are insufficient to implement a promoted variant of `Show Char`.
For `Show`, we need `CharToNat`. And with `NatToChar` to accompany it, we can also define promoted `Enum Char`.
These type families were originally part of !3598, but it is currently on hold because it’s unclear whether we want to add so many built-in definitions (and also because the author currently has no time to rebase it and clean it up, at least in time for the %"9.2.1" release). However, now there’s a clear case for `CharToNat` and `NatToChar`, so this ticket is to track their addition.
Patch here: !5258
issue