{-| Helper library for KVList to use in Esqueleto.
-}

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE OverloadedLabels #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}

module Data.KVList.Esqueleto
  ( SingleValue
  , singleValue
  , ToKVList(..)
  ) where

import Prelude

import Data.Functor ((<&>))
import Data.Text (Text)
import Data.Proxy (Proxy(..))
import Database.Esqueleto.Internal.Internal (SqlSelect(..))
import Data.KVList ((:=)((:=)), (&=), KVList, ListKey(..))
import qualified Data.KVList as KVList
import GHC.TypeLits (KnownSymbol)


class ToKVList a kvls | kvls -> a, a -> kvls where
  toKVList :: a -> Either Text kvls

instance
  ( ToKVList a ls
  ) => ToKVList (Maybe a) (Maybe ls) where
  toKVList :: Maybe a -> Either Text (Maybe ls)
toKVList Maybe a
ma =
    case Maybe a
ma of
      Maybe a
Nothing -> forall a b. b -> Either a b
Right forall a. Maybe a
Nothing
      Just a
a ->
        forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList a
a
          forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall a. a -> Maybe a
Just

{-| -}
newtype SingleValue e = SingleValue e

{-| -}
singleValue :: e -> SingleValue e
singleValue :: forall e. e -> SingleValue e
singleValue = forall e. e -> SingleValue e
SingleValue

instance
  forall a ra recA.
  ( SqlSelect a ra
  , ToKVList ra recA
  ) => SqlSelect (SingleValue a) (KVList '[ "value" := recA ]) where
  sqlSelectCols :: IdentInfo -> SingleValue a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (SingleValue a
a) =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc a
a
  sqlSelectColCount :: Proxy (SingleValue a) -> Int
sqlSelectColCount Proxy (SingleValue a)
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy a)
  sqlSelectProcessRow :: [PersistValue] -> Either Text (KVList '["value" := recA])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
recA <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (k :: Symbol) v.
KnownSymbol k =>
(k := v) -> KVList '[k := v]
KVList.singleton (forall a. IsLabel "value" a => a
#value forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
recA)

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , KnownSymbol la
  , KnownSymbol lb
  , ToKVList ra recA
  , ToKVList rb recB
  , KVList.HasKey la '[la := a, lb := b] a
  , KVList.HasKey lb '[la := a, lb := b] b
  ) => SqlSelect (KVList '[ la := a, lb := b ]) (KVList '[ la := recA, lb := recB ]) where
  sqlSelectCols :: IdentInfo
-> KVList '[la := a, lb := b] -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList '[la := a, lb := b]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList '[la := a, lb := b]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList '[la := a, lb := b]
r :: b)
  sqlSelectColCount :: Proxy (KVList '[la := a, lb := b]) -> Int
sqlSelectColCount Proxy (KVList '[la := a, lb := b])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b))
  sqlSelectProcessRow :: [PersistValue] -> Either Text (KVList '[la := recA, lb := recB])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , kvs ~ '[ la := a, lb := b, lc := c]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c]) (KVList '[ la := recA, lb := recB, lc := recC ]) where
  sqlSelectCols :: IdentInfo
-> KVList '[la := a, lb := b, lc := c] -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList '[la := a, lb := b, lc := c]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList '[la := a, lb := b, lc := c]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList '[la := a, lb := b, lc := c]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList '[la := a, lb := b, lc := c]
r :: c)
  sqlSelectColCount :: Proxy (KVList '[la := a, lb := b, lc := c]) -> Int
sqlSelectColCount Proxy (KVList '[la := a, lb := b, lc := c])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c))
  sqlSelectProcessRow :: [PersistValue]
-> Either Text (KVList '[la := recA, lb := recB, lc := recC])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD ]) where
  sqlSelectCols :: IdentInfo
-> KVList '[la := a, lb := b, lc := c, ld := d]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList '[la := a, lb := b, lc := c, ld := d]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList '[la := a, lb := b, lc := c, ld := d]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList '[la := a, lb := b, lc := c, ld := d]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList '[la := a, lb := b, lc := c, ld := d]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList '[la := a, lb := b, lc := c, ld := d]
r :: d)
  sqlSelectColCount :: Proxy (KVList '[la := a, lb := b, lc := c, ld := d]) -> Int
sqlSelectColCount Proxy (KVList '[la := a, lb := b, lc := c, ld := d])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text (KVList '[la := recA, lb := recB, lc := recC, ld := recD])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE ]) where
  sqlSelectCols :: IdentInfo
-> KVList '[la := a, lb := b, lc := c, ld := d, le := e]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList '[la := a, lb := b, lc := c, ld := d, le := e]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList '[la := a, lb := b, lc := c, ld := d, le := e]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList '[la := a, lb := b, lc := c, ld := d, le := e]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList '[la := a, lb := b, lc := c, ld := d, le := e]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList '[la := a, lb := b, lc := c, ld := d, le := e]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList '[la := a, lb := b, lc := c, ld := d, le := e]
r :: e)
  sqlSelectColCount :: Proxy (KVList '[la := a, lb := b, lc := c, ld := d, le := e])
-> Int
sqlSelectColCount Proxy (KVList '[la := a, lb := b, lc := c, ld := d, le := e])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF ]) where
  sqlSelectCols :: IdentInfo
-> KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f]
r :: f)
  sqlSelectColCount :: Proxy
  (KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f])
