{-# 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 ::
( 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