►
From YouTube: Universes and Lifetimes
Description
An overview of how higher-ranked types/trait-bounds (`for<'a> fn(&'a u32)` or `for<'a> T: Foo<'a>`) are implemented in rustc. Focuses on the idea of universes and placeholders and how those are used in subtyping.
The paper doc used in the video is readable here:
https://paper.dropbox.com/doc/Universes-and-57639--AXjnSUh91ZmbD0dDMwTTfFHfAg-vVrMCkndUoXzyrHCOQdq8
Or in gist form:
https://gist.github.com/nikomatsakis/848f6bd0db706b1f0596e7e559588128
A
Obviously,
I'm
gonna
cut
the
spoiler
recording
so
welcome
to
Arden
evening.
So
what
I'm
gonna
talk
I.
This
is
an
interesting
book
that
I
wanted
to
kind
of
dive
into
interesting
topic
to
dive
into
because
it's
I
kind
of
wanted
to
pursue
a
specific
bug
a
little
bit,
but
also
it
is
a
kind
of
cross-cutting,
but
it
affects
two
fundamental
issues:
things
in
the
way
the
rusty
works.
So
there's
we'll
see
how
far
we
get
we
may
want
to
do
another
meeting,
but
it's
kind
of
an
interesting
way
to
it
to
instruct
so.
A
I
put
a
little
rough
agenda
if
you're
in
the
paper,
doc
and
I,
guess
you're
sure
I'm
sharing
it
I
put
a
rough
agenda
here.
These
are
the
two
things
so
the
first
one
is
like
how
to
handle
how
to
deal
with
higher
ranked
trade
bound
like
things
and
solve
constraints
like
for
all
a
to
get
to
be
or
other
similar
things
and
how
we,
how
we
do
that
I
would
kind
of
implemented
that
no
low
level
and
rusty
today-
and
this
is
something
that
I
recently
changed
and
that's
kind
of
the
problem.
A
This
is
like
a
minimal
example
of
it,
but
what
it
let
me
see
if
I
can
remember
right
and
I
kind
of
laid
out
some
of
the
things,
but
it
comes
down
to
is
that
the
compiler
is
making
a
poor
choice
and
forcing
a
for
all
requirement
that
is
stricter
than
what
is
actually
necessary
and
it
didn't
use
to
do
this
in
the
older
system
and
I
guess:
I'll
have
to
talk
a
little
bit
about
that
too.
So
you
have
to
sort
of
cover.
A
A
A
A
You
could
have
like
a
type
like
this
right
and
you
might
ask
yourself
a
question
like:
is
this
a
subtype
of
this
other
type
so
that
what
this
says
is
I
have
a
function
pointer
that
takes
a
reference
of
any
lifetime
and
I
want
to
know?
Can
I
use
that
function?
Let's
make
it
more
concrete.
I
might
have
like.
A
A
There
is
basically
an
algorithm
for
doing
this,
and
the
way
it
works
is
that
when
you
see
for
all
binders
on
the
left
like
on
the
subtype
side,
well,
let
me
go
to
a
more
intuitive
level.
So,
first
of
all
is
the
answer.
Yes
or
no,
should
this
be
allowed,
or
should
it
not
be
allowed?
The
answer
is
yes
in
this
case
and
intuitively.
A
The
reason
is
this:
this
function
is
able
to
accept
a
reference
with
any
lifetime,
or
so
he
claims-
and
this
type
is
a
lot-
is
a
function
that
accepts
the
reference
with
exactly
one
lifetime
and
that's
kind
of
a
subset
right,
because
tip
B
is
a
lifetime.
This
function
is
able
to
accept
any
so
that
should
be
okay.
That
means
you
can
accept
it.
Li.
A
The
other
direction
is
more
problematic.
Let's
we'll
get
to
that
in
a
second,
so
the
way
that
this
this
works
in
rusty
today
is
when
you
come
like
when
you
come
to
you're
doing
your
you're
kind
of
trying
to
compute.
You
have
two
types:
t1
and
t2,
and
you
want
to
know
is
t1
a
subtype
of
t2
and
the
outcome
of
this
in
general.
When
we're
asking
this
question
or
rusty,
the
outcome
is
either
yes
or
no,
basically
and
a
yes.
A
If
the
answer
is
yes
become
me,
can
we
give
back
some
what
we
call
region
constraints
or
lifetime
constraints?
Incidentally,
I
remember
I
realize
now
I
covered
more
or
less
exactly
this
in
my
recent
blog
post.
So
for
all
of
you
who
are
like
following
along
on
the
Internet's,
and
you
feel
like
reading
this
blog
post,
its
kind
of
covering
similar
stuff.
A
A
A
A
We
can
kind
of
make
sure
that
the
t1
and
t2
will
have
to
be
some
types
of
one
another,
so
we
can
recursively
do
that,
and
that
gives
us
back
some
constraints
and
then
we
return
like
c1
plus
2k,
all
those
TV
I,
don't
know
it's
kind
of
pseudocode.
Does
that
make
sense?
So
this
is
the
sort
of
definition
of
sub
type
t1
t2
map
this
to
the
rescue
code
in
a
second
to
make
it
more
concrete
because
I
think
that's
important,
but
but
what
about,
if
t1
equals
for
all
something?
A
Something
which
is
the
case
that
we
have
here
right
for
now,
I'll
make
it
specific
to
functions.
It
actually
applies
also
to
trade
objects,
and
the
answer
is
what
we
do
if
this,
if
the
thing
that
has
to
be
a
subtype,
that's
t1
has
binders
like
this.
Let's
just
say
for
all
today:
right
now
we
make
a
fresh
variable
inference
variable
the
idea
is
it's
valid
for
any
it's
valid
for
any
lifetime
or
region
today.
A
So,
let's
make
a
variable,
we'll
call
it
tick:
zero,
let's
replace
together
with
tick
zero
in
the
function
type
and
then
let's
that's
gonna,
yield
us
like
yielding
a
type
t1
prime
and
then
let's
relate
t1
prime,
to
teach
him
so
to
make
it
to
come
to
our
example.
We
had
for
all
of
take
a
function
and
again
you
32.
We
would
we
would
sort
of
replace
and
get
a
type
like
this.
We
replace
the
the
today
with
a
variable.
A
Take
0
and
why
we
do
that,
as
we
say:
hey,
it
was
valid
for
all
things,
so
we're
trying
to
find.
Is
there
any
value
that
we
could
give
to
today?
That
would
be
would
make
it
would
make
these
types
compatible
right.
That's
why
it's
an
inference
variable
because
it's
like,
let's
find
a
value
that
is
compatible.
A
A
How
sure
how
to
pose
Equis?
We'll
do
it
like
this?
You
can
imagine
there's
some
rule
that
says
if
you
have
a
function
type
by
itself
without
the
for
all's
around
it,
then
you
have
to
you
have
to
require
that
first
of
all,
the
arguments
have
to
be
subtypes
and
the
return
type
have
to
be
related
more
or
less,
and
you
notice
I
swapped
the
orders
here.
That's
because
of
how
functions
work.
Their
so-called
countries
are
not
that
important
to
this
particular
thing.
So
that's
how
we
get
to
our
answer,
so
that
will
get
us.
A
A
It
also
may
make
fresh
variables,
as
he
feels
so
it's
kind
of
like
plus
fresh
variables,
and
if
this
is
the
only
use
of
tick
zero
like
when
we're
gonna
come
back
later
and
do
our
inference
process,
we
have
to
find
a
value
for
tick.
Zero.
That
works
in
this
case
of
one
answer
might
be
to
be.
That's
like
whatever
tick
B
turns
out
to
be
take
zero.
Can
there's
no
other
constraints
on
it,
so
it's
not
a
hard
problem
to
solve.
This
is
only
used
once
okay,
that
that's
sort
of
the
easy
part.
A
A
A
We
want
to,
you
probably
want
to
error,
because
not
necessarily
actually
will
see
nothing
out,
but
because,
whatever
sort
of
whatever
today,
whatever
value
TK,
is
that's
going
to
be
a
function
that
demands
one
specific
lifetime
in
the
end
of
the
day
and
we're
wanting
to
use
it
as
if
it
can
accept
any
lifetime
right
and
that's
not
necessarily
valid
and
the
way
we
do
this.
This
is
where
the
is,
but
we
don't
before
we
replaced
tik,
be
where
we
replace
the
bound
variable
tonight
with
the
inference
variable.
A
But
that
doesn't
make
sense
here,
because
that
would
give
us
the
same
sort
of
thing.
Everything
is
there
any
value
of
tik
beat
it
works,
and
what
we
want
to
show
is
more
like.
Does
this
work
for
any
value
look
technique?
It
could
be
anything
not.
Is
there
a
some
specific
value,
but
does
it
work
for
all
of
them?
So
this
is
essentially
4l4
since
there
exists.
Is
the
question
right
and
the
way
we
do,
that
is
we
introduce
the
idea
of
a
place
holder
and
universe
is
a
place.
A
A
It's
like
I'm
maximally,
conservative
right
and
the
idea
of
universes
is
that
we
say:
okay,
there's
some
set
of
names
that
are
kind
of
global
that,
like,
if
you
think,
of
lifetime,
sighs,
what's
the
right
intuition
to
go
for
here.
Well,
if
we
use
them
as
polonius
than
our
lifetime
is
the
set
of
loans
right
and
those
Nate
there's
some
set
of
loans
that
are
alone
is
like
a
specific
ampersand
expression
in
the
program
and
those
are
kind
of
global
names
that
any
region
could
contain,
but
this
placeholder
name.
A
This
is
like
a
special
loan,
that's
different
from
all
the
loans
we
know
so
far,
and
so
when
we
make
one
of
those
special
loans
we
do
it
by
creating.
We
put.
We
say
that
all
the
names
of
loans
are
in
universes
and
a
variable
is
associated
with
a
universe
and
that
basically
describes
the
set
of
loans
that
it
is
allowed
to
contain,
and
so
you
start
out
with
this.
A
A
I'm
gonna
use
this
same
notation.
We
now
have
a
function
that
doesn't
have
any
binders,
but
has
this
sort
of
placeholder
region?
That's
gentle
and
we
want
to
relate.
Then
we
sort
of
relate
t1
and
t2
as
before,
so
where
we
had.
So
if
we
go
through
our
step,
we
would
wind
up
saying
we
were
checking
this
in.
Let's
say
in
university
room
and
now
we're
checking.
A
This
result,
which
says
basically
that
is
this,
is
true,
so
long,
oops
I
have
this
backward
its
contravariant.
Let
me
do
it
one
more
step.
This
will
be
true
if
the
argument
types
relate
and
they
flip
orders,
and
that
gives
rise
to
this
region-
constraint
right,
which
basically
says
take
a
whatever
it
is,
has
to
outlive
every
region,
like
some
reason
that
we
don't
know
which
you
can't
really
do.
Is
we
don't
or
I
can't
do.
A
A
So
this
is
probably
an
error,
or
at
least
it's
an
error.
Let's
say
if
the
function
is
ever
called,
because
the
reason
that
would
be
required
is
that,
like
maybe
you
could
infer
that
it's
a
function,
that's
well
typed
as
long
as
it's
never
cold
or
something,
but
it's
not
I,
don't
think
we
even
support
that.
Okay,
that's
the
kind
of
theoretical
side
of
this.
So
you
can
you
can
view
this
constraint.
A
You
could
sort
of
take
it
out
of
the
universes
and
go
back
to
before
all
notation,
and
you
could
sort
of
see
it
as
saying
this
right
and
that's
sort
of
what
I
just
how
I
described
it
in
the
blog
post,
but
in
the
way
that
the
compiler
thinks
about
it.
This
is
actually
much
closer,
so
I
maybe
will
type
a
little
into
that.
A
So
another
thing
to
note:
that's
important
is
I
described
just
like
shifting
to
the
implementation
side
of
this
I
described
the
universe
tree
as
a
tree,
and
that
and
it
is,
however,
in
the
compiler-
we
only
keep
a
single
integer.
So
what
we
do
is
we
kind
of
rely
on
the
fact
that
we
will
never
fall.
We
will
never
ask
cousins
to
interact
with
one
another.
The
only
way
for
things
to
interact
is
by
sharing
an
inference.
A
Variable
Oh,
suffice
to
say
it's
enough
to
keep
just
an
integer,
so
you
just
remember
like
the
index
and
if
the
index
is
greater-
and
you
know
it's
a
child,
and
if
it's
not
it's
not.
Let
me
you
try
to
make
that
a
little
more
concrete,
so
I
didn't
show
you
this
other
case,
which
is
like
this
is
maybe
a
good
case
to
talk
about
before
we
move
on.
A
But
if
you
have
four
hours
on
both
sides,
we
would
like
this
to
be
true.
Obviously
this
is
the
same
type.
So
what
happens?
Is
you
do
a
combination
of
these
things,
but
you
first
process
the
super
tape.
This
would
be
important
in
a
second,
so
we
kind
of
started
out
with
this
like
in
the
universe,
zero,
and
we
would
first
process
the
super
type
and
say:
okay,.
A
The
left-hand
side
with
an
infant's
variable,
but
this
is
the
important
part,
the
each
infant
variable
has
a
universe,
and
so
the
infant's
variable
tick.
Zero
is
in
universe,
U,
one
because
it's
that
universe
is
taken
basically
from
what
is
the
current
universe
at
the
point
where
were
of
this
thing
were?
A
B
C
A
And
so
we
we
model
that
by
having
like,
we
make
one
fresh
universe
with
two
names
in
it,
and
that's
okay,
but
if
you
had
a
system
like
this
is
like
a
subtle
difference
between
some
of
the
formal
work,
because
often
these
are
modeled
as
like.
If
you
go
to
a
system
ask
for
whatever
this
is
like
our
function
from
types
and
then
the
ordering
is
think
if
you
can
partially
apply
it,
you
can
say
I
just
say:
what
today
is
that
I
don't
stay
with
to
be?
A
A
A
C
A
You
can
see
it
has
various
variants.
The
one
I
wanted
to
call
your
attention
to
is:
is
this
placeholder
here?
So
if
you
have
a
placeholder
region,
this
is
what
it
would
be
represented
as
and
what
is
happening
now.
Okay,
so
if
I
jump,
what
is
placeholder
region
yeah,
taking
me
some
time
to
get
used
to
this,
you
can
anticipate
this
problem
by
good.
A
A
A
There
we
go
it's
this
placeholder
type,
which
somewhere
is
defined
that
there
it
is
which
has
the
universe
index
and
the
name
so
air
into
your
question
of.
Can
there
be
more
than
one
thing?
This
is
basically
why
you
might
have
one
universe
in
you
would
have
distinct
names.
So
that's
how
our
region
is
represented
and
then
actually
region
inference.
We
do
inference.
A
Let's
see,
he's
broken
up
into
a
couple
of
different
things:
I'm
just
going
to
jump
to
some
file
but
the
relevant
code.
So
if
you
go
into
the
infer
directory,
this
is
our
hole,
type
inference
set
of
code
right
and
the
kind
the
bit
of
code
I'm
most
interested
in
right
now
is
this
region
constraints
module
and
what
that
contains
is
basically
the
code
to
collect
these
constraints.
So
what
I
was
writing
in
the
document?
I
wrote
like
like
this.
A
Take
take
one
all
that
stuff.
This
is
how
we
represent
those
MSC,
and
it's
also
where
we
track
the
set
of
region
variables.
So
it's
this
big
struct.
It's
got
a
lot
of
stuff
in
it.
That's
not
too
relevant
here,
but
the
most
important
thing
is
for
each
region
variable.
We
have
some
information,
this
maps
from
the
FID,
which
is
the
variable
ID
to
the
information
about
the
variable
and
then
there's
a
struct
called
data
which
has
like
the
set
of
constraints
and
I'll
get
to
that
in
a
second.
A
So
a
region
variable
info
is
really
not
a
lot
of
stuff,
it's
basically
the
origin.
This
is
for
Diagnostics.
This
is
like.
Why
did
I
make
this
inference
variable?
It
doesn't
affect
the
type
system
rules
in
any
way
and
then
the
other
one
is
the
universe
that
we
created
the
variable
in,
and
so
when
we
make
a
new
region
variable,
you
just
give
those
two
pieces
of
information
and
it
gets
stored.
A
A
So
this
is
it's
a
b-tree
map
only
because
we
want
to
detect
duplicates,
but
it
says
as
a
constraint
and
then
the
key
the
value
is.
Why
did
we
create
this
constraint?
That's
again
for
Diagnostics.
So
if
we
look
at
this
constraint,
this
is
one
of
these
ticket
out
lipstick,
be
the
four
variants
are
all
the
same.
The
only
difference
between
them
is
in
which
case
it.
This
is
to
infants
variables.
A
A
We
don't
track
the
four
alls
and
all
that
stuff
we
just
track
which
were
the
two
variables
and
then
we
know
what
universe
the
inference
rule
was
in
and
we
know
what
universe
the
placeholder
is
in
and
you
can
kind
of
figure
out
all
we
have
to
know
and
the
way
we
do
inference
for
now,
I'm
going
to
ignore
nlll
for
a
second,
because
it's
not
actually
relevant
to
this,
it's
sort
of
easier
and
not
the
lexical.
So
this
is
the
old
region
solver,
but
nll
has
a
similar
character
for
this
purpose.
A
The
way
we
do
region
inference
is
that's
all
in
this
module
called
lexical
region
result
and
it's
basically
a
really
simple
process
in
which
it's
right
here,
infer
variable
values
and
what
it
does
is
this
all
in
this
function,
expansion.
The
idea
is
that
for
each
region
variable
we
start
out
with
what
its
value
is,
and
we
start
out
I
think
with
empty,
meaning
that
it's
not
usable
anywhere
and
then
we
keep
growing
it
in
response
to
constraints.
A
So
if
you
have
a
constraint
that
says
like
the
variable
must
outlive
tick
static,
then
we
will
say:
okay,
it
must
be
text
attic,
but
that's
a
kind
of
an
extreme
point
because
you
can
never
get
bigger
than
that.
But
if
we
say
the
variable
must
outlive
so
this
is
lexical
region
resolves,
so
it
would,
it
might
be
like
it
has
to
be
as
big
as
this
statement
that
this
part
of
the
code
right
and
then
we
would
grow
into
that
statement.
A
And
then,
if
it
has
to
outlive
the
neighboring
statement,
then
it
has
to
get
big
enough
to
encompass
its
current
value,
which
was
saving
a
and
the
neighboring
statement.
B,
and
the
only
way
for
it
to
do
that
is
to
jump
up
to
the
whole
enclosing
block.
So
it
will
become
the
closing
block
and
so
forth.
That's
pretty
easy,
but
that's
all
assuming
you're
kind
of
in
the
root
universe.
A
So
what
you
basically
do
now,
as
we
extend
for
well
what
happens
if
it
has
to
outlive
a
placeholder
right,
so
if
it
has
to
outlive
all
the
regions
and
so
here's
the
expansion
code,
it
does
this
iterate
until
fixed
point.
So
this
is
just
going
over
and
over
again
and
recursively
growing
things
until
we
meet
you
on
fix
point
where
we
don't
where
all
the
things
are
satisfied,
and
then
we
see
so
I
should
point
out.
A
This
was
written
in
the
old
days,
so
you
see
how
it
says:
sub:
u
I've
been
showing
the
constraints
as
to
K
:,
tick,
B,
meaning
today,
outlives
to
P.
These
constraints
are
actually
stored
in,
took
me
less
than
or
equal
to
today
for
him
so
they're
the
same
constraint
but
reversed,
because
that
was
how
my
phone
was
more
natural
of
the
time,
but
so
yeah.
So
this
is.
That
requires
a
bit
of
a
mental
shift,
but
this
is
saying
like
if
you
have
some
region
variable
which
outlives
some
specific
region.
A
This
is
like
a
blah.
That's
gonna
call
this
in
function,
expand
node,
so
essentially
in
this.
What
we're
doing
here
is
we're
trying
to
get
some
specific
region
and
sorry
some
variable
and
some
specific
region
it
has
to
be
bigger
than
and
we're
gonna
pass
that
to
expand
node,
which
is
going
to
make
the
value
of
that
variable
be
big
enough
to
enclose
its
current
value
plus
this
region.
Now
we're
going
to
do
that.
Iteratively
I
forget
what
this
other
stuff
is,
but
not
important.
So
here's
the
function,
expand,
node
and.
A
Takes
the
region,
the
variable
that
has
to
be
bigger
than
this
region
when
it's
done
and
some
data
will
figure
out,
that
is
I.
Think
that's
like
some.
This
is
like
some
some
other
information,
okay
yeah.
So
this
is
I
think
this
basically
contains
the
current
values
of
all
the
variables.
If
I'm
not
mistaken,
ignore
the
Givens.
Please
like
embarrass
that
that
coastal
they
come
back
to
it.
It's
not
real.
So
this
being
the
Gibbons,
don't
don't
look
there
don't
look
where
my
mouth
is
so
the.
A
So
what
happens?
We
look
well
B.
What
is
B
data?
Actually,
that's,
oh
I,
see
so
B
data
is
actually
the
value
for
this
exact
variable.
That's
what
it
is.
It's
not
the
set
of
values
for
all
variables,
it's
the
value
for
this
particular
variable.
So
we
look
at
what
is
the
current
value
and
either
it's
an
error,
meaning
that
we
already
found
that
for
some
reason
there
was
an
error.
In
that
case
we
can
just
ignore
it
or
it
has
some
value
now,
which
is
this
current
region
right
and
then
we
can
check
this.
A
Just
checks
is
the
current
region
already
the
same
as
the
red
as
the
region
it
has
to
outlive.
Then
Leslie,
that's
like
saying
today,
all
this
to
Gay's,
it's
mine
to
Noah,
that's
a
performance
optimization!
Otherwise
we
find
soul
of
concrete
region,
says:
okay,
we
got
two
exact
Scopes
in
the
lexical
system.
Let's
find
their
least
upper
bound.
Let's
find
some
scope
that
encloses
both
of
them
and
if
that's
the
same
as
the
value
we
already
have,
then
we're
done
because
we
didn't
need
to
grow.
A
We
already
included
the
new
value
we
have
to
include
otherwise
and
here
because
here
comes
the
placeholder
code.
Otherwise,
let's
look
at
what
let
universe
this
variable
was
declared
in
and
let's
look
if,
if
the
value
that
it
has
to
take
on
is
a
placeholder,
then
we
check
if
that
placeholder
is
in
scope
for
the
universe
and
if
not,
we
make
it
beat
ecstatic
when
we
take
this
back
now
to
the
to
the
paper
drop
box
paper
and
I,
try
to
explain
that
logic.
A
A
A
A
A
A
A
It
would
be
like
that
right
and
now
this
is
interesting,
because
we're
now
and
now
when
the
solver
runs,
it's
trying
to
it's
trying
to
change
the
value
of
tick
zero
to
be
something
that
lives
like
it,
doesn't
matter
what
it
is
as
long
as
it's
longer
than
this
thing.
But
this
thing
we
don't
know
exactly
what
it
is.
A
So
there
are
two
options:
either:
if
tick
zero
is
in
an
appropriate
universe
like
if
it
were
in
the
universe,
one
we
could
set
its
value
it
to
be
the
place
holder
itself
not
be
great,
but
if
tick
zero
is
not
in
that
universe,
there
is
still
another
option:
it
could
equal
tick,
static
and
Ecstatic
is
no
doubt
of
all
the
things.
So
that
would
be
okay.
So
that's
what
this
code
is
doing.
A
Okay,
so
it's
saying
assuming
that
I
can't
name
it
then
I'm
gonna,
basically,
love
is
the
least
upper
bound
is
going
to
be
assuming
you
can
name
the
placeholder,
and
so
this
is
saying
in
the
case
that
I
can't.
Let
me
reset
that
I
have
to
grow
even
further.
I
have
to
go
all
the
way
to
take
static.
To
make
this
be
satisfied,
and
then
we
can
just
set
the
value
to
whatever
this
least
upper
bound
is,
and
it
should
be.
A
Okay,
and
so
the
kind
of
interesting
thing
about
this
is
that
in
a
sense
you
don't
get
often
in
error.
You
kind
of
get
success,
but
you
get
just
a
really
really
big
vision
that
may
give
other
errors
later
like.
Maybe
because
you
were
in
first
ecstatic,
you
now
hold
a
borough
for
a
really
long
time
longer
than
you
expect
and
stuff
like
that
and
I.
Don't
know,
there's
also
the
reverse
error,
as
that
play
out.
I'm,
not
sure
I,
think
that
comes
to
do
with
the
least
upper
bound
right.
A
So
sorry,
if
we,
if
we
go
back
now
to
my
original
example,
so
here
I
put
it
in
the
return
type.
But
if
you
have
the
placeholder
like
like
in
this
case,
the
placeholder
was
in
the
parameter
type.
We
wound
up
with
the
placeholder
being
done
so
sort
of
lower
variable
or
sorry.
It
becomes
the
outlived
thing,
then,
that
winds
up
reporting
an
error
through
a
different
kind
of,
because
when
we're
doing
the
region
solving
we're
only
interested
in
in
in
growing
the
inference
variables,
we
try
to
make
them.
A
Let's
try
me
little
crazy,
okay,
so
right
so
the
expansion
is
this
phase,
where
we're
growing
all
the
things
to
be
the
smallest
values
that
satisfy
the
constraints
and
then
the
collect
errors
and
collect
far
errors
is
where
we
go
back
over
and
say:
how
are
those
two
big
is
so,
let's
report
an
ear
and
that's
where
this
placeholder
the
fact
that
this
variable
had
to
be
smaller
than
a
placeholder,
and
we
don't
know
what
the
policeman
is.
We
would
feel.
C
A
Not
necessarily
an
error
that
it
grows
to
be
tick
static.
There
are
examples
where
that
that
will
type
just
fine.
So
if
you
recall
I
could
give
you
one
if
you
want,
but
if
you
remember
from
the
very
first
thing
we
looked
at
I
said
something
like
we'll
make
an
inference
variable
and
it's
not
going
to
be
constrained
anywhere
outside
of
this,
like
subtyping
relationship,
so
all
the
constraints
arise
from
them
there
they
may
well
be
tit.
A
B
Not
related
to
that
so
in
the
sort
of
case
that
there
is
ultimately
an
error,
does
the
compiler
do
some
work
to
sort
of
so
I
can
imagine
like
this
picking
tick
static
thing?
If
the
code
is
ultimately
erroneous,
you
could
get
a
very
confusing
message
where
something
is
claimed
to
be
tick
static
and
it's
hard
to
understand
where
that's
coming
from.
Is
there
some
logic
to
try
to
like
catch
that
case
and
explain
it?
Yes,
yes,.
C
A
And
one
of
them
is
called
placeholder
error,
and
indeed
this
is
the
way
this
basically
works
is
when
you
get
it,
you
get
an
error
from
region
inference
it's
it's
kind
of
like
here's.
A
constraint
I
couldn't
satisfy
it's
kind
of
the
shape
it
takes,
and
then
the
job
of
the
nice
region
errors
is
to
like
look
at
that
constraint
and
try
to
see
if
we
can
categorize
it
into
something
for
which
we
have
a
Taylor
to
error.
Message:
try
to
take
a
guess
as
to
what's
going
on.
A
Basically,
so
this
particular
one
tries
to
detect
if
it
came
came
about
as
a
result
of
a
place,
holder,
conflict
and
there's
various
scenarios,
you
see
it.
Let's
do
a
reasonable
amount
of
effort
to
make
a
nice
message
and
say
things
like
you
know.
This
thing
would
have
to
be
implemented
for
this
type
for
any
two
lifetimes,
but
it's
only
implemented
for
this
type
for
some
specific
lifetime
instantly.
So
yeah
we
put
a
lot
of
effort.
A
Actually,
this
transition
in
two
universes
was
accompanied
with
the
we
never
did
have
nice
errors
for
this
case
sense,
and
we
tried
to
link
do
that
at
the
same
time,
and
there
are
some
cases,
that's
still
a
work
in
progress.
There's
still
a
few
I
think
we
fixed
all
the
major
regressions.
Maybe
there's
one
left:
okay,
lq
d's
been
working
on
that
kind
of
extending
this
to
cover
more
and
more
cases,
but
so.
B
B
A
I
baited,
rather
to
start
with
this,
and
even
I,
should
happen
anyway.
Do
you
like
now,
but
let
me
because
we
only
have
a
few
minutes
left
anyway,
so
we're
not
going
to
get
to
the
rest
of
my
agent
I
will
have
to
schedule
a
follow
me,
but
this
is
good
I.
Think
now
that
I've
walked
through
all
of
this
with
you,
you
can
look
at
the
pure
logic
side,
which
is
like
what
basically,
what
Aaron
was
saying
is
you
could
have
a
couple
of
to
imagine
a
and
B
are
variables
of
any
kind.
A
A
The
only
way
you
can
say
that
for
sure
is
if
there's
like,
you
know
something
about
the
domains
and
these
variables
there's
only
exactly
one
value
and
okay
sure
so
or
rather
yeah.
You
said,
I
mean
you
can't
pick
some
a
and
then
know
that
it's
gonna
be
equal
to
all
the
B's.
Unless
there's
exactly
one
being
money
and.
A
So
the
only
way
that
a
value
like
here's,
a
situation
where
you
have
for
all
be
some
stuff
and
for
all
see
some
stuff-
and
these
are
two
siblings
now
B
and
C
are
two
different
universes.
They
can't
communicate,
but
the
only
way
that,
like
solving
the
stuff
in
this
first
half
could
have
side-effects.
Somehow
that
are
like
visible
to
this.
Other
half
is
if
it
changes
the
value
of
a
so
only
thing
they
have
in
common
and
a
is
already
in
the
root
universe.
A
So
any
value
of
that
a
you
can
have
is
some
player.
They
can
both
name
so
so
long
as
we
don't
allow
like.
If
the
bad
case
would
be
like
this,
you
know
if
we
were,
if
we
were
buggy
for
illogic
silver
was
buggy
or
something
it
might
say.
Oh
okay,
B
is
a
is
equal
to
B
and
therefore
this
is
like
saying:
B
is
equal
asking
if
B
is
equal
to
C
or
not,
and
since
we're
not
since
we've
assigned
this
index
1
and
we've
assigned
this
index.
A
2
and
2
is
greater
than
1
like
it's
okay,
because
we
think
that
they're
a
but
the
parent-child
relationship
when
actually
don't,
but
that
just
can't
happen,
because
we
would
never
allow
a
to
take
the
value
B
in
the
first
place.
It
would
instead
the
TIC,
static
or
or
error
or
something
so
that's
convenient
cuz
it.
An
integer
is
like
small
yeah,
so
that's
the
universe
system
and
I
guess
we
should
schedule
a
follow-up
meeting
to
walk
through
the
trades
over
and
actually
that's
sort
of
nice.
This
is
enough
for
a
day
all
right.