Skip to content

WIP: Rework inference - #409

Draft
tiif wants to merge 11 commits into
rust-lang:mainfrom
tiif:rework-inference
Draft

WIP: Rework inference#409
tiif wants to merge 11 commits into
rust-lang:mainfrom
tiif:rework-inference

Conversation

@tiif

@tiif tiif commented Jun 29, 2026

Copy link
Copy Markdown
Member

What does this PR do?

Refactor how we handle substitution. Don't review it yet, it's still WIP, push this so it is easier to read and fetch.

AI disclosure

  • I did not use any AI tools

nikomatsakis and others added 4 commits June 18, 2026 09:04
@nikomatsakis
WIP:
a949715 
In the process of changing from Env=>Constraints
to Env=>Env.

Next steps -- change the "existential eq" to add
the substitution to the environment. Keep
the weird algorithm but let's discuss later.

Then propagate and fix compilation errors.

Then see what still works.
@tiif
Clean up
661e03b
@tiif
Leave one TODO to think about
f184cc2
@tiif
Clean up again
888a9e8
@tiif

tiif commented Jul 6, 2026

Copy link
Copy Markdown
Member Author

This is mostly ok, there are a few questions left:

  1. should we keep seq? I initially thought we no longer need seq as we always apply the substitution in prove, but there are some other places (zip and for_all) that still use seq in a way that couldn't be replaced with prove.
  2. I think we should update the variable field in Env when calling add_substitution? Do we have assumption such as every variable there is unique?

tiif
tiif commented Jul 6, 2026
View reviewed changes
Comment thread crates/formality-rust/src/prove/prove/prove/env.rs
Comment on lines +475 to +476
// TODO: tiif thinks we need to update the substitution here, but tiif might be wrong
substitution: vs.apply(&self.substitution()),

@tiif tiif Jul 6, 2026 •
edited by rustbot
Loading

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this correct?

View changes since the review

Comment thread crates/formality-rust/src/prove/prove/prove/prove_wc.rs
Comment on lines +100 to +102
(prove(decls, env, assumptions, Wcs::all_eq(&trait_ref.parameters, &i.trait_ref.parameters)) => env)
// TODO: check the correctness of this?
(prove(decls, env, assumptions, &i.where_clause) => env)

@tiif tiif Jul 6, 2026 •
edited by rustbot
Loading

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems weird to have two proves, but this is basically extracting the previous logic.

View changes since the review

@rustbot

rustbot commented Jul 21, 2026

Copy link
Copy Markdown
Collaborator

☔ The latest upstream changes (possibly #431) made this pull request unmergeable. Please resolve the merge conflicts.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

S-waiting-on-author

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@tiif @rustbot @nikomatsakis