ccfffc3efd9b398d8bc723b183eb20b9ee30f328
[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 (<=), type (<=?), type (+), type (*), type (^), type (-)
38 , AppendSymbol
39 , 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 infix 4 <=?, <=
133 infixl 6 +, -
134 infixl 7 *
135 infixr 8 ^
136
137 -- | Comparison of type-level naturals, as a constraint.
138 type x <= y = (x <=? y) ~ 'True
139
140 -- | Comparison of type-level symbols, as a function.
141 --
142 -- @since 4.7.0.0
143 type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
144
145 -- | Comparison of type-level naturals, as a function.
146 --
147 -- @since 4.7.0.0
148 type family CmpNat (m :: Nat) (n :: Nat) :: Ordering
149
150 {- | Comparison of type-level naturals, as a function.
151 NOTE: The functionality for this function should be subsumed
152 by 'CmpNat', so this might go away in the future.
153 Please let us know, if you encounter discrepancies between the two. -}
154 type family (m :: Nat) <=? (n :: Nat) :: Bool
155
156 -- | Addition of type-level naturals.
157 type family (m :: Nat) + (n :: Nat) :: Nat
158
159 -- | Multiplication of type-level naturals.
160 type family (m :: Nat) * (n :: Nat) :: Nat
161
162 -- | Exponentiation of type-level naturals.
163 type family (m :: Nat) ^ (n :: Nat) :: Nat
164
165 -- | Subtraction of type-level naturals.
166 --
167 -- @since 4.7.0.0
168 type family (m :: Nat) - (n :: Nat) :: Nat
169
170 -- | Concatenation of type-level symbols.
171 --
172 -- @since 4.10.0.0
173 type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
174
175 -- | A description of a custom type error.
176 data {-kind-} ErrorMessage = Text Symbol
177 -- ^ Show the text as is.
178
179 | forall t. ShowType t
180 -- ^ Pretty print the type.
181 -- @ShowType :: k -> ErrorMessage@
182
183 | ErrorMessage :<>: ErrorMessage
184 -- ^ Put two pieces of error message next
185 -- to each other.
186
187 | ErrorMessage :$$: ErrorMessage
188 -- ^ Stack two pieces of error message on top
189 -- of each other.
190
191 infixl 5 :$$:
192 infixl 6 :<>:
193
194 -- | The type-level equivalent of 'error'.
195 --
196 -- The polymorphic kind of this type allows it to be used in several settings.
197 -- For instance, it can be used as a constraint, e.g. to provide a better error
198 -- message for a non-existent instance,
199 --
200 -- @
201 -- -- in a context
202 -- instance TypeError (Text "Cannot 'Show' functions." :$$:
203 -- Text "Perhaps there is a missing argument?")
204 -- => Show (a -> b) where
205 -- showsPrec = error "unreachable"
206 -- @
207 --
208 -- It can also be placed on the right-hand side of a type-level function
209 -- to provide an error for an invalid case,
210 --
211 -- @
212 -- type family ByteSize x where
213 -- ByteSize Word16 = 2
214 -- ByteSize Word8 = 1
215 -- ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
216 -- Text " is not exportable.")
217 -- @
218 --
219 -- @since 4.9.0.0
220 type family TypeError (a :: ErrorMessage) :: b where
221
222
223 --------------------------------------------------------------------------------
224
225 -- | We either get evidence that this function was instantiated with the
226 -- same type-level symbols, or 'Nothing'.
227 --
228 -- @since 4.7.0.0
229 sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
230 Proxy a -> Proxy b -> Maybe (a :~: b)
231 sameSymbol x y
232 | symbolVal x == symbolVal y = Just (unsafeCoerce Refl)
233 | otherwise = Nothing
234
235 --------------------------------------------------------------------------------
236 -- PRIVATE:
237
238 newtype SSymbol (s :: Symbol) = SSymbol String
239
240 data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
241
242 -- See Note [magicDictId magic] in "basicType/MkId.hs"
243 withSSymbol :: (KnownSymbol a => Proxy a -> b)
244 -> SSymbol a -> Proxy a -> b
245 withSSymbol f x y = magicDict (WrapS f) x y