Refactoring : change the functors' order of application.

client/Infer.ml

@@ -40,6 +40,9 @@ module O = struct
     | S.TyConstr (tyconstr, ts) ->
         F.TyConstr(tyconstr, ts)
 
+  let abstract n =
+    F.TyConstr(Datatype.Type (Printf.sprintf "Abstract#%d" n), [])
+
   let mu x t =
     F.TyMu (x, t)
 

client/bin/midml.ml

@@ -5,6 +5,7 @@ let rectypes =
   ref false
 
 let test_ok filename =
+  ignore (Sys.command ("cat " ^ Filename.quote filename));
   match from_file filename with
   | exception (ParsingError range) ->
     Printf.eprintf "%!%sSyntax error.\n%!"

client/test/suite.t/run.t

@@ -340,7 +340,7 @@ its binding scope.
   $ midml rigid-level-escape-wrong.midml
   Type inference and translation to System F...
   File "test", line 2, characters 12-13:
-  A rigid variable at level 1 escaped its scope when we tried to decrease it at level 0.
+  A rigid variable escapes its scope.
 
 
 The example below is incorrect, a rigid variable tries to escape
@@ -360,4 +360,4 @@ adjusting the level of the type nodes below the arrow.
   $ midml rigid-level-escape-later-wrong.midml
   Type inference and translation to System F...
   File "test", line 2, characters 2-24:
-  A rigid variable at level 1 escaped its scope when we tried to decrease it at level 0.
+  A rigid variable escapes its scope.

src/Generalization.ml

@@ -11,7 +11,7 @@
 
 open Signatures
 
-module Make (S : STRUCTURE_LEAF) = struct
+module Make (UserS : HSTRUCTURE) = struct
 
 (* -------------------------------------------------------------------------- *)
 
@@ -50,13 +50,8 @@ type rank =
 let base_rank =
   0
 
-
 (* -------------------------------------------------------------------------- *)
 
