diff --git a/hindley-milner-type-check.cabal b/hindley-milner-type-check.cabal
--- a/hindley-milner-type-check.cabal
+++ b/hindley-milner-type-check.cabal
@@ -1,5 +1,5 @@
 name:                   hindley-milner-type-check
-version:                0.1.0.0
+version:                0.1.1.0
 synopsis:               Type inference for Hindley-Milner based languages
 description:
     This package contains an implemention of Hindley-Milner inference algorithm.
@@ -55,6 +55,7 @@
   default-language:     Haskell2010
 
   default-extensions:
+    ConstraintKinds
     DeriveDataTypeable
     DeriveFunctor,
     DeriveFoldable,
@@ -73,9 +74,10 @@
     TemplateHaskell,
     TupleSections,
     TypeFamilies,
+    TypeApplications
     TypeSynonymInstances
 
-test-suite hindley-milner-tests
+test-suite hindley-milner-type-check-tests
   Type:                exitcode-stdio-1.0
   Ghc-options:         -Wall -threaded -rtsopts
   Default-Language:    Haskell2010
diff --git a/src/Type/Check/HM/Infer.hs b/src/Type/Check/HM/Infer.hs
--- a/src/Type/Check/HM/Infer.hs
+++ b/src/Type/Check/HM/Infer.hs
@@ -11,7 +11,7 @@
 -- >   type Src  TestLang = ()              -- ^ define type for source code locations
 -- >   type Var  TestLang = Text            -- ^ define type for variables
 -- >   type Prim TestLang = NoPrim          -- ^ define type for primitive operators
--- >   getPrimType _ = error "No primops"   -- ^ reports types for primitives
+-- >   getPrimType _ _ = error "No primops"   -- ^ reports types for primitives
 --
 -- Also we define context for type inference that holds types for all known variables
 -- Often it defines types for all global variables or functions that are external.
@@ -40,17 +40,23 @@
     Context(..)
   , insertCtx
   , lookupCtx
+  , insertConstructorCtx
+  , lookupConstructorCtx
   , ContextOf
   -- * Inference
   , inferType
   , inferTerm
+  , inferTypeList
+  , inferTermList
   , subtypeOf
   , unifyTypes
   -- * Utils
   , closeSignature
+  , printInfer
 ) where
 
 import Control.Monad.Identity
+import Control.Monad.Writer.Strict
 
 import Control.Applicative
 import Control.Arrow (second)
@@ -69,29 +75,49 @@
 import Type.Check.HM.Type
 import Type.Check.HM.TypeError
 import Type.Check.HM.TyTerm
+import Type.Check.HM.Pretty
 
 import qualified Data.Map.Strict as M
 import qualified Data.Set as S
 import qualified Data.List as L
 
 -- | Context holds map of proven signatures for free variables in the expression.
-newtype Context loc v = Context { unContext :: Map v (Signature loc v) }
-  deriving (Show, Eq, Semigroup, Monoid)
+data Context loc v = Context
+  { context'binds         :: Map v (Signature loc v)   -- ^ known binds
+  , context'constructors  :: Map v (Signature loc v)   -- ^ known constructors for user-defined types
+  }
+  deriving (Show, Eq)
 
+instance Ord v => Semigroup (Context loc v) where
+  (<>) (Context bs1 cs1) (Context bs2 cs2) = Context (bs1 <> bs2) (cs1 <> cs2)
+
+instance Ord v => Monoid (Context loc v) where
+  mempty = Context mempty mempty
+
 -- | Type synonym for context.
 type ContextOf q = Context (Src q) (Var q)
 
 instance CanApply Context where
-  apply subst = Context . fmap (apply subst) . unContext
+  apply subst ctx = ctx
+      { context'binds = fmap (apply subst) $ context'binds ctx
+      }
 
 -- | Insert signature into context
 insertCtx :: Ord v => v -> Signature loc v ->  Context loc v -> Context loc v
-insertCtx v sign (Context ctx) = Context $ M.insert v sign ctx
+insertCtx v sign (Context binds cons) = Context (M.insert v sign binds) cons
 
 -- | Lookup signature by name in the context of inferred terms.
 lookupCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)
-lookupCtx v (Context ctx) = M.lookup v ctx
+lookupCtx v (Context binds _cons) = M.lookup v binds
 
+-- | Insert signature into context
+insertConstructorCtx :: Ord v => v -> Signature loc v ->  Context loc v -> Context loc v
+insertConstructorCtx v sign (Context binds cons) = Context binds (M.insert v sign cons)
+
+-- | Lookup signature by name in the context of inferred terms.
+lookupConstructorCtx :: Ord v => v -> Context loc v -> Maybe (Signature loc v)
+lookupConstructorCtx v (Context _binds cons) = M.lookup v cons
+
 -- | Wrapper with ability to generate fresh names
 data Name v
   = Name v
@@ -127,20 +153,24 @@
 -- To check the term we need only variables that are free in the term.
 -- So we can safely remove everything else and speed up lookup times.
 restrictContext :: Ord v => Term prim loc v -> Context loc v -> Context loc v
-restrictContext t (Context ctx) = Context $ M.intersection ctx fv
+restrictContext t (Context binds cons) = Context (M.intersection binds fv) cons
   where
     fv = M.fromList $ fmap (, ()) $ S.toList $ freeVars t
 
 wrapContextNames :: Ord v => Context loc v -> Context loc (Name v)
 wrapContextNames = fmapCtx Name
   where
-    fmapCtx f (Context m) = Context $ M.mapKeys f $ M.map (fmap f) m
+    fmapCtx f (Context bs cs) = Context (wrap bs)  (wrap cs)
+      where
+        wrap = M.mapKeys f . M.map (fmap f)
 
 wrapTermNames :: Term prim loc v -> Term prim loc (Name v)
 wrapTermNames = fmap Name
 
 markProven :: Context loc v -> Context (Origin loc) v
-markProven = Context . M.map (mapLoc Proven) . unContext
+markProven (Context bs cs) = Context (mark bs) (mark cs)
+  where
+    mark = M.map (mapLoc Proven)
 
 markUserCode :: Term prim loc v -> Term prim (Origin loc) v
 markUserCode = mapLoc UserCode
@@ -180,33 +210,58 @@
 
 -- | Type-inference monad.
 -- Contains integer counter for fresh variables and possibility to report type-errors.
-newtype InferM loc var a = InferM (StateT Int (Except (TypeError loc (Name var))) a)
-  deriving (Functor, Applicative, Monad, MonadState Int, MonadError (TypeError loc (Name var)))
+newtype InferM loc var a = InferM (StateT Int (Writer [TypeError loc (Name var)]) a)
+  deriving (Functor, Applicative, Monad, MonadState Int, MonadWriter [TypeError loc (Name var)])
 
 -- | Runs inference monad.
-runInferM :: InferM loc var a -> Either (TypeError loc (Name var)) a
-runInferM (InferM m) = runExcept $ evalStateT m 0
+runInferM :: InferM loc var a -> Either [TypeError loc (Name var)] a
+runInferM (InferM m) = case runWriter $ evalStateT m 0 of
+  (res, []) -> Right res
+  (_, errs) -> Left errs
 
 type InferOf q = InferM (Src q) (Var q) (Out (Prim q) (Src q) (Var q))
 
 -- | Type-inference function.
 -- We provide a context of already proven type-signatures and term to infer the type.
-inferType :: Lang q => ContextOf q -> TermOf q -> Either (ErrorOf q) (TypeOf q)
+inferType :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TypeOf q)
 inferType ctx term = fmap termType $ inferTerm ctx term
 
 -- | Infers types for all subexpressions of the given term.
 -- We provide a context of already proven type-signatures and term to infer the type.
-inferTerm :: Lang q => ContextOf q -> TermOf q -> Either (ErrorOf q) (TyTermOf q)
-inferTerm ctx term = join $
-  bimap (fromTypeErrorNameVar . normaliseType) ((\(_, tyTerm) -> toTyTerm tyTerm)) $
-    runInferM $ infer (wrapContextNames $ markProven $ restrictContext term ctx) (wrapTermNames $ markUserCode term)
+inferTerm :: Lang q => ContextOf q -> TermOf q -> Either [ErrorOf q] (TyTermOf q)
+inferTerm ctx term =
+  case runInferM $ infer (wrapContextNames $ markProven $ restrictContext term ctx) (wrapTermNames $ markUserCode term) of
+    Right (_, tyTerm) -> toTyTerm tyTerm
+    Left errs -> Left $ fmap (fromTypeErrorNameVar . normaliseType) errs
   where
