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