Recursion in Unif closer to Surface

src/Lang/Unif.mli

@@ -318,8 +318,25 @@ and expr_data =
   | ELetMono of var * expr * expr
     (** Monomorphic let-definition *)
 
-  | ELetRec of rec_def list * expr
-    (** Mutually recursive let-definitions *)
+  | ELetRec of (** Mutually recursive let-definitions *)
+    { targs : named_tvar list;
+      (** Type parameters common to all definitions *)
+
+      named : (name * var * scheme_expr) list;
+      (** Named parameters common to all definitions *)
+
+      defs  : rec_def list;
+      (** Mutually recursive definitions *)
+
+      body  : expr
+      (** Body of the let-rec *)
+    }
+
+  | ERecCtx of expr
+    (** Context for mutually recursive definitions. It is used to bind
+      less polymorphic variables in mutually recursive definitions.
+      It should appear only in the recursive definitions under some impure
+      function. *)
 
   | EData of data_def list * expr
     (** Definition of mutually recursive ADTs. *)
@@ -401,7 +418,26 @@ and expr_data =
       expression, then continue to the second expression. *)
 
 (** Definition of recursive value *)
-and rec_def = var * scheme * poly_expr
+and rec_def =
+  { rd_pos      : Position.t;
+    (** Position of the definition *)
+
+    rd_poly_var : var;
+    (** More polymorphic variable that represents the definition. It is bound
+      in the body of let-rec. *)
+
+    rd_var      : var;
+    (** Less polymorphic variable that represents the definition. It is bound
+      locally by the nearest [ERecCtx] in the mutually recursive definitions.
+      *)
+
+    rd_scheme   : scheme_expr;
+    (** Scheme of the definition, or more precisely, the scheme of [rd_var].
+      It doesn't contain common parameters. *)
+
+    rd_body     : poly_expr;
+    (** Body of the definition *)
+  }
 
 (** Clause of a pattern matching *)
 and match_clause = pattern * expr
@@ -843,6 +879,9 @@ module Ren : sig
   (** Rename type scheme *)
   val rename_scheme : t -> scheme -> scheme
 
+  (** Rename scheme expression *)
+  val rename_scheme_expr : t -> scheme_expr -> scheme_expr
+
   (** Rename variables in pattern *)
   val rename_pattern : t -> pattern -> pattern
 end

src/Lang/UnifPriv/Ren.mli

@@ -33,5 +33,8 @@ val rename_type : t -> typ -> typ
 (** Rename type scheme *)
 val rename_scheme : t -> scheme -> scheme
 
+(** Rename type scheme expression *)
+val rename_scheme_expr : t -> scheme_expr -> scheme_expr
+
 (** Rename variables in pattern *)
 val rename_pattern : t -> pattern -> pattern

src/Lang/UnifPriv/Syntax.ml

@@ -95,7 +95,13 @@ and expr_data =
   | EAppMono    of expr * expr
   | ELetPoly    of var * poly_expr * expr
   | ELetMono    of var * expr * expr
-  | ELetRec     of rec_def list * expr
+  | ELetRec     of
+    { targs : named_tvar list;
+      named : (name * var * scheme_expr) list;
+      defs  : rec_def list;
+      body  : expr
+    }
+  | ERecCtx     of expr
   | EData       of data_def list * expr
   | EMatchEmpty of proof_expr * expr * typ * effct
   | EMatch      of expr * match_clause list * typ * effct
@@ -119,7 +125,13 @@ and expr_data =
   | ERepl       of (unit -> expr) * typ
   | EReplExpr   of expr * expr
 
-and rec_def = var * scheme * poly_expr
+and rec_def =
+  { rd_pos      : Position.t;
+    rd_poly_var : var;
+    rd_var      : var;
+    rd_scheme   : scheme_expr;
+    rd_body     : poly_expr;
+  }
 
 and match_clause = pattern * expr
 

src/TypeInference/Def.ml

@@ -200,7 +200,12 @@ let check_def : type st dir. tcfix:tcfix ->
     let rest = cont.run env (Check tp) in
     { er_expr   =
         make rest (T.EData(result.rec_dds,
-          make rest (T.ELetRec(result.rec_fds, rest.er_expr))));
+          make rest (T.ELetRec
+            { targs = result.rec_targs;
+              named = result.rec_named;
+              defs  = result.rec_fds;
+              body  = rest.er_expr
+            })));
       er_type   = resp;
       er_effect = T.Effect.join result.rec_eff rest.er_effect;
       er_constr = result.rec_constr @ rest.er_constr

