{-# LANGUAGE ConstraintKinds, DataKinds, FlexibleContexts, FlexibleInstances,
             KindSignatures, MultiParamTypeClasses, PolyKinds,
             ScopedTypeVariables, TypeFamilies, TypeOperators,
             UndecidableInstances, TemplateHaskell, QuasiQuotes,
             Rank2Types, TypeApplications, AllowAmbiguousTypes #-}
module Frames.Joins (innerJoin
                    , outerJoin
                    , leftJoin
                    , rightJoin)
where
import Data.Discrimination
import Data.Foldable as F
import Frames.Frame
import Frames.Rec
import Frames.InCore (toFrame)
import Frames.Melt (RDeleteAll)
import Frames.InCore (RecVec)
import Data.Vinyl.TypeLevel
import Data.Vinyl
import Data.Vinyl.Functor
mergeRec :: forall fs rs rs2 rs2'.
  (fs ⊆ rs2
  , rs2' ⊆ rs2
  , rs2' ~ RDeleteAll fs rs2
  , rs ⊆ (rs ++ rs2')) =>
  Record rs ->
  Record rs2 ->
  Record (rs ++ rs2')
{-# INLINE mergeRec #-}
mergeRec :: Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec Record rs
rec1 Record rs2
rec2 =
  Record rs
rec1 Record rs -> Rec ElField rs2' -> Record (rs ++ rs2')
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Rec ElField rs2'
rec2'
  where
    rec2' :: Rec ElField rs2'
rec2' = Record rs2 -> Rec ElField rs2'
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @rs2' Record rs2
rec2
innerJoin :: forall fs rs rs2 rs2'.
  (fs    ⊆ rs
    , fs   ⊆ rs2
    , rs ⊆ (rs ++ rs2')
    , rs2' ⊆ rs2
    , rs2' ~ RDeleteAll fs rs2
    , Grouping (Record fs)
    , RecVec rs
    , RecVec rs2'
    , RecVec (rs ++ rs2')
    ) =>
  Frame (Record rs)  
  -> Frame (Record rs2) 
  -> Frame (Record (rs ++ rs2')) 
innerJoin :: Frame (Record rs)
-> Frame (Record rs2) -> Frame (Record (rs ++ rs2'))
innerJoin Frame (Record rs)
a Frame (Record rs2)
b =
    [Record (rs ++ rs2')] -> Frame (Record (rs ++ rs2'))
forall (f :: * -> *) (rs :: [(Symbol, *)]).
(Foldable f, RecVec rs) =>
f (Record rs) -> Frame (Record rs)
toFrame ([Record (rs ++ rs2')] -> Frame (Record (rs ++ rs2')))
-> [Record (rs ++ rs2')] -> Frame (Record (rs ++ rs2'))
forall a b. (a -> b) -> a -> b
$
    [[Record (rs ++ rs2')]] -> [Record (rs ++ rs2')]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
    (Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Record (rs ++ rs2'))
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Record (rs ++ rs2')]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d -> (a -> b -> c) -> (a -> d) -> (b -> d) -> [a] -> [b] -> [[c]]
inner Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeFun Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b))
    where
      {-# INLINE mergeFun #-}
      mergeFun :: Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeFun = forall (rs :: [(Symbol, *)]) (rs2 :: [(Symbol, *)])
       (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
 rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
       (rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
 rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs
      {-# INLINE proj1 #-}
      proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
      {-# INLINE proj2 #-}
      proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
justsFromRec :: RMap fs => Record fs -> Rec (Maybe :. ElField) fs
{-# INLINE justsFromRec #-}
justsFromRec :: Record fs -> Rec (Maybe :. ElField) fs
justsFromRec = (forall (x :: (Symbol, *)). ElField x -> (:.) Maybe ElField x)
-> Record fs -> Rec (Maybe :. ElField) fs
forall u (rs :: [u]) (f :: u -> *) (g :: u -> *).
RMap rs =>
(forall (x :: u). f x -> g x) -> Rec f rs -> Rec g rs
rmap (Maybe (ElField x) -> Compose Maybe ElField x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose (Maybe (ElField x) -> Compose Maybe ElField x)
-> (ElField x -> Maybe (ElField x))
-> ElField x
-> Compose Maybe ElField x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ElField x -> Maybe (ElField x)
forall a. a -> Maybe a
Just)
mkNothingsRec :: forall fs.
  (RecApplicative fs) =>
  Rec (Maybe :. ElField) fs
{-# INLINE mkNothingsRec #-}
mkNothingsRec :: Rec (Maybe :. ElField) fs
mkNothingsRec = (forall (x :: (Symbol, *)). (:.) Maybe ElField x)
-> Rec (Maybe :. ElField) fs
forall u (rs :: [u]) (f :: u -> *).
RecApplicative rs =>
(forall (x :: u). f x) -> Rec f rs
rpure @fs (Maybe (ElField x) -> Compose Maybe ElField x
forall l k (f :: l -> *) (g :: k -> l) (x :: k).
f (g x) -> Compose f g x
Compose Maybe (ElField x)
forall a. Maybe a
Nothing)
outerJoin :: forall fs rs rs' rs2  rs2' ors.
  (fs    ⊆ rs
    , fs   ⊆ rs2
    , rs ⊆ (rs ++ rs2')
    , rs' ⊆ rs
    , rs' ~ RDeleteAll fs rs
    , rs2' ⊆ rs2
    , rs2' ~ RDeleteAll fs rs2
    , ors ~ (rs ++ rs2')
    , ors :~: (rs' ++ rs2)
    , RecApplicative rs2'
    , RecApplicative rs
    , RecApplicative rs'
    , Grouping (Record fs)
    , RMap rs
    , RMap rs2
    , RMap ors
    , RecVec rs
    , RecVec rs2'
    , RecVec ors
    ) =>
  Frame (Record rs)  
  -> Frame (Record rs2) 
  -> [Rec (Maybe :. ElField) ors] 
outerJoin :: Frame (Record rs)
-> Frame (Record rs2) -> [Rec (Maybe :. ElField) ors]
outerJoin Frame (Record rs)
a Frame (Record rs2)
b =
  [[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  (Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs -> Rec (Maybe :. ElField) ors)
-> (Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Rec (Maybe :. ElField) ors]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d
-> (a -> b -> c)
-> (a -> c)
-> (b -> c)
-> (a -> d)
-> (b -> d)
-> [a]
-> [b]
-> [[c]]
outer Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs -> Rec (Maybe :. ElField) ors
Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty
    Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b))
  where
    {-# INLINE proj1 #-}
    proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
    {-# INLINE proj2 #-}
    proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
    {-# INLINE mergeFun #-}
    mergeFun :: Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs
l Record rs2
r = Record ors -> Rec (Maybe :. ElField) ors
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec (Record ors -> Rec (Maybe :. ElField) ors)
-> Record ors -> Rec (Maybe :. ElField) ors
forall a b. (a -> b) -> a -> b
$ Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
       (rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
 rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs Record rs
l Record rs2
r
    {-# INLINE mergeLeftEmpty #-}
    mergeLeftEmpty :: Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty Record rs
l = Record rs -> Rec (Maybe :. ElField) rs
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs
l Rec (Maybe :. ElField) rs
-> Rec (Maybe :. ElField) rs2'
-> Rec (Maybe :. ElField) (rs ++ rs2')
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> RecApplicative rs2' => Rec (Maybe :. ElField) rs2'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs2'
    {-# INLINE mergeRightEmpty #-}
    mergeRightEmpty :: Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty Record rs2
r = Rec (Maybe :. ElField) (rs' ++ rs2) -> Rec (Maybe :. ElField) ors
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @ors (RecApplicative rs' => Rec (Maybe :. ElField) rs'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs' Rec (Maybe :. ElField) rs'
-> Rec (Maybe :. ElField) rs2
-> Rec (Maybe :. ElField) (rs' ++ rs2)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Record rs2 -> Rec (Maybe :. ElField) rs2
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs2
r)
rightJoin :: forall fs rs rs' rs2  rs2' ors.
  (fs    ⊆ rs
    , fs   ⊆ rs2
    , rs ⊆ (rs ++ rs2')
    , rs' ⊆ rs
    , rs' ~ RDeleteAll fs rs
    , rs2' ⊆ rs2
    , rs2' ~ RDeleteAll fs rs2
    , ors ~ (rs ++ rs2')
    , ors :~: (rs' ++ rs2)
    , RecApplicative rs2'
    , RecApplicative rs
    , RecApplicative rs'
    , Grouping (Record fs)
    , RMap rs2
    , RMap ors
    , RecVec rs
    , RecVec rs2'
    , RecVec ors
    ) =>
  Frame (Record rs)  
  -> Frame (Record rs2) 
  -> [Rec (Maybe :. ElField) ors] 
rightJoin :: Frame (Record rs)
-> Frame (Record rs2) -> [Rec (Maybe :. ElField) ors]
rightJoin Frame (Record rs)
a Frame (Record rs2)
b =
  [[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat  ([[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors])
-> [[Rec (Maybe :. ElField) ors]] -> [Rec (Maybe :. ElField) ors]
forall a b. (a -> b) -> a -> b
$
  Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs2 -> Rec (Maybe :. ElField) ors)
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Rec (Maybe :. ElField) ors]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d
-> (a -> b -> c)
-> (b -> c)
-> (a -> d)
-> (b -> d)
-> [a]
-> [b]
-> [[c]]
rightOuter Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty
  Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b)
  where
    {-# INLINE proj1 #-}
    proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
    {-# INLINE proj2 #-}
    proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
    {-# INLINE mergeFun #-}
    mergeFun :: Record rs -> Record rs2 -> Rec (Maybe :. ElField) ors
mergeFun Record rs
l Record rs2
r = Record ors -> Rec (Maybe :. ElField) ors
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec (Record ors -> Rec (Maybe :. ElField) ors)
-> Record ors -> Rec (Maybe :. ElField) ors
forall a b. (a -> b) -> a -> b
$ Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
       (rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
 rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs Record rs
l Record rs2
r
    {-# INLINE mergeRightEmpty #-}
    mergeRightEmpty :: Record rs2 -> Rec (Maybe :. ElField) ors
mergeRightEmpty Record rs2
r = Rec (Maybe :. ElField) (rs' ++ rs2) -> Rec (Maybe :. ElField) ors
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @ors (RecApplicative rs' => Rec (Maybe :. ElField) rs'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs' Rec (Maybe :. ElField) rs'
-> Rec (Maybe :. ElField) rs2
-> Rec (Maybe :. ElField) (rs' ++ rs2)
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> Record rs2 -> Rec (Maybe :. ElField) rs2
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs2
r)
leftJoin :: forall fs rs rs2  rs2'.
  (fs    ⊆ rs
    , fs   ⊆ rs2
    , rs ⊆ (rs ++ rs2')
    , rs2' ⊆ rs2
    , rs2' ~ RDeleteAll fs rs2
    , RMap rs
    , RMap (rs ++ rs2')
    , RecApplicative rs2'
    , Grouping (Record fs)
    , RecVec rs
    , RecVec rs2'
    , RecVec (rs ++ rs2')
    ) =>
  Frame (Record rs)  
  -> Frame (Record rs2) 
  -> [Rec (Maybe :. ElField) (rs ++ rs2')] 
leftJoin :: Frame (Record rs)
-> Frame (Record rs2) -> [Rec (Maybe :. ElField) (rs ++ rs2')]
leftJoin Frame (Record rs)
a Frame (Record rs2)
b =
  [[Rec (Maybe :. ElField) (rs ++ rs2')]]
-> [Rec (Maybe :. ElField) (rs ++ rs2')]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
  (Group (Rec ElField fs)
-> (Record rs -> Record rs2 -> Rec (Maybe :. ElField) (rs ++ rs2'))
-> (Record rs -> Rec (Maybe :. ElField) (rs ++ rs2'))
-> (Record rs -> Rec ElField fs)
-> (Record rs2 -> Rec ElField fs)
-> [Record rs]
-> [Record rs2]
-> [[Rec (Maybe :. ElField) (rs ++ rs2')]]
forall (f :: * -> *) d a b c.
Discriminating f =>
f d
-> (a -> b -> c)
-> (a -> c)
-> (a -> d)
-> (b -> d)
-> [a]
-> [b]
-> [[c]]
leftOuter Group (Rec ElField fs)
forall a. Grouping a => Group a
grouping Record rs -> Record rs2 -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeFun Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty
    Record rs -> Rec ElField fs
proj1 Record rs2 -> Rec ElField fs
proj2 (Frame (Record rs) -> [Record rs]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs)
a) (Frame (Record rs2) -> [Record rs2]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Frame (Record rs2)
b))
  where
    proj1 :: Record rs -> Rec ElField fs
proj1 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
    proj2 :: Record rs2 -> Rec ElField fs
proj2 = forall (ss :: [(Symbol, *)]) (f :: (Symbol, *) -> *)
       (record :: ((Symbol, *) -> *) -> [(Symbol, *)] -> *) (is :: [Nat]).
(RecSubset record fs ss is, RecSubsetFCtx record f) =>
record f ss -> record f fs
forall k1 k2 (rs :: [k1]) (ss :: [k1]) (f :: k2 -> *)
       (record :: (k2 -> *) -> [k1] -> *) (is :: [Nat]).
(RecSubset record rs ss is, RecSubsetFCtx record f) =>
record f ss -> record f rs
rcast @fs
    mergeFun :: Record rs -> Record rs2 -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeFun Record rs
l Record rs2
r = Record (rs ++ rs2') -> Rec (Maybe :. ElField) (rs ++ rs2')
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec (Record (rs ++ rs2') -> Rec (Maybe :. ElField) (rs ++ rs2'))
-> Record (rs ++ rs2') -> Rec (Maybe :. ElField) (rs ++ rs2')
forall a b. (a -> b) -> a -> b
$ Record rs -> Record rs2 -> Record (rs ++ rs2')
forall (fs :: [(Symbol, *)]) (rs :: [(Symbol, *)])
       (rs2 :: [(Symbol, *)]) (rs2' :: [(Symbol, *)]).
(fs ⊆ rs2, rs2' ⊆ rs2, rs2' ~ RDeleteAll fs rs2,
 rs ⊆ (rs ++ rs2')) =>
Record rs -> Record rs2 -> Record (rs ++ rs2')
mergeRec @fs Record rs
l Record rs2
r
    mergeLeftEmpty :: Record rs -> Rec (Maybe :. ElField) (rs ++ rs2')
mergeLeftEmpty Record rs
l = Record rs -> Rec (Maybe :. ElField) rs
forall (fs :: [(Symbol, *)]).
RMap fs =>
Record fs -> Rec (Maybe :. ElField) fs
justsFromRec Record rs
l Rec (Maybe :. ElField) rs
-> Rec (Maybe :. ElField) rs2'
-> Rec (Maybe :. ElField) (rs ++ rs2')
forall k (f :: k -> *) (as :: [k]) (bs :: [k]).
Rec f as -> Rec f bs -> Rec f (as ++ bs)
<+> RecApplicative rs2' => Rec (Maybe :. ElField) rs2'
forall (fs :: [(Symbol, *)]).
RecApplicative fs =>
Rec (Maybe :. ElField) fs
mkNothingsRec @rs2'