functor (T : TermInner.S) ->
  sig
    type t
    val empty :
      ?check_non_empty_tys:bool ->
      ?env:(T.t, T.t) Env.t -> unit -> TypeCheck.Make.t
    val check_statement :
      TypeCheck.Make.t -> (T.t, T.t) Statement.t -> TypeCheck.Make.t
    val check_problem : TypeCheck.Make.t -> (T.t, T.t) Problem.t -> unit
  end