Data.Singletons.Decide

Defines the class SDecide, allowing for decidable equality over singletons.

The SDecide class

class SDecide k where

Members of the SDecide "kind" class support decidable equality. Instances of this class are generated alongside singleton definitions for datatypes that derive an Eq instance.

Minimal complete definition

(%~)

Methods

(%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b) infix 4

Compute a proof or disproof of equality, given two singletons.

Instances

SDecide Bool

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SDecide Ordering

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SDecide Type

Defined in Data.Singletons.TypeRepStar

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SDecide Nat

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SDecide Symbol

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SDecide ()

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SDecide Void

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Maybe a)

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

(SDecide a, SDecide b) => SDecide (a, b)

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

Supporting definitions

data (a :: k) :~: (b :: k) :: forall k. k -> k -> * where infix 4

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: a :~: a

Instances

TestCoercion ((:~:) a :: k -> *)

Since: base-4.7.0.0

Defined in Data.Type.Coercion

Methods

testCoercion :: (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)

TestEquality ((:~:) a :: k -> *)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)

a ~ b => Bounded (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

minBound :: a :~: b

maxBound :: a :~: b

a ~ b => Enum (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

succ :: (a :~: b) -> a :~: b

pred :: (a :~: b) -> a :~: b

toEnum :: Int -> a :~: b

fromEnum :: (a :~: b) -> Int

enumFrom :: (a :~: b) -> [a :~: b]

enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b]

enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b]

Eq (a :~: b)

Defined in Data.Type.Equality

Methods

(==) :: (a :~: b) -> (a :~: b) -> Bool

(/=) :: (a :~: b) -> (a :~: b) -> Bool

(a ~ b, Data a) => Data (a :~: b)

Since: base-4.7.0.0

Defined in Data.Data

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> (a :~: b) -> c (a :~: b)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (a :~: b)

toConstr :: (a :~: b) -> Constr

dataTypeOf :: (a :~: b) -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (a :~: b))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (a :~: b))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> (a :~: b) -> a :~: b

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (a :~: b) -> r

gmapQ :: (forall d. Data d => d -> u) -> (a :~: b) -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> (a :~: b) -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (a :~: b) -> m (a :~: b)

Ord (a :~: b)

Defined in Data.Type.Equality

Methods

compare :: (a :~: b) -> (a :~: b) -> Ordering

(<) :: (a :~: b) -> (a :~: b) -> Bool

(<=) :: (a :~: b) -> (a :~: b) -> Bool

(>) :: (a :~: b) -> (a :~: b) -> Bool

(>=) :: (a :~: b) -> (a :~: b) -> Bool

max :: (a :~: b) -> (a :~: b) -> a :~: b

min :: (a :~: b) -> (a :~: b) -> a :~: b

a ~ b => Read (a :~: b)

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

readsPrec :: Int -> ReadS (a :~: b)

readList :: ReadS [a :~: b]

readPrec :: ReadPrec (a :~: b)

readListPrec :: ReadPrec [a :~: b]

Show (a :~: b)

Defined in Data.Type.Equality

Methods

showsPrec :: Int -> (a :~: b) -> ShowS

show :: (a :~: b) -> String

showList :: [a :~: b] -> ShowS

data Void

Uninhabited data type

Since: base-4.8.0.0

Instances

Eq Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

(==) :: Void -> Void -> Bool

(/=) :: Void -> Void -> Bool

Data Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Void -> c Void

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Void

toConstr :: Void -> Constr

dataTypeOf :: Void -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Void)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Void)

gmapT :: (forall b. Data b => b -> b) -> Void -> Void

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Void -> r

gmapQ :: (forall d. Data d => d -> u) -> Void -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Void -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Void -> m Void

Ord Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

compare :: Void -> Void -> Ordering

(<) :: Void -> Void -> Bool

(<=) :: Void -> Void -> Bool

(>) :: Void -> Void -> Bool

(>=) :: Void -> Void -> Bool

max :: Void -> Void -> Void

min :: Void -> Void -> Void

Read Void

Reading a Void value is always a parse error, considering Void as a data type with no constructors.

Since: base-4.8.0.0

Defined in Data.Void

Methods

readsPrec :: Int -> ReadS Void

readList :: ReadS [Void]

readPrec :: ReadPrec Void

readListPrec :: ReadPrec [Void]

Show Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

showsPrec :: Int -> Void -> ShowS

show :: Void -> String

showList :: [Void] -> ShowS

Ix Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

range :: (Void, Void) -> [Void]

index :: (Void, Void) -> Void -> Int

unsafeIndex :: (Void, Void) -> Void -> Int

inRange :: (Void, Void) -> Void -> Bool

rangeSize :: (Void, Void) -> Int

unsafeRangeSize :: (Void, Void) -> Int

Generic Void

Defined in Data.Void

Associated Types

type Rep Void :: * -> *

