Data.Eq.Singletons

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.

Documentation

class PEq a

Associated Types

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

type (arg :: a) == (arg1 :: a) = Apply (Apply (TFHelper_6989586621679137938Sym0 :: TyFun a (a ~> Bool) -> Type) arg) arg1

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

type (arg :: a) /= (arg1 :: a) = Apply (Apply (TFHelper_6989586621679137927Sym0 :: TyFun a (a ~> Bool) -> Type) arg) arg1

Instances

PEq All

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Associated Types

type (a1 :: All) == (a2 :: All)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type (a1 :: All) == (a2 :: All)

type (arg :: All) /= (arg1 :: All)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type (arg :: All) /= (arg1 :: All)

PEq Any

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Associated Types

type (a1 :: Any) == (a2 :: Any)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type (a1 :: Any) == (a2 :: Any)

type (arg :: Any) /= (arg1 :: Any)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

type (arg :: Any) /= (arg1 :: Any)

PEq Void

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: Void) == (a2 :: Void)

Defined in Data.Eq.Singletons

type (a1 :: Void) == (a2 :: Void)

type (arg1 :: Void) /= (arg2 :: Void)

Defined in Data.Eq.Singletons

type (arg1 :: Void) /= (arg2 :: Void)

PEq Ordering

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: Ordering) == (a2 :: Ordering)

Defined in Data.Eq.Singletons

type (a1 :: Ordering) == (a2 :: Ordering)

type (arg1 :: Ordering) /= (arg2 :: Ordering)

Defined in Data.Eq.Singletons

type (arg1 :: Ordering) /= (arg2 :: Ordering)

PEq Natural

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type (x :: Natural) == (y :: Natural)

Defined in GHC.TypeLits.Singletons.Internal

type (x :: Natural) == (y :: Natural) = DefaultEq x y

type (arg :: Natural) /= (arg1 :: Natural)

Defined in GHC.TypeLits.Singletons.Internal

type (arg :: Natural) /= (arg1 :: Natural)

PEq ()

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: ()) == (a2 :: ())

Defined in Data.Eq.Singletons

type (a1 :: ()) == (a2 :: ())

type (arg1 :: ()) /= (arg2 :: ())

Defined in Data.Eq.Singletons

type (arg1 :: ()) /= (arg2 :: ())

PEq Bool

Defined in Data.Eq.Singletons

Associated Types

type (a1 :: Bool) == (a2 :: Bool)

Defined in Data.Eq.Singletons

type (a1 :: Bool) == (a2 :: Bool)

type (arg1 :: Bool) /= (arg2 :: Bool)

Defined in Data.Eq.Singletons

type (arg1 :: Bool) /= (arg2 :: Bool)

PEq Char

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type (x :: Char) == (y :: Char)

Defined in GHC.TypeLits.Singletons.Internal

type (x :: Char) == (y :: Char) = DefaultEq x y

type (arg :: Char) /= (arg1 :: Char)

Defined in GHC.TypeLits.Singletons.Internal

type (arg :: Char) /= (arg1 :: Char)

PEq Symbol

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type (x :: Symbol) == (y :: Symbol)

Defined in GHC.TypeLits.Singletons.Internal

type (x :: Symbol) == (y :: Symbol) = DefaultEq x y

type (arg :: Symbol) /= (arg1 :: Symbol)

Defined in GHC.TypeLits.Singletons.Internal

type (arg :: Symbol) /= (arg1 :: Symbol)

PEq (Identity a)

Defined in Data.Eq.Singletons

PEq (First a)

Defined in Data.Monoid.Singletons

PEq (Last a)

Defined in Data.Monoid.Singletons

PEq (Down a)

Defined in Data.Ord.Singletons

PEq (First a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Last a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Max a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Min a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Dual a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Product a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (Sum a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

PEq (NonEmpty a)

Defined in Data.Eq.Singletons

PEq (Maybe a)

Defined in Data.Eq.Singletons

PEq (TYPE rep)

Defined in Data.Singletons.Base.TypeRepTYPE

PEq [a]

Defined in Data.Eq.Singletons

PEq (Either a b)

Defined in Data.Eq.Singletons

PEq (Proxy s)

Defined in Data.Proxy.Singletons

PEq (Arg a b)

Defined in Data.Semigroup.Singletons

PEq (a, b)

Defined in Data.Eq.Singletons

PEq (Const a b)

Defined in Data.Functor.Const.Singletons

PEq (a, b, c)

Defined in Data.Eq.Singletons

PEq (Product f g a)

Defined in Data.Functor.Product.Singletons

PEq (Sum f g a)

Defined in Data.Functor.Sum.Singletons

PEq (a, b, c, d)

Defined in Data.Eq.Singletons

PEq (Compose f g a)

Defined in Data.Functor.Compose.Singletons

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

Defined in Data.Eq.Singletons

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

Defined in Data.Eq.Singletons

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

Defined in Data.Eq.Singletons

class SEq a where

Minimal complete definition

Nothing

Methods

(%==) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) t1) t2) infix 4

