-- | A class for unification

{-# LANGUAGE FlexibleContexts #-}

module Hyper.Class.Unify
    ( Unify(..), UVarOf
    , UnifyGen(..)
    , BindingDict(..)
    , applyBindings, semiPruneLookup, occursError
    ) where

import Control.Monad (unless)
import Control.Monad.Error.Class (MonadError(..))
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Trans.State (runStateT, get, put)
import Data.Kind (Type)
import Hyper.Class.Nodes (HNodes(..), (#>))
import Hyper.Class.Optic (HSubset(..), HSubset')
import Hyper.Class.Recursive
import Hyper.Class.Traversable (htraverse)
import Hyper.Class.ZipMatch (ZipMatch)
import Hyper.Type (HyperType, type (#))
import Hyper.Type.Pure (Pure, _Pure)
import Hyper.Unify.Constraints
import Hyper.Unify.Error (UnifyError(..))
import Hyper.Unify.QuantifiedVar (MonadQuantify(..), HasQuantifiedVar(..))
import Hyper.Unify.Term (UTerm(..), UTermBody(..), uBody)

import Hyper.Internal.Prelude

-- | Unification variable type for a unification monad
type family UVarOf (m :: Type -> Type) :: HyperType

-- | BindingDict implements unification variables for a type in a unification monad.
--
-- It is parameterized on:
--
-- * @v@: The unification variable 'HyperType'
-- * @m@: The 'Monad' to bind in
-- * @t@: The unified term's 'HyperType'
--
-- Has 2 implementations in hypertypes:
--
-- * 'Hyper.Unify.Binding.bindingDict' for pure state based unification
-- * 'Hyper.Unify.Binding.ST.stBinding' for 'Control.Monad.ST.ST' based unification
data BindingDict v m t = BindingDict
    { BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar :: !(v # t -> m (UTerm v # t))
    , BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar :: !(UTerm v # t -> m (v # t))
    , BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar :: !(v # t -> UTerm v # t -> m ())
    }

-- | @Unify m t@ enables 'Hyper.Unify.unify' to perform unification for @t@ in the 'Monad' @m@.
--
-- The 'unifyRecursive' method represents the constraint that @Unify m@ applies to all recursive child nodes.
-- It replaces context for 'Unify' to avoid @UndecidableSuperClasses@.
class
    ( Eq (UVarOf m # t)
    , RTraversable t
    , ZipMatch t
    , HasTypeConstraints t
    , HasQuantifiedVar t
    , Monad m
    , MonadQuantify (TypeConstraintsOf t) (QVar t) m
    ) => Unify m t where

    -- | The implementation for unification variables binding and lookup
    binding :: BindingDict (UVarOf m) m t

    -- | Handles a unification error.
    --
    -- If 'unifyError' is called then unification has failed.
    -- A compiler implementation may present an error message based on the provided 'UnifyError' when this occurs.
    unifyError :: UnifyError t # UVarOf m -> m a
    default unifyError ::
        (MonadError (e # Pure) m, HSubset' e (UnifyError t)) =>
        UnifyError t # UVarOf m -> m a
    unifyError UnifyError t # UVarOf m
e =
        Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) => m a) -> m a
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
unifyRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (Unify m) => m a) -> m a)
-> (HNodesConstraint t (Unify m) => m a) -> m a
forall a b. (a -> b) -> a -> b
$
        (forall (n :: HyperType).
 HWitness (UnifyError t) n -> (UVarOf m # n) -> m (Pure # n))
-> (UnifyError t # UVarOf m) -> m (UnifyError t # Pure)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (UVarOf m # n) -> m (Pure # n))
-> HWitness (UnifyError t) n
-> (UVarOf m # n)
-> m (Pure # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Unify m n => (UVarOf m # n) -> m (Pure # n)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (Pure # t)
applyBindings) UnifyError t # UVarOf m
e
        m (UnifyError t # Pure) -> ((UnifyError t # Pure) -> m a) -> m a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (e # Pure) -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ((e # Pure) -> m a)
-> ((UnifyError t # Pure) -> e # Pure)
-> (UnifyError t # Pure)
-> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tagged (UnifyError t # Pure) (Identity (UnifyError t # Pure))
-> Tagged (e # Pure) (Identity (e # Pure))
forall (s :: HyperType) (t :: HyperType) (a :: HyperType)
       (b :: HyperType) (h :: HyperType).
HSubset s t a b =>
Prism (s # h) (t # h) (a # h) (b # h)
hSubset (Tagged (UnifyError t # Pure) (Identity (UnifyError t # Pure))
 -> Tagged (e # Pure) (Identity (e # Pure)))
-> (UnifyError t # Pure) -> e # Pure
forall t b. AReview t b -> b -> t
#)

    -- | What to do when top-levels of terms being unified do not match.
    --
    -- Usually this will cause a 'unifyError'.
    --
    -- Some AST terms could be equivalent despite not matching structurally,
    -- like record field extentions with the fields ordered differently.
    -- Those would override the default implementation to handle the unification of mismatching structures.
    structureMismatch ::
        (forall c. Unify m c => UVarOf m # c -> UVarOf m # c -> m (UVarOf m # c)) ->
        t # UVarOf m -> t # UVarOf m -> m ()
    structureMismatch forall (c :: HyperType).
Unify m c =>
(UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c)
_ t # UVarOf m
x t # UVarOf m
y = (UnifyError t # UVarOf m) -> m ()
forall (m :: * -> *) (t :: HyperType) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError ((t # UVarOf m) -> (t # UVarOf m) -> UnifyError t # UVarOf m
forall (t :: HyperType) (h :: AHyperType).
t h -> t h -> UnifyError t h
Mismatch t # UVarOf m
x t # UVarOf m
y)

    -- TODO: Putting documentation here causes duplication in the haddock documentation
    unifyRecursive :: Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
    {-# INLINE unifyRecursive #-}
    default unifyRecursive ::
        HNodesConstraint t (Unify m) =>
        Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
    unifyRecursive Proxy m
_ Proxy t
_ = Dict (HNodesConstraint t (Unify m))
forall (a :: Constraint). a => Dict a
Dict

instance Recursive (Unify m) where
    {-# INLINE recurse #-}
    recurse :: proxy (Unify m h) -> Dict (HNodesConstraint h (Unify m))
recurse = Proxy m -> Proxy h -> Dict (HNodesConstraint h (Unify m))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
unifyRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy h -> Dict (HNodesConstraint h (Unify m)))
-> (proxy (Unify m h) -> Proxy h)
-> proxy (Unify m h)
-> Dict (HNodesConstraint h (Unify m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy (Unify m h) -> Proxy h
forall (proxy :: Constraint -> *) (f :: HyperType -> Constraint)
       (h :: HyperType).
proxy (f h) -> Proxy h
proxyArgument

-- | A class for unification monads with scope levels
class Unify m t => UnifyGen m t where
    -- | Get the current scope constraint
    scopeConstraints :: Proxy t -> m (TypeConstraintsOf t)

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

instance Recursive (UnifyGen m) where
    {-# INLINE recurse #-}
    recurse :: proxy (UnifyGen m h) -> Dict (HNodesConstraint h (UnifyGen m))
recurse = Proxy m -> Proxy h -> Dict (HNodesConstraint h (UnifyGen m))
forall (m :: * -> *) (t :: HyperType).
UnifyGen m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (UnifyGen m))
unifyGenRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy h -> Dict (HNodesConstraint h (UnifyGen m)))
-> (proxy (UnifyGen m h) -> Proxy h)
-> proxy (UnifyGen m h)
-> Dict (HNodesConstraint h (UnifyGen m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. proxy (UnifyGen m h) -> Proxy h
forall (proxy :: Constraint -> *) (f :: HyperType -> Constraint)
       (h :: HyperType).
proxy (f h) -> Proxy h
proxyArgument

-- | Look up a variable, and return last variable pointing to result.
-- Prunes all variables on way to point to the last variable
-- (path-compression ala union-find).
{-# INLINE semiPruneLookup #-}
semiPruneLookup ::
    Unify m t =>
    UVarOf m # t ->
    m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup :: (UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v0 =
    BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> m (UTerm (UVarOf m) # t)
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> m (UTerm v # t)
lookupVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v0
    m (UTerm (UVarOf m) # t)
-> ((UTerm (UVarOf m) # t)
    -> m (UVarOf m # t, UTerm (UVarOf m) # t))
-> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    \case
    UToVar UVarOf m # t
v1 ->
        do
            (UVarOf m # t
v, UTerm (UVarOf m) # t
r) <- (UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v1
            BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v0 ((UVarOf m # t) -> UTerm (UVarOf m) # t
forall (v :: HyperType) (ast :: AHyperType). v ast -> UTerm v ast
UToVar UVarOf m # t
v)
            (UVarOf m # t, UTerm (UVarOf m) # t)
-> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVarOf m # t
v, UTerm (UVarOf m) # t
r)
    UTerm (UVarOf m) # t
t -> (UVarOf m # t, UTerm (UVarOf m) # t)
-> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UVarOf m # t
v0, UTerm (UVarOf m) # t
t)

-- | Resolve a term from a unification variable.
--
-- Note that this must be done after
-- all unifications involving the term and its children are done,
-- as it replaces unification state with cached resolved terms.
{-# INLINE applyBindings #-}
applyBindings ::
    forall m t.
    Unify m t =>
    UVarOf m # t ->
    m (Pure # t)
applyBindings :: (UVarOf m # t) -> m (Pure # t)
applyBindings UVarOf m # t
v0 =
    (UVarOf m # t)
-> m (UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
v0
    m (UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
-> ((UVarOf m # t, UTerm (UVarOf m) ('AHyperType t))
    -> m (Pure # t))
-> m (Pure # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    \(UVarOf m # t
v1, UTerm (UVarOf m) ('AHyperType t)
x) ->
    let result :: (Pure # t) -> m (Pure # t)
result Pure # t
r = Pure # t
r (Pure # t) -> m () -> m (Pure # t)
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 :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v1 ((Pure # t) -> UTerm (UVarOf m) ('AHyperType t)
forall (v :: HyperType) (ast :: AHyperType).
Pure ast -> UTerm v ast
UResolved Pure # t
r)
        quantify :: TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
c =
            TypeConstraintsOf t -> m (QVar t)
forall typeConstraints q (m :: * -> *).
MonadQuantify typeConstraints q m =>
typeConstraints -> m q
newQuantifiedVariable TypeConstraintsOf t
c m (QVar t) -> (QVar t -> Pure # t) -> m (Pure # t)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure # t) (Identity (Pure # t))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (t # Pure) (Identity (t # Pure))
 -> Tagged (Pure # t) (Identity (Pure # t)))
-> (Tagged (QVar t) (Identity (QVar t))
    -> Tagged (t # Pure) (Identity (t # Pure)))
-> Tagged (QVar t) (Identity (QVar t))
-> Tagged (Pure # t) (Identity (Pure # t))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged (QVar t) (Identity (QVar t))
-> Tagged (t # Pure) (Identity (t # Pure))
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar (Tagged (QVar t) (Identity (QVar t))
 -> Tagged (Pure # t) (Identity (Pure # t)))
-> QVar t -> Pure # t
forall t b. AReview t b -> b -> t
#)
            m (Pure # t) -> ((Pure # t) -> m (Pure # t)) -> m (Pure # t)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Pure # t) -> m (Pure # t)
result
    in
    case UTerm (UVarOf m) ('AHyperType t)
x of
    UResolving UTermBody (UVarOf m) ('AHyperType t)
t -> (UVarOf m # t)
-> UTermBody (UVarOf m) ('AHyperType t) -> m (Pure # t)
forall (m :: * -> *) (t :: HyperType) a.
Unify m t =>
(UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> m a
occursError UVarOf m # t
v1 UTermBody (UVarOf m) ('AHyperType t)
t
    UResolved Pure # t
t -> (Pure # t) -> m (Pure # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Pure # t
t
    UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
c -> TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
c
    USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
c -> TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
c
    UTerm UTermBody (UVarOf m) ('AHyperType t)
b ->
        do
            (t # Pure
r, Bool
anyChild) <-
                Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) => m (t # Pure, Bool))
-> m (t # Pure, Bool)
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
Proxy m -> Proxy t -> Dict (HNodesConstraint t (Unify m))
unifyRecursive (Proxy m
forall k (t :: k). Proxy t
Proxy @m) (Proxy t
forall k (t :: k). Proxy t
Proxy @t)) ((HNodesConstraint t (Unify m) => m (t # Pure, Bool))
 -> m (t # Pure, Bool))
-> (HNodesConstraint t (Unify m) => m (t # Pure, Bool))
-> m (t # Pure, Bool)
forall a b. (a -> b) -> a -> b
$
                (forall (n :: HyperType).
 HWitness t n -> (UVarOf m # n) -> StateT Bool m (Pure # n))
-> (t # UVarOf m) -> StateT Bool m (t # Pure)
forall (f :: * -> *) (h :: HyperType) (p :: HyperType)
       (q :: HyperType).
(Applicative f, HTraversable h) =>
(forall (n :: HyperType). HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse
                ( Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n => (UVarOf m # n) -> StateT Bool m (Pure # n))
-> HWitness t n
-> (UVarOf m # n)
-> StateT Bool m (Pure # n)
forall (h :: HyperType) (c :: HyperType -> Constraint)
       (n :: HyperType) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#>
                    \UVarOf m # n
c ->
                    do
                        StateT Bool m Bool
forall (m :: * -> *) s. Monad m => StateT s m s
get StateT Bool m Bool
-> (Bool -> StateT Bool m ()) -> StateT Bool m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= m () -> StateT Bool m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT Bool m ())
-> (Bool -> m ()) -> Bool -> StateT Bool m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
`unless` BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> UTerm (UVarOf m) ('AHyperType t) -> m ()
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
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 :: HyperType) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UResolving UTermBody (UVarOf m) ('AHyperType t)
b))
                        Bool -> StateT Bool m ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put Bool
True
                        (UVarOf m # n) -> m (Pure # n)
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
(UVarOf m # t) -> m (Pure # t)
applyBindings UVarOf m # n
c m (Pure # n)
-> (m (Pure # n) -> StateT Bool m (Pure # n))
-> StateT Bool m (Pure # n)
forall a b. a -> (a -> b) -> b
& m (Pure # n) -> StateT Bool m (Pure # n)
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift
                ) (UTermBody (UVarOf m) ('AHyperType t)
b 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 :: HyperType) (ast :: AHyperType) (v2 :: HyperType).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody)
                StateT Bool m (t # Pure)
-> (StateT Bool m (t # Pure) -> m (t # Pure, Bool))
-> m (t # Pure, Bool)
forall a b. a -> (a -> b) -> b
& (StateT Bool m (t # Pure) -> Bool -> m (t # Pure, Bool)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
`runStateT` Bool
False)
            Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure # t) (Identity (Pure # t))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (t # Pure) (Identity (t # Pure))
 -> Tagged (Pure # t) (Identity (Pure # t)))
-> (t # Pure) -> Pure # t
forall t b. AReview t b -> b -> t
# t # Pure
r (Pure # t) -> ((Pure # t) -> m (Pure # t)) -> m (Pure # t)
forall a b. a -> (a -> b) -> b
& if Bool
anyChild then (Pure # t) -> m (Pure # t)
result else (Pure # t) -> m (Pure # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure
    UToVar{} -> [Char] -> m (Pure # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"lookup not expected to result in var"
    UConverted{} -> [Char] -> m (Pure # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"conversion state not expected in applyBindings"
    UInstantiated{} ->
        -- This can happen in alphaEq,
        -- where UInstantiated marks that var from one side matches var in the other.
        TypeConstraintsOf t -> m (Pure # t)
quantify TypeConstraintsOf t
forall a. Monoid a => a
mempty

-- | Format and throw an occurs check error
occursError ::
    Unify m t =>
    UVarOf m # t -> UTermBody (UVarOf m) # t -> m a
occursError :: (UVarOf m # t) -> (UTermBody (UVarOf m) # t) -> m a
occursError UVarOf m # t
v (UTermBody TypeConstraintsOf (GetHyperType ('AHyperType t))
c 'AHyperType t :# UVarOf m
b) =
    do
        QVar t
q <- TypeConstraintsOf t -> m (QVar t)
forall typeConstraints q (m :: * -> *).
MonadQuantify typeConstraints q m =>
typeConstraints -> m q
newQuantifiedVariable TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
c
        BindingDict (UVarOf m) m t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (v :: HyperType) (m :: * -> *) (t :: HyperType).
BindingDict v m t -> (v # t) -> (UTerm v # t) -> m ()
bindVar BindingDict (UVarOf m) m t
forall (m :: * -> *) (t :: HyperType).
Unify m t =>
BindingDict (UVarOf m) m t
binding UVarOf m # t
v (Pure ('AHyperType t) -> UTerm (UVarOf m) # t
forall (v :: HyperType) (ast :: AHyperType).
Pure ast -> UTerm v ast
UResolved (Tagged (t # Pure) (Identity (t # Pure))
-> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t)))
forall (h :: HyperType) (j :: HyperType).
Iso (Pure # h) (Pure # j) (h # Pure) (j # Pure)
_Pure (Tagged (t # Pure) (Identity (t # Pure))
 -> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t))))
-> (Tagged (QVar t) (Identity (QVar t))
    -> Tagged (t # Pure) (Identity (t # Pure)))
-> Tagged (QVar t) (Identity (QVar t))
-> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tagged (QVar t) (Identity (QVar t))
-> Tagged (t # Pure) (Identity (t # Pure))
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar (Tagged (QVar t) (Identity (QVar t))
 -> Tagged (Pure ('AHyperType t)) (Identity (Pure ('AHyperType t))))
-> QVar t -> Pure ('AHyperType t)
forall t b. AReview t b -> b -> t
# QVar t
q))
        (UnifyError t # UVarOf m) -> m a
forall (m :: * -> *) (t :: HyperType) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError (t ('AHyperType (UVarOf m))
-> t ('AHyperType (UVarOf m)) -> UnifyError t # UVarOf m
forall (t :: HyperType) (h :: AHyperType).
t h -> t h -> UnifyError t h
Occurs (Tagged (QVar t) (Identity (QVar t))
-> Tagged
     (t ('AHyperType (UVarOf m)))
     (Identity (t ('AHyperType (UVarOf m))))
forall (t :: HyperType) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar (Tagged (QVar t) (Identity (QVar t))
 -> Tagged
      (t ('AHyperType (UVarOf m)))
      (Identity (t ('AHyperType (UVarOf m)))))
-> QVar t -> t ('AHyperType (UVarOf m))
forall t b. AReview t b -> b -> t
# QVar t
q) t ('AHyperType (UVarOf m))
'AHyperType t :# UVarOf m
b)