diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.1.9
+version: 0.1.11
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
@@ -36,6 +36,7 @@
                      Language.PureScript.TypeChecker.Monad
                      Language.PureScript.TypeChecker.Types
                      Language.PureScript.TypeChecker.Synonyms
+                     Language.PureScript.Unknown
     exposed: True
     buildable: True
     hs-source-dirs: src
diff --git a/src/Language/PureScript.hs b/src/Language/PureScript.hs
--- a/src/Language/PureScript.hs
+++ b/src/Language/PureScript.hs
@@ -32,7 +32,7 @@
 compile :: [Declaration] -> Either String (String, String, Environment)
 compile decls = do
   bracketted <- rebracket decls
-  (_, env) <- check (typeCheckAll bracketted)
-  let js = prettyPrintJS . map optimize . concat . mapMaybe (declToJs Nothing global) $ bracketted
+  (_, env) <- runCheck (typeCheckAll bracketted)
+  let js = prettyPrintJS . map optimize . concat . mapMaybe (\decl -> declToJs Nothing global decl env) $ bracketted
   let exts = intercalate "\n" . mapMaybe (externToPs 0 global env) $ bracketted
   return (js, exts, env)
diff --git a/src/Language/PureScript/CodeGen/Externs.hs b/src/Language/PureScript/CodeGen/Externs.hs
--- a/src/Language/PureScript/CodeGen/Externs.hs
+++ b/src/Language/PureScript/CodeGen/Externs.hs
@@ -27,12 +27,12 @@
 externToPs :: Int -> ModulePath -> Environment -> Declaration -> Maybe String
 externToPs indent path env (ValueDeclaration name _) = do
   (ty, _) <- M.lookup (path, name) $ names env
-  return $ replicate indent ' ' ++ "foreign import " ++ show name ++ " :: " ++ prettyPrintPolyType ty
+  return $ replicate indent ' ' ++ "foreign import " ++ show name ++ " :: " ++ prettyPrintType ty
 externToPs indent path env (DataDeclaration name _ _) = do
   (kind, _) <- M.lookup (path, name) $ types env
   return $ replicate indent ' ' ++ "foreign import data " ++ show name ++ " :: " ++ prettyPrintKind kind
 externToPs indent path env (ExternMemberDeclaration member name ty) =
-  return $ replicate indent ' ' ++ "foreign import member " ++ show member ++ " " ++ show name ++ " :: " ++ prettyPrintPolyType ty
+  return $ replicate indent ' ' ++ "foreign import member " ++ show member ++ " " ++ show name ++ " :: " ++ prettyPrintType ty
 externToPs indent path env (ExternDataDeclaration name kind) =
   return $ replicate indent ' ' ++ "foreign import data " ++ show name ++ " :: " ++ prettyPrintKind kind
 externToPs indent path env (TypeSynonymDeclaration name args ty) =
diff --git a/src/Language/PureScript/CodeGen/JS.hs b/src/Language/PureScript/CodeGen/JS.hs
--- a/src/Language/PureScript/CodeGen/JS.hs
+++ b/src/Language/PureScript/CodeGen/JS.hs
@@ -20,11 +20,13 @@
 import Data.Char
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.List (intercalate)
+import qualified Data.Map as M
 import qualified Control.Arrow as A
 import Control.Arrow ((<+>), second)
 import Control.Monad (forM)
 import Control.Applicative
 
+import Language.PureScript.TypeChecker (Environment, names)
 import Language.PureScript.Types
 import Language.PureScript.Values
 import Language.PureScript.Names
@@ -33,17 +35,17 @@
 import Language.PureScript.CodeGen.Monad
 import Language.PureScript.CodeGen.JS.AST as AST
 
-declToJs :: Maybe Ident -> ModulePath -> Declaration -> Maybe [JS]
-declToJs mod mp (ValueDeclaration ident (Abs args ret)) =
+declToJs :: Maybe Ident -> ModulePath -> Declaration -> Environment -> Maybe [JS]
+declToJs mod mp (ValueDeclaration ident (Abs args ret)) _ =
   Just $ JSFunction (Just ident) args (JSBlock [JSReturn (valueToJs mp ret)]) :
          maybe [] (return . setProperty (identToJs ident) (JSVar ident)) mod
-declToJs mod mp (ValueDeclaration ident val) =
+declToJs mod mp (ValueDeclaration ident val) _ =
   Just $ JSVariableIntroduction ident (Just (valueToJs mp val)) :
          maybe [] (return . setProperty (identToJs ident) (JSVar ident)) mod
-declToJs mod _ (ExternMemberDeclaration member ident _) =
+declToJs mod _ (ExternMemberDeclaration member ident _) _ =
   Just $ JSFunction (Just ident) [Ident "value"] (JSBlock [JSReturn (JSAccessor member (JSVar (Ident "value")))]) :
          maybe [] (return . setProperty (show ident) (JSVar ident)) mod
-declToJs mod mp (DataDeclaration _ _ ctors) =
+declToJs mod mp (DataDeclaration _ _ ctors) _ =
   Just $ flip concatMap ctors $ \(pn@(ProperName ctor), maybeTy) ->
     let
       ctorJs =
@@ -54,14 +56,21 @@
                         (JSObjectLiteral [ ("ctor", JSStringLiteral (show (Qualified mp pn)))
                                          , ("value", JSVar (Ident "value")) ])])
     in ctorJs : maybe [] (return . setProperty ctor (JSVar (Ident ctor))) mod
-declToJs mod mp (ModuleDeclaration pn@(ProperName name) decls) =
+declToJs mod mp (ModuleDeclaration pn@(ProperName name) decls) env =
   Just $ [ JSVariableIntroduction (Ident name) Nothing
          , JSApp (JSFunction Nothing [Ident name]
-                             (JSBlock (concat $ mapMaybe (declToJs (Just (Ident name)) (subModule mp pn)) decls)))
-                 [JSAssignment (JSAssignVariable (Ident name) )
+                             (JSBlock (concat $ mapMaybe (\decl -> declToJs (Just (Ident name)) (subModule mp pn) decl env) decls)))
+                 [JSAssignment (JSAssignVariable (Ident name))
                                (JSBinary Or (JSVar (Ident name)) (JSObjectLiteral []))]] ++
          maybe [] (return . setProperty name (JSVar (Ident name))) mod
-declToJs _ _ _ = Nothing
+declToJs mod omp (ImportDeclaration mp idents) env =
+  Just $ case idents of
+    Nothing ->
+      let idents = map snd  . filter ((== mp) . fst) . M.keys $ names env
+      in map mkLocal idents
+    Just idents -> map mkLocal idents
+ where mkLocal ident = JSVariableIntroduction ident (Just (qualifiedToJS identToJs (Qualified mp ident)))
+declToJs _ _ _ _ = Nothing
 
 setProperty :: String -> JS -> Ident -> JS
 setProperty prop val mod = JSAssignment (JSAssignProperty prop (JSAssignVariable mod)) val
@@ -87,10 +96,10 @@
 valueToJs m (TypedValue val _) = valueToJs m val
 
 qualifiedToJS :: (a -> String) -> Qualified a -> JS
-qualifiedToJS f (Qualified (ModulePath parts) a) = delimited (f a : reverse (map show parts))
-  where
-  delimited [part] = JSVar (Ident (part))
-  delimited (part:parts) = JSAccessor part (delimited parts)
+qualifiedToJS f (Qualified (ModulePath parts) a) =
+  delimited (f a : reverse (map show parts))
+ where delimited [part]       = JSVar (Ident (part))
+       delimited (part:parts) = JSAccessor part (delimited parts)
 
 bindersToJs :: ModulePath -> [(Binder, Value)] -> JS -> Gen JS
 bindersToJs m binders val = do
diff --git a/src/Language/PureScript/Declarations.hs b/src/Language/PureScript/Declarations.hs
--- a/src/Language/PureScript/Declarations.hs
+++ b/src/Language/PureScript/Declarations.hs
@@ -30,12 +30,14 @@
 data Fixity = Fixity Associativity Precedence deriving (Show, D.Data, D.Typeable)
 
 data Declaration
-  = DataDeclaration ProperName [String] [(ProperName, Maybe Type)]
-  | TypeSynonymDeclaration ProperName [String] Type
+  = DataDeclaration ProperName [String] [(ProperName, Maybe PolyType)]
+  | TypeSynonymDeclaration ProperName [String] PolyType
   | TypeDeclaration Ident PolyType
   | ValueDeclaration Ident Value
   | ExternDeclaration Ident PolyType
   | ExternMemberDeclaration String Ident PolyType
   | ExternDataDeclaration ProperName Kind
   | FixityDeclaration Fixity String
-  | ModuleDeclaration ProperName [Declaration] deriving (Show, D.Data, D.Typeable)
+  | ModuleDeclaration ProperName [Declaration]
+  | ImportDeclaration ModulePath (Maybe [Ident])
+  deriving (Show, D.Data, D.Typeable)
diff --git a/src/Language/PureScript/Kinds.hs b/src/Language/PureScript/Kinds.hs
--- a/src/Language/PureScript/Kinds.hs
+++ b/src/Language/PureScript/Kinds.hs
@@ -17,9 +17,10 @@
 module Language.PureScript.Kinds where
 
 import Data.Data
+import Language.PureScript.Unknown
 
 data Kind
-  = KUnknown Int
+  = KUnknown (Unknown Kind)
   | Star
   | Row
   | FunKind Kind Kind deriving (Show, Eq, Data, Typeable)
diff --git a/src/Language/PureScript/Names.hs b/src/Language/PureScript/Names.hs
--- a/src/Language/PureScript/Names.hs
+++ b/src/Language/PureScript/Names.hs
@@ -30,7 +30,10 @@
 instance Show ProperName where
   show = runProperName
 
-data ModulePath = ModulePath [ProperName] deriving (Show, Eq, Ord, Data, Typeable)
+data ModulePath = ModulePath [ProperName] deriving (Eq, Ord, Data, Typeable)
+
+instance Show ModulePath where
+  show (ModulePath segments) = intercalate "." $ map show segments
 
 subModule :: ModulePath -> ProperName -> ModulePath
 subModule (ModulePath mp) name = ModulePath (mp ++ [name])
diff --git a/src/Language/PureScript/Parser/Common.hs b/src/Language/PureScript/Parser/Common.hs
--- a/src/Language/PureScript/Parser/Common.hs
+++ b/src/Language/PureScript/Parser/Common.hs
@@ -120,22 +120,27 @@
 operator         = PT.operator          tokenParser
 stringLiteral    = PT.stringLiteral     tokenParser
 whiteSpace       = PT.whiteSpace        tokenParser
-parens           = PT.parens            tokenParser
-braces           = PT.braces            tokenParser
-angles           = PT.angles            tokenParser
 squares          = PT.squares           tokenParser
 semi             = PT.semi              tokenParser
 comma            = PT.comma             tokenParser
 colon            = PT.colon             tokenParser
 dot              = PT.dot               tokenParser
-semiSep          = PT.semiSep           tokenParser
-semiSep1         = PT.semiSep1          tokenParser
-commaSep         = PT.commaSep          tokenParser
-commaSep1        = PT.commaSep1         tokenParser
 natural          = PT.natural           tokenParser
 
-tick :: P.Parsec String u Char
+parens = P.between (lexeme $ P.char '(') (lexeme $ indented *> P.char ')') . (indented *>)
+braces = P.between (lexeme $ P.char '{') (lexeme $ indented *> P.char '}') . (indented *>)
+angles = P.between (lexeme $ P.char '<') (lexeme $ indented *> P.char '>') . (indented *>)
+
+sepBy p s = P.sepBy (indented *> p) (indented *> s)
+sepBy1 p s = P.sepBy1 (indented *> p) (indented *> s)
+
+semiSep          = flip sepBy semi
+semiSep1         = flip sepBy1 semi
+commaSep         = flip sepBy comma
+commaSep1        = flip sepBy1 comma
+
 tick = lexeme $ P.char '`'
+pipe = lexeme $ P.char '|'
 
 properName :: P.Parsec String u ProperName
 properName = lexeme $ ProperName <$> P.try ((:) <$> P.upper <*> many (PT.identLetter langDef) P.<?> "name")
@@ -167,7 +172,7 @@
 operatorOrBuiltIn :: P.Parsec String u String
 operatorOrBuiltIn = P.try operator <|> P.choice (map (\s -> P.try (reservedOp s) >> return s) builtInOperators)
 
-parseIdent :: P.Parsec String u Ident
+parseIdent :: P.Parsec String ParseState Ident
 parseIdent = (Ident <$> identifier) <|> (Op <$> parens operatorOrBuiltIn)
 
 parseIdentInfix :: P.Parsec String ParseState (Qualified Ident)
diff --git a/src/Language/PureScript/Parser/Declarations.hs b/src/Language/PureScript/Parser/Declarations.hs
--- a/src/Language/PureScript/Parser/Declarations.hs
+++ b/src/Language/PureScript/Parser/Declarations.hs
@@ -28,6 +28,7 @@
 import qualified Text.Parsec as P
 import qualified Text.Parsec.Pos as P
 
+import Language.PureScript.Names
 import Language.PureScript.Values
 import Language.PureScript.Types
 import Language.PureScript.Parser.State
@@ -43,7 +44,7 @@
   name <- indented *> properName
   tyArgs <- many (indented *> identifier)
   lexeme $ indented *> P.char '='
-  ctors <- P.sepBy1 ((,) <$> (indented *> properName) <*> P.optionMaybe parseType) (lexeme $ indented *> P.char '|')
+  ctors <- sepBy1 ((,) <$> properName <*> P.optionMaybe (indented *> parsePolyType)) pipe
   return $ DataDeclaration name tyArgs ctors
 
 parseTypeDeclaration :: P.Parsec String ParseState Declaration
@@ -55,7 +56,7 @@
 parseTypeSynonymDeclaration =
   TypeSynonymDeclaration <$> (P.try (reserved "type") *> indented *> properName)
                          <*> many (indented *> identifier)
