-- | See <https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html here> for
-- the original term-level code by Stefan Kahrs. It is also copied at the end
-- of this file.  Some parts of the type-level code include the correspondign
-- term-level parts in their comments.
{-# LANGUAGE DataKinds,
             TypeOperators,
             ConstraintKinds,
             PolyKinds,
             TypeFamilies,
             GADTs,
             MultiParamTypeClasses,
             FunctionalDependencies,
             FlexibleInstances,
             FlexibleContexts,
             UndecidableInstances,
             UndecidableSuperClasses,
             TypeApplications,
             ScopedTypeVariables,
             AllowAmbiguousTypes,
             ExplicitForAll,
             RankNTypes, 
             DefaultSignatures,
             PartialTypeSignatures,
             LambdaCase,
             EmptyCase 
#-}
{-#  OPTIONS_GHC -Wno-partial-type-signatures  #-}

module Data.RBR.Internal where

import           Data.Proxy
import           Data.Kind
import           Data.Typeable
import           Data.Coerce
import           Data.Bifunctor (first)
import           Data.Monoid (Endo(..))
import           Data.List (intersperse)
import           Data.Foldable (asum)
import           GHC.TypeLits
import           GHC.Generics (D1,C1,S1(..),M1(..),K1(..),Rec0(..))
import qualified GHC.Generics as G

import           Data.SOP (I(..),K(..),unI,unK,NP(..),NS(..),All,SListI,type (-.->)(Fn,apFn),mapKIK)
import           Data.SOP.NP (collapse_NP,liftA_NP,liftA2_NP,cliftA_NP,cliftA2_NP,pure_NP)
import           Data.SOP.NS (collapse_NS,ap_NS,injections,Injection)

-- | The color of a node.
data Color = R
           | B
    deriving (Show,Eq)

-- | A Red-Black tree. It will be used as a kind, to index the 'Record' and 'Variant' types.
data Map k v = E
             | N Color (Map k v) k v (Map k v)
    deriving (Show,Eq)

-- | A map without entries. See also 'unit' and 'impossible'.
type Empty = E

{-# DEPRECATED EmptyMap "Use Empty instead." #-}
type EmptyMap = E

--
--
-- This code has been copied and adapted from the corresponding Data.SOP code (the All constraint).
--

-- Why is this KeysValuesAllF type family needed at all? Why is not KeysValuesAll sufficient by itself?
-- In fact, if I delete KeysValuesAllF and use eclusively KeysValuesAll, functions like demoteKeys seem to still work fine.
--
-- UndecidableSuperClasses and RankNTypes seem to be required by KeysValuesAllF.
type family
  KeysValuesAllF (c :: k -> v -> Constraint) (t :: Map k v) :: Constraint where
  KeysValuesAllF  _ E                        = ()
  KeysValuesAllF  c (N color left k v right) = (c k v, KeysValuesAll c left, KeysValuesAll c right)

{- | Require a constraint for every key-value pair in a tree. This is a generalization of 'Data.SOP.All' from "Data.SOP".
 
     'cpara_Map' constructs a 'Record' by means of a constraint for producing
     the nodes of the tree. The constraint is passed as a 'Data.Proxy.Proxy'.
     
-}
class KeysValuesAllF c t => KeysValuesAll (c :: k -> v -> Constraint) (t :: Map k v) where
  cpara_Map ::
       proxy c
    -> r E
    -> (forall left k v right color . (c k v, KeysValuesAll c left, KeysValuesAll c right)
                                   => r left -> r right -> r (N color left k v right))
    -> r t

instance KeysValuesAll c E where
  cpara_Map _p nil _step = nil

instance (c k v, KeysValuesAll c left, KeysValuesAll c right) => KeysValuesAll c (N color left k v right) where
  cpara_Map p nil cons =
    cons (cpara_Map p nil cons) (cpara_Map p nil cons)

{- |
    Create a 'Record', knowing that both keys and values satisfy a 2-place constraint. The constraint is passed as a 'Data.Proxy.Proxy'.

    The naming scheme follows that of 'Data.SOP.NP.cpure_NP'.
 -}
cpure_Record :: forall c t f. KeysValuesAll c t => (Proxy c) -> (forall k v. c k v => f v) -> Record f t
cpure_Record _ fpure = cpara_Map (Proxy @c) unit go
    where
    go :: forall left k' v' right color. (c k' v', KeysValuesAll c left, KeysValuesAll c right)
       => Record f left
       -> Record f right
       -> Record f (N color left k' v' right)
    go left right = Node left (fpure @k' @v') right

{- | Create a 'Record' containing the names of each field. 
    
     The names are represented by a constant functor 'K' carrying an annotation
     of type 'String'. This means that there aren't actually any values of the
     type that corresponds to each field, only the 'String' annotations.
-}
demoteKeys :: forall t. KeysValuesAll KnownKey t => Record (K String) t
demoteKeys = cpara_Map (Proxy @KnownKey) unit go
    where
    go :: forall left k v right color. (KnownKey k v, KeysValuesAll KnownKey left, KeysValuesAll KnownKey right)
       => Record (K String) left
       -> Record (K String) right
       -> Record (K String) (N color left k v right)
    go left right = Node left (K (symbolVal (Proxy @k))) right

{- |
  Two-place constraint saying that a 'Symbol' key can be demoted to 'String'. Nothing is required from the corresponding value.

  Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.
-}
class KnownSymbol k => KnownKey (k :: Symbol) (v :: z)
instance KnownSymbol k => KnownKey k v

{- | 
  Create a record containing the names of each field along with a term-level
  representation of each type.

  See also 'collapse_Record' for getting the entries as a list.
-}
demoteEntries :: forall t. KeysValuesAll KnownKeyTypeableValue t => Record (K (String,TypeRep)) t
demoteEntries = cpara_Map (Proxy @KnownKeyTypeableValue) unit go
    where
    go :: forall left k v right color. (KnownKeyTypeableValue k v, KeysValuesAll KnownKeyTypeableValue left, KeysValuesAll KnownKeyTypeableValue right)
       => Record (K (String,TypeRep)) left
       -> Record (K (String,TypeRep)) right
       -> Record (K (String,TypeRep)) (N color left k v right)
    go left right = Node left (K (symbolVal (Proxy @k),typeRep (Proxy @v))) right

{- |
  Two-place constraint saying that a 'Symbol' key can be demoted to 'String', and that the corresponding value 'Type' has a term-level representation. 

  Defined using the "class synonym" <https://www.reddit.com/r/haskell/comments/ab8ypl/monthly_hask_anything_january_2019/edk1ot3/ trick>.
-}
class (KnownSymbol k, Typeable v) => KnownKeyTypeableValue (k :: Symbol) (v :: Type)
instance (KnownSymbol k, Typeable v) => KnownKeyTypeableValue k v

-- class KeyValueTop (k :: Symbol) (v :: z)
-- instance KeyValueTop k v

--
--

{- | An extensible product-like type with named fields.
 
     The values in the 'Record' come wrapped in a type constructor @f@, which
     por pure records will be the identity functor 'I'.

     See also 'insert', 'delete' and 'project'.
-}
data Record (f :: Type -> Type) (t :: Map Symbol Type)  where
    Empty :: Record f E
    Node  :: Record f left -> f v -> Record f right -> Record f (N color left k v right)

instance (Productlike '[] t result, Show (NP f result)) => Show (Record f t) where
    show x = "fromNP (" ++ show (toNP x) ++ ")"


{- | Collapse a 'Record' composed of 'K' annotations.
    
     The naming scheme follows that of 'Data.SOP.NP.collapse_NP'.

-}
collapse_Record :: forall t result a. (Productlike '[] t result) => Record (K a) t -> [a]
collapse_Record = collapse_NP . toNP

{- | Show a 'Record' in a friendlier way than the default 'Show' instance. The
     function argument will usually be 'show', but it can be used to unwrap the
     value of each field before showing it.
-}
prettyShowRecord :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat)
                 => (forall x. Show x => f x -> String)
                 -> Record f t
                 -> String
prettyShowRecord showf r =
    let keysflat = toNP @t (demoteKeys @t)
        valuesflat = toNP @t r
        entries = cliftA2_NP (Proxy @Show) (\(K key) fv -> K (key ++ " = " ++ showf fv))
                                           keysflat
                                           valuesflat
     in "{" ++ mconcat (intersperse ", " (collapse_NP entries)) ++ "}"


{- | Like 'prettyShowRecord' but specialized to pure records.
-}
prettyShowRecordI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, All Show flat, SListI flat) => Record I t -> String
prettyShowRecordI r = prettyShowRecord (show . unI) r

{-| A Record without components is a boring, uninformative type whose single value can be conjured out of thin air.
-}
unit :: Record f Empty
unit = Empty

{- | An extensible sum-like type with named branches.
 
     The values in the 'Variant' come wrapped in a type constructor @f@, which
     por pure variants will be the identity functor 'I'.

     See also 'widen', 'winnow' and 'inject'.
-}
data Variant (f :: Type -> Type) (t :: Map Symbol Type)  where
    Here       :: f v -> Variant f (N color left k v right)
    LookRight  :: Variant f t -> Variant f (N color' left' k' v' t)
    LookLeft   :: Variant f t -> Variant f (N color' t k' v' right')

instance (Sumlike '[] t result, Show (NS f result)) => Show (Variant f t) where
    show x = "fromNS (" ++ show (toNS x) ++ ")"

{-| A Variant without branches doesn't have any values. From an impossible thing, anything can come out. 
-}
impossible :: Variant f Empty -> b
impossible v = case v of

{- | Show a 'Variant' in a friendlier way than the default 'Show' instance. The
     function argument will usually be 'show', but it can be used to unwrap the
     value of the branch before showing it.
-}
prettyShowVariant :: forall t flat f. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat)
                  => (forall x. Show x => f x -> String)
                  -> Variant f t
                  -> String
prettyShowVariant showf v =
    let keysflat = toNP @t (demoteKeys @t)
        eliminators = cliftA_NP (Proxy @Show) (\(K k) -> Fn (\fv -> (K (k ++ " (" ++ showf fv ++ ")")))) keysflat
        valuesflat = toNS @t v
     in collapse_NS (ap_NS eliminators valuesflat)

{- | Like 'prettyShowVariant' but specialized to pure variants.
-}
prettyShowVariantI :: forall t flat. (KeysValuesAll KnownKey t,Productlike '[] t flat, Sumlike '[] t flat, All Show flat, SListI flat)
                   => Variant I t -> String
prettyShowVariantI v = prettyShowVariant (show . unI) v

--
--
-- Insertion

{- | Insert a list of type level key / value pairs into a type-level map. 
-}
type family InsertAll (es :: [(Symbol,Type)]) (t :: Map Symbol Type) :: Map Symbol Type where
    InsertAll '[] t = t
    InsertAll ( '(name,fieldType) ': es ) t = Insert name fieldType (InsertAll es t)

{- | Build a type-level map out of a list of type level key / value pairs. 
-}
type FromList (es :: [(Symbol,Type)]) = InsertAll es Empty

{- | Alias for 'insert'. 
-}
addField :: forall k v t f . Insertable k v t => f v -> Record f t -> Record f (Insert k v t)
addField = insert @k @v @t @f

{- | Like 'insert' but specialized to pure 'Record's.
-}
insertI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t)
insertI = insert @k @v @t . I

{- | Like 'addField' but specialized to pure 'Record's.
-}
addFieldI :: forall k v t . Insertable k v t => v -> Record I t -> Record I (Insert k v t)
addFieldI = insertI @k @v @t

{- | Class that determines if the pair of a 'Symbol' key and a 'Type' can
     be inserted into a type-level map.
 
     The associated type family 'Insert' produces the resulting map.

     At the term level, this manifests in 'insert', which adds a new field to a
     record, and in 'widen', which lets you use a 'Variant' in a bigger context
     than the one in which is was defined. 'insert' tends to be more useful in
     practice.

     If the map already has the key but with a /different/ 'Type', the
     insertion fails to compile.
 -}
class Insertable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
    type Insert k v t :: Map Symbol Type
    insert :: f v -> Record f t -> Record f (Insert k v t)
    widen :: Variant f t -> Variant f (Insert k v t)

-- insert x s =
--  T B a z b
--  where
--  T _ a z b = ins s
instance (InsertableHelper1 k v t, Insert1 k v t ~ inserted, CanMakeBlack inserted) => Insertable k v t where
    type Insert k v t = MakeBlack (Insert1 k v t)
    insert fv r = makeBlackR (insert1 @k @v fv r)
    widen v = makeBlackV (widen1 @k @v v)

class CanMakeBlack (t :: Map Symbol Type) where
    type MakeBlack t :: Map Symbol Type
    makeBlackR :: Record f t -> Record f (MakeBlack t)
    makeBlackV :: Variant f t -> Variant f (MakeBlack t)

instance CanMakeBlack (N color left k v right) where
    type MakeBlack (N color left k v right) = N B left k v right
    makeBlackR (Node left fv right) = Node left fv right
    makeBlackV v = case v of
        LookLeft l -> LookLeft l
        Here v -> Here v
        LookRight r -> LookRight r

instance CanMakeBlack E where
    type MakeBlack E = E
    makeBlackR Empty = Empty
    makeBlackV = impossible

class InsertableHelper1 (k :: Symbol)
                        (v :: Type)
                        (t :: Map Symbol Type) where
    type Insert1 k v t :: Map Symbol Type
    insert1 :: f v -> Record f t -> Record f (Insert1 k v t)
    widen1 :: Variant f t -> Variant f (Insert1 k v t)

instance InsertableHelper1 k v E where
    type Insert1 k v E = N R E k v E
    insert1 fv Empty = Node Empty fv Empty
    widen1 = impossible

instance (CmpSymbol k k' ~ ordering,
          InsertableHelper2 ordering k v color left k' v' right
         )
         => InsertableHelper1 k v (N color left k' v' right) where
    -- FIXME possible duplicate work with CmpSymbol: both in constraint and in associated type family. 
    -- Is that bad? How to avoid it?
    type Insert1 k v (N color left k' v' right) = Insert2 (CmpSymbol k k') k v color left k' v' right
    insert1 = insert2 @ordering @k @v @color @left @k' @v' @right
    widen1  = widen2 @ordering @k @v @color @left @k' @v' @right

class InsertableHelper2 (ordering :: Ordering)
                        (k :: Symbol)
                        (v :: Type)
                        (color :: Color)
                        (left :: Map Symbol Type)
                        (k' :: Symbol)
                        (v' :: Type)
                        (right :: Map Symbol Type) where
    type Insert2 ordering k v color left k' v' right :: Map Symbol Type
    insert2 :: f v -> Record f (N color left k' v' right) -> Record f (Insert2 ordering k v color left k' v' right)
    widen2 :: Variant f (N color left k' v' right) -> Variant f (Insert2 ordering k v color left k' v' right)

--  ins s@(T B a y b)
--      | x<y = balance (ins a) y b
instance (InsertableHelper1 k v left, Insert1 k v left ~ inserted,
          Balanceable inserted k' v' right
         )
         => InsertableHelper2 LT k v B left k' v' right where
    type Insert2              LT k v B left k' v' right = Balance (Insert1 k v left) k' v' right
    insert2 fv (Node left fv' right) = balanceR @_ @k' @v' @right (Node (insert1 @k @v fv left) fv' right)
    widen2 v = balanceV @(Insert1 k v left) @k' @v' @right $ case v of
        Here x -> Here x
        LookLeft x -> LookLeft (widen1 @k @v x)
        LookRight x -> LookRight x

--  ins s@(T B a y b)
--      | x<y = balance (ins a) y b
instance (InsertableHelper1 k v left, Insert1 k v left ~ inserted,
          Balanceable inserted k' v' right
         )
         => InsertableHelper2 LT k v R left k' v' right where
    type Insert2              LT k v R left k' v' right = N R (Insert1 k v left) k' v' right
    insert2 fv (Node left fv' right) = Node (insert1 @k @v fv left) fv' right
    widen2 v = case v of
        Here x -> Here x
        LookLeft x -> LookLeft (widen1 @k @v x)
        LookRight x -> LookRight x


-- This instance implies that we can't change the type associated to an
-- existing key. If we did that, we wouldn't be able to widen Variants that
-- happen to match that key!
instance InsertableHelper2 EQ k v color left k v right where
    type Insert2           EQ k v color left k v right = N color left k v right
    insert2 fv (Node left _ right) = Node left fv right
    widen2 = id

--  ins s@(T B a y b)
--      | ...
--      | x>y = balance a y (ins b)
instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted,
          Balanceable left  k' v' inserted
         )
         => InsertableHelper2 GT k v B left k' v' right where
    type Insert2              GT k v B left k' v' right = Balance left  k' v' (Insert1 k v right)
    insert2 fv (Node left fv' right) = balanceR @left @k' @v' @_ (Node left  fv' (insert1 @k @v fv right))
    widen2 v = balanceV @left @k' @v' @(Insert1 k v right) $ case v of
        Here x -> Here x
        LookLeft x -> LookLeft x
        LookRight x -> LookRight (widen1 @k @v x)

--  ins s@(T R a y b)
--      | ...
--      | x>y = T R a y (ins b)
instance (InsertableHelper1 k v right, Insert1 k v right ~ inserted,
          Balanceable left  k' v' inserted
         )
         => InsertableHelper2 GT k v R left k' v' right where
    type Insert2              GT k v R left k' v' right = N R left k' v' (Insert1 k v right)
    insert2 fv (Node left fv' right) = Node left fv' (insert1 @k @v fv right)
    widen2 v = case v of
        Here x -> Here x
        LookLeft x -> LookLeft x
        LookRight x -> LookRight (widen1 @k @v x)

data BalanceAction = BalanceSpecial
                   | BalanceLL
                   | BalanceLR
                   | BalanceRL
                   | BalanceRR
                   | DoNotBalance
                   deriving Show

type family ShouldBalance (left :: Map k' v') (right :: Map k' v') :: BalanceAction where
    ShouldBalance (N R _ _ _ _) (N R _ _ _ _) = BalanceSpecial
    ShouldBalance (N R (N R _ _ _ _) _ _ _) _ = BalanceLL
    ShouldBalance (N R _ _ _ (N R _ _ _ _)) _ = BalanceLR
    ShouldBalance _ (N R (N R _ _ _ _) _ _ _) = BalanceRL
    ShouldBalance _ (N R _ _ _ (N R _ _ _ _)) = BalanceRR
    ShouldBalance _ _                         = DoNotBalance

class Balanceable (left :: Map Symbol Type) (k :: Symbol) (v :: Type) (right :: Map Symbol Type) where
    type Balance left k v right :: Map Symbol Type
    balanceR :: Record f (N color left k v right) -> Record f (Balance left k v right)
    balanceV :: Variant f (N color left k v right) -> Variant f (Balance left k v right)

instance (ShouldBalance left right ~ action,
          BalanceableHelper action left k v right
         )
         => Balanceable left k v right where
    -- FIXME possible duplicate work with ShouldBalance: both in constraint and in associated type family. 
    -- Is that bad? How to avoid it?
    type Balance left k v right = Balance' (ShouldBalance left right) left k v right
    balanceR = balanceR' @action @left @k @v @right
    balanceV = balanceV' @action @left @k @v @right

class BalanceableHelper (action :: BalanceAction)
                        (left :: Map Symbol Type)
                        (k :: Symbol)
                        (v :: Type)
                        (right :: Map Symbol Type) where
    type Balance' action left k v right :: Map Symbol Type
    balanceR' :: Record f (N color left k v right) -> Record f (Balance' action left k v right)
    balanceV' :: Variant f (N color left k v right) -> Variant f (Balance' action left k v right)

-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) where
    type Balance'          BalanceSpecial (N R left1 k1 v1 right1) kx vx (N R left2 k2 v2 right2) =
                                      N R (N B left1 k1 v1 right1) kx vx (N B left2 k2 v2 right2)
    balanceR' (Node (Node left1 v1 right1) vx (Node left2 v2 right2)) =
              (Node (Node left1 v1 right1) vx (Node left2 v2 right2))
    balanceV' v = case v of
        LookLeft (LookLeft x)   -> LookLeft (LookLeft x)
        LookLeft (Here x)       -> LookLeft (Here x)
        LookLeft (LookRight x)  -> LookLeft (LookRight x)
        Here x -> Here x
        LookRight (LookLeft x)  -> LookRight (LookLeft x)
        LookRight (Here x)      -> LookRight (Here x)
        LookRight (LookRight x) -> LookRight (LookRight x)

-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d where
    type Balance'          BalanceLL (N R (N R a k1 v1 b) k2 v2 c) k3 v3 d =
                                 N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
    balanceR' (Node (Node (Node a fv1 b) fv2 c) fv3 d) =
               Node (Node a fv1 b) fv2 (Node c fv3 d)
    balanceV' v = case v of
        LookLeft (LookLeft x)  -> LookLeft (case x of LookLeft y  -> LookLeft y
                                                      Here y      -> Here y
                                                      LookRight y -> LookRight y)
        LookLeft (Here x)      -> Here x
        LookLeft (LookRight x) -> LookRight (LookLeft x)
        Here x                 -> LookRight (Here x)
        LookRight x            -> LookRight (LookRight x)

-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d where
    type Balance'          BalanceLR (N R a k1 v1 (N R b k2 v2 c)) k3 v3 d =
                                 N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
    balanceR' (Node (Node a fv1 (Node b fv2 c)) fv3 d) =
               Node (Node a fv1 b) fv2 (Node c fv3 d)
    balanceV' v = case v of
        LookLeft (LookLeft x)   -> LookLeft (LookLeft x)
        LookLeft (Here x)       -> LookLeft (Here x)
        LookLeft (LookRight x)  -> case x of LookLeft y  -> LookLeft (LookRight y)
                                             Here y      -> Here y
                                             LookRight y -> LookRight (LookLeft y)
        Here x                  -> LookRight (Here x)
        LookRight x             -> LookRight (LookRight x)

-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) where
    type Balance'          BalanceRL a k1 v1 (N R (N R b k2 v2 c) k3 v3 d) =
                                 N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
    balanceR' (Node a fv1 (Node (Node b fv2 c) fv3 d)) =
               Node (Node a fv1 b) fv2 (Node c fv3 d)
    balanceV' v = case v of
        LookLeft x              -> LookLeft (LookLeft x)
        Here x                  -> LookLeft (Here x)
        LookRight (LookLeft x)  -> case x of LookLeft y  -> LookLeft (LookRight y)
                                             Here y      -> Here y
                                             LookRight y -> LookRight (LookLeft y)
        LookRight (Here x)      -> LookRight (Here x)
        LookRight (LookRight x) -> LookRight (LookRight x)


-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
instance BalanceableHelper BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) where
    type Balance'          BalanceRR a k1 v1 (N R b k2 v2 (N R c k3 v3 d)) =
                                 N R (N B a k1 v1 b) k2 v2 (N B c k3 v3 d)
    balanceR' (Node a fv1 (Node b fv2 (Node c fv3 d))) =
               Node (Node a fv1 b) fv2 (Node c fv3 d)
    balanceV' v = case v of
        LookLeft x              -> LookLeft (LookLeft x)
        Here x                  -> LookLeft (Here x)
        LookRight (LookLeft x)  -> LookLeft (LookRight x)
        LookRight (Here x)      -> Here x
        LookRight (LookRight x) -> LookRight (case x of LookLeft y  -> LookLeft y
                                                        Here y      -> Here y
                                                        LookRight y -> LookRight y)

-- balance a x b = T B a x b
instance BalanceableHelper DoNotBalance a k v b where
    type Balance'          DoNotBalance a k v b = N B a k v b
    balanceR' (Node left v right) = (Node left v right)
    balanceV' v = case v of
        LookLeft l -> LookLeft l
        Here v -> Here v
        LookRight r -> LookRight r

--
--
-- Accessing fields

--
-- These two type families exist to avoid duplicating expensive type-level
-- computations, in particular the Value' computations.
--
-- Record accessors are compiled WAY slower without them!
--
{- | Auxiliary type family to avoid repetition and help improve compilation times.
 -}
type family Field (f :: Type -> Type) (t :: Map Symbol Type) (v :: Type) where
    Field f t v = Record f t -> (f v -> Record f t, f v)

{- | Auxiliary type family to avoid repetition and help improve compilation times.
 -}
type family Branch (f :: Type -> Type) (t :: Map Symbol Type) (v :: Type) where
    Branch f t v = (Variant f t -> Maybe (f v), f v -> Variant f t)

--
{- | 
     Class that determines if a given 'Symbol' key is present in a type-level
     map.

     The 'Value' type family gives the 'Type' corresponding to the key.

     'field' takes a field name (given through @TypeApplications@) and a
     'Record', and returns a pair of a setter for the field and the original
     value of the field.
     
     'branch' takes a branch name (given through @TypeApplications@) and
     returns a pair of a match function and a constructor.
-}
class Key (k :: Symbol) (t :: Map Symbol Type) where
    type Value k t :: Type
    field  :: Field  f t (Value k t)
    branch :: Branch f t (Value k t)

-- member :: Ord a => a -> RB a -> Bool
class KeyHelper (ordering :: Ordering) (k :: Symbol) (left :: Map Symbol Type) (v :: Type) (right :: Map Symbol Type) where
    type Value' ordering k left v right :: Type
    field'  :: Field  f (N colorx left kx v right) (Value' ordering k left v right)
    branch' :: Branch f (N colorx left kx v right) (Value' ordering k left v right)

