Neutral ~> Return here?

Good catch, I'll fix this.

There are a couple TODO remaining, is it on purpose?

Yes, I wanted @yallop to have a chance to comment on them, because he wrote the original implementation. I believe that using Guard here would be correct, but I wanted his opinion before making the check more liberal than the one we replace. (Other opinions are also welcome, of course.)

It's a dereference because writing a value to a mutable field involves accessing the value. Here's a program that fails with a segmentation fault if Dereference is weakened to Return here:

    type t = { mutable f: float }
    let g = { f = 0.0 }
    let rec x = (g.f <- y; ()) and y = 2.0

(You could add the program to the test suite.)

abording ~> aborting ?

The first underscore can be turned into a [] which saves a few brain cycles to the reader.

Deref -> Dereference

This last case confused me for a moment, because I read it as Guard[m] = m, which is not the case.
Because of the earlier m', Return -> m' innocuous-looking case we have Guard[Return] = Guard, and Guard[m] = m otherwise.
I wonder if it would be worth adding an explicit (redundant) case for Guard[Return], to showcase more explicitly the role of the Guard mode.

identifiers in e -> identifiers in l
Also, ungarded of dereferenced -> dereferenced or returned ?

unguarded e l -> dependent e l, identifiers in e -> identifiers in l

It would maybe nice to have a comment indicating that environments sharing bindings is supported, and that in that case the right thing happens (the most conservative mode is picked).

@gasche says a better name for this could be join

Shouldn't 'a be ... instead, to match the convention used in the line above?

Which one of Gamma and Gamma' is the exterior (resp interior) environment?

There's an issue with this rule I think (name collision on G; and the final output of the rule is likely not just one of the two Gs in the scope).
Would the correct rule be something like as follows?

       G |- e : m + m'
       -----------------------------------
       x:m', G, G' |- (let x = e : m) -| x:m', G'

(also, I assume m + m' is prec m m'? whatever it is it should be made explicit)

(done)

This is in contradiction with the comment above? (which says that bind_judg takes an interior environment and returns an exterior environment)

(also, I assume m + m' is prec m m'? whatever it is it should be made explicit)

The closing parenthesis is off there.

Minor: more conservative, not most.

I think "most conservative" could be clarified here: it means something like "the more demanding context".

Minor: I think Unused should be Discard or Ignore, since all the others are verbs. (Alternatively, change them all to adjectives: Dereferenced, Returned, etc.)

I went for Ignore, to me Discard includes the idea of an (active) action.

Minor: compos? Why not compose?

Aside: 'not' patterns would be useful here.

Besides noting that Return is neutral for composition, you might also note that compos is associative (I checked that it is), and that Unused is an annihilator.

Two things to fix in this comment: it should say "dependent", not "unguarded", and it should say "in l", not "in e"

This should say "where (m) is an input of the code"

It's a dereference because writing a value to a mutable field involves accessing the value. Here's a program that fails with a segmentation fault if Dereference is weakened to Return here:

    type t = { mutable f: float }
    let g = { f = 0.0 }
    let rec x = (g.f <- y; ()) and y = 2.0

(You could add the program to the test suite.)

As with Texp_setfield, this really should be a Dereference, so we can drop the TODO.

Here's a program for the test suite that fails with a segmentation fault if Dereference is weakened to Return:

    class c = object
      val mutable f = 0.0
      method m =
        let rec x = (f <- y; ()) and y = 2.0 in f
    end
    let _ = print_float (new c)#m

I'm expecting this to break when somebody implements (e.g.) the lazy value optimization for unboxed constructors. (But perhaps having the common code in Typeopt will be enough to prevent that.)

Yes, I'm expecting such future changes to return one of the known-to-be-shortcut variants (for unboxed constructors, typically the classifier of the underlying argument), or to add a new variants to be handled properly here.

This looks like unnecessary churn.

"weird"? That word doesn't make you look confident...

It doesn't, because we aren't. The code must be safe because Dereference is the most conservative possible choice for eo, but I still have mostly no idea what this eo thing does (despite having looked at the compilation scheme). It's right that people hitting this case would be less-confident and would want (if they are changing it) to check things by themselves.

but I still have mostly no idea what this eo thing does

I'm not sure how much "mostly" covers here, but the eo is for representing calls to a superclass method through an ancestor variable, like this:

class b = object
  method m = 0
end
class d = object
  inherit b as parent   (* 'parent' is an ancestor *)
  method m = parent#m  (* Call to method 'm' in class 'b' *)
end