-- | Serialize the state of unification

{-# LANGUAGE FlexibleContexts #-}

module Hyper.Unify.Binding.Save
    ( save
    ) where

import qualified Control.Lens as Lens
import           Control.Monad.Trans.Class (MonadTrans(..))
import           Control.Monad.Trans.State (StateT(..))
import           Hyper
import           Hyper.Class.Optic (HNodeLens(..))
import           Hyper.Class.Unify (Unify(..), UVarOf, BindingDict(..))
import           Hyper.Recurse
import           Hyper.Unify.Binding (Binding, _Binding, UVar(..))
import           Hyper.Unify.Term (UTerm(..), uBody)

import           Hyper.Internal.Prelude

saveUTerm ::
    forall m typeVars t.
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    UTerm (UVarOf m) # t ->
    StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
saveUTerm :: (UTerm (UVarOf m) # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
saveUTerm (UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = TypeConstraintsOf (GetHyperType ('AHyperType t)) -> UTerm UVar # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c (UTerm UVar # t)
-> ((UTerm UVar # t)
    -> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t))
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall a b. a -> (a -> b) -> b
& (UTerm UVar # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
saveUTerm (USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = TypeConstraintsOf (GetHyperType ('AHyperType t)) -> UTerm UVar # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c (UTerm UVar # t)
-> ((UTerm UVar # t)
    -> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t))
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall a b. a -> (a -> b) -> b
& (UTerm UVar # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
saveUTerm (UToVar UVarOf m ('AHyperType t)
v) = UVarOf m ('AHyperType t)
-> StateT (typeVars # Binding, [m ()]) m (UVar # t)
forall (m :: * -> *) (t :: AHyperType -> *)
       (typeVars :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(UVarOf m # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t)
saveVar UVarOf m ('AHyperType t)
v StateT (typeVars # Binding, [m ()]) m (UVar # t)
-> ((UVar # t) -> UTerm UVar # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (UVar # t) -> UTerm UVar # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UToVar
saveUTerm (UTerm UTermBody (UVarOf m) ('AHyperType t)
u) = (('AHyperType t :# UVarOf m)
 -> StateT (typeVars # Binding, [m ()]) m ('AHyperType t :# UVar))
-> UTermBody (UVarOf m) ('AHyperType t)
-> StateT
     (typeVars # Binding, [m ()]) m (UTermBody UVar ('AHyperType t))
forall (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody ('AHyperType t :# UVarOf m)
-> StateT (typeVars # Binding, [m ()]) m ('AHyperType t :# UVar)
forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody UTermBody (UVarOf m) ('AHyperType t)
u StateT
  (typeVars # Binding, [m ()]) m (UTermBody UVar ('AHyperType t))
-> (UTermBody UVar ('AHyperType t) -> UTerm UVar # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> UTermBody UVar ('AHyperType t) -> UTerm UVar # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm
saveUTerm UInstantiated{} = [Char] -> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings during instantiation"
saveUTerm UResolving{} = [Char] -> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
saveUTerm UResolved{} = [Char] -> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
saveUTerm UConverted{} = [Char] -> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"converting variable again"

saveVar ::
    forall m t typeVars.
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    UVarOf m # t ->
    StateT (typeVars # Binding, [m ()]) m (UVar # t)
saveVar :: (UVarOf m # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t)
saveVar UVarOf m # t
v =
    Dict
  (HNodeLens typeVars t,
   HNodesConstraint t (Recursively (HNodeLens typeVars)))
-> ((HNodeLens typeVars t,
     HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
    StateT (typeVars # Binding, [m ()]) m (UVar # t))
-> StateT (typeVars # Binding, [m ()]) m (UVar # t)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HNodeLens typeVars t)
-> Dict
     (HNodeLens typeVars t,
      HNodesConstraint t (Recursively (HNodeLens typeVars)))
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HNodeLens typeVars t)
forall k (t :: k). Proxy t
Proxy @(HNodeLens typeVars t))) (((HNodeLens typeVars t,
   HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
  StateT (typeVars # Binding, [m ()]) m (UVar # t))
 -> StateT (typeVars # Binding, [m ()]) m (UVar # t))
-> ((HNodeLens typeVars t,
     HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
    StateT (typeVars # Binding, [m ()]) m (UVar # t))
-> StateT (typeVars # Binding, [m ()]) m (UVar # t)
forall a b. (a -> b) -> a -> b
$
    BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> m (UTerm (UVarOf m) # t)
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v m (UTerm (UVarOf m) # t)
-> (m (UTerm (UVarOf m) # t)
    -> StateT (typeVars # Binding, [m ()]) m (UTerm (UVarOf m) # t))
-> StateT (typeVars # Binding, [m ()]) m (UTerm (UVarOf m) # t)
forall a b. a -> (a -> b) -> b
& m (UTerm (UVarOf m) # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm (UVarOf m) # t)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
    StateT (typeVars # Binding, [m ()]) m (UTerm (UVarOf m) # t)
-> ((UTerm (UVarOf m) # t)
    -> StateT (typeVars # Binding, [m ()]) m (UVar # t))
-> StateT (typeVars # Binding, [m ()]) m (UVar # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    \case
    UConverted Int
i -> (UVar # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> UVar # t
forall (t :: AHyperType). Int -> UVar t
UVar Int
i)
    UTerm (UVarOf m) # t
srcBody ->
        do
            Binding # t
pb <- Getting (Binding # t) (typeVars # Binding, [m ()]) (Binding # t)
-> StateT (typeVars # Binding, [m ()]) m (Binding # t)
forall s (m :: * -> *) a. MonadState s m => Getting a s a -> m a
Lens.use (((typeVars # Binding) -> Const (Binding # t) (typeVars # Binding))
-> (typeVars # Binding, [m ()])
-> Const (Binding # t) (typeVars # Binding, [m ()])
forall s t a b. Field1 s t a b => Lens s t a b
Lens._1 (((typeVars # Binding) -> Const (Binding # t) (typeVars # Binding))
 -> (typeVars # Binding, [m ()])
 -> Const (Binding # t) (typeVars # Binding, [m ()]))
-> (((Binding # t) -> Const (Binding # t) (Binding # t))
    -> (typeVars # Binding)
    -> Const (Binding # t) (typeVars # Binding))
-> Getting (Binding # t) (typeVars # Binding, [m ()]) (Binding # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Binding # t) -> Const (Binding # t) (Binding # t))
-> (typeVars # Binding) -> Const (Binding # t) (typeVars # Binding)
forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens)
            let r :: Int
r = Binding # t
pb (Binding # t)
-> Getting
     (Seq (UTerm UVar ('AHyperType t)))
     (Binding # t)
     (Seq (UTerm UVar ('AHyperType t)))
-> Seq (UTerm UVar ('AHyperType t))
forall s a. s -> Getting a s a -> a
^. Getting
  (Seq (UTerm UVar ('AHyperType t)))
  (Binding # t)
  (Seq (UTerm UVar ('AHyperType t)))
forall (t1 :: AHyperType) (t2 :: AHyperType).
Iso
  (Binding t1)
  (Binding t2)
  (Seq (UTerm UVar t1))
  (Seq (UTerm UVar t2))
_Binding Seq (UTerm UVar ('AHyperType t))
-> (Seq (UTerm UVar ('AHyperType t)) -> Int) -> Int
forall a b. a -> (a -> b) -> b
& Seq (UTerm UVar ('AHyperType t)) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
            Int -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
Int -> UTerm v ast
UConverted Int
r (UTerm (UVarOf m) # t) -> ((UTerm (UVarOf m) # t) -> m ()) -> m ()
forall a b. a -> (a -> b) -> b
& BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v m ()
-> (m () -> StateT (typeVars # Binding, [m ()]) m ())
-> StateT (typeVars # Binding, [m ()]) m ()
forall a b. a -> (a -> b) -> b
& m () -> StateT (typeVars # Binding, [m ()]) m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            ([m ()] -> Identity [m ()])
-> (typeVars # Binding, [m ()])
-> Identity (typeVars # Binding, [m ()])
forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 (([m ()] -> Identity [m ()])
 -> (typeVars # Binding, [m ()])
 -> Identity (typeVars # Binding, [m ()]))
-> ([m ()] -> [m ()]) -> StateT (typeVars # Binding, [m ()]) m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ([m ()] -> [m ()] -> [m ()]
forall a. Semigroup a => a -> a -> a
<> [BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v UTerm (UVarOf m) # t
srcBody])
            UTerm UVar ('AHyperType t)
dstBody <- (UTerm (UVarOf m) # t)
-> StateT
     (typeVars # Binding, [m ()]) m (UTerm UVar ('AHyperType t))
forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(UTerm (UVarOf m) # t)
-> StateT (typeVars # Binding, [m ()]) m (UTerm UVar # t)
saveUTerm UTerm (UVarOf m) # t
srcBody
            ((typeVars # Binding) -> Identity (typeVars # Binding))
-> (typeVars # Binding, [m ()])
-> Identity (typeVars # Binding, [m ()])
forall s t a b. Field1 s t a b => Lens s t a b
Lens._1 (((typeVars # Binding) -> Identity (typeVars # Binding))
 -> (typeVars # Binding, [m ()])
 -> Identity (typeVars # Binding, [m ()]))
-> (((Binding # t) -> Identity (Binding # t))
    -> (typeVars # Binding) -> Identity (typeVars # Binding))
-> ((Binding # t) -> Identity (Binding # t))
-> (typeVars # Binding, [m ()])
-> Identity (typeVars # Binding, [m ()])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Binding # t) -> Identity (Binding # t))
-> (typeVars # Binding) -> Identity (typeVars # Binding)
forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((Binding # t) -> Identity (Binding # t))
 -> (typeVars # Binding, [m ()])
 -> Identity (typeVars # Binding, [m ()]))
-> (Binding # t) -> StateT (typeVars # Binding, [m ()]) m ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> b -> m ()
.= (Binding # t
pb (Binding # t) -> ((Binding # t) -> Binding # t) -> Binding # t
forall a b. a -> (a -> b) -> b
& (Seq (UTerm UVar ('AHyperType t))
 -> Identity (Seq (UTerm UVar ('AHyperType t))))
-> (Binding # t) -> Identity (Binding # t)
forall (t1 :: AHyperType) (t2 :: AHyperType).
Iso
  (Binding t1)
  (Binding t2)
  (Seq (UTerm UVar t1))
  (Seq (UTerm UVar t2))
_Binding ((Seq (UTerm UVar ('AHyperType t))
  -> Identity (Seq (UTerm UVar ('AHyperType t))))
 -> (Binding # t) -> Identity (Binding # t))
-> (Seq (UTerm UVar ('AHyperType t))
    -> Seq (UTerm UVar ('AHyperType t)))
-> (Binding # t)
-> Binding # t
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ (Seq (UTerm UVar ('AHyperType t))
-> UTerm UVar ('AHyperType t) -> Seq (UTerm UVar ('AHyperType t))
forall s a. Snoc s s a a => s -> a -> s
Lens.|> UTerm UVar ('AHyperType t)
dstBody))
            Int -> UVar # t
forall (t :: AHyperType). Int -> UVar t
UVar Int
r (UVar # t)
-> ((UVar # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t))
-> StateT (typeVars # Binding, [m ()]) m (UVar # t)
forall a b. a -> (a -> b) -> b
& (UVar # t) -> StateT (typeVars # Binding, [m ()]) m (UVar # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure

saveBody ::
    forall m typeVars t.
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    t # UVarOf m ->
    StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody :: (t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody =
    Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) =>
    (t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
-> (t # UVarOf m)
-> StateT (typeVars # Binding, [m ()]) m (t # UVar)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (Unify m t) -> Dict (HNodesConstraint t (Unify m))
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (Unify m t)
forall k (t :: k). Proxy t
Proxy @(Unify m t))) ((HNodesConstraint t (Unify m) =>
  (t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
 -> (t # UVarOf m)
 -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
-> (HNodesConstraint t (Unify m) =>
    (t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
-> (t # UVarOf m)
-> StateT (typeVars # Binding, [m ()]) m (t # UVar)
forall a b. (a -> b) -> a -> b
$
    Dict
  (HNodeLens typeVars t,
   HNodesConstraint t (Recursively (HNodeLens typeVars)))
-> ((HNodeLens typeVars t,
     HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
    (t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
-> (t # UVarOf m)
-> StateT (typeVars # Binding, [m ()]) m (t # UVar)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HNodeLens typeVars t)
-> Dict
     (HNodeLens typeVars t,
      HNodesConstraint t (Recursively (HNodeLens typeVars)))
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HNodeLens typeVars t)
forall k (t :: k). Proxy t
Proxy @(HNodeLens typeVars t))) (((HNodeLens typeVars t,
   HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
  (t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
 -> (t # UVarOf m)
 -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
-> ((HNodeLens typeVars t,
     HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
    (t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar))
-> (t # UVarOf m)
-> StateT (typeVars # Binding, [m ()]) m (t # UVar)
forall a b. (a -> b) -> a -> b
$
    (forall (n :: AHyperType -> *).
 HWitness t n
 -> (UVarOf m # n)
 -> StateT (typeVars # Binding, [m ()]) m (UVar # n))
-> (t # UVarOf m)
-> StateT (typeVars # Binding, [m ()]) m (t # UVar)
forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
(Applicative f, HTraversable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse
    ( Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n =>
    HWitness t n
    -> (UVarOf m # n)
    -> StateT (typeVars # Binding, [m ()]) m (UVar # n))
-> HWitness t n
-> (UVarOf m # n)
-> StateT (typeVars # Binding, [m ()]) m (UVar # n)
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*# Proxy (Recursively (HNodeLens typeVars))
forall k (t :: k). Proxy t
Proxy @(Recursively (HNodeLens typeVars))
        #> saveVar
    )

-- | Serialize the state of unification for
-- the unification variables in a given value,
-- and transform the value's unification variables
-- to their serialized identifiers.
save ::
    (Unify m t, Recursively (HNodeLens typeVars) t) =>
    t # UVarOf m ->
    StateT (typeVars # Binding) m (t # UVar)
save :: (t # UVarOf m) -> StateT (typeVars # Binding) m (t # UVar)
save t # UVarOf m
collection =
    ((typeVars # Binding) -> m (t # UVar, typeVars # Binding))
-> StateT (typeVars # Binding) m (t # UVar)
forall s (m :: * -> *) a. (s -> m (a, s)) -> StateT s m a
StateT (((typeVars # Binding) -> m (t # UVar, typeVars # Binding))
 -> StateT (typeVars # Binding) m (t # UVar))
-> ((typeVars # Binding) -> m (t # UVar, typeVars # Binding))
-> StateT (typeVars # Binding) m (t # UVar)
forall a b. (a -> b) -> a -> b
$
    \typeVars # Binding
dstState ->
    do
        (t # UVar
r, (typeVars # Binding
finalState, [m ()]
recover)) <- StateT (typeVars # Binding, [m ()]) m (t # UVar)
-> (typeVars # Binding, [m ()])
-> m (t # UVar, (typeVars # Binding, [m ()]))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT ((t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar)
forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(Unify m t, Recursively (HNodeLens typeVars) t) =>
(t # UVarOf m) -> StateT (typeVars # Binding, [m ()]) m (t # UVar)
saveBody t # UVarOf m
collection) (typeVars # Binding
dstState, [])
        (t # UVar
r, typeVars # Binding
finalState) (t # UVar, typeVars # Binding)
-> m () -> m (t # UVar, typeVars # Binding)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover