{-# LANGUAGE FlexibleContexts, FlexibleInstances #-}

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

import Control.Lens (mapped, from, _Wrapped, _1, _2)
import Hyper.Combinator.Compose (HCompose(..), _HCompose, decompose)
import Hyper.Combinator.Flip
import Hyper.Combinator.Func (HFunc(..), _HFunc)
import Hyper.Class.Functor (HFunctor(..))
import Hyper.Class.Nodes ((#*#), (#>))
import Hyper.Class.Recursive (Recursively(..))
import Hyper.Combinator.Ann (Ann(..))
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 :: (Pure # p) -> Pure # (HFunc p (Const (Pure # p)) :*: p)
hcontext = ((p # Pure)
 -> Identity ((HFunc p (Const (Pure # p)) :*: p) # Pure))
-> (Pure # p)
-> Identity (Pure # (HFunc p (Const (Pure # p)) :*: p))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (((p # Pure)
  -> Identity ((HFunc p (Const (Pure # p)) :*: p) # Pure))
 -> (Pure # p)
 -> Identity (Pure # (HFunc p (Const (Pure # p)) :*: p)))
-> ((p # Pure) -> (HFunc p (Const (Pure # p)) :*: p) # Pure)
-> (Pure # p)
-> Pure # (HFunc p (Const (Pure # p)) :*: p)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ \p # Pure
x -> ((p # Pure) -> Const (Pure # p) ('AHyperType Pure))
-> HFunc p (Const (Pure # p)) ('AHyperType Pure)
forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc ((Pure # p) -> Const (Pure # p) ('AHyperType Pure)
forall k a (b :: k). a -> Const a b
Const ((Pure # p) -> Const (Pure # p) ('AHyperType Pure))
-> ((p # Pure) -> Pure # p)
-> (p # Pure)
-> Const (Pure # p) ('AHyperType Pure)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p # Pure) -> Pure # p
forall (h :: AHyperType). (h :# Pure) -> Pure h
Pure) HFunc p (Const (Pure # p)) ('AHyperType Pure)
-> (p # Pure) -> (HFunc p (Const (Pure # p)) :*: p) # Pure
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p # Pure
x

instance (HContext a, HFunctor a) => HContext (Ann a) where
    hcontext :: (Ann a # p) -> Ann a # (HFunc p (Const (Ann a # p)) :*: p)
hcontext (Ann a ('AHyperType p)
a 'AHyperType p :# Ann a
b) =
        a ('AHyperType (HFunc p (Const (Ann a # p)) :*: p))
-> ('AHyperType (HFunc p (Const (Ann a # p)) :*: p) :# Ann a)
-> Ann a # (HFunc p (Const (Ann a # p)) :*: p)
forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann
        ((forall (n :: HyperType).
 HWitness a n
 -> ((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
 -> (HFunc p (Const (Ann a # p)) :*: p) # n)
-> (a # (HFunc p (Const (a ('AHyperType p))) :*: p))
-> a ('AHyperType (HFunc p (Const (Ann a # p)) :*: p))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap ((((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
 -> (HFunc p (Const (Ann a # p)) :*: p) # n)
-> HWitness a n
-> ((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
-> (HFunc p (Const (Ann a # p)) :*: p) # n
forall a b. a -> b -> a
const (((HFunc p (Const (a ('AHyperType p))) # n)
 -> Identity (HFunc p (Const (Ann a # p)) # n))
-> ((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
-> Identity ((HFunc p (Const (Ann a # p)) :*: p) # n)
forall s t a b. Field1 s t a b => Lens s t a b
_1 (((HFunc p (Const (a ('AHyperType p))) # n)
  -> Identity (HFunc p (Const (Ann a # p)) # n))
 -> ((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
 -> Identity ((HFunc p (Const (Ann a # p)) :*: p) # n))
-> ((a ('AHyperType p) -> Identity (Ann a # p))
    -> (HFunc p (Const (a ('AHyperType p))) # n)
    -> Identity (HFunc p (Const (Ann a # p)) # n))
-> (a ('AHyperType p) -> Identity (Ann a # p))
-> ((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
-> Identity ((HFunc p (Const (Ann a # p)) :*: p) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((p # n) -> Const (a ('AHyperType p)) # n)
 -> Identity ((p # n) -> Const (Ann a # p) # n))
-> (HFunc p (Const (a ('AHyperType p))) # n)
-> Identity (HFunc p (Const (Ann a # p)) # n)
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 ((((p # n) -> Const (a ('AHyperType p)) # n)
  -> Identity ((p # n) -> Const (Ann a # p) # n))
 -> (HFunc p (Const (a ('AHyperType p))) # n)
 -> Identity (HFunc p (Const (Ann a # p)) # n))
-> ((a ('AHyperType p) -> Identity (Ann a # p))
    -> ((p # n) -> Const (a ('AHyperType p)) # n)
    -> Identity ((p # n) -> Const (Ann a # p) # n))
-> (a ('AHyperType p) -> Identity (Ann a # p))
-> (HFunc p (Const (a ('AHyperType p))) # n)
-> Identity (HFunc p (Const (Ann a # p)) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Const (a ('AHyperType p)) # n)
 -> Identity (Const (Ann a # p) # n))
-> ((p # n) -> Const (a ('AHyperType p)) # n)
-> Identity ((p # n) -> Const (Ann a # p) # n)
forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
mapped (((Const (a ('AHyperType p)) # n)
  -> Identity (Const (Ann a # p) # n))
 -> ((p # n) -> Const (a ('AHyperType p)) # n)
 -> Identity ((p # n) -> Const (Ann a # p) # n))
-> ((a ('AHyperType p) -> Identity (Ann a # p))
    -> (Const (a ('AHyperType p)) # n)
    -> Identity (Const (Ann a # p) # n))
-> (a ('AHyperType p) -> Identity (Ann a # p))
-> ((p # n) -> Const (a ('AHyperType p)) # n)
-> Identity ((p # n) -> Const (Ann a # p) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a ('AHyperType p) -> Identity (Ann a # p))
-> (Const (a ('AHyperType p)) # n)
-> Identity (Const (Ann a # p) # n)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped ((a ('AHyperType p) -> Identity (Ann a # p))
 -> ((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
 -> Identity ((HFunc p (Const (Ann a # p)) :*: p) # n))
-> (a ('AHyperType p) -> Ann a # p)
-> ((HFunc p (Const (a ('AHyperType p))) :*: p) # n)
-> (HFunc p (Const (Ann a # p)) :*: p) # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (a ('AHyperType p) -> ('AHyperType p :# Ann a) -> Ann a # p
forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
`Ann` 'AHyperType p :# Ann a
b))) (a ('AHyperType p)
-> a # (HFunc p (Const (a ('AHyperType p))) :*: p)
forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext a ('AHyperType p)
a))
        ((p ('AHyperType (Ann a))
 -> Const (Ann a # p) ('AHyperType (Ann a)))
-> HFunc p (Const (Ann a # p)) ('AHyperType (Ann a))
forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc ((Ann a # p) -> Const (Ann a # p) ('AHyperType (Ann a))
forall k a (b :: k). a -> Const a b
Const ((Ann a # p) -> Const (Ann a # p) ('AHyperType (Ann a)))
-> (p ('AHyperType (Ann a)) -> Ann a # p)
-> p ('AHyperType (Ann a))
-> Const (Ann a # p) ('AHyperType (Ann a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a ('AHyperType p) -> ('AHyperType p :# Ann a) -> Ann a # p
forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann a ('AHyperType p)
a) HFunc p (Const (Ann a # p)) ('AHyperType (Ann a))
-> p ('AHyperType (Ann a))
-> (:*:) (HFunc p (Const (Ann a # p))) p ('AHyperType (Ann a))
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType (Ann a))
'AHyperType p :# Ann a
b)

instance (HFunctor h0, HContext h0, HFunctor h1, HContext h1) => HContext (HCompose h0 h1) where
    hcontext :: (HCompose h0 h1 # p)
-> HCompose h0 h1 # (HFunc p (Const (HCompose h0 h1 # p)) :*: p)
hcontext =
        ((h0 # HCompose h1 p)
 -> Identity
      (h0 # HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p)))
-> (HCompose h0 h1 # p)
-> Identity
     (HCompose h0 h1 # (HFunc p (Const (HCompose h0 h1 # p)) :*: p))
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 (((h0 # HCompose h1 p)
  -> Identity
       (h0 # HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p)))
 -> (HCompose h0 h1 # p)
 -> Identity
      (HCompose h0 h1 # (HFunc p (Const (HCompose h0 h1 # p)) :*: p)))
-> ((h0 # HCompose h1 p)
    -> h0 # HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p))
-> (HCompose h0 h1 # p)
-> HCompose h0 h1 # (HFunc p (Const (HCompose h0 h1 # p)) :*: p)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
        (forall (n :: HyperType).
 HWitness h0 n
 -> ((HFunc (HCompose h1 p) (Const (h0 # HCompose h1 p))
      :*: HCompose h1 p)
     # n)
 -> HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # n)
-> (h0
    # (HFunc (HCompose h1 p) (Const (h0 # HCompose h1 p))
       :*: HCompose h1 p))
-> h0 # HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p)
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 h0 n
_ (HFunc c0 :*: x0) ->
            HCompose h1 p ('AHyperType n)
x0 HCompose h1 p ('AHyperType n)
-> (HCompose h1 p ('AHyperType n)
    -> HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # n)
-> HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # n
forall a b. a -> (a -> b) -> b
& ((h1 # HCompose p n)
 -> Identity
      (h1 # HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n))
-> HCompose h1 p ('AHyperType n)
-> Identity
     (HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # n)
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 (((h1 # HCompose p n)
  -> Identity
       (h1 # HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n))
 -> HCompose h1 p ('AHyperType n)
 -> Identity
      (HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # n))
-> ((h1 # HCompose p n)
    -> h1 # HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n)
-> HCompose h1 p ('AHyperType n)
-> HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
            (forall (n :: HyperType).
 HWitness h1 n
 -> ((HFunc (HCompose p n) (Const (h1 # HCompose p n))
      :*: HCompose p n)
     # n)
 -> HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n # n)
-> (h1
    # (HFunc (HCompose p n) (Const (h1 # HCompose p n))
       :*: HCompose p n))
-> h1 # HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n
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 h1 n
_ (HFunc c1 :*: x1) ->
                HCompose p n ('AHyperType n)
x1 HCompose p n ('AHyperType n)
-> (HCompose p n ('AHyperType n)
    -> HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n # n)
-> HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n # n
forall a b. a -> (a -> b) -> b
& ((p # HCompose n n)
 -> Identity
      ((HFunc p (Const (HCompose h0 h1 # p)) :*: p) # HCompose n n))
-> HCompose p n ('AHyperType n)
-> Identity
     (HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n # n)
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 (((p # HCompose n n)
  -> Identity
       ((HFunc p (Const (HCompose h0 h1 # p)) :*: p) # HCompose n n))
 -> HCompose p n ('AHyperType n)
 -> Identity
      (HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n # n))
-> ((p # HCompose n n)
    -> (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # HCompose n n)
-> HCompose p n ('AHyperType n)
-> HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
                (((p # HCompose n n)
 -> Const (HCompose h0 h1 # p) ('AHyperType (HCompose n n)))
-> HFunc
     p (Const (HCompose h0 h1 # p)) ('AHyperType (HCompose n n))
forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc ((HCompose h0 h1 # p)
-> Const (HCompose h0 h1 # p) ('AHyperType (HCompose n n))
forall k a (b :: k). a -> Const a b
Const ((HCompose h0 h1 # p)
 -> Const (HCompose h0 h1 # p) ('AHyperType (HCompose n n)))
-> ((p # HCompose n n) -> HCompose h0 h1 # p)
-> (p # HCompose n n)
-> Const (HCompose h0 h1 # p) ('AHyperType (HCompose n n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged (h0 # HCompose h1 p) (Identity (h0 # HCompose h1 p))
-> Tagged (HCompose h0 h1 # p) (Identity (HCompose h0 h1 # p))
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 (Tagged (h0 # HCompose h1 p) (Identity (h0 # HCompose h1 p))
 -> Tagged (HCompose h0 h1 # p) (Identity (HCompose h0 h1 # p)))
-> (h0 # HCompose h1 p) -> HCompose h0 h1 # p
forall t b. AReview t b -> b -> t
#) ((h0 # HCompose h1 p) -> HCompose h0 h1 # p)
-> ((p # HCompose n n) -> h0 # HCompose h1 p)
-> (p # HCompose n n)
-> HCompose h0 h1 # p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const (h0 # HCompose h1 p) ('AHyperType n) -> h0 # HCompose h1 p
forall a k (b :: k). Const a b -> a
getConst (Const (h0 # HCompose h1 p) ('AHyperType n) -> h0 # HCompose h1 p)
-> ((p # HCompose n n)
    -> Const (h0 # HCompose h1 p) ('AHyperType n))
-> (p # HCompose n n)
-> h0 # HCompose h1 p
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HCompose h1 p ('AHyperType n)
-> Const (h0 # HCompose h1 p) ('AHyperType n)
c0 (HCompose h1 p ('AHyperType n)
 -> Const (h0 # HCompose h1 p) ('AHyperType n))
-> ((p # HCompose n n) -> HCompose h1 p ('AHyperType n))
-> (p # HCompose n n)
-> Const (h0 # HCompose h1 p) ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged (h1 # HCompose p n) (Identity (h1 # HCompose p n))
-> Tagged
     (HCompose h1 p ('AHyperType n))
     (Identity (HCompose h1 p ('AHyperType n)))
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 (Tagged (h1 # HCompose p n) (Identity (h1 # HCompose p n))
 -> Tagged
      (HCompose h1 p ('AHyperType n))
      (Identity (HCompose h1 p ('AHyperType n))))
-> (h1 # HCompose p n) -> HCompose h1 p ('AHyperType n)
forall t b. AReview t b -> b -> t
#) ((h1 # HCompose p n) -> HCompose h1 p ('AHyperType n))
-> ((p # HCompose n n) -> h1 # HCompose p n)
-> (p # HCompose n n)
-> HCompose h1 p ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const (h1 # HCompose p n) ('AHyperType n) -> h1 # HCompose p n
forall a k (b :: k). Const a b -> a
getConst (Const (h1 # HCompose p n) ('AHyperType n) -> h1 # HCompose p n)
-> ((p # HCompose n n)
    -> Const (h1 # HCompose p n) ('AHyperType n))
-> (p # HCompose n n)
-> h1 # HCompose p n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HCompose p n ('AHyperType n)
-> Const (h1 # HCompose p n) ('AHyperType n)
c1 (HCompose p n ('AHyperType n)
 -> Const (h1 # HCompose p n) ('AHyperType n))
-> ((p # HCompose n n) -> HCompose p n ('AHyperType n))
-> (p # HCompose n n)
-> Const (h1 # HCompose p n) ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged (p # HCompose n n) (Identity (p # HCompose n n))
-> Tagged
     (HCompose p n ('AHyperType n))
     (Identity (HCompose p n ('AHyperType n)))
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 (Tagged (p # HCompose n n) (Identity (p # HCompose n n))
 -> Tagged
      (HCompose p n ('AHyperType n))
      (Identity (HCompose p n ('AHyperType n))))
-> (p # HCompose n n) -> HCompose p n ('AHyperType n)
forall t b. AReview t b -> b -> t
#)) HFunc p (Const (HCompose h0 h1 # p)) ('AHyperType (HCompose n n))
-> (p # HCompose n n)
-> (HFunc p (Const (HCompose h0 h1 # p)) :*: p) # HCompose n n
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*:)
            ) ((h1
  # (HFunc (HCompose p n) (Const (h1 # HCompose p n))
     :*: HCompose p n))
 -> h1 # HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n)
-> ((h1 # HCompose p n)
    -> h1
       # (HFunc (HCompose p n) (Const (h1 # HCompose p n))
          :*: HCompose p n))
-> (h1 # HCompose p n)
-> h1 # HCompose (HFunc p (Const (HCompose h0 h1 # p)) :*: p) n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (h1 # HCompose p n)
-> h1
   # (HFunc (HCompose p n) (Const (h1 # HCompose p n))
      :*: HCompose p n)
forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext
        ) ((h0
  # (HFunc (HCompose h1 p) (Const (h0 # HCompose h1 p))
     :*: HCompose h1 p))
 -> h0 # HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p))
-> ((h0 # HCompose h1 p)
    -> h0
       # (HFunc (HCompose h1 p) (Const (h0 # HCompose h1 p))
          :*: HCompose h1 p))
-> (h0 # HCompose h1 p)
-> h0 # HCompose h1 (HFunc p (Const (HCompose h0 h1 # p)) :*: p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (h0 # HCompose h1 p)
-> h0
   # (HFunc (HCompose h1 p) (Const (h0 # HCompose h1 p))
      :*: HCompose h1 p)
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 :: (HFlip Ann h # p)
-> HFlip Ann h # (HFunc p (Const (HFlip Ann h # p)) :*: p)
hcontext =
        (forall (n :: HyperType).
 HWitness (HFlip Ann h) n
 -> ((HFunc p (Const (Ann p # h)) :*: p) # n)
 -> (HFunc p (Const (HFlip Ann h # p)) :*: p) # n)
-> (HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p))
-> HFlip Ann h # (HFunc p (Const (HFlip Ann h # p)) :*: p)
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap ((((HFunc p (Const (Ann p # h)) :*: p) # n)
 -> (HFunc p (Const (HFlip Ann h # p)) :*: p) # n)
-> HWitness (HFlip Ann h) n
-> ((HFunc p (Const (Ann p # h)) :*: p) # n)
-> (HFunc p (Const (HFlip Ann h # p)) :*: p) # n
forall a b. a -> b -> a
const (((HFunc p (Const (Ann p # h)) # n)
 -> Identity (HFunc p (Const (HFlip Ann h # p)) # n))
-> ((HFunc p (Const (Ann p # h)) :*: p) # n)
-> Identity ((HFunc p (Const (HFlip Ann h # p)) :*: p) # n)
forall s t a b. Field1 s t a b => Lens s t a b
_1 (((HFunc p (Const (Ann p # h)) # n)
  -> Identity (HFunc p (Const (HFlip Ann h # p)) # n))
 -> ((HFunc p (Const (Ann p # h)) :*: p) # n)
 -> Identity ((HFunc p (Const (HFlip Ann h # p)) :*: p) # n))
-> (((Ann p # h) -> Identity (HFlip Ann h # p))
    -> (HFunc p (Const (Ann p # h)) # n)
    -> Identity (HFunc p (Const (HFlip Ann h # p)) # n))
-> ((Ann p # h) -> Identity (HFlip Ann h # p))
-> ((HFunc p (Const (Ann p # h)) :*: p) # n)
-> Identity ((HFunc p (Const (HFlip Ann h # p)) :*: p) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((p # n) -> Const (Ann p # h) # n)
 -> Identity ((p # n) -> Const (HFlip Ann h # p) # n))
-> (HFunc p (Const (Ann p # h)) # n)
-> Identity (HFunc p (Const (HFlip Ann h # p)) # n)
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 ((((p # n) -> Const (Ann p # h) # n)
  -> Identity ((p # n) -> Const (HFlip Ann h # p) # n))
 -> (HFunc p (Const (Ann p # h)) # n)
 -> Identity (HFunc p (Const (HFlip Ann h # p)) # n))
-> (((Ann p # h) -> Identity (HFlip Ann h # p))
    -> ((p # n) -> Const (Ann p # h) # n)
    -> Identity ((p # n) -> Const (HFlip Ann h # p) # n))
-> ((Ann p # h) -> Identity (HFlip Ann h # p))
-> (HFunc p (Const (Ann p # h)) # n)
-> Identity (HFunc p (Const (HFlip Ann h # p)) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Const (Ann p # h) # n) -> Identity (Const (HFlip Ann h # p) # n))
-> ((p # n) -> Const (Ann p # h) # n)
-> Identity ((p # n) -> Const (HFlip Ann h # p) # n)
forall (f :: * -> *) a b. Functor f => Setter (f a) (f b) a b
mapped (((Const (Ann p # h) # n)
  -> Identity (Const (HFlip Ann h # p) # n))
 -> ((p # n) -> Const (Ann p # h) # n)
 -> Identity ((p # n) -> Const (HFlip Ann h # p) # n))
-> (((Ann p # h) -> Identity (HFlip Ann h # p))
    -> (Const (Ann p # h) # n)
    -> Identity (Const (HFlip Ann h # p) # n))
-> ((Ann p # h) -> Identity (HFlip Ann h # p))
-> ((p # n) -> Const (Ann p # h) # n)
-> Identity ((p # n) -> Const (HFlip Ann h # p) # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Ann p # h) -> Identity (HFlip Ann h # p))
-> (Const (Ann p # h) # n)
-> Identity (Const (HFlip Ann h # p) # n)
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
_Wrapped (((Ann p # h) -> Identity (HFlip Ann h # p))
 -> ((HFunc p (Const (Ann p # h)) :*: p) # n)
 -> Identity ((HFunc p (Const (HFlip Ann h # p)) :*: p) # n))
-> ((Ann p # h) -> HFlip Ann h # p)
-> ((HFunc p (Const (Ann p # h)) :*: p) # n)
-> (HFunc p (Const (HFlip Ann h # p)) :*: p) # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Tagged (Ann p # h) (Identity (Ann p # h))
-> Tagged (HFlip Ann h # p) (Identity (HFlip Ann h # p))
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 (Tagged (Ann p # h) (Identity (Ann p # h))
 -> Tagged (HFlip Ann h # p) (Identity (HFlip Ann h # p)))
-> (Ann p # h) -> HFlip Ann h # p
forall t b. AReview t b -> b -> t
#))) ((HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p))
 -> HFlip Ann h # (HFunc p (Const (HFlip Ann h # p)) :*: p))
-> ((HFlip Ann h # p)
    -> HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p))
-> (HFlip Ann h # p)
-> HFlip Ann h # (HFunc p (Const (HFlip Ann h # p)) :*: p)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AnIso
  (Ann (HFunc p (Const (Ann p # h)) :*: p) # h)
  (Ann p # h)
  (HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p))
  (HFlip Ann h # p)
-> Iso
     (HFlip Ann h # p)
     (HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p))
     (Ann p # h)
     (Ann (HFunc p (Const (Ann p # h)) :*: p) # h)
forall s t a b. AnIso s t a b -> Iso b a t s
from AnIso
  (Ann (HFunc p (Const (Ann p # h)) :*: p) # h)
  (Ann p # h)
  (HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p))
  (HFlip Ann h # p)
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 (((Ann p # h)
  -> Identity (Ann (HFunc p (Const (Ann p # h)) :*: p) # h))
 -> (HFlip Ann h # p)
 -> Identity (HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p)))
-> ((Ann p # h) -> Ann (HFunc p (Const (Ann p # h)) :*: p) # h)
-> (HFlip Ann h # p)
-> HFlip Ann h # (HFunc p (Const (Ann p # h)) :*: p)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Ann (HFunc (Ann p) (Const (Ann p # h)) :*: p) # h)
-> Ann (HFunc p (Const (Ann p # h)) :*: p) # h
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) (Const (Ann p # h)) :*: p) # h)
 -> Ann (HFunc p (Const (Ann p # h)) :*: p) # h)
-> ((Ann p # h)
    -> Ann (HFunc (Ann p) (Const (Ann p # h)) :*: p) # h)
-> (Ann p # h)
-> Ann (HFunc p (Const (Ann p # h)) :*: p) # h
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Ann p # h) -> Ann (HFunc (Ann p) (Const (Ann p # h)) :*: p) # h
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 :: (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) =
                Dict (HFunctor n, HNodesConstraint n (Recursively HFunctor))
-> ((HFunctor n, HNodesConstraint n (Recursively HFunctor)) =>
    Ann (HFunc p (Const r) :*: p) # n)
-> Ann (HFunc p (Const r) :*: p) # n
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor n)
-> Dict (HFunctor n, HNodesConstraint n (Recursively HFunctor))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor n)
forall k (t :: k). Proxy t
Proxy @(HFunctor n))) (((HFunctor n, HNodesConstraint n (Recursively HFunctor)) =>
  Ann (HFunc p (Const r) :*: p) # n)
 -> Ann (HFunc p (Const r) :*: p) # n)
-> ((HFunctor n, HNodesConstraint n (Recursively HFunctor)) =>
    Ann (HFunc p (Const r) :*: p) # n)
-> Ann (HFunc p (Const r) :*: p) # n
forall a b. (a -> b) -> a -> b
$
                (:*:) (HFunc p (Const r)) p ('AHyperType n)
-> ('AHyperType n :# Ann (HFunc p (Const r) :*: p))
-> Ann (HFunc p (Const r) :*: p) # n
forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann ((p ('AHyperType n) -> Const r ('AHyperType n))
-> HFunc p (Const r) ('AHyperType n)
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 (Ann p ('AHyperType n) -> Const r ('AHyperType n))
-> (p ('AHyperType n) -> Ann p ('AHyperType n))
-> p ('AHyperType n)
-> Const r ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p ('AHyperType n)
-> ('AHyperType n :# Ann p) -> Ann p ('AHyperType n)
forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
`Ann` (n # Ann (HFunc (Ann p) (Const r) :*: p)) -> n # Ann p
forall (n :: HyperType) (a :: HyperType) (b :: HyperType).
Recursively HFunctor n =>
(n # Ann (a :*: b)) -> n # Ann b
g n # Ann (HFunc (Ann p) (Const r) :*: p)
'AHyperType n :# Ann (HFunc (Ann p) (Const r) :*: p)
b)) HFunc p (Const r) ('AHyperType n)
-> p ('AHyperType n) -> (:*:) (HFunc p (Const r)) p ('AHyperType n)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: p ('AHyperType n)
a) ((forall (n :: HyperType).
 HWitness n n
 -> (Ann (HFunc (Ann p) (Const r) :*: p) # n)
 -> Ann (HFunc p (Const r) :*: p) # n)
-> (n # Ann (HFunc (Ann p) (Const r) :*: p))
-> n # Ann (HFunc p (Const r) :*: p)
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor) Proxy (Recursively HFunctor)
-> (Recursively HFunctor n =>
    (Ann (HFunc (Ann p) (Const r) :*: p) # n)
    -> Ann (HFunc p (Const r) :*: p) # n)
-> HWitness n n
-> (Ann (HFunc (Ann p) (Const r) :*: p) # n)
-> Ann (HFunc p (Const r) :*: p) # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Recursively HFunctor n =>
(Ann (HFunc (Ann p) (Const r) :*: p) # n)
-> Ann (HFunc p (Const r) :*: p) # n
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) n # Ann (HFunc (Ann p) (Const r) :*: p)
'AHyperType n :# Ann (HFunc (Ann p) (Const r) :*: p)
b)
            g ::
                forall n a b.
                Recursively HFunctor n => n # Ann (a :*: b) -> n # Ann b
            g :: (n # Ann (a :*: b)) -> n # Ann b
g =
                Dict (HFunctor n, HNodesConstraint n (Recursively HFunctor))
-> ((HFunctor n, HNodesConstraint n (Recursively HFunctor)) =>
    (n # Ann (a :*: b)) -> n # Ann b)
-> (n # Ann (a :*: b))
-> n # Ann b
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor n)
-> Dict (HFunctor n, HNodesConstraint n (Recursively HFunctor))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor n)
forall k (t :: k). Proxy t
Proxy @(HFunctor n))) (((HFunctor n, HNodesConstraint n (Recursively HFunctor)) =>
  (n # Ann (a :*: b)) -> n # Ann b)
 -> (n # Ann (a :*: b)) -> n # Ann b)
-> ((HFunctor n, HNodesConstraint n (Recursively HFunctor)) =>
    (n # Ann (a :*: b)) -> n # Ann b)
-> (n # Ann (a :*: b))
-> n # Ann b
forall a b. (a -> b) -> a -> b
$
                (forall (n :: HyperType).
 HWitness n n -> (Ann (a :*: b) # n) -> Ann b # n)
-> (n # Ann (a :*: b)) -> n # Ann b
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor) Proxy (Recursively HFunctor)
-> (Recursively HFunctor n => (Ann (a :*: b) # n) -> Ann b # n)
-> HWitness n n
-> (Ann (a :*: b) # n)
-> Ann b # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> ((HFlip Ann n # (a :*: b)) -> Identity (HFlip Ann n # b))
-> (Ann (a :*: b) # n) -> Identity (Ann b # n)
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 (((HFlip Ann n # (a :*: b)) -> Identity (HFlip Ann n # b))
 -> (Ann (a :*: b) # n) -> Identity (Ann b # n))
-> ((HFlip Ann n # (a :*: b)) -> HFlip Ann n # b)
-> (Ann (a :*: b) # n)
-> Ann b # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (forall (n :: HyperType).
 HWitness (HFlip Ann n) n -> ((a :*: b) # n) -> b # n)
-> (HFlip Ann n # (a :*: b)) -> HFlip Ann n # b
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap ((((a :*: b) # n) -> b ('AHyperType n))
-> HWitness (HFlip Ann n) n -> ((a :*: b) # n) -> b ('AHyperType n)
forall a b. a -> b -> a
const (((a :*: b) # n)
-> Getting (b ('AHyperType n)) ((a :*: b) # n) (b ('AHyperType n))
-> b ('AHyperType n)
forall s a. s -> Getting a s a -> a
^. Getting (b ('AHyperType n)) ((a :*: b) # n) (b ('AHyperType n))
forall s t a b. Field2 s t a b => Lens s t a b
_2)))

-- | 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 :: (p # h) -> HCompose (Ann (HFunc Pure (Const (p # h)))) p # h
recursiveContexts = ((HFunc p (Const (p # h)) :*: p) # h)
-> HCompose (Ann (HFunc Pure (Const (p # h)))) p # h
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 (Const (p # h)) :*: p) # h)
 -> HCompose (Ann (HFunc Pure (Const (p # h)))) p # h)
-> ((p # h) -> (HFunc p (Const (p # h)) :*: p) # h)
-> (p # h)
-> HCompose (Ann (HFunc Pure (Const (p # h)))) p # h
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((p # h) -> Const (p # h) ('AHyperType h))
-> HFunc p (Const (p # h)) ('AHyperType h)
forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc (p # h) -> Const (p # h) ('AHyperType h)
forall k a (b :: k). a -> Const a b
Const HFunc p (Const (p # h)) ('AHyperType h)
-> (p # h) -> (HFunc p (Const (p # h)) :*: p) # h
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 :: ((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) =
    Dict (HFunctor p, HNodesConstraint p (Recursively HFunctor))
-> ((HFunctor p, HNodesConstraint p (Recursively HFunctor)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor p)
-> Dict (HFunctor p, HNodesConstraint p (Recursively HFunctor))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor p)
forall k (t :: k). Proxy t
Proxy @(HFunctor p))) (((HFunctor p, HNodesConstraint p (Recursively HFunctor)) =>
  HCompose (Ann (HFunc Pure (Const r))) p # h)
 -> HCompose (Ann (HFunc Pure (Const r))) p # h)
-> ((HFunctor p, HNodesConstraint p (Recursively HFunctor)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall a b. (a -> b) -> a -> b
$
    Dict (HFunctor h, HNodesConstraint h (Recursively HFunctor))
-> ((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor h)
-> Dict (HFunctor h, HNodesConstraint h (Recursively HFunctor))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor h)
forall k (t :: k). Proxy t
Proxy @(HFunctor h))) (((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
  HCompose (Ann (HFunc Pure (Const r))) p # h)
 -> HCompose (Ann (HFunc Pure (Const r))) p # h)
-> ((HFunctor h, HNodesConstraint h (Recursively HFunctor)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall a b. (a -> b) -> a -> b
$
    Dict (HContext p, HNodesConstraint p (Recursively HContext))
-> ((HContext p, HNodesConstraint p (Recursively HContext)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HContext p)
-> Dict (HContext p, HNodesConstraint p (Recursively HContext))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HContext p)
forall k (t :: k). Proxy t
Proxy @(HContext p))) (((HContext p, HNodesConstraint p (Recursively HContext)) =>
  HCompose (Ann (HFunc Pure (Const r))) p # h)
 -> HCompose (Ann (HFunc Pure (Const r))) p # h)
-> ((HContext p, HNodesConstraint p (Recursively HContext)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall a b. (a -> b) -> a -> b
$
    Dict (HContext h, HNodesConstraint h (Recursively HContext))
-> ((HContext h, HNodesConstraint h (Recursively HContext)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HContext h)
-> Dict (HContext h, HNodesConstraint h (Recursively HContext))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HContext h)
forall k (t :: k). Proxy t
Proxy @(HContext h))) (((HContext h, HNodesConstraint h (Recursively HContext)) =>
  HCompose (Ann (HFunc Pure (Const r))) p # h)
 -> HCompose (Ann (HFunc Pure (Const r))) p # h)
-> ((HContext h, HNodesConstraint h (Recursively HContext)) =>
    HCompose (Ann (HFunc Pure (Const r))) p # h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall a b. (a -> b) -> a -> b
$
    Tagged
  (Ann (HFunc Pure (Const r)) # HCompose p h)
  (Identity (Ann (HFunc Pure (Const r)) # HCompose p h))
-> Tagged
     (HCompose (Ann (HFunc Pure (Const r))) p # h)
     (Identity (HCompose (Ann (HFunc Pure (Const r))) p # h))
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 (Tagged
   (Ann (HFunc Pure (Const r)) # HCompose p h)
   (Identity (Ann (HFunc Pure (Const r)) # HCompose p h))
 -> Tagged
      (HCompose (Ann (HFunc Pure (Const r))) p # h)
      (Identity (HCompose (Ann (HFunc Pure (Const r))) p # h)))
-> (Ann (HFunc Pure (Const r)) # HCompose p h)
-> HCompose (Ann (HFunc Pure (Const r))) p # h
forall t b. AReview t b -> b -> t
# Ann :: forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann
    { _hAnn :: HFunc Pure (Const r) ('AHyperType (HCompose p h))
_hAnn = Tagged
  ((Pure # HCompose p h) -> Const r # HCompose p h)
  (Identity ((Pure # HCompose p h) -> Const r # HCompose p h))
-> Tagged
     (HFunc Pure (Const r) ('AHyperType (HCompose p h)))
     (Identity (HFunc Pure (Const r) ('AHyperType (HCompose p h))))
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 (Tagged
   ((Pure # HCompose p h) -> Const r # HCompose p h)
   (Identity ((Pure # HCompose p h) -> Const r # HCompose p h))
 -> Tagged
      (HFunc Pure (Const r) ('AHyperType (HCompose p h)))
      (Identity (HFunc Pure (Const r) ('AHyperType (HCompose p h)))))
-> ((Pure # HCompose p h) -> Const r # HCompose p h)
-> HFunc Pure (Const r) ('AHyperType (HCompose p h))
forall t b. AReview t b -> b -> t
# r -> Const r # HCompose p h
forall k a (b :: k). a -> Const a b
Const (r -> Const r # HCompose p h)
-> ((Pure # HCompose p h) -> r)
-> (Pure # HCompose p h)
-> Const r # HCompose p h
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const r ('AHyperType h) -> r
forall a k (b :: k). Const a b -> a
getConst (Const r ('AHyperType h) -> r)
-> ((Pure # HCompose p h) -> Const r ('AHyperType h))
-> (Pure # HCompose p h)
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ('AHyperType h) -> Const r ('AHyperType h)
s0 (p ('AHyperType h) -> Const r ('AHyperType h))
-> ((Pure # HCompose p h) -> p ('AHyperType h))
-> (Pure # HCompose p h)
-> Const r ('AHyperType h)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Pure # HCompose p h)
-> Getting
     (p ('AHyperType h)) (Pure # HCompose p h) (p ('AHyperType h))
-> p ('AHyperType h)
forall s a. s -> Getting a s a -> a
^. Getting
  (p ('AHyperType h)) (Pure # HCompose p h) (p ('AHyperType h))
forall (a0 :: HyperType) (b0 :: HyperType) (a1 :: HyperType)
       (b1 :: HyperType).
(Recursively HFunctor a0, Recursively HFunctor b0,
 Recursively HFunctor a1, Recursively HFunctor b1) =>
Iso
  (Pure # HCompose a0 b0) (Pure # HCompose a1 b1) (a0 # b0) (a1 # b1)
decompose)
    , _hVal :: 'AHyperType (HCompose p h) :# Ann (HFunc Pure (Const r))
_hVal =
        Tagged
  (p # HCompose h (Ann (HFunc Pure (Const r))))
  (Identity (p # HCompose h (Ann (HFunc Pure (Const r)))))
-> Tagged
     (HCompose p h # Ann (HFunc Pure (Const r)))
     (Identity (HCompose p h # Ann (HFunc Pure (Const r))))
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 (Tagged
   (p # HCompose h (Ann (HFunc Pure (Const r))))
   (Identity (p # HCompose h (Ann (HFunc Pure (Const r)))))
 -> Tagged
      (HCompose p h # Ann (HFunc Pure (Const r)))
      (Identity (HCompose p h # Ann (HFunc Pure (Const r)))))
-> (p # HCompose h (Ann (HFunc Pure (Const r))))
-> HCompose p h # Ann (HFunc Pure (Const r))
forall t b. AReview t b -> b -> t
#
        (forall (n :: HyperType).
 HWitness p n
 -> ((HFunc h (Const (p ('AHyperType h))) :*: h) # n)
 -> HCompose h (Ann (HFunc Pure (Const r))) # n)
-> (p # (HFunc h (Const (p ('AHyperType h))) :*: h))
-> p # HCompose h (Ann (HFunc Pure (Const r)))
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
        ( Proxy (Recursively HContext)
forall k (t :: k). Proxy t
Proxy @(Recursively HContext) Proxy (Recursively HContext)
-> (Recursively HContext n =>
    HWitness p n
    -> ((HFunc h (Const (p ('AHyperType h))) :*: h) # n)
    -> HCompose h (Ann (HFunc Pure (Const r))) # n)
-> HWitness p n
-> ((HFunc h (Const (p ('AHyperType h))) :*: h) # n)
-> HCompose h (Ann (HFunc Pure (Const r))) # n
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
#*# Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor) Proxy (Recursively HFunctor)
-> (Recursively HFunctor n =>
    ((HFunc h (Const (p ('AHyperType h))) :*: h) # n)
    -> HCompose h (Ann (HFunc Pure (Const r))) # n)
-> HWitness p n
-> ((HFunc h (Const (p ('AHyperType h))) :*: h) # n)
-> HCompose h (Ann (HFunc Pure (Const r))) # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
            \(HFunc h ('AHyperType n) -> Const (p ('AHyperType h)) ('AHyperType n)
s1 :*: h ('AHyperType n)
x1) ->
            Tagged
  (h # HCompose (Ann (HFunc Pure (Const r))) n)
  (Identity (h # HCompose (Ann (HFunc Pure (Const r))) n))
-> Tagged
     (HCompose h (Ann (HFunc Pure (Const r))) # n)
     (Identity (HCompose h (Ann (HFunc Pure (Const r))) # n))
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 (Tagged
   (h # HCompose (Ann (HFunc Pure (Const r))) n)
   (Identity (h # HCompose (Ann (HFunc Pure (Const r))) n))
 -> Tagged
      (HCompose h (Ann (HFunc Pure (Const r))) # n)
      (Identity (HCompose h (Ann (HFunc Pure (Const r))) # n)))
-> (h # HCompose (Ann (HFunc Pure (Const r))) n)
-> HCompose h (Ann (HFunc Pure (Const r))) # n
forall t b. AReview t b -> b -> t
#
            (forall (n :: HyperType).
 HWitness h n
 -> ((HFunc n (Const (h ('AHyperType n))) :*: n) # n)
 -> HCompose (Ann (HFunc Pure (Const r))) n # n)
-> (h # (HFunc n (Const (h ('AHyperType n))) :*: n))
-> h # HCompose (Ann (HFunc Pure (Const r))) n
forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
            ( Proxy (Recursively HContext)
forall k (t :: k). Proxy t
Proxy @(Recursively HContext) Proxy (Recursively HContext)
-> (Recursively HContext n =>
    HWitness h n
    -> ((HFunc n (Const (h ('AHyperType n))) :*: n) # n)
    -> HCompose (Ann (HFunc Pure (Const r))) n # n)
-> HWitness h n
-> ((HFunc n (Const (h ('AHyperType n))) :*: n) # n)
-> HCompose (Ann (HFunc Pure (Const r))) n # n
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
#*# Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor) Proxy (Recursively HFunctor)
-> (Recursively HFunctor n =>
    ((HFunc n (Const (h ('AHyperType n))) :*: n) # n)
    -> HCompose (Ann (HFunc Pure (Const r))) n # n)
-> HWitness h n
-> ((HFunc n (Const (h ('AHyperType n))) :*: n) # n)
-> HCompose (Ann (HFunc Pure (Const r))) n # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                \(HFunc n ('AHyperType n) -> Const (h ('AHyperType n)) ('AHyperType n)
s2 :*: n ('AHyperType n)
x2) ->
                ((HFunc n (Const r) :*: n) # n)
-> HCompose (Ann (HFunc Pure (Const r))) n # n
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 ((n ('AHyperType n) -> Const r ('AHyperType n))
-> HFunc n (Const r) ('AHyperType n)
forall (i :: HyperType) (o :: HyperType) (h :: AHyperType).
(i h -> o h) -> HFunc i o h
HFunc (r -> Const r ('AHyperType n)
forall k a (b :: k). a -> Const a b
Const (r -> Const r ('AHyperType n))
-> (n ('AHyperType n) -> r)
-> n ('AHyperType n)
-> Const r ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const r ('AHyperType h) -> r
forall a k (b :: k). Const a b -> a
getConst (Const r ('AHyperType h) -> r)
-> (n ('AHyperType n) -> Const r ('AHyperType h))
-> n ('AHyperType n)
-> r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p ('AHyperType h) -> Const r ('AHyperType h)
s0 (p ('AHyperType h) -> Const r ('AHyperType h))
-> (n ('AHyperType n) -> p ('AHyperType h))
-> n ('AHyperType n)
-> Const r ('AHyperType h)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const (p ('AHyperType h)) ('AHyperType n) -> p ('AHyperType h)
forall a k (b :: k). Const a b -> a
getConst (Const (p ('AHyperType h)) ('AHyperType n) -> p ('AHyperType h))
-> (n ('AHyperType n) -> Const (p ('AHyperType h)) ('AHyperType n))
-> n ('AHyperType n)
-> p ('AHyperType h)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. h ('AHyperType n) -> Const (p ('AHyperType h)) ('AHyperType n)
s1 (h ('AHyperType n) -> Const (p ('AHyperType h)) ('AHyperType n))
-> (n ('AHyperType n) -> h ('AHyperType n))
-> n ('AHyperType n)
-> Const (p ('AHyperType h)) ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const (h ('AHyperType n)) ('AHyperType n) -> h ('AHyperType n)
forall a k (b :: k). Const a b -> a
getConst (Const (h ('AHyperType n)) ('AHyperType n) -> h ('AHyperType n))
-> (n ('AHyperType n) -> Const (h ('AHyperType n)) ('AHyperType n))
-> n ('AHyperType n)
-> h ('AHyperType n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n ('AHyperType n) -> Const (h ('AHyperType n)) ('AHyperType n)
s2) HFunc n (Const r) ('AHyperType n)
-> n ('AHyperType n) -> (HFunc n (Const r) :*: n) # n
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: n ('AHyperType n)
x2)
            ) (h ('AHyperType n)
-> h # (HFunc n (Const (h ('AHyperType n))) :*: n)
forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext h ('AHyperType n)
x1)
        ) (p ('AHyperType h)
-> p # (HFunc h (Const (p ('AHyperType h))) :*: h)
forall (h :: HyperType) (p :: HyperType).
HContext h =>
(h # p) -> h # (HFunc p (Const (h # p)) :*: p)
hcontext p ('AHyperType h)
x0)
    }

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