Merge Env and SVMap.

client/FPrinter.ml

@@ -42,9 +42,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)
@@ -88,7 +88,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.PInj (_, tys, i, p) ->
       P.PInj (Some (List.map (translate_type env) tys), i, self env p)
   | F.PTuple (_, ps) ->

client/Infer.ml

@@ -129,11 +129,32 @@ end
 (* -------------------------------------------------------------------------- *)
 
 (* Instantiate the solver. *)
+type tvar =
+  | Tevar of string
+  | SVar of int
+
+let fresh () : tvar =
+  let uid = Inferno.Utils.gensym()() in
+  SVar uid
 
 module X = struct
-  type tevar = string
-  let compare = String.compare
-  let to_string s = s
+  type tevar = tvar
+  let compare v1 v2 =
+    match v1, v2 with
+    | Tevar v1, Tevar v2 ->
+       compare v1 v2
+    | SVar v1, SVar v2 ->
+       Stdlib.compare v1 v2
+    | Tevar _, SVar _ ->
+       -1
+    | SVar _, Tevar _ ->
+       1
+  let to_string v =
+    match v with
+    | Tevar v ->
+       v
+    | SVar v ->
+       string_of_int v
 end
 
 module Solver = Inferno.Solver.Make(X)(S)(O)
@@ -304,25 +325,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
 
 (* -------------------------------------------------------------------------- *)
 
@@ -351,7 +354,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 (Tevar x) w in
         (* The translation makes the type application explicit. *)
         F.ftyapp (F.Var (pos, x)) tys
 
@@ -367,7 +370,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 (Tevar x) v1 (hastype u v2)
         and+ ty1 = witness v1
         in
         (* Once these constraints are solved, we obtain the translated function
@@ -388,7 +391,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+ ((b, _), a, t', u') = let1 (Tevar 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
@@ -401,11 +404,31 @@ 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) ->
+          let sv = fresh () in
+          let+ (alphas, t', tys) =
+            letr1 vs sv
+              (fun tyvs w -> convert_annot typedecl_env tyvs w t ty)
+              (instance sv 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 =
@@ -424,7 +447,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 (Tevar x) v (k v)
         in
 
         let@ vs = mapM_now on_var xs in
@@ -521,7 +544,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 (Tevar x) v1 @@ bind_pattern_vars pat_env u
     in
 
     let on_branch ((pat,u) : ML.branch)
@@ -552,15 +575,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) ->
 
@@ -619,13 +652,16 @@ 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 * string
 exception Unify = Solver.Unify
 exception Cycle = Solver.Cycle
 
 let translate ~rectypes (env : ML.datatype_env) (t : ML.term) : F.nominal_term =
-  Solver.solve ~rectypes (
-    let+ (vs, t) = let0 (exist (hastype env t)) in
-    (* [vs] are the binders that we must introduce *)
-    F.ftyabs vs t
-  )
+  try
+    Solver.solve ~rectypes (
+      let+ (vs, t) = let0 (exist (hastype env t)) in
+      (* [vs] are the binders that we must introduce *)
+      F.ftyabs vs t
+    )
+  with Solver.Unbound (range, Tevar x) ->
+    raise (Unbound (range, x))

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

@@ -13,7 +13,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

@@ -121,11 +121,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/TestML.ml

@@ -143,7 +143,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 );
     ])
