Struct lt wf

[BennoLossin]

(depends on #344)

What does this PR do?

@_Benno Lossin|458499 said:

@nikomatsakis I tried to make it work, but the following test already doesn't work:

#[test]
fn missing_constraint() {
    crate::assert_err!(
        [
            crate test {
                struct Foo<'a> {
                    y: &'a u32,
                }

                fn foo() -> () {
                    exists<'y> {
                        let a: u32 = 22 _ u32;
                        let f: Foo<'y> = Foo { y: &'y a };
                    }
                }
            }
        ]
        expect_test::expect![[r#"
            crates/formality-rust/src/prove/prove/prove/prove_via.rs:9:1: no applicable rules for prove_via { goal: @ wf(Foo<?lt_0>), via: @ wf(?lt_0), assumptions: {@ wf(?lt_0)}, env: Env { variables: [?lt_0], bias: Soundness, pending: [], allow_pending_outlives: true } }

            crates/formality-rust/src/prove/prove/prove/prove_wf.rs:14:1: no applicable rules for prove_wf { goal: ?lt_0, assumptions: {@ wf(?lt_0)}, env: Env { variables: [?lt_0], bias: Soundness, pending: [], allow_pending_outlives: true } }"#]]
    )
}

This seems wrong?

Xiang and I looked into this a bit in our meeting today and we think that we actually found the issue:

prove_wf doesn't have a rule to prove wf via assumption and it is directly called from itself (when checking wf of parameters for example), so any assumption proving logic in prove_wc doesn't get used.

There are two solutions:

• call prove_wc or prove from prove_wf instead of directly recursing,
• add a via-assumption rule to prove_wf

I have implemented the latter one (since I thought it would be less overall churn) to see what other things break/change. There are some test output changes and I'll send a PR.

From an overall design perspective, I think we should either handle assumptions once at the very top in prove. Or each prove_* function should do it themselves.

Disclosure questions

AI disclosure.

No ai used.

Confidence level.

• It seems reasonable to me, I'd like to know what others think

[rustbot]

Thanks for contributing to formality! :)
A reviewer will take a look at your PR within a week or two. If not, come talk to us on https://rust-lang.zulipchat.com/#narrow/channel/402470-t-types.2Fformality

[BennoLossin]

I totally forgot about this PR...

@nikomatsakis I updated the implementation as well, instead of having an by-assumption rule in prove_wf, instead it now recurses into prove, which handles assumptions.