{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DataKinds             #-}
{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}

-- | Full record representation
--
-- Intended for qualified import.
--
-- > import Data.Record.Anon.Internal.Advanced (Record)
-- > import qualified Data.Record.Anon.Internal.Advanced as A
module Data.Record.Anon.Internal.Advanced (
    -- * Definition
    Record -- opaque
    -- * Main API
  , Field(..)
  , empty
  , insert
  , insertA
  , get
  , set
  , merge
  , lens
  , project
  , inject
  , applyPending
    -- * Combinators
    -- ** " Foldable "
  , map
  , cmap
    -- ** " Applicable "
  , pure
  , cpure
  , ap
    -- ** " Foldable "
  , collapse
  , toList
    -- ** " Traversable "
  , mapM
  , cmapM
  , sequenceA
  , sequenceA'
    -- ** Zipping
  , zip
  , zipWith
  , zipWithM
  , czipWith
  , czipWithM
    -- * Reification and reflection
  , reifyKnownFields
  , reflectKnownFields
  , reifyAllFields
  , reflectAllFields
  , InRow(..)
  , reifySubRow
  , reflectSubRow
    -- * Existential records
  , Some(..)
  , SomeRecord(..)
  , someRecord
    -- * Support for @typelet@
  , letRecordT
  , letInsertAs
  ) where

import Prelude hiding (map, mapM, zip, zipWith, sequenceA, pure)
import qualified Prelude

import Data.Aeson (ToJSON(..), FromJSON(..))
import Data.Bifunctor
import Data.Coerce (coerce)
import Data.Functor.Product
import Data.Kind
import Data.Primitive.SmallArray
import Data.Proxy
import Data.Record.Generic hiding (FieldName)
import Data.SOP.Classes (fn_2)
import Data.SOP.Constraint
import Data.Tagged
import GHC.Exts (Any)
import GHC.OverloadedLabels
import GHC.Records.Compat
import GHC.TypeLits
import TypeLet.UserAPI

import qualified Optics.Core as Optics

import qualified Data.Record.Generic.Eq   as Generic
import qualified Data.Record.Generic.JSON as Generic
import qualified Data.Record.Generic.Show as Generic

import Data.Record.Anon.Internal.Core.Canonical (Canonical)
import Data.Record.Anon.Internal.Core.Diff (Diff)
import Data.Record.Anon.Internal.Core.FieldName
import Data.Record.Anon.Internal.Reflection (Reflected(..))
import Data.Record.Anon.Internal.Util.StrictArray (StrictArray)

import Data.Record.Anon.Plugin.Internal.Runtime

import qualified Data.Record.Anon.Internal.Core.Canonical   as Canon
import qualified Data.Record.Anon.Internal.Core.Diff        as Diff
import qualified Data.Record.Anon.Internal.Reflection       as Unsafe
import qualified Data.Record.Anon.Internal.Util.StrictArray as Strict

{-------------------------------------------------------------------------------
  Definition
-------------------------------------------------------------------------------}

-- | Anonymous record
data Record (f :: k -> Type) (r :: Row k) =
    NoPending  {-# UNPACK #-} !(Canonical f)
  | HasPending {-# UNPACK #-} !(Canonical f) !(Diff f)

{-------------------------------------------------------------------------------
  Conversion
-------------------------------------------------------------------------------}

-- | Construct canonical form of the record (i.e., apply the internal 'Diff')
--
-- This is @O(n)@, and should be done only for operations on records that are
-- @O(n)@ /anyway/, so that the cost can be absorbed.
toCanonical :: Record f r -> Canonical f
toCanonical :: Record f r -> Canonical f
toCanonical (NoPending  Canonical f
c)   = Canonical f
c
toCanonical (HasPending Canonical f
c Diff f
d) = Diff f -> Canonical f -> Canonical f
forall k (f :: k -> *). Diff f -> Canonical f -> Canonical f
Diff.apply Diff f
d Canonical f
c

-- | Construct 'Record' from 'Canonical' representation (empty 'Diff')
--
-- This function is unsafe because we cannot verify whether the record matches
-- it's row specification @r@.
unsafeFromCanonical :: Canonical f -> Record f r
unsafeFromCanonical :: Canonical f -> Record f r
unsafeFromCanonical = Canonical f -> Record f r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
NoPending

{-------------------------------------------------------------------------------
  HasField
-------------------------------------------------------------------------------}

-- | Proxy for a field name, with 'IsLabel' instance
--
-- The 'IsLabel' instance makes it possible to write
--
-- > #foo
--
-- to mean
--
-- > Field (Proxy @"foo")
data Field n where
  Field :: (KnownSymbol n, KnownHash n) => Proxy n -> Field n

instance (n ~ n', KnownSymbol n, KnownHash n) => IsLabel n' (Field n) where
  fromLabel :: Field n
fromLabel = Proxy n -> Field n
forall (n :: Symbol).
(KnownSymbol n, KnownHash n) =>
Proxy n -> Field n
Field (Proxy n
forall k (t :: k). Proxy t
Proxy @n)

instance forall k (n :: Symbol) (f :: k -> Type) (r :: Row k) (a :: k).
       (KnownSymbol n, KnownHash n, RowHasField n r a)
    => HasField n (Record f r) (f a) where

  -- INLINE pragma important: it makes the 'NoPendingCases' cases very close
  -- to the performance of using a 'SmallArray' directly.
  {-# INLINE hasField #-}
  hasField :: Record f r -> (f a -> Record f r, f a)
hasField Record f r
r = (
        \f a
x -> Int -> FieldName -> f a -> Record f r -> Record f r
forall k (f :: k -> *) (r :: Row k) (a :: k).
Int -> FieldName -> f a -> Record f r -> Record f r
unsafeSetField Int
ix FieldName
name f a
x Record f r
r
      , Int -> FieldName -> Record f r -> f a
forall k (f :: k -> *) (r :: Row k) (a :: k).
Int -> FieldName -> Record f r -> f a
unsafeGetField Int
ix FieldName
name Record f r
r
      )
    where
      name :: FieldName
      name :: FieldName
name = Proxy n -> FieldName
forall (n :: Symbol).
(KnownSymbol n, KnownHash n) =>
Proxy n -> FieldName
mkFieldName (Proxy n
forall k (t :: k). Proxy t
Proxy @n)

      ix :: Int
      ix :: Int
ix = Tagged '(n, r, a) Int -> Proxy '(n, r, a) -> Int
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged '(n, r, a) Int
forall k (n :: Symbol) (r :: Row k) (a :: k).
RowHasField n r a =>
DictRowHasField k n r a
rowHasField (Proxy '(n, r, a)
forall k (t :: k). Proxy t
Proxy @'(n, r, a))

-- | Compile-time construction of a 'FieldName'
mkFieldName :: (KnownSymbol n, KnownHash n) => Proxy n -> FieldName
mkFieldName :: Proxy n -> FieldName
mkFieldName Proxy n
p = Int -> String -> FieldName
FieldName (Proxy n -> Int
forall (s :: Symbol) (proxy :: Symbol -> *).
KnownHash s =>
proxy s -> Int
hashVal Proxy n
p) (Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
p)

instance (RowHasField n r a, KnownSymbol n, KnownHash n)
      => Optics.LabelOptic n Optics.A_Lens (Record f r) (Record f r) (f a) (f a) where
  labelOptic :: Optic A_Lens NoIx (Record f r) (Record f r) (f a) (f a)
labelOptic = Field n -> Optic A_Lens NoIx (Record f r) (Record f r) (f a) (f a)
aux (forall a. IsLabel n a => a
forall (x :: Symbol) a. IsLabel x a => a
fromLabel @n)
    where
      aux :: Field n -> Optics.Lens' (Record f r) (f a)
      aux :: Field n -> Optic A_Lens NoIx (Record f r) (Record f r) (f a) (f a)
aux Field n
n = (Record f r -> f a)
-> (Record f r -> f a -> Record f r)
-> Optic A_Lens NoIx (Record f r) (Record f r) (f a) (f a)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
Optics.lens (Field n -> Record f r -> f a
forall k (n :: Symbol) (f :: k -> *) (r :: Row k) (a :: k).
RowHasField n r a =>
Field n -> Record f r -> f a
get Field n
n) ((f a -> Record f r -> Record f r)
-> Record f r -> f a -> Record f r
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Field n -> f a -> Record f r -> Record f r
forall k (n :: Symbol) (f :: k -> *) (r :: Row k) (a :: k).
RowHasField n r a =>
Field n -> f a -> Record f r -> Record f r
set Field n
n))

-- | Low level field accessor
--
-- It is the responsibility of the plugin to ensure that the field index and
-- the field type match.
unsafeGetField :: forall k (f :: k -> Type) (r :: Row k) (a :: k).
    Int -> FieldName -> Record f r -> f a
unsafeGetField :: Int -> FieldName -> Record f r -> f a
unsafeGetField Int
i FieldName
n = f Any -> f a
co (f Any -> f a) -> (Record f r -> f Any) -> Record f r -> f a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \case
    NoPending  Canonical f
c   -> Canonical f -> Int -> f Any
forall k (f :: k -> *). Canonical f -> Int -> f Any
Canon.getAtIndex Canonical f
c Int
i
    HasPending Canonical f
c Diff f
d -> (Int, FieldName) -> Diff f -> Canonical f -> f Any
forall k (f :: k -> *).
(Int, FieldName) -> Diff f -> Canonical f -> f Any
Diff.get (Int
i, FieldName
n) Diff f
d Canonical f
c
  where
    co  :: f Any -> f a
    co :: f Any -> f a
co = f Any -> f a
forall a b. a -> b
noInlineUnsafeCo

-- | Low level field update
--
-- See comments in 'getField'.
unsafeSetField :: forall k (f :: k -> Type) (r :: Row k) (a :: k).
    Int -> FieldName -> f a -> Record f r -> Record f r
unsafeSetField :: Int -> FieldName -> f a -> Record f r -> Record f r
unsafeSetField Int
i FieldName
n f a
x = \case
    NoPending  Canonical f
c   -> Canonical f -> Diff f -> Record f r
forall k (f :: k -> *) (r :: Row k).
Canonical f -> Diff f -> Record f r
HasPending Canonical f
c (Diff f -> Diff f
go Diff f
forall k (f :: k -> *). Diff f
Diff.empty)
    HasPending Canonical f
c Diff f
d -> Canonical f -> Diff f -> Record f r
forall k (f :: k -> *) (r :: Row k).
Canonical f -> Diff f -> Record f r
HasPending Canonical f
c (Diff f -> Diff f
go Diff f
d)
  where
    go :: Diff f -> Diff f
    go :: Diff f -> Diff f
go = (Int, FieldName) -> f Any -> Diff f -> Diff f
forall k (f :: k -> *).
(Int, FieldName) -> f Any -> Diff f -> Diff f
Diff.set (Int
i, FieldName
n) (f a -> f Any
co f a
x)

    co :: f a -> f Any
    co :: f a -> f Any
co = f a -> f Any
forall a b. a -> b
noInlineUnsafeCo

get :: forall n f r a.
     RowHasField n r a
  => Field n -> Record f r -> f a
get :: Field n -> Record f r -> f a
get (Field Proxy n
_) = forall a. HasField n (Record f r) a => Record f r -> a
forall k (x :: k) r a. HasField x r a => r -> a
getField @n @(Record f r)

set :: forall n f r a.
     RowHasField n r a
  => Field n -> f a -> Record f r -> Record f r
set :: Field n -> f a -> Record f r -> Record f r
set (Field Proxy n
_) = (Record f r -> f a -> Record f r)
-> f a -> Record f r -> Record f r
forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall a.
HasField n (Record f r) a =>
Record f r -> a -> Record f r
forall k (x :: k) r a. HasField x r a => r -> a -> r
setField @n @(Record f r))

{-------------------------------------------------------------------------------
  Main API
-------------------------------------------------------------------------------}

empty :: Record f '[]
empty :: Record f '[]
empty = Canonical f -> Record f '[]
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
NoPending Canonical f
forall a. Monoid a => a
mempty

insert :: forall k (f :: k -> Type) (r :: Row k) (a :: k) (n :: Symbol).
    Field n -> f a -> Record f r -> Record f (n := a : r)
insert :: Field n -> f a -> Record f r -> Record f ((n ':= a) : r)
insert (Field Proxy n
n) f a
x = \case
    NoPending  Canonical f
c   -> Canonical f -> Diff f -> Record f ((n ':= a) : r)
forall k (f :: k -> *) (r :: Row k).
Canonical f -> Diff f -> Record f r
HasPending Canonical f
c (Diff f -> Diff f
go Diff f
forall k (f :: k -> *). Diff f
Diff.empty)
    HasPending Canonical f
c Diff f
d -> Canonical f -> Diff f -> Record f ((n ':= a) : r)
forall k (f :: k -> *) (r :: Row k).
Canonical f -> Diff f -> Record f r
HasPending Canonical f
c (Diff f -> Diff f
go Diff f
d)
  where
    go :: Diff f -> Diff f
    go :: Diff f -> Diff f
go = FieldName -> f Any -> Diff f -> Diff f
forall k (f :: k -> *). FieldName -> f Any -> Diff f -> Diff f
Diff.insert (Proxy n -> FieldName
forall (n :: Symbol).
(KnownSymbol n, KnownHash n) =>
Proxy n -> FieldName
mkFieldName Proxy n
n) (f a -> f Any
co f a
x)

    co :: f a -> f Any
    co :: f a -> f Any
co = f a -> f Any
forall a b. a -> b
noInlineUnsafeCo

insertA ::
     Applicative m
  => Field n -> m (f a) -> m (Record f r) -> m (Record f (n := a : r))
insertA :: Field n
-> m (f a) -> m (Record f r) -> m (Record f ((n ':= a) : r))
insertA Field n
f m (f a)
x m (Record f r)
r = Field n -> f a -> Record f r -> Record f ((n ':= a) : r)
forall k (f :: k -> *) (r :: Row k) (a :: k) (n :: Symbol).
Field n -> f a -> Record f r -> Record f ((n ':= a) : r)
insert Field n
f (f a -> Record f r -> Record f ((n ':= a) : r))
-> m (f a) -> m (Record f r -> Record f ((n ':= a) : r))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (f a)
x m (Record f r -> Record f ((n ':= a) : r))
-> m (Record f r) -> m (Record f ((n ':= a) : r))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> m (Record f r)
r

merge :: Record f r -> Record f r' -> Record f (Merge r r')
merge :: Record f r -> Record f r' -> Record f (Merge r r')
merge (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) (Record f r' -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r') =
    Canonical f -> Record f (Merge r r')
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical f -> Record f (Merge r r'))
-> Canonical f -> Record f (Merge r r')
forall a b. (a -> b) -> a -> b
$ Canonical f
r Canonical f -> Canonical f -> Canonical f
forall a. Semigroup a => a -> a -> a
<> Canonical f
r'

lens :: forall f r r'.
     SubRow r r'
  => Record f r -> (Record f r', Record f r' -> Record f r)
lens :: Record f r -> (Record f r', Record f r' -> Record f r)
lens = \(Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) ->
    (Canonical f -> Record f r')
-> ((Canonical f -> Canonical f) -> Record f r' -> Record f r)
-> (Canonical f, Canonical f -> Canonical f)
-> (Record f r', Record f r' -> Record f r)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Canonical f -> Record f r'
getter (Canonical f -> Canonical f) -> Record f r' -> Record f r
setter ((Canonical f, Canonical f -> Canonical f)
 -> (Record f r', Record f r' -> Record f r))
-> (Canonical f, Canonical f -> Canonical f)
-> (Record f r', Record f r' -> Record f r)
forall a b. (a -> b) -> a -> b
$
      StrictArray Int
-> Canonical f -> (Canonical f, Canonical f -> Canonical f)
forall k (f :: k -> *).
StrictArray Int
-> Canonical f -> (Canonical f, Canonical f -> Canonical f)
Canon.lens (Tagged '(r, r') (StrictArray Int)
-> Proxy '(r, r') -> StrictArray Int
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged '(r, r') (StrictArray Int)
forall k (r :: Row k) (r' :: Row k).
SubRow r r' =>
DictSubRow k r r'
projectIndices (Proxy '(r, r')
forall k (t :: k). Proxy t
Proxy @'(r, r'))) Canonical f
r
  where
    getter :: Canonical f -> Record f r'
    getter :: Canonical f -> Record f r'
getter = Canonical f -> Record f r'
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical

    setter :: (Canonical f -> Canonical f) -> Record f r' -> Record f r
    setter :: (Canonical f -> Canonical f) -> Record f r' -> Record f r
setter Canonical f -> Canonical f
f (Record f r' -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) = Canonical f -> Record f r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical f -> Canonical f
f Canonical f
r)

-- | Project out subrecord
--
-- This is just the 'lens' getter.
project :: SubRow r r' => Record f r -> Record f r'
project :: Record f r -> Record f r'
project = (Record f r', Record f r' -> Record f r) -> Record f r'
forall a b. (a, b) -> a
fst ((Record f r', Record f r' -> Record f r) -> Record f r')
-> (Record f r -> (Record f r', Record f r' -> Record f r))
-> Record f r
-> Record f r'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record f r -> (Record f r', Record f r' -> Record f r)
forall k (f :: k -> *) (r :: Row k) (r' :: Row k).
SubRow r r' =>
Record f r -> (Record f r', Record f r' -> Record f r)
lens

-- | Inject subrecord
--
-- This is just the 'lens' setter.
inject :: SubRow r r' => Record f r' -> Record f r -> Record f r
inject :: Record f r' -> Record f r -> Record f r
inject Record f r'
small = ((Record f r' -> Record f r) -> Record f r' -> Record f r
forall a b. (a -> b) -> a -> b
$ Record f r'
small) ((Record f r' -> Record f r) -> Record f r)
-> (Record f r -> Record f r' -> Record f r)
-> Record f r
-> Record f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Record f r', Record f r' -> Record f r)
-> Record f r' -> Record f r
forall a b. (a, b) -> b
snd ((Record f r', Record f r' -> Record f r)
 -> Record f r' -> Record f r)
-> (Record f r -> (Record f r', Record f r' -> Record f r))
-> Record f r
-> Record f r'
-> Record f r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record f r -> (Record f r', Record f r' -> Record f r)
forall k (f :: k -> *) (r :: Row k) (r' :: Row k).
SubRow r r' =>
Record f r -> (Record f r', Record f r' -> Record f r)
lens

applyPending :: Record f r -> Record f r
applyPending :: Record f r -> Record f r
applyPending (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) = Canonical f -> Record f r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical Canonical f
r

{-------------------------------------------------------------------------------
  Unconstrained combinators
-------------------------------------------------------------------------------}

map :: (forall x. f x -> g x) -> Record f r -> Record g r
map :: (forall (x :: k). f x -> g x) -> Record f r -> Record g r
map forall (x :: k). f x -> g x
f (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) = Canonical g -> Record g r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical g -> Record g r) -> Canonical g -> Record g r
forall a b. (a -> b) -> a -> b
$
    (forall (x :: k). f x -> g x) -> Canonical f -> Canonical g
forall k (f :: k -> *) (g :: k -> *).
(forall (x :: k). f x -> g x) -> Canonical f -> Canonical g
Canon.map forall (x :: k). f x -> g x
f Canonical f
r

mapM ::
     Applicative m
  => (forall x. f x -> m (g x))
  -> Record f r -> m (Record g r)
mapM :: (forall (x :: k). f x -> m (g x)) -> Record f r -> m (Record g r)
mapM forall (x :: k). f x -> m (g x)
f (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) = (Canonical g -> Record g r) -> m (Canonical g) -> m (Record g r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Canonical g -> Record g r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (m (Canonical g) -> m (Record g r))
-> m (Canonical g) -> m (Record g r)
forall a b. (a -> b) -> a -> b
$
    (forall (x :: k). f x -> m (g x)) -> Canonical f -> m (Canonical g)
forall k (m :: * -> *) (f :: k -> *) (g :: k -> *).
Applicative m =>
(forall (x :: k). f x -> m (g x)) -> Canonical f -> m (Canonical g)
Canon.mapM forall (x :: k). f x -> m (g x)
f Canonical f
r

zip :: Record f r -> Record g r -> Record (Product f g) r
zip :: Record f r -> Record g r -> Record (Product f g) r
zip = (forall (x :: k). f x -> g x -> Product f g x)
-> Record f r -> Record g r -> Record (Product f g) r
forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (r :: Row k).
(forall (x :: k). f x -> g x -> h x)
-> Record f r -> Record g r -> Record h r
zipWith forall (x :: k). f x -> g x -> Product f g x
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair

zipWith ::
     (forall x. f x -> g x -> h x)
  -> Record f r -> Record g r -> Record h r
zipWith :: (forall (x :: k). f x -> g x -> h x)
-> Record f r -> Record g r -> Record h r
zipWith forall (x :: k). f x -> g x -> h x
f (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) (Record g r -> Canonical g
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical g
r') = Canonical h -> Record h r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical h -> Record h r) -> Canonical h -> Record h r
forall a b. (a -> b) -> a -> b
$
    (forall (x :: k). f x -> g x -> h x)
-> Canonical f -> Canonical g -> Canonical h
forall k (f :: k -> *) (g :: k -> *) (h :: k -> *).
(forall (x :: k). f x -> g x -> h x)
-> Canonical f -> Canonical g -> Canonical h
Canon.zipWith forall (x :: k). f x -> g x -> h x
f Canonical f
r Canonical g
r'

zipWithM ::
     Applicative m
  => (forall x. f x -> g x -> m (h x))
  -> Record f r -> Record g r -> m (Record h r)
zipWithM :: (forall (x :: k). f x -> g x -> m (h x))
-> Record f r -> Record g r -> m (Record h r)
zipWithM forall (x :: k). f x -> g x -> m (h x)
f (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) (Record g r -> Canonical g
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical g
r') = (Canonical h -> Record h r) -> m (Canonical h) -> m (Record h r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Canonical h -> Record h r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (m (Canonical h) -> m (Record h r))
-> m (Canonical h) -> m (Record h r)
forall a b. (a -> b) -> a -> b
$
    (forall (x :: k). f x -> g x -> m (h x))
-> Canonical f -> Canonical g -> m (Canonical h)
forall k (m :: * -> *) (f :: k -> *) (g :: k -> *) (h :: k -> *).
Applicative m =>
(forall (x :: k). f x -> g x -> m (h x))
-> Canonical f -> Canonical g -> m (Canonical h)
Canon.zipWithM forall (x :: k). f x -> g x -> m (h x)
f Canonical f
r Canonical g
r'

collapse :: Record (K a) r -> [a]
collapse :: Record (K a) r -> [a]
collapse (Record (K a) r -> Canonical (K a)
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical (K a)
r) =
    Canonical (K a) -> [a]
forall k a. Canonical (K a) -> [a]
Canon.collapse Canonical (K a)
r

sequenceA :: Applicative m => Record (m :.: f) r -> m (Record f r)
sequenceA :: Record (m :.: f) r -> m (Record f r)
sequenceA (Record (m :.: f) r -> Canonical (m :.: f)
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical (m :.: f)
r) = (Canonical f -> Record f r) -> m (Canonical f) -> m (Record f r)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Canonical f -> Record f r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (m (Canonical f) -> m (Record f r))
-> m (Canonical f) -> m (Record f r)
forall a b. (a -> b) -> a -> b
$
    Canonical (m :.: f) -> m (Canonical f)
forall k (m :: * -> *) (f :: k -> *).
Applicative m =>
Canonical (m :.: f) -> m (Canonical f)
Canon.sequenceA Canonical (m :.: f)
r

sequenceA' :: Applicative m => Record m r -> m (Record I r)
sequenceA' :: Record m r -> m (Record I r)
sequenceA' = Record (m :.: I) r -> m (Record I r)
forall k (m :: * -> *) (f :: k -> *) (r :: Row k).
Applicative m =>
Record (m :.: f) r -> m (Record f r)
sequenceA (Record (m :.: I) r -> m (Record I r))
-> (Record m r -> Record (m :.: I) r)
-> Record m r
-> m (Record I r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record m r -> Record (m :.: I) r
forall (m :: * -> *) (r :: Row *). Record m r -> Record (m :.: I) r
co
  where
    co :: Record m r -> Record (m :.: I) r
    co :: Record m r -> Record (m :.: I) r
co = Record m r -> Record (m :.: I) r
forall a b. a -> b
noInlineUnsafeCo

pure :: forall f r. KnownFields r => (forall x. f x) -> Record f r
pure :: (forall (x :: k). f x) -> Record f r
pure forall (x :: k). f x
f = Canonical f -> Record f r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical f -> Record f r) -> Canonical f -> Record f r
forall a b. (a -> b) -> a -> b
$
    [f Any] -> Canonical f
forall k (f :: k -> *). [f Any] -> Canonical f
Canon.fromList ([f Any] -> Canonical f) -> [f Any] -> Canonical f
forall a b. (a -> b) -> a -> b
$ (String -> f Any) -> [String] -> [f Any]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map (f Any -> String -> f Any
forall a b. a -> b -> a
const f Any
forall (x :: k). f x
f) (Tagged r [String] -> Proxy r -> [String]
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged r [String]
forall k (r :: Row k). KnownFields r => DictKnownFields k r
fieldNames (Proxy r
forall k (t :: k). Proxy t
Proxy @r))

ap :: Record (f -.-> g) r -> Record f r -> Record g r
ap :: Record (f -.-> g) r -> Record f r -> Record g r
ap (Record (f -.-> g) r -> Canonical (f -.-> g)
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical (f -.-> g)
r) (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r') = Canonical g -> Record g r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical g -> Record g r) -> Canonical g -> Record g r
forall a b. (a -> b) -> a -> b
$
    Canonical (f -.-> g) -> Canonical f -> Canonical g
forall k (f :: k -> *) (g :: k -> *).
Canonical (f -.-> g) -> Canonical f -> Canonical g
Canon.ap Canonical (f -.-> g)
r Canonical f
r'

{-------------------------------------------------------------------------------
  Reification and reflection

  The @KnownFields@ constraint on @reifyProject@ is a little dissatisfying, as
  it feels like an orthogonal concern. Ultimately the reason is that in

  > Record f (r :: Row k)

  we have @f :: k -> Type@, as opposed to @f :: Symbol -> k -> Type@. That is
  a generalization we could at some point consider, but until we do, the

  > RowHasField n r a

  constraint introduced in the body 'InRow' involves an /existential/ @n@;
  a /separate/ record with 'KnownSymbol' evidence would therefore not give us
  any information about /this/ @n@.
-------------------------------------------------------------------------------}

reifyKnownFields :: forall k (r :: Row k) proxy.
     KnownFields r
  => proxy r -> Record (K String) r
reifyKnownFields :: proxy r -> Record (K String) r
reifyKnownFields proxy r
_ =
    Canonical (K String) -> Record (K String) r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical (K String) -> Record (K String) r)
-> Canonical (K String) -> Record (K String) r
forall a b. (a -> b) -> a -> b
$
      [K String Any] -> Canonical (K String)
forall k (f :: k -> *). [f Any] -> Canonical f
Canon.fromList ([K String Any] -> Canonical (K String))
-> [K String Any] -> Canonical (K String)
forall a b. (a -> b) -> a -> b
$ [String] -> [K String Any]
forall k. [String] -> [K String Any]
co ([String] -> [K String Any]) -> [String] -> [K String Any]
forall a b. (a -> b) -> a -> b
$ Tagged r [String] -> Proxy r -> [String]
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged r [String]
forall k (r :: Row k). KnownFields r => DictKnownFields k r
fieldNames (Proxy r
forall k (t :: k). Proxy t
Proxy @r)
  where
    co :: [String] -> [K String Any]
    co :: [String] -> [K String Any]
co = [String] -> [K String Any]
coerce

reflectKnownFields :: forall k (r :: Row k).
     Record (K String) r
  -> Reflected (KnownFields r)
reflectKnownFields :: Record (K String) r -> Reflected (KnownFields r)
reflectKnownFields Record (K String) r
names =
    DictKnownFields k r -> Reflected (KnownFields r)
forall k (r :: Row k).
DictKnownFields k r -> Reflected (KnownFields r)
Unsafe.reflectKnownFields (DictKnownFields k r -> Reflected (KnownFields r))
-> DictKnownFields k r -> Reflected (KnownFields r)
forall a b. (a -> b) -> a -> b
$ [String] -> DictKnownFields k r
forall k (s :: k) b. b -> Tagged s b
Tagged ([String] -> DictKnownFields k r)
-> [String] -> DictKnownFields k r
forall a b. (a -> b) -> a -> b
$ Record (K String) r -> [String]
forall k a (r :: Row k). Record (K a) r -> [a]
collapse Record (K String) r
names

reifyAllFields :: forall k (r :: Row k) (c :: k -> Constraint) proxy.
     AllFields r c
  => proxy c -> Record (Dict c) r
reifyAllFields :: proxy c -> Record (Dict c) r
reifyAllFields proxy c
_ = Canonical (Dict c) -> Record (Dict c) r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical (Dict c) -> Record (Dict c) r)
-> Canonical (Dict c) -> Record (Dict c) r
forall a b. (a -> b) -> a -> b
$
    StrictArray (Dict c Any) -> Canonical (Dict c)
forall k (f :: k -> *). StrictArray (f Any) -> Canonical f
Canon.fromVector (StrictArray (Dict c Any) -> Canonical (Dict c))
-> (SmallArray (Dict c Any) -> StrictArray (Dict c Any))
-> SmallArray (Dict c Any)
-> Canonical (Dict c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SmallArray (Dict c Any) -> StrictArray (Dict c Any)
forall a. SmallArray a -> StrictArray a
Strict.fromLazy (SmallArray (Dict c Any) -> Canonical (Dict c))
-> SmallArray (Dict c Any) -> Canonical (Dict c)
forall a b. (a -> b) -> a -> b
$
      (DictAny c -> Dict c Any)
-> SmallArray (DictAny c) -> SmallArray (Dict c Any)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DictAny c -> Dict c Any
aux (SmallArray (DictAny c) -> SmallArray (Dict c Any))
-> SmallArray (DictAny c) -> SmallArray (Dict c Any)
forall a b. (a -> b) -> a -> b
$ Tagged r (SmallArray (DictAny c))
-> Proxy r -> SmallArray (DictAny c)
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged r (SmallArray (DictAny c))
forall k (r :: Row k) (c :: k -> Constraint).
AllFields r c =>
DictAllFields k r c
fieldDicts (Proxy r
forall k (t :: k). Proxy t
Proxy @r)
  where
    aux :: DictAny c -> Dict c Any
    aux :: DictAny c -> Dict c Any
aux DictAny c
DictAny = Dict c Any
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

reflectAllFields :: forall k (c :: k -> Constraint) (r :: Row k).
     Record (Dict c) r
  -> Reflected (AllFields r c)
reflectAllFields :: Record (Dict c) r -> Reflected (AllFields r c)
reflectAllFields Record (Dict c) r
dicts =
    DictAllFields k r c -> Reflected (AllFields r c)
forall k (r :: Row k) (c :: k -> Constraint).
DictAllFields k r c -> Reflected (AllFields r c)
Unsafe.reflectAllFields (DictAllFields k r c -> Reflected (AllFields r c))
-> DictAllFields k r c -> Reflected (AllFields r c)
forall a b. (a -> b) -> a -> b
$ SmallArray (DictAny c) -> DictAllFields k r c
forall k (s :: k) b. b -> Tagged s b
Tagged (SmallArray (DictAny c) -> DictAllFields k r c)
-> SmallArray (DictAny c) -> DictAllFields k r c
forall a b. (a -> b) -> a -> b
$
      (Dict c Any -> DictAny c)
-> SmallArray (Dict c Any) -> SmallArray (DictAny c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Dict c Any -> DictAny c
aux (SmallArray (Dict c Any) -> SmallArray (DictAny c))
-> SmallArray (Dict c Any) -> SmallArray (DictAny c)
forall a b. (a -> b) -> a -> b
$ StrictArray (Dict c Any) -> SmallArray (Dict c Any)
forall a. StrictArray a -> SmallArray a
Strict.toLazy (StrictArray (Dict c Any) -> SmallArray (Dict c Any))
-> StrictArray (Dict c Any) -> SmallArray (Dict c Any)
forall a b. (a -> b) -> a -> b
$ Canonical (Dict c) -> StrictArray (Dict c Any)
forall k (f :: k -> *). Canonical f -> StrictArray (f Any)
Canon.toVector (Canonical (Dict c) -> StrictArray (Dict c Any))
-> Canonical (Dict c) -> StrictArray (Dict c Any)
forall a b. (a -> b) -> a -> b
$ Record (Dict c) r -> Canonical (Dict c)
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical Record (Dict c) r
dicts
  where
    aux :: Dict c Any -> DictAny c
    aux :: Dict c Any -> DictAny c
aux Dict c Any
Dict = DictAny c
forall k (c :: k -> Constraint). c Any => DictAny c
DictAny

-- | @InRow r a@ is evidence that there exists some @n@ s.t. @(n := a)@ in @r@.
data InRow (r :: Row k) (a :: k) where
  InRow :: forall k (n :: Symbol) (r :: Row k) (a :: k).
       ( KnownSymbol n
       , RowHasField n r a
       )
    => Proxy n -> InRow r a

reifySubRow :: forall k (r :: Row k) (r' :: Row k).
     (SubRow r r', KnownFields r')
  => Record (InRow r) r'
reifySubRow :: Record (InRow r) r'
reifySubRow =
    (forall (x :: k). K Int x -> K String x -> InRow r x)
-> Record (K Int) r' -> Record (K String) r' -> Record (InRow r) r'
forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (r :: Row k).
(forall (x :: k). f x -> g x -> h x)
-> Record f r -> Record g r -> Record h r
zipWith forall (x :: k). K Int x -> K String x -> InRow r x
aux Record (K Int) r'
ixs (Proxy r' -> Record (K String) r'
forall k (r :: Row k) (proxy :: Row k -> *).
KnownFields r =>
proxy r -> Record (K String) r
reifyKnownFields (Proxy r'
forall k (t :: k). Proxy t
Proxy @r'))
  where
    ixs :: Record (K Int) r'
    ixs :: Record (K Int) r'
ixs = Canonical (K Int) -> Record (K Int) r'
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical (K Int) -> Record (K Int) r')
-> Canonical (K Int) -> Record (K Int) r'
forall a b. (a -> b) -> a -> b
$
            StrictArray (K Int Any) -> Canonical (K Int)
forall k (f :: k -> *). StrictArray (f Any) -> Canonical f
Canon.fromVector (StrictArray (K Int Any) -> Canonical (K Int))
-> StrictArray (K Int Any) -> Canonical (K Int)
forall a b. (a -> b) -> a -> b
$ StrictArray Int -> StrictArray (K Int Any)
forall k. StrictArray Int -> StrictArray (K Int Any)
co (StrictArray Int -> StrictArray (K Int Any))
-> StrictArray Int -> StrictArray (K Int Any)
forall a b. (a -> b) -> a -> b
$ Tagged '(r, r') (StrictArray Int)
-> Proxy '(r, r') -> StrictArray Int
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged '(r, r') (StrictArray Int)
forall k (r :: Row k) (r' :: Row k).
SubRow r r' =>
DictSubRow k r r'
projectIndices (Proxy '(r, r')
forall k (t :: k). Proxy t
Proxy @'(r, r'))

    co :: StrictArray Int -> StrictArray (K Int Any)
    co :: StrictArray Int -> StrictArray (K Int Any)
co = StrictArray Int -> StrictArray (K Int Any)
coerce

    aux :: forall x. K Int x -> K String x -> InRow r x
    aux :: K Int x -> K String x -> InRow r x
aux (K Int
i) (K String
name) =
        case String -> SomeSymbol
someSymbolVal String
name of
          SomeSymbol Proxy n
p -> Int -> Proxy n -> InRow r x
forall k (n :: Symbol) (r :: Row k) (a :: k).
KnownSymbol n =>
Int -> Proxy n -> InRow r a
unsafeInRow Int
i Proxy n
p

reflectSubRow :: forall k (r :: Row k) (r' :: Row k).
     Record (InRow r) r'
  -> Reflected (SubRow r r')
reflectSubRow :: Record (InRow r) r' -> Reflected (SubRow r r')
reflectSubRow (Record (InRow r) r' -> Canonical (InRow r)
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical (InRow r)
ixs) =
    DictSubRow k r r' -> Reflected (SubRow r r')
forall k (r :: Row k) (r' :: Row k).
DictSubRow k r r' -> Reflected (SubRow r r')
Unsafe.reflectSubRow (DictSubRow k r r' -> Reflected (SubRow r r'))
-> DictSubRow k r r' -> Reflected (SubRow r r')
forall a b. (a -> b) -> a -> b
$ StrictArray Int -> DictSubRow k r r'
forall k (s :: k) b. b -> Tagged s b
Tagged (StrictArray Int -> DictSubRow k r r')
-> StrictArray Int -> DictSubRow k r r'
forall a b. (a -> b) -> a -> b
$
      (\inRow :: InRow r Any
inRow@(InRow Proxy n
p) -> InRow r Any -> Proxy n -> Int
forall (x :: k) (n :: Symbol).
RowHasField n r x =>
InRow r x -> Proxy n -> Int
aux InRow r Any
inRow Proxy n
p) (InRow r Any -> Int)
-> StrictArray (InRow r Any) -> StrictArray Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Canonical (InRow r) -> StrictArray (InRow r Any)
forall k (f :: k -> *). Canonical f -> StrictArray (f Any)
Canon.toVector Canonical (InRow r)
ixs
  where
    aux :: forall x n. RowHasField n r x => InRow r x -> Proxy n -> Int
    aux :: InRow r x -> Proxy n -> Int
aux InRow r x
_ Proxy n
_ = Tagged '(n, r, x) Int -> Proxy '(n, r, x) -> Int
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged '(n, r, x) Int
forall k (n :: Symbol) (r :: Row k) (a :: k).
RowHasField n r a =>
DictRowHasField k n r a
rowHasField (Proxy '(n, r, x)
forall k (t :: k). Proxy t
Proxy @'(n, r, x))

unsafeInRow :: forall n r a. KnownSymbol n => Int -> Proxy n -> InRow r a
unsafeInRow :: Int -> Proxy n -> InRow r a
unsafeInRow Int
i Proxy n
p =
    case Reflected (RowHasField n r a)
reflected of
      Reflected (RowHasField n r a)
Reflected -> Proxy n -> InRow r a
forall k (n :: Symbol) (r :: Row k) (a :: k).
(KnownSymbol n, RowHasField n r a) =>
Proxy n -> InRow r a
InRow Proxy n
p
  where
    reflected :: Reflected (RowHasField n r a)
    reflected :: Reflected (RowHasField n r a)
reflected = DictRowHasField k n r a -> Reflected (RowHasField n r a)
forall k (n :: Symbol) (r :: Row k) (a :: k).
DictRowHasField k n r a -> Reflected (RowHasField n r a)
Unsafe.reflectRowHasField (DictRowHasField k n r a -> Reflected (RowHasField n r a))
-> DictRowHasField k n r a -> Reflected (RowHasField n r a)
forall a b. (a -> b) -> a -> b
$ Int -> DictRowHasField k n r a
forall k (s :: k) b. b -> Tagged s b
Tagged Int
i

{-------------------------------------------------------------------------------
  Existential records
-------------------------------------------------------------------------------}

-- | Existential type ("there exists an @x@ such that @f x@")
data Some (f :: k -> Type) where
  Some :: forall k (f :: k -> Type) (x :: k). f x -> Some f

-- | Discovered row variable
--
-- See 'Data.Record.Anon.Advanced.someRecord' for detailed discussion.
data SomeRecord (f :: k -> Type) where
  SomeRecord :: forall k (r :: Row k) (f :: k -> Type).
       KnownFields r
    => Record (Product (InRow r) f) r
    -> SomeRecord f

someRecord :: forall k (f :: k -> Type). [(String, Some f)] -> SomeRecord f
someRecord :: [(String, Some f)] -> SomeRecord f
someRecord [(String, Some f)]
fields =
    Record (Product (InRow Any) f) Any -> SomeRecord f
forall (r :: Row k). Record (Product (InRow r) f) r -> SomeRecord f
mkSomeRecord (Record (Product (InRow Any) f) Any -> SomeRecord f)
-> Record (Product (InRow Any) f) Any -> SomeRecord f
forall a b. (a -> b) -> a -> b
$
      Canonical (Product (InRow Any) f)
-> Record (Product (InRow Any) f) Any
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical (Product (InRow Any) f)
 -> Record (Product (InRow Any) f) Any)
-> ([Product (InRow Any) f Any]
    -> Canonical (Product (InRow Any) f))
-> [Product (InRow Any) f Any]
-> Record (Product (InRow Any) f) Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Product (InRow Any) f Any] -> Canonical (Product (InRow Any) f)
forall k (f :: k -> *). [f Any] -> Canonical f
Canon.fromList ([Product (InRow Any) f Any] -> Record (Product (InRow Any) f) Any)
-> [Product (InRow Any) f Any]
-> Record (Product (InRow Any) f) Any
forall a b. (a -> b) -> a -> b
$
        (Int -> (SomeSymbol, Some f) -> Product (InRow Any) f Any)
-> [Int] -> [(SomeSymbol, Some f)] -> [Product (InRow Any) f Any]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Prelude.zipWith Int -> (SomeSymbol, Some f) -> Product (InRow Any) f Any
forall (r :: Row k).
Int -> (SomeSymbol, Some f) -> Product (InRow r) f Any
aux [Int
0..] (((String, Some f) -> (SomeSymbol, Some f))
-> [(String, Some f)] -> [(SomeSymbol, Some f)]
forall a b. (a -> b) -> [a] -> [b]
Prelude.map ((String -> SomeSymbol) -> (String, Some f) -> (SomeSymbol, Some f)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first String -> SomeSymbol
someSymbolVal) [(String, Some f)]
fields)
  where
    aux :: Int -> (SomeSymbol, Some f) -> Product (InRow r) f Any
    aux :: Int -> (SomeSymbol, Some f) -> Product (InRow r) f Any
aux Int
i (SomeSymbol Proxy n
n, Some f x
fx) = InRow r Any -> f Any -> Product (InRow r) f Any
forall k (f :: k -> *) (g :: k -> *) (a :: k).
f a -> g a -> Product f g a
Pair (Int -> Proxy n -> InRow r Any
forall k (n :: Symbol) (r :: Row k) (a :: k).
KnownSymbol n =>
Int -> Proxy n -> InRow r a
unsafeInRow Int
i Proxy n
n) (f x -> f Any
forall (x :: k). f x -> f Any
co f x
fx)

    co :: f x -> f Any
    co :: f x -> f Any
co = f x -> f Any
forall a b. a -> b
noInlineUnsafeCo

    mkSomeRecord :: forall r. Record (Product (InRow r) f) r -> SomeRecord f
    mkSomeRecord :: Record (Product (InRow r) f) r -> SomeRecord f
mkSomeRecord Record (Product (InRow r) f) r
r =
        case Reflected (KnownFields r)
reflected of
          Reflected (KnownFields r)
Reflected -> Record (Product (InRow r) f) r -> SomeRecord f
forall k (r :: Row k) (f :: k -> *).
KnownFields r =>
Record (Product (InRow r) f) r -> SomeRecord f
SomeRecord Record (Product (InRow r) f) r
r
      where
        reflected :: Reflected (KnownFields r)
        reflected :: Reflected (KnownFields r)
reflected = Record (K String) r -> Reflected (KnownFields r)
forall k (r :: Row k).
Record (K String) r -> Reflected (KnownFields r)
reflectKnownFields (Record (K String) r -> Reflected (KnownFields r))
-> Record (K String) r -> Reflected (KnownFields r)
forall a b. (a -> b) -> a -> b
$ (forall (x :: k). Product (InRow r) f x -> K String x)
-> Record (Product (InRow r) f) r -> Record (K String) r
forall k (f :: k -> *) (g :: k -> *) (r :: Row k).
(forall (x :: k). f x -> g x) -> Record f r -> Record g r
map forall (x :: k). Product (InRow r) f x -> K String x
getName Record (Product (InRow r) f) r
r

        getName :: Product (InRow r) f x -> K String x
        getName :: Product (InRow r) f x -> K String x
getName (Pair (InRow Proxy n
p) f x
_) = String -> K String x
forall k a (b :: k). a -> K a b
K (String -> K String x) -> String -> K String x
forall a b. (a -> b) -> a -> b
$ Proxy n -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy n
p

{-------------------------------------------------------------------------------
  Conversion to/from generic 'Rep'
-------------------------------------------------------------------------------}

recordToRep :: Record f r -> Rep I (Record f r)
recordToRep :: Record f r -> Rep I (Record f r)
recordToRep (Record f r -> Canonical f
forall k (f :: k -> *) (r :: Row k). Record f r -> Canonical f
toCanonical -> Canonical f
r) =
    SmallArray (I Any) -> Rep I (Record f r)
forall (f :: * -> *) a. SmallArray (f Any) -> Rep f a
Rep (SmallArray (I Any) -> Rep I (Record f r))
-> SmallArray (I Any) -> Rep I (Record f r)
forall a b. (a -> b) -> a -> b
$ SmallArray (f Any) -> SmallArray (I Any)
forall k (f :: k -> *). SmallArray (f Any) -> SmallArray (I Any)
co (SmallArray (f Any) -> SmallArray (I Any))
-> (Canonical f -> SmallArray (f Any))
-> Canonical f
-> SmallArray (I Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StrictArray (f Any) -> SmallArray (f Any)
forall a. StrictArray a -> SmallArray a
Strict.toLazy (StrictArray (f Any) -> SmallArray (f Any))
-> (Canonical f -> StrictArray (f Any))
-> Canonical f
-> SmallArray (f Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Canonical f -> StrictArray (f Any)
forall k (f :: k -> *). Canonical f -> StrictArray (f Any)
Canon.toVector (Canonical f -> SmallArray (I Any))
-> Canonical f -> SmallArray (I Any)
forall a b. (a -> b) -> a -> b
$ Canonical f
r
  where
    -- Second @Any@ is really (f (Any))
    co :: SmallArray (f Any) -> SmallArray (I Any)
    co :: SmallArray (f Any) -> SmallArray (I Any)
co = SmallArray (f Any) -> SmallArray (I Any)
forall a b. a -> b
noInlineUnsafeCo

repToRecord :: Rep I (Record f r) -> Record f r
repToRecord :: Rep I (Record f r) -> Record f r
repToRecord (Rep SmallArray (I Any)
r) =
    Canonical f -> Record f r
forall k (f :: k -> *) (r :: Row k). Canonical f -> Record f r
unsafeFromCanonical (Canonical f -> Record f r) -> Canonical f -> Record f r
forall a b. (a -> b) -> a -> b
$ StrictArray (f Any) -> Canonical f
forall k (f :: k -> *). StrictArray (f Any) -> Canonical f
Canon.fromVector (StrictArray (f Any) -> Canonical f)
-> (SmallArray (I Any) -> StrictArray (f Any))
-> SmallArray (I Any)
-> Canonical f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SmallArray (f Any) -> StrictArray (f Any)
forall a. SmallArray a -> StrictArray a
Strict.fromLazy (SmallArray (f Any) -> StrictArray (f Any))
-> (SmallArray (I Any) -> SmallArray (f Any))
-> SmallArray (I Any)
-> StrictArray (f Any)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SmallArray (I Any) -> SmallArray (f Any)
forall k (f :: k -> *). SmallArray (I Any) -> SmallArray (f Any)
co (SmallArray (I Any) -> Canonical f)
-> SmallArray (I Any) -> Canonical f
forall a b. (a -> b) -> a -> b
$ SmallArray (I Any)
r
  where
    -- First @Any@ is really (f Any)@
    co :: SmallArray (I Any) -> SmallArray (f Any)
    co :: SmallArray (I Any) -> SmallArray (f Any)
co = SmallArray (I Any) -> SmallArray (f Any)
forall a b. a -> b
noInlineUnsafeCo

{-------------------------------------------------------------------------------
  Generics instance
-------------------------------------------------------------------------------}

class    (AllFields r (Compose c f), KnownFields r) => RecordConstraints f r c
instance (AllFields r (Compose c f), KnownFields r) => RecordConstraints f r c

recordConstraints :: forall f r c.
     RecordConstraints f r c
  => Proxy c -> Rep (Dict c) (Record f r)
recordConstraints :: Proxy c -> Rep (Dict c) (Record f r)
recordConstraints Proxy c
_ = SmallArray (Dict c Any) -> Rep (Dict c) (Record f r)
forall (f :: * -> *) a. SmallArray (f Any) -> Rep f a
Rep (SmallArray (Dict c Any) -> Rep (Dict c) (Record f r))
-> SmallArray (Dict c Any) -> Rep (Dict c) (Record f r)
forall a b. (a -> b) -> a -> b
$
    Dict (Compose c f) Any -> Dict c Any
co (Dict (Compose c f) Any -> Dict c Any)
-> (DictAny (Compose c f) -> Dict (Compose c f) Any)
-> DictAny (Compose c f)
-> Dict c Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DictAny (Compose c f) -> Dict (Compose c f) Any
aux (DictAny (Compose c f) -> Dict c Any)
-> SmallArray (DictAny (Compose c f)) -> SmallArray (Dict c Any)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Tagged r (SmallArray (DictAny (Compose c f)))
-> Proxy r -> SmallArray (DictAny (Compose c f))
forall k (s :: k) a (proxy :: k -> *). Tagged s a -> proxy s -> a
proxy Tagged r (SmallArray (DictAny (Compose c f)))
forall k (r :: Row k) (c :: k -> Constraint).
AllFields r c =>
DictAllFields k r c
fieldDicts (Proxy r
forall k (t :: k). Proxy t
Proxy @r)
  where
    aux :: DictAny (Compose c f) -> Dict (Compose c f) Any
    aux :: DictAny (Compose c f) -> Dict (Compose c f) Any
aux DictAny (Compose c f)
DictAny = Dict (Compose c f) Any
forall k (c :: k -> Constraint) (a :: k). c a => Dict c a
Dict

    -- The second 'Any' is really (f Any)
    co :: Dict (Compose c f) Any -> Dict c Any
    co :: Dict (Compose c f) Any -> Dict c Any
co = Dict (Compose c f) Any -> Dict c Any
forall a b. a -> b
noInlineUnsafeCo

recordMetadata :: forall k (f :: k -> Type) (r :: Row k).
     KnownFields r
  => Metadata (Record f r)
recordMetadata :: Metadata (Record f r)
recordMetadata = Metadata :: forall a.
String -> String -> Int -> Rep FieldMetadata a -> Metadata a
Metadata {
      recordName :: String
recordName          = String
"Record"
    , recordConstructor :: String
recordConstructor   = String
"Record"
    , recordSize :: Int
recordSize          = [FieldMetadata Any] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FieldMetadata Any]
fields
    , recordFieldMetadata :: Rep FieldMetadata (Record f r)
recordFieldMetadata = SmallArray (FieldMetadata Any) -> Rep FieldMetadata (Record f r)
forall (f :: * -> *) a. SmallArray (f Any) -> Rep f a
Rep (SmallArray (FieldMetadata Any) -> Rep FieldMetadata (Record f r))
-> SmallArray (FieldMetadata Any) -> Rep FieldMetadata (Record f r)
forall a b. (a -> b) -> a -> b
$ [FieldMetadata Any] -> SmallArray (FieldMetadata Any)
forall a. [a] -> SmallArray a
smallArrayFromList [FieldMetadata Any]
fields
    }
  where
    fields :: [FieldMetadata Any]
    fields :: [FieldMetadata Any]
fields = Proxy r -> [FieldMetadata Any]
forall k (r :: Row k) (proxy :: Row k -> *).
KnownFields r =>
proxy r -> [FieldMetadata Any]
fieldMetadata (Proxy r
forall k (t :: k). Proxy t
Proxy @r)

instance KnownFields r => Generic (Record f r) where
  type Constraints (Record f r) = RecordConstraints f r
  type MetadataOf  (Record f r) = FieldTypes        f r

  from :: Record f r -> Rep I (Record f r)
from     = Record f r -> Rep I (Record f r)
forall k (f :: k -> *) (r :: Row k).
Record f r -> Rep I (Record f r)
recordToRep
  to :: Rep I (Record f r) -> Record f r
to       = Rep I (Record f r) -> Record f r
forall k (f :: k -> *) (r :: Row k).
Rep I (Record f r) -> Record f r
repToRecord
  dict :: Proxy c -> Rep (Dict c) (Record f r)
dict     = Proxy c -> Rep (Dict c) (Record f r)
forall k (f :: k -> *) (r :: Row k) (c :: * -> Constraint).
RecordConstraints f r c =>
Proxy c -> Rep (Dict c) (Record f r)
recordConstraints
  metadata :: proxy (Record f r) -> Metadata (Record f r)
metadata = Metadata (Record f r)
-> proxy (Record f r) -> Metadata (Record f r)
forall a b. a -> b -> a
const Metadata (Record f r)
forall k (f :: k -> *) (r :: Row k).
KnownFields r =>
Metadata (Record f r)
recordMetadata

{-------------------------------------------------------------------------------
  Instances for standard type classes

  These instances all depend on the generics integration.
-------------------------------------------------------------------------------}

instance RecordConstraints f r Show => Show (Record f r) where
  showsPrec :: Int -> Record f r -> ShowS
showsPrec = Int -> Record f r -> ShowS
forall a. (Generic a, Constraints a Show) => Int -> a -> ShowS
Generic.gshowsPrec

instance RecordConstraints f r Eq => Eq (Record f r) where
  == :: Record f r -> Record f r -> Bool
(==) = Record f r -> Record f r -> Bool
forall a. (Generic a, Constraints a Eq) => a -> a -> Bool
Generic.geq

instance ( RecordConstraints f r Eq
         , RecordConstraints f r Ord
         ) => Ord (Record f r) where
  compare :: Record f r -> Record f r -> Ordering
compare = Record f r -> Record f r -> Ordering
forall a. (Generic a, Constraints a Ord) => a -> a -> Ordering
Generic.gcompare

instance RecordConstraints f r ToJSON => ToJSON (Record f r) where
  toJSON :: Record f r -> Value
toJSON = Record f r -> Value
forall a. (Generic a, Constraints a ToJSON) => a -> Value
Generic.gtoJSON

instance RecordConstraints f r FromJSON => FromJSON (Record f r) where
  parseJSON :: Value -> Parser (Record f r)
parseJSON = Value -> Parser (Record f r)
forall a. (Generic a, Constraints a FromJSON) => Value -> Parser a
Generic.gparseJSON

{-------------------------------------------------------------------------------
  UTIL. Not sure if we still need this
-------------------------------------------------------------------------------}

{-

data Constrained (c :: k -> Constraint) (f :: k -> Type) (x :: k) where
  Constrained :: c x => f x -> Constrained c f x

constrain :: forall k (c :: k -> Constraint) (f :: k -> Type) (r :: Row k).
      AllFields r c
   => Proxy c -> Record f r -> Record (Constrained c f) r
constrain p (Record.toCanonical -> r) = Record.unsafeFromCanonical $
    Canon.fromLazyVector $
      V.zipWith aux (Canon.toLazyVector r) (fieldDicts (Proxy @r) p)
  where
    aux :: f Any -> DictAny c -> Constrained c f Any
    aux x DictAny = Constrained x

-}

{-------------------------------------------------------------------------------
  Constrained combinators
-------------------------------------------------------------------------------}

cpure :: forall r f c.
     AllFields r c
  => Proxy c
  -> (forall x. c x => f x)
  -> Record f r
cpure :: Proxy c -> (forall (x :: k). c x => f x) -> Record f r
cpure Proxy c
p forall (x :: k). c x => f x
f = (forall (x :: k). Dict c x -> f x)
-> Record (Dict c) r -> Record f r
forall k (f :: k -> *) (g :: k -> *) (r :: Row k).
(forall (x :: k). f x -> g x) -> Record f r -> Record g r
map (\Dict c x
Dict -> f x
forall (x :: k). c x => f x
f) (Record (Dict c) r -> Record f r)
-> Record (Dict c) r -> Record f r
forall a b. (a -> b) -> a -> b
$ Proxy c -> Record (Dict c) r
forall k (r :: Row k) (c :: k -> Constraint)
       (proxy :: (k -> Constraint) -> *).
AllFields r c =>
proxy c -> Record (Dict c) r
reifyAllFields Proxy c
p

cmap :: forall r c f g.
     AllFields r c
  => Proxy c
  -> (forall x. c x => f x -> g x)
  -> Record f r -> Record g r
cmap :: Proxy c
-> (forall (x :: k). c x => f x -> g x) -> Record f r -> Record g r
cmap Proxy c
p forall (x :: k). c x => f x -> g x
f = (forall (x :: k). Dict c x -> f x -> g x)
-> Record (Dict c) r -> Record f r -> Record g r
forall k (f :: k -> *) (g :: k -> *) (h :: k -> *) (r :: Row k).
(forall (x :: k). f x -> g x -> h x)
-> Record f r -> Record g r -> Record h r
zipWith (\Dict c x
Dict -> f x -> g x
forall (x :: k). c x => f x -> g x
f) (Proxy c -> Record (Dict c) r
forall k (r :: Row k) (c :: k -> Constraint)
       (proxy :: (k -> Constraint) -> *).
AllFields r c =>
proxy c -> Record (Dict c) r
reifyAllFields Proxy c
p)

cmapM ::
     (Applicative m, AllFields r c)
  => Proxy c
  -> (forall x. c x => f x -> m (g x))
  -> Record f r -> m (Record g r)
cmapM :: Proxy c
-> (forall (x :: k). c x => f x -> m (g x))
-> Record f r
-> m (Record g r)
cmapM Proxy c
p forall (x :: k). c x => f x -> m (g x)
f = Record (m :.: g) r -> m (Record g r)
forall k (m :: * -> *) (f :: k -> *) (r :: Row k).
Applicative m =>
Record (m :.: f) r -> m (Record f r)
sequenceA (Record (m :.: g) r -> m (Record g r))
-> (Record f r -> Record (m :.: g) r)
-> Record f r
-> m (Record g r)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy c
-> (forall (x :: k). c x => f x -> (:.:) m g x)
-> Record f r
-> Record (m :.: g) r
forall k (r :: Row k) (c :: k -> Constraint) (f :: k -> *)
       (g :: k -> *).
AllFields r c =>
Proxy c
-> (forall (x :: k). c x => f x -> g x) -> Record f r -> Record g r
cmap Proxy c
p (m (g x) -> (:.:) m g x
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (m (g x) -> (:.:) m g x) -> (f x -> m (g x)) -> f x -> (:.:) m g x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f x -> m (g x)
forall (x :: k). c x => f x -> m (g x)
f)

toList :: forall r a. KnownFields r => Record (K a) r -> [(String, a)]
toList :: Record (K a) r -> [(String, a)]
toList = (FieldMetadata Any -> a -> (String, a))
-> [FieldMetadata Any] -> [a] -> [(String, a)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
Prelude.zipWith FieldMetadata Any -> a -> (String, a)
forall b. FieldMetadata b -> a -> (String, a)
aux (Proxy r -> [FieldMetadata Any]
forall k (r :: Row k) (proxy :: Row k -> *).
KnownFields r =>
proxy r -> [FieldMetadata Any]
fieldMetadata (Proxy r
forall k (t :: k). Proxy t
Proxy @r)) ([a] -> [(String, a)])
-> (Record (K a) r -> [a]) -> Record (K a) r -> [(String, a)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Record (K a) r -> [a]
forall k a (r :: Row k). Record (K a) r -> [a]
collapse
  where
    aux :: FieldMetadata b -> a -> (String, a)
    aux :: FieldMetadata b -> a -> (String, a)
aux (FieldMetadata Proxy name
p FieldStrictness
_) a
a = (Proxy name -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal Proxy name
p, a
a)

czipWithM :: forall m r c f g h.
     (Applicative m, AllFields r c)
  => Proxy c
  -> (forall x. c x => f x -> g x -> m (h x))
  -> Record f r -> Record g r -> m (Record h r)
czipWithM :: Proxy c
-> (forall (x :: k). c x => f x -> g x -> m (h x))
-> Record f r
-> Record g r
-> m (Record h r)
czipWithM Proxy c
p forall (x :: k). c x => f x -> g x -> m (h x)
f Record f r
r Record g r
r' =
    Record (m :.: h) r -> m (Record h r)
forall k (m :: * -> *) (f :: k -> *) (r :: Row k).
Applicative m =>
Record (m :.: f) r -> m (Record f r)
sequenceA (Record (m :.: h) r -> m (Record h r))
-> Record (m :.: h) r -> m (Record h r)
forall a b. (a -> b) -> a -> b
$ (forall (x :: k). Dict c x -> (-.->) f (g -.-> (m :.: h)) x)
-> Record (Dict c) r -> Record (f -.-> (g -.-> (m :.: h))) r
forall k (f :: k -> *) (g :: k -> *) (r :: Row k).
(forall (x :: k). f x -> g x) -> Record f r -> Record g r
map ((f x -> g x -> (:.:) m h x) -> (-.->) f (g -.-> (m :.: h)) x
forall k (f :: k -> *) (a :: k) (f' :: k -> *) (f'' :: k -> *).
(f a -> f' a -> f'' a) -> (-.->) f (f' -.-> f'') a
fn_2 ((f x -> g x -> (:.:) m h x) -> (-.->) f (g -.-> (m :.: h)) x)
-> (Dict c x -> f x -> g x -> (:.:) m h x)
-> Dict c x
-> (-.->) f (g -.-> (m :.: h)) x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dict c x -> f x -> g x -> (:.:) m h x
forall (x :: k). Dict c x -> f x -> g x -> (:.:) m h x
f') (Proxy c -> Record (Dict c) r
forall k (r :: Row k) (c :: k -> Constraint)
       (proxy :: (k -> Constraint) -> *).
AllFields r c =>
proxy c -> Record (Dict c) r
reifyAllFields Proxy c
p) Record (f -.-> (g -.-> (m :.: h))) r
-> Record f r -> Record (g -.-> (m :.: h)) r
forall k (f :: k -> *) (g :: k -> *) (r :: Row k).
Record (f -.-> g) r -> Record f r -> Record g r
`ap` Record f r
r Record (g -.-> (m :.: h)) r -> Record g r -> Record (m :.: h) r
forall k (f :: k -> *) (g :: k -> *) (r :: Row k).
Record (f -.-> g) r -> Record f r -> Record g r
`ap` Record g r
r'
  where
    f' :: Dict c x -> f x -> g x -> (m :.: h) x
    f' :: Dict c x -> f x -> g x -> (:.:) m h x
f' Dict c x
Dict f x
fx g x
gx = m (h x) -> (:.:) m h x
forall l k (f :: l -> *) (g :: k -> l) (p :: k).
f (g p) -> (:.:) f g p
Comp (m (h x) -> (:.:) m h x) -> m (h x) -> (:.:) m h x
forall a b. (a -> b) -> a -> b
$ f x -> g x -> m (h x)
forall (x :: k). c x => f x -> g x -> m (h x)
f f x
fx g x
gx

czipWith ::
     AllFields r c
  => Proxy c
  -> (forall x. c x => f x -> g x -> h x)
  -> Record f r -> Record g r -> Record h r
czipWith :: Proxy c
-> (forall (x :: k). c x => f x -> g x -> h x)
-> Record f r
-> Record g r
-> Record h r
czipWith Proxy c
p forall (x :: k). c x => f x -> g x -> h x
f Record f r
a Record g r
b = I (Record h r) -> Record h r
forall a. I a -> a
unI (I (Record h r) -> Record h r) -> I (Record h r) -> Record h r
forall a b. (a -> b) -> a -> b
$ Proxy c
-> (forall (x :: k). c x => f x -> g x -> I (h x))
-> Record f r
-> Record g r
-> I (Record h r)
forall k (m :: * -> *) (r :: Row k) (c :: k -> Constraint)
       (f :: k -> *) (g :: k -> *) (h :: k -> *).
(Applicative m, AllFields r c) =>
Proxy c
-> (forall (x :: k). c x => f x -> g x -> m (h x))
-> Record f r
-> Record g r
-> m (Record h r)
czipWithM Proxy c
p (\f x
x g x
y -> h x -> I (h x)
forall a. a -> I a
I (f x -> g x -> h x
forall (x :: k). c x => f x -> g x -> h x
f f x
x g x
y)) Record f r
a Record g r
b

{-------------------------------------------------------------------------------
  Support for @typelet@
-------------------------------------------------------------------------------}

-- | Introduce type variable for a row
letRecordT :: forall r f.
     (forall r'. Let r' r => Proxy r' -> Record f r)
  -> Record f r
letRecordT :: (forall (r' :: Row k). Let r' r => Proxy r' -> Record f r)
-> Record f r
letRecordT forall (r' :: Row k). Let r' r => Proxy r' -> Record f r
f = Proxy r
-> (forall (r' :: Row k). Let r' r => Proxy r' -> Record f r)
-> Record f r
forall k r (a :: k).
Proxy a -> (forall (b :: k). Let b a => Proxy b -> r) -> r
letT' (Proxy r
forall k (t :: k). Proxy t
Proxy @r) forall (r' :: Row k). Let r' r => Proxy r' -> Record f r
f

-- | Insert field into a record and introduce type variable for the result
letInsertAs :: forall r r' f n a.
     Proxy r       -- ^ Type of the record we are constructing
  -> Field n       -- ^ New field to be inserted
  -> f a           -- ^ Value of the new field
  -> Record f r'   -- ^ Record constructed so far
  -> (forall r''. Let r'' (n := a : r') => Record f r'' -> Record f r)
                   -- ^ Assign type variable to new partial record, and continue
  -> Record f r
letInsertAs :: Proxy r
-> Field n
-> f a
-> Record f r'
-> (forall (r'' :: Row k).
    Let r'' ((n ':= a) : r') =>
    Record f r'' -> Record f r)
-> Record f r
letInsertAs Proxy r
_ Field n
n f a
x Record f r'
r = Record f ((n ':= a) : r')
-> (forall (r'' :: Row k).
    Let r'' ((n ':= a) : r') =>
    Record f r'' -> Record f r)
-> Record f r
forall k r (f :: k -> *) (a :: k).
f a -> (forall (b :: k). Let b a => f b -> r) -> r
letAs' (Field n -> f a -> Record f r' -> Record f ((n ':= a) : r')
forall k (f :: k -> *) (r :: Row k) (a :: k) (n :: Symbol).
Field n -> f a -> Record f r -> Record f ((n ':= a) : r)
insert Field n
n f a
x Record f r'
r)