-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type-safe and interoperable static values and closures
--   
--   Serialise closures in a type-safe way that interoperates across
--   binaries.
--   
--   This package is inspired by <tt>distributed-static</tt> and GHC's
--   <i>static pointers</i> in <tt>GHC.StaticPtr</tt>, which came out of
--   the same research. However, we make some significantly-different
--   design choices, described below.
--   
--   GHC made the design choice to focus on guaranteeing that static values
--   could be passed between nodes if they were running the exact same
--   binary, since they are indexed by 64-bit integers
--   automatically-generated by the compiler. <tt>distributed-static</tt>
--   attempts to support the same source program compiled by different
--   versions of GHC. As part of this effort to preserve stability, one
--   must pass in a table (<a>RemoteTable</a>) whose keys represent the
--   stability, and whose values are resolved potentially differently
--   across compiler versions.
--   
--   The need for the caller to pass in a <a>RemoteTable</a> is seen as a
--   liability, so two subsequent packages <tt>distributed-closure</tt> and
--   <tt>static-closure</tt> take the opposite approach, ripping out the
--   <a>RemoteTable</a> but doubling down on GHC's choice to guarantee
--   compatibility only across different processes running the exact same
--   binary program. Their uses cases are focused around compute clusters
--   and other forms of centralised distributed computing, where this is
--   easy to achieve and not a problem.
--   
--   Sometimes security is cited as a reason to have this restriction, but
--   this is a <i>bogus argument</i>. "Guarantee compatibility only across
--   same binary" means "same binary =&gt; compatibility" whereas the bogus
--   security argument depends on "compatibility =&gt; same binary", which
--   is not true - anyone who analyses your binary will know which numbers
--   to spoof, to convince your program via this interface that they are
--   "running the same code". Guaranteeing "same binary" in an adversial
--   setting is in fact extremely hard and cannot be achieved perfectly; in
--   the real-world it can only be approximated, and should be done so via
--   mechanisms designed for it, not via numbers that are slightly hard to
--   brute force at best and trivial to find out at worst.
--   
--   This package makes the <i>opposite</i> choice, intended for less
--   restricted and more open distributed computing environments such as
--   the internet and decentralised protocols. In these contexts, the
--   requirement of running the exact same binary program is impossible to
--   achieve in practise. Furthermore, we see it as an <i>advantage</i>
--   that code does not need to be exactly the same - for example, one can
--   serialise a closure and its inputs, <i>upgrade your code</i>, then
--   resume running the closure on the same deserialised input arguments
--   but with a bugfixed closure. The necessity to pass in an explicit
--   <a>RemoteTable</a> (here simply called <a>staticTab</a>) is not a
--   liability, but a useful tool to represent high-level compatibility and
--   interoperability. Two nodes with the same keys in their
--   <a>staticTab</a>s, know that they can talk to each other interoperably
--   even if their implementations differ significantly. One node that
--   wishes to talk to different nodes running different minor versions of
--   the same protocol, could instantiate two different <a>staticTab</a>s
--   with the same keys but different implementations, to handle
--   behavioural nuances between the minor versions. In general, it's a
--   useful bit of metadata to keep around in your program code, and can
--   help you perform smooth upgrades of a non-centralised networking
--   protocol more easily.
--   
--   There are also a few technical differences between this and
--   <tt>distributed-static</tt>, some of which could be re-adopted there
--   too:
--   
--   <ul>
--   <li>We use dependent-types and type-level programming to guarantee
--   type safety, rather than <a>Rank1Dynamic</a>. This enables us to store
--   all possible closure types instead of just rank-1 polymorphic
--   functions, including but not limited to: rank-n functions, functions
--   with constraints, those using higher-kinded types, etc.</li>
--   <li>Our serialisation typeclasses are designed to interoperate with
--   many different serialisation frameworks. Instances for
--   <a>Data.Binary</a> and <a>Codec.Serialise</a> are provided here for
--   convenience.</li>
--   <li>We have additional Template Haskell splices that support creating
--   static values from top-level definitions that must refer to other
--   static values, whether they be recursive or mutually-recursive or
--   neither. This is achieved using an implementation of <tt>mfix</tt> for
--   the <tt>Q</tt> monad.</li>
--   </ul>
--   
--   We did <i>not</i> implement the ability to compose static references.
--   The main reason is that, in our view, the <i>purpose</i> of static
--   closures is to represent which top-level tasks to execute, and the
--   inputs to execute it on. This is the <i>interface</i> or
--   <i>contract</i> of this concept. <i>How you run</i> the task is an
--   implementation detail, and as discussed above, this might be different
--   across different machines or as time passes and we upgrade the code.
--   Therefore it makes no sense to serialise a representation of "task A
--   is the composition of closure B and closure C", because it is
--   irrelevant to the <i>interface</i>.
--   
--   If your <i>interface</i> is actually "run arbitrary user-defined code"
--   (e.g. in a VM or EDSL evaluator) then it would indeed make sense to
--   support composition, but then you should define your own AST,
--   evaluator, and serialiser for this; and pass the ASTs around as
--   regular runtime values, not static values. Supporting arbitrary ASTs
--   like this is outside of the scope of this library.
--   
--   Further, in Haskell there are many ways of applying values not just
--   <tt>(_ :: a -&gt; b) (_ :: a) :: b</tt>, e.g. with constraints, with a
--   combination of static and non-static arguments, with type
--   applications, and so on. Only the simple form <tt>(_ :: a -&gt; b) (_
--   :: a) :: b</tt> is likely to be interoperable across multiple
--   languages. Supporting AST statics would therefore unnecessarily
--   restrict how we can implement the behaviour of a static closure in our
--   chosen language.
--   
--   See unit tests for example usage, e.g. <a>UnitTests</a>
@package static
@version 0.1.0.0

module Control.Static.Common

-- | Type family representing the type of a continuation.
type family TyCont r (a :: Type)
type TyContSym2 (r6989586621679058218 :: Type) (a6989586621679060060 :: Type) = TyCont r6989586621679058218 a6989586621679060060
data TyContSym1 (r6989586621679058218 :: Type) :: (~>) Type Type
[TyContSym1KindInference] :: forall r6989586621679058218 a6989586621679060060 arg_afRV. SameKind (Apply (TyContSym1 r6989586621679058218) arg_afRV) (TyContSym2 r6989586621679058218 arg_afRV) => TyContSym1 r6989586621679058218 a6989586621679060060
data TyContSym0 :: (~>) Type ((~>) Type Type)
[TyContSym0KindInference] :: forall r6989586621679058218 arg_afRW. SameKind (Apply TyContSym0 arg_afRW) (TyContSym1 arg_afRW) => TyContSym0 r6989586621679058218

-- | Type family representing the type of a continuation of 2 args.
type family TyCont2 r (a1 :: Type) (a2 :: Type)
type TyCont2Sym3 (r6989586621679070803 :: Type) (a16989586621679070804 :: Type) (a26989586621679070805 :: Type) = TyCont2 r6989586621679070803 a16989586621679070804 a26989586621679070805
data TyCont2Sym2 (r6989586621679070803 :: Type) (a16989586621679070804 :: Type) :: (~>) Type Type
[TyCont2Sym2KindInference] :: forall r6989586621679070803 a16989586621679070804 a26989586621679070805 arg_auve. SameKind (Apply (TyCont2Sym2 r6989586621679070803 a16989586621679070804) arg_auve) (TyCont2Sym3 r6989586621679070803 a16989586621679070804 arg_auve) => TyCont2Sym2 r6989586621679070803 a16989586621679070804 a26989586621679070805
data TyCont2Sym1 (r6989586621679070803 :: Type) :: (~>) Type ((~>) Type Type)
[TyCont2Sym1KindInference] :: forall r6989586621679070803 a16989586621679070804 arg_auvf. SameKind (Apply (TyCont2Sym1 r6989586621679070803) arg_auvf) (TyCont2Sym2 r6989586621679070803 arg_auvf) => TyCont2Sym1 r6989586621679070803 a16989586621679070804
data TyCont2Sym0 :: (~>) Type ((~>) Type ((~>) Type Type))
[TyCont2Sym0KindInference] :: forall r6989586621679070803 arg_auvg. SameKind (Apply TyCont2Sym0 arg_auvg) (TyCont2Sym1 arg_auvg) => TyCont2Sym0 r6989586621679070803

