Replace hand-written Bounded instances with derived ones
[ghc.git] / libraries / base / Data / Type / Equality.hs
1 {-# LANGUAGE DeriveGeneric #-}
2 {-# LANGUAGE TypeOperators #-}
3 {-# LANGUAGE GADTs #-}
4 {-# LANGUAGE FlexibleInstances #-}
5 {-# LANGUAGE StandaloneDeriving #-}
6 {-# LANGUAGE NoImplicitPrelude #-}
7 {-# LANGUAGE PolyKinds #-}
8 {-# LANGUAGE RankNTypes #-}
9 {-# LANGUAGE DataKinds #-}
10 {-# LANGUAGE TypeFamilies #-}
11 {-# LANGUAGE UndecidableInstances #-}
12 {-# LANGUAGE ExplicitNamespaces #-}
13 {-# LANGUAGE MultiParamTypeClasses #-}
14 {-# LANGUAGE FunctionalDependencies #-}
15 {-# LANGUAGE Trustworthy #-}
16
17 -----------------------------------------------------------------------------
18 -- |
19 -- Module : Data.Type.Equality
20 -- License : BSD-style (see the LICENSE file in the distribution)
21 --
22 -- Maintainer : libraries@haskell.org
23 -- Stability : experimental
24 -- Portability : not portable
25 --
26 -- Definition of propositional equality @(:~:)@. Pattern-matching on a variable
27 -- of type @(a :~: b)@ produces a proof that @a ~ b@.
28 --
29 -- @since 4.7.0.0
30 -----------------------------------------------------------------------------
31
32
33
34 module Data.Type.Equality (
35 -- * The equality types
36 (:~:)(..), type (~~),
37
38 -- * Working with equality
39 sym, trans, castWith, gcastWith, apply, inner, outer,
40
41 -- * Inferring equality from other types
42 TestEquality(..),
43
44 -- * Boolean type-level equality
45 type (==)
46 ) where
47
48 import Data.Maybe
49 import GHC.Enum
50 import GHC.Show
51 import GHC.Read
52 import GHC.Base
53 import Data.Type.Bool
54
55 -- | Lifted, homogeneous equality. By lifted, we mean that it can be
56 -- bogus (deferred type error). By homogeneous, the two types @a@
57 -- and @b@ must have the same kind.
58 class a ~~ b => (a :: k) ~ (b :: k)
59 -- See Note [The equality types story] in TysPrim
60 -- NB: All this class does is to wrap its superclass, which is
61 -- the "real", inhomogeneous equality; this is needed when
62 -- we have a Given (a~b), and we want to prove things from it
63 -- NB: Not exported, as (~) is magical syntax. That's also why there's
64 -- no fixity.
65
66 -- It's tempting to put functional dependencies on (~), but it's not
67 -- necessary because the functional-dependency coverage check looks
68 -- through superclasses, and (~#) is handled in that check.
69
70 instance {-# INCOHERENT #-} a ~~ b => a ~ b
71 -- See Note [The equality types story] in TysPrim
72 -- If we have a Wanted (t1 ~ t2), we want to immediately
73 -- simplify it to (t1 ~~ t2) and solve that instead
74 --
75 -- INCOHERENT because we want to use this instance eagerly, even when
76 -- the tyvars are partially unknown.
77
78 infix 4 :~:
79
80 -- | Propositional equality. If @a :~: b@ is inhabited by some terminating
81 -- value, then the type @a@ is the same as the type @b@. To use this equality
82 -- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;
83 -- in the body of the pattern-match, the compiler knows that @a ~ b@.
84 --
85 -- @since 4.7.0.0
86 data a :~: b where -- See Note [The equality types story] in TysPrim
87 Refl :: a :~: a
88
89 -- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
90 -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
91 -- for 'type-eq'
92
93 -- | Symmetry of equality
94 sym :: (a :~: b) -> (b :~: a)
95 sym Refl = Refl
96
97 -- | Transitivity of equality
98 trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
99 trans Refl Refl = Refl
100
101 -- | Type-safe cast, using propositional equality
102 castWith :: (a :~: b) -> a -> b
103 castWith Refl x = x
104
105 -- | Generalized form of type-safe cast using propositional equality
106 gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
107 gcastWith Refl x = x
108
109 -- | Apply one equality to another, respectively
110 apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)
111 apply Refl Refl = Refl
112
113 -- | Extract equality of the arguments from an equality of a applied types
114 inner :: (f a :~: g b) -> (a :~: b)
115 inner Refl = Refl
116
117 -- | Extract equality of type constructors from an equality of applied types
118 outer :: (f a :~: g b) -> (f :~: g)
119 outer Refl = Refl
120
121 deriving instance Eq (a :~: b)
122 deriving instance Show (a :~: b)
123 deriving instance Ord (a :~: b)
124
125 instance a ~ b => Read (a :~: b) where
126 readsPrec d = readParen (d > 10) (\r -> [(Refl, s) | ("Refl",s) <- lex r ])
127
128 instance a ~ b => Enum (a :~: b) where
129 toEnum 0 = Refl
130 toEnum _ = errorWithoutStackTrace "Data.Type.Equality.toEnum: bad argument"
131
132 fromEnum Refl = 0
133
134 deriving instance a ~ b => Bounded (a :~: b)
135
136 -- | This class contains types where you can learn the equality of two types
137 -- from information contained in /terms/. Typically, only singleton types should
138 -- inhabit this class.
139 class TestEquality f where
140 -- | Conditionally prove the equality of @a@ and @b@.
141 testEquality :: f a -> f b -> Maybe (a :~: b)
142
143 instance TestEquality ((:~:) a) where
144 testEquality Refl Refl = Just Refl
145
146 -- | A type family to compute Boolean equality. Instances are provided
147 -- only for /open/ kinds, such as @*@ and function kinds. Instances are
148 -- also provided for datatypes exported from base. A poly-kinded instance
149 -- is /not/ provided, as a recursive definition for algebraic kinds is
150 -- generally more useful.
151 type family (a :: k) == (b :: k) :: Bool
152 infix 4 ==
153
154 {-
155 This comment explains more about why a poly-kinded instance for (==) is
156 not provided. To be concrete, here would be the poly-kinded instance:
157
158 type family EqPoly (a :: k) (b :: k) where
159 EqPoly a a = True
160 EqPoly a b = False
161 type instance (a :: k) == (b :: k) = EqPoly a b
162
163 Note that this overlaps with every other instance -- if this were defined,
164 it would be the only instance for (==).
165
166 Now, consider
167 data Nat = Zero | Succ Nat
168
169 Suppose I want
170 foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
171 foo = Refl
172
173 This would not type-check with the poly-kinded instance. `Succ n == Succ m`
174 quickly becomes `EqPoly (Succ n) (Succ m)` but then is stuck. We don't know
175 enough about `n` and `m` to reduce further.
176
177 On the other hand, consider this:
178
179 type family EqNat (a :: Nat) (b :: Nat) where
180 EqNat Zero Zero = True
181 EqNat (Succ n) (Succ m) = EqNat n m
182 EqNat n m = False
183 type instance (a :: Nat) == (b :: Nat) = EqNat a b
184
185 With this instance, `foo` type-checks fine. `Succ n == Succ m` becomes `EqNat
186 (Succ n) (Succ m)` which becomes `EqNat n m`. Thus, we can conclude `(n == m)
187 ~ True` as desired.
188
189 So, the Nat-specific instance allows strictly more reductions, and is thus
190 preferable to the poly-kinded instance. But, if we introduce the poly-kinded
191 instance, we are barred from writing the Nat-specific instance, due to
192 overlap.
193
194 Even better than the current instance for * would be one that does this sort
195 of recursion for all datatypes, something like this:
196
197 type family EqStar (a :: *) (b :: *) where
198 EqStar Bool Bool = True
199 EqStar (a,b) (c,d) = a == c && b == d
200 EqStar (Maybe a) (Maybe b) = a == b
201 ...
202 EqStar a b = False
203
204 The problem is the (...) is extensible -- we would want to add new cases for
205 all datatypes in scope. This is not currently possible for closed type
206 families.
207 -}
208
209 -- all of the following closed type families are local to this module
210 type family EqStar (a :: *) (b :: *) where
211 EqStar a a = 'True
212 EqStar a b = 'False
213
214 -- This looks dangerous, but it isn't. This allows == to be defined
215 -- over arbitrary type constructors.
216 type family EqArrow (a :: k1 -> k2) (b :: k1 -> k2) where
217 EqArrow a a = 'True
218 EqArrow a b = 'False
219
220 type family EqBool a b where
221 EqBool 'True 'True = 'True
222 EqBool 'False 'False = 'True
223 EqBool a b = 'False
224
225 type family EqOrdering a b where
226 EqOrdering 'LT 'LT = 'True
227 EqOrdering 'EQ 'EQ = 'True
228 EqOrdering 'GT 'GT = 'True
229 EqOrdering a b = 'False
230
231 type EqUnit (a :: ()) (b :: ()) = 'True
232
233 type family EqList a b where
234 EqList '[] '[] = 'True
235 EqList (h1 ': t1) (h2 ': t2) = (h1 == h2) && (t1 == t2)
236 EqList a b = 'False
237
238 type family EqMaybe a b where
239 EqMaybe 'Nothing 'Nothing = 'True
240 EqMaybe ('Just x) ('Just y) = x == y
241 EqMaybe a b = 'False
242
243 type family Eq2 a b where
244 Eq2 '(a1, b1) '(a2, b2) = a1 == a2 && b1 == b2
245
246 type family Eq3 a b where
247 Eq3 '(a1, b1, c1) '(a2, b2, c2) = a1 == a2 && b1 == b2 && c1 == c2
248
249 type family Eq4 a b where
250 Eq4 '(a1, b1, c1, d1) '(a2, b2, c2, d2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2
251
252 type family Eq5 a b where
253 Eq5 '(a1, b1, c1, d1, e1) '(a2, b2, c2, d2, e2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2
254
255 type family Eq6 a b where
256 Eq6 '(a1, b1, c1, d1, e1, f1) '(a2, b2, c2, d2, e2, f2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2
257
258 type family Eq7 a b where
259 Eq7 '(a1, b1, c1, d1, e1, f1, g1) '(a2, b2, c2, d2, e2, f2, g2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2
260
261 type family Eq8 a b where
262 Eq8 '(a1, b1, c1, d1, e1, f1, g1, h1) '(a2, b2, c2, d2, e2, f2, g2, h2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2
263
264 type family Eq9 a b where
265 Eq9 '(a1, b1, c1, d1, e1, f1, g1, h1, i1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2
266
267 type family Eq10 a b where
268 Eq10 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2
269
270 type family Eq11 a b where
271 Eq11 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2
272
273 type family Eq12 a b where
274 Eq12 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2
275
276 type family Eq13 a b where
277 Eq13 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2
278
279 type family Eq14 a b where
280 Eq14 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2
281
282 type family Eq15 a b where
283 Eq15 '(a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1) '(a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2) = a1 == a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 && f1 == f2 && g1 == g2 && h1 == h2 && i1 == i2 && j1 == j2 && k1 == k2 && l1 == l2 && m1 == m2 && n1 == n2 && o1 == o2
284
285 -- these all look to be overlapping, but they are differentiated by their kinds
286 type instance a == b = EqStar a b
287 type instance a == b = EqArrow a b
288 type instance a == b = EqBool a b
289 type instance a == b = EqOrdering a b
290 type instance a == b = EqUnit a b
291 type instance a == b = EqList a b
292 type instance a == b = EqMaybe a b
293 type instance a == b = Eq2 a b
294 type instance a == b = Eq3 a b
295 type instance a == b = Eq4 a b
296 type instance a == b = Eq5 a b
297 type instance a == b = Eq6 a b
298 type instance a == b = Eq7 a b
299 type instance a == b = Eq8 a b
300 type instance a == b = Eq9 a b
301 type instance a == b = Eq10 a b
302 type instance a == b = Eq11 a b
303 type instance a == b = Eq12 a b
304 type instance a == b = Eq13 a b
305 type instance a == b = Eq14 a b
306 type instance a == b = Eq15 a b