diff --git a/libraries/prelude/prelude.purs b/libraries/prelude/prelude.purs
--- a/libraries/prelude/prelude.purs
+++ b/libraries/prelude/prelude.purs
@@ -61,10 +61,37 @@
     read "true" = true
     read _ = false
 
+  infixl 4 <$>
+
+  class Functor f where
+    (<$>) :: forall a b. (a -> b) -> f a -> f b
+
+  infixl 4 <*>
+
+  class Applicative f where
+    pure :: forall a. a -> f a
+    (<*>) :: forall a b. f (a -> b) -> f a -> f b
+
+  instance (Applicative f) => Functor f where
+    (<$>) f a = pure f <*> a
+
+  infixl 3 <|>
+
+  class Alternative f where
+    empty :: forall a. f a
+    (<|>) :: forall a. f a -> f a -> f a
+
   class Monad m where
     ret :: forall a. a -> m a
     (>>=) :: forall a b. m a -> (a -> m b) -> m b
 
+  instance (Monad m) => Applicative m where
+    pure = ret
+    (<*>) f a = do
+      f' <- f
+      a' <- a
+      ret (f' a')
+
   infixl 5 *
   infixl 5 /
   infixl 5 %
@@ -326,6 +353,74 @@
                       \  };\
                       \}" :: String -> String -> String
 
+module Monoid where
+
+  import Prelude
+
+  infixr 6 <>
+
+  class Monoid m where
+    mempty :: m
+    (<>) :: m -> m -> m
+  
+  instance Monoid String where
+    mempty = ""
+    (<>) = (++)
+
+  mconcat :: forall m. (Monoid m) => [m] -> m
+  mconcat [] = mempty
+  mconcat (m:ms) = m <> mconcat ms
+
+module Monad where
+
+  import Prelude
+  import Arrays
+
+  replicateM :: forall m a. (Monad m) => Number -> m a -> m [a]
+  replicateM 0 _ = ret []
+  replicateM n m = do
+    a <- m
+    as <- replicateM (n - 1) m
+    ret (a : as) 
+
+  mapM :: forall m a b. (Monad m) => (a -> m b) -> [a] -> m [b]
+  mapM _ [] = ret []
+  mapM f (a:as) = do
+    b <- f a
+    bs <- mapM f as
+    ret (b : bs)
+
+  infixr 1 >=>
+  infixr 1 <=<
+
+  (>=>) :: forall m a b c. (Monad m) => (a -> m b) -> (b -> m c) -> a -> m c
+  (>=>) f g a = do
+    b <- f a
+    g b
+    
+  (<=<) :: forall m a b c. (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c 
+  (<=<) = flip (>=>)
+
+  sequence :: forall m a. (Monad m) => [m a] -> m [a]
+  sequence [] = ret []
+  sequence (m:ms) = do
+    a <- m
+    as <- sequence ms
+    ret (a : as)
+
+  join :: forall m a. (Monad m) => m (m a) -> m a
+  join mm = do
+    m <- mm
+    m
+
+  foldM :: forall m a b. (Monad m) => (a -> b -> m a) -> a -> [b] -> m a
+  foldM _ a [] = ret a
+  foldM f a (b:bs) = f a b >>= \a' -> foldM f a' bs
+
+  when :: forall m. (Monad m) => Boolean -> m {} -> m {}
+  when true m = m
+  when false _ = ret {}
+
 module Maybe where
 
   import Prelude
@@ -408,9 +503,9 @@
                         \  };\
                         \}" :: forall a. [a] -> [a] -> [a]
 
-  foreign import join "function join(l) {\
-                      \  return l.join();\
-                      \}" :: [String] -> String
+  foreign import joinS "function joinS(l) {\
+                       \  return l.join();\
+                       \}" :: [String] -> String
 
   foreign import joinWith "function joinWith(l) {\
                           \  return function (s) {\
@@ -467,6 +562,9 @@
   (:) :: forall a. a -> [a] -> [a]
   (:) a = concat [a]
 
+  singleton :: forall a. a -> [a]
+  singleton a = [a]
+
   concatMap :: forall a b. [a] -> (a -> [b]) -> [b]
   concatMap [] f = []
   concatMap (a:as) f = f a `concat` concatMap as f
@@ -476,9 +574,9 @@
   filter p (x:xs) | p x = x : filter p xs
   filter p (_:xs) = filter p xs
 
