# 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

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

struct Type<const C: u32> { }

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

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.

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
}

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

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
}

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

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`