{-# LANGUAGE FlexibleContexts #-}

module Hyper.Infer
    ( infer

    , InferResultsConstraint
    , inferUVarsApplyBindings

    , module Hyper.Class.Infer
    , module Hyper.Class.Infer.Env
    , module Hyper.Class.Infer.InferOf
    , module Hyper.Infer.ScopeLevel
    , module Hyper.Infer.Result

    , -- | Exported only for SPECIALIZE pragmas
      inferH
    ) where

import qualified Control.Lens as Lens
import           Hyper
import           Hyper.Class.Infer
import           Hyper.Class.Infer.Env
import           Hyper.Class.Infer.InferOf
import           Hyper.Class.Nodes (HNodesHaveConstraint(..))
import           Hyper.Infer.Result
import           Hyper.Infer.ScopeLevel
import           Hyper.Unify (Unify, UVarOf, applyBindings)

import           Hyper.Internal.Prelude

-- | Perform Hindley-Milner type inference of a term
{-# INLINE infer #-}
infer ::
    forall m t a.
    Infer m t =>
    Ann a # t ->
    m (Ann (a :*: InferResult (UVarOf m)) # t)
infer :: (Ann a # t) -> m (Ann (a :*: InferResult (UVarOf m)) # t)
infer (Ann a ('AHyperType t)
a 'AHyperType t :# Ann a
x) =
    Dict
  (HNodesConstraint t (Infer m),
   HNodesConstraint (InferOf t) (UnifyGen m))
-> ((HNodesConstraint t (Infer m),
     HNodesConstraint (InferOf t) (UnifyGen m)) =>
    m (Ann (a :*: InferResult (UVarOf m)) # t))
-> m (Ann (a :*: InferResult (UVarOf m)) # t)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m
-> Proxy t
-> Dict
     (HNodesConstraint t (Infer m),
      HNodesConstraint (InferOf t) (UnifyGen m))
forall (m :: * -> *) (t :: HyperType) (proxy0 :: (* -> *) -> *)
       (proxy1 :: HyperType -> *).
Infer m t =>
proxy0 m
-> proxy1 t
-> Dict
     (HNodesConstraint t (Infer m),
      HNodesConstraint (InferOf t) (UnifyGen m))
inferContext (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) (((HNodesConstraint t (Infer m),
   HNodesConstraint (InferOf t) (UnifyGen m)) =>
  m (Ann (a :*: InferResult (UVarOf m)) # t))
 -> m (Ann (a :*: InferResult (UVarOf m)) # t))
-> ((HNodesConstraint t (Infer m),
     HNodesConstraint (InferOf t) (UnifyGen m)) =>
    m (Ann (a :*: InferResult (UVarOf m)) # t))
-> m (Ann (a :*: InferResult (UVarOf m)) # t)
forall a b. (a -> b) -> a -> b
$
    (t # InferChild m (Ann (a :*: InferResult (UVarOf m))))
-> m (t # Ann (a :*: InferResult (UVarOf m)),
      InferOf t ('AHyperType (UVarOf m)))
forall (m :: * -> *) (t :: HyperType) (h :: HyperType).
Infer m t =>
(t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferBody ((forall (n :: HyperType).
 HWitness t n
 -> (Ann a # n)
 -> InferChild m (Ann (a :*: InferResult (UVarOf m))) # n)
-> (t # Ann a)
-> t # InferChild m (Ann (a :*: InferResult (UVarOf m)))
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 (Infer m)
forall k (t :: k). Proxy t
Proxy @(Infer m) Proxy (Infer m)
-> (Infer m n =>
    (Ann a # n)
    -> InferChild m (Ann (a :*: InferResult (UVarOf m))) # n)
-> HWitness t n
-> (Ann a # n)
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # n
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Infer m n =>
(Ann a # n)
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # n
forall (m :: * -> *) (t :: HyperType) (a :: HyperType).
Infer m t =>
(Ann a # t)
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
inferH) t # Ann a
'AHyperType t :# Ann a
x)
    m (t # Ann (a :*: InferResult (UVarOf m)),
   InferOf t ('AHyperType (UVarOf m)))
-> ((t # Ann (a :*: InferResult (UVarOf m)),
     InferOf t ('AHyperType (UVarOf m)))
    -> Ann (a :*: InferResult (UVarOf m)) # t)
-> m (Ann (a :*: InferResult (UVarOf m)) # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (\(t # Ann (a :*: InferResult (UVarOf m))
xI, InferOf t ('AHyperType (UVarOf m))
t) -> (:*:) a (InferResult (UVarOf m)) ('AHyperType t)
-> ('AHyperType t :# Ann (a :*: InferResult (UVarOf m)))
-> Ann (a :*: InferResult (UVarOf m)) # t
forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann (a ('AHyperType t)
a a ('AHyperType t)
-> InferResult (UVarOf m) ('AHyperType t)
-> (:*:) a (InferResult (UVarOf m)) ('AHyperType t)
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: (InferOf (GetHyperType ('AHyperType t)) # UVarOf m)
-> InferResult (UVarOf m) ('AHyperType t)
forall (v2 :: HyperType) (e2 :: AHyperType).
(InferOf (GetHyperType e2) # v2) -> InferResult v2 e2
InferResult InferOf t ('AHyperType (UVarOf m))
InferOf (GetHyperType ('AHyperType t)) # UVarOf m
t) t # Ann (a :*: InferResult (UVarOf m))
'AHyperType t :# Ann (a :*: InferResult (UVarOf m))
xI)

{-# INLINE inferH #-}
inferH ::
    Infer m t =>
    Ann a # t ->
    InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
inferH :: (Ann a # t)
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
inferH Ann a # t
c = (Ann a # t) -> m (Ann (a :*: InferResult (UVarOf m)) # t)
forall (m :: * -> *) (t :: HyperType) (a :: HyperType).
Infer m t =>
(Ann a # t) -> m (Ann (a :*: InferResult (UVarOf m)) # t)
infer Ann a # t
c m (Ann (a :*: InferResult (UVarOf m)) # t)
-> ((Ann (a :*: InferResult (UVarOf m)) # t)
    -> InferredChild
         (UVarOf m) (Ann (a :*: InferResult (UVarOf m))) ('AHyperType t))
-> m (InferredChild
        (UVarOf m) (Ann (a :*: InferResult (UVarOf m))) ('AHyperType t))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (\Ann (a :*: InferResult (UVarOf m)) # t
i -> (Ann (a :*: InferResult (UVarOf m)) # t)
-> (InferOf (GetHyperType ('AHyperType t)) # UVarOf m)
-> InferredChild
     (UVarOf m) (Ann (a :*: InferResult (UVarOf m))) ('AHyperType t)
forall (v :: HyperType) (h :: HyperType) (t :: AHyperType).
h t -> (InferOf (GetHyperType t) # v) -> InferredChild v h t
InferredChild Ann (a :*: InferResult (UVarOf m)) # t
i (Ann (a :*: InferResult (UVarOf m)) # t
i (Ann (a :*: InferResult (UVarOf m)) # t)
-> Getting
     (InferOf t # UVarOf m)
     (Ann (a :*: InferResult (UVarOf m)) # t)
     (InferOf t # UVarOf m)
-> InferOf t # UVarOf m
forall s a. s -> Getting a s a -> a
^. ((:*:) a (InferResult (UVarOf m)) ('AHyperType t)
 -> Const
      (InferOf t # UVarOf m)
      ((:*:) a (InferResult (UVarOf m)) ('AHyperType t)))
-> (Ann (a :*: InferResult (UVarOf m)) # t)
-> Const
     (InferOf t # UVarOf m) (Ann (a :*: InferResult (UVarOf m)) # t)
forall (a :: HyperType) (h :: AHyperType). Lens' (Ann a h) (a h)
hAnn (((:*:) a (InferResult (UVarOf m)) ('AHyperType t)
  -> Const
       (InferOf t # UVarOf m)
       ((:*:) a (InferResult (UVarOf m)) ('AHyperType t)))
 -> (Ann (a :*: InferResult (UVarOf m)) # t)
 -> Const
      (InferOf t # UVarOf m) (Ann (a :*: InferResult (UVarOf m)) # t))
-> (((InferOf t # UVarOf m)
     -> Const (InferOf t # UVarOf m) (InferOf t # UVarOf m))
    -> (:*:) a (InferResult (UVarOf m)) ('AHyperType t)
    -> Const
         (InferOf t # UVarOf m)
         ((:*:) a (InferResult (UVarOf m)) ('AHyperType t)))
-> Getting
     (InferOf t # UVarOf m)
     (Ann (a :*: InferResult (UVarOf m)) # t)
     (InferOf t # UVarOf m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InferResult (UVarOf m) ('AHyperType t)
 -> Const
      (InferOf t # UVarOf m) (InferResult (UVarOf m) ('AHyperType t)))
-> (:*:) a (InferResult (UVarOf m)) ('AHyperType t)
-> Const
     (InferOf t # UVarOf m)
     ((:*:) a (InferResult (UVarOf m)) ('AHyperType t))
forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 ((InferResult (UVarOf m) ('AHyperType t)
  -> Const
       (InferOf t # UVarOf m) (InferResult (UVarOf m) ('AHyperType t)))
 -> (:*:) a (InferResult (UVarOf m)) ('AHyperType t)
 -> Const
      (InferOf t # UVarOf m)
      ((:*:) a (InferResult (UVarOf m)) ('AHyperType t)))
-> (((InferOf t # UVarOf m)
     -> Const (InferOf t # UVarOf m) (InferOf t # UVarOf m))
    -> InferResult (UVarOf m) ('AHyperType t)
    -> Const
         (InferOf t # UVarOf m) (InferResult (UVarOf m) ('AHyperType t)))
-> ((InferOf t # UVarOf m)
    -> Const (InferOf t # UVarOf m) (InferOf t # UVarOf m))
-> (:*:) a (InferResult (UVarOf m)) ('AHyperType t)
-> Const
     (InferOf t # UVarOf m)
     ((:*:) a (InferResult (UVarOf m)) ('AHyperType t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((InferOf t # UVarOf m)
 -> Const (InferOf t # UVarOf m) (InferOf t # UVarOf m))
-> InferResult (UVarOf m) ('AHyperType t)
-> Const
     (InferOf t # UVarOf m) (InferResult (UVarOf m) ('AHyperType t))
forall (v1 :: HyperType) (e1 :: AHyperType) (v2 :: HyperType)
       (e2 :: AHyperType).
Iso
  (InferResult v1 e1)
  (InferResult v2 e2)
  (InferOf (GetHyperType e1) # v1)
  (InferOf (GetHyperType e2) # v2)
_InferResult)) m (InferredChild
     (UVarOf m) (Ann (a :*: InferResult (UVarOf m))) ('AHyperType t))
-> (m (InferredChild
         (UVarOf m) (Ann (a :*: InferResult (UVarOf m))) ('AHyperType t))
    -> InferChild m (Ann (a :*: InferResult (UVarOf m))) # t)
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
forall a b. a -> (a -> b) -> b
& m (InferredChild
     (UVarOf m) (Ann (a :*: InferResult (UVarOf m))) ('AHyperType t))
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
forall (m :: * -> *) (h :: HyperType) (t :: AHyperType).
m (InferredChild (UVarOf m) h t) -> InferChild m h t
InferChild

type InferResultsConstraint c = Recursively (InferOfConstraint (HNodesHaveConstraint c))

inferUVarsApplyBindings ::
    forall m t a.
    ( Applicative m, RTraversable t, RTraversableInferOf t
    , InferResultsConstraint (Unify m) t
    ) =>
    Ann (a :*: InferResult (UVarOf m)) # t ->
    m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t)
inferUVarsApplyBindings :: (Ann (a :*: InferResult (UVarOf m)) # t)
-> m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t)
inferUVarsApplyBindings =
    (forall (n :: HyperType).
 HWitness (HFlip Ann t) n
 -> ((a :*: InferResult (UVarOf m)) # n)
 -> m ((a :*: InferResult (Pure :*: UVarOf m)) # n))
-> (Ann (a :*: InferResult (UVarOf m)) # t)
-> m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t)
forall (f :: * -> *) (h :: HyperType -> HyperType) (a :: HyperType)
       (p :: HyperType) (q :: HyperType).
(Applicative f, HTraversable (HFlip h a)) =>
(forall (n :: HyperType).
 HWitness (HFlip h a) n -> (p # n) -> f (q # n))
-> (h p # a) -> f (h q # a)
htraverseFlipped ((forall (n :: HyperType).
  HWitness (HFlip Ann t) n
  -> ((a :*: InferResult (UVarOf m)) # n)
  -> m ((a :*: InferResult (Pure :*: UVarOf m)) # n))
 -> (Ann (a :*: InferResult (UVarOf m)) # t)
 -> m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t))
-> (forall (n :: HyperType).
    HWitness (HFlip Ann t) n
    -> ((a :*: InferResult (UVarOf m)) # n)
    -> m ((a :*: InferResult (Pure :*: UVarOf m)) # n))
-> (Ann (a :*: InferResult (UVarOf m)) # t)
-> m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t)
forall a b. (a -> b) -> a -> b
$
    Proxy RTraversableInferOf
forall k (t :: k). Proxy t
Proxy @RTraversableInferOf Proxy RTraversableInferOf
-> (RTraversableInferOf n =>
    HWitness (HFlip Ann t) n
    -> ((a :*: InferResult (UVarOf m)) # n)
    -> m ((a :*: InferResult (Pure :*: UVarOf m)) # n))
-> HWitness (HFlip Ann t) n
-> ((a :*: InferResult (UVarOf m)) # n)
-> m ((a :*: InferResult (Pure :*: UVarOf m)) # 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 (InferResultsConstraint (Unify m))
forall k (t :: k). Proxy t
Proxy @(InferResultsConstraint (Unify m)) Proxy (InferResultsConstraint (Unify m))
-> (InferResultsConstraint (Unify m) n =>
    ((a :*: InferResult (UVarOf m)) # n)
    -> m ((a :*: InferResult (Pure :*: UVarOf m)) # n))
-> HWitness (HFlip Ann t) n
-> ((a :*: InferResult (UVarOf m)) # n)
-> m ((a :*: InferResult (Pure :*: UVarOf m)) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
    ((InferResult (UVarOf m) # n)
 -> m (InferResult (Pure :*: UVarOf m) # n))
-> ((a :*: InferResult (UVarOf m)) # n)
-> m ((a :*: InferResult (Pure :*: UVarOf m)) # n)
forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall (n :: HyperType).
(HTraversable (InferOf n), InferResultsConstraint (Unify m) n) =>
(InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
f
    where
        f ::
            forall n.
            ( HTraversable (InferOf n)
            , InferResultsConstraint (Unify m) n
            ) =>
            InferResult (UVarOf m) # n ->
            m (InferResult (Pure :*: UVarOf m) # n)
        f :: (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
f = Dict
  (InferOfConstraint (HNodesHaveConstraint (Unify m)) n,
   HNodesConstraint n (InferResultsConstraint (Unify m)))
-> ((InferOfConstraint (HNodesHaveConstraint (Unify m)) n,
     HNodesConstraint n (InferResultsConstraint (Unify m))) =>
    (InferResult (UVarOf m) # n)
    -> m (InferResult (Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (InferOfConstraint (HNodesHaveConstraint (Unify m)) n)
-> Dict
     (InferOfConstraint (HNodesHaveConstraint (Unify m)) n,
      HNodesConstraint n (InferResultsConstraint (Unify m)))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (InferOfConstraint (HNodesHaveConstraint (Unify m)) n)
forall k (t :: k). Proxy t
Proxy @(InferOfConstraint (HNodesHaveConstraint (Unify m)) n))) (((InferOfConstraint (HNodesHaveConstraint (Unify m)) n,
   HNodesConstraint n (InferResultsConstraint (Unify m))) =>
  (InferResult (UVarOf m) # n)
  -> m (InferResult (Pure :*: UVarOf m) # n))
 -> (InferResult (UVarOf m) # n)
 -> m (InferResult (Pure :*: UVarOf m) # n))
-> ((InferOfConstraint (HNodesHaveConstraint (Unify m)) n,
     HNodesConstraint n (InferResultsConstraint (Unify m))) =>
    (InferResult (UVarOf m) # n)
    -> m (InferResult (Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall a b. (a -> b) -> a -> b
$
            Dict (HNodesHaveConstraint (Unify m) (InferOf n))
-> (HNodesHaveConstraint (Unify m) (InferOf n) =>
    (InferResult (UVarOf m) # n)
    -> m (InferResult (Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HNodesHaveConstraint (Unify m))
-> Proxy n -> Dict (HNodesHaveConstraint (Unify m) (InferOf n))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy0 :: (HyperType -> Constraint) -> *)
       (proxy1 :: HyperType -> *).
InferOfConstraint c h =>
proxy0 c -> proxy1 h -> Dict (c (InferOf h))
inferOfConstraint (Proxy (HNodesHaveConstraint (Unify m))
forall k (t :: k). Proxy t
Proxy @(HNodesHaveConstraint (Unify m))) (Proxy n
forall k (t :: k). Proxy t
Proxy @n)) ((HNodesHaveConstraint (Unify m) (InferOf n) =>
  (InferResult (UVarOf m) # n)
  -> m (InferResult (Pure :*: UVarOf m) # n))
 -> (InferResult (UVarOf m) # n)
 -> m (InferResult (Pure :*: UVarOf m) # n))
-> (HNodesHaveConstraint (Unify m) (InferOf n) =>
    (InferResult (UVarOf m) # n)
    -> m (InferResult (Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall a b. (a -> b) -> a -> b
$
            Dict (HNodesConstraint (InferOf n) (Unify m))
-> (HNodesConstraint (InferOf n) (Unify m) =>
    (InferResult (UVarOf m) # n)
    -> m (InferResult (Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (Unify m)
-> Proxy (InferOf n)
-> Dict (HNodesConstraint (InferOf n) (Unify m))
forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy0 :: (HyperType -> Constraint) -> *)
       (proxy1 :: HyperType -> *).
HNodesHaveConstraint c h =>
proxy0 c -> proxy1 h -> Dict (HNodesConstraint h c)
hNodesHaveConstraint (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m)) (Proxy (InferOf n)
forall k (t :: k). Proxy t
Proxy @(InferOf n))) ((HNodesConstraint (InferOf n) (Unify m) =>
  (InferResult (UVarOf m) # n)
  -> m (InferResult (Pure :*: UVarOf m) # n))
 -> (InferResult (UVarOf m) # n)
 -> m (InferResult (Pure :*: UVarOf m) # n))
-> (HNodesConstraint (InferOf n) (Unify m) =>
    (InferResult (UVarOf m) # n)
    -> m (InferResult (Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall a b. (a -> b) -> a -> b
$
            (forall (n :: HyperType).
 HWitness (HFlip InferResult n) n
 -> (UVarOf m # n) -> m ((Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall (f :: * -> *) (h :: HyperType -> HyperType) (a :: HyperType)
       (p :: HyperType) (q :: HyperType).
(Applicative f, HTraversable (HFlip h a)) =>
(forall (n :: HyperType).
 HWitness (HFlip h a) n -> (p # n) -> f (q # n))
-> (h p # a) -> f (h q # a)
htraverseFlipped ((forall (n :: HyperType).
  HWitness (HFlip InferResult n) n
  -> (UVarOf m # n) -> m ((Pure :*: UVarOf m) # n))
 -> (InferResult (UVarOf m) # n)
 -> m (InferResult (Pure :*: UVarOf m) # n))
-> (forall (n :: HyperType).
    HWitness (HFlip InferResult n) n
    -> (UVarOf m # n) -> m ((Pure :*: UVarOf m) # n))
-> (InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
forall a b. (a -> b) -> a -> b
$
            Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (UVarOf m # n) -> m ((Pure :*: UVarOf m) # n))
-> HWitness (HFlip InferResult n) n
-> (UVarOf m # n)
-> m ((Pure :*: UVarOf m) # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
            \UVarOf m # n
x -> (UVarOf m # n) -> m (Pure # n)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (Pure # t)
applyBindings UVarOf m # n
x m (Pure # n)
-> ((Pure # n) -> (Pure :*: UVarOf m) # n)
-> m ((Pure :*: UVarOf m) # n)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ((Pure # n) -> (UVarOf m # n) -> (Pure :*: UVarOf m) # n
forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: UVarOf m # n
x)