Reexport CmpNat and friends (defined in GHC.TypeNats) from GHC.TypeLits
[ghc.git] / libraries / base / GHC / TypeLits.hs
1 {-# LANGUAGE Trustworthy #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE KindSignatures #-}
4 {-# LANGUAGE TypeFamilies #-}
5 {-# LANGUAGE TypeOperators #-}
6 {-# LANGUAGE FlexibleInstances #-}
7 {-# LANGUAGE FlexibleContexts #-}
8 {-# LANGUAGE ScopedTypeVariables #-}
9 {-# LANGUAGE ConstraintKinds #-}
10 {-# LANGUAGE ExistentialQuantification #-}
11 {-# LANGUAGE RankNTypes #-}
12 {-# LANGUAGE UndecidableInstances #-} -- for compiling instances of (==)
13 {-# LANGUAGE NoImplicitPrelude #-}
14 {-# LANGUAGE MagicHash #-}
15 {-# LANGUAGE PolyKinds #-}
16
17 {-| This module is an internal GHC module. It declares the constants used
18 in the implementation of type-level natural numbers. The programmer interface
19 for working with type-level naturals should be defined in a separate library.
20
21 @since 4.6.0.0
22 -}
23
24 module GHC.TypeLits
25 ( -- * Kinds
26 Nat, Symbol -- Both declared in GHC.Types in package ghc-prim
27
28 -- * Linking type and value level
29 , N.KnownNat, natVal, natVal'
30 , KnownSymbol, symbolVal, symbolVal'
31 , N.SomeNat(..), SomeSymbol(..)
32 , someNatVal, someSymbolVal
33 , N.sameNat, sameSymbol
34
35
36 -- * Functions on type literals
37 , type (N.<=), type (N.<=?), type (N.+), type (N.*), type (N.^), type (N.-)
38 , AppendSymbol
39 , N.CmpNat, CmpSymbol
40
41 -- * User-defined type errors
42 , TypeError
43 , ErrorMessage(..)
44
45 ) where
46
47 import GHC.Base(Eq(..), Ord(..), Bool(True,False), Ordering(..), otherwise)
48 import GHC.Types( Nat, Symbol )
49 import GHC.Num(Integer, fromInteger)
50 import GHC.Base(String)
51 import GHC.Show(Show(..))
52 import GHC.Read(Read(..))
53 import GHC.Real(toInteger)
54 import GHC.Prim(magicDict, Proxy#)
55 import Data.Maybe(Maybe(..))
56 import Data.Proxy (Proxy(..))
57 import Data.Type.Equality(type (==), (:~:)(Refl))
58 import Unsafe.Coerce(unsafeCoerce)
59
60 import GHC.TypeNats (KnownNat)
61 import qualified GHC.TypeNats as N
62
63 --------------------------------------------------------------------------------
64
65 -- | This class gives the string associated with a type-level symbol.
66 -- There are instances of the class for every concrete literal: "hello", etc.
67 --
68 -- @since 4.7.0.0
69 class KnownSymbol (n :: Symbol) where
70 symbolSing :: SSymbol n
71
72 -- | @since 4.7.0.0
73 natVal :: forall n proxy. KnownNat n => proxy n -> Integer
74 natVal p = toInteger (N.natVal p)
75
76 -- | @since 4.7.0.0
77 symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
78 symbolVal _ = case symbolSing :: SSymbol n of
79 SSymbol x -> x
80
81 -- | @since 4.8.0.0
82 natVal' :: forall n. KnownNat n => Proxy# n -> Integer
83 natVal' p = toInteger (N.natVal' p)
84
85 -- | @since 4.8.0.0
86 symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
87 symbolVal' _ = case symbolSing :: SSymbol n of
88 SSymbol x -> x
89
90
91 -- | This type represents unknown type-level symbols.
92 data SomeSymbol = forall n. KnownSymbol n => SomeSymbol (Proxy n)
93 -- ^ @since 4.7.0.0
94
95 -- | Convert an integer into an unknown type-level natural.
96 --
97 -- @since 4.7.0.0
98 someNatVal :: Integer -> Maybe N.SomeNat
99 someNatVal n
100 | n >= 0 = Just (N.someNatVal (fromInteger n))
101 | otherwise = Nothing
102
103 -- | Convert a string into an unknown type-level symbol.
104 --
105 -- @since 4.7.0.0
106 someSymbolVal :: String -> SomeSymbol
107 someSymbolVal n = withSSymbol SomeSymbol (SSymbol n) Proxy
108
109 -- | @since 4.7.0.0
110 instance Eq SomeSymbol where
111 SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y
112
113 -- | @since 4.7.0.0
114 instance Ord SomeSymbol where
115 compare (SomeSymbol x) (SomeSymbol y) = compare (symbolVal x) (symbolVal y)
116
117 -- | @since 4.7.0.0
118 instance Show SomeSymbol where
119 showsPrec p (SomeSymbol x) = showsPrec p (symbolVal x)
120
121 -- | @since 4.7.0.0
122 instance Read SomeSymbol where
123 readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
124
125 type family EqSymbol (a :: Symbol) (b :: Symbol) where
126 EqSymbol a a = 'True
127 EqSymbol a b = 'False
128 type instance a == b = EqSymbol a b
129
130 --------------------------------------------------------------------------------
131
132 -- | Comparison of type-level symbols, as a function.
133 --
134 -- @since 4.7.0.0
135 type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
136
137 -- | Concatenation of type-level symbols.
138 --
139 -- @since 4.10.0.0
140 type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
141
142 -- | A description of a custom type error.
143 data {-kind-} ErrorMessage = Text Symbol
144 -- ^ Show the text as is.
145
146 | forall t. ShowType t
147 -- ^ Pretty print the type.
148 -- @ShowType :: k -> ErrorMessage@
149
150 | ErrorMessage :<>: ErrorMessage
151 -- ^ Put two pieces of error message next
152 -- to each other.
153
154 | ErrorMessage :$$: ErrorMessage
155 -- ^ Stack two pieces of error message on top
156 -- of each other.
157
158 infixl 5 :$$:
159 infixl 6 :<>:
160
161 -- | The type-level equivalent of 'error'.
162 --
163 -- The polymorphic kind of this type allows it to be used in several settings.
164 -- For instance, it can be used as a constraint, e.g. to provide a better error
165 -- message for a non-existent instance,
166 --
167 -- @
168 -- -- in a context
169 -- instance TypeError (Text "Cannot 'Show' functions." :$$:
170 -- Text "Perhaps there is a missing argument?")
171 -- => Show (a -> b) where
172 -- showsPrec = error "unreachable"
173 -- @
174 --
175 -- It can also be placed on the right-hand side of a type-level function
176 -- to provide an error for an invalid case,
177 --
178 -- @
179 -- type family ByteSize x where
180 -- ByteSize Word16 = 2
181 -- ByteSize Word8 = 1
182 -- ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
183 -- Text " is not exportable.")
184 -- @
185 --
186 -- @since 4.9.0.0
187 type family TypeError (a :: ErrorMessage) :: b where
188
189
190 --------------------------------------------------------------------------------
191
192 -- | We either get evidence that this function was instantiated with the
193 -- same type-level symbols, or 'Nothing'.
194 --
195 -- @since 4.7.0.0
196 sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
197 Proxy a -> Proxy b -> Maybe (a :~: b)
198 sameSymbol x y
199 | symbolVal x == symbolVal y = Just (unsafeCoerce Refl)
200 | otherwise = Nothing
201
202 --------------------------------------------------------------------------------
203 -- PRIVATE:
204
205 newtype SSymbol (s :: Symbol) = SSymbol String
206
207 data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
208
209 -- See Note [magicDictId magic] in "basicType/MkId.hs"
210 withSSymbol :: (KnownSymbol a => Proxy a -> b)
211 -> SSymbol a -> Proxy a -> b
212 withSSymbol f x y = magicDict (WrapS f) x y