external_trait_specification: consistency check causes panic

[BLepers]

Commit e4c33bf

The following code:

use vstd::prelude::*;

pub trait ForeignOwnable: Sized {
    type Borrowed<'a>;
}

verus!{

#[verifier(external_trait_specification)]
pub trait ExForeignOwnable: Sized {
    type ExternalTraitSpecificationFor: ForeignOwnable;
    type Borrowed<'a>; // Problem comes from this line
}

fn main() {
}
}

Produces the following error:

error: internal compiler error: compiler/rustc_middle/src/ty/generic_args.rs:806:13: Region parameter out of range when substituting in region 'a (index=1, args = [Alias(Projection, AliasTy { args: [Self/#0], def_id: DefId(0:8 ~ test7[2c30]::ExForeignOwnable::ExternalTraitSpecificationFor) })])

thread 'rustc' panicked at /rustc/07dca489ac2d933c78d3c5158e3f43beefeb02ce/compiler/rustc_errors/src/lib.rs:1119:75:
Box<dyn Any>
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: aborting due to 1 previous error

I may have misunderstood the external_trait_specification interface?

[tjhance]

@Chris-Hawblitzel

Code that causes the panic is here (rust_to_vir_trait.rs):

                if let Some(ex_trait_ref_for) = ex_trait_ref_for {
                    let ex_item_id_for = ex_item_id_for.expect("ex_item_id_for");
                    let external_predicates = tcx.item_bounds(ex_item_id_for);
                    let proxy_predicates = tcx.item_bounds(owner_id.to_def_id());
                    let preds1 = external_predicates.instantiate(tcx, ex_trait_ref_for.args); // panic here
                    let preds2 = proxy_predicates.instantiate(tcx, ex_trait_ref_for.args);
                    // TODO, but low priority, since this is just a check for trusted declarations:
                    // crate::rust_to_vir_func::predicates_match(tcx, true, &preds1.iter().collect(), &preds2.iter().collect())?;
                    // (would need to fix up the TyKind::Alias projections inside the clauses)

                    if preds1.len() != preds2.len() {
                        return err_span(
                            trait_span,
                            format!(
                                "Mismatched bounds on associated type\n{:?}\n vs.\n{:?}",
                                preds1, preds2
                            ),  
                        );  
                    }   
                } 

Naturally, the external_predicates have an 'a param which isn't in the ex_trait_ref_for.args

We could be lazy and just comment out the check, under the same reasoning in the comment, that external_trait_specification is trusted ...