Built-in type families: CharToNat, NatToChar (#19535)

Co-authored-by: Daniel Rogozin <daniel.rogozin@serokell.io>
Co-authored-by: Rinat Stryungis <rinat.stryungis@serokell.io>

8 files changed, 191 insertions, 31 deletions

diff --git a/compiler/GHC/Builtin/Names.hs b/compiler/GHC/Builtin/Names.hs
index 4779ca8de2..ec8d5a0afc 100644
--- a/compiler/GHC/Builtin/Names.hs
+++ b/compiler/GHC/Builtin/Names.hs
@@ -2000,41 +2000,10 @@ uFloatTyConKey  = mkPreludeTyConUnique 161
 uIntTyConKey    = mkPreludeTyConUnique 162
 uWordTyConKey   = mkPreludeTyConUnique 163
 
--- Type-level naturals
-typeSymbolKindConNameKey, typeCharKindConNameKey,
-  typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
-  typeNatSubTyFamNameKey
-  , typeSymbolCmpTyFamNameKey, typeNatCmpTyFamNameKey, typeCharCmpTyFamNameKey
-  , typeLeqCharTyFamNameKey
-  , typeNatDivTyFamNameKey
-  , typeNatModTyFamNameKey
-  , typeNatLogTyFamNameKey
-  , typeConsSymbolTyFamNameKey, typeUnconsSymbolTyFamNameKey
-  :: Unique
-typeSymbolKindConNameKey  = mkPreludeTyConUnique 165
-typeCharKindConNameKey    = mkPreludeTyConUnique 166
-typeNatAddTyFamNameKey    = mkPreludeTyConUnique 167
-typeNatMulTyFamNameKey    = mkPreludeTyConUnique 168
-typeNatExpTyFamNameKey    = mkPreludeTyConUnique 169
-typeNatSubTyFamNameKey    = mkPreludeTyConUnique 171
-typeSymbolCmpTyFamNameKey = mkPreludeTyConUnique 172
-typeNatCmpTyFamNameKey    = mkPreludeTyConUnique 173
-typeCharCmpTyFamNameKey   = mkPreludeTyConUnique 174
-typeLeqCharTyFamNameKey   = mkPreludeTyConUnique 175
-typeNatDivTyFamNameKey  = mkPreludeTyConUnique 176
-typeNatModTyFamNameKey  = mkPreludeTyConUnique 177
-typeNatLogTyFamNameKey  = mkPreludeTyConUnique 178
-typeConsSymbolTyFamNameKey = mkPreludeTyConUnique 179
-typeUnconsSymbolTyFamNameKey = mkPreludeTyConUnique 180
-
 -- Custom user type-errors
 errorMessageTypeErrorFamKey :: Unique
 errorMessageTypeErrorFamKey =  mkPreludeTyConUnique 181
 
-
-
-ntTyConKey:: Unique
-ntTyConKey = mkPreludeTyConUnique 182
 coercibleTyConKey :: Unique
 coercibleTyConKey = mkPreludeTyConUnique 183
 
@@ -2093,6 +2062,38 @@ multMulTyConKey = mkPreludeTyConUnique 199
 
 #include "primop-vector-uniques.hs-incl"
 
+------------- Type-level Symbol, Nat, Char ----------
+--      USES TyConUniques 400-499
+-----------------------------------------------------
+typeSymbolKindConNameKey, typeCharKindConNameKey,
+  typeNatAddTyFamNameKey, typeNatMulTyFamNameKey, typeNatExpTyFamNameKey,
+  typeNatSubTyFamNameKey
+  , typeSymbolCmpTyFamNameKey, typeNatCmpTyFamNameKey, typeCharCmpTyFamNameKey
+  , typeLeqCharTyFamNameKey
+  , typeNatDivTyFamNameKey
+  , typeNatModTyFamNameKey
+  , typeNatLogTyFamNameKey
+  , typeConsSymbolTyFamNameKey, typeUnconsSymbolTyFamNameKey
+  , typeCharToNatTyFamNameKey, typeNatToCharTyFamNameKey
+  :: Unique
+typeSymbolKindConNameKey  = mkPreludeTyConUnique 400
+typeCharKindConNameKey    = mkPreludeTyConUnique 401
+typeNatAddTyFamNameKey    = mkPreludeTyConUnique 402
+typeNatMulTyFamNameKey    = mkPreludeTyConUnique 403
+typeNatExpTyFamNameKey    = mkPreludeTyConUnique 404
+typeNatSubTyFamNameKey    = mkPreludeTyConUnique 405
+typeSymbolCmpTyFamNameKey = mkPreludeTyConUnique 406
+typeNatCmpTyFamNameKey    = mkPreludeTyConUnique 407
+typeCharCmpTyFamNameKey   = mkPreludeTyConUnique 408
+typeLeqCharTyFamNameKey   = mkPreludeTyConUnique 409
+typeNatDivTyFamNameKey  = mkPreludeTyConUnique 410
+typeNatModTyFamNameKey  = mkPreludeTyConUnique 411
+typeNatLogTyFamNameKey  = mkPreludeTyConUnique 412
+typeConsSymbolTyFamNameKey = mkPreludeTyConUnique 413
+typeUnconsSymbolTyFamNameKey = mkPreludeTyConUnique 414
+typeCharToNatTyFamNameKey = mkPreludeTyConUnique 415
+typeNatToCharTyFamNameKey = mkPreludeTyConUnique 416
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/GHC/Builtin/Types/Literals.hs b/compiler/GHC/Builtin/Types/Literals.hs
index 6b21a68bd3..19dcba7116 100644
--- a/compiler/GHC/Builtin/Types/Literals.hs
+++ b/compiler/GHC/Builtin/Types/Literals.hs
@@ -21,6 +21,8 @@ module GHC.Builtin.Types.Literals
   , typeCharCmpTyCon
   , typeConsSymbolTyCon
   , typeUnconsSymbolTyCon
+  , typeCharToNatTyCon
+  , typeNatToCharTyCon
   ) where
 
 import GHC.Prelude
