diff --git a/src/Compiler/RlpcError.hs b/src/Compiler/RlpcError.hs
index 6cb242e..6d97912 100644
--- a/src/Compiler/RlpcError.hs
+++ b/src/Compiler/RlpcError.hs
@@ -14,6 +14,9 @@ module Compiler.RlpcError
     -- * Located Comonad
     , Located(..)
     , SrcSpan(..)
+
+    -- * Common error messages
+    , undefinedVariableErr
     )
     where
 ----------------------------------------------------------------------------------
@@ -74,3 +77,8 @@ debugMsg tag e = MsgEnvelope
     , _msgSeverity = SevDebug tag
     }
 
+undefinedVariableErr :: Text -> RlpcError
+undefinedVariableErr n = Text
+    [ "Variable not in scope: `" <> n <> "'."
+    ]
+
diff --git a/src/Core/Syntax.hs b/src/Core/Syntax.hs
index 56bf9f4..3ab57e9 100644
--- a/src/Core/Syntax.hs
+++ b/src/Core/Syntax.hs
@@ -38,7 +38,7 @@ module Core.Syntax
     , HasRHS(_rhs), HasLHS(_lhs)
     , _BindingF, _MkVar
     -- ** Classy optics
-    , HasBinders(..), HasArrowStops(..)
+    , HasBinders(..), HasArrowStops(..), HasApplicants1(..), HasApplicants(..)
     )
     where
 ----------------------------------------------------------------------------------
@@ -577,23 +577,34 @@ deriving instance Lift b => Lift (Program b)
 
 --------------------------------------------------------------------------------
 
--- class HasApplicants s t a b | s -> a, t -> b, s b -> t, t a -> s where
---     applicants :: Traversal s t a b
+class HasApplicants1 s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    applicants1 :: Traversal s t a b
 
--- instance HasApplicants (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b)))
+class HasApplicants s t a b | s -> a, t -> b, s b -> t, t a -> s where
+    applicants :: Traversal s t a b
+
+instance HasApplicants1 Type Type Type Type where
+    applicants1 k (TyApp f x) = TyApp <$> applicants1 k f <*> k x
+    applicants1 k x           = k x
+
+instance HasApplicants Type Type Type Type where
+    applicants k (TyApp f x) = TyApp <$> applicants k f <*> k x
+    applicants k x           = pure x
+
+-- instance HasArguments (ExprF b (Fix (ExprF b))) (ExprF b (Fix (ExprF b)))
 --                        (Fix (ExprF b)) (Fix (ExprF b)) where
---     applicants k (AppF f x) = AppF <$> applicants k f <*> k x
---     applicants k x          = unwrapFix <$> k (wrapFix x)
+--     arguments k (AppF f x) = AppF <$> arguments k f <*> k x
+--     arguments k x          = unwrapFix <$> k (wrapFix x)
 
--- instance HasApplicants (f (Fix f)) (f (Fix f)) (Fix f) (Fix f)
---       => HasApplicants (Fix f) (Fix f) (Fix f) (Fix f) where
---     applicants :: forall g. Applicative g
+-- instance HasArguments (f (Fix f)) (f (Fix f)) (Fix f) (Fix f)
+--       => HasArguments (Fix f) (Fix f) (Fix f) (Fix f) where
+--     arguments :: forall g. Applicative g
 --                => LensLike' g (Fix f) (Fix f)
---     applicants k (Fix f) = Fix <$> applicants k f
+--     arguments k (Fix f) = Fix <$> arguments k f
 
--- applicants :: Traversal' (Expr b) (Expr b)
--- applicants k (App f x) = App <$> applicants k f <*> k x
--- applicants k x         = k x
+-- arguments :: Traversal' (Expr b) (Expr b)
+-- arguments k (App f x) = App <$> arguments k f <*> k x
+-- arguments k x         = k x
 
 class HasBinders s t a b | s -> a, t -> b, s b -> t, t a -> s where
     binders :: Traversal s t a b
diff --git a/src/Core/SystemF.hs b/src/Core/SystemF.hs
index 5b79fca..9cc555f 100644
--- a/src/Core/SystemF.hs
+++ b/src/Core/SystemF.hs
@@ -14,6 +14,9 @@ import Data.Foldable
 import Data.List.Extra
 import Control.Monad.Utils
 import Control.Monad
