Nearlyuniversal quantification
This issue is about an interaction between polymorphism and constrained type constructors. These are a feature of several type systems allowing the definition of a type constructor $T[]$, where $T[A]$ is a valid type only for certain $A$.
This feature is different from GADTs (indexed types), which allow the definition of a type constructor $T[]$ where $T[A]$ is always a valid type, but one which is only inhabited for certain $A$.
To explain this distinction, here's a GADT $\n{G}$ and a constrained type $\n{C}$:
type 'a g = G_int : { name : string } > int g
type 'a c = { name: string } constraint 'a = int
sealed trait G[T]
case class G_int(i: Int) extends G[Int]
class C[A >: Int <: Int](name : String)
The type $\n{C}[A]$ is only legal when $A = \n{Int}$, whereas $\n{G}[A]$ is always valid, but is an empty type unless $A = \n{Int}$:
type ok = string g
type bad = string c
(* Error: This type string should be an instance of type int *)
type Ok = G[String]
type Bad = C[String]
// Error: type arguments [A] do not conform to
// class C's type parameter bounds [A >: Int <: Int]
With constrained types, there are two different ways to interpret a polymorphic type such as $∀α. \n{C}[α] → \n{String}$:

$∀α.;\dots$ really means "for all $α$", so the type above is invalid since $\n{C}[α]$ is not a valid type for all $α$.

$∀α.;\dots$ means "for all $α$ for which the righthand side is valid", so the type above is valid, but can only be used with $α = \n{Int}$.
Both OCaml and Scala choose option (1):
let poly : 'a . 'a c > string =
fun _ > "hello"
(* Error: The universal type variable 'a cannot be generalized:
it is bound to int. *)
def poly[A](x: C[A]): String = "hello"
// Error: type arguments [A] do not conform to
// class C's type parameter bounds [A >: Int <: Int]
Option (2) requires slightly less annotation by the programmer, but it can be easy to lose track of the implicit constraints on $α$. Rust chooses this option, which led to a tricky bug ^{1}.
In Rust, the type &'a T
means a reference to type T
which is valid
for lifetime 'a
. Lifetimes are ordered by a subtyping relation 'a: 'b
(pronounced "'a
outlives 'b
"), if the lifetime 'a
contains
all of 'b
. References to references &'a &'b T
are valid, but only
if 'b: 'a
as the reference's lifetime must not outlive its
contents.
There is also a longest lifetime 'static
, such that 'static: 'a
for any lifetime 'a
. The bug allows any reference to be converted to
a 'static
reference, breaking soundness guarantees:
// Counterexample by Aaron Turon
static UNIT: &'static &'static () = &&();
fn foo<'a, 'b, T>(_: &'a &'b (), v: &'b T) > &'a T { v }
fn bad<'c, T>(x: &'c T) > &'static T {
let f: fn(&'static &'c (), &'c T) > &'static T = foo;
f(UNIT, x)
}
The issue is that the type of foo
uses &'a &'b ()
, which is a
wellformed type only if 'b: 'a
, as a reference cannot outlive its
contents. This constraint 'b: 'a
is relied upon, to allow v
to be
returned.
Since Rust uses option (2) above, this constraint does not
appear explicitly in the type of foo
:
fn foo<'a, 'b, T> (_: &'a &'b (), v: &'b T) > &'a T
Contravariance allows arguments to be passed with a longer lifetime
than required by the function, allowing foo
to be used at the
following type, where one argument lifetime has been extended to
'static
:
fn foo<'a, 'b, T> (_: &'a &'static (), v: &'b T) > &'a T
However, the implicit constraint 'b: 'a
has been lost, as validity
now requires only that 'static: 'a
, which is always true. This
allows the type to be instantiated with 'a := 'static
, 'b := 'c
:
fn foo<T> (_: &'static &'static (), v: &'c T) > &'static T
which is unsound.