{-# 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
)
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