-- | Type family representing the type of a continuation of 3 args.
type family TyCont3 r (a1 :: Type) (a2 :: Type) (a3 :: Type)
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
[TyCont3Sym3KindInference] :: forall r6989586621679127059 a16989586621679127060 a26989586621679127061 a36989586621679127062 arg_auAy. SameKind (Apply (TyCont3Sym3 r6989586621679127059 a16989586621679127060 a26989586621679127061) arg_auAy) (TyCont3Sym4 r6989586621679127059 a16989586621679127060 a26989586621679127061 arg_auAy) => TyCont3Sym3 r6989586621679127059 a16989586621679127060 a26989586621679127061 a36989586621679127062
data TyCont3Sym2 (r6989586621679127059 :: Type) (a16989586621679127060 :: Type) :: (~>) Type ((~>) Type Type)
[TyCont3Sym2KindInference] :: forall r6989586621679127059 a16989586621679127060 a26989586621679127061 arg_auAz. SameKind (Apply (TyCont3Sym2 r6989586621679127059 a16989586621679127060) arg_auAz) (TyCont3Sym3 r6989586621679127059 a16989586621679127060 arg_auAz) => TyCont3Sym2 r6989586621679127059 a16989586621679127060 a26989586621679127061
data TyCont3Sym1 (r6989586621679127059 :: Type) :: (~>) Type ((~>) Type ((~>) Type Type))
[TyCont3Sym1KindInference] :: forall r6989586621679127059 a16989586621679127060 arg_auAA. SameKind (Apply (TyCont3Sym1 r6989586621679127059) arg_auAA) (TyCont3Sym2 r6989586621679127059 arg_auAA) => TyCont3Sym1 r6989586621679127059 a16989586621679127060
data TyCont3Sym0 :: (~>) Type ((~>) Type ((~>) Type ((~>) Type Type)))
[TyCont3Sym0KindInference] :: forall r6989586621679127059 arg_auAB. SameKind (Apply TyCont3Sym0 arg_auAB) (TyCont3Sym1 arg_auAB) => TyCont3Sym0 r6989586621679127059
type family Ap (a_auJa :: (~>) x_auJ3 ((~>) y_auJ4 z_auJ5)) (a_auJb :: (~>) x_auJ3 y_auJ4) (a_auJc :: x_auJ3) :: z_auJ5
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
[ApSym2KindInference] :: forall a6989586621679127912 a6989586621679127913 a6989586621679127914 arg_auJd. SameKind (Apply (ApSym2 a6989586621679127912 a6989586621679127913) arg_auJd) (ApSym3 a6989586621679127912 a6989586621679127913 arg_auJd) => ApSym2 a6989586621679127912 a6989586621679127913 a6989586621679127914
data ApSym1 (a6989586621679127912 :: (~>) x6989586621679127905 ((~>) y6989586621679127906 z6989586621679127907)) :: (~>) ((~>) x6989586621679127905 y6989586621679127906) ((~>) x6989586621679127905 z6989586621679127907)
[ApSym1KindInference] :: forall a6989586621679127912 a6989586621679127913 arg_auJe. SameKind (Apply (ApSym1 a6989586621679127912) arg_auJe) (ApSym2 a6989586621679127912 arg_auJe) => ApSym1 a6989586621679127912 a6989586621679127913
data ApSym0 :: forall x6989586621679127905 y6989586621679127906 z6989586621679127907. (~>) ((~>) x6989586621679127905 ((~>) y6989586621679127906 z6989586621679127907)) ((~>) ((~>) x6989586621679127905 y6989586621679127906) ((~>) x6989586621679127905 z6989586621679127907))
[ApSym0KindInference] :: forall a6989586621679127912 arg_auJf. SameKind (Apply ApSym0 arg_auJf) (ApSym1 arg_auJf) => ApSym0 a6989586621679127912
sAp :: forall x_auJ3 y_auJ4 z_auJ5 (t_auJj :: (~>) x_auJ3 ((~>) y_auJ4 z_auJ5)) (t_auJk :: (~>) x_auJ3 y_auJ4) (t_auJl :: x_auJ3). Sing t_auJj -> Sing t_auJk -> Sing t_auJl -> Sing (Apply (Apply (Apply ApSym0 t_auJj) t_auJk) t_auJl :: z_auJ5)
ap :: (x_auJ3 -> y_auJ4 -> z_auJ5) -> (x_auJ3 -> y_auJ4) -> x_auJ3 -> z_auJ5

-- | Data type wrapping a constraint, to avoid ImpredicativeTypes GHC
--   error.
newtype CxtW c a
CxtW :: (c => a) -> CxtW c a
[unCxtW] :: CxtW c a -> c => a

-- | Convert a list of constraints into a single constraint
type family ConstrainList (cc :: [Constraint]) :: Constraint

-- | Null constraint over 1 type param.
type family NullC (t :: k) :: Constraint
type NullCSym1 (t6989586621679127945 :: k6989586621679127944) = NullC t6989586621679127945
data NullCSym0 :: forall k6989586621679127944. (~>) k6989586621679127944 Constraint
[NullCSym0KindInference] :: forall t6989586621679127945 arg_auZv. SameKind (Apply NullCSym0 arg_auZv) (NullCSym1 arg_auZv) => NullCSym0 t6989586621679127945

-- | Null constraint over 2 type params.
type family NullC2 (t :: k) (t' :: k') :: Constraint
type NullC2Sym2 (t6989586621679128932 :: k6989586621679128930) (t'6989586621679128933 :: k'6989586621679128931) = NullC2 t6989586621679128932 t'6989586621679128933
data NullC2Sym1 (t6989586621679128932 :: k6989586621679128930) :: forall k'6989586621679128931. (~>) k'6989586621679128931 Constraint
[NullC2Sym1KindInference] :: forall t6989586621679128932 t'6989586621679128933 arg_av1V. SameKind (Apply (NullC2Sym1 t6989586621679128932) arg_av1V) (NullC2Sym2 t6989586621679128932 arg_av1V) => NullC2Sym1 t6989586621679128932 t'6989586621679128933
data NullC2Sym0 :: forall k'6989586621679128931 k6989586621679128930. (~>) k6989586621679128930 ((~>) k'6989586621679128931 Constraint)
[NullC2Sym0KindInference] :: forall t6989586621679128932 arg_av1W. SameKind (Apply NullC2Sym0 arg_av1W) (NullC2Sym1 arg_av1W) => NullC2Sym0 t6989586621679128932

-- | Combine two constraints
type family AndC c0 c1 :: Constraint
type AndCSym2 (c06989586621679129083 :: Constraint) (c16989586621679129084 :: Constraint) = AndC c06989586621679129083 c16989586621679129084
data AndCSym1 (c06989586621679129083 :: Constraint) :: (~>) Constraint Constraint
[AndCSym1KindInference] :: forall c06989586621679129083 c16989586621679129084 arg_av6E. SameKind (Apply (AndCSym1 c06989586621679129083) arg_av6E) (AndCSym2 c06989586621679129083 arg_av6E) => AndCSym1 c06989586621679129083 c16989586621679129084
data AndCSym0 :: (~>) Constraint ((~>) Constraint Constraint)
[AndCSym0KindInference] :: forall c06989586621679129083 arg_av6F. SameKind (Apply AndCSym0 arg_av6F) (AndCSym1 arg_av6F) => AndCSym0 c06989586621679129083

