sig
  type 'a or_error = [ `Error of string | `Ok of 'a ]
  type type_ = TypedSTerm.t
  type untyped = STerm.t
  type typed = TypedSTerm.t
  type loc = ParseLocation.t
  exception Error of string
  val section : Util.Section.t
  module TyBuiltin :
    sig
      val ty : Builtin.t -> TypeInference.type_ option
      val ty_exn : Builtin.t -> TypeInference.type_
    end
  module Ctx :
    sig
      type t
      val create :
        ?default:TypeInference.type_ -> unit -> TypeInference.Ctx.t
      val copy : TypeInference.Ctx.t -> TypeInference.Ctx.t
      val exit_scope : TypeInference.Ctx.t -> unit
      val declare :
        TypeInference.Ctx.t -> ID.t -> TypeInference.type_ -> unit
      val pop_new_types :
        TypeInference.Ctx.t -> (ID.t * TypeInference.type_) list
    end
  val unify :
    ?loc:TypeInference.loc ->
    TypeInference.type_ -> TypeInference.type_ -> unit
  val infer_ty_exn :
    TypeInference.Ctx.t -> TypeInference.untyped -> TypeInference.type_
  val infer_ty :
    TypeInference.Ctx.t ->
    TypeInference.untyped -> TypeInference.type_ TypeInference.or_error
  val infer_exn :
    TypeInference.Ctx.t -> TypeInference.untyped -> TypeInference.typed
  val infer :
    TypeInference.Ctx.t ->
    TypeInference.untyped -> TypeInference.typed TypeInference.or_error
  val infer_prop_exn :
    TypeInference.Ctx.t -> TypeInference.untyped -> TypeInference.typed
  val infer_clause_exn :
    TypeInference.Ctx.t ->
    TypeInference.untyped list -> TypeInference.typed list
  val constrain_term_term_exn :
    ?loc:TypeInference.loc ->
    TypeInference.Ctx.t ->
    TypeInference.untyped -> TypeInference.untyped -> unit
  val constrain_term_type_exn :
    ?loc:TypeInference.loc ->
    TypeInference.Ctx.t ->
    TypeInference.untyped -> TypeInference.type_ -> unit
  val constrain_term_term :
    ?loc:TypeInference.loc ->
    TypeInference.Ctx.t ->
    TypeInference.untyped ->
    TypeInference.untyped -> unit TypeInference.or_error
  val constrain_term_type :
    ?loc:TypeInference.loc ->
    TypeInference.Ctx.t ->
    TypeInference.untyped ->
    TypeInference.type_ -> unit TypeInference.or_error
  type typed_statement =
      (TypeInference.typed, TypeInference.typed, TypeInference.type_,
       UntypedAST.attrs)
      Statement.t
  val infer_statement_exn :
    TypeInference.Ctx.t ->
    UntypedAST.statement ->
    TypeInference.typed_statement * TypeInference.typed_statement list
  val infer_statements_exn :
    ?ctx:TypeInference.Ctx.t ->
    UntypedAST.statement Sequence.t ->
    TypeInference.typed_statement CCVector.ro_vector
  val infer_statements :
    ?ctx:TypeInference.Ctx.t ->
    UntypedAST.statement Sequence.t ->
    TypeInference.typed_statement CCVector.ro_vector TypeInference.or_error
end