+import Data.Text                    qualified as T
+import Data.Pretty
+import Text.Printf
 
 import Control.Comonad
 import Control.Comonad.Cofree
@@ -24,6 +27,7 @@ import Control.Lens                 hiding ((:<))
 import Control.Lens.Unsound
 
 import Compiler.RLPC
+import Compiler.RlpcError
 import Core
 --------------------------------------------------------------------------------
 
@@ -46,12 +50,27 @@ lint = undefined
 
 type ET = Cofree (ExprF Var) Type
 
-type SysF = Either TypeError
+type SysF = Either SystemFError
 
-data TypeError = TypeErrorUndefinedVariable Name
-               | TypeErrorKindMismatch Kind Kind
-               | TypeErrorCouldNotMatch Type Type
-               deriving Show
+data SystemFError = SystemFErrorUndefinedVariable Name
+                  | SystemFErrorKindMismatch Kind Kind
+                  | SystemFErrorCouldNotMatch Type Type
+                  deriving Show
+
+instance IsRlpcError SystemFError where
+    liftRlpcError = \case
+        SystemFErrorUndefinedVariable n ->
+            undefinedVariableErr n
+        SystemFErrorKindMismatch k k' ->
+            Text [ T.pack $ printf "Could not match kind `%s' with `%s'"
+                                   (pretty k) (pretty k')
+                 ]
+        SystemFErrorCouldNotMatch t t' ->
+            Text [ T.pack $ printf "Could not match type `%s' with `%s'"
+                                   (pretty t) (pretty t')
+                 ]
+
+justLintCoreExpr = fmap (fmap (prettyPrec appPrec1)) . lintE demoContext
 
 lintE :: Gamma -> Expr Var -> SysF ET
 lintE g = \case
@@ -97,7 +116,7 @@ lintE g = \case
         g' = supplementVars vs g
         checkBind v@(MkVar n t) e = case lintE g' e of
             Right (t' :< e') | t == t'   -> Right (BindingF v e')
-                             | otherwise -> Left (TypeErrorCouldNotMatch t t')
+                             | otherwise -> Left (SystemFErrorCouldNotMatch t t')
             Left e -> Left e
     Let NonRec bs e -> do
         (g',bs') <- mapAccumLM checkBind g bs
@@ -109,38 +128,50 @@ lintE g = \case
         checkBind g (BindingF v@(n :^ t) e) = case lintE g (wrapFix e) of
             Right (t' :< e')
                 | t == t'   -> Right (supplementVar n t g, BindingF v e')
-                | otherwise -> Left (TypeErrorCouldNotMatch t t')
+                | otherwise -> Left (SystemFErrorCouldNotMatch t t')
             Left e -> Left e
 
     Case e as -> do
-        (ts,as') <- unzip <$> checkAlt `traverse` as
-        unless (allSame ts) $
-            Left (error "unifica oh my god fix this later")
-        e' <- lintE g e
-        pure $ head ts :< CaseF e' as'
+        e'@(et :< _) <- lintE g e
+        (ts,as') <- unzip <$> checkAlt et `traverse` as
+        case allUnify ts of
+            Just err -> Left err
+            Nothing  -> pure $ head ts  :< CaseF e' as'
       where
-        checkAlt :: Alter Var -> SysF (Type, AlterF Var ET)
-        checkAlt (AlterF (AltData con) bs e) = do
+        checkAlt :: Type -> Alter Var -> SysF (Type, AlterF Var ET)
+        checkAlt scrutineeType (AlterF (AltData con) bs e) = do
             ct <- lookupVar g con
-            zipWithM_ fzip bs (ct ^.. arrowStops)
+            ct' <- foldrMOf applicants (elimForall g) ct scrutineeType
+            zipWithM_ fzip bs (ct' ^.. arrowStops)
             (t :< e') <- lintE (supplementVars (varsToPairs bs) g) (wrapFix e)
             pure (t, AlterF (AltData con) bs e')
           where
             fzip (MkVar _ t) t'
                 | t == t'   = Right ()
-                | otherwise = Left (TypeErrorCouldNotMatch t t')
+                | otherwise = Left (SystemFErrorCouldNotMatch t t')
 
-unforall :: Type -> Type
-unforall (TyForall _ m) = m
-unforall m = m
+allUnify :: [Type] -> Maybe SystemFError
+allUnify [] = Nothing
+allUnify [t] = Nothing
+allUnify (t:t':ts)
+    | t == t'   = allUnify ts
+    | otherwise = Just (SystemFErrorCouldNotMatch t t')
 
+elimForall :: Gamma -> Type -> Type -> SysF Type
+elimForall g t (TyForall (n :^ k) m) = do
+    k' <- kindOf g t
+    case k == k' of
+        True -> pure $ subst n t m
+        False -> Left $ SystemFErrorKindMismatch k k'
+elimForall _ m _ = pure m
+ 
 varsToPairs :: [Var] -> [(Name, Type)]
 varsToPairs = toListOf (each . _MkVar)
 
 checkAgainst :: Gamma -> Var -> Expr Var -> SysF ET
 checkAgainst g v@(MkVar n t) e = case lintE g e of
     Right e'@(t' :< _) | t == t'      -> Right e'
-                       | otherwise    -> Left (TypeErrorCouldNotMatch t t')
+                       | otherwise    -> Left (SystemFErrorCouldNotMatch t t')
     Left a -> Left a
 
 supplementVars :: [(Name, Type)] -> Gamma -> Gamma
@@ -174,17 +205,17 @@ kindOf _ e          = error (show e)
 lookupCon :: Gamma -> Name -> SysF Kind
 lookupCon g n = case g ^. gammaTyCons . at n of
     Just k  -> Right k
-    Nothing -> Left (TypeErrorUndefinedVariable n)
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
 
 lookupVar :: Gamma -> Name -> SysF Type
 lookupVar g n = case g ^. gammaVars . at n of
     Just t -> Right t
-    Nothing -> Left (TypeErrorUndefinedVariable n)
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
 
 lookupTyVar :: Gamma -> Name -> SysF Kind
 lookupTyVar g n = case g ^. gammaTyVars . at n of
     Just k -> Right k
-    Nothing -> Left (TypeErrorUndefinedVariable n)
+    Nothing -> Left (SystemFErrorUndefinedVariable n)
 
 demoContext :: Gamma
 demoContext = Gamma
diff --git a/src/Data/Pretty.hs b/src/Data/Pretty.hs
index 972ed9f..13cfab0 100644
--- a/src/Data/Pretty.hs
+++ b/src/Data/Pretty.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE QuantifiedConstraints #-}
 module Data.Pretty
     ( Pretty(..)
     , rpretty
@@ -18,10 +19,13 @@ import Text.PrettyPrint             hiding ((<>))
 import Text.PrettyPrint.HughesPJ    hiding ((<>))
 import Text.Printf
 import Data.String                  (IsString(..))
-import Data.Text.Lens
+import Data.Text.Lens               hiding ((:<))
 import Data.Monoid
-import Data.Text                    qualified as T
 import Control.Lens
+
+-- instances
+import Control.Comonad.Cofree
+import Data.Text                    qualified as T
 ----------------------------------------------------------------------------------
 
 class Pretty a where
@@ -48,6 +52,9 @@ instance (Show a) => Pretty (Showing a) where
 
 deriving via Showing Int instance Pretty Int
 
+class (forall a. Pretty a => Pretty (f a)) => Pretty1 f where
+    liftPrettyPrec :: (Int -> a -> Doc) -> f a -> Doc
+
 --------------------------------------------------------------------------------
 
 ttext :: Pretty t => t -> Doc
@@ -75,3 +82,10 @@ appPrec, appPrec1 :: Int
 appPrec  = 10
 appPrec1 = 11
 
+instance PrintfArg Doc where
+    formatArg d fmt
+        | fmtChar (vFmt 'D' fmt) == 'D' = formatString (render d) fmt'
+        | otherwise                     = errorBadFormat $ fmtChar fmt
+      where
+        fmt' = fmt { fmtChar = 's', fmtPrecision = Nothing }
+