diff --git a/check/src/kindcheck.rs b/check/src/kindcheck.rs
index 4c2ca2d59d..40fe50abbd 100644
--- a/check/src/kindcheck.rs
+++ b/check/src/kindcheck.rs
@@ -157,7 +157,7 @@ impl<'a> KindCheck<'a> {
                 gen.kind = try!(self.find(&gen.id));
                 Ok((gen.kind.clone(), Type::generic(gen)))
             }
-            Type::Variable(_) => panic!("kindcheck called on variable"),
+            Type::Variable(_) => Ok((self.subs.new_var(), typ.clone())),
             Type::Builtin(builtin_typ) => Ok((self.builtin_kind(builtin_typ), typ.clone())),
             Type::App(ref ctor, ref args) => {
                 let (mut kind, ctor) = try!(self.kindcheck(ctor));
diff --git a/check/src/typecheck.rs b/check/src/typecheck.rs
index 9536ee9974..3816751a0a 100644
--- a/check/src/typecheck.rs
+++ b/check/src/typecheck.rs
@@ -636,7 +636,7 @@ impl<'a> Typecheck<'a> {
                 let types = try!(types.iter_mut()
                     .map(|&mut (ref mut symbol, ref mut typ)| {
                         if let Some(ref mut typ) = *typ {
-                            *typ = self.refresh_symbols_in_type(typ.clone());
+                            *typ = self.create_unifiable_signature(typ.clone());
                         }
                         let alias = try!(self.find_type_info(symbol));
 
@@ -856,7 +856,7 @@ impl<'a> Typecheck<'a> {
         if is_recursive {
             for bind in bindings.iter_mut() {
                 let typ = {
-                    bind.typ = self.refresh_symbols_in_type(bind.typ.clone());
+                    bind.typ = self.create_unifiable_signature(bind.typ.clone());
                     try!(self.kindcheck(&mut bind.typ));
                     self.instantiate_signature(&bind.typ)
                 };
@@ -876,7 +876,7 @@ impl<'a> Typecheck<'a> {
             // recursive
             let mut typ = if bind.arguments.is_empty() {
                 self.instantiate_signature(&bind.typ);
-                bind.typ = self.refresh_symbols_in_type(bind.typ.clone());
+                bind.typ = self.create_unifiable_signature(bind.typ.clone());
                 try!(self.kindcheck(&mut bind.typ));
                 self.typecheck(&mut bind.expression)
             } else {
@@ -912,6 +912,9 @@ impl<'a> Typecheck<'a> {
         debug!("Generalize {}", level);
         for bind in bindings {
             self.generalize_variables(level, &mut bind.expression);
+            if let Some(typ) = self.finish_type(level, &bind.typ) {
+                bind.typ = typ;
+            }
             self.finish_binding(level, bind);
         }
         debug!("Typecheck `in`");
@@ -938,7 +941,7 @@ impl<'a> Typecheck<'a> {
                 .typ
                 .as_mut()
                 .expect("Expected binding to have an aliased type");
-            *typ = self.refresh_symbols_in_type(typ.clone());
+            *typ = self.create_unifiable_signature(typ.clone());
         }
         {
             let subs = Substitution::new();
@@ -1165,7 +1168,11 @@ impl<'a> Typecheck<'a> {
         typ
     }
 
-    fn refresh_symbols_in_type(&mut self, typ: ArcType) -> ArcType {
+    // Replaces `Type::Id` types with the actual `Type::Alias` type it refers to
+    // Replaces variant names with the actual symbol they should refer to
+    // Instantiates Type::Hole with a fresh type variable to ensure the hole only ever refers to a
+    // single type variable
+    fn create_unifiable_signature(&mut self, typ: ArcType) -> ArcType {
         let mut f = |typ: &Type<Symbol, ArcType>| {
             match *typ {
                 Type::Alias(ref alias) => {
@@ -1218,6 +1225,7 @@ impl<'a> Typecheck<'a> {
                         None
                     }
                 }
+                Type::Hole => Some(self.subs.new_var()),
                 _ => None,
             }
         };
diff --git a/check/src/unify_type.rs b/check/src/unify_type.rs
index b37f009eb2..c186e2e7b0 100644
--- a/check/src/unify_type.rs
+++ b/check/src/unify_type.rs
@@ -425,9 +425,6 @@ impl<'a, 'e> Unifier<State<'a>, ArcType> for Merge<'e> {
         // `l` and `r` must have the same type, if one is a variable that variable is
         // unified with whatever the other type is
         let result = match (&**l, &**r) {
-            (&Type::Hole, &Type::Hole) => Ok(Some(subs.new_var())),
-            (_, &Type::Hole) => Ok(Some(l.clone())),
-            (&Type::Hole, _) => Ok(Some(r.clone())),
             (&Type::Variable(ref l), &Type::Variable(ref r)) if l.id == r.id => Ok(None),
             (&Type::Generic(ref l_gen), &Type::Variable(ref r_var)) => {
                 let left = match unifier.unifier.variables.get(&l_gen.id) {
diff --git a/check/tests/completion.rs b/check/tests/completion.rs
index dc6db1d104..30623a4c3a 100644
--- a/check/tests/completion.rs
+++ b/check/tests/completion.rs
@@ -94,6 +94,8 @@ let f x = f x
 
 #[test]
 fn binop() {
+    let _ = env_logger::init();
+    
     let env = MockEnv::new();
 
     let (mut expr, result) = support::typecheck_expr(r#"
diff --git a/check/tests/pass.rs b/check/tests/pass.rs
index 87f962ed2f..d76d1e5b39 100644
--- a/check/tests/pass.rs
+++ b/check/tests/pass.rs
@@ -176,7 +176,7 @@ macro_rules! assert_match {
     ($i: expr, $p: pat => $e: expr) => {
         match $i {
             $p => $e,
-            ref x => assert!(false, "Unexpected {}, found {:?}", stringify!($p), x)
+            ref x => assert!(false, "Expected {}, found {:?}", stringify!($p), x)
         }
     };
 }