singletons-2.5.1: 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) :: forall k. k -> k -> Type where
  - Refl :: forall k (a :: k) (b :: k). a :~: a
- data Void
- type Refuted a = a -> Void
- data Decision a
  - = Proved a
  - | Disproved (Refuted a)

# 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

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

# Supporting definitions

data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type where infix 4 Source #

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

Instances

TestCoercion ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in Data.Type.Coercion Methods testCoercion :: (a :~: a0) -> (a :~: b) -> Maybe (Coercion a0 b) Source #
TestEquality ((:~:) a :: k -> Type) | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) Source #
a ~ b => Bounded (a :~: b) | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b Source # maxBound :: a :~: b Source #
a ~ b => Enum (a :~: b) | Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~: b Source #

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

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

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

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

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

Eq (a :~: b) | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool Source # (/=) :: (a :~: b) -> (a :~: b) -> Bool Source #
(a ~ b, Data a) => Data (a :~: b) | Since: base-4.7.0.0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Ord (a :~: b) | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods compare :: (a :~: b) -> (a :~: b) -> Ordering Source # (<) :: (a :~: b) -> (a :~: b) -> Bool Source # (<=) :: (a :~: b) -> (a :~: b) -> Bool Source # (>) :: (a :~: b) -> (a :~: b) -> Bool Source # (>=) :: (a :~: b) -> (a :~: b) -> Bool Source # max :: (a :~: b) -> (a :~: b) -> a :~: b Source # min :: (a :~: b) -> (a :~: b) -> a :~: b Source #
a ~ b => Read (a :~: b) | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) Source # readList :: ReadS [a :~: b] Source # readPrec :: ReadPrec (a :~: b) Source # readListPrec :: ReadPrec [a :~: b] Source #
Show (a :~: b) | Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS Source # show :: (a :~: b) -> String Source # showList :: [a :~: b] -> ShowS Source #

data Void Source #

Uninhabited data type

Since: base-4.8.0.0

Instances

Eq Void | Since: base-4.8.0.0
Instance details Defined in Data.Void Methods (==) :: Void -> Void -> Bool Source # (/=) :: Void -> Void -> Bool Source #
Data Void | Since: base-4.8.0.0

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

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

toConstr :: Void -> Constr Source #

dataTypeOf :: Void -> DataType Source #

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

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

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

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

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

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

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

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

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

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

Ord Void | Since: base-4.8.0.0
Instance details Defined in Data.Void Methods compare :: Void -> Void -> Ordering Source # (<) :: Void -> Void -> Bool Source # (<=) :: Void -> Void -> Bool Source # (>) :: Void -> Void -> Bool Source # (>=) :: Void -> Void -> Bool Source # max :: Void -> Void -> Void Source # min :: Void -> Void -> Void Source #
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
Instance details Defined in Data.Void Methods readsPrec :: Int -> ReadS Void Source # readList :: ReadS [Void] Source # readPrec :: ReadPrec Void Source # readListPrec :: ReadPrec [Void] Source #
Show Void | Since: base-4.8.0.0
Instance details Defined in Data.Void Methods showsPrec :: Int -> Void -> ShowS Source # show :: Void -> String Source # showList :: [Void] -> ShowS Source #
Ix Void | Since: base-4.8.0.0
Instance details Defined in Data.Void Methods range :: (Void, Void) -> [Void] Source # index :: (Void, Void) -> Void -> Int Source # unsafeIndex :: (Void, Void) -> Void -> Int inRange :: (Void, Void) -> Void -> Bool Source # rangeSize :: (Void, Void) -> Int Source # unsafeRangeSize :: (Void, Void) -> Int
Generic Void |
Instance details Defined in Data.Void Associated Types type Rep Void :: Type -> Type Source # Methods from :: Void -> Rep Void x Source # to :: Rep Void x -> Void Source #
Semigroup Void | Since: base-4.9.0.0
Instance details Defined in Data.Void Methods (<>) :: Void -> Void -> Void Source # sconcat :: NonEmpty Void -> Void Source # stimes :: Integral b => b -> Void -> Void Source #
Exception Void | Since: base-4.8.0.0
Instance details Defined in Data.Void Methods toException :: Void -> SomeException Source # fromException :: SomeException -> Maybe Void Source # displayException :: Void -> String Source #
SingKind Void Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Associated Types type Demote Void = (r :: Type) Source # Methods fromSing :: Sing a -> Demote Void Source # toSing :: Demote Void -> SomeSing Void Source #
SDecide Void Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods (%~) :: 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 (%==) :: Sing a -> Sing b -> Sing (a == b) Source # (%/=) :: Sing a -> Sing b -> Sing (a /= b) Source #
SOrd Void Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

Methods

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

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

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

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

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

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

sMin :: 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 (%<>) :: Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source # sSconcat :: 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 :: Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: 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 #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
SingI (AbsurdSym0 :: TyFun Void a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Void Methods sing :: Sing AbsurdSym0 Source #
SuppressUnusedWarnings (AbsurdSym0 :: TyFun Void a6989586621679357946 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Void Methods suppressUnusedWarnings :: () Source #
type Rep Void | Since: base-4.8.0.0
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
data Sing (a :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
type Sconcat (arg :: NonEmpty Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sconcat (arg :: NonEmpty Void)
type Show_ (arg :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Show type Show_ (arg :: 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) (a6989586621679357949 :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Void type Apply (AbsurdSym0 :: TyFun Void k2 -> Type) (a6989586621679357949 :: Void) = (Absurd a6989586621679357949 :: 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

# Orphan instances

SDecide k => TestCoercion (Sing :: k -> Type) Source # |
Instance details Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) Source #
SDecide k => TestEquality (Sing :: k -> Type) Source # |
Instance details Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) Source #