Module Mlsem_types.FieldCtx

Decorrelation of row variables.

A row variable stands for "all the fields other than those named explicitly", so the same row variable occurring in two record types that mention different labels does not stand for the same thing. Solving constraints over such types requires first replacing each row variable by a combination of fresh per-label variables — that is what a field context records, so that the solution can afterwards be expressed back in terms of the original variables.

type fvar = RVar.t * string

An original row variable together with the label it was split on.

type t
val of_ty : RVarSet.t -> Ty.t -> t

of_ty mono ty builds the context splitting the row variables of ty that are not in mono, over the labels ty mentions.

val of_tys : RVarSet.t -> Ty.t list -> t
val decorrelate : t -> Ty.t -> Ty.t

Rewrites a type in terms of the context's fresh per-label variables.

val recombine : t -> Ty.t -> Ty.t

Inverse of decorrelate.

val recombine' : t -> Mlsem_types__.Tvar.Subst.t -> Mlsem_types__.Tvar.Subst.t

recombine applied to a substitution obtained on decorrelated types, yielding a substitution over the original row variables.

val fresh_vars : t -> RVarSet.t
val fvar_of_fresh_var : t -> RVar.t -> fvar option

Which original variable and label a fresh variable came from; None if it is not one of the context's fresh variables.

val empty : t
val merge : t -> t -> t
val merge_many : t list -> t