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

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) == (arg :: a) :: Bool
- type (arg :: a) /= (arg :: a) :: Bool
class SEq a where
- (%==) :: forall (t :: a) (t :: a). 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)
type family DefaultEq (a :: k) (b :: k) :: Bool where ...
data (==@#@$) :: (~>) a ((~>) a Bool)
data (==@#@$$) (a6989586621679146321 :: a) :: (~>) a Bool
type family (a6989586621679146321 :: a) ==@#@$$$ (a6989586621679146322 :: a) :: Bool where ...
data (/=@#@$) :: (~>) a ((~>) a Bool)
data (/=@#@$$) (a6989586621679146326 :: a) :: (~>) a Bool
type family (a6989586621679146326 :: a) /=@#@$$$ (a6989586621679146327 :: a) :: Bool where ...
data DefaultEqSym0 :: (~>) k ((~>) k Bool)
data DefaultEqSym1 (a6989586621679148343 :: k) :: (~>) k Bool
type family DefaultEqSym2 (a6989586621679148343 :: k) (a6989586621679148344 :: k) :: Bool where ...

Documentation

class PEq a Source #

Associated Types

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

type a == a = Apply (Apply TFHelper_6989586621679146341Sym0 a) a

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

type a /= a = Apply (Apply TFHelper_6989586621679146330Sym0 a) a

Instances

Instances details

PEq All Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq Any Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq Void Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq Ordering Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq Natural Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq () Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq Bool Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq Char Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Identity a) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (First a) Source #
Instance details Defined in Data.Monoid.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Last a) Source #
Instance details Defined in Data.Monoid.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Down a) Source #
Instance details Defined in Data.Ord.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (First a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Last a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Max a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Min a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (WrappedMonoid m) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Dual a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Product a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Sum a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (NonEmpty a) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Maybe a) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (TYPE rep) Source #
Instance details Defined in Data.Singletons.Base.TypeRepTYPE Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq [a] Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Either a b) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Proxy s) Source #
Instance details Defined in Data.Proxy.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Arg a b) Source #
Instance details Defined in Data.Semigroup.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (a, b) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (Const a b) Source #
Instance details Defined in Data.Functor.Const.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (a, b, c) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (a, b, c, d) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (a, b, c, d, e) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (a, b, c, d, e, f) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #
PEq (a, b, c, d, e, f, g) Source #
Instance details Defined in Data.Eq.Singletons Associated Types type arg == arg :: Bool Source # type arg /= arg :: Bool Source #

class SEq a where Source #

Minimal complete definition

Nothing

Methods

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

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

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

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

Instances

Instances details

