Skip to content

Commit 8181ef6

Browse files
goldfireregasche
andauthored
Document [row_more] (#3934)
Document [row_more] and [row_fixed]. Co-authored-by: Gabriel Scherer <[email protected]>
1 parent 8ee18ce commit 8181ef6

File tree

1 file changed

+45
-0
lines changed

1 file changed

+45
-0
lines changed

typing/types.mli

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -258,6 +258,8 @@ and arrow_desc =
258258

259259

260260

261+
(** See also documentation for [row_more], which enumerates how these
262+
constructors arise. *)
261263
and fixed_explanation =
262264
| Univar of type_expr (** The row type was bound to an univar *)
263265
| Fixed_private (** The row type is private *)
@@ -533,9 +535,52 @@ val create_row:
533535
name:(Path.t * type_expr list) option -> row_desc
534536

535537
val row_fields: row_desc -> (label * row_field) list
538+
539+
(** [row_more] returns a [type_expr] with one of the following [type_desc]s
540+
(also described with the return from [row_fixed], which varies similarly):
541+
542+
* [Tvar]: This is a row variable; it would occur in e.g. [val f :
543+
[> `A | `B] -> int]. When/if we learn more about a polymorphic variant, this
544+
variable might get unified with one of the other [type_desc]s listed here,
545+
or a [Tvariant] that represents a new set of constructors to add to the row.
546+
547+
During [constraint] checking (toward the end of checking a type declaration,
548+
in [Typedecl.check_constraints_rec]) we [Ctype.rigidify] a type to make it
549+
so that its unification variables will not unify. When a [Tvar] row variable
550+
is rigidified, its [fixed_explanation] will be [Rigid].
551+
552+
* [Tunivar]: This is a universally quantified row variable; it would occur
553+
in e.g. [type t = { f : 'a. ([> `A | `B ] as 'a) -> int }]. A [Tunivar] has
554+
a [fixed_explanation] of [Univar].
555+
556+
* [Tconstr]: There are two possible ways this can happen:
557+
558+
1. This is an abstract [#row] type created by a [private] row type, as in
559+
[type t = private [> `A | `B]]. In this case, the [fixed_explanation] will
560+
be [Fixed_private].
561+
562+
2. This is a locally abstract type created by [Ctype.reify], which happens
563+
when a row variable is free in the type of the scrutinee in a GADT pattern
564+
match. The [fixed_explanation] will be [Reified]. Note that any manifest
565+
of a reified row variable is actually ignored by [row_repr]; this causes
566+
some incompletness in type inference.
567+
568+
* [Tnil]: Used to denote a static polymorphic variant (with no [>] or [<]).
569+
570+
----------------------------------------
571+
572+
It is an invariant that row variables are never shared between different
573+
types. That is, if [row_more row1 == row_more row2], then [row1] and [row2]
574+
come from structurally identical [Tvariant]s (but they might not be
575+
physically equal). When copying types, two types with the same [row_more]
576+
field are replaced by the same copy.
577+
*)
536578
val row_more: row_desc -> type_expr
537579
val row_closed: row_desc -> bool
580+
581+
(** See documentation for [row_more]. *)
538582
val row_fixed: row_desc -> fixed_explanation option
583+
539584
val row_name: row_desc -> (Path.t * type_expr list) option
540585

541586
val set_row_name: row_desc -> (Path.t * type_expr list) option -> row_desc

0 commit comments

Comments
 (0)