Typo.

client/test/suite.t/run.t

@@ -346,3 +346,24 @@ its binding scope.
   r2
   and the type:
   r8
+
+
+The example below is incorrect, a rigid variable tries to escape
+its binding scope. The escape is only noticed at generalization
+time when adjusting levels.
+
+  $ cat >rigid-level-escape-later-wrong.midml <<EOF
+  > let g = fun f ->
+  >   (f : for 'a. 'a -> 'a)
+  > EOF
+
+In the example above,* the type of f is "old" relative to the
+rigid-introducing annotation, but we don't notice during the
+unification itself which only touches the arrow type ->, not the rigid
+variable 'a. The escape will be noticed at generalization time, when
+adjusting the level of the type nodes below the arrow.
+
+  $ midml rigid-level-escape-later-wrong.midml
+  Type inference and translation to System F...
+  Fatal error: exception Inferno.Generalization.Make(S).VariableEscapeScope(0, 1)
+  [2]

src/Generalization.ml

@@ -129,10 +129,17 @@ type 'a data = {
   mutable mark: mark;
 }
 
-(* [adjust_rank data k] is equivalent to [data.rank <- min k data.rank]. *)
+exception VariableEscapeScope of rank * rank
+
+(* [adjust_rank data k] is equivalent to [data.rank <- min k data.rank].
+   Only flexible variables can decrease their ranks. *)
 
 let adjust_rank (data : 'a data) (k : rank) =
-  if k < data.rank then data.rank <- k
+  if k < data.rank then
+    if data.status = Flexible then
+      data.rank <- k
+    else
+      raise (VariableEscapeScope (k, data.rank))
 
 (* The module [Data] satisfies the signature [USTRUCTURE] required by the
    functor [Unifier.Make]. *)
@@ -445,7 +452,7 @@ let discover_young_generation () =
    discovering a variable [v] cannot improve the value of [k] that we are
    pushing down).
 
-   In the presence of cycles, the upward propation phase is incomplete, in the
+   In the presence of cycles, the upward propagation phase is incomplete, in the
    sense that it may compute ranks that are higher than necessary. For
    instance, imagine a cycle at rank 2, such that every leaf that is reachable
    from this cycle is at rank 1. Then, in principle, this cycle can be demoted
@@ -668,7 +675,7 @@ let schemify (root : variable) : scheme =
 let exit ~rectypes roots =
 
   (* Because calls to [enter] and [exit] must be balanced, we must have: *)
-  assert (state.young >= 0);
+  assert (state.young >= base_rank);
 
   (* Discover the young variables. *)
   let generation = discover_young_generation() in

src/Solver.ml

@@ -492,7 +492,7 @@ let rec solve : type a . range -> a co -> a on_sol =
          side of a [let] construct. *)
       G.enter();
       (* Register the rigid prefix [rs] with th generalization engine. *)
-      let _ = List.map (fun v -> ubind v G.Rigid None) rs in
+      let urs = List.map (fun v -> ubind v G.Rigid None) rs in
       (* Register the variables [vs] with the generalization engine, just as
          if they were existentially bound in [c1]. This is what they are,
          basically, but they also serve as named entry points. *)
@@ -507,6 +507,8 @@ let rec solve : type a . range -> a co -> a on_sol =
          [generalizable] of the young variables that should be universally
          quantified here. *)
       let generalizable, ss = exit range ~rectypes vs in
+      (* All rigid variables of [rs] must be generalizable *)
+      assert (urs |> List.for_all (fun r -> List.mem r generalizable));
       List.iter (fun (_, v) -> uunbind v) xvs;
       (* Extend the environment [env] and compute the type schemes [xss]. *)
       let xss =