Relaxed method resolution, based on sizes

[ppolesiuk]

This PR 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.

[Copilot]

Pull Request Overview

This PR implements a relaxed method resolution strategy that allows the same method to be used multiple times in a parameter resolution path, provided each successive usage operates on a smaller type. The previous implementation prohibited any duplicate method usage, which was overly restrictive for cases like pretty-printing nested data structures.

Key Changes:

• Replaces size-agnostic duplicate detection with size-based tracking using int Var.Map.t instead of Var.Set.t
• Adds a size function to compute type sizes, enabling comparison of type complexity
• Updates the restrict_var function to compare sizes and allow reuse when the new usage has a strictly smaller type size

Reviewed Changes

Copilot reviewed 7 out of 7 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
test/ok/ok0139_sizedMethodResolve.fram	Adds a test case demonstrating nested method resolution on progressively smaller types
src/TypeInference/ParamResolve.mli	Updates the vset parameter type from Var.Set.t to int Var.Map.t
src/TypeInference/ParamResolve.ml	Implements size-based restriction logic and updates all vset initializations
src/TypeInference/Constr.mli	Updates vset type and clarifies its usage in documentation
src/TypeInference/Constr.ml	Updates vset field type to match interface
src/Lang/UnifPriv/Type.ml	Implements size and scheme_size functions for computing type sizes
src/Lang/Unif.mli	Exports the new size function in the public API

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

The documentation describes vset as a 'Set of variables that cannot be used' but it's now a map from variables to their sizes. The comment should clarify that the map values represent size thresholds - variables can only be reused if the new usage has a strictly smaller size than the recorded value.

Suggested change

	(** 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.
	(** Map from variables to their size thresholds during method resolution.
	A variable can only be reused if the new usage has a strictly smaller size than the recorded value.
	This map is just passed as [~vset] to [ParamResolve.resolve_method]. Do not use it directly.

[ppolesiuk]

Technically, that is correct. However, the actual representation of this "variable set" is an implementation detail of the ParamResolve module, but since the method constraints should be defined earlier, the actual type representation leaks to the public interface. I added the comment "Do not use it directly" to stress that this is an implementation detail, and the actual representation doesn't matter. I don't see any point in making the documentation more precise here.

[Brychlikov]

I would like the comments to at least acknowledge in any way that vset is a map. If I were to stumble upon this fragment while working on something else, I would probably feel very lost: a variable named vset, that comments repeatedly insist is a Set, but has type int Var.Map.t.
You are right that the comment stresses to "not use it directly", and links to the very place where the type and role of vset is explained, but I still think the code as it is now is needlessly arcane.

[ppolesiuk]

Maybe we should change vset name to something that doesn't suggest a representation, like used_vars. Or, we can introduce another module, that provides some basic functionality related to these "sets". The type would remain abstract, and the code should be cleaner, but at the cost of introducing a new module. What do you think?

[Brychlikov]

I'd be perfectly happy with renaming it to used_vars. I don't think it's worth introducing a new module for such a small part of what ultimately is a stopgap measure.

[ppolesiuk]

The longer I look at this code, the more convinced I am that we should add a separate module for this "stopgap measure". I see at least two reasons to do that:

1. data abstraction — I feel really bad that some internal data representation leaks, and pollutes types in other modules;
2. code maintainability — this is simple data structure with a well-defined interface. However, I can imagine the situation when this module might grow in the future. For instance we can add command-line parameters to tune looping detection, like max depth proposed on the last meeting. Or when we will add type-classes we will face additional challenges that could be addressed there. If the implementation will stay in the ParamResolve module we could end up with spaghetti code, that is hard to maintain.

[Foxinio]

All changes seem correct w.r.t. what was discussed.

[Brychlikov]

I have a small issue with the internal documentation, but I don't feel very strongly about it and am willing to let it go.
LGTM

[Brychlikov]

I would like the comments to at least acknowledge in any way that vset is a map. If I were to stumble upon this fragment while working on something else, I would probably feel very lost: a variable named vset, that comments repeatedly insist is a Set, but has type int Var.Map.t.
You are right that the comment stresses to "not use it directly", and links to the very place where the type and role of vset is explained, but I still think the code as it is now is needlessly arcane.

[forell]

No complaints regarding this one from me. The idea to rename vset seems reasonable, though.

[ppolesiuk]

I decided to move cycle detection to a separate module. Moreover, as the number of parameters of functions in ParamResolve grows and grows, I grouped some parameters to a record, called resolve_env.

[Copilot]

Pull Request Overview

Copilot reviewed 10 out of 10 changed files in this pull request and generated no new comments.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[forell]

I found your arguments for a separate cycle detection module convincing.

[Brychlikov]

Looks great! No issues with readability or documentation for me.