diff --git a/examples/passing/Operators.purs b/examples/passing/Operators.purs
--- a/examples/passing/Operators.purs
+++ b/examples/passing/Operators.purs
@@ -73,6 +73,11 @@
   test19 :: Number
   test19 = negate $ negate (-1)
 
+  test20 :: Number
+  test20 = 1 @ 2
+    where
+    (@) x y = x + y * y
+
   main = do
     let t1 = test1 1 2 (\x y -> x + y)
     let t2 = test2
@@ -93,4 +98,5 @@
     let t17 = test17
     let t18 = test18
     let t19 = test19
+    let t20 = test20
     trace "Done"
diff --git a/examples/passing/RowPolyInstanceContext.purs b/examples/passing/RowPolyInstanceContext.purs
new file mode 100644
--- /dev/null
+++ b/examples/passing/RowPolyInstanceContext.purs
@@ -0,0 +1,20 @@
+module Main where
+
+class T s m where
+  state :: (s -> s) -> m Unit
+
+data S s a = S (s -> { new :: s, ret :: a })
+
+instance st :: T s (S s) where
+  state f = S $ \s -> { new: f s, ret: unit }
+
+test1 :: forall r . S { foo :: String | r } Unit
+test1 = state $ \o -> o { foo = o.foo ++ "!" }
+
+test2 :: forall m r . (T { foo :: String | r } m) => m Unit
+test2 = state $ \o -> o { foo = o.foo ++ "!" }
+
+main = do
+  let t1 = test1
+  let t2 = test2
+  Debug.Trace.trace "Done"
diff --git a/examples/passing/ScopedTypeVariables.purs b/examples/passing/ScopedTypeVariables.purs
new file mode 100644
--- /dev/null
+++ b/examples/passing/ScopedTypeVariables.purs
@@ -0,0 +1,34 @@
+module Main where
+
+test1 :: forall a. (a -> a) -> a -> a
+test1 f x = g (g x)
+  where
+  g :: a -> a
+  g y = f (f y)
+
+test2 :: forall a. (a -> a) -> a -> a
+test2 = h
+  where
+  h :: forall b. (b -> b) -> b -> b
+  h f x = g (g x)
+    where
+    g :: b -> b
+    g y = f (f y)
+
+test3 :: Number 
+test3 = ((\b -> b :: b) :: forall b. b -> b) 0
+
+test4 :: forall a. (a -> a) -> a -> a
+test4 = h
+  where
+  h :: forall b. (b -> b) -> b -> b
+  h f x = g (g x)
+    where
+    g :: b -> b
+    g y = j (f (f y))
+      where
+      j :: forall b. b -> b
+      j x = x
+
+
+main = Debug.Trace.trace "Done"
diff --git a/examples/passing/UnknownInInstance.purs b/examples/passing/UnknownInInstance.purs
new file mode 100644
--- /dev/null
+++ b/examples/passing/UnknownInInstance.purs
@@ -0,0 +1,8 @@
+module Main where
+
+data Proxy a = Proxy
+
+test :: forall a. (Show (Proxy a)) => String
+test = show Proxy
+
+main = Debug.Trace.trace "Done"
diff --git a/prelude/prelude.purs b/prelude/prelude.purs
--- a/prelude/prelude.purs
+++ b/prelude/prelude.purs
@@ -24,15 +24,32 @@
   , Unit(..), unit
   ) where
 
+  -- | An alias for `true`, which can be useful in guard clauses: 
+  -- | 
+  -- | E.g.
+  -- | 
+  -- |     max x y | x >= y = x 
+  -- |             | otherwise = y
   otherwise :: Boolean
   otherwise = true
 
+  -- | Flips the order of the arguments to a function of two arguments. 
   flip :: forall a b c. (a -> b -> c) -> b -> a -> c
   flip f b a = f a b
 
+  -- | Returns its first argument and ignores its second. 
   const :: forall a b. a -> b -> a
   const a _ = a
 
+  -- | This function returns its first argument, and can be used to assert type equalities.
+  -- | This can be useful when types are otherwise ambiguous. 
+  -- | 
+  -- | E.g.
+  -- | 
+  -- |     main = print $ [] `asTypeOf` [0]
+  -- |
+  -- | If instead, we had written `main = print []`, the type of the argument `[]` would have
+  -- | been ambiguous, resulting in a compile-time error.
   asTypeOf :: forall a. a -> a -> a
   asTypeOf x _ = x
 
diff --git a/psc-docs/Main.hs b/psc-docs/Main.hs
--- a/psc-docs/Main.hs
+++ b/psc-docs/Main.hs
@@ -22,6 +22,7 @@
 import Data.List
 import Data.Maybe (fromMaybe)
 import Data.Version (showVersion)
+import Data.Foldable (traverse_)
 
 import Options.Applicative
 
