diff --git a/libraries/prelude/prelude.purs b/libraries/prelude/prelude.purs
--- a/libraries/prelude/prelude.purs
+++ b/libraries/prelude/prelude.purs
@@ -24,6 +24,20 @@
 
   infixr 1000 $
 
+  class Show a where
+    show :: a -> String
+
+  instance Show String where
+    show s = s
+
+  instance Show Boolean where
+    show true = "true"
+    show false = "false"
+
+  class Monad m where
+    ret :: forall a. a -> m a
+    (>>=) :: forall a b. m a -> (a -> m b) -> m b
+
 module Maybe where
 
   data Maybe a = Nothing | Just a
@@ -277,7 +291,9 @@
 
   foreign import runPure "function runPure(f) { return f(); }" :: forall a. Pure a -> a
 
-  eff = { ret: retEff, bind: bindEff }
+  instance Prelude.Monad (Eff e) where
+    ret = retEff
+    (>>=) = bindEff
 
 module Errors where
 
@@ -311,7 +327,7 @@
   
   foreign import trace "function trace(s) { return function() { console.log(s); return {}; }; }" :: forall r. String -> Eff (trace :: Trace | r) {}
 
-  foreign import print "function print(o) { return function() { console.log(JSON.stringify(o)); return {}; }; }" :: forall a r. a -> Eff (trace :: Trace | r) {}
+  foreign import print "function print(dict) { return function (o) { return function() { console.log(Prelude.show(dict)(o)); return {}; }; }; }" :: forall a r. (Prelude.Show a) => a -> Eff (trace :: Trace | r) {}
 
 module ST where
 
diff --git a/psci/Main.hs b/psci/Main.hs
--- a/psci/Main.hs
+++ b/psci/Main.hs
@@ -60,14 +60,12 @@
   let
     moduleName = P.ProperName "Main"
     importDecl m = P.ImportDeclaration m Nothing
-    effModule = P.ModuleName (P.ProperName "Eff")
     traceModule = P.ModuleName (P.ProperName "Trace")
-    effMonad = P.Var (P.Qualified (Just effModule) (P.Ident "eff"))
     trace = P.Var (P.Qualified (Just traceModule) (P.Ident "print"))
     mainDecl = P.ValueDeclaration (P.Ident "main") [] Nothing
-        (P.Do effMonad [ P.DoNotationBind (P.VarBinder (P.Ident "it")) value
-                       , P.DoNotationValue (P.App trace [ P.Var (P.Qualified Nothing (P.Ident "it")) ] )
-                       ])
+        (P.Do [ P.DoNotationBind (P.VarBinder (P.Ident "it")) value
+              , P.DoNotationValue (P.App trace [ P.Var (P.Qualified Nothing (P.Ident "it")) ] )
+              ])
   in
     P.Module moduleName $ map (importDecl . P.ModuleName) imports ++ [mainDecl]
 
diff --git a/purescript.cabal b/purescript.cabal
--- a/purescript.cabal
+++ b/purescript.cabal
@@ -1,5 +1,5 @@
 name: purescript
-version: 0.2.14
+version: 0.2.15
 cabal-version: >=1.8
 build-type: Simple
 license: MIT
@@ -34,6 +34,7 @@
                      Language.PureScript.Sugar.TypeDeclarations
                      Language.PureScript.Sugar.BindingGroups
                      Language.PureScript.Sugar.Operators
+                     Language.PureScript.Sugar.TypeClasses
                      Language.PureScript.CodeGen
                      Language.PureScript.CodeGen.Externs
                      Language.PureScript.CodeGen.JS
@@ -82,7 +83,7 @@
     hs-source-dirs: psci
     buildable: True
     other-modules:
-    ghc-options: -Wall -O2 -fno-warn-unused-do-bind
+    ghc-options: -Wall -O2
 
 test-suite tests
     build-depends: base >=4 && <5, containers -any,
diff --git a/src/Language/PureScript.hs b/src/Language/PureScript.hs
--- a/src/Language/PureScript.hs
+++ b/src/Language/PureScript.hs
@@ -27,15 +27,17 @@
 import Language.PureScript.Options as P
 
 import Data.List (intercalate)
-import Control.Monad (when, forM_)
+import Control.Monad (when, forM)
+import Control.Applicative ((<$>))
 import qualified Data.Map as M
 
 compile :: Options -> [Module] -> Either String (String, String, Environment)
 compile opts ms = do
   desugared <- desugar ms
-  (_, env) <- runCheck $ forM_ desugared $ \(Module moduleName decls) -> typeCheckAll (ModuleName moduleName) decls
-  let js = concatMap (flip (moduleToJs opts) env) $ desugared
-  let exts = intercalate "\n" . map (flip moduleToPs env) $ desugared
+  (elaborated, env) <- runCheck $ forM desugared $ \(Module moduleName decls) -> Module moduleName <$> typeCheckAll (ModuleName moduleName) decls
+  let regrouped = createBindingGroupsModule . collapseBindingGroupsModule $ elaborated
+  let js = concatMap (flip (moduleToJs opts) env) $ regrouped
+  let exts = intercalate "\n" . map (flip moduleToPs env) $ regrouped
   js' <- case () of
               _ | optionsRunMain opts -> do
                     when ((ModuleName (ProperName "Main"), Ident "main") `M.notMember` (names 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
@@ -19,10 +19,13 @@
 ) where
 
 import Data.Maybe (mapMaybe)
-import qualified Data.Map as M
+import Data.List (sortBy)
+
 import Control.Arrow (second)
 import Control.Monad (replicateM, forM)
 
+import qualified Data.Map as M
+
 import Language.PureScript.TypeChecker (Environment(..), NameKind(..))
 import Language.PureScript.Values
 import Language.PureScript.Names
@@ -40,13 +43,17 @@
   mapMaybe filterRawDecls decls ++
   [ JSVariableIntroduction (Ident name) Nothing
   , JSApp (JSFunction Nothing [Ident name]
-                      (JSBlock (concat $ mapMaybe (\decl -> fmap (map $ optimize opts) $ declToJs opts (ModuleName pname) decl env) decls)))
+                      (JSBlock (concat $ mapMaybe (\decl -> fmap (map $ optimize opts) $ declToJs opts (ModuleName pname) decl env) (sortBy typeClassesLast decls))))
           [JSAssignment (JSAssignVariable (Ident name))
                          (JSBinary Or (JSVar (Ident name)) (JSObjectLiteral []))]
   ]
   where
-  filterRawDecls (ExternDeclaration _ (Just js) _) = Just js
+  filterRawDecls (ExternDeclaration ForeignImport _ (Just js) _) = Just js
   filterRawDecls _ = Nothing
+  typeClassesLast (ExternDeclaration TypeClassDictionaryImport _ _ _) (ExternDeclaration TypeClassDictionaryImport _ _ _) = EQ
+  typeClassesLast (ExternDeclaration TypeClassDictionaryImport _ _ _) _ = GT
+  typeClassesLast _ (ExternDeclaration TypeClassDictionaryImport _ _ _) = LT
+  typeClassesLast _ _ = EQ
 
 declToJs :: Options -> ModuleName -> Declaration -> Environment -> Maybe [JS]
 declToJs opts mp (ValueDeclaration ident _ _ val) e =
@@ -68,6 +75,9 @@
                         (JSObjectLiteral [ ("ctor", JSStringLiteral (show (Qualified (Just mp) pn)))
                                          , ("value", JSVar (Ident "value")) ])])
     in [ ctorJs, setProperty ctor (JSVar (Ident ctor)) mp ]
+declToJs _ mp (ExternDeclaration importTy ident (Just js) _) _ | importTy /= ForeignImport =
+  Just [ js
+       , setProperty (identToJs ident) (JSVar ident) mp ]
 declToJs _ _ _ _ = Nothing
 
 setProperty :: String -> JS -> ModuleName -> JS
@@ -92,11 +102,12 @@
 valueToJs opts m e (Indexer index val) = JSIndexer (valueToJs opts m e index) (valueToJs opts m e val)
 valueToJs opts m e (App val args) = JSApp (valueToJs opts m e val) (map (valueToJs opts m e) args)
 valueToJs opts m e (Abs args val) = JSFunction Nothing args (JSBlock [JSReturn (valueToJs opts m e val)])
-valueToJs opts m e (TypedValue (Abs args val) ty) | optionsPerformRuntimeTypeChecks opts = JSFunction Nothing args (JSBlock $ runtimeTypeChecks args ty ++ [JSReturn (valueToJs opts m e val)])
+valueToJs opts m e (TypedValue _ (Abs args val) ty) | optionsPerformRuntimeTypeChecks opts = JSFunction Nothing args (JSBlock $ runtimeTypeChecks args ty ++ [JSReturn (valueToJs opts m e val)])
 valueToJs opts m e (Unary op val) = JSUnary op (valueToJs opts m e val)
 valueToJs opts m e (Binary op v1 v2) = JSBinary op (valueToJs opts m e v1) (valueToJs opts m e v2)
 valueToJs _ m e (Var ident) = varToJs m e ident
-valueToJs opts m e (TypedValue val _) = valueToJs opts m e val
+valueToJs opts m e (TypedValue _ val _) = valueToJs opts m e val
+valueToJs _ _ _ (TypeClassDictionary _ _) = error "Type class dictionary was not replaced"
 valueToJs _ _ _ _ = error "Invalid argument to valueToJs"
 
 runtimeTypeChecks :: [Ident] -> Type -> [JS]
@@ -134,7 +145,7 @@
   Just (_, Alias aliasModule aliasIdent) -> qualifiedToJS identToJs (Qualified (Just aliasModule) aliasIdent)
   _ -> qualifiedToJS identToJs qual
   where
-  isExtern Extern = True
+  isExtern (Extern ForeignImport) = True
   isExtern (Alias m' ident') = case M.lookup (m', ident') (names e) of
     Just (_, ty') -> isExtern ty'
     Nothing -> error "Undefined alias in varToJs"
diff --git a/src/Language/PureScript/Declarations.hs b/src/Language/PureScript/Declarations.hs
--- a/src/Language/PureScript/Declarations.hs
+++ b/src/Language/PureScript/Declarations.hs
@@ -32,6 +32,11 @@
 
 data Module = Module ProperName [Declaration] deriving (Show, D.Data, D.Typeable)
 
+data ForeignImportType
+  = ForeignImport
+  | TypeClassDictionaryImport
+  | TypeClassAccessorImport deriving (Show, Eq, D.Data, D.Typeable)
+
 data Declaration
   = DataDeclaration ProperName [String] [(ProperName, Maybe Type)]
   | DataBindingGroupDeclaration [(ProperName, [String], [(ProperName, Maybe Type)])]
@@ -39,8 +44,10 @@
   | TypeDeclaration Ident Type
   | ValueDeclaration Ident [[Binder]] (Maybe Guard) Value
   | BindingGroupDeclaration [(Ident, Value)]
-  | ExternDeclaration Ident (Maybe JS) Type
+  | ExternDeclaration ForeignImportType Ident (Maybe JS) Type
   | ExternDataDeclaration ProperName Kind
   | FixityDeclaration Fixity String
   | ImportDeclaration ModuleName (Maybe [Either Ident ProperName])
+  | TypeClassDeclaration ProperName String [Declaration]
+  | TypeInstanceDeclaration [(Qualified ProperName, Type)] (Qualified ProperName) Type [Declaration]
   deriving (Show, D.Data, D.Typeable)
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
@@ -71,14 +71,17 @@
                 , "infixl"
                 , "infixr"
                 , "module"
-                , "let" ]
+                , "let"
+                , "class"
+                , "instance"
+                , "where" ]
 
 builtInOperators :: [String]
 builtInOperators = [ "~", "-", "<=", ">=", "<", ">", "*", "/", "%", "++", "+", "<<", ">>>", ">>"
                   , "==", "!=", "&&", "||", "&", "^", "|", "!!", "!" ]
 
 reservedOpNames :: [String]
-reservedOpNames = builtInOperators ++ [ "->", "=", ".", "\\" ]
+reservedOpNames = builtInOperators ++ [ "=>", "->", "=", ".", "\\" ]
 
 identStart :: P.Parsec String u Char
 identStart = P.lower <|> P.oneOf "_"
