Control.Static.Common

Documentation

type family TyCont r (a :: Type) where ...

Type family representing the type of a continuation.

Equations

TyCont r a = a -> r

type TyContSym2 (r6989586621679058218 :: Type) (a6989586621679060060 :: Type) = TyCont r6989586621679058218 a6989586621679060060

data TyContSym1 (r6989586621679058218 :: Type) :: (~>) Type Type where

Constructors

TyContSym1KindInference :: forall r6989586621679058218 a6989586621679060060 arg. SameKind (Apply (TyContSym1 r6989586621679058218) arg) (TyContSym2 r6989586621679058218 arg) => TyContSym1 r6989586621679058218 a6989586621679060060

Instances

SuppressUnusedWarnings (TyContSym1 r6989586621679058218 :: TyFun Type Type -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (TyContSym1 r6989586621679058218 :: TyFun Type Type -> Type) (a6989586621679060060 :: Type)

Defined in Control.Static.Common

type Apply (TyContSym1 r6989586621679058218 :: TyFun Type Type -> Type) (a6989586621679060060 :: Type) = TyCont r6989586621679058218 a6989586621679060060

data TyContSym0 :: (~>) Type ((~>) Type Type) where

Constructors

TyContSym0KindInference :: forall r6989586621679058218 arg. SameKind (Apply TyContSym0 arg) (TyContSym1 arg) => TyContSym0 r6989586621679058218

Instances

SuppressUnusedWarnings TyContSym0

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply TyContSym0 (r6989586621679058218 :: Type)

Defined in Control.Static.Common

type Apply TyContSym0 (r6989586621679058218 :: Type) = TyContSym1 r6989586621679058218

type family TyCont2 r (a1 :: Type) (a2 :: Type) where ...

Type family representing the type of a continuation of 2 args.

Equations

TyCont2 r a1 a2 = a1 -> a2 -> r

type TyCont2Sym3 (r6989586621679070803 :: Type) (a16989586621679070804 :: Type) (a26989586621679070805 :: Type) = TyCont2 r6989586621679070803 a16989586621679070804 a26989586621679070805

data TyCont2Sym2 (r6989586621679070803 :: Type) (a16989586621679070804 :: Type) :: (~>) Type Type where

Constructors

TyCont2Sym2KindInference :: forall r6989586621679070803 a16989586621679070804 a26989586621679070805 arg. SameKind (Apply (TyCont2Sym2 r6989586621679070803 a16989586621679070804) arg) (TyCont2Sym3 r6989586621679070803 a16989586621679070804 arg) => TyCont2Sym2 r6989586621679070803 a16989586621679070804 a26989586621679070805

Instances

SuppressUnusedWarnings (TyCont2Sym2 a16989586621679070804 r6989586621679070803 :: TyFun Type Type -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (TyCont2Sym2 a16989586621679070804 r6989586621679070803 :: TyFun Type Type -> Type) (a26989586621679070805 :: Type)

Defined in Control.Static.Common

type Apply (TyCont2Sym2 a16989586621679070804 r6989586621679070803 :: TyFun Type Type -> Type) (a26989586621679070805 :: Type) = TyCont2 a16989586621679070804 r6989586621679070803 a26989586621679070805

data TyCont2Sym1 (r6989586621679070803 :: Type) :: (~>) Type ((~>) Type Type) where

Constructors

TyCont2Sym1KindInference :: forall r6989586621679070803 a16989586621679070804 arg. SameKind (Apply (TyCont2Sym1 r6989586621679070803) arg) (TyCont2Sym2 r6989586621679070803 arg) => TyCont2Sym1 r6989586621679070803 a16989586621679070804

Instances

SuppressUnusedWarnings (TyCont2Sym1 r6989586621679070803 :: TyFun Type (Type ~> Type) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (TyCont2Sym1 r6989586621679070803 :: TyFun Type (Type ~> Type) -> Type) (a16989586621679070804 :: Type)

Defined in Control.Static.Common

type Apply (TyCont2Sym1 r6989586621679070803 :: TyFun Type (Type ~> Type) -> Type) (a16989586621679070804 :: Type) = TyCont2Sym2 r6989586621679070803 a16989586621679070804

data TyCont2Sym0 :: (~>) Type ((~>) Type ((~>) Type Type)) where

Constructors

TyCont2Sym0KindInference :: forall r6989586621679070803 arg. SameKind (Apply TyCont2Sym0 arg) (TyCont2Sym1 arg) => TyCont2Sym0 r6989586621679070803

Instances

SuppressUnusedWarnings TyCont2Sym0

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply TyCont2Sym0 (r6989586621679070803 :: Type)

Defined in Control.Static.Common

type Apply TyCont2Sym0 (r6989586621679070803 :: Type) = TyCont2Sym1 r6989586621679070803

type family TyCont3 r (a1 :: Type) (a2 :: Type) (a3 :: Type) where ...

Type family representing the type of a continuation of 3 args.

Equations

TyCont3 r a1 a2 a3 = a1 -> a2 -> a3 -> r

type TyCont3Sym4 (r6989586621679127059 :: Type) (a16989586621679127060 :: Type) (a26989586621679127061 :: Type) (a36989586621679127062 :: Type) = TyCont3 r6989586621679127059 a16989586621679127060 a26989586621679127061 a36989586621679127062

data TyCont3Sym3 (r6989586621679127059 :: Type) (a16989586621679127060 :: Type) (a26989586621679127061 :: Type) :: (~>) Type Type where

Constructors

TyCont3Sym3KindInference :: forall r6989586621679127059 a16989586621679127060 a26989586621679127061 a36989586621679127062 arg. SameKind (Apply (TyCont3Sym3 r6989586621679127059 a16989586621679127060 a26989586621679127061) arg) (TyCont3Sym4 r6989586621679127059 a16989586621679127060 a26989586621679127061 arg) => TyCont3Sym3 r6989586621679127059 a16989586621679127060 a26989586621679127061 a36989586621679127062

Instances

SuppressUnusedWarnings (TyCont3Sym3 a26989586621679127061 a16989586621679127060 r6989586621679127059 :: TyFun Type Type -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (TyCont3Sym3 a26989586621679127061 a16989586621679127060 r6989586621679127059 :: TyFun Type Type -> Type) (a36989586621679127062 :: Type)

Defined in Control.Static.Common

type Apply (TyCont3Sym3 a26989586621679127061 a16989586621679127060 r6989586621679127059 :: TyFun Type Type -> Type) (a36989586621679127062 :: Type) = TyCont3 a26989586621679127061 a16989586621679127060 r6989586621679127059 a36989586621679127062

data TyCont3Sym2 (r6989586621679127059 :: Type) (a16989586621679127060 :: Type) :: (~>) Type ((~>) Type Type) where

Constructors

TyCont3Sym2KindInference :: forall r6989586621679127059 a16989586621679127060 a26989586621679127061 arg. SameKind (Apply (TyCont3Sym2 r6989586621679127059 a16989586621679127060) arg) (TyCont3Sym3 r6989586621679127059 a16989586621679127060 arg) => TyCont3Sym2 r6989586621679127059 a16989586621679127060 a26989586621679127061

Instances

SuppressUnusedWarnings (TyCont3Sym2 a16989586621679127060 r6989586621679127059 :: TyFun Type (Type ~> Type) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (TyCont3Sym2 a16989586621679127060 r6989586621679127059 :: TyFun Type (Type ~> Type) -> Type) (a26989586621679127061 :: Type)

Defined in Control.Static.Common

type Apply (TyCont3Sym2 a16989586621679127060 r6989586621679127059 :: TyFun Type (Type ~> Type) -> Type) (a26989586621679127061 :: Type) = TyCont3Sym3 a16989586621679127060 r6989586621679127059 a26989586621679127061

data TyCont3Sym1 (r6989586621679127059 :: Type) :: (~>) Type ((~>) Type ((~>) Type Type)) where

Constructors

TyCont3Sym1KindInference :: forall r6989586621679127059 a16989586621679127060 arg. SameKind (Apply (TyCont3Sym1 r6989586621679127059) arg) (TyCont3Sym2 r6989586621679127059 arg) => TyCont3Sym1 r6989586621679127059 a16989586621679127060

Instances

SuppressUnusedWarnings (TyCont3Sym1 r6989586621679127059 :: TyFun Type (Type ~> (Type ~> Type)) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (TyCont3Sym1 r6989586621679127059 :: TyFun Type (Type ~> (Type ~> Type)) -> Type) (a16989586621679127060 :: Type)

Defined in Control.Static.Common

type Apply (TyCont3Sym1 r6989586621679127059 :: TyFun Type (Type ~> (Type ~> Type)) -> Type) (a16989586621679127060 :: Type) = TyCont3Sym2 r6989586621679127059 a16989586621679127060

data TyCont3Sym0 :: (~>) Type ((~>) Type ((~>) Type ((~>) Type Type))) where

Constructors

TyCont3Sym0KindInference :: forall r6989586621679127059 arg. SameKind (Apply TyCont3Sym0 arg) (TyCont3Sym1 arg) => TyCont3Sym0 r6989586621679127059

Instances

SuppressUnusedWarnings TyCont3Sym0

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply TyCont3Sym0 (r6989586621679127059 :: Type)

Defined in Control.Static.Common

type Apply TyCont3Sym0 (r6989586621679127059 :: Type) = TyCont3Sym1 r6989586621679127059

type family Ap (a :: (~>) x ((~>) y z)) (a :: (~>) x y) (a :: x) :: z where ...

Equations

Ap f g x = Apply (Apply f x) (Apply g x)

type ApSym3 (a6989586621679127912 :: (~>) x6989586621679127905 ((~>) y6989586621679127906 z6989586621679127907)) (a6989586621679127913 :: (~>) x6989586621679127905 y6989586621679127906) (a6989586621679127914 :: x6989586621679127905) = Ap a6989586621679127912 a6989586621679127913 a6989586621679127914

data ApSym2 (a6989586621679127912 :: (~>) x6989586621679127905 ((~>) y6989586621679127906 z6989586621679127907)) (a6989586621679127913 :: (~>) x6989586621679127905 y6989586621679127906) :: (~>) x6989586621679127905 z6989586621679127907 where

Constructors

ApSym2KindInference :: forall a6989586621679127912 a6989586621679127913 a6989586621679127914 arg. SameKind (Apply (ApSym2 a6989586621679127912 a6989586621679127913) arg) (ApSym3 a6989586621679127912 a6989586621679127913 arg) => ApSym2 a6989586621679127912 a6989586621679127913 a6989586621679127914

Instances

SuppressUnusedWarnings (ApSym2 a6989586621679127913 a6989586621679127912 :: TyFun x6989586621679127905 z6989586621679127907 -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SingI d1, SingI d2) => SingI (ApSym2 d1 d2 :: TyFun x z -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (ApSym2 d1 d2)

type Apply (ApSym2 a6989586621679127913 a6989586621679127912 :: TyFun x z -> Type) (a6989586621679127914 :: x)

Defined in Control.Static.Common

type Apply (ApSym2 a6989586621679127913 a6989586621679127912 :: TyFun x z -> Type) (a6989586621679127914 :: x) = Ap a6989586621679127913 a6989586621679127912 a6989586621679127914

data ApSym1 (a6989586621679127912 :: (~>) x6989586621679127905 ((~>) y6989586621679127906 z6989586621679127907)) :: (~>) ((~>) x6989586621679127905 y6989586621679127906) ((~>) x6989586621679127905 z6989586621679127907) where

Constructors

ApSym1KindInference :: forall a6989586621679127912 a6989586621679127913 arg. SameKind (Apply (ApSym1 a6989586621679127912) arg) (ApSym2 a6989586621679127912 arg) => ApSym1 a6989586621679127912 a6989586621679127913

Instances

SuppressUnusedWarnings (ApSym1 a6989586621679127912 :: TyFun (x6989586621679127905 ~> y6989586621679127906) (x6989586621679127905 ~> z6989586621679127907) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

SingI d => SingI (ApSym1 d :: TyFun (x ~> y) (x ~> z) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (ApSym1 d)

type Apply (ApSym1 a6989586621679127912 :: TyFun (x6989586621679127905 ~> y6989586621679127906) (x6989586621679127905 ~> z6989586621679127907) -> Type) (a6989586621679127913 :: x6989586621679127905 ~> y6989586621679127906)

Defined in Control.Static.Common

type Apply (ApSym1 a6989586621679127912 :: TyFun (x6989586621679127905 ~> y6989586621679127906) (x6989586621679127905 ~> z6989586621679127907) -> Type) (a6989586621679127913 :: x6989586621679127905 ~> y6989586621679127906) = ApSym2 a6989586621679127912 a6989586621679127913

data ApSym0 :: forall x6989586621679127905 y6989586621679127906 z6989586621679127907. (~>) ((~>) x6989586621679127905 ((~>) y6989586621679127906 z6989586621679127907)) ((~>) ((~>) x6989586621679127905 y6989586621679127906) ((~>) x6989586621679127905 z6989586621679127907)) where

Constructors

ApSym0KindInference :: forall a6989586621679127912 arg. SameKind (Apply ApSym0 arg) (ApSym1 arg) => ApSym0 a6989586621679127912

Instances

SuppressUnusedWarnings (ApSym0 :: TyFun (x6989586621679127905 ~> (y6989586621679127906 ~> z6989586621679127907)) ((x6989586621679127905 ~> y6989586621679127906) ~> (x6989586621679127905 ~> z6989586621679127907)) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

SingI (ApSym0 :: TyFun (x ~> (y ~> z)) ((x ~> y) ~> (x ~> z)) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing ApSym0

type Apply (ApSym0 :: TyFun (x6989586621679127905 ~> (y6989586621679127906 ~> z6989586621679127907)) ((x6989586621679127905 ~> y6989586621679127906) ~> (x6989586621679127905 ~> z6989586621679127907)) -> Type) (a6989586621679127912 :: x6989586621679127905 ~> (y6989586621679127906 ~> z6989586621679127907))

Defined in Control.Static.Common

type Apply (ApSym0 :: TyFun (x6989586621679127905 ~> (y6989586621679127906 ~> z6989586621679127907)) ((x6989586621679127905 ~> y6989586621679127906) ~> (x6989586621679127905 ~> z6989586621679127907)) -> Type) (a6989586621679127912 :: x6989586621679127905 ~> (y6989586621679127906 ~> z6989586621679127907)) = ApSym1 a6989586621679127912

sAp :: forall x y z (t :: (~>) x ((~>) y z)) (t :: (~>) x y) (t :: x). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ApSym0 t) t) t :: z)

ap :: (x -> y -> z) -> (x -> y) -> x -> z

newtype CxtW c a

Data type wrapping a constraint, to avoid ImpredicativeTypes GHC error.

Constructors

CxtW

Fields

• unCxtW :: c => a

Instances

PreClosure (CxtW c (e -> v -> r))

Defined in Control.Static.Closure

Associated Types

type Cxt (CxtW c (e -> v -> r)) :: Constraint

type Env (CxtW c (e -> v -> r)) :: Type

type Part (CxtW c (e -> v -> r)) :: Type

Methods

applyPre :: CxtW c (e -> v -> r) -> Env (CxtW c (e -> v -> r)) -> Part (CxtW c (e -> v -> r))

type Cxt (CxtW c (e -> v -> r))

Defined in Control.Static.Closure

type Cxt (CxtW c (e -> v -> r)) = c

type Env (CxtW c (e -> v -> r))

Defined in Control.Static.Closure

type Env (CxtW c (e -> v -> r)) = e

type Part (CxtW c (e -> v -> r))

Defined in Control.Static.Closure

type Part (CxtW c (e -> v -> r)) = v -> r

type family ConstrainList (cc :: [Constraint]) :: Constraint where ...

Convert a list of constraints into a single constraint

Equations

ConstrainList '[] = ()

ConstrainList (c ': cc) = (c, ConstrainList cc)

type family NullC (t :: k) :: Constraint where ...

Null constraint over 1 type param.

Equations

NullC t = ()

type NullCSym1 (t6989586621679127945 :: k6989586621679127944) = NullC t6989586621679127945

data NullCSym0 :: forall k6989586621679127944. (~>) k6989586621679127944 Constraint where

Constructors

NullCSym0KindInference :: forall t6989586621679127945 arg. SameKind (Apply NullCSym0 arg) (NullCSym1 arg) => NullCSym0 t6989586621679127945

Instances

SuppressUnusedWarnings (NullCSym0 :: TyFun k6989586621679127944 Constraint -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (NullCSym0 :: TyFun k Constraint -> Type) (t6989586621679127945 :: k)

Defined in Control.Static.Common

type Apply (NullCSym0 :: TyFun k Constraint -> Type) (t6989586621679127945 :: k) = NullC t6989586621679127945

type family NullC2 (t :: k) (t' :: k') :: Constraint where ...

Null constraint over 2 type params.

Equations

NullC2 t t' = ()

type NullC2Sym2 (t6989586621679128932 :: k6989586621679128930) (t'6989586621679128933 :: k'6989586621679128931) = NullC2 t6989586621679128932 t'6989586621679128933

data NullC2Sym1 (t6989586621679128932 :: k6989586621679128930) :: forall k'6989586621679128931. (~>) k'6989586621679128931 Constraint where

Constructors

NullC2Sym1KindInference :: forall t6989586621679128932 t'6989586621679128933 arg. SameKind (Apply (NullC2Sym1 t6989586621679128932) arg) (NullC2Sym2 t6989586621679128932 arg) => NullC2Sym1 t6989586621679128932 t'6989586621679128933

Instances

SuppressUnusedWarnings (NullC2Sym1 t6989586621679128932 k'6989586621679128931 :: TyFun k'6989586621679128931 Constraint -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (NullC2Sym1 t6989586621679128932 k' :: TyFun k' Constraint -> Type) (t'6989586621679128933 :: k')

Defined in Control.Static.Common

type Apply (NullC2Sym1 t6989586621679128932 k' :: TyFun k' Constraint -> Type) (t'6989586621679128933 :: k') = NullC2 t6989586621679128932 t'6989586621679128933

data NullC2Sym0 :: forall k'6989586621679128931 k6989586621679128930. (~>) k6989586621679128930 ((~>) k'6989586621679128931 Constraint) where

Constructors

NullC2Sym0KindInference :: forall t6989586621679128932 arg. SameKind (Apply NullC2Sym0 arg) (NullC2Sym1 arg) => NullC2Sym0 t6989586621679128932

Instances

SuppressUnusedWarnings (NullC2Sym0 :: TyFun k6989586621679128930 (k'6989586621679128931 ~> Constraint) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (NullC2Sym0 :: TyFun k6989586621679128930 (k'6989586621679128931 ~> Constraint) -> Type) (t6989586621679128932 :: k6989586621679128930)

Defined in Control.Static.Common

type Apply (NullC2Sym0 :: TyFun k6989586621679128930 (k'6989586621679128931 ~> Constraint) -> Type) (t6989586621679128932 :: k6989586621679128930) = (NullC2Sym1 t6989586621679128932 k'6989586621679128931 :: TyFun k'6989586621679128931 Constraint -> Type)

type family AndC c0 c1 :: Constraint where ...

Combine two constraints

Equations

AndC c0 c1 = (c0, c1)

type AndCSym2 (c06989586621679129083 :: Constraint) (c16989586621679129084 :: Constraint) = AndC c06989586621679129083 c16989586621679129084

data AndCSym1 (c06989586621679129083 :: Constraint) :: (~>) Constraint Constraint where

Constructors

AndCSym1KindInference :: forall c06989586621679129083 c16989586621679129084 arg. SameKind (Apply (AndCSym1 c06989586621679129083) arg) (AndCSym2 c06989586621679129083 arg) => AndCSym1 c06989586621679129083 c16989586621679129084

Instances

SuppressUnusedWarnings (AndCSym1 c06989586621679129083 :: TyFun Constraint Constraint -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (AndCSym1 c06989586621679129083 :: TyFun Constraint Constraint -> Type) (c16989586621679129084 :: Constraint)

Defined in Control.Static.Common

type Apply (AndCSym1 c06989586621679129083 :: TyFun Constraint Constraint -> Type) (c16989586621679129084 :: Constraint) = AndC c06989586621679129083 c16989586621679129084

data AndCSym0 :: (~>) Constraint ((~>) Constraint Constraint) where

Constructors

AndCSym0KindInference :: forall c06989586621679129083 arg. SameKind (Apply AndCSym0 arg) (AndCSym1 arg) => AndCSym0 c06989586621679129083

Instances

SuppressUnusedWarnings AndCSym0

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply AndCSym0 (c06989586621679129083 :: Constraint)

Defined in Control.Static.Common

type Apply AndCSym0 (c06989586621679129083 :: Constraint) = AndCSym1 c06989586621679129083

type AndC1 c0 c1 = ApSym2 (AndCSym0 .@#@$$$ c0) c1

Combine two constraint constructors into a single constraint constructor.

This is analogous to the term-level idiom ap ((,) . c0) c1 that combines two functions c0, c1 into a single one.

type AndC2 c0 c1 = ApSym2 (ApSym0 .@#@$$$ ((.@#@$$) AndCSym0 .@#@$$$ c0)) c1

Combine two constraint constructors, each taking 2 type params, into a single constraint constructor taking 2 type params.

This is analogous to the term-level idiom ap (ap . ((,) .) . c0) c1 that combines two functions c0, c1 that each take 2 params, into a single one.

type family Class2 c0 c1 t t' where ...

Entailment over 2 type params.

Equations

Class2 c0 c1 t t' = Class ((c0 @@ t) @@ t') ((c1 @@ t) @@ t')

type Class2Sym4 (c06989586621679129378 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) (c16989586621679129379 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) (t6989586621679129380 :: k16989586621679129616) (t'6989586621679129381 :: k16989586621679129614) = Class2 c06989586621679129378 c16989586621679129379 t6989586621679129380 t'6989586621679129381

data Class2Sym3 (c06989586621679129378 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) (c16989586621679129379 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) (t6989586621679129380 :: k16989586621679129616) :: (~>) k16989586621679129614 Constraint where

Constructors

Class2Sym3KindInference :: forall c06989586621679129378 c16989586621679129379 t6989586621679129380 t'6989586621679129381 arg. SameKind (Apply (Class2Sym3 c06989586621679129378 c16989586621679129379 t6989586621679129380) arg) (Class2Sym4 c06989586621679129378 c16989586621679129379 t6989586621679129380 arg) => Class2Sym3 c06989586621679129378 c16989586621679129379 t6989586621679129380 t'6989586621679129381

Instances

SuppressUnusedWarnings (Class2Sym3 t6989586621679129380 c16989586621679129379 c06989586621679129378 :: TyFun k16989586621679129614 Constraint -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (Class2Sym3 t6989586621679129380 c16989586621679129379 c06989586621679129378 :: TyFun k3 Constraint -> Type) (t'6989586621679129381 :: k3)

Defined in Control.Static.Common

type Apply (Class2Sym3 t6989586621679129380 c16989586621679129379 c06989586621679129378 :: TyFun k3 Constraint -> Type) (t'6989586621679129381 :: k3) = Class2 t6989586621679129380 c16989586621679129379 c06989586621679129378 t'6989586621679129381

data Class2Sym2 (c06989586621679129378 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) (c16989586621679129379 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint) where

Constructors

Class2Sym2KindInference :: forall c06989586621679129378 c16989586621679129379 t6989586621679129380 arg. SameKind (Apply (Class2Sym2 c06989586621679129378 c16989586621679129379) arg) (Class2Sym3 c06989586621679129378 c16989586621679129379 arg) => Class2Sym2 c06989586621679129378 c16989586621679129379 t6989586621679129380

Instances

SuppressUnusedWarnings (Class2Sym2 c16989586621679129379 c06989586621679129378 :: TyFun k16989586621679129616 (k16989586621679129614 ~> Constraint) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (Class2Sym2 c16989586621679129379 c06989586621679129378 :: TyFun k16989586621679129616 (k16989586621679129614 ~> Constraint) -> Type) (t6989586621679129380 :: k16989586621679129616)

Defined in Control.Static.Common

type Apply (Class2Sym2 c16989586621679129379 c06989586621679129378 :: TyFun k16989586621679129616 (k16989586621679129614 ~> Constraint) -> Type) (t6989586621679129380 :: k16989586621679129616) = Class2Sym3 c16989586621679129379 c06989586621679129378 t6989586621679129380

data Class2Sym1 (c06989586621679129378 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) :: (~>) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) where

Constructors

Class2Sym1KindInference :: forall c06989586621679129378 c16989586621679129379 arg. SameKind (Apply (Class2Sym1 c06989586621679129378) arg) (Class2Sym2 c06989586621679129378 arg) => Class2Sym1 c06989586621679129378 c16989586621679129379

Instances

SuppressUnusedWarnings (Class2Sym1 c06989586621679129378 :: TyFun (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (Class2Sym1 c06989586621679129378 :: TyFun (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) -> Type) (c16989586621679129379 :: k16989586621679129616 ~> (k16989586621679129614 ~> Constraint))

Defined in Control.Static.Common

type Apply (Class2Sym1 c06989586621679129378 :: TyFun (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) -> Type) (c16989586621679129379 :: k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) = Class2Sym2 c06989586621679129378 c16989586621679129379

data Class2Sym0 :: forall k16989586621679129614 k16989586621679129616. (~>) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) ((~>) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint))) where

Constructors

Class2Sym0KindInference :: forall c06989586621679129378 arg. SameKind (Apply Class2Sym0 arg) (Class2Sym1 arg) => Class2Sym0 c06989586621679129378

Instances

SuppressUnusedWarnings (Class2Sym0 :: TyFun (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) ((k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) ~> (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint))) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

type Apply (Class2Sym0 :: TyFun (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) ((k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) ~> (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint))) -> Type) (c06989586621679129378 :: k16989586621679129616 ~> (k16989586621679129614 ~> Constraint))

Defined in Control.Static.Common

type Apply (Class2Sym0 :: TyFun (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) ((k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) ~> (k16989586621679129616 ~> (k16989586621679129614 ~> Constraint))) -> Type) (c06989586621679129378 :: k16989586621679129616 ~> (k16989586621679129614 ~> Constraint)) = Class2Sym1 c06989586621679129378

type family LookupKV_If (a :: k) (a :: k) (a :: [k]) (a :: v) (a :: [v]) (a :: Bool) :: Maybe (k, v) where ...

Equations

LookupKV_If k k' _ v' _ True = Apply JustSym0 (Apply (Apply Tuple2Sym0 k') v')

LookupKV_If k _ kk _ vv False = Apply (Apply (Apply LookupKVSym0 k) kk) vv

data LookupKVSym0 :: forall k6989586621679130586 v6989586621679130587. (~>) k6989586621679130586 ((~>) [k6989586621679130586] ((~>) [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587)))) where

Constructors

LookupKVSym0KindInference :: forall a6989586621679135078 arg. SameKind (Apply LookupKVSym0 arg) (LookupKVSym1 arg) => LookupKVSym0 a6989586621679135078

Instances

SuppressUnusedWarnings (LookupKVSym0 :: TyFun k6989586621679130586 ([k6989586621679130586] ~> ([v6989586621679130587] ~> Maybe (k6989586621679130586, v6989586621679130587))) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

SEq k => SingI (LookupKVSym0 :: TyFun k ([k] ~> ([v] ~> Maybe (k, v))) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing LookupKVSym0

type Apply (LookupKVSym0 :: TyFun k6989586621679130586 ([k6989586621679130586] ~> ([v6989586621679130587] ~> Maybe (k6989586621679130586, v6989586621679130587))) -> Type) (a6989586621679135078 :: k6989586621679130586)

Defined in Control.Static.Common

type Apply (LookupKVSym0 :: TyFun k6989586621679130586 ([k6989586621679130586] ~> ([v6989586621679130587] ~> Maybe (k6989586621679130586, v6989586621679130587))) -> Type) (a6989586621679135078 :: k6989586621679130586) = (LookupKVSym1 a6989586621679135078 v6989586621679130587 :: TyFun [k6989586621679130586] ([v6989586621679130587] ~> Maybe (k6989586621679130586, v6989586621679130587)) -> Type)

data LookupKVSym1 (a6989586621679135078 :: k6989586621679130586) :: forall v6989586621679130587. (~>) [k6989586621679130586] ((~>) [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587))) where

Constructors

LookupKVSym1KindInference :: forall a6989586621679135078 a6989586621679135079 arg. SameKind (Apply (LookupKVSym1 a6989586621679135078) arg) (LookupKVSym2 a6989586621679135078 arg) => LookupKVSym1 a6989586621679135078 a6989586621679135079

Instances

SuppressUnusedWarnings (LookupKVSym1 a6989586621679135078 v6989586621679130587 :: TyFun [k6989586621679130586] ([v6989586621679130587] ~> Maybe (k6989586621679130586, v6989586621679130587)) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SEq k, SingI d) => SingI (LookupKVSym1 d v :: TyFun [k] ([v] ~> Maybe (k, v)) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (LookupKVSym1 d v)

type Apply (LookupKVSym1 a6989586621679135078 v6989586621679130587 :: TyFun [k6989586621679130586] ([v6989586621679130587] ~> Maybe (k6989586621679130586, v6989586621679130587)) -> Type) (a6989586621679135079 :: [k6989586621679130586])

Defined in Control.Static.Common

type Apply (LookupKVSym1 a6989586621679135078 v6989586621679130587 :: TyFun [k6989586621679130586] ([v6989586621679130587] ~> Maybe (k6989586621679130586, v6989586621679130587)) -> Type) (a6989586621679135079 :: [k6989586621679130586]) = (LookupKVSym2 a6989586621679135078 a6989586621679135079 v6989586621679130587 :: TyFun [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587)) -> Type)

data LookupKVSym2 (a6989586621679135078 :: k6989586621679130586) (a6989586621679135079 :: [k6989586621679130586]) :: forall v6989586621679130587. (~>) [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587)) where

Constructors

LookupKVSym2KindInference :: forall a6989586621679135078 a6989586621679135079 a6989586621679135080 arg. SameKind (Apply (LookupKVSym2 a6989586621679135078 a6989586621679135079) arg) (LookupKVSym3 a6989586621679135078 a6989586621679135079 arg) => LookupKVSym2 a6989586621679135078 a6989586621679135079 a6989586621679135080

Instances

SuppressUnusedWarnings (LookupKVSym2 a6989586621679135079 a6989586621679135078 v6989586621679130587 :: TyFun [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587)) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SEq k, SingI d1, SingI d2) => SingI (LookupKVSym2 d1 d2 v :: TyFun [v] (Maybe (k, v)) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (LookupKVSym2 d1 d2 v)

type Apply (LookupKVSym2 a6989586621679135079 a6989586621679135078 v :: TyFun [v] (Maybe (k, v)) -> Type) (a6989586621679135080 :: [v])

Defined in Control.Static.Common

type Apply (LookupKVSym2 a6989586621679135079 a6989586621679135078 v :: TyFun [v] (Maybe (k, v)) -> Type) (a6989586621679135080 :: [v]) = LookupKV a6989586621679135079 a6989586621679135078 a6989586621679135080

type LookupKVSym3 (a6989586621679135078 :: k6989586621679130586) (a6989586621679135079 :: [k6989586621679130586]) (a6989586621679135080 :: [v6989586621679130587]) = LookupKV a6989586621679135078 a6989586621679135079 a6989586621679135080

type family LookupKV (a :: k) (a :: [k]) (a :: [v]) :: Maybe (k, v) where ...

Equations

LookupKV k '[] '[] = NothingSym0

LookupKV k ((:) k' kk) ((:) v' vv) = Apply (Apply (Apply (Apply (Apply (Apply LookupKV_IfSym0 k) k') kk) v') vv) (Apply (Apply (==@#@$) k) k')

data LookupKV_IfSym0 :: forall k6989586621679130584 v6989586621679130585. (~>) k6989586621679130584 ((~>) k6989586621679130584 ((~>) [k6989586621679130584] ((~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585))))))) where

Constructors

LookupKV_IfSym0KindInference :: forall a6989586621679135090 arg. SameKind (Apply LookupKV_IfSym0 arg) (LookupKV_IfSym1 arg) => LookupKV_IfSym0 a6989586621679135090

Instances

SuppressUnusedWarnings (LookupKV_IfSym0 :: TyFun k6989586621679130584 (k6989586621679130584 ~> ([k6989586621679130584] ~> (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)))))) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

SEq k => SingI (LookupKV_IfSym0 :: TyFun k (k ~> ([k] ~> (v ~> ([v] ~> (Bool ~> Maybe (k, v)))))) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing LookupKV_IfSym0

type Apply (LookupKV_IfSym0 :: TyFun k6989586621679130584 (k6989586621679130584 ~> ([k6989586621679130584] ~> (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)))))) -> Type) (a6989586621679135090 :: k6989586621679130584)

Defined in Control.Static.Common

type Apply (LookupKV_IfSym0 :: TyFun k6989586621679130584 (k6989586621679130584 ~> ([k6989586621679130584] ~> (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)))))) -> Type) (a6989586621679135090 :: k6989586621679130584) = (LookupKV_IfSym1 a6989586621679135090 v6989586621679130585 :: TyFun k6989586621679130584 ([k6989586621679130584] ~> (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))))) -> Type)

data LookupKV_IfSym1 (a6989586621679135090 :: k6989586621679130584) :: forall v6989586621679130585. (~>) k6989586621679130584 ((~>) [k6989586621679130584] ((~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585)))))) where

Constructors

LookupKV_IfSym1KindInference :: forall a6989586621679135090 a6989586621679135091 arg. SameKind (Apply (LookupKV_IfSym1 a6989586621679135090) arg) (LookupKV_IfSym2 a6989586621679135090 arg) => LookupKV_IfSym1 a6989586621679135090 a6989586621679135091

Instances

SuppressUnusedWarnings (LookupKV_IfSym1 a6989586621679135090 v6989586621679130585 :: TyFun k6989586621679130584 ([k6989586621679130584] ~> (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))))) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SEq k, SingI d) => SingI (LookupKV_IfSym1 d v :: TyFun k ([k] ~> (v ~> ([v] ~> (Bool ~> Maybe (k, v))))) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (LookupKV_IfSym1 d v)

type Apply (LookupKV_IfSym1 a6989586621679135090 v6989586621679130585 :: TyFun k6989586621679130584 ([k6989586621679130584] ~> (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))))) -> Type) (a6989586621679135091 :: k6989586621679130584)

Defined in Control.Static.Common

type Apply (LookupKV_IfSym1 a6989586621679135090 v6989586621679130585 :: TyFun k6989586621679130584 ([k6989586621679130584] ~> (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))))) -> Type) (a6989586621679135091 :: k6989586621679130584) = (LookupKV_IfSym2 a6989586621679135090 a6989586621679135091 v6989586621679130585 :: TyFun [k6989586621679130584] (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)))) -> Type)

data LookupKV_IfSym2 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) :: forall v6989586621679130585. (~>) [k6989586621679130584] ((~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585))))) where

Constructors

LookupKV_IfSym2KindInference :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 arg. SameKind (Apply (LookupKV_IfSym2 a6989586621679135090 a6989586621679135091) arg) (LookupKV_IfSym3 a6989586621679135090 a6989586621679135091 arg) => LookupKV_IfSym2 a6989586621679135090 a6989586621679135091 a6989586621679135092

Instances

SuppressUnusedWarnings (LookupKV_IfSym2 a6989586621679135091 a6989586621679135090 v6989586621679130585 :: TyFun [k6989586621679130584] (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)))) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SEq k, SingI d1, SingI d2) => SingI (LookupKV_IfSym2 d1 d2 v :: TyFun [k] (v ~> ([v] ~> (Bool ~> Maybe (k, v)))) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (LookupKV_IfSym2 d1 d2 v)

type Apply (LookupKV_IfSym2 a6989586621679135091 a6989586621679135090 v6989586621679130585 :: TyFun [k6989586621679130584] (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)))) -> Type) (a6989586621679135092 :: [k6989586621679130584])

Defined in Control.Static.Common

type Apply (LookupKV_IfSym2 a6989586621679135091 a6989586621679135090 v6989586621679130585 :: TyFun [k6989586621679130584] (v6989586621679130585 ~> ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)))) -> Type) (a6989586621679135092 :: [k6989586621679130584]) = (LookupKV_IfSym3 a6989586621679135091 a6989586621679135090 a6989586621679135092 v6989586621679130585 :: TyFun v6989586621679130585 ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))) -> Type)

