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_6989586621679131024Sym0 a) a

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

type a /= a = Apply (Apply TFHelper_6989586621679131013Sym0 a) a

Instances

PEq Bool

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq Ordering

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq Nat

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq Symbol

Defined in GHC.TypeLits.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq ()

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq Void

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq All

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq Any

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq [a]

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Maybe a)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (TYPE rep)

Defined in Data.Singletons.Base.TypeRepTYPE

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Min a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Max a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (First a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Last a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Identity a)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (First a)

Defined in Data.Monoid.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Last a)

Defined in Data.Monoid.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Dual a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Sum a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Product a)

Defined in Data.Semigroup.Singletons.Internal

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Down a)

Defined in Data.Ord.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (NonEmpty a)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Either a b)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (a, b)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Arg a b)

Defined in Data.Semigroup.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Proxy s)

Defined in Data.Proxy.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (a, b, c)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (Const a b)

Defined in Data.Functor.Const.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

PEq (a, b, c, d)

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

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

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

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

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: Bool

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

Defined in Data.Eq.Singletons

Associated Types

type arg == arg :: Bool

type arg /= arg :: 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_6989586621679131024Sym0 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_6989586621679131013Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t :: Bool)

Instances

SEq Bool

Defined in Data.Eq.Singletons

Methods

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

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

SEq Ordering

Defined in Data.Eq.Singletons

Methods

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

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

SEq Nat

Defined in GHC.TypeLits.Singletons.Internal

Methods

(%==) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: Nat) (t :: Nat). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

SEq Symbol

Defined in GHC.TypeLits.Singletons.Internal

Methods

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

(%/=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

SEq ()

Defined in Data.Eq.Singletons

Methods

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

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

SEq Void

Defined in Data.Eq.Singletons

Methods

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

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

SEq Bool => SEq All

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq Bool => SEq Any

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

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

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

SEq a => SEq (Maybe a)

Defined in Data.Eq.Singletons

Methods

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

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

SEq (TYPE rep)

Defined in Data.Singletons.Base.TypeRepTYPE

Methods

(%==) :: forall (t :: TYPE rep) (t :: TYPE rep). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: TYPE rep) (t :: TYPE rep). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

SEq a => SEq (Min a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Max a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (First a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Last a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq m => SEq (WrappedMonoid m)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Identity a)

Defined in Data.Eq.Singletons

Methods

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

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

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

Defined in Data.Monoid.Singletons

Methods

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

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

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

Defined in Data.Monoid.Singletons

Methods

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

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

SEq a => SEq (Dual a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Sum a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Product a)

Defined in Data.Semigroup.Singletons.Internal

Methods

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

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

SEq a => SEq (Down a)

Defined in Data.Ord.Singletons

Methods

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

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

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

Defined in Data.Eq.Singletons

Methods

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

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

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

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

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

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

SEq a => SEq (Arg a b)

Defined in Data.Semigroup.Singletons

Methods

(%==) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

SEq (Proxy s)

Defined in Data.Proxy.Singletons

Methods

(%==) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

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

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

SEq a => SEq (Const a b)

Defined in Data.Functor.Const.Singletons

Methods

(%==) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

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

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

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

Defined in Data.Eq.Singletons

Methods

(%==) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

(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 (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

(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 (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t)

(%/=) :: forall (t :: (a, b, c, d, e, f, g)) (t :: (a, b, c, d, e, f, g)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t)

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. Three concrete examples of this are Nat, Symbol, 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) (a6989586621679131004 :: a)

Defined in Data.Eq.Singletons

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

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

Instances

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply ((==@#@$$) a6989586621679131004 :: TyFun a Bool -> Type) (a6989586621679131005 :: a)

Defined in Data.Eq.Singletons

type Apply ((==@#@$$) a6989586621679131004 :: TyFun a Bool -> Type) (a6989586621679131005 :: a) = a6989586621679131004 == a6989586621679131005

type family (a6989586621679131004 :: a) ==@#@$$$ (a6989586621679131005 :: a) :: Bool where ... infix 4

Equations

a6989586621679131004 ==@#@$$$ a6989586621679131005 = (==) a6989586621679131004 a6989586621679131005

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) (a6989586621679131009 :: a)

Defined in Data.Eq.Singletons

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

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

Instances

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

Defined in Data.Eq.Singletons

Methods

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

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

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

Defined in Data.Eq.Singletons

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

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

Equations

a6989586621679131009 /=@#@$$$ a6989586621679131010 = (/=) a6989586621679131009 a6989586621679131010

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) (a6989586621679133266 :: k)

Defined in Data.Eq.Singletons

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

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

Instances

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

Defined in Data.Eq.Singletons

Methods

suppressUnusedWarnings :: ()

type Apply (DefaultEqSym1 a6989586621679133266 :: TyFun k Bool -> Type) (a6989586621679133267 :: k)

Defined in Data.Eq.Singletons

type Apply (DefaultEqSym1 a6989586621679133266 :: TyFun k Bool -> Type) (a6989586621679133267 :: k) = DefaultEq a6989586621679133266 a6989586621679133267

type family DefaultEqSym2 (a6989586621679133266 :: k) (a6989586621679133267 :: k) :: Bool where ...

Equations

DefaultEqSym2 a6989586621679133266 a6989586621679133267 = DefaultEq a6989586621679133266 a6989586621679133267