flux-rs / flux

Refinement Types for Rust
MIT License
637 stars 17 forks source link

Better Normalization Needed #737

Open ranjitjhala opened 3 weeks ago

ranjitjhala commented 3 weeks ago

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 commented 1 week ago

@nilehmann -- is this still open?

nilehmann commented 1 week ago

Yes still open