-- | Generalization of type schemes

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

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
    = GMono (v ast) -- ^ Completely monomoprhic term
    | GPoly (v ast)
        -- ^ Points to a quantified variable (instantiation will
        -- create fresh unification terms) (`Hyper.Unify.Term.USkolem`
        -- or `Hyper.Unify.Term.UResolved`)
    | GBody (ast :# GTerm v) -- ^ Term with some polymorphic parts
    deriving (forall x. GTerm v ast -> Rep (GTerm v ast) x)
-> (forall x. Rep (GTerm v ast) x -> GTerm v ast)
-> Generic (GTerm v ast)
forall x. Rep (GTerm v ast) x -> GTerm v ast
forall x. GTerm v ast -> Rep (GTerm v ast) x
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 :: HWitness (HFlip GTerm a) n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitness HWitnessType (HFlip GTerm a) n
HRecSelf) = \Proxy c
_ c n => r
x -> r
c n => r
x
    hLiftConstraint (HWitness (HRecSub c n)) = HWitness a c -> HRecWitness c n -> Proxy c -> (c n => r) -> r
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 :: 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 =
    Dict (HNodesConstraint a RNodes)
-> (HNodesConstraint a RNodes => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (RNodes a) -> Dict (HNodesConstraint a RNodes)
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (RNodes a)
forall k (t :: k). Proxy t
Proxy @(RNodes a))) ((HNodesConstraint a RNodes => r) -> r)
-> (HNodesConstraint a RNodes => r) -> r
forall a b. (a -> b) -> a -> b
$
    Dict (HNodesConstraint a c) -> (HNodesConstraint a c => r) -> r
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (c a) -> Dict (HNodesConstraint a c)
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (c a)
forall k (t :: k). Proxy t
Proxy @(c a))) ((HNodesConstraint a c => r) -> r)
-> (HNodesConstraint a c => r) -> r
forall a b. (a -> b) -> a -> b
$
    HWitness a b -> Proxy RNodes -> (RNodes b => r) -> r
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness a b
c (Proxy RNodes
forall k (t :: k). Proxy t
Proxy @RNodes)
    ( HWitness a b -> Proxy c -> (c b => r) -> r
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness a b
c Proxy c
p
        (HWitness (HFlip GTerm b) n -> Proxy c -> (c n => r) -> r
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint (HWitnessType (HFlip GTerm b) n -> HWitness (HFlip GTerm b) n
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness @(HFlip GTerm _) HWitnessType (HFlip GTerm b) n
HRecWitness b n
n) Proxy c
p c n => r
f)
    )

