rec_check.ml: fix a bug in recursive class declarations check.

(cherry picked from commit 9e45a79)

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

This work was conducted by Alban Reynaud during an internship at INRIA
Saclay, with the help and under the supervision of Gabriel Scherer in
the Parsifal team.

A summary is included below. For more details, see

  https://github.com/Cemoixerestre/Internship-2018-ocaml-recursive-value

or the comments in the code itself, which has evolved a bit from
Alban's internship report above.

Summary:
--------

Rec_check is based on the idea of assigning "access modes" to variables

    m ::= Dereference (* full access and inspection of the value *)
        | Unguarded (* the value result is directly returned *)
        | Guard (* the value is stored under a data constructor *)
        | Delayed (* the value is not needed at definition time *)
        | Unused (* the value is not used at all *)

Before this patchset, the implementation (contributed by Jeremy Yallop)
was formulated as a type-checker manipulating "uses", which are mappings
from free variables to modes

    u ::= (x : m)*

and contexts Γ mapping variables to uses

    Γ ::= (x : u)*

The check relied on a judgment of the form

    Γ ⊢ e : u

where, in the typing algorithm, `Γ` and `e` are the inputs, and `u` is
the output — this could be written `-Γ ⊢ e : +u`.

After this patchset, the implementation uses a simpler notion of context
mapping variables to mods

    Γ ::= (x : m)*

and the judgment has the simpler structure

     Γ ⊢ e : m

but now `m` is an input to the judgment, indicating in which usage
context `e` is checked, and `Γ` is the output: `+Γ ⊢ e : -m`.

Other fixes:
------------

This patchset also fixes a soundness bug around `{ foo with ... }`
which is already present in 4.06 and 4.07.

Another soundness bug found during this work was submitted and fixed
independently as GPR ocaml#1915.

This work also led to the refactoring of GPR ocaml#1922, and the refactoring
of the testsuite in GPR ocaml#1937.

Co-authored-by: cuihtlauac <cuihtlauac@users.noreply.github.com>