-- | Combine two constraint constructors into a single constraint
--   constructor.
--   
--   This is analogous to the term-level idiom <tt>ap ((,) . c0) c1</tt>
--   that combines two functions c0, c1 into a single one.
type AndC1 c0 c1 = ApSym2 (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 <tt>ap (ap . ((,) .) . c0)
--   c1</tt> that combines two functions c0, c1 that each take 2 params,
--   into a single one.
type AndC2 c0 c1 = ApSym2 (ApSym0 .@#@$$$ (.@#@$$) AndCSym0 .@#@$$$ c0) c1

-- | Entailment over 2 type params.
type family Class2 c0 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
[Class2Sym3KindInference] :: forall c06989586621679129378 c16989586621679129379 t6989586621679129380 t'6989586621679129381 arg_avbM. SameKind (Apply (Class2Sym3 c06989586621679129378 c16989586621679129379 t6989586621679129380) arg_avbM) (Class2Sym4 c06989586621679129378 c16989586621679129379 t6989586621679129380 arg_avbM) => Class2Sym3 c06989586621679129378 c16989586621679129379 t6989586621679129380 t'6989586621679129381
data Class2Sym2 (c06989586621679129378 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) (c16989586621679129379 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)
[Class2Sym2KindInference] :: forall c06989586621679129378 c16989586621679129379 t6989586621679129380 arg_avbN. SameKind (Apply (Class2Sym2 c06989586621679129378 c16989586621679129379) arg_avbN) (Class2Sym3 c06989586621679129378 c16989586621679129379 arg_avbN) => Class2Sym2 c06989586621679129378 c16989586621679129379 t6989586621679129380
data Class2Sym1 (c06989586621679129378 :: (~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) :: (~>) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint))
[Class2Sym1KindInference] :: forall c06989586621679129378 c16989586621679129379 arg_avbO. SameKind (Apply (Class2Sym1 c06989586621679129378) arg_avbO) (Class2Sym2 c06989586621679129378 arg_avbO) => Class2Sym1 c06989586621679129378 c16989586621679129379
data Class2Sym0 :: forall k16989586621679129614 k16989586621679129616. (~>) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) ((~>) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)) ((~>) k16989586621679129616 ((~>) k16989586621679129614 Constraint)))
[Class2Sym0KindInference] :: forall c06989586621679129378 arg_avbP. SameKind (Apply Class2Sym0 arg_avbP) (Class2Sym1 arg_avbP) => Class2Sym0 c06989586621679129378
type family LookupKV_If (a_awAW :: k_avqg) (a_awAX :: k_avqg) (a_awAY :: [k_avqg]) (a_awAZ :: v_avqh) (a_awB0 :: [v_avqh]) (a_awB1 :: Bool) :: Maybe (k_avqg, v_avqh)
data LookupKVSym0 :: forall k6989586621679130586 v6989586621679130587. (~>) k6989586621679130586 ((~>) [k6989586621679130586] ((~>) [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587))))
[LookupKVSym0KindInference] :: forall a6989586621679135078 arg_awAP. SameKind (Apply LookupKVSym0 arg_awAP) (LookupKVSym1 arg_awAP) => LookupKVSym0 a6989586621679135078
data LookupKVSym1 (a6989586621679135078 :: k6989586621679130586) :: forall v6989586621679130587. (~>) [k6989586621679130586] ((~>) [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587)))
[LookupKVSym1KindInference] :: forall a6989586621679135078 a6989586621679135079 arg_awAO. SameKind (Apply (LookupKVSym1 a6989586621679135078) arg_awAO) (LookupKVSym2 a6989586621679135078 arg_awAO) => LookupKVSym1 a6989586621679135078 a6989586621679135079
data LookupKVSym2 (a6989586621679135078 :: k6989586621679130586) (a6989586621679135079 :: [k6989586621679130586]) :: forall v6989586621679130587. (~>) [v6989586621679130587] (Maybe (k6989586621679130586, v6989586621679130587))
[LookupKVSym2KindInference] :: forall a6989586621679135078 a6989586621679135079 a6989586621679135080 arg_awAN. SameKind (Apply (LookupKVSym2 a6989586621679135078 a6989586621679135079) arg_awAN) (LookupKVSym3 a6989586621679135078 a6989586621679135079 arg_awAN) => LookupKVSym2 a6989586621679135078 a6989586621679135079 a6989586621679135080
type LookupKVSym3 (a6989586621679135078 :: k6989586621679130586) (a6989586621679135079 :: [k6989586621679130586]) (a6989586621679135080 :: [v6989586621679130587]) = LookupKV a6989586621679135078 a6989586621679135079 a6989586621679135080
type family LookupKV (a_awAK :: k_avqi) (a_awAL :: [k_avqi]) (a_awAM :: [v_avqj]) :: Maybe (k_avqi, v_avqj)
data LookupKV_IfSym0 :: forall k6989586621679130584 v6989586621679130585. (~>) k6989586621679130584 ((~>) k6989586621679130584 ((~>) [k6989586621679130584] ((~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585)))))))
[LookupKV_IfSym0KindInference] :: forall a6989586621679135090 arg_awB7. SameKind (Apply LookupKV_IfSym0 arg_awB7) (LookupKV_IfSym1 arg_awB7) => LookupKV_IfSym0 a6989586621679135090
data LookupKV_IfSym1 (a6989586621679135090 :: k6989586621679130584) :: forall v6989586621679130585. (~>) k6989586621679130584 ((~>) [k6989586621679130584] ((~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585))))))
[LookupKV_IfSym1KindInference] :: forall a6989586621679135090 a6989586621679135091 arg_awB6. SameKind (Apply (LookupKV_IfSym1 a6989586621679135090) arg_awB6) (LookupKV_IfSym2 a6989586621679135090 arg_awB6) => LookupKV_IfSym1 a6989586621679135090 a6989586621679135091
data LookupKV_IfSym2 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) :: forall v6989586621679130585. (~>) [k6989586621679130584] ((~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585)))))
[LookupKV_IfSym2KindInference] :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 arg_awB5. SameKind (Apply (LookupKV_IfSym2 a6989586621679135090 a6989586621679135091) arg_awB5) (LookupKV_IfSym3 a6989586621679135090 a6989586621679135091 arg_awB5) => LookupKV_IfSym2 a6989586621679135090 a6989586621679135091 a6989586621679135092
data LookupKV_IfSym3 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) :: forall v6989586621679130585. (~>) v6989586621679130585 ((~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585))))
[LookupKV_IfSym3KindInference] :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 arg_awB4. SameKind (Apply (LookupKV_IfSym3 a6989586621679135090 a6989586621679135091 a6989586621679135092) arg_awB4) (LookupKV_IfSym4 a6989586621679135090 a6989586621679135091 a6989586621679135092 arg_awB4) => LookupKV_IfSym3 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093
data LookupKV_IfSym4 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) (a6989586621679135093 :: v6989586621679130585) :: (~>) [v6989586621679130585] ((~>) Bool (Maybe (k6989586621679130584, v6989586621679130585)))
[LookupKV_IfSym4KindInference] :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 arg_awB3. SameKind (Apply (LookupKV_IfSym4 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093) arg_awB3) (LookupKV_IfSym5 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 arg_awB3) => LookupKV_IfSym4 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094
data LookupKV_IfSym5 (a6989586621679135090 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) (a6989586621679135093 :: v6989586621679130585) (a6989586621679135094 :: [v6989586621679130585]) :: (~>) Bool (Maybe (k6989586621679130584, v6989586621679130585))
[LookupKV_IfSym5KindInference] :: forall a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 a6989586621679135095 arg_awB2. SameKind (Apply (LookupKV_IfSym5 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094) arg_awB2) (LookupKV_IfSym6 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 arg_awB2) => LookupKV_IfSym5 a6989586621679135090 a6989586621679135091 a6989586621679135092 a6989586621679135093 a6989586621679135094 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_avqg v_avqh (t_awBk :: k_avqg) (t_awBl :: k_avqg) (t_awBm :: [k_avqg]) (t_awBn :: v_avqh) (t_awBo :: [v_avqh]) (t_awBp :: Bool). SEq k_avqg => Sing t_awBk -> Sing t_awBl -> Sing t_awBm -> Sing t_awBn -> Sing t_awBo -> Sing t_awBp -> Sing (Apply (Apply (Apply (Apply (Apply (Apply LookupKV_IfSym0 t_awBk) t_awBl) t_awBm) t_awBn) t_awBo) t_awBp :: Maybe (k_avqg, v_avqh))
sLookupKV :: forall k_avqi v_avqj (t_awBe :: k_avqi) (t_awBf :: [k_avqi]) (t_awBg :: [v_avqj]). SEq k_avqi => Sing t_awBe -> Sing t_awBf -> Sing t_awBg -> Sing (Apply (Apply (Apply LookupKVSym0 t_awBe) t_awBf) t_awBg :: Maybe (k_avqi, v_avqj))
lookupKV_If :: Eq k_avqg => k_avqg -> k_avqg -> [k_avqg] -> v_avqh -> [v_avqh] -> Bool -> Maybe (k_avqg, v_avqh)
lookupKV :: Eq k_avqi => k_avqi -> [k_avqi] -> [v_avqj] -> Maybe (k_avqi, v_avqj)
class (Fmap (FmapSym1 f) (LookupKV k kk vv) ~ LookupKV k kk (Fmap f vv)) => ProofLookupKV f k (kk :: [kt]) vv
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

-- | Maybe that carries its type.
data TMaybe (t :: Maybe k)
[TNothing] :: TMaybe  'Nothing
[TJust] :: !t -> TMaybe ( 'Just t)

-- | Heterogeneous constrained table.
data TCTab (c :: kt ~> Type ~> Constraint) (kk :: [kt]) (vv :: [Type]) :: Type
[TCNil] :: TCTab c '[] '[]
[TCCons] :: (c @@ k) @@ v => !Sing (k :: kt) -> !v -> !TCTab c kk vv -> TCTab c (k : kk) (v : vv)

-- | A <a>TCTab</a> with a constraint that applies only to the value, not
--   the key.
type TCTab' c = TCTab (ConstSym1 (TyCon1 c))

-- | Heterogeneous unconstrained table.
--   
--   To add or remove constraints, see <a>strengthenTC0</a>,
--   <a>strengthenTC</a> and <a>weakenTC</a>.
type TTab = TCTab NullC2Sym0

-- | Result type of <a>lookupTC</a>.
data TCMaybe c (t :: Maybe (kt, Type))
[TCNothing] :: TCMaybe c  'Nothing
[TCJust] :: Dict ((c @@ k) @@ v) -> !Sing k -> !v -> TCMaybe c ( 'Just '(k, v))

-- | Lookup an element in the table, and generate some proofs about the
--   result that can be used by the caller.
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 two elements in two related tables.
--   
--   The types of the outputs are provably related.
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)))

-- | Zip two related tables, giving a third table related to both.
--   
--   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 three related tables, giving a fourth 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)
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)

-- | Weaken the constraint on a <a>TCTab</a>.
weakenTC :: forall kt c0 c1 (kk :: [kt]) vv. ConstrainList (ZipWith (Class2Sym2 c1 c0) kk vv) => TCTab c0 kk vv -> TCTab c1 kk vv