@@ -30,13 +31,11 @@
 import System.Exit (exitSuccess, exitFailure)
 import System.IO (hPutStrLn, stderr)
 
-
 data PSCDocsOptions = PSCDocsOptions
   { pscdIncludeHeir :: Bool
   , pscdInputFiles  :: [FilePath]
   }
 
-
 docgen :: PSCDocsOptions -> IO ()
 docgen (PSCDocsOptions showHierarchy input) = do
   e <- P.parseModulesFromFiles (fromMaybe "") <$> mapM (fmap (first Just) . parseFile) (nub input)
@@ -62,11 +61,17 @@
 headerLevel :: Int -> String -> Docs
 headerLevel level hdr = tell [replicate level '#' ++ ' ' : hdr]
 
+withIndent :: Int -> Docs -> Docs
+withIndent indent = censor (map (replicate indent ' ' ++ ))
+
 atIndent :: Int -> String -> Docs
 atIndent indent text =
   let ls = lines text in
-  forM_ ls $ \l -> tell [replicate indent ' ' ++ l]
+  withIndent indent (tell ls)
 
+ticks :: String -> String
+ticks = ("`" ++) . (++ "`")
+
 renderModules :: Bool -> [P.Module] -> Docs
 renderModules showHierarchy ms = do
   headerLevel 1 "Module Documentation"
@@ -109,61 +114,91 @@
 
 renderTopLevel :: Maybe [P.DeclarationRef] -> [P.Declaration] -> Docs
 renderTopLevel exps decls = forM_ (sortBy (compare `on` getName) decls) $ \decl -> do
-  renderDeclaration 4 exps decl
+  traverse_ (headerLevel 4) (ticks `fmap` getDeclarationTitle decl)
   spacer
+  renderDeclaration exps decl
+  spacer
 
 renderTypeclassImage :: P.ModuleName -> Docs
 renderTypeclassImage name =
   let name' = P.runModuleName name
   in tell ["![" ++ name' ++ "](images/" ++ name' ++ ".png)"]
 
-renderDeclaration :: Int -> Maybe [P.DeclarationRef] -> P.Declaration -> Docs
-renderDeclaration n _ (P.TypeDeclaration ident ty) =
-  atIndent n $ show ident ++ " :: " ++ prettyPrintType' ty
-renderDeclaration n _ (P.ExternDeclaration _ ident _ ty) =
-  atIndent n $ show ident ++ " :: " ++ prettyPrintType' ty
-renderDeclaration n exps (P.DataDeclaration dtype name args ctors) = do
+getDeclarationTitle :: P.Declaration -> Maybe String
+getDeclarationTitle (P.TypeDeclaration name _)                      = Just (show name)
+getDeclarationTitle (P.ExternDeclaration _ name _ _)                = Just (show name)
+getDeclarationTitle (P.DataDeclaration _ name _ _)                  = Just (show name)
+getDeclarationTitle (P.ExternDataDeclaration name _)                = Just (show name)
+getDeclarationTitle (P.TypeSynonymDeclaration name _ _)             = Just (show name)
+getDeclarationTitle (P.TypeClassDeclaration name _ _ _)   = Just (show name)
+getDeclarationTitle (P.TypeInstanceDeclaration name _ _ _ _)        = Just (show name)
+getDeclarationTitle (P.PositionedDeclaration _ _ d)                 = getDeclarationTitle d
+getDeclarationTitle _                                               = Nothing
+
+renderDeclaration :: Maybe [P.DeclarationRef] -> P.Declaration -> Docs
+renderDeclaration _ (P.TypeDeclaration ident ty) =
+  atIndent 4 $ show ident ++ " :: " ++ prettyPrintType' ty
+renderDeclaration _ (P.ExternDeclaration _ ident _ ty) =
+  atIndent 4 $ show ident ++ " :: " ++ prettyPrintType' ty
+renderDeclaration exps (P.DataDeclaration dtype name args ctors) = do
   let
     typeApp  = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)
     typeName = prettyPrintType' typeApp
     exported = filter (P.isDctorExported name exps . fst) ctors
-  atIndent n $ show dtype ++ " " ++ typeName ++ (if null exported then "" else " where")
-  forM_ exported $ \(ctor, tys) ->
-    let ctorTy = foldr P.function typeApp tys
-    in atIndent (n + 2) $ P.runProperName ctor ++ " :: " ++ prettyPrintType' ctorTy
-renderDeclaration n _ (P.ExternDataDeclaration name kind) =
-  atIndent n $ "data " ++ P.runProperName name ++ " :: " ++ P.prettyPrintKind kind
-renderDeclaration n _ (P.TypeSynonymDeclaration name args ty) = do
+  atIndent 4 $ show dtype ++ " " ++ typeName
+  zipWithM_ (\isFirst (ctor, tys) ->
+              atIndent 6 $ (if isFirst then "= " else "| ") ++ P.runProperName ctor ++ " " ++ unwords (map P.prettyPrintTypeAtom tys))
+            (True : repeat False) exported
+renderDeclaration _ (P.ExternDataDeclaration name kind) =
+  atIndent 4 $ "data " ++ P.runProperName name ++ " :: " ++ P.prettyPrintKind kind
+renderDeclaration _ (P.TypeSynonymDeclaration name args ty) = do
   let
     typeApp  = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)
     typeName = prettyPrintType' typeApp
