diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -2,6 +2,7 @@
 
 import Data.Version
 
+import Data.Semigroup
 import Options.Applicative hiding (ParseError)
 import System.Console.Shell
 import System.Console.Shell.ShellMonad
diff --git a/lambda-calculator.cabal b/lambda-calculator.cabal
--- a/lambda-calculator.cabal
+++ b/lambda-calculator.cabal
@@ -1,5 +1,5 @@
 name:                lambda-calculator
-version:             1.1.1
+version:             2.0.0
 synopsis:            A lambda calculus interpreter
 description:         Please see README.md
 homepage:            https://github.com/sgillespie/lambda-calculus#readme
@@ -24,8 +24,10 @@
 
                        Language.SystemF,
                        Language.SystemF.Expression,
-                       Language.SystemF.Parser
-  build-depends:       base <= 5,
+                       Language.SystemF.Parser,
+                       Language.SystemF.TypeCheck
+  build-depends:       base >= 4.9 && < 5,
+                       containers,
                        parsec
   default-language:    Haskell2010
 
@@ -34,9 +36,9 @@
   main-is:             Main.hs
   other-modules:       Paths_lambda_calculator
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N
-  build-depends:       base,
+  build-depends:       base >= 4.9,
                        lambda-calculator,
-                       optparse-applicative < 0.13,
+                       optparse-applicative >= 0.13,
                        Shellac,
                        Shellac-readline
   default-language:    Haskell2010
@@ -58,9 +60,11 @@
 
                        Language.SystemFSpec,
                        Language.SystemF.ExpressionSpec,
-                       Language.SystemF.ParserSpec
-  build-depends:       base <= 5,
+                       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
--- 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
@@ -19,6 +18,7 @@
 data Ty name
   = TyVar name                  -- Type variable (T)
   | TyArrow (Ty name) (Ty name) -- Type arrow    (T -> U)
+  | TyForAll name (Ty name)     -- Universal type (forall T. X)
   deriving (Eq, Show)
 
 -- Pretty printing
@@ -94,6 +94,7 @@
       -> PDoc String
 pprTy pdoc space (TyVar n) = prettyPrint n `add` pdoc
 pprTy pdoc space (TyArrow a b) = pprTyArrow pdoc space a b
+pprTy pdoc _     (TyForAll n t) =  pprTyForAll pdoc n t
 
 pprTyArrow :: PrettyPrint n
            => PDoc String
@@ -113,6 +114,14 @@
 pprTyArrow' space a b = a <> arrow <> b
   where arrow | space     = " -> " `add` empty
               | otherwise = "->" `add` empty
+
+pprTyForAll :: PrettyPrint n
+            => PDoc String
+            -> n
+            -> Ty n
+            -> PDoc String
+pprTyForAll pdoc n t = prefix <> prettyPrint t `add` pdoc
+  where prefix = between (prettyPrint n `add` empty) "forall " ". " empty
 
 -- Pretty print a type abstraction
 pprTAbs :: (PrettyPrint n, PrettyPrint t)
