Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	GHC2021

Data.Eq.Singletons

Contents

Defunctionalization symbols

Description

Defines the promoted version of Eq, PEq, and the singleton version, SEq. Also defines the DefaultEq type family, which is useful for implementing boolean equality for non-inductively defined data types.

Synopsis

class PEq a where
- type (arg :: a) == (arg1 :: a) :: Bool
- type (arg :: a) /= (arg1 :: a) :: Bool
class SEq a where
- (%==) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 == t2)
- (%/=) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 /= t2)
type family DefaultEq (a :: k) (b :: k) :: Bool where ...
data (==@#@$) (a1 :: TyFun a (a ~> Bool))
data (a6989586621679128025 :: a) ==@#@$$ (b :: TyFun a Bool)
type family (a6989586621679128025 :: a) ==@#@$$$ (a6989586621679128026 :: a) :: Bool where ...
data (/=@#@$) (a1 :: TyFun a (a ~> Bool))
data (a6989586621679128030 :: a) /=@#@$$ (b :: TyFun a Bool)
type family (a6989586621679128030 :: a) /=@#@$$$ (a6989586621679128031 :: a) :: Bool where ...
data DefaultEqSym0 (a :: TyFun k (k ~> Bool))
data DefaultEqSym1 (a6989586621679129674 :: k) (b :: TyFun k Bool)
type family DefaultEqSym2 (a6989586621679129674 :: k) (a6989586621679129675 :: k) :: Bool where ...

Documentation

class PEq a Source #

Associated Types

type (arg :: a) == (arg1 :: a) :: Bool infix 4 Source #

type (arg :: a) == (arg1 :: a) = TFHelper_6989586621679128045 arg arg1

type (arg :: a) /= (arg1 :: a) :: Bool infix 4 Source #

type (arg :: a) /= (arg1 :: a) = TFHelper_6989586621679128034 arg arg1

Instances

Instances details

PEq Void Source #

Instance details

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: Void) == (a2 :: Void)
Instance details Defined in Data.Eq.Singletons type (a1 :: Void) == (a2 :: Void)
type (arg1 :: Void) /= (arg2 :: Void)
Instance details Defined in Data.Eq.Singletons type (arg1 :: Void) /= (arg2 :: Void)

PEq All Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Associated Types

type (a1 :: All) == (a2 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (a1 :: All) == (a2 :: All)
type (arg :: All) /= (arg1 :: All)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: All) /= (arg1 :: All)

PEq Any Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Associated Types

type (a1 :: Any) == (a2 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (a1 :: Any) == (a2 :: Any)
type (arg :: Any) /= (arg1 :: Any)
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers type (arg :: Any) /= (arg1 :: Any)

PEq Ordering Source #

Instance details

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: Ordering) == (a2 :: Ordering)
Instance details Defined in Data.Eq.Singletons type (a1 :: Ordering) == (a2 :: Ordering)
type (arg1 :: Ordering) /= (arg2 :: Ordering)
Instance details Defined in Data.Eq.Singletons type (arg1 :: Ordering) /= (arg2 :: Ordering)

PEq Natural Source #

Instance details

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type (x :: Natural) == (y :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (x :: Natural) == (y :: Natural) = DefaultEq x y
type (arg :: Natural) /= (arg1 :: Natural)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Natural) /= (arg1 :: Natural)

PEq () Source #

Instance details

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: ()) == (a2 :: ())
Instance details Defined in Data.Eq.Singletons type (a1 :: ()) == (a2 :: ())
type (arg1 :: ()) /= (arg2 :: ())
Instance details Defined in Data.Eq.Singletons type (arg1 :: ()) /= (arg2 :: ())

PEq Bool Source #

Instance details

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: Bool) == (a2 :: Bool)
Instance details Defined in Data.Eq.Singletons type (a1 :: Bool) == (a2 :: Bool)
type (arg1 :: Bool) /= (arg2 :: Bool)
Instance details Defined in Data.Eq.Singletons type (arg1 :: Bool) /= (arg2 :: Bool)

PEq Char Source #

Instance details

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type (x :: Char) == (y :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (x :: Char) == (y :: Char) = DefaultEq x y
type (arg :: Char) /= (arg1 :: Char)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Char) /= (arg1 :: Char)

PEq Symbol Source #

