diff --git a/src/libcore/task.rs b/src/libcore/task.rs
index 2cdd24fb746b..c6dfd326e03d 100644
--- a/src/libcore/task.rs
+++ b/src/libcore/task.rs
@@ -694,7 +694,7 @@ fn test_try_fail() {
         fail
     } {
         result::err(()) { }
-        _ { fail; }
+        result::ok(()) { fail; }
     }
 }
 
diff --git a/src/rustc/middle/infer.rs b/src/rustc/middle/infer.rs
index abd44d6a8513..6a246f6d4bc3 100644
--- a/src/rustc/middle/infer.rs
+++ b/src/rustc/middle/infer.rs
@@ -293,14 +293,32 @@ impl unify_methods for infer_ctxt {
     }
 
     fn vars(a_id: uint, b_id: uint) -> ures {
-        #debug["vars(<T%u> <: <T%u>)",
-               a_id, b_id];
-
         // Need to make sub_id a subtype of sup_id.
         let {root: a_id, bounds: a_bounds} = self.get(a_id);
         let {root: b_id, bounds: b_bounds} = self.get(b_id);
 
+        #debug["vars(<T%u>=%s <: <T%u>=%s)",
+               a_id, self.bounds_to_str(a_bounds),
+               b_id, self.bounds_to_str(b_bounds)];
+
         if a_id == b_id { ret self.uok(); }
+
+        // If both A's UB and B's LB have already been bound to types,
+        // see if we can make those types subtypes.
+        alt (a_bounds.ub, b_bounds.lb) {
+          (some(a_ub), some(b_lb)) {
+            let r = self.try {|| self.tys(a_ub, b_lb) };
+            alt r {
+              result::ok(()) { ret result::ok(()); }
+              result::err(_) { /*fallthrough */ }
+            }
+          }
+          _ { /*fallthrough*/ }
+        }
+
+        // Otherwise, we need to merge A and B so as to guarantee that
+        // A remains a subtype of B.  Actually, there are other options,
+        // but that's the route we choose to take.
         self.merge(a_id, a_bounds, b_bounds).then {||
             // For max perf, we should consider the rank here.
             self.set(b_id, redirect(a_id));
@@ -309,18 +327,20 @@ impl unify_methods for infer_ctxt {
     }
 
     fn varty(a_id: uint, b: ty::t) -> ures {
-        #debug["varty(<T%u> <: %s)",
-               a_id, self.ty_to_str(b)];
         let {root: a_id, bounds: a_bounds} = self.get(a_id);
+        #debug["varty(<T%u>=%s <: %s)",
+               a_id, self.bounds_to_str(a_bounds),
+               self.ty_to_str(b)];
         let b_bounds = {lb: none, ub: some(b)};
         self.merge(a_id, a_bounds, b_bounds)
     }
 
     fn tyvar(a: ty::t, b_id: uint) -> ures {
-        #debug["tyvar(%s <: <T%u>)",
-               self.ty_to_str(a), b_id];
         let a_bounds = {lb: some(a), ub: none};
         let {root: b_id, bounds: b_bounds} = self.get(b_id);
+        #debug["tyvar(%s <: <T%u>=%s)",
+               self.ty_to_str(a),
+               b_id, self.bounds_to_str(b_bounds)];
         self.merge(b_id, a_bounds, b_bounds)
     }
 
