-- | Alpha-equality for schemes
{-# LANGUAGE FlexibleContexts #-}

module Hyper.Type.AST.Scheme.AlphaEq
    ( alphaEq
    ) where

import Control.Lens (ix)
import Hyper
import Hyper.Class.Optic (HNodeLens(..))
import Hyper.Class.ZipMatch (zipMatch_)
import Hyper.Recurse (wrapM, (#>>))
import Hyper.Type.AST.Scheme
import Hyper.Unify
import Hyper.Unify.New (newTerm)
import Hyper.Unify.QuantifiedVar
import Hyper.Unify.Term (UTerm(..), uBody)

import Hyper.Internal.Prelude

makeQVarInstancesInScope ::
    forall m typ.
    UnifyGen m typ =>
    QVars # typ -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstancesInScope :: (QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstancesInScope (QVars Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls) =
    (TypeConstraintsOf typ -> m (UVarOf m # typ))
-> Map (QVar typ) (TypeConstraintsOf typ)
-> m (Map (QVar typ) (UVarOf m # typ))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TypeConstraintsOf typ -> m (UVarOf m # typ)
makeSkolem Map (QVar typ) (TypeConstraintsOf typ)
Map
  (QVar (GetHyperType ('AHyperType typ)))
  (TypeConstraintsOf (GetHyperType ('AHyperType typ)))
foralls m (Map (QVar typ) (UVarOf m # typ))
-> (Map (QVar typ) (UVarOf m # typ)
    -> QVarInstances (UVarOf m) # typ)
-> m (QVarInstances (UVarOf m) # typ)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Map (QVar typ) (UVarOf m # typ) -> QVarInstances (UVarOf m) # typ
forall (h2 :: AHyperType -> *) (typ2 :: AHyperType).
Map (QVar (GetHyperType typ2)) (h2 typ2) -> QVarInstances h2 typ2
QVarInstances
    where
        makeSkolem :: TypeConstraintsOf typ -> m (UVarOf m # typ)
makeSkolem TypeConstraintsOf typ
c = Proxy typ -> m (TypeConstraintsOf typ)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
Proxy t -> m (TypeConstraintsOf t)
scopeConstraints (Proxy typ
forall k (t :: k). Proxy t
Proxy @typ) m (TypeConstraintsOf typ)
-> (TypeConstraintsOf typ -> m (UVarOf m # typ))
-> m (UVarOf m # typ)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= BindingDict (UVarOf m) m typ
-> (UTerm (UVarOf m) # typ) -> m (UVarOf m # typ)
forall (v :: AHyperType -> *) (m :: * -> *) (t :: AHyperType -> *).
BindingDict v m t -> (UTerm v # t) -> m (v # t)
newVar BindingDict (UVarOf m) m typ
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
BindingDict (UVarOf m) m t
binding ((UTerm (UVarOf m) # typ) -> m (UVarOf m # typ))
-> (TypeConstraintsOf typ -> UTerm (UVarOf m) # typ)
-> TypeConstraintsOf typ
-> m (UVarOf m # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeConstraintsOf typ -> UTerm (UVarOf m) # typ
forall (v :: AHyperType -> *) (ast :: AHyperType).
TypeConstraintsOf (GetHyperType ast) -> UTerm v ast
USkolem (TypeConstraintsOf typ -> UTerm (UVarOf m) # typ)
-> (TypeConstraintsOf typ -> TypeConstraintsOf typ)
-> TypeConstraintsOf typ
-> UTerm (UVarOf m) # typ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TypeConstraintsOf typ
c TypeConstraintsOf typ
-> TypeConstraintsOf typ -> TypeConstraintsOf typ
forall a. Semigroup a => a -> a -> a
<>)

schemeBodyToType ::
    (UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
    varTypes # QVarInstances (UVarOf m) -> typ # UVarOf m -> m (UVarOf m # typ)
schemeBodyToType :: (varTypes # QVarInstances (UVarOf m))
-> (typ # UVarOf m) -> m (UVarOf m # typ)
schemeBodyToType varTypes # QVarInstances (UVarOf m)
foralls typ # UVarOf m
x =
    case typ # UVarOf m
x (typ # UVarOf m)
-> Getting (First (QVar typ)) (typ # UVarOf m) (QVar typ)
-> Maybe (QVar typ)
forall s a. s -> Getting (First a) s a -> Maybe a
^? Getting (First (QVar typ)) (typ # UVarOf m) (QVar typ)
forall (t :: AHyperType -> *) (f :: AHyperType).
HasQuantifiedVar t =>
Prism' (t f) (QVar t)
quantifiedVar Maybe (QVar typ)
-> (QVar typ -> Maybe (UVarOf m # typ)) -> Maybe (UVarOf m # typ)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= QVar typ -> Maybe (UVarOf m # typ)
getForAll of
    Maybe (UVarOf m # typ)
Nothing -> (typ # UVarOf m) -> m (UVarOf m # typ)
forall (m :: * -> *) (t :: AHyperType -> *).
UnifyGen m t =>
(t # UVarOf m) -> m (UVarOf m # t)
newTerm typ # UVarOf m
x
    Just UVarOf m # typ
r -> (UVarOf m # typ) -> m (UVarOf m # typ)
forall (f :: * -> *) a. Applicative f => a -> f a
pure UVarOf m # typ
r
    where
        getForAll :: QVar typ -> Maybe (UVarOf m # typ)
getForAll QVar typ
v = varTypes # QVarInstances (UVarOf m)
foralls (varTypes # QVarInstances (UVarOf m))
-> Getting
     (First (UVarOf m # typ))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m # typ)
-> Maybe (UVarOf m # typ)
forall s a. s -> Getting (First a) s a -> Maybe a
^? ((QVarInstances (UVarOf m) # typ)
 -> Const (First (UVarOf m # typ)) (QVarInstances (UVarOf m) # typ))
-> (varTypes # QVarInstances (UVarOf m))
-> Const
     (First (UVarOf m # typ)) (varTypes # QVarInstances (UVarOf m))
forall (s :: AHyperType -> *) (a :: AHyperType -> *)
       (h :: AHyperType -> *).
HNodeLens s a =>
Lens' (s # h) (h # a)
hNodeLens (((QVarInstances (UVarOf m) # typ)
  -> Const (First (UVarOf m # typ)) (QVarInstances (UVarOf m) # typ))
 -> (varTypes # QVarInstances (UVarOf m))
 -> Const
      (First (UVarOf m # typ)) (varTypes # QVarInstances (UVarOf m)))
-> (((UVarOf m # typ)
     -> Const (First (UVarOf m # typ)) (UVarOf m # typ))
    -> (QVarInstances (UVarOf m) # typ)
    -> Const (First (UVarOf m # typ)) (QVarInstances (UVarOf m) # typ))
-> Getting
     (First (UVarOf m # typ))
     (varTypes # QVarInstances (UVarOf m))
     (UVarOf m # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (QVar typ) (UVarOf m # typ)
 -> Const
      (First (UVarOf m # typ)) (Map (QVar typ) (UVarOf m # typ)))
-> (QVarInstances (UVarOf m) # typ)
-> Const (First (UVarOf m # typ)) (QVarInstances (UVarOf m) # typ)
forall (h1 :: AHyperType -> *) (typ1 :: AHyperType)
       (h2 :: AHyperType -> *) (typ2 :: AHyperType).
Iso
  (QVarInstances h1 typ1)
  (QVarInstances h2 typ2)
  (Map (QVar (GetHyperType typ1)) (h1 typ1))
  (Map (QVar (GetHyperType typ2)) (h2 typ2))
_QVarInstances ((Map (QVar typ) (UVarOf m # typ)
  -> Const
       (First (UVarOf m # typ)) (Map (QVar typ) (UVarOf m # typ)))
 -> (QVarInstances (UVarOf m) # typ)
 -> Const (First (UVarOf m # typ)) (QVarInstances (UVarOf m) # typ))
-> (((UVarOf m # typ)
     -> Const (First (UVarOf m # typ)) (UVarOf m # typ))
    -> Map (QVar typ) (UVarOf m # typ)
    -> Const
         (First (UVarOf m # typ)) (Map (QVar typ) (UVarOf m # typ)))
-> ((UVarOf m # typ)
    -> Const (First (UVarOf m # typ)) (UVarOf m # typ))
-> (QVarInstances (UVarOf m) # typ)
-> Const (First (UVarOf m # typ)) (QVarInstances (UVarOf m) # typ)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Index (Map (QVar typ) (UVarOf m # typ))
-> Traversal'
     (Map (QVar typ) (UVarOf m # typ))
     (IxValue (Map (QVar typ) (UVarOf m # typ)))
forall m. Ixed m => Index m -> Traversal' m (IxValue m)
ix Index (Map (QVar typ) (UVarOf m # typ))
QVar typ
v

schemeToRestrictedType ::
    forall m varTypes typ.
    ( Monad m
    , HTraversable varTypes
    , HNodesConstraint varTypes (UnifyGen m)
    , HasScheme varTypes m typ
    ) =>
    Pure # Scheme varTypes typ -> m (UVarOf m # typ)
schemeToRestrictedType :: (Pure # Scheme varTypes typ) -> m (UVarOf m # typ)
schemeToRestrictedType (Pure (Scheme vars typ)) =
    do
        varTypes # QVarInstances (UVarOf m)
foralls <- (forall (n :: AHyperType -> *).
 HWitness varTypes n
 -> (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> (varTypes # QVars) -> m (varTypes # QVarInstances (UVarOf m))
forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
(Applicative f, HTraversable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> f (q # n))
-> (h # p) -> f (h # q)
htraverse (Proxy (UnifyGen m)
forall k (t :: k). Proxy t
Proxy @(UnifyGen m) Proxy (UnifyGen m)
-> (UnifyGen m n =>
    (QVars # n) -> m (QVarInstances (UVarOf m) # n))
-> HWitness varTypes n
-> (QVars # n)
-> m (QVarInstances (UVarOf m) # n)
forall (h :: AHyperType -> *)
       (c :: (AHyperType -> *) -> Constraint) (n :: AHyperType -> *) r.
(HNodes h, HNodesConstraint h c) =>
Proxy c -> (c n => r) -> HWitness h n -> r
#> UnifyGen m n => (QVars # n) -> m (QVarInstances (UVarOf m) # n)
forall (m :: * -> *) (typ :: AHyperType -> *).
UnifyGen m typ =>
(QVars # typ) -> m (QVarInstances (UVarOf m) # typ)
makeQVarInstancesInScope) varTypes # QVars
vars
        (forall (n :: AHyperType -> *).
 HRecWitness typ n -> (n # UVarOf m) -> m (UVarOf m # n))
-> (Pure # typ) -> m (UVarOf m # typ)
forall (m :: * -> *) (h :: AHyperType -> *) (w :: AHyperType -> *).
(Monad m, RTraversable h) =>
(forall (n :: AHyperType -> *).
 HRecWitness h n -> (n # w) -> m (w # n))
-> (Pure # h) -> m (w # h)
wrapM (Proxy (HasScheme varTypes m)
forall k (t :: k). Proxy t
Proxy @(HasScheme varTypes m) Proxy (HasScheme varTypes m)
-> (HasScheme varTypes m n => (n # UVarOf m) -> m (UVarOf m # n))
-> HRecWitness typ n
-> (n # UVarOf m)
-> m (UVarOf m # n)
forall (c :: (AHyperType -> *) -> Constraint)
       (h :: AHyperType -> *) (n :: AHyperType -> *) r.
(Recursive c, c h, RNodes h) =>
Proxy c -> (c n => r) -> HRecWitness h n -> r
#>> (varTypes # QVarInstances (UVarOf m))
-> (n # UVarOf m) -> m (UVarOf m # n)
forall (m :: * -> *) (typ :: AHyperType -> *)
       (varTypes :: AHyperType -> *).
(UnifyGen m typ, HNodeLens varTypes typ, Ord (QVar typ)) =>
(varTypes # QVarInstances (UVarOf m))
-> (typ # UVarOf m) -> m (UVarOf m # typ)
schemeBodyToType varTypes # QVarInstances (UVarOf m)
foralls) 'AHyperType Pure :# typ
Pure # typ
typ

goUTerm ::
    forall m t.
    Unify m t =>
    UVarOf m # t -> UTerm (UVarOf m) # t ->
    UVarOf m # t -> UTerm (UVarOf m) # t ->
    m ()
goUTerm :: (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
goUTerm UVarOf m # t
xv USkolem{} UVarOf m # t
yv USkolem{} =
    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
xv ((UVarOf m # t) -> UTerm (UVarOf m) # t
forall (v :: AHyperType -> *) (ast :: AHyperType).
v ast -> UTerm v ast
UInstantiated UVarOf m # t
yv)
        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
UInstantiated UVarOf m # t
xv)
goUTerm UVarOf m # t
xv (UInstantiated UVarOf m # t
xt) UVarOf m # t
yv (UInstantiated UVarOf m # t
yt)
    | UVarOf m # t
xv (UVarOf m # t) -> (UVarOf m # t) -> Bool
forall a. Eq a => a -> a -> Bool
== UVarOf m # t
yt Bool -> Bool -> Bool
&& UVarOf m # t
yv (UVarOf m # t) -> (UVarOf m # t) -> Bool
forall a. Eq a => a -> a -> Bool
== UVarOf m # t
xt = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    | Bool
otherwise = (UnifyError t # UVarOf m) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *) a.
Unify m t =>
(UnifyError t # UVarOf m) -> m a
unifyError (('AHyperType (UVarOf m) :# t) -> UnifyError t # UVarOf m
forall (t :: AHyperType -> *) (h :: AHyperType).
(h :# t) -> UnifyError t h
SkolemEscape 'AHyperType (UVarOf m) :# t
UVarOf m # t
xv)
goUTerm UVarOf m # t
xv USkolem{} UVarOf m # t
yv UUnbound{} = 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)
goUTerm UVarOf m # t
xv UUnbound{} UVarOf m # t
yv USkolem{} = 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)
goUTerm UVarOf m # t
xv UInstantiated{} UVarOf m # t
yv UUnbound{} = 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)
goUTerm UVarOf m # t
xv UUnbound{} UVarOf m # t
yv UInstantiated{} = 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)
goUTerm UVarOf m # t
_ (UToVar UVarOf m # t
xv) UVarOf m # t
yv UTerm (UVarOf m) # t
yu =
    do
        UTerm (UVarOf m) # t
xu <- 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
xv
        (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
xu UVarOf m # t
yv UTerm (UVarOf m) # t
yu
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
xu UVarOf m # t
_ (UToVar UVarOf m # t
yv) =
    do
        UTerm (UVarOf m) # t
yu <- 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
yv
        (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
xu UVarOf m # t
yv UTerm (UVarOf m) # t
yu
goUTerm UVarOf m # t
xv USkolem{} UVarOf m # t
yv UTerm (UVarOf m) # t
_ = (UnifyError t # UVarOf m) -> m ()
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)
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
_ UVarOf m # t
yv USkolem{} = (UnifyError t # UVarOf m) -> m ()
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)
goUTerm UVarOf m # t
xv UInstantiated{} UVarOf m # t
yv UTerm (UVarOf m) # t
_ = (UnifyError t # UVarOf m) -> m ()
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)
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
_ UVarOf m # t
yv UInstantiated{} = (UnifyError t # UVarOf m) -> m ()
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)
goUTerm UVarOf m # t
xv UUnbound{} UVarOf m # t
yv UTerm (UVarOf m) # t
yu = (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
yu UVarOf m # t
yv UTerm (UVarOf m) # t
yu -- Term created in structure mismatch
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
xu UVarOf m # t
yv UUnbound{} = (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
xu UVarOf m # t
yv UTerm (UVarOf m) # t
xu -- Term created in structure mismatch
goUTerm UVarOf m # t
_ (UTerm UTermBody (UVarOf m) ('AHyperType t)
xt) UVarOf m # t
_ (UTerm UTermBody (UVarOf m) ('AHyperType t)
yt) =
    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
$
    (forall (n :: AHyperType -> *).
 HWitness t n -> (UVarOf m # n) -> (UVarOf m # n) -> m ())
-> (t # UVarOf m) -> (t # UVarOf m) -> Maybe (m ())
forall (f :: * -> *) (h :: AHyperType -> *) (p :: AHyperType -> *)
       (q :: AHyperType -> *).
(Applicative f, ZipMatch h, HFoldable h) =>
(forall (n :: AHyperType -> *).
 HWitness h n -> (p # n) -> (q # n) -> f ())
-> (h # p) -> (h # q) -> Maybe (f ())
zipMatch_ (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 ())
-> HWitness t n
-> (UVarOf m # n)
-> (UVarOf m # n)
-> 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 n => (UVarOf m # n) -> (UVarOf m # n) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m ()
goUVar) (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 (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (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 (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody)
    Maybe (m ()) -> (Maybe (m ()) -> m ()) -> m ()
forall a b. a -> (a -> b) -> b
& m () -> Maybe (m ()) -> m ()
forall a. a -> Maybe a -> a
fromMaybe ((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 (\UVarOf m # c
x UVarOf m # c
y -> UVarOf m # c
x (UVarOf m # c) -> m () -> m (UVarOf m # c)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ (UVarOf m # c) -> (UVarOf m # c) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m ()
goUVar UVarOf m # c
x UVarOf m # c
y) (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 (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (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 (v1 :: AHyperType -> *) (ast :: AHyperType)
       (v2 :: AHyperType -> *).
Lens (UTermBody v1 ast) (UTermBody v2 ast) (ast :# v1) (ast :# v2)
uBody))
goUTerm UVarOf m # t
_ UTerm (UVarOf m) # t
_ UVarOf m # t
_ UTerm (UVarOf m) # t
_ = [Char] -> m ()
forall a. HasCallStack => [Char] -> a
error [Char]
"unexpected state at alpha-eq"

goUVar ::
    Unify m t =>
    UVarOf m # t -> UVarOf m # t -> m ()
goUVar :: (UVarOf m # t) -> (UVarOf m # t) -> m ()
goUVar UVarOf m # t
xv UVarOf m # t
yv =
    do
        UTerm (UVarOf m) # t
xu <- 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
xv
        UTerm (UVarOf m) # t
yu <- 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
yv
        (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> (UVarOf m # t)
-> (UTerm (UVarOf m) # t)
-> m ()
goUTerm UVarOf m # t
xv UTerm (UVarOf m) # t
xu UVarOf m # t
yv UTerm (UVarOf m) # t
yu

-- Check for alpha equality. Raises a `unifyError` when mismatches.
alphaEq ::
    ( HTraversable varTypes
    , HNodesConstraint varTypes (UnifyGen m)
    , HasScheme varTypes m typ
    ) =>
    Pure # Scheme varTypes typ ->
    Pure # Scheme varTypes typ ->
    m ()
alphaEq :: (Pure # Scheme varTypes typ)
-> (Pure # Scheme varTypes typ) -> m ()
alphaEq Pure # Scheme varTypes typ
s0 Pure # Scheme varTypes typ
s1 =
    do
        UVarOf m # typ
t0 <- (Pure # Scheme varTypes typ) -> m (UVarOf m # typ)
forall (m :: * -> *) (varTypes :: AHyperType -> *)
       (typ :: AHyperType -> *).
(Monad m, HTraversable varTypes,
 HNodesConstraint varTypes (UnifyGen m),
 HasScheme varTypes m typ) =>
(Pure # Scheme varTypes typ) -> m (UVarOf m # typ)
schemeToRestrictedType Pure # Scheme varTypes typ
s0
        UVarOf m # typ
t1 <- (Pure # Scheme varTypes typ) -> m (UVarOf m # typ)
forall (m :: * -> *) (varTypes :: AHyperType -> *)
       (typ :: AHyperType -> *).
(Monad m, HTraversable varTypes,
 HNodesConstraint varTypes (UnifyGen m),
 HasScheme varTypes m typ) =>
(Pure # Scheme varTypes typ) -> m (UVarOf m # typ)
schemeToRestrictedType Pure # Scheme varTypes typ
s1
        (UVarOf m # typ) -> (UVarOf m # typ) -> m ()
forall (m :: * -> *) (t :: AHyperType -> *).
Unify m t =>
(UVarOf m # t) -> (UVarOf m # t) -> m ()
goUVar UVarOf m # typ
t0 UVarOf m # typ
t1