Instance details

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type (x :: Symbol) == (y :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (x :: Symbol) == (y :: Symbol) = DefaultEq x y
type (arg :: Symbol) /= (arg1 :: Symbol)
Instance details Defined in GHC.TypeLits.Singletons.Internal type (arg :: Symbol) /= (arg1 :: Symbol)

PEq (First a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Last a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Max a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Min a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (WrappedMonoid m) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (NonEmpty a) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (Identity a) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (First a) Source #

Instance details

Defined in Data.Monoid.Singletons

PEq (Last a) Source #

Instance details

Defined in Data.Monoid.Singletons

PEq (Down a) Source #

Instance details

Defined in Data.Ord.Singletons

PEq (Dual a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Product a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Sum a) Source #

Instance details

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Maybe a) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (TYPE rep) Source #

Instance details

Defined in Data.Singletons.Base.TypeRepTYPE

PEq [a] Source #

Instance details

Defined in Data.Eq.Singletons

PEq (Arg a b) Source #

Instance details

Defined in Data.Semigroup.Singletons

PEq (Either a b) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (Proxy s) Source #

Instance details

Defined in Data.Proxy.Singletons

PEq (a, b) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (Const a b) Source #

Instance details

Defined in Data.Functor.Const.Singletons

PEq (a, b, c) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (Product f g a) Source #

Instance details

Defined in Data.Functor.Product.Singletons

PEq (Sum f g a) Source #

Instance details

Defined in Data.Functor.Sum.Singletons

PEq (a, b, c, d) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (Compose f g a) Source #

Instance details

Defined in Data.Functor.Compose.Singletons

PEq (a, b, c, d, e) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (a, b, c, d, e, f) Source #

Instance details

Defined in Data.Eq.Singletons

PEq (a, b, c, d, e, f, g) Source #

Instance details

Defined in Data.Eq.Singletons

class SEq a where Source #

Minimal complete definition

Nothing

Methods

(%==) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 == t2) infix 4 Source #

default (%==) :: forall (t1 :: a) (t2 :: a). (t1 == t2) ~ TFHelper_6989586621679128045 t1 t2 => Sing t1 -> Sing t2 -> Sing (t1 == t2) Source #

(%/=) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) infix 4 Source #

default (%/=) :: forall (t1 :: a) (t2 :: a). (t1 /= t2) ~ TFHelper_6989586621679128034 t1 t2 => Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #

Instances

Instances details

