Documentation for [letr1] and [letrn].

src/Solver.mli

@@ -249,8 +249,8 @@ module Make
      This constraint requires [∃α.c1(α)] to be satisfied. This is required
      even if the term variable [x] is not used in [c2].
 
-     Inside [c2], an instantiation constraint of the form [x(β)] is logically
-     equivalent to [c1(β)]. In other words, a [let] constraint acts like a
+     Inside [c2], an instantiation constraint of the form [x(α')] is logically
+     equivalent to [c1(α')]. In other words, a [let] constraint acts like a
      macro definition: every use of the variable [x] in the scope of this
      definition is equivalent to a copy of the constraint abstraction [c1].
 
@@ -332,21 +332,54 @@ module Make
      it can be passed as an argument to {!solve}. *)
   val let0: 'a co  -> (tyvars * 'a) co
 
-  (* [letr1 alphas x (fun alphavs v -> c1) c2] binds the scheme variable [x]
-     to the constraint abstraction [fun v -> c1] in the contstraint [c2],
-     where [c1] is also abstracted over a list of rigid variables, one for
-     each client type variable passed in the list [alphas]. *)
-  val letr1: int
-             -> tevar
-             -> (variables -> variable -> 'a co)
-             -> 'b co
-             -> (tyvars * scheme * 'a * 'b) co
-
-  val letrn: int
-             ->  tevars
-             -> (variables -> variables -> 'a co)
-             -> 'b co
-             -> (tyvars * schemes * 'a * 'b) co
+  (**[letr1] is a more general form of the combinator {!let1}. It takes an
+     integer parameter [k] and binds [k] rigid type variables [βs] in the
+     left-hand constraint. Like [let1], it also binds a type variable [α]
+     in the left-hand constraint. Thus, [c1] is a function of [βs] and [α]
+     to a constraint. On paper, we write [let x = Rβs.λα.c1(βs)(α) in c2].
+
+     This constraint requires [∀βs.∃α.c1(α)] to be satisfied.
+     This is required even if the term variable [x] is not used in [c2].
+     Thus, the variables [βs] are regarded as rigid while [c1] is solved.
+
+     Then, while solving [c2], the term variable [x] is bound to
+     the constraint abstraction [λα.∃βs.c1(βs)(α)].
+     In other words, inside [c2], an instantiation constraint of the form
+     [x(α')] is logically equivalent to [∃βs.c1(βs)(α')].
+     At this stage, the variables [βs] are no longer treated as rigid,
+     and can be instantiated.
+
+     The combinator [letr1] helps deal with programming language constructs
+     where one or more rigid variables are explicitly introduced, such as
+     [let id (type a) (x : a) : a = x in id 0] in OCaml. In this example,
+     the type variable [a] must be treated as rigid while type-checking the
+     left-hand side; then, the term variable [id] must receive the scheme
+     [∀a.a → a], where [a] is no longer regarded as rigid, so this scheme
+     can be instantiated to [int → int] while type-checking the right-hand
+     side. *)
+  val letr1:
+    (*  k: *) int ->
+    (*  x: *) tevar ->
+    (* c1: *) (variables -> variable -> 'a co) ->
+    (* c2: *) 'b co ->
+              (tyvars * scheme * 'a * 'b) co
+
+  (**[letrn] subsumes {!let1}, {!letr1}, and {!letrn}.
+
+     Like {!letr1}, it takes an integer parameter [k] and binds [k]
+     rigid type variables [βs] in the left-hand constraint.
+
+     Like {!letn}, it takes a list [xs] of term variables and binds a
+     corresponding list [αs] of type variables in the left-hand constraint.
+
+     On paper, we write [let xs = Rβs.λαs.c1(βs)(αs) in c2] for the
+     constraint that it constructs. *)
+  val letrn:
+    (*  k: *) int ->
+    (* xs: *) tevars ->
+    (* c1: *) (variables -> variables -> 'a co) ->
+    (* c2: *) 'b co ->
+              (tyvars * schemes * 'a * 'b) co
 
   (* ---------------------------------------------------------------------- *)
 
@@ -360,8 +393,9 @@ module Make
   (**The constraint [correlate range c] is equivalent to [c], but records that
      this constraint is correlated with the range [range] in the source code.
      This information is used in error reports. The exceptions {!Unbound},
-     {!Unify}, and {!Cycle} carry a range: it is the nearest range that
-     encloses the abstract syntax tree node where the error is detected. *)
+     {!Unify}, {!Cycle}, and {!VariableScopeEscape} carry a range: it is the
+     nearest range that encloses the abstract syntax tree node where the error
+     is detected. *)
   val correlate: range -> 'a co -> 'a co
 
   (** {2 Solving Constraints} *)