-- | Strengthen the constraint on a <a>TCTab</a>.
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 <a>TTab</a>.
strengthenTC0 :: forall kt c1 (kk :: [kt]) vv. ConstrainList (ZipWith c1 kk vv) => TTab kk vv -> TCTab c1 kk vv
instance forall a v kt (f :: a Data.Singletons.Internal.~> v) (k :: kt) (k' :: kt) (kk :: [kt]) (v' :: a) (vv :: [a]). Control.Static.Common.ProofLookupKV_If f k k' kk v' vv (k Data.Singletons.Prelude.Eq.== k') => Control.Static.Common.ProofLookupKV f k (k' : kk) (v' : vv)
instance forall kt a b (f :: a Data.Singletons.Internal.~> b) (k :: kt) (k' :: kt) (kk :: [kt]) (v' :: a) (vv :: [a]). Control.Static.Common.ProofLookupKV_If f k k' kk v' vv 'GHC.Types.True
instance forall kt a b (f :: a Data.Singletons.Internal.~> b) (k :: kt) (kk :: [kt]) (vv :: [a]) (k' :: kt) (v' :: a). Control.Static.Common.ProofLookupKV f k kk vv => Control.Static.Common.ProofLookupKV_If f k k' kk v' vv 'GHC.Types.False
instance forall kt a v (f :: a Data.Singletons.Internal.~> v) (k :: kt). Control.Static.Common.ProofLookupKV f k '[] '[]
instance forall v6989586621679130587 k6989586621679130586 (a6989586621679135079 :: k6989586621679130586) (a6989586621679135078 :: [k6989586621679130586]). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.LookupKVSym2 a6989586621679135079 a6989586621679135078)
instance forall v6989586621679130587 k6989586621679130586 (a6989586621679135078 :: k6989586621679130586). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.LookupKVSym1 a6989586621679135078)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.LookupKVSym0
instance forall v6989586621679130585 k6989586621679130584 (a6989586621679135094 :: k6989586621679130584) (a6989586621679135093 :: k6989586621679130584) (a6989586621679135092 :: [k6989586621679130584]) (a6989586621679135091 :: v6989586621679130585) (a6989586621679135090 :: [v6989586621679130585]). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.LookupKV_IfSym5 a6989586621679135094 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090)
instance forall v6989586621679130585 k6989586621679130584 (a6989586621679135093 :: k6989586621679130584) (a6989586621679135092 :: k6989586621679130584) (a6989586621679135091 :: [k6989586621679130584]) (a6989586621679135090 :: v6989586621679130585). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.LookupKV_IfSym4 a6989586621679135093 a6989586621679135092 a6989586621679135091 a6989586621679135090)
instance forall v6989586621679130585 k6989586621679130584 (a6989586621679135092 :: k6989586621679130584) (a6989586621679135091 :: k6989586621679130584) (a6989586621679135090 :: [k6989586621679130584]). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.LookupKV_IfSym3 a6989586621679135092 a6989586621679135091 a6989586621679135090)
instance forall v6989586621679130585 k6989586621679130584 (a6989586621679135091 :: k6989586621679130584) (a6989586621679135090 :: k6989586621679130584). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.LookupKV_IfSym2 a6989586621679135091 a6989586621679135090)
instance forall v6989586621679130585 k6989586621679130584 (a6989586621679135090 :: k6989586621679130584). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.LookupKV_IfSym1 a6989586621679135090)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.LookupKV_IfSym0
instance Data.Singletons.Prelude.Eq.SEq k => Data.Singletons.Internal.SingI Control.Static.Common.LookupKVSym0
instance forall k v (d :: k). (Data.Singletons.Prelude.Eq.SEq k, Data.Singletons.Internal.SingI d) => Data.Singletons.Internal.SingI (Control.Static.Common.LookupKVSym1 d)
instance forall k v (d1 :: k) (d2 :: [k]). (Data.Singletons.Prelude.Eq.SEq k, Data.Singletons.Internal.SingI d1, Data.Singletons.Internal.SingI d2) => Data.Singletons.Internal.SingI (Control.Static.Common.LookupKVSym2 d1 d2)
instance Data.Singletons.Prelude.Eq.SEq k => Data.Singletons.Internal.SingI Control.Static.Common.LookupKV_IfSym0
instance forall k v (d :: k). (Data.Singletons.Prelude.Eq.SEq k, Data.Singletons.Internal.SingI d) => Data.Singletons.Internal.SingI (Control.Static.Common.LookupKV_IfSym1 d)
instance forall k v (d1 :: k) (d2 :: k). (Data.Singletons.Prelude.Eq.SEq k, Data.Singletons.Internal.SingI d1, Data.Singletons.Internal.SingI d2) => Data.Singletons.Internal.SingI (Control.Static.Common.LookupKV_IfSym2 d1 d2)
instance forall k v (d1 :: k) (d2 :: k) (d3 :: [k]). (Data.Singletons.Prelude.Eq.SEq k, Data.Singletons.Internal.SingI d1, Data.Singletons.Internal.SingI d2, Data.Singletons.Internal.SingI d3) => Data.Singletons.Internal.SingI (Control.Static.Common.LookupKV_IfSym3 d1 d2 d3)
instance forall k v (d1 :: k) (d2 :: k) (d3 :: [k]) (d4 :: v). (Data.Singletons.Prelude.Eq.SEq k, Data.Singletons.Internal.SingI d1, Data.Singletons.Internal.SingI d2, Data.Singletons.Internal.SingI d3, Data.Singletons.Internal.SingI d4) => Data.Singletons.Internal.SingI (Control.Static.Common.LookupKV_IfSym4 d1 d2 d3 d4)
instance forall k v (d1 :: k) (d2 :: k) (d3 :: [k]) (d4 :: v) (d5 :: [v]). (Data.Singletons.Prelude.Eq.SEq k, Data.Singletons.Internal.SingI d1, Data.Singletons.Internal.SingI d2, Data.Singletons.Internal.SingI d3, Data.Singletons.Internal.SingI d4, Data.Singletons.Internal.SingI d5) => Data.Singletons.Internal.SingI (Control.Static.Common.LookupKV_IfSym5 d1 d2 d3 d4 d5)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.Class2Sym0
instance forall k16989586621679129616 k16989586621679129614 (c06989586621679129378 :: k16989586621679129616 Data.Singletons.Internal.~> (k16989586621679129614 Data.Singletons.Internal.~> GHC.Types.Constraint)). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.Class2Sym1 c06989586621679129378)
instance forall k16989586621679129616 k16989586621679129614 (c16989586621679129379 :: k16989586621679129616 Data.Singletons.Internal.~> (k16989586621679129614 Data.Singletons.Internal.~> GHC.Types.Constraint)) (c06989586621679129378 :: k16989586621679129616 Data.Singletons.Internal.~> (k16989586621679129614 Data.Singletons.Internal.~> GHC.Types.Constraint)). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.Class2Sym2 c16989586621679129379 c06989586621679129378)
instance forall k16989586621679129616 k16989586621679129614 (t6989586621679129380 :: k16989586621679129616 Data.Singletons.Internal.~> (k16989586621679129614 Data.Singletons.Internal.~> GHC.Types.Constraint)) (c16989586621679129379 :: k16989586621679129616 Data.Singletons.Internal.~> (k16989586621679129614 Data.Singletons.Internal.~> GHC.Types.Constraint)) (c06989586621679129378 :: k16989586621679129616). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.Class2Sym3 t6989586621679129380 c16989586621679129379 c06989586621679129378)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.AndCSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.AndCSym1 c06989586621679129083)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.NullC2Sym0
instance forall k'6989586621679128931 k6989586621679128930 (t6989586621679128932 :: k6989586621679128930). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.NullC2Sym1 t6989586621679128932)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.NullCSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.ApSym0
instance Data.Singletons.Internal.SingI Control.Static.Common.ApSym0
instance forall x6989586621679127905 y6989586621679127906 z6989586621679127907 (a6989586621679127912 :: x6989586621679127905 Data.Singletons.Internal.~> (y6989586621679127906 Data.Singletons.Internal.~> z6989586621679127907)). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.ApSym1 a6989586621679127912)
instance forall x y z (d :: x Data.Singletons.Internal.~> (y Data.Singletons.Internal.~> z)). Data.Singletons.Internal.SingI d => Data.Singletons.Internal.SingI (Control.Static.Common.ApSym1 d)
instance forall x6989586621679127905 y6989586621679127906 z6989586621679127907 (a6989586621679127913 :: x6989586621679127905 Data.Singletons.Internal.~> (y6989586621679127906 Data.Singletons.Internal.~> z6989586621679127907)) (a6989586621679127912 :: x6989586621679127905 Data.Singletons.Internal.~> y6989586621679127906). Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.ApSym2 a6989586621679127913 a6989586621679127912)
instance forall x y z (d1 :: x Data.Singletons.Internal.~> (y Data.Singletons.Internal.~> z)) (d2 :: x Data.Singletons.Internal.~> y). (Data.Singletons.Internal.SingI d1, Data.Singletons.Internal.SingI d2) => Data.Singletons.Internal.SingI (Control.Static.Common.ApSym2 d1 d2)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.TyCont3Sym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.TyCont3Sym1 r6989586621679127059)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.TyCont3Sym2 a16989586621679127060 r6989586621679127059)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.TyCont3Sym3 a26989586621679127061 a16989586621679127060 r6989586621679127059)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.TyCont2Sym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.TyCont2Sym1 r6989586621679070803)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.TyCont2Sym2 a16989586621679070804 r6989586621679070803)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Common.TyContSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Common.TyContSym1 r6989586621679058218)

module Control.Static.Serialise

-- | Serialisable external value, with an associated static-key.
--   
--   <tt>g</tt> is a type that can generically represent all the external
--   interface of your static values. See <a>RepVal</a> and
--   <a>DoubleEncoding</a> for more details.
data SKeyedExt g
SKeyedExt :: !String -> !g -> SKeyedExt g

