Add letrn combinator and rewrite the other let-combinators accordingly.

client/FPrinter.ml

@@ -52,9 +52,9 @@ let rec translate_term env (t : F.nominal_term) : P.term =
   | F.Hole (_, ty, ts) ->
       P.Hole (Some (translate_type env ty), List.map (self env) ts)
   | F.Annot (_, t, ty) ->
-      P.Annot (self env t, ([], translate_type env ty))
+      P.Annot (self env t, (P.Flexible, [], translate_type env ty))
   | F.Abs (_, x, ty, t) ->
-      let annot = P.PAnnot (P.PVar x, ([], translate_type env ty)) in
+      let annot = P.PAnnot (P.PVar x, (P.Flexible, [], translate_type env ty)) in
       P.Abs (annot, self env t)
   | F.App (_, t1, t2) ->
       P.App (self env t1, self env t2)
@@ -96,7 +96,7 @@ and translate_pattern env pat =
   | F.PWildcard _ ->
       P.PWildcard
   | F.PAnnot (_, p, ty) ->
-      P.PAnnot (self env p, ([], translate_type env ty))
+      P.PAnnot (self env p, (P.Flexible, [], translate_type env ty))
   | F.PTuple (_, ps) ->
       P.PTuple (List.map (self env) ps)
   | F.PVariant (_, lbl, (tid, tys), p) ->

client/Infer.ml

@@ -50,9 +50,41 @@ end
 (* Instantiate the solver. *)
 
 module X = struct
