functor (T : Global_defs) ->
  sig
    val new_type : unit -> Types.t
    val new_nexp : unit -> Types.nexp
    val equate_types : Ast.l -> string -> Types.t -> Types.t -> unit
    val in_range : Ast.l -> Types.nexp -> Types.nexp -> unit
    val add_constraint : Path.t -> Types.t -> unit
    val add_length_constraint : Types.range -> unit
    val add_tyvar : Tyvar.t -> unit
    val add_nvar : Nvar.t -> unit
    val inst_leftover_uvars : Ast.l -> Types.typ_constraints
    val check_numeric_constraint_implication :
      Ast.l -> Types.range -> Types.range list -> unit
  end