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

Better Normalization Needed #737

Open
ranjitjhala opened this issue Aug 21, 2024 · 2 comments
Open

Better Normalization Needed #737

ranjitjhala opened this issue Aug 21, 2024 · 2 comments
Labels
enhancement New feature or request normalization Issue related to normalization of associated types unsoundness

Comments

@ranjitjhala
Copy link
Contributor

Related to #701 and #734

Currently we hack around flux's limited normalization (cf. issues above) by falling back to rustc -- see normalize_projection_ty_with_rustc. However, the real issue here is that the flux param_env doesn't
contain all the clauses, e.g. those implied by super-traits.

The current method, @nilehmann notes is

I think the PR is unsound because it forgets refinements in the obligation, which is mostly fine unless you are dealing with invariant type constructors. We could either grab the candidates from rustc and then confirm them which would preserve refinements or only apply the hack when the obligation is unrefined. That'd be less unsound

The correct method @nilehmann suggests is to reimplement, in flux, the rustc code that builds the param_env. The extra predicates are added in the call to this function in particular they come from a call to this

/// "Elaboration" is the process of identifying all the predicates that
/// are implied by a source predicate. Currently, this basically means
/// walking the "supertraits" and other similar assumptions. For example,
/// if we know that `T: Ord`, the elaborator would deduce that `T: PartialOrd`
/// holds as well. Similarly, if we have `trait Foo: 'static`, and we know that
/// `T: Foo`, then we know that `T: 'static`.

Opening this issue so we can do this properly.

@ranjitjhala ranjitjhala added enhancement New feature or request unsoundness labels Aug 21, 2024
@nilehmann nilehmann added the normalization Issue related to normalization of associated types label Aug 23, 2024
@ranjitjhala
Copy link
Contributor Author

@nilehmann -- is this still open?

@nilehmann
Copy link
Member

Yes still open

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request normalization Issue related to normalization of associated types unsoundness
Projects
None yet
Development

No branches or pull requests

2 participants