instance (CmpSymbol k' k ~ ordering, KeyHelper ordering k left v' right) => Key k (N color left k' v' right) where
    type Value k (N color left k' v' right) = Value' (CmpSymbol k' k) k left v' right
    field = field' @ordering @k @left @v' @right
    branch = branch' @ordering @k @left @v' @right

--  | x<y = member x a
instance (CmpSymbol k2 k ~ ordering, KeyHelper ordering k left2 v2 right2)
      => KeyHelper LT k left v (N color2 left2 k2 v2 right2) where
    type Value'    LT k left v (N color2 left2 k2 v2 right2) = Value' (CmpSymbol k2 k) k left2 v2 right2
    field' (Node left fv right) =
        let (setter,x) = field' @ordering @k @left2 @v2 @right2 right
         in (\z -> Node left fv (setter z),x)
    branch' =
        let (match,inj) = branch' @ordering @k @left2 @v2 @right2
         in (\case LookRight x -> match x
                   _ -> Nothing,
             \fv -> LookRight (inj fv))

--  | x>y = member x b
instance (CmpSymbol k2 k ~ ordering, KeyHelper ordering k left2 v2 right2)
      => KeyHelper GT k (N color2 left2 k2 v2 right2) v' right where
    type    Value' GT k (N color2 left2 k2 v2 right2) v' right = Value' (CmpSymbol k2 k) k left2 v2 right2
    field' (Node left fv right) =
        let (setter,x) = field' @ordering @k @left2 @v2 @right2 left
         in (\z -> Node (setter z) fv right,x)
    branch' =
        let (match,inj) = branch' @ordering @k @left2 @v2 @right2
         in (\case LookLeft x -> match x
                   _ -> Nothing,
             \fv -> LookLeft (inj fv))

