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 b. Sing a -> Sing b -> Decision (a :~: b)

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

Supporting definitions

data (k :~: a) b :: 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: 4.7.0.0

Constructors

Refl :: (:~:) k a a

Instances

TestCoercion k ((:~:) k a)

Methods

testCoercion :: f a -> f b -> Maybe (Coercion (k :~: a) a b)

TestEquality k ((:~:) k a)

Methods

testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b)

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

Methods

minBound :: (k :~: a) b

maxBound :: (k :~: a) b

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

Methods

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

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

toEnum :: Int -> (k :~: a) b

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

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

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

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

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

Eq ((:~:) k a b)

Methods

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

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

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

Methods

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

gunfold :: (forall c r. Data c => c (c -> 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 c. Data c => c -> c) -> (* :~: 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 ((:~:) k a b)

Methods

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

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

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

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

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

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

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

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

Methods

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

readList :: ReadS [(k :~: a) b]

readPrec :: ReadPrec ((k :~: a) b)

readListPrec :: ReadPrec [(k :~: a) b]

Show ((:~:) k a b)

Methods

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

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

showList :: [(k :~: a) b] -> ShowS

data Void :: *

Uninhabited data type

Since: 4.8.0.0

Instances

Eq Void

Methods

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

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

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

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.

Methods

readsPrec :: Int -> ReadS Void

readList :: ReadS [Void]

readPrec :: ReadPrec Void

readListPrec :: ReadPrec [Void]

Show Void

Methods

showsPrec :: Int -> Void -> ShowS

show :: Void -> String

showList :: [Void] -> ShowS

Ix 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

Associated Types

type Rep Void :: * -> *

Methods

from :: Void -> Rep Void x

to :: Rep Void x -> Void

Semigroup Void

Methods

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

sconcat :: NonEmpty Void -> Void

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

Exception Void

Methods

toException :: Void -> SomeException

fromException :: SomeException -> Maybe Void

displayException :: Void -> String

type Rep Void

type Rep Void = D1 (MetaData "Void" "Data.Void" "base" False) V1

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 k2 => TestEquality k2 (Sing k2)

Methods

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