-- | Possible errors when resolving a key in a static table.
data SKeyedError
SKeyedNotFound :: String -> SKeyedError
SKeyedExtDecodeFailure :: String -> SKeyedError

-- | A value and its external representation, indexed by some key.
class RepVal g (v :: Type) (k :: kt)

-- | Convert an external value into its generic representation.
toRep :: RepVal g v k => Sing k -> v -> g

-- | Convert a generic representation into its external value.
--   
--   This may fail, since <tt>g</tt> may have to represent several other
--   <tt>v'</tt> as well, which <tt>k</tt> should help determine.
fromRep :: RepVal g v k => Sing k -> g -> Either String v
type RepValSym3 (g6989586621679180882 :: Type) (v6989586621679180883 :: Type) (k6989586621679180884 :: kt6989586621679180881) = RepVal g6989586621679180882 v6989586621679180883 k6989586621679180884
data RepValSym2 (g6989586621679180882 :: Type) (v6989586621679180883 :: Type) :: forall kt6989586621679180881. (~>) kt6989586621679180881 Constraint
[RepValSym2KindInference] :: forall g6989586621679180882 v6989586621679180883 k6989586621679180884 arg_aLuN. SameKind (Apply (RepValSym2 g6989586621679180882 v6989586621679180883) arg_aLuN) (RepValSym3 g6989586621679180882 v6989586621679180883 arg_aLuN) => RepValSym2 g6989586621679180882 v6989586621679180883 k6989586621679180884
data RepValSym1 (g6989586621679180882 :: Type) :: forall kt6989586621679180881. (~>) Type ((~>) kt6989586621679180881 Constraint)
[RepValSym1KindInference] :: forall g6989586621679180882 v6989586621679180883 arg_aLuO. SameKind (Apply (RepValSym1 g6989586621679180882) arg_aLuO) (RepValSym2 g6989586621679180882 arg_aLuO) => RepValSym1 g6989586621679180882 v6989586621679180883
data RepValSym0 :: forall kt6989586621679180881. (~>) Type ((~>) Type ((~>) kt6989586621679180881 Constraint))
[RepValSym0KindInference] :: forall g6989586621679180882 arg_aLuP. SameKind (Apply RepValSym0 arg_aLuP) (RepValSym1 arg_aLuP) => RepValSym0 g6989586621679180882
castOrFail :: forall s t. (Typeable s, Typeable t) => s -> Either String t

-- | Uniform generic wrapper.
--   
--   In a type-safe language like Haskell, one needs to know in advance the
--   type of something in order to deserialise it successfully. In many
--   applications however, the point at which data enters the program is
--   separate from the point at which we have enough type information to
--   fully deserialise a statically-keyed value. Between these points, we
--   often want to deserialise the <i>other</i> parts of that data, and
--   perform logic based on its value.
--   
--   This wrapper works around that fact by double-encoding the
--   static-value. This is perhaps suboptimal performance-wise, but is
--   simple to implement and use, especially in a compositional manner.
--   When data first enters the program, one can deserialise the whole data
--   using the mechanism represented by <tt>s</tt>, which will then contain
--   <tt><a>HalfEncoded</a> b</tt> instances of this type inside it. When
--   you finally have enough type information to perform the rest of the
--   deserialise you can call <a>fromRep</a> on these parts, to recovered
--   the typed value corresponding to each part.
--   
--   This wrapper also short-circuits the case of calling <a>toRep</a> then
--   <a>fromRep</a> without attempting to serialise the value in between.
--   In this case the original value is simply wrapped in the
--   <a>Decoded</a> constructor, no attempt to serialise based on
--   <tt>s</tt> is actually made, and no value based on <tt>b</tt> is ever
--   constructed.
--   
--   If you need optimal performance and really must avoid
--   double-serialising, you can instead define your own ADT as a sum-type
--   over all your possible serialisation types, make this serialisable,
--   and implement <a>RepVal</a> for it.
--   
--   <tt>s</tt> is a constraint over serialisable types, e.g
--   <a>Serialise</a> or <a>Binary</a>. <tt>b</tt> is the concrete
--   serialisation type, e.g. <a>ByteString</a>.
data DoubleEncoding s b
[Decoded] :: (Typeable t, s t) => !t -> DoubleEncoding s b
[HalfEncoded] :: !b -> DoubleEncoding s b
type DSerialise = DoubleEncoding Serialise ByteString
type DBinary = DoubleEncoding Binary ByteString
decodeFullyOrFail :: Binary a => ByteString -> Either String a
instance Data.Binary.Class.Binary Control.Static.Serialise.DBinary
instance forall kt v (k :: kt). (Data.Typeable.Internal.Typeable v, Data.Binary.Class.Binary v) => Control.Static.Serialise.RepVal Control.Static.Serialise.DBinary v k
instance GHC.Classes.Eq Control.Static.Serialise.DBinary
instance GHC.Classes.Ord Control.Static.Serialise.DBinary
instance Codec.Serialise.Class.Serialise Control.Static.Serialise.DSerialise
instance forall kt v (k :: kt). (Data.Typeable.Internal.Typeable v, Codec.Serialise.Class.Serialise v) => Control.Static.Serialise.RepVal Control.Static.Serialise.DSerialise v k
instance GHC.Classes.Eq Control.Static.Serialise.DSerialise
instance GHC.Classes.Ord Control.Static.Serialise.DSerialise
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Serialise.RepValSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Serialise.RepValSym1 g6989586621679180882)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Serialise.RepValSym2 v6989586621679180883 g6989586621679180882)
instance forall kt v (k :: kt). Data.Typeable.Internal.Typeable v => Control.Static.Serialise.RepVal Data.Dynamic.Dynamic v k
instance GHC.Classes.Ord Control.Static.Serialise.SKeyedError
instance GHC.Classes.Eq Control.Static.Serialise.SKeyedError
instance Codec.Serialise.Class.Serialise Control.Static.Serialise.SKeyedError
instance Data.Binary.Class.Binary Control.Static.Serialise.SKeyedError
instance GHC.Generics.Generic Control.Static.Serialise.SKeyedError
instance GHC.Show.Show Control.Static.Serialise.SKeyedError
instance GHC.Read.Read Control.Static.Serialise.SKeyedError
instance GHC.Base.Functor Control.Static.Serialise.SKeyedExt
instance GHC.Classes.Ord g => GHC.Classes.Ord (Control.Static.Serialise.SKeyedExt g)
instance GHC.Classes.Eq g => GHC.Classes.Eq (Control.Static.Serialise.SKeyedExt g)
instance Codec.Serialise.Class.Serialise g => Codec.Serialise.Class.Serialise (Control.Static.Serialise.SKeyedExt g)
instance Data.Binary.Class.Binary g => Data.Binary.Class.Binary (Control.Static.Serialise.SKeyedExt g)
instance GHC.Generics.Generic (Control.Static.Serialise.SKeyedExt g)
instance GHC.Show.Show g => GHC.Show.Show (Control.Static.Serialise.SKeyedExt g)
instance GHC.Read.Read g => GHC.Read.Read (Control.Static.Serialise.SKeyedExt g)

module Control.Static.Static

-- | Standalone static key with no associated value.
--   
--   Users typically don't need this, and should use <a>SKeyed</a> or
--   <a>SKeyedExt</a> as appropriate.
type SKey (k :: Symbol) = Sing k

-- | Internal value, typed-indexed by an associated static-key.
--   
--   Generally, <tt>v</tt> is not expected to be serialisable or otherwise
--   representable outside of the program. For cases where it is, you
--   should define an instance of <a>RepVal</a>. That then enables you to
--   use <a>toSKeyedExt</a> and other utility functions with this
--   constraint.
data SKeyed k v
SKeyed :: !SKey k -> !v -> SKeyed k v

-- | Similar to <a>withSomeSing</a> for a <a>SKeyedExt</a>, extract the
--   type from the <a>String</a> key and run a typed function on the typed
--   value.
withSKeyedExt :: SKeyedExt g -> (forall (a :: Symbol). SKeyed a g -> r) -> r

-- | Convert an internal value to an external value, depending on the
--   existence of an instance of <a>RepVal</a> to help perform the
--   conversion.
toSKeyedExt :: RepVal g v k => SKeyed k v -> SKeyedExt g
toSKeyedEither :: Sing (k :: Symbol) -> Maybe (Either String v) -> Either SKeyedError v

-- | Helper function for building <a>TCTab</a>s.
skeyedCons :: (c @@ k) @@ v => SKeyed k v -> TCTab c kk vv -> TCTab c (k : kk) (v : vv)

-- | <tt>RepExt c g ext k v</tt> is a constraint comprising:
--   
--   <ul>
--   <li><pre>RepVal g (ext v) k</pre></li>
--   <li><pre>c k v</pre></li>
--   </ul>
--   
--   modulo singletons defunctionalisation on <tt>c</tt> and <tt>ext</tt>.
type RepExtSym3 c g ext = AndC2 c (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ext))