--  | otherwise = True
instance KeyHelper EQ k left v right where
    type Value'    EQ k left v right = v
    field' (Node left fv right) = (\x -> Node left x right, fv)
    branch' = (\case Here x -> Just x
                     _ -> Nothing,
               Here)

{- | Get the value of a field for a 'Record'. 
-}
project :: forall k t f . Key k t => Record f t -> f (Value k t)
project = snd . field @k @t

{- | Alias for 'project'.
-}
getField :: forall k t f . Key k t => Record f t -> f (Value k t)
getField = project @k @t @f

{- | Set the value of a field for a 'Record'. 
-}
setField :: forall k t f . Key k t => f (Value k t) -> Record f t -> Record f t
setField fv r = fst (field @k @t @f r) fv

{- | Modify the value of a field for a 'Record'. 
-}
modifyField :: forall k t f . Key k t => (f (Value k t) -> f (Value k t)) -> Record f t -> Record f t
modifyField f r = uncurry ($) (fmap f (field @k @t @f r))

{- | Put a value into the branch of a 'Variant'.
-}
inject :: forall k t f. Key k t => f (Value k t) -> Variant f t
inject = snd (branch @k @t)

{- | Check if a 'Variant' value is the given branch.
-}
match :: forall k t f. Key k t => Variant f t -> Maybe (f (Value k t))
match = fst (branch @k @t)

{- | Like 'project' but specialized to pure 'Record's.
-}
projectI :: forall k t . Key k t => Record I t -> Value k t
projectI = unI . snd . field @k @t

{- | Like 'getField' but specialized to pure 'Record's.
-}
getFieldI :: forall k t . Key k t => Record I t -> Value k t
getFieldI = projectI @k @t

{- | Like 'setField' but specialized to pure 'Record's.
-}
setFieldI :: forall k t . Key k t => Value k t -> Record I t -> Record I t
setFieldI v r = fst (field @k @t r) (I v)

{- | Like 'modifyField' but specialized to pure 'Record's.
-}
modifyFieldI :: forall k t . Key k t => (Value k t -> Value k t) -> Record I t -> Record I t
modifyFieldI f = modifyField @k @t (I . f . unI)

{- | Like 'inject' but specialized to pure 'Variant's.
-}
injectI :: forall k t. Key k t => Value k t -> Variant I t
injectI = snd (branch @k @t) . I

{- | Like 'match' but specialized to pure 'Variants's.
-}
matchI :: forall k t . Key k t => Variant I t ->  Maybe (Value k t)
matchI v = unI <$> fst (branch @k @t) v