src/TypeInference/Expr.ml

@@ -72,6 +72,7 @@ let infer_expr_type ~tcfix ?app_type env (e : S.expr) =
   | EFn(pat, body) ->
     let tp2 = Env.fresh_uvar env T.Kind.k_type in
     let (env, pat, sch, eff1) = Pattern.infer_scheme_ext env pat in
+    let sch = T.SchemeExpr.to_scheme sch in
     let er_body = check_expr_type env body tp2 in
     let eff = T.Effect.join eff1 er_body.er_effect in
     let (x, body) = ExprUtils.match_var pat er_body.er_expr tp2 eff in

src/TypeInference/Name.ml

@@ -25,7 +25,7 @@ type scheme =
     sch_body  : T.typ
   }
 
-type pattern = t * T.pattern * T.scheme
+type pattern = t * T.pattern * T.scheme_expr
 
 let to_unif name =
   match name with

src/TypeInference/Name.mli

@@ -36,7 +36,7 @@ type scheme =
   }
 
 (** Named pattern that uses more precise names *)
-type pattern = t * T.pattern * T.scheme
+type pattern = t * T.pattern * T.scheme_expr
 
 (** Translate a name to Unif representation. *)
 val to_unif : t -> T.name

src/TypeInference/NameUtils.ml

@@ -79,5 +79,7 @@ let rename ren (name : Name.t) =
   | NMethod(owner, m) ->
     Name.NMethod(rename_method_owner ren owner, m)
 
-let rename_pattern ren (name, pat, sch) =
-  (rename ren name, T.Ren.rename_pattern ren pat, T.Ren.rename_scheme ren sch)
+let rename_pattern ren (name, pat, sch_expr) =
+  ( rename ren name,
+    T.Ren.rename_pattern ren pat,
+    T.Ren.rename_scheme_expr ren sch_expr )

src/TypeInference/Pattern.ml

@@ -371,16 +371,15 @@ let infer_scheme env (pat : S.pattern) =
   match pat.data with
   | PWildcard | PId _ | PCtor _ ->
     let tp = Env.fresh_uvar env T.Kind.k_type in
-    let sch = T.Scheme.of_type tp in
+    let sch = T.SchemeExpr.of_type_expr { pat with data = T.TE_Type tp } in
     let (penv, pat, eff) = check_type env pat tp in
     (penv, pat, sch, eff)
 
   | PAnnot(pat, sch) ->
     let sch_expr = Type.tr_scheme env sch in
     let sch = T.SchemeExpr.to_scheme sch_expr in
     let (penv, pat, eff) = check_scheme env pat sch in
