Loading...

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

• ​​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)​?

​​