Fix haddocks for marker events in Debug.Trace
[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 infix 4 :~:, :~~:
57
58 -- | Propositional equality. If @a :~: b@ is inhabited by some terminating
59 -- value, then the type @a@ is the same as the type @b@. To use this equality
60 -- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;
61 -- in the body of the pattern-match, the compiler knows that @a ~ b@.
62 --
63 -- @since 4.7.0.0
64 data a :~: b where -- See Note [The equality types story] in TysPrim
65 Refl :: a :~: a
66
67 -- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
68 -- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
69 -- for 'type-eq'
70
71 -- | Symmetry of equality
72 sym :: (a :~: b) -> (b :~: a)
73 sym Refl = Refl
74
75 -- | Transitivity of equality
76 trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
77 trans Refl Refl = Refl
78
79 -- | Type-safe cast, using propositional equality
80 castWith :: (a :~: b) -> a -> b
81 castWith Refl x = x
82
83 -- | Generalized form of type-safe cast using propositional equality
84 gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
85 gcastWith Refl x = x
86
87 -- | Apply one equality to another, respectively
88 apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)
89 apply Refl Refl = Refl
90
91 -- | Extract equality of the arguments from an equality of applied types
92 inner :: (f a :~: g b) -> (a :~: b)
93 inner Refl = Refl
94
95 -- | Extract equality of type constructors from an equality of applied types
96 outer :: (f a :~: g b) -> (f :~: g)
97 outer Refl = Refl
98
99 -- | @since 4.7.0.0
100 deriving instance Eq (a :~: b)
101
102 -- | @since 4.7.0.0
103 deriving instance Show (a :~: b)
104
105 -- | @since 4.7.0.0
106 deriving instance Ord (a :~: b)
107
108 -- | @since 4.7.0.0
109 deriving instance a ~ b => Read (a :~: b)
110
111 -- | @since 4.7.0.0
112 instance a ~ b => Enum (a :~: b) where
113 toEnum 0 = Refl
114 toEnum _ = errorWithoutStackTrace "Data.Type.Equality.toEnum: bad argument"
115
116 fromEnum Refl = 0
117
118 -- | @since 4.7.0.0
119 deriving instance a ~ b => Bounded (a :~: b)
120
121 -- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is
122 -- inhabited by a terminating value if and only if @a@ is the same type as @b@.
123 --
124 -- @since 4.10.0.0
125 data (a :: k1) :~~: (b :: k2) where
126 HRefl :: a :~~: a
127
128 -- | @since 4.10.0.0
129 deriving instance Eq (a :~~: b)
130 -- | @since 4.10.0.0
131 deriving instance Show (a :~~: b)
132 -- | @since 4.10.0.0
133 deriving instance Ord (a :~~: b)
134
135 -- | @since 4.10.0.0
136 deriving instance a ~~ b => Read (a :~~: b)
137
138 -- | @since 4.10.0.0
139 instance a ~~ b => Enum (a :~~: b) where
140 toEnum 0 = HRefl
141 toEnum _ = errorWithoutStackTrace "Data.Type.Equality.toEnum: bad argument"
142
143 fromEnum HRefl = 0
144
145 -- | @since 4.10.0.0
146 deriving instance a ~~ b => Bounded (a :~~: b)
147
148 -- | This class contains types where you can learn the equality of two types
149 -- from information contained in /terms/. Typically, only singleton types should
150 -- inhabit this class.
151 class TestEquality f where
152 -- | Conditionally prove the equality of @a@ and @b@.
153 testEquality :: f a -> f b -> Maybe (a :~: b)
154
155 -- | @since 4.7.0.0
156 instance TestEquality ((:~:) a) where
157 testEquality Refl Refl = Just Refl
158
159 -- | @since 4.10.0.0
160 instance TestEquality ((:~~:) a) where
161 testEquality HRefl HRefl = Just Refl
162
163 infix 4 ==
164
165 -- | A type family to compute Boolean equality.
166 type family (a :: k) == (b :: k) :: Bool where
167 f a == g b = f == g && a == b
168 a == a = 'True
169 _ == _ = 'False
170
171 -- The idea here is to recognize equality of *applications* using
172 -- the first case, and of *constructors* using the second and third
173 -- ones. It would be wonderful if GHC recognized that the
174 -- first and second cases are compatible, which would allow us to
175 -- prove
176 --
177 -- a ~ b => a == b
178 --
179 -- but it (understandably) does not.
180 --
181 -- It is absolutely critical that the three cases occur in precisely
182 -- this order. In particular, if
183 --
184 -- a == a = 'True
185 --
186 -- came first, then the type application case would only be reached
187 -- (uselessly) when GHC discovered that the types were not equal.
188 --
189 -- One might reasonably ask what's wrong with a simpler version:
190 --
191 -- type family (a :: k) == (b :: k) where
192 -- a == a = True
193 -- a == b = False
194 --
195 -- Consider
196 -- data Nat = Zero | Succ Nat
197 --
198 -- Suppose I want
199 -- foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
200 -- foo = Refl
201 --
202 -- This would not type-check with the simple version. `Succ n == Succ m`
203 -- is stuck. We don't know enough about `n` and `m` to reduce the family.
204 -- With the recursive version, `Succ n == Succ m` reduces to
205 -- `Succ == Succ && n == m`, which can reduce to `'True && n == m` and
206 -- finally to `n == m`.