Implicit Kind Declarations

Type variable names can be declared to have implicit kinds. A type variable with a name that has an implicit kind will be instantiated with that kind. Here’s an example:

[@@@implicit_kind: ('elt : word)]

type 'elt collection

val singleton : 'elt -> 'elt collection
val lenght : 'elt collection -> int

This signature is equivalent to:

type ('elt : word) collection

val singleton : ('elt : word) . 'elt -> 'elt collection
val lenght : ('elt : word) . 'elt collection -> int

You can declare implicit kinds for multiple variable names at once:

[@@@implicit_kind: ('a : immediate) * ('b : immediate)]

val swap : 'a * 'b -> 'b * 'a

Implicit kinds can’t be overridden – a variable declared with an implicit kind must always have that kind. Attempts to narrow or change it will fail:

module type S = sig
  [@@@implicit_kind: ('a : value_or_null)]
  val i : ('a : value mod external_) -> 'a
  val j : ('a : bits64) -> 'a
end

[%%expect{|
Line 3, characters 10-36:
3 |   val i : ('a : value mod external_) -> 'a
              ^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: The universal type variable 'a was declared to have kind value_or_null
       But it was inferred to have kind value mod external_
         because of the annotation on the type variable 'a.
|}]

Implicit kinds are inherited by signatures:

module type Outer = sig
  [@@@implicit_kind: ('t : bits64)]

  val outer : 't -> 't

  module Inner : sig
    (* Also [bits64] *)
    val inner : 't -> 't
  end
end

You can re-declare implicit kinds:

module type Outer = sig
  [@@@implicit_kind: ('t : bits64)]

  val outer : 't -> 't

  module Inner : sig
    [@@@implicit_kind: ('t : immediate)]

    val inner : 't -> 't
  end
end

Implicit kind declarations can be made in structures (or at the module toplevel):

module M = struct
  [@@@implicit_kind: ('elt : bits64)]

  let f : 'elt -> 'elt array = fun x -> [| x |]
end

Implicit kinds are lexical defaults, not a part of the module interface. They are syntactically limited to the signature or structure they are declared in and won’t be included:

module type S = sig
  [@@@implicit_kind: ('a : value_or_null) * ('b : immediate)]

  val fst : 'a * 'b -> 'a
end

module type T = sig
  include S

  (* ['a] and ['b] are defaulted to [value] here: *)
  val snd : 'a * 'b -> 'b
end

Implicit kinds affect constraints and are, for now, the only way to set constraints to certain kind values:

module Constrained : sig
  [@@@implicit_kind ('a : value_or_null) * ('b : value_or_null)]

  type 'c t constraint 'c = 'a * 'b
                       (* the only way to get [value_or_null] here *)
end

Topics

Implicit Kind Declarations