---
tags: weekly-meeting
---

# 2023-05-15 meeting - opaque types meeting

## goals

Agree on a path forward towards TAIT stabilization and on how to implement opaque types in the new solver. For this I want a shared understanding of both the status quo and a common mental model of how TAIT works in the trait solver.

## no, eager, and lazy normalization

We tend to group a lot of things into "lazy norm". For this context I going to use the following perspective:

Given an alias `Foo<T, U>` which can be normalized to `Vec<T>`,

- no normalization means that we only to observe `Foo<T, U>`, without having access to the normalized type,
- eager normalization means that we are only able to observe `Vec<T>`, without any knowledge that we got this type from normalizing `Foo<T, U>`,
- and lazy normalization means that we are able to observe a type as both `Foo<T, U>` and `Vec<T>` at the same time.

By eagerly normalizing we lose information about `Foo<T, U>`. Lazy normalization should ideally be strictly more powerful than eager normalization.

## how the current implementation handles opaque types

This is significantly simplified, but should hopefully be enough as guidance for the rest of this writeup.

### opaque types outside of the defining scope

Opaque types which are not defined by the current context are not normalized and we interact with the opaque itself without looking at its hidden type.

An exception here is "auto trait leakage". To check `impl Trait: AutoTrait` bounds we normalize[^1] opaque types to check which auto traits they implement.

We currently also sometimes lazily normalize them when using `DefiningAnchor::Bubble` which then later results in errors, more on that later.

### opaque types in the defining scope

We are inside of the defining scope of all opaque types defined by `def_id` if we're inside of an inference context with [`DefiningAnchor::Bind(def_id)`](https://doc.rust-lang.org/nightly/nightly-rustc/rustc_infer/infer/enum.DefiningAnchor.html).

We mostly use lazy normalization for opaque types in the defining scope, most notably [relating opaques] is fully lazy when using `DefineOpaqueTypes::Yes` (more on that later). This is done by using [`handle_opaque_type`].

There is also some code which does no normalization itself. This is the case whenever we relate with `DefineOpaqueTypes::No`. We also currently do not lazily normalize during candidate assembly. This means that `impl Trait: OtherTrait` never holds even if we could prove it by first normalizing `impl Trait`. This forces us to eagerly normalize in some places by using [`replace_opaque_types_with_inference_vars`].

### `DefiningAnchor::Bubble`

Whether or not we use `DefineOpaqueTypes::No` when relating types is somewhat arbitrary. The main reason for `DefineOpaqueTypes::No` is `DefiningAnchor::Bubble`. Mostly added as it is necessary for cross-function caching with canonical queries. With `DefiningAnchor::Bubble` we treat all opaque types as if they are in the defining scope and then check whether any opaques have been incorrectly constrained in the caller.

Because treating all opaque types as in the defining scope would cause us to frequently incorrectly normalize, we disable some normalization with `DefineOpaqueTypes::Bubble`. Most notably [`replace_opaque_types_with_inference_vars`] is a noop. Because of this we mostly use `DefineOpaqueTypes::No` in the trait solver to prevent ourselves from incorrectly constraining any opaque types in canonical queries.

## issues with the status quo

The behavior wrt to opaque types differs between different parts of rustc due to a lot of factors. This generally makes it very hard to understand what's going on and results in subtle bugs where different parts of the code expect equivalent behavior but have differences due to either `DefineOpaqueTypes` or `DefiningAnchor`. These differences also make it hard to support in the new solver which tries to unify multiple code paths and wants to be able to cache as efficiently as possible.

TODO: write an example where MIR typeck ICEs because of this difference.

There are also some snippets which are very difficult to support with the current system, e.g.

use std::fmt::Debug;
fn foo() -> impl Debug {
    if false {
        let mut x = foo();
        x = std::iter::empty().collect();
        // `impl Debug: FromIterator<_>` currently fails because
        // we don't normalize opaque types in the trait solver.
    }
    vec![""]
}

## where to go from here

