Embrace -XTypeInType, add -XStarIsType
[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 RankNTypes #-}
8 {-# LANGUAGE TypeFamilies #-}
9 {-# LANGUAGE UndecidableInstances #-}
10 {-# LANGUAGE ExplicitNamespaces #-}
11 {-# LANGUAGE MultiParamTypeClasses #-}
12 {-# LANGUAGE FunctionalDependencies #-}
13 {-# LANGUAGE DataKinds #-}
14 {-# LANGUAGE PolyKinds #-}
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
39 -- * Working with equality
40 sym, trans, castWith, gcastWith, apply, inner, outer,
41
42 -- * Inferring equality from other types
43 TestEquality(..),
44
45 -- * Boolean type-level equality
46 type (==)
47 ) where
48
49 import Data.Maybe
50 import GHC.Enum
51 import GHC.Show
52 import GHC.Read
53 import GHC.Base
54 import Data.Type.Bool
55
56 -- | Lifted, homogeneous equality. By lifted, we mean that it can be
57 -- bogus (deferred type error). By homogeneous, the two types @a@
58 -- and @b@ must have the same kind.
59 class a ~~ b => (a :: k) ~ (b :: k)
60 -- See Note [The equality types story] in TysPrim
61 -- NB: All this class does is to wrap its superclass, which is
62 -- the "real", inhomogeneous equality; this is needed when
63 -- we have a Given (a~b), and we want to prove things from it
64 -- NB: Not exported, as (~) is magical syntax. That's also why there's
65 -- no fixity.
66
67 -- It's tempting to put functional dependencies on (~), but it's not
68 -- necessary because the functional-dependency coverage check looks
69 -- through superclasses, and (~#) is handled in that check.
70
71 -- | @since 4.9.0.0
72 instance {-# INCOHERENT #-} a ~~ b => a ~ b
73 -- See Note [The equality types story] in TysPrim
74 -- If we have a Wanted (t1 ~ t2), we want to immediately
75 -- simplify it to (t1 ~~ t2) and solve that instead
76 --
77 -- INCOHERENT because we want to use this instance eagerly, even when
78 -- the tyvars are partially unknown.
79
80 infix 4 :~:, :~~:
81
82 -- | Propositional equality. If @a :~: b@ is inhabited by some terminating
83 -- value, then the type @a@ is the same as the type @b@. To use this equality
84 -- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;
85 -- in the body of the pattern-match, the compiler knows that @a ~ b@.
86 --
87 -- @since 4.7.0.0
88 data a :~: b where -- See Note [The equality types story] in TysPrim
89 Refl :: a :~: a
90
91 -- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
92 -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
93 -- for 'type-eq'
94
95 -- | Symmetry of equality
96 sym :: (a :~: b) -> (b :~: a)
97 sym Refl = Refl
98
99 -- | Transitivity of equality
100 trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
101 trans Refl Refl = Refl
102
103 -- | Type-safe cast, using propositional equality
104 castWith :: (a :~: b) -> a -> b
105 castWith Refl x = x
106
107 -- | Generalized form of type-safe cast using propositional equality
108 gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
109 gcastWith Refl x = x
110
111 -- | Apply one equality to another, respectively
112 apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)
113 apply Refl Refl = Refl
114
115 -- | Extract equality of the arguments from an equality of applied types
116 inner :: (f a :~: g b) -> (a :~: b)
117 inner Refl = Refl
118
119 -- | Extract equality of type constructors from an equality of applied types
120 outer :: (f a :~: g b) -> (f :~: g)
121 outer Refl = Refl
122
123 -- | @since 4.7.0.0
124 deriving instance Eq (a :~: b)
125
126 -- | @since 4.7.0.0
127 deriving instance Show (a :~: b)
128
129 -- | @since 4.7.0.0
130 deriving instance Ord (a :~: b)
131
132 -- | @since 4.7.0.0
133 deriving instance a ~ b => Read (a :~: b)
134
135 -- | @since 4.7.0.0
136 instance a ~ b => Enum (a :~: b) where
137 toEnum 0 = Refl
138 toEnum _ = errorWithoutStackTrace "Data.Type.Equality.toEnum: bad argument"
139
140 fromEnum Refl = 0
141
142 -- | @since 4.7.0.0
143 deriving instance a ~ b => Bounded (a :~: b)
144
145 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is
146 -- inhabited by a terminating value if and only if @a@ is the same type as @b@.
147 --
148 -- @since 4.10.0.0
149 data (a :: k1) :~~: (b :: k2) where
150 HRefl :: a :~~: a
151
152 -- | @since 4.10.0.0
153 deriving instance Eq (a :~~: b)
154 -- | @since 4.10.0.0
155 deriving instance Show (a :~~: b)
156 -- | @since 4.10.0.0
157 deriving instance Ord (a :~~: b)
158
159 -- | @since 4.10.0.0
160 deriving instance a ~~ b => Read (a :~~: b)
161
162 -- | @since 4.10.0.0
163 instance a ~~ b => Enum (a :~~: b) where
164 toEnum 0 = HRefl
165 toEnum _ = errorWithoutStackTrace "Data.Type.Equality.toEnum: bad argument"
166
167 fromEnum HRefl = 0
168
169 -- | @since 4.10.0.0
170 deriving instance a ~~ b => Bounded (a :~~: b)
171
172 -- | This class contains types where you can learn the equality of two types
173 -- from information contained in /terms/. Typically, only singleton types should
174 -- inhabit this class.
175 class TestEquality f where
176 -- | Conditionally prove the equality of @a@ and @b@.
177 testEquality :: f a -> f b -> Maybe (a :~: b)
178
179 -- | @since 4.7.0.0
180 instance TestEquality ((:~:) a) where
181 testEquality Refl Refl = Just Refl
182
183 -- | @since 4.10.0.0
184 instance TestEquality ((:~~:) a) where
185 testEquality HRefl HRefl = Just Refl
186
187 infix 4 ==
188
189 -- | A type family to compute Boolean equality.
190 type family (a :: k) == (b :: k) :: Bool where
191 f a == g b = f == g && a == b
192 a == a = 'True
193 _ == _ = 'False
194
195 -- The idea here is to recognize equality of *applications* using
196 -- the first case, and of *constructors* using the second and third
197 -- ones. It would be wonderful if GHC recognized that the
198 -- first and second cases are compatible, which would allow us to
199 -- prove
200 --
201 -- a ~ b => a == b
202 --
203 -- but it (understandably) does not.
204 --
205 -- It is absolutely critical that the three cases occur in precisely
206 -- this order. In particular, if
207 --
208 -- a == a = 'True
209 --
210 -- came first, then the type application case would only be reached
211 -- (uselessly) when GHC discovered that the types were not equal.
212 --
213 -- One might reasonably ask what's wrong with a simpler version:
214 --
215 -- type family (a :: k) == (b :: k) where
216 -- a == a = True
217 -- a == b = False
218 --
219 -- Consider
220 -- data Nat = Zero | Succ Nat
221 --
222 -- Suppose I want
223 -- foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
224 -- foo = Refl
225 --
226 -- This would not type-check with the simple version. `Succ n == Succ m`
227 -- is stuck. We don't know enough about `n` and `m` to reduce the family.
228 -- With the recursive version, `Succ n == Succ m` reduces to
229 -- `Succ == Succ && n == m`, which can reduce to `'True && n == m` and
230 -- finally to `n == m`.