NLL doesn't check user type annotations are well-formed

[matthewjasper]

For example, this code is accepted with NLL enabled:

rust/src/test/ui/regions/regions-free-region-ordering-caller.rs

Lines 19 to 30 in f1694ea

	fn call2<'a, 'b>(a: &'a usize, b: &'b usize) {
	let z: Option<&'b &'a usize> = None;//~ ERROR E0623
	}
	fn call3<'a, 'b>(a: &'a usize, b: &'b usize) {
	let y: Paramd<'a> = Paramd { x: a };
	let z: Option<&'b Paramd<'a>> = None;//~ ERROR E0623
	}
	fn call4<'a, 'b>(a: &'a usize, b: &'b usize) {
	let z: Option<&'a &'b usize> = None;//~ ERROR E0623
	}

cc #47184

[nikomatsakis]

(Related: #54105)

I imagine that the way to fix this is that we have to prove a WellFormed predicate with-respect-to the user-given type annotations:

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

Lines 1284 to 1288 in 1c5e9c6

	self.prove_predicates(
	sig.inputs().iter().map(|ty| ty::Predicate::WellFormed(ty)),
	term_location.to_locations(),
	ConstraintCategory::Boring,
	);

Probably the place to do this is on the relate_type_and_user_type function:

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

Lines 946 to 953 in 1c5e9c6

	fn relate_type_and_user_type(
	&mut self,
	a: Ty<'tcx>,
	v: ty::Variance,
	b: CanonicalTy<'tcx>,
	locations: Locations,
	category: ConstraintCategory,
	) -> Fallible<()> {

One complication, though, is that the user-given type is a "canonical type":

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

Line 950 in 1c5e9c6

b: CanonicalTy<'tcx>,

which means that it might have _ and things encoded in it. However, the relate_type_and_user_type fn already creates type variables representing each of those _ and things. Right now it just stores them into a vector:

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

Lines 128 to 139 in 1c5e9c6

	/// As we execute, the type on the LHS *may* come from a canonical
	/// source. In that case, we will sometimes find a constraint like
	/// `?0 = B`, where `B` is a type from the RHS. The first time we
	/// find that, we simply record `B` (and the list of scopes that
	/// tells us how to *interpret* `B`). The next time we encounter
	/// `?0`, then, we can read this value out and use it.
	///
	/// One problem: these variables may be in some other universe,
	/// how can we enforce that? I guess I could add some kind of
	/// "minimum universe constraint" that we can feed to the NLL checker.
	/// --> also, we know this doesn't happen
	canonical_var_values: IndexVec<CanonicalVar, Option<Kind<'tcx>>>,

I guess what we would need to do is -- after equating, relating, whatever -- to instantiate the canonical type with these final values (presumably using the substitute function), and then create the WellFormed predicate.

[blitzerr]

The issue is that this code compiles and executes file with NLL enabled as you can see here. But with NLL turned off, it errors out as here.
This RFC (unrelated) but helps defined what wellFormed types are.