data LookupKV_IfSym3 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) :: forall v6989586621679130585. (~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585)))) where

Constructors

LookupKV_IfSym3KindInference :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 arg. SameKind (Apply (LookupKV_IfSym3 a6989586621679135090 a6989586621679135091 a6989586621679135092) arg) (LookupKV_IfSym4 a6989586621679135090 a6989586621679135091 a6989586621679135092 arg) => LookupKV_IfSym3 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093

Instances

SuppressUnusedWarnings (LookupKV_IfSym3 a6989586621679135092 a6989586621679135091 a6989586621679135090 v6989586621679130585 :: TyFun v6989586621679130585 ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SEq k, SingI d1, SingI d2, SingI d3) => SingI (LookupKV_IfSym3 d1 d2 d3 v :: TyFun v ([v] ~> (Bool ~> Maybe (k, v))) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (LookupKV_IfSym3 d1 d2 d3 v)

type Apply (LookupKV_IfSym3 a6989586621679135092 a6989586621679135091 a6989586621679135090 v6989586621679130585 :: TyFun v6989586621679130585 ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))) -> Type) (a6989586621679135093 :: v6989586621679130585)

Defined in Control.Static.Common

type Apply (LookupKV_IfSym3 a6989586621679135092 a6989586621679135091 a6989586621679135090 v6989586621679130585 :: TyFun v6989586621679130585 ([v6989586621679130585] ~> (Bool ~> Maybe (k6989586621679130584, v6989586621679130585))) -> Type) (a6989586621679135093 :: v6989586621679130585) = LookupKV_IfSym4 a6989586621679135092 a6989586621679135091 a6989586621679135090 a6989586621679135093

