singletons-3.0.1: Basic singleton types and definitions

Data.Singletons.Decide

Description

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

Synopsis

The SDecide class

class SDecide k where Source #

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.

Methods

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

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

Supporting definitions

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

Instances

Instances details
 TestCoercion ((:~:) a :: k -> Type) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Coercion MethodstestCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) # TestEquality ((:~:) a :: k -> Type) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality MethodstestEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) # a ~ b => Bounded (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality MethodsminBound :: a :~: b #maxBound :: a :~: b # a ~ b => Enum (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality Methodssucc :: (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) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality Methods(==) :: (a :~: b) -> (a :~: b) -> Bool #(/=) :: (a :~: b) -> (a :~: b) -> Bool # Ord (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality Methodscompare :: (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 Instance detailsDefined in Data.Type.Equality MethodsreadsPrec :: Int -> ReadS (a :~: b) #readList :: ReadS [a :~: b] #readPrec :: ReadPrec (a :~: b) #readListPrec :: ReadPrec [a :~: b] # Show (a :~: b) Since: base-4.7.0.0 Instance detailsDefined in Data.Type.Equality MethodsshowsPrec :: Int -> (a :~: b) -> ShowS #show :: (a :~: b) -> String #showList :: [a :~: b] -> ShowS #

data Void #

Uninhabited data type

Since: base-4.8.0.0

Instances

Instances details
 Since: base-4.8.0.0 Instance detailsDefined in Data.Void Methods(==) :: Void -> Void -> Bool #(/=) :: Void -> Void -> Bool # Since: base-4.8.0.0 Instance detailsDefined in Data.Void Methodsgfoldl :: (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 #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 :: forall r r'. (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 # Since: base-4.8.0.0 Instance detailsDefined in Data.Void Methodscompare :: Void -> Void -> Ordering #(<) :: Void -> Void -> Bool #(<=) :: Void -> Void -> Bool #(>) :: Void -> Void -> Bool #(>=) :: Void -> Void -> Bool #max :: Void -> Void -> Void #min :: Void -> Void -> 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 Instance detailsDefined in Data.Void Methods Since: base-4.8.0.0 Instance detailsDefined in Data.Void MethodsshowsPrec :: Int -> Void -> ShowS #show :: Void -> String #showList :: [Void] -> ShowS # Since: base-4.8.0.0 Instance detailsDefined in Data.Void Methodsrange :: (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 # Since: base-4.8.0.0 Instance detailsDefined in Data.Void Associated Typestype Rep Void :: Type -> Type # Methodsfrom :: Void -> Rep Void x #to :: Rep Void x -> Void # Since: base-4.9.0.0 Instance detailsDefined in Data.Void Methods(<>) :: Void -> Void -> Void #stimes :: Integral b => b -> Void -> Void # Since: base-4.8.0.0 Instance detailsDefined in Data.Void Methods type Rep Void Instance detailsDefined in Data.Void type Rep Void = D1 ('MetaData "Void" "Data.Void" "base" 'False) (V1 :: Type -> Type)

type Refuted a = a -> Void Source #

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 Source #

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

decideEquality :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (a :~: b) Source #

A suitable default implementation for testEquality that leverages SDecide.

decideCoercion :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (Coercion a b) Source #

A suitable default implementation for testCoercion that leverages SDecide.

Orphan instances

 SDecide k => TestCoercion (WrappedSing :: k -> Type) Source # Instance details MethodstestCoercion :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (Coercion a b) # SDecide k => TestEquality (WrappedSing :: k -> Type) Source # Instance details MethodstestEquality :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (a :~: b) #