-  atIndent n $ "type " ++ typeName ++ " = " ++ prettyPrintType' ty
-renderDeclaration n exps (P.TypeClassDeclaration name args implies ds) = do
+  atIndent 4 $ "type " ++ typeName ++ " = " ++ prettyPrintType' ty
+renderDeclaration _ (P.TypeClassDeclaration name args implies ds) = do
   let impliesText = case implies of
                       [] -> ""
                       is -> "(" ++ intercalate ", " (map (\(pn, tys') -> show pn ++ " " ++ unwords (map P.prettyPrintTypeAtom tys')) is) ++ ") <= "
       classApp  = foldl P.TypeApp (P.TypeConstructor (P.Qualified Nothing name)) (map toTypeVar args)
       className = prettyPrintType' classApp
-  atIndent n $ "class " ++ impliesText ++ className ++ " where"
-  mapM_ (renderDeclaration (n + 2) exps) ds
-renderDeclaration n _ (P.TypeInstanceDeclaration name constraints className tys _) = do
+  atIndent 4 $ "class " ++ impliesText ++ className ++ " where"
+  mapM_ renderClassMember ds
+  where
+    renderClassMember (P.PositionedDeclaration _ _ d) = renderClassMember d
+    renderClassMember (P.TypeDeclaration ident ty) = atIndent 6 $ show ident ++ " :: " ++ prettyPrintType' ty
+    renderClassMember _ = error "Invalid argument to renderClassMember."
+renderDeclaration _ (P.TypeInstanceDeclaration name constraints className tys _) = do
   let constraintsText = case constraints of
                           [] -> ""
                           cs -> "(" ++ intercalate ", " (map (\(pn, tys') -> show pn ++ " " ++ unwords (map P.prettyPrintTypeAtom tys')) cs) ++ ") => "
-  atIndent n $ "instance " ++ show name ++ " :: " ++ constraintsText ++ show className ++ " " ++ unwords (map P.prettyPrintTypeAtom tys)
-renderDeclaration n exps (P.PositionedDeclaration _ com d) = do
-  renderComments n com
-  spacer
-  renderDeclaration n exps d
-renderDeclaration _ _ _ = return ()
+  atIndent 4 $ "instance " ++ show name ++ " :: " ++ constraintsText ++ show className ++ " " ++ unwords (map P.prettyPrintTypeAtom tys)
+renderDeclaration exps (P.PositionedDeclaration _ com d) = do
+  renderComments com
+  renderDeclaration exps d
+renderDeclaration _ _ = return ()
 
-renderComments :: Int -> [P.Comment] -> Docs
-renderComments n cs = mapM_ (atIndent n) ls
+renderComments :: [P.Comment] -> Docs
+renderComments cs = do
+  let raw = concatMap toLines cs
+  
+  if all hasPipe raw
+    then atIndent 0 . unlines . map stripPipes $ raw
+    else atIndent 4 $ unlines raw
+  
+  unless (null raw) spacer
   where
-  ls = concatMap toLines cs
 
   toLines (P.LineComment s) = [s]
   toLines (P.BlockComment s) = lines s
+  
+  hasPipe s = case dropWhile (== ' ') s of { ('|':_) -> True; _ -> False }
+  
+  stripPipes = dropPipe . dropWhile (== ' ')
+
+  dropPipe ('|':' ':s) = s
+  dropPipe ('|':s) = s
+  dropPipe s = s
 
 toTypeVar :: (String, Maybe P.Kind) -> P.Type
 toTypeVar (s, Nothing) = P.TypeVar s
diff --git a/psci/Commands.hs b/psci/Commands.hs
--- a/psci/Commands.hs
+++ b/psci/Commands.hs
@@ -52,7 +52,7 @@
   -- |
   -- Binds a value to a name
   --
-  | Let (Expr -> Expr)
+  | Let [Declaration]
   -- |
   -- Find the type of an expression
   --
diff --git a/psci/Main.hs b/psci/Main.hs
--- a/psci/Main.hs
+++ b/psci/Main.hs
@@ -69,7 +69,7 @@
   { psciImportedFilenames   :: [FilePath]
   , psciImportedModuleNames :: [P.ModuleName]
   , psciLoadedModules       :: [(Either P.RebuildPolicy FilePath, P.Module)]
-  , psciLetBindings         :: [P.Expr -> P.Expr]
+  , psciLetBindings         :: [P.Declaration]
   }
 
 -- State helpers