-(* Rigid variables have a fixed rank -- lowering their rank is an error --
-   and a fixed leaf structure -- unifying them with a non-leaf structure
-   is an error. *)
-
 (* We want to be able to mark an equivalence class as either "active" or
    "generic". The unifier works with active variables only; it never sees a
    generic variable. Generic variables are used as part of the representation
@@ -71,15 +66,7 @@ let base_rank =
 (* An active variable is intended to become generic some day. A generic
    variable never becomes active again. *)
 
-type status = Rigid | Flexible | Generic
-
-type rigidity = Rigid | Flexible
-
-let status_of_rigidity : rigidity -> status = function
-  | Flexible ->
-     Flexible
-  | Rigid ->
-     Rigid
+type status = Active | Generic
 
 (* -------------------------------------------------------------------------- *)
 
@@ -109,6 +96,16 @@ let fresh_mark : unit -> mark =
 
 (* -------------------------------------------------------------------------- *)
 
+(* We define a [structure] type which is either abstract or a user-defined
+   structure from the module S.
+   Rigid variables have abstract strucutres.
+ *)
+
+module AS = Structure.AbstractS(UserS)
+module S = Structure.OptionS(AS)
+
+(* -------------------------------------------------------------------------- *)
+
 (* The type ['a data] groups all of the information that we associate with an
    equivalence class. *)
 
@@ -125,21 +122,47 @@ type 'a data = {
   id: id;
   mutable structure: 'a S.structure;
   mutable rank: rank;
+  mutable scope: rank;
   mutable status: status;
   mutable mark: mark;
 }
 
-exception VariableScopeEscape of int * int
-
-(* [adjust_rank data k] is equivalent to [data.rank <- min k data.rank].
-   Only flexible variables can decrease their ranks. *)
+(* Ranks correspond to binding sites / De Bruijn levels, and they also
+   determine a lexical regions within the source program: the part of
+   the program where the variable is "in scope". Lowering the rank of
+   a variable moves its binding site closer to the root of the term
+   and widens the lexical region.
+
+   Certain types are only valid (well-formed) within certain lexical
+   regions. For example the type [int -> a], if [a] is a locally-bound
+   rigid/polymorphic variable, is only valid within the scope of [a].
+   In addition to a "rank", our inference variables will also have a
+   "scope", that tracks their lexical region of validity. This "scope"
+   is also represented by the [rank] type, and the well-formedness
+   invariant is that the [rank] of a variable must always be above its
+   [scope]: its binding site lies within its region of
+   well-formedness. *)
+
+exception VariableScopeEscape of { rank: rank; scope: rank }
+
+(* The rank of variable must always be above its scope. *)
+let check_rank_scope (data : 'a data) =
+  if data.rank < data.scope then
+    raise (VariableScopeEscape {rank = data.rank; scope = data.scope})
 
 let adjust_rank (data : 'a data) (k : rank) =
-  if k < data.rank then
-    if data.status = Flexible then
-      data.rank <- k
-    else
-      raise (VariableScopeEscape (k, data.rank))
+  assert (data.status = Active);
+  if k < data.rank then begin
+    data.rank <- k;
+    check_rank_scope data;
+  end
+
+let adjust_scope (data : 'a data) (s : rank) =
+  assert (data.status = Active);
+  if s > data.scope then begin
+    data.scope <- s;
+    check_rank_scope data;
+  end
 
 (* The module [Data] satisfies the signature [USTRUCTURE] required by the
    functor [Unifier.Make]. *)
@@ -155,10 +178,10 @@ module Data = struct
   let dummy : mark =
     fresh_mark()
 
-  let make structure rank status =
+  let make structure ~rank ~scope status =
     let id = fresh_id() in
     let mark = dummy in
-    { id; structure; rank; status; mark }
+    { id; structure; rank; scope; status; mark }
 
   let map f data =
     { data with structure = S.map f data.structure }
@@ -187,45 +210,37 @@ module Data = struct
      fresh identifier. Here, we keep an arbitrary identifier. *)
 
   let conjunction equate data1 data2 =
+    assert (data1.status <> Generic);
+    assert (data2.status <> Generic);
     let id = data1.id in
     (* The new structural constraint is the logical conjunction of the two
        structural constraints. *)
     let structure = S.conjunction equate data1.structure data2.structure in
     (* The new rank is the minimum of the two ranks. *)
     let rank = min data1.rank data2.rank in
-    adjust_rank data1 rank;
-    adjust_rank data2 rank;
-    let fail () = raise InconsistentConjunction in
-    (* If either variables is rigid, the conjunction is also rigid. *)
-    let status : status =
-      match data1.status, data2.status with
-      | Generic, _
-      | _, Generic ->
-         assert false
-      | Flexible, Flexible ->
-         Flexible
-      (* One cannot unify two rigid variables, *)
-      | Rigid, Rigid ->
-         fail ()
-      | Rigid, Flexible ->
-         (* ... or give it a non-leaf structure. *)
-         if not (S.is_leaf structure) then fail ();
-         Rigid
-      | Flexible, Rigid ->
-         (* ... or give it a non-leaf structure. *)
-         if not (S.is_leaf structure) then fail ();
-         Rigid
-    in
+    (* The new scope is the maximum of the two scopes. *)
+    let scope = max data1.scope data2.scope in
+    (* If the scope becomes greater than the rank, it means we tried to use
+     * an equation outside of its scope. *)
+    if rank < scope then
+      raise (VariableScopeEscape { rank; scope });
+    let status : status = Active in
     (* There is no need to preserve marks during unification. *)
     let mark = dummy in
-    { id; structure; rank; status; mark }
+    { id; structure; rank; scope; status; mark }
 
   let is_leaf data =
     S.is_leaf data.structure
 
-  let project data =
+  let project (data : 'a structure) =
     data.structure
 
+  let rank (data : 'a structure) =
+    data.rank
+
+  let scope (data : 'a structure) =
+    data.scope
+
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -319,12 +334,21 @@ let register v r =
 (* When a fresh unification variable is created, it receives the current rank,
    and it is immediately registered at this rank. *)
 
-let fresh (rigidity : rigidity) structure =
-  let r = state.young in
-  if rigidity = Rigid then
-    assert (S.is_leaf structure);
-  let v = U.fresh (Data.make structure r (status_of_rigidity rigidity)) in
-  register v r;
+let fresh structure =
+  let rank = state.young in
+  let scope = base_rank in
+  let v = U.fresh (Data.make structure ~rank ~scope Active) in
+  register v rank;
+  v
+
+let fresh_rigid =
+  let fresh_abstract = Utils.gensym() in
+  fun () ->
+  let structure = Some (Structure.Abstract (fresh_abstract ())) in
+  let rank = state.young in
+  let scope = rank in
+  let v = U.fresh (Data.make structure ~rank ~scope Active) in
+  register v rank;
   v
 
 (* -------------------------------------------------------------------------- *)
@@ -473,7 +497,7 @@ let update_ranks generation =
 
     (* A postcondition of [traverse v] is [U.rank v <= k]. (This is downward
        propagation.) [traverse v] returns the updated rank of [v]. *)
-    let rec traverse v : rank =
+    let rec traverse v =
       let data = get v in
       (* The downward propagation phase can never reach a generic variable.
          Indeed, a generic variable is never a child of an active variable. *)
@@ -500,21 +524,38 @@ let update_ranks generation =
              it must now be [k]. *)
           assert (data.rank = k);
           (* If [v] carries some structure, ... *)
-          if not (Data.is_leaf data) then
-            (* ... traverse [v]'s children; on the way back up, compute the
-               maximum of their ranks, and use it to adjust [v]'s rank. *)
+          if not (Data.is_leaf data) then begin
+            (* Update the rank and scope of all children. *)
+            Data.iter traverse data;
+            (* On the way back up, compute the maximum of their
+               scopes, and use it to adjust [v]'s scope.
+
+               Note: we are not sure that this propagation is strictly
+               necessary. We must detect all cases where a variable
+               rank goes below its scope, but it may be enough to
+               propagate ranks "down" and never propagate scopes "up".
+               However propagating scopes in this way follows more
+               closely the intended meaning of scopes as "lexical
+               region of vadility / well-formedness": if a variable
+               [v] is only valid within scope 10, then a variable
+               representing the type (int -> v) arguably is also only
+               valid within scope 10. *)
+            adjust_scope data (
+              Data.fold (fun child accu ->
+                max (get child).scope accu
+              ) data data.scope
+            );
+            (* As an optimization we also adjust [v]'s rank, which needs
+               not be higher than its children ranks and its scope. *)
             adjust_rank data (
               Data.fold (fun child accu ->
-                max (traverse child) accu
-              ) data base_rank (* the base rank is neutral for [max] *)
-            )
+                max (get child).rank accu
+              ) data data.scope
+            );
+            end
+          end
         end
-      end;
-      (* In allowed cases, return [v]'s final rank. *)
-      data.rank
-
     in
-    let traverse v = ignore (traverse v) in
     List.iter traverse generation.by_rank.(k)
 
   done
@@ -733,7 +774,7 @@ let instantiate { generics; quantifiers; root } =
       let data = get v in
       assert (data.status = Generic);
       data.mark <- i;
-      fresh Flexible S.leaf
+      fresh None
     )
   in
 
@@ -766,10 +807,8 @@ let pp_status ppf s =
   match s with
   | Generic ->
       Printf.fprintf ppf "generic"
-  | Flexible ->
-      Printf.fprintf ppf "flexible"
-  | Rigid ->
-      Printf.fprintf ppf "rigid"
+  | Active ->
+      Printf.fprintf ppf "active"
 
 let show_variable v =
   let data = get v in

src/Generalization.mli

@@ -22,9 +22,15 @@ open Signatures
    operations that allow constructing, inspecting, and instantiating
    schemes. *)
 module Make
-  (S : sig (** @inline *) include STRUCTURE_LEAF end)
+  (UserS : sig (** @inline *) include HSTRUCTURE end)
 : sig
 
+  module S : sig
+    type 'a structure =
+      | Abstract of int
+      | User of 'a UserS.structure
+  end
+
   (** {2 Unification} *)
 
   (**This submodule defines the data attached with a unification variable. *)
@@ -39,6 +45,10 @@ module Make
        structure. *)
     val project : 'a structure -> 'a S.structure
 
+    val rank : 'a structure -> int
+
+    val scope : 'a structure -> int
+
   end
 
   (**This unifier operates with the structure specified by the submodule
@@ -64,9 +74,7 @@ module Make
      variables/types that cannot escape their scope, such as local
      abstract types or existential unpacking. *)
 
-  type status = Rigid | Flexible | Generic
-
-  type rigidity = Rigid | Flexible
+  type status = Active | Generic
 
   (* The literature defines a type scheme as a type (the ``body''), placed in
      the scope of a list of universal quantifiers. Here, the quantifiers are
@@ -128,12 +136,16 @@ module Make
      are merged, the merged variable is thereafter considered bound at the
      most ancient of these stack frames. *)
 
-  (**[fresh ~rigidity s] creates a fresh unifier variable with structure [s].
+  (**[fresh s] creates a fresh flexible unifier variable with structure [s].
      This variable is initially bound at the most recent stack frame. Invoking
      {!fresh} is permitted only if the stack is currently nonempty, that is,
      if the current balance of calls to {!enter} versus calls to {!exit} is at
      least one. *)
-  val fresh: rigidity -> variable S.structure -> variable
+  val fresh: variable S.structure -> variable
+
+  (** [fresh_rigid ()] behaves as [fresh] above but with an abstract
+      structure. *)
+  val fresh_rigid: unit -> variable
 
   (**[enter()] updates the current state by pushing a new frame onto the
      current constraint context. It is invoked when the left-hand side of a
@@ -142,7 +154,7 @@ module Make
 
   (**These exceptions are raised by {!exit}. *)
   exception Cycle of variable
-  exception VariableScopeEscape of int * int
+  exception VariableScopeEscape of { rank: int; scope: int }
 
   (**[exit ~rectypes roots] updates the current state by popping a frame off
      the current constraint context. It is invoked when the left-hand side of

src/Signatures.ml

@@ -246,6 +246,9 @@ module type GUNIFIER = sig
      error, a cyclic decoder should be used: see {!Decoder.Make}. *)
   val unify: variable -> variable -> unit
 
+  (** equality between variables up to equivalence classes. *)
+  val eq: variable -> variable -> bool
+
 end
 
 (* [UNIFIER] describes the output of [Unifier.Make]. *)
@@ -319,6 +322,8 @@ module type OUTPUT = sig
      into a decoded type. *)
   val structure: ty structure -> ty
 
+  val abstract: int -> ty
+
   (**If [v] is a type variable and [t] is a decoded type, then [mu v t] is a
      representation of the recursive type [mu v.t]. The function [mu] is used
      only by the cyclic decoder. *)

src/Solver.ml

@@ -255,8 +255,7 @@ open C
 
 (* TODO explain why we use [Structure.Option] *)
 
-module OS = Structure.Option(S)
-module G = Generalization.Make(OS)
+module G = Generalization.Make(S)
 module U = G.U
 
 (* -------------------------------------------------------------------------- *)
@@ -304,9 +303,15 @@ module UVar = struct
       (* This should never happen. *)
       Printf.ksprintf failwith "Unbound variable %d" v
 
-  let ubind (v : variable) rigidity so =
+  let ubind (v : variable) so =
     assert (not (VarTable.mem table v));
-    let uv = G.fresh rigidity (OS.map uvar so) in
+    let uv = G.fresh (G.S.User (OS.map uvar so)) in
+    VarTable.add table v uv;
+    uv
+
+  let ubind_rigid (v : variable) =
+    assert (not (VarTable.mem table v));
+    let uv = G.fresh_rigid () in
     VarTable.add table v uv;
     uv
 
@@ -338,7 +343,11 @@ module D =
   Decoder.Make (G.Data) (U) (struct
     include O
     let structure (s : O.ty U.structure) : O.ty =
-      O.structure (OS.project_nonleaf (G.Data.project s))
+      match G.Data.project s with
+      | G.S.Abstract n ->
+         O.abstract n
+      | G.S.User s ->
+         O.structure (OS.project_nonleaf s)
   end)
 
 (* -------------------------------------------------------------------------- *)
@@ -349,14 +358,22 @@ module D =
    A cyclic decoder is used even if [rectypes] is [false]. Indeed, recursive
    types can appear before the occurs check has been performed. *)
 
+let print_var v =
+  let data = G.U.get v in
+  Printf.printf "rank=%d | scope=%d | is_leaf=%b\n%!"
+    (G.Data.rank data) (G.Data.scope data)
+    (G.Data.is_leaf data)
+
 let unify range v1 v2 =
   try
     U.unify v1 v2
   with
   | U.Unify (v1, v2) ->
      let decode = D.new_cyclic_decoder() in
+     print_var v1;
+     print_var v2;
      raise (Unify (range, decode v1, decode v2))
-  | G.VariableScopeEscape (_k, _rank) ->
+  | G.VariableScopeEscape { rank=_ ; scope=_ } ->
      raise (VariableScopeEscape range)
 
 let exit range ~rectypes vs =
@@ -366,7 +383,7 @@ let exit range ~rectypes vs =
   | G.Cycle v ->
      let decode = D.new_cyclic_decoder() in
      raise (Cycle (range, decode v))
-  | G.VariableScopeEscape (_k, _rank) ->
+  | G.VariableScopeEscape { rank=_ ; scope=_ } ->
      raise (VariableScopeEscape range)
 
 (* -------------------------------------------------------------------------- *)
@@ -473,7 +490,7 @@ let rec solve : type a . range -> a co -> a on_sol =
       unify range (uvar v) (uvar w);
       On_sol (fun () -> ())
   | CExist (v, s, c) ->
-      ignore (ubind v G.Flexible s);
+      ignore (ubind v s);
       let result = solve range c in
       uunbind v;
       result
@@ -499,11 +516,11 @@ 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 urs = List.map (fun v -> ubind v G.Rigid None) rs in
+      let urs = List.map ubind_rigid 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. *)
-      let vs = List.map (fun (_, v) -> ubind v G.Flexible None) xvs in
+      let vs = List.map (fun (_, v) -> ubind v None) xvs in
       (* Solve the constraint [c1]. *)
       let (On_sol r1) = solve range c1 in
       (* Ask the generalization engine to perform an occurs check, to adjust
@@ -515,7 +532,8 @@ let rec solve : type a . range -> a co -> a on_sol =
          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));