-    toTyTerm = fromTyTermNameVar . normaliseType . mapLoc fromOrigin
+    toTyTerm = either (Left . pure) Right . fromTyTermNameVar . normaliseType . mapLoc fromOrigin
 
 type Out prim loc var = ( Subst (Origin loc) (Name var)
                         , TyTerm prim (Origin loc) (Name var)
                         )
 
+-- | Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies.
+inferTermList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TyTermOf q)]
+inferTermList ctx defs = case defs of
+  []  -> pure []
+  d:_ ->
+    let topLoc = bind'loc d
+    in  fmap fromLetExpr $ inferTerm ctx (toLetExpr topLoc defs)
+  where
+    toLetExpr loc ds = letRecE loc (fmap toBind ds) (bottomE loc)
+
+    fromLetExpr = \case
+      (TyTerm (Fix (Ann _ (LetRec _ bs _)))) -> fmap fromBind bs
+      _                                      -> error "Imposible happened. Found non let-rec expression"
+
+    toBind = id
+    fromBind = fmap TyTerm
+
+-- | Infers types for bunch of terms. Terms can be recursive and not-sorted by depndencies.
+-- It returns only top-level types for all terms.
+inferTypeList :: Lang q => ContextOf q -> [Bind (Src q) (Var q) (TermOf q)] -> Either [ErrorOf q] [Bind (Src q) (Var q) (TypeOf q)]
+inferTypeList ctx defs = fmap (fmap (fmap termType)) $ inferTermList ctx defs
+
 infer :: Lang q => ContextOf' q -> TermOf' q -> InferOf q
 infer ctx (Term (Fix x)) = case x of
   Var loc v           -> inferVar ctx loc v
@@ -216,14 +271,19 @@
   Let loc v a         -> inferLet ctx loc (fmap Term v) (Term a)
   LetRec loc vs a     -> inferLetRec ctx loc (fmap (fmap Term) vs) (Term a)
   AssertType loc a ty -> inferAssertType ctx loc (Term a) ty
-  Constr loc ty tag   -> inferConstr loc ty tag
+  Constr loc tag      -> inferConstr ctx loc tag
   Case loc e alts     -> inferCase ctx loc (Term e) (fmap (fmap Term) alts)
   Bottom loc          -> inferBottom loc
 
+retryWithBottom :: Lang q => TypeError (Src q) (Name (Var q)) -> Origin (Src q) -> InferOf q
+retryWithBottom err loc = do
+  tell [err]
+  inferBottom loc
+
 inferVar :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
 inferVar ctx loc v = {- trace (unlines ["VAR", ppShow ctx, ppShow v]) $ -}
-  case M.lookup v (unContext ctx) of
-    Nothing  -> throwError $ NotInScopeErr (fromOrigin loc) v
+  case lookupCtx v ctx of
+    Nothing  -> retryWithBottom (NotInScopeErr (fromOrigin loc) v) loc
     Just sig -> do ty <- newInstance $ setLoc loc sig
                    return (mempty, tyVarE ty loc v)
 
@@ -231,17 +291,19 @@
 inferPrim loc prim =
   return (mempty, tyPrimE ty loc prim)
   where
-    ty = fmap Name $ mapLoc UserCode $ getPrimType prim
+    ty = fmap Name $ mapLoc UserCode $ getPrimType (fromOrigin loc) prim
 
 inferApp :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TermOf' q -> InferOf q
 inferApp ctx loc f a = {- fmap (\res -> trace (unlines ["APP", ppCtx ctx, ppShow' f, ppShow' a, ppShow' $ snd res]) res) $-} do
   tvn <- fmap (varT loc) $ freshVar
   res <- inferTerms ctx [f, a]
   case res of
-    (phi, [(tf, f'), (ta, a')]) -> fmap (\subst ->
-                                            let ty   = apply subst tvn
-                                                term = tyAppE ty loc (apply subst f') (apply subst a')
-                                            in  (subst, term)) $ unify phi tf (arrowT loc ta tvn)
+    (phi, [(tf, f'), (ta, a')]) -> case unify phi tf (arrowT loc ta tvn) of
+      Left err    -> retryWithBottom err loc
+      Right subst -> let ty   = apply subst tvn
+                         term = tyAppE ty loc (apply subst f') (apply subst a')
+                     in  pure (subst, term)
+
     _               -> error "Impossible has happened!"
 
 inferLam :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
@@ -270,10 +332,11 @@
   -> InferOf q
 inferLetRec ctx topLoc vs body = do
   lhsCtx <- getTypesLhs vs
-  (phi, rhsTyTerms) <- inferTerms (ctx <> Context (M.fromList lhsCtx)) exprBinds
+  (phi, rhsTyTerms) <- inferTerms (ctx <> Context (M.fromList lhsCtx) mempty) exprBinds
   let (tBinds, bindsTyTerms) = unzip rhsTyTerms
-  (ctx1, lhsCtx1, subst) <- unifyRhs ctx lhsCtx phi tBinds
-  inferBody bindsTyTerms ctx1 lhsCtx1 subst body
+  case unifyRhs ctx lhsCtx phi tBinds of
+    Right (ctx1, lhsCtx1, subst) -> inferBody bindsTyTerms ctx1 lhsCtx1 subst body
+    Left err                     -> retryWithBottom err topLoc
   where
     exprBinds = fmap bind'rhs vs
     locBinds  = fmap bind'loc vs
@@ -303,60 +366,75 @@
 inferAssertType :: Lang q => ContextOf' q -> Origin (Src q) -> TermOf' q -> TypeOf' q -> InferOf q
 inferAssertType ctx loc a ty = do
   (phi, aTyTerm) <- infer ctx a
-  subst <- genSubtypeOf phi ty (termType aTyTerm)
-  let subst' = phi <> subst
-  return (subst', apply subst' $ tyAssertTypeE loc aTyTerm ty)
+  case genSubtypeOf phi ty (termType aTyTerm) of
+    Right subst -> do
+      let subst' = phi <> subst
+      return (subst', apply subst' $ tyAssertTypeE loc aTyTerm ty)
+    Left err -> retryWithBottom err loc
 
-inferConstr :: Lang q => Origin (Src q) -> TypeOf' q -> Name (Var q) -> InferOf q
-inferConstr loc ty tag = do
-  vT <- newInstance $ typeToSignature ty
-  return (mempty, tyConstrE loc vT tag)
+inferConstr :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> InferOf q
+inferConstr ctx loc tag = do
+  case lookupConstructorCtx tag ctx of
+    Just ty -> do
+      vT <- newInstance ty
+      return (mempty, tyConstrE loc vT tag)
+    Nothing -> retryWithBottom (NotInScopeErr (fromOrigin loc) tag) loc
 
 inferCase :: forall q . Lang q
   => ContextOf' q -> Origin (Src q) -> TermOf' q -> [CaseAltOf' q (TermOf' q)]
   -> InferOf q
 inferCase ctx loc e caseAlts = do
   (phi, tyTermE) <- infer ctx e
-  (psi, tRes, tyAlts) <- inferAlts phi (termType tyTermE) $ caseAlts
-  return ( psi
-         , apply psi $ tyCaseE tRes loc (apply psi tyTermE) $ fmap (applyAlt psi) tyAlts)
+  mAlts <- inferAlts phi (termType tyTermE) $ caseAlts
+  case mAlts of
+    Just (psi, tRes, tyAlts) -> return ( psi
+                                       , apply psi $ tyCaseE tRes loc (apply psi tyTermE) tyAlts)
+    Nothing -> retryWithBottom (EmptyCaseExpr (fromOrigin loc)) loc
   where
-    inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (SubstOf' q, TypeOf' q, [CaseAltOf' q (TyTermOf' q)])
-    inferAlts substE tE alts =
-      fmap (\(subst, _, tRes, as) -> (subst, tRes, L.reverse as)) $ foldM go (substE, tE, tE, []) alts
+    inferAlts :: SubstOf' q -> TypeOf' q -> [CaseAltOf' q (TermOf' q)] -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, [CaseAltOf' q (TyTermOf' q)]))
+    inferAlts substE tE alts = do
+      (subst, _, mTRes, as) <- foldM go (substE, tE, Nothing, []) alts
+      pure $ case mTRes of
+        Just tRes -> Just (subst, tRes, L.reverse as)
+        Nothing   -> Nothing
       where
