{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Internal module of "Proarrow.Tools.SMC": patterns and binders. It exports everything, also what
-- the public module keeps hidden.
module Proarrow.Tools.SMC.Internal.Pattern where

import Data.Kind (Constraint, Type)
import GHC.TypeNats (Nat, type (+))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor)
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Category.Monoidal.Dialogue (Dialogue (..), bindDual)
import Proarrow.Core (CAT, CategoryOf (..), Hom, Profunctor (..), Promonad (..), obj)
import Prelude (type (~))

import Proarrow.Tools.SMC.Internal.Context
import Proarrow.Tools.SMC.Internal.Syntax
import Proarrow.Tools.SMC.Internal.Term

-- | Compile a function on terms to a morphism. The function receives the input through a pattern
-- (see /Patterns/), so @()@ compiles a term without inputs and a tuple takes a tensor apart.
{-# INLINE toSMC #-}
toSMC
  :: forall {k} (a :: SYN k) b t cont
   . (Monoidal k, Binds (~>) 0 '[] a b t cont)
  => (t -> cont)
  -> Interp a ~> Interp b
toSMC :: forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
toSMC = forall {k} (a :: SYN k) (b :: SYN k) t cont (p :: CAT k).
(MonoidalProfunctor p, Binds p 0 '[] a b t cont) =>
(t -> cont) -> p (Interp a) (Interp b)
forall (a :: SYN k) (b :: SYN k) t cont (p :: CAT k).
(MonoidalProfunctor p, Binds p 0 '[] a b t cont) =>
(t -> cont) -> p (Interp a) (Interp b)
proc @a @b

-- | 'toSMC' with both boundary objects embedded by 'F'. The surrounding morphism type
-- determines the input and output objects, so their type applications can be omitted.
-- Use 'toSMC' when a boundary needs other syntax, such as a function or computation type.
{-# INLINE toSMC1 #-}
toSMC1
  :: forall {k} (a :: k) b t cont
   . (Monoidal k, Binds (~>) 0 '[] (F a) (F b) t cont)
  => (t -> cont) -> a ~> b
toSMC1 :: forall {k} (a :: k) (b :: k) t cont.
(Monoidal k, Binds (~>) 0 '[] (F a) (F b) t cont) =>
(t -> cont) -> a ~> b
toSMC1 = forall {k} (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
forall (a :: SYN k) (b :: SYN k) t cont.
(Monoidal k, Binds (~>) 0 '[] a b t cont) =>
(t -> cont) -> Interp a ~> Interp b
toSMC @(F a) @(F b)

-- | Compile a function on terms to an arrow of the promonad @p@, as 'toSMC' does for the morphisms
-- of the category, which are the case @p = ('~>')@. The terms' computations are arrows of @p@,
-- lifted with '(-<)' or 'lift', and run in the order they are written; variables are values,
-- which the category's structure copies and discards. This mirrors @proc@ in Haskell's arrow
-- notation, whose @Arrows@ extension must be disabled.
{-# INLINE proc #-}
proc
  :: forall {k} (a :: SYN k) b t cont (p :: CAT k)
   . (MonoidalProfunctor p, Binds p 0 '[] a b t cont)
  => (t -> cont)
  -> p (Interp a) (Interp b)
proc :: forall {k} (a :: SYN k) (b :: SYN k) t cont (p :: CAT k).
(MonoidalProfunctor p, Binds p 0 '[] a b t cont) =>
(t -> cont) -> p (Interp a) (Interp b)
proc t -> cont
k = 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))
-> p (Unit ** Interp a) (Interp b) -> p (Interp a) (Interp b)
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (forall k (a :: k). (Monoidal k, Ob a) => a ~> (Unit ** a)
leftUnitorInv @k @(Interp a)) (forall {k} (p :: CAT k) (n :: Nat) (g :: Ctx k) (a :: SYN k)
       (b :: SYN k) t cont.
Binds p n g a b t cont =>
(t -> cont) -> p (Interp (Mul g) ** Interp a) (Interp b)
forall (p :: CAT k) (n :: Nat) (g :: Ctx k) (a :: SYN k)
       (b :: SYN k) t cont.
Binds p n g a b t cont =>
(t -> cont) -> p (Interp (Mul g) ** Interp a) (Interp b)
bound @p @0 @'[] @a @b t -> cont
k))

-- | Lift an arrow onto a term or tuple of terms, with its result embedded by 'F'.
-- The result object is inferred from the arrow. Use 'lift' for composite result syntax.
{-# INLINE liftF #-}
liftF
  :: forall {k} (a :: SYN k) b t (p :: CAT k) d
   . (Promonad p, Tuple p t a)
  => p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
liftF :: forall {k} (a :: SYN k) (b :: k) t (p :: CAT k) (d :: Nat).
(Promonad p, Tuple p t a) =>
p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
liftF p (Interp a) b
f t
t = forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k)
       (p :: CAT k).
Promonad p =>
p (Interp a) (Interp b) -> TermP p d g a -> TermP p d g b
forall (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k)
       (p :: CAT k).
Promonad p =>
p (Interp a) (Interp b) -> TermP p d g a -> TermP p d g b
lift @a @(F b) p (Interp a) b
p (Interp a) (Interp (F b))
f (forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p t
t)

infixr 0 -<

-- | Arrow application, mirroring @f -< x@ in Haskell's arrow notation.
-- This is infix 'liftF': the input may be a term or tuple, and the result is embedded by 'F'.
-- The @Arrows@ extension must be disabled, since it reserves this symbol.
{-# INLINE (-<) #-}
(-<)
  :: forall {k} (a :: SYN k) b t (p :: CAT k) d
   . (Promonad p, Tuple p t a)
  => p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
-< :: forall {k} (a :: SYN k) (b :: k) t (p :: CAT k) (d :: Nat).
(Promonad p, Tuple p t a) =>
p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
(-<) = forall {k} (a :: SYN k) (b :: k) t (p :: CAT k) (d :: Nat).
(Promonad p, Tuple p t a) =>
p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
forall (a :: SYN k) (b :: k) t (p :: CAT k) (d :: Nat).
(Promonad p, Tuple p t a) =>
p (Interp a) b -> t -> TermP p d (TupleCtx k t) (F b)
liftF @a @b

-- | The identity morphism, named as in Haskell's arrow notation.
-- An alias for 'Proarrow.Core.id'; @returnA -< x@ embeds the input by 'F'.
{-# INLINE returnA #-}
returnA :: (Promonad p, Ob a) => p a a
returnA :: forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
returnA = p a a
forall (a :: k). Ob a => p a a
forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id

-- | The shift of a positive type to a negative one: a computation that produces an @a@. A term of
-- it is a consumer of consumers of @a@, so in a category with @'Dual' a = a ~~> r@ it is the
-- continuation passing type @(a -> r) -> r@.
type Up :: forall {k}. SYN k -> SYN k
type Up a = Not (Not a)

-- | Run a computation against the rest of a block. The body is what the rest does with the value,
-- given the context @r@; it becomes a consumer of the computation, whose context @g@ joins. What
-- the binds of a computation share, the counterpart of 'bound'.
{-# INLINE runUp #-}
runUp
  :: forall {k} d g r (a :: SYN k) y
   . (Dialogue k, KnownObj a, KnownObj y, Merge g r)
  => Term d g (Up a)
  -> (Interp (Mul r) ** Interp a ~> Interp (Not y))
  -> Term d (Union g r) (Not y)
runUp :: forall {k} (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (y :: SYN k).
(Dialogue k, KnownObj a, KnownObj y, Merge g r) =>
Term d g (Up a)
-> ((Interp (Mul r) ** Interp a) ~> Interp (Not y))
-> Term d (Union g r) (Not y)
runUp (MkTerm Interp (Mul g) ~> Interp (Up a)
m) (Interp (Mul r) ** Interp a) ~> Interp (Not y)
body =
  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 @r
    ( 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} (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
forall (s :: SYN k) r. KnownObj s => (Ob (Interp s) => r) -> r
withSynOb @y
            ( (Interp (Mul (Union g r)) ~> Interp (Not y))
-> TermP (~>) d (Union g r) (Not y)
forall {k} (p :: CAT k) (g :: Ctx k) (a :: SYN k) (d :: Nat).
p (Interp (Mul g)) (Interp a) -> TermP p d g a
MkTerm
                ( forall (g :: k) (a :: k) (y :: k).
(Dialogue k, Ob g, Ob a, Ob y) =>
((g ** a) ~> Dual y) -> (Dual (Dual a) ** g) ~> Dual y
forall {k} (g :: k) (a :: k) (y :: k).
(Dialogue k, Ob g, Ob a, Ob y) =>
((g ** a) ~> Dual y) -> (Dual (Dual a) ** g) ~> Dual y
bindDual @(Interp (Mul r)) @(Interp a) @(Interp y) (Interp (Mul r) ** Interp a) ~> Dual (Interp y)
(Interp (Mul r) ** Interp a) ~> Interp (Not y)
body
                    ((Dual (Dual (Interp a)) ** Interp (Mul r)) ~> Dual (Interp y))
-> (Interp (Mul (Union g r))
    ~> (Dual (Dual (Interp a)) ** Interp (Mul r)))
-> Interp (Mul (Union g r)) ~> Dual (Interp y)
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
. (Interp (Mul g) ~> Dual (Dual (Interp a))
Interp (Mul g) ~> Interp (Up a)
m (Interp (Mul g) ~> Dual (Dual (Interp a)))
-> (Interp (Mul r) ~> Interp (Mul r))
-> (Interp (Mul g) ** Interp (Mul r))
   ~> (Dual (Dual (Interp a)) ** Interp (Mul r))
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 (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Interp (Mul r)))
                    ((Interp (Mul g) ** Interp (Mul r))
 ~> (Dual (Dual (Interp a)) ** Interp (Mul r)))
-> (Interp (Mul (Union g r)) ~> (Interp (Mul g) ** Interp (Mul r)))
-> Interp (Mul (Union g r))
   ~> (Dual (Dual (Interp a)) ** Interp (Mul r))
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 @g @r
                )
            )
        )
    )

-- | A value as the computation that produces it: double negation introduction, and the return of
-- a @do@ block in the continuation reading. It also reads as a producer of @a@ handed over as a
-- consumer of @'Not' a@. The value can be given as a 'Tuple' of terms, built by the type expected.
{-# INLINE ret #-}
ret
  :: forall {k} {p} (a :: SYN k) t d
   . (Dialogue k, Profunctor p, KnownObj a, Tuple p t a)
  => t -> TermP p d (TupleCtx k t) (Up a)
ret :: forall {k} {p :: k +-> k} (a :: SYN k) t (d :: Nat).
(Dialogue k, Profunctor p, KnownObj a, Tuple p t a) =>
t -> TermP p d (TupleCtx k t) (Up a)
ret t
t = 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 ~> Interp (Up a))
-> TermP p d (TupleCtx k t) a -> TermP p d (TupleCtx k t) (Up a)
forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (g :: Ctx k)
       (p :: CAT k).
Profunctor p =>
(Interp a ~> Interp b) -> TermP p d g a -> TermP p d g b
rmapT (forall k (a :: k). (Dialogue k, Ob a) => a ~> Dual (Dual a)
doubleNegInv @k @(Interp a)) (forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p @t @a t
t))

-- | A term built from a tuple of terms, by the type it is expected to have: a term is itself, a
-- pair at a tensor is the tensor of its parts, and a pair at a computation @'Up' a@ is the
-- computation of the pair at @a@. A tuple of three to six stands for pairs nested to the left, as in
-- patterns. The parts may come from different binding depths; the result adopts the depth
-- where it is used, and their contexts are merged.
type Tuple :: forall {k}. CAT k -> Type -> SYN k -> Constraint
class Tuple (p :: CAT k) t a where
  tuple :: t -> TermP p d (TupleCtx k t) a

-- | The context of a tuple of terms: the union of the contexts of its parts.
type TupleCtx :: forall k -> Type -> Ctx k
type family TupleCtx k t where
  TupleCtx k (x, y) = Union (TupleCtx k x) (TupleCtx k y)
  TupleCtx k (x, y, z) = TupleCtx k ((x, y), z)
  TupleCtx k (w, x, y, z) = TupleCtx k ((w, x, y), z)
  TupleCtx k (v, w, x, y, z) = TupleCtx k ((v, w, x, y), z)
  TupleCtx k (u, v, w, x, y, z) = TupleCtx k ((u, v, w, x, y), z)
  TupleCtx k t = CtxOf @k t

-- The generic instances are incoherent, as for patterns: a term's type is often still unknown when
-- the instance is chosen, and a pair defaults to a tensor until its type is known to be an 'Up'.

-- | A term keeps its context and type, adapting to the depth where it is used.
-- Variable ids in the context are unchanged.
instance {-# INCOHERENT #-} (t ~ TermP p d g a) => Tuple p t a where
  {-# INLINE tuple #-}
  tuple :: forall (d :: Nat). t -> TermP p d (TupleCtx k t) a
tuple t
t = TermP p d g a -> TermP p d g a
forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (d' :: Nat)
       (g :: Ctx k) (p :: CAT k).
(Interp a ~ Interp b) =>
TermP p d g a -> TermP p d' g b
recast t
TermP p d g a
t

-- | A pair at a tensor is the tensor of its parts.
instance
  {-# INCOHERENT #-}
  ( MonoidalProfunctor p
  , a ~ (a1 :** a2)
  , Tuple p x a1
  , Tuple p y a2
  , Merge (TupleCtx k x) (TupleCtx k y)
  )
  => Tuple p (x, y) (a :: SYN k)
  where
  {-# INLINE tuple #-}
  tuple :: forall (d :: Nat). (x, y) -> TermP p d (TupleCtx k (x, y)) a
tuple (x
x, y
y) = forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: k +-> k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p @x @a1 x
x TermP p d (TupleCtx k x) a1
-> TermP p d (TupleCtx k y) a2
-> TermP p d (Union (TupleCtx k x) (TupleCtx k y)) (a1 :** a2)
forall {k} (d :: Nat) (g1 :: Ctx k) (g2 :: Ctx k) (a :: SYN k)
       (b :: SYN k) (p :: CAT k).
(MonoidalProfunctor p, Merge g1 g2) =>
TermP p d g1 a
-> TermP p d g2 b -> TermP p d (Union g1 g2) (a :** b)
** forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: k +-> k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p @y @a2 y
y

-- | A pair at a computation is the computation of the pair at the value.
instance (Dialogue k, Profunctor p, KnownObj a, Tuple p (x, y) a) => Tuple p (x, y) (Not (Not a) :: SYN k) where
  {-# INLINE tuple #-}
  tuple :: forall (d :: Nat).
(x, y) -> TermP p d (TupleCtx k (x, y)) (Not (Not a))
tuple (x, y)
p = forall {k} {p :: k +-> k} (a :: SYN k) t (d :: Nat).
(Dialogue k, Profunctor p, KnownObj a, Tuple p t a) =>
t -> TermP p d (TupleCtx k t) (Up a)
forall (a :: SYN k) t (d :: Nat).
(Dialogue k, Profunctor p, KnownObj a, Tuple p t a) =>
t -> TermP p d (TupleCtx k t) (Up a)
ret @a (x, y)
p

instance (Tuple p ((x, y), z) a) => Tuple p (x, y, z) a where
  {-# INLINE tuple #-}
  tuple :: forall (d :: Nat). (x, y, z) -> TermP p d (TupleCtx k (x, y, z)) a
tuple (x
x, y
y, z
z) = forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p @((x, y), z) @a ((x
x, y
y), z
z)

instance (Tuple p ((w, x, y), z) a) => Tuple p (w, x, y, z) a where
  {-# INLINE tuple #-}
  tuple :: forall (d :: Nat).
(w, x, y, z) -> TermP p d (TupleCtx k (w, x, y, z)) a
tuple (w
w, x
x, y
y, z
z) = forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p @((w, x, y), z) @a ((w
w, x
x, y
y), z
z)

instance (Tuple p ((v, w, x, y), z) a) => Tuple p (v, w, x, y, z) a where
  {-# INLINE tuple #-}
  tuple :: forall (d :: Nat).
(v, w, x, y, z) -> TermP p d (TupleCtx k (v, w, x, y, z)) a
tuple (v
v, w
w, x
x, y
y, z
z) = forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p @((v, w, x, y), z) @a ((v
v, w
w, x
x, y
y), z
z)

instance (Tuple p ((u, v, w, x, y), z) a) => Tuple p (u, v, w, x, y, z) a where
  {-# INLINE tuple #-}
  tuple :: forall (d :: Nat).
(u, v, w, x, y, z) -> TermP p d (TupleCtx k (u, v, w, x, y, z)) a
tuple (u
u, v
v, w
w, x
x, y
y, z
z) = forall {k} (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
forall (p :: CAT k) t (a :: SYN k) (d :: Nat).
Tuple p t a =>
t -> TermP p d (TupleCtx k t) a
tuple @p @((u, v, w, x, y), z) @a ((u
u, v
v, w
w, x
x, y
y), z
z)

-- | The pattern @t@ of a binder: it takes apart the variable @(n, a)@, and the binder's body
-- @cont@ then gives a term at depth @n + 1@ with type @b@, whose context is @g@ and possibly that
-- variable. Both the variable's type and the rest of the context must be known.
type Binds :: forall {k}. CAT k -> Nat -> Ctx k -> SYN k -> SYN k -> Type -> Type -> Constraint
class (KnownObj a, KnownCtx g) => Binds p n g (a :: SYN k) b t cont where
  -- | The body of a binder, with the pattern taking apart its new variable, as a morphism from the
  -- context around it and the variable. This is what 'toSMC', 'Proarrow.Tools.SMC.lam',
  -- 'Proarrow.Tools.SMC.loop', 'Proarrow.Tools.SMC.cont', 'Proarrow.Tools.SMC.caseOf',
  -- 'Proarrow.Tools.SMC.sumOver' and the binds of @do@ notation share.
  bound :: (t -> cont) -> p (Interp (Mul g) ** Interp a) (Interp b)

-- The context of the body is @g'@, which only the instance needs to name.
instance
  ( Promonad p
  , KnownObj a
  , KnownCtx g
  , BindPat p (TermP p (n + 1) '[ '(n, a)] a) t cont (TermP p (n + 1) g' b)
  , BindVar n a g' g
  )
  => Binds p n g (a :: SYN k) b t cont
  where
  {-# INLINE bound #-}
  bound :: (t -> cont) -> p (Interp (Mul g) ** Interp a) (Interp b)
bound t -> cont
k =
    case forall {k} (p :: CAT k) m t cont r.
BindPat p m t cont r =>
m -> (t -> cont) -> r
forall (p :: CAT k) m t cont r.
BindPat p m t cont r =>
m -> (t -> cont) -> r
bindPat @p @(TermP p (n + 1) '[ '(n, a)] a) @t @cont @(TermP p (n + 1) g' b) (forall (n :: Nat) (a :: SYN k) (d :: Nat) (p :: CAT k).
(Promonad p, KnownObj a) =>
TermP p d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat) (p :: CAT k).
(Promonad p, KnownObj a) =>
TermP p d '[ '(n, a)] a
var @n @a @(n + 1) @p) t -> cont
k of
      MkTerm p (Interp (Mul g')) (Interp b)
body -> ((Interp (Mul g) ** Interp a) ~> Interp (Mul g'))
-> p (Interp (Mul g')) (Interp b)
-> p (Interp (Mul g) ** Interp a) (Interp b)
forall (c :: k) (a :: k) (b :: k). (c ~> a) -> p a b -> p c b
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j).
Profunctor p =>
(c ~> a) -> p a b -> p c b
lmap (forall (n :: Nat) (a :: SYN k) (g :: Ctx k) (r :: Ctx k).
BindVar n a g r =>
(Interp (Mul r) ** Interp a) ~> Interp (Mul g)
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k) (r :: Ctx k).
BindVar n a g r =>
(Interp (Mul r) ** Interp a) ~> Interp (Mul g)
bindVar @n @a @g' @g) p (Interp (Mul g')) (Interp b)
body

-- | A term on the right hand side taken apart by the pattern of the continuation. The types of the
-- continuation and the result are matched with equalities, so that the instance is chosen as soon
-- as the right hand side is known.
type BindPat :: forall {k}. CAT k -> Type -> Type -> Type -> Type -> Constraint
class BindPat p m t cont r | m -> p where
  bindPat :: m -> (t -> cont) -> r

instance
  ( cont ~ TermP p (d + PSize t) (CtxOf @k cont) (TyOf @k cont)
  , r ~ TermP p d gr (TyOf @k cont)
  , Pat p t d g a (CtxOf @k cont) (TyOf @k cont) gr
  )
  => BindPat p (TermP p d g (a :: SYN k)) t cont r
  where
  {-# INLINE bindPat #-}
  bindPat :: TermP p d g a -> (t -> cont) -> r
bindPat = forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @t @d @g @a @(CtxOf @k cont) @(TyOf @k cont) @gr

-- | A pattern: a variable, @()@, or a pair of patterns. A tuple of three to six stands for pairs
-- nested to the left, as @a ':**' b ':**' c@ is: @(x, y, z)@ is @((x, y), z)@. Binding it at depth
-- @d@ to a term with context @g@ and type @a@, with a continuation with context @g'@ and type @c@,
-- gives a term with context @gr@, which each instance fixes. A pair or @()@ at a computation,
-- @'Up' a@, runs it and matches its value, so @c@ is then negative.
type Pat :: forall {k}. CAT k -> Type -> Nat -> Ctx k -> SYN k -> Ctx k -> SYN k -> Ctx k -> Constraint
class Pat p t d g a g' c gr where
  pat :: TermP p d g a -> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c

-- | The number of variables a pattern binds on the way, and so the depth it adds.
type PSize :: Type -> Nat
type family PSize t where
  PSize (x, y) = 2 + PSize x + PSize y
  PSize (x, y, z) = PSize ((x, y), z)
  PSize (w, x, y, z) = PSize ((w, x, y), z)
  PSize (v, w, x, y, z) = PSize ((v, w, x, y), z)
  PSize (u, v, w, x, y, z) = PSize ((u, v, w, x, y), z)
  PSize t = 0

-- The generic instances are incoherent: a variable pattern's type is often still unknown when the
-- instance is chosen, and a pair pattern's type is always a pair by then. The instances at a
-- computation are more specific, so they win once the type is known to be an 'Up'.

-- | The pattern @()@ at a computation of the unit runs it.
instance
  (p ~ Hom k, Dialogue k, KnownObj y, c ~ Not y, Merge g g', gr ~ Union g g')
  => Pat p () d g (Not (Not I) :: SYN k) g' c gr
  where
  {-# INLINE pat #-}
  pat :: TermP p d g (Not (Not I))
-> (() -> TermP p (d + PSize ()) g' c) -> TermP p d gr c
pat TermP p d g (Not (Not I))
u () -> TermP p (d + PSize ()) g' c
k = case () -> TermP p (d + PSize ()) g' c
k () of
    MkTerm p (Interp (Mul g')) (Interp c)
t -> forall (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (y :: SYN k).
(Dialogue k, KnownObj a, KnownObj y, Merge g r) =>
Term d g (Up a)
-> ((Interp (Mul r) ** Interp a) ~> Interp (Not y))
-> Term d (Union g r) (Not y)
forall {k} (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (y :: SYN k).
(Dialogue k, KnownObj a, KnownObj y, Merge g r) =>
Term d g (Up a)
-> ((Interp (Mul r) ** Interp a) ~> Interp (Not y))
-> Term d (Union g r) (Not y)
runUp @d @g @g' @I @y TermP p d g (Not (Not I))
Term d g (Not (Not I))
u (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' (p (Interp (Mul g')) (Dual (Interp y))
p (Interp (Mul g')) (Interp c)
t p (Interp (Mul g')) (Dual (Interp y))
-> p (Interp (Mul g') ** Unit) (Interp (Mul g'))
-> p (Interp (Mul g') ** Unit) (Dual (Interp y))
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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 k (a :: k). (Monoidal k, Ob a) => (a ** Unit) ~> a
rightUnitor @k @(Interp (Mul g'))))

-- | A pair pattern at a computation runs it and takes its value apart. The value needs no variable
-- of its own: the pattern's variables take the ids it would have taken.
instance
  ( p ~ Hom k
  , Dialogue k
  , KnownObj a
  , KnownObj y
  , c ~ Not y
  , Pat p (x, y') d '[ '(d, a)] a g' c gp
  , BindVar d a gp r
  , Merge g r
  , gr ~ Union g r
  )
  => Pat p (x, y') d g (Not (Not a) :: SYN k) g' c gr
  where
  {-# INLINE pat #-}
  pat :: TermP p d g (Not (Not a))
-> ((x, y') -> TermP p (d + PSize (x, y')) g' c) -> TermP p d gr c
pat TermP p d g (Not (Not a))
m (x, y') -> TermP p (d + PSize (x, y')) g' c
k = case forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @(x, y') @d @'[ '(d, a)] @a @g' @c @gp (forall (n :: Nat) (a :: SYN k) (d :: Nat) (p :: CAT k).
(Promonad p, KnownObj a) =>
TermP p d '[ '(n, a)] a
forall {k} (n :: Nat) (a :: SYN k) (d :: Nat) (p :: CAT k).
(Promonad p, KnownObj a) =>
TermP p d '[ '(n, a)] a
var @d @a @d) (x, y') -> TermP p (d + PSize (x, y')) g' c
k of
    MkTerm p (Interp (Mul gp)) (Interp c)
body -> forall (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (y :: SYN k).
(Dialogue k, KnownObj a, KnownObj y, Merge g r) =>
Term d g (Up a)
-> ((Interp (Mul r) ** Interp a) ~> Interp (Not y))
-> Term d (Union g r) (Not y)
forall {k} (d :: Nat) (g :: Ctx k) (r :: Ctx k) (a :: SYN k)
       (y :: SYN k).
(Dialogue k, KnownObj a, KnownObj y, Merge g r) =>
Term d g (Up a)
-> ((Interp (Mul r) ** Interp a) ~> Interp (Not y))
-> Term d (Union g r) (Not y)
runUp @d @g @r @a @y TermP p d g (Not (Not a))
Term d g (Not (Not a))
m (p (Interp (Mul gp)) (Dual (Interp y))
p (Interp (Mul gp)) (Interp c)
body p (Interp (Mul gp)) (Dual (Interp y))
-> p (Interp (Mul r) ** Interp a) (Interp (Mul gp))
-> p (Interp (Mul r) ** Interp a) (Dual (Interp y))
forall (b :: k) (c :: k) (a :: k). p b c -> p a b -> p 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) (r :: Ctx k).
BindVar n a g r =>
(Interp (Mul r) ** Interp a) ~> Interp (Mul g)
forall {k} (n :: Nat) (a :: SYN k) (g :: Ctx k) (r :: Ctx k).
BindVar n a g r =>
(Interp (Mul r) ** Interp a) ~> Interp (Mul g)
bindVar @d @a @gp @r)

-- | The pattern @()@ uses up a term of the unit type.
instance
  {-# INCOHERENT #-}
  (MonoidalProfunctor p, a ~ I, KnownObj c, Merge g g', gr ~ Union g g')
  => Pat p () d g (a :: SYN k) g' c gr
  where
  {-# INLINE pat #-}
  pat :: TermP p d g a
-> (() -> TermP p (d + PSize ()) g' c) -> TermP p d gr c
pat (MkTerm p (Interp (Mul g)) (Interp a)
u) () -> TermP p (d + PSize ()) g' c
k = case () -> TermP p (d + PSize ()) g' c
k () of
    MkTerm p (Interp (Mul g')) (Interp c)
t -> 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 @c (p (Interp (Mul gr)) (Interp c) -> TermP p d gr c
forall {k} (p :: CAT k) (g :: Ctx k) (a :: SYN k) (d :: Nat).
p (Interp (Mul g)) (Interp a) -> TermP p d g a
MkTerm ((Interp (Mul gr) ~> (Interp (Mul g) ** Interp (Mul g')))
-> ((Unit ** Interp c) ~> Interp c)
-> p (Interp (Mul g) ** Interp (Mul g')) (Unit ** Interp c)
-> p (Interp (Mul gr)) (Interp c)
forall (c :: k) (a :: k) (b :: k) (d :: k).
(c ~> a) -> (b ~> d) -> p a b -> p c d
forall {j} {k} (p :: j +-> k) (c :: k) (a :: k) (b :: j) (d :: j).
Profunctor p =>
(c ~> a) -> (b ~> d) -> p a b -> p c d
dimap (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 @g @g') (forall k (a :: k). (Monoidal k, Ob a) => (Unit ** a) ~> a
leftUnitor @k @(Interp c)) (p (Interp (Mul g)) Unit
p (Interp (Mul g)) (Interp a)
u p (Interp (Mul g)) Unit
-> p (Interp (Mul g')) (Interp c)
-> p (Interp (Mul g) ** Interp (Mul g')) (Unit ** Interp c)
forall (x1 :: k) (x2 :: k) (y1 :: k) (y2 :: k).
p x1 x2 -> p y1 y2 -> p (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.** p (Interp (Mul g')) (Interp c)
t)))

-- | A variable pattern names the right hand side, which is always a variable. If the body does not
-- use it, the binder discards it.
instance {-# INCOHERENT #-} (t ~ TermP p (DepthOf t) g a, gr ~ g') => Pat p t d g a g' c gr where
  {-# INLINE pat #-}
  pat :: TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat TermP p d g a
x t -> TermP p (d + PSize t) g' c
k = t -> TermP p (d + PSize t) g' c
k (TermP p d g a -> TermP p (DepthOf t) g a
forall {k} (a :: SYN k) (b :: SYN k) (d :: Nat) (d' :: Nat)
       (g :: Ctx k) (p :: CAT k).
(Interp a ~ Interp b) =>
TermP p d g a -> TermP p d' g b
recast TermP p d g a
x)

-- | A pair pattern at an embedded tensor exposes its two embedded components.
-- The tensor pattern supplies the binding and context operations.
instance
  ( a ~ (a1 ** a2)
  , Pat p (x, y) d g (F a1 :** F a2) g' c gr
  )
  => Pat p (x, y) d g (F (a :: k)) g' c gr
  where
  {-# INLINE pat #-}
  pat :: TermP p d g (F a)
-> ((x, y) -> TermP p (d + PSize (x, y)) g' c) -> TermP p d gr c
pat (MkTerm p (Interp (Mul g)) (Interp (F a))
f) (x, y) -> TermP p (d + PSize (x, y)) g' c
k = forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @(x, y) @d @g @(F a1 :** F a2) (p (Interp (Mul g)) (Interp (F a1 :** F a2))
-> TermP p d g (F a1 :** F a2)
forall {k} (p :: CAT k) (g :: Ctx k) (a :: SYN k) (d :: Nat).
p (Interp (Mul g)) (Interp a) -> TermP p d g a
MkTerm p (Interp (Mul g)) (Interp (F a1 :** F a2))
p (Interp (Mul g)) (Interp (F a))
f) (x, y) -> TermP p (d + PSize (x, y)) g' c
k

instance
  {-# INCOHERENT #-}
  ( Promonad p
  , MonoidalProfunctor p
  , a ~ (a1 :** a2)
  , KnownObj a1
  , KnownObj a2
  , Pat p y (d + 2 + PSize x) '[ '(d + 1, a2)] a2 g' c gy
  , Pat p x (d + 2) '[ '(d, a1)] a1 gy c gxy
  , d + 2 + PSize x + PSize y ~ d + PSize (x, y)
  , BindVar (d + 1) a2 gxy r1
  , BindVar d a1 r1 r
  , Merge r g
  , gr ~ Union r g
  )
  => Pat p (x, y) d g (a :: SYN k) g' c gr
  where
  {-# INLINE pat #-}
  pat :: TermP p d g a
-> ((x, y) -> TermP p (d + PSize (x, y)) g' c) -> TermP p d gr c
pat TermP p d g a
s (x, y) -> TermP p (d + PSize (x, y)) g' c
k =
    forall (d :: Nat) (g :: Ctx k) (g' :: Ctx k) (r1 :: Ctx k)
       (r :: Ctx k) (a :: SYN k) (b :: SYN k) (c :: SYN k) (da :: Nat)
       (db :: Nat) (p :: CAT k).
(Promonad p, MonoidalProfunctor p, KnownObj a, KnownObj b,
 BindVar (d + 1) b g' r1, BindVar d a r1 r, Merge r g) =>
TermP p d g (a :** b)
-> (TermP p da '[ '(d, a)] a
    -> TermP p db '[ '(d + 1, b)] b -> TermP p (d + 2) g' c)
-> TermP p d (Union r g) c
forall {k} (d :: Nat) (g :: Ctx k) (g' :: Ctx k) (r1 :: Ctx k)
       (r :: Ctx k) (a :: SYN k) (b :: SYN k) (c :: SYN k) (da :: Nat)
       (db :: Nat) (p :: CAT k).
(Promonad p, MonoidalProfunctor p, KnownObj a, KnownObj b,
 BindVar (d + 1) b g' r1, BindVar d a r1 r, Merge r g) =>
TermP p d g (a :** b)
-> (TermP p da '[ '(d, a)] a
    -> TermP p db '[ '(d + 1, b)] b -> TermP p (d + 2) g' c)
-> TermP p d (Union r g) c
split @d @g @gxy @r1 @r
      TermP p d g a
TermP p d g (a1 :** a2)
s
      ( \TermP p (d + 2) '[ '(d, a1)] a1
a TermP p ((d + 2) + PSize x) '[ '(d + 1, a2)] a2
b ->
          forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @x @(d + 2) @'[ '(d, a1)] @a1 @gy @c @gxy
            TermP p (d + 2) '[ '(d, a1)] a1
a
            (\x
px -> forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @y @(d + 2 + PSize x) @'[ '(d + 1, a2)] @a2 @g' @c @gy TermP p ((d + 2) + PSize x) '[ '(d + 1, a2)] a2
b (\y
py -> (x, y) -> TermP p (d + PSize (x, y)) g' c
k (x
px, y
py)))
      )

instance {-# INCOHERENT #-} (Pat p ((x, y), z) d g a g' c gr) => Pat p (x, y, z) d g a g' c gr where
  {-# INLINE pat #-}
  pat :: TermP p d g a
-> ((x, y, z) -> TermP p (d + PSize (x, y, z)) g' c)
-> TermP p d gr c
pat TermP p d g a
s (x, y, z) -> TermP p (d + PSize (x, y, z)) g' c
k = forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @((x, y), z) @d @g @a @g' @c @gr TermP p d g a
s (\((x
px, y
py), z
pz) -> (x, y, z) -> TermP p (d + PSize (x, y, z)) g' c
k (x
px, y
py, z
pz))

instance {-# INCOHERENT #-} (Pat p ((w, x, y), z) d g a g' c gr) => Pat p (w, x, y, z) d g a g' c gr where
  {-# INLINE pat #-}
  pat :: TermP p d g a
-> ((w, x, y, z) -> TermP p (d + PSize (w, x, y, z)) g' c)
-> TermP p d gr c
pat TermP p d g a
s (w, x, y, z) -> TermP p (d + PSize (w, x, y, z)) g' c
k = forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @((w, x, y), z) @d @g @a @g' @c @gr TermP p d g a
s (\((w
pw, x
px, y
py), z
pz) -> (w, x, y, z) -> TermP p (d + PSize (w, x, y, z)) g' c
k (w
pw, x
px, y
py, z
pz))

instance {-# INCOHERENT #-} (Pat p ((v, w, x, y), z) d g a g' c gr) => Pat p (v, w, x, y, z) d g a g' c gr where
  {-# INLINE pat #-}
  pat :: TermP p d g a
-> ((v, w, x, y, z) -> TermP p (d + PSize (v, w, x, y, z)) g' c)
-> TermP p d gr c
pat TermP p d g a
s (v, w, x, y, z) -> TermP p (d + PSize (v, w, x, y, z)) g' c
k = forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @((v, w, x, y), z) @d @g @a @g' @c @gr TermP p d g a
s (\((v
pv, w
pw, x
px, y
py), z
pz) -> (v, w, x, y, z) -> TermP p (d + PSize (v, w, x, y, z)) g' c
k (v
pv, w
pw, x
px, y
py, z
pz))

instance
  {-# INCOHERENT #-}
  (Pat p ((u, v, w, x, y), z) d g a g' c gr)
  => Pat p (u, v, w, x, y, z) d g a g' c gr
  where
  {-# INLINE pat #-}
  pat :: TermP p d g a
-> ((u, v, w, x, y, z)
    -> TermP p (d + PSize (u, v, w, x, y, z)) g' c)
-> TermP p d gr c
pat TermP p d g a
s (u, v, w, x, y, z) -> TermP p (d + PSize (u, v, w, x, y, z)) g' c
k =
    forall {k} (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
forall (p :: CAT k) t (d :: Nat) (g :: Ctx k) (a :: SYN k)
       (g' :: Ctx k) (c :: SYN k) (gr :: Ctx k).
Pat p t d g a g' c gr =>
TermP p d g a
-> (t -> TermP p (d + PSize t) g' c) -> TermP p d gr c
pat @p @((u, v, w, x, y), z) @d @g @a @g' @c @gr
      TermP p d g a
s
      (\((u
pu, v
pv, w
pw, x
px, y
py), z
pz) -> (u, v, w, x, y, z) -> TermP p (d + PSize (u, v, w, x, y, z)) g' c
k (u
pu, v
pv, w
pw, x
px, y
py, z
pz))