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) == (arg :: a) :: Bool infix 4

type a == a = Apply (Apply TFHelper_6989586621679140225Sym0 a) a

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

type a /= a = Apply (Apply TFHelper_6989586621679140214Sym0 a) a

Instances

PEq All

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq Any

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq Void

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq Ordering

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq Natural

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq ()

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq Bool

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq Char

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq Symbol

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Identity a)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (First a)

Defined in Data.Monoid.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Last a)

Defined in Data.Monoid.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Down a)

Defined in Data.Ord.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (First a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Last a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Max a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Min a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Dual a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Product a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Sum a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (NonEmpty a)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Maybe a)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (TYPE rep)

Defined in Data.Singletons.Base.TypeRepTYPE

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq [a]

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Either a b)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Proxy s)

Defined in Data.Proxy.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Arg a b)

Defined in Data.Semigroup.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (a, b)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (Const a b)

Defined in Data.Functor.Const.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (a, b, c)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

PEq (a, b, c, d)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

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

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

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

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

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

Defined in Data.Eq.Singletons

Associated Types

type arg == arg1 :: Bool

type arg /= arg1 :: Bool

class SEq a where

Minimal complete definition

Nothing

Methods

(%==) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t :: Bool) infix 4

default (%==) :: forall (t :: a) (t :: a). (Apply (Apply (==@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679140225Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t :: Bool)

(%/=) :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t :: Bool) infix 4

default (%/=) :: forall (t :: a) (t :: a). (Apply (Apply (/=@#@$) t) t :: Bool) ~ Apply (Apply TFHelper_6989586621679140214Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t :: Bool)

Instances

SEq Bool => SEq All

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq Bool => SEq Any

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq Void

Defined in Data.Eq.Singletons

Methods

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

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

SEq Ordering

Defined in Data.Eq.Singletons

Methods

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

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

SEq Natural

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

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

SEq ()

Defined in Data.Eq.Singletons

Methods

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

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

SEq Bool

Defined in Data.Eq.Singletons

Methods

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

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

SEq Char

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

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

SEq Symbol

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

(%/=) :: forall (t1 :: Symbol) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Identity a) (t2 :: Identity a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: First a) (t2 :: First a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Last a) (t2 :: Last a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

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

SEq a => SEq (First a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Last a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Max a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Min a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq m => SEq (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Dual a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Product a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Sum a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

(%/=) :: forall (t1 :: Sum a) (t2 :: Sum a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: NonEmpty a) (t2 :: NonEmpty a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Maybe a) (t2 :: Maybe a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: TYPE rep) (t2 :: TYPE rep). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: [a]) (t2 :: [a]). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Either a b) (t2 :: Either a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Proxy s) (t2 :: Proxy s). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Arg a b) (t2 :: Arg a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: (a, b)) (t2 :: (a, b)). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: (a, b, c)) (t2 :: (a, b, c)). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: (a, b, c, d)) (t2 :: (a, b, c, d)). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: (a, b, c, d, e)) (t2 :: (a, b, c, d, e)). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) t1) t2)

(%/=) :: forall (t1 :: (a, b, c, d, e, f)) (t2 :: (a, b, c, d, e, f)). Sing t1 -> Sing t2 -> Sing (Apply (Apply (/=@#@$) 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 (==@#@$) 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 (/=@#@$) 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 a = 'True

DefaultEq a b = 'False

Defunctionalization symbols

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

Instances

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Eq.Singletons

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

data (==@#@$$) (a6989586621679140205 :: a) :: (~>) a Bool infix 4

Instances

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((==@#@$$) a6989586621679140205 :: TyFun a Bool -> Type) (a6989586621679140206 :: a)

Defined in Data.Eq.Singletons

type Apply ((==@#@$$) a6989586621679140205 :: TyFun a Bool -> Type) (a6989586621679140206 :: a) = a6989586621679140205 == a6989586621679140206

type family (a6989586621679140205 :: a) ==@#@$$$ (a6989586621679140206 :: a) :: Bool where ... infix 4

Equations

a6989586621679140205 ==@#@$$$ a6989586621679140206 = (==) a6989586621679140205 a6989586621679140206

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

Instances

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Eq.Singletons

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

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

Instances

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Eq.Singletons

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

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

Equations

a6989586621679140210 /=@#@$$$ a6989586621679140211 = (/=) a6989586621679140210 a6989586621679140211

data DefaultEqSym0 :: (~>) 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) (a6989586621679142401 :: k)

Defined in Data.Eq.Singletons

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

data DefaultEqSym1 (a6989586621679142401 :: k) :: (~>) k Bool

Instances

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (DefaultEqSym1 a6989586621679142401 :: TyFun k Bool -> Type) (a6989586621679142402 :: k)

Defined in Data.Eq.Singletons

type Apply (DefaultEqSym1 a6989586621679142401 :: TyFun k Bool -> Type) (a6989586621679142402 :: k) = DefaultEq a6989586621679142401 a6989586621679142402

type family DefaultEqSym2 (a6989586621679142401 :: k) (a6989586621679142402 :: k) :: Bool where ...

Equations

DefaultEqSym2 a6989586621679142401 a6989586621679142402 = DefaultEq a6989586621679142401 a6989586621679142402