@@ -95,8 +95,8 @@
 -- |
 -- Updates the state to have more let bindings.
 --
-updateLets :: (P.Expr -> P.Expr) -> PSCiState -> PSCiState
-updateLets name st = st { psciLetBindings = name : psciLetBindings st }
+updateLets :: [P.Declaration] -> PSCiState -> PSCiState
+updateLets ds st = st { psciLetBindings = ds ++ psciLetBindings st }
 
 -- File helpers
 -- |
@@ -141,6 +141,16 @@
     return (Right filename, content)
   return $ P.parseModulesFromFiles (either (const "") id) $ (Left P.RebuildNever, P.prelude) : filesAndContent
 
+-- |
+-- Load all modules, updating the application state
+--
+loadAllImportedModules :: PSCI ()
+loadAllImportedModules = do
+  files <- PSCI . lift $ fmap psciImportedFilenames get
+  modulesOrFirstError <- psciIO $ loadAllModules files
+  case modulesOrFirstError of
+    Left err -> psciIO $ print err
+    Right modules -> PSCI . lift . modify $ \st -> st { psciLoadedModules = modules } 
 
 -- |
 -- Expands tilde in path.
@@ -348,14 +358,14 @@
     importDecl m = P.ImportDeclaration m P.Unqualified Nothing
     traceModule = P.ModuleName [P.ProperName "Debug", P.ProperName "Trace"]
     trace = P.Var (P.Qualified (Just traceModule) (P.Ident "print"))
-    itValue = foldl (\x f -> f x) val lets
     mainValue = P.App trace (P.Var (P.Qualified Nothing (P.Ident "it")))
-    itDecl = P.ValueDeclaration (P.Ident "it") P.Value [] $ Right itValue
+    itDecl = P.ValueDeclaration (P.Ident "it") P.Value [] $ Right val
     mainDecl = P.ValueDeclaration (P.Ident "main") P.Value [] $ Right mainValue
     decls = if exec then [itDecl, mainDecl] else [itDecl]
   in
-    P.Module moduleName ((importDecl `map` imports) ++ decls) Nothing
+    P.Module moduleName ((importDecl `map` imports) ++ lets ++ decls) Nothing
 
+
 -- |
 -- Makes a volatile module to hold a non-qualified type synonym for a fully-qualified data type declaration.
 --
@@ -408,10 +418,10 @@
 -- Takes a let declaration and updates the environment, then run a make. If the declaration fails,
 -- restore the pre-let environment.
 --
-handleLet :: (P.Expr -> P.Expr) -> PSCI ()
-handleLet l = do
+handleLet :: [P.Declaration] -> PSCI ()
+handleLet ds = do
   st <- PSCI $ lift get
-  let st' = updateLets l st
+  let st' = updateLets ds st
   let m = createTemporaryModule False st' (P.ObjectLiteral [])
   e <- psciIO . runMake $ P.make modulesDir options (psciLoadedModules st' ++ [(Left P.RebuildAlways, m)]) []
   case e of
@@ -561,10 +571,12 @@
     PSCI . outputStrLn $ "Couldn't locate: " ++ filePath
 handleCommand Reset = do
   files <- psciImportedFilenames <$> PSCI (lift get)
-  modulesOrFirstError <- psciIO $ loadAllModules files
-  case modulesOrFirstError of
-    Left err -> psciIO $ print err >> exitFailure
-    Right modules -> PSCI . lift $ put (PSCiState files defaultImports modules [])
+  PSCI . lift . modify $ \st -> st 
+    { psciImportedFilenames   = files
+    , psciImportedModuleNames = defaultImports
+    , psciLetBindings         = []
+    }
+  loadAllImportedModules
 handleCommand (TypeOf val) = handleTypeOf val
 handleCommand (KindOf typ) = handleKindOf typ
 handleCommand (Browse moduleName) = handleBrowse moduleName
@@ -609,7 +621,7 @@
             Left err -> outputStrLn err >> go
             Right Nothing -> go
             Right (Just Quit) -> outputStrLn quitMessage
-            Right (Just c') -> runPSCI (handleCommand c') >> go
+            Right (Just c') -> runPSCI (loadAllImportedModules >> handleCommand c') >> go
 
 singleLineFlag :: Parser Bool
 singleLineFlag = switch $
diff --git a/psci/Parser.hs b/psci/Parser.hs
--- a/psci/Parser.hs
+++ b/psci/Parser.hs
@@ -76,7 +76,7 @@
   -- we actually want the normal @let@.
   --
   psciLet :: P.TokenParser Command
-  psciLet = Let <$> (P.Let <$> (P.reserved "let" *> P.indented *> manyDecls))
+  psciLet = Let <$> (P.reserved "let" *> P.indented *> manyDecls)
     where
     manyDecls :: P.TokenParser [P.Declaration]
     manyDecls = C.mark (many1 (C.same *> P.parseDeclaration))
diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.6.6
+version: 0.6.7
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
diff --git a/src/Language/PureScript/CodeGen/JS/Common.hs b/src/Language/PureScript/CodeGen/JS/Common.hs
--- a/src/Language/PureScript/CodeGen/JS/Common.hs
+++ b/src/Language/PureScript/CodeGen/JS/Common.hs
@@ -135,7 +135,47 @@
               , "volatile"
               , "while"
               , "with"
-              , "yield" ]
+              , "yield" ] || properNameIsJsReserved name
 
 moduleNameToJs :: ModuleName -> String