data LookupKV_IfSym4 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) (a6989586621679135093 :: v6989586621679130585) :: (~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585))) where

Constructors

LookupKV_IfSym4KindInference :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 arg. SameKind (Apply (LookupKV_IfSym4 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093) arg) (LookupKV_IfSym5 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 arg) => LookupKV_IfSym4 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094

Instances

SuppressUnusedWarnings (LookupKV_IfSym4 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 :: TyFun [v6989586621679130585] (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SEq k, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LookupKV_IfSym4 d1 d2 d3 d4 :: TyFun [v] (Bool ~> Maybe (k, v)) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (LookupKV_IfSym4 d1 d2 d3 d4)

type Apply (LookupKV_IfSym4 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 :: TyFun [v6989586621679130585] (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)) -> Type) (a6989586621679135094 :: [v6989586621679130585])

Defined in Control.Static.Common

type Apply (LookupKV_IfSym4 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 :: TyFun [v6989586621679130585] (Bool ~> Maybe (k6989586621679130584, v6989586621679130585)) -> Type) (a6989586621679135094 :: [v6989586621679130585]) = LookupKV_IfSym5 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 a6989586621679135094

data LookupKV_IfSym5 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) (a6989586621679135093 :: v6989586621679130585) (a6989586621679135094 :: [v6989586621679130585]) :: (~>) Bool (Maybe (k6989586621679130584, v6989586621679130585)) where