-> Int
sqlSelectColCount Proxy
  (KVList '[la := a, lb := b, lc := c, ld := d, le := e, lf := f])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g]
r :: g)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h]
r :: h)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i]
r :: i)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , SqlSelect j rj
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , KnownSymbol lj
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , ToKVList rj recJ
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  , KVList.HasKey lj kvs j
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI, lj := recJ ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: i, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j]
r :: j)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i, j))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI, lj := recJ])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri, rj
rj :: rj) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      recJ
j <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rj
rj
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recJ
j

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , SqlSelect j rj
  , SqlSelect k rk
  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , KnownSymbol lj
  , KnownSymbol lk
  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , ToKVList rj recJ
  , ToKVList rk recK
  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  , KVList.HasKey lj kvs j
  , KVList.HasKey lk kvs k
  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI, lj := recJ, lk := recK ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: i, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: j, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k]
r :: k)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i, j, k))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI, lj := recJ,
          lk := recK])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri, rj
rj :: rj, rk
rk :: rk) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      recJ
j <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rj
rj
      recK
k <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rk
rk
      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recJ
j
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recK
k

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , SqlSelect j rj
  , SqlSelect k rk
  , SqlSelect l rl

  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , KnownSymbol lj
  , KnownSymbol lk
  , KnownSymbol ll

  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , ToKVList rj recJ
  , ToKVList rk recK
  , ToKVList rl recL

  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  , KVList.HasKey lj kvs j
  , KVList.HasKey lk kvs k
  , KVList.HasKey ll kvs l

  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI, lj := recJ, lk := recK, ll := recL ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: i, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: j, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: k, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l]
r :: l)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i, j, k, l))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI, lj := recJ,
          lk := recK, ll := recL])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri, rj
rj :: rj, rk
rk :: rk, rl
rl :: rl) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      recJ
j <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rj
rj
      recK
k <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rk
rk
      recL
l <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rl
rl

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recJ
j
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recK
k
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recL
l

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , SqlSelect j rj
  , SqlSelect k rk
  , SqlSelect l rl
  , SqlSelect m rm

  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , KnownSymbol lj
  , KnownSymbol lk
  , KnownSymbol ll
  , KnownSymbol lm

  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , ToKVList rj recJ
  , ToKVList rk recK
  , ToKVList rl recL
  , ToKVList rm recM

  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  , KVList.HasKey lj kvs j
  , KVList.HasKey lk kvs k
  , KVList.HasKey ll kvs l
  , KVList.HasKey lm kvs m

  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI, lj := recJ, lk := recK, ll := recL, lm := recM ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: i, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: j, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: k, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: l, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m]
r :: m)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i, j, k, l, m))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI, lj := recJ,
          lk := recK, ll := recL, lm := recM])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri, rj
rj :: rj, rk
rk :: rk, rl
rl :: rl, rm
rm :: rm) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      recJ
j <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rj
rj
      recK
k <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rk
rk
      recL
l <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rl
rl
      recM
m <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rm
rm

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recJ
j
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recK
k
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recL
l
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recM
m

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , SqlSelect j rj
  , SqlSelect k rk
  , SqlSelect l rl
  , SqlSelect m rm
  , SqlSelect n rn

  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , KnownSymbol lj
  , KnownSymbol lk
  , KnownSymbol ll
  , KnownSymbol lm
  , KnownSymbol ln

  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , ToKVList rj recJ
  , ToKVList rk recK
  , ToKVList rl recL
  , ToKVList rm recM
  , ToKVList rn recN

  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  , KVList.HasKey lj kvs j
  , KVList.HasKey lk kvs k
  , KVList.HasKey ll kvs l
  , KVList.HasKey lm kvs m
  , KVList.HasKey ln kvs n

  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI, lj := recJ, lk := recK, ll := recL, lm := recM, ln := recN ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: i, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: j, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: k, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: l, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: m, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ln) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n]
