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.

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

(%~) :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Decision (a :~: b)

SDecide Ordering

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a :: Ordering) (b :: Ordering). Sing a -> Sing b -> Decision (a :~: b)

SDecide Nat

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: forall (a :: Nat) (b :: Nat). Sing a -> Sing b -> Decision (a :~: b)

SDecide Symbol

Defined in Data.Singletons.TypeLits.Internal

Methods

(%~) :: forall (a :: Symbol) (b :: Symbol). Sing a -> Sing b -> Decision (a :~: b)

SDecide ()

Defined in Data.Singletons.Prelude.Instances

Methods

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

SDecide Void

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a :: Void) (b :: Void). Sing a -> Sing b -> Decision (a :~: b)

SDecide Bool => SDecide All

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a :: All) (b :: All). Sing a -> Sing b -> Decision (a :~: b)

SDecide Bool => SDecide Any

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a :: Any) (b :: Any). Sing a -> Sing b -> Decision (a :~: b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a0 :: [a]) (b :: [a]). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Maybe a)

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a0 :: Maybe a) (b :: Maybe a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide (TYPE rep)

Defined in Data.Singletons.TypeRepTYPE

Methods

(%~) :: forall (a :: TYPE rep) (b :: TYPE rep). Sing a -> Sing b -> Decision (a :~: b)

SDecide a => SDecide (Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: Min a) (b :: Min a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: Max a) (b :: Max a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: First a) (b :: First a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: Last a) (b :: Last a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide m => SDecide (WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a :: WrappedMonoid m) (b :: WrappedMonoid m). Sing a -> Sing b -> Decision (a :~: b)

SDecide (Maybe a) => SDecide (Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: Option a) (b :: Option a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Identity a)

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a0 :: Identity a) (b :: Identity a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide (Maybe a) => SDecide (First a)

Defined in Data.Singletons.Prelude.Monoid

Methods

(%~) :: forall (a0 :: First a) (b :: First a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide (Maybe a) => SDecide (Last a)

Defined in Data.Singletons.Prelude.Monoid

Methods

(%~) :: forall (a0 :: Last a) (b :: Last a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: Dual a) (b :: Dual a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: Sum a) (b :: Sum a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

(%~) :: forall (a0 :: Product a) (b :: Product a). Sing a0 -> Sing b -> Decision (a0 :~: b)

SDecide a => SDecide (Down a)

Defined in Data.Singletons.Prelude.Ord

Methods

(%~) :: forall (a0 :: Down a) (b :: Down a). Sing a0 -> Sing b -> Decision (a0 :~: b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a0 :: NonEmpty a) (b :: NonEmpty a). Sing a0 -> Sing b -> Decision (a0 :~: b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a0 :: Either a b) (b0 :: Either a b). Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a0 :: (a, b)) (b0 :: (a, b)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

SDecide (Proxy t)

Defined in Data.Singletons.Prelude.Proxy

Methods

(%~) :: forall (a :: Proxy t) (b :: Proxy t). Sing a -> Sing b -> Decision (a :~: b)

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

Defined in Data.Singletons.Prelude.Instances

Methods

(%~) :: forall (a0 :: (a, b, c)) (b0 :: (a, b, c)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

SDecide a => SDecide (Const a b)

Defined in Data.Singletons.Prelude.Const

Methods

(%~) :: forall (a0 :: Const a b) (b0 :: Const a b). 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

(%~) :: forall (a0 :: (a, b, c, d)) (b0 :: (a, b, c, d)). 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

(%~) :: forall (a0 :: (a, b, c, d, e)) (b0 :: (a, b, c, d, e)). 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

(%~) :: forall (a0 :: (a, b, c, d, e, f)) (b0 :: (a, b, c, d, e, f)). 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

(%~) :: forall (a0 :: (a, b, c, d, e, f, g)) (b0 :: (a, b, c, d, e, f, g)). Sing a0 -> Sing b0 -> Decision (a0 :~: b0)

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

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

Since: base-4.7.0.0

Defined in Data.Type.Coercion

Methods

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

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

Since: base-4.7.0.0

Defined in Data.Type.Equality

Methods

testEquality :: forall (a0 :: k0) (b :: k0). (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)

Since: base-4.7.0.0

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

Since: base-4.7.0.0

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)

Since: base-4.7.0.0

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

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

Since: base-4.8.0.0

Defined in Data.Void

Associated Types

type Rep Void :: Type -> Type

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

Methods

fromSing :: forall (a :: Void). Sing a -> Demote Void

toSing :: Demote Void -> SomeSing Void

SDecide Void

Defined in Data.Singletons.Prelude.Instances

Methods

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

(%==) :: forall (a :: Void) (b :: Void). Sing a -> Sing b -> Sing (a == b)

(%/=) :: forall (a :: Void) (b :: Void). Sing a -> Sing b -> Sing (a /= b)

SOrd Void

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

sMin :: forall (t :: Void) (t :: Void). 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

SSemigroup Void

Defined in Data.Singletons.Prelude.Semigroup.Internal

Methods

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

sSconcat :: forall (t :: NonEmpty Void). Sing t -> Sing (Apply SconcatSym0 t)

PSemigroup Void

Defined in Data.Singletons.Prelude.Semigroup.Internal

Associated Types

type arg <> arg :: a

type Sconcat arg :: a

SShow Void

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)

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

sShowList :: forall (t :: [Void]) (t :: Symbol). 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

Lift Void

Since: template-haskell-2.15.0.0

Defined in Language.Haskell.TH.Syntax

Methods

lift :: Void -> Q Exp

liftTyped :: Void -> Q (TExp Void)

TestCoercion SVoid

Defined in Data.Singletons.Prelude.Instances

Methods

testCoercion :: forall (a :: k) (b :: k). SVoid a -> SVoid b -> Maybe (Coercion a b)

TestEquality SVoid

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)

Defined in Data.Singletons.Prelude.Void

Methods

sing :: Sing AbsurdSym0

SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a -> Type)

Defined in Data.Singletons.Prelude.Void

Methods

suppressUnusedWarnings :: ()

type Rep Void

Defined in Data.Void

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

type Demote Void

Defined in Data.Singletons.Prelude.Instances

type Demote Void = Void

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SVoid

type Sconcat (arg :: NonEmpty Void)

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sconcat (arg :: NonEmpty 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 (a1 :: Void) <> (a2 :: Void)

Defined in Data.Singletons.Prelude.Semigroup.Internal

type (a1 :: Void) <> (a2 :: 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 -> Type) (a6989586621679359469 :: Void)

Defined in Data.Singletons.Prelude.Void

type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679359469 :: Void) = AbsurdSym1 a6989586621679359469 :: 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

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

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)

A suitable default implementation for testCoercion that leverages SDecide.

Orphan instances

SDecide k => TestCoercion (WrappedSing :: k -> Type)

Methods

testCoercion :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (Coercion a b)

SDecide k => TestEquality (WrappedSing :: k -> Type)

Methods

testEquality :: forall (a :: k0) (b :: k0). WrappedSing a -> WrappedSing b -> Maybe (a :~: b)