sig
  module Field :
    sig
      type name = SurfaceSyntax.Field.name
      type t = name
      val register : string -> name
      val print : name -> string
      val equal : name -> name -> bool
      val compare : name -> name -> int
      val hash : name -> int
      module Map :
        sig
          type key = name
          type 'a t
          val empty : 'a t
          val lookup : key -> 'a t -> 'a
          val find : key -> 'a t -> 'a
          val add : key -> 'a -> 'a t -> 'a t
          exception Unchanged
          val strict_add : key -> 'a -> 'a t -> 'a t
          type 'a decision = 'a -> 'a -> 'a
          val fine_add : 'a decision -> key -> 'a -> 'a t -> 'a t
          val mem : key -> 'a t -> bool
          val singleton : key -> 'a -> 'a t
          val is_empty : 'a t -> bool
          val is_singleton : 'a t -> (key * 'a) option
          val cardinal : 'a t -> int
          val choose : 'a t -> key * 'a
          val lookup_and_remove : key -> 'a t -> 'a * 'a t
          val find_and_remove : key -> 'a t -> 'a * 'a t
          val remove : key -> 'a t -> 'a t
          val union : 'a t -> 'a t -> 'a t
          val fine_union : 'a decision -> 'a t -> 'a t -> 'a t
          val iter : (key -> 'a -> unit) -> 'a t -> unit
          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val fold_rev : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
          val iter2 : (key -> 'a -> 'b -> unit) -> 'a t -> 'b t -> unit
          val map : ('a -> 'b) -> 'a t -> 'b t
          val endo_map : ('a -> 'a) -> 'a t -> 'a t
          val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
          module Domain :
            sig
              type element = key
              type t
              val empty : t
              val is_empty : t -> bool
              val singleton : element -> t
              val cardinal : t -> int
              val choose : t -> element
              val mem : element -> t -> bool
              val add : element -> t -> t
              val remove : element -> t -> t
              val union : t -> t -> t
              val diff : t -> t -> t
              val inter : t -> t -> t
              val disjoint : t -> t -> bool
              val iter : (element -> unit) -> t -> unit
              val fold : (element -> 'b -> 'b) -> t -> 'b -> 'b
              val elements : t -> element list
              val compare : t -> t -> int
              val equal : t -> t -> bool
              val subset : t -> t -> bool
            end
          val domain : 'a t -> Domain.t
          val lift : (key -> 'a) -> Domain.t -> 'a t
          val corestrict : 'a t -> Domain.t -> 'a t
        end
      val memoize : (name -> 'a) -> name -> 'a
      val p : Buffer.t -> name -> unit
    end
  type name = User of Module.name * Variable.name | Auto of Variable.name
  type location = Lexing.position * Lexing.position
  type quantifier = Forall | Exists
  type type_binding = TypeCore.name * Kind.kind * TypeCore.location
  type flavor =
    SurfaceSyntax.binding_flavor =
      UserIntroduced
    | AutoIntroduced
  type db_index = int
  type var
  type data_field_def = TypeCore.Field.name * TypeCore.typ
  and typ =
      TyUnknown
    | TyDynamic
    | TyBound of TypeCore.db_index
    | TyOpen of TypeCore.var
    | TyQ of TypeCore.quantifier * TypeCore.type_binding * TypeCore.flavor *
        TypeCore.typ
    | TyApp of TypeCore.typ * TypeCore.typ list
    | TyTuple of TypeCore.typ list
    | TyConcrete of TypeCore.branch
    | TySingleton of TypeCore.typ
    | TyArrow of TypeCore.typ * TypeCore.typ
    | TyBar of TypeCore.typ * TypeCore.typ
    | TyAnchoredPermission of TypeCore.typ * TypeCore.typ
    | TyEmpty
    | TyStar of TypeCore.typ * TypeCore.typ
    | TyAnd of TypeCore.mode_constraint * TypeCore.typ
  and mode_constraint = Mode.mode * TypeCore.typ
  and branch = {
    branch_flavor : DataTypeFlavor.flavor;
    branch_datacon : TypeCore.resolved_datacon;
    branch_fields : TypeCore.data_field_def list;
    branch_adopts : TypeCore.typ;
  }
  and resolved_datacon = TypeCore.typ * Datacon.name
  type variance =
    SurfaceSyntax.variance =
      Invariant
    | Covariant
    | Contravariant
    | Bivariant
  type type_def =
      Concrete of TypeCore.typ list
    | Abstract
    | Abbrev of TypeCore.typ
  type data_type = {
    data_name : Variable.name;
    data_location : TypeCore.location;
    data_definition : TypeCore.type_def;
    data_variance : TypeCore.variance list;
    data_fact : Fact.fact;
    data_kind : Kind.kind;
  }
  type data_type_group = {
    group_recursive : SurfaceSyntax.rec_flag;
    group_items : TypeCore.data_type list;
  }
  module DataconMap :
    sig
      type key = Module.name * Datacon.name
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val keys : 'a t -> key list
      val union : 'a t -> 'a t -> 'a t
      val inter : 'a t -> 'a t -> 'a t
      val minus : 'a t -> 'a t -> 'a t
      val xor : 'a t -> 'a t -> 'a t
      val to_list : 'a t -> (key * 'a) list
      val find_opt : key -> 'a t -> 'a option
    end
  module VarMap :
    sig
      type key = var
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> 'a -> 'a t -> 'a t
      val singleton : key -> 'a -> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
      val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val for_all : (key -> 'a -> bool) -> 'a t -> bool
      val exists : (key -> 'a -> bool) -> 'a t -> bool
      val filter : (key -> 'a -> bool) -> 'a t -> 'a t
      val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('a -> 'b) -> 'a t -> 'b t
      val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
      val keys : 'a t -> key list
      val union : 'a t -> 'a t -> 'a t
      val inter : 'a t -> 'a t -> 'a t
      val minus : 'a t -> 'a t -> 'a t
      val xor : 'a t -> 'a t -> 'a t
      val to_list : 'a t -> (key * 'a) list
      val find_opt : key -> 'a t -> 'a option
    end
  module IVarMap :
    sig
      type key = var
      type 'data t
      val create : unit -> 'data t
      val clear : 'data t -> unit
      val add : key -> 'data -> 'data t -> unit
      val find : key -> 'data t -> 'data
      val iter : (key -> 'data -> unit) -> 'data t -> unit
    end
  type env
  val empty_env : TypeCore.env
  val locate : TypeCore.env -> TypeCore.location -> TypeCore.env
  val location : TypeCore.env -> TypeCore.location
  val module_name : TypeCore.env -> Module.name
  val enter_module : TypeCore.env -> Module.name -> TypeCore.env
  val is_inconsistent : TypeCore.env -> bool
  val mark_inconsistent : TypeCore.env -> TypeCore.env
  val modify_kenv :
    TypeCore.env ->
    (TypeCore.var KindCheck.env ->
     (TypeCore.var KindCheck.env -> (TypeCore.env -> 'a) -> 'a) -> 'a) ->
    'a
  val kenv : TypeCore.env -> TypeCore.var KindCheck.env
  val is_flexible : TypeCore.env -> TypeCore.var -> bool
  val is_rigid : TypeCore.env -> TypeCore.var -> bool
  val modulo_flex : TypeCore.env -> TypeCore.typ -> TypeCore.typ
  val import_flex_instanciations_raw :
    TypeCore.env -> TypeCore.env -> TypeCore.env
  val instantiate_flexible_raw :
    TypeCore.env -> TypeCore.var -> TypeCore.typ -> TypeCore.env option
  val same : TypeCore.env -> TypeCore.var -> TypeCore.var -> bool
  val merge_left :
    TypeCore.env -> TypeCore.var -> TypeCore.var -> TypeCore.env option
  val get_floating_permissions : TypeCore.env -> TypeCore.typ list
  val set_floating_permissions :
    TypeCore.env -> TypeCore.typ list -> TypeCore.env
  val get_names : TypeCore.env -> TypeCore.var -> TypeCore.name list
  val get_name : TypeCore.env -> TypeCore.var -> TypeCore.name
  val get_kind : TypeCore.env -> TypeCore.var -> Kind.kind
  val get_fact : TypeCore.env -> TypeCore.var -> Fact.fact
  val get_locations : TypeCore.env -> TypeCore.var -> TypeCore.location list
  val get_definition :
    TypeCore.env -> TypeCore.var -> TypeCore.type_def option
  val get_variance : TypeCore.env -> TypeCore.var -> TypeCore.variance list
  val add_location :
    TypeCore.env -> TypeCore.var -> TypeCore.location -> TypeCore.env
  val get_permissions : TypeCore.env -> TypeCore.var -> TypeCore.typ list
  val set_permissions :
    TypeCore.env -> TypeCore.var -> TypeCore.typ list -> TypeCore.env
  val reset_permissions : TypeCore.env -> TypeCore.var -> TypeCore.env
  val set_fact : TypeCore.env -> TypeCore.var -> Fact.fact -> TypeCore.env
  val set_definition :
    TypeCore.env ->
    TypeCore.var ->
    TypeCore.type_def -> TypeCore.variance list -> TypeCore.env
  val update_definition :
    TypeCore.env ->
    TypeCore.var -> (TypeCore.type_def -> TypeCore.type_def) -> TypeCore.env
  val update_variance :
    TypeCore.env ->
    TypeCore.var ->
    (TypeCore.variance list -> TypeCore.variance list) -> TypeCore.env
  exception UnboundPoint
  val clean : TypeCore.env -> TypeCore.env -> TypeCore.typ -> TypeCore.typ
  val equal : TypeCore.env -> TypeCore.typ -> TypeCore.typ -> bool
  val resolved_datacons_equal :
    TypeCore.env ->
    TypeCore.resolved_datacon -> TypeCore.resolved_datacon -> bool
  val construct_branch :
    TypeCore.type_binding list ->
    TypeCore.branch -> TypeCore.typ list -> TypeCore.typ
  val find_branch : TypeCore.typ -> TypeCore.branch
  val touch_branch :
    TypeCore.typ -> (TypeCore.branch -> TypeCore.branch) -> TypeCore.typ
  val bind_rigid :
    TypeCore.env -> TypeCore.type_binding -> TypeCore.env * TypeCore.var
  val bind_flexible :
    TypeCore.env -> TypeCore.type_binding -> TypeCore.env * TypeCore.var
  val bind_flexible_before :
    TypeCore.env ->
    TypeCore.type_binding -> TypeCore.var -> TypeCore.env * TypeCore.var
  val fold_definitions :
    TypeCore.env ->
    ('acc -> TypeCore.var -> TypeCore.type_def -> 'acc) -> 'acc -> 'acc
  val fold_terms :
    TypeCore.env ->
    ('acc -> TypeCore.var -> TypeCore.typ list -> 'acc) -> 'acc -> 'acc
  val fold : TypeCore.env -> ('acc -> TypeCore.var -> 'acc) -> 'acc -> 'acc
  val map : TypeCore.env -> (TypeCore.var -> 'a) -> 'a list
  val is_marked : TypeCore.env -> TypeCore.var -> bool
  val mark : TypeCore.env -> TypeCore.var -> TypeCore.env
  val refresh_mark : TypeCore.env -> TypeCore.env
  class virtual ['env, 'result] visitor :
    object
      method extend : 'env -> Kind.kind -> 'env
      method normalize : 'env -> TypeCore.typ -> TypeCore.typ
      method virtual tyanchoredpermission :
        'env -> TypeCore.typ -> TypeCore.typ -> 'result
      method virtual tyand :
        'env -> TypeCore.mode_constraint -> TypeCore.typ -> 'result
      method virtual tyapp :
        'env -> TypeCore.typ -> TypeCore.typ list -> 'result
      method virtual tyarrow :
        'env -> TypeCore.typ -> TypeCore.typ -> 'result
      method virtual tybar : 'env -> TypeCore.typ -> TypeCore.typ -> 'result
      method virtual tybound : 'env -> TypeCore.db_index -> 'result
      method virtual tyconcrete : 'env -> TypeCore.branch -> 'result
      method virtual tydynamic : 'env -> 'result
      method virtual tyempty : 'env -> 'result
      method virtual tyopen : 'env -> TypeCore.var -> 'result
      method virtual tyq :
        'env ->
        TypeCore.quantifier ->
        TypeCore.type_binding -> TypeCore.flavor -> TypeCore.typ -> 'result
      method virtual tysingleton : 'env -> TypeCore.typ -> 'result
      method virtual tystar : 'env -> TypeCore.typ -> TypeCore.typ -> 'result
      method virtual tytuple : 'env -> TypeCore.typ list -> 'result
      method virtual tyunknown : 'env -> 'result
      method visit : 'env -> TypeCore.typ -> 'result
    end
  class ['env] map :
    object
      method branch : 'env -> TypeCore.branch -> TypeCore.branch
      method data_type_group :
        'env -> TypeCore.data_type_group -> TypeCore.data_type_group
      method extend : 'env -> Kind.kind -> 'env
      method field :
        'env -> TypeCore.data_field_def -> TypeCore.data_field_def
      method normalize : 'env -> typ -> typ
      method resolved_datacon :
        'env -> TypeCore.resolved_datacon -> TypeCore.resolved_datacon
      method tyanchoredpermission :
        'env -> TypeCore.typ -> TypeCore.typ -> TypeCore.typ
      method tyand :
        'env -> TypeCore.mode_constraint -> TypeCore.typ -> TypeCore.typ
      method tyapp :
        'env -> TypeCore.typ -> TypeCore.typ list -> TypeCore.typ
      method tyarrow : 'env -> TypeCore.typ -> TypeCore.typ -> TypeCore.typ
      method tybar : 'env -> TypeCore.typ -> TypeCore.typ -> TypeCore.typ
      method tybound : 'env -> TypeCore.db_index -> TypeCore.typ
      method tyconcrete : 'env -> TypeCore.branch -> TypeCore.typ
      method tydynamic : 'env -> TypeCore.typ
      method tyempty : 'env -> TypeCore.typ
      method tyopen : 'env -> TypeCore.var -> TypeCore.typ
      method tyq :
        'env ->
        TypeCore.quantifier ->
        TypeCore.type_binding ->
        TypeCore.flavor -> TypeCore.typ -> TypeCore.typ
      method tysingleton : 'env -> TypeCore.typ -> TypeCore.typ
      method tystar : 'env -> TypeCore.typ -> TypeCore.typ -> TypeCore.typ
      method tytuple : 'env -> TypeCore.typ list -> TypeCore.typ
      method tyunknown : 'env -> TypeCore.typ
      method visit : 'env -> typ -> TypeCore.typ
    end
  class ['env] iter :
    object
      method branch : 'env -> TypeCore.branch -> unit
      method data_type_group : 'env -> TypeCore.data_type_group -> unit
      method extend : 'env -> Kind.kind -> 'env
      method field : 'env -> TypeCore.data_field_def -> unit
      method normalize : 'env -> typ -> typ
      method resolved_datacon : 'env -> TypeCore.resolved_datacon -> unit
      method tyanchoredpermission :
        'env -> TypeCore.typ -> TypeCore.typ -> unit
      method tyand : 'env -> TypeCore.mode_constraint -> TypeCore.typ -> unit
      method tyapp : 'env -> TypeCore.typ -> TypeCore.typ list -> unit
      method tyarrow : 'env -> TypeCore.typ -> TypeCore.typ -> unit
      method tybar : 'env -> TypeCore.typ -> TypeCore.typ -> unit
      method tybound : 'env -> TypeCore.db_index -> unit
      method tyconcrete : 'env -> TypeCore.branch -> unit
      method tydynamic : 'env -> unit
      method tyempty : 'env -> unit
      method tyopen : 'env -> TypeCore.var -> unit
      method tyq :
        'env ->
        TypeCore.quantifier ->
        TypeCore.type_binding -> TypeCore.flavor -> TypeCore.typ -> unit
      method tysingleton : 'env -> TypeCore.typ -> unit
      method tystar : 'env -> TypeCore.typ -> TypeCore.typ -> unit
      method tytuple : 'env -> TypeCore.typ list -> unit
      method tyunknown : 'env -> unit
      method visit : 'env -> typ -> unit
    end
  val ty_bottom : TypeCore.typ
  val is_non_bottom : TypeCore.typ -> TypeCore.typ option
  val internal_ptype :
    (Buffer.t -> TypeCore.env * TypeCore.typ -> unit) Pervasives.ref
  val internal_pnames :
    (Buffer.t -> TypeCore.env * TypeCore.name list -> unit) Pervasives.ref
  val internal_ppermissions :
    (Buffer.t -> TypeCore.env -> unit) Pervasives.ref
  val internal_pfact : (Buffer.t -> Fact.fact -> unit) Pervasives.ref
  val internal_pflexlist : Buffer.t -> TypeCore.env -> unit
  val internal_uniqvarid : TypeCore.env -> TypeCore.var -> int
  val internal_checklevel : TypeCore.env -> TypeCore.typ -> unit
  val internal_wasflexible : TypeCore.var -> bool
end