{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ExplicitNamespaces #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE TypeInType #-} {-# LANGUAGE Trustworthy #-} ----------------------------------------------------------------------------- -- | -- Module : Data.Type.Equality -- License : BSD-style (see the LICENSE file in the distribution) -- -- Maintainer : [email protected] -- Stability : experimental -- Portability : not portable -- -- Definition of propositional equality @(:~:)@. Pattern-matching on a variable -- of type @(a :~: b)@ produces a proof that @a ~ [email protected] -- -- @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 -- | Lifted, homogeneous equality. By lifted, we mean that it can be -- bogus (deferred type error). By homogeneous, the two types @[email protected] -- and @[email protected] must have the same kind. class a ~~ b => (a :: k) ~ (b :: k) -- See Note [The equality types story] in TysPrim -- NB: All this class does is to wrap its superclass, which is -- the "real", inhomogeneous equality; this is needed when -- we have a Given (a~b), and we want to prove things from it -- NB: Not exported, as (~) is magical syntax. That's also why there's -- no fixity. -- It's tempting to put functional dependencies on (~), but it's not -- necessary because the functional-dependency coverage check looks -- through superclasses, and (~#) is handled in that check. -- | @since 4.9.0.0 instance {-# INCOHERENT #-} a ~~ b => a ~ b -- See Note [The equality types story] in TysPrim -- If we have a Wanted (t1 ~ t2), we want to immediately -- simplify it to (t1 ~~ t2) and solve that instead -- -- INCOHERENT because we want to use this instance eagerly, even when -- the tyvars are partially unknown. infix 4 :~:, :~~: -- | Propositional equality. If @a :~: [email protected] is inhabited by some terminating -- value, then the type @[email protected] is the same as the type @[email protected] To use this equality -- in practice, pattern-match on the @a :~: [email protected] to get out the @[email protected] constructor; -- in the body of the pattern-match, the compiler knows that @a ~ [email protected] -- -- @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 deriving instance Eq (a :~: b) deriving instance Show (a :~: b) 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 :~~: [email protected] is -- inhabited by a terminating value if and only if @[email protected] is the same type as @[email protected] -- -- @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 @[email protected] and @[email protected] 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`.