@@ -55,10 +57,13 @@ import GHC.Builtin.Names
                   , typeCharCmpTyFamNameKey
                   , typeConsSymbolTyFamNameKey
                   , typeUnconsSymbolTyFamNameKey
+                  , typeCharToNatTyFamNameKey
+                  , typeNatToCharTyFamNameKey
                   )
 import GHC.Data.FastString
 import Control.Monad ( guard )
 import Data.List  ( isPrefixOf, isSuffixOf )
+import qualified Data.Char as Char
 
 {-
 Note [Type-level literals]
@@ -155,6 +160,8 @@ typeNatTyCons =
   , typeCharCmpTyCon
   , typeConsSymbolTyCon
   , typeUnconsSymbolTyCon
+  , typeCharToNatTyCon
+  , typeNatToCharTyCon
   ]
 
 typeNatAddTyCon :: TyCon
@@ -321,6 +328,43 @@ typeUnconsSymbolTyCon =
       , sfInteractInert = interactInertUnconsSymbol
       }
 
+typeCharToNatTyCon :: TyCon
+typeCharToNatTyCon =
+  mkFamilyTyCon name
+    (mkTemplateAnonTyConBinders [ charTy ])
+    naturalTy
+    Nothing
+    (BuiltInSynFamTyCon ops)
+    Nothing
+    (Injective [True])
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "CharToNat")
+                  typeCharToNatTyFamNameKey typeCharToNatTyCon
+  ops = BuiltInSynFamily
+      { sfMatchFam      = matchFamCharToNat
+      , sfInteractTop   = interactTopCharToNat
+      , sfInteractInert = \_ _ _ _ -> []
+      }
+
+
+typeNatToCharTyCon :: TyCon
+typeNatToCharTyCon =
+  mkFamilyTyCon name
+    (mkTemplateAnonTyConBinders [ naturalTy ])
+    charTy
+    Nothing
+    (BuiltInSynFamTyCon ops)
+    Nothing
+    (Injective [True])
+  where
+  name = mkWiredInTyConName UserSyntax gHC_TYPELITS (fsLit "NatToChar")
+                  typeNatToCharTyFamNameKey typeNatToCharTyCon
+  ops = BuiltInSynFamily
+      { sfMatchFam      = matchFamNatToChar
+      , sfInteractTop   = interactTopNatToChar
+      , sfInteractInert = \_ _ _ _ -> []
+      }
+
 -- Make a unary built-in constructor of kind: Nat -> Nat
 mkTypeNatFunTyCon1 :: Name -> BuiltInSynFamily -> TyCon
 mkTypeNatFunTyCon1 op tcb =
@@ -369,6 +413,8 @@ axAddDef
   , axAppendSymbolDef
   , axConsSymbolDef
   , axUnconsSymbolDef
+  , axCharToNatDef
+  , axNatToCharDef
   , axAdd0L
   , axAdd0R
   , axMul0L
