owned this note
owned this note
Published
Linked with GitHub
# lcnr nikomatsakis
## 2025-09-18
- think types team stuff
- foundation what does lcnr want
- council to decide priorities for long term project health
- no full time pay :<
## 2025-04-16
### Opaque stuff is "done"
* "Perfectly" works
* Absolutely horrible
* https://github.com/rust-lang/rust/pull/139587
* checking the closures together with the parent
* separately: collect all region constraints
* together: handle opaques
* separately: regionck + borrowck
### Dyn trait dispatch and async functions
```rust
trait Observe {
async fn changed(&mut self);
}
struct Signal {
on_change: Vec<Box<dyn Observe>>
}
impl Signal {
async fn signal_change(&mut self) {
for o in &mut self.on_change {
o.changed().await;
}
}
}
```
* support `dyn Trait` type for any trait
* if the trait is dyn-safe, then `dyn Trait: Trait` (niko would like to revise in future editions)
* extension: (and with any subset of associating type bindings)
* `dyn Trait` has inherent members for
* dyn-safe methods
* async fn methods
* you can generalize this to `-> impl Trait`
* for async fn methods:
* `fn changed(&mut self) -> dyn Future<Output = ()>`
* unsized return value!
* can't call it directly
* some intrinsic or other ways to call it where you provide the "emplacement" function
* syntax-wise:
* we support a `.box` operator that, when used in this place, does the thing it should do
```rust
trait Observe {
async fn changed(&mut self);
}
struct Signal {
on_change: Vec<Box<dyn Observe>>
}
impl Signal {
async fn signal_change(&mut self) {
for o in &mut self.on_change {
o.changed().box.await;
}
}
}
```
`<dyn Trait>::changed`
what does have to change:
* the `Fn` trait, the `Output` is currently `Sized`
* people can't name it in stable code without it being normalizable
* not be true
* must have a bound like `Fn() -> T`
RFC 1: "rudiments"
* everything above except for `.box` and with some intrinsics instead
RFC 2: "box box box"
* add box as a keyword in various places where it'd be nice
* `.box` is one example (the fundamental one)
* the nice to have
* `box struct Foo` -- where it can be recursive and so forth
* `box async fn` -- same deal
* `enum Foo { box BigVariant(BigData), SmallVariant }`
RFC 3: "dyn safety is dead, long live dyn safety"
* future:
* `dyn Trait` is always allowed
* but `dyn Trait` does not implement `Trait` unless
* the trait is declared to do it
* and when you do that, we check if
* all methods are dyn-safe or at least *adaptable* (you can specify "strategy")
* async fns
* if you declare a trait to be dyn then
* we add the `dyn Trait: Trait` impl
* but we also add the impls you really should have
* e.g., some subset of
* `impl<T: Observe + ?Sized> Observe for &T` (but not in this case)
* `impl<T: Observe + ?Sized> Observe for &mut T`
* `impl<T: Observe + ?Sized> Observe for Box<T>`
* which are dependent on the `self` if your methods
so you would write something like this
```rust
dyn(box) trait Observe {
async fn changed(&mut self);
}
struct Signal {
on_change: Vec<Box<dyn Observe>>
}
impl Signal {
async fn signal_change(&mut self) {
for o in &mut self.on_change {
o.changed().await;
}
}
}
```
#### example of associated types
```rust
trait Width {
type Arg;
fn len(&self) -> usize;
fn with(&self, arg: Self::Arg);
}
fn foo(d: &dyn Width) -> usize {
d.len() // OK
d.with(...) // NOT OK -- inherent member not accessible
}
fn foo(d: &dyn Width<Arg = u32>) -> usize {
d.len() // OK
d.with(22) // <-- suggests `<dyn Width>::with` is an inherent member
}
```
```rust
trait Mirror: Width {
type Foo = <Self as Width>::Arg;
}
trait Width {
type Arg;
fn len(&self) -> usize;
fn with(&self, arg: <Self as Mirror>::Foo);
}
```
```rust
trait Id {
type This: ?Sized;
}
impl<T: ?Sized> Id for T {
type This = T;
}
trait Width {
type Arg;
fn len(&self) -> usize;
fn with(&self, arg: <<Self as Id>::This as Width>::Arg); // not inherent method for `dyn Width`
}
```
- given `dyn Trait<AssocI = ..>`, method `foo`is accessible if
- eagerly walk sig, structural lookup for aliases in sig, replace with specified type (structural type equality `==`)
- if sig still references `Self` afterwards, don't add method
### emplacement intrinsic proposal a la lcnr
```rust
fn with_unsized_ret() -> dyn Trait { body }
// gets transformed to
trait Emplace<T> {
type Storage;
fn insert(this: &mut Self::Storage, value: T);
fn initialized(this: Self::Storage) -> Self;
}
fn with_unsized_ret(prev_args: .., out: &mut dyn Emplace<Output = dyn Trait>) -> dyn Trait { body // replace all return with `}
fn with_unsized_ret(prev_args: .., out: &mut dyn Emplace) { body // replace all return with `}
```
```rust
intrinsic fn call_boxed<F, A>(
f: F,
args: A
) -> Box<F::Output>
where
F: FnOnce<A, Output: ?Sized>; // <-- not stable
```
```rust
trait Emplacer {
type Storage;
type Blessed;
fn alloc(self, layout: Layout) -> (Self::Storage, *mut ());
// lcnr initialization
//
// does not support async fn in trait without already
// specifying the emplacer there :<
fn write_return<T: Unsize<UnsizedActualReturn>>(self, r: T) {}
fn initialized(storage: Self::Storage, pointer: *mut ()) -> Self::Blessed;
}
trait RawCallable<A> {
type Output: ?Sized;
unsafe fn call_unsized<E>(self, args: A, e: &mut E) -> E::Blessed;
unsafe fn call_sized(self, args: A) -> Self::Output
where
Self::Output: Sized;
}
```
```rust
returns_unsized().emplace::<MyType>().wahtever
```
### cycle semantics normalizes-to goal (info)
https://github.com/rust-lang/rust/pull/139900
### crater run updates (info)
top 1000 is working !
post to the project goal!!!
## 2025-03-19
### opaque types :3
two issues
- need to support 'revealing' uses in the defining scope
- this first
- need to also support defining in parent, revealing in closure
- then this
- whenever u use an opaque in its defining scope in mir borrowck
- do structural lookup based on the opaque type args in the `infcx.opaque_type_storage`
- if not already there, use hidden type from HIR with region infer vars
After MIR typeck, we've got storage full of opaque type uses
Compute region graph to check whether any of the opaque type uses have universal arguments rarw
These are defining!
Apply member constraints for them to constrain regions in hidden type, map them to the opaque type definition
Use that definition to check all other uses of the opaque. This uses type equality
```rust
impl Foo {
fn defines_rpit<'a>(&'a self) -> impl Sized + 'a {
if false {
let temp = Foo;
temp.defines_rpit();
// desugars to `Foo::defines_rpit(&temp);`
}
self
}
}
```
- end of MIR typeck, two uses:
- `opaque<'a> = &'?1 Foo` // from the return
- `opaque<'?2> = &'?3 Foo` // from the recursive call
- `oapque<'a>` has a universal arg -> defining use
- apply member constraint `'1 member ['a, 'static]` -> `'1 = 'a`
- mapping to definition `for<'a> opaque<'a> = &'a Foo`
- `opaque<'?2>` is revealing, check by using the definition from the defining use
- `&'3 Foo == defining_use['a/'temp] = &'temp Foo`
- takeaways: u can't assume different scc -> different values
- current algorithm
- create SCCs, yielding a dag with a single entry point S
- walk the dag starting from S
- [for each node N](https://github.com/rust-lang/rust/blob/c4b38a596767c9c6275c937cf3a2d4b9612b4875/compiler/rustc_borrowck/src/region_infer/mod.rs#L739-L753)
- let V = the "base outlives" that comes from liveness
- [V = V union (the values of all successors)](https://github.com/rust-lang/rust/blob/c4b38a596767c9c6275c937cf3a2d4b9612b4875/compiler/rustc_borrowck/src/region_infer/mod.rs#L743)
- apply_member_constraints(V, C) --
- make V equal to one of the options in C, if we can figure out which one to use
- return V as the value of N
- niko's sketch
- create SCCs on the initial set of region constraints
- propagate region values
- https://github.com/rust-lang/rust/blob/c4b38a596767c9c6275c937cf3a2d4b9612b4875/compiler/rustc_borrowck/src/region_infer/mod.rs#L739-L753
- walk defining uses to find one where:
- the current value meets the member constraints and we can compute the hidden type
- if there are revealing uses:
- invoke the type checker to compute eq and get a list of constraints C
- loop until fixed point
- for each (A:B) in C
- for each parent P of A:
- value(P) = value(P) union value(B)
- finish up borrow check etc "as normal"
- things to be resolved
- interaction with placeholders
-
## 2025-03-12
currently moving
unstable impls
* boxy is mentoring the former (:tada:)
module-private impls
* nikomatsakis doesn't want coherence
* but he does want ability to not commit to implementing a trait
* but be able to make use of it
* examples
* enum discriminants, which would be best exposed via a trait but we want privacy
* unsafe transmute
* things you might want
* expose that it's implemented but not permit normalization
* e.g., salsa/bevy would like to hide those details, kind of the same as opaque type
* hide that it's implemented entirely
* caching
* can you cache based on what was *needed* in the environment
* instead of what was *present*
module-private impls
types team lead, some ideas
* all hands:
* can we have a discussion about "stuff we treat as fixed" and/or "blockers"
* will work be *resourced*?
* Probably not, but maybe knowing what's possible will help us find resources later
* project goals
* breaking out "core" from "stretch" goals
* pre-read with team leads before RFC is opened to discuss cross-team opportunities
power of refactoring and clarifying how we think about things
* unstable impls -- now seem easy, used to seem impossible
* falls out from the desugaring + impl work
* alias -- combining
effects modeling and development
* modeling as "associated effects" --
* they are never "trait inputs", for a given trait ref --
* they may affect where there is an impl or not
* but cannot affect which impl out of many
* except they can through where-clauses
* do we care? niko doesn't (yet)
* what niko does think
* don't want two impls that differ only in effects (at least not yet)
* e.g. `impl async Default for Type`, `impl Default for Type` -- don't particularly want this
* `impl Default for Type`, `impl const Default for Type` -- what the heck this is weird
* `impl (const) Default for Type` -- one impl that can be const or not (and later... could be async)
* lcnr: I would much rather have specialization than effects
* going from async to a code transformation vs async as a "proper effect"
* making something generic over async-ness, having a maybe-async map
* feels like it's very difficult
* specific example:
* impacting associated types -- have a fn that either returns a value or a future `let x = Iterator::map(todo!(), infer);`
* is it semver compatible to go from sync to async?
* and will this leave us with a confusing stdlib
* need more marker:
* const
* target feature(s)
* panic
* loop
* io
* non-det
* static-access
* alloc
Sized trait and edition migration
* related also to Leak etc
* for Sized
* migrating from `Sized` to `const Sized`
* migrating from `T: ?Sized` to `T: ValueSized` or whatever
* could post-mono error when things are not const that should be const
* `fn foo<T: Sized>() { bar::<T>() }`
* `fn bar<T: Sized>() { const { size_of::<T>() } }`
* `trait Sized { (const) fn size_of() -> usize; }`
* editions changing default trait bounds is horrible
* niko? why
* explicit supertraits, where-bounds
* switching to new edition either adds a lot of noise to the code as the previously implied bounds now have to be explicit. Or is a breaking change
* could we avoid the need for such a migration by only linting in the old edition and accepting post-mono errors
## 2025-02-26
- project board https://github.com/orgs/rust-lang/projects/61
#137314 -- making unproductive cycles errors fixes rust-lang/trait-system-refactor-initiative#114
rust-lang/rust-trait-system-initiative#104
rust-lang/rust-trait-system-initiative#109 -- rayon hangs
lazy norm issue:
* tuple of large arity (T0...Tn)
* `where Ti: IntoIterator, Ti::IntoIter: Iterator` for T0...Tn
* for each Ti:
* try to prove `Ti: Iterator`
* use where-clause `<Tj as IntoIterator>::IntoIter: Iterator`
* normalize `<Tj as IntoIterator>::IntoIter = Ti` for some Tj
* finds the `impl<T: Iterator> IntoIterator for T` impl
* tries to prove `Tj: Iterator`
* use where-clause `<Tk as IntoIterator>::IntoIter: Iterator`
* ...
* for rayon, introduced a fast path
* `<A as Iterator>::IntoIter` cannot equal `B` because `B` does not appear in there
* caching offers an answer, but we currently re-run cycles when provisional results change which makes it ineffective
* cycle is "artificial-ish" because the canonical form is same but existential variables are not the same
* note that "iterative deepening" of search space will not help -- we need to rule out all the candidates
- https://github.com/rust-lang/rust/blob/master/tests/ui/traits/next-solver/cycles/coinduction/fixpoint-exponential-growth.rs
```rust
trait Trait {}
trait Indir {
type Assoc;
}
impl<T: Trait> Indir for T {
type Assoc = ();
}
fn foo<A, B, C>()
where
A: Indir,
B: Indir,
C: Indir,
A::Assoc: Trait,
B::Assoc: Trait,
C::Assoc: Trait,
{}
```
- `A: Trait` with candidates
- where-bound `A::Assoc: Trait` -> `A::Assoc = A`
- `normalize(A::Assoc) = ?`
- use `impl<T: Trait> Indir`
- `A: Trait` cycle unproductive
- use `? = rigid(A::Assoc)`
- `rigid(A::Assoc) = B`? -> fail
- where-bound `B::Assoc: Trait` -> `B::Assoc = A`
- `normalize(B::Assoc)` use `impl<T: Trait> Indir`
- `B: Trait`
- where-bound `A::Assoc: Trait` -> `A::Assoc = B`
- `normalize(A::Assoc)` use `impl<T: Trait> Indir`
- `A: Trait` cycle unproductive
- where-bound `B::Assoc: Trait` -> `B::Assoc = B`
- `normalize(B::Assoc)` use `impl<T: Trait> Indir`
- `B: Trait` cycle unproductive
- where-bound `C::Assoc: Trait` -> `C::Assoc = B`
- `normalize(C::Assoc)` use `impl<T: Trait> Indir`
- `C: Trait`
- where-bound `A::Assoc: Trait` -> `A::Assoc = C`
- `normalize(A::Assoc)` use `impl<T: Trait> Indir`
- `A: Trait` cycle unproductive
- where-bound `B::Assoc: Trait` -> `B::Assoc = C`
- `normalize(B::Assoc)` use `impl<T: Trait> Indir`
- `B: Trait` cycle unproductive
- where-bound `C::Assoc: Trait` -> `C::Assoc = C`
- `normalize(C::Assoc)` use `impl<T: Trait> Indir`
- `C: Trait` cycle unproductive
- where-bound `C::Assoc: Trait` -> `C::Assoc = A`
- `normalize(C::Assoc)` use `impl<T: Trait> Indir`
- ... whole thing but with B/C flipped ...
Question:
1. Why do rigid alias handling in `normalizes_to` vs having it just *fail* (and caller somehow decides to fallback to rigid), kind of the equivalent of having these two rules
- `<X as Trait>::Assoc eq Z :- normalizes_to(<X as Trait>::Assoc, Y), Y eq Z`
- `<X as Trait>::Assoc eq rigid(<X as Trait>::Assoc).`
3. Does not doing so actually help?
---
- normalization first constraints then fails: `<T as Trait<?x>>::Assoc` normalizes-to `u32` if `?x: Copy`, otherwise rigid
- return AMBIGUOUS, but returning `u32`
## 2025-02-19
- coinduction :3 https://github.com/rust-lang/rust/pull/136824
- using async to do progressively deeper search
- "A trait solver cycle is now coinductive if it has at least one coinductive step. A step is only considered coinductive if it's a where-clause of an impl of a coinductive trait. The only coinductive traits are Sized and auto traits."
- "a cycle is considered *productive* if it has at least one step that meets these criteria"
- https://gist.github.com/lcnr/c49d887bbd34f5d05c36d1cf7a1bf5a5
niko reads
questions
```rust
trait Magic: Copy {}
impl<T: Magic> Magic for T {}
fn magic_copy<T: Magic>(x: T) -> (T, T) { (x, x) }
```
```rust
trait Magic: Copy {}
impl<T: Magic> Magic for T {}
fn magic_copy<T: Magic>(x: T) -> (T, T) { (x, x) }
impl Copy for u32 { }
```
```
inductive Copy (self : Type) : Type where
| mk : Copy self
inductive Magic (self : Type) : Type where
| mk : Copy self -> Magic self
def impl_Magic_for_T (t : Type) (dict: Magic t) : Magic t :=
let (Magic.mk dictC) := dict
Magic.mk dictC
def impl_Copy_for_u32 : Copy u32 := Copy.mk
/- To call `fn magic_copy::<u32>`, we need to prove `u32: Magic` -/
def call_magic_copy (t: Type) : Magic t :=
impl_Magic_for_T t (call_magic_copy t)
```
```rust
// A variation of #135246 where the cyclic bounds are part of
// the impl instead of the impl associated item.
trait Trait<R>: Sized {
type Proof: Trait<R, Proof = Self>;
}
impl<L, R> Trait<R> for L
where
L: Trait<R>,
// normalize this where-bound via item bound of `L::Proof` to
// R: Trait<R, Proof = L>
// Item bound `L::Proof: Trait<R, Proof = L>`
R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>,
// ------------------------------ to L via the trait bound
{
// need to prove item bound `R: Trait<R, Proof = L>`
type Proof = R;
}
// Using the impl proves `R: Trait<R, Proof = <L::Proof as Trait<R>>::Proof>`
// while normalizing `<L::Proof as Trait<R>>::Proof` via the
// impl
fn transmute<L: Trait<R>, R>(r: L) -> <L::Proof as Trait<R>>::Proof { r }
fn main() {
let s: String = transmute::<_, String>(vec![65_u8, 66, 67]);
println!("{}", s); // ABC
}
```
- recursion in negative position unsoundness in koka https://github.com/koka-lang/koka/issues/263
```rust=
trait Magic
where
(Self: Magic) => (Self: Copy) // (Magic self -> Copy Self)
{
}
```
```lean
inductive Magic (self : Type) : Type where
| mk : (Magic self -> Copy self) -> Magic self
```
```rust
trait Magic {
type Assoc<T: Magic>: Copy;
}
```
```lean
inductive Copy (self : Type 0) : Type 1 where
| mk : Copy self
inductive MagicAssoc (self : Type 0) (t : Type 0) : Type 1 where
| mk : (assoc_type : Type 0) -> Copy assoc_type -> MagicAssoc self t
inductive Magic : (self : Type 0) -> Type 1 where
| mk : (assoc : (t : Type) -> Magic t -> MagicAssoc self t) -> Magic self
```
> (kernel) arg #2 of 'Magic.mk' has a non positive occurrence of the datatypes being declared
## 2025-01-29
* Project Board (!)
* https://github.com/orgs/rust-lang/projects/61/views/1
Implied bounds
* Region constraint solving
* Needs to be able to handle region constraints with different where-clauses in scope
* Or we eagerly handle them when exiting the binder
```rust
struct Set<T: Ord> { }
fn gimme_a_set<T>(s: Set<T>) {
// Today: error
//
// Niko's current thinking: ok
// * `WF(Set<T>)` is assumed
// * but `WF(Set<T>)` does not imply `T: Ord`
}
```
* Unstable trait impls.... seems eminently doable?
* why not add a `stability_feature_enabled(F)` where-clause...?
* ambiguous unless feature is enabled
* target features...
* `where Platform: SupportsTargetFeatureX`
## 2025-01-22
* contract - tyler unclear
* lcnr proposes $230/hr
* $184000 = 20 * 10 * 4 * 230
* new solver major initiatives and timelines
* unblock the stabilization of TAITs and ITATs
* project goal slate https://github.com/nikomatsakis/rfcs/blob/2025h1/text/0000-Project-Goals-2025h1.md
* https://rust-lang.github.io/rust-project-goals/2025h1/next-solver.html
* plausible goal:
* unify TAIT impl between old and new trait solver, unblock types team side of stabilization
* types team "contract"
* don't want to worry about places that "could define opaques but don't" -- passthrough, unconstrained opaques
* alternatively, need
* a "syntactically driven" way to define the defining scope
* requirement that within defining scope, TAIT is defined
* other questions:
* attributes used to indicate when a particular function is a defining use
* with what teams will
* https://rust-lang.github.io/rust-project-goals/2025h1/next-solver.html
* rust-analyzer talked to jack?
* yes, during office hours
* goals
* formality
* support rust test cases <-- "joint hackathon"
* align on coherence-y
* *how to manage this*
* model borrow check (with Ralf student)
* model const (with tiif + oli)
* "rusty logic"
* super minimal Rust model, move it to lean --
* trait solver pattern:
* impl + reviewer
* get formality reviewers
* lcnr to review
* boxy to review
## 2025-01-15
lcnr discovered a TRAGEDY
```rust
struct Foo;
impl Foo {
fn recur<'a>(&'a self, b: bool) -> impl Sized + 'a {
if b {
let temp = Foo;
let borrow = &temp;
let _: () = borrow.recur(false);
// defining use `opaque<'local_var> = ()`
// requires `'local_var` to be universal
}
}
}
```
- https://github.com/rust-lang-nursery/gll/blob/3e82b327f5dff5a7ab2c7c20498b597a0d47b581/src/generate/rust.rs#L724-L727
```rust
struct Foo;
impl Foo {
fn recur<'a>(&'a self, b: bool) -> impl Sized + 'a {
if b {
let temp = Foo;
let borrow = &temp;
let _: () = borrow.recur(false);
// defining use `opaque<'local_var> = ()` therefore
// * add a `member('local_var, ['a ... any other universals in scope ...])` constraint
// * instantiate the `opaque` with a fresh inference variable `H` as normal
// * require `H` to meet member requirements as well, as normal
}
}
}
```
### require universal args
- if we had `opaque<u8> = u8`, should this be `opaque<T> = T` or `opaque<T> = u8`?
- if we had `opaque<'static> = 'static`, as above
- notably, local var lifetimes can't be static, seems relevant
- if we had `opaque<'a, 'a> = 'a`, should this be `opaque<'a, 'b> = 'a` or `opaque<'a, 'b> = 'b`?
- they definitely have to be unique
- do they have to be universal though? WE THINK IT SHOULD ("could" -- nikomatsakis) BE FINE
### does this mess with member constraint inference/closure requirement propagation
```rust
struct Foo;
impl Foo {
fn recur<'a, 'b>(&'a self, input: &'b [u32]) -> impl Sized + use<'a, 'b> {
if false {
let temp = Foo;
let borrow = &temp;
let data = [1, 2, 3];
let _: &'?4 [u32] = Foo::recur::<?1, ?2>(&?3 *borrow, &data);
// `opaque<'1, '2> = &'4` ()`
// - '4 member ['1, '2, 'static]
} else {
input // return type has to be `&'b u32`
}
}
}
```
```rust
struct Foo;
impl Foo {
fn recur() -> impl Sized {
if true {
(22_u32, panic!())
} else {
(panic!(), 22_u32)
}
}
}
```
Lcnr proposal on how to "fix the source"
```rust
struct Foo;
impl Foo {
fn recur_wrap<'a>(&'a self, b: bool) -> impl Sized + 'a {
self.recur(b)
}
fn recur<'a>(&'a self, b: bool) -> impl Sized + 'a {
if b {
let temp = Foo;
let borrow = &temp;
borrow.recur_wrap(false);
}
}
}
```
nikomatsakis concern from [gll](https://github.com/rust-lang-nursery/gll/blob/3e82b327f5dff5a7ab2c7c20498b597a0d47b581/src/generate/rust.rs#L724-L727)
```rust
struct Foo;
impl Foo {
fn recur_wrap<'a>(&'a self, b: bool) -> Thunk<impl Cont + 'a> {
self.recur(b)
}
fn recur<'a>(&'a self, b: bool) -> Thunk<impl Cont + 'a> {
if b {
let temp = Foo;
let borrow = &temp;
borrow.recur_wrap(false)
} else {
other_stuff
}
}
}
```
https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=5351a85d676098047873ec1ea5aaec4d
```rust
// we manage to pick 'static here
struct Bar;
impl Bar {
fn recur<'a, 'b>(&'a self, input: &'b [u32]) -> impl Sized + use<'a, 'b> {
&[1]
}
}
```
```rust
// this errors but could be accepted if we had a more general notion of region
//
// error[E0700]: hidden type for `impl Sized` captures lifetime that does not appear in bounds
struct Bar;
impl Bar {
fn recur<'a, 'b>(self, input1: &'a [u32], input2: &'b [u32]) -> impl Sized + use<'a, 'b> {
if false { input1 } else { input2 }
}
}
```
```rust
// This errors because 'a or 'b are ambig
//
// removing `'b` makes it compile
struct Bar;
impl Bar {
fn recur<'a, 'b, 'c: 'a + 'b>(&'a self, input: &'c [u32]) -> impl Sized + use<'a, 'b> {
input
}
}
```
## 2024-01-10
- lcnr notes https://github.com/lcnr/notes/tree/main/opaque-types
```rust
fn foo<'a>() -> impl Sized + use<'a> {
let _ = || foo();
1
}
// for mir borrowck
fn closure() -> i32 {
foo();
}
```
### member constraints
defining use `Opaque<'a, 'b> = &'?x ()`: need to make sure `?x member ['a, 'b, 'static]`
needs to know the way `?x` is related to the choice regions:
- if `?x` is equal to one of the choice regions, just choose that one
- if `?x` is outlived by some choice which is "smaller" than all others, choose that one
### why we don't know how these things relate
```rust
struct Inv<'a>(&'a mut &'a ());
fn relate_lts<'a>(x: Inv<'a>, cond: bool) -> impl Sized + 'a {
if cond {
let closure = |x| relate_lts(x, false);
closure(x)
} else {
x
}
}
```
The closure desugars to
```rust
fn closure<'aext>(x: Inv<'ext1>) -> Inv<'ext2> {
let x: Inv<'local1> = relate_tys::<'local2>(x);
x
}
```
The assignment equates `Opaque<'local2>` with `Inv<'local1>`. After region constraint propagation we get `Opaque<'ext1> = Inv<'ext2>`. The member constraint `'ext2 member ['ext1, 'static]` is ambiguous.
We only know what to do once the caller requires that `'ext1` and `'ext2` are the same. This requires information from the caller to propagate into the closure.
- walkthrough of code https://github.com/lcnr/notes/blob/main/opaque-types/status-quo.md#regioninferencecontextsolve
- https://github.com/rust-lang/rust/blob/b44e14f762fd4062faeba97f8f2bc470298ec1ac/compiler/rustc_borrowck/src/region_infer/mod.rs#L739
```rust
fn closure<'aext>(x: &'ext1 ()) -> &'ext2 () {
let x: &'local1 () = relate_tys::<'local2>(x);
x
}
```
`Opaque<'local2> = &'local1 ()` with `'ext1: local2` and `'local1: 'ext2`
Final member constraint `'local1 member ['local2, 'static]`
Currently fails even outside of closures as `'local2` is not universal
```rust
fn foo<'a>() -> impl Sized + 'a {
if false {
let _: &'a () = foo(); // error
}
&()
}
```
```rust
fn closure<'aext>(x: &'ext1 ()) -> &'ext2 () {
let x: &'local1 () = relate_tys::<'aext>(x);
x
}
```
`Opaque<'aext> = &'local1 ()` with `'local1: 'ext2`
member constraint `'local1 member ['aext, 'static]` need to propagate to caller
need to constrain `'local1` to some external region
conceivably `'local1` could be set to `min('aext, 'static)`
```rust
trait SomeTrait {
fn trait_method(&self);
}
fn recursive() -> impl SomeTrait {
let _ = || recursive().trait_method();
}
```
actual example: https://github.com/kurnevsky/esxtool/blob/88538ca7c8e068b5e38d4b386eb1bf3d5cede3d0/src/mwscript/parser.rs#L186-L191
- https://docs.rs/combine/latest/combine/fn.parser.html
Conclusions
There are 3 "steps" that build on one another
1. Propagate member constraints to caller
2. Ability to inject a "fresh external region" (alternatively, to propagate an `exists<X> { .. }` solution to caller) so that we can transform `'local member ['ext1, 'ext2]` to `'exists3` where `'exists3 member ['ext1, 'ext2]`
3. Transform `'local1 member ['local2, ..]` to
* `'exists1 member [all free things]` (where `'local2 = 'exists2`)
* `'exists2 member ['exists1]` (where `'local1 = 'exists2`)
```rust
fn foo<'a>() {
let x: for<'b> |x: Inv<'b>| let _: &'local () = opaque::<'a, 'b>;
}
```
- `'local member ['exta, 'b, 'static]` forbid universal regions from the closure
- compute region constraints via type check
- incorporating constraints from closures we create
- create SCCs, remove higher-ranked stuff
- solve region constraints -- creating a value for each SCC
- independently:
- "do borrow check"
- check verifys
- check outlives between universals
## 2024-12-18
Ideas
* schedule time to do joint reviewing (niko to schedule with Andrew Zhonig)
* mir-formality
### Rotating hack-o-rama
maybe for all hands
* simple task
* oracle role
* group of people who are collectively working towards a goal
* rotating every N minutes
why this structure?
* it's fun and wacky
* it's a good way to introduce a bunch of people to a codebase without having to come up with N simple tasks, which are often in short supply
### Mentored on-call / office hours / interning / externing
* person has complex task to do
* mentor is online for some specified time to answer questions, but they're doing other things at the time
* rinse and repeat
## 2024-12-04
* always prefer trivial builtin impls
* if there is a conflict between a non-global where-bound and some other where bound, declare ambiguity <-- change
* if there is a single non-global where-bound, guide inference
* then prefer alias bounds and builtin trait object candidates
* merge everything ignoring trivial where-bounds, if there are no candidates, try using global where-bounds
## 2024-11-27
### status
* Worked on solver, able to compile all of rustc
### onboarding folks
### goals
* new solver can do a bors perf run
* mir-formality: cover coherence and negative trait impls
* able to be tested against rustc
* coinductive trait matching
* TAIT
*
* async stuff
### disjunctive traits
* blocks generator design
*
## 2024-11-11
https://github.com/nikomatsakis/rusty-logic
https://github.com/nikomatsakis/rusty-logic/blob/main/doc/intro.md
https://github.com/nikomatsakis/rusty-logic/blob/main/doc/judgments.md
This version is "not quite" the problem:
```rust
trait Foo {
type Bar: Copy
where
Self: Copy;
}
impl<T> Foo for T {
type Bar = T
where
T: Copy;
}
fn foo<T: Foo>() {
T::Bar as Copy; // lcnr expects it to error here
// req T: Copy
// alias-bound T eq T::Bar
}
struct String { }
fn main() {
foo::<String>;
}
```
This version shows the problem more clearly:
```rust
trait Foo {
type Bar: Copy
where
Self: Foo;
}
impl<T> Foo for T {
type Bar = String // this uses alias bound of T::Bar
where
T: Foo;
}
fn foo<T: F>() {
T::Bar as Copy;
}
```
Want this to work
```rust
trait Foo {
type Bar: Copy;
}
fn foo<T: Foo<Bar = X>, X>() {
X as Copy;
}
```
WF check on the impl is
* for all impl parameters
* assuming the impl where clauses
* lint: prove trait supertraits (not necessary for soundness)
* for each associated type `A<Q..> = t where W`
* for all `Q`
* assuming `W`
* prove `t` meets bounds in trait
For this check to not be broken, you must not be able to alias-bounds of `A` for `t`
```rust
trait A {
type B: Copy
where
Self: A;
}
trait C {
type D: Copy
where
Self: C;
}
impl<T> A for T {
type Bar = T::D // this uses alias bound of T::Bar
where
T: Foo;
}
fn foo<T: F>() {
T::Bar as Copy;
}
```
* If our goal is `X: Bar`
* and there exists in the environment
* `T: Foo<FooItem = U>`
* and `FooItem: Bar` in `Foo`
* and we can unify `X = U`
* then we have a "match"
Worry, can we always fund a path
```rust
trait Foo {
type FooItem: Bar.
}
// Γ |- (FooItem X) : Bar
trait Bar { }
trait Trait<U>
where
U: OtherTrait<Self>,
{}
// ForAll Self, U:
// Γ |- (OtherTrait U Self) :- [eins]
// Γ |- (Trait Self U)
trait OtherTrait<T>: Foo<FooItem = T> {}
// ForAll Self, T:
// Γ |- (Foo Self) :- [zwei]
// Γ |- (OtherTrait Self T)
// Γ |- ((FooItem Self) ~~> T) :- [drei]
// Γ |- (OtherTrait Self T)
fn scope<T: Trait<U>, U>() {
T as Bar
// (Trait T U) |- (Bar T) ?
}
```
Niko's theory
* We need to prove `(Bar T)` and we know `(FooItem ?X) : Bar`
* Can we find an assumption unifiable with `(FooItem ?X) ~~> T`?
* By rule drei we can if we can find an assumption unifiable with `(OtherTrait ?X T)`
* By rule eins we can if we can find an assumption unifiable with `Trait T ?X`
* which we can if `?X = U` because `(Trait T U) \in \Gamma`
## 2024-10-30
### cycle semantics
- https://hackmd.io/yDpNrmqxRxG1ChCdRmGNSg had two issues:
- https://github.com/rust-lang/trait-system-refactor-initiative/issues/133
How to handle alias bounds:
- https://hackmd.io/yDpNrmqxRxG1ChCdRmGNSg#alias-bounds
why no check on normalization:
```rust
trait Trait {
type Assoc;
}
fn inner<T>() {}
fn foo<T: Trait>() {
inner::<<T as Trait>::Assoc>();
}
```
imagine the "alias-bounds hold" check fails for `<T as Trait>::Assoc` here. We only ever normalize that alias inside of `foo`, so instantiating `foo` would not need to prove anything, causing post-mono errors.
### example
```rust
trait Trait {
type Assoc: Copy
where
Self: Trait;
}
impl<T> Trait for T {
// Proving `T: Copy` while being able to assume `T: Trait`
// and therefore `<T as Trait>::Assoc: Copy` can be made to
// fail, but feels highly dangerous.
type Assoc = T
where
Self: Trait;
}
fn copy_via_alias_bound<T: Trait>() {
let x: Option<T::Assoc> = None;
drop(x);
drop(x);
}
fn main() {
let x = String::new();
copy_via_alias_bound::<String>(x);
}
```
Three possible places to error:
- trait definition
- only allowed where-clauses
- generic use of `T: Trait`
- using the impl non-generically
### Trait Definition X1
* One rule might be:
* Disallow all where-clauses on aliases where the Self type is not a newly introduced generic parameter
* obviously breaking, but ignore that for now
```rust
trait Trait {
type Assoc<T>: Copy
where
T: Something<Self>;
}
trait Something<T: Trait>: Supertrait {
// assuming a more expansive definition of
}
impl<T: Trait, U> Something<T> for U { }
fn copy_via_alias_bound<T: Trait>() {
let x: Option<T::Assoc> = None;
drop(x);
drop(x);
}
fn main() {
let x = String::new();
copy_via_alias_bound::<String>(x);
}
```
### Later Modality X2
* To prove `T: Trait` given `impl<Q..> Trait for _ where WC_impl`...
* Equate the impl parameters duh
* Productively:
* prove the impl where clauses `WC_impl`
* Nonproductively:
* the supertraits
* for each alias A<P..>: Bound = V where WC,
* `later(WC) => V: Bound`
* you can only remove something from the "later" box if it involves some parameter in P
* Concerns
* can the person using the alias wind up using some kind of self-supporting cycle
* `later(WC) => V: Bound` relies on the callee using the alias has to productively prove something about the `WC`
*
```rust
trait Trait {
type Assoc<T>: Copy
where
T: Copy;
}
fn foo<T: Trait>() {
}
```
### Later Modality X3
* To prove `T: Trait` given `impl<Q..> Trait for _ where WC_impl`...
* Equate the impl parameters duh
* Productively:
* prove the impl where clauses `WC_impl`
* Nonproductively:
* the supertraits
* for each alias A<P..>: Bound = V where WC,
* `later(WC) => V: Bound`
* you can only remove a term `X` from the "later" box if `FV(X) subset P`
* all its free variables are in P
Niko claims this variation feels like it *has* to be true, but why...
* because the caller is relying nonproductively on things about P
* the callee
```rust
trait Factory {
type Set<W: Ord>: Copy;
}
fn callee<F: Factory>() {
let x: F::Set<X>... // must prove X: Ord
calls::<X>()
}
fn calls<W: Ord>() {}
```
```rust
trait Trait {
type Assoc<T: Trait>: Copy;
}
fn type_of_self<U: Trait>() {
// Proof of `U: Trait` for the GAT-param happens *at the same time*
// as the proof of `U: Trait`.
//
// The `U: Trait` in the caller will be able to assume the GAT
// where-clause `U: Trait` even though that where-clause is just
// `Self: Trait` here.
let x: U::Assoc<U>;
}
fn caller() {
type_of_self::<V>();
}
```
* `caller` finds an impl of `Trait` for `V` and proves
* supertrait implications of `V: Trait` (there are none)
* associated type bound `Assoc<T>: Copy` productively, subject to `T: Trait`
* this may make use of some derived predicate `P` based on `T: Trait`
* `callee` assumes `U: Trait`
* `callee` assumes `U::Assoc<U>` is `Copy`
* which relies on `P[U/T]`
* but `P` was dependent on `U: Trait`
* "and maybe there's a nonproductive cycle here"
under the most lenient rules and our original motivating example
```trait
trait Trait {
type Assoc: Copy
where
Self: Trait;
}
```
* `caller` finds an impl of `Trait` for `V` and proves
* associated type bound `Assoc = SomeType: Copy` productively, subject to `V: Trait`
* this made use of a derived predicate `P = V::Assoc: Copy` which held because `V: Trait` implies `V::Assoc: Copy`
* `callee` assumes `U: Trait`
* `callee` assumes `U::Assoc` is `Copy`
* which relies on `P` (with appropriate substitution)
* but `P` was dependent on `U: Trait`
*
we should read https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf
### mir formality
## 2024-10-23
- https://github.com/lcnr/random-rust-snippets/issues/10
possible project goals
* cycle semantics ("coinduction")
implementable trait aliases
```rust
pub trait LocalService {
async fn method();
}
pub trait Service = LocalService<method(..): Send> + Send;
```
for users
```rust
impl Service for MyType {
async fn method() {
} // error: if this is not Send
}
```
Niko's goal is to enable the above pattern
---
Niko would like a way to guarantee Send for things and get a compilation error if not
```rust
struct MyType;
impl Send for MyType {
// look ma, a safe impl
}
```
```rust
pub trait Service = LocalService<method(..): Send> + Send;
// equivalent to a series of impls for its parts
```
---
Niko would like trait aliases to be equivalent to a pair of impls
```rust
// trait A = B + C;
trait A: B + C {}
impl<T: B + C> A for T { }
```
* `T: A` is equivalent to `T: B + C`
* and `A` is implemented
```rust
// trait Foo<T> = Send where T: Ord;
trait Foo<T>: Send
where
T: Ord;
impl<S: Send, T> Foo for S
where
T: Ord,
{ }
```
* `X: Foo<Y>` is equivalent to ... what?
* `X: Send` and an error if `Y: Ord` does not hold (for traits)
* `X: Send, Y: Ord` (for trait aliases)
* and `A` is implemented
Potentially introduces some kind of cycle. Elaboration doesn't terminate.
```
// clearly not elaborable
trait Foo<T> where Vec<T>: Foo<T>;
```
## 2024-10-18
* nalgebra
* Alias of a struct normalizes to a struct of that alias
* Alias of struct normalizes to Alias1 ...
* dev-guide work
* paying her to write documents
* improving the types team documentation, everybody who has the in-depth knowledge
* baseline type system maintenance + cleanup
*
## 2024-09-10
- https://hackmd.io/yDpNrmqxRxG1ChCdRmGNSg
* productive and not productive cycles
* much better terminology
* B is implemented if A is implemented
* A is implemented (via impl) if B is implemented
* cycle
invariant:
* all implications (that are not just an impl)
* must validate them when using the impl
true soundness criteria
* for every "X is implemented" in the cycle
* there is a corresponding `impl` in the program
4 non-productive cycles we currently have to deal with
https://hackmd.io/nwRk504pQQ2qUPr87HXkWQ
```rust
trait Trait {
type Assoc;
}
type Alias = <() as Trait>::Assoc;
impl Trait for () {
type Assoc = Vec<Alias>;
}
```
- `normalizes_to(Alias, Vec<Alias>)`
- `equate(Vec<Alias>, Vec<Alias>)` productive
- `equate(Alias, Alias)` trivial identity: OK
- `normalizes_to(Alias, ?0)`
- `equate(Vec<Alias>, ?0)` productive: `?0 = Vec<?1>`[^2]
- `equate(Alias, ?1)`
- `normalizes_to(Alias, ?1)` productive cycle: OK
what actually happens in rustc:
- `AliasRelate(Alias, Vec<Alias>)`
- `NormalizesTo(Alias, ?fresh_infer)`
- `?fresh_infer = Vec<Alias>`
- equate `Vec<Alias>` with `Vec<Alias>` ok
- `AliasRelate(Alias, ?0)`
- `NormalizesTo(Alias, ?fresh_infer)`
- `?fresh_infer = Vec<Alias>`
- equate `Vec<Alias>` with `?0`. Instantiate `?0` with `Vec<Alias>` which may normalize `Alias`, which would then result in
- `AliasRelate(Alias, ?1)` which cycles (and errors)
- https://github.com/rust-lang/trait-system-refactor-initiative/issues/75 may be relevant
- related: occurs check, why `Vec<Alias> = Alias` ok but `Vec<?0> = ?0` not
- can't change occurs check, neccessary for coherence
- e.g. `impl<T> From<T> for T`
Have to rerun here because `normalizes_to` constrains an inference var, resulting in overflow at some point.
```rust
trait Trait {
type Assoc;
}
type Alias2 = <u8 as Trait>::Assoc;
impl Trait for u8 {
type Assoc = Alias2;
}
type Alias = <() as Trait>::Assoc;
impl Trait for () {
type Assoc = Alias2;
}
```
- `normalizes_to(Alias, Alias2)` to `Alias2`
- `equate(Alias2, Alias2)` trivial identity: OK not actually :shrug:
-
we can modify the details of how this is expanded, e.g., normalizes-to (when target is another alias) recursively expand
the doc: https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?both
summary:
* should be produ
### finite size is good, actually
We want some kind of "finite size" predicate that must be proven when you normalize...
```rust
trait Trait {
type Assoc;
}
type Alias = <() as Trait>::Assoc;
impl Trait for () {
type Assoc = Vec<Alias>;
}
// normalizes_to(Alias, ?T) :-
// equal(Vec<Alias>, ?T),
// finite_size(Vec<Alias>)
```
```rust
fn foo<T: Trait>() {
// we want to be able to assume `T::Assoc`
// has finite size / is normalizable
//
// implies that:
// * we need to prove it is normalizable
// when calling `foo`
}
```
What Niko is thinking
* Impls
* require: where-clauses
* declare (assuming where-clauses hold...)
* trait is implemented
* values for the associated types
* assert (assuming where-clauses hold...)
* super traits are implemented
* normalized associated types meet their bounds
* associated types are normalizable
* "assert" means:
* "you" can rely on this to be true assuming all WF checks succeed
Fact:
* You can check the assertions but:
* where-clauses may provide the assertion itself
* Productive
```rust
trait Trait {
type Assoc;
}
type Alias = <() as Trait>::Assoc;
impl Trait for () {
type Assoc = Vec<Alias>;
}
```
```rust
trait Trait {
type Assoc;
}
impl<T: Trait> Trait for Vec<T> {
type Assoc = T::Assoc;
}
trait Indir {
type IndirAssoc<T: Trait>: Trait;
}
struct Map<T>(T);
impl<T: Indir> Trait for Map<T> {
type Assoc = <T::IndirAssoc<Self> as Trait>::Assoc;
}
// in a downstream crate
struct Local;
impl Indir for Local {
type IndirAssoc<T: Trait> = Vec<T>;
}
// `<Map<Local> as Trait>::Assoc` is now infinite,
// all impls are
// fine by itself.
```
```rust
trait Alpha {
type Alpha;
}
trait Beta {
type Beta<T: Alpha>: Alpha;
}
impl<T: Alpha> Alpha for Vec<T> {
type Alpha = T::Alpha;
}
impl<T: Beta> Alpha for Option<T> {
type Alpha = T::Beta<Self>::Alpha; // <-- Line IMPL
// type Alpha = Vec<Option<T>>::Alpha;
// type Alpha = Option<T>::Alpha;
// type Alpha = Vec<Option<T>>::Alpha;
}
impl Beta for () {
type Beta<T: Alpha> = Vec<T>;
}
// Type Option<()>::Alpha cannot be normalized
```
```rust
fn is_alpha<A: Alpha>() {}
fn is_beta<B: Beta>() {}
fn foo<B: Beta>() {
// foo assumes Beta's GATs are normalizable
is_alpha::<Option<B>>();
}
fn main() {
// main would have to look at Alpha
// to see the problem. Why.
foo::<()>();
}
```
How it could be Line IMPL that is at fault
* `AlphaWf(Option<T>) :-`
* `T: Beta =>`
* `Wf(T::Beta<Option<T>>::Alpha) :-`
* `Option<T>: Alpha :-`
* `AlphaWf(Option<T>)` -- cycle
Actually this would make it an error on both IMPL and at USE. Is that ok?
## 2024-06-10
* `G :=`
* `[] G` -- G is true in all possible worlds
```
(G :- C) in A
A |- [] C
----------
A |- [] G
```
```
(G :- C) in A
not (A |- <> C)
----------
A |- not [] G
```
```
Traitgoal += (Bias, TraitRef)
```
```rust=
enum Predicate {
TraitRef(TraitRef),
All(Vec<Predicate>),
Not(Rc<Predicate>)
}
```
might be easier if we do
```rust=
enum Predicate {
TraitRef(Polarity, TraitRef),
All(Vec<Predicate>),
Any(Vec<Predicate>),
Not(Rc<Predicate>)
}
```
```
P = TraitRef(Polarity, TraitRef)
A |- TraitRef(!Polarity, TraitRef)
-----
A |- Not(P)
```
```
P = All(Q0...Qn)
A |- Any(not Q0...not Qn)
----- "demorgan"
A |- Not(P)
```
```
// conditions for when a trait is known NOT to be implemented
-----
A |- TraitRef(NegPolarity, ...)
```
```
(
---------
Something(foo, ForAllWorlds(TraitRef))
)
```
## 2024-04-11
* Arthur / Bastian
* Two killer domains
* Third killer domain: high-assurance programming / cve-rs etc
* hypervisors (firecracker)
* Prioritization
* Enabling the standard async interface (extensibility)
* needs more research but ...
* marker traits
* specialization
* inference defaults
* solve the "catch 22" of creating standard interfaces in the wild
* coherence
* Close all the unsoundnesses
* solver
* a-mir-formality
* spec
* General usability
* Polonius
* Implied bounds
* ...
* a-mir-formality
* want to have a full verification but this is a job for researchers
* wants a model quite removed from the way we implement the trait system
* what they do need is a bridge from rustc to the formal model
* requirements
* able to fuzz it
* superset of rustc: rustc only accepts things also accepted by a-mir-formality
* rustc can produce more errors
* should we be based on thir
* after HIR type check, incompleteness banished (or nearly)
* fuzzing
* 1. assertion testing
* 2. here's a program mir-formality rejects, does rustc also reject
* 3. here's a program mir-formality accepts, does rustc also accept
* incompleteness
* reverse direction
* 1. generate rust source
* run rustc on it
* does it ICE?
* file a bug
* if it is accepted, does a-mir-formality accept it
* testing:
* soundness of rustc
* completeness of a-mir-formality
* next steps
* load rust test cases into formality
* model thir + thir type check
* borrow check
* steps after
Niko's time
* 20% slack
* 20% project goals
* 20% amazon overhead
* 10% async
* 10% lang team
* 20% trait solver stuff
* 20% understand genai
* 3b1b video about GPT https://www.youtube.com/watch?v=wjZofJX0v4M
## 2024-03-08
* PM'd Jack about new types lead
* Contracts
* $220/hr, initial request
* April - December
* 4 * 5days/wk * 4wks/month * 9 months * $220
* 720 hr * 220/hr = 158400
* Schedule 1:1
* Gracie Gregory
* Joel Marcey
* Bec Rumbul
* Microsoft manager (Daniel Framptom)
* New trait solver
* ready to go
* Types
* "project org stuff"
* lang-team
* async
* polonius / borrow checking
* "other things"
* a-mir-formality
* where Niko would probably write code
* is it useful? how to get more people involved?
* Dada model
* https://github.com/dada-lang/dada-model/
* supports interior borrows
---
* a-mir-formality
* where Niko would probably write code
* is it useful? how to get more people involved?
* playground for experimenting with approaches?
* very possible
* same with higher-ranked lifetimes etc
* fuzzing? seems hard.
* Rust has omg so many corner cases
* potential focus areas
* can model coherence, borrow checker
* converting from Rust input tests automatically
* what are the things we need to prove out the areas of most uncertainty?
* implied bounds
* `trait Foo<T: Ord>: Bar + Baz`
* coinduction
* time to write the RFC
* add to the new trait solver
* higher-ranked subtyping
* eager placeholders
* borrow checking
* differences between a-mir-formality
---
coinduction breakage: https://github.com/rust-lang/trait-system-refactor-initiative/issues/80
---
```mermaid
flowchart LR
Think --> Model --> Implement
Implement -- find problem --> Model
Implement -- feel good --> Stabilize
```
AGREE THAT
* mir-formality is useful as a modeling tool / pliable, but not going to give strong correctness nor performance
* strong correctness would come from a combination of coq and real world validation
* performance comes from rustc
BIG UNKNOWNS
* how much correctness can we get from mir-formality with some sort of fuzzing?
* how much can a-mir-formality help us derive the invariants we expect type system to uphold, and can they be used to fuzz?
* how "complete" should a-mir-formality be
* complete = details of the language
* complete = details of the implementation
* how much can we fuzz it against rustc
## 2023-06-09
- default associated types and coinduction
- anything you can derive using `AliasBound` (elaborated bounds), have to recheck when using impl, can assume when using where clauses
- using impl with default assoc items doesn't work, have to prove item bounds for an unknown type
```rust
trait Trait {
type Assoc: Copy;
}
impl<T> Trait for T {
default type Assoc = u32;
}
fn impls_trait<T: Trait>() {}
fn foo<T>() {
impls_trait<T>();
}
```
---
```rust
trait Foo {
type Item: Default + Copy where <Self as Foo>::Item: Copy;
fn copy_me(x: &Self::Item) -> Self::Item {
*x
}
}
impl<T> Foo for Option<T> {
default type Item = u32 where u32: Copy;
}
impl Foo for Option<()> {
// impl check does not check this
default type Item = String where String: Copy;
}
fn main() {
// when is this an error?
// Has to prove `<Option<()> as Foo>::Item: Copy`
//
// Option A. Check at normalization time
// (monomorphization at the latest); check eagerly
// at impl definition (fails to catch edge cases
// like the above, but catches most real-world cases).
//
// Option B. ??
drop(<Option<()> as Foo>::copy_me(&Default::default()));
println!("{x}");
}
```
Rule for normalization
https://github.com/rust-lang/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-prove/src/prove/prove_normalize.rs#L35-L48
example where proof objects or "recording used candidates" is difficult: https://github.com/lcnr/random-rust-snippets/issues/2
- negative impls
### new solver dealing with alias bounds
- alias bound only works for `<T as Trait>::Assoc: Send` if `T: Trait` is proven using param env or alias bound candidates.
- for builtin impls we currently just assume alias bound even from builin impl candidates
- for default associated types :shrug: also allow alias bound, even if unsound, because specialization is unstable
### negative impls meh
- https://github.com/rust-lang/rust/pull/111308
```rust
impl<T: FnPtr> Debug for T { .. }
```
```rust
trait Foo {}
trait NegImpld {}
impl !NegImpld for u32 {}
impl<T: NegImpld> Foo for T {}
impl<T: Foo> Bar for T {}
impl Bar for u32 {}
```
niko: what stops you from adding `impl Foo for u32` in future release? If you could do this...
```rust
impl<T: !NegImpld> !Foo for T { }
```
the overlap we get...
```rust
// builtin
impl<A: ?Sized> !FnPtr for &A {}
impl<A: ?Sized, B: ?Sized> PartialEq<&B> for &A {}
impl<F: FnPtr> PartialEq for F {}
```
...this should work? Proving `F = &A, F: !FnPtr` should be possible.
## 2023-05-26
- mir formality things of interest
- implied bounds
- environment elaboration
- coinductive matching
- type relations?
- overall structure
- terms
- judgments
- coherence
- coherence mode
- lazy normalization / alias equality
- fuzzing
- new solver:
- https://github.com/rust-lang/trait-system-refactor-initiative/issues
- how coherence is implemented
- other interesting topics
- subtyping and the "simplesub" algorithm (leave this out)
```rust
trait Foo { }
impl Foo for () { }
impl<T: Foo> Foo for Option<T> { }
fn test<X: Foo>() { }
fn main() { test::<Option<()>>(); }
```
```rust
trait Foo: Bar { }
fn is_foo<X: Foo>() { is_bar::<X>()}
fn is_bar<X: Bar>() { }
```
```rust
#[rustc_coinductive]
trait Coinductive { }
impl Coinductive for () { }
impl<T> Coinductive for Option<T>
where
T: Coinductive
{ }
impl<T> Coinductive for List<T>
where
Option<List<T>>: Coinductive
{ }
struct List<T> { next: Option<List<T>> }
fn test<X: Coinductive>() { }
fn main() { test::<Option<List<()>>>(); }
```
- PR to talk through: https://github.com/rust-lang/rust/pull/111881
- https://github.com/rust-lang/rust/commit/5c200d88a91b75bd0875b973150655bd581ef97a
- https://github.com/rust-lang/rust/commit/cfc230d54188d9c7ed867a9a0d1f51be77b485f9
- for auto traits partial negative impls are very sus and forbidding them is nice
```rust
trait Foo { }
trait Bar { }
// Foo is never implemented if Bar is implemented
impl<T> !Foo for T where T: Bar { }
// Foo is implemented for u32
impl<T> Foo for Vec<T> where T: Debug { }
```
* We need to prove:
* For all positive impls of Foo:
* there is no negative impl of Foo that applies
* `forall<T>`
* `if(WC)`
* `not { Vec<T>: !Foo }`
* not
* `exists<T>`
* `if(T: Debug)` // <-- environment has an inference variable in it
* `Vec<T>: !Foo`
* If we know all negative impls are always applicable
* we can just unify things
* is `MyType<T>: Trait<U>` always applicable
* what do we do with alias types?
* we should make an example
```rust
trait Foo<X> { }
trait Bar { }
struct RequiresIterator<T: Iterator> { t: T }
// Foo is never implemented if Bar is implemented
impl<A> !Foo<A::Item> for RequiresIterator<A> {
}
// Foo is implemented for u32
impl<B> Foo<B> for RequiresIterator<vec::IntoIter<B>> where B: Debug {
// Equating will have to prove
// * `A = vec::IntoIter<B>`
// * `A::Item = B`
// * `vec::IntoIter<B>: Iterator<Item = B>`
// * true
}
impl<B, C> Foo<C> for RequiresIterator<vec::IntoIter<B>> where B: Debug {
// Equating will have to prove
// * `A = vec::IntoIter<B>`
// * `A::Item = B`
// * `vec::IntoIter<B>: Iterator<Item = B>`
// * true
}
impl<B> Foo<u32> for RequiresIterator<vec::IntoIter<B>> where B: Debug {
// Equating will have to prove
// * `?a = vec::IntoIter<?b>`
// * coherence-mode:
// * `<?a>::Item = u32`
// * `vec::IntoIter<?b>: Iterator<Item = u32>`
//
}
```
* final lcnr thought: could only consider stuff always applicable if the self type is `SimplifiedType` with identity substs (and trait args all all unique params), then we can have a quick hashmap lookup to check whether a trait is guaranteed to not be implemented
- stash: lcnr worries that negative impls being both a stability guarantee and used to disable auto traits will cause libraries to end up with breaking changes where there shouldn't be any
- response: agreed, I kind of want `impl ?Foo`
## 2023-05-05
- Rust will get old
- are we still growing and are new features important for it
- niko: yes-ish
- lcnr: no-ish
- async in trait is necessary for growth
- also, exponential size blowup
very unhelpful notes :tada:
## 2023-04-10
Item bounds for opaque types and soundness
https://github.com/rust-lang/rust/issues/109387
```rust
type Foo<T> = impl Debug;
fn define_foo<T: Ord>() -> Foo<T> {
BTreeMap::new()
} // doesn't compile
```
```rust
type Foo<T> = H as impl Debug where WC;
```
When is this "well formed" and what can we assume...
* `forall<T> { WC => H: Debug, WF(H) }`
```rust
trait Trait<T> {
type Assoc: Default;
}
type Ty<T> = H as impl Trait<T> where WC;
```
```rust
forall<T> { WC => H: Trait<T>, WF(H) }
```
when we have `Ty<T>: Trait<T>`
```
IsImplemented(T: Trait) :-
HasImpl(T: Trait),
WellFormed(T: Trait) // includes proving projection bounds
```
in the full example:
```rust
trait Trait<T> {
type Assoc: Default;
}
type Ty<T> = T as impl Trait<T>;
impl<T> Trait<T> for T
where
<Ty<T> as Trait<T>>::Assoc: Default,
{
type Assoc = <Ty<T> as Trait<T>>::Assoc;
}
```
Proving `Ty<T>` is well-formed--
* prove `T: Trait<T>`
* apply impl ...
* then we have to prove `<T as Trait<T>>::Assoc: Default`
* normalize this to `<Ty<T> as Trait<T>>::Assoc: Default`
* prove this via a built-in rule that permits you to assume opaque is WF
Conclusion:
* the right way to think about opaque types is as module-level generics
* where:
* during type-checking, we assume WF(O) for any opaque type O
* and we have a rule that says WF(O) => (O: Trait)
* during reveal-all, we instead have `normalize(O => Hidden)`
* and so the WF(O) => O: Trait rule is not useful
* and we have to prove everything based on the hidden type alone
* sound, but you may get post-momorphization errors
* in the same way that you can write circular impls that compile but cannot be used
can write a pass post borrowck which checks opaques being able to normalize them and without assuming `WF(O)`.
Question: what about multiple
#### uniquifying lifetimes
`<?0 as Trait<'a>>::Assoc == <?0 as Trait<'a>>::Assoc`
- uniquify `exists<T, '0, '1> <T as Trait<'0>>::Assoc == <T as Trait<'1>>::Assoc`
- equating projection substs adds external constraint `'0 == '1` => non trivial
## 2023-03-24
Niko's proposal for a topic:
* specialization, auto traits, generators, oh my!
lcnr's proposal for a topic:
* intersections in external constraints
## 2023-03-17
lcnr: "alias bounds"
https://github.com/lcnr/solver-woes/issues/9#issuecomment-1456284249
nikomatsakis: a-mir-formality update
https://github.com/nikomatsakis/a-mir-formality/blob/75ae1aaf323e36caa789db0edadce0886cd51721/crates/formality-prove/src/prove/prove_wc.rs#L46-L57
Example:
* Prove `{} => {u32: PartialEq}` where it's not true :)
* try with "trait implied bound":
* "trait Eq: PartialEq"
* "u32: PartialEq => u32: PartialEq" ok
* "u32: Eq"
* try with "impl"
* `impl Eq for u32` // suppose here is no `impl PartialEq for u32`
* no where clauses, so trivially true
* prove the trait superbounds:
* prove "u32: PartialEq" -- cycle, error
* try with "impl"
* there is no impl, so this fails
* cannot prove
* Prove `{} => {u32: PartialEq}` where it IS true
* try with "trait implied bound":
* "trait Eq: PartialEq"
* "u32: PartialEq => u32: PartialEq" ok
* "u32: Eq"
* try with "impl"
* `impl Eq for u32` // suppose here is no `impl PartialEq for u32`
* no where clauses, so trivially true
* prove the trait superbounds:
* prove "u32: PartialEq" -- cycle, error
* try with "impl"
* succeeds, no where-clauses, no supertraits
* cannot prove
* Prove `forall T. {T: Eq} => {T: PartialEq}`
* try with "trait implied bound":
* "trait Eq: PartialEq"
* "T: PartialEq => T: PartialEq" ok
* "T: Eq"
* ["assumption"](https://github.com/nikomatsakis/a-mir-formality/blob/75ae1aaf323e36caa789db0edadce0886cd51721/crates/formality-prove/src/prove/prove_wc.rs#L39-L44)
* true
- minimal param env https://hackmd.io/5IdqPjpCQ5-19GWTBnDdyA
## 2023-02-13
## 2023-01-26
region stuff: https://hackmd.io/DiPJDUCFS4CN-9LI4l2W4A?view#Region-obligations-leak-check
```rust
trait Direct<'a, 'b> where 'a: 'b { }
trait Indirect<'a, 'b>: Direct<'a, 'b> { }
// Goal
for<'a, 'b> Direct<'a, 'b> // false
for<'a, 'b> if ('a: 'b) { Direct<'a, 'b> } // true
for<'a, 'b> if ('a: 'b) { Indirect<'a, 'b> } // true
```
`u32: Trait<'a, 'b> where 'a: 'b`
`i32: Trait<'a, 'b>`
if we ask `for<'a, 'b> _: Trait<'a, 'b>`
niko's hackmd
https://hackmd.io/jqiadXq4SJ67DhjQqUFnew
## 2022-12-20
Coinduction and things
- https://hackmd.io/cnX6oA28RwOPfRCTeyLw4Q?view
## 2022-06-30
cases where it might be nice to discuss
* rust zulip
* if emailing GH sponsor people, being able to say "thank you I have contracts"
* would publish on GH page, as long as lcnr doesn't interact with people in some way, have to pay taxes
* or on twitter
* blog post saying "hey I did Rust full time and I had these sorts of clients"
* private discussion with other potential clients
* "lcnr GmbH" webpage as a list of clients
## 2022-06-02
- hackmd: https://hackmd.io/3zu19-LFSxmd2e4yHdNInw
```rust
trait Super {
type Assoc;
}
trait Trait: Super<Assoc = Self> {}
```
---
```rust
trait Foo {
fn foo(&self) -> impl Iterator<Item = u32> + '_;
}
trait Foo {
type foo<'b>: Iterator<Item = u32> + 'b;
fn foo(&self) -> Self::foo<'_>;
}
x: &dyn Foo
<dyn Foo as Foo>::foo == dyn* Iterator<Item = u32>
trait DynFoo: Foo<foo = dyn* Iterator<Item = u32>> {
}
impl<T> DynFoo for T
where
T: Foo
{
type foo = dyn* Iterator<Item = u32>;
}
```
annoying `Relate`: https://github.com/rust-lang/rust/blob/9598b4b594c97dff66feb93522e22db500deea07/compiler/rustc_middle/src/ty/relate.rs#L718-L724
elaborate lattice.
my concern wrt suppression
```rust
trait Super {
type Assoc;
}
trait Trait: Super<Assoc = u32> {}
fn foo<T: Trait + ?Sized>() -> <T as Super>::Assoc {
1u32
}
```
```rust
trait Super {
type Assoc1;
type Assoc2;
}
trait Trait: Super<Assoc2 = Self::Assoc1> { }
trait Trait: Super<Assoc2 = Self> { }
dyn Trait<Assoc1 = u32, Assoc2 = u64>
```
Requirement:
* if you have a `dyn Foo<X = ...>`
* then for that to be WF, `dyn Foo<X = ...>: Foo<X = ...>` must hold
* which means
* `dyn Foo<X = ...>: Foo` <-- will fail for all the bad cases we have identified so far
* `<dyn Foo<X = ...> as Foo>::X = ...`
* then for that to be WF, `dyn Foo<X = ...>: Foo<X = ...>` must hold
https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=b7b533af61d452da7edec4c619a07bdb
---
current state is that *somehow* we detect that `dyn Trait<Assoc2 = ...>: Trait` does not satisfy the super bound:
https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=10590d62d211b378c16fafe69d3bb80e
but
```rust
trait Super {
type Assoc1: ?Sized;
}
trait Trait: Super<Assoc1 = Self> { }
dyn Trait<Assoc1 = X>
// should this be illegal?
//
// we will try to prove that
//
// * `dyn Trait<Assoc1 = X>: Trait`
// * `dyn Trait<Assoc1 = X>: Super<Assoc1 = dyn Trait<Assoc1 = X>>`
// * this will fail
//
// there is no finite type that will satisfy this
//
// mu X: dyn Trait<Assoc1 = X> // if we had this ...
fn foo<T: Trait + ?Sized>() {
// cannot call `foo` with `T = dyn Trait<Assoc1 = X>`
// because I cannot prove that `X = T`
}
// if we had recursive types like mu above...
fn foo<T: Trait + ?Sized>(t: T::Assoc1) -> T {
// could call `foo` with `T = mu M. dyn Trait<Assoc1 = M>`
// but---
//
// * (A) how do I get an instance of that type?
// -- we think it's impossible to instantiate
// * (B) .. so what?
}
struct M {
}
impl Trait for M {
type Assoc1 = mu M. dyn Trait<M = M>; // will fail
}
```
---
Conclusions:
* if we say that you can have `dyn Foo` for ANY trait or trait bounds Foo, and you don't have to list all associated types either
* we add a check that `dyn Foo: Foo` which also checks that
* and checks that `Foo` "fully holds" (including where clauses)
* and checks that all items on Foo are "dyn safe"
* for methods, they have to be "vtable-able"
* for associated types, they have to normalize to "something" (*)
* (optional) we make the methods of `Foo` available as inherent methods of `dyn Foo` so long as they meet some criteria
* (dyn Foo).len() ==> `<dyn Foo as Foo>::len(x)`
* for that to work when `dyn Foo: Foo` doesn't hold, need inherent method
```rust
// be wary of loops
impl<T: Super> Super for T {
type Assoc1 = T::Assoc1;
}
```
## 2022-05-26
- bevy has pretty much `HashMap<TypeId, ...>`
- access via `iter_component<T: IsInQuery>` where `IsInQuery` means that the `TypeId` is in the hashmap.
- good bye subtyping in equate: https://github.com/rust-lang/rust/compare/master...lcnr:equate-uwu-uwu
Related case:
```
// same value, upcast to distinct type-ids
let v: fn(&u8) = ...;
let w: fn(&'static u8) = v;
```
```rust
trait Trait {
fn foo<'a>(x: &'a (), y: &'a ());
}
impl Trait for () {
fn foo(x: &(), y: &()) {}
}
```
```rust
// Compiles today
trait Trait {
fn foo<'a>(x: &'a (), y: &'a ()) -> &'a ();
}
impl Trait for () {
fn foo<'a>(x: &'a (), y: &()) -> &'a () { panic!() }
}
```
Space of solutions:
* Separate *type equality* from `T <: U` and `U <: T`
* Acknowledge that `TypeId` is partial
* Some alternative to `TypeId`...?
## 2022-05-19
- https://github.com/rust-lang/rust/pull/97024
- `Placeholder` to `Universal` t-types MCP
- https://github.com/rust-lang/rust/pull/96515
- https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/ty/context/struct.CanonicalUserTypeAnnotation.html
should error:
```rust
let (mut a, _): (&'static u32, u32) = (&22, 44);
let b = 66;
a = &b;
```
should not:
```rust
let (mut a, _) = (&22, &44): (&'static u32, &'static u32);
let b = 66;
a = &b;
```
We have
UserTy: `&'a u32`
inferred_ty `&'static u32` (current) replaced with ``&'?x u32`
input: `&'static u32`
UserTy == inferred_ty
inferred_ty :> input
```rust
fn test<'a>(input: &'a u32) {
let x: &'static u32 = &22;
let (mut y,): (&'a u32,)= (x,);
y = input;
}
```
```
| Free Region Mapping
| '_#0r | Global | ['_#0r, '_#2r, '_#1r]
| '_#1r | Local | ['_#2r, '_#1r]
| '_#2r | Local | ['_#2r]
|
| Inferred Region Values
| '_#0r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#1r | U0 | {bb0[0..=24], '_#1r}
| '_#2r | U0 | {bb0[0..=24], '_#2r}
| '_#3r | U0 | {}
| '_#4r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#5r | U0 | {}
| '_#6r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#7r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#8r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#9r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#10r | U0 | {bb0[0..=24], '_#1r}
| '_#11r | U0 | {bb0[0..=24], '_#1r}
| '_#12r | U0 | {bb0[0..=24], '_#1r}
| '_#13r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#14r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#15r | U0 | {bb0[0..=24], '_#1r}
| '_#16r | U0 | {bb0[0..=24], '_#1r}
| '_#17r | U0 | {bb0[0..=24], '_#1r}
| '_#18r | U0 | {bb0[0..=24], '_#1r}
| '_#19r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#20r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#21r | U0 | {bb0[0..=24], '_#0r, '_#1r, '_#2r}
| '_#22r | U0 | {bb0[0..=24], '_#1r}
| '_#23r | U0 | {bb0[0..=24], '_#1r}
|
| Inference Constraints
| '_#0r live at {bb0[0..=24]}
| '_#1r live at {bb0[0..=24]}
| '_#2r live at {bb0[0..=24]}
| '_#7r live at {bb0[2]}
| '_#8r live at {bb0[3]}
| '_#9r live at {bb0[4]}
| '_#10r live at {bb0[10]}
| '_#11r live at {bb0[15]}
| '_#0r: '_#20r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#0r: '_#21r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#1r: '_#12r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:1:13: 1:18) (/Users/nikomat/tmp/foo.rs:1:13: 1:18 (#0)
| '_#1r: '_#22r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:3:19: 3:29) (/Users/nikomat/tmp/foo.rs:3:19: 3:29 (#0)
| '_#1r: '_#23r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:3:19: 3:29) (/Users/nikomat/tmp/foo.rs:3:19: 3:29 (#0)
| '_#4r: '_#6r due to Boring at Single(bb0[2]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#6r: '_#7r due to Boring at Single(bb0[2]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#7r: '_#6r due to Boring at Single(bb0[2]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#7r: '_#19r due to Boring at Single(bb0[2]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#8r: '_#14r due to Boring at Single(bb0[3]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#9r: '_#13r due to Assignment at Single(bb0[4]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#10r: '_#17r due to Boring at Single(bb0[10]) (/Users/nikomat/tmp/foo.rs:3:32: 3:33 (#0)
| '_#11r: '_#15r due to Assignment at Single(bb0[15]) (/Users/nikomat/tmp/foo.rs:3:10: 3:15 (#0)
| '_#11r: '_#16r due to Boring at Single(bb0[15]) (/Users/nikomat/tmp/foo.rs:3:10: 3:15 (#0)
| '_#12r: '_#1r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:1:13: 1:18) (/Users/nikomat/tmp/foo.rs:1:13: 1:18 (#0)
| '_#12r: '_#18r due to Boring at Single(bb0[18]) (/Users/nikomat/tmp/foo.rs:4:9: 4:14 (#0)
| '_#13r: '_#10r due to Boring at Single(bb0[10]) (/Users/nikomat/tmp/foo.rs:3:32: 3:33 (#0)
| '_#13r: '_#20r due to TypeAnnotation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#13r: '_#21r due to TypeAnnotation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#14r: '_#9r due to Boring at Single(bb0[4]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#15r: '_#22r due to TypeAnnotation at All(/Users/nikomat/tmp/foo.rs:3:19: 3:29) (/Users/nikomat/tmp/foo.rs:3:19: 3:29 (#0)
| '_#16r: '_#11r due to Boring at Single(bb0[15]) (/Users/nikomat/tmp/foo.rs:3:10: 3:15 (#0)
| '_#16r: '_#23r due to TypeAnnotation at All(/Users/nikomat/tmp/foo.rs:3:19: 3:29) (/Users/nikomat/tmp/foo.rs:3:19: 3:29 (#0)
| '_#17r: '_#16r due to Boring at Single(bb0[11]) (/Users/nikomat/tmp/foo.rs:3:31: 3:35 (#0)
| '_#18r: '_#15r due to Assignment at Single(bb0[19]) (/Users/nikomat/tmp/foo.rs:4:5: 4:14 (#0)
| '_#19r: '_#8r due to Boring at Single(bb0[3]) (/Users/nikomat/tmp/foo.rs:2:27: 2:30 (#0)
| '_#20r: '_#0r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#20r: '_#13r due to TypeAnnotation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#21r: '_#0r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#21r: '_#13r due to TypeAnnotation at All(/Users/nikomat/tmp/foo.rs:2:12: 2:24) (/Users/nikomat/tmp/foo.rs:2:12: 2:24 (#0)
| '_#22r: '_#1r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:3:19: 3:29) (/Users/nikomat/tmp/foo.rs:3:19: 3:29 (#0)
| '_#22r: '_#15r due to TypeAnnotation at All(/Users/nikomat/tmp/foo.rs:3:19: 3:29) (/Users/nikomat/tmp/foo.rs:3:19: 3:29 (#0)
| '_#23r: '_#1r due to BoringNoLocation at All(/Users/nikomat/tmp/foo.rs:3:19: 3:29) (/Users/nikomat/tmp/foo.rs:3:19: 3:29 (#0)
|
| User Type Annotations
| 0: Canonical { max_universe: U0, variables: [], value: Ty(&ReStatic u32) } at /Users/nikomat/tmp/foo.rs:2:12: 2:24
| 1: Canonical { max_universe: U0, variables: [], value: Ty(&ReStatic u32) } at /Users/nikomat/tmp/foo.rs:2:12: 2:24
| 2: Canonical { max_universe: U0, variables: [], value: Ty((&ReFree(DefId(0:3 ~ foo[61e2]::test), BrNamed(DefId(0:4 ~ foo[61e2]::test::'a), 'a)) u32,)) } at /Users/nikomat/tmp/foo.rs:3:19: 3:29
| 3: Canonical { max_universe: U0, variables: [], value: Ty((&ReFree(DefId(0:3 ~ foo[61e2]::test), BrNamed(DefId(0:4 ~ foo[61e2]::test::'a), 'a)) u32,)) } at /Users/nikomat/tmp/foo.rs:3:19: 3:29
fn test(_1: &'_#12r u32) -> () {
debug input => _1; // in scope 0 at /Users/nikomat/tmp/foo.rs:1:13: 1:18
let mut _0: (); // return place in scope 0 at /Users/nikomat/tmp/foo.rs:1:29: 1:29
let _2: &'_#13r u32 as UserTypeProjection { base: UserType(0), projs: [] }; // in scope 0 at /Users/nikomat/tmp/foo.rs:2:9: 2:10
let _3: &'_#14r u32; // in scope 0 at /Users/nikomat/tmp/foo.rs:2:27: 2:30
let _4: u32; // in scope 0 at /Users/nikomat/tmp/foo.rs:2:28: 2:30
let mut _6: (&'_#16r u32,); // in scope 0 at /Users/nikomat/tmp/foo.rs:3:31: 3:35
let mut _7: &'_#17r u32; // in scope 0 at /Users/nikomat/tmp/foo.rs:3:32: 3:33
let mut _8: &'_#18r u32; // in scope 0 at /Users/nikomat/tmp/foo.rs:4:9: 4:14
let mut _9: &'_#19r u32; // in scope 0 at /Users/nikomat/tmp/foo.rs:2:27: 2:30
scope 1 {
debug x => _2; // in scope 1 at /Users/nikomat/tmp/foo.rs:2:9: 2:10
let mut _5: &'_#15r u32 as UserTypeProjection { base: UserType(2), projs: [Field(field[0], ())] }; // in scope 1 at /Users/nikomat/tmp/foo.rs:3:10: 3:15
scope 2 {
debug y => _5; // in scope 2 at /Users/nikomat/tmp/foo.rs:3:10: 3:15
}
}
bb0: {
StorageLive(_2); // bb0[0]: scope 0 at /Users/nikomat/tmp/foo.rs:2:9: 2:10
StorageLive(_3); // bb0[1]: scope 0 at /Users/nikomat/tmp/foo.rs:2:27: 2:30
_9 = const Const(Unevaluated(Unevaluated { def: WithOptConstParam { did: DefId(0:3 ~ foo[61e2]::test), const_param_did: None }, substs: [], promoted: Some(promoted[0]) }): &'_#7r u32); // bb0[2]: scope 0 at /Users/nikomat/tmp/foo.rs:2:27: 2:30
// mir::Constant
// + span: /Users/nikomat/tmp/foo.rs:2:27: 2:30
// + literal: Const { ty: &'_#7r u32, val: Unevaluated(test, [], Some(promoted[0])) }
_3 = &'_#8r (*_9); // bb0[3]: scope 0 at /Users/nikomat/tmp/foo.rs:2:27: 2:30
_2 = &'_#9r (*_3); // bb0[4]: scope 0 at /Users/nikomat/tmp/foo.rs:2:27: 2:30
FakeRead(ForLet(None), _2); // bb0[5]: scope 0 at /Users/nikomat/tmp/foo.rs:2:9: 2:10
AscribeUserType(_2, o, UserTypeProjection { base: UserType(1), projs: [] }); // bb0[6]: scope 0 at /Users/nikomat/tmp/foo.rs:2:12: 2:24
StorageDead(_3); // bb0[7]: scope 0 at /Users/nikomat/tmp/foo.rs:2:30: 2:31
StorageLive(_6); // bb0[8]: scope 1 at /Users/nikomat/tmp/foo.rs:3:31: 3:35
StorageLive(_7); // bb0[9]: scope 1 at /Users/nikomat/tmp/foo.rs:3:32: 3:33
_7 = &'_#10r (*_2); // bb0[10]: scope 1 at /Users/nikomat/tmp/foo.rs:3:32: 3:33
_6 = (move _7,); // bb0[11]: scope 1 at /Users/nikomat/tmp/foo.rs:3:31: 3:35
StorageDead(_7); // bb0[12]: scope 1 at /Users/nikomat/tmp/foo.rs:3:34: 3:35
AscribeUserType(_6, +, UserTypeProjection { base: UserType(3), projs: [] }); // bb0[13]: scope 1 at /Users/nikomat/tmp/foo.rs:3:19: 3:29
StorageLive(_5); // bb0[14]: scope 1 at /Users/nikomat/tmp/foo.rs:3:10: 3:15
_5 = (_6.0: &'_#11r u32); // bb0[15]: scope 1 at /Users/nikomat/tmp/foo.rs:3:10: 3:15
StorageDead(_6); // bb0[16]: scope 1 at /Users/nikomat/tmp/foo.rs:3:35: 3:36
StorageLive(_8); // bb0[17]: scope 2 at /Users/nikomat/tmp/foo.rs:4:9: 4:14
_8 = _1; // bb0[18]: scope 2 at /Users/nikomat/tmp/foo.rs:4:9: 4:14
_5 = move _8; // bb0[19]: scope 2 at /Users/nikomat/tmp/foo.rs:4:5: 4:14
StorageDead(_8); // bb0[20]: scope 2 at /Users/nikomat/tmp/foo.rs:4:13: 4:14
_0 = const ConstValue(Scalar(<ZST>): ()); // bb0[21]: scope 0 at /Users/nikomat/tmp/foo.rs:1:29: 5:2
StorageDead(_5); // bb0[22]: scope 1 at /Users/nikomat/tmp/foo.rs:5:1: 5:2
StorageDead(_2); // bb0[23]: scope 0 at /Users/nikomat/tmp/foo.rs:5:1: 5:2
return; // bb0[24]: scope 0 at /Users/nikomat/tmp/foo.rs:5:2: 5:2
}
}
```
- https://github.com/rust-lang/rust/pull/95309
## 2022-04-28
* Contract deliverables and work items:
* In coordination with Rust types team, deliver on roadmap to create next generation trait solver
* Author 3 public blog posts (one every 2 months), either on the Inside Rust blog or a personal blog, explaining the work that was done.
* How to debug #95763:
* your best friend is `-Zdump-mir=nll` and `-Zverbose`
* in the output you can see the constraints, the value of each variable, etc
* look into `apply_requirements`: error happens in parent function but constraint is from closure
## 2022-03-24
- lcnr: locals wf, needed for region obligations?
```rust=
fn foo<'a, 'b>(x: &'a (), y: &'b ()) {
let a = b;
// ^ ^ could check that the result of this expression is WF
// |
// and assume that whatever type we infer for a will be wf,
// because type check never successfully yields a non-wf type
needs_a_outlives_b(x, y);
// ^^^^^^^^^^^^^^^ we definitely check this
let x: T = y;
// ^ some special rule to check that this is wf?
}
fn needs_a_outlives_b(x: &'a (), y: &'b ())
where 'a: 'b {}
```
submitted https://github.com/rust-lang/rust/issues/95272
the outlives gets added here [pernosco](https://pernos.co/debug/htXeKc1a8UUuLCqIcSVm8w/index.html#f{m[Bbw,AA_,t[Ag,Bog5_,f{e[BaU,Ahk_,s{afzHi08AA,bUQ,uGMiXpg,oGMoPJQ___,v[{wrTY,v[{f'list',q'stdouterr',p{_,xAYag_,{f'container',q'stack',p{_,xAYag_,{f'list',q'alerts',p{_,xAYag___,{w2Wk,v[{f'source',q'source',p{_,xAYag____/)
which seems a bit fragile because it *looks* to be specialzed to `TyFnDef`...?
### const generics
https://github.com/rust-lang/project-const-generics/issues/43
https://github.com/rust-lang/project-const-generics/issues/37
## 2022-03-03
- for later [#94057](https://github.com/rust-lang/rust/pull/94057)
- this one now https://github.com/rust-lang/rust/pull/93856
- https://github.com/rust-lang/rust/issues/25860
```
in: for<'a, 'b> fn(&'a &'b(), &'b T) -> &'a T
out: fn(&'static &'static (), &'c T) -> &'static T
```
implied bounds for `in`: `'b: 'a`.
implied bounds for `out`: `'static: 'static`
outlives during unification: `'static: 'a`, `'static: 'b`, `'c: 'b`, `'a: 'static`
to prove: assuming `'static: 'a`, `'static: 'b`, `'c: 'b`, `'a: 'static`, `'static: 'static`, does `'b: 'a` hold?
Can't prove that -> error!
* `for<P_L...> T_L <: for<P_R...> T_R`
* forall P_R. exists P_L. T_L <: T_R
* `for<P_L...> if (I_L) T_L <: for<P_R...> if(I_R) T_R`
* `forall P_R. exists P_L. if(I_L) T_L <: if(I_R) T_R`
* `if(I_L) T_L <: if(I_R) T_R` if
* `T_L <: T_R`
* `I_R => I_L` or the other way around <-- not doing this today
```
in: for<'a, 'b> fn(&'a &'b (), &'b T) -> &'a T
out: for<'b> fn(&'b &'b (), &'b T) -> &'static T
```
implied bounds for `in`: `'b: 'a`
implied bounds for `out`: `'b: 'b`
outlives during unification: `'b: 'a'`, ... --> ok
## 2022-02-10
- projections `simplify_type`: https://github.com/rust-lang/rust/pull/92721
- debug assert stuff, keep projections.
- rename param
- implied bounds + variance https://github.com/rust-lang/rust/issue/25860
```rust
x: for<'a, 'b> fn(&'a &'b u32, &'a u32, &'b u32)
T = (P => T) // if P is true, the value is of type T; else, value is garbage
x: for<'a, 'b> (OK(&'a &'b u32, &'a u32, &'b u32) => fn(&'a &'b u32, &'a u32, &'b u32))
fn foo(&'a &'b u32, &'a u32, &'b u32)
where
OK(forall i. Ii, O)
P1 |- P
---------------
(P => T) <: (P1 => T)
T <: T
---------------
(P => T) <: (P => T1)
(Ty_1 <: Ty) ...
---------------
fn(Ty ...) <: fn(Ty_1 ...)
what does not hold is:
forall(T <: U) OK(U) |- OK(T)
```
Today in the compiler:
```rust
for<'a> fn(<&'a u32 as Something>::Bar)
// shorthand for
for<'a> (OK(<&'a u32 as Something>::Bar) => fn(<&'a u32 as Something>::Bar))
trait Something { } /* no impls at all */
// try to prove:
//
// For P => T
// Try to prove not { P } and warn if you succeed
```
### why implication types?
* https://tmandry.gitlab.io/blog/posts/2021-12-21-context-capabilities/
#### early vs late bound
```rust
fn foo<T>() -> T
where
T: Default
```
In Rust type system, we get:
```rust
struct Foo<T>
where // <-- "early bound"
T: Debug;
impl<T> Fn() for Foo<T>
where // <-- "late"
T: Debug,
{
type Output = T;
fn call(..) -> T {
T::default() // where does where clause go that lets this type check?
}
}
```
```rust
let t = foo::<NoDefault>;
// never call it, is this ok?
```
```rust
fn foo<T>(T)
where
T: Default
```
we could do this
```rust
struct Foo;
impl<T> Fn(T) for Foo
where // <-- "late"
T: Debug,
{
type Output = T;
fn call(..) -> T {
T::default() // where does where clause go that lets this type check?
}
}
```
```rust
let t = foo;
t(22);
t("foo");
```
not *quite* backwards compatible. No way to have turbofish, plus today this works:
```rust
let t = foo;
t(Some(22));
t(None);
```
in fact, with today's language, no way to specify T *explicitly*, must give arguments of valid type, e.g.
```rust
t(None::<i32>);
<Foo as Fn(Option<i32>)>::call(t, None)
```
---
### Implied bounds, how to think about it
```diff
Predicate:
OK(T)
| OK(P0: Trait<P1..Pn>)
OK(&'a T) :- OK(T), T: 'a.
For user defined types:
struct Foo<T: Debug> { }
OK(Foo<T>) :- T: Debug.
Implied bounds come in the reverse direction:
OK(&'a T) => T: 'a.
trait Foo<T>: Bar where T: Debug { }
OK(Self: Foo<T>) :- Self: Foo<T>, OK(Self: Bar), OK(T: Debug).
OK(Self: Foo<T>) => OK(Self: Bar).
```
```rust
trait GetItem {
type Item;
fn get<'b>(&self) -> &Self::Item
where
OK(&'b Self);
}
impl<'a, T> GetItem for &'a [T] {
type Item = T;
fn get<'b>(&'b self) -> &'b Self::Item
where
OK(&'b Self)
{
&self[0]
// This has the lifetime &'a T
// Need to know that 'a: 'b
}
}
OK(&'b &'a [T]) =>
&'a [T]: 'b =>
T: 'b, 'a: 'b
```
### Covariance in ret type bad
```rust
// we again have an implied `'input: 'out` bound, this time because of the return type
fn foo<'out, 'input, T>(_dummy: &'out (), value: &'input T) -> (&'out &'input (), &'out T) {
(&&(), value)
}
fn bad<'short, T>(x: &'short T) -> &'static T {
// instantiate `foo`
let foo1: for<'out, 'input> fn(&'out (), &'input T) -> (&'out &'input (), &'out T) = foo;
// instantiate 'out as 'static
let foo2: for<'input> fn(&'static (), &'input T) -> (&'static &'input (), &'static T) = foo1;
// function return types are covariant,
// go from 'static to 'input
let foo3: for<'input> fn(&'static (), &'input T) -> (&'input &'input (), &'static T) = foo2;
// instantiate 'input as 'short
let foo4: fn(&'static (), &'short T) -> (&'short &'short (), &'static T) = foo3;
// boom!
foo4(&(), x).1
}
```
## 2022-02-03
- reasons for const generics
- associated constants: https://docs.rs/odht/0.3.1/odht/trait.Config.html#associatedtype.EncodedKey
- cryptography
- r4linux https://github.com/Rust-for-Linux/linux/issues/2
- gfc and gacs rfc
- https://hackmd.io/DFl9YadqQviOv7RQoY1_Tg
* vision as we go
* status quo
* how do we write those examples today
* what are the problems we hit? which can't we do at all? which are awkward?
* one step forward
* we add generic constants plus the ability to use them as the value for a const generic
* we now have full expressiveness but things are not as ergonomic or obvious we might like
* shiny future
* generic impls over arrays
* standard things: Default, Clone, PartialOrd, Ord
* btree container code (try writing that for fun)
* linear algebra or other functions parameterized over constants like that
* sin lookup -- into some array
* something that builds a data structure at compilation time
* unknowns and interesting things
* equality
* pattern matching -- what happens when you match on patterns
* unsafe code and how it interacts
* what does unsafe mean in a const context
* trait impls
```rust
const fn multiply(x: usize, y: usize) -> usize { x * y }
const MULTIPLY<const A: usize, const B: usize>: usize = multiply(A, B);
macro_rules! const_fn {
(const fn $name:ident ($($a:ty),*) -> $r) {
}
}
```
## 2022-01-20
auto traits: https://github.com/rust-lang/rust/pull/85048
- biggest breakage: https://crates.io/crates/imagequant/4.0.0-beta.2
- file: https://github.com/ImageOptim/libimagequant/blob/main/src/seacow.rs
- error: https://crater-reports.s3.amazonaws.com/pr-85048/try%23dc0340a3a9e4e041da9a5966db8733ccb7ac87e0/reg/imagequant-4.0.0-beta.2/log.txt
- notify crate authors
- write lint
const generics shiny future
- lcnr blogpost: https://lcnr.de/blog/generic-const-expressions/
- reddit reactions: https://www.reddit.com/r/rust/comments/s6ti1a/a_path_towards_stable_generic_const_expressions/
### Regarding generic constants
We kind of already have them
```rust
trait Foo {
const C: Type;
}
<T as Foo>::C
```
how is that different from
```rust
const C<T>: Type;
```
Similarly
```rust
enum Option<T> {
None // kind of a generic constant
}
```
```rust
const DUMMY_VALUE<T>: Option<T> = None
```
### why not const fn
Initial proposal...
```
T = LexicalName<{P}>
| <P0 as Trait<P1..Pn>>::Foo<Pn..Pm>
P = T
| const C
C = X
| Literal
| Path
| Expr which does not reference generic parameters
Path = <P0 as Trait<P1..Pn>>::Foo<Pn..Pm>
| LexicalName<P0...Pm>
```
Niko proposed extending with
```
C = LexicalName::<{P}>({C}) | C_old
```
typechecking anon consts: https://github.com/rust-lang/rust/issues/79356
from
```rust=
#![feature(const_generics)]
#![allow(incomplete_features)]
struct Foo<T>(T);
fn test() where [u8; {
let _: Foo<[u8; 7]>;
3
}]: Sized {}
```
convert
```rust
struct Foo<T>(T);
const ARRAY_LENGTH: usize = {
let _: Foo<[u8; 7]>;
3
};
fn test() where [u8; ARRAY_LENGTH]: Sized {}
```
```rust
struct Foo<T>(T);
const ARRAY_LENGTH: usize = {
let _: Foo<[u8; 7]>;
3
}
const TEST<N: usize>: usize
where
[u8; {
let _: Foo<[u8; 7]>;
3
}]: Sized
= N + 1;
fn test() where [u8; ARRAY_LENGTH]: Sized {}
```
## 2022-01-13
```rust
trait Trait where Self: OtherTrait {}
```
prove that `T: Trait` holds
- show that `T: Trait` and `T: OtherTrait`
Under [the min_generic_const_exprs proposal](https://hackmd.io/utjHsFL8SWSu98kYfF99uQ?view), after name resolution, we can classify all legal generic constant as:
```
Constant = Value
| GenericConstant
GenericConstant = X
| CONSTANT<P0..Pm>
| <P0 as Trait<P1..Pn>>::CONSTANT<Pn..Pm>
where exists i. Pi references a generic const parameter in scope
Value = Expr // that does not reference any generic parameters in scope
```
Interesting design questions that remain
* evaluatable, what does WF mean
* extending the set of types that can be used as a constant
* structural equality <-> matching of constants
* `fn foo<const N: usize>()` allow `foo<_>()`
* `const ADD<const N: usize, const M: usize> = N + M`: `Add<N, 1>` vs `Add<1, N>`.
Niko wants:
* the ability to "take" the value of a const generic from an argument
* I don't care how we get it damn it
* `shuffle(x, 2)` not `shuffle::<2>(x)`
```rust
const ADD<N: usize, M: usize>: usize = N + M;
struct MyStruct<C: usize> ([u32; C]);
fn something<const N: usize>() {
let x: MyStruct<ADD<N, 1>> = ...;
let y: MyStruct<ADD<1, N>> = ...;
// do x and y have the same type?
}
```
### lcnr is working on polymorphization (!)
* two instances `A` and `B`
* is `A` a polymorphic version of `B`
* monomorphic subfunction outlining
current bug: check if `foo::<T, for<'a> fn(&'a ())>` is a polymorphic parent of `foo::<i32, fn(&'erased ())>`
* transform first to `for<> fn(foo::<T, for<'a> fn(&'a ())>)`
* transform second to `for<'a> fn(foo::<i32, fn(&'a ())>)`
* equality will fail
```
// Ownership (from a macro):
impl<'a, 'b, A, R> IntoWasmAbi for &'a (dyn Fn(A) -> R + 'b)
where
A: FromWasmAbi,
R: ReturnWasmAbi
{ /* ... */ }
// Explicitly writing the bound lifetime.
impl<'a, 'b, A, R> IntoWasmAbi for &'a (dyn for<'x> Fn(&'x A) -> R + 'b)
where
A: RefFromWasmAbi,
R: ReturnWasmAbi
{ /* ... */ }
```
current bug:
check if `foo::<'erased, 'erased>` is a polymorphic parent of `foo::<'erased, 'erased>`
* transform first to `for<'a, 'b> fn(foo::<'a, 'b>)`
* transform second to `for<'a, 'b> fn(foo::<'a, 'b>)`
* equality will fail
from https://gist.github.com/nikomatsakis/8bfda6c1119727e13ec6e98f33d2b696
idea:
* create an outermost binder and make each `'erased` a fresh lifetime in that binder
## 2022-01-11
* Last time we talked about moving closure upvars to typeck results or some other place
```rust
fn foo() {
let y = &x;
let mut z;
let x = || { drop(x); z = y; }
}
// desugar to
struct C<T> { t: T }
// with your PR struct C<&'y u32> { t: T }
impl<'a, 'b> FnOnce() for C<&'a u32, &'b u32>
where 'b: 'a {
}
```
* `min_generic_const_exprs`: https://hackmd.io/utjHsFL8SWSu98kYfF99uQ
```rust
trait Foo<'a> {
type Assoc;
}
fn something<'b, T: Foo<'b>>(x: &'b u32) -> impl Into<T::Assoc> {
// in theory, you could return a value whose type references `'b` here...
// ...but you can't.
}
// desugared to something like this and gets an error
type Something<T>: Into<T::Assoc>;
fn something<'b, T: Foo<'b>>(x: &'b u32) -> impl Into<T::Assoc> {
```
* short version: if, in a anonymous constant, we wind up referencing a parameter that is not "visible" from the syntax, we report an error and suggest a fix that rewrites `T::Assoc` to `<T as Foo<'b>>::Assoc`, side-stepping the problem
## 2021-08-18
* Reviewed https://github.com/rust-lang/rust/pull/87280
* How to do winnowing for marker traits
## 2021-07-21
* Discussing https://github.com/rust-lang/rust/pull/87280
* Question for Niko to investigate to his satisfaction:
* Why do we need "definitely needs subst"
Brainstorm of an idea
* unused parameters can prevent unification
* creating cycles
https://github.com/rust-lang/project-const-generics/blob/master/design-docs/anon-const-substs.md#unused-substs
```rust
#![feature(lazy_normalization_consts)]
struct P<T: ?Sized>([u8; 1 + 4], T);
fn main() {
let x: Box<P<[u8; 0]>> = Box::new(P(Default::default(), [0; 0]));
let _: Box<P<[u8]>> = x; //~ ERROR mismatched types
}
```
```rust
fn foo<T, U>()
where T: PartialEq<U> {}
```
could plausibly "remove" `U` from the list of generics and replace `T: SomeTrait<U>` with `exists<U> { T: SomeTrait<U> }`. `T::CONSTANT` might still be resolvable.
Google Drive
Gist
Clipboard
Sign in with Wallet
