Add a `NOINLINE` pragma on `someNatVal` (#16586)
[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 NoImplicitPrelude #-}
13 {-# LANGUAGE MagicHash #-}
14 {-# LANGUAGE PolyKinds #-}
15
16 {-| This module is an internal GHC module. It declares the constants used
17 in the implementation of type-level natural numbers. The programmer interface
18 for working with type-level naturals should be defined in a separate library.
19
20 @since 4.6.0.0
21 -}
22
23 module GHC.TypeLits
24 ( -- * Kinds
25 Nat, Symbol -- Both declared in GHC.Types in package ghc-prim
26
27 -- * Linking type and value level
28 , N.KnownNat, natVal, natVal'
29 , KnownSymbol, symbolVal, symbolVal'
30 , N.SomeNat(..), SomeSymbol(..)
31 , someNatVal, someSymbolVal
32 , N.sameNat, sameSymbol
33
34
35 -- * Functions on type literals
36 , type (N.<=), type (N.<=?), type (N.+), type (N.*), type (N.^), type (N.-)
37 , type N.Div, type N.Mod, type N.Log2
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(..), 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((:~:)(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 {-# NOINLINE someSymbolVal #-}
109 -- For details see Note [NOINLINE someNatVal] in "GHC.TypeNats"
110 -- The issue described there applies to `someSymbolVal` as well.
111
112 -- | @since 4.7.0.0
113 instance Eq SomeSymbol where
114 SomeSymbol x == SomeSymbol y = symbolVal x == symbolVal y
115
116 -- | @since 4.7.0.0
117 instance Ord SomeSymbol where
118 compare (SomeSymbol x) (SomeSymbol y) = compare (symbolVal x) (symbolVal y)
119
120 -- | @since 4.7.0.0
121 instance Show SomeSymbol where
122 showsPrec p (SomeSymbol x) = showsPrec p (symbolVal x)
123
124 -- | @since 4.7.0.0
125 instance Read SomeSymbol where
126 readsPrec p xs = [ (someSymbolVal a, ys) | (a,ys) <- readsPrec p xs ]
127
128 --------------------------------------------------------------------------------
129
130 -- | Comparison of type-level symbols, as a function.
131 --
132 -- @since 4.7.0.0
133 type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
134
135 -- | Concatenation of type-level symbols.
136 --
137 -- @since 4.10.0.0
138 type family AppendSymbol (m ::Symbol) (n :: Symbol) :: Symbol
139
140 -- | A description of a custom type error.
141 data {-kind-} ErrorMessage = Text Symbol
142 -- ^ Show the text as is.
143
144 | forall t. ShowType t
145 -- ^ Pretty print the type.
146 -- @ShowType :: k -> ErrorMessage@
147
148 | ErrorMessage :<>: ErrorMessage
149 -- ^ Put two pieces of error message next
150 -- to each other.
151
152 | ErrorMessage :$$: ErrorMessage
153 -- ^ Stack two pieces of error message on top
154 -- of each other.
155
156 infixl 5 :$$:
157 infixl 6 :<>:
158
159 -- | The type-level equivalent of 'Prelude.error'.
160 --
161 -- The polymorphic kind of this type allows it to be used in several settings.
162 -- For instance, it can be used as a constraint, e.g. to provide a better error
163 -- message for a non-existent instance,
164 --
165 -- @
166 -- -- in a context
167 -- instance TypeError (Text "Cannot 'Show' functions." :$$:
168 -- Text "Perhaps there is a missing argument?")
169 -- => Show (a -> b) where
170 -- showsPrec = error "unreachable"
171 -- @
172 --
173 -- It can also be placed on the right-hand side of a type-level function
174 -- to provide an error for an invalid case,
175 --
176 -- @
177 -- type family ByteSize x where
178 -- ByteSize Word16 = 2
179 -- ByteSize Word8 = 1
180 -- ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
181 -- Text " is not exportable.")
182 -- @
183 --
184 -- @since 4.9.0.0
185 type family TypeError (a :: ErrorMessage) :: b where
186
187
188 --------------------------------------------------------------------------------
189
190 -- | We either get evidence that this function was instantiated with the
191 -- same type-level symbols, or 'Nothing'.
192 --
193 -- @since 4.7.0.0
194 sameSymbol :: (KnownSymbol a, KnownSymbol b) =>
195 Proxy a -> Proxy b -> Maybe (a :~: b)
196 sameSymbol x y
197 | symbolVal x == symbolVal y = Just (unsafeCoerce Refl)
198 | otherwise = Nothing
199
200 --------------------------------------------------------------------------------
201 -- PRIVATE:
202
203 newtype SSymbol (s :: Symbol) = SSymbol String
204
205 data WrapS a b = WrapS (KnownSymbol a => Proxy a -> b)
206
207 -- See Note [magicDictId magic] in "basicType/MkId.hs"
208 withSSymbol :: (KnownSymbol a => Proxy a -> b)
209 -> SSymbol a -> Proxy a -> b
210 withSSymbol f x y = magicDict (WrapS f) x y