r :: n)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i, j, k, l, m, n))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI, lj := recJ,
          lk := recK, ll := recL, lm := recM, ln := recN])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri, rj
rj :: rj, rk
rk :: rk, rl
rl :: rl, rm
rm :: rm, rn
rn :: rn) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      recJ
j <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rj
rj
      recK
k <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rk
rk
      recL
l <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rl
rl
      recM
m <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rm
rm
      recN
n <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rn
rn

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recJ
j
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recK
k
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recL
l
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recM
m
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ln) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recN
n

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , SqlSelect j rj
  , SqlSelect k rk
  , SqlSelect l rl
  , SqlSelect m rm
  , SqlSelect n rn
  , SqlSelect o ro

  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , KnownSymbol lj
  , KnownSymbol lk
  , KnownSymbol ll
  , KnownSymbol lm
  , KnownSymbol ln
  , KnownSymbol lo

  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , ToKVList rj recJ
  , ToKVList rk recK
  , ToKVList rl recL
  , ToKVList rm recM
  , ToKVList rn recN
  , ToKVList ro recO

  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n, lo := o ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  , KVList.HasKey lj kvs j
  , KVList.HasKey lk kvs k
  , KVList.HasKey ll kvs l
  , KVList.HasKey lm kvs m
  , KVList.HasKey ln kvs n
  , KVList.HasKey lo kvs o

  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n, lo := o ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI, lj := recJ, lk := recK, ll := recL, lm := recM, ln := recN, lo := recO ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
       lo := o]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: i, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: j, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: k, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: l, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: m, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ln) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: n, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lo) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o]
r :: o)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
       lo := o])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
       lo := o])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI, lj := recJ,
          lk := recK, ll := recL, lm := recM, ln := recN, lo := recO])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri, rj
rj :: rj, rk
rk :: rk, rl
rl :: rl, rm
rm :: rm, rn
rn :: rn, ro
ro :: ro) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      recJ
j <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rj
rj
      recK
k <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rk
rk
      recL
l <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rl
rl
      recM
m <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rm
rm
      recN
n <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rn
rn
      recO
o <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ro
ro

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recJ
j
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recK
k
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recL
l
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recM
m
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ln) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recN
n
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lo) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recO
o

instance
  ( SqlSelect a ra
  , SqlSelect b rb
  , SqlSelect c rc
  , SqlSelect d rd
  , SqlSelect e re
  , SqlSelect f rf
  , SqlSelect g rg
  , SqlSelect h rh
  , SqlSelect i ri
  , SqlSelect j rj
  , SqlSelect k rk
  , SqlSelect l rl
  , SqlSelect m rm
  , SqlSelect n rn
  , SqlSelect o ro
  , SqlSelect p rp

  , KnownSymbol la
  , KnownSymbol lb
  , KnownSymbol lc
  , KnownSymbol ld
  , KnownSymbol le
  , KnownSymbol lf
  , KnownSymbol lg
  , KnownSymbol lh
  , KnownSymbol li
  , KnownSymbol lj
  , KnownSymbol lk
  , KnownSymbol ll
  , KnownSymbol lm
  , KnownSymbol ln
  , KnownSymbol lo
  , KnownSymbol lp

  , ToKVList ra recA
  , ToKVList rb recB
  , ToKVList rc recC
  , ToKVList rd recD
  , ToKVList re recE
  , ToKVList rf recF
  , ToKVList rg recG
  , ToKVList rh recH
  , ToKVList ri recI
  , ToKVList rj recJ
  , ToKVList rk recK
  , ToKVList rl recL
  , ToKVList rm recM
  , ToKVList rn recN
  , ToKVList ro recO
  , ToKVList rp recP

  , kvs ~ '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n, lo := o, lp := p ]
  , KVList.HasKey la kvs a
  , KVList.HasKey lb kvs b
  , KVList.HasKey lc kvs c
  , KVList.HasKey ld kvs d
  , KVList.HasKey le kvs e
  , KVList.HasKey lf kvs f
  , KVList.HasKey lg kvs g
  , KVList.HasKey lh kvs h
  , KVList.HasKey li kvs i
  , KVList.HasKey lj kvs j
  , KVList.HasKey lk kvs k
  , KVList.HasKey ll kvs l
  , KVList.HasKey lm kvs m
  , KVList.HasKey ln kvs n
  , KVList.HasKey lo kvs o
  , KVList.HasKey lp kvs p

  ) => SqlSelect (KVList '[ la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g, lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n, lo := o, lp := p ]) (KVList '[ la := recA, lb := recB, lc := recC, ld := recD, le := recE, lf := recF, lg := recG, lh := recH, li := recI, lj := recJ, lk := recK, ll := recL, lm := recM, ln := recN, lo := recO, lp := recP ]) where
  sqlSelectCols :: IdentInfo
-> KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
       lo := o, lp := p]
-> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r =
    forall a r.
SqlSelect a r =>
IdentInfo -> a -> (Builder, [PersistValue])
sqlSelectCols IdentInfo
esc (forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: a, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: b, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: c, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: d, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: e, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: f, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: g, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: h, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: i, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: j, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: k, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: l, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: m, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey ln) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: n, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lo) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: o, forall (key :: Symbol) (kvs :: [*]) v.
(KnownSymbol key, HasKey key kvs v) =>
ListKey key -> KVList kvs -> v
KVList.get (forall (t :: Symbol). ListKey t
ListKey :: ListKey lp) KVList
  '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
    lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
    lo := o, lp := p]
r :: p)
  sqlSelectColCount :: Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
       lo := o, lp := p])
-> Int
sqlSelectColCount Proxy
  (KVList
     '[la := a, lb := b, lc := c, ld := d, le := e, lf := f, lg := g,
       lh := h, li := i, lj := j, lk := k, ll := l, lm := m, ln := n,
       lo := o, lp := p])
_ =
    forall a r. SqlSelect a r => Proxy a -> Int
sqlSelectColCount (forall {k} (t :: k). Proxy t
Proxy :: Proxy (a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p))
  sqlSelectProcessRow :: [PersistValue]
-> Either
     Text
     (KVList
        '[la := recA, lb := recB, lc := recC, ld := recD, le := recE,
          lf := recF, lg := recG, lh := recH, li := recI, lj := recJ,
          lk := recK, ll := recL, lm := recM, ln := recN, lo := recO,
          lp := recP])
sqlSelectProcessRow [PersistValue]
vs =
    do
      (ra
ra :: ra, rb
rb :: rb, rc
rc :: rc, rd
rd :: rd, re
re :: re, rf
rf :: rf, rg
rg :: rg, rh
rh :: rh, ri
ri :: ri, rj
rj :: rj, rk
rk :: rk, rl
rl :: rl, rm
rm :: rm, rn
rn :: rn, ro
ro :: ro, rp
rp :: rp) <- forall a r. SqlSelect a r => [PersistValue] -> Either Text r
sqlSelectProcessRow [PersistValue]
vs
      recA
a <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ra
ra
      recB
b <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rb
rb
      recC
c <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rc
rc
      recD
d <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rd
rd
      recE
e <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList re
re
      recF
f <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rf
rf
      recG
g <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rg
rg
      recH
h <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rh
rh
      recI
i <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ri
ri
      recJ
j <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rj
rj
      recK
k <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rk
rk
      recL
l <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rl
rl
      recM
m <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rm
rm
      recN
n <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rn
rn
      recO
o <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList ro
ro
      recP
p <- forall a kvls. ToKVList a kvls => a -> Either Text kvls
toKVList rp
rp

      forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$
        KVList '[]
KVList.empty
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey la) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recA
a
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lb) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recB
b
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lc) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recC
c
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ld) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recD
d
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey le) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recE
e
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lf) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recF
f
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lg) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recG
g
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lh) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recH
h
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey li) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recI
i
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lj) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recJ
j
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lk) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recK
k
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ll) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recL
l
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lm) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recM
m
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey ln) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recN
n
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lo) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recO
o
          forall (k :: Symbol) (kvs :: [*]) v (appended :: [*]).
(KnownSymbol k, Appended kvs '[k := v] ~ appended) =>
KVList kvs -> (k := v) -> KVList appended
&= (forall (t :: Symbol). ListKey t
ListKey :: ListKey lp) forall (key :: Symbol) value. ListKey key -> value -> key := value
:= recP
p