{- | Process a 'Variant' using a eliminator 'Record' that carries
     handlers for each possible branch of the 'Variant'.
-}
eliminate :: (Productlike '[] t result, Sumlike '[] t result, SListI result) => Record (Case f r) t -> Variant f t -> r
eliminate cases variant =
    let adapt (Case e) = Fn (\fv -> K (e fv))
     in collapse_NS (ap_NS (liftA_NP adapt (toNP cases)) (toNS variant))

{- | Represents a handler for a branch of a 'Variant'.  
-}
newtype Case f a b = Case (f b -> a)

{- | A form of 'addField' for creating eliminators for 'Variant's.
-}
addCase :: forall k v t f a. Insertable k v t => (f v -> a) -> Record (Case f a) t -> Record (Case f a) (Insert k v t)
addCase f = addField @k @v @t (Case f)

{- | A pure version of 'addCase'.
-}
addCaseI :: forall k v t a. Insertable k v t => (v -> a) -> Record (Case I a) t -> Record (Case I a) (Insert k v t)
addCaseI f = addField @k @v @t (Case (f . unI))

--
--
-- Subsetting

newtype SetField f a b = SetField { getSetField :: f b -> a -> a }

-- this odd trick again...
class (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol Type) (k :: Symbol) (v :: Type)
instance (Key k t, Value k t ~ v) => PresentIn (t :: Map Symbol Type) (k :: Symbol) (v :: Type)

{- | Constraint for maps that represent subsets of fields of 'Record'-like types.
-}
type ProductlikeSubset (subset :: Map Symbol Type) (whole :: Map Symbol Type) (flat :: [Type]) =
                       (KeysValuesAll (PresentIn whole) subset,
                        Productlike '[] subset flat,
                        SListI flat)

{- | Like 'field', but targets multiple fields at the same time 
-}
fieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat)
            => Record f whole -> (Record f subset -> Record f whole, Record f subset)
fieldSubset r =
    (,)
    (let goset :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left,
                                                                     KeysValuesAll (PresentIn whole) right)
               => Record (SetField f (Record f whole)) left
               -> Record (SetField f (Record f whole)) right
               -> Record (SetField f (Record f whole)) (N color left k v right)
         goset left right = Node left (SetField (\v w -> fst (field @k @whole w) v)) right
         setters = toNP @subset @_ @(SetField f (Record f whole)) (cpara_Map (Proxy @(PresentIn whole)) unit goset)
         appz (SetField func) fv = K (Endo (func fv))
      in \toset -> appEndo (mconcat (collapse_NP (liftA2_NP appz setters (toNP toset)))) r)
    (let goget :: forall left k v right color. (PresentIn whole k v, KeysValuesAll (PresentIn whole) left,
                                                                     KeysValuesAll (PresentIn whole) right)
               => Record f left
               -> Record f right
               -> Record f (N color left k v right)
         goget left right = Node left (project @k @whole r) right
      in cpara_Map (Proxy @(PresentIn whole)) unit goget)

{- | Like 'project', but extracts multiple fields at the same time.
 
     Can also be used to convert between 'Record's with structurally dissimilar
     type-level maps that nevertheless hold the same entries. 
-}
projectSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat)
              => Record f whole
              -> Record f subset
projectSubset =  snd . fieldSubset

{- | Alias for 'projectSubset'.
-}
getFieldSubset :: forall subset whole flat f. (ProductlikeSubset subset whole flat)
               => Record f whole
               -> Record f subset
getFieldSubset = projectSubset

{- | Like 'setField', but sets multiple fields at the same time.
 
-}
setFieldSubset :: forall subset whole flat f.  (ProductlikeSubset subset whole flat)
               => Record f subset
               -> Record f whole
               -> Record f whole
setFieldSubset subset whole = fst (fieldSubset whole) subset

{- | Like 'modifyField', but modifies multiple fields at the same time.
 
-}
modifyFieldSubset :: forall subset whole flat f.  (ProductlikeSubset subset whole flat)
                  => (Record f subset -> Record f subset)
                  -> Record f whole
                  -> Record f whole
modifyFieldSubset f r = uncurry ($) (fmap f (fieldSubset @subset @whole r))


{- | Constraint for maps that represent subsets of branches of 'Variant'-like types.
-}
type SumlikeSubset (subset :: Map Symbol Type) (whole :: Map Symbol Type) (subflat :: [Type]) (wholeflat :: [Type]) =
                   (KeysValuesAll (PresentIn whole) subset,
                    Productlike '[] whole  wholeflat,
                    Sumlike '[] whole  wholeflat,
                    SListI wholeflat,
                    Productlike '[] subset subflat,
                    Sumlike '[] subset subflat,
                    SListI subflat)

{- | Like 'branch', but targets multiple branches at the same time.
-}
branchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat)
             => (Variant f whole -> Maybe (Variant f subset), Variant f subset -> Variant f whole)
branchSubset =
    let inj2case :: forall t flat f v. Sumlike '[] t flat => (_ -> _) -> Injection _ flat v -> Case _ _ v
        inj2case = \adapt -> \fn -> Case (\fv -> adapt (fromNS @t (unK (apFn fn fv))))
        -- The intuition is that getting the setter and the getter together might be faster at compile-time.
        -- The intuition might be wrong.
        subs :: forall f. Record f whole -> (Record f subset -> Record f whole, Record f subset)
        subs = fieldSubset @subset @whole
     in
     (,)
     (let injs :: Record (Case f (Maybe (Variant f subset))) subset
          injs = fromNP @subset (liftA_NP (inj2case Just) (injections @subflat))
          wholeinjs :: Record (Case f (Maybe (Variant f subset))) whole
          wholeinjs = fromNP @whole (pure_NP (Case (\_ -> Nothing)))
          mixedinjs = fst (subs wholeinjs) injs
       in eliminate mixedinjs)
     (let wholeinjs :: Record (Case f (Variant f whole)) whole
          wholeinjs = fromNP @whole (liftA_NP (inj2case id) (injections @wholeflat))
          injs = snd (subs wholeinjs)
       in eliminate injs)

{- | Like 'inject', but injects one of several possible branches.
 
     Can also be used to convert between 'Variant's with structurally
     dissimilar type-level maps that nevertheless hold the same entries. 
-}
injectSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat)
             => Variant f subset -> Variant f whole
injectSubset = snd (branchSubset @subset @whole @subflat @wholeflat)

{- | Like 'match', but matches more than one branch.
-}
matchSubset :: forall subset whole subflat wholeflat f. (SumlikeSubset subset whole subflat wholeflat)
            => Variant f whole -> Maybe (Variant f subset)
matchSubset = fst (branchSubset @subset @whole @subflat @wholeflat)

{- | 
     Like 'eliminate', but allows the eliminator 'Record' to have more fields
     than there are branches in the 'Variant'.
-}
eliminateSubset :: forall subset whole subflat wholeflat f r. (SumlikeSubset subset whole subflat wholeflat)
                => Record (Case f r) whole -> Variant f subset -> r
eliminateSubset cases =
    let reducedCases = getFieldSubset @subset @whole cases
     in eliminate reducedCases

--
--
-- Interaction with Data.SOP

{- | Class from converting 'Record's to and from the n-ary product type 'NP' from "Data.SOP".
    
     'prefixNP' flattens a 'Record' and adds it to the initial part of the product.

     'breakNP' reconstructs a 'Record' from the initial part of the product and returns the unconsumed part.

     The functions 'toNP' and 'fromNP' are usually easier to use. 
-}
class Productlike (start :: [Type])
                  (t :: Map Symbol Type)
                  (result :: [Type]) | start t -> result, result t -> start where
    prefixNP:: Record f t -> NP f start -> NP f result
    breakNP :: NP f result -> (Record f t, NP f start)

instance Productlike start E start where
    prefixNP _ start = start
    breakNP start = (Empty, start)

instance (Productlike start right middle,
          Productlike (v ': middle) left result)
          => Productlike start (N color left k v right) result where
    prefixNP (Node left fv right) start =
        prefixNP @_ @left @result left (fv :* prefixNP @start @right @middle right start)
    breakNP result =
        let (left, fv :* middle) = breakNP @_ @left @result result
            (right, start) = breakNP @start @right middle
         in (Node left fv right, start)

{- | Convert a 'Record' into a n-ary product. 
-}
toNP :: forall t result f. Productlike '[] t result => Record f t -> NP f result
toNP r = prefixNP r Nil

{- | Convert a n-ary product into a compatible 'Record'. 
-}
fromNP :: forall t result f. Productlike '[] t result => NP f result -> Record f t
fromNP np = let (r,Nil) = breakNP np in r

{- | Class from converting 'Variant's to and from the n-ary sum type 'NS' from "Data.SOP".
    
     'prefixNS' flattens a 'Variant' and adds it to the initial part of the sum.

     'breakNS' reconstructs a 'Variant' from the initial part of the sum and returns the unconsumed part.

     The functions 'toNS' and 'fromNS' are usually easier to use. 
-}
class Sumlike (start :: [Type])
              (t :: Map Symbol Type)
              (result :: [Type]) | start t -> result, result t -> start where
    prefixNS :: Either (NS f start) (Variant f t) -> NS f result
    breakNS :: NS f result -> Either (NS f start) (Variant f t)

instance Sumlike start
                  (N color E k v E)
                  (v ': start) where
    prefixNS = \case
        Left  l -> S l
        Right x -> case x of Here fv -> Z @_ @v @start fv
    breakNS = \case
        Z x -> Right (Here x)
        S x -> Left x

instance (Sumlike start (N colorR leftR kR vR rightR) middle,
          Sumlike (v ': middle) (N colorL leftL kL vL rightL) result)
         => Sumlike start
                    (N color (N colorL leftL kL vL rightL) k v (N colorR leftR kR vR rightR))
                    result where
    prefixNS = \case
        Left x ->
            prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S (prefixNS @_ @(N colorR leftR kR vR rightR) (Left x))))
        Right x ->
            case x of LookLeft x  -> prefixNS @(v ': middle) @(N colorL leftL kL vL rightL) @result (Right x)
                      Here x      -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (Z x))
                      LookRight x -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S (prefixNS (Right x))))
    breakNS ns = case breakNS @(v ': middle) @(N colorL leftL kL vL rightL) ns of
        Left x -> case x of
            Z x -> Right (Here x)
            S x -> case breakNS @start @(N colorR leftR kR vR rightR) x of
                Left ns  -> Left ns
                Right v  -> Right (LookRight v)
        Right v -> Right (LookLeft v)

instance Sumlike (v ': start) (N colorL leftL kL vL rightL) result
         => Sumlike start (N color (N colorL leftL kL vL rightL) k v E) result where
    prefixNS = \case
        Left x  ->
            prefixNS @_ @(N colorL leftL kL vL rightL) (Left (S x))
        Right x ->
            case x of LookLeft x  -> prefixNS @(v ': start) @(N colorL leftL kL vL rightL) @result (Right x)
                      Here x      -> prefixNS @_ @(N colorL leftL kL vL rightL) (Left (Z x))
    breakNS ns = case breakNS @(v ': start) @(N colorL leftL kL vL rightL) ns of
        Left x -> case x of
            Z x -> Right (Here x)
            S x -> Left x
        Right v -> Right (LookLeft v)

instance Sumlike start (N colorR leftR kR vR rightR) middle
         => Sumlike start (N color E k v (N colorR leftR kR vR rightR)) (v ': middle) where
    prefixNS = \case
        Left x  -> S (prefixNS @_ @(N colorR leftR kR vR rightR) (Left x))
        Right x ->
            case x of Here x      -> Z x
                      LookRight x -> S (prefixNS @_ @(N colorR leftR kR vR rightR) (Right x))
    breakNS = \case
        Z x -> Right (Here x)
        S x -> case breakNS @_ @(N colorR leftR kR vR rightR) x of
            Left  ns     -> Left ns
            Right v      -> Right (LookRight v)

{- | Convert a 'Variant' into a n-ary sum. 
-}
toNS :: forall t result f. Sumlike '[] t result => Variant f t -> NS f result
toNS = prefixNS . Right

{- | Convert a n-ary sum into a compatible 'Variant'. 
-}
fromNS :: forall t result f. Sumlike '[] t result => NS f result -> Variant f t
fromNS ns = case breakNS ns of
    Left _ -> error "this never happens"
    Right x -> x

--
--
-- Interfacing with normal records

class ToRecord (r :: Type) where
    type RecordCode r :: Map Symbol Type
    -- https://stackoverflow.com/questions/22087549/defaultsignatures-and-associated-type-families/22088808
    type RecordCode r = RecordCode' E (G.Rep r)
    toRecord :: r -> Record I (RecordCode r)
    default toRecord :: (G.Generic r,ToRecordHelper E (G.Rep r),RecordCode r ~ RecordCode' E (G.Rep r)) => r -> Record I (RecordCode r)
    toRecord r = toRecord' unit (G.from r)

class ToRecordHelper (start :: Map Symbol Type) (g :: Type -> Type) where
    type RecordCode' start g :: Map Symbol Type
    toRecord' :: Record I start -> g x -> Record I (RecordCode' start g)

instance ToRecordHelper E fields => ToRecordHelper E (D1 meta (C1 metacons fields)) where
    type RecordCode' E (D1 meta (C1 metacons fields)) = RecordCode' E fields
    toRecord' r (M1 (M1 g)) = toRecord' @E @fields r g

instance (Insertable k v start) =>
         ToRecordHelper start
                        (S1 ('G.MetaSel ('Just k)
                                        unpackedness
                                        strictness
                                        laziness)
                            (Rec0 v))
  where
    type RecordCode'    start
                        (S1 ('G.MetaSel ('Just k)
                                        unpackedness
                                        strictness
                                        laziness)
                            (Rec0 v))                           = Insert k v start
    toRecord' start (M1 (K1 v)) = insertI @k v start

instance ( ToRecordHelper start  t2,
           RecordCode'    start  t2 ~ middle,
           ToRecordHelper middle t1
         ) =>
         ToRecordHelper start (t1 G.:*: t2)
  where
    type RecordCode'    start (t1 G.:*: t2) = RecordCode' (RecordCode' start t2) t1
    toRecord'           start (t1 G.:*: t2) = toRecord' @middle (toRecord' @start start t2) t1

--
--
class ToRecord r => FromRecord (r :: Type) where
    fromRecord :: Record I (RecordCode r) -> r
    default fromRecord :: (G.Generic r, FromRecordHelper (RecordCode r) (G.Rep r)) => Record I (RecordCode r) -> r
    fromRecord r = G.to (fromRecord' @(RecordCode r) @(G.Rep r) r)

class FromRecordHelper (t :: Map Symbol Type) (g :: Type -> Type) where
    fromRecord' :: Record I t -> g x

instance FromRecordHelper t fields => FromRecordHelper t (D1 meta (C1 metacons fields)) where
    fromRecord' r = M1 (M1 (fromRecord' @t @fields r))

instance (Key k t, Value k t ~ v) =>
         FromRecordHelper t
                          (S1 ('G.MetaSel ('Just k)
                                          unpackedness
                                          strictness
                                          laziness)
                              (Rec0 v))
 where
   fromRecord' r = let v = projectI @k r in M1 (K1 v)

instance ( FromRecordHelper t t1,
           FromRecordHelper t t2
         ) =>
         FromRecordHelper t (t1 G.:*: t2)
  where
   fromRecord' r =
        let v1 = fromRecord' @_ @t1 r
            v2 = fromRecord' @_ @t2 r
         in v1 G.:*: v2

--
--
--
type family VariantCode (s :: Type) :: Map Symbol Type where
    VariantCode s = VariantCode' E (G.Rep s)

type family VariantCode' (acc :: Map Symbol Type) (g :: Type -> Type) :: Map Symbol Type where
    VariantCode' acc (D1 meta fields) = VariantCode' acc fields
    VariantCode' acc (t1 G.:+: t2) = VariantCode' (VariantCode' acc t2) t1
    VariantCode' acc (C1 (G.MetaCons k _ _) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v))) = Insert k v acc

class FromVariant (s :: Type) where
    fromVariant :: Variant I (VariantCode s) -> s
    default fromVariant :: (G.Generic s, FromVariantHelper (VariantCode s) (G.Rep s)) => Variant I (VariantCode s) -> s
    fromVariant v = case fromVariant' @(VariantCode s) v of
        Just x -> G.to x
        Nothing -> error "fromVariant match fail. Should not happen."

class FromVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where
    fromVariant' :: Variant I t -> Maybe (g x)

instance FromVariantHelper t fields => FromVariantHelper t (D1 meta fields) where
    fromVariant' v = M1 <$> fromVariant' @t v

instance (Key k t, Value k t ~ v)
         => FromVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v)))
  where
    fromVariant' v = case matchI @k @t v of
        Just x -> Just (M1 (M1 (K1 x)) )
        Nothing -> Nothing

instance ( FromVariantHelper t t1,
           FromVariantHelper t t2
         ) =>
         FromVariantHelper t (t1 G.:+: t2)
  where
    fromVariant' v = case fromVariant' @t @t1 v of
        Just x1 -> Just (G.L1 x1)
        Nothing -> case fromVariant' @t @t2 v of
            Just x2 -> Just (G.R1 x2)
            Nothing -> Nothing

--
--
class ToVariant (s :: Type) where
    toVariant :: s -> Variant I (VariantCode s)
    default toVariant :: (G.Generic s, ToVariantHelper (VariantCode s) (G.Rep s)) => s -> Variant I (VariantCode s)
    toVariant s = toVariant' @(VariantCode s) @(G.Rep s) (G.from s)

class ToVariantHelper (t :: Map Symbol Type) (g :: Type -> Type) where
    toVariant' :: g x -> Variant I t

instance ToVariantHelper t fields => ToVariantHelper t (D1 meta fields) where
    toVariant' (M1 fields) = toVariant' @t fields

instance (Key k t, Value k t ~ v) =>
    ToVariantHelper t (C1 (G.MetaCons k x y) (S1 ('G.MetaSel Nothing unpackedness strictness laziness) (Rec0 v)))
  where
    toVariant' (M1 (M1 (K1 v))) = injectI @k v

instance ( ToVariantHelper t t1,
           ToVariantHelper t t2
         ) =>
         ToVariantHelper t (t1 G.:+: t2)
  where
    toVariant' = \case
        G.L1 l -> toVariant' @t l
        G.R1 r -> toVariant' @t r

--
--
-- deletion
--
--
--

type family DiscriminateBalL (l :: Map k v) (r :: Map k v) :: Bool where
    DiscriminateBalL (N R _ _ _ _) _ = False
    DiscriminateBalL _             _ = True

class BalanceableL (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
    type BalL l k v r :: Map Symbol Type
    balLR :: Record f (N color l k v r) -> Record f (BalL l k v r)
    balLV :: Variant f (N color l k v r) -> Variant f (BalL l k v r)

class BalanceableHelperL (b :: Bool) (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
    type BalL' b l k v r :: Map Symbol Type
    balLR' :: Record f (N color l k v r) -> Record f (BalL' b l k v r)
    balLV' :: Variant f (N color l k v r) -> Variant f (BalL' b l k v r)

instance (DiscriminateBalL l r ~ b, BalanceableHelperL b l k v r) => BalanceableL l k v r where
    type BalL l k v r = BalL' (DiscriminateBalL l r) l k v r
    balLR = balLR' @b @l @k @v @r
    balLV = balLV' @b @l @k @v @r

-- balleft :: RB a -> a -> RB a -> RB a
-- balleft (T R a x b) y c = T R (T B a x b) y c
instance BalanceableHelperL False (N R left1 k1 v1 right1) k2 v2 right2 where
    type BalL'              False (N R left1 k1 v1 right1) k2 v2 right2 =
                             (N R (N B left1 k1 v1 right1) k2 v2 right2)
    balLR' (Node (Node left' v' right') v right) = Node (Node left' v' right') v right
    balLV' v = case v of LookLeft x  -> LookLeft (case x of LookLeft y  -> LookLeft y
                                                            Here y      -> Here y
                                                            LookRight y -> LookRight y)
                         Here x      -> Here x
                         LookRight x -> LookRight x

-- balleft bl x (T B a y b) = balance bl x (T R a y b)
-- the @(N B in the call to balance tree is misleading, as it is ingored...
instance (N R t2 z zv t3 ~ g, BalanceableHelper (ShouldBalance t1 g) t1 y yv g) =>
    BalanceableHelperL True t1 y yv (N B t2 z zv t3) where
    type BalL'         True t1 y yv (N B t2 z zv t3)
                 =  Balance t1 y yv (N R t2 z zv t3)
    balLR' (Node left1 v1 (Node left2 v2 right2)) =
        balanceR @t1 @y @yv @(N R t2 z zv t3) (Node left1 v1 (Node left2 v2 right2))
    balLV' v = balanceV @t1 @y @yv @(N R t2 z zv t3) (case v of
        LookLeft l -> LookLeft l
        Here x -> Here x
        LookRight r -> LookRight (case r of
                            LookLeft l' -> LookLeft l'
                            Here x' -> Here x'
                            LookRight r' -> LookRight r'))

-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))
instance (N R l k kv r ~ g, BalanceableHelper    (ShouldBalance t3 g) t3 z zv g) =>
    BalanceableHelperL True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) where
    type BalL'         True t1 y yv (N R (N B t2 u uv t3) z zv (N B l k kv r)) =
                             N R (N B t1 y yv t2) u uv (Balance t3 z zv (N R l k kv r))
    balLR' (Node left1 v1 (Node (Node left2 v2 right2) vx (Node left3 v3 right3))) =
            Node (Node left1 v1 left2) v2 (balanceR @t3 @z @zv @(N R l k kv r) (Node right2 vx (Node left3 v3 right3)))
    balLV' v = case v of LookLeft left1                          -> LookLeft (LookLeft left1)
                         Here v1                                 -> LookLeft (Here v1)
                         LookRight (LookLeft (LookLeft left2))   -> LookLeft (LookRight left2)
                         LookRight (LookLeft (Here v2))          -> Here v2
                         LookRight (LookLeft (LookRight right2)) -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (LookLeft right2))
                         LookRight (Here vx)                     -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (Here vx))
                         LookRight (LookRight rr)                -> LookRight (balanceV @t3 @z @zv @(N R l k kv r) (LookRight (case rr of
                                                                        LookLeft left3 -> LookLeft left3
                                                                        Here v3 -> Here v3
                                                                        LookRight right3 -> LookRight right3)))