default (%==) :: forall (t1 :: a) (t2 :: a). Apply (Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) t1) t2 ~ Apply (Apply (TFHelper_6989586621679137938Sym0 :: TyFun a (a ~> Bool) -> Type) t1) t2 => Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: a) (t2 :: a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) t1) t2) infix 4

default (%/=) :: forall (t1 :: a) (t2 :: a). Apply (Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) t1) t2 ~ Apply (Apply (TFHelper_6989586621679137927Sym0 :: TyFun a (a ~> Bool) -> Type) t1) t2 => Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) t1) t2)

Instances

SEq Bool => SEq All

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: All) (t2 :: All). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun All (All ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: All) (t2 :: All). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun All (All ~> Bool) -> Type) t1) t2)

SEq Bool => SEq Any

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: Any) (t2 :: Any). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Any (Any ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Any) (t2 :: Any). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun Any (Any ~> Bool) -> Type) t1) t2)

SEq Void

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: Void) (t2 :: Void). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Void (Void ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Void) (t2 :: Void). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun Void (Void ~> Bool) -> Type) t1) t2)

SEq Ordering

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: Ordering) (t2 :: Ordering). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Ordering (Ordering ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Ordering) (t2 :: Ordering). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun Ordering (Ordering ~> Bool) -> Type) t1) t2)

SEq Natural

Defined in GHC.TypeLits.Singletons.Internal

Methods

(%==) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Natural (Natural ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun Natural (Natural ~> Bool) -> Type) t1) t2)

SEq ()

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: ()) (t2 :: ()). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun () (() ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: ()) (t2 :: ()). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun () (() ~> Bool) -> Type) t1) t2)

SEq Bool

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: Bool) (t2 :: Bool). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Bool (Bool ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Bool) (t2 :: Bool). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun Bool (Bool ~> Bool) -> Type) t1) t2)

SEq Char

Defined in GHC.TypeLits.Singletons.Internal

Methods

(%==) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Char (Char ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Char) (t2 :: Char). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun Char (Char ~> Bool) -> Type) t1) t2)

SEq Symbol

Defined in GHC.TypeLits.Singletons.Internal

Methods

(%==) :: forall (t1 :: Symbol) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun Symbol (Symbol ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Symbol) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun Symbol (Symbol ~> Bool) -> Type) t1) t2)

SEq a => SEq (Identity a)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Identity a) (Identity a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Identity a) (Identity a ~> Bool) -> Type) t1) t2)

SEq (Maybe a) => SEq (First a)

Defined in Data.Monoid.Singletons

Methods

(%==) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (First a) (First a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (First a) (First a ~> Bool) -> Type) t1) t2)

SEq (Maybe a) => SEq (Last a)

Defined in Data.Monoid.Singletons

Methods

(%==) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Last a) (Last a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Last a) (Last a ~> Bool) -> Type) t1) t2)

SEq a => SEq (Down a)

Defined in Data.Ord.Singletons

Methods

(%==) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Down a) (Down a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Down a) (Down a ~> Bool) -> Type) t1) t2)

SEq a => SEq (First a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (First a) (First a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (First a) (First a ~> Bool) -> Type) t1) t2)

SEq a => SEq (Last a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Last a) (Last a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Last a) (Last a ~> Bool) -> Type) t1) t2)

SEq a => SEq (Max a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: Max a) (t2 :: Max a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Max a) (Max a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Max a) (t2 :: Max a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Max a) (Max a ~> Bool) -> Type) t1) t2)

SEq a => SEq (Min a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: Min a) (t2 :: Min a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Min a) (Min a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Min a) (t2 :: Min a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Min a) (Min a ~> Bool) -> Type) t1) t2)

SEq m => SEq (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: WrappedMonoid m) (t2 :: WrappedMonoid m). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (WrappedMonoid m) (WrappedMonoid m ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: WrappedMonoid m) (t2 :: WrappedMonoid m). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (WrappedMonoid m) (WrappedMonoid m ~> Bool) -> Type) t1) t2)

SEq a => SEq (Dual a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: Dual a) (t2 :: Dual a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Dual a) (Dual a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Dual a) (t2 :: Dual a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Dual a) (Dual a ~> Bool) -> Type) t1) t2)

SEq a => SEq (Product a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: Product a) (t2 :: Product a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Product a) (Product a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Product a) (t2 :: Product a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Product a) (Product a ~> Bool) -> Type) t1) t2)