-moduleNameToJs (ModuleName pns) = intercalate "_" (runProperName `map` pns)
+moduleNameToJs (ModuleName pns) =
+  let name = intercalate "_" (runProperName `map` pns)
+  in if properNameIsJsReserved name then "$$" ++ name else name
+
+-- |
+-- Checks whether a proper name is reserved in Javascript.
+--
+properNameIsJsReserved :: String -> Bool
+properNameIsJsReserved name =
+  name `elem` [ "Infinity"
+              , "NaN"
+              , "Object"
+              , "Function"
+              , "Boolean"
+              , "Error"
+              , "EvalError"
+              , "InternalError"
+              , "RangeError"
+              , "ReferenceError"
+              , "SyntaxError"
+              , "TypeError"
+              , "URIError"
+              , "Number"
+              , "Math"
+              , "Date"
+              , "String"
+              , "RegExp"
+              , "Array"
+              , "Int8Array"
+              , "Uint8Array"
+              , "Uint8ClampedArray"
+              , "Int16Array"
+              , "Uint16Array"
+              , "Int32Array"
+              , "Uint32Array"
+              , "Float32Array"
+              , "Float64Array"
+              , "ArrayBuffer"
+              , "DataView"
+              , "JSON"
+              , "Intl" ]
diff --git a/src/Language/PureScript/Environment.hs b/src/Language/PureScript/Environment.hs
--- a/src/Language/PureScript/Environment.hs
+++ b/src/Language/PureScript/Environment.hs
@@ -136,7 +136,12 @@
   -- |
   -- A local type variable
   --
-  | LocalTypeVariable deriving (Show, Eq, Data, Typeable)
+  | LocalTypeVariable
+  -- |
+  -- A scoped type variable
+  --
+  | ScopedTypeVar
+   deriving (Show, Eq, Data, Typeable)
 
 -- |
 -- The type ('data' or 'newtype') of a data type declaration
diff --git a/src/Language/PureScript/Parser/Lexer.hs b/src/Language/PureScript/Parser/Lexer.hs
--- a/src/Language/PureScript/Parser/Lexer.hs
+++ b/src/Language/PureScript/Parser/Lexer.hs
@@ -422,6 +422,7 @@
   go (Symbol s) = Just s
   go Colon      = Just ":"
   go LFatArrow  = Just "<="
+  go At         = Just "@"
   go _ = Nothing
 
 symbol' :: String -> TokenParser ()
diff --git a/src/Language/PureScript/TypeChecker/Entailment.hs b/src/Language/PureScript/TypeChecker/Entailment.hs
--- a/src/Language/PureScript/TypeChecker/Entailment.hs
+++ b/src/Language/PureScript/TypeChecker/Entailment.hs
@@ -20,6 +20,7 @@
 import Data.Function (on)
 import Data.List
 import Data.Maybe (maybeToList)
+import Data.Foldable (foldMap)
 import qualified Data.Map as M
 
 import Control.Applicative
@@ -199,13 +200,35 @@
 -- 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 _ _ t (TypeVar v) = Just [(v, t)]
+typeHeadsAreEqual _ _ (Skolem _ s1 _)      (Skolem _ s2 _)      | s1 == s2 = Just []
+typeHeadsAreEqual _ _ t                    (TypeVar v)                     = Just [(v, t)]
+-- In this case, we might want type information to flow back to the typechecker.
+-- TODO: run this function in the UnifyT monad.
+typeHeadsAreEqual _ _ (TUnknown _)         _                    = Just []
 typeHeadsAreEqual _ _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = Just []
-typeHeadsAreEqual m e (TypeApp h1 t1) (TypeApp h2 t2) = (++) <$> typeHeadsAreEqual m e h1 h2 <*> typeHeadsAreEqual m e t1 t2
+typeHeadsAreEqual m e (TypeApp h1 t1)      (TypeApp h2 t2)                 = (++) <$> typeHeadsAreEqual m e h1 h2 
+                                                                                  <*> typeHeadsAreEqual m e t1 t2
 typeHeadsAreEqual m e (SaturatedTypeSynonym name args) t2 = case expandTypeSynonym' e name args of
   Left  _  -> Nothing
   Right t1 -> typeHeadsAreEqual m e t1 t2
+typeHeadsAreEqual _ _ REmpty REmpty = Just []
+typeHeadsAreEqual m e r1@(RCons _ _ _) r2@(RCons _ _ _) =
+  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 (++) <$> foldMap (\(t1, t2) -> typeHeadsAreEqual m e t1 t2) int 
+          <*> go sd1 r1' sd2 r2'
+  where
+  go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Maybe [(String, Type)]
+  go [] REmpty          [] REmpty          = Just [] 
+  go [] (TUnknown _)    _  _               = Just [] 
+  go [] (TypeVar v1)    [] (TypeVar v2)    | v1 == v2 = Just []
+  go [] (Skolem _ s1 _) [] (Skolem _ s2 _) | s1 == s2 = Just []
+  go sd r               [] (TypeVar v)     = Just [(v, rowFromList (sd, r))]
+  go _  _               _  _               = Nothing
 typeHeadsAreEqual _ _ _ _ = Nothing
 
 -- |
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
@@ -14,19 +14,22 @@
 -----------------------------------------------------------------------------
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, TupleSections #-}
 
 module Language.PureScript.TypeChecker.Kinds (
     kindOf,
+    kindOfWithScopedVars,
     kindsOf,
     kindsOfAll
 ) where
 
 import Data.Maybe (fromMaybe)
 import Data.Monoid ((<>))
+
 import qualified Data.HashMap.Strict as H
 import qualified Data.Map as M
 
+import Control.Arrow (second)
 import Control.Applicative
 import Control.Monad.Error
 import Control.Monad.State
@@ -69,11 +72,19 @@
 -- Infer the kind of a single type
 --
 kindOf :: ModuleName -> Type -> Check Kind
-kindOf _ ty =
+kindOf _ ty = fst <$> kindOfWithScopedVars ty
+    
+-- |
+-- Infer the kind of a single type, returning the kinds of any scoped type variables
+--
+kindOfWithScopedVars :: Type -> Check (Kind, [(String, Kind)])   
+kindOfWithScopedVars ty = 
   rethrow (mkErrorStack "Error checking kind" (Just (TypeError ty)) <>) $
-    fmap (starIfUnknown . tidyUp) . liftUnify $ infer ty
+    fmap tidyUp . liftUnify $ infer ty
   where
-  tidyUp (k, sub) = sub $? k
+  tidyUp ((k, args), sub) = ( starIfUnknown (sub $? k)
+                            , map (second (starIfUnknown . (sub $?))) args
+                            )
 
 -- |
 -- Infer the kind of a type constructor with a collection of arguments and a collection of associated data constructors
@@ -125,7 +136,7 @@
 --
 solveTypes :: Bool -> [Type] -> [Kind] -> Kind -> UnifyT Kind Check Kind
 solveTypes isData ts kargs tyCon = do
-  ks <- mapM infer ts
+  ks <- mapM (fmap fst . infer) ts
   when isData $ do
     tyCon =?= foldr FunKind Star kargs
     forM_ ks $ \k -> k =?= Star
@@ -145,48 +156,64 @@
 -- |
 -- Infer a kind for a type
 --
-infer :: Type -> UnifyT Kind Check Kind
+infer :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
 infer ty = rethrow (mkErrorStack "Error inferring type of value" (Just (TypeError ty)) <>) $ infer' ty
 
-infer' :: Type -> UnifyT Kind Check Kind
-infer' TypeWildcard = fresh
-infer' (TypeVar v) = do
-  Just moduleName <- checkCurrentModule <$> get
-  UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
-infer' c@(TypeConstructor v) = do
-  env <- liftCheck getEnv
-  case M.lookup v (types env) of
-    Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))
-    Just (kind, _) -> return kind
-infer' (TypeApp t1 t2) = do
-  k0 <- fresh
-  k1 <- infer t1
-  k2 <- infer t2
-  k1 =?= FunKind k2 k0
-  return k0
+infer' :: Type -> UnifyT Kind Check (Kind, [(String, Kind)])
 infer' (ForAll ident ty _) = do
   k1 <- fresh
   Just moduleName <- checkCurrentModule <$> get
-  k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
+  (k2, args) <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ infer ty
   k2 =?= Star
-  return Star
-infer' REmpty = do
-  k <- fresh
-  return $ Row k
-infer' (RCons _ ty row) = do
-  k1 <- infer ty
-  k2 <- infer row
-  k2 =?= Row k1
-  return $ Row k1
-infer' (ConstrainedType deps ty) = do
-  forM_ deps $ \(className, tys) -> do
-    _ <- infer $ foldl TypeApp (TypeConstructor className) tys
-    return ()
-  k <- infer ty
-  k =?= Star
-  return Star
+  return (Star, (ident, k1) : args)
 infer' (KindedType ty k) = do
