assert-by-compute fails to substitute type arguments

[tjhance]

Usually this results in invalid AIR. See for example this test, which I attempted to add as part of #1406:

test_verify_one_file! {
    #[ignore] #[test] default_impl_1_issue1406 verus_code! {
        trait Tr {
            spec fn foo(&self) -> bool { true }
        }

        struct X { }

        impl Tr for X {
            spec fn foo(&self) -> bool { false }
        }

        spec fn foo_wrapper<T: Tr>(t: &T) -> bool {
            t.foo()
        }

        proof fn test2() {
            let x = X { };
            assert(foo_wrapper(&x)) by(compute); // FAILS
        }
    } => Err(err) => assert_fails(err, 1)
}

This test is ignored because it currently panics.

This can also be a soundness error, when type parameters have overlapping names. This shouldn't pass, but it does:

trait Tr {
    spec fn foo() -> bool;
}

spec fn hello<A: Tr, B: Tr>() -> bool {
    A::foo()
}

proof fn test<A: Tr, B: Tr>()
    requires A::foo(),
{
    assert(hello::<B, A>()) by(compute);
    assert(B::foo());
}