-                         <*> (lexeme (indented *> P.char '=') *> parseType)
+                         <*> (lexeme (indented *> P.char '=') *> parsePolyType)
 
 parseValueDeclaration :: P.Parsec String ParseState Declaration
 parseValueDeclaration =
@@ -96,6 +97,17 @@
   decls <- mark (P.many (same *> parseDeclaration))
   return $ ModuleDeclaration name decls
 
+parseModulePath :: P.Parsec String ParseState ModulePath
+parseModulePath = ModulePath <$> properName `sepBy1` dot
+
+parseImportDeclaration :: P.Parsec String ParseState Declaration
+parseImportDeclaration = do
+  reserved "import"
+  indented
+  modulePath <- parseModulePath
+  idents <- P.optionMaybe $ parens $ commaSep1 parseIdent
+  return $ ImportDeclaration modulePath idents
+
 parseDeclaration :: P.Parsec String ParseState Declaration
 parseDeclaration = P.choice
                    [ parseDataDeclaration
@@ -104,7 +116,8 @@
                    , parseValueDeclaration
                    , parseExternDeclaration
                    , parseFixityDeclaration
-                   , parseModuleDeclaration ] P.<?> "declaration"
+                   , parseModuleDeclaration
+                   , parseImportDeclaration ] P.<?> "declaration"
 
 parseDeclarations :: P.Parsec String ParseState [Declaration]
 parseDeclarations = whiteSpace *> mark (P.many (same *> parseDeclaration)) <* P.eof
diff --git a/src/Language/PureScript/Parser/Types.hs b/src/Language/PureScript/Parser/Types.hs
--- a/src/Language/PureScript/Parser/Types.hs
+++ b/src/Language/PureScript/Parser/Types.hs
@@ -25,6 +25,7 @@
 import qualified Text.Parsec as P
 import qualified Text.Parsec.Expr as P
 import Control.Arrow (Arrow(..))
+import Control.Monad (unless)
 
 parseNumber :: P.Parsec String ParseState Type
 parseNumber = const Number <$> reserved "Number"
@@ -43,7 +44,7 @@
 
 parseFunction :: P.Parsec String ParseState Type
 parseFunction = do
-  args <- lexeme $ parens $ commaSep parseType
+  args <- lexeme $ parens $ commaSep parsePolyType
   lexeme $ P.string "->"
   resultType <- parseType
   return $ Function args resultType
@@ -54,6 +55,10 @@
 parseTypeConstructor :: P.Parsec String ParseState Type
 parseTypeConstructor = TypeConstructor <$> parseQualified properName
 
+parseForAll :: P.Parsec String ParseState Type
+parseForAll = (mkForAll <$> (P.try (reserved "forall") *> P.many1 (indented *> identifier) <* indented <* dot)
+                        <*> parseType)
+
 parseTypeAtom :: P.Parsec String ParseState Type
 parseTypeAtom = indented *> P.choice (map P.try
             [ parseNumber
@@ -64,27 +69,36 @@
             , parseFunction
             , parseTypeVariable
             , parseTypeConstructor
+            , parseForAll
             , parens parseType ])
 
-parsePolyType :: P.Parsec String ParseState PolyType
-parsePolyType = (PolyType <$> P.option [] (indented *> reserved "forall" *> many (indented *> identifier) <* indented <* dot)
-                          <*> parseType) P.<?> "polymorphic type"
-
-parseType :: P.Parsec String ParseState Type
-parseType = (P.buildExpressionParser operators . buildPostfixParser postfixTable $ parseTypeAtom) P.<?> "type"
+parseAnyType :: P.Parsec String ParseState Type
+parseAnyType = (P.buildExpressionParser operators . buildPostfixParser postfixTable $ parseTypeAtom) P.<?> "type"
   where
   postfixTable :: [P.Parsec String ParseState (Type -> Type)]
   postfixTable = [ flip TypeApp <$> P.try (indented *> parseTypeAtom) ]
   operators = [ [ P.Infix (lexeme (P.try (P.string "->")) >> return (\t1 t2 -> Function [t1] t2)) P.AssocRight ] ]
 
+parseType :: P.Parsec String ParseState Type
+parseType = do
+  ty <- parseAnyType
+  unless (isMonoType ty) $ P.unexpected "polymorphic type"
+  return ty
+
+parsePolyType :: P.Parsec String ParseState PolyType
+parsePolyType = do
+  ty <- parseAnyType
+  unless (isPolyType ty) $ P.unexpected "polymorphic type"
+  return ty
+
 parseNameAndType :: P.Parsec String ParseState (String, Type)
-parseNameAndType = (,) <$> (indented *> identifier <* indented <* lexeme (P.string "::")) <*> parseType
+parseNameAndType = (,) <$> (indented *> identifier <* indented <* lexeme (P.string "::")) <*> parsePolyType
 
 parseRowEnding :: P.Parsec String ParseState Row
 parseRowEnding = P.option REmpty (RowVar <$> (lexeme (indented *> P.char '|') *> indented *> identifier))
 
 parseRow :: P.Parsec String ParseState Row
-parseRow = (fromList <$> (parseNameAndType `P.sepBy` (indented *> comma)) <*> parseRowEnding) P.<?> "row"
+parseRow = (fromList <$> (commaSep parseNameAndType) <*> parseRowEnding) P.<?> "row"
   where
   fromList :: [(String, Type)] -> Row -> Row
   fromList [] r = r
diff --git a/src/Language/PureScript/Parser/Values.hs b/src/Language/PureScript/Parser/Values.hs
--- a/src/Language/PureScript/Parser/Values.hs
+++ b/src/Language/PureScript/Parser/Values.hs
@@ -47,10 +47,10 @@
 parseBooleanLiteral = BooleanLiteral <$> booleanLiteral
 
 parseArrayLiteral :: P.Parsec String ParseState Value
-parseArrayLiteral = ArrayLiteral <$> C.squares (parseValue `P.sepBy` (C.indented *> C.comma))
+parseArrayLiteral = ArrayLiteral <$> C.squares (C.commaSep parseValue)
 
 parseObjectLiteral :: P.Parsec String ParseState Value
-parseObjectLiteral = ObjectLiteral <$> C.braces (parseIdentifierAndValue `P.sepBy` (C.indented *> C.comma))
+parseObjectLiteral = ObjectLiteral <$> C.braces (C.commaSep parseIdentifierAndValue)
 
 parseIdentifierAndValue :: P.Parsec String ParseState (String, Value)
 parseIdentifierAndValue = (,) <$> (C.indented *> C.identifier <* C.indented <* C.colon)
@@ -66,7 +66,7 @@
   where
   manyArgs :: P.Parsec String ParseState (Value -> Value)
   manyArgs = do
-    args <- C.parens ((C.indented *> C.parseIdent) `P.sepBy` (C.indented *> C.comma))
+    args <- C.parens (C.commaSep C.parseIdent)
     return $ Abs args
   singleArg :: P.Parsec String ParseState (Value -> Value)
   singleArg = Abs . return <$> C.parseIdent
@@ -76,7 +76,7 @@
 
 parseApp :: P.Parsec String ParseState Value
 parseApp = App <$> parseValue
-               <*> (C.indented *> C.parens (parseValue `P.sepBy` (C.indented *> C.comma)))
+               <*> (C.indented *> C.parens (C.commaSep parseValue))
 
 parseVar :: P.Parsec String ParseState Value
 parseVar = Var <$> C.parseQualified C.parseIdent
@@ -134,9 +134,9 @@
   where
   indexersAndAccessors = C.buildPostfixParser postfixTable1 parseValueAtom
   postfixTable1 = [ Accessor <$> (C.indented *> C.dot *> C.indented *> C.identifier)
-                  , P.try $ flip ObjectUpdate <$> (C.indented *> C.braces ((C.indented *> parsePropertyUpdate) `P.sepBy1` (C.indented *> C.comma))) ]
+                  , P.try $ flip ObjectUpdate <$> (C.indented *> C.braces (C.commaSep1 (C.indented *> parsePropertyUpdate))) ]
   postfixTable2 = [ P.try (C.indented *> indexersAndAccessors >>= \t2 -> return (\t1 -> App t1 [t2]))
-                  , P.try $ flip App <$> (C.indented *> C.parens (parseValue `P.sepBy` (C.indented *> C.comma)))
+                  , P.try $ flip App <$> (C.indented *> C.parens (C.commaSep parseValue))
                   , flip TypedValue <$> (P.try (C.lexeme (C.indented *> P.string "::")) *> parsePolyType) ]
   operators = [ [ Prefix $ C.lexeme (P.try $ C.indented *> C.reservedOp "!") >> return (Unary Not)
                 , Prefix $ C.lexeme (P.try $ C.indented *> C.reservedOp "~") >> return (Unary BitwiseNot)
@@ -221,10 +221,10 @@
 parseUnaryBinder = UnaryBinder <$> C.lexeme (C.parseQualified C.properName) <*> (C.indented *> parseBinder)
 
 parseObjectBinder :: P.Parsec String ParseState Binder
-parseObjectBinder = ObjectBinder <$> C.braces ((C.indented *> parseIdentifierAndBinder) `P.sepBy` (C.indented *> C.comma))
+parseObjectBinder = ObjectBinder <$> C.braces (C.commaSep (C.indented *> parseIdentifierAndBinder))
 
 parseArrayBinder :: P.Parsec String ParseState Binder
-parseArrayBinder = C.squares $ ArrayBinder <$> ((C.indented *> parseBinder) `P.sepBy` (C.indented *> C.comma))
+parseArrayBinder = C.squares $ ArrayBinder <$> (C.commaSep (C.indented *> parseBinder))
                                            <*> P.optionMaybe (C.indented *> C.colon *> C.indented *> parseBinder)
 
 parseNamedBinder :: P.Parsec String ParseState Binder
diff --git a/src/Language/PureScript/Pretty/Kinds.hs b/src/Language/PureScript/Pretty/Kinds.hs
--- a/src/Language/PureScript/Pretty/Kinds.hs
+++ b/src/Language/PureScript/Pretty/Kinds.hs
@@ -25,13 +25,14 @@
 
 import Language.PureScript.Kinds
 import Language.PureScript.Pretty.Common
+import Language.PureScript.Unknown
 
 typeLiterals :: Pattern () Kind String
 typeLiterals = mkPattern match
   where
   match Star = Just "*"
   match Row = Just "#"
-  match (KUnknown u) = Just $ 'u' : show u
+  match (KUnknown (Unknown u)) = Just $ 'u' : show u
   match _ = Nothing
 
 funKind :: Pattern () Kind (Kind, Kind)
diff --git a/src/Language/PureScript/Pretty/Types.hs b/src/Language/PureScript/Pretty/Types.hs
--- a/src/Language/PureScript/Pretty/Types.hs
+++ b/src/Language/PureScript/Pretty/Types.hs
@@ -14,8 +14,7 @@
 
 module Language.PureScript.Pretty.Types (
     prettyPrintType,
-    prettyPrintRow,
-    prettyPrintPolyType
+    prettyPrintRow
 ) where
 
 import Data.Maybe (fromMaybe)
@@ -31,6 +30,7 @@
 import Language.PureScript.Declarations
 import Language.PureScript.TypeChecker.Monad
 import Language.PureScript.Pretty.Common
+import Language.PureScript.Unknown
 
 typeLiterals :: Pattern () Type String
 typeLiterals = mkPattern match
@@ -42,8 +42,10 @@
   match (Object row) = Just $ "{ " ++ prettyPrintRow row ++ " }"
   match (TypeVar var) = Just var
   match (TypeConstructor ctor) = Just $ show ctor
-  match (TUnknown u) = Just $ 'u' : show u
+  match (TUnknown (Unknown u)) = Just $ 'u' : show u
+  match (Skolem s) = Just $ 's' : show s
   match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"
+  match (ForAll ident ty) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty
   match _ = Nothing
 
 prettyPrintRow :: Row -> String
@@ -53,8 +55,9 @@
   nameAndTypeToPs name ty = name ++ " :: " ++ prettyPrintType ty
   tailToPs :: Row -> String
   tailToPs REmpty = ""
-  tailToPs (RUnknown u) = " | " ++ show u
+  tailToPs (RUnknown (Unknown u)) = " | u" ++ show u
   tailToPs (RowVar var) = " | " ++ var
+  tailToPs (RSkolem s) = " | s" ++ show s
   toList :: [(String, Type)] -> Row -> ([(String, Type)], Row)
   toList tys (RCons name ty row) = toList ((name, ty):tys) row
   toList tys r = (tys, r)
@@ -89,7 +92,3 @@
                     , Wrap function $ \args ret -> "(" ++ intercalate ", " (map prettyPrintType args) ++ ") -> " ++ ret
                     ]
                   ]
-
-prettyPrintPolyType :: PolyType -> String
-prettyPrintPolyType (PolyType [] ty) = prettyPrintType ty
-prettyPrintPolyType (PolyType idents ty) = "forall " ++ unwords idents ++ ". " ++ prettyPrintType ty
diff --git a/src/Language/PureScript/Pretty/Values.hs b/src/Language/PureScript/Pretty/Values.hs
--- a/src/Language/PureScript/Pretty/Values.hs
+++ b/src/Language/PureScript/Pretty/Values.hs
@@ -28,6 +28,7 @@
 import Language.PureScript.Values
 import Language.PureScript.Names
 import Language.PureScript.Pretty.Common
+import Language.PureScript.Pretty.Types
 
 literals :: Pattern () Value String
 literals = mkPattern match
@@ -83,6 +84,12 @@
   match (Abs args val) = Just (map show args, val)
   match _ = Nothing
 
+typed :: Pattern () Value (PolyType, Value)
+typed = mkPattern match
+  where
+  match (TypedValue val ty) = Just (ty, val)
+  match _ = Nothing
+
 unary :: UnaryOperator -> String -> Operator () Value String
 unary op str = Wrap pattern (++)
   where