diff --git a/src/Language/SystemF/TypeCheck.hs b/src/Language/SystemF/TypeCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/SystemF/TypeCheck.hs
@@ -0,0 +1,119 @@
+module Language.SystemF.TypeCheck where
+
+import Data.Map
+import Prelude hiding (lookup)
+
+import Language.Lambda.Util.PrettyPrint
+import Language.SystemF.Expression
+
+type UniqueSupply n = [n]
+type Context n t = Map n t
+
+typecheck :: (Ord n, Eq n, PrettyPrint n)
+          => UniqueSupply n 
+          -> Context n (Ty n)
+          -> SystemFExpr n n 
+          -> Either String (Ty n)
+typecheck uniqs ctx (Var v)        = tcVar uniqs ctx v
+typecheck uniqs ctx (Abs n t body) = tcAbs uniqs ctx n t body
+typecheck uniqs ctx (App e1 e2)    = tcApp uniqs ctx e1 e2
+typecheck uniqs ctx (TyAbs t body) = tcTyAbs uniqs ctx t body
+typecheck uniqs ctx (TyApp e ty)   = tcTyApp uniqs ctx e ty
+
+tcVar :: (Ord n, Eq n, PrettyPrint n)
+      => UniqueSupply n
+      -> Context n (Ty n)
+      -> n
+      -> Either String (Ty n)
+tcVar uniqs ctx var = maybe (TyVar <$> unique uniqs) return (lookup var ctx)
+
+tcAbs :: (Ord n, Eq n, PrettyPrint n)
+      => UniqueSupply n
+      -> Context n (Ty n)
+      -> n
+      -> Ty n
+      -> SystemFExpr n n
+      -> Either String (Ty n)
+tcAbs uniqs ctx name ty body = TyArrow ty <$> typecheck uniqs ctx' body
+  where ctx' = insert name ty ctx
+
+tcApp :: (Ord n, Eq n, PrettyPrint n)
+      => UniqueSupply n
+      -> Context n (Ty n)
+      -> SystemFExpr n n
+      -> SystemFExpr n n
+      -> Either String (Ty n)
+tcApp uniqs ctx e1 e2 = do
+    t1 <- typecheck uniqs ctx e1
+    t2 <- typecheck uniqs ctx e2
+
+    -- Unwrap t1; Should be (t2 -> *)
+    (t2', t3) <- either genMismatchVar return (arrow t1)
+
+    if t2' == t2
+      then return t3
+      else Left $ tyMismatchMsg (TyArrow t2 t3) (TyArrow t1 t3)
+
+  where genMismatchVar expected = tyMismatchMsg expected <$> unique uniqs >>= Left
+        arrow (TyArrow t1 t2) = return (t1, t2)
+        arrow t               = Left t
+
+tcTyAbs :: (Ord n, Eq n, PrettyPrint n)
+        => UniqueSupply n
+        -> Context n (Ty n)
+        -> n
+        -> SystemFExpr n n
+        -> Either String (Ty n)
+tcTyAbs uniqs ctx ty body = TyForAll ty <$> typecheck uniqs ctx' body
+  where ctx' = insert ty (TyVar ty) ctx
+
+tcTyApp :: (Ord n, Eq n, PrettyPrint n)
+        => UniqueSupply n
+        -> Context n (Ty n)
+        -> SystemFExpr n n
+        -> Ty n
+        -> Either String (Ty n)
+tcTyApp uniqs ctx (TyAbs t expr) ty = typecheck uniqs ctx expr'
+  where expr' = sub t ty expr
+tcTyApp uniqs ctx expr ty = typecheck uniqs ctx expr
+
+-- Utilities
+unique :: UniqueSupply t
+       -> Either String t
+unique (u:_) = return u
+unique _     = fail "Unique supply ran out"
+
+sub :: Eq n
+    => n
+    -> Ty n
+    -> SystemFExpr n n
+    -> SystemFExpr n n
+sub name ty (App e1 e2)   = App (sub name ty e1) (sub name ty e2)
+sub name ty (Abs n ty' e) = Abs n (subTy name ty ty') (sub name ty e)
+sub name ty (TyAbs ty' e) = TyAbs ty' (sub name ty e) 
+sub name ty (TyApp e ty') = TyApp (sub name ty e) (subTy name ty ty')
+sub name ty expr = expr
+
+subTy :: Eq n
+      => n
+      -> Ty n
+      -> Ty n
+      -> Ty n
+subTy name ty (TyArrow t1 t2) 
+  = TyArrow (subTy name ty t1) (subTy name ty t2)
+subTy name ty ty'@(TyVar name') 
+  | name == name' = ty
+  | otherwise     = ty'
+subTy name t1 t2@(TyForAll name' t2') 
+  | name == name' = t2
+  | otherwise     = TyForAll name' (subTy name t2 t2')
+
+
+tyMismatchMsg :: (PrettyPrint t, PrettyPrint t')
+              => t
+              -> t'
+              -> String
+tyMismatchMsg expected actual = "Couldn't match expected type " ++
+                                prettyPrint expected ++
+                                " with actual type " ++
+                                prettyPrint actual
diff --git a/test/Language/SystemF/ExpressionSpec.hs b/test/Language/SystemF/ExpressionSpec.hs
--- a/test/Language/SystemF/ExpressionSpec.hs
+++ b/test/Language/SystemF/ExpressionSpec.hs
@@ -58,6 +58,9 @@
   it "print simple arrow types" $
     prettyPrint (TyArrow (TyVar "A") (TyVar "B")) `shouldBe` "A -> B"
 
+  it "prints simple forall types" $
+    prettyPrint (TyForAll "X" (TyVar "X")) `shouldBe` "forall X. X"
+
   it "prints chained arrow types" $
     prettyPrint (TyArrow (TyVar "X") (TyArrow (TyVar "Y") (TyVar "Z")))
       `shouldBe` "X -> Y -> Z"
@@ -65,3 +68,14 @@
   it "prints nested arrow types" $
     prettyPrint (TyArrow (TyArrow (TyVar "T") (TyVar "U")) (TyVar "V"))
       `shouldBe` "(T -> U) -> V"
+
+  it "prints complex forall types" $
+    prettyPrint (TyForAll "A" (TyArrow (TyVar "A") (TyVar "A")))
+      `shouldBe` "forall A. A -> A"
+
+  it "prints nested forall types" $
+    prettyPrint (TyForAll "W" 
+                  (TyForAll "X" 
+                    (TyArrow (TyVar "W") (TyArrow (TyVar "X") (TyVar "Y")))))
+      `shouldBe` "forall W. forall X. W -> X -> Y"
+
diff --git a/test/Language/SystemF/TypeCheckSpec.hs b/test/Language/SystemF/TypeCheckSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/Language/SystemF/TypeCheckSpec.hs
@@ -0,0 +1,75 @@
+module Language.SystemF.TypeCheckSpec (spec) where
+
+import Data.Either
+import Data.Map
+
+import Test.Hspec
+
+import Language.Lambda.Util.PrettyPrint
+import Language.SystemF.Expression
+import Language.SystemF.TypeCheck
+
+tc :: (Ord n, Eq n, PrettyPrint n)
+          => UniqueSupply n 
+          -> [(n, Ty n)]
+          -> SystemFExpr n n 
+          -> Either String (Ty n)
+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"))
+
+  it "typechecks simple applications" $ do
+    let ctx = [
+          ("f", TyArrow (TyVar "T") (TyVar "U")),
+          ("a", TyVar "T")
+          ]
+
+    tc [] ctx (App (Var "f") (Var "a")) `shouldBe` Right (TyVar "U")
+
+  it "apply variable to variable fails" $ do
+    let ctx = [
+          ("a", TyVar "A"),
+          ("b", TyVar "B")
+          ]
+
+    tc ["C"] ctx (App (Var "a") (Var "b")) 
+      `shouldSatisfy` isLeft
+
+  it "apply arrow to variable of wrong type fails" $ do
+    let ctx = [
+          ("f", TyArrow (TyVar "F") (TyVar "G")),
+          ("b", TyVar "B")
+          ]
+
+    tc [] ctx (App (Var "f") (Var "b")) `shouldSatisfy` isLeft
+
+  it "typechecks simple type abstractions" $
+    tc ["A"] [] (TyAbs "X" (Var "x")) `shouldBe` Right (TyForAll "X" (TyVar "A"))
+
+  it "typechecks type abstractions with simple abstraction" $
+    tc [] [] (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) 
+      `shouldBe` Right (TyForAll "X" (TyArrow (TyVar "X") (TyVar "X")))
+
+  it "typechecks type abstractions with application" $
+    tc [] [("y", TyVar "Y")] 
+      (App (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y")) 
+           (Var "y"))
+      `shouldBe` Right (TyVar "Y")
+
+  it "typechecks simple type applications" $
+    tc [] [("x", TyVar "A")] (TyApp (TyAbs "X" (Var "x")) (TyVar "X"))
+      `shouldBe` Right (TyVar "A")
+
+  it "typechecks type applications with simple abstraction" $
+    tc [] [] (TyApp (TyAbs "X" (Abs "x" (TyVar "X") (Var "x"))) (TyVar "Y"))
+      `shouldBe` Right (TyArrow (TyVar "Y") (TyVar "Y"))