owned this note   changed 3 months ago  
Linked with GitHub

lcnr nikomatsakis

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

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
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

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

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
}

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);
}

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 foois 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

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 `}

intrinsic fn call_boxed<F, A>(
	f: F,
	args: A
) -> Box<F::Output>
where
    F: FnOnce<A, Output: ?Sized>; // <-- not stable

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;
}

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

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

  • niko's sketch

  • things to be resolved

    • interaction with placeholders

2025-03-12

currently moving

unstable impls

  • boxy is mentoring the former (
    Image Not Showing Possible Reasons
    • The image file may be corrupted
    • The server hosting the image is unavailable
    • The image path is incorrect
    • The image format is not supported
    Learn More →
    )

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

#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
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).
  2. 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

niko reads

questions

trait Magic: Copy {}
impl<T: Magic> Magic for T {}
fn magic_copy<T: Magic>(x: T) -> (T, T) { (x, x) }

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)

// 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
}







trait Magic
where
    (Self: Magic) => (Self: Copy) // (Magic self -> Copy Self)
{
    
}

inductive Magic (self : Type) : Type where
| mk : (Magic self -> Copy self) -> Magic self

trait Magic {
    type Assoc<T: Magic>: Copy;
}

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

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
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
  • with what teams will
  • 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

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
        }
    }
}

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

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`
        }
    }
}

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"

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

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

// 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]
    }
}

// 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 }
    }
}

// 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

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

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

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.

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

fn foo<'a>() -> impl Sized + 'a {
    if false {
        let _: &'a () = foo(); // error
    }

    &()
}

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)

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

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)
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:

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:

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

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

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

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

How to handle alias bounds:

why no check on normalization:

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

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
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
      *
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
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>() {}

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 {
    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

possible project goals

  • cycle semantics ("coinduction")

implementable trait aliases

pub trait LocalService {
    async fn method();
}

pub trait Service = LocalService<method(..): Send> + Send;

for users

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

struct MyType;

impl Send for MyType {
    // look ma, a safe impl
}

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

// 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
// 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

  • 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

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.

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
      Image Not Showing Possible Reasons
      • The image file may be corrupted
      • The server hosting the image is unavailable
      • The image path is incorrect
      • The image format is not supported
      Learn More →

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…

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>)

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
trait Trait {
    type Assoc;
}

type Alias = <() as Trait>::Assoc;
impl Trait for () {
    type Assoc = Vec<Alias>;
}

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.

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

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)






enum Predicate {
    TraitRef(TraitRef),
    All(Vec<Predicate>),
    Not(Rc<Predicate>)
}

might be easier if we do







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
      1. here's a program mir-formality rejects, does rustc also reject
      1. 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

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
  • 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

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
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>();
}

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
      Image Not Showing Possible Reasons
      • The image file may be corrupted
      • The server hosting the image is unavailable
      • The image path is incorrect
      • The image format is not supported
      Learn More →
      also allow alias bound, even if unsound, because specialization is unstable

negative impls meh

impl<T: FnPtr> Debug for T { .. }

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…

impl<T: !NegImpld> !Foo for T { }

the overlap we get…

// 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:
  • other interesting topics
    • subtyping and the "simplesub" algorithm (leave this out)
trait Foo { }
impl Foo for () { }
impl<T: Foo> Foo for Option<T> { }
fn test<X: Foo>() { }
fn main() { test::<Option<()>>(); }

trait Foo: Bar { }
fn is_foo<X: Foo>() { is_bar::<X>()}
fn is_bar<X: Bar>() { }

#[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<()>>>(); }

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
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

Image Not Showing Possible Reasons
  • The image file may be corrupted
  • The server hosting the image is unavailable
  • The image path is incorrect
  • The image format is not supported
Learn More →

2023-04-10

Item bounds for opaque types and soundness

https://github.com/rust-lang/rust/issues/109387

type Foo<T> = impl Debug;

fn define_foo<T: Ord>() -> Foo<T> {
    BTreeMap::new()
} // doesn't compile

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) }
trait Trait<T> {
    type Assoc: Default;
}

type Ty<T> = H as impl Trait<T> where WC;

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:

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"

2023-02-13

2023-01-26

region stuff: https://hackmd.io/DiPJDUCFS4CN-9LI4l2W4A?view#Region-obligations-leak-check

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

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

trait Super {
    type Assoc;
}

trait Trait: Super<Assoc = Self> {}

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

trait Super {
    type Assoc;
}

trait Trait: Super<Assoc = u32> {}

fn foo<T: Trait + ?Sized>() -> <T as Super>::Assoc {
    1u32
}

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

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
// 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;

trait Trait {
    fn foo<'a>(x: &'a (), y: &'a ());
}

impl Trait for () {
    fn foo(x: &(), y: &()) {}
}

// 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

should error:

let (mut a, _): (&'static u32, u32) = (&22, 44);
let b = 66;
a = &b;

should not:

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 u32input:&'static u32`

UserTy == inferred_ty
inferred_ty :> input

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
    }
}

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?















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

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

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

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:

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?

early vs late bound

fn foo<T>() -> T
where
    T: Default

In Rust type system, we get:

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?
    }
}

let t = foo::<NoDefault>;
// never call it, is this ok?

fn foo<T>(T)
where
    T: Default

we could do this

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?
    }
}

let t = foo;
t(22);
t("foo");

not quite backwards compatible. No way to have turbofish, plus today this works:

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.

t(None::<i32>);
<Foo as Fn(Option<i32>)>::call(t, None)

Implied bounds, how to think about it

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).

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

// 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

  • 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
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

Regarding generic constants

We kind of already have them

trait Foo {
    const C: Type;
}

<T as Foo>::C

how is that different from

const C<T>: Type;

Similarly

enum Option<T> {
    None // kind of a generic constant
}

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










#![feature(const_generics)]
#![allow(incomplete_features)]

struct Foo<T>(T);

fn test() where [u8; {
    let _: Foo<[u8; 7]>;
    3
}]: Sized {}

convert

struct Foo<T>(T);

const ARRAY_LENGTH: usize = {
    let _: Foo<[u8; 7]>;
    3
};

fn test() where [u8; ARRAY_LENGTH]: Sized {}

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

trait Trait where Self: OtherTrait {}

prove that T: Trait holds

  • show that T: Trait and T: OtherTrait

Under the min_generic_const_exprs proposal, 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)
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
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 {
    
}

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

2021-07-21

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

#![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
}

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.

Select a repo