1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
|
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE Trustworthy #-}
-----------------------------------------------------------------------------
-- |
-- Module : Data.Type.Equality
-- License : BSD-style (see the LICENSE file in the distribution)
--
-- Maintainer : libraries@haskell.org
-- Stability : experimental
-- Portability : not portable
--
-- Definition of propositional equality @(':~:')@. Pattern-matching on a variable
-- of type @(a ':~:' b)@ produces a proof that @a '~' b@.
--
-- @since 4.7.0.0
-----------------------------------------------------------------------------
module Data.Type.Equality (
-- * The equality types
(:~:)(..), type (~~),
(:~~:)(..),
-- * Working with equality
sym, trans, castWith, gcastWith, apply, inner, outer,
-- * Inferring equality from other types
TestEquality(..),
-- * Boolean type-level equality
type (==)
) where
import Data.Maybe
import GHC.Enum
import GHC.Show
import GHC.Read
import GHC.Base
import Data.Type.Bool
infix 4 :~:, :~~:
-- | Propositional equality. If @a :~: b@ is inhabited by some terminating
-- value, then the type @a@ is the same as the type @b@. To use this equality
-- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;
-- in the body of the pattern-match, the compiler knows that @a ~ b@.
--
-- @since 4.7.0.0
data a :~: b where -- See Note [The equality types story] in TysPrim
Refl :: a :~: a
-- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van
-- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif
-- for 'type-eq'
-- | Symmetry of equality
sym :: (a :~: b) -> (b :~: a)
sym Refl = Refl
-- | Transitivity of equality
trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
trans Refl Refl = Refl
-- | Type-safe cast, using propositional equality
castWith :: (a :~: b) -> a -> b
castWith Refl x = x
-- | Generalized form of type-safe cast using propositional equality
gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
gcastWith Refl x = x
-- | Apply one equality to another, respectively
apply :: (f :~: g) -> (a :~: b) -> (f a :~: g b)
apply Refl Refl = Refl
-- | Extract equality of the arguments from an equality of applied types
inner :: (f a :~: g b) -> (a :~: b)
inner Refl = Refl
-- | Extract equality of type constructors from an equality of applied types
outer :: (f a :~: g b) -> (f :~: g)
outer Refl = Refl
-- | @since 4.7.0.0
deriving instance Eq (a :~: b)
-- | @since 4.7.0.0
deriving instance Show (a :~: b)
-- | @since 4.7.0.0
deriving instance Ord (a :~: b)
-- | @since 4.7.0.0
deriving instance a ~ b => Read (a :~: b)
-- | @since 4.7.0.0
instance a ~ b => Enum (a :~: b) where
toEnum 0 = Refl
toEnum _ = errorWithoutStackTrace "Data.Type.Equality.toEnum: bad argument"
fromEnum Refl = 0
-- | @since 4.7.0.0
deriving instance a ~ b => Bounded (a :~: b)
-- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is
-- inhabited by a terminating value if and only if @a@ is the same type as @b@.
--
-- @since 4.10.0.0
data (a :: k1) :~~: (b :: k2) where
HRefl :: a :~~: a
-- | @since 4.10.0.0
deriving instance Eq (a :~~: b)
-- | @since 4.10.0.0
deriving instance Show (a :~~: b)
-- | @since 4.10.0.0
deriving instance Ord (a :~~: b)
-- | @since 4.10.0.0
deriving instance a ~~ b => Read (a :~~: b)
-- | @since 4.10.0.0
instance a ~~ b => Enum (a :~~: b) where
toEnum 0 = HRefl
toEnum _ = errorWithoutStackTrace "Data.Type.Equality.toEnum: bad argument"
fromEnum HRefl = 0
-- | @since 4.10.0.0
deriving instance a ~~ b => Bounded (a :~~: b)
-- | This class contains types where you can learn the equality of two types
-- from information contained in /terms/. Typically, only singleton types should
-- inhabit this class.
class TestEquality f where
-- | Conditionally prove the equality of @a@ and @b@.
testEquality :: f a -> f b -> Maybe (a :~: b)
-- | @since 4.7.0.0
instance TestEquality ((:~:) a) where
testEquality Refl Refl = Just Refl
-- | @since 4.10.0.0
instance TestEquality ((:~~:) a) where
testEquality HRefl HRefl = Just Refl
infix 4 ==
-- | A type family to compute Boolean equality.
type family (a :: k) == (b :: k) :: Bool where
f a == g b = f == g && a == b
a == a = 'True
_ == _ = 'False
-- The idea here is to recognize equality of *applications* using
-- the first case, and of *constructors* using the second and third
-- ones. It would be wonderful if GHC recognized that the
-- first and second cases are compatible, which would allow us to
-- prove
--
-- a ~ b => a == b
--
-- but it (understandably) does not.
--
-- It is absolutely critical that the three cases occur in precisely
-- this order. In particular, if
--
-- a == a = 'True
--
-- came first, then the type application case would only be reached
-- (uselessly) when GHC discovered that the types were not equal.
--
-- One might reasonably ask what's wrong with a simpler version:
--
-- type family (a :: k) == (b :: k) where
-- a == a = True
-- a == b = False
--
-- Consider
-- data Nat = Zero | Succ Nat
--
-- Suppose I want
-- foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)
-- foo = Refl
--
-- This would not type-check with the simple version. `Succ n == Succ m`
-- is stuck. We don't know enough about `n` and `m` to reduce the family.
-- With the recursive version, `Succ n == Succ m` reduces to
-- `Succ == Succ && n == m`, which can reduce to `'True && n == m` and
-- finally to `n == m`.
|