-- balright :: RB a -> a -> RB a -> RB a
-- balright a x (T R b y c) = T R a x (T B b y c)
-- balright (T B a x b) y bl = balance (T R a x b) y bl
-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
type family DiscriminateBalR (l :: Map k v) (r :: Map k v) :: Bool where
    DiscriminateBalR _ (N R _ _ _ _) = False
    DiscriminateBalR _ _             = True

class BalanceableR (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
    type BalR l k v r :: Map Symbol Type
    balRR :: Record f (N color l k v r) -> Record f (BalR l k v r)
    balRV :: Variant f (N color l k v r) -> Variant f (BalR l k v r)

class BalanceableHelperR (b :: Bool) (l :: Map Symbol Type) (k :: Symbol) (v :: Type) (r :: Map Symbol Type) where
    type BalR' b l k v r :: Map Symbol Type
    balRR' :: Record f (N color l k v r) -> Record f (BalR' b l k v r)
    balRV' :: Variant f (N color l k v r) -> Variant f (BalR' b l k v r)

instance (DiscriminateBalR l r ~ b, BalanceableHelperR b l k v r) => BalanceableR l k v r where
    type BalR l k v r = BalR' (DiscriminateBalR l r) l k v r
    balRR = balRR' @b @l @k @v @r
    balRV = balRV' @b @l @k @v @r

-- balright :: RB a -> a -> RB a -> RB a
-- balright a x (T R b y c) = T R a x (T B b y c)
instance BalanceableHelperR False right2 k2 v2 (N R left1 k1 v1 right1) where
    type BalR'              False right2 k2 v2 (N R left1 k1 v1 right1) =
                                  (N R right2 k2 v2 (N B left1 k1 v1 right1))
    balRR' (Node right v (Node left' v' right')) = Node  right v (Node left' v' right')
    balRV' v = case v of LookLeft x   -> LookLeft x
                         Here x       -> Here x
                         LookRight x  -> LookRight (case x of LookLeft y  -> LookLeft y
                                                              Here y      -> Here y
                                                              LookRight y -> LookRight y)

-- balright (T B a x b) y bl = balance (T R a x b) y bl
instance (N R t2 z zv t3 ~ g, ShouldBalance g t1 ~ shouldbalance, BalanceableHelper shouldbalance g y yv t1) =>
    BalanceableHelperR True (N B t2 z zv t3) y yv t1 where
    type BalR'         True (N B t2 z zv t3) y yv t1
             =  Balance (N R t2 z zv t3) y yv t1
    balRR' (Node (Node left1 v1 right1) v2 right2) = balanceR @(N R t2 z zv t3) @y @yv @t1
           (Node (Node left1 v1 right1) v2 right2)
    balRV' v = balanceV @(N R t2 z zv t3) @y @yv @t1 (case v of
        LookLeft l -> LookLeft (case l of
            LookLeft l' -> LookLeft l'
            Here x' -> Here x'
            LookRight r' -> LookRight r')
        Here x -> Here x
        LookRight r -> LookRight r)

-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
instance (N R t2 u uv t3 ~ g, ShouldBalance g l ~ shouldbalance, BalanceableHelper shouldbalance g z zv l) =>
    BalanceableHelperR True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 where
    type BalR'         True (N R (N B t2 u uv t3) z zv (N B l k kv r)) y yv t1 =
                             N R (Balance (N R t2 u uv t3) z zv l) k kv (N B r y yv t1)
    balRR' (Node (Node (Node left2 v2 right2) vx (Node left3 v3 right3)) v1 left1) =
            Node (balanceR @(N R t2 u uv t3) @z @zv @l (Node (Node left2 v2 right2) vx left3)) v3 (Node right3 v1 left1)
    balRV' v = case v of
        LookLeft  (LookLeft rr)                 -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (LookLeft (case rr of
                                                        LookLeft t2 -> LookLeft t2
                                                        Here uv -> Here uv
                                                        LookRight t3 -> LookRight t3)))
        LookLeft  (Here zv)                     -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (Here zv))
        LookLeft  (LookRight (LookLeft l))      -> LookLeft (balanceV @(N R t2 u uv t3) @z @zv @l (LookRight l))
        LookLeft  (LookRight (Here kv))         -> Here kv
        LookLeft  (LookRight (LookRight r))     -> LookRight (LookLeft r)
        Here      yv                            -> LookRight (Here yv)
        LookRight t1                            -> LookRight (LookRight t1)

-- app :: RB a -> RB a -> RB a
-- app E x = x
-- app x E = x
-- app (T R a x b) (T R c y d) =
--  case app b c of
--      T R b' z c' -> T R(T R a x b') z (T R c' y d)
--      bc -> T R a x (T R bc y d)
-- app (T B a x b) (T B c y d) = 
--  case app b c of
--      T R b' z c' -> T R(T B a x b') z (T B c' y d)
--      bc -> balleft a x (T B bc y d)
-- app a (T R b x c) = T R (app a b) x c
-- app (T R a x b) c = T R a x (app b c)


class Fuseable (l :: Map Symbol Type) (r :: Map Symbol Type) where
    type Fuse l r :: Map Symbol Type
    fuseRecord :: Record f l -> Record f r -> Record f (Fuse l r)
    fuseVariant :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)

instance Fuseable E E where
    type Fuse E E = E
    fuseRecord _ _ = unit
    fuseVariant v = case v of

-- app E x = x
instance Fuseable E (N color left k v right) where
    type Fuse E (N color left k v right) = N color left k v right
    fuseRecord _ r = r
    fuseVariant e = case e of
        Right v -> v

-- app x E = x
instance Fuseable (N color left k v right) E where
    type Fuse (N color left k v right) E = N color left k v right
    fuseRecord r _ = r
    fuseVariant e = case e of
        Left v -> v

-- app a (T R b x c) = T R (app a b) x c
instance Fuseable (N B left1 k1 v1 right1) left2
    => Fuseable (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) where
    type Fuse   (N B left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (Fuse (N B left1 k1 v1 right1) left2) k2 v2 right2
    fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node (fuseRecord @(N B left1 k1 v1 right1) (Node left1 v1 right1) left2) v2 right2
    fuseVariant e = case e of
        Left l  -> case l of
            LookLeft left1   -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (LookLeft left1)))
            Here v1          -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (Here v1)))
            LookRight right1 -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Left (LookRight right1)))
        Right r -> case r of
            LookLeft left2   -> LookLeft  (fuseVariant @(N B left1 k1 v1 right1) @left2 (Right left2))
            Here v2          -> Here      v2
            LookRight right2 -> LookRight right2


-- app (T R a x b) c = T R a x (app b c)
instance Fuseable right1 (N B left2 k2 v2 right2)
    => Fuseable (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) where
    type Fuse   (N R left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R left1 k1 v1 (Fuse right1 (N B left2 k2 v2 right2))
    fuseRecord (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (fuseRecord @_ @(N B left2 k2 v2 right2) right1 (Node left2 v2 right2))
    fuseVariant e = case e of
        Left l  -> case l of
            LookLeft left1   -> LookLeft left1
            Here v1          -> Here v1
            LookRight right1 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Left right1))
        Right r -> case r of
            LookLeft left2   -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (LookLeft left2)))
            Here v2          -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (Here v2)))
            LookRight right2 -> LookRight (fuseVariant @right1 @(N B left2 k2 v2 right2) (Right (LookRight right2)))