-  k' <- infer ty
+  (k', args) <- infer ty
   k =?= k'
-  return k'
-infer' _ = error "Invalid argument to infer"
+  return (k', args)
+infer' other = (, []) <$> go other
+  where
+  go :: Type -> UnifyT Kind Check Kind
+  go (ForAll ident ty _) = do
+    k1 <- fresh
+    Just moduleName <- checkCurrentModule <$> get
+    k2 <- bindLocalTypeVariables moduleName [(ProperName ident, k1)] $ go ty
+    k2 =?= Star
+    return Star
+  go (KindedType ty k) = do
+    k' <- go ty
+    k =?= k'
+    return k'
+  go TypeWildcard = fresh
+  go (TypeVar v) = do
+    Just moduleName <- checkCurrentModule <$> get
+    UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
+  go (Skolem v _ _) = do
+    Just moduleName <- checkCurrentModule <$> get
+    UnifyT . lift $ lookupTypeVariable moduleName (Qualified Nothing (ProperName v))
+  go c@(TypeConstructor v) = do
+    env <- liftCheck getEnv
+    case M.lookup v (types env) of
+      Nothing -> UnifyT . lift . throwError $ mkErrorStack "Unknown type constructor" (Just (TypeError c))
+      Just (kind, _) -> return kind
+  go (TypeApp t1 t2) = do
+    k0 <- fresh
+    k1 <- go t1
+    k2 <- go t2
+    k1 =?= FunKind k2 k0
+    return k0
+  go REmpty = do
+    k <- fresh
+    return $ Row k
+  go (RCons _ ty row) = do
+    k1 <- go ty
+    k2 <- go row
+    k2 =?= Row k1
+    return $ Row k1
+  go (ConstrainedType deps ty) = do
+    forM_ deps $ \(className, tys) -> do
+      _ <- go $ foldl TypeApp (TypeConstructor className) tys
+      return ()
+    k <- go ty
+    k =?= Star
+    return Star
+  go _ = error "Invalid argument to infer"
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
@@ -57,6 +57,12 @@
   return a
 
 -- |
+-- Temporarily bind a collection of names to types
+--
+withScopedTypeVars :: (Functor m, MonadState CheckState m) => ModuleName -> [(String, Kind)] -> m a -> m a
+withScopedTypeVars mn ks = bindTypes (M.fromList (map (\(name, k) -> (Qualified (Just mn) (ProperName name), (k, ScopedTypeVar))) ks))
+
+-- |
 -- Temporarily make a collection of type class dictionaries available
 --
 withTypeClassDictionaries :: (MonadState CheckState m) => [TypeClassDictionaryInScope] -> m a -> m a
diff --git a/src/Language/PureScript/TypeChecker/Skolems.hs b/src/Language/PureScript/TypeChecker/Skolems.hs
--- a/src/Language/PureScript/TypeChecker/Skolems.hs
+++ b/src/Language/PureScript/TypeChecker/Skolems.hs
@@ -71,6 +71,7 @@
 skolemizeTypesInValue ident sko scope = let (_, f, _) = everywhereOnValues id go id in f
   where
   go (SuperClassDictionary c ts) = SuperClassDictionary c (map (skolemize ident sko scope) ts)
+  go (TypedValue check val ty) = TypedValue check val (skolemize ident sko scope ty)
   go other = other
 
 -- |
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
@@ -129,16 +129,16 @@
   return (untyped, typed, dict, untypedDict)
 
 checkTypedBindingGroupElement :: ModuleName -> (Ident, (Expr, Type, Bool)) -> TypeData ->  UnifyT Type Check (Ident, (Expr, Type))
-checkTypedBindingGroupElement moduleName (ident, (val', ty, checkType)) dict = do
+checkTypedBindingGroupElement mn (ident, (val', ty, checkType)) dict = do
   -- Replace type wildcards
   ty' <- replaceTypeWildcards ty
   -- Kind check
-  kind <- liftCheck $ kindOf moduleName ty
-  guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty
+  checkTypeKind kind
   -- Check the type with the new names in scope
   ty'' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty'
   val'' <- if checkType
-           then bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''
+           then withScopedTypeVars mn args $ bindNames dict $ TypedValue True <$> check val' ty'' <*> pure ty''
            else return (TypedValue False val' ty'')
   return (ident, (val'', ty''))
 
@@ -183,10 +183,8 @@
 -- |
 -- Check the kind of a type, failing if it is not of kind *.
 --
-checkTypeKind :: ModuleName -> Type -> UnifyT t Check ()
-checkTypeKind moduleName ty = do
-  kind <- liftCheck $ kindOf moduleName ty
-  guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+checkTypeKind :: Kind -> UnifyT t Check ()
+checkTypeKind kind = guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
 
 -- |
 -- Remove any ForAlls and ConstrainedType constructors in a type by introducing new unknowns
@@ -293,9 +291,10 @@
   return $ TypeClassDictionary False (className, tys) dicts
 infer' (TypedValue checkType val ty) = do
   Just moduleName <- checkCurrentModule <$> get
-  checkTypeKind moduleName ty
+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty
+  checkTypeKind kind
   ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
-  val' <- if checkType then check val ty' else return val
+  val' <- if checkType then withScopedTypeVars moduleName args (check val ty') else return val
   return $ TypedValue True val' ty'
 infer' (PositionedValue pos _ val) = rethrowWithPosition pos $ infer' val
 infer' _ = error "Invalid argument to infer"
@@ -304,10 +303,11 @@
 inferLetBinding seen [] ret j = (,) seen <$> makeBindingGroupVisible (j ret)
 inferLetBinding seen (ValueDeclaration ident nameKind [] (Right (tv@(TypedValue checkType val ty))) : rest) ret j = do
   Just moduleName <- checkCurrentModule <$> get
-  checkTypeKind moduleName ty
+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty
+  checkTypeKind kind
   let dict = M.singleton (moduleName, ident) (ty, nameKind, Undefined)
   ty' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty
-  TypedValue _ val' ty'' <- if checkType then bindNames dict (check val ty') else return tv
+  TypedValue _ val' ty'' <- if checkType then withScopedTypeVars moduleName args (bindNames dict (check val ty')) else return tv
   bindNames (M.singleton (moduleName, ident) (ty'', nameKind, Defined)) $ inferLetBinding (seen ++ [ValueDeclaration ident nameKind [] (Right (TypedValue checkType val' ty''))]) rest ret j
 inferLetBinding seen (ValueDeclaration ident nameKind [] (Right val) : rest) ret j = do
   valTy <- fresh
@@ -507,14 +507,15 @@
   return $ TypeClassDictionary False (className, tys) dicts
 check' (TypedValue checkType val ty1) ty2 = do
   Just moduleName <- checkCurrentModule <$> get
-  checkTypeKind moduleName ty1
+  (kind, args) <- liftCheck $ kindOfWithScopedVars ty1
+  checkTypeKind kind
   ty1' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty1
   ty2' <- introduceSkolemScope <=< replaceAllTypeSynonyms <=< replaceTypeWildcards $ ty2
   val' <- subsumes (Just val) ty1' ty2'
   case val' of
     Nothing -> throwError . strMsg $ "Unable to check type subsumption"
     Just val'' -> do
-      val''' <- if checkType then check val'' ty2' else return val''
+      val''' <- if checkType then withScopedTypeVars moduleName args (check val'' ty2') else return val''
       return $ TypedValue checkType (TypedValue True val''' ty1') ty2'
 check' (Case vals binders) ret = do
   vals' <- mapM infer vals
@@ -562,7 +563,7 @@
   ty' <- introduceSkolemScope <=< expandAllTypeSynonyms <=< replaceTypeWildcards $ ty
   check val ty'
 check' val kt@(KindedType ty kind) = do
-  guardWith (strMsg $ "Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
+  checkTypeKind kind
   val' <- check' val ty
   return $ TypedValue True val' kt
 check' (PositionedValue pos _ val) ty =
diff --git a/src/Language/PureScript/TypeChecker/Unify.hs b/src/Language/PureScript/TypeChecker/Unify.hs
--- a/src/Language/PureScript/TypeChecker/Unify.hs
+++ b/src/Language/PureScript/TypeChecker/Unify.hs
@@ -153,6 +153,23 @@
     Left  _  -> False
     Right t1 -> unifiesWith e t1 t2
 unifiesWith e t1 t2@(SaturatedTypeSynonym _ _) = unifiesWith e t2 t1
+unifiesWith _ REmpty REmpty = True
+unifiesWith e r1@(RCons _ _ _) r2@(RCons _ _ _) =
+  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 all (\(t1, t2) -> unifiesWith e t1 t2) int && go sd1 r1' sd2 r2'
+  where
+  go :: [(String, Type)] -> Type -> [(String, Type)] -> Type -> Bool
+  go [] REmpty          [] REmpty          = True 
+  go [] (TypeVar v1)    [] (TypeVar v2)    = v1 == v2
+  go [] (Skolem _ s1 _) [] (Skolem _ s2 _) = s1 == s2
+  go _  (TUnknown _)    _  _               = True
+  go _  _               _  (TUnknown _)    = True
+  go _  _               _  _               = False
 unifiesWith _ _ _ = False
 
 -- |