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

-- | Generalization of type schemes
module Hyper.Unify.Generalize
    ( generalize
    , instantiate
    , GTerm (..)
    , _GMono
    , _GPoly
    , _GBody
    , W_GTerm (..)
    , instantiateWith
    , instantiateForAll
      -- | Exports for @SPECIALIZE@ pragmas.
    , instantiateH
    ) where

import Algebra.PartialOrd (PartialOrd (..))
import qualified Control.Lens as Lens
import Control.Monad.Trans.Class (MonadTrans (..))
import Control.Monad.Trans.Writer (WriterT (..), tell)
import Data.Monoid (All (..))
import Hyper
import Hyper.Class.Traversable
import Hyper.Class.Unify
import Hyper.Recurse
import Hyper.Unify.Constraints
import Hyper.Unify.New (newTerm)
import Hyper.Unify.Term (UTerm (..), uBody)

import Hyper.Internal.Prelude

-- | An efficient representation of a type scheme arising from
-- generalizing a unification term. Type subexpressions which are
-- completely monomoprhic are tagged as such, to avoid redundant
-- instantation and unification work
data GTerm v ast
    = -- | Completely monomoprhic term
      GMono (v ast)
    | -- | Points to a quantified variable (instantiation will
      -- create fresh unification terms) (`Hyper.Unify.Term.USkolem`
      -- or `Hyper.Unify.Term.UResolved`)
      GPoly (v ast)
    | -- | Term with some polymorphic parts
      GBody (ast :# GTerm v)
    deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (v :: AHyperType -> *) (ast :: AHyperType) x.
Rep (GTerm v ast) x -> GTerm v ast
forall (v :: AHyperType -> *) (ast :: AHyperType) x.
GTerm v ast -> Rep (GTerm v ast) x
$cto :: forall (v :: AHyperType -> *) (ast :: AHyperType) x.
Rep (GTerm v ast) x -> GTerm v ast
$cfrom :: forall (v :: AHyperType -> *) (ast :: AHyperType) x.
GTerm v ast -> Rep (GTerm v ast) x
Generic)

makePrisms ''GTerm
makeCommonInstances [''GTerm]
makeHTraversableAndBases ''GTerm

