From 43b8e7ef8ed42a7785e655f5a12b90d158a2ea1b Mon Sep 17 00:00:00 2001
From: Piotr Polesiuk <ppolesiuk@cs.uni.wroc.pl>
Date: Tue, 11 Nov 2025 08:15:57 +0100
Subject: [PATCH 1/3] Relaxed method resolution, based on sizes

This commit proposes a relaxed restriction of a method resolution. Instead
of forbidding using the same method twice, it allows multiple use of the
same method, but each consecutive usage must be on the smaller type.
Since unification variables have size 1, the solution is not perfect, but
allows, e.g., for pretty-printing of nested lists.
---
 src/Lang/Unif.mli                      |  5 +++++
 src/Lang/UnifPriv/Type.ml              | 17 ++++++++++++++++
 src/TypeInference/Constr.ml            |  2 +-
 src/TypeInference/Constr.mli           |  3 ++-
 src/TypeInference/ParamResolve.ml      | 28 ++++++++++++++++----------
 src/TypeInference/ParamResolve.mli     |  2 +-
 test/ok/ok0139_sizedMethodResolve.fram | 20 ++++++++++++++++++
 7 files changed, 63 insertions(+), 14 deletions(-)
 create mode 100644 test/ok/ok0139_sizedMethodResolve.fram

diff --git a/src/Lang/Unif.mli b/src/Lang/Unif.mli
index de4e316e..2ebab020 100644
--- a/src/Lang/Unif.mli
+++ b/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
 
 (* ========================================================================= *)
diff --git a/src/Lang/UnifPriv/Type.ml b/src/Lang/UnifPriv/Type.ml
index a15245f2..f697f4f8 100644
--- a/src/Lang/UnifPriv/Type.ml
+++ b/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
diff --git a/src/TypeInference/Constr.ml b/src/TypeInference/Constr.ml
index ac7ab532..eede5c7b 100644
--- a/src/TypeInference/Constr.ml
+++ b/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;
diff --git a/src/TypeInference/Constr.mli b/src/TypeInference/Constr.mli
index 2a2a3e81..a6e7ace6 100644
--- a/src/TypeInference/Constr.mli
+++ b/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;
diff --git a/src/TypeInference/ParamResolve.ml b/src/TypeInference/ParamResolve.ml
index a54ab810..f023779b 100644
--- a/src/TypeInference/ParamResolve.ml
+++ b/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
diff --git a/src/TypeInference/ParamResolve.mli b/src/TypeInference/ParamResolve.mli
index aa4d2de0..4e4d3095 100644
--- a/src/TypeInference/ParamResolve.mli
+++ b/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
diff --git a/test/ok/ok0139_sizedMethodResolve.fram b/test/ok/ok0139_sizedMethodResolve.fram
new file mode 100644
index 00000000..1b1a4062
--- /dev/null
+++ b/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

From 077a8c2ff0286904fbec1eb2a16f8202de3a6e8e Mon Sep 17 00:00:00 2001
From: Piotr Polesiuk <ppolesiuk@cs.uni.wroc.pl>
Date: Mon, 17 Nov 2025 22:30:43 +0100
Subject: [PATCH 2/3] Parameter cycle detection as a separate module

And a slight refactoring of ParamResolve
---
 src/TypeInference/Constr.ml            |   2 +-
 src/TypeInference/Constr.mli           |   7 +-
 src/TypeInference/ConstrSolve.ml       |   2 +-
 src/TypeInference/ParamCycleDetect.ml  |  17 ++++
 src/TypeInference/ParamCycleDetect.mli |  18 ++++
 src/TypeInference/ParamResolve.ml      | 121 ++++++++++++++-----------
 src/TypeInference/ParamResolve.mli     |   7 +-
 7 files changed, 109 insertions(+), 65 deletions(-)
 create mode 100644 src/TypeInference/ParamCycleDetect.ml
 create mode 100644 src/TypeInference/ParamCycleDetect.mli

diff --git a/src/TypeInference/Constr.ml b/src/TypeInference/Constr.ml
index eede5c7b..b74b4921 100644
--- a/src/TypeInference/Constr.ml
+++ b/src/TypeInference/Constr.ml
@@ -9,7 +9,7 @@ open Common
 type t =
   | ResolveMethod : {
       hole       : T.poly_fun option BRef.t;
-      vset       : int Var.Map.t;
+      pcyc       : ParamCycleDetect.t;
       pos        : Position.t;
       env        : 'st Env.t;
       method_env : 'st Env.t;
diff --git a/src/TypeInference/Constr.mli b/src/TypeInference/Constr.mli
index a6e7ace6..573372be 100644
--- a/src/TypeInference/Constr.mli
+++ b/src/TypeInference/Constr.mli
@@ -11,11 +11,8 @@ type t =
       hole : T.poly_fun option BRef.t;
         (** Hole to be filled with method implementation *)
 
-      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.
-        *)
+      pcyc : ParamCycleDetect.t;
+        (** Parameter cycle detector state *)
 
       pos : Position.t;
         (** Position of the place where parameter resoultion is requested *)
diff --git a/src/TypeInference/ConstrSolve.ml b/src/TypeInference/ConstrSolve.ml
index 99663e2d..eb49c0c1 100644
--- a/src/TypeInference/ConstrSolve.ml
+++ b/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
diff --git a/src/TypeInference/ParamCycleDetect.ml b/src/TypeInference/ParamCycleDetect.ml
new file mode 100644
index 00000000..d75b1919
--- /dev/null
+++ b/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
diff --git a/src/TypeInference/ParamCycleDetect.mli b/src/TypeInference/ParamCycleDetect.mli
new file mode 100644
index 00000000..eacef5a7
--- /dev/null
+++ b/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
diff --git a/src/TypeInference/ParamResolve.ml b/src/TypeInference/ParamResolve.ml
index f023779b..e7618a9f 100644
--- a/src/TypeInference/ParamResolve.ml
+++ b/src/TypeInference/ParamResolve.ml
@@ -132,23 +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 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 _ ->
+(** 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)
 
 (* ------------------------------------------------------------------------- *)
 
-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
@@ -159,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)
@@ -222,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)
@@ -242,9 +251,9 @@ 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, _, _) ->
@@ -252,33 +261,35 @@ and resolve_method ~vset ~pos env ?(method_env=env) mname (sch : T.scheme) =
       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 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
+      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.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 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;
@@ -287,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.Map.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.Map.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.Map.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
diff --git a/src/TypeInference/ParamResolve.mli b/src/TypeInference/ParamResolve.mli
index 4e4d3095..141ac853 100644
--- a/src/TypeInference/ParamResolve.mli
+++ b/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:int Var.Map.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

From 6068458ab953f03ba16dff66f47c2a1224e1f774 Mon Sep 17 00:00:00 2001
From: Piotr Polesiuk <ppolesiuk@cs.uni.wroc.pl>
Date: Sat, 22 Nov 2025 21:33:48 +0100
Subject: [PATCH 3/3] Renaming test

---
 ...139_sizedMethodResolve.fram => ok0144_sizedMethodResolve.fram} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename test/ok/{ok0139_sizedMethodResolve.fram => ok0144_sizedMethodResolve.fram} (100%)

diff --git a/test/ok/ok0139_sizedMethodResolve.fram b/test/ok/ok0144_sizedMethodResolve.fram
similarity index 100%
rename from test/ok/ok0139_sizedMethodResolve.fram
rename to test/ok/ok0144_sizedMethodResolve.fram