singletons-2.6: A framework for generating singleton types

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

Data.Singletons.Decide

Contents

- The SDecide class
- Supporting definitions
- Orphan instances

Description

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

Synopsis

- class SDecide k where
  - (%~) :: forall (a :: k) (b :: k). Sing a -> Sing b -> Decision (a :~: b)
- data (a :: k) :~: (b :: k) where
  - Refl :: forall k (a :: k). a :~: a
- data Void
- type Refuted a = a -> Void
- data Decision a
  - = Proved a
  - | Disproved (Refuted a)
- decideEquality :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (a :~: b)
- decideCoercion :: forall k (a :: k) (b :: k). SDecide k => Sing a -> Sing b -> Maybe (Coercion a b)

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

#### Instances

Instances details

SDecide Bool Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide Ordering Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a :: Ordering) (b :: Ordering). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide Nat Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide Symbol Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal Methods (%~) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide () Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a :: ()) (b :: ()). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide Void Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a :: Void) (b :: Void). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide Bool => SDecide All Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a :: All) (b :: All). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide Bool => SDecide Any Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a :: Any) (b :: Any). Sing a -> Sing b -> Decision (a :~: b) Source #
(SDecide a, SDecide [a]) => SDecide [a] Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: [a]) (b :: [a]). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Maybe a) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: Maybe a) (b :: Maybe a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide (TYPE rep) Source # |
Instance details Defined in Data.Singletons.TypeRepTYPE Methods (%~) :: forall (a :: TYPE rep) (b :: TYPE rep). Sing a -> Sing b -> Decision (a :~: b) Source #
(SDecide a, SDecide [a]) => SDecide (NonEmpty a) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: NonEmpty a) (b :: NonEmpty a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Down a) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Methods (%~) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Identity a) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: Identity a) (b :: Identity a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (First a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: First a) (b :: First a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Last a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: Last a) (b :: Last a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Max a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: Max a) (b :: Max a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Min a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: Min a) (b :: Min a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide (Maybe a) => SDecide (Option a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: Option a) (b :: Option a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide m => SDecide (WrappedMonoid m) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a :: WrappedMonoid m) (b :: WrappedMonoid m). Sing a -> Sing b -> Decision (a :~: b) Source #
SDecide a => SDecide (Dual a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: Dual a) (b :: Dual a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Product a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: Product a) (b :: Product a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide a => SDecide (Sum a) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%~) :: forall (a0 :: Sum a) (b :: Sum a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide (Maybe a) => SDecide (First a) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Methods (%~) :: forall (a0 :: First a) (b :: First a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
SDecide (Maybe a) => SDecide (Last a) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Methods (%~) :: forall (a0 :: Last a) (b :: Last a). Sing a0 -> Sing b -> Decision (a0 :~: b) Source #
(SDecide a, SDecide b) => SDecide (Either a b) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: Either a b) (b0 :: Either a b). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
(SDecide a, SDecide b) => SDecide (a, b) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: (a, b)) (b0 :: (a, b)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
(SDecide a, SDecide b, SDecide c) => SDecide (a, b, c) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: (a, b, c)) (b0 :: (a, b, c)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
SDecide a => SDecide (Const a b) Source # |
Instance details Defined in Data.Singletons.Prelude.Const Methods (%~) :: forall (a0 :: Const a b) (b0 :: Const a b). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
(SDecide a, SDecide b, SDecide c, SDecide d) => SDecide (a, b, c, d) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: (a, b, c, d)) (b0 :: (a, b, c, d)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e) => SDecide (a, b, c, d, e) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: (a, b, c, d, e)) (b0 :: (a, b, c, d, e)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f) => SDecide (a, b, c, d, e, f) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: (a, b, c, d, e, f)) (b0 :: (a, b, c, d, e, f)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #
(SDecide a, SDecide b, SDecide c, SDecide d, SDecide e, SDecide f, SDecide g) => SDecide (a, b, c, d, e, f, g) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a0 :: (a, b, c, d, e, f, g)) (b0 :: (a, b, c, d, e, f, g)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0) Source #

# Supporting definitions

data (a :: k) :~: (b :: k) where #

Constructors

Refl :: forall k (a :: k). a :~: a |

#### Instances

Instances details

TestCoercion ((:~:) a :: k -> Type) |
Instance details Defined in Data.Type.Coercion Methods testCoercion :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b)
TestEquality ((:~:) a :: k -> Type) |
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b)
a ~ b => Bounded (a :~: b) |
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b maxBound :: a :~: b
a ~ b => Enum (a :~: b) |
Instance details 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) |
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool (/=) :: (a :~: b) -> (a :~: b) -> Bool
(a ~ b, Data a) => Data (a :~: b) |

Instance details

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 :: forall r r'. (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) |
Instance details 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) |
Instance details 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) |
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS show :: (a :~: b) -> String showList :: [a :~: b] -> ShowS

data Void #

#### Instances

Instances details

Eq Void |
Instance details Defined in Data.Void Methods (==) :: Void -> Void -> Bool (/=) :: Void -> Void -> Bool
Data Void |

Instance details

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 :: 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