@@ -113,6 +120,7 @@
                   , [ Wrap app $ \args val -> val ++ "(" ++ args ++ ")" ]
                   , [ Split lam $ \args val -> "\\" ++ intercalate ", " args ++ " -> " ++ prettyPrintValue val ]
                   , [ Wrap ifThenElse $ \(th, el) cond -> cond ++ " ? " ++ prettyPrintValue th ++ " : " ++ prettyPrintValue el ]
+                  , [ Wrap typed $ \ty val -> val ++ " :: " ++ prettyPrintType ty ]
                   , [ AssocR indexer (\index val -> val ++ " !! " ++ index) ]
                   , [ binary    LessThan             "<" ]
                   , [ binary    LessThanOrEqualTo    "<=" ]
@@ -147,7 +155,7 @@
 prettyPrintBinder (BooleanBinder False) = "false"
 prettyPrintBinder (VarBinder ident) = show ident
 prettyPrintBinder (NullaryBinder ctor) = show ctor
-prettyPrintBinder (UnaryBinder ctor b) = show ctor ++ prettyPrintBinder b
+prettyPrintBinder (UnaryBinder ctor b) = show ctor ++ " " ++ prettyPrintBinder b
 prettyPrintBinder (ObjectBinder bs) = "{ " ++ intercalate ", " (map (uncurry prettyPrintObjectPropertyBinder) bs) ++ " }"
 prettyPrintBinder (ArrayBinder bs rest) = "[ " ++ intercalate ", " (map prettyPrintBinder bs) ++ maybe "" (("; " ++) . prettyPrintBinder) rest ++ " ]"
 prettyPrintBinder (NamedBinder ident binder) = show ident ++ "@" ++ prettyPrintBinder binder
diff --git a/src/Language/PureScript/TypeChecker.hs b/src/Language/PureScript/TypeChecker.hs
--- a/src/Language/PureScript/TypeChecker.hs
+++ b/src/Language/PureScript/TypeChecker.hs
@@ -42,23 +42,23 @@
 typeCheckAll :: [Declaration] -> Check ()
 typeCheckAll [] = return ()
 typeCheckAll (DataDeclaration name args dctors : rest) = do
-  rethrow (("Error in type constructor " ++ show name ++ ": ") ++) $ do
+  rethrow (("Error in type constructor " ++ show name ++ ":\n") ++) $ do
     env <- getEnv
     modulePath <- checkModulePath `fmap` get
     guardWith (show name ++ " is already defined") $ not $ M.member (modulePath, name) (types env)
     ctorKind <- kindsOf (Just name) args (mapMaybe snd dctors)
     putEnv $ env { types = M.insert (modulePath, name) (ctorKind, Data) (types env) }
     forM_ dctors $ \(dctor, maybeTy) ->
-      rethrow (("Error in data constructor " ++ show name ++ ": ") ++) $ do
+      rethrow (("Error in data constructor " ++ show name ++ ":\n") ++) $ do
         env' <- getEnv
         guardWith (show dctor ++ " is already defined") $ not $ M.member (modulePath, dctor) (dataConstructors env')
         let retTy = foldl TypeApp (TypeConstructor (Qualified modulePath name)) (map TypeVar args)
         let dctorTy = maybe retTy (\ty -> Function [ty] retTy) maybeTy
-        let polyType = PolyType args dctorTy
+        let polyType = mkForAll args dctorTy
         putEnv $ env' { dataConstructors = M.insert (modulePath, dctor) polyType (dataConstructors env') }
   typeCheckAll rest
 typeCheckAll (TypeSynonymDeclaration name args ty : rest) = do
-  rethrow (("Error in type synonym " ++ show name ++ ": ") ++) $ do
+  rethrow (("Error in type synonym " ++ show name ++ ":\n") ++) $ do
     env <- getEnv
     modulePath <- checkModulePath `fmap` get
     guardWith (show name ++ " is already defined") $ not $ M.member (modulePath, name) (types env)
@@ -70,13 +70,13 @@
   typeCheckAll (ValueDeclaration name (TypedValue val ty) : rest)
 typeCheckAll (TypeDeclaration name _ : _) = throwError $ "Orphan type declaration for " ++ show name
 typeCheckAll (ValueDeclaration name val : rest) = do
-  rethrow (("Error in declaration " ++ show name ++ ": ") ++) $ do
+  rethrow (("Error in declaration " ++ show name ++ ":\n") ++) $ do
     env <- getEnv
     modulePath <- checkModulePath `fmap` get
     case M.lookup (modulePath, name) (names env) of
       Just ty -> throwError $ show name ++ " is already defined"
       Nothing -> do
-        ty <- typeOf name val
+        ty <- typeOf (Just name) val
         putEnv (env { names = M.insert (modulePath, name) (ty, Value) (names env) })
   typeCheckAll rest
 typeCheckAll (ExternDataDeclaration name kind : rest) = do
@@ -86,7 +86,7 @@
   putEnv $ env { types = M.insert (modulePath, name) (kind, TypeSynonym) (types env) }
   typeCheckAll rest
 typeCheckAll (ExternMemberDeclaration member name ty : rest) = do
-  rethrow (("Error in foreign import member declaration " ++ show name ++ ": ") ++) $ do
+  rethrow (("Error in foreign import member declaration " ++ show name ++ ":\n") ++) $ do
     env <- getEnv
     modulePath <- checkModulePath `fmap` get
     kind <- kindOf ty
@@ -94,13 +94,17 @@
     case M.lookup (modulePath, name) (names env) of
       Just _ -> throwError $ show name ++ " is already defined"
       Nothing -> case ty of
-        (PolyType _ (Function [_] _)) -> do
+        _ | isSingleArgumentFunction ty -> do
           putEnv (env { names = M.insert (modulePath, name) (ty, Extern) (names env)
                       , members = M.insert (modulePath, name) member (members env) })
-        _ -> throwError "Foreign member declarations must have function types, with an single argument."
+          | otherwise -> throwError "Foreign member declarations must have function types, with an single argument."
   typeCheckAll rest
+  where
+    isSingleArgumentFunction (Function [_] _) = True
+    isSingleArgumentFunction (ForAll _ ty) = isSingleArgumentFunction ty
+    isSingleArgumentFunction _ = False
 typeCheckAll (ExternDeclaration name ty : rest) = do
-  rethrow (("Error in foreign import declaration " ++ show name ++ ": ") ++) $ do
+  rethrow (("Error in foreign import declaration " ++ show name ++ ":\n") ++) $ do
     env <- getEnv
     modulePath <- checkModulePath `fmap` get
     kind <- kindOf ty
@@ -117,3 +121,21 @@
 typeCheckAll (ModuleDeclaration name decls : rest) = do
   withModule name $ typeCheckAll decls
   typeCheckAll rest
+typeCheckAll (ImportDeclaration modulePath idents : rest) = do
+  env <- getEnv
+  currentModule <- checkModulePath `fmap` get
+  rethrow errorMessage $ do
+    guardWith ("Module " ++ show modulePath ++ " does not exist") $ moduleExists env
+    case idents of
+      Nothing     -> bindIdents (map snd $ filterModule env) currentModule env
+      Just idents -> bindIdents idents currentModule env
+  typeCheckAll rest
+ where errorMessage = (("Error in import declaration " ++ show modulePath ++ ":\n") ++)
+       filterModule = filter ((== modulePath) . fst) . M.keys . names
+       moduleExists env = not $ null $ filterModule env
+       bindIdents idents currentModule env =
+         forM_ idents $ \ident -> do
+           guardWith (show currentModule ++ "." ++ show ident ++ " is already defined") $ (currentModule, ident) `M.notMember` names env
+           case (modulePath, ident) `M.lookup` names env of
+             Just (pt, _) -> modifyEnv (\e -> e { names = M.insert (currentModule, ident) (pt, Alias modulePath ident) (names e) })
+             Nothing -> throwError (show modulePath ++ "." ++ show ident ++ " is undefined")
diff --git a/src/Language/PureScript/TypeChecker/Kinds.hs b/src/Language/PureScript/TypeChecker/Kinds.hs
--- a/src/Language/PureScript/TypeChecker/Kinds.hs
+++ b/src/Language/PureScript/TypeChecker/Kinds.hs
@@ -15,8 +15,6 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 
 module Language.PureScript.TypeChecker.Kinds (
-    KindConstraint(..),
-    KindSolution(..),
     kindsOf,
     kindOf
 ) where
@@ -32,6 +30,7 @@
 import Language.PureScript.Declarations
 import Language.PureScript.TypeChecker.Monad
 import Language.PureScript.Pretty
+import Language.PureScript.Unknown
 
 import Control.Monad.State
 import Control.Monad.Error
@@ -42,146 +41,92 @@
 
 import qualified Data.Map as M
 
-data KindConstraintOrigin
-  = DataDeclOrigin
-  | TypeOrigin Type
-  | RowOrigin Row deriving (Show, Data, Typeable)
-
-prettyPrintKindConstraintOrigin :: KindConstraintOrigin -> String
-prettyPrintKindConstraintOrigin (DataDeclOrigin) = "data declaration"
-prettyPrintKindConstraintOrigin (TypeOrigin ty) = prettyPrintType ty
-prettyPrintKindConstraintOrigin (RowOrigin row) = prettyPrintRow row
-
-data KindConstraint = KindConstraint Int Kind KindConstraintOrigin deriving (Show, Data, Typeable)
-
-newtype KindSolution = KindSolution { runKindSolution :: Int -> Kind }
-
-emptyKindSolution :: KindSolution
-emptyKindSolution = KindSolution KUnknown
+instance Unifiable Kind where
+  unknown = KUnknown
+  isUnknown (KUnknown u) = Just u
+  isUnknown _ = Nothing
+  KUnknown u1 ~~ KUnknown u2 | u1 == u2 = return ()
+  KUnknown u ~~ k = replace u k
+  k ~~ KUnknown u = replace u k
+  Star ~~ Star = return ()
+  Row ~~ Row = return ()
+  FunKind k1 k2 ~~ FunKind k3 k4 = do
+    k1 ~~ k3
+    k2 ~~ k4
+  k1 ~~ k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
+  apply s (KUnknown u) = runSubstitution s u
+  apply s (FunKind k1 k2) = FunKind (apply s k1) (apply s k2)
+  apply _ k = k
+  unknowns (KUnknown (Unknown u)) = [u]
+  unknowns (FunKind k1 k2) = unknowns k1 ++ unknowns k2
+  unknowns _ = []
 
-kindOf :: PolyType -> Check Kind
-kindOf (PolyType idents ty) = do
-  ns <- replicateM (length idents) fresh
-  (cs, n, m) <- kindConstraints Nothing (M.fromList (zip idents ns)) ty
-  solution <- solveKindConstraints cs emptyKindSolution
-  return $ starIfUnknown $ runKindSolution solution n
+kindOf :: Type -> Check Kind
+kindOf ty = fmap (\(k, _, _) -> k) . runSubst $ starIfUnknown <$> infer Nothing M.empty ty
 
 kindsOf :: Maybe ProperName -> [String] -> [Type] -> Check Kind
-kindsOf name args ts = do
+kindsOf name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst $ do
   tyCon <- fresh
-  nargs <- replicateM (length args) fresh
-  (cs, ns, m) <- kindConstraintsAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args nargs)) ts
-  let extraConstraints =
-        KindConstraint tyCon (foldr (FunKind . KUnknown) Star nargs) DataDeclOrigin
-        : zipWith (\n arg -> KindConstraint n Star (TypeOrigin arg)) ns ts
-  solution <- solveKindConstraints (extraConstraints ++ cs) emptyKindSolution
-  return $ starIfUnknown $ runKindSolution solution tyCon
+  kargs <- replicateM (length args) fresh
+  ks <- inferAll (fmap (\pn -> (pn, tyCon)) name) (M.fromList (zip args kargs)) ts
+  tyCon ~~ foldr FunKind Star kargs
+  forM_ ks $ \k -> k ~~ Star
+  return tyCon
 
 starIfUnknown :: Kind -> Kind
 starIfUnknown (KUnknown _) = Star
 starIfUnknown (FunKind k1 k2) = FunKind (starIfUnknown k1) (starIfUnknown k2)
 starIfUnknown k = k
 