@@ -197,12 +197,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"),
@@ -427,6 +427,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 ::
@@ -461,10 +477,16 @@ let test_suite =
       "pattern matching",
       [
         test_case "match tuple" `Quick test_match_tuple;
-        test_case "match none" `Quick test_match_tuple;
+        test_case "match none" `Quick test_match_none;
         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/TestMLRandom.ml

@@ -102,7 +102,7 @@ let let_prod k n self = QCheck.Gen.(
 
 let annot k n self = QCheck.Gen.(
   let+ t = self (k, n-1) in
-  ML.Annot (dummy_pos, t, (["'a"], ML.TyVar (dummy_pos, "'a")))
+  ML.Annot (dummy_pos, t, (ML.Flexible, ["'a"], ML.TyVar (dummy_pos, "'a")))
 )
 
 let term_gen = QCheck.Gen.(

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-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,54 @@ 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...
+
+  $ 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...
+
+  $ 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...
+
+  $ 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...
+
+  $ cat unit-rigid-wrong.midml
+  let _ =
+    (() : for 'a. 'a)
+
+  $ ../TestMidML.exe unit-rigid-wrong.midml
+  Type inference and translation to System F...
+
+  $ 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

@@ -80,6 +80,7 @@ type 'a data = {
   mutable structure: 'a OS.structure;
   mutable rank: rank;
   mutable generic: generic;
+  mutable is_rigid: bool
 }
 
 (* The module [Data] satisfies the signature [USTRUCTURE] required by the
@@ -90,10 +91,10 @@ module Data = struct
   type 'a structure =
     'a data
 
-  let make structure rank =
+  let make structure rank is_rigid =
     (* A fresh variable is ordinary, not generic. *)
     let generic = false in
-    { structure; rank; generic }
+    { structure; rank; generic; is_rigid }
 
   let map f data =
     { data with structure = OS.map f data.structure }
@@ -104,6 +105,23 @@ module Data = struct
   exception InconsistentConjunction =
     OS.InconsistentConjunction
 
+  let merge d1 d2 : int * bool =
+    match (d1.is_rigid, d2.is_rigid) with
+    | false, false ->
+       ( min d1.rank d2.rank, false )
+    | false, true ->
+       if d1.rank < d2.rank then
+         raise InconsistentConjunction
+       else
+         ( d2.rank, true )
+    | true, false ->
+       if d1.rank > d2.rank then
+         raise InconsistentConjunction
+       else
+         ( d1.rank, true )
+    | true, true ->
+       raise InconsistentConjunction
+
   (* [conjunction] is invoked by the unifier when two equivalence classes are
      unified. It is in charge of computing the data associated with the new
      class. *)
@@ -114,11 +132,13 @@ module Data = struct
     let structure = OS.conjunction equate data1.structure data2.structure in
     (* The rank of the new class is the minimum of the ranks of the two
        original classes. *)
-    let rank = min data1.rank data2.rank in
+    let (rank, is_rigid) = merge data1 data2 in
+    if is_rigid && structure <> None then
+      raise InconsistentConjunction;
     (* The unifier never acts on generic variables. *)
     assert (not data1.generic && not data2.generic);
     let generic = false in
-    { structure; rank; generic }
+    { structure; rank; generic; is_rigid }
 
 end
 
@@ -239,7 +259,13 @@ let register { pool; _ } v r =
 
 let fresh state structure =
   let r = state.young in
-  let v = U.fresh (Data.make structure r) in
+  let v = U.fresh (Data.make structure r false) in
+  register state v r;
+  v
+
+let fresh_rigid state structure =
+  let r = state.young in
+  let v = U.fresh (Data.make structure r true) in
   register state v r;
   v
 
@@ -617,6 +643,28 @@ let exit ~rectypes state roots =
   (* Done. *)
   quantifiers, schemes
 
+let exit_rigid ~rectypes state root =
+  let young_vars = discover_young_generation state in
+
+  let on_var w =
+    if U.is_representative w && rank w = state.young then
+      match structure w with
+      | None ->
+         if not (U.structure w).is_rigid then
+           set_rank w (state.young - 1)
+      | Some _ ->
+         ()
+  in
+
+  List.iter on_var young_vars.inhabitants;
+
+  let _, schemes = exit ~rectypes state [root] in
+  match schemes with
+  | [s] ->
+     s
+  | _ ->
+     assert false
+
 (* -------------------------------------------------------------------------- *)
 
 (* Instantiation amounts to copying a fragment of a graph. The variables that

src/Generalization.mli

@@ -75,6 +75,8 @@ module Make (S : GSTRUCTURE) : sig
      [enter]/[exit] balance is at least one. *)
   val fresh: state -> variable S.structure option -> variable
 
+  val fresh_rigid: state -> variable S.structure option -> 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
      type schemes are created by the functions [enter] and [exit] below. *)
@@ -120,6 +122,8 @@ module Make (S : GSTRUCTURE) : sig
 
   val exit: rectypes:bool -> state -> variable list -> variable list * scheme list
 
+  val exit_rigid: rectypes:bool -> state -> variable -> scheme
+
   (* [instantiate] takes a fresh copy of a type scheme. The generic variables
      of the type scheme are replaced with freshly created variables, which are
      automatically registered (hence, the current state is updated). The function

src/Solver.ml

@@ -118,6 +118,9 @@ type _ co =
        - the value [a2] produced by solving the constraint [c2].
       *)
 
+| CLetRigid : variable list * variable * 'a co * tevar * 'b co ->
+    (O.tyvar list * 'a * 'b) co
+
 (* -------------------------------------------------------------------------- *)
 
 (* A pretty-printer for constraints, used while debugging. *)
@@ -176,6 +179,14 @@ module Printer = struct
         next c1 ^^
         string " in")) ^/^
         self c2
+    | CLetRigid (vs, z, c1, s, c2) ->
+        string "letr " ^^
+        separate_map (string " and ") var (vs @ [z]) ^^
+        string " where" ^^ group (nest 2 (break 1 ^^
+        next c1 ^^
+        string " in")) ^/^
+        self c2 ^^
+        string " : " ^^ tevar s
     | _ ->
         next c
 
@@ -210,6 +221,7 @@ module Printer = struct
     | CExist _
     | CDef _
     | CLet _
+    | CLetRigid _
     | CConj _
       ->
         (* Introduce parentheses. *)
@@ -288,6 +300,12 @@ end) = struct
     VarTable.add table v (Some uv);
     uv
 
+  let ubind_rigid (v : variable) so =
+    assert (not (VarTable.mem table v));
+    let uv = G.fresh_rigid X.state (Option.map (S.map uvar) so) in
+    VarTable.add table v (Some uv);
+    uv
+
 end (* UVar *)
 
 (* -------------------------------------------------------------------------- *)
@@ -386,6 +404,13 @@ let exit range ~rectypes state vs =
     let decode = new_decoder ~rectypes:true in
     raise (Cycle (range, decode v))
 
+let exit_rigid range ~rectypes state z =
+  try
+    G.exit_rigid ~rectypes state z
+  with U.Cycle v ->
+    let decode = new_decoder ~rectypes:true in
+    raise (Cycle (range, decode v))
+
 (* -------------------------------------------------------------------------- *)
 
 (* The toplevel constraint that is passed to the solver must have been
@@ -411,6 +436,8 @@ let rec ok : type a . a co -> bool =
       (* The left-hand constraint [c1] does not need to be [ok], since it is
          examined after a call to [G.enter]. *)
       ok c2
+  | CLetRigid (_vs, _z, c1, _s, c2) ->
+      ok c1 && ok c2
   | CConj (c1, c2) ->
       ok c1 && ok c2
   | CEq _
@@ -532,6 +559,18 @@ let solve ~(rectypes : bool) (type a) (c : a co) : a =
           List.map (fun (x, s) -> (x, decode_scheme decode s)) xss,
           r1 (),
           r2 ())
+    | CLetRigid (vs, z, c1, sv, c2) ->
+        G.enter state;
+        let vs = List.map (fun v -> ubind_rigid v None) vs in
+        let z = ubind z None in
+        let (On_sol r1) = solve env range c1 in
+        let s = exit_rigid range ~rectypes state z in
+        let env = Env.bind sv s env in
+        let (On_sol r2) = solve env range c2 in
+        On_sol (fun () ->
+            List.map decode_variable vs,
+            r1 (),
+            r2 ())
   in
 
   let env = Env.empty
@@ -679,7 +718,6 @@ let instance x v =
 
 let instance_ x v =
   CMap (instance x v, ignore)
-
 (* -------------------------------------------------------------------------- *)
 
 (* Constraint abstractions. *)
@@ -734,6 +772,20 @@ let let0 c1 =
   letn [] (fun _ -> c1) CTrue <$$>
   fun (_, generalizable, v1, ()) -> (generalizable, v1)
 
+let letr1
+  : 'tyvar list
+    -> tevar
+    -> (('tyvar * variable) list -> variable -> 'a co)
+    -> 'b co
+    -> (O.tyvar list * 'a * 'b) co
+  = fun alphas sv f1 c2 ->
+  let xvss = List.map (fun a ->
+    a, fresh ()
+  ) alphas in
+  let z = fresh () in
+  let c1 = f1 xvss z in
+  CLetRigid (List.map snd xvss, z, c1, sv, c2)
+
 (* -------------------------------------------------------------------------- *)
 
 (* Correlation with the source code. *)

src/Solver.mli

@@ -127,7 +127,6 @@ module Make
 
   (* [instance_ x v] is equivalent to [instance x v <$$> ignore]. *)
   val instance_: tevar -> variable -> unit co
-
   (* ---------------------------------------------------------------------- *)
 
   (* Construction of constraint abstractions, a.k.a. generalization. *)
@@ -150,6 +149,12 @@ module Make
   val let1: tevar -> (variable -> 'a co) -> 'b co ->
             (scheme * tyvar list * 'a * 'b) co
 
+  val letr1: 'tyvar list
+             -> tevar
+             -> (('tyvar * variable) list -> variable -> 'a co)
+             -> 'b co
+             -> (tyvar list * 'a * 'b) co
+
   (* [let0 c] has the same meaning as [c], but, like [let1], produces a list [vs]
      of the type variables that may appear in the result of [c]. *)
   val let0: 'a co  -> (tyvar list * 'a) co