diff --git a/prelude/prelude.purs b/prelude/prelude.purs
--- a/prelude/prelude.purs
+++ b/prelude/prelude.purs
@@ -54,6 +54,13 @@
   instance Read Boolean where
     read "true" = true
     read _ = false
+    
+  foreign import readNumber "function readNumber(n) {\
+                            \  return parseInt(n, 10);\
+                            \}" :: String -> Number
+    
+  instance Read Number where
+    read = readNumber
 
   infixl 4 <$>
 
@@ -362,6 +369,10 @@
   instance Monoid String where
     mempty = ""
     (<>) = (++)
+    
+  instance Monoid [a] where
+    mempty = []
+    (<>) = Arrays.concat
 
   mconcat :: forall m. (Monoid m) => [m] -> m
   mconcat [] = mempty
@@ -429,22 +440,52 @@
 
   fromMaybe :: forall a. a -> Maybe a -> a
   fromMaybe a = maybe a (Prelude.id :: forall a. a -> a)
+  
+  instance Prelude.Functor Maybe where
+    (<$>) fn (Just x) = Just (fn x)
+    (<$>) _ _ = Nothing
+  
+  instance Prelude.Applicative Maybe where
+    pure = Just
+    (<*>) (Just fn) x = fn <$> x
+    (<*>) Nothing _ = Nothing
 
   instance Prelude.Monad Maybe where
     return = Just
     (>>=) m f = maybe Nothing f m
+    
+  instance (Show a) => Prelude.Show (Maybe a) where
+    show (Just x) = "Just " ++ (show x)
+    show Nothing = "Nothing"
 
 module Either where
 
+  import Prelude
+
   data Either a b = Left a | Right b
 
   either :: forall a b c. (a -> c) -> (b -> c) -> Either a b -> c
   either f _ (Left a) = f a
   either _ g (Right b) = g b
+  
+  {-
+  instance Prelude.Functor (Either a) where
+    (<$>) _ (Left x) = Left x
+    (<$>) f (Right y) = Right (f y)
+  -}
+    
+  instance Prelude.Applicative (Either e) where
+    pure = Right
+    (<*>) (Left e) _ = Left e
+    (<*>) (Right f) r = f <$> r
 
   instance Prelude.Monad (Either e) where
     return = Right
     (>>=) = either (\e _ -> Left e) (\a f -> f a)
+    
+  instance (Show a, Show b) => Prelude.Show (Either a b) where
+    show (Left x) = "Left " ++ (show x)
+    show (Right y) = "Right " ++ (show y)
 
 module Arrays where
 
@@ -578,7 +619,7 @@
   range lo hi = {
       var ns = [];
       for (n <- lo until hi) {
-	ns = push ns n;
+        ns = push ns n;
       }
       return ns;
     }
@@ -598,7 +639,10 @@
   instance (Prelude.Show a) => Prelude.Show [a] where
     show [] = "[]"
     show (x:xs) = show x ++ " : " ++ show xs
-
+    
+  instance Prelude.Functor [] where
+    (<$>) = map
+    
   instance Prelude.Monad [] where
     return = singleton
     (>>=) = concatMap
diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.3.11
+version: 0.3.12
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
diff --git a/src/Language/PureScript.hs b/src/Language/PureScript.hs
--- a/src/Language/PureScript.hs
+++ b/src/Language/PureScript.hs
@@ -67,4 +67,4 @@
                       Left "Main.main is undefined"
                     return $ js ++ [JSApp (JSAccessor "main" (JSVar "Main")) []]
                 | otherwise -> return js