Ord Void |
Instance details 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 |
Instance details Defined in Data.Void Methods readsPrec :: Int -> ReadS Void readList :: ReadS [Void] readPrec :: ReadPrec Void readListPrec :: ReadPrec [Void]
Show Void |
Instance details Defined in Data.Void Methods showsPrec :: Int -> Void -> ShowS show :: Void -> String showList :: [Void] -> ShowS
Ix Void |
Instance details 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 |
Instance details Defined in Data.Void Associated Types type Rep Void :: Type -> Type Methods from :: Void -> Rep Void x to :: Rep Void x -> Void
Semigroup Void |
Instance details Defined in Data.Void Methods (<>) :: Void -> Void -> Void sconcat :: NonEmpty Void -> Void stimes :: Integral b => b -> Void -> Void
Lift Void |
Instance details Defined in Language.Haskell.TH.Syntax Methods lift :: Void -> Q Exp
SingKind Void Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Associated Types type Demote Void = (r :: Type) Source # Methods fromSing :: forall (a :: Void). Sing a -> Demote Void Source # toSing :: Demote Void -> SomeSing Void Source #
Exception Void |
Instance details Defined in Data.Void Methods toException :: Void -> SomeException fromException :: SomeException -> Maybe Void displayException :: Void -> String
SDecide Void Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: forall (a :: Void) (b :: Void). Sing a -> Sing b -> Decision (a :~: b) Source #
PEq Void Source # |
Instance details Defined in Data.Singletons.Prelude.Eq Associated Types type x == y :: Bool Source # type x /= y :: Bool Source #
SEq Void Source # |
Instance details Defined in Data.Singletons.Prelude.Eq Methods (%==) :: forall (a :: Void) (b :: Void). Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: forall (a :: Void) (b :: Void). Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Void Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

sCompare :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply CompareSym0 t) t) Source #

(%<) :: 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 #

(%>) :: 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 #

sMax :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t) Source #

sMin :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t) Source #

POrd Void Source # |
Instance details Defined in Data.Singletons.Prelude.Ord Associated Types type Compare arg arg :: Ordering Source # type arg < arg :: Bool Source # type arg <= arg :: Bool Source # type arg > arg :: Bool Source # type arg >= arg :: Bool Source # type Max arg arg :: a Source # type Min arg arg :: a Source #
SSemigroup Void Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods (%<>) :: forall (t :: Void) (t :: Void). Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source # sSconcat :: forall (t :: NonEmpty Void). Sing t -> Sing (Apply SconcatSym0 t) Source #
PSemigroup Void Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Associated Types type arg <> arg :: a Source # type Sconcat arg :: a Source #
SShow Void Source # |

Instance details

Defined in Data.Singletons.Prelude.Show

Methods

sShowsPrec :: forall (t :: Nat) (t :: Void) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source #

sShow_ :: forall (t :: Void). Sing t -> Sing (Apply Show_Sym0 t) Source #

sShowList :: forall (t :: [Void]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #

PShow Void Source # |
Instance details Defined in Data.Singletons.Prelude.Show Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
TestCoercion SVoid |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a :: k) (b :: k). SVoid a -> SVoid b -> Maybe (Coercion a b)
TestEquality SVoid |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). SVoid a -> SVoid b -> Maybe (a :~: b)
SingI (AbsurdSym0 :: TyFun Void a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Void Methods sing :: Sing AbsurdSym0 Source #
SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679365215 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Void Methods suppressUnusedWarnings :: () Source #
type Rep Void |
Instance details Defined in Data.Void type Rep Void = D1 ('MetaData "Void" "Data.Void" "base" 'False) (V1 :: Type -> Type)
type Demote Void Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Demote Void = Void
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sconcat (arg0 :: NonEmpty Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sconcat (arg0 :: NonEmpty Void)
type Show_ (arg0 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg0 :: Void)
type (a :: Void) == (b :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Eq type (a :: Void) == (b :: Void)
type (x :: Void) /= (y :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: Void) /= (y :: Void) = Not (x == y)
type Compare (a1 :: Void) (a2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Compare (a1 :: Void) (a2 :: Void)
type (arg1 :: Void) < (arg2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) < (arg2 :: Void)
type (arg1 :: Void) <= (arg2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) <= (arg2 :: Void)
type (arg1 :: Void) > (arg2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) > (arg2 :: Void)
type (arg1 :: Void) >= (arg2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type (arg1 :: Void) >= (arg2 :: Void)
type Max (arg1 :: Void) (arg2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Max (arg1 :: Void) (arg2 :: Void)
type Min (arg1 :: Void) (arg2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Min (arg1 :: Void) (arg2 :: Void)
type (a1 :: Void) <> (a2 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type (a1 :: Void) <> (a2 :: Void)
type ShowList (arg1 :: [Void]) arg2 Source # |
Instance details Defined in Data.Singletons.Prelude.Show type ShowList (arg1 :: [Void]) arg2
type ShowsPrec a1 (a2 :: Void) a3 Source # |
Instance details Defined in Data.Singletons.Prelude.Show type ShowsPrec a1 (a2 :: Void) a3
type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679365218 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Void type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679365218 :: Void) = Absurd a6989586621679365218 :: k2

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 Methods testCoercion :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (Coercion a b)
SDecide k => TestEquality (WrappedSing :: k -> Type) Source # |
Instance details Methods testEquality :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (a :~: b)