Compare commits

...

2 Commits

Author SHA1 Message Date
Olivier dcdafa9ed6 Typo. 2022-03-24 14:41:24 +01:00
collaprog 26990b928f Fix rigid variables escaping. 2022-03-24 14:41:14 +01:00
3 changed files with 35 additions and 5 deletions

View File

@ -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]

View File

@ -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

View File

@ -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 =