SEq Void Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: Void) (t2 :: Void). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Void) (t2 :: Void). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq Bool => SEq All Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: All) (t2 :: All). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: All) (t2 :: All). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq Bool => SEq Any Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: Any) (t2 :: Any). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Any) (t2 :: Any). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq Ordering Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: Ordering) (t2 :: Ordering). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Ordering) (t2 :: Ordering). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq Natural Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%==) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq () Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: ()) (t2 :: ()). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: ()) (t2 :: ()). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq Bool Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: Bool) (t2 :: Bool). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Bool) (t2 :: Bool). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq Char Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%==) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%==) :: forall (t1 :: Symbol) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Symbol) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (First a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Last a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Max a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: Max a) (t2 :: Max a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Max a) (t2 :: Max a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Min a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: Min a) (t2 :: Min a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Min a) (t2 :: Min a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq m => SEq (WrappedMonoid m) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: WrappedMonoid m) (t2 :: WrappedMonoid m). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: WrappedMonoid m) (t2 :: WrappedMonoid m). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq [a]) => SEq (NonEmpty a) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: NonEmpty a) (t2 :: NonEmpty a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: NonEmpty a) (t2 :: NonEmpty a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Identity a) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq (Maybe a) => SEq (First a) Source #
Instance details Defined in Data.Monoid.Singletons Methods (%==) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq (Maybe a) => SEq (Last a) Source #
Instance details Defined in Data.Monoid.Singletons Methods (%==) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Down a) Source #
Instance details Defined in Data.Ord.Singletons Methods (%==) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Dual a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: Dual a) (t2 :: Dual a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Dual a) (t2 :: Dual a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Product a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: Product a) (t2 :: Product a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Product a) (t2 :: Product a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Sum a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal.Wrappers Methods (%==) :: forall (t1 :: Sum a) (t2 :: Sum a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Sum a) (t2 :: Sum a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Maybe a) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq (TYPE rep) Source #
Instance details Defined in Data.Singletons.Base.TypeRepTYPE Methods (%==) :: forall (t1 :: TYPE rep) (t2 :: TYPE rep). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: TYPE rep) (t2 :: TYPE rep). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq [a]) => SEq [a] Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: [a]) (t2 :: [a]). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: [a]) (t2 :: [a]). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Arg a b) Source #
Instance details Defined in Data.Semigroup.Singletons Methods (%==) :: forall (t1 :: Arg a b) (t2 :: Arg a b). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Arg a b) (t2 :: Arg a b). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq b) => SEq (Either a b) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: Either a b) (t2 :: Either a b). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Either a b) (t2 :: Either a b). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq (Proxy s) Source #
Instance details Defined in Data.Proxy.Singletons Methods (%==) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq b) => SEq (a, b) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: (a, b)) (t2 :: (a, b)). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: (a, b)) (t2 :: (a, b)). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq a => SEq (Const a b) Source #
Instance details Defined in Data.Functor.Const.Singletons Methods (%==) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq b, SEq c) => SEq (a, b, c) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: (a, b, c)) (t2 :: (a, b, c)). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: (a, b, c)) (t2 :: (a, b, c)). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq (f a), SEq (g a)) => SEq (Product f g a) Source #
Instance details Defined in Data.Functor.Product.Singletons Methods (%==) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq (f a), SEq (g a)) => SEq (Sum f g a) Source #
Instance details Defined in Data.Functor.Sum.Singletons Methods (%==) :: forall (t1 :: Sum f g a) (t2 :: Sum f g a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Sum f g a) (t2 :: Sum f g a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: (a, b, c, d)) (t2 :: (a, b, c, d)). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: (a, b, c, d)) (t2 :: (a, b, c, d)). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
SEq (f (g a)) => SEq (Compose f g a) Source #
Instance details Defined in Data.Functor.Compose.Singletons Methods (%==) :: forall (t1 :: Compose f g a) (t2 :: Compose f g a). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: Compose f g a) (t2 :: Compose f g a). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: (a, b, c, d, e)) (t2 :: (a, b, c, d, e)). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: (a, b, c, d, e)) (t2 :: (a, b, c, d, e)). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: (a, b, c, d, e, f)) (t2 :: (a, b, c, d, e, f)). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: (a, b, c, d, e, f)) (t2 :: (a, b, c, d, e, f)). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #
(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t1 :: (a, b, c, d, e, f, g)) (t2 :: (a, b, c, d, e, f, g)). Sing t1 -> Sing t2 -> Sing (t1 == t2) Source # (%/=) :: forall (t1 :: (a, b, c, d, e, f, g)) (t2 :: (a, b, c, d, e, f, g)). Sing t1 -> Sing t2 -> Sing (t1 /= t2) Source #

type family DefaultEq (a :: k) (b :: k) :: Bool where ... Source #

One way to compute Boolean equality for types of any kind. This will return True if the two arguments are known to be the same type and False if they are known to be apart. Examples:

>>> DefaultEq Nothing Nothing
True
>>> DefaultEq Nothing (Just a)
False
>>> DefaultEq a a
True

DefaultEq is most suited for data types that are not inductively defined. Four concrete examples of this are Natural, Symbol, Char, and Type. One cannot implement boolean equality for these types by pattern matching alone, so DefaultEq is a good fit instead.

The downside to DefaultEq is that it can fail to reduce if it is unable to determine if two types are equal or apart. Here is one such example:

DefaultEq (Just a) (Just b)

What should this reduce to? It depends on what a and b are. DefaultEq has no way of knowing what these two types are, and as a result, this type will be stuck. This is a pitfall that you can run into if you use DefaultEq to implement boolean equality for an inductive data type like Maybe. For this reason, it is usually recommended to implement boolean equality for inductive data types using pattern matching and recursion, not DefaultEq.

Note that this definition is slightly different from the (==) type family from Data.Type.Equality in base, as (==) attempts to distinguish applications of type constructors from other types. As a result, a == a does not reduce to True for every a, but DefaultEq a a does reduce to True for every a. The latter behavior is more desirable for singletons' purposes, so we use it instead of (==).

Equations

DefaultEq (a :: k) (a :: k) = 'True
DefaultEq (a :: k) (b :: k) = 'False

