diff --git a/lambda-calculator.cabal b/lambda-calculator.cabal
index d0071b0e7f56c86d7e2816470485e18f64d7e60a..9fd17c5a42effe0425f3ed7d086a63877d7b4378 100644
--- a/lambda-calculator.cabal
+++ b/lambda-calculator.cabal
@@ -24,8 +24,10 @@ library
 
                        Language.SystemF,
                        Language.SystemF.Expression,
-                       Language.SystemF.Parser
+                       Language.SystemF.Parser,
+                       Language.SystemF.TypeCheck
   build-depends:       base <= 5,
+                       containers,
                        parsec
   default-language:    Haskell2010
 
@@ -58,9 +60,11 @@ test-suite lambda-calculus-test
 
                        Language.SystemFSpec,
                        Language.SystemF.ExpressionSpec,
-                       Language.SystemF.ParserSpec
+                       Language.SystemF.ParserSpec,
+                       Language.SystemF.TypeCheckSpec
   build-depends:       base <= 5,
                        lambda-calculator,
+                       containers,
                        hspec,
                        HUnit
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N
diff --git a/src/Language/SystemF/Expression.hs b/src/Language/SystemF/Expression.hs
index ece7e15c896c9210e5c6c828e73226d053739e6b..0bfa1675d821268730be95772b481e69767106ef 100644
--- a/src/Language/SystemF/Expression.hs
+++ b/src/Language/SystemF/Expression.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE FlexibleInstances #-}
 module Language.SystemF.Expression where
 
 import Data.Monoid
diff --git a/src/Language/SystemF/TypeCheck.hs b/src/Language/SystemF/TypeCheck.hs
new file mode 100644
index 0000000000000000000000000000000000000000..76616f967c36a58625cf7b7721a46957e72c9c13
--- /dev/null
+++ b/src/Language/SystemF/TypeCheck.hs
@@ -0,0 +1,41 @@
+module Language.SystemF.TypeCheck where
+
+import Data.Map
+import Prelude hiding (lookup)
+
+import Language.SystemF.Expression
+
+type UniqueSupply n = [n]
+type Context n t = Map n t
+
+typecheck :: (Ord n, Eq t)
+          => UniqueSupply t 
+          -> Context n (Ty t)
+          -> SystemFExpr n t 
+          -> Either String (Ty t)
+typecheck uniqs ctx (Var v)        = tcVar uniqs ctx v
+typecheck uniqs ctx (Abs n t body) = tcAbs uniqs ctx n t body
+typecheck _     _   _       = undefined
+
+tcVar :: (Ord n, Eq t)
+      => UniqueSupply t
+      -> Context n (Ty t)
+      -> n
+      -> Either String (Ty t)
+tcVar uniqs ctx var = maybe (TyVar <$> unique uniqs) return (lookup var ctx)
+
+tcAbs :: (Ord n, Eq t)
+      => UniqueSupply t
+      -> Context n (Ty t)
+      -> n
+      -> Ty t
+      -> SystemFExpr n t
+      -> Either String (Ty t)
+tcAbs uniqs ctx name ty body = TyArrow ty <$> typecheck uniqs ctx' body
+  where ctx' = insert name ty ctx
+
+-- Utilities
+unique :: UniqueSupply t
+       -> Either String t
+unique (u:_) = return u
+unique _     = fail "Unique supply ran out"
diff --git a/test/Language/SystemF/TypeCheckSpec.hs b/test/Language/SystemF/TypeCheckSpec.hs
new file mode 100644
index 0000000000000000000000000000000000000000..2776892691b47ea423d78d24fc27af289307015f
--- /dev/null
+++ b/test/Language/SystemF/TypeCheckSpec.hs
@@ -0,0 +1,22 @@
+module Language.SystemF.TypeCheckSpec (spec) where
+
+import Data.Map
+
+import Test.Hspec
+
+import Language.SystemF.Expression
+import Language.SystemF.TypeCheck
+
+tc uniqs ctx = typecheck uniqs (fromList ctx)
+
+spec :: Spec
+spec = describe "typecheck" $ do
+  it "typechecks simple variables in context" $
+    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")
+
+  it "typechecks simple variables not in context" $ 
+    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")
+
+  it "typechecks simple abstractions" $
+    tc [] [] (Abs "x" (TyVar "A") (Var "x")) 
+      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))