-  empty :: forall a. [a] -> Boolean
-  empty [] = true
-  empty _ = false
+  isEmpty :: forall a. [a] -> Boolean
+  isEmpty [] = true
+  isEmpty _ = false
 
   range :: Number -> Number -> [Number]
   range lo hi = {
@@ -505,6 +603,14 @@
     show [] = "[]"
     show (x:xs) = show x ++ " : " ++ show xs
 
+  instance Prelude.Monad [] where
+    ret = singleton
+    (>>=) = concatMap
+
+  instance Prelude.Alternative [] where
+    empty = []
+    (<|>) = concat
+
 module Tuple where
 
   import Prelude
@@ -783,6 +889,46 @@
     ret = retEff
     (>>=) = bindEff
 
+  foreign import untilE "function untilE(f) {\
+			\  return function() {\
+			\    while (!f()) { }\
+			\    return {};\
+			\  };\
+                        \}" :: forall e. Eff e Boolean -> Eff e {}
+
+  foreign import whileE "function whileE(f) {\
+			\  return function(a) {\
+			\    return function() {\
+			\      while (f()) {\
+                        \        a();\
+                        \      }\
+			\      return {};\
+                        \    };\
+                        \  };\
+                        \}" :: forall e. Eff e Boolean -> Eff e {} -> Eff e {}
+ 
+  foreign import forE "function forE(lo) {\
+	              \  return function(hi) {\
+	              \    return function(f) {\
+	              \      return function() {\
+	              \        for (var i = lo; i < hi; i++) {\
+		      \          f(i)();\
+                      \        }\
+                      \      };\
+                      \    };\
+                      \  };\
+                      \}" :: forall e. Number -> Number -> (Number -> Eff e {}) -> Eff e {}
+
+
+  foreign import foreachE "function foreachE(as) {\
+	                  \  return function(f) {\
+	                  \    for (var i = 0; i < as.length; i++) {\
+		          \      f(as[i])();\
+                          \    }\
+                          \  };\
+                          \}" :: forall e a. [a] -> (a -> Eff e {}) -> Eff e {}
+
+
 module Random where
 
   import Eff
@@ -790,9 +936,7 @@
   foreign import data Random :: !
 
   foreign import random "function random() {\
-                        \  return function() {\
-                        \    return Math.random();\
-                        \  };\
+                        \  return Math.random();\
                         \}" :: forall e. Eff (random :: Random | e) Number
 
 module Errors where
diff --git a/psc/Main.hs b/psc/Main.hs
--- a/psc/Main.hs
+++ b/psc/Main.hs
@@ -28,10 +28,10 @@
 preludeFilename = Paths.getDataFileName "libraries/prelude/prelude.purs"
 
 readInput :: Maybe [FilePath] -> IO (Either ParseError [P.Module])
-readInput Nothing = getContents >>= return . P.runIndentParser P.parseModules
+readInput Nothing = getContents >>= return . P.runIndentParser "" P.parseModules
 readInput (Just input) = fmap (fmap concat . sequence) $ forM input $ \inputFile -> do
   text <- U.readFile inputFile
-  return $ P.runIndentParser P.parseModules text
+  return $ P.runIndentParser inputFile P.parseModules text
 
 compile :: P.Options -> Maybe [FilePath] -> Maybe FilePath -> Maybe FilePath -> IO ()
 compile opts input output externs = do
diff --git a/psci/Main.hs b/psci/Main.hs
--- a/psci/Main.hs
+++ b/psci/Main.hs
@@ -106,7 +106,7 @@
 loadModule moduleFile = do
   print moduleFile
   moduleText <- U.readFile moduleFile
-  return . either (Left . show) Right $ P.runIndentParser P.parseModules moduleText
+  return . either (Left . show) Right $ P.runIndentParser "" P.parseModules moduleText
 
 main :: IO ()
 main = do
@@ -128,7 +128,7 @@
     case cmd of
       Empty -> go imports loadedModules
       Expression ls -> do
-        case P.runIndentParser (P.whiteSpace *> P.parseValue <* Parsec.eof) (unlines ls) of
+        case P.runIndentParser "" (P.whiteSpace *> P.parseValue <* Parsec.eof) (unlines ls) of
           Left err -> outputStrLn (show err)
           Right decl -> handleDeclaration loadedModules imports decl
         go imports loadedModules
diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.3.8.1
+version: 0.3.9
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
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
@@ -128,7 +128,7 @@
   where
   getFunctionArgumentType :: Type -> Maybe Type
   getFunctionArgumentType (TypeApp (TypeApp t funArg) _) | t == tyFunction = Just funArg
-  getFunctionArgumentType (ForAll _ ty') = getFunctionArgumentType ty'
+  getFunctionArgumentType (ForAll _ ty' _) = getFunctionArgumentType ty'
   getFunctionArgumentType _ = Nothing
   argumentCheck :: JS -> Type -> [JS]
   argumentCheck val t | t == tyNumber = [typeCheck val "number"]
@@ -141,7 +141,7 @@
     in
       typeCheck val "object" : concatMap (\(prop, ty') -> argumentCheck (JSAccessor prop val) ty') pairs
   argumentCheck val (TypeApp (TypeApp t _) _) | t == tyFunction = [typeCheck val "function"]
-  argumentCheck val (ForAll _ ty') = argumentCheck val ty'
+  argumentCheck val (ForAll _ ty' _) = argumentCheck val ty'
   argumentCheck _ _ = []
   typeCheck :: JS -> String -> JS
   typeCheck js ty' = JSIfElse (JSBinary NotEqualTo (JSTypeOf js) (JSStringLiteral ty')) (JSBlock [JSThrow (JSStringLiteral $ ty' ++ " expected")]) Nothing
@@ -253,7 +253,7 @@
   where
   numConstructors ty = length $ filter (\(ty1, _) -> ((==) `on` typeConstructor) ty ty1) $ M.elems $ dataConstructors e
   typeConstructor (TypeConstructor qual) = qualify m qual
-  typeConstructor (ForAll _ ty) = typeConstructor ty
+  typeConstructor (ForAll _ ty _) = typeConstructor ty
   typeConstructor (TypeApp (TypeApp t _) ty) | t == tyFunction = typeConstructor ty
   typeConstructor (TypeApp ty _) = typeConstructor ty
   typeConstructor fn = error $ "Invalid arguments to typeConstructor: " ++ show fn
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
@@ -399,5 +399,5 @@
 -- |
 -- Run a parser which supports indentation
 --
-runIndentParser :: P.Parsec String ParseState a -> String -> Either P.ParseError a
-runIndentParser p = P.runParser p (ParseState 0) ""
+runIndentParser :: FilePath -> P.Parsec String ParseState a -> String -> Either P.ParseError a
+runIndentParser filePath p = P.runParser p (ParseState 0) filePath
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
@@ -36,10 +36,10 @@
   match (TypeApp arr ty) | arr == tyArray = Just $ "[" ++ prettyPrintType ty ++ "]"
   match (TypeConstructor ctor) = Just $ show ctor
   match (TUnknown (Unknown u)) = Just $ 'u' : show u
-  match (Skolem s) = Just $ 's' : show s
+  match (Skolem s _) = Just $ 's' : show s
   match (ConstrainedType deps ty) = Just $ "(" ++ intercalate "," (map (\(pn, ty') -> show pn ++ " (" ++ prettyPrintType ty' ++ ")") deps) ++ ") => " ++ prettyPrintType ty
   match (SaturatedTypeSynonym name args) = Just $ show name ++ "<" ++ intercalate "," (map prettyPrintType args) ++ ">"
-  match (ForAll ident ty) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty
+  match (ForAll ident ty _) = Just $ "forall " ++ ident ++ ". " ++ prettyPrintType ty
   match REmpty = Just $ prettyPrintRow REmpty
   match row@(RCons _ _ _) = Just $ prettyPrintRow row
   match _ = Nothing
@@ -56,7 +56,7 @@
   tailToPs REmpty = ""
   tailToPs (TUnknown (Unknown u)) = " | u" ++ show u
   tailToPs (TypeVar var) = " | " ++ var
-  tailToPs (Skolem s) = " | s" ++ show s
+  tailToPs (Skolem s _) = " | s" ++ show s
   tailToPs _ = error "Invalid row tail"
   toList :: [(String, Type)] -> Type -> ([(String, Type)], Type)
   toList tys (RCons name ty row) = toList ((name, ty):tys) row
diff --git a/src/Language/PureScript/Sugar/TypeClasses.hs b/src/Language/PureScript/Sugar/TypeClasses.hs
--- a/src/Language/PureScript/Sugar/TypeClasses.hs
+++ b/src/Language/PureScript/Sugar/TypeClasses.hs
@@ -74,7 +74,7 @@
 typeClassMemberToDictionaryAccessor name arg (TypeDeclaration ident ty) =
   ExternDeclaration TypeClassAccessorImport ident
     (Just (JSFunction (Just $ identToJs ident) ["dict"] (JSBlock [JSReturn (JSAccessor (identToJs ident) (JSVar "dict"))])))
-    (ForAll arg (ConstrainedType [(Qualified Nothing name, TypeVar arg)] ty))
+    (ForAll arg (ConstrainedType [(Qualified Nothing name, TypeVar arg)] ty) Nothing)
 typeClassMemberToDictionaryAccessor _ _ _ = error "Invalid declaration in type class definition"
 
 typeInstanceDictionaryDeclaration :: ModuleName -> [(Qualified ProperName, Type)] -> Qualified ProperName -> Type -> [Declaration] -> Desugar Declaration
@@ -120,7 +120,7 @@
 qualifiedToString _ (Qualified (Just (ModuleName mn)) pn) = runProperName mn ++ "_" ++ runProperName pn
 
 quantify :: Type -> Type
-quantify ty' = foldr ForAll ty' tyVars
+quantify ty' = foldr (\arg t -> ForAll arg t Nothing) ty' tyVars
   where
   tyVars = nub $ everything (++) (mkQ [] collect) ty'
   collect (TypeVar v) = [v]
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
@@ -230,7 +230,7 @@
       addTypeClassDictionaries [tcd { tcdName = (Qualified (Just currentModule) ident), tcdType = TCDAlias (tcdName tcd) }]
   constructs (TypeConstructor (Qualified (Just mn) pn')) pn
     = mn == moduleName && pn' == pn
-  constructs (ForAll _ ty) pn = ty `constructs` pn
+  constructs (ForAll _ ty _) pn = ty `constructs` pn
   constructs (TypeApp (TypeApp t _) ty) pn | t == tyFunction = ty `constructs` pn
   constructs (TypeApp ty _) pn = ty `constructs` pn
   constructs fn _ = error $ "Invalid arguments to constructs: " ++ show fn
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
@@ -142,7 +142,7 @@
   k2 <- infer t2
   k1 =?= FunKind k2 k0
   return k0
-infer (ForAll ident ty) = do
+infer (ForAll ident ty _) = do
   k <- fresh
   Just moduleName <- checkCurrentModule <$> get
   bindLocalTypeVariables moduleName [(ProperName ident, k)] $ infer ty
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
@@ -45,7 +45,8 @@
 import Data.Maybe (maybeToList, isNothing, isJust, fromMaybe)
 import qualified Data.Data as D
 import Data.Generics
-       (mkM, everywhereM, everything, mkT, something, everywhere, mkQ)
+       (everythingWithContext, mkM, everywhereM, everything, mkT,
+        something, everywhere, mkQ)
 
 import Language.PureScript.Values
 import Language.PureScript.Types
@@ -66,6 +67,7 @@
 
 import qualified Data.Map as M
 import Data.Function (on)
+import Debug.Trace (trace)
 
 instance Partial Type where
   unknown = TUnknown
@@ -86,17 +88,23 @@
   unifyTypes' (TUnknown u) t = u =:= t
   unifyTypes' t (TUnknown u) = u =:= t
   unifyTypes' (SaturatedTypeSynonym name args) ty = do
-    ty1 <- expandTypeSynonym name args
+    ty1 <- introduceSkolemScope <=< 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 <- replaceVarWithUnknown ident2 ty2
-    sk `unifyTypes` replaced
-  unifyTypes' (ForAll ident ty1) ty2 = do
-    sk <- skolemize ident ty1
+  unifyTypes' (ForAll ident1 ty1 sc1) (ForAll ident2 ty2 sc2) =
+    case (sc1, sc2) of
+      (Just sc1', Just sc2') -> do
+        sko <- newSkolemConstant
+        let sk1 = skolemize ident1 sko sc1' ty1
+        let sk2 = skolemize ident2 sko sc2' ty2
+        sk1 `unifyTypes` sk2
+      _ -> throwError (prettyPrintType ty1)
+  unifyTypes' (ForAll ident ty1 (Just sc)) ty2 = do
+    sko <- newSkolemConstant
+    let sk = skolemize ident sko sc ty1
     sk `unifyTypes` ty2
-  unifyTypes' ty f@(ForAll _ _) = f `unifyTypes` ty
+  unifyTypes' (ForAll _ _ _) _ = throwError "Skolem variable scope is unspecified"
+  unifyTypes' ty f@(ForAll _ _ _) = f `unifyTypes` ty
   unifyTypes' (Object row1) (Object row2) = row1 =?= row2
   unifyTypes' (TypeVar v1) (TypeVar v2) | v1 == v2 = return ()
   unifyTypes' (TypeConstructor c1) (TypeConstructor c2) = do
@@ -106,7 +114,7 @@
   unifyTypes' (TypeApp t3 t4) (TypeApp t5 t6) = do
     t3 `unifyTypes` t5
     t4 `unifyTypes` t6
-  unifyTypes' (Skolem s1) (Skolem s2) | s1 == s2 = return ()
+  unifyTypes' (Skolem s1 _) (Skolem s2 _) | s1 == s2 = return ()
   unifyTypes' r1@(RCons _ _ _) r2 = unifyRows r1 r2
   unifyTypes' r1 r2@(RCons _ _ _) = unifyRows r1 r2
   unifyTypes' r1@REmpty r2 = unifyRows r1 r2
@@ -143,7 +151,7 @@
     unifyRows' row r others u'
   unifyRows' [] REmpty [] REmpty = return ()
   unifyRows' [] (TypeVar v1) [] (TypeVar v2) | v1 == v2 = return ()
-  unifyRows' [] (Skolem s1) [] (Skolem s2) | s1 == s2 = return ()
+  unifyRows' [] (Skolem s1 _) [] (Skolem s2 _) | s1 == s2 = return ()
   unifyRows' sd3 r3 sd4 r4 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd3, r3)) ++ " with " ++ prettyPrintRow (rowFromList (sd4, r4)) ++ "."
 
 -- |
@@ -171,22 +179,24 @@
         (ident, (val, Just (ty, checkType))) -> do
           kind <- liftCheck $ kindOf moduleName ty
           guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
-          ty' <- replaceAllTypeSynonyms ty
-          val' <- bindNames dict $ if checkType then check val ty' else return val
+          ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
+          val' <- bindNames dict $ if checkType
+                                   then TypedValue True <$> check val ty' <*> pure ty'
+                                   else return (TypedValue False val ty')
           return (ident, (val', ty'))
         (ident, (val, Nothing)) -> do
           TypedValue _ val' ty <- bindNames dict $ infer val
           ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
-          return (ident, (val', ty))
+          return (ident, (TypedValue True val' ty, ty))
       when (moduleName == ModuleName (ProperName "Main") && fst e == Ident "main") $ do
         [eff, a] <- replicateM 2 fresh
         ty =?= TypeApp (TypeApp (TypeConstructor (Qualified (Just (ModuleName (ProperName "Eff"))) (ProperName "Eff"))) eff) a
       escapeCheck val ty
       return triple
-  forM_ tys $ skolemEscapeCheck . snd . snd
   forM tys $ \(ident, (val, ty)) -> do
     val' <- replaceTypeClassDictionaries moduleName val
-    return (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'
+    rethrow (("Error in " ++ show ident ++ ": \n") ++) $ skolemEscapeCheck val'
+    return $ (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'
                    , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))
   where
   tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
@@ -238,7 +248,7 @@
     return $ Just dict
   mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
   mkDictionary fnName Nothing = Var fnName
-  mkDictionary fnName (Just dicts) = foldr (flip App) (Var fnName) dicts
+  mkDictionary fnName (Just dicts) = foldl App (Var fnName) dicts
   filterModule :: TypeClassDictionaryInScope -> Bool
   filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True
   filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
@@ -252,7 +262,9 @@
 -- and return a substitution from type variables to types which makes the type heads unify.
 --
 typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
-typeHeadsAreEqual _ _ (Skolem s1) (Skolem s2) | s1 == s2 = Just []
+typeHeadsAreEqual _ _ (Skolem s1 _) (Skolem s2 _) | s1 == s2 = Just []
+typeHeadsAreEqual _ _ (TypeVar v) t = Just [(v, t)]
+typeHeadsAreEqual _ _ t (TypeVar v) = Just [(v, t)]
 typeHeadsAreEqual m e (TypeConstructor c1) (TypeConstructor c2) | typeConstructorsAreEqual e m c1 c2 = Just []
 typeHeadsAreEqual m e (TypeApp h1 (TypeVar v)) (TypeApp h2 arg) = (:) (v, arg) <$> typeHeadsAreEqual m e h1 h2
 typeHeadsAreEqual m e t1@(TypeApp _ _) t2@(TypeApp _ (TypeVar _)) = typeHeadsAreEqual m e t2 t1
@@ -268,7 +280,7 @@
   let allUnknowns = findAllTypes value
   forM_ allUnknowns $ \t -> do
     let unsolvedUnknowns = nub . unknowns $ subst $? t
-    guardWith ("Escape check fails" ++ show (subst $? ty, subst $? t)) $ null $ unsolvedUnknowns \\ visibleUnknowns
+    guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
 
 -- |
 -- Find all type annotations occuring inside a value
@@ -282,14 +294,31 @@
 -- |
 -- Ensure skolem variables do not escape their scope
 --
-skolemEscapeCheck :: Type -> Check ()
-skolemEscapeCheck ty =
-  case something (mkQ Nothing findSkolems) ty of
-    Nothing -> return ()
-    Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature."
+skolemEscapeCheck :: Value -> Check ()
+skolemEscapeCheck (TypedValue False _ _) = return ()
+skolemEscapeCheck root@(TypedValue _ _ _) =
+  case everythingWithContext [] (++) (mkQ ((,) []) go) root of
+    [] -> return ()
+    ((binding, val) : _) -> throwError $ "Rigid/skolem type variable bound by " ++ maybe "<unknown>" prettyPrintValue binding ++ " has escaped at " ++ prettyPrintValue val
   where
-    findSkolems (Skolem _) = return ()
-    findSkolems _ = mzero
+  go :: Value -> [(SkolemScope, Value)] -> ([(Maybe Value, Value)], [(SkolemScope, Value)])
+  go val@(TypedValue _ _ (ForAll _ _ (Just sco))) scos = ([], (sco, val) : scos)
+  go val@(TypedValue _ _ ty) scos = case collectSkolems ty \\ map fst scos of
+                                      (sco : _) -> ([(findBindingScope sco, val)], scos)
+                                      _ -> ([], scos)
+    where
+    collectSkolems :: Type -> [SkolemScope]
+    collectSkolems = nub . everything (++) (mkQ [] collect)
+      where
+      collect (Skolem _ scope) = [scope]
+      collect _ = []
+  go _ scos = ([], scos)
+  findBindingScope :: SkolemScope -> Maybe Value
+  findBindingScope sco = something (mkQ Nothing go) root
+    where
+    go val@(TypedValue _ _ (ForAll _ _ (Just sco'))) | sco == sco' = Just val
+    go _ = Nothing
+skolemEscapeCheck val = throwError $ "Untyped value passed to skolemEscapeCheck: " ++ prettyPrintValue val
 
 -- |
 -- Ensure a row contains no duplicate labels
@@ -326,7 +355,7 @@
 -- Replace named type variables with new unification variables
 --
 replaceAllVarsWithUnknowns :: Type -> UnifyT Type Check Type
-replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
+replaceAllVarsWithUnknowns (ForAll ident ty _) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
 replaceAllVarsWithUnknowns ty = return ty
 
 -- |
@@ -404,7 +433,8 @@
   newVals <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
   let newTys = map (\(name, TypedValue _ _ ty) -> (name, ty)) newVals
   oldTys <- zip (map fst ps) <$> replicateM (length ps) fresh
-  o' <- check o $ Object $ rowFromList (oldTys, row)
+  let oldTy = Object $ rowFromList (oldTys, row)
+  o' <- TypedValue True <$> check o oldTy <*> pure oldTy
   return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
 infer' (Accessor prop val) = do
   typed@(TypedValue _ _ objTy) <- infer val
@@ -424,19 +454,17 @@
     return $ TypedValue True (Abs arg body) $ function ty bodyTy
 infer' (App f arg) = do
   f'@(TypedValue _ _ ft) <- infer f
-  ret <- fresh
-  app <- checkFunctionApplication f' ft arg ret
+  (ret, app) <- checkFunctionApplication f' ft arg
   return $ TypedValue True app ret
 infer' (Var var) = do
   Just moduleName <- checkCurrentModule <$> get
-  ty <- lookupVariable moduleName var
-  ty' <- replaceAllTypeSynonyms ty
-  case ty' of
+  ty <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
+  case ty of
     ConstrainedType constraints _ -> do
       env <- getEnv
       dicts <- getTypeClassDictionaries
-      return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty'
-    _ -> return $ TypedValue True (Var var) ty'
+      return $ TypedValue True (foldl App (Var var) (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) ty
+    _ -> return $ TypedValue True (Var var) ty
 infer' (Block ss) = do
   ret <- fresh
   (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
@@ -447,7 +475,7 @@
   Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName c) (dataConstructors env) of
     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
-    Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty
+    Just (ty, _) -> do ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
                        return $ TypedValue True v ty'
 infer' (Case vals binders) = do
   ts <- mapM infer vals
@@ -464,9 +492,9 @@
   Just moduleName <- checkCurrentModule <$> get
   kind <- liftCheck $ kindOf moduleName ty
   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
-  ty' <- replaceAllTypeSynonyms ty
+  ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $  ty
   val' <- if checkType then check val ty' else return val
-  return $ TypedValue True val' ty
+  return $ TypedValue True val' ty'
 infer' _ = error "Invalid argument to infer"
 
 -- |
@@ -477,9 +505,9 @@
   let (props, _) = rowToList row
   return $ lookup prop props
 inferProperty (SaturatedTypeSynonym name args) prop = do
-  replaced <- expandTypeSynonym name args
+  replaced <- introduceSkolemScope <=< expandTypeSynonym name $ args
   inferProperty replaced prop
-inferProperty (ForAll ident ty) prop = do
+inferProperty (ForAll ident ty _) prop = do
   replaced <- replaceVarWithUnknown ident ty
   inferProperty replaced prop
 inferProperty _ _ = return Nothing
@@ -551,7 +579,7 @@
   Just moduleName <- checkCurrentModule <$> get
   m1 <- M.unions <$> zipWithM inferBinder nvals binders
   r <- bindLocalVariables moduleName (M.toList m1) $ do
-    val' <- check val ret
+    val' <- TypedValue True <$> check val ret <*> pure ret
     case grd of
       Nothing -> return (binders, Nothing, val')
       Just g -> do
@@ -602,7 +630,7 @@
   return (allCodePathsReturn, mass, For ident start' end' inner')
 checkStatement mass ret (Return val) = do
   val' <- check val ret
-  return (True, mass, Return val')
+  return (True, mass, Return (TypedValue True val' ret))
 
 -- |
 -- Check the type of an if-then-else statement
@@ -643,14 +671,33 @@
       return (b, m, s':ss'')
 
 -- |
+-- Generate a new skolem constant
+--
+newSkolemConstant :: UnifyT Type Check Int
+newSkolemConstant = runUnknown <$> fresh'
+
+-- |
+-- Generate a new skolem scope
+--
+newSkolemScope :: UnifyT Type Check SkolemScope
+newSkolemScope = SkolemScope . runUnknown <$> fresh'
+
+-- |
 -- Skolemize a type variable by replacing its instances with fresh skolem constants
 --
-skolemize :: String -> Type -> UnifyT Type Check Type
-skolemize ident ty = do
-  tsk <- Skolem . runUnknown <$> fresh'
-  return $ replaceTypeVars ident tsk ty
+skolemize :: (D.Data d) => String -> Int -> SkolemScope -> d -> d
+skolemize ident sko scope d = replaceTypeVars ident (Skolem sko scope) d
 
 -- |
+-- Introduce skolem scope at every occurence of a ForAll
+--
+introduceSkolemScope :: Type -> UnifyT Type Check Type
+introduceSkolemScope = everywhereM (mkM go)
+  where
+  go (ForAll ident ty Nothing) = ForAll ident ty <$> (Just <$> newSkolemScope)
+  go other = return other
+
+-- |
 -- Check the type of a value, rethrowing errors to provide a better error message
 --
 check :: Value -> Type -> UnifyT Type Check Value
@@ -668,10 +715,13 @@
 -- Check the type of a value
 --
 check' :: Value -> Type -> UnifyT Type Check Value
-check' val (ForAll idents ty) = do
-  sk <- skolemize idents ty
-  check val sk
-check' val (ConstrainedType constraints ty) = do
+check' val t@(ForAll ident ty _) = do
+  scope <- newSkolemScope
+  sko <- newSkolemConstant
+  let sk = skolemize ident sko scope ty
+  val' <- check val sk
+  return $ TypedValue True val' (ForAll ident ty (Just scope))
+check' val t@(ConstrainedType constraints ty) = do
   env <- getEnv
   Just moduleName <- checkCurrentModule <$> get
   dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do
@@ -681,34 +731,43 @@
     TypeClassDictionaryInScope name className instanceTy Nothing TCDRegular) (map (Qualified Nothing) dictNames)
       (qualifyAllUnqualifiedNames moduleName env constraints)) $
         check val ty
-  return $ foldr Abs val' dictNames
+  return $ TypedValue True (foldr Abs val' dictNames) t
+check' val t@(SaturatedTypeSynonym name args) = do
+  ty <- introduceSkolemScope <=< expandTypeSynonym name $ args
+  val' <- check val ty
+  return $ TypedValue True val' ty
 check' val u@(TUnknown _) = do
   val'@(TypedValue _ _ ty) <- infer val
   -- Don't unify an unknown with an inferred polytype
   ty' <- replaceAllVarsWithUnknowns ty
   ty' =?= u
-  return val'
-check' v@(NumericLiteral _) t | t == tyNumber = return v
-check' v@(StringLiteral _) t | t == tyString = return v
-check' v@(BooleanLiteral _) t | t == tyBoolean = return v
-check' (ArrayLiteral vals) (TypeApp a ty) | a == tyArray = ArrayLiteral <$> forM vals (\val -> check val ty)
-check' (Abs arg ret) (TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
+  return $ TypedValue True val' ty'
+check' v@(NumericLiteral _) t | t == tyNumber =
+  return $ TypedValue True v t
+check' v@(StringLiteral _) t | t == tyString =
+  return $ TypedValue True v t
+check' v@(BooleanLiteral _) t | t == tyBoolean =
+  return $ TypedValue True v t
+check' (ArrayLiteral vals) t@(TypeApp a ty) | a == tyArray = do
+  arr <- ArrayLiteral <$> forM vals (\val -> check val ty)
+  return $ TypedValue True arr t
+check' (Abs arg ret) ty@(TypeApp (TypeApp t argTy) retTy) | t == tyFunction = do
   Just moduleName <- checkCurrentModule <$> get
   ret' <- bindLocalVariables moduleName [(arg, argTy)] $ check ret retTy
-  return $ Abs arg ret'
+  return $ TypedValue True (Abs arg ret') ty
 check' (App f arg) ret = do
   f'@(TypedValue _ _ ft) <- infer f
-  app <- checkFunctionApplication f' ft arg ret
-  return $ app
+  (ret', app) <- checkFunctionApplication f' ft arg
+  subsumes Nothing ret' ret
+  return $ TypedValue True app ret
 check' v@(Var var) ty = do
   Just moduleName <- checkCurrentModule <$> get
-  ty1 <- lookupVariable moduleName var
-  repl <- replaceAllTypeSynonyms ty1
-  ty' <- replaceAllTypeSynonyms ty
+  repl <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< lookupVariable moduleName $ var
+  ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
   v' <- subsumes (Just v) repl ty'
   case v' of
     Nothing -> throwError "Unable to check type subsumption"
-    Just v'' -> return v''
+    Just v'' -> return $ TypedValue True v'' ty'
 check' (TypedValue checkType val ty1) ty2 = do
   Just moduleName <- checkCurrentModule <$> get
   kind <- liftCheck $ kindOf moduleName ty1
@@ -718,22 +777,22 @@
     Nothing -> throwError "Unable to check type subsumption"
     Just val'' -> do
       val''' <- if checkType then check val'' ty1 else return val''
-      return $ TypedValue True val''' ty1
+      return $ TypedValue checkType (TypedValue True val''' ty1) ty2
 check' (Case vals binders) ret = do
   vals' <- mapM infer vals
   let ts = map (\(TypedValue _ _ t) -> t) vals'
   binders' <- checkBinders ts ret binders
-  return $ Case vals' binders'
+  return $ TypedValue True (Case vals' binders') ret
 check' (IfThenElse cond th el) ty = do
   cond' <- check cond tyBoolean
   th' <- check th ty
   el' <- check el ty
-  return $ IfThenElse cond' th' el'
-check' (ObjectLiteral ps) (Object row) = do
+  return $ TypedValue True (IfThenElse cond' th' el') ty
+check' (ObjectLiteral ps) t@(Object row) = do
   ensureNoDuplicateProperties ps
   ps' <- checkProperties ps row False
-  return $ ObjectLiteral ps'
-check' (ObjectUpdate obj ps) (Object row) = do
+  return $ TypedValue True (ObjectLiteral ps') t
+check' (ObjectUpdate obj ps) t@(Object row) = do
   ensureNoDuplicateProperties ps
   us <- zip (map fst ps) <$> replicateM (length ps) fresh
   let (propsToCheck, rest) = rowToList row
@@ -741,27 +800,24 @@
       remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
   obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))
   ps' <- checkProperties ps row True
-  return $ ObjectUpdate obj' ps'
+  return $ TypedValue True (ObjectUpdate obj' ps') t
 check' (Accessor prop val) ty = do
   rest <- fresh
   val' <- check val (Object (RCons prop ty rest))
-  return $ Accessor prop val'
+  return $ TypedValue True (Accessor prop val') ty
 check' (Block ss) ret = do
   (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
   guardWith "Block is missing a return statement" allCodePathsReturn
-  return $ Block ss'
+  return $ TypedValue True (Block ss') ret
 check' (Constructor c) ty = do
   env <- getEnv
   Just moduleName <- checkCurrentModule <$> get
   case M.lookup (qualify moduleName c) (dataConstructors env) of
     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
     Just (ty1, _) -> do
-      repl <- replaceAllTypeSynonyms ty1
+      repl <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty1
       _ <- subsumes Nothing repl ty
-      return $ Constructor c
-check' val (SaturatedTypeSynonym name args) = do
-  ty <- expandTypeSynonym name args
-  check val ty
+      return $ TypedValue True (Constructor c) ty
 check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
 
 -- |
@@ -774,7 +830,7 @@
   go [] [] REmpty = return []
   go [] [] u@(TUnknown _) = do u =?= REmpty
                                return []
-  go [] [] (Skolem _) | lax = return []
+  go [] [] (Skolem _ _) | 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
@@ -801,8 +857,8 @@
 -- |
 -- Check the type of a function application, rethrowing errors to provide a better error message
 --
-checkFunctionApplication :: Value -> Type -> Value -> Type -> UnifyT Type Check Value
-checkFunctionApplication fn fnTy arg ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg ret
+checkFunctionApplication :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
+checkFunctionApplication fn fnTy arg = rethrow errorMessage $ checkFunctionApplication' fn fnTy arg
   where
   errorMessage msg = "Error applying function of type "
     ++ prettyPrintType fnTy
@@ -812,34 +868,33 @@
 -- |
 -- Check the type of a function application
 --
-checkFunctionApplication' :: Value -> Type -> Value -> Type -> UnifyT Type Check Value
-checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg ret = do
+checkFunctionApplication' :: Value -> Type -> Value -> UnifyT Type Check (Type, Value)
+checkFunctionApplication' fn (TypeApp (TypeApp tyFunction' argTy) retTy) arg = do
   tyFunction' =?= tyFunction
   arg' <- check arg argTy
-  _ <- subsumes Nothing retTy ret
-  return $ App fn arg'
-checkFunctionApplication' fn (ForAll ident ty) arg ret = do
+  return (retTy, App fn arg')
+checkFunctionApplication' fn (ForAll ident ty _) arg = do
   replaced <- replaceVarWithUnknown ident ty
-  checkFunctionApplication fn replaced arg ret
-checkFunctionApplication' fn u@(TUnknown _) arg ret = do
+  checkFunctionApplication fn replaced arg
+checkFunctionApplication' fn u@(TUnknown _) arg = do
   arg' <- do
     TypedValue _ v t <- infer arg
     TypedValue True v <$> replaceAllVarsWithUnknowns t
   let ty = (\(TypedValue _ _ t) -> t) arg'
+  ret <- fresh
   u =?= function ty ret
-  return $ App fn arg'
-checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg ret = do
-  ty <- expandTypeSynonym name tyArgs
-  checkFunctionApplication fn ty arg ret
-checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg ret = do
+  return (ret, App fn arg')
+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) arg = do
+  ty <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
+  checkFunctionApplication fn ty arg
+checkFunctionApplication' fn (ConstrainedType constraints fnTy) arg = do
   env <- getEnv
   dicts <- getTypeClassDictionaries
   Just moduleName <- checkCurrentModule <$> get
-  checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg ret
-checkFunctionApplication' _ fnTy arg ret = throwError $ "Applying a function of type "
+  checkFunctionApplication' (foldl App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy arg
+checkFunctionApplication' _ fnTy arg = throwError $ "Cannot apply a function of type "
   ++ prettyPrintType fnTy
-  ++ " to argument(s) " ++ prettyPrintValue arg
-  ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."
+  ++ " to argument " ++ prettyPrintValue arg
 
 -- |
 -- Check whether one type subsumes another, rethrowing errors to provide a better error message
@@ -857,18 +912,25 @@
 -- Check whether one type subsumes another
 --
 subsumes' :: Maybe Value -> Type -> Type -> UnifyT Type Check (Maybe Value)
-subsumes' val (ForAll ident ty1) ty2 = do
+subsumes' val (ForAll ident ty1 _) ty2 = do
   replaced <- replaceVarWithUnknown ident ty1
   subsumes val replaced ty2
+subsumes' val ty1 (ForAll ident ty2 sco) =
+  case sco of
+    Just sco' -> do
+      sko <- newSkolemConstant
+      let sk = skolemize ident sko sco' ty2
+      subsumes val ty1 sk
+    Nothing -> throwError "Skolem variable scope is unspecified"
 subsumes' val (TypeApp (TypeApp f1 arg1) ret1) (TypeApp (TypeApp f2 arg2) ret2) | f1 == tyFunction && f2 == tyFunction = do
   subsumes Nothing arg2 arg1
   subsumes Nothing ret1 ret2
   return val
 subsumes' val (SaturatedTypeSynonym name tyArgs) ty2 = do
-  ty1 <- expandTypeSynonym name tyArgs
+  ty1 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
   subsumes val ty1 ty2
 subsumes' val ty1 (SaturatedTypeSynonym name tyArgs) = do
-  ty2 <- expandTypeSynonym name tyArgs
+  ty2 <- introduceSkolemScope <=< expandTypeSynonym name $ tyArgs
   subsumes val ty1 ty2
 subsumes' (Just val) (ConstrainedType constraints ty1) ty2 = do
   env <- getEnv
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
@@ -25,6 +25,11 @@
 import Language.PureScript.Names
 
 -- |
+-- An identifier for the scope of a skolem variable
+--
+newtype SkolemScope = SkolemScope { runSkolemScope :: Int } deriving (Show, Eq, Ord, Data, Typeable)
+
+-- |
 -- The type of types
 --
 data Type
@@ -55,7 +60,7 @@
   -- |
   -- Forall quantifier
   --
-  | ForAll String Type
+  | ForAll String Type (Maybe SkolemScope)
   -- |
   -- A type with a set of type class constraints
   --
@@ -63,7 +68,7 @@
   -- |
   -- A skolem constant
   --
-  | Skolem Int
+  | Skolem Int SkolemScope
   -- |
   -- An empty row
   --
@@ -128,14 +133,14 @@
 -- Check whether a type is a monotype
 --
 isMonoType :: Type -> Bool
-isMonoType (ForAll _ _) = False
+isMonoType (ForAll _ _ _) = False
 isMonoType ty = True
 
 -- |
 -- Universally quantify a type
 --
 mkForAll :: [String] -> Type -> Type
-mkForAll = flip . foldl . flip $ ForAll
+mkForAll args ty = foldl (\t arg -> ForAll arg t Nothing) ty args
 
 -- |
 -- The empty record type
@@ -151,5 +156,5 @@
   where
   replaceTypeVar (TypeVar v) | v == name = t
   replaceTypeVar other = other
-  isShadowed (ForAll v _) | v == name = True
+  isShadowed (ForAll v _ _) | v == name = True
   isShadowed _ = False
diff --git a/tests/Main.hs b/tests/Main.hs
--- a/tests/Main.hs
+++ b/tests/Main.hs
@@ -39,7 +39,7 @@
 readInput :: [FilePath] -> IO (Either ParseError [P.Module])
 readInput inputFiles = fmap (fmap concat . sequence) $ forM inputFiles $ \inputFile -> do
   text <- U.readFile inputFile
-  return $ P.runIndentParser P.parseModules text
+  return $ P.runIndentParser inputFile P.parseModules text
 
 compile :: P.Options -> [FilePath] -> IO (Either String String)
 compile opts inputFiles = do