Ensure that types from packed modules are always generalised

[stedolan]

The type system ensures that in the right-hand side of a type definition type t = foo, the type foo is always generalised.

This invariant is violated in one case, when the right-hand side comes not from the module language but from a with constraint on a first class module (e.g. (module T with type t = foo)). In this case, types with level below generic_level could end up in declarations.

In older versions of OCaml, I think this still occurred but mostly was ignored. When OCaml 4.13 (specifically, #10277) introduced stricter level and scope checking, this issue began to cause some code to spuriously fail to typecheck. Under OCaml 4.14 and later, the second example in the attached test yields the following nonsensical error message:

Error: Signature mismatch:
       Modules do not match:
         sig type t = foo end
       is not included in
         sig type t = int end
       Type declarations do not match:
         type t = foo
       is not included in
         type t = int
       The type foo = int is not equal to the type int

where foo is simultaneously equal to and not equal to int.

The fix is to ensure that the type is at generic_level before adding it to the environment, by calling Ctype.correct_levels.

[garrigue]

Well spotted. The fix is correct.
In this case the types are given explicitly somewhere, so there is no question of principality on those parameters.

[Octachron]

The fix looks worthwhile to backport to 4.14 (and 5.0), any objections @garrigue ?

[garrigue]

No problem with backporting. This is clearly a simple bug fix.

[Octachron]

Cherry picked on 5.0 (as aecdd88) and 4.14 (as bc510ed). I have cherry-picked #11340 to 4.14 along the way to avoid a conflict since this change seemed worthy of a backport to 4.14 too.