error messages: include module inclusion errors for first class modules

[Octachron]

Currently, the error message for subtyping errors on first class modules:

module type XY = sig  val x: int val y: int end
module type XYZ = sig include XY val z:int end
let convert x = (x: < f : < g : int -> (module XY); h:int >; i:int > :> <f: <g: int -> (module XYZ) > >)

stops abruptly at the frontier between the core level and the module level:

Error: Type < f : < g : int -> (module XYZ); h : int >; i : int >
      is not a subtype of < f : < g : int -> (module XY) > >
      Type (module XY) is not a subtype of (module XYZ)

This PR proposes to expand the subtyping error message with the inclusion trace for first class modules:

Error: Type < f : < g : int -> (module XY); h : int >; i : int >
      is not a subtype of < f : < g : int -> (module XYZ) > >
      Type (module XY) is not a subtype of (module XYZ)
      Modules do not match: XY is not included in XYZ
      The value z is required but not provided

This changes also makes it possible to explain that if

let convert x = (x: (module XYZ):>(module XY))

fails with

Error: Type (module XYZ) is not a subtype of (module XY)

it is because the first-class module subtyping relationship requires that the two first-class modules share the same
memory representation:

Error: Type (module XYZ) is not a subtype of (module XY)
      The two first-class module types differ by their runtime size.

[gasche]

(cc @lthls)

[gasche]

In principle the change looks fine, I think this only needs a review for reasonableness and non-regression inside the type checker.

[lthls]

I don't know enough of the type checker to vouch for the safety of this patch, but it looks reasonable.
My comments are a mix of style nitpicks and brain dumps of why I believe the code is correct; I don't think any of them should be blocking so I'm approving right now. Feel free to address my comments as you see fit.

[lthls]

Could we have a comment explaining the n < 0 case ?
My understanding is that before this patch, we couldn't reach the n < 0 case because it would have caused another error earlier.
With this patch we also use this code in contexts where the condition can occur, but n < 0 implies that there is a Tcoerce_alias or Tcoerce_primitive coercion and we will get a better message error using the first_non_id function below.

[Octachron]

Indeed, the previous state of the code was using the invariant that it was only called on equivalent module types. Thus the coercion was necessarily a permutation of components.

Maybe

(* if n < 0, this is not a permutation but a kind coercion, which will be covered in the first_non_id case *)

?

[lthls]

I don't know how it reads for someone familiar with this part of the code, but I spent some time wondering why we did not report this as an error before eventually managing to find that not_fixpoint runs before first_non_id and so we would get worse messages if we did not skip this case.
So I would prefer if you could manage to fit somewhere in the comment that n < 0 is not a fixpoint (or rename not_fixpoint to find_permutation, this way your proposed comment becomes very clear).

[Octachron]

Hm, there are too many negative here: n<0 is not a transposition (aka not not-a-fixpoint in the permutation). But this is indeed a sign that the names should be improved: find_transposition should be clearer (probably even for people that don't have the definition of transposition in mind?).

[lthls]

That works for me, indeed. Although the functions transposition and transposition_under now return a change that could be a transposition or not, so maybe a few more names need to be adapted.
If you don't want to spend too much time on this, you can also just adopt the comment in your earlier suggestion and leave further cleanup to an hypothetical future PR.

[Octachron]

I have changed few more names to better reflect that we are now extracting a small atomic change from any coercion rather than just a transposition from a permutation.

[gasche]

If I understand correctly, @Octachron did a substantial change just now, and we need a second review round of @lthls (or someone else) before we can merge.

[Octachron]

Indeed, after discussion with @lthls , it sounded better to re-review the PR after this change since it makes the PR substantially simpler while covering more case of first-class module related error messages.

[lthls]

Yes, I had already looked at the new commit and I plan to redo a review (I've tried to find a way to mark my previous review as stale, the closest I could fine was re-requesting a review, which also works).

[lthls]

This looks more obviously correct than the previous version.

[lthls]

Same as below, position could be plural (or runtime components could be singular).

[shindere]

It seems the dependencies need to be updated, make alldepend.

Would have done it but was not sure how many commits you wanted to keep.

If you want to keep several commits and several of them change the
dependencies, it's IMHO nice if each commit includes the dependency
updates it induces.

[Octachron]

I squashed and merged all commit together, since in this case there was conceptually a single change with one back-and-forth iteration.