SEq Bool => SEq All Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: All) (t :: All). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq Bool => SEq Any Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Any) (t :: Any). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq Void Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq Ordering Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Ordering) (t :: Ordering). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq Natural Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%==) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Natural) (t :: Natural). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq () Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: ()) (t :: ()). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq Bool Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq Char Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%==) :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Char) (t :: Char). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq Symbol Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal Methods (%==) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Symbol) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Identity a) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq (Maybe a) => SEq (First a) Source #
Instance details Defined in Data.Monoid.Singletons Methods (%==) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq (Maybe a) => SEq (Last a) Source #
Instance details Defined in Data.Monoid.Singletons Methods (%==) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Down a) Source #
Instance details Defined in Data.Ord.Singletons Methods (%==) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Down a) (t :: Down a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (First a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: First a) (t :: First a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Last a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Last a) (t :: Last a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Max a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Max a) (t :: Max a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Min a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Min a) (t :: Min a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq m => SEq (WrappedMonoid m) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: WrappedMonoid m) (t :: WrappedMonoid m). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Dual a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Dual a) (t :: Dual a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Product a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Product a) (t :: Product a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Sum a) Source #
Instance details Defined in Data.Semigroup.Singletons.Internal Methods (%==) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Sum a) (t :: Sum a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
(SEq a, SEq [a]) => SEq (NonEmpty a) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: NonEmpty a) (t :: NonEmpty a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Maybe a) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Maybe a) (t :: Maybe a). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq (TYPE rep) Source #
Instance details Defined in Data.Singletons.Base.TypeRepTYPE Methods (%==) :: forall (t :: TYPE rep) (t :: TYPE rep). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: TYPE rep) (t :: TYPE rep). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
(SEq a, SEq [a]) => SEq [a] Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
(SEq a, SEq b) => SEq (Either a b) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Either a b) (t :: Either a b). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq (Proxy s) Source #
Instance details Defined in Data.Proxy.Singletons Methods (%==) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Proxy s) (t :: Proxy s). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Arg a b) Source #
Instance details Defined in Data.Semigroup.Singletons Methods (%==) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: Arg a b) (t :: Arg a b). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
(SEq a, SEq b) => SEq (a, b) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: (a, b)) (t :: (a, b)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
SEq a => SEq (Const a b) Source #
Instance details 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) Source # (%/=) :: forall (t :: Const a b) (t :: Const a b). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
(SEq a, SEq b, SEq c) => SEq (a, b, c) Source #
Instance details Defined in Data.Eq.Singletons Methods (%==) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: (a, b, c)) (t :: (a, b, c)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) Source #
(SEq a, SEq b, SEq c, SEq d) => SEq (a, b, c, d) Source #
Instance details 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) Source # (%/=) :: forall (t :: (a, b, c, d)) (t :: (a, b, c, d)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) 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 (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: (a, b, c, d, e)) (t :: (a, b, c, d, e)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) 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 (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (==@#@$) t) t) Source # (%/=) :: forall (t :: (a, b, c, d, e, f)) (t :: (a, b, c, d, e, f)). Sing t -> Sing t -> Sing (Apply (Apply (/=@#@$) t) t) 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 (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) Source # (%/=) :: 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) 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 a = 'True
DefaultEq a b = 'False

Defunctionalization symbols

data (==@#@$) :: (~>) 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 (==@#@$)
SuppressUnusedWarnings ((==@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679146321 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((==@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679146321 :: a) = (==@#@$$) a6989586621679146321

data (==@#@$$) (a6989586621679146321 :: a) :: (~>) 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 :: k1). 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 ((==@#@$$) a6989586621679146321 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((==@#@$$) a6989586621679146321 :: TyFun a Bool -> Type) (a6989586621679146322 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((==@#@$$) a6989586621679146321 :: TyFun a Bool -> Type) (a6989586621679146322 :: a) = a6989586621679146321 == a6989586621679146322

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

Equations

a6989586621679146321 ==@#@$$$ a6989586621679146322 = (==) a6989586621679146321 a6989586621679146322

data (/=@#@$) :: (~>) 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 (/=@#@$)
SuppressUnusedWarnings ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679146326 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((/=@#@$) :: TyFun a (a ~> Bool) -> Type) (a6989586621679146326 :: a) = (/=@#@$$) a6989586621679146326

data (/=@#@$$) (a6989586621679146326 :: a) :: (~>) 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 :: k1). 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 ((/=@#@$$) a6989586621679146326 :: TyFun a Bool -> Type) Source #
Instance details Defined in Data.Eq.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((/=@#@$$) a6989586621679146326 :: TyFun a Bool -> Type) (a6989586621679146327 :: a) Source #
Instance details Defined in Data.Eq.Singletons type Apply ((/=@#@$$) a6989586621679146326 :: TyFun a Bool -> Type) (a6989586621679146327 :: a) = a6989586621679146326 /= a6989586621679146327

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

Equations

a6989586621679146326 /=@#@$$$ a6989586621679146327 = (/=) a6989586621679146326 a6989586621679146327

data DefaultEqSym0 :: (~>) 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) (a6989586621679148343 :: k) Source #
Instance details Defined in Data.Eq.Singletons type Apply (DefaultEqSym0 :: TyFun k (k ~> Bool) -> Type) (a6989586621679148343 :: k) = DefaultEqSym1 a6989586621679148343

data DefaultEqSym1 (a6989586621679148343 :: k) :: (~>) k Bool Source #

Instances

Instances details

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

type family DefaultEqSym2 (a6989586621679148343 :: k) (a6989586621679148344 :: k) :: Bool where ... Source #

Equations

DefaultEqSym2 a6989586621679148343 a6989586621679148344 = DefaultEq a6989586621679148343 a6989586621679148344