Variable dependent types?

Not necessarily. It may be desirable to borrow in some case (or even possibly to move a) but it does not have to be either mandatory or even the default case. The minimal semantics are just that u and v are somehow related to a. More specifically u and v may be used together as parameters of certain functions only because their types match (=i.e. they are related to the same a). This naturally implies that:

  • a must be specified when u and v are created ;
  • neither u nor v can outlive a.

But that does not mean that the value of a needs to be used anywhere in functions that consumes items of types Foo<a>. And even when such value is actually needed, the borrow can perfectly start when the function is called, not when u is created. Certainly a dedicated syntax would be necessary to specify which behavior is intended.

Let's imagine something like this (the syntax proposed here is cumbersome and ugly, but let's agree this is not the point):

// a is not used anywhere inside bar_tag
fn bar_tag<let a: MyContext>(u: &Foo<a>, v: &Foo<a>) { … }
// a is borrowed when calling bar_ref
fn bar_ref<let ref a: MyContext>(u: &Foo<a>, v: &Foo<a>) { … }
// a is mutably borrowed when calling bar_ref
fn bar_mut<let mut ref a: MyContext>(u: &Foo<a>, v: &Foo<a>) { … }

…

let a : MyContext = …
let u = Foo::<a>::new( … );
let v = Foo::<a>::new( … );

// a is not borrowed when we reach this point
bar_tag(u, v); // u and v are borrowed at this point but a is not impacted
bar_ref(u, v); // a is immutably borrowed here
// ... and released here
bar_mut(u, v); // ... and reborrowed mutably here
// but neither u not v can outlive a

An interesting aspect is that u and v do not necessarily have to carry any internal reference to a (that would require a to be locked). However they do represent data that may only be interpreted in the light of a (sometimes the actual value of a is required, sometimes we just need to know that it is the same a, independently of its actual value). Of course you may also want to borrow a from the start (when u or v are created) but this can be handled independently by lifetimes.

That may work indeed, although it requires that token() copies some information.