@@ -436,6 +482,14 @@ axUnconsSymbolDef =
     \str -> Just $
       mkPromotedMaybeTy charSymbolPairKind (fmap reifyCharSymbolPairTy (unconsFS str))
 
+axCharToNatDef =
+  mkUnAxiom "CharToNatDef" typeCharToNatTyCon isCharLitTy $
+    \c -> Just $ num (charToInteger c)
+
+axNatToCharDef =
+  mkUnAxiom "NatToCharDef" typeNatToCharTyCon isNumLitTy $
+    \n -> fmap mkCharLitTy (integerToChar n)
+
 axSubDef = mkBinAxiom "SubDef" typeNatSubTyCon isNumLitTy isNumLitTy $
               \x y -> fmap num (minus x y)
 
@@ -740,6 +794,29 @@ matchFamUnconsSymbol [s]
   mbX = isStrLitTy s
 matchFamUnconsSymbol _ = Nothing
 
+matchFamCharToNat :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamCharToNat [c]
+  | Just c' <- isCharLitTy c, n <- charToInteger c'
+  = Just (axCharToNatDef, [c], mkNumLitTy n)
+  | otherwise = Nothing
+matchFamCharToNat _ = Nothing
+
+matchFamNatToChar :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
+matchFamNatToChar [n]
+  | Just n' <- isNumLitTy n, Just c <- integerToChar n'
+  = Just (axNatToCharDef, [n], mkCharLitTy c)
+  | otherwise = Nothing
+matchFamNatToChar _ = Nothing
+
+charToInteger :: Char -> Integer
+charToInteger c = fromIntegral (Char.ord c)
+
+integerToChar :: Integer -> Maybe Char
+integerToChar n | inBounds = Just (Char.chr (fromInteger n))
+  where inBounds = n >= charToInteger minBound &&
+                   n <= charToInteger maxBound
+integerToChar _ = Nothing
+
 {-------------------------------------------------------------------------------
 Interact with axioms
 -------------------------------------------------------------------------------}
@@ -887,6 +964,20 @@ interactTopUnconsSymbol [s] r
 
 interactTopUnconsSymbol _ _ = []
 
+interactTopCharToNat :: [Xi] -> Xi -> [Pair Type]
+interactTopCharToNat [s] r
+  -- (CharToNat c ~ 122) => (c ~ 'z')
+  | Just n <- isNumLitTy r
+  , Just c <- integerToChar n
+  = [ s === mkCharLitTy c ]
+interactTopCharToNat _ _ = []
+
+interactTopNatToChar :: [Xi] -> Xi -> [Pair Type]
+interactTopNatToChar [s] r
+  -- (NatToChar n ~ 'z') => (n ~ 122)
+  | Just c <- isCharLitTy r
+  = [ s === mkNumLitTy (charToInteger c) ]
+interactTopNatToChar _ _ = []
 
 {-------------------------------------------------------------------------------
 Interaction with inerts
diff --git a/docs/users_guide/9.2.1-notes.rst b/docs/users_guide/9.2.1-notes.rst
index 10677b5327..bbd36c1dc3 100644
--- a/docs/users_guide/9.2.1-notes.rst
+++ b/docs/users_guide/9.2.1-notes.rst
@@ -298,6 +298,8 @@ Eventlog
     type family CmpChar (a :: Char) (b :: Char) :: Ordering
     type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol
     type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol)
+    type family CharToNat (c :: Char) :: Natural
+    type family NatToChar (n :: Natural) :: Char
 
   and with the type class ``KnownChar`` (and such additional functions as ``charVal`` and ``charVal'``): ::
 
diff --git a/libraries/base/GHC/TypeLits.hs b/libraries/base/GHC/TypeLits.hs
index b0daf341c8..2dcc28b223 100644
--- a/libraries/base/GHC/TypeLits.hs
+++ b/libraries/base/GHC/TypeLits.hs
@@ -50,6 +50,7 @@ module GHC.TypeLits
   , AppendSymbol
   , N.CmpNat, CmpSymbol, CmpChar
   , ConsSymbol, UnconsSymbol
+  , CharToNat, NatToChar
 
   -- * User-defined type errors
   , TypeError
@@ -240,6 +241,16 @@ type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol
 -- @since 4.16.0.0
 type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol)
 