SEq a => SEq (Sum a)

Defined in Data.Semigroup.Singletons.Internal.Wrappers

Methods

(%==) :: forall (t1 :: Sum a) (t2 :: Sum a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Sum a) (Sum a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Sum a) (t2 :: Sum a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Sum a) (Sum a ~> Bool) -> Type) t1) t2)

(SEq a, SEq [a]) => SEq (NonEmpty a)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: NonEmpty a) (t2 :: NonEmpty a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (NonEmpty a) (NonEmpty a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: NonEmpty a) (t2 :: NonEmpty a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (NonEmpty a) (NonEmpty a ~> Bool) -> Type) t1) t2)

SEq a => SEq (Maybe a)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Maybe a) (Maybe a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Maybe a) (Maybe a ~> Bool) -> Type) t1) t2)

SEq (TYPE rep)

Defined in Data.Singletons.Base.TypeRepTYPE

Methods

(%==) :: forall (t1 :: TYPE rep) (t2 :: TYPE rep). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (TYPE rep) (TYPE rep ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: TYPE rep) (t2 :: TYPE rep). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (TYPE rep) (TYPE rep ~> Bool) -> Type) t1) t2)

(SEq a, SEq [a]) => SEq [a]

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: [a]) (t2 :: [a]). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun [a] ([a] ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: [a]) (t2 :: [a]). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun [a] ([a] ~> Bool) -> Type) t1) t2)

(SEq a, SEq b) => SEq (Either a b)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: Either a b) (t2 :: Either a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Either a b) (Either a b ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Either a b) (t2 :: Either a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Either a b) (Either a b ~> Bool) -> Type) t1) t2)

SEq (Proxy s)

Defined in Data.Proxy.Singletons

Methods

(%==) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Proxy s) (Proxy s ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Proxy s) (Proxy s ~> Bool) -> Type) t1) t2)

SEq a => SEq (Arg a b)

Defined in Data.Semigroup.Singletons

Methods

(%==) :: forall (t1 :: Arg a b) (t2 :: Arg a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Arg a b) (Arg a b ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Arg a b) (t2 :: Arg a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Arg a b) (Arg a b ~> Bool) -> Type) t1) t2)

(SEq a, SEq b) => SEq (a, b)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: (a, b)) (t2 :: (a, b)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (a, b) ((a, b) ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: (a, b)) (t2 :: (a, b)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (a, b) ((a, b) ~> Bool) -> Type) t1) t2)

SEq a => SEq (Const a b)

Defined in Data.Functor.Const.Singletons

Methods

(%==) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Const a b) (Const a b ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Const a b) (Const a b ~> Bool) -> Type) t1) t2)

(SEq a, SEq b, SEq c) => SEq (a, b, c)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: (a, b, c)) (t2 :: (a, b, c)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (a, b, c) ((a, b, c) ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: (a, b, c)) (t2 :: (a, b, c)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (a, b, c) ((a, b, c) ~> Bool) -> Type) t1) t2)

(SEq (f a), SEq (g a)) => SEq (Product f g a)

Defined in Data.Functor.Product.Singletons

Methods

(%==) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2)

(SEq (f a), SEq (g a)) => SEq (Sum f g a)

Defined in Data.Functor.Sum.Singletons

Methods

(%==) :: forall (t1 :: Sum f g a) (t2 :: Sum f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Sum f g a) (Sum f g a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Sum f g a) (t2 :: Sum f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Sum f g a) (Sum f g a ~> Bool) -> Type) t1) t2)

(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: (a, b, c, d)) (t2 :: (a, b, c, d)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (a, b, c, d) ((a, b, c, d) ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: (a, b, c, d)) (t2 :: (a, b, c, d)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (a, b, c, d) ((a, b, c, d) ~> Bool) -> Type) t1) t2)

SEq (f (g a)) => SEq (Compose f g a)

Defined in Data.Functor.Compose.Singletons

Methods

(%==) :: forall (t1 :: Compose f g a) (t2 :: Compose f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Compose f g a) (Compose f g a ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: Compose f g a) (t2 :: Compose f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Compose f g a) (Compose f g a ~> Bool) -> Type) t1) t2)

(SEq a, SEq b, SEq c, SEq d, SEq e) => SEq (a, b, c, d, e)

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t1 :: (a, b, c, d, e)) (t2 :: (a, b, c, d, e)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (a, b, c, d, e) ((a, b, c, d, e) ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: (a, b, c, d, e)) (t2 :: (a, b, c, d, e)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (a, b, c, d, e) ((a, b, c, d, e) ~> Bool) -> Type) t1) t2)

