Prototype callable lifetime dependencies

[enginespot]

What does this PR do?

I'm adding an a-mir-formality model for the callable lifetime dependencies discussed in rust-lang/rust#162745. The question is when a callable's complete input types determine its output type, including through equalities supplied by associated type declarations.

The compiler prototype enables the proposed behavior with -Znext-solver=globally. This PR expresses the underlying relationships as inference rules and executable cases in formality.

The motivating example

This function passes a value to a callback and returns the result:

trait Family {
    type View<'a>;
}

fn apply<'a, T, F>(f: F, value: T::View<'a>) -> T::View<'a>
where
    T: Family,
    F: for<'b> Fn(T::View<'b>) -> T::View<'b>,
{
    f(value)
}

This is the pattern from rust-lang/rust#107572. The existing check reports E0582 on the callback's output: 'b appears in the input only as an argument to an associated type, which does not establish that the input constrains it.

An associated type need not retain its lifetime argument. Both of these implementations are possible:

struct Borrowed;

impl Family for Borrowed {
    type View<'a> = &'a u32;
}

struct Erased;

impl Family for Erased {
    type View<'a> = ();
}

For Erased, knowing that View<'a> is () tells us nothing about 'a. In apply, however, the input and output always use the same complete type. For Borrowed, both are &'b u32; for Erased, both are (). If an implementation erases the lifetime from the input, it also erases it from the output.

How does it work, what questions do you have?

1. Input types must determine the output type

The proposed criterion fixes the outer type parameters and independently established bounds. For any two lifetime instantiations that satisfy the signature's requirements, equal input types must imply equal output types:

I('a) = I('b)  ⇒  O('a) = O('b)

The callable's proposed output equation is excluded from the assumptions, so the check cannot justify itself.

In the original example, I('a) and O('a) are both T::View<'a>, so the conclusion follows directly from the input equality. An output such as Option<T::View<'a>> is determined in the same way. Formality's existing equality rules already express this simplest case; the new declaration reasoning and obligation handling support the cases that need further derivation.

These output shapes need additional evidence:

Input	Output	Missing information
T::View<'a>	U::View<'a>	A relationship between the two families; T: Family, U: Family alone is insufficient
T::View<'a>	(T::View<'a>, &'a ())	A constraint on the lifetime of the additional reference

For the first row, choosing T = Erased and U = Borrowed gives a callback from () to &'a u32. Its inputs are equal at every lifetime, but that does not establish equality between the output reference types. issue_107572.rs checks these dependencies directly, without assuming the candidate callable's output equation.

2. Associated type declarations can supply the equality

Using the same Family trait, consider:

trait Identity {
    type Output: Family;
}

trait Carrier {
    type Assoc: Identity<Output = Self::Assoc>;
}

Given C: Carrier, T: Family, and C::Assoc = T, the declaration supplies this derivation:

C::Assoc: Identity<Output = C::Assoc>
C::Assoc = T
    ⇒ T: Identity<Output = T>
    ⇒ <<T as Identity>::Output as Family>::View<'a>
       = <T as Family>::View<'a>

The model now supports associated equality bounds and follows associated type and supertrait declarations to derive facts needed by the current goal. Nested equalities can compose while the types remain abstract. callable_signature_proofs.rs covers this derivation, its use in a function body, and a consumer in another crate.

3. Declaration bounds retain their prerequisites

This separate example uses formality syntax, where square brackets list the associated type's bounds:

trait Item { type Out: []; }
trait Lending<T> {
    type View<'a>: [Item::Out => &'a T] where T: 'a;
}

Each valid instance of View<'a> must implement Item with Out = &'a T. Using that guarantee requires both premises:

C: Lending<T>    T: 'a
    ⇒ <C as Lending<T>>::View<'a>: Item
    ⇒ <<C as Lending<T>>::View<'a> as Item>::Out = &'a T

C: Lending<T> alone cannot establish T: 'a. The implementation retains the item's where clause as a condition on each consequence. It also checks projections on both sides of the equality against their trait and associated item requirements, including whether the item exists and its arguments have the expected number and kinds.

4. Equality search preserves conditions and rejects circular justification

Normalization can advance either side of an equality. Each step carries its substitution and pending obligations. A visited state includes both types and their full constraints, so reaching the same types under a different condition preserves an alternative proof.

For example, one path might establish an equality subject to 'a: 'static, while another requires 'b: 'static. Either path can suffice. Combining them must not turn these alternatives into a requirement that both conditions hold.

The model's existing coinductive trait rules use provisional hypotheses to close trait cycles. A cycle through an associated equality needs a different treatment:

Prove Claim(())
    → requires <bool as Item>::Out = u32
    → the Item impl used to normalize Out requires Claim(())

I represent provisional trait hypotheses separately from established assumptions. Equality proofs and declaration reasoning cannot use those hypotheses to satisfy their own prerequisites. The existing rules for pure trait cycles remain available. A growing search path returns ambiguity when it reaches the model's size limit.

5. Lifetime obligations reach the checks that use the result

A declaration can also supply a relationship needed by borrow checking:

trait Has<'r> {
    type Assoc: 'r;
}

Given C: Has<'r> and C::Assoc = &'a (), the bound establishes 'a: 'r. A function body can therefore return that reference as &'r (). A model test checks that this derived relationship is available when checking the body.

When a proof leaves lifetime obligations pending, substitutions must apply to those obligations as well as to the resulting type. Leaving a binder must also preserve the relationships between its variables. For example:

{ 'a: ?x, ?x: 'b }
    ⇒ exists<'x> { 'a: 'x, 'x: 'b }

Both conditions share the same witness for 'x. Similarly, in for<'a> exists<'x>, the witness may depend on the current 'a; reversing the quantifier order changes the requirement. These obligations remain pending after their variables are bound.

Scope and open questions

This PR and the compiler prototype address the same examples. The model checks the type equalities, declaration prerequisites, and lifetime relationships on which the compiler changes rely. Cases involving function item matching, function pointers, and trait objects are expressed through their quantified signature obligations; they do not reproduce rustc's conversion machinery.

I've run the workspace tests and formatting checks locally. The tests cover successful derivations and counterexamples involving missing premises, escaping lifetimes, attempts to recover projection arguments, and circular justification. This is not a general soundness proof or a proof that the model and rustc implementation agree. The cyclic normalization and rigid alias consistency issues recorded in #162745 still need to be addressed in the compiler.

The changes affect shared equality and lifetime rules, so they can change the conclusions available elsewhere in the model and the reported failure traces. Declaration traversal and equality search with pending conditions also add solver work. The search tracks visited states and applies a term size limit, but I have not completed a systematic comparison of execution time and memory use.

The borrow-checking consumer still rejects quantified pending obligations it cannot handle. It also requires the candidates to agree on the output and to include a candidate whose conditions follow from each of the others under the established assumptions. Preserving alternative proofs in the solver therefore does not make every such result usable by borrow checking.

I'd like feedback on whether equality of complete inputs is the right criterion for output dependency, whether the declaration prerequisites and treatment of recursion are sufficient, and how subsequent checks should consume results that still carry conditions. That review would also help assess the design of the compiler prototype.

AI disclosure

• I used an AI to author the main logic of the code

[rustbot]

Thanks for contributing to formality! :)
A reviewer will take a look at your PR within a week or two. If not, come talk to us on https://rust-lang.zulipchat.com/#narrow/channel/402470-t-types.2Fformality

[tiif]

This PR contains a lot of changes without prior discussion with the team. Since this is part of an experimental work related to types team, I think it is reasonable to expect this PR will move forward only if types team wants to model this in formality or someone in formality team is up for reviewing this.