Lifetime polymorphism brainstorm

Lifetime polymorphism. What do I do?

There are few interwoven issues:

• Do we want lifetimes to be partially ordered or totally ordered?
• We want &'a T to be coercible to &'b T if we know that 'a <: 'b (i.e. 'b' is strictly shorter than 'a).
• We want to express something very similar to stack polymorphism.

The typing of a function is effectively a promise, that:

I (here meaning the function in question) can be called with any stack S, as long as P(S) holds, though this predicate only looks at a small subset of the stack. I might change this subset (push/pop values), but I will not change the rest of the stack. By using forall instantiation, you can give me a continuation that can depend on the rest of the stack, even though I cannot. This continuation can also depend on any changes I have made.

By changing that phrasing slightly, we arrive at what we would like our lifetime polymorphism to achieve:

I (here meaning the function in question) can be called with any lifetime graph L, as long as P(L) holds, though this preducate only looks at a small subset of the graph. I might change this subset (add/remove lifetimes), but I will not change the rest of the graph. By using forall instantiation, you can give me a continuation that can depend on the rest of the graph, even though I cannot. This continuation can also depend on any changes I have made.

Here we run into an issue: With stack polymorphism we could express P(S) as the front S looks like this, while we cannot do this for P(G). In fact no matter who we represent G, we might depend on lifetimes present in the middle of G.