-kindConstraintsAll :: Maybe (ProperName, Int) -> M.Map String Int -> [Type] -> Check ([KindConstraint], [Int], M.Map String Int)
-kindConstraintsAll _ m [] = return ([], [], m)
-kindConstraintsAll name m (t:ts) = do
-  (cs, n1, m') <- kindConstraints name m t
-  (cs', ns, m'') <- kindConstraintsAll name m' ts
-  return (KindConstraint n1 Star (TypeOrigin t) : cs ++ cs', n1:ns, m'')
+inferAll :: Maybe (ProperName, Kind) -> M.Map String Kind -> [Type] -> Subst Check [Kind]
+inferAll name m = mapM (infer name m)
 
-kindConstraints :: Maybe (ProperName, Int) -> M.Map String Int -> Type -> Check ([KindConstraint], Int, M.Map String Int)
-kindConstraints name m a@(Array t) = do
-  me <- fresh
-  (cs, n1, m') <- kindConstraints name m t
-  return (KindConstraint n1 Star (TypeOrigin t) : KindConstraint me Star (TypeOrigin a) : cs, me, m')
-kindConstraints name m o@(Object row) = do
-  me <- fresh
-  (cs, r, m') <- kindConstraintsForRow name m row
-  return (KindConstraint me Star (TypeOrigin o) : KindConstraint r Row (RowOrigin row) : cs, me, m')
-kindConstraints name m f@(Function args ret) = do
-  me <- fresh
-  (cs, ns, m') <- kindConstraintsAll name m args
-  (cs', retN, m'') <- kindConstraints name m' ret
-  return (KindConstraint retN Star (TypeOrigin ret) : KindConstraint me Star (TypeOrigin f) : zipWith (\n arg -> KindConstraint n Star (TypeOrigin arg)) ns args ++ cs ++ cs', me, m'')
-kindConstraints _ m (TypeVar v) =
+infer :: Maybe (ProperName, Kind) -> M.Map String Kind -> Type -> Subst Check Kind
+infer name m (Array t) = do
+  k <- infer name m t
+  k ~~ Star
+  return Star
+infer name m (Object row) = do
+  k <- inferRow name m row
+  k ~~ Row
+  return Star
+infer name m (Function args ret) = do
+  ks <- inferAll name m args
+  k <- infer name m ret
+  k ~~ Star
+  forM ks $ \k -> k ~~ Star
+  return Star
+infer _ m (TypeVar v) =
   case M.lookup v m of
-    Just u -> return ([], u, m)
+    Just k -> return k
     Nothing -> throwError $ "Unbound type variable " ++ v
-kindConstraints (Just (name, u)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = do
-  env <- getEnv
-  me <- fresh
-  modulePath <- checkModulePath `fmap` get
-  return ([KindConstraint me (KUnknown u) (TypeOrigin c)], me, m)
-kindConstraints name m c@(TypeConstructor v) = do
-  env <- getEnv
-  me <- fresh
-  modulePath <- checkModulePath `fmap` get
+infer (Just (name, k)) m c@(TypeConstructor v@(Qualified (ModulePath []) pn)) | name == pn = return k
+infer name m (TypeConstructor v) = do
+  env <- lift getEnv
+  modulePath <- checkModulePath `fmap` lift get
   case M.lookup (qualify modulePath v) (types env) of
     Nothing -> throwError $ "Unknown type constructor '" ++ show v ++ "'"
-    Just (kind, _) -> return ([KindConstraint me kind (TypeOrigin c)], me, m)
-kindConstraints name m a@(TypeApp t1 t2) = do
-  me <- fresh
-  (cs1, n1, m1) <- kindConstraints name m t1
-  (cs2, n2, m2) <- kindConstraints name m1 t2
-  return (KindConstraint n1 (FunKind (KUnknown n2) (KUnknown me)) (TypeOrigin a) : cs1 ++ cs2, me, m2)
-kindConstraints _ m t = do
-  me <- fresh
-  return ([KindConstraint me Star (TypeOrigin t)], me, m)
-
-kindConstraintsForRow :: Maybe (ProperName, Int) -> M.Map String Int -> Row -> Check ([KindConstraint], Int, M.Map String Int)
-kindConstraintsForRow _ m r@(RowVar v) = do
-  me <- case M.lookup v m of
-    Just u -> return u
-    Nothing -> fresh
-  return ([KindConstraint me Row (RowOrigin r)], me, M.insert v me m)
-kindConstraintsForRow _ m r@REmpty = do
-  me <- fresh
-  return ([KindConstraint me Row (RowOrigin r)], me, m)
-kindConstraintsForRow name m r@(RCons _ ty row) = do
-  me <- fresh
-  (cs1, n1, m1) <- kindConstraints name m ty
-  (cs2, n2, m2) <- kindConstraintsForRow name m1 row
-  return (KindConstraint me Row (RowOrigin r) : KindConstraint n1 Star (TypeOrigin ty) : KindConstraint n2 Row (RowOrigin r) : cs1 ++ cs2, me, m2)
-
-solveKindConstraints :: [KindConstraint] -> KindSolution -> Check KindSolution
-solveKindConstraints [] s = return s
-solveKindConstraints all@(KindConstraint n k t : cs) s = do
-  (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintKindConstraintOrigin t ++ ": " ++ err) $ do
-    guardWith "Occurs check failed" $ not $ kindOccursCheck False n k
-    let s' = KindSolution $ replaceUnknownKind n k . runKindSolution s
-    cs' <- fmap concat $ mapM (substituteKindConstraint n k) cs
-    return (cs', s')
-  solveKindConstraints cs' s'
-
-substituteKindConstraint :: Int -> Kind -> KindConstraint -> Check [KindConstraint]
-substituteKindConstraint n k (KindConstraint m l t)
-  | n == m = unifyKinds t k l
-  | otherwise = return [KindConstraint m (replaceUnknownKind n k l) t]
-
-replaceUnknownKind :: Int -> Kind -> Kind -> Kind
-replaceUnknownKind n k = f
-  where
-  f (KUnknown m) | m == n = k
-  f (FunKind k1 k2) = FunKind (f k2) (f k2)
-  f other = other
-
-unifyKinds :: KindConstraintOrigin -> Kind -> Kind -> Check [KindConstraint]
-unifyKinds _ (KUnknown u1) (KUnknown u2) | u1 == u2 = return []
-unifyKinds t (KUnknown u) k = do
-  guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
-  return [KindConstraint u k t]
-unifyKinds t k (KUnknown u) = do
-  guardWith "Occurs check failed" $ not $ kindOccursCheck False u k
-  return [KindConstraint u k t]
-unifyKinds _ Star Star = return []
-unifyKinds _ Row Row = return []
-unifyKinds t (FunKind k1 k2) (FunKind k3 k4) = do
-  cs1 <- unifyKinds t k1 k3
-  cs2 <- unifyKinds t k2 k4
-  return $ cs1 ++ cs2
-unifyKinds _ k1 k2 = throwError $ "Cannot unify " ++ prettyPrintKind k1 ++ " with " ++ prettyPrintKind k2 ++ "."
+    Just (kind, _) -> return kind
+infer name m (TypeApp t1 t2) = do
+  k0 <- fresh
+  k1 <- infer name m t1
+  k2 <- infer name m t2
+  k1 ~~ FunKind k2 k0
+  return k0
+infer name m (ForAll ident ty) = do
+  k <- fresh
+  infer name (M.insert ident k m) ty
+infer _ m t = return Star
 
-kindOccursCheck :: Bool -> Int -> Kind -> Bool
-kindOccursCheck b u (KUnknown u') | u == u' = b
-kindOccursCheck _ u (FunKind k1 k2) = kindOccursCheck True u k1 || kindOccursCheck True u k2
-kindOccursCheck _ _ _ = False
+inferRow :: Maybe (ProperName, Kind) -> M.Map String Kind -> Row -> Subst Check Kind
+inferRow _ m (RowVar v) = do
+  case M.lookup v m of
+    Just k -> return k
+    Nothing -> throwError $ "Unbound row variable " ++ v
+inferRow _ m r@REmpty = return Row
+inferRow name m r@(RCons _ ty row) = do
+  k1 <- infer name m ty
+  k2 <- inferRow name m row
+  k1 ~~ Star
+  k2 ~~ Row
+  return Row
diff --git a/src/Language/PureScript/TypeChecker/Monad.hs b/src/Language/PureScript/TypeChecker/Monad.hs
--- a/src/Language/PureScript/TypeChecker/Monad.hs
+++ b/src/Language/PureScript/TypeChecker/Monad.hs
@@ -12,14 +12,20 @@
 --
 -----------------------------------------------------------------------------
 
-{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving, FlexibleInstances, RankNTypes, DeriveDataTypeable,
+    GADTs, StandaloneDeriving, MultiParamTypeClasses, FlexibleContexts #-}
 
 module Language.PureScript.TypeChecker.Monad where
 
 import Language.PureScript.Types
 import Language.PureScript.Kinds
 import Language.PureScript.Names
+import Language.PureScript.Unknown
 
+import Data.Data
+import Data.Maybe
+import Data.Monoid
+import Data.Typeable
 import Control.Applicative
 import Control.Monad.State
 import Control.Monad.Error
@@ -28,14 +34,14 @@
 
 import qualified Data.Map as M
 
-data NameKind = Value | Extern deriving Show
+data NameKind = Value | Extern | Alias ModulePath Ident deriving Show
 
 data TypeDeclarationKind = Data | ExternData | TypeSynonym deriving Show
 
 data Environment = Environment
-  { names :: M.Map (ModulePath, Ident) (PolyType, NameKind)
+  { names :: M.Map (ModulePath, Ident) (Type, NameKind)
   , types :: M.Map (ModulePath, ProperName) (Kind, TypeDeclarationKind)
-  , dataConstructors :: M.Map (ModulePath, ProperName) PolyType
+  , dataConstructors :: M.Map (ModulePath, ProperName) Type
   , typeSynonyms :: M.Map (ModulePath, ProperName) ([String], Type)
   , members :: M.Map (ModulePath, Ident) String
   } deriving (Show)
@@ -43,10 +49,13 @@
 emptyEnvironment :: Environment
 emptyEnvironment = Environment M.empty M.empty M.empty M.empty M.empty
 
+data AnyUnifiable where
+  AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable
+
 data CheckState = CheckState { checkEnv :: Environment
                              , checkNextVar :: Int
                              , checkModulePath :: ModulePath
-                             } deriving (Show)
+                             }
 
 newtype Check a = Check { unCheck :: StateT CheckState (Either String) a }
   deriving (Functor, Monad, Applicative, MonadPlus, MonadState CheckState, MonadError String)
@@ -57,14 +66,13 @@
 putEnv :: Environment -> Check ()
 putEnv env = modify (\s -> s { checkEnv = env })
 
-fresh :: Check Int
-fresh = do
-  st <- get
-  put $ st { checkNextVar = checkNextVar st + 1 }
-  return $ checkNextVar st
+modifyEnv :: (Environment -> Environment) -> Check ()
+modifyEnv f = modify (\s -> s { checkEnv = f (checkEnv s) })
 
-check :: Check a -> Either String (a, Environment)
-check = fmap (second checkEnv) . flip runStateT (CheckState emptyEnvironment 0 global) . unCheck
+runCheck :: Check a -> Either String (a, Environment)
+runCheck c = do
+  (a, s) <- flip runStateT (CheckState emptyEnvironment 0 global) $ unCheck c
+  return (a, checkEnv s)
 
 guardWith :: (MonadError e m) => e -> Bool -> m ()
 guardWith _ True = return ()
@@ -80,3 +88,69 @@
   a <- act
   modify $ \s -> s { checkModulePath = original }
   return a
+
+newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }
+
+instance Monoid Substitution where
+  mempty = Substitution unknown
+  s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))
+
+data SubstState = SubstState { substSubst :: Substitution
+                             , substFutureEscapeChecks :: [AnyUnifiable] }
+
+newtype Subst m a = Subst { unSubst :: StateT SubstState m a }
+  deriving (Functor, Monad, Applicative, MonadPlus, MonadTrans)
+
+deriving instance (MonadError String m) => MonadError String (Subst m)
+
+runSubst :: (Unifiable a, Monad m) => Subst m a -> m (a, Substitution, [AnyUnifiable])
+runSubst subst = do
+  (a, s) <- flip runStateT (SubstState mempty []) . unSubst $ subst
+  return (apply (substSubst s) a, substSubst s, substFutureEscapeChecks s)
+
+substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution
+substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do
+  u1 <- cast u
+  cast (f u1)
+
+substituteOne :: (Unifiable t) => Unknown t -> t -> Substitution
+substituteOne u t = substituteWith $ \u1 ->
+  case u1 of
+    u2 | u2 == u -> t
+       | otherwise -> unknown u2
+
+replace :: (Unifiable t) => Unknown t -> t -> Subst Check ()
+replace u t' = do
+  sub <- substSubst <$> Subst get
+  let t = apply sub t'
+  occursCheck u t
+  let current = apply sub $ unknown u
+  case isUnknown current of
+    Just u1 | u1 == u -> return ()
+    _ -> current ~~ t
+  Subst . modify $ \s -> s { substSubst = substituteOne u t <> substSubst s }
+
+class (Typeable t, Data t, Show t) => Unifiable t where
+  unknown :: Unknown t -> t
+  (~~) :: t -> t -> Subst Check ()
+  isUnknown :: t -> Maybe (Unknown t)
+  apply :: Substitution -> t -> t
+  unknowns :: t -> [Int]
+
+occursCheck :: (Unifiable t) => Unknown s -> t -> Subst Check ()
+occursCheck (Unknown u) t =
+  case isUnknown t of
+    Nothing -> guardWith "Occurs check fails" (u `notElem` unknowns t)
+    _ -> return ()
+
+fresh' :: Subst Check Int
+fresh' = do
+  n <- lift $ checkNextVar <$> get
+  lift . modify $ \s -> s { checkNextVar = succ (checkNextVar s) }
+  return n
+
+fresh :: (Unifiable t) => Subst Check t
+fresh = unknown . Unknown <$> fresh'
+
+escapeCheckLater :: (Unifiable t) => t -> Subst Check ()
+escapeCheckLater t = Subst . modify $ \s -> s { substFutureEscapeChecks = AnyUnifiable t : substFutureEscapeChecks s  }
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
@@ -15,626 +15,749 @@
 {-# LANGUAGE DeriveDataTypeable #-}
 
 module Language.PureScript.TypeChecker.Types (
-    TypeConstraint(..),
-    TypeSolution(..),
-    typeOf
-) where
-
-import Debug.Trace
-
-import Data.List
-import Data.Function
-import qualified Data.Data as D
-import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
-
-import Language.PureScript.Values
-import Language.PureScript.Types
-import Language.PureScript.Kinds
-import Language.PureScript.Names
-import Language.PureScript.TypeChecker.Monad
-import Language.PureScript.TypeChecker.Kinds
-import Language.PureScript.TypeChecker.Synonyms
-import Language.PureScript.Pretty
-
-import Control.Monad.State
-import Control.Monad.Error
-
-import Control.Applicative
-import Control.Arrow (Kleisli(..), (***), (&&&), first)
-import qualified Control.Category as C
-
-import qualified Data.Map as M
-
-data TypeConstraintOrigin
-  = ValueOrigin Value
-  | BinderOrigin Binder
-  | AssignmentTargetOrigin Ident deriving (Show, D.Data, D.Typeable)
-
-prettyPrintOrigin :: TypeConstraintOrigin -> String
-prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
-prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
-prettyPrintOrigin (AssignmentTargetOrigin ident) = show ident
-
-data TypeConstraint
-  = TypeConstraint Int Type TypeConstraintOrigin
-  | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
-
-newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
-
-emptyTypeSolution :: TypeSolution
-emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
-
-isFunction :: Value -> Bool
-isFunction (Abs _ _) = True
-isFunction (TypedValue untyped _) = isFunction untyped
-isFunction _ = False
-
-allConstraints :: Ident -> Value -> Check ([TypeConstraint], Int)
-allConstraints name val | isFunction val = do
-  me <- fresh
-  (cs, n) <- typeConstraints (M.singleton name me) val
-  return (TypeConstraint me (TUnknown n) (ValueOrigin val): cs, n)
-allConstraints _ val = typeConstraints M.empty val
-
-typeOf :: Ident -> Value -> Check PolyType
-typeOf name val = do
-  (cs, n) <- allConstraints name val
-  desugared <- replaceAllTypeSynonyms cs
-  solution <- solveTypeConstraints desugared emptyTypeSolution
-  let ty = fst (runTypeSolution solution) n
-  allUnknownsBecameQuantified desugared solution ty
-  return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
-
-allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
-allUnknownsBecameQuantified cs solution ty = do
-  let
-    typesMentioned = findUnknownTypes ty
-    unknownTypes = nub $ flip concatMap cs $ \c -> case c of
-      TypeConstraint u t _ -> u : findUnknownTypes t
-      RowConstraint _ r _ -> findUnknownTypes r
-    unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes
-  guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned
-  let
-    rowsMentioned = findUnknownRows ty
-    unknownRows = nub $ flip concatMap cs $ \c -> case c of
-      TypeConstraint _ t _ -> findUnknownRows t
-      RowConstraint u r _ -> u : findUnknownRows r
-    unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
-  guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
-
-setify :: Row -> Row
-setify = rowFromList . first (M.toList . M.fromList) . rowToList
-
-setifyAll :: (D.Data d) => d -> d
-setifyAll = everywhere (mkT setify)
-
-findUnknownTypes :: (D.Data d) => d -> [Int]
-findUnknownTypes = everything (++) (mkQ [] f)
-  where
-  f :: Type -> [Int]
-  f (TUnknown n) = [n]
-  f _ = []
-
-findTypeVars :: (D.Data d) => d -> [String]
-findTypeVars = everything (++) (mkQ [] f)
-  where
-  f :: Type -> [String]
-  f (TypeVar v) = [v]
-  f _ = []
-
-findUnknownRows :: (D.Data d) => d -> [Int]
-findUnknownRows = everything (++) (mkQ [] f)
-  where
-  f :: Row -> [Int]
-  f (RUnknown n) = [n]
-  f _ = []
-
-varIfUnknown :: Type -> PolyType
-varIfUnknown ty =
-  let
-    (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
-  in
-    PolyType (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
-  where
-  f :: Type -> State (M.Map Int String) Type
-  f (TUnknown n) = do
-    m <- get
-    case M.lookup n m of
-      Nothing -> do
-        let name = 't' : show (M.size m)
-        put $ M.insert n name m
-        return $ TypeVar name
-      Just name -> return $ TypeVar name
-  f t = return t
-  g :: Row -> State (M.Map Int String) Row
-  g (RUnknown n) = do
-    m <- get
-    case M.lookup n m of
-      Nothing -> do
-        let name = 'r' : show (M.size m)
-        put $ M.insert n name m
-        return $ RowVar name
-      Just name -> return $ RowVar name
-  g r = return r
-
-replaceTypeVars :: M.Map String Type -> Type -> Type
-replaceTypeVars m = everywhere (mkT replace)
-  where
-  replace (TypeVar v) = case M.lookup v m of
-    Just ty -> ty
-    _ -> TypeVar v
-  replace t = t
-
-replaceVarsWithUnknowns :: [String] -> Type -> Check Type
-replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
-  where
-  f :: Type -> StateT (M.Map String Int) 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 n
-      Just u -> return $ TUnknown u
-  f t = return t
-  g :: Row -> StateT (M.Map String Int) 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 n
-      Just u -> return $ RUnknown u
-  g r = return r
-
-replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
-replaceAllTypeSynonyms d = do
-  env <- getEnv
-  let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env
-  either throwError return $ saturateAllTypeSynonyms syns d
-
-desaturateAllTypeSynonyms :: (D.Data d) => d -> d
-desaturateAllTypeSynonyms = everywhere (mkT replace)
-  where
-  replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
-  replace t = t
-
-replaceType :: (D.Data d) => Int -> Type -> d -> d
-replaceType n t = everywhere (mkT go)
-  where
-  go (TUnknown m) | m == n = t
-  go t = t
-
-replaceRow :: (D.Data d) => Int -> Row -> d -> d
-replaceRow n r = everywhere (mkT go)
-  where
-  go (RUnknown m) | m == n = r
-  go r = r
-
-typeOccursCheck :: Int -> Type -> Check ()
-typeOccursCheck u (TUnknown _) = return ()
-typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
-
-rowOccursCheck :: Int -> Row -> Check ()
-rowOccursCheck u (RUnknown _) = return ()
-rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
-
-occursCheck :: (D.Data d) => Int -> d -> Bool
-occursCheck u = everything (||) $ flip extQ g $ mkQ False f
-  where
-  f (TUnknown u') | u' == u = True
-  f _ = False
-  g (RUnknown u') | u' == u = True
-  g _ = False
-
-typesToRow :: [(String, Type)] -> Row
-typesToRow [] = REmpty
-typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
-
-rowToList :: Row -> ([(String, Type)], Row)
-rowToList (RCons name ty row) = let (tys, rest) = rowToList row
-                               in ((name, ty):tys, rest)
-rowToList r = ([], r)
-
-rowFromList :: ([(String, Type)], Row) -> Row
-rowFromList ([], r) = r
-rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
-
-ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
-ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
-
-typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
-typeConstraints _ v@(NumericLiteral _) = do
-  me <- fresh
-  return ([TypeConstraint me Number (ValueOrigin v)], me)
-typeConstraints _ v@(StringLiteral _) = do
-  me <- fresh
-  return ([TypeConstraint me String (ValueOrigin v)], me)
-typeConstraints _ v@(BooleanLiteral _) = do
-  me <- fresh
-  return ([TypeConstraint me Boolean (ValueOrigin v)], me)
-typeConstraints m v@(ArrayLiteral vals) = do
-  all <- mapM (typeConstraints m) vals
-  let (cs, ns) = (concatMap fst &&& map snd) all
-  me <- fresh
-  return (cs ++ zipWith (\n el -> TypeConstraint me (Array $ TUnknown n) (ValueOrigin el)) ns vals, me)
-typeConstraints m u@(Unary op val) = do
-  (cs, n1) <- typeConstraints m val
-  me <- fresh
-  return (cs ++ unaryOperatorConstraints u op n1 me, me)
-typeConstraints m b@(Binary op left right) = do
-  (cs1, n1) <- typeConstraints m left
-  (cs2, n2) <- typeConstraints m right
-  me <- fresh
-  return (cs1 ++ cs2 ++ binaryOperatorConstraints b op n1 n2 me, me)
-typeConstraints m v@(ObjectLiteral ps) = do
-  ensureNoDuplicateProperties ps
-  all <- mapM (typeConstraints m . snd) ps
-  let (cs, ns) = (concatMap fst &&& map snd) all
-  me <- fresh
-  let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
-  return (TypeConstraint me (Object (typesToRow tys)) (ValueOrigin v) : cs, me)
-typeConstraints m v@(ObjectUpdate o ps) = do
-  ensureNoDuplicateProperties ps
-  (cs1, n1) <- typeConstraints m o
-  all <- mapM (typeConstraints m . snd) ps
-  let (cs2, ns) = (concatMap fst &&& map snd) all
-  row <- fresh
-  let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
-  return (TypeConstraint n1 (Object (rowFromList (tys, RUnknown row))) (ValueOrigin v) : cs1 ++ cs2, n1)
-typeConstraints m v@(Indexer index val) = do
-  (cs1, n1) <- typeConstraints m index
-  (cs2, n2) <- typeConstraints m val
-  me <- fresh
-  return (TypeConstraint n1 Number (ValueOrigin index) : TypeConstraint n2 (Array (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
-typeConstraints m v@(Accessor prop val) = do
-  (cs, n1) <- typeConstraints m val
-  me <- fresh
-  rest <- fresh
-  return (TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest))) (ValueOrigin v) : cs, me)
-typeConstraints m v@(Abs args ret) = do
-  ns <- replicateM (length args) fresh
-  let m' = m `M.union` M.fromList (zip args ns)
-  (cs, n') <- typeConstraints m' ret
-  me <- fresh
-  return (TypeConstraint me (Function (map TUnknown ns) (TUnknown n')) (ValueOrigin v) : cs, me)
-typeConstraints m v@(App f xs) = do
-  (cs1, n1) <- typeConstraints m f
-  all <- mapM (typeConstraints m) xs
-  let (cs2, ns) = (concatMap fst &&& map snd) all
-  me <- fresh
-  return (TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me)) (ValueOrigin v) : cs1 ++ cs2, me)
-typeConstraints m v@(Var var@(Qualified mp name)) = do
-  case mp of
-    ModulePath [] ->
-      case M.lookup name m of
-        Just u -> do
-          me <- fresh
-          return ([TypeConstraint u (TUnknown me) (ValueOrigin v)], me)
-        Nothing -> lookupGlobal
-    _ -> lookupGlobal
-  where
-  lookupGlobal = do
-    env <- getEnv
-    modulePath <- checkModulePath `fmap` get
-    case M.lookup (qualify modulePath var) (names env) of
-      Nothing -> throwError $ show var ++ " is undefined"
-      Just (PolyType idents ty, _) -> do
-        me <- fresh
-        replaced <- replaceVarsWithUnknowns idents ty
-        return ([TypeConstraint me replaced (ValueOrigin v)], me)
-typeConstraints m (Block ss) = do
-  ret <- fresh
-  (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
-  guardWith "Block is missing a return statement" allCodePathsReturn
-  return (cs, ret)
-typeConstraints m v@(Constructor c) = do
-  env <- getEnv
-  modulePath <- checkModulePath `fmap` get
-  case M.lookup (qualify modulePath c) (dataConstructors env) of
-    Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
-    Just (PolyType idents ty) -> do
-      me <- fresh
-      replaced <- replaceVarsWithUnknowns idents ty
-      return ([TypeConstraint me replaced (ValueOrigin v)], me)
-typeConstraints m (Case val binders) = do
-  (cs1, n1) <- typeConstraints m val
-  ret <- fresh
-  cs2 <- typeConstraintsForBinders m n1 ret binders
-  return (cs1 ++ cs2, ret)
-typeConstraints m v@(IfThenElse cond th el) = do
-  (cs1, n1) <- typeConstraints m cond
-  (cs2, n2) <- typeConstraints m th
-  (cs3, n3) <- typeConstraints m el
-  return (TypeConstraint n1 Boolean (ValueOrigin cond) : TypeConstraint n2 (TUnknown n3) (ValueOrigin v) : cs1 ++ cs2 ++ cs3, n2)
-typeConstraints m v@(TypedValue val poly@(PolyType idents ty)) = do
-  kind <- kindOf poly
-  guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
-  (cs, n1) <- typeConstraints m val
-  return (TypeConstraint n1 ty (ValueOrigin v) : cs, n1)
-
-unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
-unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
-unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
-unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
-
-binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
-binaryOperatorConstraints v Add = symBinOpConstraints v Number
-binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
-binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
-binaryOperatorConstraints v Divide = symBinOpConstraints v Number
-binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
-binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
-binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
-binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
-binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
-binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
-binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
-binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
-binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
-binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
-binaryOperatorConstraints v And = symBinOpConstraints v Boolean
-binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
-binaryOperatorConstraints v Concat = symBinOpConstraints v String
-
-equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
-equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
-
-symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
-symBinOpConstraints v ty = asymBinOpConstraints v ty ty
-
-asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
-asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
-
-typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
-typeConstraintsForBinder _ NullBinder = return ([], M.empty)
-typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
-typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
-typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
-typeConstraintsForBinder val b@(VarBinder name) = do
-  me <- fresh
-  return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
-typeConstraintsForBinder val b@(NullaryBinder ctor) = do
-  env <- getEnv
-  modulePath <- checkModulePath `fmap` get
-  case M.lookup (qualify modulePath ctor) (dataConstructors env) of
-    Just (PolyType args ret) -> do
-      ret' <- replaceVarsWithUnknowns args ret
-      return ([TypeConstraint val ret' (BinderOrigin b)], M.empty)
-    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
-typeConstraintsForBinder val b@(UnaryBinder ctor binder) = do
-  env <- getEnv
-  modulePath <- checkModulePath `fmap` get
-  case M.lookup (qualify modulePath ctor) (dataConstructors env) of
-    Just (PolyType idents f@(Function [_] _)) -> do
-      obj <- fresh
-      (Function [ty] ret) <- replaceVarsWithUnknowns idents f
-      (cs, m1) <- typeConstraintsForBinder obj binder
-      return (TypeConstraint val ret (BinderOrigin b) : TypeConstraint obj ty (BinderOrigin b) : cs, m1)
-    Just _ -> throwError $ show ctor ++ " is not a unary constructor"
-    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
-typeConstraintsForBinder val b@(ObjectBinder props) = do
-  row <- fresh
-  rest <- fresh
-  (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
-  return (TypeConstraint val (Object (RUnknown row)) (BinderOrigin b) : cs, m1)
-  where
-  typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
-  typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row (BinderOrigin b)], M.empty)
-  typeConstraintsForProperties nrow row ((name, binder):binders) = do
-    propTy <- fresh
-    (cs1, m1) <- typeConstraintsForBinder propTy binder
-    (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
-    return (cs1 ++ cs2, m1 `M.union` m2)
-typeConstraintsForBinder val b@(ArrayBinder binders rest) = do
-  el <- fresh
-  all <- mapM (typeConstraintsForBinder el) binders
-  let (cs1, m1) = (concatMap fst &&& M.unions . map snd) all
-  let arrayConstraint = TypeConstraint val (Array (TUnknown el)) (BinderOrigin b)
-  case rest of
-    Nothing -> return (arrayConstraint : cs1, m1)
-    Just binder -> do
-      (cs2, m2) <- typeConstraintsForBinder val binder
-      return (arrayConstraint : cs1 ++ cs2, m1 `M.union` m2)
-typeConstraintsForBinder val b@(NamedBinder name binder) = do
-  me <- fresh
-  (cs, m) <- typeConstraintsForBinder val binder
-  return (TypeConstraint me (TUnknown val) (BinderOrigin b) : cs, M.insert name me m)
-
-typeConstraintsForGuardedBinder :: M.Map Ident Int -> Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
-typeConstraintsForGuardedBinder m val b@(GuardedBinder cond binder) = do
-  (cs1, m1) <- typeConstraintsForBinder val binder
-  (cs2, n) <- typeConstraints (m `M.union` m1) cond
-  return (TypeConstraint n Boolean (ValueOrigin cond) : cs1 ++ cs2, m1)
-typeConstraintsForGuardedBinder m val b = typeConstraintsForBinder val b >>= return
-
-constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
-constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
-
-typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
-typeConstraintsForBinders _ _ _ [] = return []
-typeConstraintsForBinders m nval ret ((binder, val):bs) = do
-  (cs1, m1) <- typeConstraintsForGuardedBinder m nval binder
-  (cs2, n2) <- typeConstraints (m `M.union` m1) val
-  cs3 <- typeConstraintsForBinders m nval ret bs
-  return (TypeConstraint n2 (TUnknown ret) (BinderOrigin binder) : cs1 ++ cs2 ++ cs3)
-
-assignVariable :: Ident -> M.Map Ident Int -> Check ()
-assignVariable name m =
-  case M.lookup name m of
-    Nothing -> return ()
-    Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
-
-typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
-typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
-  assignVariable name (m `M.union` mass)
-  (cs1, n1) <- typeConstraints m val
-  return (cs1, False, M.insert name n1 mass)
-typeConstraintsForStatement m mass ret (Assignment ident val) = do
-  (cs1, n1) <- typeConstraints m val
-  case M.lookup ident mass of
-    Nothing -> throwError $ "No local variable with name " ++ show ident
-    Just ty ->
-     return (TypeConstraint n1 (TUnknown ty) (AssignmentTargetOrigin ident) : cs1, False, mass)
-typeConstraintsForStatement m mass ret (While val inner) = do
-  (cs1, n1) <- typeConstraints m val
-  (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
-  return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, allCodePathsReturn, mass)
-typeConstraintsForStatement m mass ret (If ifst) = do
-  (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
-  return (cs, allCodePathsReturn, mass)
-typeConstraintsForStatement m mass ret (For ident start end inner) = do
-  assignVariable ident (m `M.union` mass)
-  (cs1, n1) <- typeConstraints (m `M.union` mass) start
-  (cs2, n2) <- typeConstraints (m `M.union` mass) end
-  let mass1 = M.insert ident n1 mass
-  (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
-  return (TypeConstraint n1 Number (ValueOrigin start) : TypeConstraint n2 Number (ValueOrigin end) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
-typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
-  assignVariable ident (m `M.union` mass)
-  val <- fresh
-  (cs1, n1) <- typeConstraints (m `M.union` mass) vals
-  let mass1 = M.insert ident val mass
-  (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
-  guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
-  return (TypeConstraint n1 (Array (TUnknown val)) (ValueOrigin vals) : cs1 ++ cs2, False, mass)
-typeConstraintsForStatement m mass ret (Return val) = do
-  (cs1, n1) <- typeConstraints (m `M.union` mass) val
-  return (TypeConstraint n1 (TUnknown ret) (ValueOrigin val) : cs1, True, mass)
-
-typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
-typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
-  (cs1, n1) <- typeConstraints m val
-  (cs2, _, _) <- typeConstraintsForBlock m mass ret thens
-  return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2, False)
-typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
-  (cs1, n1) <- typeConstraints m val
-  (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
-  (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
-  return (TypeConstraint n1 Boolean (ValueOrigin val) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
-
-typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
-typeConstraintsForElseStatement m mass ret (Else elses) = do
-  (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
-  return (cs, allCodePathsReturn)
-typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
-  (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
-  return (cs, allCodePathsReturn)
-
-typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
-typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
-typeConstraintsForBlock m mass ret (s:ss) = do
-  (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
-  case (b1, ss) of
-    (True, []) -> return (cs1, True, mass1)
-    (True, _) -> throwError "Unreachable code"
-    (False, ss) -> do
-      (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
-      return (cs1 ++ cs2, b2, mass2)
-
-solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
-solveTypeConstraints [] s = return s
-solveTypeConstraints all@(TypeConstraint n t o:cs) s = do
-  (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
-    typeOccursCheck n t
-    let s' = let (f, g) = runTypeSolution s
-             in TypeSolution (replaceType n t . f, replaceType n t . g)
-    cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
-    return (cs', s')
-  solveTypeConstraints cs' s'
-solveTypeConstraints (RowConstraint n r o:cs) s = do
-  (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
-    rowOccursCheck n r
-    let s' = let (f, g) = runTypeSolution s
-             in TypeSolution (replaceRow n r . f, replaceRow n r . g)
-    cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
-    return (cs', s')
-  solveTypeConstraints cs' s'
-
-substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
-substituteTypeInConstraint n s (TypeConstraint m t v)
-  | n == m = unifyTypes v s t
-  | otherwise = return [TypeConstraint m (replaceType n s t) v]
-substituteTypeInConstraint n s (RowConstraint m r v)
-  = return [RowConstraint m (replaceType n s r) v]
-
-substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
-substituteRowInConstraint n r (TypeConstraint m t v)
-  = return [TypeConstraint m (replaceRow n r t) v]
-substituteRowInConstraint n r (RowConstraint m r1 v)
-  | m == n = unifyRows v r r1
-  | otherwise = return [RowConstraint m (replaceRow n r r1) v]
-
-unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
-unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
-unifyTypes o (TUnknown u) t = do
-  typeOccursCheck u t
-  return [TypeConstraint u t o]
-unifyTypes o t (TUnknown u) = do
-  typeOccursCheck u t
-  return [TypeConstraint u t o]
-unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
-  fmap concat $ zipWithM (unifyTypes o) args1 args2
-unifyTypes o (SaturatedTypeSynonym name args) ty = do
-  env <- getEnv
-  modulePath <- checkModulePath `fmap` get
-  case M.lookup (qualify modulePath name) (typeSynonyms env) of
-    Just (synArgs, body) -> do
-      let m = M.fromList $ zip synArgs args
-      let replaced = replaceTypeVars m body
-      unifyTypes o replaced ty
-    Nothing -> error "Type synonym was not defined"
-unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
-unifyTypes _ Number Number = return []
-unifyTypes _ String String = return []
-unifyTypes _ Boolean Boolean = return []
-unifyTypes o (Array s) (Array t) = unifyTypes o s t
-unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
-unifyTypes o (Function args1 ret1) (Function args2 ret2) = do
-  guardWith "Function applied to incorrect number of args" $ length args1 == length args2
-  cs1 <- fmap concat $ zipWithM (unifyTypes o) args1 args2
-  cs2 <- unifyTypes o ret1 ret2
-  return $ cs1 ++ cs2
-unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
-unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) = do
-  modulePath <- checkModulePath `fmap` get
-  guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
-  return []
-unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
-  cs1 <- unifyTypes o t1 t3
-  cs2 <- unifyTypes o t2 t4
-  return $ cs1 ++ cs2
-unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
-
-unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
-unifyRows o r1 r2 =
-  let
-    (s1, r1') = rowToList r1
-    (s2, r2') = rowToList r2
-    int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
-    sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
-    sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
-  in do
-    cs1 <- fmap concat $ mapM (uncurry $ unifyTypes o) int
-    cs2 <- unifyRows' o sd1 r1' sd2 r2'
-    return $ cs1 ++ cs2
-  where
-  unifyRows' :: TypeConstraintOrigin -> [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
-  unifyRows' o [] (RUnknown u) sd r = do
-    rowOccursCheck u r
-    return [RowConstraint u (rowFromList (sd, r)) o]
-  unifyRows' o sd r [] (RUnknown u) = do
-    rowOccursCheck u r
-    return [RowConstraint u (rowFromList (sd, r)) o]
-  unifyRows' o ns@((name, ty):row) r others (RUnknown u) | not (occursCheck u (ty, row)) = do
-    u' <- fresh
-    cs <- unifyRows' o row r others (RUnknown u')
-    return (RowConstraint u (RCons name ty (RUnknown u')) o : cs)
-  unifyRows' _ [] REmpty [] REmpty = return []
-  unifyRows' _ [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return []
-  unifyRows' _ sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
+    typeOf
+) where
+
+import Data.List
+import Data.Maybe (isJust, fromMaybe)
+import Data.Function
+import qualified Data.Data as D
+import Data.Generics
+       (something, everywhere, everywhereM, everything, everywhereBut,
+        mkT, mkM, mkQ, extM, extQ)
+
+import Language.PureScript.Values
+import Language.PureScript.Types
+import Language.PureScript.Kinds
+import Language.PureScript.Names
+import Language.PureScript.TypeChecker.Monad
+import Language.PureScript.TypeChecker.Kinds
+import Language.PureScript.TypeChecker.Synonyms
+import Language.PureScript.Pretty
+import Language.PureScript.Unknown
+
+import Control.Monad.State
+import Control.Monad.Error
+
+import Control.Applicative
+import Control.Arrow (Arrow(..), Kleisli(..), (***), (&&&), second)
+import qualified Control.Category as C
+
+import qualified Data.Map as M
+
+instance Unifiable Type where
+  unknown = TUnknown
+  isUnknown (TUnknown u) = Just u
+  isUnknown _ = Nothing
+  (~~) = unifyTypes
+  apply s (TUnknown u) = runSubstitution s u
+  apply s (SaturatedTypeSynonym name tys) = SaturatedTypeSynonym name $ map (apply s) tys
+  apply s (ForAll idents ty) = ForAll idents $ apply s ty
+  apply s (Array t) = Array (apply s t)
+  apply s (Object r) = Object (apply s r)
+  apply s (Function args ret) = Function (map (apply s) args) (apply s ret)
+  apply s (TypeApp t1 t2) = TypeApp (apply s t1) (apply s t2)
+  apply _ t = t
+  unknowns (TUnknown (Unknown u)) = [u]
+  unknowns (SaturatedTypeSynonym _ tys) = concatMap unknowns tys
+  unknowns (ForAll idents ty) = unknowns ty
+  unknowns (Array t) = unknowns t
+  unknowns (Object r) = unknowns r
+  unknowns (Function args ret) = concatMap unknowns args ++ unknowns ret
+  unknowns (TypeApp t1 t2) = unknowns t1 ++ unknowns t2
+  unknowns _ = []
+
+instance Unifiable Row where
+  unknown = RUnknown
+  isUnknown (RUnknown u) = Just u
+  isUnknown _ = Nothing
+  r1 ~~ r2 =
+      let
+        (s1, r1') = rowToList r1
+        (s2, r2') = rowToList r2
+        int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
+        sd1 = [ (name, t1) | (name, t1) <- s1, name `notElem` map fst s2 ]
+        sd2 = [ (name, t2) | (name, t2) <- s2, name `notElem` map fst s1 ]
+      in do
+        forM_ int (uncurry (~~))
+        unifyRows sd1 r1' sd2 r2'
+      where
+      unifyRows :: [(String, Type)] -> Row -> [(String, Type)] -> Row -> Subst Check ()
+      unifyRows [] (RUnknown u) sd r = replace u (rowFromList (sd, r))
+      unifyRows sd r [] (RUnknown u) = replace u (rowFromList (sd, r))
+      unifyRows ns@((name, ty):row) r others u@(RUnknown un) = do
+        occursCheck un ty
+        forM row $ \(_, ty) -> occursCheck un ty
+        u' <- fresh
+        u ~~ RCons name ty u'
+        unifyRows row r others u'
+      unifyRows [] REmpty [] REmpty = return ()
+      unifyRows [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return ()
+      unifyRows [] (RSkolem s1) [] (RSkolem s2) | s1 == s2 = return ()
+      unifyRows sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."
+  apply s (RUnknown u) = runSubstitution s u
+  apply s (RCons name ty r) = RCons name (apply s ty) (apply s r)
+  apply _ r = r
+  unknowns (RUnknown (Unknown u)) = [u]
+  unknowns (RCons _ ty r) = unknowns ty ++ unknowns r
+  unknowns _ = []
+
+unifyTypes :: Type -> Type -> Subst Check ()
+unifyTypes t1 t2 = rethrow (\e -> "Error unifying type " ++ prettyPrintType t1 ++ " with type " ++ prettyPrintType t2 ++ ":\n" ++ e) $ do
+  unifyTypes' t1 t2
+  where
+  unifyTypes' (TUnknown u1) (TUnknown u2) | u1 == u2 = return ()
+  unifyTypes' (TUnknown u) t = replace u t
+  unifyTypes' t (TUnknown u) = replace u t
+  unifyTypes' (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2)
+    | name1 == name2 = zipWithM_ unifyTypes args1 args2
+  unifyTypes' (SaturatedTypeSynonym name args) ty = do
+    ty1 <- expandTypeSynonym name args
+    ty1 `unifyTypes` ty
+  unifyTypes' ty s@(SaturatedTypeSynonym _ _) = s `unifyTypes` ty
+  unifyTypes' (ForAll ident1 ty1) (ForAll ident2 ty2) = do
+    sk <- skolemize ident1 ty1
+    replaced <- replaceVarsWithUnknowns [ident2] ty2
+    sk `unifyTypes` replaced
+  unifyTypes' (ForAll ident ty1) ty2 = do
+    sk <- skolemize ident ty1
+    sk `unifyTypes` ty2
+  unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
+  unifyTypes' Number Number = return ()
+  unifyTypes' String String = return ()
+  unifyTypes' Boolean Boolean = return ()
+  unifyTypes' (Array s) (Array t) = s `unifyTypes` t
+  unifyTypes' (Object row1) (Object row2) = row1 ~~ row2
+  unifyTypes' (Function args1 ret1) (Function args2 ret2) = do
+    guardWith "Function applied to incorrect number of args" $ length args1 == length args2
+    zipWithM_ unifyTypes args1 args2
+    ret1 `unifyTypes` ret2
+  unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
+  unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
+    modulePath <- checkModulePath `fmap` lift get
+    guardWith ("Cannot unify " ++ show c1 ++ " with " ++ show c2 ++ ".") (qualify modulePath c1 == qualify modulePath c2)
+  unifyTypes' (TypeApp t1 t2) (TypeApp t3 t4) = do
+    t1 `unifyTypes` t3
+    t2 `unifyTypes` t4
+  unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()
+  unifyTypes' t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
+
+isFunction :: Value -> Bool
+isFunction (Abs _ _) = True
+isFunction (TypedValue untyped _) = isFunction untyped
+isFunction _ = False
+
+typeOf :: Maybe Ident -> Value -> Check Type
+typeOf name val = do
+  (ty, sub, checks) <- runSubst $ case name of
+        Just ident | isFunction val ->
+          case val of
+            TypedValue val ty -> do
+              kind <- lift $ kindOf ty
+              guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+              ty' <- lift $ replaceAllTypeSynonyms ty
+              check (M.singleton ident ty) val ty'
+              return ty'
+            _ -> do
+              me <- fresh
+              ty <- infer (M.singleton ident me) val
+              ty ~~ me
+              return ty
+        _ -> infer M.empty val
+  escapeCheck checks ty sub
+  skolemEscapeCheck ty
+  return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
+
+escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
+escapeCheck checks ty sub =
+  let
+    visibleUnknowns = nub $ unknowns ty
+  in
+    forM_ checks $ \check -> case check of
+      AnyUnifiable t -> do
+        let unsolvedUnknowns = nub . unknowns $ apply sub t
+        guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
+
+skolemEscapeCheck :: Type -> Check ()
+skolemEscapeCheck ty =
+  case something (extQ (mkQ Nothing findSkolems) findRSkolems) ty of
+    Nothing -> return ()
+    Just _ -> throwError "Skolem variables cannot escape. Consider adding a type signature."
+  where
+    findSkolems (Skolem _) = return ()
+    findSkolems _ = mzero
+    findRSkolems (RSkolem _) = return ()
+    findRSkolems _ = mzero
+
+setify :: Row -> Row
+setify = rowFromList . first (M.toList . M.fromList) . rowToList
+
+setifyAll :: (D.Data d) => d -> d
+setifyAll = everywhere (mkT setify)
+
+varIfUnknown :: Type -> Type
+varIfUnknown ty = mkForAll (sort . map ((:) 'u' . show) . nub $ unknowns ty) ty
+
+replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
+replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
+
+replaceTypeVars :: (D.Data d) => String -> Type -> d -> d
+replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replace)
+  where
+  replace (TypeVar v) | v == name = t
+  replace t = t
+  isShadowed (ForAll v _) | v == name = True
+  isShadowed _ = False
+
+replaceRowVars :: (D.Data d) => String -> Row -> d -> d
+replaceRowVars name r = everywhere (mkT replace)
+  where
+  replace (RowVar v) | v == name = r
+  replace t = t
+
+replaceAllVarsWithUnknowns :: Type -> Subst Check Type
+replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarsWithUnknowns [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
+
+replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
+replaceAllTypeSynonyms d = do
+  env <- getEnv
+  let syns = map (\((path, name), (args, _)) -> (Qualified path name, length args)) . M.toList $ typeSynonyms env
+  either throwError return $ saturateAllTypeSynonyms syns d
+
+desaturateAllTypeSynonyms :: (D.Data d) => d -> d
+desaturateAllTypeSynonyms = everywhere (mkT replace)
+  where
+  replace (SaturatedTypeSynonym name args) = foldl TypeApp (TypeConstructor name) args
+  replace t = t
+
+expandAllTypeSynonyms :: Type -> Subst Check Type
+expandAllTypeSynonyms (SaturatedTypeSynonym name args) = expandTypeSynonym name args >>= expandAllTypeSynonyms
+expandAllTypeSynonyms ty = return ty
+
+expandTypeSynonym :: Qualified ProperName -> [Type] -> Subst Check Type
+expandTypeSynonym name args = do
+  env <- lift getEnv
+  modulePath <- checkModulePath `fmap` lift get
+  case M.lookup (qualify modulePath name) (typeSynonyms env) of
+    Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body
+    Nothing -> error "Type synonym was not defined"
+
+ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
+ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
+
+infer :: M.Map Ident Type -> Value -> Subst Check Type
+infer m val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ do
+  ty <- infer' m val
+  escapeCheckLater ty
+  return ty
+
+infer' _ (NumericLiteral _) = return Number
+infer' _ (StringLiteral _) = return String
+infer' _ (BooleanLiteral _) = return Boolean
+infer' m (ArrayLiteral vals) = do
+  ts <- mapM (infer m) vals
+  arr <- fresh
+  forM_ ts $ \t -> arr ~~ Array t
+  return arr
+infer' m (Unary op val) = do
+  t <- infer m val
+  inferUnary op t
+infer' m (Binary op left right) = do
+  t1 <- infer m left
+  t2 <- infer m right
+  inferBinary op t1 t2
+infer' m (ObjectLiteral ps) = do
+  lift $ ensureNoDuplicateProperties ps
+  ts <- mapM (infer m . snd) ps
+  let fields = zipWith (\(name, _) t -> (name, t)) ps ts
+  return $ Object $ typesToRow fields
+infer' m (ObjectUpdate o ps) = do
+  lift $ ensureNoDuplicateProperties ps
+  obj <- infer m o
+  row <- fresh
+  ts <- mapM (infer m . snd) ps
+  let tys = zipWith (\(name, _) t -> (name, t)) ps ts
+  obj ~~ Object (rowFromList (tys, row))
+  return obj
+infer' m (Indexer index val) = do
+  el <- fresh
+  check m index Number
+  check m val (Array el)
+  return el
+infer' m (Accessor prop val) = do
+  obj <- infer m val
+  propTy <- inferProperty obj prop
+  case propTy of
+    Nothing -> do
+      field <- fresh
+      rest <- fresh
+      obj `subsumes` Object (RCons prop field rest)
+      return field
+    Just ty -> return ty
+infer' m (Abs args ret) = do
+  ts <- replicateM (length args) fresh
+  let m' = m `M.union` M.fromList (zip args ts)
+  body <- infer m' ret
+  return $ Function ts body
+infer' m app@(App _ _) = do
+  let (f, argss) = unfoldApplication app
+  ft <- infer m f
+  ret <- fresh
+  checkFunctionApplications m ft argss ret
+  return ret
+infer' m (Var var@(Qualified mp name)) = do
+  case mp of
+    ModulePath [] ->
+      case M.lookup name m of
+        Just ty -> lift $ replaceAllTypeSynonyms ty
+        Nothing -> lookupGlobal
+    _ -> lookupGlobal
+  where
+  lookupGlobal = do
+    env <- lift getEnv
+    modulePath <- checkModulePath `fmap` lift get
+    case M.lookup (qualify modulePath var) (names env) of
+      Nothing -> throwError $ show var ++ " is undefined"
+      Just (ty, _) -> lift $ replaceAllTypeSynonyms ty
+infer' m (Block ss) = do
+  ret <- fresh
+  (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
+  guardWith "Block is missing a return statement" allCodePathsReturn
+  return ret
+infer' m (Constructor c) = do
+  env <- lift getEnv
+  modulePath <- checkModulePath `fmap` lift get
+  case M.lookup (qualify modulePath c) (dataConstructors env) of
+    Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
+    Just ty -> lift $ replaceAllTypeSynonyms ty
+infer' m (Case val binders) = do
+  t1 <- infer m val
+  ret <- fresh
+  checkBinders m t1 ret binders
+  return ret
+infer' m (IfThenElse cond th el) = do
+  check m cond Boolean
+  t2 <- infer m th
+  t3 <- infer m el
+  t2 ~~ t3
+  return t2
+infer' m (TypedValue val ty) = do
+  kind <- lift $ kindOf ty
+  guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+  ty' <- lift $ replaceAllTypeSynonyms ty
+  check m val ty'
+  return ty'
+
+inferProperty :: Type -> String -> Subst Check (Maybe Type)
+inferProperty (Object row) prop = do
+  let (props, _) = rowToList row
+  return $ lookup prop props
+inferProperty (SaturatedTypeSynonym name args) prop = do
+  replaced <- expandTypeSynonym name args
+  inferProperty replaced prop
+inferProperty (ForAll ident ty) prop = do
+  replaced <- replaceVarsWithUnknowns [ident] ty
+  inferProperty replaced prop
+inferProperty _ prop = return Nothing
+
+inferUnary :: UnaryOperator -> Type -> Subst Check Type
+inferUnary op val =
+  case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
+    (valTy, resTy) -> do
+      val ~~ valTy
+      return resTy
+
+checkUnary :: M.Map Ident Type -> UnaryOperator -> Value -> Type -> Subst Check ()
+checkUnary m op val res =
+  case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
+    (valTy, resTy) -> do
+      res ~~ resTy
+      check m val valTy
+
+unaryOps :: [(UnaryOperator, (Type, Type))]
+unaryOps = [ (Negate, (Number, Number))
+           , (Not, (Boolean, Boolean))
+           , (BitwiseNot, (Number, Number))
+           ]
+
+inferBinary :: BinaryOperator -> Type -> Type -> Subst Check Type
+inferBinary op left right | isEqualityTest op = do
+  left ~~ right
+  return Boolean
+inferBinary op left right =
+  case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
+    (valTy, resTy) -> do
+      left ~~ valTy
+      right ~~ valTy
+      return resTy
+
+checkBinary :: M.Map Ident Type -> BinaryOperator -> Value -> Value -> Type -> Subst Check ()
+checkBinary m op left right res | isEqualityTest op = do
+  res ~~ Boolean
+  t1 <- infer m left
+  t2 <- infer m right
+  t1 ~~ t2
+checkBinary m op left right res =
+  case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
+    (valTy, resTy) -> do
+      res ~~ resTy
+      check m left valTy
+      check m right valTy
+
+isEqualityTest :: BinaryOperator -> Bool
+isEqualityTest EqualTo = True
+isEqualityTest NotEqualTo = True
+isEqualityTest _ = False
+
+binaryOps :: [(BinaryOperator, (Type, Type))]
+binaryOps = [ (Add, (Number, Number))
+            , (Subtract, (Number, Number))
+            , (Multiply, (Number, Number))
+            , (Divide, (Number, Number))
+            , (Modulus, (Number, Number))
+            , (BitwiseAnd, (Number, Number))
+            , (BitwiseOr, (Number, Number))
+            , (BitwiseXor, (Number, Number))
+            , (ShiftRight, (Number, Number))
+            , (ZeroFillShiftRight, (Number, Number))
+            , (And, (Boolean, Boolean))
+            , (Or, (Boolean, Boolean))
+            , (Concat, (String, String))
+            , (Modulus, (Number, Number))
+            , (LessThan, (Number, Boolean))
+            , (LessThanOrEqualTo, (Number, Boolean))
+            , (GreaterThan, (Number, Boolean))
+            , (GreaterThanOrEqualTo, (Number, Boolean))
+            ]
+
+inferBinder :: Type -> Binder -> Subst Check (M.Map Ident Type)
+inferBinder _ NullBinder = return M.empty
+inferBinder val (StringBinder _) = val ~~ String >> return M.empty
+inferBinder val (NumberBinder _) = val ~~ Number >> return M.empty
+inferBinder val (BooleanBinder _) = val ~~ Boolean >> return M.empty
+inferBinder val (VarBinder name) = return $ M.singleton name val
+inferBinder val (NullaryBinder ctor) = do
+  env <- lift getEnv
+  modulePath <- checkModulePath `fmap` lift get
+  case M.lookup (qualify modulePath ctor) (dataConstructors env) of
+    Just ty -> do
+      ty `subsumes` val
+      return M.empty
+    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
+inferBinder val (UnaryBinder ctor binder) = do
+  env <- lift getEnv
+  modulePath <- checkModulePath `fmap` lift get
+  case M.lookup (qualify modulePath ctor) (dataConstructors env) of
+    Just ty -> do
+      Function [obj] ret <- replaceAllVarsWithUnknowns ty
+      val `subsumes` ret
+      inferBinder obj binder
+    _ -> throwError $ "Constructor " ++ show ctor ++ " is not defined"
+inferBinder val (ObjectBinder props) = do
+  row <- fresh
+  rest <- fresh
+  m1 <- inferRowProperties row rest props
+  val ~~ Object row
+  return m1
+  where
+  inferRowProperties :: Row -> Row -> [(String, Binder)] -> Subst Check (M.Map Ident Type)
+  inferRowProperties nrow row [] = nrow ~~ row >> return M.empty
+  inferRowProperties nrow row ((name, binder):binders) = do
+    propTy <- fresh
+    m1 <- inferBinder propTy binder
+    m2 <- inferRowProperties nrow (RCons name propTy row) binders
+    return $ m1 `M.union` m2
+inferBinder val (ArrayBinder binders rest) = do
+  el <- fresh
+  m1 <- M.unions <$> mapM (inferBinder el) binders
+  val ~~ Array el
+  case rest of
+    Nothing -> return m1
+    Just binder -> do
+      m2 <- inferBinder val binder
+      return $ m1 `M.union` m2
+inferBinder val (NamedBinder name binder) = do
+  m <- inferBinder val binder
+  return $ M.insert name val m
+
+inferGuardedBinder :: M.Map Ident Type -> Type -> Binder -> Subst Check (M.Map Ident Type)
+inferGuardedBinder m val (GuardedBinder cond binder) = do
+  m1 <- inferBinder val binder
+  check (m1 `M.union` m) cond Boolean
+  return m1
+inferGuardedBinder m val b = inferBinder val b
+
+checkBinders :: M.Map Ident Type -> Type -> Type -> [(Binder, Value)] -> Subst Check ()
+checkBinders _ _ _ [] = return ()
+checkBinders m nval ret ((binder, val):bs) = do
+  m1 <- inferGuardedBinder m nval binder
+  check (m1 `M.union` m) val ret
+  checkBinders m nval ret bs
+
+assignVariable :: Ident -> M.Map Ident Type -> Subst Check ()
+assignVariable name m =
+  case M.lookup name m of
+    Nothing -> return ()
+    Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
+
+checkStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> Statement -> Subst Check (Bool, M.Map Ident Type)
+checkStatement m mass ret (VariableIntroduction name val) = do
+  assignVariable name (m `M.union` mass)
+  t <- infer m val
+  return (False, M.insert name t mass)
+checkStatement m mass ret (Assignment ident val) = do
+  t <- infer m val
+  case M.lookup ident mass of
+    Nothing -> throwError $ "No local variable with name " ++ show ident
+    Just ty -> do t ~~ ty
+                  return (False, mass)
+checkStatement m mass ret (While val inner) = do
+  check m val Boolean
+  (allCodePathsReturn, _) <- checkBlock m mass ret inner
+  return (allCodePathsReturn, mass)
+checkStatement m mass ret (If ifst) = do
+  allCodePathsReturn <- checkIfStatement m mass ret ifst
+  return (allCodePathsReturn, mass)
+checkStatement m mass ret (For ident start end inner) = do
+  assignVariable ident (m `M.union` mass)
+  check (m `M.union` mass) start Number
+  check (m `M.union` mass) end Number
+  let mass1 = M.insert ident Number mass
+  (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
+  return (allCodePathsReturn, mass)
+checkStatement m mass ret (ForEach ident vals inner) = do
+  assignVariable ident (m `M.union` mass)
+  val <- fresh
+  check (m `M.union` mass) vals (Array val)
+  let mass1 = M.insert ident val mass
+  (allCodePathsReturn, _) <- checkBlock (m `M.union` mass1) mass1 ret inner
+  guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
+  return (False, mass)
+checkStatement m mass ret (Return val) = do
+  check (m `M.union` mass) val ret
+  return (True, mass)
+
+checkIfStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> IfStatement -> Subst Check Bool
+checkIfStatement m mass ret (IfStatement val thens Nothing) = do
+  check m val Boolean
+  _ <- checkBlock m mass ret thens
+  return False
+checkIfStatement m mass ret (IfStatement val thens (Just elses)) = do
+  check m val Boolean
+  (allCodePathsReturn1, _) <- checkBlock m mass ret thens
+  allCodePathsReturn2 <- checkElseStatement m mass ret elses
+  return $ allCodePathsReturn1 && allCodePathsReturn2
+
+checkElseStatement :: M.Map Ident Type -> M.Map Ident Type -> Type -> ElseStatement -> Subst Check Bool
+checkElseStatement m mass ret (Else elses) = fst <$> checkBlock m mass ret elses
+checkElseStatement m mass ret (ElseIf ifst) = checkIfStatement m mass ret ifst
+
+checkBlock :: M.Map Ident Type -> M.Map Ident Type -> Type -> [Statement] -> Subst Check (Bool, M.Map Ident Type)
+checkBlock _ mass _ [] = return (False, mass)
+checkBlock m mass ret (s:ss) = do
+  (b1, mass1) <- checkStatement (m `M.union` mass) mass ret s
+  case (b1, ss) of
+    (True, []) -> return (True, mass1)
+    (True, _) -> throwError "Unreachable code"
+    (False, ss) -> do
+      (b2, mass2) <- checkBlock m mass1 ret ss
+      return (b2, mass2)
+
+skolemize :: String -> Type -> Subst Check Type
+skolemize ident ty = do
+  tsk <- Skolem <$> fresh'
+  rsk <- RSkolem <$> fresh'
+  return $ replaceRowVars ident rsk $ replaceTypeVars ident tsk ty
+
+check :: M.Map Ident Type -> Value -> Type -> Subst Check ()
+check m val ty = rethrow errorMessage $ check' m val ty
+  where
+  errorMessage msg =
+    "Error checking type of term " ++
+    prettyPrintValue val ++
+    " against type " ++
+    prettyPrintType ty ++
+    ":\n" ++
+    msg
+
+check' :: M.Map Ident Type -> Value -> Type -> Subst Check ()
+check' m val (ForAll idents ty) = do
+  sk <- skolemize idents ty
+  check m val sk
+check' m val u@(TUnknown _) = do
+  ty <- infer m val
+  -- Don't unify an unknown with an inferred polytype
+  ty' <- replaceAllVarsWithUnknowns ty
+  ty' ~~ u
+check' m (NumericLiteral _) Number = return ()
+check' m (StringLiteral _) String = return ()
+check' m (BooleanLiteral _) Boolean = return ()
+check' m (Unary op val) ty = checkUnary m op val ty
+check' m (Binary op left right) ty = checkBinary m op left right ty
+check' m (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check m val ty)
+check' m (Indexer index vals) ty = check m index Number >> check m vals (Array ty)
+check' m (Abs args ret) (Function argTys retTy) = do
+  guardWith "Incorrect number of function arguments" (length args == length argTys)
+  let bindings = M.fromList (zip args argTys)
+  check (bindings `M.union` m) ret retTy
+check' m app@(App _ _) ret = do
+  let (f, argss) = unfoldApplication app
+  ft <- infer m f
+  checkFunctionApplications m ft argss ret
+check' m v@(Var var@(Qualified mp name)) ty = do
+  case mp of
+    ModulePath [] ->
+      case M.lookup name m of
+        Just ty1 -> do
+          repl <- lift $ replaceAllTypeSynonyms ty1
+          repl `subsumes` ty
+        Nothing -> lookupGlobal
+    _ -> lookupGlobal
+  where
+  lookupGlobal = do
+    env <- lift getEnv
+    modulePath <- checkModulePath `fmap` lift get
+    case M.lookup (qualify modulePath var) (names env) of
+      Nothing -> throwError $ show var ++ " is undefined"
+      Just (ty1, _) -> do
+        repl <- lift $ replaceAllTypeSynonyms ty1
+        repl `subsumes` ty
+check' m (TypedValue val ty1) ty2 = do
+  kind <- lift $ kindOf ty1
+  guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+  ty1 `subsumes` ty2
+  check m val ty1
+check' m (Case val binders) ret = do
+  t1 <- infer m val
+  checkBinders m t1 ret binders
+check' m (IfThenElse cond th el) ty = do
+  check m cond Boolean
+  check m th ty
+  check m el ty
+check' m (ObjectLiteral ps) (Object row) = do
+  lift $ ensureNoDuplicateProperties ps
+  checkProperties m ps row False
+check' m (ObjectUpdate obj ps) objTy@(Object row) = do
+  lift $ ensureNoDuplicateProperties ps
+  check m obj objTy
+  checkProperties m ps row True
+check' m (Accessor prop val) ty = do
+  rest <- fresh
+  check m val (Object (RCons prop ty rest))
+check' m (Block ss) ret = do
+  (allCodePathsReturn, _) <- checkBlock m M.empty ret ss
+  guardWith "Block is missing a return statement" allCodePathsReturn
+check' m (Constructor c) ty = do
+  env <- lift getEnv
+  modulePath <- checkModulePath `fmap` lift get
+  case M.lookup (qualify modulePath c) (dataConstructors env) of
+    Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
+    Just ty1 -> do
+      repl <- lift $ replaceAllTypeSynonyms ty1
+      repl `subsumes` ty
+check' m val (SaturatedTypeSynonym name args) = do
+  ty <- expandTypeSynonym name args
+  check m val ty
+check' _ val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
+
+checkProperties :: M.Map Ident Type -> [(String, Value)] -> Row -> Bool -> Subst Check ()
+checkProperties m ps row lax = let (ts, r') = rowToList row in go ps ts r' where
+  go [] [] REmpty = return ()
+  go [] [] u@(RUnknown _) = u ~~ REmpty
+  go [] [] (RSkolem _) | lax = return ()
+  go [] ((p, _): _) _ | lax = return ()
+                      | otherwise = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have property " ++ p
+  go ((p,_):_) [] REmpty = throwError $ "Property " ++ p ++ " is not present in closed object type " ++ prettyPrintRow row
+  go ((p,v):ps) [] u@(RUnknown _) = do
+    ty <- infer m v
+    rest <- fresh
+    u ~~ RCons p ty rest
+    go ps [] rest
+  go ((p,v):ps) ts r =
+    case lookup p ts of
+      Nothing -> do
+        ty <- infer m v
+        rest <- fresh
+        r ~~ RCons p ty rest
+        go ps ts rest
+      Just ty -> do
+        check m v ty
+        go ps (delete (p, ty) ts) r
+  go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)
+
+unfoldApplication :: Value -> (Value, [[Value]])
+unfoldApplication = go []
+  where
+  go argss (App f args) = go (args:argss) f
+  go argss f = (f, argss)
+
+checkFunctionApplications :: M.Map Ident Type -> Type -> [[Value]] -> Type -> Subst Check ()
+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
+  checkFunctionApplications m f argss ret
+
+checkFunctionApplication :: M.Map Ident Type -> Type -> [Value] -> Type -> Subst Check ()
+checkFunctionApplication m fnTy args ret = rethrow errorMessage $ checkFunctionApplication' m fnTy args ret
+  where
+  errorMessage msg = "Error applying function of type "
+    ++ prettyPrintType fnTy
+    ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
+    ++ ", expecting value of type "
+    ++ prettyPrintType ret ++ ":\n" ++ msg
+
+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
+  checkFunctionApplication m replaced args ret
+checkFunctionApplication' m u@(TUnknown _) args ret = do
+  tyArgs <- mapM (\arg -> infer m arg >>= replaceAllVarsWithUnknowns) args
+  u ~~ Function tyArgs ret
+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 "
+  ++ prettyPrintType fnTy
+  ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
+  ++ ". Expecting value of type " ++ prettyPrintType ret ++ "."
+
+subsumes :: Type -> Type -> Subst Check ()
+subsumes (ForAll ident ty1) ty2 = do
+  replaced <- replaceVarsWithUnknowns [ident] ty1
+  replaced `subsumes` ty2
+subsumes (Function args1 ret1) (Function args2 ret2) = do
+  zipWithM subsumes args2 args1
+  ret1 `subsumes` ret2
+subsumes ty1 ty2 = ty1 ~~ ty2
+
diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs
--- a/src/Language/PureScript/Types.hs
+++ b/src/Language/PureScript/Types.hs
@@ -18,27 +18,57 @@
 
 import Data.Data
 import Language.PureScript.Names
+import Language.PureScript.Unknown (Unknown(..))
 
 data Type
-  = TUnknown Int
+  = TUnknown (Unknown Type)
   | Number
   | String
   | Boolean
   | Array Type
   | Object Row
-  | Function [Type] Type
+  | Function [PolyType] Type
   | TypeVar String
   | TypeConstructor (Qualified ProperName)
   | TypeApp Type Type
-  | SaturatedTypeSynonym (Qualified ProperName) [Type] deriving (Show, Eq, Data, Typeable)
+  | SaturatedTypeSynonym (Qualified ProperName) [Type]
+  | ForAll String Type
+  | Skolem Int deriving (Show, Eq, Data, Typeable)
 
-data PolyType = PolyType [String] Type deriving (Show, Eq, Data, Typeable)
+type PolyType = Type
 
 data Row
-  = RUnknown Int
+  = RUnknown (Unknown Row)
   | RowVar String
   | REmpty
-  | RCons String Type Row deriving (Show, Eq, Data, Typeable)
+  | RCons String Type Row
+  | RSkolem Int deriving (Show, Eq, Data, Typeable)
 
-monoType :: Type -> PolyType
-monoType = PolyType []
+typesToRow :: [(String, Type)] -> Row
+typesToRow [] = REmpty
+typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
+
+rowToList :: Row -> ([(String, Type)], Row)
+rowToList (RCons name ty row) = let (tys, rest) = rowToList row
+                               in ((name, ty):tys, rest)
+rowToList r = ([], r)
+
+rowFromList :: ([(String, Type)], Row) -> Row
+rowFromList ([], r) = r
+rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
+
+isMonoType :: Type -> Bool
+isMonoType (ForAll _ _) = False
+isMonoType ty = isPolyType ty
+
+isPolyType :: Type -> Bool
+isPolyType (Array ty) = isMonoType ty
+isPolyType (Object ps) = all isPolyType (map snd . fst $ rowToList ps)
+isPolyType (Function args ret) = all isPolyType args && isPolyType ret
+isPolyType (TypeApp t1 t2) = isMonoType t1 && isMonoType t2
+isPolyType (SaturatedTypeSynonym _ args) = all isPolyType args
+isPolyType (ForAll idents ty) = isPolyType ty
+isPolyType _ = True
+
+mkForAll :: [String] -> Type -> Type
+mkForAll = flip . foldl . flip $ ForAll
diff --git a/src/Language/PureScript/Unknown.hs b/src/Language/PureScript/Unknown.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PureScript/Unknown.hs
@@ -0,0 +1,25 @@
+-----------------------------------------------------------------------------
+--
+-- Module      :  Language.PureScript.Unknown
+-- Copyright   :  (c) Phil Freeman 2013
+-- License     :  MIT
+--
+-- Maintainer  :  Phil Freeman <paf31@cantab.net>
+-- Stability   :  experimental
+-- Portability :
+--
+-- |
+--
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE DeriveDataTypeable #-}
+
+module Language.PureScript.Unknown where
+
+import Data.Data
+import Data.Typeable
+
+newtype Unknown t = Unknown { runUnknown :: Int } deriving (Show, Eq, Ord, Data, Typeable)
+
+
+