-- app (T R a x b) (T R c y d) =
instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper1 fused (N R left1 k1 v1 right1) (N R left2 k2 v2 right2))
    => Fuseable (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where
    type Fuse   (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = Fuse1 (Fuse right1 left2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2)
    fuseRecord = fuseRecord1 @(Fuse right1 left2)
    fuseVariant = fuseVariant1 @(Fuse right1 left2)

class FuseableHelper1 (fused :: Map Symbol Type) (l :: Map Symbol Type) (r :: Map Symbol Type) where
    type Fuse1 fused l r :: Map Symbol Type
    fuseRecord1 :: Record f l -> Record f r -> Record f (Fuse l r)
    fuseVariant1 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)

-- app (T R a x b) (T R c y d) =
--  case app b c of
--      T R b' z c' -> T R (T R a x b') z (T R c' y d)
-- FIXME: The Fuseable constraint is repeated from avobe :(
instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2)
    => FuseableHelper1 (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where
    type Fuse1         (N R s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R (N R left1 k1 v1 s1) z zv (N R s2 k2 v2 right2)
    fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) =
        case fuseRecord right1 left2 of
            Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2)
    fuseVariant1 e =
        case e of
            Left l  -> case l of
                            LookLeft  left1  -> LookLeft (LookLeft left1)
                            Here      v1     -> LookLeft (Here v1)
                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
                                                    LookLeft s1  -> LookLeft (LookRight s1)
                                                    Here zv      -> Here zv
                                                    LookRight s2 -> LookRight (LookLeft s2)
            Right r -> case r of
                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
                                                    LookLeft s1  -> LookLeft (LookRight s1)
                                                    Here zv      -> Here zv
                                                    LookRight s2 -> LookRight (LookLeft s2)
                            Here      v2     -> LookRight (Here v2)
                            LookRight right2 -> LookRight (LookRight right2)


-- app (T R a x b) (T R c y d) =
--  case app b c of
--      ...
--      bc -> T R a x (T R bc y d)
-- FIXME: The Fuseable constraint is repeated from above :(
instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2)
    => FuseableHelper1 (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) where
    type Fuse1         (N B s1 z zv s2) (N R left1 k1 v1 right1) (N R left2 k2 v2 right2) = N R left1 k1 v1 (N R (N B s1 z zv s2) k2 v2 right2)
    fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) =
        case fuseRecord right1 left2 of
            Node s1 zv s2 -> Node left1 v1 (Node (Node s1 zv s2) v2 right2)
    fuseVariant1 e =
        case e of
            Left l  -> case l of
                            LookLeft  left1  -> LookLeft left1
                            Here      v1     -> Here v1
                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
                                                    LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                    Here zv      -> LookRight (LookLeft (Here zv))
                                                    LookRight s2 -> LookRight (LookLeft (LookRight s2))
            Right r -> case r of
                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
                                                    LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                    Here zv      -> LookRight (LookLeft (Here zv))
                                                    LookRight s2 -> LookRight (LookLeft (LookRight s2))
                            Here      v2     -> LookRight (Here v2)
                            LookRight right2 -> LookRight (LookRight right2)

-- app (T R a x b) (T R c y d) =
--  case app b c of
--      ...
--      bc -> T R a x (T R bc y d)
instance FuseableHelper1 E (N R left1 k1 v1 E) (N R E k2 v2 right2) where
    type Fuse1           E (N R left1 k1 v1 E) (N R E k2 v2 right2) = N R left1 k1 v1 (N R E k2 v2 right2)
    fuseRecord1 (Node left1 v1 right1) (Node left2 v2 right2) = Node left1 v1 (Node Empty v2 right2)
    fuseVariant1 e =
        case e of
            Left l  -> case l of
                            LookLeft  left1  -> LookLeft left1
                            Here      v1     -> Here v1
            Right r -> case r of
                            Here      v2     -> LookRight (Here v2)
                            LookRight right2 -> LookRight (LookRight right2)

-- app (T B a x b) (T B c y d) = 
instance (Fuseable right1 left2, Fuse right1 left2 ~ fused, FuseableHelper2 fused (N B left1 k1 v1 right1) (N B left2 k2 v2 right2))
    => Fuseable (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
    type Fuse   (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = Fuse2 (Fuse right1 left2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2)
    fuseRecord = fuseRecord2 @(Fuse right1 left2)
    fuseVariant = fuseVariant2 @(Fuse right1 left2)

-- could FuseableHelper1 and FuseableHelper2 be, well... fused?
class FuseableHelper2 (fused :: Map Symbol Type) (l :: Map Symbol Type) (r :: Map Symbol Type) where
    type Fuse2 fused l r :: Map Symbol Type
    fuseRecord2 :: Record f l -> Record f r -> Record f (Fuse l r)
    fuseVariant2 :: Either (Variant f l) (Variant f r) -> Variant f (Fuse l r)

-- app (T B a x b) (T B c y d) = 
--  case app b c of
--      T R b' z c' -> T R (T B a x b') z (T B c' y d)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N R s1 z zv s2)
    => FuseableHelper2 (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
    type Fuse2         (N R s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = N R (N B left1 k1 v1 s1) z zv (N B s2 k2 v2 right2)
    fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) =
        case fuseRecord right1 left2 of
            Node s1 zv s2 -> Node (Node left1 v1 s1) zv (Node s2 v2 right2)
    fuseVariant2 e =
        case e of
            Left l  -> case l of
                            LookLeft  left1  -> LookLeft (LookLeft left1)
                            Here      v1     -> LookLeft (Here v1)
                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
                                                    LookLeft s1  -> LookLeft (LookRight s1)
                                                    Here zv      -> Here zv
                                                    LookRight s2 -> LookRight (LookLeft s2)
            Right r -> case r of
                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
                                                    LookLeft s1  -> LookLeft (LookRight s1)
                                                    Here zv      -> Here zv
                                                    LookRight s2 -> LookRight (LookLeft s2)
                            Here      v2     -> LookRight (Here v2)
                            LookRight right2 -> LookRight (LookRight right2)

-- app (T B a x b) (T B c y d) = 
--  case app b c of
--      ...
--      bc -> balleft a x (T B bc y d)
instance (Fuseable right1 left2, Fuse right1 left2 ~ N B s1 z zv s2, BalanceableL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2))
    => FuseableHelper2 (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) where
    type Fuse2         (N B s1 z zv s2) (N B left1 k1 v1 right1) (N B left2 k2 v2 right2) = BalL left1 k1 v1 (N B (N B s1 z zv s2) k2 v2 right2)
    fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) =
        case fuseRecord @right1 @left2 right1 left2 of
            Node s1 zv s2 -> balLR @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (Node left1 v1 (Node (Node s1 zv s2) v2 right2))
    fuseVariant2 e = balLV @left1 @k1 @v1 @(N B (N B s1 z zv s2) k2 v2 right2) (case e of
            Left l  -> case l of
                            LookLeft  left1  -> LookLeft left1
                            Here      v1     -> Here v1
                            LookRight right1 -> case fuseVariant @right1 @left2 (Left right1) of
                                                    LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                    Here zv      -> LookRight (LookLeft (Here zv))
                                                    LookRight s2 -> LookRight (LookLeft (LookRight s2))
            Right r -> case r of
                            LookLeft  left2  -> case fuseVariant @right1 @left2 (Right left2) of
                                                    LookLeft s1  -> LookRight (LookLeft (LookLeft s1))
                                                    Here zv      -> LookRight (LookLeft (Here zv))
                                                    LookRight s2 -> LookRight (LookLeft (LookRight s2))
                            Here      v2     -> LookRight (Here v2)
                            LookRight right2 -> LookRight (LookRight right2))

-- app (T B a x b) (T B c y d) = 
--  case app b c of
--      ...
--      bc -> balleft a x (T B bc y d)
instance (BalanceableL left1 k1 v1 (N B E k2 v2 right2))
    => FuseableHelper2 E (N B left1 k1 v1 E) (N B E k2 v2 right2) where
    type Fuse2         E (N B left1 k1 v1 E) (N B E k2 v2 right2) = BalL left1 k1 v1 (N B E k2 v2 right2)
    fuseRecord2 (Node left1 v1 right1) (Node left2 v2 right2) =
            balLR @left1 @k1 @v1 @(N B E k2 v2 right2) (Node left1 v1 (Node Empty v2 right2))
    fuseVariant2 e = balLV @left1 @k1 @v1 @(N B E k2 v2 right2) (case e of
            Left l  -> case l of
                            LookLeft  left1  -> LookLeft left1
                            Here      v1     -> Here v1
            Right r -> case r of
                            Here      v2     -> LookRight (Here v2)
                            LookRight right2 -> LookRight (LookRight right2))


--  del E = E
--  del (T _ a y b)
--      | x<y = delformLeft a y b
--      | x>y = delformRight a y b
--      | otherwise = app a b
class Delable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
    type Del k v t :: Map Symbol Type
    del :: Record f t -> Record f (Del k v t)
    win :: Variant f t -> Either (Variant f (Del k v t)) (f v)

--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
--  delformLeft a y b = T R (del a) y b
--  In the term-level code, the k to delete is already on the environment.
class DelableL (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
    type DelL k v l kx vx r :: Map Symbol Type
    delL :: Record f (N color l kx vx r) -> Record f (DelL k v l kx vx r)
    winL :: Variant f (N color l kx vx r) -> Either (Variant f (DelL k v l kx vx r)) (f v)

--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableL deleted kx vx right)
    => DelableL k v (N B leftz kz vz rightz) kx vx right where
    type DelL   k v (N B leftz kz vz rightz) kx vx right = BalL (Del k v (N B leftz kz vz rightz)) kx vx right
    delL (Node left vx right) = balLR @(Del k v (N B leftz kz vz rightz)) @kx @vx @right (Node (del @k @v left) vx right)
    winL v = first (balLV @(Del k v (N B leftz kz vz rightz)) @kx @vx @right) (case v of
        LookLeft l -> first LookLeft (win @k @v l)
        Here vx -> Left $ Here vx
        LookRight r -> Left $ LookRight r)

