diff options
| -rw-r--r-- | compiler/GHC/Builtin/Names.hs | 63 | ||||
| -rw-r--r-- | compiler/GHC/Builtin/Types/Literals.hs | 91 | ||||
| -rw-r--r-- | docs/users_guide/9.2.1-notes.rst | 2 | ||||
| -rw-r--r-- | libraries/base/GHC/TypeLits.hs | 11 | ||||
| -rw-r--r-- | libraries/base/changelog.md | 5 | ||||
| -rw-r--r-- | testsuite/tests/ghci/scripts/T9181.stdout | 4 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/T19535.hs | 44 | ||||
| -rw-r--r-- | testsuite/tests/typecheck/should_compile/all.T | 2 |
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, ['']) |