{-# LANGUAGE AllowAmbiguousTypes #-}

-- | Internal module of "Proarrow.Tools.SMC": terms and the operations that need no binder. It
-- exports everything, also what the public module keeps hidden.
module Proarrow.Tools.SMC.Internal.Term where

import Data.Kind (Type)
import GHC.TypeNats (Nat, type (+))
import Proarrow.Category.Monoidal (Monoidal (..), MonoidalProfunctor (one), associatorInv')
import Proarrow.Category.Monoidal qualified as M
import Proarrow.Core (CAT, CategoryOf (..), Profunctor (..), Promonad (..), obj)
import Proarrow.Monoid (Comonoid (..))
import Prelude (type (~))

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

infixl 7 **

-- | A term at binding depth @d@ with context @g@ and type @a@, whose computations are arrows of
-- the promonad @p@: an arrow of @p@ from the tensor of the context to @a@. Variables and the
-- structure of contexts are morphisms of the category @k@, which @p@ takes in with 'lmap' and
-- 'rmap'. At @p = ('~>')@ this is 'Term'.
type TermP :: forall {k}. CAT k -> Nat -> Ctx k -> SYN k -> Type
data TermP p d g a where
  MkTerm :: p (Interp (Mul g)) (Interp a) -> TermP p d g a

-- | A term whose computations are the morphisms of the category itself.
type Term :: forall {k}. Nat -> Ctx k -> SYN k -> Type
type Term d g a = TermP (~>) d g a

-- | The variable with id @n@: the identity on its type.
{-# INLINE var #-}
var :: forall {k} n (a :: SYN k) d (p :: CAT k). (Promonad p, KnownObj a) => TermP p d '[ '(n, a)] a
var :: forall {k} (n :: Nat) (a :: SYN k) (d :: Nat) (p :: CAT k).
(Promonad p, KnownObj a) =>
TermP p d '[ '(n, a)] a
var = 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 (p (Interp (Mul '[ '(n, a)])) (Interp a) -> TermP p d '[ '(n, a)] a
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 {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id @p @(Interp a)))

-- | Copy a term whose type is a comonoid: @(x1, x2) <- dup x@. Using a variable twice copies it too,
-- but needs a 'Proarrow.Monoid.CocommutativeComonoid'; 'dup' needs only a 'Comonoid', and its two copies come out
-- in the order of 'comult'.
{-# INLINE dup #-}
dup :: forall {k} (s :: SYN k) d g p. (Profunctor p, Comonoid (Interp s)) => TermP p d g s -> TermP p d g (s :** s)
dup :: forall {k} (s :: SYN k) (d :: Nat) (g :: Ctx k) (p :: k +-> k).
(Profunctor p, Comonoid (Interp s)) =>
TermP p d g s -> TermP p d g (s :** s)
dup = 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
forall (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 @s @(s :** s) Interp s ~> (Interp s ** Interp s)
Interp s ~> Interp (s :** s)
forall {k} (c :: k). Comonoid c => c ~> (c ** c)
comult

-- | Discard a term whose type is a comonoid: @() <- drop t@. A variable that is not used is
-- discarded without it.
{-# INLINE drop #-}
drop :: forall {k} (s :: SYN k) d g p. (Profunctor p, Comonoid (Interp s)) => TermP p d g s -> TermP p d g I
drop :: forall {k} (s :: SYN k) (d :: Nat) (g :: Ctx k) (p :: k +-> k).
(Profunctor p, Comonoid (Interp s)) =>
TermP p d g s -> TermP p d g I
drop = 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
forall (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 @s @I Interp s ~> Unit
Interp s ~> Interp I
forall {k} (c :: k). Comonoid c => c ~> Unit
counit

-- | Lift an arrow of the promonad to a function on terms: it runs after the term.
{-# INLINE lift #-}
lift
  :: forall {k} (a :: SYN k) b d g (p :: CAT k)
   . (Promonad p) => p (Interp a) (Interp b) -> TermP p d g a -> TermP p d g b
lift :: 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
lift p (Interp a) (Interp b)
f (MkTerm p (Interp (Mul g)) (Interp a)
t) = p (Interp (Mul g)) (Interp b) -> TermP p d g b
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 a) (Interp b)
f p (Interp a) (Interp b)
-> p (Interp (Mul g)) (Interp a) -> p (Interp (Mul g)) (Interp b)
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
. p (Interp (Mul g)) (Interp a)
t)

-- | Lift a morphism of the category to a function on terms, with 'rmap'. For @p = ('~>')@ this is
-- 'lift'; for other promonads it is how the structure of @k@ acts on terms.
{-# INLINE rmapT #-}
rmapT
  :: forall {k} (a :: SYN k) b d g (p :: CAT k)
   . (Profunctor p) => (Interp a ~> Interp b) -> TermP p d g a -> TermP p d g b
rmapT :: 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 Interp a ~> Interp b
f (MkTerm p (Interp (Mul g)) (Interp a)
t) = p (Interp (Mul g)) (Interp b) -> TermP p d g b
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 a ~> Interp b)
-> p (Interp (Mul g)) (Interp a) -> p (Interp (Mul g)) (Interp b)
forall (b :: k) (d :: k) (a :: k). (b ~> d) -> p a b -> p a d
forall {j} {k} (p :: j +-> k) (b :: j) (d :: j) (a :: k).
Profunctor p =>
(b ~> d) -> p a b -> p a d
rmap Interp a ~> Interp b
f p (Interp (Mul g)) (Interp a)
t)

-- | Two terms side by side. A variable both use is copied. With effects, the left term's run
-- first.
{-# INLINE (**) #-}
(**)
  :: forall {k} d g1 g2 (a :: SYN k) b (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)
MkTerm p (Interp (Mul g1)) (Interp a)
f ** :: 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)
** MkTerm p (Interp (Mul g2)) (Interp b)
g = p (Interp (Mul (Union g1 g2))) (Interp (a :** b))
-> TermP p d (Union g1 g2) (a :** b)
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 (Union g1 g2))
 ~> (Interp (Mul g1) ** Interp (Mul g2)))
