diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.1.12
+version: 0.1.13
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
diff --git a/src/Language/PureScript/TypeChecker/Types.hs b/src/Language/PureScript/TypeChecker/Types.hs
--- a/src/Language/PureScript/TypeChecker/Types.hs
+++ b/src/Language/PureScript/TypeChecker/Types.hs
@@ -23,8 +23,8 @@
 import Data.Function
 import qualified Data.Data as D
 import Data.Generics
-       (something, everywhere, everywhereM, everything, everywhereBut,
-        mkT, mkM, mkQ, extM, extQ)
+       (extT, something, everywhere, everywhereM, everything,
+        everywhereBut, mkT, mkM, mkQ, extM, extQ)
 
 import Language.PureScript.Values
 import Language.PureScript.Types
@@ -117,7 +117,7 @@
   unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
   unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do
     sk <- skolemize ident1 ty1
-    replaced <- replaceVarsWithUnknowns [ident2] ty2
+    replaced <- replaceVarWithUnknown ident2 ty2
     sk `unifyTypes` replaced
   unifyTypes' (ForAll ident ty1) ty2 = do
     sk <- skolemize ident ty1
@@ -196,7 +196,17 @@
 setifyAll = everywhere (mkT setify)
 
 varIfUnknown :: Type -> Type
-varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) ty
+varIfUnknown ty =
+  let unks = nub $ unknowns ty
+      toName = (:) 't' . show
+      ty' = everywhere (mkT rowToVar) . everywhere (mkT typeToVar) $ ty
+      typeToVar :: Type -> Type
+      typeToVar (TUnknown (Unknown u)) = TypeVar (toName u)
+      typeToVar t = t
+      rowToVar :: Row -> Row
+      rowToVar (RUnknown (Unknown u)) = RowVar (toName u)
+      rowToVar t = t
+  in mkForAll (sort . map toName $ unks) ty'
 
 replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
 replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
@@ -216,32 +226,14 @@
   replace t = t
 
 replaceAllVarsWithUnknowns :: Type -> Subst Check Type
-replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [ident] ty >>= replaceAllVarsWithUnknowns
+replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
 replaceAllVarsWithUnknowns ty = return ty
 
-replaceVarsWithUnknowns :: [String] -> Type -> Subst Check Type
-replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
-  where
-  f :: Type -> StateT (M.Map String Int) (Subst Check) Type
-  f (TypeVar var) | var `elem` idents = do
-    m <- get
-    n <- lift fresh'
-    case M.lookup var m of
-      Nothing -> do
-        put (M.insert var n m)
-        return $ TUnknown (Unknown n)
-      Just u -> return $ TUnknown (Unknown u)
-  f t = return t
-  g :: Row -> StateT (M.Map String Int) (Subst Check) Row
-  g (RowVar var) | var `elem` idents = do
-    m <- get
-    n <- lift fresh'
-    case M.lookup var m of
-      Nothing -> do
-        put (M.insert var n m)
-        return $ RUnknown (Unknown n)
-      Just u -> return $ RUnknown (Unknown u)
-  g r = return r
+replaceVarWithUnknown :: String -> Type -> Subst Check Type
+replaceVarWithUnknown ident ty = do
+  tu <- fresh
+  ru <- fresh
+  return $ replaceRowVars ident ru . replaceTypeVars ident tu $ ty
 
 replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
 replaceAllTypeSynonyms d = do
@@ -380,7 +372,7 @@
   replaced <- expandTypeSynonym name args
   inferProperty replaced prop
 inferProperty (ForAll ident ty) prop = do
-  replaced <- replaceVarsWithUnknowns [ident] ty
+  replaced <- replaceVarWithUnknown ident ty
   inferProperty replaced prop
 inferProperty _ prop = return Nothing
 
@@ -723,8 +715,8 @@
 checkFunctionApplications _ _ [] _ = error "Nullary function application"
 checkFunctionApplications m fnTy [args] ret = checkFunctionApplication m fnTy args ret
 checkFunctionApplications m fnTy (args:argss) ret = do
-  f <- fresh
-  checkFunctionApplication m fnTy args f
+  argTys <- mapM (infer m) args
+  f <- inferFunctionApplication m fnTy argTys
   checkFunctionApplications m f argss ret
 
 checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
@@ -736,13 +728,33 @@
     ++ ", expecting value of type "
     ++ prettyPrintType ret ++ ":\n" ++ msg
 
+inferFunctionApplication :: M.Map Ident Type -> Type -> [Type] -> Subst Check Type
+inferFunctionApplication m (Function argTys retTy) args = do
+  guardWith "Incorrect number of function arguments" (length args == length argTys)
+  zipWithM subsumes args argTys
+  return retTy
+inferFunctionApplication m (ForAll ident ty) args = do
+  replaced <- replaceVarWithUnknown ident ty
+  inferFunctionApplication m replaced args
+inferFunctionApplication m u@(TUnknown _) args = do
+  ret <- fresh
+  args' <- mapM replaceAllVarsWithUnknowns args
+  u ~~ Function args' ret
+  return ret
+inferFunctionApplication m (SaturatedTypeSynonym name tyArgs) args  = do
+  ty <- expandTypeSynonym name tyArgs
+  inferFunctionApplication m ty args
+inferFunctionApplication _ fnTy args = throwError $ "Cannot apply function of type "
+  ++ prettyPrintType fnTy
+  ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)
+
 checkFunctionApplication' :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
 checkFunctionApplication' m (Function argTys retTy) args ret = do
   guardWith "Incorrect number of function arguments" (length args == length argTys)
   zipWithM (check m) args argTys
   retTy `subsumes` ret
 checkFunctionApplication' m (ForAll ident ty) args ret = do
-  replaced <- replaceVarsWithUnknowns [ident] ty
+  replaced <- replaceVarWithUnknown ident ty
   checkFunctionApplication m replaced args ret
 checkFunctionApplication' m u@(TUnknown _) args ret = do
   tyArgs <- mapM (\arg -> infer m arg >>= replaceAllVarsWithUnknowns) args
@@ -750,14 +762,14 @@
 checkFunctionApplication' m (SaturatedTypeSynonym name tyArgs) args ret = do
   ty <- expandTypeSynonym name tyArgs
   checkFunctionApplication' m ty args ret
-checkFunctionApplication' _ fnTy args ret = throwError $ "Cannot apply function of type "
+checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "
   ++ prettyPrintType fnTy
-  ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
-  ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."
+  ++ " to argument(s) " ++ intercalate ", " (map prettyPrintValue args)
+  ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."
 
 subsumes :: Type -> Type -> Subst Check ()
 subsumes (ForAll ident ty1) ty2 = do
-  replaced <- replaceVarsWithUnknowns [ident] ty1
+  replaced <- replaceVarWithUnknown ident ty1
   replaced `subsumes` ty2
 subsumes (Function args1 ret1) (Function args2 ret2) = do
   zipWithM subsumes args2 args1