instance Recursively HFunctor ast => HFunctor (HFlip GTerm ast) where
    {-# INLINE hmap #-}
    hmap :: (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 =
        ((GTerm p # ast) -> Identity (GTerm q # ast))
-> (HFlip GTerm ast # p) -> Identity (HFlip GTerm ast # q)
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 (((GTerm p # ast) -> Identity (GTerm q # ast))
 -> (HFlip GTerm ast # p) -> Identity (HFlip GTerm ast # q))
-> ((GTerm p # ast) -> GTerm q # ast)
-> (HFlip GTerm ast # p)
-> HFlip GTerm ast # q
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
        \case
        GMono p ('AHyperType ast)
x -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> q # ast
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x (q # ast) -> ((q # ast) -> GTerm q # ast) -> GTerm q # ast
forall a b. a -> (a -> b) -> b
& (q # ast) -> GTerm q # ast
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
        GPoly p ('AHyperType ast)
x -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> q # ast
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x (q # ast) -> ((q # ast) -> GTerm q # ast) -> GTerm q # ast
forall a b. a -> (a -> b) -> b
& (q # ast) -> GTerm q # ast
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
        GBody 'AHyperType ast :# GTerm p
x ->
            Dict (HFunctor ast, HNodesConstraint ast (Recursively HFunctor))
-> ((HFunctor ast, HNodesConstraint ast (Recursively HFunctor)) =>
    GTerm q # ast)
-> GTerm q # ast
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFunctor ast)
-> Dict (HFunctor ast, HNodesConstraint ast (Recursively HFunctor))
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFunctor ast)
forall k (t :: k). Proxy t
Proxy @(HFunctor ast))) (((HFunctor ast, HNodesConstraint ast (Recursively HFunctor)) =>
  GTerm q # ast)
 -> GTerm q # ast)
-> ((HFunctor ast, HNodesConstraint ast (Recursively HFunctor)) =>
    GTerm q # ast)
-> GTerm q # ast
forall a b. (a -> b) -> a -> b
$
            (forall (n :: AHyperType -> *).
 HWitness ast n -> (GTerm p # n) -> GTerm q # n)
-> (ast # GTerm p) -> ast # GTerm q
forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap
            ( \HWitness ast n
cw ->
                HWitness ast n
-> Proxy (Recursively HFunctor)
-> (Recursively HFunctor n => (GTerm p # n) -> GTerm q # n)
-> (GTerm p # n)
-> GTerm q # n
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness ast n
cw (Proxy (Recursively HFunctor)
forall k (t :: k). Proxy t
Proxy @(Recursively HFunctor)) ((Recursively HFunctor n => (GTerm p # n) -> GTerm q # n)
 -> (GTerm p # n) -> GTerm q # n)
-> (Recursively HFunctor n => (GTerm p # n) -> GTerm q # n)
-> (GTerm p # n)
-> GTerm q # n
forall a b. (a -> b) -> a -> b
$
                ((HFlip GTerm n # p) -> Identity (HFlip GTerm n # q))
-> (GTerm p # n) -> Identity (GTerm q # n)
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 (((HFlip GTerm n # p) -> Identity (HFlip GTerm n # q))
 -> (GTerm p # n) -> Identity (GTerm q # n))
-> ((HFlip GTerm n # p) -> HFlip GTerm n # q)
-> (GTerm p # n)
-> GTerm q # n
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
                (forall (n :: AHyperType -> *).
 HWitness (HFlip GTerm n) n -> (p # n) -> q # n)
-> (HFlip GTerm n # p) -> HFlip GTerm n # q
forall (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
HFunctor h =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> q # n)
-> (h # p) -> h # q
hmap (HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> q # n
f (HWitness (HFlip GTerm ast) n -> (p # n) -> q # n)
-> (HWitness (HFlip GTerm n) n -> HWitness (HFlip GTerm ast) n)
-> HWitness (HFlip GTerm n) n
-> (p # n)
-> q # n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> HWitnessType (HFlip GTerm ast) n -> HWitness (HFlip GTerm ast) n
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (HWitness ast n -> HRecWitness n n -> HRecWitness ast n
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
HRecWitness n n
nw)))
            ) ast # GTerm p
'AHyperType ast :# GTerm p
x
            (ast # GTerm q)
-> ((ast # GTerm q) -> GTerm q # ast) -> GTerm q # ast
forall a b. a -> (a -> b) -> b
& (ast # GTerm q) -> GTerm q # ast
forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody

instance Recursively HFoldable ast => HFoldable (HFlip GTerm ast) where
    {-# INLINE hfoldMap #-}
    hfoldMap :: (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 -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> a
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
        GPoly p ('AHyperType ast)
x -> HWitness (HFlip GTerm ast) ast -> p ('AHyperType ast) -> a
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (HWitnessType (HFlip GTerm ast) ast
-> HWitness (HFlip GTerm ast) ast
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness HWitnessType (HFlip GTerm ast) ast
forall (h :: AHyperType -> *). HRecWitness h h
HRecSelf) p ('AHyperType ast)
x
        GBody 'AHyperType ast :# GTerm p
x ->
            Dict (HFoldable ast, HNodesConstraint ast (Recursively HFoldable))
-> ((HFoldable ast,
     HNodesConstraint ast (Recursively HFoldable)) =>
    a)
-> a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (HFoldable ast)
-> Dict
     (HFoldable ast, HNodesConstraint ast (Recursively HFoldable))
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
Recursively c h =>
proxy (c h) -> Dict (c h, HNodesConstraint h (Recursively c))
recursively (Proxy (HFoldable ast)
forall k (t :: k). Proxy t
Proxy @(HFoldable ast))) (((HFoldable ast, HNodesConstraint ast (Recursively HFoldable)) =>
  a)
 -> a)
-> ((HFoldable ast,
     HNodesConstraint ast (Recursively HFoldable)) =>
    a)
-> a
forall a b. (a -> b) -> a -> b
$
            (forall (n :: AHyperType -> *).
 HWitness ast n -> (GTerm p # n) -> a)
-> (ast # GTerm p) -> a
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap
            ( \HWitness ast n
cw ->
                HWitness ast n
-> Proxy (Recursively HFoldable)
-> (Recursively HFoldable n => (GTerm p # n) -> a)
-> (GTerm p # n)
-> a
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
HWitness h n -> Proxy c -> (c n => r) -> r
hLiftConstraint HWitness ast n
cw (Proxy (Recursively HFoldable)
forall k (t :: k). Proxy t
Proxy @(Recursively HFoldable)) ((Recursively HFoldable n => (GTerm p # n) -> a)
 -> (GTerm p # n) -> a)
-> (Recursively HFoldable n => (GTerm p # n) -> a)
-> (GTerm p # n)
-> a
forall a b. (a -> b) -> a -> b
$
                (forall (n :: AHyperType -> *).
 HWitness (HFlip GTerm n) n -> (p # n) -> a)
-> (HFlip GTerm n # p) -> a
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (HWitness (HFlip GTerm ast) n -> (p # n) -> a
forall (n :: AHyperType -> *).
HWitness (HFlip GTerm ast) n -> (p # n) -> a
f (HWitness (HFlip GTerm ast) n -> (p # n) -> a)
-> (HWitness (HFlip GTerm n) n -> HWitness (HFlip GTerm ast) n)
-> HWitness (HFlip GTerm n) n
-> (p # n)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (\(HWitness HWitnessType (HFlip GTerm n) n
nw) -> HWitnessType (HFlip GTerm ast) n -> HWitness (HFlip GTerm ast) n
forall (h :: AHyperType -> *) (n :: AHyperType -> *).
HWitnessType h n -> HWitness h n
HWitness (HWitness ast n -> HRecWitness n n -> HRecWitness ast n
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
HRecWitness n n
nw)))
                ((HFlip GTerm n # p) -> a)
-> ((GTerm p # n) -> HFlip GTerm n # p) -> (GTerm p # n) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged (GTerm p # n) (Identity (GTerm p # n))
-> Tagged (HFlip GTerm n # p) (Identity (HFlip GTerm n # p))
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 (Tagged (GTerm p # n) (Identity (GTerm p # n))
 -> Tagged (HFlip GTerm n # p) (Identity (HFlip GTerm n # p)))
-> (GTerm p # n) -> HFlip GTerm n # p
forall t b. AReview t b -> b -> t
#)
            ) ast # GTerm p
'AHyperType ast :# GTerm p
x
        (GTerm p ('AHyperType ast) -> a)
-> ((HFlip GTerm ast # p) -> GTerm p ('AHyperType ast))
-> (HFlip GTerm ast # p)
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HFlip GTerm ast # p)
-> Getting
     (GTerm p ('AHyperType ast))
     (HFlip GTerm ast # p)
     (GTerm p ('AHyperType ast))
-> GTerm p ('AHyperType ast)
forall s a. s -> Getting a s a -> a
^. Getting
  (GTerm p ('AHyperType ast))
  (HFlip GTerm ast # p)
  (GTerm p ('AHyperType ast))
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 :: (HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p)
hsequence =
        \case
        GMono ContainedH f p ('AHyperType ast)
x -> ContainedH f p ('AHyperType ast) -> f (p ('AHyperType ast))
forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x f (p ('AHyperType ast))
-> (p ('AHyperType ast) -> GTerm p ('AHyperType ast))
-> f (GTerm p ('AHyperType ast))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> p ('AHyperType ast) -> GTerm p ('AHyperType ast)
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono
        GPoly ContainedH f p ('AHyperType ast)
x -> ContainedH f p ('AHyperType ast) -> f (p ('AHyperType ast))
forall (f :: * -> *) (p :: AHyperType -> *) (h :: AHyperType).
ContainedH f p h -> f (p h)
runContainedH ContainedH f p ('AHyperType ast)
x f (p ('AHyperType ast))
-> (p ('AHyperType ast) -> GTerm p ('AHyperType ast))
-> f (GTerm p ('AHyperType ast))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> p ('AHyperType ast) -> GTerm p ('AHyperType ast)
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly
        GBody 'AHyperType ast :# GTerm (ContainedH f p)
x ->
            Dict (HNodesConstraint ast RTraversable)
-> (HNodesConstraint ast RTraversable =>
    f (GTerm p ('AHyperType ast)))
-> f (GTerm p ('AHyperType ast))
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy (RTraversable ast)
-> Dict (HNodesConstraint ast RTraversable)
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (proxy :: Constraint -> *).
(Recursive c, HNodes h, c h) =>
proxy (c h) -> Dict (HNodesConstraint h c)
recurse (Proxy (RTraversable ast)
forall k (t :: k). Proxy t
Proxy @(RTraversable ast))) ((HNodesConstraint ast RTraversable =>
  f (GTerm p ('AHyperType ast)))
 -> f (GTerm p ('AHyperType ast)))
-> (HNodesConstraint ast RTraversable =>
    f (GTerm p ('AHyperType ast)))
-> f (GTerm p ('AHyperType ast))
forall a b. (a -> b) -> a -> b
$
            -- HTraversable will be required when not implied by Recursively
            (forall (n :: AHyperType -> *).
 HWitness ast n -> (GTerm (ContainedH f p) # n) -> f (GTerm p # n))
-> (ast # GTerm (ContainedH f p)) -> f (ast # GTerm p)
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 RTraversable
forall k (t :: k). Proxy t
Proxy @RTraversable Proxy RTraversable
-> (RTraversable n =>
    (GTerm (ContainedH f p) # n) -> f (GTerm p # n))
-> HWitness ast n
-> (GTerm (ContainedH f p) # n)
-> f (GTerm p # n)
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> ((HFlip GTerm n # ContainedH f p) -> f (HFlip GTerm n # p))
-> (GTerm (ContainedH f p) # n) -> f (GTerm p # n)
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 (HFlip GTerm n # ContainedH f p) -> f (HFlip GTerm n # p)
forall (h :: AHyperType -> *) (f :: * -> *) (p :: AHyperType -> *).
(HTraversable h, Applicative f) =>
(h # ContainedH f p) -> f (h # p)
hsequence) ast # GTerm (ContainedH f p)
'AHyperType ast :# GTerm (ContainedH f p)
x
            f (ast # GTerm p)
-> ((ast # GTerm p) -> GTerm p ('AHyperType ast))
-> f (GTerm p ('AHyperType ast))
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (ast # GTerm p) -> GTerm p ('AHyperType ast)
forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody
        (GTerm (ContainedH f p) ('AHyperType ast)
 -> f (GTerm p ('AHyperType ast)))
-> ((GTerm (ContainedH f p) ('AHyperType ast)
     -> f (GTerm p ('AHyperType ast)))
    -> (HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p))
-> (HFlip GTerm ast # ContainedH f p)
-> f (HFlip GTerm ast # p)
forall a b. a -> (a -> b) -> b
& (GTerm (ContainedH f p) ('AHyperType ast)
 -> f (GTerm p ('AHyperType ast)))
-> (HFlip GTerm ast # ContainedH f p) -> f (HFlip GTerm ast # p)
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 :: (UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize UVarOf m # t
v0 =
    do
        (UVarOf m # t
v1, UTerm (UVarOf m) ('AHyperType t)
u) <- (UVarOf m # t)
-> m (UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
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 <- Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t)
        case UTerm (UVarOf m) ('AHyperType t)
u of
            UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
l | TypeConstraintsOf t -> TypeConstraintsOf t
forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l TypeConstraintsOf t -> TypeConstraintsOf t -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c ->
                (UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1 (GTerm (UVarOf m) # t) -> m () -> m (GTerm (UVarOf m) # t)
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.
                BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (TypeConstraintsOf (GetHyperType ('AHyperType t))
-> UTerm (UVarOf m) ('AHyperType t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem (TypeConstraintsOf t -> TypeConstraintsOf t
forall c. TypeConstraints c => c -> c
generalizeConstraints TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l))
            USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l | TypeConstraintsOf t -> TypeConstraintsOf t
forall c. TypeConstraints c => c -> c
toScopeConstraints TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l TypeConstraintsOf t -> TypeConstraintsOf t -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
c -> (GTerm (UVarOf m) # t) -> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GPoly UVarOf m # t
v1)
            UTerm UTermBody (UVarOf m) ('AHyperType t)
t ->
                Dict (HNodesConstraint t (UnifyGen m))
-> (HNodesConstraint t (UnifyGen m) => m (GTerm (UVarOf m) # t))
-> m (GTerm (UVarOf m) # t)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
unifyGenRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (UnifyGen m) => m (GTerm (UVarOf m) # t))
 -> m (GTerm (UVarOf m) # t))
-> (HNodesConstraint t (UnifyGen m) => m (GTerm (UVarOf m) # t))
-> m (GTerm (UVarOf m) # t)
forall a b. (a -> b) -> a -> b
$
                do
                    BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (UTermBody (UVarOf m) ('AHyperType t)
-> UTerm (UVarOf m) ('AHyperType t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UResolving UTermBody (UVarOf m) ('AHyperType t)
t)
                    t # GTerm (UVarOf m)
r <- (forall (n :: AHyperType -> *).
 HWitness t n -> (UVarOf m # n) -> m (GTerm (UVarOf m) # n))
-> (t # UVarOf m) -> m (t # GTerm (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 => (UVarOf m # n) -> m (GTerm (UVarOf m) # n))
-> HWitness t n
-> (UVarOf m # n)
-> m (GTerm (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 => (UVarOf m # n) -> m (GTerm (UVarOf m) # n)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(UVarOf m # t) -> m (GTerm (UVarOf m) # t)
generalize) (UTermBody (UVarOf m) ('AHyperType t)
t UTermBody (UVarOf m) ('AHyperType t)
-> Getting
     (t # UVarOf m)
     (UTermBody (UVarOf m) ('AHyperType t))
     (t # UVarOf m)
-> t # UVarOf m
forall s a. s -> Getting a s a -> a
^. Getting
  (t # UVarOf m)
  (UTermBody (UVarOf m) ('AHyperType t))
  (t # UVarOf m)
forall (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody)
                    t # GTerm (UVarOf m)
r (t # GTerm (UVarOf m)) -> m () -> m (t # GTerm (UVarOf m))
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 (UTermBody (UVarOf m) ('AHyperType t)
-> UTerm (UVarOf m) ('AHyperType t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm UTermBody (UVarOf m) ('AHyperType t)
t)
                m (t # GTerm (UVarOf m))
-> ((t # GTerm (UVarOf m)) -> GTerm (UVarOf m) # t)
-> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&>
                \t # GTerm (UVarOf m)
b ->
                if (forall (n :: AHyperType -> *).
 HWitness t n -> (GTerm (UVarOf m) # n) -> All)
-> (t # GTerm (UVarOf m)) -> All
forall (h :: AHyperType -> *) a (p :: AHyperType -> *).
(HFoldable h, Monoid a) =>
(forall (n :: AHyperType -> *). HWitness h n -> (p # n) -> a)
-> (h # p) -> a
hfoldMap (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n => (GTerm (UVarOf m) # n) -> All)
-> HWitness t n
-> (GTerm (UVarOf m) # n)
-> All
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 (Bool -> All)
-> ((GTerm (UVarOf m) # n) -> Bool)
-> (GTerm (UVarOf m) # n)
-> All
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting Any (GTerm (UVarOf m) # n) (UVarOf m ('AHyperType n))
-> (GTerm (UVarOf m) # n) -> Bool
forall s a. Getting Any s a -> s -> Bool
Lens.has Getting Any (GTerm (UVarOf m) # n) (UVarOf m ('AHyperType n))
forall (v :: AHyperType -> *) (ast :: AHyperType).
Prism' (GTerm v ast) (v ast)
_GMono) t # GTerm (UVarOf m)
b All -> Getting Bool All Bool -> Bool
forall s a. s -> Getting a s a -> a
^. Getting Bool All Bool
forall s t. Rewrapping s t => Iso s t (Unwrapped s) (Unwrapped t)
Lens._Wrapped
                then (UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1
                else ('AHyperType t :# GTerm (UVarOf m)) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
(ast :# GTerm v) -> GTerm v ast
GBody t # GTerm (UVarOf m)
'AHyperType t :# GTerm (UVarOf m)
b
            UResolving UTermBody (UVarOf m) ('AHyperType t)
t -> (UVarOf m # t) -> GTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> GTerm v ast
GMono UVarOf m # t
v1 (GTerm (UVarOf m) # t) -> m Any -> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (UVarOf m # t) -> UTermBody (UVarOf m) ('AHyperType t) -> m Any
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)
_ -> (GTerm (UVarOf m) # t) -> m (GTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((UVarOf m # t) -> GTerm (UVarOf m) # t
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 :: (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 =
    BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> m (UTerm (UVarOf m) # t)
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x m (UTerm (UVarOf m) # t)
-> (m (UTerm (UVarOf m) # t)
    -> WriterT [m ()] m (UTerm (UVarOf m) # t))
-> WriterT [m ()] m (UTerm (UVarOf m) # t)
forall a b. a -> (a -> b) -> b
& m (UTerm (UVarOf m) # t) -> WriterT [m ()] m (UTerm (UVarOf m) # t)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
    WriterT [m ()] m (UTerm (UVarOf m) # t)
-> ((UTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    \case
    USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l ->
        do
            [m ()] -> WriterT [m ()] m ()
forall (m :: * -> *) w. Monad m => w -> WriterT w m ()
tell [BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x (TypeConstraintsOf (GetHyperType ('AHyperType t))
-> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l)]
            UVarOf m # t
r <- Proxy t -> m (TypeConstraintsOf t)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy t
forall k (t :: k). Proxy t
Proxy @t) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> TypeConstraintsOf t)
-> m (TypeConstraintsOf t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (TypeConstraintsOf t -> TypeConstraintsOf t -> TypeConstraintsOf t
forall a. Semigroup a => a -> a -> a
<> TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l) m (TypeConstraintsOf t)
-> (TypeConstraintsOf t -> m (UVarOf m # t)) -> m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BindingDict (UVarOf m) m t
-> (UTerm (UVarOf m) # t) -> m (UVarOf m # t)
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding ((UTerm (UVarOf m) # t) -> m (UVarOf m # t))
-> (TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> TypeConstraintsOf t
-> m (UVarOf m # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf t -> UTerm (UVarOf m) # t
cons m (UVarOf m # t)
-> (m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall a b. a -> (a -> b) -> b
& m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            (UVarOf m # t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UInstantiated UVarOf m # t
r (UTerm (UVarOf m) # t) -> ((UTerm (UVarOf m) # t) -> m ()) -> m ()
forall a b. a -> (a -> b) -> b
& BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
x m () -> (m () -> WriterT [m ()] m ()) -> WriterT [m ()] m ()
forall a b. a -> (a -> b) -> b
& m () -> WriterT [m ()] m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
            (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
r
    UInstantiated UVarOf m # t
v -> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
v
    UTerm (UVarOf m) # t
_ -> String -> WriterT [m ()] m (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 (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 # t
x) = (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GPoly UVarOf m # t
x) = (TypeConstraintsOf t -> UTerm (UVarOf m) # t)
-> (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
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
forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons UVarOf m # t
x
instantiateH forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
cons (GBody 'AHyperType t :# GTerm (UVarOf m)
x) =
    Dict (HNodesConstraint t (UnifyGen m))
-> (HNodesConstraint t (UnifyGen m) =>
    WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
unifyGenRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (UnifyGen m) =>
  WriterT [m ()] m (UVarOf m # t))
 -> WriterT [m ()] m (UVarOf m # t))
-> (HNodesConstraint t (UnifyGen m) =>
    WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall a b. (a -> b) -> a -> b
$
    (forall (n :: AHyperType -> *).
 HWitness t n
 -> (GTerm (UVarOf m) # n) -> WriterT [m ()] m (UVarOf m # n))
-> (t # GTerm (UVarOf m)) -> WriterT [m ()] m (t # 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 =>
    (GTerm (UVarOf m) # n) -> WriterT [m ()] m (UVarOf m # n))
-> HWitness t n
-> (GTerm (UVarOf m) # n)
-> WriterT [m ()] m (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
#> (forall (n :: AHyperType -> *).
 TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # n) -> WriterT [m ()] m (UVarOf m # n)
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) t # GTerm (UVarOf m)
'AHyperType t :# GTerm (UVarOf m)
x WriterT [m ()] m (t # UVarOf m)
-> ((t # UVarOf m) -> WriterT [m ()] m (UVarOf m # t))
-> WriterT [m ()] m (UVarOf m # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (UVarOf m # t) -> WriterT [m ()] m (UVarOf m # t))
-> ((t # UVarOf m) -> m (UVarOf m # t))
-> (t # UVarOf m)
-> WriterT [m ()] m (UVarOf m # t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (t # UVarOf m) -> m (UVarOf m # t)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm

{-# 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 :: 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 (n :: AHyperType -> *).
 TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t) -> WriterT [m ()] m (UVarOf m # t)
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
            WriterT [m ()] m (UVarOf m # t)
-> (WriterT [m ()] m (UVarOf m # t) -> m (UVarOf m # t, [m ()]))
-> m (UVarOf m # t, [m ()])
forall a b. a -> (a -> b) -> b
& WriterT [m ()] m (UVarOf m # t) -> m (UVarOf m # t, [m ()])
forall w (m :: * -> *) a. WriterT w m a -> m (a, w)
runWriterT
        m a
action m a -> m () -> m a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* [m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [m ()]
recover m a -> (a -> (UVarOf m # t, a)) -> m (UVarOf m # t, a)
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 :: (GTerm (UVarOf m) # t) -> m (UVarOf m # t)
instantiate GTerm (UVarOf m) # t
g = m ()
-> (forall (n :: AHyperType -> *).
    TypeConstraintsOf n -> UTerm (UVarOf m) # n)
-> (GTerm (UVarOf m) # t)
-> m (UVarOf m # t, ())
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 ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) forall (n :: AHyperType -> *).
TypeConstraintsOf n -> UTerm (UVarOf m) # n
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound GTerm (UVarOf m) # t
g m (UVarOf m # t, ())
-> ((UVarOf m # t, ()) -> UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> ((UVarOf m # t, ())
-> Getting (UVarOf m # t) (UVarOf m # t, ()) (UVarOf m # t)
-> UVarOf m # t
forall s a. s -> Getting a s a -> a
^. Getting (UVarOf m # t) (UVarOf m # t, ()) (UVarOf m # t)
forall s t a b. Field1 s t a b => Lens s t a b
Lens._1)