instance RNodes a => HNodes (HFlip GTerm a) where
    type HNodesConstraint (HFlip GTerm a) c = (c a, Recursive c)
    type HWitnessType (HFlip GTerm a) = HRecWitness a
    {-# INLINE hLiftConstraint #-}
    hLiftConstraint :: forall (c :: (AHyperType -> *) -> Constraint)
       (n :: AHyperType -> *) r.
HNodesConstraint (HFlip GTerm a) c =>
HWitness (HFlip GTerm a) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (HFlip GTerm a) n
HRecWitness a n
HRecSelf) = \Proxy c
_ c n => r
x -> c n => r
x
    hLiftConstraint (HWitness (HRecSub HWitness a c
c HRecWitness c n
n)) = forall (a :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (b :: AHyperType -> *)
       (n :: AHyperType -> *) r.
(RNodes a, HNodesConstraint (HFlip GTerm a) c) =>
HWitness a b -> HRecWitness b n -> Proxy c -> (c n => r) -> r
hLiftConstraintH HWitness a c
c HRecWitness c n
n

hLiftConstraintH ::
    forall a c b n r.
    (RNodes a, HNodesConstraint (HFlip GTerm a) c) =>
    HWitness a b ->
    HRecWitness b n ->
    Proxy c ->
    (c n => r) ->
    r
hLiftConstraintH :: forall (a :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (b :: AHyperType -> *)
       (n :: AHyperType -> *) r.
(RNodes a, HNodesConstraint (HFlip GTerm a) c) =>
HWitness a b -> HRecWitness b n -> Proxy c -> (c n => r) -> r
hLiftConstraintH HWitness a b
c HRecWitness b n
n Proxy c
p c n => r
f =
    (forall {k} (t :: k). Proxy t
Proxy @RNodes forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (Proxy c
p forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> (Proxy c
p forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> c n => r
f) (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness @(HFlip GTerm _) HRecWitness b n
n)) HWitness a b
c) HWitness a b
c
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (forall {k} (t :: k). Proxy t
Proxy @(c a))
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (forall {k} (t :: k). Proxy t
Proxy @(RNodes a))

instance Recursively HFunctor ast => HFunctor (HFlip GTerm ast) where
    {-# INLINE hmap #-}
    hmap :: forall (p :: AHyperType -> *) (q :: AHyperType -> *).
(forall (n :: AHyperType -> *).
 HWitness (HFlip GTerm ast) n -> (p # n) -> q # n)
-> (HFlip GTerm ast # p) -> HFlip GTerm ast # q
hmap forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f =
        forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip
            forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ \case
                GMono p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
                GPoly p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
                GBody 'AHyperType ast :# GTerm p
x ->
                    forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
                        ( forall {k} (t :: k). Proxy t
Proxy @(Recursively HFunctor) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*#
                            \HWitness ast n
cw ->
                                forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (k0 :: AHyperType -> *) (x0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (k1 :: AHyperType -> *) (x1 :: AHyperType -> *).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped
                                    forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~ forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (forall (h :: AHyperType -> *) (c :: AHyperType -> *)
       (n :: AHyperType -> *).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness ast n
cw HWitnessType (HFlip GTerm n) n
nw)))
                        )
                        'AHyperType ast :# GTerm p
x
                        forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody
                        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HFunctor ast))

instance Recursively HFoldable ast => HFoldable (HFlip GTerm ast) where
    {-# INLINE hfoldMap #-}
    hfoldMap :: forall a (p :: AHyperType -> *).
Monoid a =>
(forall (n :: AHyperType -> *).
 HWitness (HFlip GTerm ast) n -> (p # n) -> a)
-> (HFlip GTerm ast # p) -> a
hfoldMap forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f =
        \case
            GMono p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
            GPoly p ('AHyperType ast)
x -> forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
            GBody 'AHyperType ast :# GTerm p
x ->
                forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap
                    ( forall {k} (t :: k). Proxy t
Proxy @(Recursively HFoldable) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => HWitness h n -> r) -> HWitness h n -> r
#*#
                        \HWitness ast n
cw ->
                            forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (forall (h :: AHyperType -> *) (c :: AHyperType -> *)
       (n :: AHyperType -> *).
HWitness h c -> HRecWitness c n -> HRecWitness h n
HRecSub HWitness ast n
cw HWitnessType (HFlip GTerm n) n
nw)))
                                forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip forall t b. AReview t b -> b -> t
#)
                    )
                    'AHyperType ast :# GTerm p
x
                    forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (forall {k} (t :: k). Proxy t
Proxy @(HFoldable ast))
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip)

instance RTraversable ast => HTraversable (HFlip GTerm ast) where
    {-# INLINE hsequence #-}
    hsequence :: forall (f :: * -> *) (p :: AHyperType -> *).
Applicative f =>
(HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p)
hsequence =
        \case
            GMono ContainedH f p ('AHyperType ast)
x -> forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
            GPoly ContainedH f p ('AHyperType ast)
x -> forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
            GBody 'AHyperType ast :# GTerm (ContainedH f p)
x ->
                -- HTraversable will be required when not implied by Recursively
                forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
(Applicative f, HTraversable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (forall {k} (t :: k). Proxy t
Proxy @RTraversable forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (k0 :: AHyperType -> *) (x0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (k1 :: AHyperType -> *) (x1 :: AHyperType -> *).
Iso (f0 k0 # x0) (f1 k1 # x1) (HFlip f0 x0 # k0) (HFlip f1 x1 # k1)
hflipped forall (h :: AHyperType -> *) (f :: * -> *) (p :: AHyperType -> *).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence) 'AHyperType ast :# GTerm (ContainedH f p)
x
                    forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (forall {k} (t :: k). Proxy t
Proxy @(RTraversable ast))
                    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody
            forall a b. a -> (a -> b) -> b
& forall (f0 :: (AHyperType -> *) -> AHyperType -> *)
       (x0 :: AHyperType -> *) (k0 :: AHyperType -> *)
       (f1 :: (AHyperType -> *) -> AHyperType -> *)
       (x1 :: AHyperType -> *) (k1 :: AHyperType -> *).
Iso (HFlip f0 x0 # k0) (HFlip f1 x1 # k1) (f0 k0 # x0) (f1 k1 # x1)
_HFlip

-- | Generalize a unification term pointed by the given variable to a `GTerm`.
-- Unification variables that are scoped within the term
-- become universally quantified skolems.
generalize ::
    forall m t.
    UnifyGen m t =>
    UVarOf m # t ->
    m (GTerm (UVarOf m) # t)
generalize :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize UVarOf m # t
v0 =
    do
        (UVarOf m # t
v1, UTerm (UVarOf m) ('AHyperType t)
u) <- forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v0
        TypeConstraintsOf t
c <- forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @t)
        case UTerm (UVarOf m) ('AHyperType t)
u of
            UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
l
                | forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf (GetHyperType ('AHyperType t))
l forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c ->
                    forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1
                        forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$
                        -- We set the variable to a skolem,
                        -- so additional unifications after generalization
                        -- (for example hole resumptions where supported)
                        -- cannot unify it with anything.
                        forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem (forall c. TypeConstraints c => c -> c
generalizeConstraints TypeConstraintsOf (GetHyperType ('AHyperType t))
l))
            USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l | forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf (GetHyperType ('AHyperType t))
l forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1)
            UTerm UTermBody (UVarOf m) ('AHyperType t)
t ->
                do
                    forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UResolving UTermBody (UVarOf m) ('AHyperType t)
t)
                    t # GTerm (UVarOf m)
b <- forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
(Applicative f, HTraversable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize) (UTermBody (UVarOf m) ('AHyperType t)
t forall s a. s -> Getting a s a -> a
^. forall (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody)
                    forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm UTermBody (UVarOf m) ('AHyperType t)
t)
                    forall (f :: * -> *) a. Applicative f => a -> f a
pure
                        ( if forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Bool -> All
All forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. Getting Any s a -> s -> Bool
Lens.has forall (v :: AHyperType -> *) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono) t # GTerm (UVarOf m)
b forall s a. s -> Getting a s a -> a
^. forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Lens._Wrapped
                            then forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1
                            else forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody t # GTerm (UVarOf m)
b
                        )
                    forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> RecMethod (UnifyGen m) t
unifyGenRecursive (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @t)
            UResolving UTermBody (UVarOf m) ('AHyperType t)
t -> forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1 forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (m :: * -> *) (t :: AHyperType -> *) a.
Unify m t =>
(UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> m a
occursError UVarOf m # t
v1 UTermBody (UVarOf m) ('AHyperType t)
t
            UTerm (UVarOf m) ('AHyperType t)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1)

{-# INLINE instantiateForAll #-}
instantiateForAll ::
    forall m t.
    UnifyGen m t =>
    (TypeConstraintsOf t -> UTerm (UVarOf m) # t) ->
    UVarOf m # t ->
    WriterT [m ()] m (UVarOf m # t)
instantiateForAll :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll TypeConstraintsOf t -> UTerm (UVarOf m) # t
cons UVarOf m # t
x =
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x)
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l ->
                do
                    forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell [forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x (forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l)]
                    UVarOf m # t
r <- forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (forall {k} (t :: k). Proxy t
Proxy @t) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf t -> UTerm (UVarOf m) # t
cons forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf (GetHyperType ('AHyperType t))
l) forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                    forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UInstantiated UVarOf m # t
r forall a b. a -> (a -> b) -> b
& forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x forall a b. a -> (a -> b) -> b
& forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                    forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
r
            UInstantiated UVarOf m # t
v -> forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
v
            UTerm (UVarOf m) # t
_ -> forall a. HasCallStack => String -> a
error String
"unexpected state at instantiate's forall"

-- TODO: Better name?
{-# INLINE instantiateH #-}
instantiateH ::
    forall m t.
    UnifyGen m t =>
    (forall n. TypeConstraintsOf n -> UTerm (UVarOf m) # n) ->
    GTerm (UVarOf m) # t ->
    WriterT [m ()] m (UVarOf m # t)
instantiateH :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(forall (n :: AHyperType -> *).
 TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
_ (GMono UVarOf m ('AHyperType t)
x) = forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m ('AHyperType t)
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GPoly UVarOf m ('AHyperType t)
x) = forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateForAll forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons UVarOf m ('AHyperType t)
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GBody 'AHyperType t :# GTerm (UVarOf m)
x) =
    forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
(Applicative f, HTraversable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (forall {k} (t :: k). Proxy t
Proxy @(UnifyGen m) forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(forall (n :: AHyperType -> *).
 TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons) 'AHyperType t :# GTerm (UVarOf m)
x
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm
        forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> RecMethod (UnifyGen m) t
unifyGenRecursive (forall {k} (t :: k). Proxy t
Proxy @m) (forall {k} (t :: k). Proxy t
Proxy @t)

{-# INLINE instantiateWith #-}
instantiateWith ::
    forall m t a.
    UnifyGen m t =>
    m a ->
    (forall n. TypeConstraintsOf n -> UTerm (UVarOf m) # n) ->
    GTerm (UVarOf m) # t ->
    m (UVarOf m # t, a)
instantiateWith :: forall (m :: * -> *) (t :: AHyperType -> *) a.
UnifyGen m t =>
m a
-> (forall (n :: AHyperType -> *).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith m a
action forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons GTerm (UVarOf m) # t
g =
    do
        (UVarOf m # t
r, [m ()]
recover) <- forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT (forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(forall (n :: AHyperType -> *).
 TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons GTerm (UVarOf m) # t
g)
        m a
action forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (UVarOf m # t
r,)

-- | Instantiate a generalized type with fresh unification variables
-- for the quantified variables
{-# INLINE instantiate #-}
instantiate ::
    UnifyGen m t =>
    GTerm (UVarOf m) # t ->
    m (UVarOf m # t)
instantiate :: forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(GTerm (UVarOf m) # t) -> m (UVarOf m # t)
instantiate GTerm (UVarOf m) # t
g = forall (m :: * -> *) (t :: AHyperType -> *) a.
UnifyGen m t =>
m a
-> (forall (n :: AHyperType -> *).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, a)
instantiateWith (forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (UVarOf m) # t
g forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (forall s a. s -> Getting a s a -> a
^. forall s t a b. Field1 s t a b => Lens s t a b
Lens._1)