diff --git a/src/Language/PureScript/Parser/Declarations.hs b/src/Language/PureScript/Parser/Declarations.hs
--- a/src/Language/PureScript/Parser/Declarations.hs
+++ b/src/Language/PureScript/Parser/Declarations.hs
@@ -18,6 +18,7 @@
     parseModules
 ) where
 
+import Data.Maybe (fromMaybe)
 import Control.Applicative
 import qualified Text.Parsec as P
 
@@ -37,7 +38,7 @@
   reserved "data"
   name <- indented *> properName
   tyArgs <- many (indented *> identifier)
-  lexeme $ indented *> P.char '='
+  _ <- lexeme $ indented *> P.char '='
   ctors <- sepBy1 ((,) <$> properName <*> P.optionMaybe (indented *> parsePolyType)) pipe
   return $ DataDeclaration name tyArgs ctors
 
@@ -66,9 +67,9 @@
 parseExternDeclaration = P.try (reserved "foreign") *> indented *> (reserved "import") *> indented *>
    (ExternDataDeclaration <$> (P.try (reserved "data") *> indented *> properName)
                              <*> (lexeme (indented *> P.string "::") *> parseKind)
-   <|> ExternDeclaration <$> parseIdent
-                         <*> P.optionMaybe (parseJSLiteral <$> stringLiteral)
-                         <*> (lexeme (indented *> P.string "::") *> parsePolyType))
+   <|> ExternDeclaration ForeignImport <$> parseIdent
+                                       <*> P.optionMaybe (parseJSLiteral <$> stringLiteral)
+                                       <*> (lexeme (indented *> P.string "::") *> parsePolyType))
 
 parseJSLiteral :: String -> JS
 parseJSLiteral s = either (const $ JSRaw s) id $ P.runParser parseJS () "Javascript" s
@@ -96,6 +97,29 @@
   idents <- P.optionMaybe $ parens $ commaSep1 (Left <$> parseIdent <|> Right <$> properName)
   return $ ImportDeclaration moduleName idents
 
+parseTypeClassDeclaration :: P.Parsec String ParseState Declaration
+parseTypeClassDeclaration = do
+  reserved "class"
+  className <- indented *> properName
+  ident <- indented *> identifier
+  indented *> reserved "where"
+  members <- mark (P.many (same *> parseTypeDeclaration))
+  return $ TypeClassDeclaration className ident members
+
+parseTypeInstanceDeclaration :: P.Parsec String ParseState Declaration
+parseTypeInstanceDeclaration = do
+  reserved "instance"
+  deps <- P.optionMaybe $ do
+    deps <- parens (commaSep1 ((,) <$> parseQualified properName <*> parseType))
+    indented
+    reservedOp "=>"
+    return deps
+  className <- indented *> parseQualified properName
+  ty <- indented *> parseType
+  indented *> reserved "where"
+  members <- mark (P.many (same *> parseValueDeclaration))
+  return $ TypeInstanceDeclaration (fromMaybe [] deps) className ty members
+
 parseDeclaration :: P.Parsec String ParseState Declaration
 parseDeclaration = P.choice
                    [ parseDataDeclaration
@@ -104,14 +128,16 @@
                    , parseValueDeclaration
                    , parseExternDeclaration
                    , parseFixityDeclaration
-                   , parseImportDeclaration ] P.<?> "declaration"
+                   , parseImportDeclaration
+                   , parseTypeClassDeclaration
+                   , parseTypeInstanceDeclaration ] P.<?> "declaration"
 
 parseModule :: P.Parsec String ParseState Module
 parseModule = do
   reserved "module"
   indented
   name <- properName
-  lexeme $ P.string "where"
+  _ <- lexeme $ P.string "where"
   decls <- mark (P.many (same *> parseDeclaration))
   return $ Module name decls
 
diff --git a/src/Language/PureScript/Parser/JS.hs b/src/Language/PureScript/Parser/JS.hs
--- a/src/Language/PureScript/Parser/JS.hs
+++ b/src/Language/PureScript/Parser/JS.hs
@@ -87,9 +87,9 @@
 
 parseConditional :: JS -> P.Parsec String u JS
 parseConditional js = P.try $ do
-  C.lexeme $ P.char '?'
+  _ <- C.lexeme $ P.char '?'
   tr <- parseJS
-  C.lexeme $ P.char ':'
+  _ <- C.lexeme $ P.char ':'
   fa <- parseJS
   return $ JSConditional js tr fa
 
@@ -139,18 +139,18 @@
   C.reserved "var"
   name <- Ident <$> P.identifier C.tokenParser
   value <- P.optionMaybe $ do
-    C.lexeme $ P.char '='
+    _ <- C.lexeme $ P.char '='
     value <- parseJS
-    C.semi
+    _ <- C.semi
     return value
   return $ JSVariableIntroduction name value
 
 parseAssignment :: P.Parsec String u JS
 parseAssignment = do
   tgt <- parseAssignmentTarget
-  C.lexeme $ P.char '='
+  _ <- C.lexeme $ P.char '='
   value <- parseJS
-  C.semi
+  _ <- C.semi
   return $ JSAssignment tgt value
 
 parseAssignmentTarget :: P.Parsec String u JSAssignment
diff --git a/src/Language/PureScript/Parser/Types.hs b/src/Language/PureScript/Parser/Types.hs
--- a/src/Language/PureScript/Parser/Types.hs
+++ b/src/Language/PureScript/Parser/Types.hs
@@ -44,7 +44,7 @@
 parseFunction :: P.Parsec String ParseState Type
 parseFunction = do
   args <- lexeme $ parens $ commaSep parsePolyType
-  lexeme $ P.string "->"
+  _ <- lexeme $ P.string "->"
   resultType <- parseType
   return $ Function args resultType
 
@@ -56,7 +56,7 @@
 
 parseForAll :: P.Parsec String ParseState Type
 parseForAll = (mkForAll <$> (P.try (reserved "forall") *> P.many1 (indented *> identifier) <* indented <* dot)
-                        <*> parseType)
+                        <*> parseConstrainedType)
 
 parseTypeAtom :: P.Parsec String ParseState Type
 parseTypeAtom = indented *> P.choice (map P.try
@@ -71,6 +71,20 @@
             , parseForAll
             , parens parseRow
             , parens parseType ])
+
+parseConstrainedType :: P.Parsec String ParseState Type
+parseConstrainedType = do
+  constraints <- P.optionMaybe . P.try $ do
+    constraints <- parens . commaSep1 $ do
+      className <- parseQualified properName
+      indented
+      ty <- parseType
+      return (className, ty)
+    _ <- lexeme $ P.string "=>"
+    return constraints
+  indented
+  ty <- parseType
+  return $ maybe ty (flip ConstrainedType ty) constraints
 
 parseAnyType :: P.Parsec String ParseState Type
 parseAnyType = (P.buildExpressionParser operators . buildPostfixParser postfixTable $ parseTypeAtom) P.<?> "type"
diff --git a/src/Language/PureScript/Parser/Values.hs b/src/Language/PureScript/Parser/Values.hs
--- a/src/Language/PureScript/Parser/Values.hs
+++ b/src/Language/PureScript/Parser/Values.hs
@@ -94,10 +94,10 @@
 
 parseManyStatements :: P.Parsec String ParseState [Statement]
 parseManyStatements = (do
-  C.lexeme $ P.char '{'
+  _ <- C.lexeme $ P.char '{'
   C.indented
   sts <- C.mark (P.many (C.same *> C.mark parseStatement))
-  C.lexeme (P.char '}')
+  _ <- C.lexeme (P.char '}')
   return sts) P.<?> "block"
 
 parseValueAtom :: P.Parsec String ParseState Value
@@ -113,12 +113,13 @@
             , parseBlock
             , parseCase
             , parseIfThenElse
+            , parseDo
             , Parens <$> C.parens parseValue ]
 
 parsePropertyUpdate :: P.Parsec String ParseState (String, Value)
 parsePropertyUpdate = do
   name <- C.lexeme C.identifier
-  C.lexeme $ C.indented *> P.char '='
+  _ <- C.lexeme $ C.indented *> P.char '='
   value <- C.indented *> parseValue
   return (name, value)
 
@@ -126,6 +127,12 @@
 parseAccessor (Constructor _) = P.unexpected "constructor"
 parseAccessor obj = P.try $ Accessor <$> (C.indented *> C.dot *> P.notFollowedBy C.opLetter *> C.indented *> C.identifier) <*> pure obj
 
+parseDo :: P.Parsec String ParseState Value
+parseDo = do
+  C.reserved "do"
+  C.indented
+  Do <$> C.mark (P.many (C.same *> C.mark parseDoNotationElement))
+
 parseDoNotationLet :: P.Parsec String ParseState DoNotationElement
 parseDoNotationLet = DoNotationLet <$> (C.reserved "let" *> C.indented *> parseBinder)
                                    <*> (C.indented *> C.reservedOp "=" *> parseValue)
@@ -133,21 +140,12 @@
 parseDoNotationBind :: P.Parsec String ParseState DoNotationElement
 parseDoNotationBind = DoNotationBind <$> parseBinder <*> (C.indented *> C.reservedOp "<-" *> parseValue)
 
-parseDoNotationReturn :: P.Parsec String ParseState DoNotationElement
-parseDoNotationReturn = DoNotationReturn <$> (C.reserved "return" *> C.indented *> parseValue)
-
 parseDoNotationElement :: P.Parsec String ParseState DoNotationElement
 parseDoNotationElement = P.choice
             [ P.try parseDoNotationBind
             , parseDoNotationLet
-            , parseDoNotationReturn
             , P.try (DoNotationValue <$> parseValue) ]
 
