Universes and #57639

Universes_and_#57639.md

Universes and #57639

• Background #1:
  • Solving for<``'``a> { '``a: '``b }
  • Universes
  • Integration into rustc
• Background #2:
  • How rustc’s trait solver works
    • Candidates
    • Confirmation + fulfillment context
• How the interaction of these two points leads to #57639
  • what used to happen

This gist is associated with a YouTube video, which explains its contents.

---

Background #1

for<'a> fn(&'a u32) <: fn(&'b u32)

let x: for<'a> fn(&'a u32) = ...
let y: fn(&'b u32) = x;

• Subtyping T1 <: T2:

  • Yes

    • with these region constraints + fresh variables

  • No

  • similar to Polonius and Region Errors blog post

    &'a u32 <: &'b u32

    • Yes, if 'a: 'b

• subtype(T1, T2):

  • If T1 = &’a T1’ and T2 = &’b T2’

    • let C1 = subtype(T1’, T2’)
    • return C1 + { ‘a: ‘b }

  • If T1 = for<’a> fn(…):

    • Make a fresh inference variable ‘0
    • Replace ‘a with ’0 in the fn type yielding a type T1’
    • Relate T1’ to T2

  • If T1 = fn(A1) → B1, T2 = fn(A2) → B2:

    • no forall binders
    • subtype(A2, A1) + subtype(B1, B2)

    for<'a> fn(&'a u32) fn(&'0 u32) // 'a => '0 where '0 is a fresh variable

Applied to our original problem

for<``'``a> fn(&``'``a u32) <: fn(&``'``b u32)?

Yes, if:

'``0: '``b

---

fn(&'a u32) <: for<'b> fn(&'b u32)

• Introduce the idea of a placeholder and universes

  • “symbolic region”
  • maximally conservative

• Universes:

  • U0 (root universe)
    • U1 (add one fresh name to U0)
      • U2
    • U3

• when we have a forall on the supertype side:

  • Create a fresh universe U’ that extends the “current universe” U

    • add some placeholder names into U’ for each region

  • Replace the for<``'``b> with these placeholders

    • for<``'``b> fn(&``'``b u32)
      • fn(&``'``!1 u32)

  • Relate T1 and T2 as before

    fn(&'a u32) <: for<'b> fn(&'b u32) in U0 fn(&'a u32) <: fn(&'!1 u32) in U1 &'!1 u32 <: &'a u32 '!1: 'a in U1 // for<'b> { 'b: 'a } // error? // or at least it's an error if the fn is ever called

• Shifting to the implementation side of this:

  • Universe tree — we only keep a single integer

    for<'a> fn(&'a u32) <: for<'b> fn(&'b u32) in U0

    for<'a> fn(&'a u32) <: fn(&'!1 u32) in U1

    fn(&'0 u32) <: fn(&'!1 u32) in U1 the inf. variable '0 is in universe U1

    '!1: '0 // not an error because we can infer '0 to be '!1

    for<'a, 'b> fn(&'a u32, &'b u32)

    fn() -> &'0 u32 <: for<'b> fn() -> &'b u32

    fn() -> &'0 u32 <: fn() -> &'!1 u32 // in U1

    &'0 u32 <: &'!1 u32

    '0: '!1 // '!1 <= '0

---

Stepping back to “pure logic”

exists<A> { // A being in Universe 0
  forall<B> { // B being in Universe 1
    A = B // not so good
  }
}

forall<A> { // placeholder is in universe 1
  exists<B> { // variable is also in universe 1
    A = B // OK, B = A
  }
}

exists<A> {
  forall<B> { A = B } // index 1
  forall<C> { A = C } // index 2
}