---
# System prepended metadata

title: Types team EOY meeting notes

---

# Types team EOY meeting notes

* New trait solver
* Polonius goal
* Min generic const args from Boxy
* Niko plans to create: a-mir-formality and coherence

## Relationship of Spec to Types team

* For now pretty far away from types team but it will get closer
* My current thinking is that the starting point would be
    * invariants are encoded in spec
    * a-mir-formality is a stronger definition for "how it works"

## Formality strategy

* We should really get it to the point where we can run Rust tests
    * Need to handle std
    * Just focused on impls, std
    * Can we use stable MIR?

## Min generic const args

* prev approach: arbitrary expressions
    * didn't work out, determining if exprs are eq is hard (NP)
    * typecking exprs causes cycles everywhere
* plan:
    * just allow assoc consts and generic const items
        * `T::CONST`
        * `const FOO<T: ...> = `
    * easier lowering
    * clear rules about evaluation order and typeck order and stuff
* what about `const fn` ?
    * restricting to const items means we can check at the def'n site that arguments are good
    * maybe can't use arbitrary items but have to mark them specifically to make them some kind of "alias"
* one challenge:
    * with const fn, post monomorphization errors when are instantiated

```rust
const FOO: u32 = 2 + 2;
const BAR: u32 = 3 + 1;

struct Type<const C: u32> { }

fn main() {
    let x: Type<FOO> = Type::<BAR> {}; // ??
}
```

```rust
const FOO: u32 = 2 + 2;
const ADD_ONE<C: u32>: u32 = C + 1;
    // this might require some annotation

struct Type<const C: u32> { }

fn foo<const N: usize>() {
    let x: Type<FOO> = Type::<ADD_ONE<3>> {}; // pass
    let x: Type<FOO> = Type::<ADD_ONE<N>> {}; // fail
}
```

you'd have to declare `type` (need new keyword =) `const`, in which case RHS must also be "evaluatable", so e.g.

```rust!
type const ADD_ONE<C: u32> = C + 1; // error
const ADD_ONE<C: u32> = C; // OK

trait AddOne {
    type const OUTPUT: u32;
}

struct MyType<const C: u32> { }
impl<const C: u32> AddOne for MyType<C> {
    type const OUTPUT = C + 1; // ERROR
}

struct MyOtherType<const C: u32> { }
impl<const C: u32> AddOne for MyOtherType<C> {
    type const OUTPUT = C; // OK
}
```

```rust
const fn foo<const N: usize>() {
    let _: [u32; N - 1];
    //         ----- error today!
}

fn main() {
    foo::<0>(); // else, this would error during codegen, but not cargo check
}
```

post-mono-error today

```rust
trait Trait {
    const ASSOC: usize;
}
impl<const N: usize> Trait for [u8; N] {
    const ASSOC: usize = N - 1;
}

fn foo<const N: usize>() -> usize {
    <[u8; N] as Trait>::ASSOC // post mono error
}
```

```rust
const fn evaluate<const N: u32>() -> u32 {
    N - 1
}
```

https://blog.rust-lang.org/2024/06/26/types-team-update.html#roadmap


* next-generation trait solver
    * stable in coherence (3rd of Jan)
    * used by rust-analyzer <-- Jack is working on this but it won't happen by end of year
* ATPIT stabilized <-- nope but we did try awfully
* a-mir-formality <-- nope but it has a fuzzer
    * support for fuzzing and testing Rust snippets
    * complete model of coherence and coinductive trait semantics
* full polonius implementation available on nightly <-- nope but we are making progress
    * Amanda landed higher-ranked check refactoring
        * now working on next step
            * https://github.com/rust-lang/rust/pull/130227
    * lqd has on a branch a "native" impl of polonius
        * all but 16 tests 


```rust
for<'b> 'a: 'b --> 'a: 'static
```

## trait solver stuff

* trait solver stable in coherence
    * API has been extracted and it lives in a self-standing crate
* rust-analyzer integration happening, still exploratory
    * what to do with inference context?
    * https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/trait.InferCtxtLike.html

## trait upcasting

## onboarding

## pattern types

`Type is Pattern`



