| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Morley.Util.Sing
Synopsis
- eqI :: forall a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a))) => Maybe (a :~: b)
- geqI :: forall f a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a)), Eq (f b)) => f a -> f b -> Maybe (a :~: b)
- eqParamSing :: forall a1 a2 t. (SingI a1, SingI a2, SDecide (KindOf a1), Eq (t a1)) => t a1 -> t a2 -> Bool
- eqParamSing2 :: forall a1 a2 b1 b2 t. (SingI a1, SingI a2, SingI b1, SingI b2, SDecide (KindOf a1), SDecide (KindOf b1), Eq (t a1 b2)) => t a1 b1 -> t a2 b2 -> Bool
- eqParamSing3 :: forall a1 a2 b1 b2 c1 c2 t. (SingI a1, SingI a2, SingI b1, SingI b2, SingI c1, SingI c2, SDecide (KindOf a1), SDecide (KindOf b1), SDecide (KindOf c1), Eq (t a1 b1 c1)) => t a1 b1 c1 -> t a2 b2 c2 -> Bool
- eqParamMixed3 :: forall instr1 instr2 a1 a2 b1 b2 t. (Typeable instr1, Typeable instr2, SingI a1, SingI a2, SingI b1, SingI b2, SDecide (KindOf a1), SDecide (KindOf b1), Eq (t instr1 a1 b1)) => t instr1 a1 b1 -> t instr2 a2 b2 -> Bool
- castSing :: forall a b t. (SingI a, SingI b, SDecide (KindOf a)) => t a -> Maybe (t b)
- class (forall x. SingI x => SingI (f x)) => SingIOne f
- withSingIOne :: forall f x r. (SingIOne f, SingI x) => (SingI (f x) => r) -> r
- genSingletonsType :: OptionsMonad q => Name -> q [Dec]
Documentation
eqI :: forall a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a))) => Maybe (a :~: b) Source #
Version of testEquality that uses SingI
geqI :: forall f a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a)), Eq (f b)) => f a -> f b -> Maybe (a :~: b) Source #
Singleton-based implementation of geq
eqParamSing :: forall a1 a2 t. (SingI a1, SingI a2, SDecide (KindOf a1), Eq (t a1)) => t a1 -> t a2 -> Bool Source #
Suppose you have a data type X with parameter a and you have
two values: x1 :: X a1 and x2 :: X a2. You can't compare them
using ==, because they have different types. However, you can
compare them using eqParamSing as long as both parameters have
SingI instances and their kind is SDecide.
eqParamSing2 :: forall a1 a2 b1 b2 t. (SingI a1, SingI a2, SingI b1, SingI b2, SDecide (KindOf a1), SDecide (KindOf b1), Eq (t a1 b2)) => t a1 b1 -> t a2 b2 -> Bool Source #
Version of eqParamSing for types with 2 parameters.
eqParamSing3 :: forall a1 a2 b1 b2 c1 c2 t. (SingI a1, SingI a2, SingI b1, SingI b2, SingI c1, SingI c2, SDecide (KindOf a1), SDecide (KindOf b1), SDecide (KindOf c1), Eq (t a1 b1 c1)) => t a1 b1 c1 -> t a2 b2 c2 -> Bool Source #
Version of eqParamSing for types with 3 parameters.
eqParamMixed3 :: forall instr1 instr2 a1 a2 b1 b2 t. (Typeable instr1, Typeable instr2, SingI a1, SingI a2, SingI b1, SingI b2, SDecide (KindOf a1), SDecide (KindOf b1), Eq (t instr1 a1 b1)) => t instr1 a1 b1 -> t instr2 a2 b2 -> Bool Source #
Version of eqParamSing for types with 3 parameters.
class (forall x. SingI x => SingI (f x)) => SingIOne f Source #
A second-order analogue of SingI. This serves the same purpose as the
Data.Singletons. class. However, the SingIOnesingletons
version requires a separate instance for each type in order to support GHC
versions that don't offer QuantifiedConstraints. We only need one instance
for all types.
genSingletonsType :: OptionsMonad q => Name -> q [Dec] Source #