mode-checking for struct patterns mismatches fields

[tjhance]

This wrongly passes mode-checking (it actually fails due to an unrelated erasure error, but this issue isn't about that):

struct Foo {
    #[spec] a: u64,
    #[proof] b: u64,
}

#[proof]
fn some_call(#[spec] x: u64, #[proof] y: u64) { }

#[proof]
fn t() {
    #[proof] let foo = Foo { a: 5, b: 6 };
    #[proof] let Foo { b, a } = foo;

    some_call(b, a);
}

Meanwhile, this wrongly gives an error:

#[proof]
fn t() {
    #[proof] let foo = Foo { a: 5, b: 6 };
    #[proof] let Foo { b, a } = foo;

    some_call(a, b);
}

error: expression has mode spec, expected mode proof
  --> test_pat_destruct.rs:26:18
   |
26 |     some_call(a, b);
   |                  ^

It looks like mode-checking doesn't handle let Foo { b, a } correctly because the order of its fields are wrong.

[tjhance]

fixed by 9eb7b12