Relaxed method resolution, based on sizes

src/Lang/Unif.mli

@@ -808,6 +808,11 @@ module Type : sig
     of unification variables accordingly. On error, it returns escaping type
     variable. *)
   val shrink_scope : scope:Scope.t -> typ -> (typ, tvar) result
+
+  (** Compute size of a type. Unification variables have size one, so
+    this function is not stable under instantiation of unification variables.
+  *)
+  val size : typ -> int
 end
 
 (* ========================================================================= *)

src/Lang/UnifPriv/Type.ml

@@ -270,3 +270,20 @@ let scheme_is_monomorphic sch =
   match scheme_to_type sch with
   | Some _ -> true
   | None   -> false
+
+(* ========================================================================= *)
+
+let rec size tp =
+  match view tp with
+  | TEffect | TUVar _ | TVar _ -> 1
+  | TArrow(sch, tp, _)         -> scheme_size sch + size tp
+  | THandler(_, tp, itp, otp)  -> size tp + size itp + size otp
+  | TLabel tp                  -> 1 + size tp
+  | TApp(tp1, tp2)             -> size tp1 + size tp2
+  | TAlias(_, tp)              -> size tp
+
+and scheme_size sch =
+  List.fold_left
+    (fun acc (_, sch) -> acc + scheme_size sch)
+    (size sch.sch_body)
+    sch.sch_named

src/TypeInference/Constr.ml