@@ -532,6 +552,8 @@ impl unify_methods for infer_ctxt {
         if a == b { ret self.uok(); }
 
         alt (ty::get(a).struct, ty::get(b).struct) {
+          (ty::ty_bot, _) { self.uok() }
+
           (ty::ty_var(a_id), ty::ty_var(b_id)) {
             self.vars(a_id as uint, b_id as uint)
           }
@@ -542,9 +564,6 @@ impl unify_methods for infer_ctxt {
             self.tyvar(a, b_id as uint)
           }
 
-          (_, ty::ty_bot) { self.uok() }
-          (ty::ty_bot, _) { self.uok() }
-
           (ty::ty_nil, _) |
           (ty::ty_bool, _) |
           (ty::ty_int(_), _) |
diff --git a/src/rustc/middle/typeck.rs b/src/rustc/middle/typeck.rs
index 5c512690c17b..2dabc5b9faa3 100644
--- a/src/rustc/middle/typeck.rs
+++ b/src/rustc/middle/typeck.rs
@@ -2483,15 +2483,11 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
         let (if_t, if_bot) =
             alt elsopt {
               some(els) {
+                let if_t = next_ty_var(fcx);
                 let thn_bot = check_block(fcx, thn);
                 let thn_t = block_ty(fcx.ccx.tcx, thn);
-                let els_bot = check_expr_with(fcx, els, thn_t);
-                let els_t = expr_ty(fcx.ccx.tcx, els);
-                let if_t = if !ty::type_is_bot(els_t) {
-                    els_t
-                } else {
-                    thn_t
-                };
+                demand::simple(fcx, thn.span, if_t, thn_t);
+                let els_bot = check_expr_with(fcx, els, if_t);
                 (if_t, thn_bot & els_bot)
               }
               none {
@@ -2565,7 +2561,9 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
           }
 
           (_, _) if ty::is_binopable(tcx, lhs_t, op) {
-            let rhs_bot = check_expr_with(fcx, rhs, lhs_t);
+            let tvar = next_ty_var(fcx);
+            demand::simple(fcx, expr.span, tvar, lhs_t);
+            let rhs_bot = check_expr_with(fcx, rhs, tvar);
             let rhs_t = alt op {
               ast::eq | ast::lt | ast::le | ast::ne | ast::ge |
               ast::gt {
@@ -2646,9 +2644,9 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
       ast::expr_binary(ast::gt, lhs, rhs) |
       ast::expr_binary(ast::ge, lhs, rhs) {
         let tcx = fcx.ccx.tcx;
-        bot |= check_expr(fcx, lhs);
-        let lhs_t = expr_ty(tcx, lhs);
-        bot |= check_expr_with(fcx, rhs, lhs_t);
+        let tvar = next_ty_var(fcx);
+        bot |= check_expr_with(fcx, lhs, tvar);
+        bot |= check_expr_with(fcx, rhs, tvar);
         write_ty(tcx, id, ty::mk_bool(tcx));
       }
       ast::expr_binary(op, lhs, rhs) {
@@ -2782,7 +2780,8 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
       }
       ast::expr_log(_, lv, e) {
         bot = check_expr_with(fcx, lv, ty::mk_mach_uint(tcx, ast::ty_u32));
-        bot |= check_expr(fcx, e);
+        // Note: this does not always execute, so do not propagate bot:
+        check_expr(fcx, e);
         write_nil(tcx, id);
       }
       ast::expr_check(_, e) {
@@ -2850,13 +2849,14 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
           bot = !may_break(body);
       }
       ast::expr_alt(discrim, arms, _) {
-        bot = check_expr(fcx, discrim);
+        let pattern_ty = next_ty_var(fcx);
+        bot = check_expr_with(fcx, discrim, pattern_ty);
 
         let parent_block = tcx.region_map.rvalue_to_block.get(discrim.id);
 
         // Typecheck the patterns first, so that we get types for all the
         // bindings.
-        let pattern_ty = ty::expr_ty(tcx, discrim);
+        //let pattern_ty = ty::expr_ty(tcx, discrim);
         for arm: ast::arm in arms {
             let pcx = {
                 fcx: fcx,
@@ -3205,6 +3205,11 @@ fn check_expr_with_unifier(fcx: @fn_ctxt, expr: @ast::expr, unify: unifier,
     }
     if bot { write_ty(tcx, expr.id, ty::mk_bot(tcx)); }
 
+    #debug("type of expr %s is %s, expected is %s",
+           syntax::print::pprust::expr_to_str(expr),
+           ty_to_str(tcx, expr_ty(tcx, expr)),
+           ty_to_str(tcx, expected));
+
     unify(fcx, expr.span, expected, expr_ty(tcx, expr));
     ret bot;
 }
diff --git a/src/test/compile-fail/fn-variance-1.rs b/src/test/compile-fail/fn-variance-1.rs
new file mode 100644
index 000000000000..cb2dbde3d48f
--- /dev/null
+++ b/src/test/compile-fail/fn-variance-1.rs
@@ -0,0 +1,17 @@
+fn takes_mut(&&x: @mut int) { }
+fn takes_const(&&x: @const int) { }
+fn takes_imm(&&x: @int) { }
+
+fn apply<T>(t: T, f: fn(T)) {
+    f(t)
+}
+
+fn main() {
+    apply(@3, takes_mut); //! ERROR (values differ in mutability)
+    apply(@3, takes_const);
+    apply(@3, takes_imm);
+
+    apply(@mut 3, takes_mut);
+    apply(@mut 3, takes_const);
+    apply(@mut 3, takes_imm); //! ERROR (values differ in mutability)
+}
diff --git a/src/test/compile-fail/fn-variance-2.rs b/src/test/compile-fail/fn-variance-2.rs
new file mode 100644
index 000000000000..9d4254a708e2
--- /dev/null
+++ b/src/test/compile-fail/fn-variance-2.rs
@@ -0,0 +1,22 @@
+fn reproduce<T:copy>(t: T) -> fn@() -> T {
+    fn@() -> T { t }
+}
+
+fn main() {
+    // type of x is the variable X,
+    // with the lower bound @mut int
+    let x = @mut 3;
+
+    // type of r is fn@() -> X
+    let r = reproduce(x);
+
+    // Requires that X be a subtype of
+    // @mut int.
+    let f: @mut int = r();
+
+    // OK.
+    let g: @const int = r();
+
+    // Bad.
+    let h: @int = r(); //! ERROR (values differ in mutability)
+}
diff --git a/src/test/compile-fail/fn-variance-3.rs b/src/test/compile-fail/fn-variance-3.rs
new file mode 100644
index 000000000000..ab5b3b897a79
--- /dev/null
+++ b/src/test/compile-fail/fn-variance-3.rs
@@ -0,0 +1,21 @@
+fn mk_identity<T:copy>() -> fn@(T) -> T {
+    fn@(t: T) -> T { t }
+}
+
+fn main() {
+    // type of r is fn@(X) -> X
+    // for some fresh X
+    let r = mk_identity();
+
+    // @mut int <: X
+    r(@mut 3);
+
+    // @int <: X
+    //
+    // Note: this is really an inference failure.
+    // The correct answer would be to make X
+    // equal to @const int, but we are not (yet)
+    // smart enough.
+    r(@3); //! ERROR (values differ in mutability)
+
+}
diff --git a/src/test/run-pass/unreachable-code.rs b/src/test/run-pass/unreachable-code.rs
index 5b3a65bee01c..71f3fa6d3ef6 100644
--- a/src/test/run-pass/unreachable-code.rs
+++ b/src/test/run-pass/unreachable-code.rs
@@ -35,9 +35,9 @@ fn ret_guard() {
     }
 }
 
-fn rec_ret() { let _r = {c: ret}; }
+fn rec_ret() { let _r: {c: int} = {c: ret}; }
 
-fn vec_ret() { let _v = [1, 2, ret, 4]; }
+fn vec_ret() { let _v: [int] = [1, 2, ret, 4]; }
 
 fn fail_then_concat() {
     let mut x = [], y = [3];
diff --git a/src/test/run-pass/weird-exprs.rs b/src/test/run-pass/weird-exprs.rs
index 6da9397044ce..4e0c69cdbcc5 100644
--- a/src/test/run-pass/weird-exprs.rs
+++ b/src/test/run-pass/weird-exprs.rs
@@ -1,6 +1,6 @@
 // Just a grab bag of stuff that you wouldn't want to actually write.
 
-fn strange() -> bool { let _x = ret true; }
+fn strange() -> bool { let _x: bool = ret true; }
 
 fn funny() {
     fn f(_x: ()) { }
@@ -19,8 +19,8 @@ fn zombiejesus() {
     do  {
         while (ret) {
             if (ret) {
-                alt (ret) {
-                    _ {
+                alt check (ret) {
+                    1 {
                         if (ret) {
                             ret
                         } else {
@@ -51,13 +51,13 @@ fn canttouchthis() -> uint {
     pure fn p() -> bool { true }
     let _a = (assert (true)) == (check (p()));
     let _c = (check (p())) == ();
-    let _b = (log(debug, 0) == (ret 0u));
+    let _b: bool = (log(debug, 0) == (ret 0u));
 }
 
 fn angrydome() {
     loop { if break { } }
     let mut i = 0;
-    do  { i += 1; if i == 1 { alt cont { _ { } } } } while false
+    do  { i += 1; if i == 1 { alt check cont { 1 { } } } } while false
 }
 
 fn evil_lincoln() { let evil <- #debug("lincoln"); }