(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) => SEq (a, b, c, d, e, f)

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 (Apply (Apply ((==@#@$) :: TyFun (a, b, c, d, e, f) ((a, b, c, d, e, f) ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: (a, b, c, d, e, f)) (t2 :: (a, b, c, d, e, f)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (a, b, c, d, e, f) ((a, b, c, d, e, f) ~> Bool) -> Type) t1) t2)

(SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) => SEq (a, b, c, d, e, f, g)

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 (Apply (Apply ((==@#@$) :: TyFun (a, b, c, d, e, f, g) ((a, b, c, d, e, f, g) ~> Bool) -> Type) t1) t2)

(%/=) :: forall (t1 :: (a, b, c, d, e, f, g)) (t2 :: (a, b, c, d, e, f, g)). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (a, b, c, d, e, f, g) ((a, b, c, d, e, f, g) ~> Bool) -> Type) t1) t2)

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

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

Instances

SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing ((==@#@$) :: TyFun a (a ~> Bool) -> Type)

SuppressUnusedWarnings ((==@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679137918 :: a)

Defined in Data.Eq.Singletons

type Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679137918 :: a) = (==@#@$$) a6989586621679137918

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

Instances

SEq a => SingI1 ((==@#@$$) :: a -> TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

liftSing :: forall (x :: a). Sing x -> Sing ((==@#@$$) x)

(SEq a, SingI d) => SingI ((==@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing ((==@#@$$) d)

SuppressUnusedWarnings ((==@#@$$) a6989586621679137918 :: TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((==@#@$$) a6989586621679137918 :: TyFun a Bool -> Type) (a6989586621679137919 :: a)

Defined in Data.Eq.Singletons

type Apply ((==@#@$$) a6989586621679137918 :: TyFun a Bool -> Type) (a6989586621679137919 :: a) = a6989586621679137918 == a6989586621679137919

type family (a6989586621679137918 :: a) ==@#@$$$ (a6989586621679137919 :: a) :: Bool where ... infix 4

Equations

(a6989586621679137918 :: a) ==@#@$$$ (a6989586621679137919 :: a) = a6989586621679137918 == a6989586621679137919

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

Instances

SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing ((/=@#@$) :: TyFun a (a ~> Bool) -> Type)

SuppressUnusedWarnings ((/=@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679137923 :: a)

Defined in Data.Eq.Singletons

type Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679137923 :: a) = (/=@#@$$) a6989586621679137923

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

Instances

SEq a => SingI1 ((/=@#@$$) :: a -> TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

liftSing :: forall (x :: a). Sing x -> Sing ((/=@#@$$) x)

(SEq a, SingI d) => SingI ((/=@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing ((/=@#@$$) d)

SuppressUnusedWarnings ((/=@#@$$) a6989586621679137923 :: TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((/=@#@$$) a6989586621679137923 :: TyFun a Bool -> Type) (a6989586621679137924 :: a)

Defined in Data.Eq.Singletons

type Apply ((/=@#@$$) a6989586621679137923 :: TyFun a Bool -> Type) (a6989586621679137924 :: a) = a6989586621679137923 /= a6989586621679137924

type family (a6989586621679137923 :: a) /=@#@$$$ (a6989586621679137924 :: a) :: Bool where ... infix 4

Equations

(a6989586621679137923 :: a) /=@#@$$$ (a6989586621679137924 :: a) = a6989586621679137923 /= a6989586621679137924

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

Instances

SuppressUnusedWarnings (DefaultEqSym0 :: TyFun k (k ~> Bool) -> Type)

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (DefaultEqSym0 :: TyFun k (k ~> Bool) -> Type) (a6989586621679140066 :: k)

Defined in Data.Eq.Singletons

type Apply (DefaultEqSym0 :: TyFun k (k ~> Bool) -> Type) (a6989586621679140066 :: k) = DefaultEqSym1 a6989586621679140066

data DefaultEqSym1 (a6989586621679140066 :: k) (b :: TyFun k Bool)

Instances

SuppressUnusedWarnings (DefaultEqSym1 a6989586621679140066 :: TyFun k Bool -> Type)

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (DefaultEqSym1 a6989586621679140066 :: TyFun k Bool -> Type) (a6989586621679140067 :: k)

Defined in Data.Eq.Singletons

type Apply (DefaultEqSym1 a6989586621679140066 :: TyFun k Bool -> Type) (a6989586621679140067 :: k) = DefaultEq a6989586621679140066 a6989586621679140067

type family DefaultEqSym2 (a6989586621679140066 :: k) (a6989586621679140067 :: k) :: Bool where ...

Equations

DefaultEqSym2 (a6989586621679140066 :: k) (a6989586621679140067 :: k) = DefaultEq a6989586621679140066 a6989586621679140067