summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--compiler/GHC/Builtin/Names.hs63
-rw-r--r--compiler/GHC/Builtin/Types/Literals.hs91
-rw-r--r--docs/users_guide/9.2.1-notes.rst2
-rw-r--r--libraries/base/GHC/TypeLits.hs11
-rw-r--r--libraries/base/changelog.md5
-rw-r--r--testsuite/tests/ghci/scripts/T9181.stdout4
-rw-r--r--testsuite/tests/typecheck/should_compile/T19535.hs44
-rw-r--r--testsuite/tests/typecheck/should_compile/all.T2
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, [''])