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;
+      vset       : int Var.Map.t;
       pos        : Position.t;
       env        : 'st Env.t;
       method_env : 'st Env.t;

src/TypeInference/Constr.mli

@@ -11,9 +11,10 @@ type t =
       hole : T.poly_fun option BRef.t;
         (** Hole to be filled with method implementation *)
 
-      vset : Var.Set.t;
+      vset : int Var.Map.t;
         (** Set of variables that cannot be used during method resolution.
           This set is just passed as [~vset] to [ParamResolve.resolve_method].
+          Do not use it directly.
         *)
 
       pos : Position.t;

src/TypeInference/ParamResolve.ml

@@ -132,13 +132,18 @@ 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
+(** Check for cyclic dependencies in named parameters, and extend a set of
+  restricted variables. A parameter might be used several times, but each
+  next usage on the same path must have a smaller size. For methods, the
+  size is determined from the [self] type, while for other kinds of
+  parameters, the size is 0. *)
+let restrict_var ~vset ~pos ~pp x ?(size=0) name =
+  match Var.Map.find_opt x vset with
+  | None -> Var.Map.add x size vset
+  | Some old_size when size < old_size ->
+    Var.Map.add x size vset
+  | Some _ ->
     Error.fatal (Error.looping_named_param ~pos ~pp name)
-  else
-    Var.Set.add x vset
 
 (* ------------------------------------------------------------------------- *)
 
@@ -253,7 +258,8 @@ and resolve_method ~vset ~pos env ?(method_env=env) mname (sch : T.scheme) =
     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 size = T.Type.size self_tp in
+      let vset = restrict_var ~vset ~pos ~pp x ~size 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
 
@@ -270,7 +276,7 @@ and resolve_method ~vset ~pos env ?(method_env=env) mname (sch : T.scheme) =
 
 (* ========================================================================= *)
 let instantiate ~pos env rctx poly_expr (sch : T.scheme) =
-  let vset = Var.Set.empty in
+  let vset = Var.Map.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 e =
@@ -281,12 +287,12 @@ 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
+  let vset = Var.Map.empty in
   coerce_scheme ~vset ~pos ~name env poly_expr sch_in sch_out
 
 let resolve_implicit ~pos env iname sch =
-  let vset = Var.Set.empty in
+  let vset = Var.Map.empty in
   resolve_implicit ~vset ~pos env no_reinst iname sch
 
-let resolve_method ?(vset=Var.Set.empty) ~pos env ?method_env mname sch =
+let resolve_method ?(vset=Var.Map.empty) ~pos env ?method_env mname sch =
   resolve_method ~vset ~pos env ?method_env mname sch

src/TypeInference/ParamResolve.mli

@@ -62,6 +62,6 @@ val resolve_implicit :
   visible in the interface because it is used by the constraint solver.
   Do not use it directly. *)
 val resolve_method :
-  ?vset:Var.Set.t ->
+  ?vset:int Var.Map.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/ok0139_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