-- | A continuation from an internal and external value, to a result type
--   <tt>r</tt>.
type family TyContIX r ext (v :: Type)
type TyContIXSym3 (r6989586621679205952 :: Type) (ext6989586621679205953 :: (~>) Type Type) (v6989586621679205954 :: Type) = TyContIX r6989586621679205952 ext6989586621679205953 v6989586621679205954
data TyContIXSym2 (r6989586621679205952 :: Type) (ext6989586621679205953 :: (~>) Type Type) :: (~>) Type Type
[TyContIXSym2KindInference] :: forall r6989586621679205952 ext6989586621679205953 v6989586621679205954 arg_aP9e. SameKind (Apply (TyContIXSym2 r6989586621679205952 ext6989586621679205953) arg_aP9e) (TyContIXSym3 r6989586621679205952 ext6989586621679205953 arg_aP9e) => TyContIXSym2 r6989586621679205952 ext6989586621679205953 v6989586621679205954
data TyContIXSym1 (r6989586621679205952 :: Type) :: (~>) ((~>) Type Type) ((~>) Type Type)
[TyContIXSym1KindInference] :: forall r6989586621679205952 ext6989586621679205953 arg_aP9f. SameKind (Apply (TyContIXSym1 r6989586621679205952) arg_aP9f) (TyContIXSym2 r6989586621679205952 arg_aP9f) => TyContIXSym1 r6989586621679205952 ext6989586621679205953
data TyContIXSym0 :: (~>) Type ((~>) ((~>) Type Type) ((~>) Type Type))
[TyContIXSym0KindInference] :: forall r6989586621679205952 arg_aP9g. SameKind (Apply TyContIXSym0 arg_aP9g) (TyContIXSym1 arg_aP9g) => TyContIXSym0 r6989586621679205952

-- | Given an <a>SKeyed</a> of an external value <tt>g</tt>, do the
--   following:
--   
--   <ol>
--   <li>Lookup the corresponding internal value (I) of type
--   <tt>v</tt>.</li>
--   <li>Decode the external value (X) of type <tt>g</tt>, if its type can
--   be decoded into the type <tt>ext v</tt>.</li>
--   <li>Lookup the corresponding continuation (C).</li>
--   <li>Apply (C) to (I) and (X), returning a value of type
--   <tt>r</tt>.</li>
--   </ol>
gwithStatic :: forall c0 c1 f g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyed k g -> TCTab c1 kk (Fmap f vv) -> (forall k' v.  'Just '(k', v) ~ LookupKV k kk vv =>  'Just '(k', f @@ v) ~ Fmap (FmapSym1 f) (LookupKV k kk vv) => (c0 @@ k') @@ v => (c1 @@ k') @@ (f @@ v) => Sing k' -> (f @@ v) -> v -> (ext @@ v) -> r) -> Either SKeyedError r
withStaticCts :: forall c0 c1 g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyed k g -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv) -> Either SKeyedError r
withSomeStaticCts :: forall c0 c1 g ext (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyedExt g -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv) -> Either SKeyedError r
withStaticCxt :: forall c f g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c g ext) kk vv -> SKeyed k g -> (forall k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ v => Sing k' -> v -> (ext @@ v) -> r) -> Either SKeyedError r
withSomeStaticCxt :: forall c f g ext (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c g ext) kk vv -> SKeyedExt g -> (forall k k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ v => Sing k' -> v -> (ext @@ v) -> r) -> Either SKeyedError r
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Static.TyContIXSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Static.TyContIXSym1 r6989586621679205952)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Static.Static.TyContIXSym2 ext6989586621679205953 r6989586621679205952)
instance GHC.Base.Functor (Control.Static.Static.SKeyed k)

module Control.Static.Closure

-- | Closure, internal representation.
--   
--   The type parameter <tt>env</tt> is meant for a bag of functions known
--   statically at compile time, that you don't need to serialise and so
--   don't want the added complexity of dealing with $(mkStatic). For
--   example, if your function takes in extra utility functions, but these
--   are all statically-known. The type parameter <tt>cxt</tt> are the
--   constraint types, which is effectively similar to <tt>env</tt> except
--   that Haskell deals with them slightly differently.
type ClosureFunc cxt env arg res = CxtW cxt (env -> arg -> res)

-- | An applied closure, consisting of its static key and an argument.
type ClosureApply g = SKeyedExt g

-- | Create a <a>ClosureApply</a> in its serialisable static form.
applyClosure :: RepVal g arg k => SKeyed k (CxtW cxt (env -> arg -> res)) -> arg -> ClosureApply g
envTabCons :: SKeyed k (CxtW cxt (env -> arg -> res)) -> env -> TTab kk vv -> TTab (k : kk) (env : vv)
envTabNil :: TTab '[] '[]

-- | A pre-closure is a function that takes two statically-known arguments:
--   a constraint, and an explicit argument; and gives a closure.
--   
--   Typically, you define a bunch of top-level functions of the form
--   <tt>(ctx =&gt; env -&gt; arg -&gt; res)</tt>, then create a table of
--   pre-closures using the TH function <a>mkStaticTab</a>.
class Closure (Part pcl) => PreClosure pcl where {
    type family Cxt pcl :: Constraint;
    type family Env pcl;
    type family Part pcl;
}
applyPre :: (PreClosure pcl, Cxt pcl) => pcl -> Env pcl -> Part pcl

-- | A closure is a function that takes a runtime argument, and gives a
--   result.
--   
--   It is created by applying a constraint and environment to a
--   pre-closure. Typically you do this once on a table of pre-closures,
--   using <a>mkClosureTab</a>.
class Closure cl where {
    type family Arg cl;
    type family Res cl;
}
apply :: Closure cl => cl -> Arg cl -> Res cl

-- | A post-closure is a function that takes a runtime result, and converts
--   all the results of all different closures into the same type.
class PostClosure x f where {
    type family Pre f;
}
applyPost :: PostClosure x f => f -> Pre f -> x
type CxtSym1 (pcl6989586621679210425 :: Type) = Cxt pcl6989586621679210425
data CxtSym0 :: (~>) Type Constraint
[CxtSym0KindInference] :: forall pcl6989586621679210425 arg_aQkg. SameKind (Apply CxtSym0 arg_aQkg) (CxtSym1 arg_aQkg) => CxtSym0 pcl6989586621679210425
type EnvSym1 (pcl6989586621679210425 :: Type) = Env pcl6989586621679210425
data EnvSym0 :: (~>) Type Type
[EnvSym0KindInference] :: forall pcl6989586621679210425 arg_aQkh. SameKind (Apply EnvSym0 arg_aQkh) (EnvSym1 arg_aQkh) => EnvSym0 pcl6989586621679210425
type PartSym1 (pcl6989586621679210425 :: Type) = Part pcl6989586621679210425
data PartSym0 :: (~>) Type Type
[PartSym0KindInference] :: forall pcl6989586621679210425 arg_aQki. SameKind (Apply PartSym0 arg_aQki) (PartSym1 arg_aQki) => PartSym0 pcl6989586621679210425
type ArgSym1 (cl6989586621679210424 :: Type) = Arg cl6989586621679210424
data ArgSym0 :: (~>) Type Type
[ArgSym0KindInference] :: forall cl6989586621679210424 arg_aQkj. SameKind (Apply ArgSym0 arg_aQkj) (ArgSym1 arg_aQkj) => ArgSym0 cl6989586621679210424
type ResSym1 (cl6989586621679210424 :: Type) = Res cl6989586621679210424
data ResSym0 :: (~>) Type Type
[ResSym0KindInference] :: forall cl6989586621679210424 arg_aQkk. SameKind (Apply ResSym0 arg_aQkk) (ResSym1 arg_aQkk) => ResSym0 cl6989586621679210424
type PreSym1 (f6989586621679210423 :: Type) = Pre f6989586621679210423
data PreSym0 :: (~>) Type Type
[PreSym0KindInference] :: forall f6989586621679210423 arg_aQkl. SameKind (Apply PreSym0 arg_aQkl) (PreSym1 arg_aQkl) => PreSym0 f6989586621679210423

-- | A continuation from the result type to <tt>x</tt>.
type ResCont x = TyContSym1 x .@#@$$$ ResSym0

-- | Apply a table of pre-closures to its inputs, creating a table of
--   closures.
applyClosureTabPre :: forall c1 kk vv. ConstrainList (Fmap CxtSym0 vv) => TCTab' PreClosure kk vv -> TCTab c1 kk (Fmap EnvSym0 vv) -> TCTab' Closure kk (Fmap PartSym0 vv)

-- | Apply a table of closures to its inputs, creating a table of results.
applyClosureTab :: forall c1 kk vv. TCTab' Closure kk vv -> TCTab c1 kk (Fmap ArgSym0 vv) -> TTab kk (Fmap ResSym0 vv)

-- | Apply a table of results to its post-closures, creating a table of
--   values.
applyClosureTabPost :: forall c0 kk rr x. TCTab c0 kk rr -> TCTab' (PostClosure x) kk (Fmap (TyContSym1 x) rr) -> TTab kk (Fmap (ConstSym1 x) rr)

-- | Apply a table of closures to a table of inputs and post-closures,
--   giving a table of values.
--   
--   This method is just a demo, users will want one of the exported
--   functions.
evalClosureTab :: forall (kk :: [Symbol]) vv x. TCTab' Closure kk vv -> TTab kk (Fmap ArgSym0 vv) -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv) -> TTab kk (Fmap (ConstSym1 x) vv)