Methods

from :: Void -> Rep Void x

to :: Rep Void x -> Void

Semigroup Void

Since: base-4.9.0.0

Defined in Data.Void

Methods

(<>) :: Void -> Void -> Void

sconcat :: NonEmpty Void -> Void

stimes :: Integral b => b -> Void -> Void

Exception Void

Since: base-4.8.0.0

Defined in Data.Void

Methods

toException :: Void -> SomeException

fromException :: SomeException -> Maybe Void

displayException :: Void -> String

SingKind Void

Defined in Data.Singletons.Prelude.Instances

Associated Types

type Demote Void = (r :: *)

Methods

fromSing :: Sing a -> Demote Void

toSing :: Demote Void -> SomeSing Void

SDecide Void

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

PEq Void

Defined in Data.Singletons.Prelude.Eq

Associated Types

type x == y :: Bool

type x /= y :: Bool

SEq Void

Defined in Data.Singletons.Prelude.Eq

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: Sing a -> Sing b -> Sing (a /= b)

SOrd Void

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t)

(%<) :: Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t)

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

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

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

sMax :: Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)

sMin :: Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)

POrd Void

Defined in Data.Singletons.Prelude.Ord

Associated Types

type Compare arg arg :: Ordering

type arg < arg :: Bool

type arg <= arg :: Bool

type arg > arg :: Bool

type arg >= arg :: Bool

type Max arg arg :: a

type Min arg arg :: a

ShowSing Void

Defined in Data.Singletons.ShowSing

Methods

showsSingPrec :: Int -> Sing a -> ShowS

SShow Void

Defined in Data.Singletons.Prelude.Show

Methods

sShowsPrec :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t)

sShow_ :: Sing t -> Sing (Apply Show_Sym0 t)

sShowList :: Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t)

PShow Void

Defined in Data.Singletons.Prelude.Show

Associated Types

type ShowsPrec arg arg arg :: Symbol

type Show_ arg :: Symbol

type ShowList arg arg :: Symbol

Show (Sing z)

Defined in Data.Singletons.ShowSing

Methods

showsPrec :: Int -> Sing z -> ShowS

show :: Sing z -> String

showList :: [Sing z] -> ShowS

SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679303847 -> *)

Defined in Data.Singletons.Prelude.Void

Methods

suppressUnusedWarnings :: ()

type Rep Void

Since: base-4.8.0.0

Defined in Data.Void

type Rep Void = D1 (MetaData "Void" "Data.Void" "base" False) (V1 :: * -> *)

type Demote Void

Defined in Data.Singletons.Prelude.Instances

type Demote Void = Void

data Sing (z :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (z :: Void)

type Show_ (arg :: Void)

Defined in Data.Singletons.Prelude.Show

type Show_ (arg :: Void)

type (a :: Void) == (b :: Void)

Defined in Data.Singletons.Prelude.Eq

type (a :: Void) == (b :: Void)

type (x :: Void) /= (y :: Void)

Defined in Data.Singletons.Prelude.Eq

type (x :: Void) /= (y :: Void) = Not (x == y)

type Compare (a1 :: Void) (a2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type Compare (a1 :: Void) (a2 :: Void)

type (arg1 :: Void) < (arg2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Void) < (arg2 :: Void)

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

Defined in Data.Singletons.Prelude.Ord

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

type (arg1 :: Void) > (arg2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type (arg1 :: Void) > (arg2 :: Void)

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

Defined in Data.Singletons.Prelude.Ord

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

type Max (arg1 :: Void) (arg2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type Max (arg1 :: Void) (arg2 :: Void)

type Min (arg1 :: Void) (arg2 :: Void)

Defined in Data.Singletons.Prelude.Ord

type Min (arg1 :: Void) (arg2 :: Void)

type ShowList (arg1 :: [Void]) arg2

Defined in Data.Singletons.Prelude.Show

type ShowList (arg1 :: [Void]) arg2

type ShowsPrec a1 (a2 :: Void) a3

Defined in Data.Singletons.Prelude.Show

type ShowsPrec a1 (a2 :: Void) a3

type Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void)

Defined in Data.Singletons.Prelude.Void

type Apply (AbsurdSym0 :: TyFun Void k2 -> *) (l :: Void) = (Absurd l :: k2)

type Refuted a = a -> Void

Because we can never create a value of type Void, a function that type-checks at a -> Void shows that objects of type a can never exist. Thus, we say that a is Refuted

data Decision a

A Decision about a type a is either a proof of existence or a proof that a cannot exist.

Constructors

Proved a

Witness for a

Disproved (Refuted a)

Proof that no a exists

Orphan instances

SDecide k => TestCoercion (Sing :: k -> *)

Methods

testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b)

SDecide k => TestEquality (Sing :: k -> *)

Methods

testEquality :: Sing a -> Sing b -> Maybe (a :~: b)