-    let pat = { pat with T.data = T.PAnnot(pat, sch_expr) } in
-    (penv, pat, sch, eff)
+    (penv, pat, sch_expr, eff)
 
 (** Translate a named pattern. Returns the tuple of the following:
   - environment extended with type parameters, but not with existential types
@@ -409,42 +408,46 @@ let infer_named_pattern env (np : S.named_pattern) =
     (env, penv, tvars, [], T.Pure)
 
   | NP_Val(NOptionalVar x, pat, sch_expr) ->
-    let tp =
+    let tp_expr =
       match sch_expr with
       | Some sch_expr ->
-        let sch = T.SchemeExpr.to_scheme (Type.tr_scheme env sch_expr) in
-        begin match T.Scheme.to_type sch with
-        | Some tp -> tp
+        let sch_expr = Type.tr_scheme env sch_expr in
+        begin match T.SchemeExpr.to_type_expr sch_expr with
+        | Some tp_expr -> tp_expr
         | None    ->
           Error.fatal
-            (Error.polymorphic_optional_parameter ~pos:sch_expr.sch_pos)
+            (Error.polymorphic_optional_parameter ~pos:sch_expr.se_pos)
         end
-      | None -> Env.fresh_uvar env T.Kind.k_type
+      | None ->
+        { np with data = T.TE_Type (Env.fresh_uvar env T.Kind.k_type) }
     in
-    let sch = BuiltinTypes.mk_option_scheme tp in
-    let (penv, pat, eff) = check_scheme env pat sch in
-    let arg = (np.pos, Name.NOptionalVar x, pat, sch) in
+    let sch_expr = BuiltinTypes.mk_option_scheme_expr tp_expr in
+    let (penv, pat, eff) =
+      check_scheme env pat (T.SchemeExpr.to_scheme sch_expr) in
+    let arg = (np.pos, Name.NOptionalVar x, pat, sch_expr) in
     (env, penv, [], [arg], eff)
 
   | NP_Val(name, pat, sch_expr) ->
-    let (penv, pat, sch, eff) =
+    let (penv, pat, sch_expr, eff) =
       match sch_expr with
       | Some sch_expr ->
-        let sch = T.SchemeExpr.to_scheme (Type.tr_scheme env sch_expr) in
-        let (penv, pat, eff) = check_scheme env pat sch in
-        (penv, pat, sch, eff)
+        let sch_expr = Type.tr_scheme env sch_expr in
+        let (penv, pat, eff) =
+          check_scheme env pat (T.SchemeExpr.to_scheme sch_expr) in
+        (penv, pat, sch_expr, eff)
       | None ->
         infer_scheme env pat
     in
     let arg =
       match name with
-      | NVar x -> (np.pos, Name.NVar x, pat, sch)
+      | NVar x -> (np.pos, Name.NVar x, pat, sch_expr)
       | NOptionalVar _ -> assert false
-      | NImplicit n -> (np.pos, Name.NImplicit n, pat, sch)
+      | NImplicit n -> (np.pos, Name.NImplicit n, pat, sch_expr)
       | NMethod mname ->
         let pp = Env.pp_tree env in
+        let sch = T.SchemeExpr.to_scheme sch_expr in
         let owner = NameUtils.method_owner_of_scheme ~pos:np.pos ~pp sch in
-        (np.pos, Name.NMethod(owner, mname), pat, sch)
+        (np.pos, Name.NMethod(owner, mname), pat, sch_expr)
     in
     (env, penv, [], [arg], eff)
 

src/TypeInference/Pattern.mli

@@ -11,11 +11,11 @@ open Common
 val check_type : 'st Env.t -> S.pattern -> T.typ ->
   PartialEnv.t * T.pattern * T.effct
 
-(** Infer type-scheme of given pattern. Returns partial-environment (variables
-  bound by this pattern), translated pattern, its scheme, and the effect of
-  pattern-matching *)
+(** Infer scheme expression of given pattern. Returns partial-environment
+  (variables bound by this pattern), translated pattern, its scheme
+  expression, and the effect of pattern-matching *)
 val infer_scheme : 'st Env.t -> S.pattern ->
-  PartialEnv.t * T.pattern * T.scheme * T.effct
+  PartialEnv.t * T.pattern * T.scheme_expr * T.effct
 
 (** Enter a new scope and translate a list of named patterns. The returned
   environment contains type parameters, but not the type variables bound by
@@ -30,7 +30,7 @@ val infer_named_patterns :
   environment, translated pattern, its scheme, and the effect of
   pattern-matching *)
 val infer_scheme_ext :
-  'st Env.t -> S.pattern -> 'st Env.t * T.pattern * T.scheme * T.effct
+  'st Env.t -> S.pattern -> 'st Env.t * T.pattern * T.scheme_expr * T.effct
 
 (** Check if given pattern has given type scheme. Returns extended
   environment, translated pattern, and the effect of pattern-matching *)

src/TypeInference/PolyExpr.ml

@@ -201,7 +201,9 @@ let infer_def_scheme ~tcfix env (e : S.poly_expr_def) =
       List.map (fun (name, pat, sch) ->
         let x = Var.fresh () in
         (name, x, pat, sch)) in
-    let sch_named = List.map (fun (name, _, _, sch) -> (name, sch)) named in
+    let sch_named =
+      List.map (fun (name, _, _, sch) -> (name, T.SchemeExpr.to_scheme sch))
+        named in
     let match_named = List.map (fun (_, x, pat, _) -> (x, pat)) named in
     let body_expr =
       ExprUtils.match_args match_named body.er_expr body_tp eff in
@@ -211,6 +213,9 @@ let infer_def_scheme ~tcfix env (e : S.poly_expr_def) =
         Name.sch_body  = body_tp
       } in
     let named =
-      List.map (fun (name, x, _, sch) -> (Name.to_unif name, x, sch)) named in
+      List.map
+        (fun (name, x, _, sch) ->
+          (Name.to_unif name, x, T.SchemeExpr.to_scheme sch))
+      named in
     let poly_expr = { T.pos; T.data = T.EPolyFun(targs, named, body_expr) } in
     PPure(poly_expr, sch, body.er_constr)