-- | Create a table of closures from a table of pre-closures.
--   
--   We apply the relevant constraints and environment arguments,
--   statically-known at compile time.
mkClosureTab :: forall c1 kk vv. ConstrainList (Fmap CxtSym0 vv) => ConstrainList (ZipWith (ConstSym1 (TyCon1 PreClosure)) kk vv) => TTab kk vv -> TCTab c1 kk (Fmap EnvSym0 vv) -> TCTab' Closure kk (Fmap PartSym0 vv)

-- | <tt>RepClosure c g k v</tt> is a constraint comprising:
--   
--   <ul>
--   <li><pre>RepVal g (Arg v) k</pre></li>
--   <li><pre>c k (Res v)</pre></li>
--   <li><pre>Closure v</pre></li>
--   </ul>
--   
--   modulo singletons defunctionalisation on <tt>c</tt>.
type RepClosure c g = RepExtSym3 (AndC2 (ConstSym1 (TyCon1 Closure)) (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c)) g ArgSym0

-- | A <a>RepClosure</a> whose result is exactly <tt>r</tt>.
type RepClosure' r g = RepClosure (ConstSym1 (TyCon1 ((~) r))) g

-- | Convert a <a>Closure</a> table into a <a>RepClosure</a> table,
--   deducing constraints.
--   
--   This is used to convert the result of <a>mkClosureTab</a> into a form
--   that can be passed to the other functions e.g. <a>evalSomeClosure</a>.
repClosureTab :: forall c g (kk :: [Symbol]) vv. ConstrainList (ZipWith (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c) kk vv) => ConstrainList (ZipWith (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ArgSym0)) kk vv) => TCTab' Closure kk vv -> TCTab (RepClosure c g) kk vv

-- | Apply a closure table to a single input and a post-processing table,
--   giving a single result (if the input key was found).
--   
--   This is the statically-typed version; for a version that runs for
--   unknown keys see <a>withEvalSomeClosureCts</a>.
withEvalClosureCts :: forall c g (k :: Symbol) (kk :: [Symbol]) vv x. TCTab (RepClosure c g) kk vv -> SKeyed k g -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv) -> Either SKeyedError x

-- | Apply a closure table to a single input and a post-processing table,
--   giving a single result (if the input key was found).
--   
--   This is the dynamically-typed version; for a version that type-checks
--   for statically-known keys see <a>withEvalClosureCts</a>.
withEvalSomeClosureCts :: forall c g (kk :: [Symbol]) vv x. TCTab (RepClosure c g) kk vv -> ClosureApply g -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv) -> Either SKeyedError x