Constructors

LookupKV_IfSym5KindInference :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 a6989586621679135095 arg. SameKind (Apply (LookupKV_IfSym5 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094) arg) (LookupKV_IfSym6 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 arg) => LookupKV_IfSym5 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 a6989586621679135095

Instances

SuppressUnusedWarnings (LookupKV_IfSym5 a6989586621679135094 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 :: TyFun Bool (Maybe (k6989586621679130584, v6989586621679130585)) -> Type)

Defined in Control.Static.Common

Methods

suppressUnusedWarnings :: ()

(SEq k, SingI d1, SingI d2, SingI d3, SingI d4, SingI d5) => SingI (LookupKV_IfSym5 d1 d2 d3 d4 d5 :: TyFun Bool (Maybe (k, v)) -> Type)

Defined in Control.Static.Common

Methods

sing :: Sing (LookupKV_IfSym5 d1 d2 d3 d4 d5)

type Apply (LookupKV_IfSym5 a6989586621679135094 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 :: TyFun Bool (Maybe (k, v)) -> Type) (a6989586621679135095 :: Bool)

Defined in Control.Static.Common

type Apply (LookupKV_IfSym5 a6989586621679135094 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 :: TyFun Bool (Maybe (k, v)) -> Type) (a6989586621679135095 :: Bool) = LookupKV_If a6989586621679135094 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090 a6989586621679135095

