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.

[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).

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