-- | Unification

{-# LANGUAGE BangPatterns #-}

module Hyper.Unify
    ( unify
    , module Hyper.Class.Unify
    , module Hyper.Unify.Binding
    , module Hyper.Unify.Constraints
    , module Hyper.Unify.Error

    , -- | Exported only for SPECIALIZE pragmas
      updateConstraints, updateTermConstraints, updateTermConstraintsH
    , unifyUTerms, unifyUnbound
    ) where

import Algebra.PartialOrd (PartialOrd(..))
import Hyper
import Hyper.Class.Unify
import Hyper.Class.ZipMatch (zipMatchA)
import Hyper.Unify.Binding (UVar)
import Hyper.Unify.Constraints
import Hyper.Unify.Error (UnifyError(..))
import Hyper.Unify.Term (UTerm(..), UTermBody(..), uConstraints, uBody)

import Hyper.Internal.Prelude

-- TODO: implement when need / better understand motivations for -
-- occursIn, seenAs, getFreeVars, freshen, equals, equiv
-- (from unification-fd package)

{-# INLINE updateConstraints #-}
updateConstraints ::
    Unify m t =>
    TypeConstraintsOf t ->
    UVarOf m # t ->
    UTerm (UVarOf m) # t ->
    m ()
updateConstraints :: TypeConstraintsOf t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
updateConstraints !TypeConstraintsOf t
newConstraints UVarOf m # t
v UTerm (UVarOf m) # t
x =
    case UTerm (UVarOf m) # t
x of
    UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
l
        | TypeConstraintsOf t
newConstraints TypeConstraintsOf t -> TypeConstraintsOf t -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        | Bool
otherwise -> 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
v (TypeConstraintsOf (GetHyperType ('AHyperType t))
-> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
UUnbound TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
newConstraints)
    USkolem TypeConstraintsOf (GetHyperType ('AHyperType t))
l
        | TypeConstraintsOf t
newConstraints TypeConstraintsOf t -> TypeConstraintsOf t -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
l -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        | Bool
otherwise -> ('AHyperType (UVarOf m) :# t)
-> UnifyError t ('AHyperType (UVarOf m))
forall (t :: AHyperType -> *) (h :: AHyperType).
(h :# t) -> UnifyError t h
SkolemEscape 'AHyperType (UVarOf m) :# t
UVarOf m # t
v UnifyError t ('AHyperType (UVarOf m))
-> (UnifyError t ('AHyperType (UVarOf m)) -> m ()) -> m ()
forall a b. a -> (a -> b) -> b
& UnifyError t ('AHyperType (UVarOf m)) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError
    UTerm UTermBody (UVarOf m) ('AHyperType t)
t -> (UVarOf m # t)
-> UTermBody (UVarOf m) ('AHyperType t)
-> TypeConstraintsOf t
-> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> (UTermBody (UVarOf m) # t) -> TypeConstraintsOf t -> m ()
updateTermConstraints UVarOf m # t
v UTermBody (UVarOf m) ('AHyperType t)
t TypeConstraintsOf t
newConstraints
    UResolving UTermBody (UVarOf m) ('AHyperType t)
t -> () () -> m Any -> m ()
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
v UTermBody (UVarOf m) ('AHyperType t)
t
    UTerm (UVarOf m) # t
_ -> [Char] -> m ()
forall a. HasCallStack => [Char] -> a
error [Char]
"This shouldn't happen in unification stage"

{-# INLINE updateTermConstraints #-}
updateTermConstraints ::
    forall m t.
    Unify m t =>
    UVarOf m # t ->
    UTermBody (UVarOf m) # t ->
    TypeConstraintsOf t ->
    m ()
updateTermConstraints :: (UVarOf m # t)
-> (UTermBody (UVarOf m) # t) -> TypeConstraintsOf t -> m ()
updateTermConstraints UVarOf m # t
v UTermBody (UVarOf m) # t
t TypeConstraintsOf t
newConstraints
    | TypeConstraintsOf t
newConstraints TypeConstraintsOf t -> TypeConstraintsOf t -> Bool
forall a. PartialOrd a => a -> a -> Bool
`leq` (UTermBody (UVarOf m) # t
t (UTermBody (UVarOf m) # t)
-> Getting
     (TypeConstraintsOf t)
     (UTermBody (UVarOf m) # t)
     (TypeConstraintsOf t)
-> TypeConstraintsOf t
forall s a. s -> Getting a s a -> a
^. Getting
  (TypeConstraintsOf t)
  (UTermBody (UVarOf m) # t)
  (TypeConstraintsOf t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
Lens' (UTermBody v ast) (TypeConstraintsOf (GetHyperType ast))
uConstraints) = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    | Bool
otherwise =
        Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) => m ()) -> m ()
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 :: AHyperType -> *).
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 ()) -> m ())
-> (HNodesConstraint t (Unify m) => m ()) -> m ()
forall a b. (a -> b) -> a -> b
$
        do
            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
v ((UTermBody (UVarOf m) # t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UResolving UTermBody (UVarOf m) # t
t)
            case TypeConstraintsOf t
-> (t # UVarOf m) -> Maybe (t # WithConstraint (UVarOf m))
forall (ast :: AHyperType -> *) (h :: AHyperType -> *).
HasTypeConstraints ast =>
TypeConstraintsOf ast
-> (ast # h) -> Maybe (ast # WithConstraint h)
verifyConstraints TypeConstraintsOf t
newConstraints (UTermBody (UVarOf m) # t
t (UTermBody (UVarOf m) # t)
-> Getting (t # UVarOf m) (UTermBody (UVarOf m) # t) (t # UVarOf m)
-> t # UVarOf m
forall s a. s -> Getting a s a -> a
^. Getting (t # UVarOf m) (UTermBody (UVarOf m) # t) (t # UVarOf m)
forall (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody) of
                Maybe (t # WithConstraint (UVarOf m))
Nothing -> (t # UVarOf m)
-> TypeConstraintsOf t -> UnifyError t ('AHyperType (UVarOf m))
forall (t :: AHyperType -> *) (h :: AHyperType).
t h -> TypeConstraintsOf t -> UnifyError t h
ConstraintsViolation (UTermBody (UVarOf m) # t
t (UTermBody (UVarOf m) # t)
-> Getting (t # UVarOf m) (UTermBody (UVarOf m) # t) (t # UVarOf m)
-> t # UVarOf m
forall s a. s -> Getting a s a -> a
^. Getting (t # UVarOf m) (UTermBody (UVarOf m) # t) (t # UVarOf m)
forall (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody) TypeConstraintsOf t
newConstraints UnifyError t ('AHyperType (UVarOf m))
-> (UnifyError t ('AHyperType (UVarOf m)) -> m ()) -> m ()
forall a b. a -> (a -> b) -> b
& UnifyError t ('AHyperType (UVarOf m)) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError
                Just t # WithConstraint (UVarOf m)
prop ->
                    do
                        (forall (c :: AHyperType -> *).
 HWitness t c -> (WithConstraint (UVarOf m) # c) -> m ())
-> (t # WithConstraint (UVarOf m)) -> m ()
forall (f :: * -> *) (h :: AHyperType -> *) (m :: AHyperType -> *).
(Applicative f, HFoldable h) =>
(forall (c :: AHyperType -> *). HWitness h c -> (m # c) -> f ())
-> (h # m) -> f ()
htraverse_ (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m c => (WithConstraint (UVarOf m) # c) -> m ())
-> HWitness t c
-> (WithConstraint (UVarOf m) # c)
-> m ()
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> Unify m c => (WithConstraint (UVarOf m) # c) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(WithConstraint (UVarOf m) # t) -> m ()
updateTermConstraintsH) t # WithConstraint (UVarOf m)
prop
                        TypeConstraintsOf (GetHyperType ('AHyperType t))
-> ('AHyperType t :# UVarOf m) -> UTermBody (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast)
-> (ast :# v) -> UTermBody v ast
UTermBody TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
newConstraints (UTermBody (UVarOf m) # t
t (UTermBody (UVarOf m) # t)
-> Getting (t # UVarOf m) (UTermBody (UVarOf m) # t) (t # UVarOf m)
-> t # UVarOf m
forall s a. s -> Getting a s a -> a
^. Getting (t # UVarOf m) (UTermBody (UVarOf m) # t) (t # UVarOf m)
forall (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody) (UTermBody (UVarOf m) # t)
-> ((UTermBody (UVarOf m) # t) -> UTerm (UVarOf m) # t)
-> UTerm (UVarOf m) # t
forall a b. a -> (a -> b) -> b
& (UTermBody (UVarOf m) # t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm (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
v

{-# INLINE updateTermConstraintsH #-}
updateTermConstraintsH ::
    Unify m t =>
    WithConstraint (UVarOf m) # t ->
    m ()
updateTermConstraintsH :: (WithConstraint (UVarOf m) # t) -> m ()
updateTermConstraintsH (WithConstraint TypeConstraintsOf (GetHyperType ('AHyperType t))
c UVarOf m ('AHyperType t)
v0) =
    do
        (UVarOf m ('AHyperType t)
v1, UTerm (UVarOf m) # t
x) <- UVarOf m ('AHyperType t)
-> m (UVarOf m ('AHyperType t), UTerm (UVarOf m) # t)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m ('AHyperType t)
v0
        TypeConstraintsOf t
-> UVarOf m ('AHyperType t) -> (UTerm (UVarOf m) # t) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
TypeConstraintsOf t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
updateConstraints TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
c UVarOf m ('AHyperType t)
v1 UTerm (UVarOf m) # t
x

-- | Unify unification variables
{-# INLINE unify #-}
unify ::
    forall m t.
    Unify m t =>
    UVarOf m # t -> UVarOf m # t -> m (UVarOf m # t)
unify :: (UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
unify UVarOf m # t
x0 UVarOf m # t
y0
    | UVarOf m # t
x0 (UVarOf m # t) -> (UVarOf m # t) -> Bool
forall a. Eq a => a -> a -> Bool
== UVarOf m # t
y0 = (UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
x0
    | Bool
otherwise =
        do
            (UVarOf m # t
x1, UTerm (UVarOf m) # t
xu) <- (UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
x0
            if UVarOf m # t
x1 (UVarOf m # t) -> (UVarOf m # t) -> Bool
forall a. Eq a => a -> a -> Bool
== UVarOf m # t
y0
                then (UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
x1
                else
                    do
                        (UVarOf m # t
y1, UTerm (UVarOf m) # t
yu) <- (UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> m (UVarOf m # t, UTerm (UVarOf m) # t)
semiPruneLookup UVarOf m # t
y0
                        if UVarOf m # t
x1 (UVarOf m # t) -> (UVarOf m # t) -> Bool
forall a. Eq a => a -> a -> Bool
== UVarOf m # t
y1
                            then (UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
x1
                            else (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
unifyUTerms UVarOf m # t
x1 UTerm (UVarOf m) # t
xu UVarOf m # t
y1 UTerm (UVarOf m) # t
yu

{-# INLINE unifyUnbound #-}
unifyUnbound ::
    Unify m t =>
    UVarOf m # t -> TypeConstraintsOf t ->
    UVarOf m # t -> UTerm (UVarOf m) # t ->
    m (UVarOf m # t)
unifyUnbound :: (UVarOf m # t)
-> TypeConstraintsOf t
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
unifyUnbound UVarOf m # t
xv TypeConstraintsOf t
level UVarOf m # t
yv UTerm (UVarOf m) # t
yt =
    do
        TypeConstraintsOf t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
TypeConstraintsOf t
-> (UVarOf m # t) -> (UTerm (UVarOf m) # t) -> m ()
updateConstraints TypeConstraintsOf t
level UVarOf m # t
yv UTerm (UVarOf m) # t
yt
        UVarOf m # t
yv (UVarOf m # t) -> m () -> m (UVarOf m # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ 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
xv ((UVarOf m # t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UToVar UVarOf m # t
yv)

{-# INLINE unifyUTerms #-}
unifyUTerms ::
    forall m t.
    Unify m t =>
    UVarOf m # t -> UTerm (UVarOf m) # t ->
    UVarOf m # t -> UTerm (UVarOf m) # t ->
    m (UVarOf m # t)
unifyUTerms :: (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
unifyUTerms UVarOf m # t
xv (UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
level) UVarOf m # t
yv UTerm (UVarOf m) # t
yt = (UVarOf m # t)
-> TypeConstraintsOf t
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> TypeConstraintsOf t
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
unifyUnbound UVarOf m # t
xv TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
level UVarOf m # t
yv UTerm (UVarOf m) # t
yt
unifyUTerms UVarOf m # t
xv UTerm (UVarOf m) # t
xt UVarOf m # t
yv (UUnbound TypeConstraintsOf (GetHyperType ('AHyperType t))
level) = (UVarOf m # t)
-> TypeConstraintsOf t
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> TypeConstraintsOf t
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m (UVarOf m # t)
unifyUnbound UVarOf m # t
yv TypeConstraintsOf t
TypeConstraintsOf (GetHyperType ('AHyperType t))
level UVarOf m # t
xv UTerm (UVarOf m) # t
xt
unifyUTerms UVarOf m # t
xv USkolem{} UVarOf m # t
yv UTerm (UVarOf m) # t
_ = UVarOf m # t
xv (UVarOf m # t) -> m Any -> m (UVarOf m # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (UnifyError t # UVarOf m) -> m Any
forall (m :: * -> *) (t :: AHyperType -> *) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError (('AHyperType (UVarOf m) :# t)
-> ('AHyperType (UVarOf m) :# t) -> UnifyError t # UVarOf m
forall (t :: AHyperType -> *) (h :: AHyperType).
(h :# t) -> (h :# t) -> UnifyError t h
SkolemUnified 'AHyperType (UVarOf m) :# t
UVarOf m # t
xv 'AHyperType (UVarOf m) :# t
UVarOf m # t
yv)
unifyUTerms UVarOf m # t
xv UTerm (UVarOf m) # t
_ UVarOf m # t
yv USkolem{} = UVarOf m # t
yv (UVarOf m # t) -> m Any -> m (UVarOf m # t)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (UnifyError t # UVarOf m) -> m Any
forall (m :: * -> *) (t :: AHyperType -> *) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError (('AHyperType (UVarOf m) :# t)
-> ('AHyperType (UVarOf m) :# t) -> UnifyError t # UVarOf m
forall (t :: AHyperType -> *) (h :: AHyperType).
(h :# t) -> (h :# t) -> UnifyError t h
SkolemUnified 'AHyperType (UVarOf m) :# t
UVarOf m # t
yv 'AHyperType (UVarOf m) :# t
UVarOf m # t
xv)
unifyUTerms UVarOf m # t
xv (UTerm UTermBody (UVarOf m) ('AHyperType t)
xt) UVarOf m # t
yv (UTerm UTermBody (UVarOf m) ('AHyperType t)
yt) =
    Dict (HNodesConstraint t (Unify m))
-> (HNodesConstraint t (Unify m) => m (UVarOf m # t))
-> m (UVarOf m # t)
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 :: AHyperType -> *).
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 (UVarOf m # t))
 -> m (UVarOf m # t))
-> (HNodesConstraint t (Unify m) => m (UVarOf m # t))
-> m (UVarOf m # t)
forall a b. (a -> b) -> a -> b
$
    do
        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
yv ((UVarOf m # t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UToVar UVarOf m # t
xv)
        (forall (n :: AHyperType -> *).
 HWitness t n
 -> (UVarOf m # n) -> (UVarOf m # n) -> m (UVarOf m # n))
-> (t # UVarOf m) -> (t # UVarOf m) -> Maybe (m (t # UVarOf m))
forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *) (r :: AHyperType -> *).
(Applicative f, ZipMatch h, HTraversable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> (q # n) -> f (r # n))
-> (h # p) -> (h # q) -> Maybe (f (h # r))
zipMatchA (Proxy (Unify m)
forall k (t :: k). Proxy t
Proxy @(Unify m) Proxy (Unify m)
-> (Unify m n =>
    (UVarOf m # n) -> (UVarOf m # n) -> m (UVarOf m # n))
-> HWitness t n
-> (UVarOf m # n)
-> (UVarOf m # n)
-> 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
#> Unify m n => (UVarOf m # n) -> (UVarOf m # n) -> m (UVarOf m # n)
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
unify) (UTermBody (UVarOf m) ('AHyperType t)
xt 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 (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody) (UTermBody (UVarOf m) ('AHyperType t)
yt 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 (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody)
            Maybe (m (t # UVarOf m))
-> (Maybe (m (t # UVarOf m)) -> m (t # UVarOf m))
-> m (t # UVarOf m)
forall a b. a -> (a -> b) -> b
& m (t # UVarOf m) -> Maybe (m (t # UVarOf m)) -> m (t # UVarOf m)
forall a. a -> Maybe a -> a
fromMaybe (UTermBody (UVarOf m) ('AHyperType t)
xt 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 (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody (t # UVarOf m) -> m () -> m (t # UVarOf m)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (forall (c :: AHyperType -> *).
 Unify m c =>
 (UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c))
-> (t # UVarOf m) -> (t # UVarOf m) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(forall (c :: AHyperType -> *).
 Unify m c =>
 (UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c))
-> (t # UVarOf m) -> (t # UVarOf m) -> m ()
structureMismatch forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m (UVarOf m # t)
forall (c :: AHyperType -> *).
Unify m c =>
(UVarOf m # c) -> (UVarOf m # c) -> m (UVarOf m # c)
unify (UTermBody (UVarOf m) ('AHyperType t)
xt 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 (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody) (UTermBody (UVarOf m) ('AHyperType t)
yt 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 (v :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v ast) (UTermBody v2 ast) (ast :# v) (ast :# v2)
uBody))
            m (t # UVarOf m) -> ((t # UVarOf m) -> m ()) -> m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m 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
xv ((UTerm (UVarOf m) # t) -> m ())
-> ((t # UVarOf m) -> UTerm (UVarOf m) # t)
-> (t # UVarOf m)
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTermBody (UVarOf m) ('AHyperType t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
UTermBody v ast -> UTerm v ast
UTerm (UTermBody (UVarOf m) ('AHyperType t) -> UTerm (UVarOf m) # t)
-> ((t # UVarOf m) -> UTermBody (UVarOf m) ('AHyperType t))
-> (t # UVarOf m)
-> UTerm (UVarOf m) # t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf (GetHyperType ('AHyperType t))
-> ('AHyperType t :# UVarOf m)
-> UTermBody (UVarOf m) ('AHyperType t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast)
-> (ast :# v) -> UTermBody v ast
UTermBody (UTermBody (UVarOf m) ('AHyperType t)
xt UTermBody (UVarOf m) ('AHyperType t)
-> Getting
     (TypeConstraintsOf t)
     (UTermBody (UVarOf m) ('AHyperType t))
     (TypeConstraintsOf t)
-> TypeConstraintsOf t
forall s a. s -> Getting a s a -> a
^. Getting
  (TypeConstraintsOf t)
  (UTermBody (UVarOf m) ('AHyperType t))
  (TypeConstraintsOf t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
Lens' (UTermBody v ast) (TypeConstraintsOf (GetHyperType ast))
uConstraints TypeConstraintsOf t -> TypeConstraintsOf t -> TypeConstraintsOf t
forall a. Semigroup a => a -> a -> a
<> UTermBody (UVarOf m) ('AHyperType t)
yt UTermBody (UVarOf m) ('AHyperType t)
-> Getting
     (TypeConstraintsOf t)
     (UTermBody (UVarOf m) ('AHyperType t))
     (TypeConstraintsOf t)
-> TypeConstraintsOf t
forall s a. s -> Getting a s a -> a
^. Getting
  (TypeConstraintsOf t)
  (UTermBody (UVarOf m) ('AHyperType t))
  (TypeConstraintsOf t)
forall (v :: AHyperType -> *) (ast :: AHyperType).
Lens' (UTermBody v ast) (TypeConstraintsOf (GetHyperType ast))
uConstraints)
        (UVarOf m # t) -> m (UVarOf m # t)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # t
xv
unifyUTerms UVarOf m # t
_ UTerm (UVarOf m) # t
_ UVarOf m # t
_ UTerm (UVarOf m) # t
_ = [Char] -> m (UVarOf m # t)
forall a. HasCallStack => [Char] -> a
error [Char]
"This shouldn't happen in unification stage"