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