{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Internal module of "Proarrow.Tools.SMC": the contexts of terms, and the operations on them that
-- reorder, copy and discard variables. It exports everything, also what the public module keeps
-- hidden.
module Proarrow.Tools.SMC.Internal.Context where

import Data.Kind (Constraint, Type)
import GHC.TypeNats (CmpNat, Nat)
import Proarrow.Category.Monoidal
  ( Monoidal (..)
  , SymMonoidal (..)
  , associator'
  , associatorInv'
  , rightUnitorWith
  , swapInner
  )
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Core (CategoryOf (..), Promonad (..), obj)
import Proarrow.Monoid (CocommutativeComonoid, Comonoid (..))
import Proarrow.Object (Obj)
import Prelude (Ordering (..), type (~))

import Proarrow.Tools.SMC.Internal.Syntax

-- | A context: the variables a term uses, each with its id and type, by descending id.
type Ctx :: Type -> Type
type Ctx k = [(Nat, SYN k)]

-- | The type standing in for a context: the tensor of its variables' types, with the most
-- recently bound variable on the right. A single variable is just its type, so a variable is the
-- identity. The cost is that @Mul ('(n, a) ': g)@ only reduces once @g@ is known to be empty or
-- not, which 'ctxCase' tells.
type Mul :: forall {k}. Ctx k -> SYN k
type family Mul g where
  Mul '[] = I
  Mul '[ '(n, a)] = a
  Mul ('(n, a) ': g) = Mul g :** a