-        go (subst, tyTop, _, res) alt = do
-          (phi, tRes, alt1) <- inferAlt (applyAlt subst alt)
-          let subst1 = subst <> phi
-          subst2 <- unify subst1 (apply subst1 tyTop) (apply subst1 $ caseAlt'constrType alt1)
-          return (subst2, apply subst2 tyTop, apply subst2 tRes, applyAlt subst2 alt1 : res)
-
-
-    inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (SubstOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q))
-    inferAlt preAlt = do
-      alt <- newCaseAltInstance preAlt
-      let argVars = fmap  (\ty -> (snd $ typed'value ty, (fst $ typed'value ty, typed'type ty))) $ caseAlt'args alt
-          ctx1 = Context (M.fromList $ fmap (second $ monoT . snd) argVars) <> ctx
-      (subst, tyTermRhs) <- infer ctx1 $ caseAlt'rhs alt
-      let args = fmap (\(v, (argLoc, tv)) -> Typed (apply subst tv) (argLoc, v)) argVars
-          alt' = alt
-                  { caseAlt'rhs = tyTermRhs
-                  , caseAlt'args = args
-                  , caseAlt'constrType = apply subst $ caseAlt'constrType alt
-                  }
-      return (subst, termType tyTermRhs, alt')
-
-    newCaseAltInstance :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (CaseAltOf' q (TermOf' q))
-    newCaseAltInstance alt = do
-      tv <- newInstance $ typeToSignature $ getCaseType alt
-      let (argsT, resT)= splitFunT tv
-      return $ alt
-        { caseAlt'constrType = resT
-        , caseAlt'args = zipWith (\aT ty -> ty { typed'type = aT }) argsT $ caseAlt'args alt
-        }
+        go initSt@(subst, tyTop, mTyPrevRhs, res) alt = do
+          mRes <- inferAlt (applyAlt subst alt)
+          case mRes of
+            Just (phi, tyRhs, tResExpected, alt1) -> do
+              let subst1 = subst <> phi
+              case unify subst1 (apply subst1 tyTop) (apply subst1 tResExpected) of
+                Right subst2 -> do
+                  case mTyPrevRhs of
+                    Nothing -> pure (subst2, apply subst2 tyTop, Just $ apply subst2 tyRhs, applyAlt subst2 alt1 : res)
+                    Just tyPrevRhs -> do
+                      case unify subst2 (apply subst2 tyRhs) (apply subst2 tyPrevRhs) of
+                        Right subst3 -> pure (subst3, apply subst3 tyTop, Just $ apply subst3 tyRhs, applyAlt subst3 alt1 : res)
+                        Left err     -> do
+                          tell [err]
+                          pure initSt
+                Left err     -> do
+                  tell [err]
+                  pure initSt
+            Nothing -> do
+              tell [NotInScopeErr (fromOrigin $ caseAlt'loc alt) (caseAlt'tag alt)]
+              pure initSt
 