-parseManyDoNotationElements :: P.Parsec String ParseState [DoNotationElement]
-parseManyDoNotationElements = do
-  C.indented
-  C.mark (P.many (C.same *> C.mark parseDoNotationElement))
-
 parseValue :: P.Parsec String ParseState Value
 parseValue =
   (buildExpressionParser operators
@@ -159,8 +157,7 @@
                   , \v -> P.try $ flip ObjectUpdate <$> (C.indented *> C.braces (C.commaSep1 (C.indented *> parsePropertyUpdate))) <*> pure v ]
   postfixTable2 = [ \v -> P.try (C.indented *> indexersAndAccessors >>= \t2 -> return (\t1 -> App t1 [t2])) <*> pure v
                   , \v -> P.try $ flip App <$> (C.indented *> C.parens (C.commaSep parseValue)) <*> pure v
-                  , \v -> flip TypedValue <$> (P.try (C.lexeme (C.indented *> P.string "::")) *> parsePolyType) <*> pure v
-                  , \v -> P.try $ Do v <$> (C.indented *> C.reserved "do" *> parseManyDoNotationElements)
+                  , \v -> flip (TypedValue True) <$> (P.try (C.lexeme (C.indented *> P.string "::")) *> parsePolyType) <*> pure v
                   ]
   operators = [ [ Prefix $ C.lexeme (P.try $ C.indented *> C.reservedOp "!") >> return (Unary Not)
                 , Prefix $ C.lexeme (P.try $ C.indented *> C.reservedOp "~") >> return (Unary BitwiseNot)
@@ -174,19 +171,19 @@
 parseVariableIntroduction = do
   C.reserved "var"
   name <- C.indented *> C.parseIdent
-  C.lexeme $ C.indented *> P.char '='
+  _ <- C.lexeme $ C.indented *> P.char '='
   value <- parseValue
-  C.indented *> C.semi
+  _ <- C.indented *> C.semi
   return $ VariableIntroduction name value
 
 parseAssignment :: P.Parsec String ParseState Statement
 parseAssignment = do
   tgt <- P.try $ do
     tgt <- C.parseIdent
-    C.lexeme $ C.indented *> P.char '='
+    _ <- C.lexeme $ C.indented *> P.char '='
     return tgt
   value <- parseValue
-  C.indented *> C.semi
+  _ <- C.indented *> C.semi
   return $ Assignment tgt value
 
 parseWhile :: P.Parsec String ParseState Statement
@@ -258,7 +255,7 @@
 parseIdentifierAndBinder :: P.Parsec String ParseState (String, Binder)
 parseIdentifierAndBinder = do
   name <- C.lexeme C.identifier
-  C.lexeme $ C.indented *> P.char '='
+  _ <- C.lexeme $ C.indented *> P.char '='
   binder <- C.indented *> parseBinder
   return (name, binder)
 
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
@@ -37,6 +37,7 @@
   match (TypeConstructor ctor) = Just $ show ctor
   match (TUnknown (Unknown u)) = Just $ 'u' : show u
   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 REmpty = Just $ prettyPrintRow REmpty
diff --git a/src/Language/PureScript/Pretty/Values.hs b/src/Language/PureScript/Pretty/Values.hs
--- a/src/Language/PureScript/Pretty/Values.hs
+++ b/src/Language/PureScript/Pretty/Values.hs
@@ -40,6 +40,8 @@
   match (Case values binders) = Just $ "case " ++ intercalate " " (map prettyPrintValue values) ++
     " of { " ++ intercalate " ; " (map prettyPrintCaseAlternative binders) ++ " }"
   match (Var ident) = Just $ show ident
+  match (Do els) = Just $ " do { " ++ intercalate "; " (map prettyPrintDoNotationElement els) ++ " }"
+  match (TypeClassDictionary _ _) = error "Type class dictionary was not replaced"
   match _ = Nothing
 
 prettyPrintCaseAlternative :: ([Binder], Maybe Guard, Value) -> String
@@ -85,7 +87,7 @@
 typed :: Pattern () Value (Type, Value)
 typed = mkPattern match
   where
-  match (TypedValue val ty) = Just (ty, val)
+  match (TypedValue _ val ty) = Just (ty, val)
   match _ = Nothing
 
 unary :: UnaryOperator -> String -> Operator () Value String
@@ -106,17 +108,10 @@
     match' (Binary op' v1 v2) | op' == op = Just (v1, v2)
     match' _ = Nothing
 
-_do :: Pattern () Value ([DoNotationElement], Value)
-_do = mkPattern match
-  where
-  match (Do val els) = Just (els, val)
-  match _ = Nothing
-
 prettyPrintDoNotationElement :: DoNotationElement -> String
 prettyPrintDoNotationElement (DoNotationValue val) = prettyPrintValue val
 prettyPrintDoNotationElement (DoNotationBind binder val) = prettyPrintBinder binder ++ " <- " ++ prettyPrintValue val
 prettyPrintDoNotationElement (DoNotationLet binder val) = "let " ++ prettyPrintBinder binder ++ " = " ++ prettyPrintValue val
-prettyPrintDoNotationElement (DoNotationReturn val) = "return " ++ prettyPrintValue val
 
 prettyPrintValue :: Value -> String
 prettyPrintValue = fromMaybe (error "Incomplete pattern") . pattern matchValue ()
@@ -128,7 +123,6 @@
     OperatorTable [ [ Wrap accessor $ \prop val -> val ++ "." ++ prop ]
                   , [ Wrap objectUpdate $ \ps val -> val ++ "{ " ++ intercalate ", " ps ++ " }" ]
                   , [ Wrap app $ \args val -> val ++ "(" ++ args ++ ")" ]
-                  , [ Wrap _do $ \els val -> val ++ " do { " ++ intercalate "; " (map prettyPrintDoNotationElement els) ++ " }" ]
                   , [ Split lam $ \args val -> "\\" ++ intercalate ", " args ++ " -> " ++ prettyPrintValue val ]
                   , [ Wrap ifThenElse $ \(th, el) cond -> cond ++ " ? " ++ prettyPrintValue th ++ " : " ++ prettyPrintValue el ]
                   , [ Wrap typed $ \ty val -> val ++ " :: " ++ prettyPrintType ty ]
diff --git a/src/Language/PureScript/Sugar.hs b/src/Language/PureScript/Sugar.hs
--- a/src/Language/PureScript/Sugar.hs
+++ b/src/Language/PureScript/Sugar.hs
@@ -23,9 +23,11 @@
 import Language.PureScript.Sugar.CaseDeclarations as S
 import Language.PureScript.Sugar.TypeDeclarations as S
 import Language.PureScript.Sugar.BindingGroups as S
+import Language.PureScript.Sugar.TypeClasses as S
 
 desugar :: [Module] -> Either String [Module]
-desugar = rebracket
+desugar = desugarTypeClasses
+          >=> rebracket
           >=> desugarDo
           >=> desugarCasesModule
           >=> desugarTypeDeclarationsModule
diff --git a/src/Language/PureScript/Sugar/BindingGroups.hs b/src/Language/PureScript/Sugar/BindingGroups.hs
--- a/src/Language/PureScript/Sugar/BindingGroups.hs
+++ b/src/Language/PureScript/Sugar/BindingGroups.hs
@@ -14,7 +14,9 @@
 
 module Language.PureScript.Sugar.BindingGroups (
     createBindingGroups,
-    createBindingGroupsModule
+    createBindingGroupsModule,
+    collapseBindingGroups,
+    collapseBindingGroupsModule
 ) where
 
 import Data.Data
@@ -30,6 +32,9 @@
 createBindingGroupsModule :: [Module] -> [Module]
 createBindingGroupsModule = map $ \(Module name ds) -> Module name (createBindingGroups ds)
 
+collapseBindingGroupsModule :: [Module] -> [Module]
+collapseBindingGroupsModule = map $ \(Module name ds) -> Module name (collapseBindingGroups ds)
+
 createBindingGroups :: [Declaration] -> [Declaration]
 createBindingGroups ds =
   let
@@ -44,6 +49,13 @@
     bindingGroupDecls = map toBindingGroup $ stronglyConnComp valueVerts
   in
     dataBindingGroupDecls ++ nonValues ++ bindingGroupDecls
+
+collapseBindingGroups :: [Declaration] -> [Declaration]
+collapseBindingGroups ds = concatMap go ds
+  where
+  go (DataBindingGroupDeclaration ds) = map (\(name, args, dctors) -> DataDeclaration name args dctors) ds
+  go (BindingGroupDeclaration ds) = map (\(ident, val) -> ValueDeclaration ident [] Nothing val) ds
+  go other = [other]
 
 usedIdents :: (Data d) => d -> [Ident]
 usedIdents = nub . everything (++) (mkQ [] namesV `extQ` namesS)
diff --git a/src/Language/PureScript/Sugar/DoNotation.hs b/src/Language/PureScript/Sugar/DoNotation.hs
--- a/src/Language/PureScript/Sugar/DoNotation.hs
+++ b/src/Language/PureScript/Sugar/DoNotation.hs
@@ -26,27 +26,31 @@
 desugarDo :: (Data d) => d -> Either String d
 desugarDo = everywhereM (mkM replace)
   where
+  prelude :: ModuleName
+  prelude = ModuleName (ProperName "Prelude")
+  ret :: Value
+  ret = Var (Qualified (Just prelude) (Ident "ret"))
+  bind :: Value
+  bind = Var (Qualified (Just prelude) (Op ">>="))
   replace :: Value -> Either String Value
-  replace (Do monad els) = go monad els
+  replace (Do els) = go els
   replace other = return other
-  go :: Value -> [DoNotationElement] -> Either String Value
-  go _ [] = error "The impossible happened in desugarDo"
-  go monad [DoNotationReturn val] = return $ App (Accessor "ret" monad) [val]
-  go _ (DoNotationReturn _ : _) = Left "Return statement must be the last statement in a do block"
-  go _ [DoNotationValue val] = return val
-  go monad (DoNotationValue val : rest) = do
-    rest' <- go monad rest
-    return $ App (App (Accessor "bind" monad) [val]) [Abs [Ident "_"] rest']
-  go _ [DoNotationBind _ _] = Left "Bind statement cannot be the last statement in a do block"
-  go monad (DoNotationBind NullBinder val : rest) = go monad (DoNotationValue val : rest)
-  go monad (DoNotationBind (VarBinder ident) val : rest) = do
-    rest' <- go monad rest
-    return $ App (App (Accessor "bind" monad) [val]) [Abs [ident] rest']
-  go monad (DoNotationBind binder val : rest) = do
-    rest' <- go monad rest
+  go :: [DoNotationElement] -> Either String Value
+  go [] = error "The impossible happened in desugarDo"
+  go [DoNotationValue val] = return val
+  go (DoNotationValue val : rest) = do
+    rest' <- go rest
+    return $ App (App bind [val]) [Abs [Ident "_"] rest']
+  go [DoNotationBind _ _] = Left "Bind statement cannot be the last statement in a do block"
+  go (DoNotationBind NullBinder val : rest) = go (DoNotationValue val : rest)
+  go (DoNotationBind (VarBinder ident) val : rest) = do
+    rest' <- go rest
+    return $ App (App bind [val]) [Abs [ident] rest']
+  go (DoNotationBind binder val : rest) = do
+    rest' <- go rest
     let ident = head $ unusedNames rest'
-    return $ App (App (Accessor "bind" monad) [val]) [Abs [ident] (Case [Var (Qualified Nothing ident)] [([binder], Nothing, rest')])]
-  go _ [DoNotationLet _ _] = Left "Let statement cannot be the last statement in a do block"
-  go monad (DoNotationLet binder val : rest) = do
-    rest' <- go monad rest
+    return $ App (App bind [val]) [Abs [ident] (Case [Var (Qualified Nothing ident)] [([binder], Nothing, rest')])]
+  go [DoNotationLet _ _] = Left "Let statement cannot be the last statement in a do block"
+  go (DoNotationLet binder val : rest) = do
+    rest' <- go rest
     return $ Case [val] [([binder], Nothing, rest')]
diff --git a/src/Language/PureScript/Sugar/TypeClasses.hs b/src/Language/PureScript/Sugar/TypeClasses.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/PureScript/Sugar/TypeClasses.hs
@@ -0,0 +1,133 @@
+-----------------------------------------------------------------------------
+--
+-- Module      :  Language.PureScript.Sugar.TypeClasses
+-- Copyright   :  (c) Phil Freeman 2013
+-- License     :  MIT
+--
+-- Maintainer  :  Phil Freeman <paf31@cantab.net>
+-- Stability   :  experimental
+-- Portability :
+--
+-- |
+--
+-----------------------------------------------------------------------------
+
+module Language.PureScript.Sugar.TypeClasses (
+  desugarTypeClasses,
+  mkDictionaryValueName,
+  mkDictionaryEntryName
+) where
+
+import Language.PureScript.Declarations
+import Language.PureScript.Names
+import Language.PureScript.Types
+import Language.PureScript.Values
+import Language.PureScript.CodeGen.JS.AST
+import Language.PureScript.Sugar.CaseDeclarations
+
+import qualified Data.Map as M
+
+import Control.Applicative
+import Control.Monad.State
+import Data.Maybe (fromMaybe)
+import Data.List (nub)
+import Data.Generics (mkQ, everything)
+import Language.PureScript.Pretty.Common (identToJs)
+
+type MemberMap = M.Map (ModuleName, ProperName) (String, [(String, Type)])
+
+type Desugar = StateT MemberMap (Either String)
+
+desugarTypeClasses :: [Module] -> Either String [Module]
+desugarTypeClasses = flip evalStateT M.empty . mapM desugarModule
+
+desugarModule :: Module -> Desugar Module
+desugarModule (Module name decls) = Module name <$> concat <$> mapM (desugarDecl (ModuleName name)) decls
+
+desugarDecl :: ModuleName -> Declaration -> Desugar [Declaration]
+desugarDecl mn d@(TypeClassDeclaration name arg members) = do
+  let tys = map memberToNameAndType members
+  modify (M.insert (mn, name) (arg, tys))
+  return $ d : typeClassDictionaryDeclaration name arg members : map (typeClassMemberToDictionaryAccessor name arg) members
+desugarDecl mn d@(TypeInstanceDeclaration deps name ty members) = do
+  desugared <- lift $ desugarCases members
+  entries <- mapM (typeInstanceDictionaryEntryDeclaration mn deps name ty) desugared
+  dictDecl <- typeInstanceDictionaryDeclaration mn deps name ty desugared
+  return $ d : entries ++ [dictDecl]
+desugarDecl _ other = return [other]
+
+memberToNameAndType :: Declaration -> (String, Type)
+memberToNameAndType (TypeDeclaration ident ty) = (identToJs ident, ty)
+memberToNameAndType _ = error "Invalid declaration in type class definition"
+
+typeClassDictionaryDeclaration :: ProperName -> String -> [Declaration] -> Declaration
+typeClassDictionaryDeclaration name arg members =
+  TypeSynonymDeclaration name [arg] (Object $ rowFromList (map memberToNameAndType members, REmpty))
+
+typeClassMemberToDictionaryAccessor :: ProperName -> String -> Declaration -> Declaration
+typeClassMemberToDictionaryAccessor name arg (TypeDeclaration ident ty) =
+  ExternDeclaration TypeClassAccessorImport ident
+    (Just (JSFunction (Just ident) [Ident "dict"] (JSBlock [JSReturn (JSAccessor (identToJs ident) (JSVar (Ident "dict")))])))
+    (ForAll arg (ConstrainedType [(Qualified Nothing name, TypeVar arg)] ty))
+typeClassMemberToDictionaryAccessor _ _ _ = error "Invalid declaration in type class definition"
+
+typeInstanceDictionaryDeclaration :: ModuleName -> [(Qualified ProperName, Type)] -> Qualified ProperName -> Type -> [Declaration] -> Desugar Declaration
+typeInstanceDictionaryDeclaration mn deps name ty decls = do
+  entryName <- lift $ mkDictionaryValueName mn name ty
+  memberNames <- mapM memberToNameAndValue decls
+  return $ ValueDeclaration entryName [] Nothing
+    (TypedValue False
+      (Abs
+        (map (\n -> Ident ('_' : show n)) [1..length deps])
+        (ObjectLiteral memberNames))
+      (quantify (Function (map (\(pn, ty') -> TypeApp (TypeConstructor pn) ty') deps) (TypeApp (TypeConstructor name) ty)))
+    )
+  where
+  memberToNameAndValue :: Declaration -> Desugar (String, Value)
+  memberToNameAndValue (ValueDeclaration ident _ _ _) = do
+    memberName <- mkDictionaryEntryName mn name ty ident
+    return (identToJs ident, if null deps then Var (Qualified Nothing memberName)
+                             else App (Var (Qualified Nothing memberName)) (map (\n -> Var (Qualified Nothing (Ident ('_' : show n)))) [1..length deps]))
+  memberToNameAndValue _ = error "Invalid declaration in type instance definition"
+
+typeInstanceDictionaryEntryDeclaration :: ModuleName -> [(Qualified ProperName, Type)] -> Qualified ProperName -> Type -> Declaration -> Desugar Declaration
+typeInstanceDictionaryEntryDeclaration mn deps name ty (ValueDeclaration ident [] _ val) = do
+  m <- get
+  valTy <- lift $ maybe (Left $ "Type class " ++ show name ++ " is undefined. Type class names must be qualified.") Right $
+                do (arg, members) <- M.lookup (qualify mn name) m
+                   ty' <- lookup (identToJs ident) members
+                   return $ replaceTypeVars arg ty ty'
+  entryName <- mkDictionaryEntryName mn name ty ident
+  return $ ValueDeclaration entryName [] Nothing
+    (TypedValue True val (quantify (if null deps then valTy else ConstrainedType deps valTy)))
+typeInstanceDictionaryEntryDeclaration _ _ _ _ _ = error "Invalid declaration in type instance definition"
+
+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 ForAll ty' tyVars
+  where
+  tyVars = nub $ everything (++) (mkQ [] collect) ty'
+  collect (TypeVar v) = [v]
+  collect _ = []
+
+mkDictionaryValueName :: ModuleName -> Qualified ProperName -> Type -> Either String Ident
+mkDictionaryValueName mn cl ty = do
+  tyStr <- typeToString mn ty
+  return $ Ident $ "__" ++ qualifiedToString mn cl ++ "_" ++ tyStr
+
+typeToString :: ModuleName -> Type -> Either String String
+typeToString _ String = return "string"
+typeToString _ Number = return "number"
+typeToString _ Boolean = return "boolean"
+typeToString _ (Array (TypeVar _)) = return "array"
+typeToString mn (TypeConstructor ty') = return $ qualifiedToString mn ty'
+typeToString mn (TypeApp ty' (TypeVar _)) = typeToString mn ty'
+typeToString _ _ = Left "Type class instance must be of the form T a1 ... an"
+
+mkDictionaryEntryName :: ModuleName -> Qualified ProperName -> Type -> Ident -> Desugar Ident
+mkDictionaryEntryName mn name ty ident = do
+  Ident dictName <- lift $ mkDictionaryValueName mn name ty
+  return $ Ident $ dictName ++ "_" ++ identToJs ident
diff --git a/src/Language/PureScript/Sugar/TypeDeclarations.hs b/src/Language/PureScript/Sugar/TypeDeclarations.hs
--- a/src/Language/PureScript/Sugar/TypeDeclarations.hs
+++ b/src/Language/PureScript/Sugar/TypeDeclarations.hs
@@ -29,7 +29,7 @@
 
 desugarTypeDeclarations :: [Declaration] -> Either String [Declaration]
 desugarTypeDeclarations (TypeDeclaration name ty : ValueDeclaration name' [] Nothing val : rest) | name == name' =
-  desugarTypeDeclarations (ValueDeclaration name [] Nothing (TypedValue val ty) : rest)
+  desugarTypeDeclarations (ValueDeclaration name [] Nothing (TypedValue True val ty) : rest)
 desugarTypeDeclarations (TypeDeclaration name _ : _) = throwError $ "Orphan type declaration for " ++ show name
 desugarTypeDeclarations (d:ds) = (:) d <$> desugarTypeDeclarations ds
 desugarTypeDeclarations [] = return []
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
@@ -24,8 +24,6 @@
 import Language.PureScript.TypeChecker.Types as T
 import Language.PureScript.TypeChecker.Synonyms as T
 
-import Data.Data
-import Data.Generics (mkT, everywhere)
 import Data.Maybe
 import qualified Data.Map as M
 import Control.Monad.State
@@ -34,8 +32,10 @@
 
 import Language.PureScript.Types
 import Language.PureScript.Names
+import Language.PureScript.Values
 import Language.PureScript.Kinds
 import Language.PureScript.Declarations
+import Language.PureScript.Sugar.TypeClasses
 
 addDataType :: ModuleName -> ProperName -> [String] -> [(ProperName, Maybe Type)] -> Kind -> Check ()
 addDataType moduleName name args dctors ctorKind = do
@@ -84,63 +84,78 @@
   env <- getEnv
   putEnv (env { names = M.insert (moduleName, name) (qualifyAllUnqualifiedNames moduleName env ty, Value) (names env) })
 
-typeCheckAll :: ModuleName -> [Declaration] -> Check ()
-typeCheckAll _ [] = return ()
-typeCheckAll moduleName (DataDeclaration name args dctors : rest) = do
+addTypeClassDictionaries :: [TypeClassDictionaryInScope] -> Check ()
+addTypeClassDictionaries entries = do
+  modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = entries ++ (typeClassDictionaries . checkEnv $ st) } }
+
+typeCheckAll :: ModuleName -> [Declaration] -> Check [Declaration]
+typeCheckAll _ [] = return []
+typeCheckAll moduleName (d@(DataDeclaration name args dctors) : rest) = do
   rethrow (("Error in type constructor " ++ show name ++ ":\n") ++) $ do
     typeIsNotDefined moduleName name
     ctorKind <- kindsOf moduleName name args (mapMaybe snd dctors)
     addDataType moduleName name args dctors ctorKind
-  typeCheckAll moduleName rest
-typeCheckAll moduleName (DataBindingGroupDeclaration tys : rest) = do
+  ds <- typeCheckAll moduleName rest
+  return $ d : ds
+typeCheckAll moduleName (d@(DataBindingGroupDeclaration tys) : rest) = do
   rethrow (("Error in data binding group " ++ show (map (\(name, _, _) -> name) tys) ++ ":\n") ++) $ do
     forM_ tys $ \(name, _, _) ->
       typeIsNotDefined moduleName name
     ks <- kindsOfAll moduleName (map (\(name, args, dctors) -> (name, args, mapMaybe snd dctors)) tys)
-    forM (zip tys ks) $ \((name, args, dctors), ctorKind) ->
+    forM_ (zip tys ks) $ \((name, args, dctors), ctorKind) ->
       addDataType moduleName name args dctors ctorKind
-  typeCheckAll moduleName rest
-typeCheckAll moduleName (TypeSynonymDeclaration name args ty : rest) = do
+  ds <- typeCheckAll moduleName rest
+  return $ d : ds
+typeCheckAll moduleName (d@(TypeSynonymDeclaration name args ty) : rest) = do
   rethrow (("Error in type synonym " ++ show name ++ ":\n") ++) $ do
     typeIsNotDefined moduleName name
     kind <- kindsOf moduleName name args [ty]
     addTypeSynonym moduleName name args ty kind
-  typeCheckAll moduleName rest
+  ds <- typeCheckAll moduleName rest
+  return $ d : ds
 typeCheckAll _ (TypeDeclaration _ _ : _) = error "Type declarations should have been removed"
 typeCheckAll moduleName (ValueDeclaration name [] Nothing val : rest) = do
-  rethrow (("Error in declaration " ++ show name ++ ":\n") ++) $ do
+  d <- rethrow (("Error in declaration " ++ show name ++ ":\n") ++) $ do
     valueIsNotDefined moduleName name
-    [ty] <- typesOf moduleName [(name, val)]
+    [(_, (val', ty))] <- typesOf moduleName [(name, val)]
     addValue moduleName name ty
-  typeCheckAll moduleName rest
+    return $ ValueDeclaration name [] Nothing val'
+  ds <- typeCheckAll moduleName rest
+  return $ d : ds
 typeCheckAll _ (ValueDeclaration _ _ _ _ : _) = error "Binders were not desugared"
 typeCheckAll moduleName (BindingGroupDeclaration vals : rest) = do
-  rethrow (("Error in binding group " ++ show (map fst vals) ++ ":\n") ++) $ do
+  d <- rethrow (("Error in binding group " ++ show (map fst vals) ++ ":\n") ++) $ do
     forM_ (map fst vals) $ \name ->
       valueIsNotDefined moduleName name
     tys <- typesOf moduleName vals
-    forM (zip (map fst vals) tys) $ \(name, ty) ->
+    vals' <- forM (zip (map fst vals) (map snd tys)) $ \(name, (val, ty)) -> do
       addValue moduleName name ty
-  typeCheckAll moduleName rest
-typeCheckAll moduleName (ExternDataDeclaration name kind : rest) = do
+      return (name, val)
+    return $ BindingGroupDeclaration vals'
+  ds <- typeCheckAll moduleName rest
+  return $ d : ds
+typeCheckAll moduleName (d@(ExternDataDeclaration name kind) : rest) = do
   env <- getEnv
   guardWith (show name ++ " is already defined") $ not $ M.member (moduleName, name) (types env)
   putEnv $ env { types = M.insert (moduleName, name) (kind, TypeSynonym) (types env) }
-  typeCheckAll moduleName rest
-typeCheckAll moduleName (ExternDeclaration name _ ty : rest) = do
+  ds <- typeCheckAll moduleName rest
+  return $ d : ds
+typeCheckAll moduleName (d@(ExternDeclaration importTy name _ ty) : rest) = do
   rethrow (("Error in foreign import declaration " ++ show name ++ ":\n") ++) $ do
     env <- getEnv
     kind <- kindOf moduleName ty
     guardWith "Expected kind *" $ kind == Star
     case M.lookup (moduleName, name) (names env) of
       Just _ -> throwError $ show name ++ " is already defined"
-      Nothing -> putEnv (env { names = M.insert (moduleName, name) (qualifyAllUnqualifiedNames moduleName env ty, Extern) (names env) })
-  typeCheckAll moduleName rest
-typeCheckAll moduleName (FixityDeclaration _ name : rest) = do
-  typeCheckAll moduleName rest
+      Nothing -> putEnv (env { names = M.insert (moduleName, name) (qualifyAllUnqualifiedNames moduleName env ty, Extern importTy) (names env) })
+  ds <- typeCheckAll moduleName rest
+  return $ d : ds
+typeCheckAll moduleName (d@(FixityDeclaration _ name) : rest) = do
+  ds <- typeCheckAll moduleName rest
   env <- getEnv
   guardWith ("Fixity declaration with no binding: " ++ name) $ M.member (moduleName, Op name) $ names env
-typeCheckAll currentModule (ImportDeclaration moduleName idents : rest) = do
+  return $ d : ds
+typeCheckAll currentModule (d@(ImportDeclaration moduleName idents) : rest) = do
   env <- getEnv
   rethrow errorMessage $ do
     guardWith ("Module " ++ show moduleName ++ " does not exist") $ moduleExists env
@@ -151,7 +166,8 @@
       Just idents' -> do
         shadowIdents (lefts idents') env
         shadowTypes (rights idents') env
-  typeCheckAll currentModule rest
+  ds <- typeCheckAll currentModule rest
+  return $ d : ds
  where errorMessage = (("Error in import declaration " ++ show moduleName ++ ":\n") ++)
        filterModule = filter ((== moduleName) . fst) . M.keys
        moduleExists env = not (null (filterModule (names env))) || not (null (filterModule (types env)))
@@ -185,11 +201,13 @@
        constructs (Function _ ty) pn = ty `constructs` pn
        constructs (TypeApp ty _) pn = ty `constructs` pn
        constructs fn _ = error $ "Invalid arguments to constructs: " ++ show fn
-
-qualifyAllUnqualifiedNames :: (Data d) => ModuleName -> Environment -> d -> d
-qualifyAllUnqualifiedNames mn env = everywhere (mkT go)
-  where
-  go :: Qualified ProperName -> Qualified ProperName
-  go qual = let (mn', pn') = canonicalizeType mn env qual
-            in Qualified (Just mn') pn'
-
+typeCheckAll moduleName (d@(TypeClassDeclaration _ _ _) : rest) = do
+  env <- getEnv
+  ds <- typeCheckAll moduleName rest
+  return $ qualifyAllUnqualifiedNames moduleName env d : ds
+typeCheckAll moduleName (d@(TypeInstanceDeclaration deps className ty _) : rest) = do
+  env <- getEnv
+  dictName <- Check . lift $ mkDictionaryValueName moduleName className ty
+  addTypeClassDictionaries (qualifyAllUnqualifiedNames moduleName env [TypeClassDictionaryInScope dictName className ty (Just deps)])
+  ds <- typeCheckAll moduleName rest
+  return $ qualifyAllUnqualifiedNames moduleName env d : ds
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
@@ -58,10 +58,10 @@
   unknowns _ = []
 
 kindOf :: ModuleName -> Type -> Check Kind
-kindOf moduleName ty = fmap (\(k, _, _) -> k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty
+kindOf moduleName ty = fmap (\(k, s) -> apply s k) . runSubst (SubstContext moduleName) $ starIfUnknown <$> infer ty
 
 kindsOf :: ModuleName -> ProperName -> [String] -> [Type] -> Check Kind
-kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, _, _) -> k)) . runSubst (SubstContext moduleName) $ do
+kindsOf moduleName name args ts = fmap (starIfUnknown . (\(k, s) -> apply s k)) . runSubst (SubstContext moduleName) $ do
   tyCon <- fresh
   kargs <- replicateM (length args) fresh
   let dict = (name, tyCon) : zip (map ProperName args) kargs
@@ -69,7 +69,7 @@
     solveTypes ts kargs tyCon
 
 kindsOfAll :: ModuleName -> [(ProperName, [String], [Type])] -> Check [Kind]
-kindsOfAll moduleName tys = fmap (map starIfUnknown . (\(ks, _, _) -> ks)) . runSubst (SubstContext moduleName) $ do
+kindsOfAll moduleName tys = fmap (map starIfUnknown . (\(ks, s) -> apply s ks)) . runSubst (SubstContext moduleName) $ do
   tyCons <- replicateM (length tys) fresh
   let dict = zipWith (\(name, _, _) tyCon -> (name, tyCon)) tys tyCons
   bindLocalTypeVariables moduleName dict $
@@ -107,7 +107,7 @@
   ks <- mapM infer args
   k <- infer ret
   k ~~ Star
-  forM ks (~~ Star)
+  forM_ ks (~~ Star)
   return Star
 infer (TypeVar v) = do
   moduleName <- substCurrentModule <$> ask
@@ -136,4 +136,9 @@
   k2 <- infer row
   k2 ~~ Row k1
   return $ Row k1
+infer (ConstrainedType deps ty) = do
+  mapM_ (infer . snd) deps
+  k <- infer ty
+  k ~~ Star
+  return Star
 infer _ = 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
@@ -19,12 +19,16 @@
 
 import Language.PureScript.Types
 import Language.PureScript.Kinds
+import Language.PureScript.Values
 import Language.PureScript.Names
 import Language.PureScript.Unknown
+import Language.PureScript.Declarations
 
 import Data.Data
 import Data.Maybe
 import Data.Monoid
+import Data.Generics (mkT, everywhere)
+
 import Control.Applicative
 import Control.Monad.State
 import Control.Monad.Error
@@ -34,7 +38,7 @@
 
 data NameKind
   = Value
-  | Extern
+  | Extern ForeignImportType
   | Alias ModuleName Ident
   | LocalVariable
   | DataConstructor deriving Show
@@ -51,10 +55,11 @@
   , types :: M.Map (ModuleName, ProperName) (Kind, TypeDeclarationKind)
   , dataConstructors :: M.Map (ModuleName, ProperName) (Type, NameKind)
   , typeSynonyms :: M.Map (ModuleName, ProperName) ([String], Type)
+  , typeClassDictionaries :: [TypeClassDictionaryInScope]
   } deriving (Show)
 
 emptyEnvironment :: Environment
-emptyEnvironment = Environment M.empty M.empty M.empty M.empty
+emptyEnvironment = Environment M.empty M.empty M.empty M.empty []
 
 bindNames :: (MonadState CheckState m) => M.Map (ModuleName, Ident) (Type, NameKind) -> m a -> m a
 bindNames newNames action = do
@@ -72,6 +77,17 @@
   modify $ \st -> st { checkEnv = (checkEnv st) { types = types . checkEnv $ orig } }
   return a
 
+withTypeClassDictionaries :: (MonadState CheckState m) => [TypeClassDictionaryInScope] -> m a -> m a
+withTypeClassDictionaries entries action = do
+  orig <- get
+  modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = entries ++ (typeClassDictionaries . checkEnv $ st) } }
+  a <- action
+  modify $ \st -> st { checkEnv = (checkEnv st) { typeClassDictionaries = typeClassDictionaries . checkEnv $ orig } }
+  return a
+
+getTypeClassDictionaries :: (Functor m, MonadState CheckState m) => m [TypeClassDictionaryInScope]
+getTypeClassDictionaries = typeClassDictionaries . checkEnv <$> get
+
 bindLocalVariables :: (Functor m, MonadState CheckState m) => ModuleName -> [(Ident, Type)] -> m a -> m a
 bindLocalVariables moduleName bindings action =
   bindNames (M.fromList $ flip map bindings $ \(name, ty) -> ((moduleName, name), (ty, LocalVariable))) action
@@ -106,11 +122,9 @@
   Just (_, DataAlias mn' pn') -> (mn', pn')
   _ -> (mn, nm)
 
-data AnyUnifiable where
-  AnyUnifiable :: forall t. (Unifiable t) => t -> AnyUnifiable
-
 data CheckState = CheckState { checkEnv :: Environment
                              , checkNextVar :: Int
+                             , checkNextDictName :: Int
                              }
 
 newtype Check a = Check { unCheck :: StateT CheckState (Either String) a }
@@ -127,7 +141,7 @@
 
 runCheck :: Check a -> Either String (a, Environment)
 runCheck c = do
-  (a, s) <- flip runStateT (CheckState emptyEnvironment 0) $ unCheck c
+  (a, s) <- flip runStateT (CheckState emptyEnvironment 0 0) $ unCheck c
   return (a, checkEnv s)
 
 guardWith :: (MonadError e m) => e -> Bool -> m ()
@@ -137,14 +151,19 @@
 rethrow :: (MonadError e m) => (e -> e) -> m a -> m a
 rethrow f = flip catchError $ \e -> throwError (f e)
 
+freshDictionaryName :: Check Int
+freshDictionaryName = do
+  n <- checkNextDictName <$> get
+  modify $ \s -> s { checkNextDictName = succ (checkNextDictName s) }
+  return n
+
 newtype Substitution = Substitution { runSubstitution :: forall t. (Unifiable t) => Unknown t -> t }
 
 instance Monoid Substitution where
   mempty = Substitution unknown
   s1 `mappend` s2 = Substitution $ \u -> apply s1 (apply s2 (unknown u))
 
-data SubstState = SubstState { substSubst :: Substitution
-                             , substFutureEscapeChecks :: [AnyUnifiable] }
+data SubstState = SubstState { substSubst :: Substitution }
 
 newtype SubstContext = SubstContext { substCurrentModule :: ModuleName } deriving (Show)
 
@@ -160,10 +179,13 @@
 liftCheck :: Check a -> Subst a
 liftCheck = Subst . lift . lift
 
-runSubst :: (Unifiable a) => SubstContext -> Subst a -> Check (a, Substitution, [AnyUnifiable])
+getSubstState :: Subst SubstState
+getSubstState = Subst . lift $ get
+
+runSubst :: SubstContext -> Subst a -> Check (a, Substitution)
 runSubst context subst = do
-  (a, s) <- flip runStateT (SubstState mempty []) . flip runReaderT context . unSubst $ subst
-  return (apply (substSubst s) a, substSubst s, substFutureEscapeChecks s)
+  (a, s) <- flip runStateT (SubstState mempty) . flip runReaderT context . unSubst $ subst
+  return (a, substSubst s)
 
 substituteWith :: (Typeable t) => (Unknown t -> t) -> Substitution
 substituteWith f = Substitution $ \u -> fromMaybe (unknown u) $ do
@@ -216,5 +238,9 @@
 fresh :: (Unifiable t) => Subst t
 fresh = unknown . Unknown <$> fresh'
 
-escapeCheckLater :: (Unifiable t) => t -> Subst ()
-escapeCheckLater t = Subst . modify $ \s -> s { substFutureEscapeChecks = AnyUnifiable t : substFutureEscapeChecks s  }
+qualifyAllUnqualifiedNames :: (Data d) => ModuleName -> Environment -> d -> d
+qualifyAllUnqualifiedNames mn env = everywhere (mkT go)
+  where
+  go :: Qualified ProperName -> Qualified ProperName
+  go qual = let (mn', pn') = canonicalizeType mn env qual
+            in Qualified (Just mn') pn'
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
@@ -20,10 +20,10 @@
 ) where
 
 import Data.List
-import Data.Maybe (isNothing, isJust, fromMaybe)
+import Data.Maybe (maybeToList, isNothing, isJust, fromMaybe)
 import qualified Data.Data as D
 import Data.Generics
-       (mkT, something, everywhere, everywhereBut, mkQ)
+       (mkM, everywhereM, everything, mkT, something, everywhere, mkQ)
 
 import Language.PureScript.Values
 import Language.PureScript.Types
@@ -129,7 +129,7 @@
   unifyRows' sd r [] (TUnknown u) = replace u (rowFromList (sd, r))
   unifyRows' ((name, ty):row) r others u@(TUnknown un) = do
     occursCheck un ty
-    forM row $ \(_, t) -> occursCheck un t
+    forM_ row $ \(_, t) -> occursCheck un t
     u' <- fresh
     u ~~ RCons name ty u'
     unifyRows' row r others u'
@@ -141,56 +141,106 @@
 typeConstructorsAreEqual :: Environment -> ModuleName -> Qualified ProperName -> Qualified ProperName -> Bool
 typeConstructorsAreEqual env moduleName = (==) `on` canonicalizeType moduleName env
 
-typesOf :: ModuleName -> [(Ident, Value)] -> Check [Type]
+typesOf :: ModuleName -> [(Ident, Value)] -> Check [(Ident, (Value, Type))]
 typesOf moduleName vals = do
-  (tys, sub, checks) <- runSubst (SubstContext moduleName) $ do
+  tys <- fmap (\(tys, s) -> map (\(ident, (val, ty)) -> (ident, (overTypes (apply s) val, apply s ty))) tys)
+         . runSubst (SubstContext moduleName) $ 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
     untypedNames <- replicateM (length untyped) fresh
     let untypedDict = zip (map fst untyped) untypedNames
-        dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ typedDict ++ untypedDict)
-    tys <- forM es $ \e -> do
-      ty <- case e of
-        (_, (val, Just ty)) -> do
+        dict = M.fromList (map (\(ident, ty) -> ((moduleName, ident), (ty, LocalVariable))) $ (map (id *** fst) typedDict) ++ untypedDict)
+    forM es $ \e -> do
+      triple@(_, (val, ty)) <- case e of
+        (ident, (val, Just (ty, checkType))) -> do
           kind <- liftCheck $ kindOf moduleName ty
           guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
           ty' <- replaceAllTypeSynonyms ty
-          bindNames dict $ check val ty'
-          return ty'
+          val' <- bindNames dict $ if checkType then check val ty' else return val
+          return (ident, (val', ty'))
         (ident, (val, Nothing)) -> do
-          ty <- bindNames dict $ infer val
+          TypedValue _ val' ty <- bindNames dict $ infer val
           ty ~~ fromMaybe (error "name not found in dictionary") (lookup ident untypedDict)
-          return ty
+          return (ident, (val', 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
-      return ty
-    return tys
-  forM tys $ flip (escapeCheck checks) sub
-  forM tys $ skolemEscapeCheck
-  return $ map (varIfUnknown . desaturateAllTypeSynonyms . setifyAll) tys
+      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'
+                   , varIfUnknown . desaturateAllTypeSynonyms . setifyAll $ ty))
 
-isTyped :: (Ident, Value) -> (Ident, (Value, Maybe Type))
-isTyped (name, TypedValue value ty) = (name, (value, Just ty))
+isTyped :: (Ident, Value) -> (Ident, (Value, Maybe (Type, Bool)))
+isTyped (name, TypedValue checkType value ty) = (name, (value, Just (ty, checkType)))
 isTyped (name, value) = (name, (value, Nothing))
 
-escapeCheck :: [AnyUnifiable] -> Type -> Substitution -> Check ()
-escapeCheck checks ty sub =
-  let
-    visibleUnknowns = nub $ unknowns ty
-  in
-    forM_ checks $ \c -> case c of
-      AnyUnifiable t -> do
-        let unsolvedUnknowns = nub . unknowns $ apply sub t
-        guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
+overTypes :: (Type -> Type) -> Value -> Value
+overTypes f = everywhere (mkT f)
 
+replaceTypeClassDictionaries :: ModuleName -> Value -> Check Value
+replaceTypeClassDictionaries mn = everywhereM (mkM go)
+  where
+  go (TypeClassDictionary constraint dicts) = entails mn dicts constraint
+  go other = return other
+
+entails :: ModuleName -> [TypeClassDictionaryInScope] -> (Qualified ProperName, Type) -> Check Value
+entails moduleName context goal@(className, ty) = do
+  env <- getEnv
+  case go env goal of
+    [] -> throwError $ "No " ++ show className ++ " instance found for " ++ prettyPrintType ty
+    (dict : _) -> return dict
+  where
+  go env (className', ty') =
+    [ mkDictionary (tcdName tcd) args
+    | tcd <- context
+    , qualify moduleName className' == qualify moduleName (tcdClassName tcd)
+    , subst <- maybeToList $ typeHeadsAreEqual moduleName env ty' (tcdInstanceType tcd)
+    , args <- solveSubgoals env subst (tcdDependencies tcd) ]
+  solveSubgoals _ _ Nothing = return Nothing
+  solveSubgoals env subst (Just subgoals) = do
+    dict <- mapM (go env) (replaceAllTypeVars subst subgoals)
+    return $ Just dict
+  mkDictionary fnName Nothing = Var (Qualified Nothing fnName)
+  mkDictionary fnName (Just args) = App (Var (Qualified Nothing fnName)) args
+
+typeHeadsAreEqual :: ModuleName -> Environment -> Type -> Type -> Maybe [(String, Type)]
+typeHeadsAreEqual _ _ String String = Just []
+typeHeadsAreEqual _ _ Number Number = Just []
+typeHeadsAreEqual _ _ Boolean Boolean = Just []
+typeHeadsAreEqual _ _ (Skolem s1) (Skolem s2) | s1 == s2 = Just []
+typeHeadsAreEqual _ _ (Array (TypeVar v)) (Array ty) = Just [(v, ty)]
+typeHeadsAreEqual _ _ (Array ty) (Array (TypeVar v)) = Just [(v, ty)]
+typeHeadsAreEqual m e (Array ty1) (Array ty2) = typeHeadsAreEqual m e ty1 ty2
+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 _ _ _ _ = Nothing
+
+escapeCheck :: Value -> Type -> Subst ()
+escapeCheck value ty = do
+  subst <- substSubst <$> getSubstState
+  let visibleUnknowns = nub $ unknowns $ apply subst ty
+  let allUnknowns = findAllTypes value
+  forM_ allUnknowns $ \t -> do
+    let unsolvedUnknowns = nub . unknowns $ apply subst t
+    guardWith "Escape check fails" $ null $ unsolvedUnknowns \\ visibleUnknowns
+
+findAllTypes :: Value -> [Type]
+findAllTypes = everything (++) (mkQ [] go)
+  where
+  go (TypedValue _ _ ty) = [ty]
+  go _ = []
+
 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."
+    Just _ -> throwError $ "Skolem variables cannot escape. Consider adding a type signature." ++ show ty
   where
     findSkolems (Skolem _) = return ()
     findSkolems _ = mzero
@@ -214,14 +264,6 @@
 replaceAllTypeVars :: (D.Data d) => [(String, Type)] -> d -> d
 replaceAllTypeVars = foldl' (\f (name, ty) -> replaceTypeVars name ty . f) id
 
-replaceTypeVars :: (D.Data d) => String -> Type -> d -> d
-replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replaceTypeVar)
-  where
-  replaceTypeVar (TypeVar v) | v == name = t
-  replaceTypeVar other = other
-  isShadowed (ForAll v _) | v == name = True
-  isShadowed _ = False
-
 replaceAllVarsWithUnknowns :: Type -> Subst Type
 replaceAllVarsWithUnknowns (ForAll ident ty) = replaceVarWithUnknown ident ty >>= replaceAllVarsWithUnknowns
 replaceAllVarsWithUnknowns ty = return ty
@@ -255,100 +297,105 @@
 ensureNoDuplicateProperties :: (MonadError String m) => [(String, Value)] -> m ()
 ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
 
-infer :: Value -> Subst Type
-infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ do
-  ty <- infer' val
-  escapeCheckLater ty
-  return ty
+infer :: Value -> Subst Value
+infer val = rethrow (\e -> "Error inferring type of term " ++ prettyPrintValue val ++ ":\n" ++ e) $ infer' val
 
-infer' :: Value -> Subst Type
-infer' (NumericLiteral _) = return Number
-infer' (StringLiteral _) = return String
-infer' (BooleanLiteral _) = return Boolean
+infer' :: Value -> Subst Value
+infer' v@(NumericLiteral _) = return $ TypedValue True v Number
+infer' v@(StringLiteral _) = return $ TypedValue True v String
+infer' v@(BooleanLiteral _) = return $ TypedValue True v Boolean
 infer' (ArrayLiteral vals) = do
-  ts <- mapM (infer) vals
+  ts <- mapM infer vals
   els <- fresh
-  forM_ ts $ \t -> els ~~ Array t
-  return els
+  forM_ ts $ \(TypedValue _ _ t) -> els ~~ Array t
+  return $ TypedValue True (ArrayLiteral ts) els
 infer' (Unary op val) = do
-  t <- infer val
-  inferUnary op t
+  v <- infer val
+  inferUnary op v
 infer' (Binary op left right) = do
-  t1 <- infer left
-  t2 <- infer right
-  inferBinary op t1 t2
+  v1 <- infer left
+  v2 <- infer right
+  inferBinary op v1 v2
 infer' (ObjectLiteral ps) = do
   ensureNoDuplicateProperties ps
   ts <- mapM (infer . snd) ps
-  let fields = zipWith (\(name, _) t -> (name, t)) ps ts
-  return $ Object $ rowFromList (fields, REmpty)
+  let fields = zipWith (\name (TypedValue _ _ t) -> (name, t)) (map fst ps) ts
+      ty = Object $ rowFromList (fields, REmpty)
+  return $ TypedValue True (ObjectLiteral (zip (map fst ps) ts)) ty
 infer' (ObjectUpdate o ps) = do
   ensureNoDuplicateProperties ps
   row <- fresh
-  newTys <- zipWith (\(name, _) t -> (name, t)) ps <$> mapM (infer . snd) ps
+  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
-  check o $ Object $ rowFromList (oldTys, row)
-  return $ Object $ rowFromList (newTys, row)
+  o' <- check o $ Object $ rowFromList (oldTys, row)
+  return $ TypedValue True (ObjectUpdate o' newVals) $ Object $ rowFromList (newTys, row)
 infer' (Indexer index val) = do
   el <- fresh
-  check index Number
-  check val (Array el)
-  return el
+  index' <- check index Number
+  val' <- check val (Array el)
+  return $ TypedValue True (Indexer (TypedValue True index' Number) (TypedValue True val' (Array el))) el
 infer' (Accessor prop val) = do
-  obj <- infer val
-  propTy <- inferProperty obj prop
+  typed@(TypedValue _ _ objTy) <- infer val
+  propTy <- inferProperty objTy prop
   case propTy of
     Nothing -> do
       field <- fresh
       rest <- fresh
-      obj `subsumes` Object (RCons prop field rest)
-      return field
-    Just ty -> return ty
+      objTy `subsumes` Object (RCons prop field rest)
+      return $ TypedValue True (Accessor prop typed) field
+    Just ty -> return $ TypedValue True (Accessor prop typed) ty
 infer' (Abs args ret) = do
   ts <- replicateM (length args) fresh
   moduleName <- substCurrentModule <$> ask
   bindLocalVariables moduleName (zip args ts) $ do
-    body <- infer' ret
-    return $ Function ts body
-infer' app@(App _ _) = do
-  let (f, argss) = unfoldApplication app
-  ft <- infer f
+    body@(TypedValue _ _ bodyTy) <- infer' ret
+    return $ TypedValue True (Abs args body) $ Function ts bodyTy
+infer' (App f args) = do
+  f'@(TypedValue _ _ ft) <- infer f
   ret <- fresh
-  checkFunctionApplications ft argss ret
-  return ret
+  app <- checkFunctionApplication f' ft args ret
+  return $ TypedValue True app ret
 infer' (Var var) = do
   moduleName <- substCurrentModule <$> ask
   ty <- lookupVariable moduleName var
-  replaceAllTypeSynonyms ty
+  ty' <- replaceAllTypeSynonyms ty
+  case ty' of
+    ConstrainedType constraints _ -> do
+      env <- getEnv
+      dicts <- getTypeClassDictionaries
+      return $ TypedValue True (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, _) <- checkBlock M.empty ret ss
+  (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
   guardWith "Block is missing a return statement" allCodePathsReturn
-  return ret
-infer' (Constructor c) = do
+  return $ TypedValue True (Block ss') ret
+infer' v@(Constructor c) = do
   env <- getEnv
   moduleName <- substCurrentModule `fmap` ask
   case M.lookup (qualify moduleName c) (dataConstructors env) of
     Nothing -> throwError $ "Constructor " ++ show c ++ " is undefined"
-    Just (ty, _) -> replaceAllTypeSynonyms ty
+    Just (ty, _) -> do ty' <- replaceAllTypeSynonyms ty
+                       return $ TypedValue True v ty'
 infer' (Case vals binders) = do
   ts <- mapM infer vals
   ret <- fresh
-  checkBinders ts ret binders
-  return ret
+  binders' <- checkBinders (map (\(TypedValue _ _ t) -> t) ts) ret binders
+  return $ TypedValue True (Case ts binders') ret
 infer' (IfThenElse cond th el) = do
-  check cond Boolean
-  t2 <- infer th
-  t3 <- infer el
+  cond' <- check cond Boolean
+  v2@(TypedValue _ _ t2) <- infer th
+  v3@(TypedValue _ _ t3) <- infer el
   t2 ~~ t3
-  return t2
-infer' (TypedValue val ty) = do
+  return $ TypedValue True (IfThenElse cond' v2 v3) t2
+infer' (TypedValue checkType val ty) = do
   moduleName <- substCurrentModule <$> ask
   kind <- liftCheck $ kindOf moduleName ty
   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
   ty' <- replaceAllTypeSynonyms ty
-  check val ty'
-  return ty'
+  val' <- if checkType then check val ty' else return val
+  return $ TypedValue True val' ty
 infer' _ = error "Invalid argument to infer"
 
 inferProperty :: Type -> String -> Subst (Maybe Type)
@@ -363,19 +410,21 @@
   inferProperty replaced prop
 inferProperty _ _ = return Nothing
 
-inferUnary :: UnaryOperator -> Type -> Subst Type
-inferUnary op val =
+inferUnary :: UnaryOperator -> Value -> Subst Value
+inferUnary op (TypedValue _ val valTy) =
   case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
-    (valTy, resTy) -> do
-      val ~~ valTy
-      return resTy
+    (valTy', resTy) -> do
+      valTy' ~~ valTy
+      return $ TypedValue True (Unary op val) resTy
+inferUnary _ _ = error "Invalid arguments to inferUnary"
 
-checkUnary :: UnaryOperator -> Value -> Type -> Subst ()
+checkUnary :: UnaryOperator -> Value -> Type -> Subst Value
 checkUnary op val res =
   case fromMaybe (error "Invalid operator") $ lookup op unaryOps of
     (valTy, resTy) -> do
       res ~~ resTy
-      check val valTy
+      val' <- check val valTy
+      return $ Unary op val'
 
 unaryOps :: [(UnaryOperator, (Type, Type))]
 unaryOps = [ (Negate, (Number, Number))
@@ -383,29 +432,32 @@
            , (BitwiseNot, (Number, Number))
            ]
 
-inferBinary :: BinaryOperator -> Type -> Type -> Subst Type
-inferBinary op left right | isEqualityTest op = do
-  left ~~ right
-  return Boolean
-inferBinary op left right =
+inferBinary :: BinaryOperator -> Value -> Value -> Subst Value
+inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) | isEqualityTest op = do
+  leftTy ~~ rightTy
+  return $ TypedValue True (Binary op left right) Boolean
+inferBinary op left@(TypedValue _ _ leftTy) right@(TypedValue _ _ rightTy) =
   case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
     (valTy, resTy) -> do
-      left ~~ valTy
-      right ~~ valTy
-      return resTy
+      leftTy ~~ valTy
+      rightTy ~~ valTy
+      return $ TypedValue True (Binary op left right) resTy
+inferBinary _ _ _ = error "Invalid arguments to inferBinary"
 
-checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst ()
+checkBinary :: BinaryOperator -> Value -> Value -> Type -> Subst Value
 checkBinary op left right res | isEqualityTest op = do
   res ~~ Boolean
-  t1 <- infer left
-  t2 <- infer right
+  left'@(TypedValue _ _ t1) <- infer left
+  right'@(TypedValue _ _ t2) <- infer right
   t1 ~~ t2
+  return $ Binary op left' right'
 checkBinary op left right res =
   case fromMaybe (error "Invalid operator") $ lookup op binaryOps of
     (valTy, resTy) -> do
       res ~~ resTy
-      check left valTy
-      check right valTy
+      left' <- check left valTy
+      right' <- check right valTy
+      return $ Binary op left' right'
 
 isEqualityTest :: BinaryOperator -> Bool
 isEqualityTest EqualTo = True
@@ -488,17 +540,20 @@
   m <- inferBinder val binder
   return $ M.insert name val m
 
-checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst ()
-checkBinders _ _ [] = return ()
+checkBinders :: [Type] -> Type -> [([Binder], Maybe Guard, Value)] -> Subst [([Binder], Maybe Guard, Value)]
+checkBinders _ _ [] = return []
 checkBinders nvals ret ((binders, grd, val):bs) = do
   moduleName <- substCurrentModule <$> ask
   m1 <- M.unions <$> zipWithM inferBinder nvals binders
-  bindLocalVariables moduleName (M.toList m1) $ do
-    check val ret
+  r <- bindLocalVariables moduleName (M.toList m1) $ do
+    val' <- check val ret
     case grd of
-      Nothing -> return ()
-      Just g -> check g Boolean
-  checkBinders nvals ret bs
+      Nothing -> return (binders, Nothing, val')
+      Just g -> do
+        g' <- check g Boolean
+        return (binders, Just g', val')
+  rs <- checkBinders nvals ret bs
+  return $ r : rs
 
 assignVariable :: Ident -> Subst ()
 assignVariable name = do
@@ -508,66 +563,70 @@
     Just (_, LocalVariable) -> throwError $ "Variable with name " ++ show name ++ " already exists."
     _ -> return ()
 
-checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type)
+checkStatement :: M.Map Ident Type -> Type -> Statement -> Subst (Bool, M.Map Ident Type, Statement)
 checkStatement mass _ (VariableIntroduction name val) = do
   assignVariable name
-  t <- infer val
-  return (False, M.insert name t mass)
+  val'@(TypedValue _ _ t) <- infer val
+  return (False, M.insert name t mass, VariableIntroduction name val')
 checkStatement mass _ (Assignment ident val) = do
-  t <- infer val
+  val'@(TypedValue _ _ t) <- infer val
   case M.lookup ident mass of
     Nothing -> throwError $ "No local variable with name " ++ show ident
     Just ty -> do t ~~ ty
-                  return (False, mass)
+                  return (False, mass, Assignment ident val')
 checkStatement mass ret (While val inner) = do
-  check val Boolean
-  (allCodePathsReturn, _) <- checkBlock mass ret inner
-  return (allCodePathsReturn, mass)
+  val' <- check val Boolean
+  (allCodePathsReturn, _, inner') <- checkBlock mass ret inner
+  return (allCodePathsReturn, mass, While val' inner')
 checkStatement mass ret (If ifst) = do
-  allCodePathsReturn <- checkIfStatement mass ret ifst
-  return (allCodePathsReturn, mass)
+  (allCodePathsReturn, ifst') <- checkIfStatement mass ret ifst
+  return (allCodePathsReturn, mass, If ifst')
 checkStatement mass ret (For ident start end inner) = do
   moduleName <- substCurrentModule <$> ask
   assignVariable ident
-  check start Number
-  check end Number
-  (allCodePathsReturn, _) <- bindLocalVariables moduleName [(ident, Number)] $ checkBlock mass ret inner
-  return (allCodePathsReturn, mass)
+  start' <- check start Number
+  end' <- check end Number
+  (allCodePathsReturn, _, inner') <- bindLocalVariables moduleName [(ident, Number)] $ checkBlock mass ret inner
+  return (allCodePathsReturn, mass, For ident start' end' inner')
 checkStatement mass ret (Return val) = do
-  check val ret
-  return (True, mass)
+  val' <- check val ret
+  return (True, mass, Return val')
 
-checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst Bool
+checkIfStatement :: M.Map Ident Type -> Type -> IfStatement -> Subst (Bool, IfStatement)
 checkIfStatement mass ret (IfStatement val thens Nothing) = do
-  check val Boolean
-  _ <- checkBlock mass ret thens
-  return False
+  val' <- check val Boolean
+  (_, _, thens') <- checkBlock mass ret thens
+  return (False, IfStatement val' thens' Nothing)
 checkIfStatement mass ret (IfStatement val thens (Just elses)) = do
-  check val Boolean
-  (allCodePathsReturn1, _) <- checkBlock mass ret thens
-  allCodePathsReturn2 <- checkElseStatement mass ret elses
-  return $ allCodePathsReturn1 && allCodePathsReturn2
+  val' <- check val Boolean
+  (allCodePathsReturn1, _, thens') <- checkBlock mass ret thens
+  (allCodePathsReturn2, elses') <- checkElseStatement mass ret elses
+  return (allCodePathsReturn1 && allCodePathsReturn2, IfStatement val' thens' (Just elses'))
 
-checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst Bool
-checkElseStatement mass ret (Else elses) = fst <$> checkBlock mass ret elses
-checkElseStatement mass ret (ElseIf ifst) = checkIfStatement mass ret ifst
+checkElseStatement :: M.Map Ident Type -> Type -> ElseStatement -> Subst (Bool, ElseStatement)
+checkElseStatement mass ret (Else elses) = do
+  (allCodePathsReturn, _, elses') <- checkBlock mass ret elses
+  return (allCodePathsReturn, Else elses')
+checkElseStatement mass ret (ElseIf ifst) = (id *** ElseIf) <$> checkIfStatement mass ret ifst
 
-checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type)
-checkBlock mass _ [] = return (False, mass)
+checkBlock :: M.Map Ident Type -> Type -> [Statement] -> Subst (Bool, M.Map Ident Type, [Statement])
+checkBlock mass _ [] = return (False, mass, [])
 checkBlock mass ret (s:ss) = do
   moduleName <- substCurrentModule <$> ask
-  (b1, mass1) <- checkStatement mass ret s
+  (b1, mass1, s') <- checkStatement mass ret s
   bindLocalVariables moduleName (M.toList mass1) $ case (b1, ss) of
-    (True, []) -> return (True, mass1)
+    (True, []) -> return (True, mass1, [s'])
     (True, _) -> throwError "Unreachable code"
-    (False, ss') -> checkBlock mass1 ret ss'
+    (False, ss') -> do
+      (b, m, ss'') <- checkBlock mass1 ret ss'
+      return (b, m, s':ss'')
 
 skolemize :: String -> Type -> Subst Type
 skolemize ident ty = do
   tsk <- Skolem <$> fresh'
   return $ replaceTypeVars ident tsk ty
 
-check :: Value -> Type -> Subst ()
+check :: Value -> Type -> Subst Value
 check val ty = rethrow errorMessage $ check' val ty
   where
   errorMessage msg =
@@ -578,65 +637,87 @@
     ":\n" ++
     msg
 
-check' :: Value -> Type -> Subst ()
+check' :: Value -> Type -> Subst Value
 check' val (ForAll idents ty) = do
   sk <- skolemize idents ty
   check val sk
+check' val (ConstrainedType constraints ty) = do
+  env <- getEnv
+  moduleName <- substCurrentModule <$> ask
+  dictNames <- flip mapM constraints $ \(Qualified _ (ProperName className), _) -> do
+    n <- liftCheck freshDictionaryName
+    return $ Ident $ "__dict_" ++ className ++ "_" ++ show n
+  val' <- withTypeClassDictionaries (zipWith (\name (className, instanceTy) -> TypeClassDictionaryInScope name className instanceTy Nothing) dictNames (qualifyAllUnqualifiedNames moduleName env constraints)) $ check val ty
+  return $ Abs dictNames val'
 check' val u@(TUnknown _) = do
-  ty <- infer val
+  val'@(TypedValue _ _ ty) <- infer val
   -- Don't unify an unknown with an inferred polytype
   ty' <- replaceAllVarsWithUnknowns ty
   ty' ~~ u
-check' (NumericLiteral _) Number = return ()
-check' (StringLiteral _) String = return ()
-check' (BooleanLiteral _) Boolean = return ()
+  return val'
+check' v@(NumericLiteral _) Number = return v
+check' v@(StringLiteral _) String = return v
+check' v@(BooleanLiteral _) Boolean = return v
 check' (Unary op val) ty = checkUnary op val ty
 check' (Binary op left right) ty = checkBinary op left right ty
-check' (ArrayLiteral vals) (Array ty) = forM_ vals (\val -> check val ty)
-check' (Indexer index vals) ty = check index Number >> check vals (Array ty)
+check' (ArrayLiteral vals) (Array ty) = ArrayLiteral <$> forM vals (\val -> check val ty)
+check' (Indexer index vals) ty = do
+  index' <- check index Number
+  vals' <- check vals (Array ty)
+  return $ Indexer index' vals'
 check' (Abs args ret) (Function argTys retTy) = do
   moduleName <- substCurrentModule <$> ask
   guardWith "Incorrect number of function arguments" (length args == length argTys)
-  bindLocalVariables moduleName (zip args argTys) $ check ret retTy
-check' app@(App _ _) ret = do
-  let (f, argss) = unfoldApplication app
-  ft <- infer f
-  checkFunctionApplications ft argss ret
+  ret' <- bindLocalVariables moduleName (zip args argTys) $ check ret retTy
+  return $ Abs args ret'
+check' (App f args) ret = do
+  f'@(TypedValue _ _ ft) <- infer f
+  app <- checkFunctionApplication f' ft args ret
+  return $ app
 check' (Var var) ty = do
   moduleName <- substCurrentModule <$> ask
   ty1 <- lookupVariable moduleName var
   repl <- replaceAllTypeSynonyms ty1
   repl `subsumes` ty
-check' (TypedValue val ty1) ty2 = do
+  return $ Var var
+check' (TypedValue checkType val ty1) ty2 = do
   moduleName <- substCurrentModule <$> ask
   kind <- liftCheck $ kindOf moduleName ty1
   guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
   ty1 `subsumes` ty2
-  check val ty1
+  val' <- if checkType then check val ty1 else return val
+  return $ TypedValue True val' ty1
 check' (Case vals binders) ret = do
-  ts <- mapM infer vals
-  checkBinders ts ret binders
+  vals' <- mapM infer vals
+  let ts = map (\(TypedValue _ _ t) -> t) vals'
+  binders' <- checkBinders ts ret binders
+  return $ Case vals' binders'
 check' (IfThenElse cond th el) ty = do
-  check cond Boolean
-  check th ty
-  check el ty
+  cond' <- check cond Boolean
+  th' <- check th ty
+  el' <- check el ty
+  return $ IfThenElse cond' th' el'
 check' (ObjectLiteral ps) (Object row) = do
   ensureNoDuplicateProperties ps
-  checkProperties ps row False
+  ps' <- checkProperties ps row False
+  return $ ObjectLiteral ps'
 check' (ObjectUpdate obj ps) (Object row) = do
   ensureNoDuplicateProperties ps
   us <- zip (map fst ps) <$> replicateM (length ps) fresh
   let (propsToCheck, rest) = rowToList row
       propsToRemove = map fst ps
       remainingProps = filter (\(p, _) -> p `notElem` propsToRemove) propsToCheck
-  check obj (Object (rowFromList (us ++ remainingProps, rest)))
-  checkProperties ps row True
+  obj' <- check obj (Object (rowFromList (us ++ remainingProps, rest)))
+  ps' <- checkProperties ps row True
+  return $ ObjectUpdate obj' ps'
 check' (Accessor prop val) ty = do
   rest <- fresh
-  check val (Object (RCons prop ty rest))
+  val' <- check val (Object (RCons prop ty rest))
+  return $ Accessor prop val'
 check' (Block ss) ret = do
-  (allCodePathsReturn, _) <- checkBlock M.empty ret ss
+  (allCodePathsReturn, _, ss') <- checkBlock M.empty ret ss
   guardWith "Block is missing a return statement" allCodePathsReturn
+  return $ Block ss'
 check' (Constructor c) ty = do
   env <- getEnv
   moduleName <- substCurrentModule <$> ask
@@ -645,95 +726,72 @@
     Just (ty1, _) -> do
       repl <- replaceAllTypeSynonyms ty1
       repl `subsumes` ty
+      return $ Constructor c
 check' val (SaturatedTypeSynonym name args) = do
   ty <- expandTypeSynonym name args
   check val ty
 check' val ty = throwError $ prettyPrintValue val ++ " does not have type " ++ prettyPrintType ty
 
-checkProperties :: [(String, Value)] -> Type -> Bool -> Subst ()
+checkProperties :: [(String, Value)] -> Type -> Bool -> Subst [(String, Value)]
 checkProperties ps row lax = let (ts, r') = rowToList row in go ps ts r' where
-  go [] [] REmpty = return ()
-  go [] [] u@(TUnknown _) = u ~~ REmpty
-  go [] [] (Skolem _) | lax = return ()
-  go [] ((p, _): _) _ | lax = return ()
+  go [] [] REmpty = return []
+  go [] [] u@(TUnknown _) = do u ~~ REmpty
+                               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
   go ((p,v):ps') [] u@(TUnknown _) = do
-    ty <- infer v
+    v'@(TypedValue _ _ ty) <- infer v
     rest <- fresh
     u ~~ RCons p ty rest
-    go ps' [] rest
+    ps'' <- go ps' [] rest
+    return $ (p, v') : ps''
   go ((p,v):ps') ts r =
     case lookup p ts of
       Nothing -> do
-        ty <- infer v
+        v'@(TypedValue _ _ ty) <- infer v
         rest <- fresh
         r ~~ RCons p ty rest
-        go ps' ts rest
+        ps'' <- go ps' ts rest
+        return $ (p, v') : ps''
       Just ty -> do
-        check v ty
-        go ps' (delete (p, ty) ts) r
+        v' <- check v ty
+        ps'' <- go ps' (delete (p, ty) ts) r
+        return $ (p, v') : ps''
   go _ _ _ = throwError $ prettyPrintValue (ObjectLiteral ps) ++ " does not have type " ++ prettyPrintType (Object row)
 
-unfoldApplication :: Value -> (Value, [[Value]])
-unfoldApplication = go []
-  where
-  go argss (App f args) = go (args:argss) f
-  go argss f = (f, argss)
-
-checkFunctionApplications :: Type -> [[Value]] -> Type -> Subst ()
-checkFunctionApplications _ [] _ = error "Nullary function application"
-checkFunctionApplications fnTy [args] ret = checkFunctionApplication fnTy args ret
-checkFunctionApplications fnTy (args:argss) ret = do
-  argTys <- mapM (infer) args
-  f <- inferFunctionApplication fnTy argTys
-  checkFunctionApplications f argss ret
-
-checkFunctionApplication :: Type -> [Value] -> Type -> Subst ()
-checkFunctionApplication fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fnTy args ret
+checkFunctionApplication :: Value -> Type -> [Value] -> Type -> Subst Value
+checkFunctionApplication fn fnTy args ret = rethrow errorMessage $ checkFunctionApplication' fn fnTy args ret
   where
   errorMessage msg = "Error applying function of type "
     ++ prettyPrintType fnTy
     ++ " to arguments " ++ intercalate ", " (map prettyPrintValue args)
-    ++ ", expecting value of type "
-    ++ prettyPrintType ret ++ ":\n" ++ msg
-
-inferFunctionApplication :: Type -> [Type] -> Subst Type
-inferFunctionApplication (Function argTys retTy) args = do
-  guardWith "Incorrect number of function arguments" (length args == length argTys)
-  zipWithM subsumes args argTys
-  return retTy
-inferFunctionApplication (ForAll ident ty) args = do
-  replaced <- replaceVarWithUnknown ident ty
-  inferFunctionApplication replaced args
-inferFunctionApplication u@(TUnknown _) args = do
-
-  ret <- fresh
-  args' <- mapM replaceAllVarsWithUnknowns args
-  u ~~ Function args' ret
-  return ret
-inferFunctionApplication (SaturatedTypeSynonym name tyArgs) args  = do
-  ty <- expandTypeSynonym name tyArgs
-  inferFunctionApplication ty args
-inferFunctionApplication fnTy args = throwError $ "Cannot apply function of type "
-  ++ prettyPrintType fnTy
-  ++ " to argument(s) of type(s) " ++ intercalate ", " (map prettyPrintType args)
+    ++ ":\n" ++ msg
 
-checkFunctionApplication' :: Type -> [Value] -> Type -> Subst ()
-checkFunctionApplication' (Function argTys retTy) args ret = do
+checkFunctionApplication' :: Value -> Type -> [Value] -> Type -> Subst Value
+checkFunctionApplication' fn (Function argTys retTy) args ret = do
   guardWith "Incorrect number of function arguments" (length args == length argTys)
-  zipWithM (check) args argTys
+  args' <- zipWithM check args argTys
   retTy `subsumes` ret
-checkFunctionApplication' (ForAll ident ty) args ret = do
+  return $ App fn args'
+checkFunctionApplication' fn (ForAll ident ty) args ret = do
   replaced <- replaceVarWithUnknown ident ty
-  checkFunctionApplication replaced args ret
-checkFunctionApplication' u@(TUnknown _) args ret = do
-  tyArgs <- mapM (\arg -> infer arg >>= replaceAllVarsWithUnknowns) args
-  u ~~ Function tyArgs ret
-checkFunctionApplication' (SaturatedTypeSynonym name tyArgs) args ret = do
+  checkFunctionApplication fn replaced args ret
+checkFunctionApplication' fn u@(TUnknown _) args ret = do
+  args' <- mapM (\arg -> infer arg >>= \(TypedValue _ v t) -> TypedValue True v <$> replaceAllVarsWithUnknowns t) args
+  let tys = map (\(TypedValue _ _ t) -> t) args'
+  u ~~ Function tys ret
+  return $ App fn args'
+checkFunctionApplication' fn (SaturatedTypeSynonym name tyArgs) args ret = do
   ty <- expandTypeSynonym name tyArgs
-  checkFunctionApplication' ty args ret
-checkFunctionApplication' fnTy args ret = throwError $ "Applying a function of type "
+  checkFunctionApplication fn ty args ret
+checkFunctionApplication' fn (ConstrainedType constraints fnTy) args ret = do
+  env <- getEnv
+  dicts <- getTypeClassDictionaries
+  moduleName <- substCurrentModule <$> ask
+  checkFunctionApplication' (App fn (map (flip TypeClassDictionary dicts) (qualifyAllUnqualifiedNames moduleName env constraints))) fnTy args ret
+checkFunctionApplication' _ fnTy args ret = throwError $ "Applying a function of type "
   ++ prettyPrintType fnTy
   ++ " to argument(s) " ++ intercalate ", " (map prettyPrintValue args)
   ++ " does not yield a value of type " ++ prettyPrintType ret ++ "."
@@ -743,7 +801,7 @@
   replaced <- replaceVarWithUnknown ident ty1
   replaced `subsumes` ty2
 subsumes (Function args1 ret1) (Function args2 ret2) = do
-  zipWithM subsumes args2 args1
+  zipWithM_ subsumes args2 args1
   ret1 `subsumes` ret2
 subsumes ty1 ty2 = ty1 ~~ ty2
 
diff --git a/src/Language/PureScript/Types.hs b/src/Language/PureScript/Types.hs
--- a/src/Language/PureScript/Types.hs
+++ b/src/Language/PureScript/Types.hs
@@ -17,6 +17,8 @@
 module Language.PureScript.Types where
 
 import Data.Data
+import Data.Generics (mkT, mkQ, everywhereBut)
+
 import Language.PureScript.Names
 import Language.PureScript.Unknown (Unknown(..))
 
@@ -33,6 +35,7 @@
   | TypeApp Type Type
   | SaturatedTypeSynonym (Qualified ProperName) [Type]
   | ForAll String Type
+  | ConstrainedType [(Qualified ProperName, Type)] Type
   | Skolem Int
   | REmpty
   | RCons String Type Type deriving (Show, Eq, Data, Typeable)
@@ -64,3 +67,11 @@
 
 unit :: Type
 unit = Object REmpty
+
+replaceTypeVars :: (Data d) => String -> Type -> d -> d
+replaceTypeVars name t = everywhereBut (mkQ False isShadowed) (mkT replaceTypeVar)
+  where
+  replaceTypeVar (TypeVar v) | v == name = t
+  replaceTypeVar other = other
+  isShadowed (ForAll v _) | v == name = True
+  isShadowed _ = False
diff --git a/src/Language/PureScript/Values.hs b/src/Language/PureScript/Values.hs
--- a/src/Language/PureScript/Values.hs
+++ b/src/Language/PureScript/Values.hs
@@ -71,14 +71,21 @@
   | Block [Statement]
   | Constructor (Qualified ProperName)
   | Case [Value] [([Binder], Maybe Guard, Value)]
-  | TypedValue Value Type
-  | Do Value [DoNotationElement] deriving (Show, Data, Typeable)
+  | TypedValue Bool Value Type
+  | Do [DoNotationElement]
+  | TypeClassDictionary (Qualified ProperName, Type) [TypeClassDictionaryInScope] deriving (Show, Data, Typeable)
 
+data TypeClassDictionaryInScope
+  = TypeClassDictionaryInScope { tcdName :: Ident
+                               , tcdClassName :: Qualified ProperName
+                               , tcdInstanceType :: Type
+                               , tcdDependencies :: Maybe [(Qualified ProperName, Type)]
+                               } deriving (Show, Data, Typeable)
+
 data DoNotationElement
   = DoNotationValue Value
   | DoNotationBind Binder Value
-  | DoNotationLet Binder Value
-  | DoNotationReturn Value deriving (Show, Data, Typeable)
+  | DoNotationLet Binder Value deriving (Show, Data, Typeable)
 
 data Statement
   = VariableIntroduction Ident Value