-- | Type schemes

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

module Hyper.Type.AST.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
    { Scheme varTypes typ h -> varTypes # QVars
_sForAlls :: varTypes # QVars
    , Scheme varTypes typ h -> h :# typ
_sTyp :: h :# typ
    } deriving (forall x. Scheme varTypes typ h -> Rep (Scheme varTypes typ h) x)
-> (forall x.
    Rep (Scheme varTypes typ h) x -> Scheme varTypes typ h)
-> Generic (Scheme varTypes typ h)
forall x. Rep (Scheme varTypes typ h) x -> Scheme varTypes typ h
forall x. Scheme varTypes typ h -> Rep (Scheme varTypes typ h) x
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 x. QVars typ -> Rep (QVars typ) x)
-> (forall x. Rep (QVars typ) x -> QVars typ)
-> Generic (QVars typ)
forall x. Rep (QVars typ) x -> QVars typ
forall x. QVars typ -> Rep (QVars typ) x
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 x. QVarInstances h typ -> Rep (QVarInstances h typ) x)
-> (forall x. Rep (QVarInstances h typ) x -> QVarInstances h typ)
-> Generic (QVarInstances h typ)
forall x. Rep (QVarInstances h typ) x -> QVarInstances h typ
forall x. QVarInstances h typ -> Rep (QVarInstances h typ) x
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 (RTraversable t, RTraversableInferOf t) => RTraversableInferOf (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 = Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
forall (typ :: AHyperType).
Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars ((TypeConstraintsOf (GetHyperType typ)
 -> TypeConstraintsOf (GetHyperType typ)
 -> TypeConstraintsOf (GetHyperType typ))
-> Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith TypeConstraintsOf (GetHyperType typ)
-> TypeConstraintsOf (GetHyperType typ)
-> TypeConstraintsOf (GetHyperType typ)
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 = Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
forall (typ :: AHyperType).
Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
-> QVars typ
QVars Map
  (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
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 = PrettyLevel -> Rational -> (h :# typ) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
p h :# typ
typ
        | Bool
otherwise = Doc
f Doc -> Doc -> Doc
<+> PrettyLevel -> Rational -> (h :# typ) -> Doc
forall a. Pretty a => PrettyLevel -> Rational -> a -> Doc
pPrintPrec PrettyLevel
lvl Rational
0 h :# typ
typ Doc -> (Doc -> Doc) -> Doc
forall a b. a -> (a -> b) -> b
& Bool -> Doc -> Doc
maybeParens (Rational
p Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
> Rational
0)
        where
            f :: Doc
f = PrettyLevel -> Rational -> (varTypes # QVars) -> Doc
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 typ) (TypeConstraintsOf typ)
Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
qvars Map (QVar typ) (TypeConstraintsOf typ)
-> IndexedGetting
     (QVar typ)
     (Endo [(QVar typ, TypeConstraintsOf typ)])
     (Map (QVar typ) (TypeConstraintsOf typ))
     (TypeConstraintsOf typ)
-> [(QVar typ, TypeConstraintsOf typ)]
forall s i a. s -> IndexedGetting i (Endo [(i, a)]) s a -> [(i, a)]
^@.. IndexedGetting
  (QVar typ)
  (Endo [(QVar typ, TypeConstraintsOf typ)])
  (Map (QVar typ) (TypeConstraintsOf typ))
  (TypeConstraintsOf typ)
forall i (t :: * -> *) a b.
TraversableWithIndex i t =>
IndexedTraversal i (t a) (t b) a b
Lens.itraversed
        [(QVar typ, TypeConstraintsOf typ)]
-> ((QVar typ, TypeConstraintsOf typ) -> Doc) -> [Doc]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (QVar typ, TypeConstraintsOf typ) -> Doc
forall a a. (Pretty a, Pretty a) => (a, a) -> Doc
printVar
        [Doc] -> (Doc -> Doc) -> [Doc]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (String -> Doc
Pretty.text String
"∀" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>) [Doc] -> (Doc -> Doc) -> [Doc]
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
".") [Doc] -> ([Doc] -> Doc) -> Doc
forall a b. a -> (a -> b) -> b
& [Doc] -> Doc
Pretty.hsep
        where
            printVar :: (a, a) -> Doc
printVar (a
q, a
c)
                | Doc
cP Doc -> Doc -> Bool
forall a. Eq a => a -> a -> Bool
== Doc
forall a. Monoid a => a
mempty = a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
q
                | Bool
otherwise = a -> Doc
forall a. Pretty a => a -> Doc
pPrint a
q Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
"(" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
cP Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
Pretty.text String
")"
                where
                    cP :: Doc
cP = a -> Doc
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 = (Map
   (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
 -> f (Map
         (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))))
-> QVars typ -> f (QVars typ)
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 ((Map
    (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
  -> f (Map
          (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))))
 -> QVars typ -> f (QVars typ))
-> ((Maybe (TypeConstraintsOf (GetHyperType typ))
     -> f (Maybe (TypeConstraintsOf (GetHyperType typ))))
    -> Map
         (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))
    -> f (Map
            (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ))))
-> (Maybe (TypeConstraintsOf (GetHyperType typ))
    -> f (Maybe (TypeConstraintsOf (GetHyperType typ))))
-> QVars typ
-> f (QVars typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index
  (Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
-> Lens'
     (Map
        (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
     (Maybe
        (IxValue
           (Map
              (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))))
forall m. At m => Index m -> Lens' m (Maybe (IxValue m))
Lens.at Index
  (Map
     (QVar (GetHyperType typ)) (TypeConstraintsOf (GetHyperType typ)))
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
    ( Monad m
    , HasInferredValue typ
    , UnifyGen m typ
    , HTraversable varTypes
    , HNodesConstraint varTypes (MonadInstantiate m)
    , RTraversable typ
    , Infer m typ
    ) =>
    Infer m (Scheme varTypes typ) where

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

inferType ::
    ( InferOf t ~ ANode t
    , HTraversable t
    , HNodesConstraint t HasInferredValue
    , UnifyGen m t
    , MonadInstantiate m t
    ) =>
    t # InferChild m h ->
    m (t # h, InferOf t # UVarOf m)
inferType :: (t # InferChild m h) -> m (t # h, InferOf t # UVarOf m)
inferType t # InferChild m h
x =
    case t # InferChild m h
x (t # InferChild m h)
-> Getting (First (QVar t)) (t # InferChild m h) (QVar t)
-> Maybe (QVar t)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First (QVar t)) (t # InferChild m h) (QVar t)
forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar of
    Just QVar t
q -> QVar t -> m (UVarOf m ('AHyperType t))
forall (m :: * -> *) (t :: AHyperType -> *).
MonadInstantiate m t =>
QVar t -> m (UVarOf m # t)
lookupQVar QVar t
q m (UVarOf m ('AHyperType t))
-> (UVarOf m ('AHyperType t)
    -> (t # h, ANode t ('AHyperType (UVarOf m))))
-> m (t # h, ANode t ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Tagged (QVar t) (Identity (QVar t))
-> Tagged (t # h) (Identity (t # h))
forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar (Tagged (QVar t) (Identity (QVar t))
 -> Tagged (t # h) (Identity (t # h)))
-> QVar t -> t # h
forall t b. AReview t b -> b -> t
# QVar t
q, ) (ANode t ('AHyperType (UVarOf m))
 -> (t # h, ANode t ('AHyperType (UVarOf m))))
-> (UVarOf m ('AHyperType t) -> ANode t ('AHyperType (UVarOf m)))
-> UVarOf m ('AHyperType t)
-> (t # h, ANode t ('AHyperType (UVarOf m)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UVarOf m ('AHyperType t) -> ANode t ('AHyperType (UVarOf m))
forall (c :: AHyperType -> *) (h :: AHyperType).
(h :# c) -> ANode c h
MkANode
    Maybe (QVar t)
Nothing ->
        do
            t # InferredChild (UVarOf m) h
xI <- (forall (n :: AHyperType -> *).
 HWitness t n
 -> (InferChild m h # n) -> m (InferredChild (UVarOf m) h # n))
-> (t # InferChild m h) -> m (t # InferredChild (UVarOf m) h)
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 (((InferChild m h # n) -> m (InferredChild (UVarOf m) h # n))
-> HWitness t n
-> (InferChild m h # n)
-> m (InferredChild (UVarOf m) h # n)
forall a b. a -> b -> a
const (InferChild m h # n) -> m (InferredChild (UVarOf m) h # n)
forall (m :: * -> *) (h :: AHyperType -> *) (t :: AHyperType).
InferChild m h t -> m (InferredChild (UVarOf m) h t)
inferChild) t # InferChild m h
x
            (forall (n :: AHyperType -> *).
 HWitness t n -> (InferredChild (UVarOf m) h # n) -> UVarOf m # n)
-> (t # InferredChild (UVarOf m) h) -> t # UVarOf m
forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (Proxy HasInferredValue
forall k (t :: k). Proxy t
Proxy @HasInferredValue Proxy HasInferredValue
-> (HasInferredValue n =>
    (InferredChild (UVarOf m) h # n) -> UVarOf m # n)
-> HWitness t n
-> (InferredChild (UVarOf m) h # n)
-> UVarOf m # n
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> ((InferredChild (UVarOf m) h # n)
-> Getting
     (UVarOf m # n) (InferredChild (UVarOf m) h # n) (UVarOf m # n)
-> UVarOf m # n
forall s a. s -> Getting a s a -> a
^. (InferOf n ('AHyperType (UVarOf m))
 -> Const (UVarOf m # n) (InferOf n ('AHyperType (UVarOf m))))
-> (InferredChild (UVarOf m) h # n)
-> Const (UVarOf m # n) (InferredChild (UVarOf m) h # n)
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 ((InferOf n ('AHyperType (UVarOf m))
  -> Const (UVarOf m # n) (InferOf n ('AHyperType (UVarOf m))))
 -> (InferredChild (UVarOf m) h # n)
 -> Const (UVarOf m # n) (InferredChild (UVarOf m) h # n))
-> (((UVarOf m # n) -> Const (UVarOf m # n) (UVarOf m # n))
    -> InferOf n ('AHyperType (UVarOf m))
    -> Const (UVarOf m # n) (InferOf n ('AHyperType (UVarOf m))))
-> Getting
     (UVarOf m # n) (InferredChild (UVarOf m) h # n) (UVarOf m # n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((UVarOf m # n) -> Const (UVarOf m # n) (UVarOf m # n))
-> InferOf n ('AHyperType (UVarOf m))
-> Const (UVarOf m # n) (InferOf n ('AHyperType (UVarOf m)))
forall (t :: AHyperType -> *) (v :: AHyperType -> *).
HasInferredValue t =>
Lens' (InferOf t # v) (v # t)
inferredValue)) t # InferredChild (UVarOf m) h
xI
                (t # UVarOf m)
-> ((t # UVarOf m) -> m (UVarOf m ('AHyperType t)))
-> m (UVarOf m ('AHyperType t))
forall a b. a -> (a -> b) -> b
& (t # UVarOf m) -> m (UVarOf m ('AHyperType t))
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
                m (UVarOf m ('AHyperType t))
-> (UVarOf m ('AHyperType t)
    -> (t # h, ANode t ('AHyperType (UVarOf m))))
-> m (t # h, ANode t ('AHyperType (UVarOf m)))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ((forall (n :: AHyperType -> *).
 HWitness t n -> (InferredChild (UVarOf m) h # n) -> h # n)
-> (t # InferredChild (UVarOf m) h) -> t # h
forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap ((InferredChild (UVarOf m) h ('AHyperType n) -> h ('AHyperType n))
-> HWitness t n
-> InferredChild (UVarOf m) h ('AHyperType n)
-> h ('AHyperType n)
forall a b. a -> b -> a
const (InferredChild (UVarOf m) h ('AHyperType n)
-> Getting
     (h ('AHyperType n))
     (InferredChild (UVarOf m) h ('AHyperType n))
     (h ('AHyperType n))
-> h ('AHyperType n)
forall s a. s -> Getting a s a -> a
^. Getting
  (h ('AHyperType n))
  (InferredChild (UVarOf m) h ('AHyperType n))
  (h ('AHyperType n))
forall (v1 :: AHyperType -> *) (h :: AHyperType -> *)
       (t :: AHyperType) (h2 :: AHyperType -> *).
Lens (InferredChild v1 h t) (InferredChild v1 h2 t) (h t) (h2 t)
inRep)) t # InferredChild (UVarOf m) h
xI, ) (ANode t ('AHyperType (UVarOf m))
 -> (t # h, ANode t ('AHyperType (UVarOf m))))
-> (UVarOf m ('AHyperType t) -> ANode t ('AHyperType (UVarOf m)))
-> UVarOf m ('AHyperType t)
-> (t # h, ANode t ('AHyperType (UVarOf m)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UVarOf m ('AHyperType t) -> ANode t ('AHyperType (UVarOf m))
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 :: (QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances (QVars Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls) =
    (TypeConstraintsOf typ -> m (UVarOf m # typ))
-> Map (QVar typ) (TypeConstraintsOf typ)
-> m (Map (QVar typ) (UVarOf m # typ))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (BindingDict (UVarOf m) m typ
-> (UTerm (UVarOf m) # typ) -> m (UVarOf m # typ)
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m typ
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding ((UTerm (UVarOf m) # typ) -> m (UVarOf m # typ))
-> (TypeConstraintsOf typ -> UTerm (UVarOf m) # typ)
-> TypeConstraintsOf typ
-> m (UVarOf m # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf typ -> UTerm (UVarOf m) # typ
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem) Map (QVar typ) (TypeConstraintsOf typ)
Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls m (Map (QVar typ) (UVarOf m # typ))
-> (Map (QVar typ) (UVarOf m # typ)
    -> QVarInstances (UVarOf m) # typ)
-> m (QVarInstances (UVarOf m) # typ)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Map (QVar typ) (UVarOf m # typ) -> QVarInstances (UVarOf m) # typ
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 :: (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 (typ # GTerm (UVarOf m))
-> Getting (First (QVar typ)) (typ # GTerm (UVarOf m)) (QVar typ)
-> Maybe (QVar typ)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First (QVar typ)) (typ # GTerm (UVarOf m)) (QVar typ)
forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar Maybe (QVar typ)
-> (QVar typ -> Maybe (UVarOf m ('AHyperType typ)))
-> Maybe (UVarOf m ('AHyperType typ))
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 -> UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m ('AHyperType typ)
r (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ))
-> m (GTerm (UVarOf m) # typ)
forall a b. a -> (a -> b) -> b
& (GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    Maybe (UVarOf m ('AHyperType typ))
Nothing ->
        case (forall (n :: AHyperType -> *).
 HWitness typ n -> (GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n))
-> (typ # GTerm (UVarOf m)) -> Maybe (typ # UVarOf 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 (((GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n))
-> HWitness typ n -> (GTerm (UVarOf m) # n) -> Maybe (UVarOf m # n)
forall a b. a -> b -> a
const ((GTerm (UVarOf m) # n)
-> Getting
     (First (UVarOf m # n)) (GTerm (UVarOf m) # n) (UVarOf m # n)
-> Maybe (UVarOf m # n)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting
  (First (UVarOf m # n)) (GTerm (UVarOf m) # n) (UVarOf m # n)
forall (v :: AHyperType -> *) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono)) typ # GTerm (UVarOf m)
x of
        Just typ # UVarOf m
xm -> (typ # UVarOf m) -> m (UVarOf m ('AHyperType typ))
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
xm m (UVarOf m ('AHyperType typ))
-> (UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ)
-> m (GTerm (UVarOf m) # typ)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> UVarOf m ('AHyperType typ) -> GTerm (UVarOf m) # typ
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
        Maybe (typ # UVarOf m)
Nothing -> ('AHyperType typ :# GTerm (UVarOf m)) -> GTerm (UVarOf m) # typ
forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody typ # GTerm (UVarOf m)
'AHyperType typ :# GTerm (UVarOf m)
x (GTerm (UVarOf m) # typ)
-> ((GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ))
-> m (GTerm (UVarOf m) # typ)
forall a b. a -> (a -> b) -> b
& (GTerm (UVarOf m) # typ) -> m (GTerm (UVarOf m) # typ)
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 (varTypes # QVarInstances (UVarOf m))
-> Getting
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m ('AHyperType typ))
-> Maybe (UVarOf m ('AHyperType typ))
forall s a. s -> Getting (First a) s a -> Maybe a
^? ((QVarInstances (UVarOf m) # typ)
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((QVarInstances (UVarOf m) # typ)
  -> Const
       (First (UVarOf m ('AHyperType typ)))
       (QVarInstances (UVarOf m) # typ))
 -> (varTypes # QVarInstances (UVarOf m))
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (varTypes # QVarInstances (UVarOf m)))
-> ((UVarOf m ('AHyperType typ)
     -> Const
          (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
    -> (QVarInstances (UVarOf m) # typ)
    -> Const
         (First (UVarOf m ('AHyperType typ)))
         (QVarInstances (UVarOf m) # typ))
-> Getting
     (First (UVarOf m ('AHyperType typ)))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m ('AHyperType typ))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (QVar typ) (UVarOf m ('AHyperType typ))
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (QVarInstances (UVarOf m) # typ)
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (QVarInstances (UVarOf m) # typ)
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 ((Map (QVar typ) (UVarOf m ('AHyperType typ))
  -> Const
       (First (UVarOf m ('AHyperType typ)))
       (Map (QVar typ) (UVarOf m ('AHyperType typ))))
 -> (QVarInstances (UVarOf m) # typ)
 -> Const
      (First (UVarOf m ('AHyperType typ)))
      (QVarInstances (UVarOf m) # typ))
-> ((UVarOf m ('AHyperType typ)
     -> Const
          (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
    -> Map (QVar typ) (UVarOf m ('AHyperType typ))
    -> Const
         (First (UVarOf m ('AHyperType typ)))
         (Map (QVar typ) (UVarOf m ('AHyperType typ))))
-> (UVarOf m ('AHyperType typ)
    -> Const
         (First (UVarOf m ('AHyperType typ))) (UVarOf m ('AHyperType typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const
     (First (UVarOf m ('AHyperType typ)))
     (QVarInstances (UVarOf m) # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
-> Traversal'
     (Map (QVar typ) (UVarOf m ('AHyperType typ)))
     (IxValue (Map (QVar typ) (UVarOf m ('AHyperType typ))))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
Lens.ix Index (Map (QVar typ) (UVarOf m ('AHyperType typ)))
QVar typ
v

class
    (UnifyGen m t, HNodeLens varTypes t, Ord (QVar t)) =>
    HasScheme varTypes m t where

    hasSchemeRecursive ::
        Proxy varTypes -> Proxy m -> Proxy t ->
        Dict (HNodesConstraint t (HasScheme varTypes m))
    {-# INLINE hasSchemeRecursive #-}
    default hasSchemeRecursive ::
        HNodesConstraint t (HasScheme varTypes m) =>
        Proxy varTypes -> Proxy m -> Proxy t ->
        Dict (HNodesConstraint t (HasScheme varTypes m))
    hasSchemeRecursive Proxy varTypes
_ Proxy m
_ Proxy t
_ = Dict (HNodesConstraint t (HasScheme varTypes m))
forall (a :: Constraint). a => Dict a
Dict

instance Recursive (HasScheme varTypes m) where
    recurse :: proxy (HasScheme varTypes m h)
-> Dict (HNodesConstraint h (HasScheme varTypes m))
recurse = Proxy varTypes
-> Proxy m
-> Proxy h
-> Dict (HNodesConstraint h (HasScheme varTypes m))
forall (varTypes :: AHyperType -> *) (m :: * -> *)
       (t :: AHyperType -> *).
HasScheme varTypes m t =>
Proxy varTypes
-> Proxy m
-> Proxy t
-> Dict (HNodesConstraint t (HasScheme varTypes m))
hasSchemeRecursive (Proxy varTypes
forall k (t :: k). Proxy t
Proxy @varTypes) (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy h -> Dict (HNodesConstraint h (HasScheme varTypes m)))
-> (proxy (HasScheme varTypes m h) -> Proxy h)
-> proxy (HasScheme varTypes m h)
-> Dict (HNodesConstraint h (HasScheme varTypes m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy (HasScheme varTypes m h) -> Proxy h
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.
    ( Monad m
    , HTraversable varTypes
    , HNodesConstraint varTypes (UnifyGen m)
    , HasScheme varTypes m typ
    ) =>
    Pure # Scheme varTypes typ ->
    m (GTerm (UVarOf m) # typ)
loadScheme :: (Pure # Scheme varTypes typ) -> m (GTerm (UVarOf m) # typ)
loadScheme (Pure (Scheme vars typ)) =
    do
        varTypes # QVarInstances (UVarOf m)
foralls <- (forall (n :: AHyperType -> *).
 HWitness varTypes n
 -> (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> (varTypes # QVars) -> m (varTypes # QVarInstances (UVarOf 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 (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n =>
    (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness varTypes n
-> (QVars # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> UnifyGen m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n)
forall (m :: * -> *) (typ :: AHyperType -> *).
Unify m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstances) varTypes # QVars
vars
        (forall (n :: AHyperType -> *).
 HRecWitness typ n
 -> (n # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # n))
-> (Pure # typ) -> m (GTerm (UVarOf m) # typ)
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 (Proxy (HasScheme varTypes m)
forall k (t :: k). Proxy t
Proxy @(HasScheme varTypes m) Proxy (HasScheme varTypes m)
-> (HasScheme varTypes m n =>
    (n # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # n))
-> HRecWitness typ n
-> (n # GTerm (UVarOf m))
-> m (GTerm (UVarOf m) # n)
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (n :: AHyperType -> *) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> (varTypes # QVarInstances (UVarOf m))
-> (n # GTerm (UVarOf m)) -> m (GTerm (UVarOf m) # n)
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
Pure # typ
typ

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