content: -- | Occurs check (check whether unification terms recursively contains themselves)
  module Hyper.Unify.Occurs
      ( occursCheck
      ) where
  
  import Control.Monad (unless, when)
  import Control.Monad.Trans.Class (MonadTrans (..))
  import Control.Monad.Trans.State (execStateT, get, put)
  import Hyper
  import Hyper.Class.Unify (BindingDict (..), UVarOf, Unify (..), occursError, semiPruneLookup)
  import Hyper.Unify.Term (UTerm (..), uBody)
  
  import Hyper.Internal.Prelude
  
  -- | Occurs check
  {-# INLINE occursCheck #-}
  occursCheck ::
      forall m t.
      Unify m t =>
      UVarOf m # t ->
      m ()
  occursCheck v0 =
      do
          (v1, x) <- semiPruneLookup v0
          case x of
              UResolving t -> occursError v1 t
              UResolved{} -> pure ()
              UUnbound{} -> pure ()
              USkolem{} -> pure ()
              UTerm b ->
                  htraverse_
                      ( Proxy @(Unify m) #>
                          \c ->
                              do
                                  get >>= lift . (`unless` bindVar binding v1 (UResolving b))
                                  put True
                                  occursCheck c & lift
                      )
                      (b ^. uBody)
                      & (`execStateT` False)
                      >>= (`when` bindVar binding v1 (UTerm b))
                      \\ unifyRecursive (Proxy @m) (Proxy @t)
              UToVar{} -> error "lookup not expected to result in var (in occursCheck)"
              UConverted{} -> error "conversion state not expected in occursCheck"
              UInstantiated{} -> error "occursCheck during instantiation"
  