@@ -122,7 +122,7 @@ stack, for example). But *how* do we reject it and *why*?
122
122
When we type-check ` main ` , and in particular the call ` bar(foo) ` , we
123
123
are going to wind up with a subtyping relationship like this one:
124
124
125
- ``` txt
125
+ ``` text
126
126
fn(&'static u32) <: for<'a> fn(&'a u32)
127
127
---------------- -------------------
128
128
the type of `foo` the type `bar` expects
@@ -137,7 +137,7 @@ regions" -- they represent, basically, "some unknown region".
137
137
138
138
Once we've done that replacement, we have the following relation:
139
139
140
- ``` txt
140
+ ``` text
141
141
fn(&'static u32) <: fn(&'!1 u32)
142
142
```
143
143
@@ -151,7 +151,7 @@ subtypes, we check if their arguments have the desired relationship
151
151
(fn arguments are [ contravariant] ( ./appendix-background.html#variance ) , so
152
152
we swap the left and right here):
153
153
154
- ``` txt
154
+ ``` text
155
155
&'!1 u32 <: &'static u32
156
156
```
157
157
@@ -201,7 +201,7 @@ Here, the name `'b` is not part of the root universe. Instead, when we
201
201
"enter" into this ` for<'b> ` (e.g., by skolemizing it), we will create
202
202
a child universe of the root, let's call it U1:
203
203
204
- ``` txt
204
+ ``` text
205
205
U0 (root universe)
206
206
│
207
207
└─ U1 (child universe)
@@ -224,7 +224,7 @@ When we enter *this* type, we will again create a new universe, which
224
224
we'll call ` U2 ` . Its parent will be the root universe, and U1 will be
225
225
its sibling:
226
226
227
- ``` txt
227
+ ``` text
228
228
U0 (root universe)
229
229
│
230
230
├─ U1 (child universe)
@@ -263,7 +263,7 @@ children, that inference variable X would have to be in U0. And since
263
263
X is in U0, it cannot name anything from U1 (or U2). This is perhaps easiest
264
264
to see by using a kind of generic "logic" example:
265
265
266
- ``` txt
266
+ ``` text
267
267
exists<X> {
268
268
forall<Y> { ... /* Y is in U1 ... */ }
269
269
forall<Z> { ... /* Z is in U2 ... */ }
@@ -296,7 +296,7 @@ does not say region elements **will** appear.
296
296
297
297
In the region inference engine, outlives constraints have the form:
298
298
299
- ``` txt
299
+ ``` text
300
300
V1: V2 @ P
301
301
```
302
302
@@ -346,7 +346,7 @@ for universal regions from the fn signature.)
346
346
Put another way, the "universal regions" check can be considered to be
347
347
checking constraints like:
348
348
349
- ``` txt
349
+ ``` text
350
350
{skol(1)}: V1
351
351
```
352
352
@@ -358,13 +358,13 @@ made to represent the `!1` region.
358
358
OK, so far so good. Now let's walk through what would happen with our
359
359
first example:
360
360
361
- ``` txt
361
+ ``` text
362
362
fn(&'static u32) <: fn(&'!1 u32) @ P // this point P is not imp't here
363
363
```
364
364
365
365
The region inference engine will create a region element domain like this:
366
366
367
- ``` txt
367
+ ``` text
368
368
{ CFG; end('static); skol(1) }
369
369
--- ------------ ------- from the universe `!1`
370
370
| 'static is always in scope
@@ -375,20 +375,20 @@ It will always create two universal variables, one representing
375
375
` 'static ` and one representing ` '!1 ` . Let's call them Vs and V1. They
376
376
will have initial values like so:
377
377
378
- ``` txt
378
+ ``` text
379
379
Vs = { CFG; end('static) } // it is in U0, so can't name anything else
380
380
V1 = { skol(1) }
381
381
```
382
382
383
383
From the subtyping constraint above, we would have an outlives constraint like
384
384
385
- ``` txt
385
+ ``` text
386
386
'!1: 'static @ P
387
387
```
388
388
389
389
To process this, we would grow the value of V1 to include all of Vs:
390
390
391
- ``` txt
391
+ ``` text
392
392
Vs = { CFG; end('static) }
393
393
V1 = { CFG; end('static), skol(1) }
394
394
```
@@ -405,15 +405,15 @@ In this case, `V1` *did* grow too large -- it is not known to outlive
405
405
406
406
What about this subtyping relationship?
407
407
408
- ``` txt
408
+ ``` text
409
409
for<'a> fn(&'a u32, &'a u32)
410
410
<:
411
411
for<'b, 'c> fn(&'b u32, &'c u32)
412
412
```
413
413
414
414
Here we would skolemize the supertype, as before, yielding:
415
415
416
- ``` txt
416
+ ``` text
417
417
for<'a> fn(&'a u32, &'a u32)
418
418
<:
419
419
fn(&'!1 u32, &'!2 u32)
@@ -423,22 +423,22 @@ then we instantiate the variable on the left-hand side with an
423
423
existential in universe U2, yielding the following (` ?n ` is a notation
424
424
for an existential variable):
425
425
426
- ``` txt
426
+ ``` text
427
427
fn(&'?3 u32, &'?3 u32)
428
428
<:
429
429
fn(&'!1 u32, &'!2 u32)
430
430
```
431
431
432
432
Then we break this down further:
433
433
434
- ``` txt
434
+ ``` text
435
435
&'!1 u32 <: &'?3 u32
436
436
&'!2 u32 <: &'?3 u32
437
437
```
438
438
439
439
and even further, yield up our region constraints:
440
440
441
- ``` txt
441
+ ``` text
442
442
'!1: '?3
443
443
'!2: '?3
444
444
```
@@ -465,7 +465,7 @@ common lifetime of our arguments. -nmatsakis)
465
465
Let's look at one last example. We'll extend the previous one to have
466
466
a return type:
467
467
468
- ``` txt
468
+ ``` text
469
469
for<'a> fn(&'a u32, &'a u32) -> &'a u32
470
470
<:
471
471
for<'b, 'c> fn(&'b u32, &'c u32) -> &'b u32
@@ -478,23 +478,23 @@ first one. That is unsound. Let's see how it plays out.
478
478
479
479
First, we skolemize the supertype:
480
480
481
- ``` txt
481
+ ``` text
482
482
for<'a> fn(&'a u32, &'a u32) -> &'a u32
483
483
<:
484
484
fn(&'!1 u32, &'!2 u32) -> &'!1 u32
485
485
```
486
486
487
487
Then we instantiate the subtype with existentials (in U2):
488
488
489
- ``` txt
489
+ ``` text
490
490
fn(&'?3 u32, &'?3 u32) -> &'?3 u32
491
491
<:
492
492
fn(&'!1 u32, &'!2 u32) -> &'!1 u32
493
493
```
494
494
495
495
And now we create the subtyping relationships:
496
496
497
- ``` txt
497
+ ``` text
498
498
&'!1 u32 <: &'?3 u32 // arg 1
499
499
&'!2 u32 <: &'?3 u32 // arg 2
500
500
&'?3 u32 <: &'!1 u32 // return type
@@ -503,15 +503,15 @@ And now we create the subtyping relationships:
503
503
And finally the outlives relationships. Here, let V1, V2, and V3 be the
504
504
variables we assign to ` !1 ` , ` !2 ` , and ` ?3 ` respectively:
505
505
506
- ``` txt
506
+ ``` text
507
507
V1: V3
508
508
V2: V3
509
509
V3: V1
510
510
```
511
511
512
512
Those variables will have these initial values:
513
513
514
- ``` txt
514
+ ``` text
515
515
V1 in U1 = {skol(1)}
516
516
V2 in U2 = {skol(2)}
517
517
V3 in U2 = {}
@@ -520,14 +520,14 @@ V3 in U2 = {}
520
520
Now because of the ` V3: V1 ` constraint, we have to add ` skol(1) ` into ` V3 ` (and
521
521
indeed it is visible from ` V3 ` ), so we get:
522
522
523
- ``` txt
523
+ ``` text
524
524
V3 in U2 = {skol(1)}
525
525
```
526
526
527
527
then we have this constraint ` V2: V3 ` , so we wind up having to enlarge
528
528
` V2 ` to include ` skol(1) ` (which it can also see):
529
529
530
- ``` txt
530
+ ``` text
531
531
V2 in U2 = {skol(1), skol(2)}
532
532
```
533
533
0 commit comments