Add a `NOINLINE` pragma on `someNatVal` (#16586)
[ghc.git] / libraries / base / GHC / TypeNats.hs
1 {-# LANGUAGE Trustworthy #-}
2 {-# LANGUAGE DataKinds #-}
3 {-# LANGUAGE KindSignatures #-}
4 {-# LANGUAGE TypeFamilies #-}
5 {-# LANGUAGE TypeOperators #-}
6 {-# LANGUAGE NoStarIsType #-}
7 {-# LANGUAGE FlexibleInstances #-}
8 {-# LANGUAGE FlexibleContexts #-}
9 {-# LANGUAGE ScopedTypeVariables #-}
10 {-# LANGUAGE ConstraintKinds #-}
11 {-# LANGUAGE ExistentialQuantification #-}
12 {-# LANGUAGE RankNTypes #-}
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.10.0.0
22 -}
23
24 module GHC.TypeNats
25 ( -- * Nat Kind
26 Nat -- declared in GHC.Types in package ghc-prim
27
28 -- * Linking type and value level
29 , KnownNat, natVal, natVal'
30 , SomeNat(..)
31 , someNatVal
32 , sameNat
33
34 -- * Functions on type literals
35 , type (<=), type (<=?), type (+), type (*), type (^), type (-)
36 , CmpNat
37 , Div, Mod, Log2
38
39 ) where
40
41 import GHC.Base(Eq(..), Ord(..), Bool(True), Ordering(..), otherwise)
42 import GHC.Types( Nat )
43 import GHC.Natural(Natural)
44 import GHC.Show(Show(..))
45 import GHC.Read(Read(..))
46 import GHC.Prim(magicDict, Proxy#)
47 import Data.Maybe(Maybe(..))
48 import Data.Proxy (Proxy(..))
49 import Data.Type.Equality((:~:)(Refl))
50 import Unsafe.Coerce(unsafeCoerce)
51
52 --------------------------------------------------------------------------------
53
54 -- | This class gives the integer associated with a type-level natural.
55 -- There are instances of the class for every concrete literal: 0, 1, 2, etc.
56 --
57 -- @since 4.7.0.0
58 class KnownNat (n :: Nat) where
59 natSing :: SNat n
60
61 -- | @since 4.10.0.0
62 natVal :: forall n proxy. KnownNat n => proxy n -> Natural
63 natVal _ = case natSing :: SNat n of
64 SNat x -> x
65
66 -- | @since 4.10.0.0
67 natVal' :: forall n. KnownNat n => Proxy# n -> Natural
68 natVal' _ = case natSing :: SNat n of
69 SNat x -> x
70
71 -- | This type represents unknown type-level natural numbers.
72 --
73 -- @since 4.10.0.0
74 data SomeNat = forall n. KnownNat n => SomeNat (Proxy n)
75
76 -- | Convert an integer into an unknown type-level natural.
77 --
78 -- @since 4.10.0.0
79 someNatVal :: Natural -> SomeNat
80 someNatVal n = withSNat SomeNat (SNat n) Proxy
81 {-# NOINLINE someNatVal #-} -- See Note [NOINLINE someNatVal]
82
83 {- Note [NOINLINE someNatVal]
84
85 `someNatVal` converts a natural number to an existentially quantified
86 dictionary for `KnowNat` (aka `SomeNat`). The existential quantification
87 is very important, as it captures the fact that we don't know the type
88 statically, although we do know that it exists. Because this type is
89 fully opaque, we should never be able to prove that it matches anything else.
90 This is why coherence should still hold: we can manufacture a `KnownNat k`
91 dictionary, but it can never be confused with a `KnownNat 33` dictionary,
92 because we should never be able to prove that `k ~ 33`.
93
94 But how to implement `someNatVal`? We can't quite implement it "honestly"
95 because `SomeNat` needs to "hide" the type of the newly created dictionary,
96 but we don't know what the actual type is! If `someNatVal` was built into
97 the language, then we could manufacture a new skolem constant,
98 which should behave correctly.
99
100 Since extra language constructors have additional maintenance costs,
101 we use a trick to implement `someNatVal` in the library. The idea is that
102 instead of generating a "fresh" type for each use of `someNatVal`, we simply
103 use GHC's placeholder type `Any` (of kind `Nat`). So, the elaborated
104 version of the code is:
105
106 someNatVal n = withSNat @T (SomeNat @T) (SNat @T n) (Proxy @T)
107 where type T = Any Nat
108
109 After inlining and simplification, this ends up looking something like this:
110
111 someNatVal n = SomeNat @T (KnownNat @T (SNat @T n)) (Proxy @T)
112 where type T = Any Nat
113
114 `KnownNat` is the constructor for dictionaries for the class `KnownNat`.
115 See Note [magicDictId magic] in "basicType/MkId.hs" for details on how
116 we actually construct the dictionry.
117
118 Note that using `Any Nat` is not really correct, as multilple calls to
119 `someNatVal` would violate coherence:
120
121 type T = Any Nat
122
123 x = SomeNat @T (KnownNat @T (SNat @T 1)) (Proxy @T)
124 y = SomeNat @T (KnownNat @T (SNat @T 2)) (Proxy @T)
125
126 Note that now the code has two dictionaries with the same type, `KnownNat Any`,
127 but they have different implementations, namely `SNat 1` and `SNat 2`. This
128 is not good, as GHC assumes coherence, and it is free to interchange
129 dictionaries of the same type, but in this case this would produce an incorrect
130 result. See #16586 for examples of this happening.
131
132 We can avoid this problem by making the definition of `someNatVal` opaque
133 and we do this by using a `NOINLINE` pragma. This restores coherence, because
134 GHC can only inspect the result of `someNatVal` by pattern matching on the
135 existential, which would generate a new type. This restores correctness,
136 at the cost of having a little more allocation for the `SomeNat` constructors.
137 -}
138
139
140
141 -- | @since 4.7.0.0
142 instance Eq SomeNat where
143 SomeNat x == SomeNat y = natVal x == natVal y
144
145 -- | @since 4.7.0.0
146 instance Ord SomeNat where
147 compare (SomeNat x) (SomeNat y) = compare (natVal x) (natVal y)
148
149 -- | @since 4.7.0.0
150 instance Show SomeNat where
151 showsPrec p (SomeNat x) = showsPrec p (natVal x)
152
153 -- | @since 4.7.0.0
154 instance Read SomeNat where
155 readsPrec p xs = do (a,ys) <- readsPrec p xs
156 [(someNatVal a, ys)]
157
158 --------------------------------------------------------------------------------
159
160 infix 4 <=?, <=
161 infixl 6 +, -
162 infixl 7 *, `Div`, `Mod`
163 infixr 8 ^
164
165 -- | Comparison of type-level naturals, as a constraint.
166 --
167 -- @since 4.7.0.0
168 type x <= y = (x <=? y) ~ 'True
169
170 -- | Comparison of type-level naturals, as a function.
171 --
172 -- @since 4.7.0.0
173 type family CmpNat (m :: Nat) (n :: Nat) :: Ordering
174
175 {- | Comparison of type-level naturals, as a function.
176 NOTE: The functionality for this function should be subsumed
177 by 'CmpNat', so this might go away in the future.
178 Please let us know, if you encounter discrepancies between the two. -}
179 type family (m :: Nat) <=? (n :: Nat) :: Bool
180
181 -- | Addition of type-level naturals.
182 --
183 -- @since 4.7.0.0
184 type family (m :: Nat) + (n :: Nat) :: Nat
185
186 -- | Multiplication of type-level naturals.
187 --
188 -- @since 4.7.0.0
189 type family (m :: Nat) * (n :: Nat) :: Nat
190
191 -- | Exponentiation of type-level naturals.
192 --
193 -- @since 4.7.0.0
194 type family (m :: Nat) ^ (n :: Nat) :: Nat
195
196 -- | Subtraction of type-level naturals.
197 --
198 -- @since 4.7.0.0
199 type family (m :: Nat) - (n :: Nat) :: Nat
200
201 -- | Division (round down) of natural numbers.
202 -- @Div x 0@ is undefined (i.e., it cannot be reduced).
203 --
204 -- @since 4.11.0.0
205 type family Div (m :: Nat) (n :: Nat) :: Nat
206
207 -- | Modulus of natural numbers.
208 -- @Mod x 0@ is undefined (i.e., it cannot be reduced).
209 --
210 -- @since 4.11.0.0
211 type family Mod (m :: Nat) (n :: Nat) :: Nat
212
213 -- | Log base 2 (round down) of natural numbers.
214 -- @Log 0@ is undefined (i.e., it cannot be reduced).
215 --
216 -- @since 4.11.0.0
217 type family Log2 (m :: Nat) :: Nat
218
219 --------------------------------------------------------------------------------
220
221 -- | We either get evidence that this function was instantiated with the
222 -- same type-level numbers, or 'Nothing'.
223 --
224 -- @since 4.7.0.0
225 sameNat :: (KnownNat a, KnownNat b) =>
226 Proxy a -> Proxy b -> Maybe (a :~: b)
227 sameNat x y
228 | natVal x == natVal y = Just (unsafeCoerce Refl)
229 | otherwise = Nothing
230
231 --------------------------------------------------------------------------------
232 -- PRIVATE:
233
234 newtype SNat (n :: Nat) = SNat Natural
235
236 data WrapN a b = WrapN (KnownNat a => Proxy a -> b)
237
238 -- See Note [magicDictId magic] in "basicType/MkId.hs"
239 withSNat :: (KnownNat a => Proxy a -> b)
240 -> SNat a -> Proxy a -> b
241 withSNat f x y = magicDict (WrapN f) x y