--  delformLeft a y b = T R (del a) y b
instance (Delable k v (N R leftz kz vz rightz))
    => DelableL k v (N R leftz kz vz rightz) kx vx right where
    type DelL   k v (N R leftz kz vz rightz) kx vx right = N R (Del k v (N R leftz kz vz rightz)) kx vx right
    delL (Node left vx right) = Node (del @k @v left) vx right
    winL v = case v of
        LookLeft l -> first LookLeft (win @k @v l)
        Here vx -> Left (Here vx)
        LookRight r -> Left (LookRight r)

--  delformLeft a y b = T R (del a) y b
instance DelableL k v E kx vx right where
    type DelL     k v E kx vx right = N R E kx vx right
    delL (Node left vx right) = Node Empty vx right
    winL v = case v of
        Here vx -> Left (Here vx)
        LookRight r -> Left (LookRight r)

--  delformRight a y b@(T B _ _ _) = balright a y (del b)
--  delformRight a y b = T R a y (del b)
class DelableR (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
    type DelR k v l kx vx r :: Map Symbol Type
    delR :: Record f (N color l kx vx r) -> Record f (DelR k v l kx vx r)
    winR :: Variant f (N color l kx vx r) -> Either (Variant f (DelR k v l kx vx r)) (f v)

--  delformRight a y b@(T B _ _ _) = balright a y (del b)
instance (N B leftz kz vz rightz ~ g, Delable k v g, Del k v g ~ deleted, BalanceableR left kx vx deleted)
    => DelableR k v left kx vx (N B leftz kz vz rightz) where
    type DelR   k v left kx vx (N B leftz kz vz rightz) = BalR left kx vx (Del k v (N B leftz kz vz rightz))
    delR (Node left vx right) = balRR @left @kx @vx @(Del k v (N B leftz kz vz rightz)) (Node left vx (del @k @v right))
    winR v = first (balRV @left @kx @vx @(Del k v (N B leftz kz vz rightz))) (case v of
        LookLeft l -> Left $ LookLeft l
        Here vx -> Left $ Here vx
        LookRight r -> first LookRight (win @k @v r))

--  delformRight a y b = T R a y (del b)
instance (Delable k v (N R leftz kz vz rightz))
    => DelableR k v left kx vx (N R leftz kz vz rightz) where
    type   DelR k v left kx vx (N R leftz kz vz rightz) = N R left kx vx (Del k v (N R leftz kz vz rightz))
    delR (Node left vx right) = Node left vx (del @k @v right)
    winR v = case v of
        LookLeft l -> Left (LookLeft l)
        Here vx -> Left (Here vx)
        LookRight r -> first LookRight (win @k @v r)

--  delformRight a y b = T R a y (del b)
instance DelableR k v left kx vx E where
    type DelR     k v left kx vx E = N R left kx vx E
    delR (Node left vx right) = Node left vx Empty
    winR v = case v of
        LookLeft l -> Left (LookLeft l)
        Here vx -> Left (Here vx)

--  del E = E
instance Delable k v E where
    type Del     k v E = E
    del _ = unit
    win = impossible

-- the color is discarded
--  del (T _ a y b)
--      | x<y = delformLeft a y b
--      | x>y = delformRight a y b
--      | otherwise = app a b
instance (CmpSymbol kx k ~ ordering, DelableHelper ordering k v left kx vx right) => Delable k v (N color left kx vx right) where
    type Del k v (N color left kx vx right) = Del' (CmpSymbol kx k) k v left kx vx right
    del = del' @(CmpSymbol kx k) @k @v @left @kx @vx @right
    win = win' @(CmpSymbol kx k) @k @v @left @kx @vx @right

class DelableHelper (ordering :: Ordering) (k :: Symbol) (v :: Type) (l :: Map Symbol Type) (kx :: Symbol) (vx :: Type) (r :: Map Symbol Type) where
    type Del' ordering k v l kx vx r :: Map Symbol Type
    del' :: Record f (N color l kx vx r) -> Record f (Del' ordering k v l kx vx r)
    win' :: Variant f (N color l kx vx r) -> Either (Variant f (Del' ordering k v l kx vx r)) (f v)

--      | x<y = delformLeft a y b
instance DelableL k v left kx vx right => DelableHelper GT k v left kx vx right where
    type Del'                                           GT k v left kx vx right = DelL k v left kx vx right
    del' = delL @k @v @left @kx @vx @right
    win' = winL @k @v @left @kx @vx @right

--      | otherwise = app a b
instance Fuseable left right => DelableHelper EQ k v left k v right where
    type Del'                                 EQ k v left k v right = Fuse left right
    del' (Node left _ right) = fuseRecord @left @right left right
    win' v = case v of
        LookLeft l  ->  Left $ fuseVariant @left @right (Left l)
        Here v      -> Right v
        LookRight r -> Left $ fuseVariant @left @right (Right r)

--      | x>y = delformRight a y b
instance DelableR k v left kx vx right => DelableHelper LT k v left kx vx right where
    type Del'                                           LT k v left kx vx right = DelR k v left kx vx right
    del' = delR @k @v @left @kx @vx @right
    win' = winR @k @v @left @kx @vx @right

{- | Class that determines if the pair of a 'Symbol' key and a 'Type' can
     be deleted from a type-level map.
 
     The associated type family 'Delete' produces the resulting map.

     At the term level, this manifests in 'delete', which removes a field from
     a record, and in 'winnow', which checks if a 'Variant' is of a given
     branch and returns the value in the branch if there's a match, or a
     reduced 'Variant' if there isn't. 'winnow' tends to be more useful in
     practice.

     If the map already has the key but with a /different/ 'Type', the deletion
     fails to compile.
 -}
class Deletable (k :: Symbol) (v :: Type) (t :: Map Symbol Type) where
    type Delete k v t :: Map Symbol Type
    delete :: Record f t -> Record f (Delete k v t)
    winnow :: Variant f t -> Either (Variant f (Delete k v t)) (f v)

instance (Delable k v t, Del k v t ~ deleted, CanMakeBlack deleted) => Deletable k v t where
    type Delete k v t = MakeBlack (Del k v t)
    delete r = makeBlackR (del @k @v r)
    winnow v = first makeBlackV (win @k @v v)


{- | Like 'winnow' but specialized to pure 'Variant's.
-}
winnowI :: forall k v t . Deletable k v t => Variant I t -> Either (Variant I (Delete k v t)) v
winnowI = fmap unI . winnow @k @v @t

-- The original term-level code, taken from:
-- https://www.cs.kent.ac.uk/people/staff/smk/redblack/rb.html
--
-- {- Version 1, 'untyped' -}
-- data Color = R | B deriving Show
-- data RB a = E | T Color (RB a) a (RB a) deriving Show
-- 
-- {- Insertion and membership test as by Okasaki -}
-- insert :: Ord a => a -> RB a -> RB a
-- insert x s =
--  T B a z b
--  where
--  T _ a z b = ins s
--  ins E = T R E x E
--  ins s@(T B a y b)
--      | x<y = balance (ins a) y b
--      | x>y = balance a y (ins b)
--      | otherwise = s
--  ins s@(T R a y b)
--      | x<y = T R (ins a) y b
--      | x>y = T R a y (ins b)
--      | otherwise = s
-- 
-- 
-- {- balance: first equation is new,
--    to make it work with a weaker invariant -}
-- balance :: RB a -> a -> RB a -> RB a
-- balance (T R a x b) y (T R c z d) = T R (T B a x b) y (T B c z d)
-- balance (T R (T R a x b) y c) z d = T R (T B a x b) y (T B c z d)
-- balance (T R a x (T R b y c)) z d = T R (T B a x b) y (T B c z d)
-- balance a x (T R b y (T R c z d)) = T R (T B a x b) y (T B c z d)
-- balance a x (T R (T R b y c) z d) = T R (T B a x b) y (T B c z d)
-- balance a x b = T B a x b
--
-- member :: Ord a => a -> RB a -> Bool
-- member x E = False
-- member x (T _ a y b)
--  | x<y = member x a
--  | x>y = member x b
--  | otherwise = True
-- 
-- {- deletion a la SMK -}
-- delete :: Ord a => a -> RB a -> RB a
-- delete x t =
--  case del t of {T _ a y b -> T B a y b; _ -> E}
--  where
--  del E = E
--  del (T _ a y b)
--      | x<y = delformLeft a y b
--      | x>y = delformRight a y b
--             | otherwise = app a b
--  delformLeft a@(T B _ _ _) y b = balleft (del a) y b
--  delformLeft a y b = T R (del a) y b
--
--  delformRight a y b@(T B _ _ _) = balright a y (del b)
--  delformRight a y b = T R a y (del b)
-- 
-- balleft :: RB a -> a -> RB a -> RB a
-- balleft (T R a x b) y c = T R (T B a x b) y c
-- balleft bl x (T B a y b) = balance bl x (T R a y b)
-- balleft bl x (T R (T B a y b) z c) = T R (T B bl x a) y (balance b z (sub1 c))
-- 
-- balright :: RB a -> a -> RB a -> RB a
-- balright a x (T R b y c) = T R a x (T B b y c)
-- balright (T B a x b) y bl = balance (T R a x b) y bl
-- balright (T R a x (T B b y c)) z bl = T R (balance (sub1 a) x b) y (T B c z bl)
-- 
-- sub1 :: RB a -> RB a
-- sub1 (T B a x b) = T R a x b
-- sub1 _ = error "invariance violation"
-- 
-- app :: RB a -> RB a -> RB a
-- app E x = x
-- app x E = x
-- app (T R a x b) (T R c y d) =
--  case app b c of
--      T R b' z c' -> T R (T R a x b') z (T R c' y d)
--      bc -> T R a x (T R bc y d)
-- app (T B a x b) (T B c y d) = 
--  case app b c of
--      T R b' z c' -> T R(T B a x b') z (T B c' y d)
--      bc -> balleft a x (T B bc y d)
-- app a (T R b x c) = T R (app a b) x c
-- app (T R a x b) c = T R a x (app b c)