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

 

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

&'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)?