{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}

module Hyper.Class.Context
    ( HContext (..)
    , recursiveContexts
    , annContexts
    ) where

import Control.Lens (from, mapped, _1, _2, _Wrapped)
import Hyper.Class.Functor (HFunctor (..))
import Hyper.Class.Nodes ((#*#), (#>))
import Hyper.Class.Recursive (Recursively (..))
import Hyper.Combinator.Ann (Ann (..))
import Hyper.Combinator.Compose (HCompose (..), decompose, _HCompose)
import Hyper.Combinator.Flip
import Hyper.Combinator.Func (HFunc (..), _HFunc)
import Hyper.Type (type (#))
import Hyper.Type.Pure (Pure (..), _Pure)

import Hyper.Internal.Prelude

class HContext h where
    -- | Add next to each node a function to replace it in the parent with a different value
    hcontext ::
        h # p ->
        h # (HFunc p (Const (h # p)) :*: p)

instance HContext Pure where
    hcontext :: forall (p :: HyperType).
(Pure # p) -> Pure # (HFunc p (Const (Pure # p)) :*: p)
hcontext = forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc (forall {k} a (b :: k). a -> Const a b
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: AHyperType). (h :# Pure) -> Pure h
Pure) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:)

instance (HContext a, HFunctor a) => HContext (Ann a) where
    hcontext :: forall (p :: HyperType).
(Ann a # p) -> Ann a # (HFunc p (Const (Ann a # p)) :*: p)
hcontext (Ann a ('AHyperType p)
a 'AHyperType p :# Ann a
b) =
        forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann
            (forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall a b. a -> b -> a
const (forall s t a b. Field1 s t a b => Lens s t a b
_1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (i0 :: HyperType) (o0 :: HyperType) (h0 :: HyperType)
       (i1 :: HyperType) (o1 :: HyperType) (h1 :: HyperType).
Iso
  (HFunc i0 o0 # h0)
  (HFunc i1 o1 # h1)
  ((i0 # h0) -> o0 # h0)
  ((i1 # h1) -> o1 # h1)
_HFunc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
mapped forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
`Ann` 'AHyperType p :# Ann a
b))) (forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext a ('AHyperType p)
a))
            (forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc (forall {k} a (b :: k). a -> Const a b
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann a ('AHyperType p)
a) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: 'AHyperType p :# Ann a
b)

instance (HFunctor c1, HContext c1, HFunctor h1, HContext h1) => HContext (HCompose c1 h1) where
    hcontext :: forall (p :: HyperType).
(HCompose c1 h1 # p)
-> HCompose c1 h1 # (HFunc p (Const (HCompose c1 h1 # p)) :*: p)
hcontext =
        forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (h :: HyperType) (p0 :: HyperType) (q0 :: HyperType)
       (p1 :: HyperType) (q1 :: HyperType).
(HFunctor h, HContext h) =>
(forall (n :: HyperType).
 ((p0 # HCompose q0 n) -> Const (h # HCompose p0 q0) # n)
 -> (p0 # HCompose q0 n) -> p1 # HCompose q1 n)
-> (h # HCompose p0 q0) -> h # HCompose p1 q1
layer (\(h1 # HCompose p n) -> Const (c1 # HCompose h1 p) # n
c0 -> forall (h :: HyperType) (p0 :: HyperType) (q0 :: HyperType)
       (p1 :: HyperType) (q1 :: HyperType).
(HFunctor h, HContext h) =>
(forall (n :: HyperType).
 ((p0 # HCompose q0 n) -> Const (h # HCompose p0 q0) # n)
 -> (p0 # HCompose q0 n) -> p1 # HCompose q1 n)
-> (h # HCompose p0 q0) -> h # HCompose p1 q1
layer forall a b. (a -> b) -> a -> b
$ \(p # HCompose n n) -> Const (h1 # HCompose p n) # n
c1 -> (forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc ((forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose forall t b. AReview t b -> b -> t
#)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (h1 # HCompose p n) -> Const (c1 # HCompose h1 p) # n
c0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p # HCompose n n) -> Const (h1 # HCompose p n) # n
c1) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:))
        where
            layer ::
                (HFunctor h, HContext h) =>
                (forall n. (p0 # HCompose q0 n -> Const (h # HCompose p0 q0) # n) -> p0 # HCompose q0 n -> p1 # HCompose q1 n) ->
                (h # HCompose p0 q0) ->
                h # HCompose p1 q1
            layer :: forall (h :: HyperType) (p0 :: HyperType) (q0 :: HyperType)
       (p1 :: HyperType) (q1 :: HyperType).
(HFunctor h, HContext h) =>
(forall (n :: HyperType).
 ((p0 # HCompose q0 n) -> Const (h # HCompose p0 q0) # n)
 -> (p0 # HCompose q0 n) -> p1 # HCompose q1 n)
-> (h # HCompose p0 q0) -> h # HCompose p1 q1
layer forall (n :: HyperType).
((p0 # HCompose q0 n) -> Const (h # HCompose p0 q0) # n)
-> (p0 # HCompose q0 n) -> p1 # HCompose q1 n
f = forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (\HWitness h n
_ (HFunc HCompose p0 q0 ('AHyperType n)
-> Const (h # HCompose p0 q0) ('AHyperType n)
c :*: HCompose p0 q0 ('AHyperType n)
x) -> HCompose p0 q0 ('AHyperType n)
x forall a b. a -> (a -> b) -> b
& forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (n :: HyperType).
((p0 # HCompose q0 n) -> Const (h # HCompose p0 q0) # n)
-> (p0 # HCompose q0 n) -> p1 # HCompose q1 n
f (HCompose p0 q0 ('AHyperType n)
-> Const (h # HCompose p0 q0) ('AHyperType n)
c forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose forall t b. AReview t b -> b -> t
#))) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext

instance (Recursively HContext h, Recursively HFunctor h) => HContext (HFlip Ann h) where
    -- The context of (HFlip Ann h) differs from annContexts in that
    -- only the annotation itself is replaced rather than the whole subexpression.
    hcontext :: forall (p :: HyperType).
(HFlip Ann h # p)
-> HFlip Ann h # (HFunc p (Const (HFlip Ann h # p)) :*: p)
hcontext =
        forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall a b. a -> b -> a
const (forall s t a b. Field1 s t a b => Lens s t a b
_1 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (i0 :: HyperType) (o0 :: HyperType) (h0 :: HyperType)
       (i1 :: HyperType) (o1 :: HyperType) (h1 :: HyperType).
Iso
  (HFunc i0 o0 # h0)
  (HFunc i1 o1 # h1)
  ((i0 # h0) -> o0 # h0)
  ((i1 # h1) -> o1 # h1)
_HFunc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
mapped forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (f0 :: HyperType -> HyperType) (x0 :: HyperType)
       (k0 :: HyperType) (f1 :: HyperType -> HyperType) (x1 :: HyperType)
       (k1 :: HyperType).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip forall t b. AReview t b -> b -> t
#))) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s t a b. AnIso s t a b -> Iso b a t s
from forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
       (x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
       (x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (n :: HyperType) (p :: HyperType) r.
Recursively HFunctor n =>
(Ann (HFunc (Ann p) (Const r) :*: p) # n)
-> Ann (HFunc p (Const r) :*: p) # n
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: HyperType) (p :: HyperType).
(Recursively HContext h, Recursively HFunctor h) =>
(Ann p # h) -> Ann (HFunc (Ann p) (Const (Ann p # h)) :*: p) # h
annContexts)
        where
            f ::
                forall n p r.
                Recursively HFunctor n =>
                Ann (HFunc (Ann p) (Const r) :*: p) # n ->
                Ann (HFunc p (Const r) :*: p) # n
            f :: forall (n :: HyperType) (p :: HyperType) r.
Recursively HFunctor n =>
(Ann (HFunc (Ann p) (Const r) :*: p) # n)
-> Ann (HFunc p (Const r) :*: p) # n
f (Ann (HFunc Ann p ('AHyperType n) -> Const r ('AHyperType n)
func :*: p ('AHyperType n)
a) 'AHyperType n :# Ann (HFunc (Ann p) (Const r) :*: p)
b) =
                forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann (forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc (Ann p ('AHyperType n) -> Const r ('AHyperType n)
func forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
`Ann` forall (n :: HyperType) (a :: HyperType) (b :: HyperType).
Recursively HFunctor n =>
(n # Ann (a :*: b)) -> n # Ann b
g 'AHyperType n :# Ann (HFunc (Ann p) (Const r) :*: p)
b)) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType n)
a) (forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall {k} (t :: k). Proxy t
Proxy @(Recursively HFunctor) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (n :: HyperType) (p :: HyperType) r.
Recursively HFunctor n =>
(Ann (HFunc (Ann p) (Const r) :*: p) # n)
-> Ann (HFunc p (Const r) :*: p) # n
f) 'AHyperType n :# Ann (HFunc (Ann p) (Const r) :*: p)
b)
                    forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HFunctor n))
            g ::
                forall n a b.
                Recursively HFunctor n =>
                n # Ann (a :*: b) ->
                n # Ann b
            g :: forall (n :: HyperType) (a :: HyperType) (b :: HyperType).
Recursively HFunctor n =>
(n # Ann (a :*: b)) -> n # Ann b
g =
                forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall {k} (t :: k). Proxy t
Proxy @(Recursively HFunctor) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (f0 :: HyperType -> HyperType) (k0 :: HyperType)
       (x0 :: HyperType) (f1 :: HyperType -> HyperType) (k1 :: HyperType)
       (x1 :: HyperType).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall a b. a -> b -> a
const (forall s a. s -> Getting a s a -> a
^. forall s t a b. Field2 s t a b => Lens s t a b
_2)))
                    forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HFunctor n))

-- | Add in the node annotations a function to replace each node in the top-level node
recursiveContexts ::
    (Recursively HContext h, Recursively HFunctor h, Recursively HContext p, Recursively HFunctor p) =>
    p # h ->
    HCompose (Ann (HFunc Pure (Const (p # h)))) p # h
recursiveContexts :: forall (h :: HyperType) (p :: HyperType).
(Recursively HContext h, Recursively HFunctor h,
 Recursively HContext p, Recursively HFunctor p) =>
(p # h) -> HCompose (Ann (HFunc Pure (Const (p # h)))) p # h
recursiveContexts = forall (h :: HyperType) (p :: HyperType) r.
(Recursively HContext h, Recursively HFunctor h,
 Recursively HContext p, Recursively HFunctor p) =>
((HFunc p (Const r) :*: p) # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
recursiveContextsWith forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc forall {k} a (b :: k). a -> Const a b
Const forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:)

recursiveContextsWith ::
    forall h p r.
    (Recursively HContext h, Recursively HFunctor h, Recursively HContext p, Recursively HFunctor p) =>
    (HFunc p (Const r) :*: p) # h ->
    HCompose (Ann (HFunc Pure (Const r))) p # h
recursiveContextsWith :: forall (h :: HyperType) (p :: HyperType) r.
(Recursively HContext h, Recursively HFunctor h,
 Recursively HContext p, Recursively HFunctor p) =>
((HFunc p (Const r) :*: p) # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
recursiveContextsWith (HFunc p ('AHyperType h) -> Const r ('AHyperType h)
s0 :*: p ('AHyperType h)
x0) =
    forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose
        # Ann
            { _hAnn = _HFunc # Const . getConst . s0 . (^. decompose)
            , _hVal =
                layer x0 $ \s1 x1 -> layer x1 $ \s2 x2 -> recursiveContextsWith (HFunc (Const . getConst . s0 . s1 . s2) :*: x2)
            }
    where
        layer ::
            forall t s c0 c1.
            (Recursively HFunctor t, Recursively HContext t) =>
            t # s ->
            (forall n. (Recursively HFunctor n, Recursively HContext n) => (s # n -> t # s) -> s # n -> HCompose c0 c1 # n) ->
            HCompose t c0 # c1
        layer :: forall (t :: HyperType) (s :: HyperType) (c0 :: HyperType)
       (c1 :: HyperType).
(Recursively HFunctor t, Recursively HContext t) =>
(t # s)
-> (forall (n :: HyperType).
    (Recursively HFunctor n, Recursively HContext n) =>
    ((s # n) -> t # s) -> (s # n) -> HCompose c0 c1 # n)
-> HCompose t c0 # c1
layer t # s
x forall (n :: HyperType).
(Recursively HFunctor n, Recursively HContext n) =>
((s # n) -> t # s) -> (s # n) -> HCompose c0 c1 # n
f =
            forall (a0 :: HyperType) (b0 :: HyperType) (h0 :: HyperType)
       (a1 :: HyperType) (b1 :: HyperType) (h1 :: HyperType).
Iso
  (HCompose a0 b0 # h0)
  (HCompose a1 b1 # h1)
  (a0 # HCompose b0 h0)
  (a1 # HCompose b1 h1)
_HCompose
                # hmap (Proxy @(Recursively HContext) #*# Proxy @(Recursively HFunctor) #> \(HFunc s :*: v) -> f (getConst . s) v) (hcontext x)
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HFunctor t))
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HContext t))

-- | Add in the node annotations a function to replace each node in the top-level node
--
-- It is possible to define annContexts in terms of 'recursiveContexts' but the conversion is quite unwieldy.
annContexts ::
    (Recursively HContext h, Recursively HFunctor h) =>
    Ann p # h ->
    Ann (HFunc (Ann p) (Const (Ann p # h)) :*: p) # h
annContexts :: forall (h :: HyperType) (p :: HyperType).
(Recursively HContext h, Recursively HFunctor h) =>
(Ann p # h) -> Ann (HFunc (Ann p) (Const (Ann p # h)) :*: p) # h
annContexts = forall (h :: HyperType) (p :: HyperType) r.
(Recursively HContext h, Recursively HFunctor h) =>
((HFunc (Ann p) (Const r) :*: Ann p) # h)
-> Ann (HFunc (Ann p) (Const r) :*: p) # h
annContextsWith forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc forall {k} a (b :: k). a -> Const a b
Const forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:)

annContextsWith ::
    forall h p r.
    (Recursively HContext h, Recursively HFunctor h) =>
    (HFunc (Ann p) (Const r) :*: Ann p) # h ->
    Ann (HFunc (Ann p) (Const r) :*: p) # h
annContextsWith :: forall (h :: HyperType) (p :: HyperType) r.
(Recursively HContext h, Recursively HFunctor h) =>
((HFunc (Ann p) (Const r) :*: Ann p) # h)
-> Ann (HFunc (Ann p) (Const r) :*: p) # h
annContextsWith (HFunc Ann p ('AHyperType h) -> Const r ('AHyperType h)
s0 :*: Ann p ('AHyperType h)
a 'AHyperType h :# Ann p
b) =
    Ann
        { _hAnn :: (:*:) (HFunc (Ann p) (Const r)) p ('AHyperType h)
_hAnn = forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc Ann p ('AHyperType h) -> Const r ('AHyperType h)
s0 forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType h)
a
        , _hVal :: 'AHyperType h :# Ann (HFunc (Ann p) (Const r) :*: p)
_hVal =
            forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
                ( forall {k} (t :: k). Proxy t
Proxy @(Recursively HContext) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*#
                    forall {k} (t :: k). Proxy t
Proxy @(Recursively HFunctor) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                        \(HFunc Ann p ('AHyperType n) -> Const (h # Ann p) ('AHyperType n)
s1 :*: Ann p ('AHyperType n)
x) ->
                            forall (h :: HyperType) (p :: HyperType) r.
(Recursively HContext h, Recursively HFunctor h) =>
((HFunc (Ann p) (Const r) :*: Ann p) # h)
-> Ann (HFunc (Ann p) (Const r) :*: p) # h
annContextsWith (forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc (forall {k} a (b :: k). a -> Const a b
Const forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ann p ('AHyperType h) -> Const r ('AHyperType h)
s0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann p ('AHyperType h)
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} a (b :: k). Const a b -> a
getConst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ann p ('AHyperType n) -> Const (h # Ann p) ('AHyperType n)
s1) forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: Ann p ('AHyperType n)
x)
                )
                (forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext 'AHyperType h :# Ann p
b)
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HFunctor h))
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HContext h))
        }