type LookupKV_IfSym6 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) (a6989586621679135093 :: v6989586621679130585) (a6989586621679135094 :: [v6989586621679130585]) (a6989586621679135095 :: Bool) = LookupKV_If a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 a6989586621679135095

sLookupKV_If :: forall k v (t :: k) (t :: k) (t :: [k]) (t :: v) (t :: [v]) (t :: Bool). SEq k => Sing t -> Sing t -> Sing t -> Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (Apply (Apply (Apply LookupKV_IfSym0 t) t) t) t) t) t :: Maybe (k, v))

sLookupKV :: forall k v (t :: k) (t :: [k]) (t :: [v]). SEq k => Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LookupKVSym0 t) t) t :: Maybe (k, v))

lookupKV_If :: Eq k => k -> k -> [k] -> v -> [v] -> Bool -> Maybe (k, v)

lookupKV :: Eq k => k -> [k] -> [v] -> Maybe (k, v)

class Fmap (FmapSym1 f) (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv) => ProofLookupKV f k (kk :: [kt]) vv

Instances

ProofLookupKV (f :: a ~> v) (k :: kt) ([] :: [kt]) ([] :: [a])

Defined in Control.Static.Common

ProofLookupKV_If f k k' kk v' vv (k == k') => ProofLookupKV (f :: a ~> v) (k :: kt) (k' ': kk :: [kt]) (v' ': vv :: [a])

Defined in Control.Static.Common

class Fmap (FmapSym1 f) (LookupKV_If k k' kk v' vv eq) ~ LookupKV_If k k' kk (f @@ v') (Fmap f vv) eq => ProofLookupKV_If f (k :: kt) k' kk v' vv eq

