`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.