-- | Apply a closure table to a single input, and pass the constrained
--   result to a continuation (if the input key was found).
--   
--   This is the statically-typed version; for a version that runs for
--   unknown keys see <a>withEvalSomeClosureCxt</a>.
withEvalClosureCxt :: forall c f g (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepClosure c g) kk vv -> SKeyed k g -> (forall k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ Res v => Sing k' -> Res v -> r) -> Either SKeyedError r

-- | Apply a closure table to a single input, and pass the constrained
--   result to a continuation (if the input key was found).
--   
--   This is the dynamically-typed version; for a version that type-checks
--   for statically-known keys see <a>withEvalClosureCxt</a>.
withEvalSomeClosureCxt :: forall c f g (kk :: [Symbol]) vv r. TCTab (RepClosure c g) kk vv -> ClosureApply g -> (forall k k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ Res v => Sing k' -> Res v -> r) -> Either SKeyedError r

-- | Evaluate a closure application with statically-known type, against a
--   table of closures, that all have the same result type.
evalClosure :: forall g (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepClosure' r g) kk vv -> SKeyed k g -> Either SKeyedError r

-- | Evaluate a closure application with statically-unknown type, against a
--   table of closures, that all have the same result type.
evalSomeClosure :: forall g (kk :: [Symbol]) vv r. TCTab (RepClosure' r g) kk vv -> ClosureApply g -> Either SKeyedError r
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Closure.PreSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Closure.ResSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Closure.ArgSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Closure.PartSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Closure.EnvSym0
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Static.Closure.CxtSym0
instance Control.Static.Closure.PostClosure x (r -> x)
instance Control.Static.Closure.PreClosure (Control.Static.Common.CxtW c (e -> v -> r))
instance Control.Static.Closure.Closure (v -> r)

module Control.Static

-- | Heterogeneous constrained table.
data TCTab (c :: kt ~> Type ~> Constraint) (kk :: [kt]) (vv :: [Type]) :: Type
[TCNil] :: TCTab c '[] '[]
[TCCons] :: (c @@ k) @@ v => !Sing (k :: kt) -> !v -> !TCTab c kk vv -> TCTab c (k : kk) (v : vv)

-- | Standalone static key with no associated value.
--   
--   Users typically don't need this, and should use <a>SKeyed</a> or
--   <a>SKeyedExt</a> as appropriate.
type SKey (k :: Symbol) = Sing k

-- | Internal value, typed-indexed by an associated static-key.
--   
--   Generally, <tt>v</tt> is not expected to be serialisable or otherwise
--   representable outside of the program. For cases where it is, you
--   should define an instance of <a>RepVal</a>. That then enables you to
--   use <a>toSKeyedExt</a> and other utility functions with this
--   constraint.
data SKeyed k v
SKeyed :: !SKey k -> !v -> SKeyed k v

-- | Serialisable external value, with an associated static-key.
--   
--   <tt>g</tt> is a type that can generically represent all the external
--   interface of your static values. See <a>RepVal</a> and
--   <a>DoubleEncoding</a> for more details.
data SKeyedExt g
SKeyedExt :: !String -> !g -> SKeyedExt g

-- | Similar to <a>withSomeSing</a> for a <a>SKeyedExt</a>, extract the
--   type from the <a>String</a> key and run a typed function on the typed
--   value.
withSKeyedExt :: SKeyedExt g -> (forall (a :: Symbol). SKeyed a g -> r) -> r

-- | Convert an internal value to an external value, depending on the
--   existence of an instance of <a>RepVal</a> to help perform the
--   conversion.
toSKeyedExt :: RepVal g v k => SKeyed k v -> SKeyedExt g

-- | Given an <a>SKeyed</a> of an external value <tt>g</tt>, do the
--   following:
--   
--   <ol>
--   <li>Lookup the corresponding internal value (I) of type
--   <tt>v</tt>.</li>
--   <li>Decode the external value (X) of type <tt>g</tt>, if its type can
--   be decoded into the type <tt>ext v</tt>.</li>
--   <li>Lookup the corresponding continuation (C).</li>
--   <li>Apply (C) to (I) and (X), returning a value of type
--   <tt>r</tt>.</li>
--   </ol>
gwithStatic :: forall c0 c1 f g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyed k g -> TCTab c1 kk (Fmap f vv) -> (forall k' v.  'Just '(k', v) ~ LookupKV k kk vv =>  'Just '(k', f @@ v) ~ Fmap (FmapSym1 f) (LookupKV k kk vv) => (c0 @@ k') @@ v => (c1 @@ k') @@ (f @@ v) => Sing k' -> (f @@ v) -> v -> (ext @@ v) -> r) -> Either SKeyedError r
withStaticCts :: forall c0 c1 g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyed k g -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv) -> Either SKeyedError r
withSomeStaticCts :: forall c0 c1 g ext (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c0 g ext) kk vv -> SKeyedExt g -> TCTab c1 kk (Fmap (TyContIXSym2 r ext) vv) -> Either SKeyedError r
withStaticCxt :: forall c f g ext (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c g ext) kk vv -> SKeyed k g -> (forall k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ v => Sing k' -> v -> (ext @@ v) -> r) -> Either SKeyedError r
withSomeStaticCxt :: forall c f g ext (kk :: [Symbol]) vv r. TCTab (RepExtSym3 c g ext) kk vv -> SKeyedExt g -> (forall k k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ v => Sing k' -> v -> (ext @@ v) -> r) -> Either SKeyedError r

-- | A pre-closure is a function that takes two statically-known arguments:
--   a constraint, and an explicit argument; and gives a closure.
--   
--   Typically, you define a bunch of top-level functions of the form
--   <tt>(ctx =&gt; env -&gt; arg -&gt; res)</tt>, then create a table of
--   pre-closures using the TH function <a>mkStaticTab</a>.
class Closure (Part pcl) => PreClosure pcl where {
    type family Cxt pcl :: Constraint;
    type family Env pcl;
    type family Part pcl;
}
applyPre :: (PreClosure pcl, Cxt pcl) => pcl -> Env pcl -> Part pcl

-- | A closure is a function that takes a runtime argument, and gives a
--   result.
--   
--   It is created by applying a constraint and environment to a
--   pre-closure. Typically you do this once on a table of pre-closures,
--   using <a>mkClosureTab</a>.
class Closure cl where {
    type family Arg cl;
    type family Res cl;
}
apply :: Closure cl => cl -> Arg cl -> Res cl

-- | A post-closure is a function that takes a runtime result, and converts
--   all the results of all different closures into the same type.
class PostClosure x f where {
    type family Pre f;
}
applyPost :: PostClosure x f => f -> Pre f -> x

-- | An applied closure, consisting of its static key and an argument.
type ClosureApply g = SKeyedExt g

-- | Create a <a>ClosureApply</a> in its serialisable static form.
applyClosure :: RepVal g arg k => SKeyed k (CxtW cxt (env -> arg -> res)) -> arg -> ClosureApply g
envTabCons :: SKeyed k (CxtW cxt (env -> arg -> res)) -> env -> TTab kk vv -> TTab (k : kk) (env : vv)
envTabNil :: TTab '[] '[]

-- | Create a table of closures from a table of pre-closures.
--   
--   We apply the relevant constraints and environment arguments,
--   statically-known at compile time.
mkClosureTab :: forall c1 kk vv. ConstrainList (Fmap CxtSym0 vv) => ConstrainList (ZipWith (ConstSym1 (TyCon1 PreClosure)) kk vv) => TTab kk vv -> TCTab c1 kk (Fmap EnvSym0 vv) -> TCTab' Closure kk (Fmap PartSym0 vv)

-- | <tt>RepClosure c g k v</tt> is a constraint comprising:
--   
--   <ul>
--   <li><pre>RepVal g (Arg v) k</pre></li>
--   <li><pre>c k (Res v)</pre></li>
--   <li><pre>Closure v</pre></li>
--   </ul>
--   
--   modulo singletons defunctionalisation on <tt>c</tt>.
type RepClosure c g = RepExtSym3 (AndC2 (ConstSym1 (TyCon1 Closure)) (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c)) g ArgSym0

-- | A <a>RepClosure</a> whose result is exactly <tt>r</tt>.
type RepClosure' r g = RepClosure (ConstSym1 (TyCon1 ((~) r))) g

-- | Convert a <a>Closure</a> table into a <a>RepClosure</a> table,
--   deducing constraints.
--   
--   This is used to convert the result of <a>mkClosureTab</a> into a form
--   that can be passed to the other functions e.g. <a>evalSomeClosure</a>.
repClosureTab :: forall c g (kk :: [Symbol]) vv. ConstrainList (ZipWith (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c) kk vv) => ConstrainList (ZipWith (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ArgSym0)) kk vv) => TCTab' Closure kk vv -> TCTab (RepClosure c g) kk vv

-- | Apply a closure table to a single input and a post-processing table,
--   giving a single result (if the input key was found).
--   
--   This is the statically-typed version; for a version that runs for
--   unknown keys see <a>withEvalSomeClosureCts</a>.
withEvalClosureCts :: forall c g (k :: Symbol) (kk :: [Symbol]) vv x. TCTab (RepClosure c g) kk vv -> SKeyed k g -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv) -> Either SKeyedError x

-- | Apply a closure table to a single input and a post-processing table,
--   giving a single result (if the input key was found).
--   
--   This is the dynamically-typed version; for a version that type-checks
--   for statically-known keys see <a>withEvalClosureCts</a>.
withEvalSomeClosureCts :: forall c g (kk :: [Symbol]) vv x. TCTab (RepClosure c g) kk vv -> ClosureApply g -> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv) -> Either SKeyedError x

-- | Apply a closure table to a single input, and pass the constrained
--   result to a continuation (if the input key was found).
--   
--   This is the statically-typed version; for a version that runs for
--   unknown keys see <a>withEvalSomeClosureCxt</a>.
withEvalClosureCxt :: forall c f g (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepClosure c g) kk vv -> SKeyed k g -> (forall k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ Res v => Sing k' -> Res v -> r) -> Either SKeyedError r

-- | Apply a closure table to a single input, and pass the constrained
--   result to a continuation (if the input key was found).
--   
--   This is the dynamically-typed version; for a version that type-checks
--   for statically-known keys see <a>withEvalClosureCxt</a>.
withEvalSomeClosureCxt :: forall c f g (kk :: [Symbol]) vv r. TCTab (RepClosure c g) kk vv -> ClosureApply g -> (forall k k' v.  'Just '(k', v) ~ LookupKV k kk vv => ProofLookupKV f k kk vv => (c @@ k') @@ Res v => Sing k' -> Res v -> r) -> Either SKeyedError r

-- | Evaluate a closure application with statically-known type, against a
--   table of closures, that all have the same result type.
evalClosure :: forall g (k :: Symbol) (kk :: [Symbol]) vv r. TCTab (RepClosure' r g) kk vv -> SKeyed k g -> Either SKeyedError r

-- | Evaluate a closure application with statically-unknown type, against a
--   table of closures, that all have the same result type.
evalSomeClosure :: forall g (kk :: [Symbol]) vv r. TCTab (RepClosure' r g) kk vv -> ClosureApply g -> Either SKeyedError r

-- | A value and its external representation, indexed by some key.
class RepVal g (v :: Type) (k :: kt)

-- | Convert an external value into its generic representation.
toRep :: RepVal g v k => Sing k -> v -> g

-- | Convert a generic representation into its external value.
--   
--   This may fail, since <tt>g</tt> may have to represent several other
--   <tt>v'</tt> as well, which <tt>k</tt> should help determine.
fromRep :: RepVal g v k => Sing k -> g -> Either String v

-- | Possible errors when resolving a key in a static table.
data SKeyedError
SKeyedNotFound :: String -> SKeyedError
SKeyedExtDecodeFailure :: String -> SKeyedError

-- | Uniform generic wrapper.
--   
--   In a type-safe language like Haskell, one needs to know in advance the
--   type of something in order to deserialise it successfully. In many
--   applications however, the point at which data enters the program is
--   separate from the point at which we have enough type information to
--   fully deserialise a statically-keyed value. Between these points, we
--   often want to deserialise the <i>other</i> parts of that data, and
--   perform logic based on its value.
--   
--   This wrapper works around that fact by double-encoding the
--   static-value. This is perhaps suboptimal performance-wise, but is
--   simple to implement and use, especially in a compositional manner.
--   When data first enters the program, one can deserialise the whole data
--   using the mechanism represented by <tt>s</tt>, which will then contain
--   <tt><a>HalfEncoded</a> b</tt> instances of this type inside it. When
--   you finally have enough type information to perform the rest of the
--   deserialise you can call <a>fromRep</a> on these parts, to recovered
--   the typed value corresponding to each part.
--   
--   This wrapper also short-circuits the case of calling <a>toRep</a> then
--   <a>fromRep</a> without attempting to serialise the value in between.
--   In this case the original value is simply wrapped in the
--   <a>Decoded</a> constructor, no attempt to serialise based on
--   <tt>s</tt> is actually made, and no value based on <tt>b</tt> is ever
--   constructed.
--   
--   If you need optimal performance and really must avoid
--   double-serialising, you can instead define your own ADT as a sum-type
--   over all your possible serialisation types, make this serialisable,
--   and implement <a>RepVal</a> for it.
--   
--   <tt>s</tt> is a constraint over serialisable types, e.g
--   <a>Serialise</a> or <a>Binary</a>. <tt>b</tt> is the concrete
--   serialisation type, e.g. <a>ByteString</a>.
data DoubleEncoding s b
[Decoded] :: (Typeable t, s t) => !t -> DoubleEncoding s b
[HalfEncoded] :: !b -> DoubleEncoding s b
type DSerialise = DoubleEncoding Serialise ByteString
type DBinary = DoubleEncoding Binary ByteString

module Control.Static.TH

-- | Refer to a static value, as a <a>SKeyed</a>.
--   
--   Be sure to pass the argument to <a>mkStaticTab</a> so the referent
--   exists.
staticRef :: Name -> Q Exp

-- | Get the symbol key of a static value, as a <a>SKey</a>.
--   
--   Be sure to pass the argument to <a>mkStaticTab</a> so the referent
--   exists.
--   
--   Users typically don't need this; <a>staticRef</a> is more type-safe as
--   it includes the type of the value, and this does not.
staticKey :: Name -> Q Exp

-- | Get the symbol key type of a static value, as a type-level string.
staticKeyType :: Name -> Q Type

-- | Create top-level statically-keyed values from regular top-level
--   values.
mkStatics :: [Name] -> Q [Dec]

-- | Create top-level statically-keyed values from regular top-level
--   values, when their definitions need to refer to other statically-keyed
--   values.
--   
--   Since TH cannot handle references to names defined later in the source
--   file, it is not possible to use <a>mkStatics</a> for this purpose; you
--   must use this function instead, and then register the names later
--   using <a>mkStaticTab</a>.
--   
--   See unit tests for example usage.
mkStaticsWithRefs :: ([Exp] -> Q [Dec]) -> Q [Dec]
defaultStaticTab :: Name

-- | Create a table holding the static values for a list of top-level
--   names, binding it to the top-level name "staticTab".
mkDefStaticTab :: [Name] -> Q [Dec]

-- | Create a table holding the static values for a list of top-level
--   names, binding it to the given top-level name.
mkStaticTab :: Name -> [Name] -> Q [Dec]

-- | Data type wrapping a constraint, to avoid ImpredicativeTypes GHC
--   error.
newtype CxtW c a
CxtW :: (c => a) -> CxtW c a
[unCxtW] :: CxtW c a -> c => a