Morley.Util.Sing

Documentation

eqI :: forall a b. (SingI a, SingI b, TestEquality (Sing @(KindOf a))) => Maybe (a :~: b)

Version of testEquality that uses SingI

eqParamSing :: forall a1 a2 t. (SingI a1, SingI a2, SDecide (KindOf a1), Eq (t a1)) => t a1 -> t a2 -> Bool

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

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

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

Version of eqParamSing for types with 3 parameters.

castSing :: forall a b t. (SingI a, SingI b, SDecide (KindOf a)) => t a -> Maybe (t b)

class SingI1 f where

Methods

withSingI1 :: forall x r. SingI x => (SingI (f x) => r) -> r

Instances

SingI1 'TList

Previously, we were using SingI constraints in SingT constructors. That was not so optimal because we have been spending too much space at runtime. Instead of that, we process values of SingT using the function withSingI in those places where the SingI constraint is required. withSingI allows one to create the SingI context for a given Sing.

Defined in Morley.Michelson.Typed.Sing

Methods

withSingI1 :: forall (x :: k) r. SingI x => (SingI ('TList x) => r) -> r

SingI k => SingI1 ('TMap k :: T -> T)

Defined in Morley.Michelson.Typed.Sing

Methods

withSingI1 :: forall (x :: k0) r. SingI x => (SingI ('TMap k x) => r) -> r