-  return (prettyPrintJS js', exts, env)
+  return (prettyPrintJS [(wrapExportsContainer js')], exts, env)
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
@@ -18,12 +18,15 @@
 module Language.PureScript.CodeGen.JS (
     module AST,
     declToJs,
-    moduleToJs
+    moduleToJs,
+    wrapExportsContainer
 ) where
 
 import Data.Maybe (fromMaybe, mapMaybe)
 import Data.List (sortBy)
 import Data.Function (on)
+import Data.Data (Data)
+import Data.Generics (mkQ, everything)
 
 import Control.Arrow (second)
 import Control.Monad (replicateM, forM)
@@ -55,6 +58,7 @@
                       (JSBlock (concat $ mapMaybe (\decl -> fmap (map $ optimize opts) $ declToJs opts (ModuleName pname) decl env) (decls))))
           [JSAssignment (JSVar name)
                         (JSBinary Or (JSVar name) (JSObjectLiteral []))]
+  , JSAssignment (JSAccessor name (JSVar "exports")) (JSVar name)
   ]
 
 -- |
@@ -141,13 +145,22 @@
 valueToJs _ _ _ _ = error "Invalid argument to valueToJs"
 
 -- |
--- Temporarily extends the environment to include a local variable name introduced by a lambda
--- abstraction.
+-- Temporarily extends the environment with a single local variable name
 --
 bindName :: ModuleName -> Ident -> Environment -> Environment
-bindName m ident env = env { names = M.insert (m, ident) (error "Temporary lambda variable type was read", LocalVariable) $ names env }
+bindName m ident = bindNames m [ident]
 
 -- |
+-- Temporarily extends the environment to include local variable names introduced by lambda
+-- abstractions or case statements
+--
+bindNames :: ModuleName -> [Ident] -> Environment -> Environment
+bindNames m idents env = env { names = M.fromList [ ((m, ident), (noType, LocalVariable)) | ident <- idents ] `M.union` names env }
+  where
+  noType = error "Temporary lambda variable type was read"
+
+
+-- |
 -- Generate code in the simplified Javascript intermediate representation for runtime type checks.
 --
 runtimeTypeChecks :: String -> Type -> [JS]
@@ -213,7 +226,7 @@
 bindersToJs :: Options -> ModuleName -> Environment -> [([Binder], Maybe Guard, Value)] -> [JS] -> JS
 bindersToJs opts m e binders vals = runGen (map identToJs (unusedNames (binders, vals))) $ do
   valNames <- replicateM (length vals) fresh
-  jss <- forM binders $ \(bs, grd, result) -> go valNames [JSReturn (valueToJs opts m e result)] bs grd
+  jss <- forM binders $ \(bs, grd, result) -> go valNames [JSReturn (valueToJs opts m (bindNames m (binderNames bs) e) result)] bs grd
   return $ JSApp (JSFunction Nothing valNames (JSBlock (concat jss ++ [JSThrow (JSStringLiteral "Failed pattern match")])))
                  vals
   where
@@ -226,6 +239,15 @@
     go _ _ _ _ = error "Invalid arguments to bindersToJs"
 
 -- |
+-- Collect all names introduced in binders in an expression
+--
+binderNames :: (Data d) => d -> [Ident]
+binderNames = everything (++) (mkQ [] go)
+  where
+  go (VarBinder ident) = [ident]
+  go _ = []
+
+-- |
 -- Generate code in the simplified Javascript intermediate representation for a pattern match
 -- binder.
 --
@@ -239,7 +261,7 @@
   return [JSIfElse (JSVar varName) (JSBlock done) Nothing]
 binderToJs _ _ varName done (BooleanBinder False) =
   return [JSIfElse (JSUnary Not (JSVar varName)) (JSBlock done) Nothing]
-binderToJs _ _ varName done (VarBinder ident) =
+binderToJs m e varName done (VarBinder ident) =
   return (JSVariableIntroduction (identToJs ident) (Just (JSVar varName)) : done)
 binderToJs m e varName done (NullaryBinder ctor) =
   if isOnlyConstructor m e ctor
@@ -294,7 +316,7 @@
 
 -- |
 -- Checks whether a data constructor is the only constructor for that type, used to simplify the
--- check when generating code for binders. 
+-- check when generating code for binders.
 --
 isOnlyConstructor :: ModuleName -> Environment -> Qualified ProperName -> Bool
 isOnlyConstructor m e ctor =
@@ -325,3 +347,11 @@
   elseToJs (Else sts) = JSBlock (map (statementToJs opts m e) sts)
   elseToJs (ElseIf elif) = ifToJs elif
 statementToJs opts m e (Return value) = JSReturn (valueToJs opts m e value)
+
+wrapExportsContainer :: [JS] -> JS
+wrapExportsContainer modules = JSApp (JSFunction Nothing ["exports"] $ JSBlock $ (JSStringLiteral "use strict") : modules) [exportSelector]
+  where exportSelector = JSConditional (JSBinary And (JSBinary NotEqualTo (JSTypeOf $ JSVar "module") (JSStringLiteral "undefined")) (JSAccessor "exports" (JSVar "module")))
+                           (JSAccessor "exports" (JSVar "module"))
+                           (JSConditional (JSBinary NotEqualTo (JSTypeOf $ JSVar "window") (JSStringLiteral "undefined"))
+                             (JSAssignment (JSAccessor "PS" (JSVar "window")) (JSObjectLiteral []))
+                             (JSApp (JSFunction Nothing [] $ JSBlock [JSThrow $ JSStringLiteral "PureScript doesn't know how to export modules in the current environment"]) []))
diff --git a/src/Language/PureScript/Pretty/JS.hs b/src/Language/PureScript/Pretty/JS.hs
--- a/src/Language/PureScript/Pretty/JS.hs
+++ b/src/Language/PureScript/Pretty/JS.hs
@@ -69,6 +69,7 @@
     , fmap (intercalate ", ") $ forM xs prettyPrintJS'
     , return " ]"
     ]
+  match (JSObjectLiteral []) = return "{}" 
   match (JSObjectLiteral ps) = fmap concat $ sequence
     [ return "{\n"
     , withIndent $ do
@@ -107,7 +108,7 @@
     , prettyPrintJS' sts
     ]
   match (JSFor ident start end sts) = fmap concat $ sequence
-    [ return $ "for (" ++ ident ++ " = "
+    [ return $ "for (var " ++ ident ++ " = "
     , prettyPrintJS' start
     , return $ "; " ++ ident ++ " < "
     , prettyPrintJS' end
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
@@ -31,6 +31,8 @@
 
 import Control.Applicative
 import Control.Monad.State
+import Control.Arrow ((***))
+
 import Data.Maybe (fromMaybe)
 import Data.List (nub)
 import Data.Generics (mkQ, everything)
@@ -50,6 +52,44 @@
 desugarModule :: Module -> Desugar Module
 desugarModule (Module name decls) = Module name <$> concat <$> mapM (desugarDecl (ModuleName name)) decls
 
+-- |
+-- Desugar type class and type class instance declarations
+--
+-- Type classes become type synonyms for their dictionaries, and type instances become dictionary declarations.
+-- Additional values are generated to access individual members of a dictionary, with the appropriate type.
+--
+-- E.g. the following
+--
+--   module Test where
+--
+--   class Foo a where
+--     foo :: a -> a
+--
+--   instance Foo String where
+--     foo s = s ++ s
+--
+--   instance (Foo a) => Foo [a] where
+--     foo = map foo
+--
+-- becomes
+--
+--   type Foo a = { foo :: a -> a }
+--
+--   foreign import foo "function foo(dict) {\
+--                      \  return dict.foo;\
+--                      \}" :: forall a. (Foo a) => a -> a
+--
+--   __Test_Foo_string_foo = (\s -> s ++ s) :: String -> String
+--
+--   __Test_Foo_string :: Foo String
+--   __Test_Foo_string = { foo: __Test_Foo_string_foo :: String -> String (unchecked) }
+--
+--   __Test_Foo_array_foo :: forall a. (Foo a) => [a] -> [a]
+--   __Test_Foo_array_foo _1 = map (foo _1)
+--
+--   __Test_Foo_array :: forall a. Foo a -> Foo [a]
+--   __Test_Foo_array _1 = { foo: __Test_Foo_array_foo _1 :: [a] -> [a] (unchecked) }
+--
 desugarDecl :: ModuleName -> Declaration -> Desugar [Declaration]
 desugarDecl mn d@(TypeClassDeclaration name arg members) = do
   let tys = map memberToNameAndType members
@@ -82,7 +122,7 @@
   m <- get
   (arg, instanceTys) <- lift $ maybe (Left $ "Type class " ++ show name ++ " is undefined. Type class names must be qualified.") Right
                         $ M.lookup (qualify mn name) m
-  let memberTypes = map (replaceTypeVars arg ty) instanceTys
+  let memberTypes = map (id *** replaceTypeVars arg ty) instanceTys
   entryName <- lift $ mkDictionaryValueName mn name ty
   memberNames <- mapM (memberToNameAndValue memberTypes) decls
   return $ ValueDeclaration entryName [] Nothing
@@ -118,13 +158,6 @@
 qualifiedToString :: ModuleName -> Qualified ProperName -> String
 qualifiedToString mn (Qualified Nothing pn) = qualifiedToString mn (Qualified (Just mn) pn)
 qualifiedToString _ (Qualified (Just (ModuleName mn)) pn) = runProperName mn ++ "_" ++ runProperName pn
-
-quantify :: Type -> Type
-quantify ty' = foldr (\arg t -> ForAll arg t Nothing) ty' tyVars
-  where
-  tyVars = nub $ everything (++) (mkQ [] collect) ty'
-  collect (TypeVar v) = [v]
-  collect _ = []
 
 -- |
 -- Generate a name for a type class dictionary, based on the module name, class name and type name
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
@@ -59,7 +59,9 @@
 -- Infer the kind of a single type
 --
 kindOf :: ModuleName -> Type -> Check Kind
-kindOf moduleName ty = fmap tidyUp . liftUnify $ starIfUnknown <$> infer ty
+kindOf moduleName ty =
+  rethrow (("Error checking kind of " ++ prettyPrintType ty ++ ":\n") ++) $
+    fmap tidyUp . liftUnify $ starIfUnknown <$> infer ty
   where
   tidyUp (k, sub) = sub $? k
 
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
@@ -67,7 +67,6 @@
 
 import qualified Data.Map as M
 import Data.Function (on)
-import Debug.Trace (trace)
 
 instance Partial Type where
   unknown = TUnknown
@@ -167,41 +166,73 @@
 typesOf :: ModuleName -> [(Ident, Value)] -> Check [(Ident, (Value, Type))]
 typesOf moduleName vals = do
   tys <- fmap tidyUp . liftUnify $ do
-    let es = map isTyped vals
-        typed = filter (isJust . snd . snd) es
-        untyped = filter (isNothing . snd . snd) es
-        typedDict = map (\(ident, (_, Just ty)) -> (ident, ty)) typed
+    let
+    -- Map each declaration to a name/value pair, with an optional type, if the declaration is typed
+      es = map isTyped vals
+    -- Filter the typed and untyped declarations
+      typed = filter (isJust . snd . snd) es
+      untyped = filter (isNothing . snd . snd) es
+    -- Make a map of names to typed declarations
+      typedDict = map (\(ident, (_, Just (ty, _))) -> (ident, ty)) typed
+    -- Create fresh unification variables for the types of untyped declarations
     untypedNames <- replicateM (length untyped) fresh
-    let untypedDict = zip (map fst untyped) untypedNames
-        dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ (map (id *** fst) typedDict) ++ untypedDict)
-    forM es $ \e -> do
+    let
+    -- Make a map of names to the unification variables of untyped declarations
+      untypedDict = zip (map fst untyped) untypedNames
+    -- Create the dictionary of all name/type pairs, which will be added to the environment during type checking
+      dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ typedDict ++ untypedDict)
+    forM es $ \e@(_, (val, _)) -> do
+      -- If the declaration is a function, it has access to other values in the binding group.
+      -- If not, the generated code might fail at runtime since those values might be undefined.
+      let dict' = if isFunction val then dict else M.empty
       triple@(_, (val, ty)) <- case e of
+        -- Typed declarations
         (ident, (val, Just (ty, checkType))) -> do
+          -- Kind check
           kind <- liftCheck $ kindOf moduleName ty
           guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+          -- Check the type with the new names in scope
           ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms $ ty
-          val' <- bindNames dict $ if checkType
+          val' <- bindNames dict' $ if checkType
                                    then TypedValue True <$> check val ty' <*> pure ty'
                                    else return (TypedValue False val ty')
           return (ident, (val', ty'))
+        -- Untyped declarations
         (ident, (val, Nothing)) -> do
-          TypedValue _ val' ty <- bindNames dict $ infer val
+          -- Infer the type with the new names in scope
+          TypedValue _ val' ty <- bindNames dict' $ infer val
           ty =?= fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
           return (ident, (TypedValue True val' ty, ty))
+      -- If run-main is enabled, need to check that Main.main has type Eff eff a for some eff, a
       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
+      -- Make sure unification variables do not escape
       escapeCheck val ty
       return triple
   forM tys $ \(ident, (val, ty)) -> do
+    -- Replace type class dictionary placeholders with actual dictionaries
     val' <- replaceTypeClassDictionaries moduleName val
-    rethrow (("Error in " ++ show ident ++ ": \n") ++) $ skolemEscapeCheck val'
-    return $ (ident, (overTypes (desaturateAllTypeSynonyms . setifyAll) $ val'
-                   , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))
+    -- Check skolem variables did not escape their scope
+    skolemEscapeCheck val'
+    -- Remove type synonyms placeholders, remove duplicate row fields, and replace
+    -- top-level unification variables with named type variables.
+    let val'' = overTypes (desaturateAllTypeSynonyms . setifyAll) val'
+        ty' = varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty
+    return $ (ident, (val'', ty'))
   where
+  -- Apply the substitution that was returned from runUnify to both types and (type-annotated) values
   tidyUp (ts, sub) = map (\(i, (val, ty)) -> (i, (overTypes (sub $?) val, sub $? ty))) ts
 
 -- |
+-- Check if a value introduces a function
+--
+isFunction :: Value -> Bool
+isFunction (Abs _ _) = True
+isFunction (TypedValue _ val _) = isFunction val
+isFunction _ = False
+
+-- |
 -- Check if a value contains a type annotation
 --
 isTyped :: (Ident, Value) -> (Ident, (Value, Maybe (Type, Bool)))
@@ -237,22 +268,33 @@
   go env (className', ty') =
     [ mkDictionary (canonicalizeDictionary tcd) args
     | tcd <- context
+    -- Choose type class dictionaries in scope in the current module
     , filterModule tcd
+    -- Make sure the type class name matches the one we are trying to satisfy
     , typeConstructorsAreEqual env moduleName className' (tcdClassName tcd)
+    -- Make sure the type unifies with the type in the type instance definition
     , subst <- maybeToList $ typeHeadsAreEqual moduleName env ty' (tcdInstanceType tcd)
+    -- Solve any necessary subgoals
     , args <- solveSubgoals env subst (tcdDependencies tcd) ]
+  -- Create dictionaries for subgoals which still need to be solved by calling go recursively
+  -- E.g. the goal (Show a, Show b) => Show (Either a b) can be satisfied if the current type
+  -- unifies with Either a b, and we can satisfy the subgoals Show a and Show b recursively.
   solveSubgoals :: Environment -> [(String, Type)] -> Maybe [(Qualified ProperName, Type)] -> [Maybe [Value]]
   solveSubgoals _ _ Nothing = return Nothing
   solveSubgoals env subst (Just subgoals) = do
-    dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
+    dict <- mapM (go env) (map (id *** replaceAllTypeVars subst) subgoals)
     return $ Just dict
+  -- Make a dictionary from subgoal dictionaries by applying the correct function
   mkDictionary :: Qualified Ident -> Maybe [Value] -> Value
   mkDictionary fnName Nothing = Var fnName
   mkDictionary fnName (Just dicts) = foldl App (Var fnName) dicts
+  -- Filter out type dictionaries which are in scope in the current module
   filterModule :: TypeClassDictionaryInScope -> Bool
   filterModule (TypeClassDictionaryInScope { tcdName = Qualified (Just mn) _ }) | mn == moduleName = True
   filterModule (TypeClassDictionaryInScope { tcdName = Qualified Nothing _ }) = True
   filterModule _ = False
+  -- Resolve a type class dictionary in scope to an actual value by following any (TCDAlias) pointers
+  -- which originated from module imports
   canonicalizeDictionary :: TypeClassDictionaryInScope -> Qualified Ident
   canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDRegular, tcdName = nm }) = nm
   canonicalizeDictionary (TypeClassDictionaryInScope { tcdType = TCDAlias nm }) = nm
@@ -268,6 +310,9 @@
 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
+typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e m name args of
+  Left err -> Nothing
+  Right t1 -> typeHeadsAreEqual m e t1 t2
 typeHeadsAreEqual _ _ _ _ = Nothing
 
 -- |
@@ -297,6 +342,12 @@
 skolemEscapeCheck :: Value -> Check ()
 skolemEscapeCheck (TypedValue False _ _) = return ()
 skolemEscapeCheck root@(TypedValue _ _ _) =
+  -- Every skolem variable is created when a ForAll type is skolemized.
+  -- This determines the scope of that skolem variable, which is copied from the SkolemScope
+  -- field of the ForAll constructor.
+  -- We traverse the tree top-down, and collect any SkolemScopes introduced by ForAlls.
+  -- If a Skolem is encountered whose SkolemScope is not in the current list, we have found
+  -- an escaped skolem variable.
   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
@@ -348,12 +399,16 @@
 -- |
 -- Replace named type variables with types
 --
-replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
+replaceAllTypeVars :: [(String, Type)] -> Type -> Type
 replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
 
 -- |
--- Replace named type variables with new unification variables
+-- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
+-- or TypeClassDictionary values.
 --
+-- This is necessary during type checking to avoid unifying a polymorphic type with a
+-- unification variable.
+--
 instantiatePolyTypeWithUnknowns :: Value -> Type -> UnifyT Type Check (Value, Type)
 instantiatePolyTypeWithUnknowns val (ForAll ident ty _) = do
   ty' <- replaceVarWithUnknown ident ty
@@ -378,12 +433,18 @@
 -- Replace fully applied type synonyms with the @SaturatedTypeSynonym@ data constructor, which helps generate
 -- better error messages during unification.
 --
-replaceAllTypeSynonyms :: (Functor m, MonadState CheckState m, MonadError String m) => (D.Data d) => d -> m d
+replaceAllTypeSynonyms' :: (D.Data d) => Environment -> ModuleName -> d -> Either String d
+replaceAllTypeSynonyms' env moduleName d =
+  let
+    syns = map (\((path, name), (args, _)) -> ((path, name), length args)) . M.toList $ typeSynonyms env
+  in
+    saturateAllTypeSynonyms env moduleName syns d
+
+replaceAllTypeSynonyms :: (Functor m, Monad m, MonadState CheckState m, MonadError String m) => (D.Data d) => d -> m d
 replaceAllTypeSynonyms d = do
   env <- getEnv
   Just moduleName <- checkCurrentModule <$> get
-  let syns = map (\((path, name), (args, _)) -> ((path, name), length args)) . M.toList $ typeSynonyms env
-  either throwError return $ saturateAllTypeSynonyms env moduleName syns d
+  either throwError return $ replaceAllTypeSynonyms' env moduleName d
 
 -- |
 -- \"Desaturate\" @SaturatedTypeSynonym@s
@@ -397,13 +458,19 @@
 -- |
 -- Replace a type synonym and its arguments with the aliased type
 --
-expandTypeSynonym :: Qualified ProperName -> [Type] -> UnifyT Type Check Type
+expandTypeSynonym' :: Environment -> ModuleName -> Qualified ProperName -> [Type] -> Either String Type
+expandTypeSynonym' env moduleName name args =
+  case M.lookup (canonicalizeType moduleName env name) (typeSynonyms env) of
+    Just (synArgs, body) -> do
+      let repl = replaceAllTypeVars (zip synArgs args) body
+      replaceAllTypeSynonyms' env moduleName repl
+    Nothing -> error "Type synonym was not defined"
+
+expandTypeSynonym :: (Functor m, Monad m, MonadState CheckState m, MonadError String m) => Qualified ProperName -> [Type] -> m Type
 expandTypeSynonym name args = do
   env <- getEnv
   Just moduleName <- checkCurrentModule <$> get
-  case M.lookup (canonicalizeType moduleName env name) (typeSynonyms env) of
-    Just (synArgs, body) -> return $ replaceAllTypeVars (zip synArgs args) body
-    Nothing -> error "Type synonym was not defined"
+  either throwError return $ expandTypeSynonym' env moduleName name args
 
 -- |
 -- Ensure a set of property names and value does not contain duplicate labels
@@ -693,8 +760,8 @@
 -- |
 -- Skolemize a type variable by replacing its instances with fresh skolem constants
 --
-skolemize :: (D.Data d) => String -> Int -> SkolemScope -> d -> d
-skolemize ident sko scope d = replaceTypeVars ident (Skolem sko scope) d
+skolemize :: String -> Int -> SkolemScope -> Type -> Type
+skolemize ident sko scope = replaceTypeVars ident (Skolem sko scope)
 
 -- |
 -- Introduce skolem scope at every occurence of a ForAll
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,9 +18,11 @@
 module Language.PureScript.Types where
 
 import Data.Data
-import Data.Generics (mkT, mkQ, everywhereBut)
+import Data.List (nub)
+import Data.Generics (everything, mkT, mkQ, everywhereBut)
 
 import Control.Monad.Unify
+import Control.Arrow ((***))
 
 import Language.PureScript.Names
 
@@ -159,10 +161,57 @@
 -- |
 -- Replace a type variable, taking into account variable shadowing
 --
-replaceTypeVars :: (Data d) => String -> Type -> d -> d
-replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replaceTypeVar)
+replaceTypeVars :: String -> Type -> Type -> Type
+replaceTypeVars = replaceTypeVars' []
   where
-  replaceTypeVar (TypeVar v) | v == name = t
-  replaceTypeVar other = other
-  isShadowed (ForAll v _ _) | v == name = True
-  isShadowed _ = False
+  replaceTypeVars' bound name replacement = go bound
+    where
+    go :: [String] -> Type -> Type
+    go bs (Object r) = Object $ go bs r
+    go bs (TypeVar v) | v == name = replacement
+    go bs (TypeApp t1 t2) = TypeApp (go bs t1) (go bs t2)
+    go bs (SaturatedTypeSynonym name ts) = SaturatedTypeSynonym name $ map (go bs) ts
+    go bs f@(ForAll v t sco) | v == name = f
+                             | v `elem` usedTypeVariables replacement =
+                                 let v' = genName v (name : bs ++ usedTypeVariables replacement)
+                                     t' = replaceTypeVars' bs v (TypeVar v') t
+                                 in ForAll v' (go (v' : bs) t') sco
+                             | otherwise = ForAll v (go (v : bs) t) sco
+    go bs (ConstrainedType cs t) = ConstrainedType (map (id *** go bs) cs) (go bs t)
+    go bs (RCons name t r) = RCons name (go bs t) (go bs r)
+    go _ ty = ty
+  genName orig inUse = try 0
+    where
+    try n | (orig ++ show n) `elem` inUse = try (n + 1)
+          | otherwise = orig ++ show n
+
+-- |
+-- Collect all type variables appearing in a type
+--
+usedTypeVariables :: Type -> [String]
+usedTypeVariables = nub . everything (++) (mkQ [] go)
+  where
+  go (TypeVar v) = [v]
+  go _ = []
+
+-- |
+-- Collect all free type variables appearing in a type
+--
+freeTypeVariables :: Type -> [String]
+freeTypeVariables = nub . go []
+  where
+  go :: [String] -> Type -> [String]
+  go bound (Object r) = go bound r
+  go bound (TypeVar v) | v `notElem` bound = [v]
+  go bound (TypeApp t1 t2) = go bound t1 ++ go bound t2
+  go bound (SaturatedTypeSynonym _ ts) = concatMap (go bound) ts
+  go bound (ForAll v t _) = go (v : bound) t
+  go bound (ConstrainedType cs t) = concatMap (go bound . snd) cs ++ go bound t
+  go bound (RCons _ t r) = go bound t ++ go bound r
+  go _ _ = []
+
+-- |
+-- Universally quantify over all type variables appearing free in a type
+--
+quantify :: Type -> Type
+quantify ty = foldr (\arg t -> ForAll arg t Nothing) ty $ freeTypeVariables ty