Defunctionalization symbols

data (==@#@$) (a1 :: TyFun a (a ~> Bool)) infix 4 Source #

Instances

Instances details

SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods sing :: Sing ((==@#@$) :: TyFun a (a ~> Bool) -> Type) #
SuppressUnusedWarnings ((==@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679128025 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679128025 :: a) = (==@#@$$) a6989586621679128025

data (a6989586621679128025 :: a) ==@#@$$ (b :: TyFun a Bool) infix 4 Source #

Instances

Instances details

SEq a => SingI1 ((==@#@$$) :: a -> TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods liftSing :: forall (x :: a). Sing x -> Sing ((==@#@$$) x) #
(SEq a, SingI d) => SingI ((==@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods sing :: Sing ((==@#@$$) d) #
SuppressUnusedWarnings ((==@#@$$) a6989586621679128025 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((==@#@$$) a6989586621679128025 :: TyFun a Bool -> Type) (a6989586621679128026 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((==@#@$$) a6989586621679128025 :: TyFun a Bool -> Type) (a6989586621679128026 :: a) = a6989586621679128025 == a6989586621679128026

type family (a6989586621679128025 :: a) ==@#@$$$ (a6989586621679128026 :: a) :: Bool where ... infix 4 Source #

Equations

(a6989586621679128025 :: a) ==@#@$$$ (a6989586621679128026 :: a) = a6989586621679128025 == a6989586621679128026

data (/=@#@$) (a1 :: TyFun a (a ~> Bool)) infix 4 Source #

Instances

Instances details

SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods sing :: Sing ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) #
SuppressUnusedWarnings ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679128030 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679128030 :: a) = (/=@#@$$) a6989586621679128030

data (a6989586621679128030 :: a) /=@#@$$ (b :: TyFun a Bool) infix 4 Source #

Instances

Instances details

SEq a => SingI1 ((/=@#@$$) :: a -> TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods liftSing :: forall (x :: a). Sing x -> Sing ((/=@#@$$) x) #
(SEq a, SingI d) => SingI ((/=@#@$$) d :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods sing :: Sing ((/=@#@$$) d) #
SuppressUnusedWarnings ((/=@#@$$) a6989586621679128030 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((/=@#@$$) a6989586621679128030 :: TyFun a Bool -> Type) (a6989586621679128031 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((/=@#@$$) a6989586621679128030 :: TyFun a Bool -> Type) (a6989586621679128031 :: a) = a6989586621679128030 /= a6989586621679128031

type family (a6989586621679128030 :: a) /=@#@$$$ (a6989586621679128031 :: a) :: Bool where ... infix 4 Source #

Equations

(a6989586621679128030 :: a) /=@#@$$$ (a6989586621679128031 :: a) = a6989586621679128030 /= a6989586621679128031

data DefaultEqSym0 (a :: TyFun k (k ~> Bool)) Source #

Instances

Instances details

SuppressUnusedWarnings (DefaultEqSym0 :: TyFun k (k ~> Bool) -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply (DefaultEqSym0 :: TyFun k (k ~> Bool) -> Type) (a6989586621679129674 :: k) Source #
Instance details Defined in Data.Eq.Singletons type Apply (DefaultEqSym0 :: TyFun k (k ~> Bool) -> Type) (a6989586621679129674 :: k) = DefaultEqSym1 a6989586621679129674

data DefaultEqSym1 (a6989586621679129674 :: k) (b :: TyFun k Bool) Source #

Instances

Instances details

SuppressUnusedWarnings (DefaultEqSym1 a6989586621679129674 :: TyFun k Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply (DefaultEqSym1 a6989586621679129674 :: TyFun k Bool -> Type) (a6989586621679129675 :: k) Source #
Instance details Defined in Data.Eq.Singletons type Apply (DefaultEqSym1 a6989586621679129674 :: TyFun k Bool -> Type) (a6989586621679129675 :: k) = DefaultEq a6989586621679129674 a6989586621679129675

type family DefaultEqSym2 (a6989586621679129674 :: k) (a6989586621679129675 :: k) :: Bool where ... Source #

Equations

DefaultEqSym2 (a6989586621679129674 :: k) (a6989586621679129675 :: k) = DefaultEq a6989586621679129674 a6989586621679129675