{-# 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 (UVarOf, Unify, 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 :: forall (m :: * -> *) (t :: HyperType) (a :: HyperType).
Infer m t =>
(Ann a # t) -> m (Ann (a :*: InferResult (UVarOf m)) # t)
infer (Ann a ('AHyperType t)
a 'AHyperType t :# Ann a
x) =
    forall (m :: * -> *) (t :: HyperType) (h :: HyperType).
Infer m t =>
(t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferBody (forall (h :: HyperType) (p :: HyperType) (q :: HyperType).
HFunctor h =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall {k} (t :: k). Proxy t
Proxy @(Infer m) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (t :: HyperType) (a :: HyperType).
Infer m t =>
(Ann a # t)
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
inferH) 'AHyperType t :# Ann a
x)
        forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (\(t # Ann (a :*: InferResult (UVarOf m))
xI, InferOf t # UVarOf m
t) -> forall (a :: HyperType) (h :: AHyperType).
a h -> (h :# Ann a) -> Ann a h
Ann (a ('AHyperType t)
a forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: forall (v :: HyperType) (e :: AHyperType).
(InferOf (GetHyperType e) # v) -> InferResult v e
InferResult InferOf t # UVarOf m
t) t # Ann (a :*: InferResult (UVarOf m))
xI)
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ 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 (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @t)

{-# INLINE inferH #-}
inferH ::
    Infer m t =>
    Ann a # t ->
    InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
inferH :: forall (m :: * -> *) (t :: HyperType) (a :: HyperType).
Infer m t =>
(Ann a # t)
-> InferChild m (Ann (a :*: InferResult (UVarOf m))) # t
inferH Ann a # t
c = forall (m :: * -> *) (t :: HyperType) (a :: HyperType).
Infer m t =>
(Ann a # t) -> m (Ann (a :*: InferResult (UVarOf m)) # t)
infer Ann a # t
c forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (\Ann (a :*: InferResult (UVarOf m)) ('AHyperType t)
i -> forall (v :: HyperType) (h :: HyperType) (t :: AHyperType).
h t -> (InferOf (GetHyperType t) # v) -> InferredChild v h t
InferredChild Ann (a :*: InferResult (UVarOf m)) ('AHyperType t)
i (Ann (a :*: InferResult (UVarOf m)) ('AHyperType t)
i forall s a. s -> Getting a s a -> a
^. forall (a :: HyperType) (h :: AHyperType). Lens' (Ann a h) (a h)
hAnn forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)) forall a b. a -> (a -> b) -> b
& 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
    , Recursively (InferOfConstraint HTraversable) t
    , InferResultsConstraint (Unify m) t
    ) =>
    Ann (a :*: InferResult (UVarOf m)) # t ->
    m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t)
inferUVarsApplyBindings :: forall (m :: * -> *) (t :: HyperType) (a :: HyperType).
(Applicative m, RTraversable t,
 Recursively (InferOfConstraint HTraversable) t,
 InferResultsConstraint (Unify m) t) =>
(Ann (a :*: InferResult (UVarOf m)) # t)
-> m (Ann (a :*: InferResult (Pure :*: UVarOf m)) # t)
inferUVarsApplyBindings =
    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 a b. (a -> b) -> a -> b
$
        forall {k} (t :: k). Proxy t
Proxy @(Recursively (InferOfConstraint HTraversable)) 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
#*#
            forall {k} (t :: k). Proxy t
Proxy @(InferResultsConstraint (Unify m)) forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 forall (n :: HyperType).
(Recursively (InferOfConstraint HTraversable) n,
 InferResultsConstraint (Unify m) n) =>
(InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
f
    where
        f ::
            forall n.
            ( Recursively (InferOfConstraint HTraversable) n
            , InferResultsConstraint (Unify m) n
            ) =>
            InferResult (UVarOf m) # n ->
            m (InferResult (Pure :*: UVarOf m) # n)
        f :: forall (n :: HyperType).
(Recursively (InferOfConstraint HTraversable) n,
 InferResultsConstraint (Unify m) n) =>
(InferResult (UVarOf m) # n)
-> m (InferResult (Pure :*: UVarOf m) # n)
f =
            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 {k} (t :: k). Proxy t
Proxy @(Unify m) 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 -> forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (Pure # t)
applyBindings UVarOf m # n
x forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall k (f :: k -> *) (g :: k -> *) (p :: k).
f p -> g p -> (:*:) f g p
:*: UVarOf m # n
x))
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: HyperType -> *).
InferOfConstraint c h =>
proxy h -> Dict (c (InferOf h))
inferOfConstraint @HTraversable (forall {k} (t :: k). Proxy t
Proxy @n)
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(InferOfConstraint HTraversable n))
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy0 :: (HyperType -> Constraint) -> *)
       (proxy1 :: HyperType -> *).
HNodesHaveConstraint c h =>
proxy0 c -> proxy1 h -> Dict (HNodesConstraint h c)
hNodesHaveConstraint (forall {k} (t :: k). Proxy t
Proxy @(Unify m)) (forall {k} (t :: k). Proxy t
Proxy @(InferOf n))
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: HyperType -> *).
InferOfConstraint c h =>
proxy h -> Dict (c (InferOf h))
inferOfConstraint @(HNodesHaveConstraint (Unify m)) (forall {k} (t :: k). Proxy t
Proxy @n)
                forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: HyperType -> Constraint) (h :: HyperType)
       (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(InferOfConstraint (HNodesHaveConstraint (Unify m)) n))