{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE Trustworthy #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Type.Equality -- License : BSD-style (see the LICENSE file in the distribution) -- -- Maintainer : libraries@haskell.org -- Stability : stable -- 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 (~), 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 GHC.Builtin.Types.Prim 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 type (:~~:) :: k1 -> k2 -> Type data a :~~: b 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/. -- -- The result should be @Just Refl@ if and only if the types applied to @f@ are -- equal: -- -- @testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b@ -- -- Typically, only singleton types should inhabit this class. In that case type -- argument equality coincides with term equality: -- -- @testEquality (x :: f a) (y :: f b) = Just Refl ⟺ a = b ⟺ x = y@ -- -- @isJust (testEquality x y) = x == y@ -- -- Singleton types are not required, however, and so the latter two would-be -- laws are not in fact valid in general. 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 (==) :: k -> k -> Bool type family a == b 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`.