-  type tevar = string
-  let compare = String.compare
-  let to_string s = s
+  (* The module X (following the naming convention of Solver.Make)
+     provides a type of variables that will be assigned polymorphic
+     schemes by the solver.
+
+     In a toy ML language, the syntact constructs that introduce
+     polymorphic schemes always correspond to binding constructs for
+     term variables: (let x = t in u) in particular, or (fun x -> t)
+     which can be considered to give a "trivial" (non-polymorphic)
+     scheme to x.
+
+     In our richer language, we also compute polymorphic schemes for
+     type annotations containing rigid variables:
+
+       (t : for 'a 'b. 'a * 'b -> 'a)
+
+     For this construct there is no term variable associated to the
+     scheme, instead we create a "symbolic" variable (a fresh integer)
+     to pass to the solver.
+   *)
+  type tevar =
+    | Var of ML.tevar
+    | Sym of int
+
+  let fresh : unit -> tevar =
+    let gensym = Inferno.Utils.gensym() in
+    fun () -> Sym (gensym ())
+
+  let compare v1 v2 = Stdlib.compare v1 v2
+
+  let to_string v =
+    match v with
+    | Var v ->
+       v
+    | Sym n ->
+       string_of_int n
 end
 
 module Solver = Inferno.Solver.Make(X)(S)(O)
@@ -203,7 +235,7 @@ let rec map_co (f : 'a -> 'b co) : 'a list -> 'b list co
       and+ ys = map_co f xs
       in y :: ys
 
-let rec convert_deep (env : ML.datatype_env) (params : (string * variable) list) (ty : ML.typ) : deep_ty =
+let rec convert_deep (env : ML.datatype_env) (params : (ML.tyvar * variable) list) (ty : ML.typ) : deep_ty =
   let conv ty = convert_deep env params ty in
   match ty with
   | ML.TyVar (_, tx) ->
@@ -223,25 +255,7 @@ let convert env params ty =
   let deep_ty = convert_deep env params ty in
   build deep_ty
 
-exception VariableConflict of string
-
-let convert_annot env ((flex_vars, ty) : ML.type_annotation)
-  : (variable * F.nominal_type co, 'r) binder
-  = fun k ->
-    let@ params, witnesses =
-      flex_vars |> mapM_both (fun alpha k ->
-        let@ v = exist in
-        k (
-          (alpha, v),
-          let+ ty' = witness v in (alpha, ty'))
-      )
-    in
-    let@ v = convert env params ty in
-    k (v,
-       let+ ws = witnesses in
-       let translate_var alpha = List.assoc alpha ws in
-       ML2F.translate_type translate_var ty
-      )
+exception VariableConflict of ML.tevar
 
 (* -------------------------------------------------------------------------- *)
 
@@ -270,7 +284,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
     | ML.Var (pos, x) ->
 
         (* [w] must be an instance of the type scheme associated with [x]. *)
-        let+ tys = instance x w in
+        let+ tys = instance (X.Var x) w in
         (* The translation makes the type application explicit. *)
         F.ftyapp (F.Var (pos, x)) tys
 
@@ -286,7 +300,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
         let+ () = w --- arrow v1 v2
         (* Under the assumption that [x] has type [domain], the term [u] must
            have type [codomain]. *)
-        and+ u' = def x v1 (hastype u v2)
+        and+ u' = def (X.Var x) v1 (hastype u v2)
         and+ ty1 = witness v1
         in
         (* Once these constraints are solved, we obtain the translated function
@@ -307,7 +321,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
     | ML.Let (pos, x, t, u) ->
 
         (* Construct a ``let'' constraint. *)
-        let+ ((b, _), a, t', u') = let1 x (hastype t) (hastype u w) in
+        let+ (a, (b, _), t', u') = let1 (X.Var x) (hastype t) (hastype u w) in
         (* [a] are the type variables that we must bind (via Lambda abstractions)
            while type-checking [t]. [(b, _)] is the type scheme that [x] must
            receive while type-checking [u]. Its quantifiers [b] are guaranteed to
@@ -320,11 +334,43 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
         u'))
 
     | ML.Annot (pos, t, annot) ->
-      let@ v, annot' = convert_annot typedecl_env annot in
-      let+ () = v -- w
-      and+ t' = hastype t v
-      and+ annot' = annot' in
-      F.Annot (pos, t', annot')
+
+       let convert_annot typedecl_env params w t ty =
+         let@ v = convert typedecl_env params ty in
+         let+ () = v -- w
+         and+ t' = hastype t v
+         and+ ty' = witness v
+         in F.Annot (pos, t', ty')
+       in
+
+       begin match annot with
+       | (_, [], ty) ->
+          convert_annot typedecl_env [] w t ty
+       | (ML.Flexible, vs, ty) ->
+          let@ params =
+            vs |> mapM_now (fun alpha k -> let@ v = exist in k (alpha, v)) in
+          convert_annot typedecl_env params w t ty
+       | (ML.Rigid, vs, ty) ->
+          (* See "The Essence of ML type inference", long version, exercise 1.10.8 page 112:
+               <<(t : forall 'a 'b. ty) : 'w>>
+             is elaborated into a rigid constraint
+               let x: forall ('a 'b) exists 'z [<<(t : ty) : 'z>>]. 'z in (x <= 'w)
+
+             After constraint solving, the witness we generate looks like
+               (Lambda 'a 'b. (t : ty)) [ty1] [ty2]
+             where ty1, ty2 are the witnesses of the instance
+             constraint between the polymorphic scheme of x and the
+             result type 'w. This enforces that 'a, 'b are used polymorphically
+             by t, but they can still be instantiated in the rest of the term.
+           *)
+          let x = X.fresh () in
+          let+ (alphas, t', tys) =
+            letr1 vs x
+              (fun tyvs z -> convert_annot typedecl_env tyvs z t ty)
+              (instance x w)
+          in
+          F.ftyapp (F.ftyabs alphas t') tys
+       end
 
     | ML.Tuple (pos, ts) ->
         let on_term (t:ML.term) : ('b * 'c co, 'r) binder =
@@ -343,7 +389,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
         let on_var (x:ML.tevar) : ('a, 'r) binder =
           fun (k : 'b -> 'r co) : 'r co ->
             let@ v = exist in
-            def x v (k v)
+            def (X.Var x) v (k v)
         in
 
         let@ vs = mapM_now on_var xs in
@@ -440,7 +486,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
              as the whole match statement *)
           hastype u v_return
       | (x, v1) :: pat_env ->
-          def x v1 @@ bind_pattern_vars pat_env u
+          def (X.Var x) v1 @@ bind_pattern_vars pat_env u
     in
 
     let on_branch ((pat,u) : ML.branch)
@@ -471,15 +517,25 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
     | ML.PWildcard pos ->
         k ([], pure (F.PWildcard pos))
 
-    | ML.PAnnot (pos, pat, annot) ->
-      let@ v, annot' = convert_annot typedecl_env annot in
-      let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
-      let+ () = v -- w
-      and+ res = k (pat_env,
-                    let+ pat = pat
-                    and+ annot' = annot'
-                    in F.PAnnot(pos, pat, annot'))
-      in res
+    | ML.PAnnot (pos, pat, (rigidity, vars, ty)) ->
+        begin match rigidity with
+        | ML.Rigid ->
+           failwith "Rigid variables are not supported in pattern annotation"
+        | ML.Flexible ->
+           let@ params =
+             vars |> mapM_now (fun alpha k ->
+                         let@ v = exist in k(alpha,v)
+                       )
+           in
+           let@ v = convert typedecl_env params ty in
+           let@ (pat_env, pat) = hastype_pat typedecl_env pat v in
+           let+ () = v -- w
+           and+ res = k (pat_env,
+                         let+ pat = pat
+                         and+ ty' = witness v
+                         in F.PAnnot(pos, pat, ty'))
+           in res
+        end
 
     | ML.PTuple (pos, pats) ->
 
@@ -538,7 +594,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
    type; it creates its own using [exist]. And it runs the solver. *)
 
 type nonrec range = range
-exception Unbound = Solver.Unbound
+exception Unbound of range * ML.tevar
 exception Unify = Solver.Unify
 exception Cycle = Solver.Cycle
 
@@ -547,8 +603,16 @@ let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
   (* [vs] are the binders that we must introduce *)
   F.ftyabs vs t
 
+let get_tevar x =
+  match x with
+  | X.Sym _ -> assert false
+  | X.Var x -> x
+
 let translate ~rectypes env t =
-  Solver.solve ~rectypes (hastype env t)
+  try
+    Solver.solve ~rectypes (hastype env t)
+  with Solver.Unbound (range, x) ->
+    raise (Unbound (range, get_tevar x))
 
 let hastype_with_hook ~(hook : unit -> 'a) (env : ML.datatype_env) (t : ML.term)
 : ('a * F.nominal_term) co
@@ -558,4 +622,7 @@ let hastype_with_hook ~(hook : unit -> 'a) (env : ML.datatype_env) (t : ML.term)
   a, u
 
 let translate_with_hook ~hook ~rectypes env t =
-  Solver.solve ~rectypes (hastype_with_hook ~hook env t)
+  try
+    Solver.solve ~rectypes (hastype_with_hook ~hook env t)
+  with Solver.Unbound (range, x) ->
+    raise (Unbound (range, get_tevar x))

client/Infer.mli

@@ -1,5 +1,5 @@
 type range = Lexing.position * Lexing.position
-exception Unbound of range * string
+exception Unbound of range * ML.tevar
 exception Unify of range * F.nominal_type * F.nominal_type
 exception Cycle of range * F.nominal_type
 

client/ML.ml

@@ -22,7 +22,11 @@ type typ =
   | TyConstr of range * Datatype.TyConstrId.t * typ list
  [@@deriving compare]
 
-type type_annotation = tyvar list * typ [@@deriving compare]
+type rigidity = Flexible | Rigid
+
+let compare_rigidity r1 r2 = compare r1 r2
+
+type type_annotation = rigidity * tyvar list * typ [@@deriving compare]
   (* some <flexible vars> . <ty> *)
 
 type term =

client/MLLexer.mll

@@ -16,6 +16,7 @@
       "of", OF;
       "some", SOME;
       "#use", USE;
+      "for", FOR;
     ]
 
   let _ =

client/MLParser.mly

@@ -32,6 +32,7 @@
 %token COLON ":"
 %token PERIOD "."
 %token SOME
+%token FOR
 
 %token USE "#use"
 %token <string> FILENAME
@@ -165,7 +166,9 @@ let type_atom :=
 
 let type_annotation :=
   | SOME ; xs = list(tyvar) ; "." ; ty = typ ;
-                                          { (xs, ty) }
+                                          { (Flexible, xs, ty) }
+  | FOR ; xs = list(tyvar) ; "." ; ty = typ ;
+                                          { (Rigid, xs, ty) }
 
 let tyconstr_decl :=
   | l = UIDENT ; arg_type = option (OF ; ~ = typ ; <>) ;

client/MLPrinter.ml

@@ -17,8 +17,14 @@ let rec translate_type (ty : ML.typ) : P.typ =
 let print_type (ty : ML.typ) =
   Printer.print_type (translate_type ty)
 
-let translate_annot (vars, ty) =
-  (vars, translate_type ty)
+let translate_rigidity = function
+  | ML.Flexible ->
+     P.Flexible
+  | ML.Rigid ->
+     P.Rigid
+
+let translate_annot (rigidity, vars, ty) =
+  (translate_rigidity rigidity, vars, translate_type ty)
 
 let rec translate_term (t : ML.term) : P.term =
   let self = translate_term in

client/P.ml

@@ -12,7 +12,9 @@ type typ =
 
 and datatype = Datatype.tyconstr_id * typ list
 
-type type_annotation = tyvar list * typ
+type rigidity = Flexible | Rigid
+
+type type_annotation = rigidity * tyvar list * typ
   (* some <flexible vars> . <ty> *)
 
 type tevar = string

client/Printer.ml

@@ -110,11 +110,21 @@ let print_let_in lhs rhs body =
   ^^ string "in"
   ^^ prefix 0 1 empty body
 
-let print_annot print_elem (tyvars, typ) =
+let print_annot print_elem (rigidity, tyvars, typ) =
+  let rigidity_kwd =
+    string @@ match rigidity with
+             | Flexible ->
+                "some"
+             | Rigid ->
+                "for"
+  in
   surround 2 0 lparen (
     print_elem ^^ space ^^ string ":"
-    ^//^ string "some" ^^ space ^^ separate_map space print_tyvar tyvars
-    ^^ dot ^//^ print_type typ
+    ^^ (if tyvars = [] then empty
+        else prefix 2 1 empty
+               (rigidity_kwd ^^ space ^^
+                separate_map space print_tyvar tyvars ^^ dot))
+    ^//^ print_type typ
   ) rparen
 
 let rec print_term t =

client/test/RandomML.ml

@@ -57,7 +57,7 @@ let let_pair self k n =
 
 let annot self k n =
   let+ t = self (k, n - 1) in
-  ML.Annot (pos, t, (["'a"], ML.TyVar (pos, "'a")))
+  ML.Annot (pos, t, (ML.Flexible, ["'a"], ML.TyVar (pos, "'a")))
 
 let term = fix (fun self (k, n) ->
   if n = 0 then begin

client/test/TestML.ml

@@ -145,7 +145,7 @@ let match_some_annotated = ML.(
       ( PAnnot (dummy_pos,
                 PVariant (dummy_pos, Datatype.Label "Some",
                           Some (PWildcard dummy_pos)),
-                (["'a"], TyConstr (dummy_pos, Datatype.Type "option",
+                (Flexible, ["'a"], TyConstr (dummy_pos, Datatype.Type "option",
                                    [ TyVar (dummy_pos, "'a") ]))),
         none );
     ])
@@ -200,12 +200,12 @@ let _list_annotated =
       Datatype.Label "Cons",
       Some (Tuple (dummy_pos, [
                   Annot (dummy_pos, id,
-                         (["'a"], TyArrow (dummy_pos,
+                         (Flexible, ["'a"], TyArrow (dummy_pos,
                                            TyVar (dummy_pos, "'a"),
                                            TyVar (dummy_pos, "'a"))));
                   nil ]))
     ),
-    (["'a"; "'b"], TyConstr (dummy_pos,
+    (Flexible, ["'a"; "'b"], TyConstr (dummy_pos,
                              Datatype.Type "list",
                              [TyArrow (dummy_pos,
                                        TyVar (dummy_pos, "'a"),
@@ -461,6 +461,22 @@ let test_regression2 () =
     "let f = fun x -> let g = fun y -> (x, y) in g in fun x -> fun y -> f"
     regression2
 
+let a = ML.TyVar (dummy_pos, "'a")
+let b = ML.TyVar (dummy_pos, "'b")
+
+let id_annot annot =
+  ML.(Annot (dummy_pos, Abs(dummy_pos, "x", Var (dummy_pos, "x")), annot))
+
+let test_id_rigid () =
+  test_ok
+    "(fun x -> x : for 'a. 'a -> 'a)"
+    (id_annot (ML.Rigid, ["'a"], ML.TyArrow (dummy_pos, a, a)))
+
+let test_id_flexible () =
+  test_ok
+    "(fun x -> x : some 'a 'b. 'a -> 'b)"
+    (id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (dummy_pos, a, b)))
+
 let test_suite =
   let open Alcotest in
   test_suite ::
@@ -499,6 +515,12 @@ let test_suite =
         test_case "match some" `Quick test_match_some;
         test_case "match some annotated" `Quick test_match_some_annotated;
       ]
+    ) ; (
+      "rigid",
+      [
+        test_case "id rigid" `Quick test_id_rigid;
+        test_case "id flexible" `Quick test_id_flexible;
+      ]
     )
   ]
 

client/test/suite.t/id-annot-flexible.midml

@@ -0,0 +1,2 @@
+let _ =
+  (fun x -> x : some 'a 'b. 'a -> 'b)

client/test/suite.t/id-annot-flexible2.midml

@@ -0,0 +1,2 @@
+let _ =
+  (fun x -> () : some 'a. 'a -> 'a)

client/test/suite.t/id-rigid-wrong.midml

@@ -0,0 +1,2 @@
+let _ =
+  (fun x -> x : for 'a 'b. 'a -> 'b)

client/test/suite.t/id-rigid.midml

@@ -0,0 +1,2 @@
+let _ =
+  (fun x -> x : for 'a. 'a -> 'a)

client/test/suite.t/id-rigid2.midml

@@ -0,0 +1,2 @@
+let _ =
+  (fun x -> x : for 'a. 'a -> 'a) ()

client/test/suite.t/rigid-level-escape-wrong.midml

@@ -0,0 +1,2 @@
+let f =
+  fun x -> (x : for 'a. 'a)

client/test/suite.t/run.t

@@ -8,7 +8,7 @@ Basics
   Type inference and translation to System F...
   Formatting the System F term...
   Pretty-printing the System F term...
-  FUN a0 -> fun (x : some . a0) -> x
+  FUN a0 -> fun (x : a0) -> x
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -20,7 +20,7 @@ Basics
   Type inference and translation to System F...
   Formatting the System F term...
   Pretty-printing the System F term...
-  FUN a0 -> (fun (x : some . a0 -> a0) -> x) (fun (x : some . a0) -> x)
+  FUN a0 -> (fun (x : a0 -> a0) -> x) (fun (x : a0) -> x)
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -62,7 +62,7 @@ Option type
   Type inference and translation to System F...
   Formatting the System F term...
   Pretty-printing the System F term...
-  FUN a0 -> Some<option (a0 -> a0)> (fun (x : some . a0) -> x)
+  FUN a0 -> Some<option (a0 -> a0)> (fun (x : a0) -> x)
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -78,10 +78,7 @@ Option type
   Pretty-printing the System F term...
   FUN a0 ->
     FUN a1 ->
-      Some<option {a1 -> a1*a0 -> a0}> (
-        fun (x : some . a1) -> x,
-        fun (x : some . a0) -> x
-      )
+      Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -112,10 +109,7 @@ List type
   Formatting the System F term...
   Pretty-printing the System F term...
   FUN a0 ->
-    Cons<list (a0 -> a0)> (
-      fun (x : some . a0) -> x,
-      Nil<list (a0 -> a0)> ()
-    )
+    Cons<list (a0 -> a0)> (fun (x : a0) -> x, Nil<list (a0 -> a0)> ())
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
 
@@ -137,11 +131,8 @@ List type
   Pretty-printing the System F term...
   FUN a0 ->
     Cons<list (a0 -> a0)> (
-      fun (x : some . a0) -> x,
-      Cons<list (a0 -> a0)> (
-        fun (x : some . a0) -> x,
-        Nil<list (a0 -> a0)> ()
-      )
+      fun (x : a0) -> x,
+      Cons<list (a0 -> a0)> (fun (x : a0) -> x, Nil<list (a0 -> a0)> ())
     )
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
@@ -172,7 +163,7 @@ Pattern-matching
   Formatting the System F term...
   Pretty-printing the System F term...
   FUN a0 ->
-    match<a0 -> a0> (fun (x : some . a0) -> x, ()) with
+    match<a0 -> a0> (fun (x : a0) -> x, ()) with
     | (f, ()) -> f
     end
   Converting the System F term to de Bruijn style...
@@ -193,10 +184,105 @@ Pattern-matching
   Pretty-printing the System F term...
   FUN a0 ->
     FUN a1 ->
-      match<option a0> Some<option (a1 -> a1)> (fun (x : some . a1) -> x) with
+      match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
       | None<option (a1 -> a1)> () -> None<option a0> ()
-      | (Some<option (a1 -> a1)> _ : some . option (a1 -> a1)) ->
-        None<option a0> ()
+      | (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
       end
   Converting the System F term to de Bruijn style...
   Type-checking the System F term...
+
+
+
+# Rigid, flexible variables.
+
+Flexible variables can be unified with some structure
+or with each other.
+
+  $ cat id-annot-flexible.midml
+  let _ =
+    (fun x -> x : some 'a 'b. 'a -> 'b)
+
+  $ ../TestMidML.exe id-annot-flexible.midml
+  Type inference and translation to System F...
+  Formatting the System F term...
+  Pretty-printing the System F term...
+  FUN a0 -> (fun (x : a0) -> x : a0 -> a0)
+  Converting the System F term to de Bruijn style...
+  Type-checking the System F term...
+
+  $ cat id-annot-flexible2.midml
+  let _ =
+    (fun x -> () : some 'a. 'a -> 'a)
+
+  $ ../TestMidML.exe id-annot-flexible2.midml
+  Type inference and translation to System F...
+  Formatting the System F term...
+  Pretty-printing the System F term...
+  (fun (x : {}) -> () : {} -> {})
+  Converting the System F term to de Bruijn style...
+  Type-checking the System F term...
+
+Rigid variables enforce polymorphism.
+The identity function below is correct.
+
+  $ cat id-rigid.midml
+  let _ =
+    (fun x -> x : for 'a. 'a -> 'a)
+
+  $ ../TestMidML.exe id-rigid.midml
+  Type inference and translation to System F...
+  Formatting the System F term...
+  Pretty-printing the System F term...
+  FUN a0 -> (FUN a1 -> (fun (x : a1) -> x : a1 -> a1)) [a0]
+  Converting the System F term to de Bruijn style...
+  Type-checking the System F term...
+
+The elaborated term is a bit strange, there is one variable a0
+corresponding to the outer polymorphism, and a1 for the rigid variable
+'a. It is easier to look at the elaboration of the simpler example below:
+
+  $ cat id-rigid2.midml
+  let _ =
+    (fun x -> x : for 'a. 'a -> 'a) ()
+
+  $ ../TestMidML.exe id-rigid2.midml
+  Type inference and translation to System F...
+  Formatting the System F term...
+  Pretty-printing the System F term...
+  (FUN a0 -> (fun (x : a0) -> x : a0 -> a0)) [{}] ()
+  Converting the System F term to de Bruijn style...
+  Type-checking the System F term...
+
+Here we see that the variable 'a is rigid inside the annotated term
+(translated to a System F type abstraction), but can be used at any
+instantiation type from the outside -- here the unit type {}.
+
+The example below is incorrect, it tries to unify two distinct rigid
+variables.
+
+  $ cat id-rigid-wrong.midml
+  let _ =
+    (fun x -> x : for 'a 'b. 'a -> 'b)
+
+  $ ../TestMidML.exe id-rigid-wrong.midml
+  Type inference and translation to System F...
+
+The example below is incorrect, it tries to unify a rigid variable
+with some structure.
+
+  $ cat unit-rigid-wrong.midml
+  let _ =
+    (() : for 'a. 'a)
+
+  $ ../TestMidML.exe unit-rigid-wrong.midml
+  Type inference and translation to System F...
+
+The example below is incorrect, a rigid variable tries to escape
+its binding scope.
+
+  $ cat rigid-level-escape-wrong.midml
+  let f =
+    fun x -> (x : for 'a. 'a)
+
+  $ ../TestMidML.exe rigid-level-escape-wrong.midml
+  Type inference and translation to System F...

client/test/suite.t/unit-rigid-wrong.midml

@@ -0,0 +1,2 @@
+let _ =
+  (() : for 'a. 'a)

src/Generalization.ml

@@ -38,7 +38,7 @@ let fresh_id : unit -> int =
 (* Ranks can be thought of as de Bruijn levels. Indeed, whenever the left-hand
    side of a [CLet] constraint is entered, the current rank is incremented by
    one. Thus, the rank of a variable indicates where (that is, at which [CLet]
-   construct) this variable is (existentially) bound. *)
+   construct) this variable is bound. *)
 
 (* [base_rank] is the smallest rank. We set [base_rank = 0], so every rank is
    nonnegative. We take advantage of this property and use ranks as indices
@@ -50,24 +50,28 @@ type rank =
 let base_rank =
   0
 
+
 (* -------------------------------------------------------------------------- *)
 
-(* We want to be able to mark an equivalence class as either "ordinary" or
-   "generic". The unifier works with ordinary variables only; it never sees a
+(* 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
    of schemes: when we create a scheme, we mark the variables that can be
    generalized as generic; when we instantiate a scheme, we replace every
-   generic variable with a fresh ordinary variables. *)
+   generic variable with a fresh active variables. *)
 
 (* The generic variables always form a prefix of the structure: the children
-   of a generic variable can be generic or ordinary; the children of an
-   ordinary variable must be ordinary. *)
+   of a generic variable can be generic or active; the children of an
+   active variable must be active. *)
 
-(* An ordinary variable is intended to become generic some day. A generic
-   variable never becomes ordinary again. *)
+(* An active variable is intended to become generic some day. A generic
+   variable never becomes active again. *)
 
-type generic =
-  bool (* [true] is generic; [false] is ordinary *)
+type status = Rigid | Flexible | Generic
 
 (* -------------------------------------------------------------------------- *)
 
@@ -76,7 +80,7 @@ type generic =
    locally, in various places, to store short-lived information. In several
    places, it allows us to save the need for a hash table. *)
 
-(* As long as a class is ordinary, the content of the [mark] field must be a
+(* As long as a class is active, the content of the [mark] field must be a
    value that has been generated in the past by [fresh_mark()]. This ensures
    that we can generate a new mark using [fresh_mark()] and that this new mark
    is distinct from the value of every [mark] field. This is exploited in the
@@ -87,7 +91,7 @@ type generic =
    used by [instantiate] to (temporarily) store an index into an array. *)
 
 (* This convention relies on the fact that a generic variable never becomes
-   ordinary again. *)
+   active again. *)
 
 type mark =
   int
@@ -113,7 +117,7 @@ type 'a data = {
   id: int;
   mutable structure: 'a S.structure;
   mutable rank: rank;
-  mutable generic: generic;
+  mutable status: status;
   mutable mark: mark;
 }
 
@@ -136,12 +140,10 @@ module Data = struct
   let dummy : mark =
     fresh_mark()
 
-  let make structure rank =
+  let make structure rank status =
     let id = fresh_id() in
-    (* A fresh variable is ordinary, not generic. *)
-    let generic = false in
     let mark = dummy in
-    { id; structure; rank; generic; mark }
+    { id; structure; rank; status; mark }
 
   let map f data =
     { data with structure = S.map f data.structure }
@@ -176,12 +178,32 @@ module Data = struct
     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
-    (* The unifier never acts on generic variables. *)
-    assert (not data1.generic && not data2.generic);
-    let generic = false in
+    let fail () = raise InconsistentConjunction in
+    (* If either variables is rigid, the conjunction is also rigid. *)
+    let status = match data1.status, data2.status with
+      | Generic, _ | _, Generic ->
+         (* The unifier never acts on generic variables. *)
+         assert false
+      | Flexible, Flexible ->
+         Flexible
+      (* One cannot unify two rigid variables, *)
+      | Rigid, Rigid ->
+         fail ()
+      (* ... or lower the rank of a rigid variable, *)
+      | Rigid, Flexible ->
+         if (rank < data1.rank) then fail ();
+         (* ... or give it a non-leaf structure. *)
+         if not (S.is_leaf structure) then fail ();
+         Rigid
+      | Flexible, Rigid ->
+         if (rank < data2.rank) then fail ();
+         (* ... or give it a non-leaf structure. *)
+         if not (S.is_leaf structure) then fail ();
+         Rigid
+    in
     (* There is no need to preserve marks during unification. *)
     let mark = dummy in
-    { id; structure; rank; generic; mark }
+    { id; structure; rank; status; mark }
 
   let is_leaf data =
     S.is_leaf data.structure
@@ -278,9 +300,11 @@ let register { pool; _ } v r =
 (* When a fresh unification variable is created, it receives the current rank,
    and it is immediately registered at this rank. *)
 
-let fresh state structure =
+let fresh state rigidity structure =
   let r = state.young in
-  let v = U.fresh (Data.make structure r) in
+  if rigidity = Rigid then
+    assert (S.is_leaf structure);
+  let v = U.fresh (Data.make structure r rigidity) in
   register state v r;
   v
 
@@ -365,7 +389,7 @@ let discover_young_generation state =
     let data = get v in
     Hashtbl.replace table data.id ();
     let r = data.rank in
-    assert (not data.generic);
+    assert (data.status <> Generic);
     assert (base_rank <= r && r <= state.young);
     by_rank.(r) <- v :: by_rank.(r)
   );
@@ -434,8 +458,8 @@ let update_ranks state generation =
     let rec traverse v : rank =
       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 ordinary variable. *)
-      assert (not data.generic);
+         Indeed, a generic variable is never a child of an active variable. *)
+      assert (data.status <> Generic);
       (* If [v] was visited before, then its rank must be below [k], as we
          adjust ranks on the way down already. *)
       if data.mark = visited then
@@ -513,7 +537,7 @@ let generalize state generation : variable list =
       else begin
         assert (r = state.young);
         (* Make this variable generic, ... *)
-        data.generic <- true;
+        data.status <- Generic;
         (* ... and keep it in the result list, if it has no structure. *)
         Data.is_leaf data
       end
@@ -524,7 +548,7 @@ let generalize state generation : variable list =
 
 (* We are in charge of constructing and instantiating schemes, that is, graph
    fragments that contain generic (universally quantified, to-be-copied)
-   variables and can have outgoing edges towards ordinary (not-to-be-copied)
+   variables and can have outgoing edges towards active (not-to-be-copied)
    variables. *)
 
 (* Schemes are built when we exit the left-hand side of a [CLet] constraint,
@@ -537,11 +561,11 @@ let generalize state generation : variable list =
 
 type scheme = {
 
-  (* A root variable [root]. This variable may be generic or ordinary. *)
+  (* A root variable [root]. This variable may be generic or active. *)
   root: variable;
 
   (* A list of all of the variables that form the generic fragment of this
-     scheme. These variables are replaced with fresh ordinary variables when
+     scheme. These variables are replaced with fresh active variables when
      the scheme is instantiated. The order of the variables in this list does
      not matter. Every variable in this list is generic. The rank of these
      variables is irrelevant, but it is the value of [state.young] at the
@@ -604,7 +628,7 @@ let schemify (root : variable) : scheme =
 
   let rec traverse v =
     let data = get v in
-    if data.generic && data.mark <> visited then begin
+    if data.status = Generic && data.mark <> visited then begin
       (* This variable is generic and has not yet been visited. Mark it as
          visited. Insert it into the accumulator. Traverse its descendants.
          The variable must be marked before the recursive call, so as to
@@ -683,15 +707,15 @@ let exit ~rectypes state roots =
 
 let instantiate state { generics; quantifiers; root } =
 
-  (* Create a copy [v'] of every generic variable [v]. At this point, the
+  (* Create a flexible copy [v'] of every generic variable [v]. At this point, the
      variable [v'] carries no structure. Record the correspondence between
      [v] and [v'] in the mapping. *)
   let mapping : variable array =
     generics |> Array.mapi (fun i v ->
       let data = get v in
-      assert (data.generic);
+      assert (data.status = Generic);
       data.mark <- i;
-      fresh state S.leaf
+      fresh state Flexible S.leaf
     )
   in
 
@@ -700,7 +724,7 @@ let instantiate state { generics; quantifiers; root } =
      [v] is generic, then it must be a member of the set [generics].) *)
   let copy (v : variable) : variable =
     let data = get v in
-    if data.generic then
+    if data.status = Generic then
       let i = data.mark in
       mapping.(i)
     else
@@ -720,10 +744,19 @@ let instantiate state { generics; quantifiers; root } =
 
 (* Debugging utilities. *)
 
+let pp_status ppf s =
+  match s with
+  | Generic ->
+      Printf.fprintf ppf "generic"
+  | Flexible ->
+      Printf.fprintf ppf "flexible"
+  | Rigid ->
+      Printf.fprintf ppf "rigid"
+
 let show_variable v =
   let data = get v in
-  Printf.printf "id = %d, rank = %d, generic = %b\n"
-    data.id data.rank data.generic
+  Printf.printf "id = %d, rank = %d, status = %a\n"
+    data.id data.rank pp_status data.status
 
 let show_pool state k =
   Printf.printf "Pool %d:\n" k;

src/Generalization.mli

@@ -31,6 +31,20 @@ module Make
   type variable =
     U.variable
 
+  (* Existentially-bound variables can "move" in the constraint: some
+     constraint-solving steps have the effect of hoisting their
+     existential quantifier out, to scope over a larger part of the
+     constraint -- this corresponds to lowering the rank of the
+     variable. They can also be unified with some structure. *)
+
+  (* We also support "rigidly-bound" variables that are not allowed to
+     move to a different binding place, or to unify with anything else
+     than themselves. This models language features with abstract
+     variables/types that cannot escape their scope, such as local
+     abstract types or existential unpacking. *)
+
+  type status = Rigid | Flexible | 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
      just variables (which definitely carry no structure), while the body is
@@ -77,12 +91,14 @@ module Make
 
   val init : unit -> state
 
-  (* [fresh state s] creates a fresh unifier variable with structure
+  (* [fresh state rigidity s] creates a fresh unifier variable with structure
      [s]. This variable is automatically regarded as bound at the most recent
-     [CLet] construct. It is permitted to invoke [fresh] only there is at
-     least one enclosing [CLet] construct, that is, if the current
+     [CLet] construct, flexibly or rigidly bound according to [rigidity].
+
+     It is permitted to invoke [fresh] only there is at least one
+     enclosing [CLet] construct, that is, if the current
      [enter]/[exit] balance is at least one. *)
-  val fresh: state -> variable S.structure -> variable
+  val fresh: state -> status -> variable S.structure -> variable
 
   (* A variable can be turned into a trivial scheme, with no quantifiers and
      no generic part: in other words, a monomorphic type scheme. Non-trivial

src/Solver.ml

@@ -103,17 +103,20 @@ type _ co =
        the trivial (monomorphic) type scheme [v] in the constraint [c]. *)
 
 | CLet :
-    (tevar * variable) list * 'a co * 'b co ->
+    variable list * (tevar * variable) list * 'a co * 'b co ->
     (O.tyvar list * (tevar * scheme) list * 'a * 'b) co
-    (**[CLet (List.combine xs vs) c1 c2] first constructs a list [cs] of
-       constraint abstractions by abstracting the type variables [vs] in the
-       constraint [c1]. Then, it binds the term variables [xs] to the constraint
-       abstractions [cs] in the constraint [c2].
+    (**[CLet rs (List.combine xs vs) c1 c2] first constructs a list
+       [cs] of constraint abstractions by abstracting the type
+       variables [vs] in the constraint [c1], under the scope of the
+       rigid variables [rs]. Then, it binds the term variables [xs] to
+       the constraint abstractions [cs] in the constraint [c2].
+
        It produces a tuple of 4 results, namely:
        - a list [ws] of (decoded) type variables that may appear in [a1], hence
          should be universally bound by the client in [a1]. In a typical
          scenario, [a1] is a System F term, and the client must build a type
-         abstraction [\Lambda vs.a1].
+         abstraction [\Lambda vs.a1]. Note that [ws] must contain at least
+         the (decodings of) the rigid variables [rs].
        - an association list that maps each term variable in [xs] to the type
          scheme that has been assigned to it while solving [c2].
        - the value [a1] produced by solving the constraint [c1].
@@ -173,8 +176,9 @@ module Printer = struct
         annot (x, v) ^^
         string " in" ^/^
         self c
-    | CLet (xvs, c1, c2) ->
-        string "let " ^^
+    | CLet (rs, xvs, c1, c2) ->
+        string "let" ^^
+        (if rs = [] then empty else brackets (separate_map space var rs)) ^^
         separate_map (string " and ") annot xvs ^^
         string " where" ^^ group (nest 2 (break 1 ^^
         next c1 ^^
@@ -289,12 +293,11 @@ end) = struct
     | Some uv ->
         uv
 
-  let ubind (v : variable) so =
+  let ubind (v : variable) rigidity so =
     assert (not (VarTable.mem table v));
-    let uv = G.fresh X.state (OS.map uvar so) in
+    let uv = G.fresh X.state rigidity (OS.map uvar so) in
     VarTable.add table v (Some uv);
     uv
-
 end (* UVar *)
 
 (* -------------------------------------------------------------------------- *)
@@ -394,7 +397,7 @@ let rec ok : type a . a co -> bool =
       true
   | CMap (c, _) ->
       ok c
-  | CLet (_, _, c2) ->
+  | CLet (_rs, _xvs, _c1, c2) ->
       (* The left-hand constraint [c1] does not need to be [ok], since it is
          examined after a call to [G.enter]. *)
       ok c2
@@ -481,7 +484,7 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
         unify range (uvar v) (uvar w);
         On_sol (fun () -> ())
     | CExist (v, s, c) ->
-        ignore (ubind v s);
+        ignore (ubind v G.Flexible s);
         solve env range c
     | CWitness v ->
         On_sol (fun () -> decode (uvar v))
@@ -497,14 +500,16 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
     | CDef (x, v, c) ->
         let env = Env.bind x (G.trivial (uvar v)) env in
         solve env range c
-    | CLet (xvs, c1, c2) ->
+    | CLet (rs, xvs, c1, c2) ->
         (* Warn the generalization engine that we are entering the left-hand
            side of a [let] construct. *)
         G.enter state;
+        (* Register the rigid prefix [rs] with th generalization engine. *)
+        let _ = 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. *)
-        let vs = List.map (fun (_, v) -> ubind v None) xvs in
+        let vs = List.map (fun (_, v) -> ubind v G.Flexible None) xvs in
         (* Solve the constraint [c1]. *)
         let (On_sol r1) = solve env range c1 in
         (* Ask the generalization engine to perform an occurs check, to adjust
@@ -656,7 +661,6 @@ let instance x v =
 
 let instance_ x v =
   CMap (instance x v, ignore)
-
 (* -------------------------------------------------------------------------- *)
 
 (* Constraint abstractions. *)
@@ -667,26 +671,6 @@ let instance_ x v =
 let def x v c =
   CDef (x, v, c)
 
-(* The general form of [CLet] involves two constraints, the left-hand side and
-   the right-hand side, yet it defines a *family* of constraint abstractions,
-   which become bound to the term variables [xs]. *)
-
-let letn xs f1 c2 =
-  (* For each term variable [x], create a fresh type variable [v], as in
-     [CExist]. *)
-  let xvs = List.map (fun x ->
-    x, fresh ()
-  ) xs in
-  (* Pass the vector of type variables to the user-supplied function [f1],
-     as in [CExist]. *)
-  let vs = List.map (fun (_, v) -> v) xvs in
-  let c1 = f1 vs in
-  (* Build a [CLet] constraint. *)
-  CMap (CLet (xvs, c1, c2),
-        fun (generalizable, xss, s1, s2) ->
-          let ss = List.map snd xss in
-          (ss, generalizable, s1, s2))
-
 (* The auxiliary function [single] asserts that its argument [xs] is a
    singleton list, and extracts its unique element. *)
 
@@ -697,19 +681,71 @@ let single xs =
   | _ ->
       assert false
 
+let letrn
+  : 'client_tyvar list
+    ->  tevar list
+    -> (('client_tyvar * variable) list
+        -> (tevar * variable) list
+        -> 'a co)
+    -> 'b co
+    -> (O.tyvar list * (tevar * scheme) list * 'a * 'b) co
+  = fun alphas xs f1 c2 ->
+  let rs = List.map (fun _a -> fresh ()) alphas in
+
+  (* For each term variable [x], create a fresh type variable [v], as in
+     [CExist]. *)
+  let xvs = List.map (fun x ->
+    x, fresh ()
+  ) xs in
+
+  let c1 = f1 (List.combine alphas rs) xvs in
+  let+ (generalizable, ss, v1, v2) =
+    CLet (rs, xvs, c1, c2)
+  in
+  (generalizable, ss, v1, v2)
+
+(* [letr1] is a special case of [letrn], where only one term variable
+   is bound. *)
+
+let letr1
+  : 'client_tyvar list
+    -> tevar
+    -> (('client_tyvar * variable) list -> variable -> 'a co)
+    -> 'b co
+    -> (O.tyvar list * 'a * 'b) co
+  = fun alphas x f1 c2 ->
+  let+ (generalizable, _ss, v1, v2) =
+    letrn alphas [x]
+      (fun rzs xzs ->
+        let (_,z) = single xzs in
+        f1 rzs z)
+      c2
+  in
+  (generalizable, v1, v2)
+
+(* The general form of [CLet] involves two constraints, the left-hand side and
+   the right-hand side, yet it defines a *family* of constraint abstractions,
+   which become bound to the term variables [xs]. *)
+
+let letn xs f1 c2 =
+  let+ (generalizable, xss, s1, s2) =
+    letrn [] xs (fun _ xvs -> f1 (List.map snd xvs)) c2 in
+  let ss = List.map snd xss in
+  (generalizable, ss, s1, s2)
+
 (* [let1] is a special case of [letn], where only one term variable is bound. *)
 
 let let1 x f1 c2 =
-  let+ (ss, generalizable, v1, v2) =
+  let+ (generalizable, ss, v1, v2) =
     letn [ x ] (fun vs -> f1 (single vs