sig
  type tnvar = Ty of Tyvar.t | Nv of Nvar.t
  val pp_tnvar : Format.formatter -> Types.tnvar -> unit
  val tnvar_to_rope : Types.tnvar -> Ulib.Text.t
  val tnvar_compare : Types.tnvar -> Types.tnvar -> int
  module TNvar :
    sig
      type t = Types.tnvar
      val compare : Types.TNvar.t -> Types.TNvar.t -> int
      val pp : Format.formatter -> Types.TNvar.t -> unit
    end
  module Pfmap :
    sig
      type k = Path.t
      module S :
        sig
          type elt = k
          type t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
          val split : elt -> t -> t * bool * t
        end
      type 'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val from_list : (k * 'a) list -> 'a t
      val from_list2 : k list -> 'a list -> 'a t
      val insert : 'a t -> k * 'a -> 'a t
      val union : 'a t -> 'a t -> 'a t
      val big_union : 'a t list -> 'a t
      val merge :
        (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val apply : 'a t -> k -> 'a option
      val in_dom : k -> 'a t -> bool
      val map : (k -> 'a -> 'b) -> 'a t -> 'b t
      val domains_overlap : 'a t -> 'b t -> k option
      val domains_disjoint : 'a t list -> bool
      val iter : (k -> 'a -> unit) -> 'a t -> unit
      val fold : ('a -> k -> 'b -> 'a) -> 'a -> 'b t -> 'a
      val filter : (k -> 'a -> bool) -> 'a t -> 'a t
      val remove : 'a t -> k -> 'a t
      val pp_map :
        (Format.formatter -> k -> unit) ->
        (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
      val domain : 'a t -> S.t
    end
  module Pset :
    sig
      type elt = Path.t
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
    end
  module TNfmap :
    sig
      type k = TNvar.t
      module S :
        sig
          type elt = k
          type t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
          val split : elt -> t -> t * bool * t
        end
      type 'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val from_list : (k * 'a) list -> 'a t
      val from_list2 : k list -> 'a list -> 'a t
      val insert : 'a t -> k * 'a -> 'a t
      val union : 'a t -> 'a t -> 'a t
      val big_union : 'a t list -> 'a t
      val merge :
        (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val apply : 'a t -> k -> 'a option
      val in_dom : k -> 'a t -> bool
      val map : (k -> 'a -> 'b) -> 'a t -> 'b t
      val domains_overlap : 'a t -> 'b t -> k option
      val domains_disjoint : 'a t list -> bool
      val iter : (k -> 'a -> unit) -> 'a t -> unit
      val fold : ('a -> k -> 'b -> 'a) -> 'a -> 'b t -> 'a
      val filter : (k -> 'a -> bool) -> 'a t -> 'a t
      val remove : 'a t -> k -> 'a t
      val pp_map :
        (Format.formatter -> k -> unit) ->
        (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
      val domain : 'a t -> S.t
    end
  module TNset :
    sig
      type elt = TNvar.t
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val pp : Format.formatter -> t -> unit
    end
  type t_uvar
  type n_uvar
  type t = { mutable t : Types.t_aux; }
  and t_aux =
      Tvar of Tyvar.t
    | Tfn of Types.t * Types.t
    | Ttup of Types.t list
    | Tapp of Types.t list * Path.t
    | Tbackend of Types.t list * Path.t
    | Tne of Types.nexp
    | Tuvar of Types.t_uvar
  and nexp = { mutable nexp : Types.nexp_aux; }
  and nexp_aux =
      Nvar of Nvar.t
    | Nconst of int
    | Nadd of Types.nexp * Types.nexp
    | Nmult of Types.nexp * Types.nexp
    | Nneg of Types.nexp
    | Nuvar of Types.n_uvar
  type range =
      LtEq of Ast.l * Types.nexp
    | Eq of Ast.l * Types.nexp
    | GtEq of Ast.l * Types.nexp
  val range_with : Types.range -> Types.nexp -> Types.range
  val range_of_n : Types.range -> Types.nexp
  val mk_gt_than : Ast.l -> Types.nexp -> Types.nexp -> Types.range
  val mk_eq_to : Ast.l -> Types.nexp -> Types.nexp -> Types.range
  val compare : Types.t -> Types.t -> int
  val multi_fun : Types.t list -> Types.t -> Types.t
  val type_subst : Types.t Types.TNfmap.t -> Types.t -> Types.t
  val nexp_subst : Types.t Types.TNfmap.t -> Types.nexp -> Types.nexp
  val free_vars : Types.t -> Types.TNset.t
  val is_var_type : Types.t -> bool
  val is_instance_type : Types.t -> bool
  val tnvar_to_name : Types.tnvar -> Name.t
  val tnvar_to_type : Types.tnvar -> Types.t
  val tnvar_split : Types.tnvar list -> Types.tnvar list * Types.tnvar list
  type const_descr_ref
  val string_of_const_descr_ref : Types.const_descr_ref -> string
  module Cdmap :
    sig
      type k = const_descr_ref
      module S :
        sig
          type elt = k
          type t
          val empty : t
          val is_empty : t -> bool
          val mem : elt -> t -> bool
          val add : elt -> t -> t
          val singleton : elt -> t
          val remove : elt -> t -> t
          val union : t -> t -> t
          val inter : t -> t -> t
          val diff : t -> t -> t
          val compare : t -> t -> int
          val equal : t -> t -> bool
          val subset : t -> t -> bool
          val iter : (elt -> unit) -> t -> unit
          val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
          val for_all : (elt -> bool) -> t -> bool
          val exists : (elt -> bool) -> t -> bool
          val filter : (elt -> bool) -> t -> t
          val partition : (elt -> bool) -> t -> t * t
          val cardinal : t -> int
          val elements : t -> elt list
          val min_elt : t -> elt
          val max_elt : t -> elt
          val choose : t -> elt
          val split : elt -> t -> t * bool * t
        end
      type 'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val from_list : (k * 'a) list -> 'a t
      val from_list2 : k list -> 'a list -> 'a t
      val insert : 'a t -> k * 'a -> 'a t
      val union : 'a t -> 'a t -> 'a t
      val big_union : 'a t list -> 'a t
      val merge :
        (k -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val apply : 'a t -> k -> 'a option
      val in_dom : k -> 'a t -> bool
      val map : (k -> 'a -> 'b) -> 'a t -> 'b t
      val domains_overlap : 'a t -> 'b t -> k option
      val domains_disjoint : 'a t list -> bool
      val iter : (k -> 'a -> unit) -> 'a t -> unit
      val fold : ('a -> k -> 'b -> 'a) -> 'a -> 'b t -> 'a
      val filter : (k -> 'a -> bool) -> 'a t -> 'a t
      val remove : 'a t -> k -> 'a t
      val pp_map :
        (Format.formatter -> k -> unit) ->
        (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
      val domain : 'a t -> S.t
    end
  module Cdset :
    sig
      type elt = const_descr_ref
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
    end
  type 'a cdmap
  val cdmap_empty : unit -> 'a Types.cdmap
  val cdmap_lookup : 'a Types.cdmap -> Types.const_descr_ref -> 'a option
  val cdmap_update :
    'a Types.cdmap -> Types.const_descr_ref -> 'a -> 'a Types.cdmap
  val cdmap_insert :
    'a Types.cdmap -> 'a -> 'a Types.cdmap * Types.const_descr_ref
  val cdmap_domain : 'a Types.cdmap -> Types.const_descr_ref list
  val nil_const_descr_ref : Types.const_descr_ref
  val is_nil_const_descr_ref : Types.const_descr_ref -> bool
  type ('a, 'b) annot = {
    term : 'a;
    locn : Ast.l;
    typ : Types.t;
    rest : 'b;
  }
  val annot_to_typ : ('a, 'b) Types.annot -> Types.t
  type ident_option = Id_none of Ast.lex_skips | Id_some of Ident.t
  type 'a id = {
    id_path : Types.ident_option;
    id_locn : Ast.l;
    descr : 'a;
    instantiation : Types.t list;
  }
  and src_t = (Types.src_t_aux, unit) Types.annot
  and src_t_aux =
      Typ_wild of Ast.lex_skips
    | Typ_var of Ast.lex_skips * Tyvar.t
    | Typ_len of Types.src_nexp
    | Typ_fn of Types.src_t * Ast.lex_skips * Types.src_t
    | Typ_tup of (Types.src_t, Ast.lex_skips) Seplist.t
    | Typ_app of Path.t Types.id * Types.src_t list
    | Typ_backend of Path.t Types.id * Types.src_t list
    | Typ_paren of Ast.lex_skips * Types.src_t * Ast.lex_skips
  and src_nexp = {
    nterm : Types.src_nexp_aux;
    nloc : Ast.l;
    nt : Types.nexp;
  }
  and src_nexp_aux =
      Nexp_var of Ast.lex_skips * Nvar.t
    | Nexp_const of Ast.lex_skips * int
    | Nexp_mult of Types.src_nexp * Ast.lex_skips * Types.src_nexp
    | Nexp_add of Types.src_nexp * Ast.lex_skips * Types.src_nexp
    | Nexp_paren of Ast.lex_skips * Types.src_nexp * Ast.lex_skips
  val src_t_to_t : Types.src_t -> Types.t
  val src_type_subst :
    Types.src_t Types.TNfmap.t -> Types.src_t -> Types.src_t
  val id_alter_init_lskips :
    (Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips) ->
    'a Types.id -> 'a Types.id * Ast.lex_skips
  val typ_alter_init_lskips :
    (Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips) ->
    Types.src_t -> Types.src_t * Ast.lex_skips
  val nexp_alter_init_lskips :
    (Ast.lex_skips -> Ast.lex_skips * Ast.lex_skips) ->
    Types.src_nexp -> Types.src_nexp * Ast.lex_skips
  type constr_family_descr = {
    constr_list : Types.const_descr_ref list;
    constr_exhaustive : bool;
    constr_case_fun : Types.const_descr_ref option;
    constr_default : bool;
    constr_targets : Target.Targetset.t;
  }
  type type_target_rep =
      TYR_simple of Ast.l * bool * Ident.t
    | TYR_subst of Ast.l * bool * Types.tnvar list * Types.src_t
  type type_descr = {
    type_tparams : Types.tnvar list;
    type_abbrev : Types.t option;
    type_varname_regexp : string option;
    type_fields : Types.const_descr_ref list option;
    type_constr : Types.constr_family_descr list;
    type_rename : (Ast.l * Name.t) Target.Targetmap.t;
    type_target_rep : Types.type_target_rep Target.Targetmap.t;
  }
  type class_descr = {
    class_tparam : Types.tnvar;
    class_record : Path.t;
    class_methods : (Types.const_descr_ref * Types.const_descr_ref) list;
    class_rename : (Ast.l * Name.t) Target.Targetmap.t;
    class_target_rep : Types.type_target_rep Target.Targetmap.t;
    class_is_inline : bool;
  }
  type tc_def = Tc_type of Types.type_descr | Tc_class of Types.class_descr
  type type_defs = Types.tc_def Types.Pfmap.t
  val type_defs_update_tc_type :
    Ast.l ->
    Types.type_defs ->
    Path.t ->
    (Types.type_descr -> Types.type_descr option) -> Types.type_defs
  val type_defs_update_tc_class :
    Ast.l ->
    Types.type_defs ->
    Path.t ->
    (Types.class_descr -> Types.class_descr option) -> Types.type_defs
  val type_defs_update_fields :
    Ast.l ->
    Types.type_defs ->
    Path.t -> Types.const_descr_ref list -> Types.type_defs
  val type_defs_add_constr_family :
    Ast.l ->
    Types.type_defs -> Path.t -> Types.constr_family_descr -> Types.type_defs
  val type_defs_get_constr_families :
    Ast.l ->
    Types.type_defs ->
    Target.target ->
    Types.t -> Types.const_descr_ref -> Types.constr_family_descr list
  val type_defs_lookup_typ :
    Ast.l -> Types.type_defs -> Types.t -> Types.type_descr option
  val type_defs_lookup :
    Ast.l -> Types.type_defs -> Path.t -> Types.type_descr
  val type_defs_update :
    Types.type_defs -> Path.t -> Types.type_descr -> Types.type_defs
  val mk_tc_type_abbrev : Types.tnvar list -> Types.t -> Types.tc_def
  val mk_tc_type : Types.tnvar list -> string option -> Types.tc_def
  val match_types : Types.t -> Types.t -> Types.t Types.TNfmap.t option
  type instance = {
    inst_l : Ast.l;
    inst_is_default : bool;
    inst_binding : Path.t;
    inst_class : Path.t;
    inst_type : Types.t;
    inst_tyvars : Types.tnvar list;
    inst_constraints : (Path.t * Types.tnvar) list;
    inst_methods : (Types.const_descr_ref * Types.const_descr_ref) list;
    inst_dict : Types.const_descr_ref;
  }
  type typ_constraints =
      Tconstraints of Types.TNset.t * (Path.t * Types.tnvar) list *
        Types.range list
  val head_norm : Types.type_defs -> Types.t -> Types.t
  val dest_fn_type :
    Types.type_defs option -> Types.t -> (Types.t * Types.t) option
  val strip_fn_type :
    Types.type_defs option -> Types.t -> Types.t list * Types.t
  val check_equal : Types.type_defs -> Types.t -> Types.t -> bool
  val assert_equal :
    Ast.l -> string -> Types.type_defs -> Types.t -> Types.t -> unit
  val compare_expand : Types.type_defs -> Types.t -> Types.t -> int
  type instance_ref
  val string_of_instance_ref : Types.instance_ref -> string
  type i_env
  val empty_i_env : Types.i_env
  val i_env_add :
    Types.i_env -> Types.instance -> Types.i_env * Types.instance_ref
  val i_env_lookup :
    Ast.l -> Types.i_env -> Types.instance_ref -> Types.instance
  val get_matching_instance :
    Types.type_defs ->
    Path.t * Types.t ->
    Types.i_env -> (Types.instance * Types.t Types.TNfmap.t) option
  val nexp_from_list : Types.nexp list -> Types.nexp
  module type Global_defs =
    sig val d : Types.type_defs val i : Types.i_env end
  module Constraint :
    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
  val pp_type : Format.formatter -> Types.t -> unit
  val pp_nexp : Format.formatter -> Types.nexp -> unit
  val pp_range : Format.formatter -> Types.range -> unit
  val pp_class_constraint : Format.formatter -> Path.t * Types.tnvar -> unit
  val pp_instance : Format.formatter -> Types.instance -> unit
  val pp_typschm :
    Format.formatter ->
    Types.tnvar list -> (Path.t * Types.tnvar) list -> Types.t -> unit
  val t_to_string : Types.t -> string
  val print_debug_typ_raw : string -> Types.t list -> unit
  val t_to_var_name : Types.t -> Name.t
end