{-# 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 : 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
-- | Lifted, homogeneous equality. By lifted, we mean that it can be
-- bogus (deferred type error). By homogeneous, the two types @a@
-- and @b@ 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 :~: 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
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 :~~: 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`.