Module Ocaml_typing.Jkind

module Sort : sig ... end
type sort = Sort.t
module Sub_failure_reason : sig ... end
module Sub_result : sig ... end
module Layout : sig ... end
module Mod_bounds : sig ... end
module With_bounds : sig ... end

A jkind is a full description of the runtime representation of values of a given type. It includes sorts, but also the abstract top jkind Any and subjkinds of other sorts, such as Immediate.

The type parameter gives information about whether the jkind can meaningfully appear to the left of a subjkind check (this is an l-jkind) or on the right of a subjkind check (this is an r-jkind).

It may be convenient to use synonyms exported from Types:

* jkind_l: This is the jkind of an actual type; it is returned from estimate_type_jkind, for example. We can compute the joins (unions) of l-jkinds and check that an l-jkind is less than an r-jkind.

* jkind_r: This is the jkind we want some type to have. Type variables have r-jkinds (because we will someday instantiate those variables). The type passed to constrain_type_jkind is an r-jkind. We can compute the meets (intersections) of r-jkinds and check that an l-jkind is less than an r-jkind.

include Allowance.Allow_disallow with type (_, _, 'd) sided = 'd Types.jkind
type (_, _, 'd) sided = 'd Types.jkind
val disallow_right : ('a, 'b, 'l * 'r) sided -> ('a, 'b, 'l * Allowance.disallowed) sided

Disallows on the right.

val disallow_left : ('a, 'b, 'l * 'r) sided -> ('a, 'b, Allowance.disallowed * 'r) sided

Disallows a the left.

val allow_right : ('a, 'b, 'l * Allowance.allowed) sided -> ('a, 'b, 'l * 'r) sided

Generalizes a right-hand-side allowed to be any allowance.

val allow_left : ('a, 'b, Allowance.allowed * 'r) sided -> ('a, 'b, 'l * 'r) sided

Generalizes a left-hand-side allowed to be any allowance.

val try_allow_r : ('l * 'r) Types.jkind -> ('l * Allowance.allowed) Types.jkind option

Try to treat this jkind as an r-jkind.

module History : sig ... end
type jkind_context = {
  1. jkind_of_type : Types.type_expr -> Types.jkind_l option;
  2. is_abstract : Path.t -> bool;
}

Context for jkind operations.

module Violation : sig ... end
module Const : sig ... end
module Builtin : sig ... end
val unsafely_set_bounds : from:'d Types.jkind -> 'd Types.jkind -> 'd Types.jkind

Forcibly change the mod- and with-bounds of a t based on the mod- and with-bounds of from.

val add_with_bounds : modality:Mode.Modality.Const.t -> type_expr:Types.type_expr -> Types.jkind_l -> Types.jkind_l

Take an existing jkind_l and add some with-bounds.

val has_with_bounds : Types.jkind_l -> bool

Does this jkind have with-bounds?

val mark_best : ('l * 'r) Types.jkind -> ('l * Allowance.disallowed) Types.jkind

Mark the given jkind as best, meaning we can never learn any more information about it that will cause it to become lower in the preorder of kinds

val is_best : ('l * Allowance.disallowed) Types.jkind -> bool

Is the given kind best?

val of_new_sort_var : why:History.concrete_creation_reason -> level:int -> 'd Types.jkind * sort

Create a fresh sort variable, packed into a jkind, returning both the resulting kind and the sort.

val of_new_sort : why:History.concrete_creation_reason -> level:int -> 'd Types.jkind

Create a fresh sort variable, packed into a jkind.

val of_new_legacy_sort_var : why:History.concrete_legacy_creation_reason -> level:int -> 'd Types.jkind * sort

Same as of_new_sort_var, but the jkind is lowered to Non_null to mirror "legacy" OCaml values. Defaulting the sort variable produces exactly value.

val of_new_legacy_sort : why:History.concrete_legacy_creation_reason -> level:int -> 'd Types.jkind

Same as of_new_sort, but the jkind is lowered to Non_null to mirror "legacy" OCaml values. Defaulting the sort variable produces exactly value.

val of_new_non_float_sort_var : why:History.concrete_creation_reason -> level:int -> 'd Types.jkind * sort

Same as of_new_sort_var, but the jkind is lowered to Non_float. Defaulting the sort variable produces exactly the sort value.

val of_const : annotation:Ocaml_parsing.Parsetree.jkind_annotation option -> why:History.creation_reason -> quality:'d Types.jkind_quality -> ran_out_of_fuel_during_normalize:bool -> 'd Const.t -> 'd Types.jkind

Construct a jkind from a constant jkind, at quality Not_best

Construct a jkind from a builtin kind, at quality Best.

val of_annotation_option_default : default:('l * Allowance.allowed) Types.jkind -> context:('l * Allowance.allowed) History.annotation_context -> Ocaml_parsing.Parsetree.jkind_annotation option -> ('l * Allowance.allowed) Types.jkind

Find a jkind from a type declaration. Type declarations are special because the jkind may have been provided via : jkind syntax (which goes through Jane Syntax) or via the old-style [@@immediate] or [@@immediate64] attributes, and of_type_decl needs to look in two different places on the type_declaration to account for these two alternatives.

Returns the jkind (at quality Not_best) and the user-written annotation.

Raises if a disallowed or unknown jkind is present.

Find a jkind from a type declaration in the same way as of_type_decl, defaulting to ~default. Returns a jkind at quality Not_best; call mark_best to mark it as Best.

Raises if a disallowed or unknown jkind is present.

val for_boxed_record : Types.label_declaration list -> Types.jkind_l

Choose an appropriate jkind for a boxed record type

val for_unboxed_record : Types.label_declaration list -> Types.jkind_l

Choose an appropriate jkind for an unboxed record type.

val for_boxed_variant : loc:Ocaml_parsing.Location.t -> decl_params:Types.type_expr list -> type_apply: (Types.type_expr list -> Types.type_expr -> Types.type_expr list -> Types.type_expr) -> free_vars:(Types.type_expr list -> Btype.TypeSet.t) -> Types.constructor_declaration list -> Types.jkind_l

Choose an appropriate jkind for a boxed variant type.

decl_params is the parameters in the head of the type declaration. type_apply should be Ctype.apply partially applied to an env.

free_vars is a function that, given a list of Types.type_exprs that are used in the boxed variant, returns all type variables that are free within the Types.type_exprs. Ctype.free_variable_set_of_list is a good candidate for implementing this function.

val for_boxed_tuple : (string option * Types.type_expr) list -> Types.jkind_l

Choose an appropriate jkind for a boxed tuple type.

val for_boxed_row : Types.row_desc -> Types.jkind_l

Choose an appropriate jkind for a row type.

val for_arrow : Types.jkind_l

The jkind of an arrow type.

val for_object : Types.jkind_l

The jkind of an object type.

val for_float : Ident.t -> Types.jkind_l

The jkind of a float.

val for_non_float : why:History.value_creation_reason -> 'd Types.jkind

The jkind for values that are not floats.

val for_or_null_argument : Ident.t -> 'd Types.jkind

The jkind for or_null type arguments.

val for_abbreviation : type_jkind_purely:(Types.type_expr -> Types.jkind_l) -> modality:Mode.Modality.Const.t -> Types.type_expr -> Types.jkind_l

The jkind for an abbreviation declaration. This implements the design in rule FIND_ABBREV in kind-inference.md, where we consider a definition

  type ... = rhs

to have the kind <<layout of rhs>> mod everything with rhs. This is important to allow code like this to type-check:

  module M : sig
    type 'a t : value mod portable with 'a
  end = struct
    type 'a t = 'a
  end
val for_array_argument : Types.jkind_lr

The jkind for array type arguments.

val for_array_element_sort : level:int -> Types.jkind_lr * sort

The jkind for array elements, creating a new sort variable.

module Desc : sig ... end
val get : 'd Types.jkind -> 'd Desc.t

Get a description of a jkind.

val get_layout_defaulting_to_value : 'd Types.jkind -> Layout.Const.t

get_layout_defaulting_to_value extracts a constant layout, defaulting any sort variable to value.

val get_const : 'd Types.jkind -> 'd Const.t option

get_const returns a Const.t if the layout has no sort variables, returning None otherwise

val default_to_value : 'd Types.jkind -> unit

default_to_value t is ignore (get_layout_defaulting_to_value t)

val is_void_defaulting : 'd Types.jkind -> bool

is_void t is Void = get_layout_defaulting_to_value t. In particular, it will default the jkind to value if needed to make this false.

val sort_of_jkind : Types.jkind_l -> sort

Returns the sort corresponding to the jkind. Call only on representable jkinds - raises on Any.

val get_layout : 'd Types.jkind -> Layout.Const.t option

Gets the layout of a jkind; returns None if the layout is still unknown. Never does mutation.

val extract_layout : 'd Types.jkind -> Sort.t Layout.t

Gets the layout of a jkind, without looking through sort variables.

val get_mode_crossing : context:jkind_context -> 'd Types.jkind -> Mode.Crossing.t

Gets the mode crossing for types of this jkind.

val to_unsafe_mode_crossing : Types.jkind_l -> Types.unsafe_mode_crossing
val get_externality_upper_bound : context:jkind_context -> 'd Types.jkind -> Jkind_axis.Externality.t
val set_externality_upper_bound : Types.jkind_r -> Jkind_axis.Externality.t -> Types.jkind_r

Computes a jkind that is the same as the input but with an updated maximum mode for the externality axis

val get_nullability : context:jkind_context -> Types.jkind_l -> Jkind_axis.Nullability.t

Gets the nullability from a jkind.

val set_nullability_upper_bound : Types.jkind_r -> Jkind_axis.Nullability.t -> Types.jkind_r

Computes a jkind that is the same as the input but with an updated maximum mode for the nullability axis

val set_separability_upper_bound : Types.jkind_r -> Jkind_axis.Separability.t -> Types.jkind_r

Computes a jkind that is the same as the input but with an updated maximum mode for the separability axis

val set_layout : 'd Types.jkind -> Sort.t Layout.t -> 'd Types.jkind

Sets the layout in a jkind.

Change a jkind to be appropriate for a type that appears under a modality. This means that the jkind will definitely cross the axes modified by the modality, by setting the mod-bounds appropriately and propagating the modality into any with-bounds.

Change a jkind to be appropriate for an expectation of a type under a modality. This means that the jkind's axes affected by the modality will all be top. The with-bounds are left unchanged.

val apply_or_null_l : Types.jkind_l -> (Types.jkind_l, unit) result

Change a jkind to be appropriate for 'a or_null based on passed 'a. Adjusts nullability to be Maybe_null, and separability to be Maybe_separable if it is already Separable. If the jkind is already Maybe_null, fails.

val apply_or_null_r : Types.jkind_r -> (Types.jkind_r, unit) result

Change a jkind to be appropriate for an expectation of a type passed to the or_null constructor. Adjusts nullability to be Non_null, and separability to be Non_float if it is demanded to be Separable. If the jkind is already Non_null, fails.

val decompose_product : 'd Types.jkind -> 'd Types.jkind list option

Extract out component jkinds from the product. Because there are no product jkinds, this is a bit of a lie: instead, this decomposes the layout but just reuses the non-layout parts of the original jkind. Never does any mutation. Because it just reuses the mode information, the resulting jkinds are higher in the jkind lattice than they might need to be.

val get_annotation : 'd Types.jkind -> Ocaml_parsing.Parsetree.jkind_annotation option

Get an annotation (that a user might write) for this t.

type normalize_mode =
  1. | Require_best
    (*

    Normalize a jkind without losing any precision. That is, keep any with-bounds if the kind of the type is not best (a stronger kind may be found).

    *)
  2. | Ignore_best
    (*

    Normalize a left jkind, conservatively rounding up. That is, if the kind of a type is not best, use the not-best kind. The resulting jkind will have no with-bounds.

    *)
val normalize : mode:normalize_mode -> context:jkind_context -> Types.jkind_l -> Types.jkind_l
val set_outcometree_of_type : (Types.type_expr -> Outcometree.out_type) -> unit

Call these before trying to print.

val set_outcometree_of_modalities : (Types.mutability -> Mode.Modality.Const.t -> Outcometree.out_mode list) -> unit
val set_printtyp_path : (Format.formatter -> Path.t -> unit) -> unit

Provides the Printtyp.path formatter back up the dependency chain to this module.

val set_print_type_expr : (Format.formatter -> Types.type_expr -> unit) -> unit

Provides the type_expr formatter back up the dependency chain to this module.

val set_raw_type_expr : (Format.formatter -> Types.type_expr -> unit) -> unit

Provides the raw_type_expr formatter back up the dependency chain to this module.

val format : Format.formatter -> 'd Types.jkind -> unit
val format_expanded : Format.formatter -> 'd Types.jkind -> unit

Similar to format, but the kind is expanded as much as possible rather than written in terms of a kind abbreviation. This is used by Merlin.

val format_history : intro:(Format.formatter -> unit) -> Format.formatter -> 'd Types.jkind -> unit

Format the history of this jkind: what interactions it has had and why it is the jkind that it is. Might be a no-op: see display_histories in the implementation of the Jkind module.

The intro is something like "The jkind of t is".

val equate : Types.jkind_lr -> Types.jkind_lr -> bool

This checks for equality, and sets any variables to make two jkinds equal, if possible. e.g. equate on a var and value will set the variable to be value

val equal : Types.jkind_lr -> Types.jkind_lr -> bool

This checks for equality, but has the invariant that it can only be called when there is no need for unification; e.g. equal on a var and value will crash.

CR layouts (v1.5): At the moment, this is actually the same as equate!

val has_intersection : level:int -> 'd1 Types.jkind -> 'd2 Types.jkind -> bool

Checks whether two jkinds have a non-empty intersection. Might mutate sort variables. Works over any mix of l- and r-jkinds, because the only way not to have an intersection is by looking at the layout: all axes have a bottom element.

val intersection_or_error : type_equal:(Types.type_expr -> Types.type_expr -> bool) -> context:jkind_context -> reason:History.interact_reason -> level:int -> ('l1 * Allowance.allowed) Types.jkind -> ('l2 * Allowance.allowed) Types.jkind -> (('l1 * Allowance.allowed) Types.jkind, Violation.t) Result.t

Finds the intersection of two jkinds, constraining sort variables to create one if needed, or returns a Violation.t if an intersection does not exist. Can update the jkinds. The returned jkind's history consists of the provided reason followed by the history of the first jkind argument. That is, due to histories, this function is asymmetric; it should be thought of as modifying the first jkind to be the intersection of the two, not something that modifies the second jkind.

val sub : type_equal:(Types.type_expr -> Types.type_expr -> bool) -> context:jkind_context -> level:int -> Types.jkind_l -> Types.jkind_r -> bool

sub t1 t2 says whether t1 is a subjkind of t2. Might update either t1 or t2 to make their layouts equal.

type sub_or_intersect =
  1. | Sub
    (*

    The first jkind is a subjkind of the second.

    *)
  2. | Disjoint of Sub_failure_reason.t Ocaml_utils.Misc_stdlib.Nonempty_list.t
    (*

    The two jkinds have no common ground.

    *)
  3. | Has_intersection of Sub_failure_reason.t Ocaml_utils.Misc_stdlib.Nonempty_list.t
    (*

    The first jkind is not a subjkind of the second, but the two jkinds have an intersection: try harder.

    *)
val sub_or_intersect : type_equal:(Types.type_expr -> Types.type_expr -> bool) -> context:jkind_context -> level:int -> (Allowance.allowed * 'r) Types.jkind -> ('l * Allowance.allowed) Types.jkind -> sub_or_intersect

sub_or_intersect t1 t2 does a subtype check, returning a sub_or_intersect; see comments there for more info.

val sub_or_error : type_equal:(Types.type_expr -> Types.type_expr -> bool) -> context:jkind_context -> level:int -> (Allowance.allowed * 'r) Types.jkind -> ('l * Allowance.allowed) Types.jkind -> (unit, Violation.t) result

sub_or_error t1 t2 does a subtype check, returning an appropriate Violation.t upon failure.

val sub_jkind_l : type_equal:(Types.type_expr -> Types.type_expr -> bool) -> context:jkind_context -> level:int -> ?allow_any_crossing:bool -> Types.jkind_l -> Types.jkind_l -> (unit, Violation.t) result

Like sub, but compares a left jkind against another left jkind. Pre-condition: the super jkind must be fully settled; no variables which might be filled in later.

val round_up : context:jkind_context -> (Allowance.allowed * 'r) Types.jkind -> ('l * Allowance.allowed) Types.jkind

"round up" a jkind_l to a jkind_r such that the input is less than the output.

Map a function over types in upper_bounds

val is_max : ('l * Allowance.allowed) Types.jkind -> bool

Checks to see whether a right-jkind is the maximum jkind. Never does any mutation.

val mod_bounds_are_max : ('l * Allowance.allowed) Types.jkind -> bool

Checks to see whether a right-jkind's mod-bounds are the maximum mod-bounds. Never does any mutation.

val has_layout_any : ('l * Allowance.allowed) Types.jkind -> bool

Checks to see whether a jkind has layout any. Never does any mutation.

val is_value_for_printing : ignore_null:bool -> 'd Types.jkind -> bool

Checks whether a jkind is value. This really should require a jkind_lr, but it works on any jkind, because it's used in printing and is somewhat unprincipled.

module Debug_printers : sig ... end
module Error : sig ... end