-- | Load serialized a binding state to 'Control.Monad.ST.ST' based bindings

{-# LANGUAGE TemplateHaskell, FlexibleContexts #-}

module Hyper.Unify.Binding.ST.Load
    ( load
    ) where

import qualified Control.Lens as Lens
import           Control.Monad.ST.Class (MonadST(..))
import           Data.Array.ST (STArray, newArray, readArray, writeArray)
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.Binding.ST (STUVar)
import           Hyper.Unify.Term (UTerm(..), uBody)

import           Hyper.Internal.Prelude

newtype ConvertState s t = ConvertState (STArray s Int (Maybe (STUVar s t)))
makePrisms ''ConvertState

makeConvertState :: MonadST m => Binding # t -> m (ConvertState (World m) # t)
makeConvertState :: (Binding # t) -> m (ConvertState (World m) # t)
makeConvertState (Binding Seq (UTerm UVar ('AHyperType t))
x) =
    (Int, Int)
-> Maybe (STUVar (World m) ('AHyperType t))
-> ST
     (World m)
     (STArray (World m) Int (Maybe (STUVar (World m) ('AHyperType t))))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Int
0, Seq (UTerm UVar ('AHyperType t)) -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (UTerm UVar ('AHyperType t))
x) Maybe (STUVar (World m) ('AHyperType t))
forall a. Maybe a
Nothing ST
  (World m)
  (STArray (World m) Int (Maybe (STUVar (World m) ('AHyperType t))))
-> (ST
      (World m)
      (STArray (World m) Int (Maybe (STUVar (World m) ('AHyperType t))))
    -> m (STArray
            (World m) Int (Maybe (STUVar (World m) ('AHyperType t)))))
-> m (STArray
        (World m) Int (Maybe (STUVar (World m) ('AHyperType t))))
forall a b. a -> (a -> b) -> b
& ST
  (World m)
  (STArray (World m) Int (Maybe (STUVar (World m) ('AHyperType t))))
-> m (STArray
        (World m) Int (Maybe (STUVar (World m) ('AHyperType t))))
forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST m (STArray
     (World m) Int (Maybe (STUVar (World m) ('AHyperType t))))
-> (STArray
      (World m) Int (Maybe (STUVar (World m) ('AHyperType t)))
    -> ConvertState (World m) # t)
-> m (ConvertState (World m) # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> STArray (World m) Int (Maybe (STUVar (World m) ('AHyperType t)))
-> ConvertState (World m) # t
forall s (t :: AHyperType).
STArray s Int (Maybe (STUVar s t)) -> ConvertState s t
ConvertState

loadUTerm ::
    forall m typeVars t.
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding -> typeVars # ConvertState (World m) ->
    UTerm UVar # t -> m (UTerm (STUVar (World m)) # t)
loadUTerm :: (typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UTerm UVar # t)
-> m (UTerm (STUVar (World m)) # t)
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ (UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = TypeConstraintsOf (GetHyperType ('AHyperType t))
-> UTerm (STUVar (World m)) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c (UTerm (STUVar (World m)) # t)
-> ((UTerm (STUVar (World m)) # t)
    -> m (UTerm (STUVar (World m)) # t))
-> m (UTerm (STUVar (World m)) # t)
forall a b. a -> (a -> b) -> b
& (UTerm (STUVar (World m)) # t) -> m (UTerm (STUVar (World m)) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ (USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c) = TypeConstraintsOf (GetHyperType ('AHyperType t))
-> UTerm (STUVar (World m)) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c (UTerm (STUVar (World m)) # t)
-> ((UTerm (STUVar (World m)) # t)
    -> m (UTerm (STUVar (World m)) # t))
-> m (UTerm (STUVar (World m)) # t)
forall a b. a -> (a -> b) -> b
& (UTerm (STUVar (World m)) # t) -> m (UTerm (STUVar (World m)) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
loadUTerm typeVars # Binding
src typeVars # ConvertState (World m)
conv (UToVar UVar ('AHyperType t)
v) = (typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> UVar ('AHyperType t)
-> m (STUVar (World m) ('AHyperType t))
forall (m :: * -> *) (t :: AHyperType -> *)
       (typeVars :: AHyperType -> *).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UVar # t)
-> m (STUVar (World m) # t)
loadVar typeVars # Binding
src typeVars # ConvertState (World m)
conv UVar ('AHyperType t)
v m (STUVar (World m) ('AHyperType t))
-> (STUVar (World m) ('AHyperType t)
    -> UTerm (STUVar (World m)) # t)
-> m (UTerm (STUVar (World m)) # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> STUVar (World m) ('AHyperType t) -> UTerm (STUVar (World m)) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UToVar
loadUTerm typeVars # Binding
src typeVars # ConvertState (World m)
conv (UTerm UTermBody UVar ('AHyperType t)
u) = (('AHyperType t :# UVar) -> m ('AHyperType t :# STUVar (World m)))
-> UTermBody UVar ('AHyperType t)
-> m (UTermBody (STUVar (World m)) ('AHyperType t))
forall (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody ((typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
loadBody typeVars # Binding
src typeVars # ConvertState (World m)
conv) UTermBody UVar ('AHyperType t)
u m (UTermBody (STUVar (World m)) ('AHyperType t))
-> (UTermBody (STUVar (World m)) ('AHyperType t)
    -> UTerm (STUVar (World m)) # t)
-> m (UTerm (STUVar (World m)) # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> UTermBody (STUVar (World m)) ('AHyperType t)
-> UTerm (STUVar (World m)) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UResolving{} = [Char] -> m (UTerm (STUVar (World m)) # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UResolved{} = [Char] -> m (UTerm (STUVar (World m)) # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"converting bindings after resolution"
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UConverted{} = [Char] -> m (UTerm (STUVar (World m)) # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"loading while saving?"
loadUTerm typeVars # Binding
_ typeVars # ConvertState (World m)
_ UInstantiated{} = [Char] -> m (UTerm (STUVar (World m)) # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"loading during instantiation"

loadVar ::
    forall m t typeVars.
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding -> typeVars # ConvertState (World m) ->
    UVar # t -> m (STUVar (World m) # t)
loadVar :: (typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UVar # t)
-> m (STUVar (World m) # t)
loadVar typeVars # Binding
src typeVars # ConvertState (World m)
conv (UVar Int
v) =
    Dict
  (HNodeLens typeVars t,
   HNodesConstraint t (Recursively (HNodeLens typeVars)))
-> ((HNodeLens typeVars t,
     HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
    m (STUVar (World m) # t))
-> m (STUVar (World m) # 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))) =>
  m (STUVar (World m) # t))
 -> m (STUVar (World m) # t))
-> ((HNodeLens typeVars t,
     HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
    m (STUVar (World m) # t))
-> m (STUVar (World m) # t)
forall a b. (a -> b) -> a -> b
$
    let tConv :: STArray (World m) Int (Maybe (STUVar (World m) # t))
tConv = typeVars # ConvertState (World m)
conv (typeVars # ConvertState (World m))
-> Getting
     (STArray (World m) Int (Maybe (STUVar (World m) # t)))
     (typeVars # ConvertState (World m))
     (STArray (World m) Int (Maybe (STUVar (World m) # t)))
-> STArray (World m) Int (Maybe (STUVar (World m) # t))
forall s a. s -> Getting a s a -> a
^. ((ConvertState (World m) # t)
 -> Const
      (STArray (World m) Int (Maybe (STUVar (World m) # t)))
      (ConvertState (World m) # t))
-> (typeVars # ConvertState (World m))
-> Const
     (STArray (World m) Int (Maybe (STUVar (World m) # t)))
     (typeVars # ConvertState (World m))
forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((ConvertState (World m) # t)
  -> Const
       (STArray (World m) Int (Maybe (STUVar (World m) # t)))
       (ConvertState (World m) # t))
 -> (typeVars # ConvertState (World m))
 -> Const
      (STArray (World m) Int (Maybe (STUVar (World m) # t)))
      (typeVars # ConvertState (World m)))
-> ((STArray (World m) Int (Maybe (STUVar (World m) # t))
     -> Const
          (STArray (World m) Int (Maybe (STUVar (World m) # t)))
          (STArray (World m) Int (Maybe (STUVar (World m) # t))))
    -> (ConvertState (World m) # t)
    -> Const
         (STArray (World m) Int (Maybe (STUVar (World m) # t)))
         (ConvertState (World m) # t))
-> Getting
     (STArray (World m) Int (Maybe (STUVar (World m) # t)))
     (typeVars # ConvertState (World m))
     (STArray (World m) Int (Maybe (STUVar (World m) # t)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (STArray (World m) Int (Maybe (STUVar (World m) # t))
 -> Const
      (STArray (World m) Int (Maybe (STUVar (World m) # t)))
      (STArray (World m) Int (Maybe (STUVar (World m) # t))))
-> (ConvertState (World m) # t)
-> Const
     (STArray (World m) Int (Maybe (STUVar (World m) # t)))
     (ConvertState (World m) # t)
forall s (t :: AHyperType) s (t :: AHyperType).
Iso
  (ConvertState s t)
  (ConvertState s t)
  (STArray s Int (Maybe (STUVar s t)))
  (STArray s Int (Maybe (STUVar s t)))
_ConvertState
    in
    STArray (World m) Int (Maybe (STUVar (World m) # t))
-> Int -> ST (World m) (Maybe (STUVar (World m) # t))
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray STArray (World m) Int (Maybe (STUVar (World m) # t))
tConv Int
v ST (World m) (Maybe (STUVar (World m) # t))
-> (ST (World m) (Maybe (STUVar (World m) # t))
    -> m (Maybe (STUVar (World m) # t)))
-> m (Maybe (STUVar (World m) # t))
forall a b. a -> (a -> b) -> b
& ST (World m) (Maybe (STUVar (World m) # t))
-> m (Maybe (STUVar (World m) # t))
forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST
    m (Maybe (STUVar (World m) # t))
-> (Maybe (STUVar (World m) # t) -> m (STUVar (World m) # t))
-> m (STUVar (World m) # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    \case
    Just STUVar (World m) # t
x -> (STUVar (World m) # t) -> m (STUVar (World m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure STUVar (World m) # t
x
    Maybe (STUVar (World m) # t)
Nothing ->
        do
            UTerm (STUVar (World m)) # t
u <-
                (typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UTerm UVar # t)
-> m (UTerm (STUVar (World m)) # t)
forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (UTerm UVar # t)
-> m (UTerm (STUVar (World m)) # t)
loadUTerm typeVars # Binding
src typeVars # ConvertState (World m)
conv
                (typeVars # Binding
src (typeVars # Binding)
-> Getting
     (Endo (UTerm UVar # t)) (typeVars # Binding) (UTerm UVar # t)
-> UTerm UVar # t
forall s a. HasCallStack => s -> Getting (Endo a) s a -> a
^?! ((Binding # t) -> Const (Endo (UTerm UVar # t)) (Binding # t))
-> (typeVars # Binding)
-> Const (Endo (UTerm UVar # t)) (typeVars # Binding)
forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((Binding # t) -> Const (Endo (UTerm UVar # t)) (Binding # t))
 -> (typeVars # Binding)
 -> Const (Endo (UTerm UVar # t)) (typeVars # Binding))
-> (((UTerm UVar # t)
     -> Const (Endo (UTerm UVar # t)) (UTerm UVar # t))
    -> (Binding # t) -> Const (Endo (UTerm UVar # t)) (Binding # t))
-> Getting
     (Endo (UTerm UVar # t)) (typeVars # Binding) (UTerm UVar # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Seq (UTerm UVar # t)
 -> Const (Endo (UTerm UVar # t)) (Seq (UTerm UVar # t)))
-> (Binding # t) -> Const (Endo (UTerm UVar # t)) (Binding # t)
forall (t1 :: AHyperType) (t2 :: AHyperType).
Iso
  (Binding t1)
  (Binding t2)
  (Seq (UTerm UVar t1))
  (Seq (UTerm UVar t2))
_Binding ((Seq (UTerm UVar # t)
  -> Const (Endo (UTerm UVar # t)) (Seq (UTerm UVar # t)))
 -> (Binding # t) -> Const (Endo (UTerm UVar # t)) (Binding # t))
-> (((UTerm UVar # t)
     -> Const (Endo (UTerm UVar # t)) (UTerm UVar # t))
    -> Seq (UTerm UVar # t)
    -> Const (Endo (UTerm UVar # t)) (Seq (UTerm UVar # t)))
-> ((UTerm UVar # t)
    -> Const (Endo (UTerm UVar # t)) (UTerm UVar # t))
-> (Binding # t)
-> Const (Endo (UTerm UVar # t)) (Binding # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Seq (UTerm UVar # t))
-> Traversal'
     (Seq (UTerm UVar # t)) (IxValue (Seq (UTerm UVar # t)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Int
Index (Seq (UTerm UVar # t))
v)
            STUVar (World m) # t
r <- BindingDict (STUVar (World m)) m t
-> (UTerm (STUVar (World m)) # t) -> m (STUVar (World m) # t)
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (STUVar (World m)) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UTerm (STUVar (World m)) # t
u
            STUVar (World m) # t
r (STUVar (World m) # t) -> m () -> m (STUVar (World m) # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ ST (World m) () -> m ()
forall (m :: * -> *) a. MonadST m => ST (World m) a -> m a
liftST (STArray (World m) Int (Maybe (STUVar (World m) # t))
-> Int -> Maybe (STUVar (World m) # t) -> ST (World m) ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray STArray (World m) Int (Maybe (STUVar (World m) # t))
tConv Int
v ((STUVar (World m) # t) -> Maybe (STUVar (World m) # t)
forall a. a -> Maybe a
Just STUVar (World m) # t
r))

loadBody ::
    forall m typeVars t.
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding -> typeVars # ConvertState (World m) ->
    t # UVar -> m (t # STUVar (World m))
loadBody :: (typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
loadBody typeVars # Binding
src typeVars # ConvertState (World m)
conv =
    Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) =>
    (t # UVar) -> m (t # STUVar (World m)))
-> (t # UVar)
-> m (t # STUVar (World m))
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 # UVar) -> m (t # STUVar (World m)))
 -> (t # UVar) -> m (t # STUVar (World m)))
-> (HNodesConstraint t (Unify m) =>
    (t # UVar) -> m (t # STUVar (World m)))
-> (t # UVar)
-> m (t # STUVar (World m))
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 # UVar) -> m (t # STUVar (World m)))
-> (t # UVar)
-> m (t # STUVar (World m))
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 # UVar) -> m (t # STUVar (World m)))
 -> (t # UVar) -> m (t # STUVar (World m)))
-> ((HNodeLens typeVars t,
     HNodesConstraint t (Recursively (HNodeLens typeVars))) =>
    (t # UVar) -> m (t # STUVar (World m)))
-> (t # UVar)
-> m (t # STUVar (World m))
forall a b. (a -> b) -> a -> b
$
    (forall (n :: AHyperType -> *).
 HWitness t n -> (UVar # n) -> m (STUVar (World m) # n))
-> (t # UVar) -> m (t # STUVar (World m))
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)
-> (HWitness t n
    -> Unify m n => (UVar # n) -> m (STUVar (World m) # n))
-> HWitness t n
-> (UVar # n)
-> m (STUVar (World m) # n)
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (HWitness h n -> c n => r) -> HWitness h n -> r
#*# Proxy (Recursively (HNodeLens typeVars))
forall k (t :: k). Proxy t
Proxy @(Recursively (HNodeLens typeVars))
        #> loadVar src conv
    )

-- | Load a given serialized unification
-- and a value with serialized unification variable identifiers
-- to a value with 'Control.Monad.ST.ST' unification variables.
load ::
    ( MonadST m
    , UVarOf m ~ STUVar (World m)
    , HTraversable typeVars
    , Unify m t
    , Recursively (HNodeLens typeVars) t
    ) =>
    typeVars # Binding -> t # UVar -> m (t #STUVar (World m))
load :: (typeVars # Binding) -> (t # UVar) -> m (t # STUVar (World m))
load typeVars # Binding
src t # UVar
collection =
    do
        typeVars # ConvertState (World m)
conv <- (forall (n :: AHyperType -> *).
 HWitness typeVars n
 -> (Binding # n) -> m (ConvertState (World m) # n))
-> (typeVars # Binding) -> m (typeVars # ConvertState (World m))
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 (((Binding # n) -> m (ConvertState (World m) # n))
-> HWitness typeVars n
-> (Binding # n)
-> m (ConvertState (World m) # n)
forall a b. a -> b -> a
const (Binding # n) -> m (ConvertState (World m) # n)
forall (m :: * -> *) (t :: AHyperType -> *).
MonadST m =>
(Binding # t) -> m (ConvertState (World m) # t)
makeConvertState) typeVars # Binding
src
        (typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
forall (m :: * -> *) (typeVars :: AHyperType -> *)
       (t :: AHyperType -> *).
(MonadST m, UVarOf m ~ STUVar (World m), Unify m t,
 Recursively (HNodeLens typeVars) t) =>
(typeVars # Binding)
-> (typeVars # ConvertState (World m))
-> (t # UVar)
-> m (t # STUVar (World m))
loadBody typeVars # Binding
src typeVars # ConvertState (World m)
conv t # UVar
collection