-    getCaseType :: CaseAltOf' q (TermOf' q) -> TypeOf' q
-    getCaseType CaseAlt{..} = funT (fmap typed'type caseAlt'args) caseAlt'constrType
+    inferAlt :: CaseAltOf' q (TermOf' q) -> InferM (Src q) (Var q) (Maybe (SubstOf' q, TypeOf' q, TypeOf' q, CaseAltOf' q (TyTermOf' q)))
+    inferAlt alt =
+      case lookupConstructorCtx (caseAlt'tag alt) ctx of
+        Just ctxConTy -> do
+          conTy <- newInstance ctxConTy
+          let (tyArgs, tyRes) = splitFunT conTy
+              expectedArity = length tyArgs
+              actualArity   = length $ caseAlt'args alt
+          when (expectedArity /= actualArity) $ tell [ConsArityMismatch (fromOrigin $ caseAlt'loc alt) (caseAlt'tag alt) expectedArity actualArity]
+          let argVars = zipWith (\ty (src, arg) -> (arg, (src, ty))) tyArgs (caseAlt'args alt)
+              ctx1 = Context (M.fromList $ fmap (second $ monoT . snd) argVars) mempty <> ctx
+          (subst, tyTermRhs) <- infer ctx1 $ caseAlt'rhs alt
+          let alt' = alt { caseAlt'rhs = tyTermRhs }
+          return $ Just (subst, termType tyTermRhs, tyRes, alt')
+        Nothing -> pure Nothing
 
     splitFunT :: TypeOf' q -> ([TypeOf' q], TypeOf' q)
     splitFunT arrT = go [] arrT
@@ -365,18 +443,9 @@
           ArrowT _loc a b -> go (Type a : argsT) (Type b)
           other           -> (reverse argsT, Type $ Fix other)
 
+    applyAlt subst alt = alt { caseAlt'rhs = apply subst $ caseAlt'rhs alt }
 
-    funT :: [TypeOf' q] -> TypeOf' q -> TypeOf' q
-    funT argsT resT = foldr (\a b -> arrowT (getLoc a) a b) resT argsT
 
-    applyAlt subst alt@CaseAlt{..} = alt
-      { caseAlt'constrType = apply subst caseAlt'constrType
-      , caseAlt'args       = fmap applyTyped caseAlt'args
-      , caseAlt'rhs        = apply subst caseAlt'rhs
-      }
-      where
-        applyTyped ty@Typed{..} = ty { typed'type = apply subst $ typed'type }
-
 inferBottom :: Lang q => Origin (Src q) -> InferOf q
 inferBottom loc = do
   ty <- fmap (varT loc) freshVar
@@ -414,11 +483,11 @@
 
 -- | Unification function. Checks weather two types unify.
 -- First argument is current substitution.
-unify :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)
+unify :: (IsVar v, Show loc)
   => Subst' loc v
   -> Type' loc v
   -> Type' loc v
-  -> m (Subst' loc v)
+  -> Either (TypeError loc (Name v)) (Subst' loc v)
 unify phi (Type (Fix x)) (Type (Fix y)) = {- trace (unlines ["UNIFY", ppShow tx, ppShow ty]) $ -}
   case (x, y) of
     (VarT loc tvn, t) ->
@@ -459,11 +528,11 @@
   | memberVarSet tvn (tyVars ty)  = throwError $ OccursErr (fromOrigin loc) (mapLoc fromOrigin ty)
   | otherwise                     = return $ phi <> delta tvn ty
 
-unifyl :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)
+unifyl :: (IsVar v, Show loc)
   => Subst' loc v
   -> [Type' loc v]
   -> [Type' loc v]
-  -> m (Subst' loc v)
+  -> Either (TypeError loc (Name v)) (Subst' loc v)
 unifyl subst as bs = foldr go (return subst) $ zip as bs
   where
     go (a, b) eSubst = (\t -> unify t a b) =<< eSubst
@@ -475,11 +544,11 @@
   join $ bimap (fromTypeErrorNameVar . normaliseType) (fromSubstNameVar . fromSubstOrigin) $
     genSubtypeOf mempty (fmap Name $ mapLoc Proven a) (fmap Name $ mapLoc UserCode b)
 
-genSubtypeOf :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)
+genSubtypeOf :: (IsVar v, Show loc)
   => Subst' loc v
   -> Type' loc v
   -> Type' loc v
-  -> m (Subst' loc v)
+  -> Either (TypeError loc (Name v)) (Subst' loc v)
 genSubtypeOf phi tx@(Type (Fix x)) ty@(Type (Fix y)) = case (x, y) of
   (_, VarT _ _) -> unify phi tx ty
   (ConT locA n xs, ConT locB m ys) ->
@@ -498,11 +567,11 @@
     subtypeErr locA locB = throwError
       $ SubtypeErr (chooseUserOrigin locA locB) (mapLoc fromOrigin tx) (mapLoc fromOrigin ty)
 
-subtypeOfL :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)
+subtypeOfL :: (IsVar v, Show loc)
   => Subst' loc v
   -> [Type' loc v]
   -> [Type' loc v]
-  -> m (Subst' loc v)
+  -> Either (TypeError loc (Name v)) (Subst' loc v)
 subtypeOfL subst as bs = foldr go (return subst) $ zip as bs
   where
     go (a, b) eSubst = (\t -> genSubtypeOf t a b) =<< eSubst
@@ -514,7 +583,7 @@
 addDecls vs ctx =
   foldM  (\c b -> addDecl unknowns b c) ctx vs
   where
-    unknowns = foldMap tyVars $ unContext ctx
+    unknowns = foldMap tyVars $ context'binds ctx
 
 addDecl :: forall loc v . IsVar v
   => VarSet' loc v
@@ -523,7 +592,8 @@
   -> InferM loc v (Context' loc v)
 addDecl unknowns b ctx = do
   scheme <- toScheme unknowns (bind'rhs b)
-  return $ Context . M.insert (bind'lhs b) scheme . unContext $ ctx
+  return $ ctx
+    { context'binds = M.insert (bind'lhs b) scheme . context'binds $ ctx }
   where
     toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
     toScheme uVars ty = do
@@ -566,6 +636,7 @@
     SubtypeErr loc tA tB -> liftA2 (SubtypeErr loc) (fromTypeNameVar tA) (fromTypeNameVar tB)
     NotInScopeErr loc v  -> fmap (NotInScopeErr loc) $ fromNameVar v
     EmptyCaseExpr loc    -> pure $ EmptyCaseExpr loc
+    ConsArityMismatch loc v expected actual -> fmap (\x -> ConsArityMismatch loc x expected actual) (fromNameVar v)
     FreshNameFound       -> pure FreshNameFound
 
 fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
@@ -590,19 +661,18 @@
       Let loc bind a      -> fmap (\b -> Let loc b a) $ fromBind bind
       LetRec loc binds a  -> fmap (\bs -> LetRec loc bs a) $ mapM fromBind binds
       AssertType loc a ty -> fmap (AssertType loc a) $ fromTypeNameVar ty
-      Constr loc t v      -> liftA2 (Constr loc) (fromTypeNameVar t) (fromNameVar v)
+      Constr loc v        -> fmap (Constr loc) (fromNameVar v)
       Bottom loc          -> pure $ Bottom loc
       Case loc e alts     -> fmap (Case loc e) $ mapM fromAlt alts
 
     fromBind b = fmap (\a -> b { bind'lhs = a }) $ fromNameVar $ bind'lhs b
 
     fromAlt alt@CaseAlt{..} =
-      liftA3 (\tag args constrType -> alt { caseAlt'tag = tag, caseAlt'args = args, caseAlt'constrType = constrType })
+      liftA2 (\tag args -> alt { caseAlt'tag = tag, caseAlt'args = args })
         (fromNameVar caseAlt'tag)
-        (mapM fromTyped caseAlt'args)
-        (fromTypeNameVar caseAlt'constrType)
+        (mapM fromAltArg caseAlt'args)
 
-    fromTyped Typed{..} = liftA2 Typed (fromTypeNameVar typed'type) (mapM fromNameVar typed'value)
+    fromAltArg (loc, v) = fmap (loc , ) (fromNameVar v)
 
 fromSubstNameVar :: Ord v => Subst loc (Name v) -> Either (TypeError loc v) (Subst loc v)
 fromSubstNameVar (Subst m) = fmap (Subst . M.fromList) $ mapM uncover $ M.toList m
@@ -617,4 +687,13 @@
 closeSignature argTys sig = apply (Subst $ M.fromList $ zip argNames argTys) monoTy
   where
     (argNames, monoTy) = splitSignature sig
+
+----------------------------------------------------------------------------------
+
+-- | Pretty printer for result of type-inference
+printInfer :: (PrettyLang q) => (Either [ErrorOf q] (TypeOf q)) -> IO ()
+printInfer = \case
+  Right ty  -> putStrLn $ show $ pretty ty
+  Left errs -> mapM_ (putStrLn . (++ "\n") . show . pretty) errs
+
 
diff --git a/src/Type/Check/HM/Lang.hs b/src/Type/Check/HM/Lang.hs
--- a/src/Type/Check/HM/Lang.hs
+++ b/src/Type/Check/HM/Lang.hs
@@ -8,8 +8,10 @@
   , TyTermOf
   , SubstOf
   , ErrorOf
+  , PrettyLang
 ) where
 
+import Type.Check.HM.Pretty
 import Type.Check.HM.Term
 import Type.Check.HM.Subst
 import Type.Check.HM.Type
@@ -48,7 +50,7 @@
   type Prim q
 
   -- | Reports type for primitive.
-  getPrimType :: Prim q -> TypeOf q
+  getPrimType :: Src q -> Prim q -> TypeOf q
 
 -- | Types of our language
 type TypeOf q = Type (Src q) (Var q)
@@ -64,5 +66,7 @@
 
 -- | Type substitutions
 type SubstOf q = Subst (Src q) (Var q)
+
+type PrettyLang q = (Lang q, PrettyVar (Var q), Pretty (Src q))
 
 
diff --git a/src/Type/Check/HM/Pretty.hs b/src/Type/Check/HM/Pretty.hs
--- a/src/Type/Check/HM/Pretty.hs
+++ b/src/Type/Check/HM/Pretty.hs
@@ -1,10 +1,12 @@
 {-# OPTIONS_GHC -Wno-orphans #-}
 -- | Pretty printer for types and terms.
 module Type.Check.HM.Pretty(
-    HasPrefix(..)
+    PrettyVar
+  , FixityCtx(..)
   , PrintCons(..)
   , OpFix(..)
   , Fixity(..)
+  , Pretty(..)
 ) where
 
 import Data.Bool
@@ -15,101 +17,116 @@
 
 import Type.Check.HM.Type
 import Type.Check.HM.Term
-
--- | Class to querry fixity of infix operations.
-class IsVar v => HasPrefix v where
-  getFixity :: v -> Maybe OpFix
-
-instance HasPrefix Text where
-  getFixity = const Nothing
+import Type.Check.HM.TypeError
 
-instance HasPrefix String where
-  getFixity = const Nothing
+-- | Type to querry fixity of infix operations in type variables.
+data FixityCtx var a = FixityCtx
+  { fixity'context :: var -> Maybe OpFix   -- ^ Function that provides fixity-type for a given variable
+  , fixity'data    :: a                    -- ^ content
+  }
 
-instance HasPrefix Int where
-  getFixity = const Nothing
+-- | Ignores fixity information
+noFixity :: forall v a . a -> FixityCtx v a
+noFixity = FixityCtx (const Nothing)
 
 -- | This class is useful to define the way to print special cases
 -- like constructors for tuples or lists.
 class PrintCons v where
   printCons :: v -> [Doc ann] -> Doc ann
 
+instance PrintCons Int where
+  printCons name args = hsep $ pretty name : args
+
+instance PrintCons String where
+  printCons name args = hsep $ pretty name : args
+
 instance PrintCons Text where
   printCons name args = hsep $ pretty name : args
 
-isPrefix :: HasPrefix v => v -> Bool
-isPrefix = isNothing . getFixity
+isPrefix :: (v -> Maybe OpFix) -> v -> Bool
+isPrefix getFixity = isNothing . getFixity
 
-isInfix :: HasPrefix v => v -> Bool
-isInfix  = not . isPrefix
+isInfix :: (v -> Maybe OpFix) -> v -> Bool
+isInfix a = not . isPrefix a
 
-instance (Pretty v, PrintCons v, HasPrefix v) => Pretty (Signature loc v) where
-  pretty = foldFix go . unSignature
+type PrettyVar a = (Pretty a, PrintCons a, IsVar a)
+
+instance (PrettyVar v) => Pretty (Signature loc v) where
+  pretty = pretty . noFixity @v
+
+instance (PrettyVar v) => Pretty (FixityCtx v (Signature loc v)) where
+  pretty (FixityCtx getFixity sign) = foldFix go $ unSignature sign
     where
       go = \case
         ForAllT _ _ r -> r
-        MonoT ty      -> pretty ty
+        MonoT ty      -> pretty (FixityCtx getFixity ty)
 
-instance (HasPrefix v, PrintCons v, Pretty v) => Pretty (Type loc v) where
-  pretty = go False initCtx . unType
+instance (PrettyVar v) => Pretty (Type loc v) where
+  pretty = pretty . noFixity @v
+
+instance (PrettyVar v) => Pretty (FixityCtx v (Type loc v)) where
+  pretty (FixityCtx getFixity ty) = go False initCtx $ unType ty
     where
       go :: Bool -> FixityContext v -> Fix (TypeF loc v) -> Doc ann
       go isArrPrev ctx (Fix expr) = case expr of
         VarT _ name   -> pretty name
-        ConT _ name [a, b] | isInfix name -> fromBin name a b
+        ConT _ name [a, b] | isInfix getFixity name -> fromBin name a b
         ConT _ name as -> fromCon isArrPrev name as
         ArrowT _ a b -> fromArrow a b
         TupleT _ as -> fromTuple as
         ListT _ a -> fromList a
         where
-          fromCon isArr name args = maybeParens (not (null args) && not isArr && needsParens ctx OpFunAp) $
+          fromCon isArr name args = maybeParens (not (null args) && not isArr && needsParens getFixity ctx OpFunAp) $
             printCons name $ fmap (go False (FcRight OpFunAp)) args
 
-          fromBin op a b = maybeParens (needsParens ctx (Op op)) $ hsep
+          fromBin op a b = maybeParens (needsParens getFixity ctx (Op op)) $ hsep
             [ go True (FcLeft $ Op op) a
             , pretty op
             , go True (FcRight $ Op op) b
             ]
 
-          fromArrow a b = maybeParens (needsParens ctx ArrowOp) $ hsep
+          fromArrow a b = maybeParens (needsParens getFixity ctx ArrowOp) $ hsep
             [ go True (FcLeft ArrowOp ) a
             , "->"
             , go True (FcRight ArrowOp) b
             ]
 
-          fromTuple as = parens $ hsep $ punctuate comma $ fmap (pretty . Type) as
+          fromTuple as = parens $ hsep $ punctuate comma $ fmap (pretty . FixityCtx getFixity . Type) as
 
-          fromList a = brackets $ pretty $ Type a
+          fromList a = brackets $ pretty $ FixityCtx getFixity $ Type a
 
       initCtx = FcNone
 
 maybeParens :: Bool -> Doc ann -> Doc ann
 maybeParens cond = bool id parens cond
 
-needsParens :: HasPrefix v => FixityContext v -> Operator v -> Bool
-needsParens = \case
+needsParens :: (v -> Maybe OpFix) -> FixityContext v -> Operator v -> Bool
+needsParens getFixity = \case
   FcNone      -> const False
   FcLeft ctx  -> fcLeft ctx
   FcRight ctx -> fcRight ctx
   where
     fcLeft ctxt op
-      | comparePrec ctxt op == PoLT = False
-      | comparePrec ctxt op == PoGT = True
-      | comparePrec ctxt op == PoNC = True
+      | comparePrec' ctxt op == PoLT = False
+      | comparePrec' ctxt op == PoGT = True
+      | comparePrec' ctxt op == PoNC = True
       -- otherwise the two operators have the same precedence
-      | fixity ctxt /= fixity op = True
-      | fixity ctxt == FixLeft = False
+      | fixity' ctxt /= fixity' op = True
+      | fixity' ctxt == FixLeft = False
       | otherwise = True
 
     fcRight ctxt op
-      | comparePrec ctxt op == PoLT = False
-      | comparePrec ctxt op == PoGT = True
-      | comparePrec ctxt op == PoNC = True
+      | comparePrec' ctxt op == PoLT = False
+      | comparePrec' ctxt op == PoGT = True
+      | comparePrec' ctxt op == PoNC = True
       -- otherwise the two operators have the same precedence
-      | fixity ctxt /= fixity op = True
-      | fixity ctxt == FixRight = False
+      | fixity' ctxt /= fixity' op = True
+      | fixity' ctxt == FixRight = False
       | otherwise = True
 
+    comparePrec' = comparePrec getFixity
+    fixity' = fixity getFixity
+
 data PartialOrdering = PoLT | PoGT | PoEQ | PoNC
   deriving Eq
 
@@ -136,14 +153,14 @@
   [ (Op "->", OpFix FixRight 2) ]
 -}
 
-getFixityEnv :: HasPrefix v => Operator v -> Maybe OpFix
-getFixityEnv = \case
+getFixityEnv :: (v -> Maybe OpFix) -> Operator v -> Maybe OpFix
+getFixityEnv getFixity = \case
   OpFunAp -> Nothing
   Op v    -> getFixity v
   ArrowOp -> Just $ OpFix FixRight 2
 
-comparePrec :: HasPrefix v => Operator v -> Operator v -> PartialOrdering
-comparePrec a b = case (getFixityEnv a, getFixityEnv b) of
+comparePrec :: (v -> Maybe OpFix) -> Operator v -> Operator v -> PartialOrdering
+comparePrec getFixity a b = case (getFixityEnv getFixity a, getFixityEnv getFixity b) of
   (Just opA, Just opB) -> toPo (opFix'prec opA) (opFix'prec opB)
   _                    -> PoNC
   where
@@ -153,13 +170,17 @@
       | otherwise = PoEQ
 
 
-fixity :: HasPrefix v => Operator v -> Fixity
-fixity op = maybe FixNone opFix'fixity $ getFixityEnv op
+fixity :: (v -> Maybe OpFix) -> Operator v -> Fixity
+fixity getFixity op = maybe FixNone opFix'fixity $ getFixityEnv getFixity op
 
----------------------------------------
+-----------------------------------------------------------------
+-- pretty terms
 
-instance (HasPrefix v, PrintCons v, Pretty v, Pretty prim) => Pretty (Term prim loc v) where
-  pretty (Term x) = foldFix prettyTermF x
+instance (PrettyVar v, Pretty prim) => Pretty (Term prim loc v) where
+  pretty = pretty . noFixity @v
+
+instance (PrettyVar v, Pretty prim) => Pretty (FixityCtx v (Term prim loc v)) where
+  pretty (FixityCtx getFixity (Term x)) = foldFix prettyTermF x
     where
       prettyTermF = \case
         Var _ v            -> pretty v
@@ -168,8 +189,8 @@
         Lam _ v a          -> parens $ hsep [hcat ["\\", pretty v], "->", a]
         Let _ v a          -> onLet [v] a
         LetRec _ vs a      -> onLet vs a
-        AssertType _ r sig -> parens $ hsep [r, "::", pretty sig]
-        Constr _ _ tag     -> pretty tag
+        AssertType _ r sig -> parens $ hsep [r, "::", pretty $ FixityCtx getFixity sig]
+        Constr _ tag       -> pretty tag
         Case _ e alts      -> vcat [ hsep ["case", e, "of"], indent 4 $ vcat $ fmap onAlt alts]
         Bottom _           -> "_|_"
         where
@@ -178,7 +199,28 @@
                  , hsep ["in ", body]]
 
           onAlt CaseAlt{..} = hsep
-            [ pretty caseAlt'tag, hsep $ fmap (pretty . snd . typed'value) caseAlt'args
+            [ pretty caseAlt'tag, hsep $ fmap (pretty . snd) caseAlt'args
             , "->"
             , caseAlt'rhs ]
+
+-----------------------------------------------------------------
+-- pretty errors
+
+instance (Pretty loc, PrettyVar var) => Pretty (TypeError loc var) where
+  pretty = pretty . noFixity @var
+
+instance (Pretty loc, PrettyVar var) => Pretty (FixityCtx var (TypeError loc var)) where
+  pretty (FixityCtx getFixity tyErr) = case tyErr of
+    OccursErr src name     -> err src $ hsep ["Occurs error", prettyTy name]
+    UnifyErr src tyA tyB   -> err src $ hsep ["Type mismatch got", inTicks $ prettyTy tyB, "expected", inTicks $ prettyTy tyA]
+    NotInScopeErr src name -> err src $ hsep ["Not in scope", pretty name]
+    SubtypeErr src tyA tyB -> err src $ hsep ["Subtype error", inTicks $ prettyTy tyB, "expected", inTicks $ prettyTy tyA]
+    EmptyCaseExpr src      -> err src $ "Case-expression should have at least one alternative case"
+    FreshNameFound         -> "Impossible happened: failed to eliminate fresh name on type-checker stage"
+    ConsArityMismatch src tag expected actual -> err src $ hsep ["Case-expression arguments mismatch for ", pretty tag, ". Expected ", pretty expected, " arguments, but got ", pretty actual]
+    where
+      err src msg = vcat [hcat [pretty src, ": error: "], indent 4 msg]
+      inTicks x = hcat ["'", x, "'"]
+      prettyTy = pretty . FixityCtx getFixity
+
 
diff --git a/src/Type/Check/HM/Term.hs b/src/Type/Check/HM/Term.hs
--- a/src/Type/Check/HM/Term.hs
+++ b/src/Type/Check/HM/Term.hs
@@ -15,12 +15,15 @@
   , constrE
   , bottomE
   , freeVars
+  , sortDeps
 ) where
 
 import Control.Arrow
 
 import Data.Data
+import Data.Graph
 import Data.Fix
+import Data.Foldable
 import Data.Set (Set)
 import Data.Eq.Deriving
 import Data.Ord.Deriving
@@ -30,6 +33,7 @@
 import Type.Check.HM.Type
 
 import qualified Data.Set as S
+import qualified Data.Sequence as Seq
 
 -- | Term functor. The arguments are
 -- @loc@ for source code locations, @v@ for variables, @r@ for recurion.
@@ -42,8 +46,7 @@
     | LetRec loc [Bind loc v r] r     -- ^ Recursive  let bindings
     | AssertType loc r (Type loc v)   -- ^ Assert type.
     | Case loc r [CaseAlt loc v r]    -- ^ case alternatives
-    | Constr loc (Type loc v) v       -- ^ constructor with tag and arity, also we should provide the type
-                                      --   of constructor as a function for a type-checker
+    | Constr loc v                    -- ^ constructor with tag
     | Bottom loc                      -- ^ value of any type that means failed program.
     deriving (Show, Eq, Functor, Foldable, Traversable, Data)
 
@@ -53,10 +56,8 @@
   -- ^ source code location
   , caseAlt'tag   :: v
   -- ^ tag of the constructor
-  , caseAlt'args  :: [Typed loc v (loc, v)]
+  , caseAlt'args  :: [(loc, v)]
   -- ^ arguments of the pattern matching
-  , caseAlt'constrType :: Type loc v
-  -- ^ type of the result expression, they should be the same for all cases
   , caseAlt'rhs   :: a
   -- ^ right-hand side of the case-alternative
   }
@@ -65,10 +66,10 @@
 -- | Local variable definition.
 --
 -- > let lhs = rhs in ...
-data Bind loc var r = Bind
+data Bind loc var a = Bind
   { bind'loc :: loc             -- ^ Source code location
   , bind'lhs :: var             -- ^ Variable name
-  , bind'rhs :: r               -- ^ Definition (right-hand side)
+  , bind'rhs :: a               -- ^ Definition (right-hand side)
   } deriving (Show, Eq, Functor, Foldable, Traversable, Data)
 
 $(deriveShow1 ''TermF)
@@ -97,17 +98,14 @@
         LetRec loc vs a -> Fix $ LetRec loc (fmap (\b ->  b { bind'lhs = f $ bind'lhs b }) vs) a
         AssertType loc r sig -> Fix $ AssertType loc r (fmap f sig)
         Case loc a alts -> Fix $ Case loc a $ fmap (mapAlt f) alts
-        Constr loc ty v -> Fix $ Constr loc (fmap f ty) (f v)
+        Constr loc v -> Fix $ Constr loc (f v)
         Bottom loc -> Fix $ Bottom loc
 
       mapAlt g alt@CaseAlt{..} = alt
         { caseAlt'tag  = f caseAlt'tag
-        , caseAlt'args = fmap (mapTyped g) caseAlt'args
-        , caseAlt'constrType = fmap f caseAlt'constrType
+        , caseAlt'args = fmap (second g) caseAlt'args
         }
 
-      mapTyped g Typed{..} = Typed (fmap f typed'type) (second g typed'value)
-
 -- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.
 varE :: loc -> var -> Term prim loc var
 varE loc = Term . Fix . Var loc
@@ -142,8 +140,8 @@
 caseE loc (Term e) alts = Term $ Fix $ Case loc e $ fmap (fmap unTerm) alts
 
 -- | 'constrE' @loc ty tag arity@ constructs constructor tag expression.
-constrE :: loc -> Type loc v -> v -> Term prim loc v
-constrE loc ty tag = Term $ Fix $ Constr loc ty tag
+constrE :: loc -> v -> Term prim loc v
+constrE loc tag = Term $ Fix $ Constr loc tag
 
 -- | 'bottomE' @loc@ constructs bottom value.
 bottomE :: loc -> Term prim loc v
@@ -162,7 +160,7 @@
     Let loc _ _ -> loc
     LetRec loc _ _ -> loc
     AssertType loc _ _ -> loc
-    Constr loc _ _ -> loc
+    Constr loc _ -> loc
     Case loc _ _ -> loc
     Bottom loc -> loc
 
@@ -177,20 +175,17 @@
         Let loc v a  -> Fix $ Let (f loc) (v { bind'loc = f $ bind'loc v }) a
         LetRec loc vs a -> Fix $ LetRec (f loc) (fmap (\b ->  b { bind'loc = f $ bind'loc b }) vs) a
         AssertType loc r sig -> Fix $ AssertType (f loc) r (mapLoc f sig)
-        Constr loc ty v -> Fix $ Constr (f loc) (mapLoc f ty) v
+        Constr loc v -> Fix $ Constr (f loc) v
         Case loc e alts -> Fix $ Case (f loc) e (fmap mapAlt alts)
         Bottom loc -> Fix $ Bottom (f loc)
 
       mapAlt alt@CaseAlt{..} = alt
         { caseAlt'loc  = f caseAlt'loc
-        , caseAlt'args = fmap mapTyped caseAlt'args
-        , caseAlt'constrType = mapLoc f caseAlt'constrType
+        , caseAlt'args = fmap (first f) caseAlt'args
         }
 
-      mapTyped (Typed ty val) = Typed (mapLoc f ty) (first f val)
-
 -- | Get free variables of the term.
-freeVars :: Ord v => Term lprim oc v -> Set v
+freeVars :: Ord v => Term prim loc v -> Set v
 freeVars = foldFix go . unTerm
   where
     go = \case
@@ -205,28 +200,37 @@
                              in  (mappend (freeBinds binds) body) `S.difference` lhs
       AssertType _ a _    -> a
       Case _ e alts       -> mappend e (foldMap freeVarAlts alts)
-      Constr _ _ _        -> mempty
+      Constr _ _          -> mempty
       Bottom _            -> mempty
 
     freeBinds = foldMap bind'rhs
 
-    freeVarAlts CaseAlt{..} = caseAlt'rhs `S.difference` (S.fromList $ fmap (snd . typed'value) caseAlt'args)
+    freeVarAlts CaseAlt{..} = caseAlt'rhs `S.difference` (S.fromList $ fmap snd caseAlt'args)
 
 instance TypeFunctor (Term prim) where
   mapType f (Term term) = Term $ foldFix go term
     where
       go = \case
-        Constr loc ty cons       -> Fix $ Constr loc (f ty) cons
-        Case loc e alts          -> Fix $ Case loc e $ fmap applyAlt alts
-        other                    -> Fix other
-
-      applyAlt alt@CaseAlt{..} = alt
-        { caseAlt'args       = fmap applyTyped caseAlt'args
-        , caseAlt'constrType = f caseAlt'constrType
-        }
-
-      applyTyped ty@Typed{..} = ty { typed'type = f typed'type }
+        AssertType loc r ty  -> Fix $ AssertType loc r (f ty)
+        other                 -> Fix other
 
 instance CanApply (Term prim) where
   apply subst term = mapType (apply subst) term
+
+-------------------------------------------------------------------------
+-- sort terms by dependency order (it ignores cyclic depepndencies)
+
+sortDeps :: Ord v => [(v, Term prim loc v)] -> [(v, Term prim loc v)]
+sortDeps = fromDepGraph . stronglyConnComp . toDepGraph
+  where
+    toDepGraph = fmap (\(name, term) -> ((name, term), name, S.toList $ freeVars term))
+
+    fromDepGraph = toList . foldMap getVertex
+      where
+        getVertex = \case
+          AcyclicSCC v -> Seq.singleton v
+          CyclicSCC vs -> Seq.fromList vs
+
+
+
 
diff --git a/src/Type/Check/HM/TyTerm.hs b/src/Type/Check/HM/TyTerm.hs
--- a/src/Type/Check/HM/TyTerm.hs
+++ b/src/Type/Check/HM/TyTerm.hs
@@ -3,6 +3,7 @@
     Ann(..)
   , TyTerm(..)
   , termType
+  , termSignature
   , tyVarE
   , tyPrimE
   , tyAppE
@@ -50,6 +51,9 @@
 termType :: TyTerm prim loc v -> Type loc v
 termType (TyTerm (Fix (Ann ty _))) = ty
 
+termSignature :: (Ord v, Eq loc) => TyTerm prim loc v -> Signature loc v
+termSignature = typeToSignature . termType
+
 -- tyTerm :: Type loc v -> TermF loc var (Ann () ) -> TyTerm loc var
 tyTerm :: Type loc v -> TermF prim loc v (Fix (Ann (Type loc v) (TermF prim loc v))) -> TyTerm prim loc v
 tyTerm ty x = TyTerm $ Fix $ Ann ty x
@@ -89,7 +93,7 @@
 
 -- | 'constrE' @loc ty tag arity@ constructs constructor tag expression.
 tyConstrE :: loc -> Type loc v -> v -> TyTerm prim loc v
-tyConstrE loc ty tag = tyTerm ty $ Constr loc ty tag
+tyConstrE loc ty tag = tyTerm ty $ Constr loc tag
 
 -- | 'bottomE' @loc@ constructs bottom value.
 tyBottomE :: Type loc v -> loc -> TyTerm prim loc v
@@ -106,33 +110,22 @@
         Let loc v a  -> Let (f loc) (v { bind'loc = f $ bind'loc v }) a
         LetRec loc vs a -> LetRec (f loc) (fmap (\b ->  b { bind'loc = f $ bind'loc b }) vs) a
         AssertType loc r sig -> AssertType (f loc) r (mapLoc f sig)
-        Constr loc ty v -> Constr (f loc) (mapLoc f ty) v
+        Constr loc v -> Constr (f loc) v
         Case loc e alts -> Case (f loc) e (fmap (mapAlt f) alts)
         Bottom loc -> Bottom (f loc)
 
       mapAlt g alt@CaseAlt{..} = alt
         { caseAlt'loc  = g caseAlt'loc
-        , caseAlt'args = fmap (mapTyped g) caseAlt'args
-        , caseAlt'constrType = mapLoc g caseAlt'constrType
+        , caseAlt'args = fmap (first g) caseAlt'args
         }
 
-      mapTyped g (Typed ty val) = Typed (mapLoc g ty) (first g val)
-
 instance TypeFunctor (TyTerm prim) where
   mapType f (TyTerm x) = TyTerm $ foldFix go x
     where
       go (Ann ty term) = Fix $ Ann (f ty) $
         case term of
-          Constr loc cty cons -> Constr loc (f cty) cons
-          Case loc e alts          -> Case loc e $ fmap applyAlt alts
-          other                    -> other
-
-      applyAlt alt@CaseAlt{..} = alt
-        { caseAlt'args       = fmap applyTyped caseAlt'args
-        , caseAlt'constrType = f caseAlt'constrType
-        }
-
-      applyTyped ty@Typed{..} = ty { typed'type = f typed'type }
+          AssertType loc r t -> AssertType loc r (f t)
+          other              -> other
 
 instance CanApply (TyTerm prim) where
   apply subst term = mapType (apply subst) term
diff --git a/src/Type/Check/HM/TypeError.hs b/src/Type/Check/HM/TypeError.hs
--- a/src/Type/Check/HM/TypeError.hs
+++ b/src/Type/Check/HM/TypeError.hs
@@ -1,7 +1,7 @@
 {-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DeriveDataTypeable #-}
 {-# LANGUAGE DerivingStrategies #-}
--- | This module contains types for structured type errors.
+-- | This module contains types for type errors.
 module Type.Check.HM.TypeError where
 
 import Control.DeepSeq (NFData)
@@ -19,8 +19,14 @@
   | UnifyErr   loc (Type loc var) (Type loc var)  -- ^ Unification error
   | SubtypeErr loc (Type loc var) (Type loc var)  -- ^ Subtype error (happens on explicit type assertions)
   | NotInScopeErr loc var                         -- ^ Missing signature in context for free-variable.
+  | ConsArityMismatch
+      { consArityMismatch'loc :: loc
+      , consArityMismatch'tag :: var
+      , consArityMismatch'expected :: Int
+      , consArityMismatch'actual   :: Int
+      } -- ^ mismatch of arity in pattern-matching
   | EmptyCaseExpr loc                             -- ^ no case alternatives in the case expression
-  | FreshNameFound                                -- ^ internal error with fresh name substitution
+  | FreshNameFound                                -- ^ internal error with fresh name substitution. Should not normally occur if algorithm is correct.
   deriving stock    (Show, Eq, Functor, Generic, Data)
   deriving anyclass (NFData)
 
@@ -30,6 +36,7 @@
     UnifyErr loc tA tB   -> UnifyErr (f loc) (mapLoc f tA) (mapLoc f tB)
     SubtypeErr loc tA tB -> SubtypeErr (f loc) (mapLoc f tA) (mapLoc f tB)
     NotInScopeErr loc v  -> NotInScopeErr (f loc) v
+    ConsArityMismatch loc tag expect actual -> ConsArityMismatch (f loc)  tag expect actual
     EmptyCaseExpr loc    -> EmptyCaseExpr (f loc)
     FreshNameFound       -> FreshNameFound
 
@@ -39,6 +46,7 @@
     UnifyErr _ a b     -> tyVars a <> tyVars b
     SubtypeErr _ a b   -> tyVars a <> tyVars b
     NotInScopeErr _ _  -> mempty
+    ConsArityMismatch _ _ _ _ -> mempty
     EmptyCaseExpr _    -> mempty
     FreshNameFound     -> mempty
 
@@ -49,6 +57,7 @@
     NotInScopeErr _ _  -> mempty
     EmptyCaseExpr _    -> mempty
     FreshNameFound     -> mempty
+    ConsArityMismatch _ _ _ _ -> mempty
 
 instance CanApply TypeError where
   apply f = \case
diff --git a/test/TM/NumLang.hs b/test/TM/NumLang.hs
--- a/test/TM/NumLang.hs
+++ b/test/TM/NumLang.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TypeFamilies #-}
 -- | Tests for language with lambda calculus with numbers and booleans.
 module TM.NumLang where
@@ -12,6 +13,8 @@
 import qualified Type.Check.HM as T
 import qualified Data.Map.Strict as M
 
+import Data.Text.Prettyprint.Doc
+
 infixr ~>
 
 data CodeLoc = CodeLoc
@@ -20,13 +23,21 @@
   }
   deriving (Show, Eq)
 
+instance Pretty CodeLoc where
+  pretty (CodeLoc row col) = hcat [pretty row, ":", pretty col]
+
 -- | Primitives of our language.
 -- We support integers and booleans
 data Prim
-  = PInt CodeLoc Int     -- ^ integers
-  | PBool CodeLoc Bool   -- ^ booleans
+  = PInt Int     -- ^ integers
+  | PBool Bool   -- ^ booleans
   deriving (Show, Eq)
 
+instance Pretty Prim where
+  pretty = \case
+    PInt  n -> pretty n
+    PBool b -> pretty b
+
 -- | Type for variables
 type Var = String
 
@@ -51,9 +62,9 @@
   type Prim NumLang = Prim      -- ^ primitives
 
   -- what type is assigned to primitive literals of the language
-  getPrimType = \case
-    PInt  loc _ -> T.conT loc "Int"  []
-    PBool loc _ -> T.conT loc "Bool" []
+  getPrimType loc = \case
+    PInt  _ -> T.conT loc "Int"  []
+    PBool _ -> T.conT loc "Bool" []
 
 -- | Expressions for our language
 newtype Expr = Expr { unExpr :: T.Term Prim CodeLoc Var }
@@ -67,11 +78,11 @@
 
 -- | constructor for integer literals
 int :: Int -> Expr
-int = Expr . T.primE defLoc . PInt defLoc
+int = Expr . T.primE defLoc . PInt
 
 -- | constructor for boolean literals
 bool :: Bool -> Expr
-bool = Expr . T.primE defLoc . PBool defLoc
+bool = Expr . T.primE defLoc . PBool
 
 -- numeric expressions
 
@@ -152,36 +163,75 @@
 -- custom constructors
 
 -- types for custom types
-pointT, circleT, rectT :: Ty
+pointT, circleT, rectT, colorT :: Ty
 pointT  = T.conT defLoc "Point" []
 circleT = T.conT defLoc "Circle" []
 rectT = T.conT defLoc "Rect" []
+colorT = T.conT defLoc "Color" []
 
+maybeT :: Ty -> Ty
+maybeT a = T.conT defLoc "Maybe" [a]
+
 -- | Point constructor
 point :: Expr -> Expr -> Expr
-point = app2 (Expr $ T.constrE defLoc (intT ~> intT ~> pointT) "Point")
+point = app2 (Expr $ T.constrE defLoc "Point")
 
 circle :: Expr -> Expr -> Expr
-circle = app2 (Expr $ T.constrE defLoc (pointT ~> intT ~> circleT) "Circle")
+circle = app2 (Expr $ T.constrE defLoc "Circle")
 
 rect :: Expr -> Expr -> Expr
-rect = app2 (Expr $ T.constrE defLoc (pointT ~> pointT ~> rectT) "Rect")
+rect = app2 (Expr $ T.constrE defLoc "Rect")
 
+red, blue, green :: Expr
+red   = Expr $ T.constrE defLoc "Red"
+blue  = Expr $ T.constrE defLoc "Blue"
+green = Expr $ T.constrE defLoc "Green"
+
+just :: Expr -> Expr
+just = app (Expr $ T.constrE defLoc "Just")
+
+nothing :: Expr
+nothing = Expr $ T.constrE defLoc "Nothing"
+
 casePoint :: Expr -> (Var, Var) -> Expr -> Expr
 casePoint (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e
-  [T.CaseAlt defLoc "Point" [tyVar intT x, tyVar intT y] pointT body]
+  [T.CaseAlt defLoc "Point" (caseArgs [x, y]) body]
 
 caseCircle :: Expr -> (Var, Var) -> Expr -> Expr
 caseCircle (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e
-  [T.CaseAlt defLoc "Circle" [tyVar pointT x, tyVar intT y] circleT body]
+  [T.CaseAlt defLoc "Circle" (caseArgs [x, y]) body]
 
 caseRect :: Expr -> (Var, Var) -> Expr -> Expr
 caseRect (Expr e) (x, y) (Expr body) = Expr $ T.caseE defLoc e
-  [T.CaseAlt defLoc "Rect" [tyVar pointT x, tyVar pointT y] rectT body]
+  [T.CaseAlt defLoc "Rect" (caseArgs [x, y]) body]
 
-tyVar :: Ty -> Var -> T.Typed CodeLoc Var (CodeLoc, Var)
-tyVar ty v = T.Typed ty (defLoc, v)
+caseArgs :: [Var] -> [(CodeLoc, Var)]
+caseArgs = fmap (\x -> (defLoc, x))
 
+data CaseColor = CaseColor
+  { case'red   :: Expr
+  , case'blue  :: Expr
+  , case'green :: Expr
+  }
+
+caseColor :: Expr -> CaseColor -> Expr
+caseColor (Expr e) CaseColor{..} = Expr $ T.caseE defLoc e
+  [ T.CaseAlt defLoc "Red"   [] (unExpr $ case'red)
+  , T.CaseAlt defLoc "Blue"  [] (unExpr $ case'blue)
+  , T.CaseAlt defLoc "Green" [] (unExpr $ case'green)
+  ]
+
+data CaseMaybe = CaseMaybe
+  { case'just    :: Expr -> Expr
+  , case'nothing :: Expr
+  }
+
+caseMaybe :: Expr -> CaseMaybe -> Expr
+caseMaybe (Expr e) CaseMaybe{..} = Expr $ T.caseE defLoc e
+  [ T.CaseAlt defLoc "Just"    [(defLoc, "$justArg")] (unExpr $ case'just "$justArg")
+  , T.CaseAlt defLoc "Nothing" []              (unExpr case'nothing)
+  ]
+
 ----------------------------------------------------------
 -- Type inference context
 --
@@ -190,13 +240,29 @@
 
 -- | Context contains types for all known definitions
 defContext :: T.Context CodeLoc Var
-defContext = T.Context $ M.fromList $ mconcat
-  [ booleans
-  , nums
-  , comparisons
-  , [("if", forA $ T.monoT $ boolT ~> aT ~> aT ~> aT)]
-  ]
+defContext = T.Context
+  { T.context'binds        = binds
+  , T.context'constructors = cons
+  }
   where
+    binds = M.fromList $ mconcat
+      [ booleans
+      , nums
+      , comparisons
+      , [("if", forA $ T.monoT $ boolT ~> aT ~> aT ~> aT)]
+      ]
+
+    cons = M.fromList
+      [ "Point"  `is` (intT ~> intT ~> pointT)
+      , "Circle" `is` (pointT ~> intT ~> circleT)
+      , "Rect"   `is` (pointT ~> pointT ~> rectT)
+      , "Red"    `is` colorT
+      , "Blue"   `is` colorT
+      , "Green"  `is` colorT
+      , ("Just"    , forA $ T.monoT $ aT ~> maybeT aT)
+      , ("Nothing" , forA $ T.monoT $ maybeT aT)
+      ]
+
     booleans =
       [ "&&"  `is` (boolT ~> boolT ~> boolT)
       , "||"  `is` (boolT ~> boolT ~> boolT)
@@ -230,6 +296,52 @@
 boolExpr1 :: Expr
 boolExpr1 = andB (andB (notB ((intExpr1 `lte` 1000) `orB` (2 `gt` 0))) (bool True)) (5 `neq` (2 + 2))
 
+colorFun :: Expr
+colorFun = lam "c" $ caseColor "c" CaseColor
+  { case'red   = 1
+  , case'blue  = 2
+  , case'green = 3
+  }
+
+colorFun2 :: Expr
+colorFun2 = lam "c" $ caseColor "c" CaseColor
+  { case'red   = nothing
+  , case'blue  = just $ bool True
+  , case'green = just $ bool False
+  }
+
+colorFun3 :: Expr
+colorFun3 = lam "c" $ caseColor "c" CaseColor
+  { case'blue  = just $ bool True
+  , case'green = just $ bool False
+  , case'red   = nothing
+  }
+
+colorFun4 :: Expr
+colorFun4 = lam "mc" $ caseMaybe "mc" CaseMaybe
+  { case'just    = id
+  , case'nothing = red
+  }
+
+colorFunFail :: Expr
+colorFunFail = lam "c" $ caseColor "c" CaseColor
+  { case'red   = 1
+  , case'blue  = bool True
+  , case'green = 3
+  }
+
+mapMaybe :: Expr
+mapMaybe = lam "f" $ lam "ma" $ caseMaybe "ma" CaseMaybe
+  { case'nothing = nothing
+  , case'just    = \a -> just $ app "f" a
+  }
+
+bindMaybe :: Expr
+bindMaybe = lam "ma" $ lam "mf" $ caseMaybe "ma" CaseMaybe
+  { case'nothing = nothing
+  , case'just    = \a -> app "mf" a
+  }
+
 failExpr1 :: Expr
 failExpr1 = lam "x" $ 2 + "x" `eq` (bool True)
 
@@ -319,9 +431,28 @@
   , check "negate point"    (pointT ~> pointT)              negatePointLam
   , check "rect square"     (rectT ~> intT)                 rectSquare
   , check "inside circle 2" (circleT ~> pointT ~> boolT)    insideCircle2
+  , check "color fun"       (colorT ~> intT)                colorFun
+  , check "color fun 2"     (colorT ~> maybeT boolT)        colorFun2
+  , check "color fun 3"     (colorT ~> maybeT boolT)        colorFun3
+  , check "color fun 4"     (maybeT colorT ~> colorT)       colorFun4
+  , check "map maybe"       ((aT ~> bT) ~> maybeT aT ~> maybeT bT) mapMaybe
+  , check "bind maybe"      (maybeT aT ~> (aT ~> maybeT bT) ~> maybeT bT) bindMaybe
+  , fails "color fun fail"  colorFunFail
+  , checkList "list of expressions" [("a", intExpr1), ("b", boolExpr1), ("c", intFun1)]
   ]
   where
+    aT = T.varT defLoc "a"
+    bT = T.varT defLoc "b"
+
     infer = T.inferType defContext . unExpr
     check msg ty expr = testCase msg $ Right ty @=? (infer expr)
     fails msg expr = testCase msg $ assertBool "Detected wrong type" $ isLeft (infer expr)
+
+    checkList msg exprs = testCase msg $ assertBool msg $ isRight (T.inferTermList defContext $ fmap (uncurry toBind) exprs)
+
+----------------------------------------------------------
+
+-- | Prints result of type-inference
+printInfer :: Expr -> IO ()
+printInfer (Expr e) = T.printInfer $ T.inferType defContext e
 
diff --git a/test/TM/SKI.hs b/test/TM/SKI.hs
--- a/test/TM/SKI.hs
+++ b/test/TM/SKI.hs
@@ -35,7 +35,7 @@
   type Src  TestLang = ()
   type Var  TestLang = Text
   type Prim TestLang = NoPrim
-  getPrimType _ = error "No primops"
+  getPrimType _ _ = error "No primops"
 
 -- I combinator
 termI,termK :: Term NoPrim () Text