Fix struct_with_invariants generic param detection for associated type prefixes

[rikosellic]

This PR fixes a bug in struct_with_invariants! where generic type parameters are used only as an associated type prefix.

Input

trait HasTarget {
    type Target;
}

struct_with_invariants!{
    pub struct S<A: HasTarget>  {
        a: AtomicBool<_,(),_>,
        _phantom: PhantomData<*const A::Target>,
    }

    closed spec fn wf(self) -> bool {
        invariant on a with (_phantom) is (v:bool,g:()) {
            true
        }
    }
}

Output

It fails to compile with this error (playground link):

error[[E0433]](https://doc.rust-lang.org/stable/error_codes/E0433.html): cannot find type `A` in this scope
  --> /playground/src/main.rs:14:38
   |
14 |         _phantom: PhantomData<*const A::Target>,
   |                                      ^ use of undeclared type `A`

error: aborting due to 1 previous error

Fix

The fix updates the generic-usage collector in struct_decl_inv.rs so it also recognizes the first segment of multi-segment type paths. A regression test is also added.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[rikosellic]

It turns out the current implementation doesn't carry enough type-bound information through the macro expansion. The generated field-type aliases and InvariantPredicate_auto_* structs now carry the relevant generic params along with their bounds, using PhantomData to anchor params that would otherwise appear only inside associated-type projections.

[rikosellic]

The doc build error seems irrelevant.