@@ -9,7 +9,7 @@ open Common
 type t =
   | ResolveMethod : {
       hole       : T.poly_fun option BRef.t;
-      vset       : Var.Set.t;
+      pcyc       : ParamCycleDetect.t;
       pos        : Position.t;
       env        : 'st Env.t;
       method_env : 'st Env.t;

src/TypeInference/Constr.mli

@@ -11,10 +11,8 @@ type t =
       hole : T.poly_fun option BRef.t;
         (** Hole to be filled with method implementation *)
 
-      vset : Var.Set.t;
-        (** Set of variables that cannot be used during method resolution.
-          This set is just passed as [~vset] to [ParamResolve.resolve_method].
-        *)
+      pcyc : ParamCycleDetect.t;
+        (** Parameter cycle detector state *)
 
       pos : Position.t;
         (** Position of the place where parameter resoultion is requested *)

src/TypeInference/ConstrSolve.ml

@@ -24,7 +24,7 @@ let rec try_solve_loop acc changed cs =
     | Some _ ->
       let (e, cs') =
         ParamResolve.resolve_method
-          ~vset:c.vset ~pos:c.pos c.env ~method_env:c.method_env c.mname c.sch
+          ~pcyc:c.pcyc ~pos:c.pos c.env ~method_env:c.method_env c.mname c.sch
       in
       BRef.set c.hole (Some e);
       try_solve_loop (List.rev_append cs' acc) true cs

src/TypeInference/ParamCycleDetect.ml

@@ -0,0 +1,17 @@
+(* This file is part of DBL, released under MIT license.
+ * See LICENSE for details.
+ *)
+
+(** Detection of cycles in named parameter resolution. *)
+
+type t = int Var.Map.t
+
+let empty = Var.Map.empty
+
+let add_var pcyc ?(size=0) x =
+  match Var.Map.find_opt x pcyc with
+  | None -> Some (Var.Map.add x size pcyc)
+  | Some old_size when size < old_size ->
+    Some (Var.Map.add x size pcyc)
+  | Some _ ->
+    None

src/TypeInference/ParamCycleDetect.mli

@@ -0,0 +1,18 @@
+(* This file is part of DBL, released under MIT license.
+ * See LICENSE for details.
+ *)
+
+(** Detection of cycles in named parameter resolution. *)
+
+(** Data structure used to detect cycles. *)
+type t
+
+(** Empty cycle detection structure. *)
+val empty : t
+
+(** Check for cyclic dependencies in named parameters, and update the state
+  of the cycle detector. Returns [None] if a cycle is detected, or
+  [Some new_state] otherwise. The [size] parameter is used to allow multiple
+  usages of the same parameter, as long as the consecutive usages have
+  decreasing sizes. If the size is not provided, it defaults to 0. *)
+val add_var : t -> ?size:int -> Var.t -> t option

src/TypeInference/ParamResolve.ml

@@ -132,18 +132,29 @@ let guess_types ~pos env targs =
   let scope = Env.scope env in
   List.fold_left_map guess_type (T.Subst.empty ~scope) targs
 
-(** Check for cyclic dependencies in the type parameters, and extend a set of
-  restricted variables. *)
-let restrict_var ~vset ~pos ~pp x name =
-  if Var.Set.mem x vset then
+(** Environment of the resolution process. *)
+type 'st resolve_env = {
+  pcyc : ParamCycleDetect.t;
+  pos  : Position.t;
+  env  : 'st Env.t;
+}
+
+let make ~resolve_env data =
+  let { pos; env; _ } = resolve_env in
+  { T.pos; T.pp = Env.pp_tree env; T.data }
+
+let restrict_var ~resolve_env ?size x name =
+  match ParamCycleDetect.add_var resolve_env.pcyc ?size x with
+  | Some pcyc -> { resolve_env with pcyc }
+  | None ->
+    let pos = resolve_env.pos in
+    let pp = Env.pp_tree resolve_env.env in
     Error.fatal (Error.looping_named_param ~pos ~pp name)
-  else
-    Var.Set.add x vset
 
 (* ------------------------------------------------------------------------- *)
 
-let rec coerce_scheme ~vset ~pos ~name env e (sch_in : T.scheme) sch_out =
-  let make data = { T.pos; T.pp = Env.pp_tree env; T.data } in
+let rec coerce_scheme ~resolve_env ~name e (sch_in : T.scheme) sch_out =
+  let { pos; env; _ } = resolve_env in
   let (env, rctx, tvs, xs, tp_out) = open_scheme ~pos env sch_out in
   (* Now we do basically the same as in [instantiate], but we perform
     unification just afeter guessing types, in order to get more precise
@@ -154,59 +165,62 @@ let rec coerce_scheme ~vset ~pos ~name env e (sch_in : T.scheme) sch_out =
   Error.check_unify_result ~pos
     (Unification.subtype env tp_in tp_out)
     ~on_error:(Error.named_param_type_mismatch ~pp name tp_in tp_out);
+  let resolve_env = { resolve_env with env } in
   let (named, cs) =
-    resolve_params ~sub ~vset ~pos env rctx sch_in.sch_named in
-  let e = make (T.PF_Fun(tvs, xs, make (T.EInst(e, tps, named)))) in
+    resolve_params ~sub ~resolve_env rctx sch_in.sch_named in
+  let e = make ~resolve_env
+    (T.PF_Fun(tvs, xs, make ~resolve_env (T.EInst(e, tps, named)))) in
   (e, cs)
 
-and resolve_params ~sub ~vset ~pos env rctx named =
+and resolve_params ~sub ~resolve_env rctx named =
   let resolve cs1 (name, sch) =
     let sch  = T.Scheme.subst sub sch in
-    let (e, cs2) = resolve_param ~vset ~pos env rctx name sch in
+    let (e, cs2) = resolve_param ~resolve_env rctx name sch in
     (cs1 @ cs2, e)
   in
   let (cs, args) = List.fold_left_map resolve [] named in
   (args, cs)
 
-and resolve_param ~vset ~pos env rctx name sch =
+and resolve_param ~resolve_env rctx name sch =
   match name with
   | T.NVar x ->
     begin match Reinst.lookup_var rctx x with
     | Some (RReg(y, y_sch)) ->
-      let vset = restrict_var ~vset ~pos ~pp:(Env.pp_tree env) y (NVar x) in
-      let e = { T.pos; T.pp = Env.pp_tree env; T.data = T.EVar y } in
-      coerce_scheme ~vset ~pos ~name:(NVar x) env e y_sch sch
+      let resolve_env = restrict_var ~resolve_env y (NVar x) in
+      let e = make ~resolve_env (T.EVar y) in
+      coerce_scheme ~resolve_env ~name:(NVar x) e y_sch sch
     | Some (ROpt _) | None ->
-      Error.fatal (Error.cannot_resolve_named_param ~pos x)
+      Error.fatal (Error.cannot_resolve_named_param ~pos:resolve_env.pos x)
     end
 
   | T.NOptionalVar x ->
-    resolve_optional ~vset ~pos env rctx x sch
+    resolve_optional ~resolve_env rctx x sch
 
   | T.NImplicit iname ->
-    resolve_implicit ~vset ~pos env rctx iname sch
+    resolve_implicit ~resolve_env rctx iname sch
 
   | T.NMethod mname ->
-    resolve_method ~vset ~pos env mname sch
+    resolve_method ~resolve_env ~method_env:resolve_env.env mname sch
 
-and resolve_optional ~vset ~pos env rctx x sch =
+and resolve_optional ~resolve_env rctx x sch =
   let tp = BuiltinTypes.scheme_to_option_arg sch in
   let name = Name.NOptionalVar x in
-  let pp = Env.pp_tree env in
-  let make data = T.{ pos; pp; data } in
+  let make data = make ~resolve_env data in
+  let pos = resolve_env.pos in
+  let pp  = Env.pp_tree resolve_env.env in
   begin match Reinst.lookup_var rctx x with
   | Some (ROpt(y, y_tp)) ->
     Error.check_unify_result ~pos
-      (Unification.subtype env y_tp tp)
+      (Unification.subtype resolve_env.env y_tp tp)
       ~on_error:(Error.named_param_type_mismatch ~pp name y_tp tp);
     let e = make (T.PF_Fun([], [], make (T.EInst(make (T.EVar y), [], [])))) in
     (e, [])
 
   | Some (RReg(y, y_sch)) ->
-    let vset = restrict_var ~vset ~pos ~pp y name in
+    let resolve_env = restrict_var ~resolve_env y name in
     let e = make (T.EVar y) in
     let (e, cs) =
-      coerce_scheme ~vset ~pos ~name env e y_sch (T.Scheme.of_type tp) in
+      coerce_scheme ~resolve_env ~name e y_sch (T.Scheme.of_type tp) in
     let e = BuiltinTypes.mk_some_poly ~pos ~pp tp e in
     let e = make (T.PF_Fun([], [], e)) in
     (e, cs)
@@ -217,17 +231,17 @@ and resolve_optional ~vset ~pos env rctx x sch =
     (e, [])
   end
 
-and resolve_implicit ~vset ~pos env rctx iname sch =
+and resolve_implicit ~resolve_env rctx iname sch =
   let name = Name.NImplicit iname in
-  match ModulePath.try_lookup_implicit ~pos env iname with
+  let make data = make ~resolve_env data in
+  let pos = resolve_env.pos in
+  match ModulePath.try_lookup_implicit ~pos resolve_env.env iname with
   | Some(x, x_sch) ->
-    let vset = restrict_var ~vset ~pos ~pp:(Env.pp_tree env) x name in
-    let e = { T.pos; T.pp = Env.pp_tree env; T.data = T.EVar x } in
-    coerce_scheme ~vset ~pos ~name env e x_sch sch
+    let resolve_env = restrict_var ~resolve_env x name in
+    let e = make (T.EVar x) in
+    coerce_scheme ~resolve_env ~name e x_sch sch
   | None ->
     (* Special implicits *)
-    let pp = Env.pp_tree env in
-    let make data = T.{data; pos; pp} in
     let (param_expr, param_tvar) = match iname with
       | "~__line__" -> 
         (make (T.ENum pos.pos_start_line), T.BuiltinType.tv_int)
@@ -237,42 +251,45 @@ and resolve_implicit ~vset ~pos env rctx iname sch =
     (* Check types *)
     let param_sch = T.Scheme.of_type (T.Type.t_var param_tvar) in
     let param = make (T.EPolyFun([], [], param_expr)) in
-    coerce_scheme ~vset ~pos ~name env param param_sch sch 
+    coerce_scheme ~resolve_env ~name param param_sch sch 
 
-and resolve_method ~vset ~pos env ?(method_env=env) mname (sch : T.scheme) =
+and resolve_method ~resolve_env ~method_env mname (sch : T.scheme) =
   let self_tp =
     match T.Type.view sch.sch_body with
     | TArrow(owner_sch, _, _) ->
       assert (T.Scheme.is_monomorphic owner_sch);
       owner_sch.sch_body
     | _ -> assert false
   in
-  let pp = Env.pp_tree env in
+  let pos = resolve_env.pos in
+  let pp  = Env.pp_tree resolve_env.env in
   match NameUtils.method_owner_of_self self_tp with
   | Some owner ->
     let name = Name.NMethod(owner, mname) in
     begin match ModulePath.try_lookup_method ~pos method_env owner mname with
     | Some(x, x_sch) ->
-      let vset = restrict_var ~vset ~pos ~pp x name in
-      let e = { T.pos; T.pp = Env.pp_tree env; T.data = T.EVar x } in
-      coerce_scheme ~vset ~pos ~name env e x_sch sch
+      let size = T.Type.size self_tp in
+      let resolve_env = restrict_var ~resolve_env ~size x name in
+      let e = make ~resolve_env (T.EVar x) in
+      coerce_scheme ~resolve_env ~name e x_sch sch
 
     | None ->
       Error.fatal (Error.cannot_resolve_method ~pos ~pp owner mname)
     end
   | None ->
     let hole = BRef.create None in
-    let e = { T.pos; T.pp = Env.pp_tree env; T.data = T.PF_Hole hole } in
+    let e = make ~resolve_env (T.PF_Hole hole) in
+    let { pcyc; pos; env } = resolve_env in
     let constr =
       Constr.ResolveMethod
-        { hole; vset; pos; env; method_env; self_tp; mname; sch } in
+        { hole; pcyc; pos; env; method_env; self_tp; mname; sch } in
     (e, [constr])
 
 (* ========================================================================= *)
 let instantiate ~pos env rctx poly_expr (sch : T.scheme) =
-  let vset = Var.Set.empty in
   let (sub, tps) = guess_types ~pos env sch.sch_targs in
-  let (named, cs) = resolve_params ~sub ~vset ~pos env rctx sch.sch_named in
+  let resolve_env = { pcyc = ParamCycleDetect.empty; pos; env } in
+  let (named, cs) = resolve_params ~sub ~resolve_env rctx sch.sch_named in
   let e =
     { T.pos  = pos;
       T.pp   = Env.pp_tree env;
@@ -281,12 +298,14 @@ let instantiate ~pos env rctx poly_expr (sch : T.scheme) =
   (e, T.Type.subst sub sch.sch_body, cs)
 
 let coerce_scheme ~pos ~name env poly_expr sch_in sch_out =
-  let vset = Var.Set.empty in
-  coerce_scheme ~vset ~pos ~name env poly_expr sch_in sch_out
+  let resolve_env = { pcyc = ParamCycleDetect.empty; pos; env } in
+  coerce_scheme ~resolve_env ~name poly_expr sch_in sch_out
 
 let resolve_implicit ~pos env iname sch =
-  let vset = Var.Set.empty in
-  resolve_implicit ~vset ~pos env no_reinst iname sch
+  let resolve_env = { pcyc = ParamCycleDetect.empty; pos; env } in
+  resolve_implicit ~resolve_env no_reinst iname sch
 
-let resolve_method ?(vset=Var.Set.empty) ~pos env ?method_env mname sch =
-  resolve_method ~vset ~pos env ?method_env mname sch
+let resolve_method
+    ?(pcyc=ParamCycleDetect.empty) ~pos env ?(method_env=env) mname sch =
+  let resolve_env = { pcyc; pos; env } in
+  resolve_method ~resolve_env ~method_env mname sch

src/TypeInference/ParamResolve.mli

@@ -58,10 +58,9 @@ val resolve_implicit :
 (** Resolve a method parameter of given scheme in given environment. If the
   [~method_env] argument is provided, the method is searched in the
   [~method_env] environment, but its parameters are resolved in the given
-  environment. The [~vset] argument is for the internal use only, but it is
-  visible in the interface because it is used by the constraint solver.
-  Do not use it directly. *)
+  environment. The [~pcyc] argument is the internal state of the parameter
+  cycle detection, saved when a method resolution was delayed. *)
 val resolve_method :
-  ?vset:Var.Set.t ->
+  ?pcyc:ParamCycleDetect.t ->
   pos:Position.t -> 'st Env.t -> ?method_env:'st Env.t ->
     S.method_name -> T.scheme -> T.poly_fun * Constr.t list

test/ok/ok0144_sizedMethodResolve.fram

@@ -0,0 +1,20 @@
+data B X = B of X
+data P X Y = P of X, Y
+
+data rec Shape =
+  | SU
+  | SB of Shape
+  | SP of Shape, Shape
+
+method shape () = SU
+method shape {X, method shape : X -> Shape} (B (x : X)) =
+  SB x.shape
+method shape
+  { X, Y
+  , method shape : X -> Shape
+  , method shape : Y -> Shape
+  } (P (x : X) (y : Y)) =
+    SP x.shape y.shape
+
+let _ =
+  (P (P (P (B (B ())) (B (P () ()))) (B (P () (B (P () ()))))) ()).shape