*This approach currently has a WIP implementation in [#111473].*

I think most of the complexity here is caused by us not relying on lazy normalization everywhere.

To always rely on lazy normalization we have to get rid of `DefiningAnchor::Bubble` and fully track the defining scope and the currently inferred hidden values everywhere. There's a separate later section on how to do so efficiently.

Because we don't incorrectly constrain the hidden type if we know the defining anchor, we can then remove `DefineOpaqueTypes`, always using the `Yes` path. Candidate selection inside of the trait solver is changed to assemble candidates for both the opaque type itself and its hidden type. In the new solver this is equivalent to the behavior for projections. With this the trait solver is fully lazy. We may need some eager normalization for hir typeck itself, e.g. for coercions, but that should only result in fairly localized complexity.

#### handling opaque types between hir typeck and `Reveal::All`

There is a bunch of code which happens on the typechecked HIR and uses `Reveal::UserFacing`, e.g. diagnostics, the MIR validator, and the actual WF check for opaque types.

This code tends to assume that the HIR (or the built MIR) is well formed, which is only the case when using the same hidden types. This is currently handled by using `DefiningAnchor::Bind` or `DefiningAnchor::Bubble` and [dropping the inferred hidden types](https://github.com/rust-lang/rust/blob/8006510ab0f69ee75e9c3f7e8bff3776886dae51/compiler/rustc_hir_analysis/src/check/check.rs#L469). This hides compiler bugs or unsound code.

TODO try to write a test which shows that `check_opaque_meets_bounds` is insufficient.

What we should instead do is to put the inferred hidden types collected during HIR typeck into the `TypeckResults` and then use them whenever we're "inside of the body" until we are able to use `Reveal::All`.

#### efficiently tracking the defining scope

If we correctly track the current `DefiningAnchor::Bind` in the query key then each function will end up with completely separate cache results.

A first step here is to change this to instead store a list of all opaque types defined by the anchor instead of the anchor itself. This will allow functions which define the same opaque types - mostly all functions which don't define any opaque type - to share cache results.

Longterm I expect us to lazily provide the defined opaque types to canonical queries. This will be very similar to more general approach for predicates in the `param_env` described in [this separate doc](https://hackmd.io/5IdqPjpCQ5-19GWTBnDdyA).

## summary of lcnr thoughts here

At the time of requesting this deep-dive my best idea relied on having an explicit list all instantiation of opaque types which may be defined by the current function. This would have restricted the design space for TAIT and was somewhat ugly.

The approach in [#111473] feels conceptionally clean to me without putting any meaningful restrictions on the design of TAIT. It nearly completely unifies the handling of opaque types and projections in the solver. The only difference is how they are actually normalized. I expect this approach to not have any significant performance cost once finished.
Supporting this approach in the new trait solver is pretty nice: the trait solver changes in [#111473] are already pretty much done.

Implementing this in the old solver may however be difficult. There are some parts which are fairly easy, like changing the defining anchor from the `DefId` of the current function to a list of opaque types. Changing the trait solver to always use lazy normalization for opaque types may prove to be hard, if not impossible.

It is especially difficult as the old solver is already relevant for performance. While we can incrementally work towards a performant implementation with good caching in the new solver, that is the only implementation we can probably land in the old one.

[relating opaques]: https://github.com/rust-lang/rust/blob/ea0c22ea4f58f181d6739fbe624329e576ce7994/compiler/rustc_infer/src/infer/equate.rs#L98-L120
[`handle_opaque_type`]: https://github.com/rust-lang/rust/blob/ea0c22ea4f58f181d6739fbe624329e576ce7994/compiler/rustc_infer/src/infer/opaque_types.rs#L90-L97
[`register_hidden_type`]: https://github.com/rust-lang/rust/blob/ea0c22ea4f58f181d6739fbe624329e576ce7994/compiler/rustc_infer/src/infer/opaque_types.rs#L511-L519
[`replace_opaque_types_with_inference_vars`]: https://github.com/rust-lang/rust/blob/ea0c22ea4f58f181d6739fbe624329e576ce7994/compiler/rustc_infer/src/infer/opaque_types.rs#L44C12-L50
[#111473]: https://github.com/rust-lang/rust/pull/111473

[^1]: this currently does not use actual normalization but instead directly uses `type_of`.

## Thoughts, questions

### How do I leave a question?

ferris: How do I leave a question?

Like this! Make a new section, summarize, and then give details

### "Strictly" more powerful?

nikomatsakis: The document says...

> Lazy normalization should ideally be strictly more powerful than eager normalization.

...I agree that lazy normalization can be more powerful, but I think that our goal should be to retain "choice" about when we normalize without loss of expressiveness. I think this sentence is talking about the example of (say) `T: Iterator<Item = U>`, from which one could derive that `U: Sized`, even if you don't know it otherwise. It's true then that `T::Item` is clearly sized while `U` is not, but I think that we should account for that more as a side effect of having `T: Iterator<Item = U>` in the environment -- i.e., it lets us conclude things about `U` we wouldn't be able to do otherwise.

lcnr: I am not sure how to get the power of lazy norm when eagerly normalizing during type inference :thinking_face: at least with the definition of this doc it feels unavoidable that lazy norm is more expressive than eager norm.

### "lazy normalization means ... both ... at the same time"

jack: This is not quite correct. The lazy norm that we mostly talk about today is we can observe *either* the normalized or unnormalized form. Once we've normalized today, we still lose info about the unnormalized type. My recent Chalk experiments are actually geared around precisely this, though.

lcnr: a bit pedantic ^^ but yeah, that's correct

### Who is responsible for computing hidden types

nikomatsakis: The document says

> What we should instead do is to put the inferred hidden types collected during HIR typeck into the `TypeckResults` and then use them whenever we're "inside of the body" until we are able to use `Reveal::All`.

To check my understanding, this would be a shift from the current model, where the borrow check is responsible for computing the hidden types during HIR type check, correct? How will we manage the need to compute region values that appear in the hidden type?

@lcnr: The idea is to prepopulate the hidden opaque types map of MIR typeck with the opaque type constraints from hir typeck with fresh region vars. These fresh region vars then get constrained by MIR typeck in the same way we already do now. This should remove the need to have special handling for opaque types in dead code. We currently already check the that the hidden types computed by hir typeck are equal to the result of mir typeck, so that shouldn't add any new restriction i think.

### Impl trait in let binding position

nikomatsakis: I'm adding a placeholder question to discuss potential interactions with

let something: impl IntoIterator<Item = u32> = vec![];

What implications would this have for the behavior of `something` here and are we happy about it? There is some interaction with lang team here, but my personal take is that types team can and should push back on the proposed language semantics if they can't be cleanly modeled. (And lang team can and should push back if we are letting our attachment to a clean model get in the way of user experience.)