Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid needless dependency on parameter .cmi by introducing Parameter_name.t #3708

Open
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

lukemaurer
Copy link
Contributor

@lukemaurer lukemaurer commented Mar 18, 2025

Based on #3172, though a bit more narrow to focus on just putting the new type in all the places.

The new type Global_module.Parameter_name.t takes the place of any Global_module.t or Global_module.Name.t that is known to be the name of a parameter. Can't have parameters. (Notably, even the current half-worked-out plans for parameterized parameters would actually keep this type in many places, so this isn't as much in the way as one might think.)

Concretely, the immediate benefit is that we no longer load the .cmi file of a parameter just because it's used in the name of an instance. (All that we actually need to check in Foo[Bar:Baz] is (a) that Foo expects a Bar, (b) that Baz implements Bar, and (c) that Foo and Baz agree on what Bar says, none of which requires loading bar.cmi.) This is tested in the Dune-like tests by removing -I flags that shouldn't be necessary.

Takes the place of any `Global_module.t` or `Global_module.Name.t` that is known
to be the name of a parameter. Can't have parameters. (Notably, even the current
half-worked-out plans for parameterized parameters would actually keep this type
in many places, so this isn't as much in the way as one might think.)
This has the benefit of not loading the .cmi file for something whose signature
we don't need (say because the parameter is only used as part of an instance
name).
@lukemaurer lukemaurer changed the title Introduce Global_module.Parameter_name.t Avoid needless dependency on parameter .cmi by introducing Parameter_name.t Mar 19, 2025
@lukemaurer lukemaurer requested a review from riaqn March 19, 2025 11:28
@riaqn
Copy link
Contributor

riaqn commented Mar 19, 2025

For the record: the failing CI wrt arm64 happened before, and is unrelated to the PR. The CI is not required so we can still merge the PR.

@mshinwell
Copy link
Collaborator

@riaqn please approve, then...

@mshinwell mshinwell added the parameterized-libs PRs needed for parameterized libraries label Mar 25, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
parameterized-libs PRs needed for parameterized libraries
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants