@@ -72,11 +72,11 @@ the same lifetime, but not the reverse.
7272Here is the algorithm we use to perform the subtyping check:
7373
74741 . Replace all bound regions in the subtype with new variables
75- 2 . Replace all bound regions in the supertype with skolemized
76- equivalents. A "skolemized " region is just a new fresh region
75+ 2 . Replace all bound regions in the supertype with placeholder
76+ equivalents. A "placeholder " region is just a new fresh region
7777 name.
78783 . Check that the parameter and return types match as normal
79- 4 . Ensure that no skolemized regions 'leak' into region variables
79+ 4 . Ensure that no placeholder regions 'leak' into region variables
8080 visible from "the outside"
8181
8282Let's walk through some examples and see how this algorithm plays out.
@@ -95,7 +95,7 @@ like so:
9595Here the upper case ` &A ` indicates a * region variable* , that is, a
9696region whose value is being inferred by the system. I also replaced
9797` &b ` with ` &x ` ---I'll use letters late in the alphabet (` x ` , ` y ` , ` z ` )
98- to indicate skolemized region names. We can assume they don't appear
98+ to indicate placeholder region names. We can assume they don't appear
9999elsewhere. Note that neither the sub- nor the supertype bind any
100100region names anymore (as indicated by the absence of ` < ` and ` > ` ).
101101
@@ -181,15 +181,15 @@ the first example, you had two functions:
181181 for<'a> fn(&'a T) <: for<'b> fn(&'b T)
182182
183183and hence ` &A ` and ` &x ` were created "together". In general, the
184- intention of the skolemized names is that they are supposed to be
184+ intention of the placeholder names is that they are supposed to be
185185fresh names that could never be equal to anything from the outside.
186186But when inference comes into play, we might not be respecting this
187187rule.
188188
189189So the way we solve this is to add a fourth step that examines the
190- constraints that refer to skolemized names. Basically, consider a
190+ constraints that refer to placeholder names. Basically, consider a
191191non-directed version of the constraint graph. Let ` Tainted(x) ` be the
192- set of all things reachable from a skolemized variable ` x ` .
192+ set of all things reachable from a placeholder variable ` x ` .
193193` Tainted(x) ` should not contain any regions that existed before the
194194step at which the skolemization was performed. So this case here
195195would fail because ` &x ` was created alone, but is relatable to ` &A ` .
0 commit comments