-> p (Interp (Mul g1) ** Interp (Mul g2)) (Interp a ** Interp b)
-> p (Interp (Mul (Union g1 g2))) (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 (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) (p (Interp (Mul g1)) (Interp a)
f p (Interp (Mul g1)) (Interp a)
-> p (Interp (Mul g2)) (Interp b)
-> p (Interp (Mul g1) ** Interp (Mul g2)) (Interp a ** Interp b)
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 g2)) (Interp b)
g))

-- | Two new variables @n@ and @n + 1@, of types @a@ and @b@, for the body of a 'split' whose
-- context is @g'@: the tensor @a ':**' b@, given from the context @g@, next to @r@, what the body
-- uses besides them.
{-# INLINE push2 #-}
push2
  :: forall {k} n (a :: SYN k) b g' r1 r g (p :: CAT k)
   . (Promonad p, MonoidalProfunctor p, KnownObj a, KnownObj b, BindVar (n + 1) b g' r1, BindVar n a r1 r, Merge r g)
  => p (Interp (Mul g)) (Interp a ** Interp b)
  -> p (Interp (Mul (Union r g))) (Interp (Mul g'))
push2 :: forall {k} (n :: Nat) (a :: SYN k) (b :: SYN k) (g' :: Ctx k)
       (r1 :: Ctx k) (r :: Ctx k) (g :: Ctx k) (p :: CAT k).
(Promonad p, MonoidalProfunctor p, KnownObj a, KnownObj b,
 BindVar (n + 1) b g' r1, BindVar n a r1 r, Merge r g) =>
p (Interp (Mul g)) (Interp a ** Interp b)
-> p (Interp (Mul (Union r g))) (Interp (Mul g'))
push2 p (Interp (Mul g)) (Interp a ** Interp b)
t =
  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 @b
        ( (Interp (Mul (Union r g)) ~> (Interp (Mul r) ** Interp (Mul g)))
-> ((Interp (Mul r) ** (Interp a ** Interp b)) ~> Interp (Mul g'))
-> p (Interp (Mul r) ** Interp (Mul g))
     (Interp (Mul r) ** (Interp a ** Interp b))
-> p (Interp (Mul (Union r g))) (Interp (Mul g'))
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 @r @g)
            ( 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 + 1) @b @g' @r1
                ((Interp (Mul r1) ** Interp b) ~> Interp (Mul g'))
-> ((Interp (Mul r) ** (Interp a ** Interp b))
    ~> (Interp (Mul r1) ** Interp b))
-> (Interp (Mul r) ** (Interp a ** Interp b)) ~> Interp (Mul g')
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) (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 @r1 @r ((Interp (Mul r) ** Interp a) ~> Interp (Mul r1))
-> (Interp b ~> Interp b)
-> ((Interp (Mul r) ** Interp a) ** Interp b)
   ~> (Interp (Mul r1) ** 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 (a :: k). (CategoryOf k, Ob a) => Obj a
forall {k} (a :: k). (CategoryOf k, Ob a) => Obj a
obj @(Interp b))
                (((Interp (Mul r) ** Interp a) ** Interp b)
 ~> (Interp (Mul r1) ** Interp b))
-> ((Interp (Mul r) ** (Interp a ** Interp b))
    ~> ((Interp (Mul r) ** Interp a) ** Interp b))
-> (Interp (Mul r) ** (Interp a ** Interp b))
   ~> (Interp (Mul r1) ** 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 r))
-> Obj (Interp a)
-> (Interp b ~> Interp b)
-> (Interp (Mul r) ** (Interp a ** Interp b))
   ~> ((Interp (Mul r) ** Interp a) ** 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 :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
forall {k} (g :: Ctx k).
(Monoidal k, KnownCtx g) =>
Obj (Interp (Mul g))
ctxOb @r) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @a) (forall {k} (s :: SYN k). KnownObj s => Obj (Interp s)
forall (s :: SYN k). KnownObj s => Obj (Interp s)
synOb @b)
            )
            (forall {k} (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
forall (p :: CAT k) (a :: k). (Promonad p, Ob a) => p a a
id @p @(Interp (Mul r)) p (Interp (Mul r)) (Interp (Mul r))
-> p (Interp (Mul g)) (Interp a ** Interp b)
-> p (Interp (Mul r) ** Interp (Mul g))
     (Interp (Mul r) ** (Interp a ** Interp b))
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 a ** Interp b)
t)
        )
    )

-- | Take a tensor apart: the continuation gets a variable for each side.
{-# INLINE split #-}
split
  :: forall {k} d g g' r1 r (a :: SYN k) b c da db (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 :: 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 (MkTerm p (Interp (Mul g)) (Interp (a :** b))
t) TermP p da '[ '(d, a)] a
-> TermP p db '[ '(d + 1, b)] b -> TermP p (d + 2) g' c
k = case TermP p da '[ '(d, a)] a
-> TermP p db '[ '(d + 1, b)] b -> TermP p (d + 2) g' c
k (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 @_ @p) (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 + 1) @b @_ @p) of
  MkTerm p (Interp (Mul g')) (Interp c)
body -> p (Interp (Mul (Union r g))) (Interp c) -> TermP p d (Union r g) 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 (p (Interp (Mul g')) (Interp c)
body p (Interp (Mul g')) (Interp c)
-> p (Interp (Mul (Union r g))) (Interp (Mul g'))
-> p (Interp (Mul (Union r g))) (Interp c)
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) (b :: SYN k) (g' :: Ctx k)
       (r1 :: Ctx k) (r :: Ctx k) (g :: Ctx k) (p :: CAT k).
(Promonad p, MonoidalProfunctor p, KnownObj a, KnownObj b,
 BindVar (n + 1) b g' r1, BindVar n a r1 r, Merge r g) =>
p (Interp (Mul g)) (Interp a ** Interp b)
-> p (Interp (Mul (Union r g))) (Interp (Mul g'))
forall {k} (n :: Nat) (a :: SYN k) (b :: SYN k) (g' :: Ctx k)
       (r1 :: Ctx k) (r :: Ctx k) (g :: Ctx k) (p :: CAT k).
(Promonad p, MonoidalProfunctor p, KnownObj a, KnownObj b,
 BindVar (n + 1) b g' r1, BindVar n a r1 r, Merge r g) =>
p (Interp (Mul g)) (Interp a ** Interp b)
-> p (Interp (Mul (Union r g))) (Interp (Mul g'))
push2 @d @a @b @g' @r1 @r @g @p p (Interp (Mul g)) (Interp a ** Interp b)
p (Interp (Mul g)) (Interp (a :** b))
t)

-- | The unit, which uses no variables.
{-# INLINE unit #-}
unit :: forall {k} d (p :: CAT k). (MonoidalProfunctor p) => TermP p d ('[] :: Ctx k) I
unit :: forall {k} (d :: Nat) (p :: CAT k).
MonoidalProfunctor p =>
TermP p d '[] I
unit = p (Interp (Mul '[])) (Interp I) -> TermP p d '[] I
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 Unit Unit
p (Interp (Mul '[])) (Interp I)
forall {j} {k} (p :: j +-> k). MonoidalProfunctor p => p Unit Unit
one

-- | The same morphism at another type expression for the same object, and at any depth: between
-- @'F' (a '**' b)@ and @'F' a ':**' 'F' b@, say, so that a pattern can take it apart, or between a
-- type and its 'Dn'. The polarity may change, the morphism does not.
{-# INLINE recast #-}
recast :: forall {k} (a :: SYN k) b d d' g p. (Interp a ~ Interp b) => TermP p d g a -> TermP p d' g b
recast :: 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 (MkTerm p (Interp (Mul g)) (Interp a)
f) = p (Interp (Mul g)) (Interp b) -> TermP p d' g b
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 a)
p (Interp (Mul g)) (Interp b)
f

type DepthOf :: Type -> Nat
type family DepthOf t where
  DepthOf (TermP p d g a) = d

type CtxOf :: forall k. Type -> Ctx k
type family CtxOf t where
  CtxOf (TermP p d g a) = g

type TyOf :: forall k. Type -> SYN k
type family TyOf t where
  TyOf (TermP p d g a) = a