ref mut bindings fail to enforce invariance

[nikomatsakis]

As originally "reported" here, ref mut bindings are not working properly:

#![allow(dead_code)]
use std::fmt::Debug;
struct S(Box<Debug + 'static>);
impl S {
    fn bar<'a>(&'a mut self)->&'a mut Box<Debug + 'a> {
        match self.0 { ref mut x => x } // should not compile, but does
    }
}
fn main() {}

[nikomatsakis]

triage: P-backcompat-lang (1.0 beta) -- soundness violation

[nikomatsakis]

Another test case:

#![allow(dead_code)]
use std::fmt::Debug;
struct S(Box<Debug + 'static>);
impl S {
    fn bar<'a>(&'a mut self)->&'a mut Box<Debug + 'a> {
        let ref mut x = self.0;
        x // should error!
    }
}
fn main() {}

[nikomatsakis]

This is a little bit more complex than I originally gave it credit for. In particular, the interaction between let ref and coercion is sort of non-obvious. Rather than trying to be too smart, I am currently thinking that I will apply a very simple rule of this form: if there are no ref bindings, we permit coercion on let and subtyping in general. Otherwise, we do no coercion on let and require an exact match. This seems to be safe and sane.

[nikomatsakis]

Some comments on my current plans (from the commit):

When matching against a pattern (either via match or let) that contains ref-bindings, do not permit any upcasting from the type of the value being matched. Similarly, do not permit coercion in a let.

This is a [breaking-change] in that it closes a type hole that previously existed, and in that coercion is not performed. You should be able to work around the latter by converting:

let ref mut x: T = expr;

into

let x: T = expr;
let ref mut x = x;

Restricting coercion not to apply in the case of let ref or let ref mut is sort of unexciting to me, but seems the best solution:

1. Mixing coercion and let ref or let ref mut is a bit odd, because you are taking
   the address of a (coerced) temporary, but only sometimes. It's not syntactically evident,
   in other words, what's going on. When you're doing a coercion, you're kind of
2. Put another way, I would like to preserve the relationship that
   equality <= subtyping <= coercion <= as-coercion, where this is
   an indication of the number of (T1,T2) pairs that are accepted by
   the various relations. Trying to mix let ref mut and coercion
   would create another kind of relation that is like coercion, but
   acts differently in the case where a precise match is needed.
3. In any case, this is strictly more conservative than what we had
   before and we can undo it in the future if we find a way to make
   coercion mix with type equality.

The change to match I feel ok about but similarly unthrilled. There is some subtle text already concerning whether to use eqtype or subtype for identifier bindings. The best fix I think would be to always have match use strict equality but use subtyping on identifier bindings, but the comment (*) explains why that's not working at the moment. As above, I think we can change this as we clean up the code there.