+-- | Convert a character to its Unicode code point (cf. `Data.Char.ord`)
+--
+-- @since 4.16.0.0
+type family CharToNat (c :: Char) :: N.Nat
+
+-- | Convert a Unicode code point to a character (cf. `Data.Char.chr`)
+--
+-- @since 4.16.0.0
+type family NatToChar (n :: N.Nat) :: Char
+
 --------------------------------------------------------------------------------
 
 -- | We either get evidence that this function was instantiated with the
diff --git a/libraries/base/changelog.md b/libraries/base/changelog.md
index fcf9c0dde6..6cf4561225 100644
--- a/libraries/base/changelog.md
+++ b/libraries/base/changelog.md
@@ -16,6 +16,11 @@
 
   * Add `cmpNat`, `cmpSymbol`, and `cmpChar` to `GHC.TypeNats` and `GHC.TypeLits`.
 
+  * Add `CmpChar`, `ConsSymbol`, `UnconsSymbol`, `CharToNat`, and `NatToChar`
+    type families to `GHC.TypeLits`.
+
+  * Add the `KnownChar` class, `charVal` and `charVal'` to `GHC.TypeLits`.
+
   * Add `Semigroup` and `Monoid` instances for `Data.Functor.Product` and
     `Data.Functor.Compose`.
 
diff --git a/testsuite/tests/ghci/scripts/T9181.stdout b/testsuite/tests/ghci/scripts/T9181.stdout
index 8ca20e265d..89c18c2f6b 100644
--- a/testsuite/tests/ghci/scripts/T9181.stdout
+++ b/testsuite/tests/ghci/scripts/T9181.stdout
@@ -1,6 +1,8 @@
 type GHC.TypeLits.AppendSymbol :: GHC.Types.Symbol
                                   -> GHC.Types.Symbol -> GHC.Types.Symbol
 type family GHC.TypeLits.AppendSymbol a b
+type GHC.TypeLits.CharToNat :: Char -> GHC.Num.Natural.Natural
+type family GHC.TypeLits.CharToNat a
 type GHC.TypeLits.ConsSymbol :: Char
                                 -> GHC.Types.Symbol -> GHC.Types.Symbol
 type family GHC.TypeLits.ConsSymbol a b
@@ -22,6 +24,8 @@ type GHC.TypeLits.KnownSymbol :: GHC.Types.Symbol -> Constraint
 class GHC.TypeLits.KnownSymbol n where
   GHC.TypeLits.symbolSing :: GHC.TypeLits.SSymbol n
   {-# MINIMAL symbolSing #-}
+type GHC.TypeLits.NatToChar :: GHC.Num.Natural.Natural -> Char
+type family GHC.TypeLits.NatToChar a
 type GHC.TypeLits.SomeChar :: *
 data GHC.TypeLits.SomeChar
   = forall (n :: Char).
diff --git a/testsuite/tests/typecheck/should_compile/T19535.hs b/testsuite/tests/typecheck/should_compile/T19535.hs
new file mode 100644
index 0000000000..e05b599b38
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T19535.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module T19535 where
+
+import GHC.TypeNats (natVal)
+import GHC.TypeLits hiding (natVal)
+import Data.Type.Equality
+import Data.Proxy
+
+e1 :: CharToNat 'a' :~: 97
+e1 = Refl
+
+e2 :: NatToChar 120 :~: 'x'
+e2 = Refl
+
+ntc :: forall {n} c. (KnownNat n, NatToChar n ~ c) => Natural
+ntc = natVal (Proxy @n)
+
+ctn :: forall {c} n. (KnownChar c, CharToNat c ~ n) => Char
+ctn = charVal (Proxy @c)
+
+n1 :: Natural
+n1 = ntc @'z'
+
+c1 :: Char
+c1 = ctn @122
+
+ntc_ntc :: forall {n} m. (KnownNat n, NatToChar n ~ NatToChar (m + 1)) => Natural
+ntc_ntc = natVal (Proxy @n)
+
+ctn_ctn :: forall {c} d. (KnownChar c, CharToNat c ~ (CharToNat d + 1)) => Char
+ctn_ctn = charVal (Proxy @c)
+
+n2 :: Natural
+n2 = ntc_ntc @119
+
+c2 :: Char
+c2 = ctn_ctn @'w'
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 6d3505c33d..392f6fb40c 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -777,3 +777,5 @@ test('InlinePatSyn_ExplicitBidiMatcher', [], makefile_test, [])
 test('T18467', normal, compile, [''])
 
 test('T19315', normal, compile, [''])
+
+test('T19535', normal, compile, [''])