sig
  type subst = Substs.t
  type 'a sequence = ('a -> unit) -> unit
  exception Fail
  val occurs_check :
    depth:int ->
    Unif.subst -> InnerTerm.t HVar.t Scoped.t -> InnerTerm.t Scoped.t -> bool
  module type S = Unif_intf.S
  module Inner :
    sig
      type ty = InnerTerm.t
      type term = InnerTerm.t
      val bind :
        Unif_intf.subst ->
        ty HVar.t Scoped.t -> term Scoped.t -> Unif_intf.subst
      val unification :
        ?subst:Unif_intf.subst ->
        term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val matching :
        ?subst:Unif_intf.subst ->
        pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val matching_same_scope :
        ?protect:ty HVar.t Sequence.t ->
        ?subst:Unif_intf.subst ->
        scope:int -> pattern:term -> term -> Unif_intf.subst
      val matching_adapt_scope :
        ?protect:ty HVar.t Sequence.t ->
        ?subst:Unif_intf.subst ->
        pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val variant :
        ?subst:Unif_intf.subst ->
        term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val equal :
        subst:Unif_intf.subst -> term Scoped.t -> term Scoped.t -> bool
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
  module Ty :
    sig
      type ty = Type.t
      type term = Type.t
      val bind :
        Unif_intf.subst ->
        ty HVar.t Scoped.t -> term Scoped.t -> Unif_intf.subst
      val unification :
        ?subst:Unif_intf.subst ->
        term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val matching :
        ?subst:Unif_intf.subst ->
        pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val matching_same_scope :
        ?protect:ty HVar.t Sequence.t ->
        ?subst:Unif_intf.subst ->
        scope:int -> pattern:term -> term -> Unif_intf.subst
      val matching_adapt_scope :
        ?protect:ty HVar.t Sequence.t ->
        ?subst:Unif_intf.subst ->
        pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val variant :
        ?subst:Unif_intf.subst ->
        term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val equal :
        subst:Unif_intf.subst -> term Scoped.t -> term Scoped.t -> bool
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
  module FO :
    sig
      type ty = Type.t
      type term = FOTerm.t
      val bind :
        Unif_intf.subst ->
        ty HVar.t Scoped.t -> term Scoped.t -> Unif_intf.subst
      val unification :
        ?subst:Unif_intf.subst ->
        term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val matching :
        ?subst:Unif_intf.subst ->
        pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val matching_same_scope :
        ?protect:ty HVar.t Sequence.t ->
        ?subst:Unif_intf.subst ->
        scope:int -> pattern:term -> term -> Unif_intf.subst
      val matching_adapt_scope :
        ?protect:ty HVar.t Sequence.t ->
        ?subst:Unif_intf.subst ->
        pattern:term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val variant :
        ?subst:Unif_intf.subst ->
        term Scoped.t -> term Scoped.t -> Unif_intf.subst
      val equal :
        subst:Unif_intf.subst -> term Scoped.t -> term Scoped.t -> bool
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
end