-- | A context that is known to be empty or not, all the way down.
type KnownCtx :: forall {k}. Ctx k -> Constraint
class KnownCtx (g :: Ctx k) where
  -- | Case analysis on the context, which is what lets @'Mul' ('(n, a) ': g)@ reduce.
  ctxCase :: ((g ~ '[]) => r) -> (forall n a g'. (g ~ ('(n, a) ': g'), KnownObj a, KnownCtx g') => r) -> r

  -- | The tensor of a context is an object. A method rather than a function over 'ctxCase', so that
  -- at a known context it is not recursive and can be inlined.
  withCtxOb :: (Monoidal k) => ((Ob (Interp (Mul g))) => r) -> r

instance KnownCtx ('[] :: Ctx k) where
  {-# INLINE ctxCase #-}
  {-# INLINE withCtxOb #-}
  ctxCase :: forall r.
(('[] ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    ('[] ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase ('[] ~ '[]) => r
e forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
('[] ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
r
_ = r
('[] ~ '[]) => r
e
  withCtxOb :: forall r. Monoidal k => (Ob (Interp (Mul '[])) => r) -> r
withCtxOb Ob (Interp (Mul '[])) => r
r = r
Ob (Interp (Mul '[])) => r
r

instance (KnownObj a, KnownCtx g) => KnownCtx ('(n, a) ': g) where
  {-# INLINE ctxCase #-}
  {-# INLINE withCtxOb #-}
  ctxCase :: forall r.
((('(n, a) : g) ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (('(n, a) : g) ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase (('(n, a) : g) ~ '[]) => r
_ forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
(('(n, a) : g) ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
r
c = r
forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
(('(n, a) : g) ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
r
c
  withCtxOb :: forall r. Monoidal k => (Ob (Interp (Mul ('(n, a) : g))) => r) -> r
withCtxOb Ob (Interp (Mul ('(n, a) : g))) => r
r = forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a r
Ob (Interp a) => r
Ob (Interp (Mul ('(n, a) : g))) => r
r) (forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall k (a :: k) (b :: k) r.
(Monoidal k, Ob a, Ob b) =>
(Ob (a ** b) => r) -> r
withOb2 @_ @(Interp (Mul g)) @(Interp a) r
Ob (Interp (Mul g) ** Interp a) => r
Ob (Interp (Mul ('(n, a) : g))) => r
r)))

-- | The identity on the tensor of a context.
{-# INLINE ctxOb #-}
ctxOb :: forall {k} (g :: Ctx k). (Monoidal k, KnownCtx g) => Obj (Interp (Mul g))
ctxOb :: forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb = forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g (forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Interp (Mul g)))

-- | A new variable on the right of a context: a unitor if the context was empty, and nothing
-- otherwise.
{-# INLINE snoc #-}
snoc
  :: forall {k} n (a :: SYN k) g
   . (Monoidal k, KnownObj a, KnownCtx g) => Interp (Mul g) ** Interp a ~> Interp (Mul ('(n, a) ': g))
snoc :: forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc = forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (Unit ** Interp a) ~> Interp a
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
Ob (Interp a) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(n, a) ': g))

-- | The context of two terms used side by side.
type Union :: forall {k}. Ctx k -> Ctx k -> Ctx k
type family Union g1 g2 where
  Union '[] g2 = g2
  Union g1 '[] = g1
  Union ('(n, a) ': g1) ('(m, b) ': g2) = UnionBy (CmpNat n m) ('(n, a) ': g1) ('(m, b) ': g2)

type UnionBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Ctx k
type family UnionBy o g1 g2 where
  UnionBy GT (x ': g1) g2 = x ': Union g1 g2
  UnionBy LT g1 (y ': g2) = y ': Union g1 g2
  UnionBy EQ (x ': g1) (y ': g2) = x ': Union g1 g2

-- | The newest variable split off the tensor of a context, the inverse of 'snoc'.
{-# INLINE unsnoc #-}
unsnoc
  :: forall {k} n (a :: SYN k) g
   . (Monoidal k, KnownObj a, KnownCtx g) => Interp (Mul ('(n, a) ': g)) ~> Interp (Mul g) ** Interp a
unsnoc :: forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
unsnoc = forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g (forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a Interp a ~> (Unit ** Interp a)
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
Ob (Interp a) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(n, a) ': g))

-- | Split the tensor of the union of two contexts into the tensors of the two contexts. This is
-- where the wires are reordered, the only place 'swap' is used, and where a variable that both
-- contexts have is copied.
type Merge :: forall {k}. Ctx k -> Ctx k -> Constraint
class (KnownCtx g1, KnownCtx g2) => Merge (g1 :: Ctx k) g2 where
  merge :: Interp (Mul (Union g1 g2)) ~> Interp (Mul g1) ** Interp (Mul g2)

instance (Monoidal k, KnownCtx g2) => Merge ('[] :: Ctx k) g2 where
  {-# INLINE merge #-}
  merge :: Interp (Mul (Union '[] g2))
~> (Interp (Mul '[]) ** Interp (Mul g2))
merge = forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g2 Interp (Mul g2) ~> (Unit ** Interp (Mul g2))
Ob (Interp (Mul g2)) =>
Interp (Mul g2) ~> (Unit ** Interp (Mul g2))
forall (a :: k). Ob a => a ~> (Unit ** a)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv

instance (Monoidal k, KnownCtx ('(n, a) ': g1)) => Merge ('(n, a) ': g1 :: Ctx k) '[] where
  {-# INLINE merge #-}
  merge :: Interp (Mul (Union ('(n, a) : g1) '[]))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul '[]))
merge = forall (g :: [(Nat, SYN k)]) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(n, a) ': g1) Interp (Mul ('(n, a) : g1))
~> (Interp (Mul ('(n, a) : g1)) ** Unit)
Ob (Interp (Mul ('(n, a) : g1))) =>
Interp (Mul ('(n, a) : g1))
~> (Interp (Mul ('(n, a) : g1)) ** Unit)
forall (a :: k). Ob a => a ~> (a ** Unit)
forall k (a :: k). (Monoidal k, Ob a) => a ~> (a ** Unit)
rightUnitorInv

instance
  ( Monoidal k
  , KnownObj a
  , KnownObj b
  , KnownCtx g1
  , KnownCtx g2
  , MergeBy (CmpNat n m) ('(n, a) ': g1 :: Ctx k) ('(m, b) ': g2)
  )
  => Merge ('(n, a) ': g1 :: Ctx k) ('(m, b) ': g2)
  where
  {-# INLINE merge #-}
  merge :: Interp (Mul (Union ('(n, a) : g1) ('(m, b) : g2)))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
merge = forall (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
MergeBy o g1 g2 =>
Interp (Mul (UnionBy o g1 g2))
~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
MergeBy o g1 g2 =>
Interp (Mul (UnionBy o g1 g2))
~> (Interp (Mul g1) ** Interp (Mul g2))
mergeBy @(CmpNat n m) @('(n, a) ': g1) @('(m, b) ': g2)

-- | 'merge' for two non-empty contexts, by which of the two has the larger head id.
type MergeBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Constraint
class (KnownCtx g1, KnownCtx g2) => MergeBy o (g1 :: Ctx k) g2 where
  mergeBy :: Interp (Mul (UnionBy o g1 g2)) ~> Interp (Mul g1) ** Interp (Mul g2)

-- The union of two non-empty contexts is not empty, so its tensor splits off the newest variable
-- as is, which the equality says for GHC. If the newest variable is alone on its side, merging is
-- one swap or nothing.
instance
  ( SymMonoidal k
  , Merge g1 ('(m, b) ': g2)
  , KnownObj (a :: SYN k)
  , KnownObj b
  , Mul ('(n, a) ': Union g1 ('(m, b) ': g2)) ~ (Mul (Union g1 ('(m, b) ': g2)) :** a)
  )
  => MergeBy GT ('(n, a) ': g1) ('(m, b) ': g2)
  where
  {-# INLINE mergeBy #-}
  mergeBy :: Interp (Mul (UnionBy 'GT ('(n, a) : g1) ('(m, b) : g2)))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
mergeBy =
    forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(m, b) ': g2)
      ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a
          ( forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g1
              (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp (Mul ('(m, b) ': g2))) @(Interp a))
              ( Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp a)
-> Obj (Interp (Mul ('(m, b) : g2)))
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp a ** Interp (Mul ('(m, b) : g2))))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp a)
       ** Interp (Mul ('(m, b) : g2)))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2))
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp a ** Interp (Mul ('(m, b) : g2))))
 ~> ((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2))))
-> ((Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a)
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp a ** Interp (Mul ('(m, b) : g2)))))
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp a)
       ** Interp (Mul ('(m, b) : g2)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1 Obj (Interp (Mul ('(n, a) : g')))
-> ((Interp (Mul ('(m, b) : g2)) ** Interp a)
    ~> (Interp a ** Interp (Mul ('(m, b) : g2))))
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp a ** Interp (Mul ('(m, b) : g2))))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp (Mul ('(m, b) ': g2))) @(Interp a))
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
 ~> (Interp (Mul ('(n, a) : g'))
     ** (Interp a ** Interp (Mul ('(m, b) : g2)))))
-> ((Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a)
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp a ** Interp (Mul ('(m, b) : g2))))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp (Mul ('(m, b) : g2)))
-> Obj (Interp a)
-> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2)) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
                  (((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
  ** Interp a)
 ~> (Interp (Mul ('(n, a) : g'))
     ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> ((Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a)
    ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
        ** Interp a))
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @g1 @('(m, b) ': g2) (Interp (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
 ~> (Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2))))
-> Obj (Interp a)
-> (Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
    ** Interp a)
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
       ** Interp a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
              )
          )
      )

instance
  ( Monoidal k
  , Merge ('(n, a) ': g1) g2
  , KnownObj a
  , KnownObj (b :: SYN k)
  , Mul ('(m, b) ': Union ('(n, a) ': g1) g2) ~ (Mul (Union ('(n, a) ': g1) g2) :** b)
  )
  => MergeBy LT ('(n, a) ': g1) ('(m, b) ': g2)
  where
  {-# INLINE mergeBy #-}
  mergeBy :: Interp (Mul (UnionBy 'LT ('(n, a) : g1) ('(m, b) : g2)))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
mergeBy =
    forall (g :: [(Nat, SYN k)]) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: [(Nat, SYN k)]).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g2
      (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': '(n, a) ': g1))
      ( Obj (Interp (Mul ('(n, a) : g1)))
-> Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp b)
-> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
    ** Interp b)
   ~> (Interp (Mul ('(n, a) : g1))
       ** (Interp (Mul ('(n, a) : g')) ** Interp b))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(n, a) ': g1)) (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g2) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
          (((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
  ** Interp b)
 ~> (Interp (Mul ('(n, a) : g1))
     ** (Interp (Mul ('(n, a) : g')) ** Interp b)))
-> ((Interp
       (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
     ** Interp b)
    ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
        ** Interp b))
-> (Interp
      (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
    ** Interp b)
   ~> (Interp (Mul ('(n, a) : g1))
       ** (Interp (Mul ('(n, a) : g')) ** Interp b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g1 :: [(Nat, SYN k)]) (g2 :: [(Nat, SYN k)]).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @('(n, a) ': g1) @g2 (Interp (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
 ~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g'))))
-> Obj (Interp b)
-> (Interp
      (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
    ** Interp b)
   ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
       ** Interp b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
      )

-- | A variable both contexts have is copied, one copy for each side.
instance
  ( SymMonoidal k
  , CocommutativeComonoid (Interp a)
  , KnownObj (a :: SYN k)
  , a ~ b
  , Merge g1 g2
  , KnownCtx (Union g1 g2)
  )
  => MergeBy EQ ('(n, a) ': g1) ('(m, b) ': g2)
  where
  {-# INLINE mergeBy #-}
  mergeBy :: Interp (Mul (UnionBy 'EQ ('(n, a) : g1) ('(m, b) : g2)))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
mergeBy = forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g1 (forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g2 (forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @(Interp a)) Interp (Mul ('(n, a) : Union g1 g2))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
Interp (Mul ('(n, b) : Union g1 g2))
~> (Interp (Mul ('(n, b) : g1)) ** Interp (Mul ('(m, b) : g2)))
forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
(g2 ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
Interp (Mul ('(n, b) : Union g1 g2))
~> (Interp (Mul ('(n, b) : g1)) ** Interp (Mul ('(m, b) : g2)))
withRest) Interp (Mul ('(n, a) : Union g1 g2))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
Interp (Mul ('(n, b) : Union g1 g2))
~> (Interp (Mul ('(n, b) : g1)) ** Interp (Mul ('(m, b) : g2)))
forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
(g1 ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
Interp (Mul ('(n, b) : Union g1 g2))
~> (Interp (Mul ('(n, b) : g1)) ** Interp (Mul ('(m, b) : g2)))
withRest
    where
      -- When the variable is all both sides have, this is just the copy.
      withRest :: Interp (Mul ('(n, a) ': Union g1 g2)) ~> Interp (Mul ('(n, a) ': g1)) ** Interp (Mul ('(m, b) ': g2))
      withRest :: Interp (Mul ('(n, a) : Union g1 g2))
~> (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
withRest =
        forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g1
          ( forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g2
              ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a
                  ( (forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc @n @a @g1 ((Interp (Mul g1) ** Interp b) ~> Interp (Mul ('(n, b) : g1)))
-> ((Interp (Mul g2) ** Interp b) ~> Interp (Mul ('(m, b) : g2)))
-> ((Interp (Mul g1) ** Interp b) ** (Interp (Mul g2) ** Interp b))
   ~> (Interp (Mul ('(n, b) : g1)) ** Interp (Mul ('(m, b) : g2)))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc @m @a @g2)
                      (((Interp (Mul g1) ** Interp b) ** (Interp (Mul g2) ** Interp b))
 ~> (Interp (Mul ('(n, b) : g1)) ** Interp (Mul ('(m, b) : g2))))
-> (Interp (Mul ('(n, b) : Union g1 g2))
    ~> ((Interp (Mul g1) ** Interp b)
        ** (Interp (Mul g2) ** Interp b)))
-> Interp (Mul ('(n, b) : Union g1 g2))
   ~> (Interp (Mul ('(n, b) : g1)) ** Interp (Mul ('(m, b) : g2)))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
forall {k} (a :: k) (b :: k) (c :: k) (d :: k).
(SymMonoidal k, Ob a, Ob b, Ob c, Ob d) =>
((a ** b) ** (c ** d)) ~> ((a ** c) ** (b ** d))
swapInner @(Interp (Mul g1)) @(Interp (Mul g2)) @(Interp a) @(Interp a)
                      (((Interp (Mul g1) ** Interp (Mul g2)) ** (Interp b ** Interp b))
 ~> ((Interp (Mul g1) ** Interp b)
     ** (Interp (Mul g2) ** Interp b)))
-> (Interp (Mul ('(n, b) : Union g1 g2))
    ~> ((Interp (Mul g1) ** Interp (Mul g2))
        ** (Interp b ** Interp b)))
-> Interp (Mul ('(n, b) : Union g1 g2))
   ~> ((Interp (Mul g1) ** Interp b) ** (Interp (Mul g2) ** Interp b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Merge g1 g2 =>
Interp (Mul (Union g1 g2)) ~> (Interp (Mul g1) ** Interp (Mul g2))
merge @g1 @g2 (Interp (Mul (Union g1 g2))
 ~> (Interp (Mul g1) ** Interp (Mul g2)))
-> (Interp b ~> (Interp b ** Interp b))
-> (Interp (Mul (Union g1 g2)) ** Interp b)
   ~> ((Interp (Mul g1) ** Interp (Mul g2)) ** (Interp b ** Interp b))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall (c :: k). Comonoid c => c ~> (c ** c)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult @(Interp a))
                      ((Interp (Mul (Union g1 g2)) ** Interp b)
 ~> ((Interp (Mul g1) ** Interp (Mul g2))
     ** (Interp b ** Interp b)))
-> (Interp (Mul ('(n, b) : Union g1 g2))
    ~> (Interp (Mul (Union g1 g2)) ** Interp b))
-> Interp (Mul ('(n, b) : Union g1 g2))
   ~> ((Interp (Mul g1) ** Interp (Mul g2)) ** (Interp b ** Interp b))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
unsnoc @n @a @(Union g1 g2)
                  )
              )
          )

-- | The inverse of 'merge' for two contexts without a variable in common, which a @rec@ block
-- uses to put the wires it feeds back together with the others.
type Unmerge :: forall {k}. Ctx k -> Ctx k -> Constraint
class (KnownCtx g1, KnownCtx g2) => Unmerge (g1 :: Ctx k) g2 where
  unmerge :: Interp (Mul g1) ** Interp (Mul g2) ~> Interp (Mul (Union g1 g2))

instance (Monoidal k, KnownCtx g2) => Unmerge ('[] :: Ctx k) g2 where
  {-# INLINE unmerge #-}
  unmerge :: (Interp (Mul '[]) ** Interp (Mul g2))
~> Interp (Mul (Union '[] g2))
unmerge = forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @g2 (Unit ** Interp (Mul g2)) ~> Interp (Mul g2)
Ob (Interp (Mul g2)) =>
(Unit ** Interp (Mul g2)) ~> Interp (Mul g2)
forall (a :: k). Ob a => (Unit ** a) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor

instance (Monoidal k, KnownCtx ('(n, a) ': g1)) => Unmerge ('(n, a) ': g1 :: Ctx k) '[] where
  {-# INLINE unmerge #-}
  unmerge :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul '[]))
~> Interp (Mul (Union ('(n, a) : g1) '[]))
unmerge = forall (g :: [(Nat, SYN k)]) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(n, a) ': g1) (Interp (Mul ('(n, a) : g1)) ** Unit)
~> Interp (Mul ('(n, a) : g1))
Ob (Interp (Mul ('(n, a) : g1))) =>
(Interp (Mul ('(n, a) : g1)) ** Unit)
~> Interp (Mul ('(n, a) : g1))
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor

instance
  ( Monoidal k
  , KnownObj a
  , KnownObj b
  , KnownCtx g1
  , KnownCtx g2
  , UnmergeBy (CmpNat n m) ('(n, a) ': g1 :: Ctx k) ('(m, b) ': g2)
  )
  => Unmerge ('(n, a) ': g1 :: Ctx k) ('(m, b) ': g2)
  where
  {-# INLINE unmerge #-}
  unmerge :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
~> Interp (Mul (Union ('(n, a) : g1) ('(m, b) : g2)))
unmerge = forall (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
UnmergeBy o g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2))
~> Interp (Mul (UnionBy o g1 g2))
forall {k} (o :: Ordering) (g1 :: Ctx k) (g2 :: Ctx k).
UnmergeBy o g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2))
~> Interp (Mul (UnionBy o g1 g2))
unmergeBy @(CmpNat n m) @('(n, a) ': g1) @('(m, b) ': g2)

-- | 'unmerge' for two non-empty contexts, by which of the two has the larger head id.
type UnmergeBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Constraint
class (KnownCtx g1, KnownCtx g2) => UnmergeBy o (g1 :: Ctx k) g2 where
  unmergeBy :: Interp (Mul g1) ** Interp (Mul g2) ~> Interp (Mul (UnionBy o g1 g2))

instance
  ( SymMonoidal k
  , Unmerge g1 ('(m, b) ': g2)
  , KnownObj (a :: SYN k)
  , KnownObj b
  , Mul ('(n, a) ': Union g1 ('(m, b) ': g2)) ~ (Mul (Union g1 ('(m, b) ': g2)) :** a)
  )
  => UnmergeBy GT ('(n, a) ': g1) ('(m, b) ': g2)
  where
  {-# INLINE unmergeBy #-}
  unmergeBy :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
~> Interp (Mul (UnionBy 'GT ('(n, a) : g1) ('(m, b) : g2)))
unmergeBy =
    forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(m, b) ': g2)
      ( forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a
          ( forall (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g1
              (forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp a) @(Interp (Mul ('(m, b) ': g2))))
              ( (forall (g1 :: Ctx k) (g2 :: Ctx k).
Unmerge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Unmerge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
unmerge @g1 @('(m, b) ': g2) ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
 ~> Interp
      (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2))))
-> (Interp a ~> Interp a)
-> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
    ** Interp a)
   ~> (Interp
         (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
       ** Interp a)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
                  (((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
  ** Interp a)
 ~> (Interp
       (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
     ** Interp a))
-> (((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2)))
    ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
        ** Interp a))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> (Interp
         (Mul (UnionBy (CmpNat n m) ('(n, a) : g') ('(m, b) : g2)))
       ** Interp a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g')))
-> Obj (Interp (Mul ('(m, b) : g2)))
-> (Interp a ~> Interp a)
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
       ** Interp a)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2)) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a)
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
 ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
     ** Interp a))
-> (((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2)))
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> ((Interp (Mul ('(n, a) : g')) ** Interp (Mul ('(m, b) : g2)))
       ** Interp a)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1 Obj (Interp (Mul ('(n, a) : g')))
-> ((Interp a ** Interp (Mul ('(m, b) : g2)))
    ~> (Interp (Mul ('(m, b) : g2)) ** Interp a))
-> (Interp (Mul ('(n, a) : g'))
    ** (Interp a ** Interp (Mul ('(m, b) : g2))))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall k (a :: k) (b :: k).
(SymMonoidal k, Ob a, Ob b) =>
(a ** b) ~> (b ** a)
swap @k @(Interp a) @(Interp (Mul ('(m, b) ': g2))))
                  ((Interp (Mul ('(n, a) : g'))
  ** (Interp a ** Interp (Mul ('(m, b) : g2))))
 ~> (Interp (Mul ('(n, a) : g'))
     ** (Interp (Mul ('(m, b) : g2)) ** Interp a)))
-> (((Interp (Mul ('(n, a) : g')) ** Interp a)
     ** Interp (Mul ('(m, b) : g2)))
    ~> (Interp (Mul ('(n, a) : g'))
        ** (Interp a ** Interp (Mul ('(m, b) : g2)))))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp (Mul ('(m, b) : g2)) ** Interp a))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g')))
-> (Interp a ~> Interp a)
-> Obj (Interp (Mul ('(m, b) : g2)))
-> ((Interp (Mul ('(n, a) : g')) ** Interp a)
    ** Interp (Mul ('(m, b) : g2)))
   ~> (Interp (Mul ('(n, a) : g'))
       ** (Interp a ** Interp (Mul ('(m, b) : g2))))
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> ((a ** b) ** c) ~> (a ** (b ** c))
associator' (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g1) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) (forall (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': g2))
              )
          )
      )

instance
  ( Monoidal k
  , Unmerge ('(n, a) ': g1) g2
  , KnownObj a
  , KnownObj (b :: SYN k)
  , Mul ('(m, b) ': Union ('(n, a) ': g1) g2) ~ (Mul (Union ('(n, a) ': g1) g2) :** b)
  )
  => UnmergeBy LT ('(n, a) ': g1) ('(m, b) ': g2)
  where
  {-# INLINE unmergeBy #-}
  unmergeBy :: (Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(m, b) : g2)))
~> Interp (Mul (UnionBy 'LT ('(n, a) : g1) ('(m, b) : g2)))
unmergeBy =
    forall (g :: [(Nat, SYN k)]) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: [(Nat, SYN k)]).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
forall {k} (g :: Ctx k) r.
KnownCtx g =>
((g ~ '[]) => r)
-> (forall (n :: Nat) (a :: SYN k) (g' :: Ctx k).
    (g ~ ('(n, a) : g'), KnownObj a, KnownCtx g') =>
    r)
-> r
ctxCase @g2
      (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(m, b) ': '(n, a) ': g1))
      ( (forall (g1 :: [(Nat, SYN k)]) (g2 :: [(Nat, SYN k)]).
Unmerge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
forall {k} (g1 :: Ctx k) (g2 :: Ctx k).
Unmerge g1 g2 =>
(Interp (Mul g1) ** Interp (Mul g2)) ~> Interp (Mul (Union g1 g2))
unmerge @('(n, a) ': g1) @g2 ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
 ~> Interp
      (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g'))))
-> (Interp b ~> Interp b)
-> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
    ** Interp b)
   ~> (Interp
         (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
       ** Interp b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
          (((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
  ** Interp b)
 ~> (Interp
       (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
     ** Interp b))
-> ((Interp (Mul ('(n, a) : g1))
     ** (Interp (Mul ('(n, a) : g')) ** Interp b))
    ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
        ** Interp b))
-> (Interp (Mul ('(n, a) : g1))
    ** (Interp (Mul ('(n, a) : g')) ** Interp b))
   ~> (Interp
         (Mul (UnionBy (CmpNat n n) ('(n, a) : g1) ('(n, a) : g')))
       ** Interp b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. Obj (Interp (Mul ('(n, a) : g1)))
-> Obj (Interp (Mul ('(n, a) : g')))
-> (Interp b ~> Interp b)
-> (Interp (Mul ('(n, a) : g1))
    ** (Interp (Mul ('(n, a) : g')) ** Interp b))
   ~> ((Interp (Mul ('(n, a) : g1)) ** Interp (Mul ('(n, a) : g')))
       ** Interp b)
forall {k} (a :: k) (b :: k) (c :: k).
Monoidal k =>
Obj a -> Obj b -> Obj c -> (a ** (b ** c)) ~> ((a ** b) ** c)
associatorInv' (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @('(n, a) ': g1)) (forall (g :: [(Nat, SYN k)]).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @g2) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
      )

-- | Keep the variables of @g@ that @h@ has and discard the others, for an alternative of the
-- additives that does not use all the variables of the other. Every variable of @h@ must be in
-- @g@.
type Thin :: forall {k}. Ctx k -> Ctx k -> Constraint
class (KnownCtx g, KnownCtx h) => Thin (g :: Ctx k) h where
  thin :: Interp (Mul g) ~> Interp (Mul h)

instance (Monoidal k) => Thin ('[] :: Ctx k) '[] where
  {-# INLINE thin #-}
  thin :: Interp (Mul '[]) ~> Interp (Mul '[])
thin = forall (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Unit :: k)

instance (Monoidal k, Comonoid (Interp a), KnownObj (a :: SYN k), Thin g '[]) => Thin ('(n, a) ': g) '[] where
  {-# INLINE thin #-}
  thin :: Interp (Mul ('(n, a) : g)) ~> Interp (Mul '[])
thin = forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @Unit ((Unit ** Unit) ~> Unit)
-> (Interp (Mul ('(n, a) : g)) ~> (Unit ** Unit))
-> Interp (Mul ('(n, a) : g)) ~> Unit
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k) (h :: Ctx k).
Thin g h =>
Interp (Mul g) ~> Interp (Mul h)
forall {k} (g :: Ctx k) (h :: Ctx k).
Thin g h =>
Interp (Mul g) ~> Interp (Mul h)
thin @g @'[] (Interp (Mul g) ~> Unit)
-> (Interp a ~> Unit)
-> (Interp (Mul g) ** Interp a) ~> (Unit ** Unit)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @(Interp a)) ((Interp (Mul g) ** Interp a) ~> (Unit ** Unit))
-> (Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a))
-> Interp (Mul ('(n, a) : g)) ~> (Unit ** Unit)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
unsnoc @n @a @g

instance
  (KnownObj a, KnownObj b, KnownCtx g, KnownCtx h, ThinBy (CmpNat n m) ('(n, a) ': g) ('(m, b) ': h))
  => Thin ('(n, a) ': g :: Ctx k) ('(m, b) ': h)
  where
  {-# INLINE thin #-}
  thin :: Interp (Mul ('(n, a) : g)) ~> Interp (Mul ('(m, b) : h))
thin = forall (o :: Ordering) (g :: Ctx k) (h :: Ctx k).
ThinBy o g h =>
Interp (Mul g) ~> Interp (Mul h)
forall {k} (o :: Ordering) (g :: Ctx k) (h :: Ctx k).
ThinBy o g h =>
Interp (Mul g) ~> Interp (Mul h)
thinBy @(CmpNat n m) @('(n, a) ': g) @('(m, b) ': h)

-- | 'thin' for two non-empty contexts, by which of the two has the larger head id.
type ThinBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Constraint
class (KnownCtx g, KnownCtx h) => ThinBy o (g :: Ctx k) h where
  thinBy :: Interp (Mul g) ~> Interp (Mul h)

instance (Monoidal k, KnownObj (a :: SYN k), a ~ b, Thin g h) => ThinBy EQ ('(n, a) ': g) ('(m, b) ': h) where
  {-# INLINE thinBy #-}
  thinBy :: Interp (Mul ('(n, a) : g)) ~> Interp (Mul ('(m, b) : h))
thinBy = forall {k} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @a (forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc @m @a @h ((Interp (Mul h) ** Interp b) ~> Interp (Mul ('(m, b) : h)))
-> (Interp (Mul ('(n, b) : g)) ~> (Interp (Mul h) ** Interp b))
-> Interp (Mul ('(n, b) : g)) ~> Interp (Mul ('(m, b) : h))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k) (h :: Ctx k).
Thin g h =>
Interp (Mul g) ~> Interp (Mul h)
forall {k} (g :: Ctx k) (h :: Ctx k).
Thin g h =>
Interp (Mul g) ~> Interp (Mul h)
thin @g @h (Interp (Mul g) ~> Interp (Mul h))
-> (Interp b ~> Interp b)
-> (Interp (Mul g) ** Interp b) ~> (Interp (Mul h) ** Interp b)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) ((Interp (Mul g) ** Interp b) ~> (Interp (Mul h) ** Interp b))
-> (Interp (Mul ('(n, b) : g)) ~> (Interp (Mul g) ** Interp b))
-> Interp (Mul ('(n, b) : g)) ~> (Interp (Mul h) ** Interp b)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
unsnoc @n @a @g)

instance
  (Monoidal k, Comonoid (Interp a), KnownObj (a :: SYN k), KnownObj b, Thin g ('(m, b) ': h))
  => ThinBy GT ('(n, a) ': g) ('(m, b) ': h)
  where
  {-# INLINE thinBy #-}
  thinBy :: Interp (Mul ('(n, a) : g)) ~> Interp (Mul ('(m, b) : h))
thinBy =
    forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(m, b) ': h)
      ((Interp (Mul ('(m, b) : h)) ** Unit) ~> Interp (Mul ('(m, b) : h))
forall (a :: k). Ob a => (a ** Unit) ~> a
forall k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor ((Interp (Mul ('(m, b) : h)) ** Unit)
 ~> Interp (Mul ('(m, b) : h)))
-> (Interp (Mul ('(n, a) : g))
    ~> (Interp (Mul ('(m, b) : h)) ** Unit))
-> Interp (Mul ('(n, a) : g)) ~> Interp (Mul ('(m, b) : h))
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. (forall (g :: Ctx k) (h :: Ctx k).
Thin g h =>
Interp (Mul g) ~> Interp (Mul h)
forall {k} (g :: Ctx k) (h :: Ctx k).
Thin g h =>
Interp (Mul g) ~> Interp (Mul h)
thin @g @('(m, b) ': h) (Interp (Mul g) ~> Interp (Mul ('(m, b) : h)))
-> (Interp a ~> Unit)
-> (Interp (Mul g) ** Interp a)
   ~> (Interp (Mul ('(m, b) : h)) ** Unit)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
(x1 ~> x2) -> (y1 ~> y2) -> (x1 ** y1) ~> (x2 ** y2)
forall {j} {k} (p :: j +-> k) (x1 :: k) (x2 :: j) (y1 :: k)
       (y2 :: j).
MonoidalProfunctor p =>
p x1 x2 -> p y1 y2 -> p (x1 ** y1) (x2 ** y2)
M.** forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @(Interp a)) ((Interp (Mul g) ** Interp a)
 ~> (Interp (Mul ('(m, b) : h)) ** Unit))
-> (Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a))
-> Interp (Mul ('(n, a) : g))
   ~> (Interp (Mul ('(m, b) : h)) ** Unit)
forall (b :: k) (c :: k) (a :: k). (b ~> c) -> (a ~> b) -> a ~> c
forall {k} (p :: CAT k) (b :: k) (c :: k) (a :: k).
Promonad p =>
p b c -> p a b -> p a c
. forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
Interp (Mul ('(n, a) : g)) ~> (Interp (Mul g) ** Interp a)
unsnoc @n @a @g)

-- | A binder's variable @n@ on the right of @r@, what the body uses besides it, given the body's
-- context @g@: 'snoc' if the body uses the variable, and its counit otherwise. The binder's
-- variable is the newest in scope, so it can only be at the head of @g@. The functional
-- dependency, rather than a type family, gives @r@, so that a binder costs one comparison of ids.
type BindVar :: forall {k}. Nat -> SYN k -> Ctx k -> Ctx k -> Constraint
class (KnownCtx r) => BindVar n (a :: SYN k) g r | n g -> r where
  bindVar :: Interp (Mul r) ** Interp a ~> Interp (Mul g)

instance (Monoidal k, Comonoid (Interp a), KnownObj (a :: SYN k)) => BindVar n a '[] '[] where
  {-# INLINE bindVar #-}
  bindVar :: (Interp (Mul '[]) ** Interp a) ~> Interp (Mul '[])
bindVar = forall (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith @Unit (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @(Interp a))

instance (KnownCtx r, BindVarBy (CmpNat n m) n a ('(m, b) ': g) r) => BindVar n (a :: SYN k) ('(m, b) ': g) r where
  {-# INLINE bindVar #-}
  bindVar :: (Interp (Mul r) ** Interp a) ~> Interp (Mul ('(m, b) : g))
bindVar = forall (o :: Ordering) (n :: Nat) (a :: SYN k) (g :: Ctx k)
       (r :: Ctx k).
BindVarBy o n a g r =>
(Interp (Mul r) ** Interp a) ~> Interp (Mul g)
forall {k} (o :: Ordering) (n :: Nat) (a :: SYN k) (g :: Ctx k)
       (r :: Ctx k).
BindVarBy o n a g r =>
(Interp (Mul r) ** Interp a) ~> Interp (Mul g)
bindVarBy @(CmpNat n m) @n @a @('(m, b) ': g) @r

-- | 'bindVar' for a non-empty context, by whether its head is the new variable.
type BindVarBy :: forall {k}. Ordering -> Nat -> SYN k -> Ctx k -> Ctx k -> Constraint
class BindVarBy o n (a :: SYN k) g r | o n g -> r where
  bindVarBy :: Interp (Mul r) ** Interp a ~> Interp (Mul g)

instance (Monoidal k, KnownObj (a :: SYN k), a ~ b, KnownCtx g) => BindVarBy EQ n a ('(m, b) ': g) g where
  {-# INLINE bindVarBy #-}
  bindVarBy :: (Interp (Mul g) ** Interp a) ~> Interp (Mul ('(m, b) : g))
bindVarBy = forall (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k).
(Monoidal k, KnownObj a, KnownCtx g) =>
(Interp (Mul g) ** Interp a) ~> Interp (Mul ('(n, a) : g))
snoc @m @a @g

instance
  (Monoidal k, Comonoid (Interp a), KnownObj (a :: SYN k), KnownObj b, KnownCtx g)
  => BindVarBy GT n a ('(m, b) ': g) ('(m, b) ': g)
  where
  {-# INLINE bindVarBy #-}
  bindVarBy :: (Interp (Mul ('(m, b) : g)) ** Interp a)
~> Interp (Mul ('(m, b) : g))
bindVarBy =
    forall (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
forall {k} (g :: Ctx k) r.
(KnownCtx g, Monoidal k) =>
(Ob (Interp (Mul g)) => r) -> r
withCtxOb @('(m, b) ': g)
      (forall (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
forall {k} (a :: k) (b :: k).
(Monoidal k, Ob a) =>
(b ~> Unit) -> (a ** b) ~> a
rightUnitorWith @(Interp (Mul ('(m, b) ': g))) (forall (c :: k). Comonoid c => c ~> Unit
forall {k} (c :: k). Comonoid c => c ~> Unit
counit @(Interp a)))

type HeadId :: forall {k}. Ctx k -> Nat
type family HeadId g where
  HeadId ('(n, a) ': g) = n

-- | The variables of @g@ whose ids are not in @h@.
type Minus :: forall {k}. Ctx k -> Ctx k -> Ctx k
type family Minus g h where
  Minus '[] h = '[]
  Minus g '[] = g
  Minus ('(n, a) ': g) ('(m, b) ': h) = MinusBy (CmpNat n m) ('(n, a) ': g) ('(m, b) ': h)

type MinusBy :: forall {k}. Ordering -> Ctx k -> Ctx k -> Ctx k
type family MinusBy o g h where
  MinusBy GT (x ': g) h = x ': Minus g h
  MinusBy EQ (x ': g) (y ': h) = Minus g h
  MinusBy LT g (y ': h) = Minus g h

-- | The variables of @g@ whose ids are in @h@.
type Inter :: forall {k}. Ctx k -> Ctx k -> Ctx k
type Inter g h = Minus g (Minus g h)