Check impl-methods are subtypes of trait-methods

flux-rs / flux

Refinement Types for Rust

MIT License

660 stars 21 forks source link

Check impl-methods are subtypes of trait-methods #864

Closed ranjitjhala closed 4 weeks ago

ranjitjhala commented 1 month ago

Fixes #592

ranjitjhala commented 4 weeks ago

Matching PR https://github.com/PLSysSec/tock/pull/4/files

ranjitjhala commented 4 weeks ago

By "outside" Checker do you mean it should be at the "level" of fn check_fn in flux-refineck/src/lib.rs?

ranjitjhala commented 4 weeks ago

or at the level of fn run_in_refine_mode?

nilehmann commented 4 weeks ago

I think this should be part of flux_fhir_analysis::compare_impl_item::check_impl_against_trait, but that would require reshuffling things across crates. Putting it in flux_refineck::check_fn would be a good start though.

ranjitjhala commented 4 weeks ago

AFAICT InferCtxt can only be initialized with a Body and so you can't initialize it in the context of a trait-method (which may not have a Body?)

ranjitjhala commented 4 weeks ago

@nilehmann I have done the refactoring, so the impl-trait check lives in

pub fn trait_impl_subtyping (currently in checker.rs) but independent of the Checker itself and
invoked as PHASE 4 in check_fn

See esp. the new args passed into RefineTree::new and the subsequent .instantiate(...)

ranjitjhala commented 4 weeks ago

ok, I'll merge if everything -- IF I get the damn tock thing to pass locally.

ranjitjhala commented 4 weeks ago

merging!