+      assert (urs |> List.for_all (fun r ->
+                         List.exists (fun v -> U.eq v r) generalizable));
       List.iter (fun (_, v) -> uunbind v) xvs;
       (* Extend the environment [env] and compute the type schemes [xss]. *)
       let xss =

src/Structure.ml

@@ -11,7 +11,53 @@
 
 open Signatures
 
-module Option (S : GSTRUCTURE) = struct
+type 'a or_abstract =
+  | Abstract of int
+  | User of 'a
+
+module AbstractS (UserS : HSTRUCTURE) = struct
+
+  type 'a structure = 'a UserS.structure or_abstract
+
+  exception InconsistentConjunction =
+    UserS.InconsistentConjunction
+
+  let conjunction f s1 s2 =
+    match s1, s2 with
+    | Abstract n1, Abstract n2 ->
+       if Int.equal n1 n2 then s1
+       else raise InconsistentConjunction
+    | User s1, User s2 ->
+       User (UserS.conjunction f s1 s2)
+    | Abstract _n, User _s
+    | User _s, Abstract _n -> (*
+       if UserS.is_leaf s then Abstract n
+       else *)
+         raise InconsistentConjunction
+
+  let iter f s =
+    match s with
+    | Abstract _ ->
+       ()
+    | User s ->
+       UserS.iter f s
+
+  let fold f s acc =
+    match s with
+    | Abstract _ ->
+       acc
+    | User s ->
+       UserS.fold f s acc
+
+  let map f s =
+    match s with
+    | Abstract n ->
+       Abstract n
+    | User s ->
+       User (UserS.map f s)
+end
+
+module OptionS (S : GSTRUCTURE) = struct
 
   type 'a structure =
     'a S.structure option

src/Structure.mli

@@ -11,6 +11,14 @@
 
 open Signatures
 
+type 'a or_abstract =
+  | Abstract of int
+  | User of 'a
+
+module AbstractS (S : sig (** @inline *) include HSTRUCTURE end) : sig
+  include GSTRUCTURE with type 'a structure = 'a S.structure or_abstract
+end
+
 (**This functor transforms a type ['a structure], equipped with [map],
    [iter] and [conjunction] operations, into the type ['a structure option],
    equipped with the same operations. The type ['a structure option] is
@@ -18,10 +26,11 @@ open Signatures
    indeed, the optional structure [None] indicates the absence of a
    constraint, while the optional structure [Some term] indicates the
    presence of an equality constraint. *)
-module Option (S : sig (** @inline *) include GSTRUCTURE end) : sig
+module OptionS (S : sig (** @inline *) include GSTRUCTURE end) : sig
 
   (** @inline *)
-  include STRUCTURE_LEAF with type 'a structure = 'a S.structure option
+  include STRUCTURE_LEAF
+          with type 'a structure = 'a S.structure option
 
   (**[project_nonleaf (Some s)] is [s], while [project_nonleaf None] is
      undefined. In other words, if [os] is a non-leaf optional structure,