Instances

ProofLookupKV f k kk vv => ProofLookupKV_If (f :: a ~> b) (k :: kt) (k' :: kt) (kk :: [kt]) (v' :: a) (vv :: [a]) False

Defined in Control.Static.Common

ProofLookupKV_If (f :: a ~> b) (k :: kt) (k' :: kt) (kk :: [kt]) (v' :: a) (vv :: [a]) True

Defined in Control.Static.Common

data TMaybe (t :: Maybe k) where

Maybe that carries its type.

Constructors

TNothing :: TMaybe Nothing

TJust :: !t -> TMaybe (Just t)

data TCTab (c :: kt ~> (Type ~> Constraint)) (kk :: [kt]) (vv :: [Type]) :: Type where

Heterogeneous constrained table.

Constructors

TCNil :: TCTab c '[] '[]

TCCons :: (c @@ k) @@ v => !(Sing (k :: kt)) -> !v -> !(TCTab c kk vv) -> TCTab c (k ': kk) (v ': vv)

type TCTab' c = TCTab (ConstSym1 (TyCon1 c))

A TCTab with a constraint that applies only to the value, not the key.

type TTab = TCTab NullC2Sym0

Heterogeneous unconstrained table.

To add or remove constraints, see strengthenTC0, strengthenTC and weakenTC.

