Converting "&'a &'b T" to "&'a T" in the presence of non-lexical lifetimes can be unsound

[exists-forall]

The following snippet should be rejected for allowing a value to be mutated while it is borrowed, but it is accepted on nightly when non-lexical lifetimes are enabled (playground):

#![feature(nll)]

fn flatten<'a, 'b, T>(x: &'a &'b T) -> &'a T {
    x
}

fn main() {
    let mut x = "original";
    let y = &x;
    let z = &y;
    let w = flatten(z);
    x = "modified";
    println!("{}", w); // prints "modified"
}

[pnkfelix]

(assigning to @nikomatsakis to write up mentoring instructions, or potentially fix outright)

[nikomatsakis]

I discussed the problem with @spastorino in gitter the other day:

https://gitter.im/rust-impl-period/WG-compiler-nll?at=5ace0ee101a2b40f382ead12

[nikomatsakis]

As I pointed out in gitter, this is the point where we instantiate the late-bound regions in the signature:

rust/src/librustc_mir/borrow_check/nll/type_check/mod.rs

Lines 890 to 895 in ca26ef3

	let (sig, map) = self.infcx.replace_late_bound_regions_with_fresh_var(
	term.source_info.span,
	LateBoundRegionConversionTime::FnCall,
	&sig,
	);
	let sig = self.normalize(&sig, term_location);

That variable sig will be a FnSig. Much like the AST-based type checker code, we need to iterate through the inputs and prove their types are well-formed. I imagine something like:

self.prove_predicates(
  sig.inputs().iter().map(|ty| ty::PredicateWellFormed(ty))
);