Module `Jkind`

module Jkind0 := Btype.Jkind0

module Sort : sig ... end

type sort = Sort.t

module Sub_failure_reason : sig ... end

module Sub_result : sig ... end

module Scannable_axes : sig ... end

module Layout : sig ... end

module Mod_bounds : sig ... end

module With_bounds : sig ... end

module Base_and_axes : 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 = {

jkind_of_type : Types.type_expr -> Types.jkind_l option;
is_abstract : Path.t -> bool;
lookup_type : Path.t -> Types.type_declaration option;

}

Context for jkind operations.

module Violation : sig ... end

module Const : sig ... end

module Builtin : sig ... end

val unsafely_set_bounds : 
  Env.t ->
  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 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 instance : 'd Types.jkind -> 'd Types.jkind

Apply Sort.instance to every sort variable in a jkind.

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_sort_univar : 
  why:History.concrete_creation_reason ->
  Jkind_types.Sort.univar ->
  'd Types.jkind

Create a jkind with a specific sort univar (for layout-polymorphic types).

val of_annotation : 
  ?use_abstract_jkinds:bool ->
  context:('l * Allowance.allowed) History.annotation_context ->
  Env.t ->
  Parsetree.jkind_annotation ->
  ('l * Allowance.allowed) Types.jkind

val of_annotation_option_default : 
  ?use_abstract_jkinds:bool ->
  default:('l * Allowance.allowed) Types.jkind ->
  context:('l * Allowance.allowed) History.annotation_context ->
  Env.t ->
  Parsetree.jkind_annotation option ->
  ('l * Allowance.allowed) Types.jkind

val of_type_decl : 
  ?use_abstract_jkinds:bool ->
  context:History.annotation_context_l ->
  transl_type:(Parsetree.core_type -> Types.type_expr) ->
  Env.t ->
  Parsetree.type_declaration ->
  (Types.jkind_l * Parsetree.jkind_annotation option) option

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.

use_abstract_jkinds controls whether references to other kinds here count as uses of them for unused abstract kind warnings.

val of_type_decl_overapproximate_unknown : 
  context:History.annotation_context_l ->
  Env.t ->
  Parsetree.type_declaration ->
  Types.jkind_l option

Find a jkind from a type declaration in the same way as of_type_decl, but avoiding translating types in with-bounds. Overapproximates kinds containing with-bounds as any.

Returns the jkind (at quality Not_best).

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 ->
  sort Layout.t list ->
  Types.jkind_l

Choose an appropriate jkind for an unboxed record type.

val for_boxed_variant : 
  loc:Location.t ->
  decl_params:Types.type_expr list ->
  type_apply:
    (Types.type_expr list ->
      Types.type_expr ->
      Types.type_expr list ->
      Types.type_expr) ->
  get_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.

get_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_non_float : why:History.value_creation_reason -> 'd Types.jkind

The jkind for values that are not floats.

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_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_scannable : 
  Env.t ->
  'd Types.jkind ->
  Layout.Const.t option

get_layout_defaulting_to_scannable extracts a constant layout, defaulting any sort variable to scannable. Returns None in the case of an abstract kind.

val default_to_scannable : 'd Types.jkind -> unit

default_to_scannable t is ignore (get_layout_defaulting_to_scannable t)

val generalize : current_level:int -> 'd Types.jkind -> unit

Generalize the sorts in a jkind when in sort generalization context. Only has an effect when called within Sort.generalize_with.

val sort_of_jkind : Env.t -> Types.jkind_l -> sort

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

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

Gets the layout of a jkind; returns None if the layout is still unknown, or the (fully expanded) kind is abstract. Never does mutation.

val extract_layout : 
  Env.t ->
  'd Types.jkind ->
  (Sort.t Layout.t, Path.t) result

Gets the layout of a jkind, without looking through sort variables. Returns Error p if the kind is abstract (and its layout is therefore unknown).

val get_mode_crossing : 
  context:jkind_context ->
  Env.t ->
  '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 ->
  Env.t ->
  '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 : 
  Env.t ->
  'd Types.jkind ->
  Jkind_axis.Nullability.t option

Gets the nullability from a jkind. Expands abstract kinds if needed.

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

Computes a jkind that is the same as the input but with an updated nullability on the layout's scannable axis

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

Computes a jkind that is the same as the input but with an updated separability on the layout's scannable axis

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

Sets the layout in a jkind.

val apply_modality_l : 
  Mode.Modality.Const.t ->
  (Allowance.allowed * 'r) Types.jkind ->
  Types.jkind_l

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.

val apply_modality_r : 
  Mode.Modality.Const.t ->
  ('l * Allowance.allowed) Types.jkind ->
  Types.jkind_r

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 : Env.t -> '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 -> Parsetree.jkind_annotation option

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

type normalize_mode =

| 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).
*)
| 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 ->
  Env.t ->
  Types.jkind_l ->
  Types.jkind_l

val set_outcometrees_of_types : 
  (Types.type_expr list -> Outcometree.out_type list) ->
  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_doc.formatter -> Path.t -> unit) -> unit

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

val set_print_type_expr : Types.type_expr Format_doc.printer -> 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 : Env.t -> Format_doc.formatter -> 'd Types.jkind -> unit

module Format_verbosity : sig ... end

val format_verbose : 
  verbosity:Format_verbosity.t ->
  Env.t ->
  Format_doc.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_doc.formatter -> unit) ->
  Env.t ->
  Format_doc.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 : Env.t -> 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 : Env.t -> 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 may_have_intersection : Env.t -> '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.

When abstract kinds are involved and we cannot determine whether there is an intersection, this conservatively returns true.

type 'd intersection_result =

| Intersection of 'd Types.jkind
| No_intersection of Violation.t
| Unknown
(*
Unknown can happen in the case of computing an intersection with an abstract kind. In cases related to GADT matching, we need to distinguish it from the No_intersection result to avoid unsoundly believing match cases are unreachable.
*)

val intersection : 
  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
  context:jkind_context ->
  reason:History.interact_reason ->
  Env.t ->
  ('l1 * Allowance.allowed) Types.jkind ->
  ('l2 * Allowance.allowed) Types.jkind ->
  ('l1 * Allowance.allowed) intersection_result

val intersection_or_error : 
  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
  context:jkind_context ->
  reason:History.interact_reason ->
  Env.t ->
  ('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.

Note: When abstract kinds are involved and we cannot determine whether there is an intersection, this returns Error since we can't prove the intersection exists. Use intersection_result if you need to distinguish this case from definite non-intersection.

val sub : 
  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
  context:jkind_context ->
  Env.t ->
  (Allowance.allowed * 'r) Types.jkind ->
  ('l * Allowance.allowed) Types.jkind ->
  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 =

| Sub
(*
The first jkind is a subjkind of the second.
*)
| Disjoint of Sub_failure_reason.t Misc.Nonempty_list.t
(*
The two jkinds have no common ground.
*)
| May_have_intersection of Sub_failure_reason.t Misc.Nonempty_list.t
(*
The first jkind is not a subjkind of the second, but the two jkinds may have an intersection: try harder.
*)

val sub_or_intersect : 
  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
  context:jkind_context ->
  Env.t ->
  (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 ->
  Env.t ->
  (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_layout_or_error : 
  context:jkind_context ->
  Env.t ->
  (Allowance.allowed * 'r1) Types.jkind ->
  ('l2 * 'r2) Types.jkind ->
  (unit, Violation.t) result

sub_layout t1 t2 says whether t1's layout is a sublayout of t2s. Might update either t1 or t2 to make their layouts equal. Does not check bounds at all.

val sub_jkind_l : 
  type_equal:(Types.type_expr -> Types.type_expr -> bool) ->
  context:jkind_context ->
  ?allow_any_crossing:bool ->
  Env.t ->
  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 ->
  Env.t ->
  (Allowance.allowed * 'r) Types.jkind ->
  ('l * Allowance.allowed) Types.jkind option

"round up" a jkind_l to a jkind_r such that the input is less than the output. If the base is abstract, it may not be possible to eliminate the with bounds, in which case this returns None.

val map_type_expr : 
  (Types.type_expr -> Types.type_expr) ->
  (Allowance.allowed * 'r) Types.jkind ->
  (Allowance.allowed * 'r) Types.jkind

Map a function over types in upper_bounds

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

Checks to see whether a right-jkind is the maximum jkind. Never does any mutation. Is conservative and does not do any expansion.

val mod_bounds_are_obviously_max : 'd Types.jkind -> bool

Checks to see whether a jkind's mod bounds are max. Never does any mutation. Is conservative and does not do any expansion.

val fully_expand_aliases : Env.t -> 'd Types.jkind -> 'd Types.jkind

Fully expands the jkind's base - useful to avoid expanding twice for clients that both want to inspect the mod bounds and apply other functions to the jkind that would expand it.

val has_layout_any : Env.t -> ('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 -> Env.t -> '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 Jkind

Module `Jkind`