data TCMaybe c (t :: Maybe (kt, Type)) where

Result type of lookupTC.

Constructors

TCNothing :: TCMaybe c Nothing

TCJust :: Dict ((c @@ k) @@ v) -> !(Sing k) -> !v -> TCMaybe c (Just '(k, v))

lookupTC :: forall kt c f (k :: kt) (kk :: [kt]) vv. SEq kt => Sing k -> TCTab c kk vv -> (TCMaybe c (LookupKV k kk vv), Dict (ProofLookupKV f k kk vv))

Lookup an element in the table, and generate some proofs about the result that can be used by the caller.

lookupTC2 :: forall kt c0 c1 f (k :: kt) (kk :: [kt]) vv. SEq kt => Sing k -> TCTab c0 kk vv -> TCTab c1 kk (Fmap f vv) -> (TCMaybe c0 (LookupKV k kk vv), TCMaybe c1 (Fmap (FmapSym1 f) (LookupKV k kk vv)))

Lookup two elements in two related tables.

The types of the outputs are provably related.

zipWithTC :: forall kt c0 c1 cr f1 r (kk :: [kt]) vv. TCTab c0 kk vv -> TCTab c1 kk (Fmap f1 vv) -> (forall k0 k1 v. (c0 @@ k0) @@ v => (c1 @@ k1) @@ (f1 @@ v) => Sing k0 -> v -> Sing k1 -> (f1 @@ v) -> (r @@ v, Dict ((cr @@ k0) @@ (r @@ v)))) -> TCTab cr kk (Fmap r vv)

Zip two related tables, giving a third table related to both.

The types of the outputs are provably related.

zipWith3TC :: forall kt c0 c1 c2 cr f1 f2 r (kk :: [kt]) vv. TCTab c0 kk vv -> TCTab c1 kk (Fmap f1 vv) -> TCTab c2 kk (Fmap f2 vv) -> (forall k0 k1 k2 v. (c0 @@ k0) @@ v => (c1 @@ k1) @@ (f1 @@ v) => (c2 @@ k2) @@ (f2 @@ v) => Sing k0 -> v -> Sing k1 -> (f1 @@ v) -> Sing k2 -> (f2 @@ v) -> (r @@ v, Dict ((cr @@ k0) @@ (r @@ v)))) -> TCTab cr kk (Fmap r vv)

Zip three related tables, giving a fourth table related to both.

The types of the outputs are provably related.

type DictOf c = TyCon1 Dict .@#@$$$ c

withTCDict :: forall kt c0 c (kk :: [kt]) vv r. TCTab c0 kk vv -> TTab kk (Fmap (DictOf c) vv) -> (ConstrainList (Fmap c vv) => r) -> r

toTCDict :: forall kt c0 c (kk :: [kt]) vv. ConstrainList (Fmap c vv) => TCTab c0 kk vv -> TTab kk (Fmap (DictOf c) vv)

weakenTC :: forall kt c0 c1 (kk :: [kt]) vv. ConstrainList (ZipWith (Class2Sym2 c1 c0) kk vv) => TCTab c0 kk vv -> TCTab c1 kk vv

Weaken the constraint on a TCTab.

strengthenTC :: forall kt c0 c1 (kk :: [kt]) vv. ConstrainList (ZipWith c1 kk vv) => TCTab c0 kk vv -> TCTab (AndC2 c0 c1) kk vv

Strengthen the constraint on a TCTab.

strengthenTC0 :: forall kt c1 (kk :: [kt]) vv. ConstrainList (ZipWith c1 kk vv) => TTab kk vv -> TCTab c1 kk vv

Strengthen the constraint on a TTab.