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

Transform associated types into type parameters #532

Merged
merged 7 commits into from
Jan 22, 2025

Conversation

Nadrieril
Copy link
Member

@Nadrieril Nadrieril commented Jan 21, 2025

This PR introduces a --remove-associated-types <name pattern> option that replaces the associated types of the selected traits and converts them into type parameters.

Fixes #127.

This has 4 know limitations today:

This also has three fundamental limitations that we can't work around:

  • We can't handle GATs, as this would require passing type-level functions as type parameters;
  • We can't handle for<'a> clauses with unconstrained associated types, for the same reason;
  • We can't add parameters to self-recursive traits, as this would require an infinite list of parameters.

Linked lists are slow to iterate through; we don't need the reordering
capabilities that hashlink provides.
@Nadrieril Nadrieril force-pushed the associated-types branch 2 times, most recently from 27678ed to 1e6e24e Compare January 22, 2025 12:26
@Nadrieril Nadrieril marked this pull request as ready for review January 22, 2025 13:03
@Nadrieril Nadrieril force-pushed the associated-types branch 2 times, most recently from 5c77cc1 to bf43b79 Compare January 22, 2025 13:12
@sonmarcho
Copy link
Member

This is really awesome to see this finally landing, thanks a lot for this! And specifying which traits this should be applied on by using a pattern is a good design choice.

I have one question: by <'a> clauses with unconstrained associated types you mean something like this?

trait Foo<'a> {
  type Bar;
  ...
}

fn f<T>(...) where for<'a> T : Foo<'a>

@Nadrieril
Copy link
Member Author

I have one question: by "<'a> clauses with unconstrained associated types" you mean something like this?

Yep exactly, because we'd have to translate that to something like

fn f<T, Bar<'_>>(...) where for<'a> T : Foo<'a, Bar<'a>>

which doesn't exist in rust.

@Nadrieril Nadrieril merged commit a40e0d7 into AeneasVerif:main Jan 22, 2025
5 checks passed
@Nadrieril Nadrieril deleted the associated-types branch January 22, 2025 16:55
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Hide associated types equality constraints
2 participants