{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Type schemes
module Hyper.Syntax.Scheme
    ( Scheme (..)
    , sForAlls
    , sTyp
    , W_Scheme (..)
    , QVars (..)
    , _QVars
    , HasScheme (..)
    , loadScheme
    , saveScheme
    , MonadInstantiate (..)
    , inferType
    , QVarInstances (..)
    , _QVarInstances
    , makeQVarInstances
    ) where

import qualified Control.Lens as Lens
import Control.Monad.Trans.Class (MonadTrans (..))
import Control.Monad.Trans.State (StateT (..))
import qualified Data.Map as Map
import Hyper
import Hyper.Class.Optic (HNodeLens (..))
import Hyper.Infer
import Hyper.Recurse
import Hyper.Unify
import Hyper.Unify.Generalize
import Hyper.Unify.New (newTerm)
import Hyper.Unify.QuantifiedVar (HasQuantifiedVar (..), MonadQuantify (..), OrdQVar)
import Hyper.Unify.Term (UTerm (..), uBody)
import Text.PrettyPrint ((<+>))
import qualified Text.PrettyPrint as Pretty
import Text.PrettyPrint.HughesPJClass (Pretty (..), maybeParens)

import Hyper.Internal.Prelude

-- | A type scheme representing a polymorphic type.
data Scheme varTypes typ h = Scheme
    { forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType).
Scheme varTypes typ h -> varTypes # QVars
_sForAlls :: varTypes # QVars
    , forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType).
Scheme varTypes typ h -> h :# typ
_sTyp :: h :# typ
    }
    deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType) x.
Rep (Scheme varTypes typ h) x -> Scheme varTypes typ h
forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType) x.
Scheme varTypes typ h -> Rep (Scheme varTypes typ h) x
$cto :: forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType) x.
Rep (Scheme varTypes typ h) x -> Scheme varTypes typ h
$cfrom :: forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType) x.
Scheme varTypes typ h -> Rep (Scheme varTypes typ h) x
Generic)

newtype QVars typ
    = QVars
        (Map (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
    deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (typ :: AHyperType) x. Rep (QVars typ) x -> QVars typ
forall (typ :: AHyperType) x. QVars typ -> Rep (QVars typ) x
$cto :: forall (typ :: AHyperType) x. Rep (QVars typ) x -> QVars typ
$cfrom :: forall (typ :: AHyperType) x. QVars typ -> Rep (QVars typ) x
Generic)

newtype QVarInstances h typ = QVarInstances (Map (QVar (GetHyperType typ)) (h typ))
    deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (h :: AHyperType -> *) (typ :: AHyperType) x.
Rep (QVarInstances h typ) x -> QVarInstances h typ
forall (h :: AHyperType -> *) (typ :: AHyperType) x.
QVarInstances h typ -> Rep (QVarInstances h typ) x
$cto :: forall (h :: AHyperType -> *) (typ :: AHyperType) x.
Rep (QVarInstances h typ) x -> QVarInstances h typ
$cfrom :: forall (h :: AHyperType -> *) (typ :: AHyperType) x.
QVarInstances h typ -> Rep (QVarInstances h typ) x
Generic)

makeLenses ''Scheme
makePrisms ''QVars
makePrisms ''QVarInstances
makeCommonInstances [''Scheme, ''QVars, ''QVarInstances]
makeHTraversableApplyAndBases ''Scheme

instance RNodes t => RNodes (Scheme v t)
instance (c (Scheme v t), Recursively c t) => Recursively c (Scheme v t)
instance (HTraversable (Scheme v t), RTraversable t) => RTraversable (Scheme v t)

instance
    ( Ord (QVar (GetHyperType typ))
    , Semigroup (TypeConstraintsOf (GetHyperType typ))
    ) =>
    Semigroup (QVars typ)
    where
    QVars Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
m <> :: QVars typ -> QVars typ -> QVars typ
<> QVars Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
n = forall (typ :: AHyperType).
Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars (forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
m Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
n)

instance
    ( Ord (QVar (GetHyperType typ))
    , Semigroup (TypeConstraintsOf (GetHyperType typ))
    ) =>
    Monoid (QVars typ)
    where
    mempty :: QVars typ
mempty = forall (typ :: AHyperType).
Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars forall a. Monoid a => a
mempty

instance
    (Pretty (varTypes # QVars), Pretty (h :# typ)) =>
    Pretty (Scheme varTypes typ h)
    where
    pPrintPrec :: PrettyLevel -> Rational -> Scheme varTypes typ h -> Doc
pPrintPrec PrettyLevel
lvl Rational
p (Scheme varTypes # QVars
forAlls h :# typ
typ)
        | Doc -> Bool
Pretty.isEmpty Doc
f = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
p h :# typ
typ
        | Bool
otherwise = Doc
f Doc -> Doc -> Doc
<+> forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 h :# typ
typ forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p forall a. Ord a => a -> a -> Bool
> Rational
0)
        where
            f :: Doc
f = forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 varTypes # QVars
forAlls

instance
    (Pretty (TypeConstraintsOf typ), Pretty (QVar typ)) =>
    Pretty (QVars # typ)
    where
    pPrint :: (QVars # typ) -> Doc
pPrint (QVars Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
qvars) =
        Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
qvars forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed
            forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
".") forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Doc
Pretty.text String
"∀" forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {a}. (Pretty a, Pretty a) => (a, a) -> Doc
printVar
            forall a b. a -> (a -> b) -> b
& [Doc] -> Doc
Pretty.hsep
        where
            printVar :: (a, a) -> Doc
printVar (a
q, a
c)
                | Doc
cP forall a. Eq a => a -> a -> Bool
== forall a. Monoid a => a
mempty = forall a. Pretty a => a -> Doc
pPrint a
q
                | Bool
otherwise = forall a. Pretty a => a -> Doc
pPrint a
q forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
"(" forall a. Semigroup a => a -> a -> a
<> Doc
cP forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
")"
                where
                    cP :: Doc
cP = forall a. Pretty a => a -> Doc
pPrint a
c

type instance Lens.Index (QVars typ) = QVar (GetHyperType typ)
type instance Lens.IxValue (QVars typ) = TypeConstraintsOf (GetHyperType typ)

instance Ord (QVar (GetHyperType typ)) => Lens.Ixed (QVars typ)

instance Ord (QVar (GetHyperType typ)) => Lens.At (QVars typ) where
    at :: Index (QVars typ)
-> Lens' (QVars typ) (Maybe (IxValue (QVars typ)))
at Index (QVars typ)
h = forall (typ :: AHyperType) (typ :: AHyperType).
Iso
  (QVars typ)
  (QVars typ)
  (Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
  (Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
_QVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at Index (QVars typ)
h

type instance InferOf (Scheme _ t) = HFlip GTerm t

class UnifyGen m t => MonadInstantiate m t where
    localInstantiations ::
        QVarInstances (UVarOf m) # t ->
        m a ->
        m a
    lookupQVar :: QVar t -> m (UVarOf m # t)

instance
    ( HasInferredValue typ
    , UnifyGen m typ
    , HTraversable varTypes
    , HNodesConstraint varTypes (MonadInstantiate m)
    , Infer m typ
    ) =>
    Infer m (Scheme varTypes typ)
    where
    {-# INLINE inferBody #-}
    inferBody :: forall (h :: AHyperType -> *).
(Scheme varTypes typ # InferChild m h)
-> m (Scheme varTypes typ # h,
      InferOf (Scheme varTypes typ) # UVarOf m)
inferBody (Scheme varTypes # QVars
vars 'AHyperType (InferChild m h) :# typ
typ) =
        do
            varTypes # QVarInstances (UVarOf m)
foralls <- 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 (forall {k} (t :: k). Proxy t
Proxy @(MonadInstantiate m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (typ :: AHyperType -> *).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) varTypes # QVars
vars
            let withForalls :: m (InferredChild (UVarOf m) h ('AHyperType typ))
-> m (InferredChild (UVarOf m) h ('AHyperType typ))
withForalls =
                    forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap
                        (forall {k} (t :: k). Proxy t
Proxy @(MonadInstantiate m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (forall a. a -> [a] -> [a]
: []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (t :: AHyperType -> *) a.
MonadInstantiate m t =>
(QVarInstances (UVarOf m) # t) -> m a -> m a
localInstantiations)
                        varTypes # QVarInstances (UVarOf m)
foralls
                        forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall a. a -> a
id
            InferredChild h ('AHyperType typ)
typI InferOf (GetHyperType ('AHyperType typ)) # UVarOf m
typR <- forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild 'AHyperType (InferChild m h) :# typ
typ forall a b. a -> (a -> b) -> b
& m (InferredChild (UVarOf m) h ('AHyperType typ))
-> m (InferredChild (UVarOf m) h ('AHyperType typ))
withForalls
            forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize (InferOf (GetHyperType ('AHyperType typ)) # UVarOf m
typR forall s a. s -> Getting a s a -> a
^. forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredValue t =>
Lens' (InferOf t # v) (v # t)
inferredValue)
                forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType).
(varTypes # QVars) -> (h :# typ) -> Scheme varTypes typ h
Scheme varTypes # QVars
vars h ('AHyperType typ)
typI,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: (AHyperType -> *) -> AHyperType -> *)
       (x :: AHyperType -> *) (h :: AHyperType).
(f (GetHyperType h) # x) -> HFlip f x h
MkHFlip

inferType ::
    ( InferOf t ~ ANode t
    , HNodesConstraint t HasInferredValue
    , MonadInstantiate m t
    ) =>
    t # InferChild m h ->
    m (t # h, InferOf t # UVarOf m)
inferType :: forall (t :: AHyperType -> *) (m :: * -> *) (h :: AHyperType -> *).
(InferOf t ~ ANode t, HNodesConstraint t HasInferredValue,
 MonadInstantiate m t) =>
(t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferType t # InferChild m h
x =
    case t # InferChild m h
x forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar of
        Just QVar t
q -> forall (m :: * -> *) (t :: AHyperType -> *).
MonadInstantiate m t =>
QVar t -> m (UVarOf m # t)
lookupQVar QVar t
q forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar forall t b. AReview t b -> b -> t
# QVar t
q,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: AHyperType -> *) (h :: AHyperType).
(h :# c) -> ANode c h
MkANode
        Maybe (QVar t)
Nothing ->
            do
                t # InferredChild (UVarOf m) h
xI <- 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 (forall a b. a -> b -> a
const forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild) t # InferChild m h
x
                forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall {k} (t :: k). Proxy t
Proxy @HasInferredValue forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (forall s a. s -> Getting a s a -> a
^. forall (v1 :: AHyperType -> *) (h :: AHyperType -> *)
       (t :: AHyperType) (v2 :: AHyperType -> *).
Lens
  (InferredChild v1 h t)
  (InferredChild v2 h t)
  (InferOf (GetHyperType t) # v1)
  (InferOf (GetHyperType t) # v2)
inType forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredValue t =>
Lens' (InferOf t # v) (v # t)
inferredValue)) t # InferredChild (UVarOf m) h
xI
                    forall a b. a -> (a -> b) -> b
& forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
                    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall a b. a -> b -> a
const (forall s a. s -> Getting a s a -> a
^. forall (v :: AHyperType -> *) (h1 :: AHyperType -> *)
       (t :: AHyperType) (h2 :: AHyperType -> *).
Lens (InferredChild v h1 t) (InferredChild v h2 t) (h1 t) (h2 t)
inRep)) t # InferredChild (UVarOf m) h
xI,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: AHyperType -> *) (h :: AHyperType).
(h :# c) -> ANode c h
MkANode

{-# INLINE makeQVarInstances #-}
makeQVarInstances ::
    Unify m typ =>
    QVars # typ ->
    m (QVarInstances (UVarOf m) # typ)
makeQVarInstances :: forall (m :: * -> *) (typ :: AHyperType -> *).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances (QVars Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls) =
    forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem) Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (h :: AHyperType -> *) (typ :: AHyperType).
Map (QVar (GetHyperType typ)) (h typ) -> QVarInstances h typ
QVarInstances

{-# INLINE loadBody #-}
loadBody ::
    ( UnifyGen m typ
    , HNodeLens varTypes typ
    , Ord (QVar typ)
    ) =>
    varTypes # QVarInstances (UVarOf m) ->
    typ # GTerm (UVarOf m) ->
    m (GTerm (UVarOf m) # typ)
loadBody :: forall (m :: * -> *) (typ :: AHyperType -> *)
       (varTypes :: AHyperType -> *).
(UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
(varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # typ)
loadBody varTypes # QVarInstances (UVarOf m)
foralls typ # GTerm (UVarOf m)
x =
    case typ # GTerm (UVarOf m)
x forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QVar typ -> Maybe (UVarOf m ('AHyperType typ))
getForAll of
        Just UVarOf m ('AHyperType typ)
r -> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m ('AHyperType typ)
r forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
        Maybe (UVarOf m ('AHyperType typ))
Nothing ->
            case 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 (forall a b. a -> b -> a
const (forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (v :: AHyperType -> *) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono)) typ # GTerm (UVarOf m)
x of
                Just typ # UVarOf m
xm -> forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
xm forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
                Maybe (typ # UVarOf m)
Nothing -> forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody typ # GTerm (UVarOf m)
x forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a. Applicative f => a -> f a
pure
    where
        getForAll :: QVar typ -> Maybe (UVarOf m ('AHyperType typ))
getForAll QVar typ
v = varTypes # QVarInstances (UVarOf m)
foralls forall s a. s -> Getting (First a) s a -> Maybe a
^? forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (h :: AHyperType -> *) (typ :: AHyperType)
       (h :: AHyperType -> *) (typ :: AHyperType).
Iso
  (QVarInstances h typ)
  (QVarInstances h typ)
  (Map (QVar (GetHyperType typ)) (h typ))
  (Map (QVar (GetHyperType typ)) (h typ))
_QVarInstances forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix QVar typ
v

class
    (UnifyGen m t, HNodeLens varTypes t, Ord (QVar t)) =>
    HasScheme varTypes m t
    where
    hasSchemeRecursive :: Proxy varTypes -> Proxy m -> RecMethod (HasScheme varTypes m) t
    {-# INLINE hasSchemeRecursive #-}
    default hasSchemeRecursive ::
        HNodesConstraint t (HasScheme varTypes m) =>
        Proxy varTypes ->
        Proxy m ->
        RecMethod (HasScheme varTypes m) t
    hasSchemeRecursive Proxy varTypes
_ Proxy m
_ Proxy t
_ = forall (a :: Constraint). a => Dict a
Dict

instance Recursive (HasScheme varTypes m) where
    recurse :: forall (h :: AHyperType -> *) (proxy :: Constraint -> *).
(HNodes h, HasScheme varTypes m h) =>
proxy (HasScheme varTypes m h)
-> Dict (HNodesConstraint h (HasScheme varTypes m))
recurse = forall (varTypes :: AHyperType -> *) (m :: * -> *)
       (t :: AHyperType -> *).
HasScheme varTypes m t =>
Proxy varTypes -> Proxy m -> RecMethod (HasScheme varTypes m) t
hasSchemeRecursive (forall {k} (t :: k). Proxy t
Proxy @varTypes) (forall {k} (t :: k). Proxy t
Proxy @m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (proxy :: Constraint -> *)
       (f :: (AHyperType -> *) -> Constraint) (h :: AHyperType -> *).
proxy (f h) -> Proxy h
proxyArgument

-- | Load scheme into unification monad so that different instantiations share
-- the scheme's monomorphic parts -
-- their unification is O(1) as it is the same shared unification term.
{-# INLINE loadScheme #-}
loadScheme ::
    forall m varTypes typ.
    ( HTraversable varTypes
    , HNodesConstraint varTypes (UnifyGen m)
    , HasScheme varTypes m typ
    ) =>
    Pure # Scheme varTypes typ ->
    m (GTerm (UVarOf m) # typ)
loadScheme :: forall (m :: * -> *) (varTypes :: AHyperType -> *)
       (typ :: AHyperType -> *).
(HTraversable varTypes, HNodesConstraint varTypes (UnifyGen m),
 HasScheme varTypes m typ) =>
(Pure # Scheme varTypes typ) -> m (GTerm (UVarOf m) # typ)
loadScheme (Pure (Scheme varTypes # QVars
vars 'AHyperType Pure :# typ
typ)) =
    do
        varTypes # QVarInstances (UVarOf m)
foralls <- 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 (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (typ :: AHyperType -> *).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) varTypes # QVars
vars
        forall (m :: * -> *) (h :: AHyperType -> *) (w :: AHyperType -> *).
(Monad m, RTraversable h) =>
(forall (n :: AHyperType -> *).
 HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM (forall {k} (t :: k). Proxy t
Proxy @(HasScheme varTypes m) forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (n :: AHyperType -> *) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> forall (m :: * -> *) (typ :: AHyperType -> *)
       (varTypes :: AHyperType -> *).
(UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
(varTypes # QVarInstances (UVarOf m))
-> (typ # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # typ)
loadBody varTypes # QVarInstances (UVarOf m)
foralls) 'AHyperType Pure :# typ
typ

saveH ::
    forall typ varTypes m.
    HasScheme varTypes m typ =>
    GTerm (UVarOf m) # typ ->
    StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH :: forall (typ :: AHyperType -> *) (varTypes :: AHyperType -> *)
       (m :: * -> *).
HasScheme varTypes m typ =>
(GTerm (UVarOf m) # typ)
-> StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH (GBody 'AHyperType typ :# GTerm (UVarOf m)
x) =
    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 (forall {k} (t :: k). Proxy t
Proxy @(HasScheme varTypes m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (typ :: AHyperType -> *) (varTypes :: AHyperType -> *)
       (m :: * -> *).
HasScheme varTypes m typ =>
(GTerm (UVarOf m) # typ)
-> StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH) 'AHyperType typ :# GTerm (UVarOf m)
x
        forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall (h :: AHyperType -> *) (j :: AHyperType -> *).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure forall t b. AReview t b -> b -> t
#)
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (varTypes :: AHyperType -> *) (m :: * -> *)
       (t :: AHyperType -> *).
HasScheme varTypes m t =>
Proxy varTypes -> Proxy m -> RecMethod (HasScheme varTypes m) t
hasSchemeRecursive (forall {k} (t :: k). Proxy t
Proxy @varTypes) (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @typ)
saveH (GMono UVarOf m ('AHyperType typ)
x) =
    forall (m :: * -> *) (h :: AHyperType -> *) (w :: AHyperType -> *).
(Monad m, RTraversable h) =>
(forall (n :: AHyperType -> *).
 HRecWitness h n -> (w # n) -> m (n # w))
-> (w # h) -> m (Pure # h)
unwrapM (forall {k} (t :: k). Proxy t
Proxy @(HasScheme varTypes m) forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (n :: AHyperType -> *) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> forall {f :: * -> *} {t :: AHyperType -> *}.
Unify f t =>
(UVarOf f # t) -> f (t # UVarOf f)
f) UVarOf m ('AHyperType typ)
x forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
    where
        f :: (UVarOf f # t) -> f (t # UVarOf f)
f UVarOf f # t
v =
            forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf f # t
v
                forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
                    (UVarOf f # t
_, UTerm UTermBody (UVarOf f) ('AHyperType t)
t) -> UTermBody (UVarOf f) ('AHyperType t)
t forall s a. s -> Getting a s a -> a
^. forall (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody
                    (UVarOf f # t
_, UUnbound{}) -> forall a. HasCallStack => String -> a
error String
"saveScheme of non-toplevel scheme!"
                    (UVarOf f # t, UTerm (UVarOf f) ('AHyperType t))
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at saveScheme of monomorphic part"
saveH (GPoly UVarOf m ('AHyperType typ)
x) =
    forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m ('AHyperType typ)
x
        forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            USkolem TypeConstraintsOf (GetHyperType ('AHyperType typ))
l ->
                do
                    QVar typ
r <-
                        forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @typ)
                            forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf (GetHyperType ('AHyperType typ))
l)
                            forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall typeConstraints q (m :: * -> *).
MonadQuantify typeConstraints q m =>
typeConstraints -> m q
newQuantifiedVariable
                            forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                    forall s t a b. Field1 s t a b => Lens s t a b
Lens._1
                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens
                        forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (\QVars # typ
v -> QVars # typ
v forall a b. a -> (a -> b) -> b
& forall (typ :: AHyperType) (typ :: AHyperType).
Iso
  (QVars typ)
  (QVars typ)
  (Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
  (Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
_QVars forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at QVar typ
r forall s t a b. ASetter s t a (Maybe b) -> b -> s -> t
?~ forall c. TypeConstraints c => c -> c
generalizeConstraints TypeConstraintsOf (GetHyperType ('AHyperType typ))
l :: QVars # typ)
                    forall s t a b. Field2 s t a b => Lens s t a b
Lens._2 forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m ('AHyperType typ)
x (forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType typ))
l) forall a. a -> [a] -> [a]
:)
                    let result :: Pure # typ
result = forall (h :: AHyperType -> *) (j :: AHyperType -> *).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar forall t b. AReview t b -> b -> t
# QVar typ
r
                    forall (v :: AHyperType -> *) (ast :: AHyperType).
Pure ast -> UTerm v ast
UResolved Pure # typ
result forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m ('AHyperType typ)
x forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                    forall (f :: * -> *) a. Applicative f => a -> f a
pure Pure # typ
result
            UResolved Pure # typ
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Pure # typ
v
            UTerm (UVarOf m) # typ
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at saveScheme's forall"

saveScheme ::
    ( HNodesConstraint varTypes OrdQVar
    , HPointed varTypes
    , HasScheme varTypes m typ
    ) =>
    GTerm (UVarOf m) # typ ->
    m (Pure # Scheme varTypes typ)
saveScheme :: forall (varTypes :: AHyperType -> *) (m :: * -> *)
       (typ :: AHyperType -> *).
(HNodesConstraint varTypes OrdQVar, HPointed varTypes,
 HasScheme varTypes m typ) =>
(GTerm (UVarOf m) # typ) -> m (Pure # Scheme varTypes typ)
saveScheme GTerm (UVarOf m) # typ
x =
    do
        (Pure # typ
t, (varTypes # QVars
v, [m ()]
recover)) <-
            forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
                (forall (typ :: AHyperType -> *) (varTypes :: AHyperType -> *)
       (m :: * -> *).
HasScheme varTypes m typ =>
(GTerm (UVarOf m) # typ)
-> StateT (varTypes # QVars, [m ()]) m (Pure # typ)
saveH GTerm (UVarOf m) # typ
x)
                ( forall (h :: AHyperType -> *) (p :: AHyperType -> *).
HPointed h =>
(forall (n :: AHyperType -> *). HWitness h n -> p # n) -> h # p
hpure (forall {k} (t :: k). Proxy t
Proxy @OrdQVar forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (typ :: AHyperType).
Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars forall a. Monoid a => a
mempty)
                , []
                )
        forall (h :: AHyperType -> *) (j :: AHyperType -> *).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure forall t b. AReview t b -> b -> t
# forall (varTypes :: AHyperType -> *) (typ :: AHyperType -> *)
       (h :: AHyperType).
(varTypes # QVars) -> (h :# typ) -> Scheme varTypes typ h
Scheme varTypes # QVars
v Pure # typ
t forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover