diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,29 @@
+Copyright MIT license 
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Anton Kholomiov nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/hindley-milner-type-check.cabal b/hindley-milner-type-check.cabal
new file mode 100644
--- /dev/null
+++ b/hindley-milner-type-check.cabal
@@ -0,0 +1,93 @@
+name:                   hindley-milner-type-check
+version:                0.1.0.0
+synopsis:               Type inference for Hindley-Milner based languages
+description:
+    This package contains an implemention of Hindley-Milner inference algorithm.
+    It supports reporting of source code locations for errors.
+    Language for type inference is labda-calculus augmented with primitive
+    functions, let-expressions,  case-expressions and bottom.
+
+    See github repo for tutorial and test-cases for examples.
+
+
+license:                MIT
+license-file:           LICENSE
+author:                 Anton Kholomiov, Aleksey Khudyakov
+maintainer:             anton.kholomiov@gmail.com
+category:               Language
+build-type:             Simple
+cabal-version:          >=1.22
+
+source-repository head
+  type:                 git
+  location:             https://github.com/anton-k/hindley-milner-type-check
+
+library
+  ghc-options:  -Wall
+  exposed-modules:
+    Type.Check.HM,
+    Type.Check.HM.Infer,
+    Type.Check.HM.Lang
+    Type.Check.HM.Pretty,
+    Type.Check.HM.Subst,
+    Type.Check.HM.Term,
+    Type.Check.HM.Type,
+    Type.Check.HM.TypeError,
+    Type.Check.HM.TyTerm
+
+  other-modules:
+
+  -- Other library packages from which modules are imported.
+  build-depends: base                      >=4.8 && <5
+               , deepseq                   >=1.4
+               , containers                >=0.5
+               , deriving-compat
+               , data-fix                  >=0.3
+               , dlist
+               , mtl
+               , prettyprinter
+               , text
+
+  -- Directories containing source files.
+  hs-source-dirs:       src
+
+  -- Base language which the package is written in.
+  default-language:     Haskell2010
+
+  default-extensions:
+    DeriveDataTypeable
+    DeriveFunctor,
+    DeriveFoldable,
+    DeriveTraversable,
+    DeriveGeneric,
+    FlexibleContexts,
+    FlexibleInstances,
+    GeneralizedNewtypeDeriving,
+    LambdaCase,
+    MultiParamTypeClasses,
+    OverloadedStrings,
+    RankNTypes
+    RecordWildCards,
+    ScopedTypeVariables,
+    StandaloneDeriving,
+    TemplateHaskell,
+    TupleSections,
+    TypeFamilies,
+    TypeSynonymInstances
+
+test-suite hindley-milner-tests
+  Type:                exitcode-stdio-1.0
+  Ghc-options:         -Wall -threaded -rtsopts
+  Default-Language:    Haskell2010
+  Build-Depends:       base              >=4.9 && <5
+                     , hindley-milner-type-check
+                     , containers
+                     , text
+                     , data-fix                  >=0.3
+                     , tasty
+                     , tasty-hunit
+                     , prettyprinter
+  hs-source-dirs:      test
+  Main-is:             Main.hs
+  Other-modules:       TM.SKI
+                     , TM.NumLang
diff --git a/src/Type/Check/HM.hs b/src/Type/Check/HM.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM.hs
@@ -0,0 +1,28 @@
+-- | This module exports all useful functions of the library
+module Type.Check.HM (
+  -- * Language definition
+  module Type.Check.HM.Lang,
+
+  -- * Types
+  module Type.Check.HM.Type,
+
+  -- * Terms
+  module Type.Check.HM.Term,
+
+  -- * Typed terms
+  module Type.Check.HM.TyTerm,
+
+  -- * Inference
+  module Type.Check.HM.Infer,
+
+  -- * Errors
+  module Type.Check.HM.TypeError,
+) where
+
+import Type.Check.HM.Infer
+import Type.Check.HM.Lang
+import Type.Check.HM.Pretty      as X()
+import Type.Check.HM.Term
+import Type.Check.HM.Type
+import Type.Check.HM.TypeError
+import Type.Check.HM.TyTerm
diff --git a/src/Type/Check/HM/Infer.hs b/src/Type/Check/HM/Infer.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/Infer.hs
@@ -0,0 +1,620 @@
+-- | Defines type-inference algorithm.
+--
+-- For type inference we have to define instance of the Lang class:
+--
+-- > data NoPrim
+-- >   deriving (Show)
+-- >
+-- > data TestLang
+-- >
+-- > instance Lang TestLang where
+-- >   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
+--
+-- 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.
+--
+-- > context = Context $ Map.fromList [...]
+--
+-- Then we can use inference to derive type for given term with @inferType@ or
+-- we can derive types for all sub-expressions of given term with @inferTerm@.
+-- See module in the test "TM.Infer" for examples of the usage.
+--
+-- > termI,termK :: Term NoPrim () Text
+-- >
+-- > -- I combinator
+-- > termI = lamE () "x" $ varE () "x"
+-- > -- K combinator
+-- > termK = lamE () "x" $ lamE () "y" $ varE () "x"
+-- >
+-- > -- Let's infer types
+-- > typeI = inferType mempty termI
+-- > typeK = inferType mempty termK
+--
+-- There are functions to check that two types unify (@unifyTypes@) or that one type
+-- is subtype of another one (@subtypeOf@).
+module Type.Check.HM.Infer(
+  -- * Context
+    Context(..)
+  , insertCtx
+  , lookupCtx
+  , ContextOf
+  -- * Inference
+  , inferType
+  , inferTerm
+  , subtypeOf
+  , unifyTypes
+  -- * Utils
+  , closeSignature
+) where
+
+import Control.Monad.Identity
+
+import Control.Applicative
+import Control.Arrow (second)
+import Control.Monad.Except
+import Control.Monad.State.Strict
+
+import Data.Bifunctor (bimap)
+import Data.Fix
+import Data.Function (on)
+import Data.Map.Strict (Map)
+import Data.Maybe
+
+import Type.Check.HM.Lang
+import Type.Check.HM.Term
+import Type.Check.HM.Subst
+import Type.Check.HM.Type
+import Type.Check.HM.TypeError
+import Type.Check.HM.TyTerm
+
+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)
+
+-- | Type synonym for context.
+type ContextOf q = Context (Src q) (Var q)
+
+instance CanApply Context where
+  apply subst = Context . fmap (apply subst) . unContext
+
+-- | 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
+
+-- | 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
+
+-- | Wrapper with ability to generate fresh names
+data Name v
+  = Name v
+  | FreshName !Int
+  deriving (Show, Eq, Ord)
+
+fromNameVar :: Name v -> Either (TypeError loc v) v
+fromNameVar = \case
+  Name v      -> Right v
+  FreshName _ -> Left FreshNameFound
+
+instance IsVar a => IsVar (Name a) where
+  prettyLetters = fmap Name (prettyLetters :: [a])
+
+-- Synonyms to simplify typing
+type Context' loc v = Context (Origin loc) (Name v)
+type Type' loc v = Type (Origin loc) (Name v)
+type Signature' loc v = Signature (Origin loc) (Name v)
+type Subst' loc v = Subst (Origin loc) (Name v)
+type Bind' loc v a = Bind (Origin loc) (Name v) a
+type VarSet' loc v = VarSet (Origin loc) (Name v)
+
+type ContextOf' q = Context (Origin (Src q)) (Name (Var q))
+type TypeOf' q = Type (Origin (Src q)) (Name (Var q))
+type TermOf' q = Term (Prim q) (Origin (Src q)) (Name (Var q))
+type TyTermOf' q = TyTerm (Prim q) (Origin (Src q)) (Name (Var q))
+type SignatureOf' q = Signature (Origin (Src q)) (Name (Var q))
+type SubstOf' q = Subst (Origin (Src q)) (Name (Var q))
+type BindOf' q a = Bind (Origin (Src q)) (Name (Var q)) a
+type CaseAltOf' q = CaseAlt (Origin (Src q)) (Name (Var q))
+
+-- | We leave in the context only terms that are truly needed.
+-- 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
+  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
+
+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
+
+markUserCode :: Term prim loc v -> Term prim (Origin loc) v
+markUserCode = mapLoc UserCode
+
+chooseUserOrigin :: Show a => Origin a -> Origin a -> a
+chooseUserOrigin x y = case (x, y) of
+  (UserCode a, _) -> a
+  (_, UserCode a) -> a
+  _               -> fromOrigin x
+
+-- | Type-tag for source locations to distinguish proven types from those
+-- that have to be checked.
+--
+-- We use it on unification failure to show source locations in the user code and not in the
+-- expression that is already was proven.
+data Origin a
+  = Proven a
+  -- ^ Proven source code location
+  | UserCode a
+  -- ^ User source code (we type-check it)
+  deriving (Show, Functor)
+
+fromOrigin :: Origin a -> a
+fromOrigin = \case
+  Proven   a -> a
+  UserCode a -> a
+
+instance Eq a => Eq (Origin a) where
+  (==) = (==) `on` fromOrigin
+
+instance Ord a => Ord (Origin a) where
+  compare = compare `on` fromOrigin
+
+instance HasLoc a => HasLoc (Origin a) where
+  type Loc (Origin a) = Loc a
+  getLoc = getLoc . fromOrigin
+
+-- | 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)))
+
+-- | Runs inference monad.
+runInferM :: InferM loc var a -> Either (TypeError loc (Name var)) a
+runInferM (InferM m) = runExcept $ evalStateT m 0
+
+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 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)
+  where
+    toTyTerm = fromTyTermNameVar . normaliseType . mapLoc fromOrigin
+
+type Out prim loc var = ( Subst (Origin loc) (Name var)
+                        , TyTerm prim (Origin loc) (Name var)
+                        )
+
+infer :: Lang q => ContextOf' q -> TermOf' q -> InferOf q
+infer ctx (Term (Fix x)) = case x of
+  Var loc v           -> inferVar ctx loc v
+  Prim loc p          -> inferPrim loc p
+  App loc a b         -> inferApp ctx loc (Term a) (Term b)
+  Lam loc v r         -> inferLam ctx loc v (Term r)
+  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
+  Case loc e alts     -> inferCase ctx loc (Term e) (fmap (fmap Term) alts)
+  Bottom loc          -> 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
+    Just sig -> do ty <- newInstance $ setLoc loc sig
+                   return (mempty, tyVarE ty loc v)
+
+inferPrim :: Lang q => Origin (Src q) -> Prim q -> InferOf q
+inferPrim loc prim =
+  return (mempty, tyPrimE ty loc prim)
+  where
+    ty = fmap Name $ mapLoc UserCode $ getPrimType 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)
+    _               -> error "Impossible has happened!"
+
+inferLam :: Lang q => ContextOf' q -> Origin (Src q) -> Name (Var q) -> TermOf' q -> InferOf q
+inferLam ctx loc x body = do
+  tvn <- freshVar
+  (phi, bodyTyTerm) <- infer (ctx1 tvn) body
+  let ty = arrowT loc (apply phi (varT loc tvn)) (termType bodyTyTerm)
+  return (phi, tyLamE ty loc x bodyTyTerm)
+  where
+    ctx1 tvn = insertCtx x (newVar loc tvn) ctx
+
+inferLet :: Lang q => ContextOf' q -> Origin (Src q) -> BindOf' q (TermOf' q) -> TermOf' q -> InferOf q
+inferLet ctx loc v body = do
+  (phi, rhsTyTerm) <- infer ctx $ bind'rhs v
+  let tBind = termType rhsTyTerm
+  ctx1 <- addDecls [fmap (const tBind) v] (apply phi ctx)
+  (subst, bodyTerm) <- infer ctx1 body
+  let subst1 = phi <> subst
+      tyBind = v { bind'rhs = apply subst1 rhsTyTerm }
+  return ( subst1
+         , apply subst1 $ tyLetE (termType bodyTerm) loc tyBind bodyTerm
+         )
+
+inferLetRec :: forall q . Lang q
+  => ContextOf' q -> Origin (Src q) -> [BindOf' q (TermOf' q)] -> TermOf' q
+  -> InferOf q
+inferLetRec ctx topLoc vs body = do
+  lhsCtx <- getTypesLhs vs
+  (phi, rhsTyTerms) <- inferTerms (ctx <> Context (M.fromList lhsCtx)) exprBinds
+  let (tBinds, bindsTyTerms) = unzip rhsTyTerms
+  (ctx1, lhsCtx1, subst) <- unifyRhs ctx lhsCtx phi tBinds
+  inferBody bindsTyTerms ctx1 lhsCtx1 subst body
+  where
+    exprBinds = fmap bind'rhs vs
+    locBinds  = fmap bind'loc vs
+
+    getTypesLhs :: [BindOf' q (TermOf' q)] -> InferM (Src q) (Var q) [(Name (Var q), SignatureOf' q)]
+    getTypesLhs lhs = mapM (\b -> fmap ((bind'lhs b, ) . newVar (bind'loc b)) freshVar) lhs
+
+    unifyRhs context lhsCtx phi tBinds =
+      fmap (\subst -> (context1, lhsCtx1, subst)) $ unifyl phi ts tBinds
+      where
+        context1 = apply phi context
+        lhsCtx1  = fmap (second $ apply phi) lhsCtx
+        ts = fmap (oldBvar . snd) lhsCtx1
+
+    oldBvar = foldFix go . unSignature
+      where
+        go  = \case
+          MonoT t       -> t
+          ForAllT _ _ t -> t
+
+    inferBody termBinds context lhsCtx subst expr = do
+      ctx1 <- addDecls (zipWith (\loc (v, ty) -> Bind loc v ty) locBinds $ fmap (second $ oldBvar . apply subst) lhsCtx) $ apply subst context
+      (phi, bodyTerm) <- infer ctx1 expr
+      let tyBinds = zipWith (\bind rhs -> bind { bind'rhs = rhs }) vs termBinds
+      return (subst <> phi, tyLetRecE (termType bodyTerm) topLoc tyBinds bodyTerm)
+
+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)
+
+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)
+
+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)
+  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
+      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
+        }
+
+    getCaseType :: CaseAltOf' q (TermOf' q) -> TypeOf' q
+    getCaseType CaseAlt{..} = funT (fmap typed'type caseAlt'args) caseAlt'constrType
+
+    splitFunT :: TypeOf' q -> ([TypeOf' q], TypeOf' q)
+    splitFunT arrT = go [] arrT
+      where
+        go argsT (Type (Fix t)) = case t of
+          ArrowT _loc a b -> go (Type a : argsT) (Type b)
+          other           -> (reverse argsT, Type $ Fix other)
+
+
+    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
+  return (mempty, tyBottomE ty loc)
+
+newInstance :: IsVar v => Signature loc (Name v) -> InferM loc' v (Type loc (Name v))
+newInstance = fmap (uncurry apply) . foldFixM go . unSignature
+  where
+    go = \case
+      MonoT ty -> return (mempty, ty)
+      ForAllT loc v (Subst m, ty) -> fmap (\nv -> (Subst $ M.insert v (varT loc nv) m, ty)) freshVar
+
+newVar :: loc -> v -> Signature loc v
+newVar loc tvn = monoT $ varT loc tvn
+
+freshVar :: IsVar v => InferM loc v (Name v)
+freshVar = do
+  n <- get
+  put $ n + 1
+  return $ FreshName n
+
+inferTerms :: Lang q
+  => ContextOf' q
+  -> [TermOf' q]
+  -> InferM (Src q) (Var q) (SubstOf' q, [(TypeOf' q, TyTermOf' q)])
+inferTerms ctx ts = case ts of
+  []   -> return $ (mempty, [])
+  a:as -> do
+    (phi, termA) <- infer ctx a
+    let ta = termType termA
+    (psi, tas) <- inferTerms (apply phi ctx) as
+    return ( phi <> psi
+           , (apply psi ta, apply psi termA) : tas
+           )
+
+-- | Unification function. Checks weather two types unify.
+-- First argument is current substitution.
+unify :: (IsVar v, Show loc, MonadError (TypeError loc (Name v)) m)
+  => Subst' loc v
+  -> Type' loc v
+  -> Type' loc v
+  -> m (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) ->
+        let phiTvn = applyVar phi loc tvn
+            phiT   = apply phi (Type (Fix t))
+        in  if phiTvn `eqIgnoreLoc` varT loc tvn
+              then extend phi loc tvn phiT
+              else unify phi phiTvn phiT
+    (a, VarT locB v) -> unify phi (varT locB v) (Type $ Fix a) -- (conT locA name $ fmap Type ts)
+    (ConT locA n xs, ConT locB m ys) ->
+      if n == m
+        then unifyl phi (fmap Type xs) (fmap Type ys)
+        else unifyErr locA locB
+    (ArrowT _ a1 a2, ArrowT _ b1 b2) -> unifyl phi (fmap Type [a1, a2]) (fmap Type [b1, b2])
+    (TupleT locA xs, TupleT locB ys) ->
+      if length xs == length ys
+        then unifyl phi (fmap Type xs) (fmap Type ys)
+        else unifyErr locA locB
+    (ListT _ a, ListT _ b) -> unify phi (Type a) (Type b)
+    (a, b) -> unifyErr (getLoc $ Type $ Fix a) (getLoc $ Type $ Fix b)
+  where
+    unifyErr locA locB = throwError $
+      UnifyErr (chooseUserOrigin locA locB)
+               (mapLoc fromOrigin $ Type (Fix x))
+               (mapLoc fromOrigin $ Type (Fix y))
+
+eqIgnoreLoc :: Eq v => Type loc v -> Type loc v -> Bool
+eqIgnoreLoc = (==) `on` mapLoc (const ())
+
+applyVar :: IsVar v => Subst' loc v -> Origin loc -> Name v -> Type' loc v
+applyVar (Subst subst) loc v = fromMaybe (varT loc v) $ M.lookup v subst
+
+extend
+  :: (IsVar v, MonadError (TypeError loc (Name v)) m)
+  => Subst' loc v -> Origin loc -> Name v -> Type' loc v -> m (Subst' loc v)
+extend phi loc tvn ty
+  | varT loc tvn `eqIgnoreLoc` ty = return phi
+  | 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)
+  => Subst' loc v
+  -> [Type' loc v]
+  -> [Type' loc v]
+  -> m (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
+
+-- | Checks if first argument one type is subtype of the second one.
+subtypeOf :: (IsVar v, Show loc, Eq loc)
+  => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
+subtypeOf a b =
+  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)
+  => Subst' loc v
+  -> Type' loc v
+  -> Type' loc v
+  -> m (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) ->
+    if n == m
+      then subtypeOfL phi (fmap Type xs) (fmap Type ys)
+      else subtypeErr locA locB
+  (ArrowT _ a1 a2, ArrowT _ b1 b2) -> subtypeOfL phi (fmap Type [a1, a2]) (fmap Type [b1, b2])
+  (TupleT locA as, TupleT locB bs) ->
+    if length as == length bs
+      then subtypeOfL phi (fmap Type as) (fmap Type bs)
+      else subtypeErr locA locB
+  (ListT _ a, ListT _ b) -> genSubtypeOf phi (Type a) (Type b)
+  (VarT locA _, _) -> subtypeErr locA (getLoc ty)
+  _ -> subtypeErr (getLoc tx) (getLoc ty)
+  where
+    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)
+  => Subst' loc v
+  -> [Type' loc v]
+  -> [Type' loc v]
+  -> m (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
+
+addDecls :: IsVar v
+  => [Bind (Origin loc) (Name v) (Type' loc v)]
+  -> Context' loc v
+  -> InferM loc v (Context' loc v)
+addDecls vs ctx =
+  foldM  (\c b -> addDecl unknowns b c) ctx vs
+  where
+    unknowns = foldMap tyVars $ unContext ctx
+
+addDecl :: forall loc v . IsVar v
+  => VarSet' loc v
+  -> Bind' loc v (Type' loc v)
+  -> Context' loc v
+  -> 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
+  where
+    toScheme :: VarSet' loc v -> Type' loc v -> InferM loc v (Signature' loc v)
+    toScheme uVars ty = do
+      (subst, newVars) <- fmap (\xs -> (toSubst xs, fmap (\((loc, _), v) -> (loc, v)) xs)) $
+          mapM (\sv -> fmap ((sv, )) freshVar) $ varSetToList schematicVars
+      return $ foldr (uncurry forAllT) (monoT (apply subst ty)) newVars
+      where
+        schematicVars = tyVars ty `differenceVarSet` uVars
+
+    toSubst = Subst . M.fromList . fmap (\((loc, v), a) -> (v, varT loc a))
+
+-------------------------------------------------------
+-- pretty letters for variables in the result type
+
+-- | Converts variable names to human-readable format.
+normaliseType :: (HasTypeVars m, CanApply m, IsVar v, Show loc, Eq loc) => m loc (Name v) -> m loc (Name v)
+normaliseType ty = apply (normaliseSubst ty) ty
+
+normaliseSubst :: (HasTypeVars m, Show loc, Eq loc, IsVar v) => m loc v -> Subst loc v
+normaliseSubst x =
+  Subst $ M.fromList $
+    zipWith (\(nameA, loc) nameB -> (nameA, varT loc nameB)) (tyVarsInOrder x) prettyLetters
+
+------------------------------------------------
+--
+
+-- | Checks weather two types unify. If they do it returns substitution that unifies them.
+unifyTypes :: (Show loc, IsVar v, Eq loc) => Type loc v -> Type loc v -> Either (TypeError loc v) (Subst loc v)
+unifyTypes a b =
+  join $ bimap (fromTypeErrorNameVar . normaliseType) (fromSubstNameVar . fromSubstOrigin) $
+    unify mempty (fmap Name $ mapLoc Proven a) (fmap Name $ mapLoc UserCode b)
+
+------------------------------------------------
+-- recover name and origin wrappers
+
+fromTypeErrorNameVar :: TypeError loc (Name var) -> TypeError loc var
+fromTypeErrorNameVar = either id id . \case
+    OccursErr loc ty     -> fmap (OccursErr loc) (fromTypeNameVar ty)
+    UnifyErr loc tA tB   -> liftA2 (UnifyErr loc) (fromTypeNameVar tA) (fromTypeNameVar tB)
+    SubtypeErr loc tA tB -> liftA2 (SubtypeErr loc) (fromTypeNameVar tA) (fromTypeNameVar tB)
+    NotInScopeErr loc v  -> fmap (NotInScopeErr loc) $ fromNameVar v
+    EmptyCaseExpr loc    -> pure $ EmptyCaseExpr loc
+    FreshNameFound       -> pure FreshNameFound
+
+fromTypeNameVar :: Type loc (Name var) -> Either (TypeError loc var) (Type loc var)
+fromTypeNameVar (Type x) = fmap Type $ foldFixM go x
+  where
+    go :: TypeF loc (Name var) (Fix (TypeF loc var)) -> Either (TypeError loc var) (Fix (TypeF loc var))
+    go = \case
+      VarT loc v     -> fmap (Fix . VarT loc) $ fromNameVar v
+      ConT loc v as  -> fmap (\con -> Fix $ ConT loc con as) $ fromNameVar v
+      ArrowT loc a b -> pure $ Fix $ ArrowT loc a b
+      TupleT loc as  -> pure $ Fix $ TupleT loc as
+      ListT loc as   -> pure $ Fix $ ListT loc as
+
+fromTyTermNameVar :: TyTerm prim loc (Name var) -> Either (TypeError loc var) (TyTerm prim loc var)
+fromTyTermNameVar (TyTerm x) = fmap TyTerm $ foldFixM go x
+  where
+    go (Ann annTy term) = liftA2 (\t val -> Fix $ Ann t val) (fromTypeNameVar annTy) $ case term of
+      Var loc v           -> fmap (Var loc) $ fromNameVar v
+      Prim loc p          -> pure $ Prim loc p
+      App loc a b         -> pure $ App loc a b
+      Lam loc v a         -> fmap (\arg -> Lam loc arg a) $ fromNameVar v
+      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)
+      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 })
+        (fromNameVar caseAlt'tag)
+        (mapM fromTyped caseAlt'args)
+        (fromTypeNameVar caseAlt'constrType)
+
+    fromTyped Typed{..} = liftA2 Typed (fromTypeNameVar typed'type) (mapM fromNameVar typed'value)
+
+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
+  where
+    uncover (v, ty) = liftA2 (,) (fromNameVar v) (fromTypeNameVar ty)
+
+fromSubstOrigin :: Ord v => Subst (Origin loc) v -> Subst loc v
+fromSubstOrigin = Subst . M.map (mapLoc fromOrigin) . unSubst
+
+-- | Substitutes all type arguments with given types.
+closeSignature :: Ord var => [Type loc var] -> Signature loc var -> Type loc var
+closeSignature argTys sig = apply (Subst $ M.fromList $ zip argNames argTys) monoTy
+  where
+    (argNames, monoTy) = splitSignature sig
+
diff --git a/src/Type/Check/HM/Lang.hs b/src/Type/Check/HM/Lang.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/Lang.hs
@@ -0,0 +1,68 @@
+{-# Language TypeFamilyDependencies #-}
+-- | Main class for the library that defines common types and primitives for the language.
+module Type.Check.HM.Lang(
+  -- * Lang
+    Lang(..)
+  , TypeOf
+  , TermOf
+  , TyTermOf
+  , SubstOf
+  , ErrorOf
+) where
+
+import Type.Check.HM.Term
+import Type.Check.HM.Subst
+import Type.Check.HM.Type
+import Type.Check.HM.TypeError
+import Type.Check.HM.TyTerm
+
+-- | Main class to define inference API.
+-- For type inference we have to define instance of the Lang class:
+--
+-- > data NoPrim
+-- >   deriving (Show)
+-- >
+-- > data TestLang
+-- >
+-- > instance Lang TestLang where
+-- >   type Src  TestLang = ()
+-- >   type Var  TestLang = Text
+-- >   type Prim TestLang = NoPrim
+-- >   getPrimType _ = error "No primops"
+--
+class
+  ( IsVar (Var q)
+  , Show (Src q)
+  , Show (Prim q)
+  , Eq (Src q)
+  ) => Lang q where
+
+  -- | Variables for our language. Notice that this type should be injective in relation to type of @Lang@.
+  -- We need to have unique type of variables for each language definition.
+  type Var q = r | r -> q
+
+  -- | Source code locations
+  type Src q
+
+  -- | Primitives
+  type Prim q
+
+  -- | Reports type for primitive.
+  getPrimType :: Prim q -> TypeOf q
+
+-- | Types of our language
+type TypeOf q = Type (Src q) (Var q)
+
+-- | |Terms of our language
+type TermOf q = Term (Prim q) (Src q) (Var q)
+
+-- | Typed terms of our language
+type TyTermOf q = TyTerm (Prim q) (Src q) (Var q)
+
+-- | Type errors of our language
+type ErrorOf q = TypeError (Src q) (Var q)
+
+-- | Type substitutions
+type SubstOf q = Subst (Src q) (Var q)
+
+
diff --git a/src/Type/Check/HM/Pretty.hs b/src/Type/Check/HM/Pretty.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/Pretty.hs
@@ -0,0 +1,184 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+-- | Pretty printer for types and terms.
+module Type.Check.HM.Pretty(
+    HasPrefix(..)
+  , PrintCons(..)
+  , OpFix(..)
+  , Fixity(..)
+) where
+
+import Data.Bool
+import Data.Fix
+import Data.Maybe
+import Data.Text (Text)
+import Data.Text.Prettyprint.Doc
+
+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
+
+instance HasPrefix String where
+  getFixity = const Nothing
+
+instance HasPrefix Int where
+  getFixity = 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 Text where
+  printCons name args = hsep $ pretty name : args
+
+isPrefix :: HasPrefix v => v -> Bool
+isPrefix = isNothing . getFixity
+
+isInfix :: HasPrefix v => v -> Bool
+isInfix  = not . isPrefix
+
+instance (Pretty v, PrintCons v, HasPrefix v) => Pretty (Signature loc v) where
+  pretty = foldFix go . unSignature
+    where
+      go = \case
+        ForAllT _ _ r -> r
+        MonoT ty      -> pretty ty
+
+instance (HasPrefix v, PrintCons v, Pretty v) => Pretty (Type loc v) where
+  pretty = go False initCtx . unType
+    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 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) $
+            printCons name $ fmap (go False (FcRight OpFunAp)) args
+
+          fromBin op a b = maybeParens (needsParens 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
+            [ go True (FcLeft ArrowOp ) a
+            , "->"
+            , go True (FcRight ArrowOp) b
+            ]
+
+          fromTuple as = parens $ hsep $ punctuate comma $ fmap (pretty . Type) as
+
+          fromList a = brackets $ pretty $ 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
+  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
+      -- otherwise the two operators have the same precedence
+      | 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
+      -- otherwise the two operators have the same precedence
+      | fixity ctxt /= fixity op = True
+      | fixity ctxt == FixRight = False
+      | otherwise = True
+
+data PartialOrdering = PoLT | PoGT | PoEQ | PoNC
+  deriving Eq
+
+-- | Defines fixity type and order of infix operation
+data OpFix = OpFix
+  { opFix'fixity :: !Fixity
+  -- ^ fixity type
+  , opFix'prec   :: !Int
+  -- ^ fixity order
+  }
+
+-- | Infix operation can be left or right associative or associativity is not known.
+data Fixity = FixLeft | FixRight | FixNone
+  deriving Eq
+
+data Operator v = OpFunAp | Op v | ArrowOp
+  deriving (Eq, Ord)
+
+data FixityContext v = FcNone | FcLeft (Operator v) | FcRight (Operator v)
+
+{-
+initEnv :: FixityEnv
+initEnv = Map.fromList
+  [ (Op "->", OpFix FixRight 2) ]
+-}
+
+getFixityEnv :: HasPrefix v => Operator v -> Maybe OpFix
+getFixityEnv = \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
+  (Just opA, Just opB) -> toPo (opFix'prec opA) (opFix'prec opB)
+  _                    -> PoNC
+  where
+    toPo m n
+      | m < n     = PoLT
+      | m > n     = PoGT
+      | otherwise = PoEQ
+
+
+fixity :: HasPrefix v => Operator v -> Fixity
+fixity op = maybe FixNone opFix'fixity $ getFixityEnv op
+
+---------------------------------------
+
+instance (HasPrefix v, PrintCons v, Pretty v, Pretty prim) => Pretty (Term prim loc v) where
+  pretty (Term x) = foldFix prettyTermF x
+    where
+      prettyTermF = \case
+        Var _ v            -> pretty v
+        Prim _ p           -> pretty p
+        App _ a b          -> parens $ hsep [a, b]
+        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
+        Case _ e alts      -> vcat [ hsep ["case", e, "of"], indent 4 $ vcat $ fmap onAlt alts]
+        Bottom _           -> "_|_"
+        where
+          onLet vs body =
+            vcat [ hsep ["let", indent 4 $ vcat $ fmap (\Bind{..} -> hsep [pretty bind'lhs, "=", bind'rhs]) vs]
+                 , hsep ["in ", body]]
+
+          onAlt CaseAlt{..} = hsep
+            [ pretty caseAlt'tag, hsep $ fmap (pretty . snd . typed'value) caseAlt'args
+            , "->"
+            , caseAlt'rhs ]
+
diff --git a/src/Type/Check/HM/Subst.hs b/src/Type/Check/HM/Subst.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/Subst.hs
@@ -0,0 +1,49 @@
+-- | Capture-avoiding substitutions.
+module Type.Check.HM.Subst(
+    CanApply(..)
+  , Subst(..)
+  , delta
+  , applyToVar
+) where
+
+import Data.Fix
+import qualified Data.Map.Strict as M
+
+import Type.Check.HM.Type
+
+-- | Substitutions of type variables for monomorphic types.
+newtype Subst loc v = Subst { unSubst :: M.Map v (Type loc v) }
+  deriving (Eq, Ord, Monoid)
+
+instance Ord v => Semigroup (Subst loc v) where
+  (Subst ma) <> sb@(Subst mb) = Subst $ fmap (apply sb) ma <> M.difference mb ma
+
+-- | Singleton substitution.
+delta :: v -> Type loc v -> Subst loc v
+delta v = Subst . M.singleton v
+
+applyToVar :: Ord v => Subst loc v -> v -> Maybe (Type loc v)
+applyToVar (Subst m) v = M.lookup v m
+
+---------------------------------------------------------------
+
+-- | Class for application of substitutions to various types.
+class CanApply f where
+  apply :: Ord v => Subst loc v -> f loc v -> f loc v
+
+instance CanApply Type where
+  apply (Subst s) = foldFix go . unType
+    where
+      go = \case
+        VarT loc v -> case M.lookup v s of
+          Nothing -> varT loc v
+          Just t  -> t
+        ConT loc name args -> conT loc name args
+        ArrowT loc a b     -> arrowT loc a b
+        TupleT loc as      -> tupleT loc as
+        ListT loc a        -> listT loc a
+
+instance CanApply Signature where
+  apply (Subst s) (Signature (Fix expr)) = case expr of
+    MonoT t     -> monoT $ apply (Subst s) t
+    ForAllT loc x t -> forAllT loc x $ apply (Subst $ M.delete x s) (Signature t)
diff --git a/src/Type/Check/HM/Term.hs b/src/Type/Check/HM/Term.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/Term.hs
@@ -0,0 +1,232 @@
+-- | This module contains the abstract syntax tree of the term language.
+module Type.Check.HM.Term(
+    Term(..)
+  , TermF(..)
+  , CaseAlt(..)
+  , Bind(..)
+  , varE
+  , primE
+  , appE
+  , lamE
+  , letE
+  , letRecE
+  , assertTypeE
+  , caseE
+  , constrE
+  , bottomE
+  , freeVars
+) where
+
+import Control.Arrow
+
+import Data.Data
+import Data.Fix
+import Data.Set (Set)
+import Data.Eq.Deriving
+import Data.Ord.Deriving
+import Text.Show.Deriving
+
+import Type.Check.HM.Subst
+import Type.Check.HM.Type
+
+import qualified Data.Set as S
+
+-- | Term functor. The arguments are
+-- @loc@ for source code locations, @v@ for variables, @r@ for recurion.
+data TermF prim loc v r
+    = Var loc v                       -- ^ Variables.
+    | Prim loc prim                   -- ^ Primitives.
+    | App loc r r                     -- ^ Applications.
+    | Lam loc v r                     -- ^ Abstractions.
+    | Let loc (Bind loc v r) r        -- ^ Let bindings.
+    | 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
+    | Bottom loc                      -- ^ value of any type that means failed program.
+    deriving (Show, Eq, Functor, Foldable, Traversable, Data)
+
+-- | Case alternatives
+data CaseAlt loc v a = CaseAlt
+  { caseAlt'loc   :: loc
+  -- ^ source code location
+  , caseAlt'tag   :: v
+  -- ^ tag of the constructor
+  , caseAlt'args  :: [Typed loc v (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
+  }
+  deriving (Show, Eq, Functor, Foldable, Traversable, Data)
+
+-- | Local variable definition.
+--
+-- > let lhs = rhs in ...
+data Bind loc var r = Bind
+  { bind'loc :: loc             -- ^ Source code location
+  , bind'lhs :: var             -- ^ Variable name
+  , bind'rhs :: r               -- ^ Definition (right-hand side)
+  } deriving (Show, Eq, Functor, Foldable, Traversable, Data)
+
+$(deriveShow1 ''TermF)
+$(deriveEq1   ''TermF)
+$(deriveOrd1  ''TermF)
+$(deriveShow1 ''Bind)
+$(deriveEq1   ''Bind)
+$(deriveOrd1  ''Bind)
+$(deriveShow1 ''CaseAlt)
+$(deriveEq1   ''CaseAlt)
+$(deriveOrd1  ''CaseAlt)
+
+-- | The type of terms.
+newtype Term prim loc v = Term { unTerm :: Fix (TermF prim loc v) }
+  deriving (Show, Eq, Data)
+
+instance Functor (Term prim loc) where
+  fmap f (Term x) =  Term $ foldFix go x
+    where
+      go = \case
+        Var loc v    -> Fix $ Var loc (f v)
+        Prim loc p   -> Fix $ Prim loc p
+        App loc a b  -> Fix $ App loc a b
+        Lam loc v a  -> Fix $ Lam loc (f v) a
+        Let loc v a  -> Fix $ Let loc (v { bind'lhs = f $ bind'lhs v }) a
+        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)
+        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
+        }
+
+      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
+
+-- | `primE` @loc prim@ constructs a primitive with source code at @loc@.
+primE :: loc -> prim -> Term prim loc var
+primE loc = Term . Fix . Prim loc
+
+-- | 'appE' @loc a b@ constructs an application of @a@ to @b@ with source code at @loc@.
+appE :: loc -> Term prim loc v -> Term prim loc v -> Term prim loc v
+appE loc (Term l) (Term r) = Term $ Fix $ App loc l r
+
+-- | 'lamE' @loc x e@ constructs an abstraction of @x@ over @e@ with source code at @loc@.
+lamE :: loc -> v -> Term prim loc v -> Term prim loc v
+lamE loc x (Term e) = Term $ Fix $ Lam loc x e
+
+-- | 'letE' @loc binds e@ constructs a binding of @binds@ in @e@ with source code at @loc@.
+-- No recursive bindings.
+letE :: loc -> Bind loc v (Term prim loc v) -> Term prim loc v -> Term prim loc v
+letE loc bind (Term e) = Term $ Fix $ Let loc (fmap unTerm bind) e
+
+-- | 'letRecE' @loc binds e@ constructs a recursive binding of @binds@ in @e@ with source code at @loc@.
+letRecE :: loc -> [Bind loc v (Term prim loc v)] -> Term prim loc v -> Term prim loc v
+letRecE loc binds (Term e) = Term $ Fix $ LetRec loc (fmap (fmap unTerm) binds) e
+
+-- | 'assertTypeE' @loc term ty@ constructs assertion of the type @ty@ to @term@.
+assertTypeE :: loc -> Term prim loc v -> Type loc v -> Term prim loc v
+assertTypeE loc (Term a) ty = Term $ Fix $ AssertType loc a ty
+
+-- | 'caseE' @loc expr alts@ constructs case alternatives expression.
+caseE :: loc -> Term prim loc v -> [CaseAlt loc v (Term prim loc v)] -> Term prim loc v
+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
+
+-- | 'bottomE' @loc@ constructs bottom value.
+bottomE :: loc -> Term prim loc v
+bottomE loc = Term $ Fix $ Bottom loc
+
+--------------------------------------------------------------------------------
+
+instance HasLoc (Term prim loc v) where
+  type Loc (Term prim loc v) = loc
+
+  getLoc (Term (Fix x)) = case x of
+    Var loc _   -> loc
+    Prim loc _  -> loc
+    App loc _ _ -> loc
+    Lam loc _ _ -> loc
+    Let loc _ _ -> loc
+    LetRec loc _ _ -> loc
+    AssertType loc _ _ -> loc
+    Constr loc _ _ -> loc
+    Case loc _ _ -> loc
+    Bottom loc -> loc
+
+instance LocFunctor (Term prim) where
+  mapLoc f (Term x) = Term $ foldFix go x
+    where
+      go = \case
+        Var loc v    -> Fix $ Var (f loc) v
+        Prim loc p   -> Fix $ Prim (f loc) p
+        App loc a b  -> Fix $ App (f loc) a b
+        Lam loc v a  -> Fix $ Lam (f loc) v a
+        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
+        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
+        }
+
+      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 = foldFix go . unTerm
+  where
+    go = \case
+      Var    _ v          -> S.singleton v
+      Prim   _ _          -> mempty
+      App    _ a b        -> mappend a b
+      Lam    _ v a        -> S.delete v a
+      Let    _ bind body  -> let lhs = S.singleton $ bind'lhs bind
+                             in  mappend (bind'rhs bind)
+                                         (body `S.difference` lhs)
+      LetRec _ binds body -> let lhs = S.fromList $ fmap bind'lhs binds
+                             in  (mappend (freeBinds binds) body) `S.difference` lhs
+      AssertType _ a _    -> a
+      Case _ e alts       -> mappend e (foldMap freeVarAlts alts)
+      Constr _ _ _        -> mempty
+      Bottom _            -> mempty
+
+    freeBinds = foldMap bind'rhs
+
+    freeVarAlts CaseAlt{..} = caseAlt'rhs `S.difference` (S.fromList $ fmap (snd . typed'value) 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 }
+
+instance CanApply (Term prim) where
+  apply subst term = mapType (apply subst) term
+
diff --git a/src/Type/Check/HM/TyTerm.hs b/src/Type/Check/HM/TyTerm.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/TyTerm.hs
@@ -0,0 +1,147 @@
+-- | This module contains type annotations for terms of the language.
+module Type.Check.HM.TyTerm(
+    Ann(..)
+  , TyTerm(..)
+  , termType
+  , tyVarE
+  , tyPrimE
+  , tyAppE
+  , tyLamE
+  , tyLetE
+  , tyLetRecE
+  , tyAssertTypeE
+  , tyCaseE
+  , tyConstrE
+  , tyBottomE
+  , mapType
+) where
+
+import Control.Arrow
+
+import Data.Fix
+import Data.Containers.ListUtils (nubOrdOn)
+import Data.Foldable
+import Data.Eq.Deriving
+import Data.Ord.Deriving
+import Text.Show.Deriving
+
+import Type.Check.HM.Subst
+import Type.Check.HM.Type
+import Type.Check.HM.Term
+
+import qualified Data.DList as D
+
+-- | Type to annotate nodes of AST.
+-- We use it for type annotations.
+data Ann note f a = Ann
+  { ann'note  :: note
+  , ann'value :: f a
+  } deriving (Show, Eq, Functor, Foldable, Traversable)
+
+$(deriveShow1 ''Ann)
+$(deriveEq1   ''Ann)
+$(deriveOrd1  ''Ann)
+
+
+-- | Terms with type annotations for all subexpressions.
+newtype TyTerm prim loc v = TyTerm { unTyTerm :: Fix (Ann (Type loc v) (TermF prim loc v)) }
+  deriving (Show, Eq)
+
+termType :: TyTerm prim loc v -> Type loc v
+termType (TyTerm (Fix (Ann ty _))) = ty
+
+-- 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
+
+-- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.
+tyVarE :: Type loc var -> loc -> var -> TyTerm prim loc var
+tyVarE ty loc var =  tyTerm ty $ Var loc var
+
+-- | 'varE' @loc x@ constructs a variable whose name is @x@ with source code at @loc@.
+tyPrimE :: Type loc var -> loc -> prim -> TyTerm prim loc var
+tyPrimE ty loc prim =  tyTerm ty $ Prim loc prim
+
+-- | 'appE' @loc a b@ constructs an application of @a@ to @b@ with source code at @loc@.
+tyAppE :: Type loc v -> loc -> TyTerm prim loc v -> TyTerm prim loc v -> TyTerm prim loc v
+tyAppE ty loc (TyTerm l) (TyTerm r) = tyTerm ty $ App loc l r
+
+-- | 'lamE' @loc x e@ constructs an abstraction of @x@ over @e@ with source code at @loc@.
+tyLamE :: Type loc v -> loc -> v -> TyTerm prim loc v -> TyTerm prim loc v
+tyLamE ty loc x (TyTerm e) = tyTerm ty $ Lam loc x e
+
+-- | 'letE' @loc binds e@ constructs a binding of @binds@ in @e@ with source code at @loc@.
+-- No recursive bindings.
+tyLetE :: Type loc v -> loc -> Bind loc v (TyTerm prim loc v) -> TyTerm prim loc v -> TyTerm prim loc v
+tyLetE ty loc bind (TyTerm e) = tyTerm ty $ Let loc (fmap unTyTerm bind) e
+
+-- | 'letRecE' @loc binds e@ constructs a recursive binding of @binds@ in @e@ with source code at @loc@.
+tyLetRecE :: Type loc v -> loc -> [Bind loc v (TyTerm prim loc v)] -> TyTerm prim loc v -> TyTerm prim loc v
+tyLetRecE ty loc binds (TyTerm e) = tyTerm ty $ LetRec loc (fmap (fmap unTyTerm) binds) e
+
+-- | 'assertTypeE' @loc term ty@ constructs assertion of the type @ty@ to @term@.
+tyAssertTypeE :: loc -> TyTerm prim loc v -> Type loc v -> TyTerm prim loc v
+tyAssertTypeE loc (TyTerm a) ty = tyTerm ty $ AssertType loc a ty
+
+-- | 'caseE' @loc expr alts@ constructs case alternatives expression.
+tyCaseE :: Type loc v -> loc -> TyTerm prim loc v -> [CaseAlt loc v (TyTerm prim loc v)] -> TyTerm prim loc v
+tyCaseE ty loc (TyTerm e) alts = tyTerm ty $ Case loc e $ fmap (fmap unTyTerm) alts
+
+-- | '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
+
+-- | 'bottomE' @loc@ constructs bottom value.
+tyBottomE :: Type loc v -> loc -> TyTerm prim loc v
+tyBottomE ty loc = tyTerm ty $ Bottom loc
+
+instance LocFunctor (TyTerm prim) where
+  mapLoc f (TyTerm x) = TyTerm $ foldFix go x
+    where
+      go (Ann annTy term) = Fix $ Ann (mapLoc f annTy) $ case term of
+        Var loc v    -> Var (f loc) v
+        Prim loc p   -> Prim (f loc) p
+        App loc a b  -> App (f loc) a b
+        Lam loc v a  -> Lam (f loc) v a
+        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
+        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
+        }
+
+      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 }
+
+instance CanApply (TyTerm prim) where
+  apply subst term = mapType (apply subst) term
+
+instance HasTypeVars (TyTerm prim) where
+  tyVars (TyTerm x) = foldFix (\(Ann ty term) -> tyVars ty <> fold term) x
+
+  tyVarsInOrder (TyTerm x) =
+    nubOrdOn fst $ D.toList $ foldFix (\(Ann ty term) -> D.fromList (tyVarsInOrder ty) <> fold term) x
+
+
+
diff --git a/src/Type/Check/HM/Type.hs b/src/Type/Check/HM/Type.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/Type.hs
@@ -0,0 +1,370 @@
+-- | This module contains the abstract syntax of Hindley-Milner types.
+module Type.Check.HM.Type (
+    IsVar(..),
+    HasLoc(..),
+    DefLoc(..),
+    -- * Monomorphic types.
+    TypeF(..),
+    Type(..),
+    varT,
+    conT,
+    arrowT,
+    tupleT,
+    listT,
+    -- * Typed values
+    Typed(..),
+
+    -- * Polymorphic types.
+    SignatureF(..),
+    Signature(..),
+    forAllT,
+    monoT,
+    stripSignature,
+    splitSignature,
+    typeToSignature,
+    getTypeVars,
+
+    VarSet(..),
+    differenceVarSet,
+    varSetToList,
+    memberVarSet,
+
+    HasTypeVars(..),
+    LocFunctor(..),
+    setLoc,
+    TypeFunctor(..),
+
+    extractFunType,
+    extractArrow,
+
+    isMono,
+    isPoly
+) where
+
+--------------------------------------------------------------------------------
+
+import Control.DeepSeq (NFData(..))
+import Control.Monad
+
+import Data.Containers.ListUtils (nubOrdOn)
+import Data.Data
+import Data.Eq.Deriving
+import Data.Ord.Deriving
+import Data.Fix
+import Data.Foldable
+import Data.Function (on)
+import Data.Map.Strict (Map)
+import Data.Monoid
+import Data.String
+import Data.Tuple (swap)
+import Data.Text (Text)
+
+import GHC.Generics
+
+import qualified Data.List as L
+import qualified Data.Map.Strict as M
+
+import Text.Show.Deriving
+
+--------------------------------------------------------------------------------
+
+-- | Class to get source code location.
+class HasLoc f where
+  -- | Type for source code location
+  type Loc f :: *
+
+  -- | Get the source code location.
+  getLoc :: f -> Loc f
+
+-- | Type class for default location
+class DefLoc f where
+  defLoc :: f
+
+-- | Functions we need for variables to do type-inference.
+class (Show v, Ord v) => IsVar v where
+  -- | Canonical leters for pretty output
+  prettyLetters :: [v]
+
+instance IsVar String where
+  prettyLetters = stringPrettyLetters
+
+instance IsVar Text where
+  prettyLetters = stringPrettyLetters
+
+instance IsVar Int where
+  prettyLetters = [0..]
+
+stringPrettyLetters :: IsString a => [a]
+stringPrettyLetters = fmap fromString $ [1..] >>= flip replicateM ['a'..'z']
+
+instance DefLoc () where
+  defLoc = ()
+
+-- | Type functor. Arguments are
+--
+-- * @loc@ - source code locations
+--
+-- * @var@ - variable name
+--
+-- * @r@ - recursion
+--
+-- There are only two requried constructors: @VarT@ and @ConT@
+-- other constructors are used for convenience of pretty-printing the type.
+data TypeF loc var r
+    = VarT loc var      -- ^ Variables
+    | ConT loc var [r]  -- ^ type constant with list of arguments
+    | ArrowT loc r r    -- ^ Special case of ConT that is rendered as ->
+    | TupleT loc [r]    -- ^ Special case of ConT that is rendered as (,,,)
+    | ListT loc r       -- ^ Special case of ConT that is rendered as [a]
+    deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic, Data)
+
+$(deriveShow1 ''TypeF)
+$(deriveEq1   ''TypeF)
+$(deriveOrd1  ''TypeF)
+
+-- | Values that are tagged explicitly with their type.
+data Typed loc v a = Typed
+  { typed'type  :: Type loc v
+  , typed'value :: a
+  } deriving (Show, Eq, Ord, Functor, Foldable, Traversable, Data)
+
+-- | Monomorphic types.
+newtype Type loc var = Type { unType :: Fix (TypeF loc var) }
+  deriving (Show, Eq, Ord, Generic, Data)
+
+instance HasLoc (Type loc v) where
+  type Loc (Type loc v) = loc
+  getLoc (Type (Fix x)) = case x of
+    VarT   loc _   -> loc
+    ConT   loc _ _ -> loc
+    ArrowT loc _ _ -> loc
+    TupleT loc _   -> loc
+    ListT  loc _   -> loc
+
+instance (NFData loc, NFData var) => NFData (Type loc var) where
+  rnf (Type m) = foldFix go m where
+    go = \case
+      VarT   l v   -> rnf l `seq` rnf v
+      ConT   l v x -> rnf l `seq` rnf v `seq` rnf x
+      ArrowT l a b -> rnf l `seq` rnf a `seq` rnf b
+      TupleT l x   -> rnf l `seq` rnf x
+      ListT  l x   -> rnf l `seq` rnf x
+
+-- | 'varT' @loc x@ constructs a type variable named @x@ with source code at @loc@.
+varT :: loc -> var -> Type loc var
+varT loc var = Type $ Fix $ VarT loc var
+
+-- | 'conT' @loc x@ constructs a type constant named @x@ with source code at @loc@.
+conT :: loc -> var -> [Type loc var] -> Type loc var
+conT loc name args = Type $ Fix $ ConT loc name $ fmap unType $ args
+
+-- | 'arrowT' @loc t0 t1@ constructs an arrow type from @t0@ to @t1@ with source code at @loc@.
+arrowT :: loc -> Type loc v -> Type loc v -> Type loc v
+arrowT loc (Type t0) (Type t1) = Type $ Fix $ ArrowT loc t0 t1
+
+-- | 'tupleT' @loc ts@ constructs tuple of types @ts@ with source code at @loc@.
+tupleT :: loc -> [Type loc var] -> Type loc var
+tupleT loc ts = Type $ Fix $ TupleT loc $ fmap unType ts
+
+-- | 'listT' @loc t@ constructs list of @t@ with source code at @loc@.
+listT :: loc -> Type loc var -> Type loc var
+listT loc (Type t) = Type $ Fix $ ListT loc t
+
+--------------------------------------------------------------------------------
+
+-- | Functor for signature is a special type that we need for type inference algorithm.
+-- We specify which variables in the type are schematic (non-free).
+data SignatureF loc var r
+    = ForAllT loc var r     -- ^ specify schematic variable
+    | MonoT (Type loc var)  -- ^ contains the type
+    deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Data)
+
+$(deriveShow1 ''SignatureF)
+$(deriveEq1   ''SignatureF)
+$(deriveOrd1  ''SignatureF)
+
+-- | Signaure is a special type that we need for type inference algorithm.
+-- We specify which variables in the type are schematic (non-free).
+newtype Signature loc var = Signature { unSignature :: Fix (SignatureF loc var)
+  } deriving (Show, Eq, Ord, Data)
+
+instance Functor (Signature loc) where
+  fmap f (Signature x) = Signature $ foldFix go x
+    where
+      go = \case
+        ForAllT loc var a -> Fix $ ForAllT loc (f var) a
+        MonoT ty          -> Fix $ MonoT $ fmap f ty
+
+instance Functor (Type a) where
+  fmap f (Type x) = Type $ foldFix go x
+    where
+      go = \case
+        VarT loc name      -> Fix $ VarT loc $ f name
+        ConT loc name args -> Fix $ ConT loc (f name) args
+        ArrowT loc a b     -> Fix $ ArrowT loc a b
+        TupleT loc as      -> Fix $ TupleT loc as
+        ListT loc a        -> Fix $ ListT loc a
+
+instance HasLoc (Signature loc var) where
+  type Loc (Signature loc var) = loc
+  getLoc (Signature x) = foldFix go x
+    where
+      go = \case
+        MonoT ty        -> getLoc ty
+        ForAllT loc _ _ -> loc
+
+-- | Mapping over source code locations. It's like functor but for source code locations.
+class LocFunctor f where
+  mapLoc :: (locA -> locB) -> f locA var -> f locB var
+
+-- | Sets the source code location to given value for all expressions in the functor.
+setLoc :: LocFunctor f => loc -> f locA v -> f loc v
+setLoc loc = mapLoc (const loc)
+
+instance LocFunctor Type where
+  mapLoc f (Type x) = Type $ foldFix go x
+    where
+      go = \case
+        VarT loc name      -> Fix $ VarT (f loc) name
+        ConT loc name args -> Fix $ ConT (f loc) name args
+        ArrowT loc a b     -> Fix $ ArrowT (f loc) a b
+        TupleT loc as      -> Fix $ TupleT (f loc) as
+        ListT loc a        -> Fix $ ListT (f loc) a
+
+instance LocFunctor Signature where
+  mapLoc f (Signature x) = Signature $ foldFix go x
+    where
+      go = \case
+        ForAllT loc var a -> Fix $ ForAllT (f loc) var a
+        MonoT ty          -> Fix $ MonoT $ mapLoc f ty
+
+-- | Mapps over all types that are contained in the value
+class TypeFunctor f where
+  mapType :: (Type loc var -> Type loc var) -> f loc var -> f loc var
+
+instance TypeFunctor Type where
+  mapType f = f
+
+-- | 'forAllT' @x t@ universally quantifies @x@ in @t@.
+forAllT :: loc -> v -> Signature loc v -> Signature loc v
+forAllT loc x (Signature t) = Signature $ Fix $ ForAllT loc x t
+
+-- | 'monoT' @t@ lifts a monomorophic type @t@ to a polymorphic one.
+monoT :: Type loc src -> Signature loc src
+monoT = Signature . Fix . MonoT
+
+-- | Converts simple type to signature with all free variables set to schematic.
+typeToSignature :: (Eq loc, Ord v) => Type loc v -> Signature loc v
+typeToSignature ty = foldr (\(v, src) a -> forAllT src v a) (monoT ty) vs
+  where
+    vs = tyVarsInOrder ty
+
+-- | Reads all type-variables.
+getTypeVars :: (Ord var, HasTypeVars f) => f src var -> [(src, var)]
+getTypeVars = varSetToList . tyVars
+
+--------------------------------------------------------------------------------
+
+-- | The class of types which have free type variables.
+class HasTypeVars f where
+    -- | 'tyVars' @t@ calculates the set of free type variables in @t@.
+    tyVars :: Ord var => f src var -> VarSet src var
+
+    -- | 'tyVarsInOrder' @t@ is like 'tyVars' @t@, except that the type
+    -- variables are returned in the order in which they are encountered.
+    tyVarsInOrder :: (Eq src, Ord var) => f src var -> [(var, src)]
+
+instance HasTypeVars Type where
+    tyVars = foldFix go . unType
+      where
+        go = \case
+          VarT loc v    -> VarSet $ M.singleton v loc
+          ConT _ _ args -> mconcat args
+          ArrowT _ a b  -> mappend a b
+          TupleT _ as   -> mconcat as
+          ListT _ a     -> a
+
+    tyVarsInOrder = nubOrdOn fst . foldFix go . unType
+      where
+        go = \case
+          VarT loc var -> [(var, loc)]
+          ConT _ _ as  -> mconcat as
+          ArrowT _ a b -> mappend a b
+          TupleT _ as  -> mconcat as
+          ListT _ a    -> a
+
+
+instance HasTypeVars Signature where
+    tyVars = foldFix go . unSignature
+      where
+        go = \case
+          MonoT t       -> tyVars t
+          ForAllT _ x t -> VarSet $ M.delete x $ unVarSet t
+
+    tyVarsInOrder = nubOrdOn fst . foldFix go . unSignature
+      where
+        go = \case
+          MonoT t         -> tyVarsInOrder t
+          ForAllT src x t -> L.deleteBy ((==) `on` fst) (x, src) t
+
+--------------------------------------------------------------------------------
+
+-- | Set with information on source code locations.
+-- We use it to keep the source code locations for variables.
+newtype VarSet src var = VarSet { unVarSet :: Map var src }
+  deriving (Semigroup, Monoid)
+
+-- | 'difference' for @VarSet@'s
+differenceVarSet :: Ord var => VarSet src var -> VarSet src var -> VarSet src var
+differenceVarSet (VarSet a) (VarSet b) = VarSet $ a `M.difference` b
+
+-- | Converts varset to list.
+varSetToList :: VarSet src var -> [(src, var)]
+varSetToList (VarSet m) = fmap swap $ M.toList m
+
+-- | Checks membership of the item in the varset.
+memberVarSet :: Ord var => var -> VarSet src var -> Bool
+memberVarSet k (VarSet m) = M.member k m
+
+--------------------------------------------------------------------------------
+
+-- | Removes all information on variables in the type.
+-- it gets the thing that we store in constructor @MonoT@.
+stripSignature :: Signature src var -> Type src var
+stripSignature = foldFix go . unSignature
+  where
+    go = \case
+      ForAllT _ _ r -> r
+      MonoT ty -> ty
+
+-- | Separates type variables from type definition.
+splitSignature :: Signature loc var -> ([var], Type loc var)
+splitSignature (Signature x) = flip foldFix x $ \case
+  ForAllT _ v (vs, t) -> (v:vs, t)
+  MonoT t             -> ([], t)
+
+-- | If underlying type is a function with several arguments it extracts its list of arguments and result type.
+extractFunType :: Type loc var -> ([Type loc var], Type loc var)
+extractFunType ty = case extractArrow ty of
+  Just (lhs, rhs) ->
+    let (args, rhs') = extractFunType rhs
+    in  (lhs : args, rhs')
+  Nothing         -> ([], ty)
+
+-- | If underlying type is an arrow it extracts its single argument and result type.
+extractArrow :: Type loc var -> Maybe (Type loc var, Type loc var)
+extractArrow (Type (Fix x)) = case x of
+  ArrowT _ a b -> Just (Type a, Type b)
+  _            -> Nothing
+
+------------------------------------
+
+-- | Checks that type is monomorphic.
+isMono :: Type loc var -> Bool
+isMono (Type t) = getAll $ flip foldFix t $ \case
+  VarT _ _  -> All False
+  other     -> fold other
+
+-- | Checks that type is polymorphic.
+isPoly :: Type loc var -> Bool
+isPoly = not . isMono
diff --git a/src/Type/Check/HM/TypeError.hs b/src/Type/Check/HM/TypeError.hs
new file mode 100644
--- /dev/null
+++ b/src/Type/Check/HM/TypeError.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE DeriveAnyClass     #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE DerivingStrategies #-}
+-- | This module contains types for structured type errors.
+module Type.Check.HM.TypeError where
+
+import Control.DeepSeq (NFData)
+import Data.Data
+import Data.Function (on)
+import GHC.Generics    (Generic)
+import Type.Check.HM.Type
+import Type.Check.HM.Subst
+
+import qualified Data.List as L
+
+-- | Type errors.
+data TypeError loc var
+  = OccursErr  loc (Type loc var)                 -- ^ error of mismatch of polymorphic constructors, infinite type. Like [a] = a
+  | 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.
+  | EmptyCaseExpr loc                             -- ^ no case alternatives in the case expression
+  | FreshNameFound                                -- ^ internal error with fresh name substitution
+  deriving stock    (Show, Eq, Functor, Generic, Data)
+  deriving anyclass (NFData)
+
+instance LocFunctor TypeError where
+  mapLoc f = \case
+    OccursErr loc ty     -> OccursErr (f loc) (mapLoc f ty)
+    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
+    EmptyCaseExpr loc    -> EmptyCaseExpr (f loc)
+    FreshNameFound       -> FreshNameFound
+
+instance HasTypeVars TypeError where
+  tyVars = \case
+    OccursErr _ ty     -> tyVars ty
+    UnifyErr _ a b     -> tyVars a <> tyVars b
+    SubtypeErr _ a b   -> tyVars a <> tyVars b
+    NotInScopeErr _ _  -> mempty
+    EmptyCaseExpr _    -> mempty
+    FreshNameFound     -> mempty
+
+  tyVarsInOrder err = L.nubBy ((==) `on` fst) $ case err of
+    OccursErr _ ty     -> tyVarsInOrder ty
+    UnifyErr _ a b     -> tyVarsInOrder a <> tyVarsInOrder b
+    SubtypeErr _ a b   -> tyVarsInOrder a <> tyVarsInOrder b
+    NotInScopeErr _ _  -> mempty
+    EmptyCaseExpr _    -> mempty
+    FreshNameFound     -> mempty
+
+instance CanApply TypeError where
+  apply f = \case
+    OccursErr loc ty   -> OccursErr loc $ apply f ty
+    UnifyErr loc a b   -> UnifyErr loc (apply f a) (apply f b)
+    SubtypeErr loc a b -> SubtypeErr loc (apply f a) (apply f b)
+    other              -> other
+
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,12 @@
+-- |
+module Main where
+
+import Test.Tasty
+import qualified TM.SKI
+import qualified TM.NumLang
+
+main :: IO ()
+main = defaultMain $ testGroup "HM"
+  [ TM.SKI.tests
+  , TM.NumLang.tests
+  ]
diff --git a/test/TM/NumLang.hs b/test/TM/NumLang.hs
new file mode 100644
--- /dev/null
+++ b/test/TM/NumLang.hs
@@ -0,0 +1,327 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeFamilies #-}
+-- | Tests for language with lambda calculus with numbers and booleans.
+module TM.NumLang where
+
+import Data.String
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Data.Either
+import qualified Type.Check.HM as T
+import qualified Data.Map.Strict as M
+
+infixr ~>
+
+data CodeLoc = CodeLoc
+  { codeLoc'line :: Int
+  , codeLoc'col  :: Int
+  }
+  deriving (Show, Eq)
+
+-- | Primitives of our language.
+-- We support integers and booleans
+data Prim
+  = PInt CodeLoc Int     -- ^ integers
+  | PBool CodeLoc Bool   -- ^ booleans
+  deriving (Show, Eq)
+
+-- | Type for variables
+type Var = String
+
+-- types for the language
+
+type Ty = T.Type CodeLoc Var
+
+(~>) :: Ty -> Ty -> Ty
+(~>) a b = T.arrowT defLoc a b
+
+boolT, intT :: Ty
+boolT = T.conT defLoc "Bool" []
+intT  = T.conT defLoc "Int" []
+
+-- | Language tag (we need it for Lang instance)
+data NumLang
+
+-- | Instanciate to provide the right components of the language
+instance T.Lang NumLang where
+  type Src  NumLang = CodeLoc   -- ^ source code locations
+  type Var  NumLang = Var       -- ^ variables
+  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" []
+
+-- | Expressions for our language
+newtype Expr = Expr { unExpr :: T.Term Prim CodeLoc Var }
+
+-- | In real case we should get this info from parser.
+-- For example we assign same code location to all expressions.
+defLoc :: CodeLoc
+defLoc = CodeLoc 0 0
+
+-- primitives
+
+-- | constructor for integer literals
+int :: Int -> Expr
+int = Expr . T.primE defLoc . PInt defLoc
+
+-- | constructor for boolean literals
+bool :: Bool -> Expr
+bool = Expr . T.primE defLoc . PBool defLoc
+
+-- numeric expressions
+
+instance Num Expr where
+  (+) = app2 "+"
+  (*) = app2 "*"
+  (-) = app2 "-"
+  negate = app "negate"
+  fromInteger = int . fromInteger
+  abs = error "undefined"
+  signum = error "undefined"
+
+-- boolean expressions
+
+-- | Boolean &&
+andB :: Expr -> Expr -> Expr
+andB = app2 "&&"
+
+-- | Boolean ||
+orB :: Expr -> Expr -> Expr
+orB = app2 "||"
+
+-- | Boolean negation
+notB :: Expr -> Expr
+notB = app "not"
+
+-- comparisons
+
+eq, neq, gt, lt, gte, lte :: Expr -> Expr -> Expr
+eq  = app2 "=="
+neq = app2 "/="
+lt  = app2 "<"
+gt  = app2 ">"
+lte = app2 "<="
+gte = app2 ">="
+
+-- if then else
+
+-- | If-expressions
+if_ :: Expr -> Expr -> Expr -> Expr
+if_ = app3 "if"
+
+----------------------------------------------------------
+-- lambda calc
+
+-- Variables (construct them from string literals)
+instance IsString Expr where
+  fromString = Expr . T.varE defLoc
+
+toBind :: Var -> Expr -> T.Bind CodeLoc Var (T.Term Prim CodeLoc Var)
+toBind v (Expr e) = T.Bind defLoc v e
+
+-- | Application
+app :: Expr -> Expr -> Expr
+app (Expr a) (Expr b) = Expr $ T.appE defLoc a b
+
+-- | Binary application
+app2 :: Expr -> Expr -> Expr -> Expr
+app2 a b c = app (app a b) c
+
+-- | Ternary application
+app3 :: Expr -> Expr -> Expr -> Expr -> Expr
+app3 a b c d = app (app2 a b c) d
+
+-- | Let-expressions
+let_ :: Var -> Expr -> Expr -> Expr
+let_ v e (Expr body) = Expr $ T.letE defLoc (toBind v e) body
+
+-- | Let-expressions with recursion
+letRec :: [(Var, Expr)] -> Expr -> Expr
+letRec es (Expr body) = Expr $ T.letRecE defLoc (fmap (uncurry toBind) es) body
+
+-- | Lambda-expressions
+lam :: Var -> Expr -> Expr
+lam v (Expr fun) = Expr $ T.lamE defLoc v fun
+
+----------------------------------------------------------
+-- custom constructors
+
+-- types for custom types
+pointT, circleT, rectT :: Ty
+pointT  = T.conT defLoc "Point" []
+circleT = T.conT defLoc "Circle" []
+rectT = T.conT defLoc "Rect" []
+
+-- | Point constructor
+point :: Expr -> Expr -> Expr
+point = app2 (Expr $ T.constrE defLoc (intT ~> intT ~> pointT) "Point")
+
+circle :: Expr -> Expr -> Expr
+circle = app2 (Expr $ T.constrE defLoc (pointT ~> intT ~> circleT) "Circle")
+
+rect :: Expr -> Expr -> Expr
+rect = app2 (Expr $ T.constrE defLoc (pointT ~> pointT ~> rectT) "Rect")
+
+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]
+
+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]
+
+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]
+
+tyVar :: Ty -> Var -> T.Typed CodeLoc Var (CodeLoc, Var)
+tyVar ty v = T.Typed ty (defLoc, v)
+
+----------------------------------------------------------
+-- Type inference context
+--
+-- We define in context type signatures for all known functions
+-- or functions that were already derived on previous steps of compilation.
+
+-- | 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)]
+  ]
+  where
+    booleans =
+      [ "&&"  `is` (boolT ~> boolT ~> boolT)
+      , "||"  `is` (boolT ~> boolT ~> boolT)
+      , "not" `is` (boolT ~> boolT)
+      ]
+
+    nums =
+      [ "+"  `is` (intT ~> intT ~> intT)
+      , "*"  `is` (intT ~> intT ~> intT)
+      , "-"  `is` (intT ~> intT ~> intT)
+      , "negate" `is` (intT ~> intT)
+      ]
+
+    comparisons = fmap ( `is` (intT ~> intT ~> boolT)) ["==", "/=", "<", ">", "<=", ">="]
+
+    is a b = (a, T.monoT b)
+
+    -- forall a . ...
+    forA = T.forAllT defLoc "a"
+
+    -- a type variable "a"
+    aT = T.varT defLoc "a"
+
+
+----------------------------------------------------------
+-- examples
+
+intExpr1 :: Expr
+intExpr1 = negate $ ((20::Expr) + 30) * 100
+
+boolExpr1 :: Expr
+boolExpr1 = andB (andB (notB ((intExpr1 `lte` 1000) `orB` (2 `gt` 0))) (bool True)) (5 `neq` (2 + 2))
+
+failExpr1 :: Expr
+failExpr1 = lam "x" $ 2 + "x" `eq` (bool True)
+
+failExpr2 :: Expr
+failExpr2 = 2 + bool True
+
+failExpr3 :: Expr
+failExpr3 = 2 + "missingVar"
+
+-- | Simple integer function
+intFun1 :: Expr
+intFun1 = lam "x" ((1 + "x") * 10)
+
+-- | Square distance of the point to zero
+squareDist :: Expr
+squareDist = lam "x" $ lam "y" $ "x" * "x" + "y" * "y"
+
+-- | Check that point is inside circle
+insideCircle :: Expr
+insideCircle = lam "d" $ lam "x" $ lam "y" $
+  let_ "squareDist" squareDist
+    (app2 "squareDist" "x" "y") `lt` ("d" * "d")
+
+-- | Factorial
+fact :: Expr
+fact = lam "x" $ letRec
+  [ ("fac", lam "n" $ if_ (eq "n" 0) 1 ("n" * app "fac" ("n" - 1)))
+  ]
+  (app "fac" "x")
+
+-- | Greatest common divisor
+gcd' :: Expr
+gcd' = lam "x" $ lam "y" $ defAbs $ defMod $
+  letRec
+    [ ("gcd", lam "a" $ lam "b" $ if_ ("b" `eq` 0) (app "abs" "a") (app2 "gcd" "b" (app2 "mod" "a" "b")))
+    ]
+  (app2 "gcd" "x" "y")
+  where
+    defAbs = let_ "abs" (lam "a" $ if_ ("a" `gte` 0) "a" (negate "a"))
+    defMod = let_ "mod" (lam "a" $ lam "b" $ letRec [("go", lam "m" $ lam "n" $ if_ ("m" `lt` "n") "m" (app2 "go" ("m" - "n") "n"))] (app2 "go" "a" "b"))
+
+-- geometry examples
+
+addPointLam :: Expr
+addPointLam = lam "a" $ lam "b" $
+  casePoint "a" ("ax", "ay") $
+    casePoint "b" ("bx", "by") $ point ("ax" + "bx") ("ay" + "by")
+
+negatePointLam :: Expr
+negatePointLam = lam "p" $ casePoint "p" ("px", "py") $
+  point (negate "px") (negate "py")
+
+addPoint :: Expr -> Expr -> Expr
+addPoint = app2 addPointLam
+
+negatePoint :: Expr -> Expr
+negatePoint = app negatePointLam
+
+rectSquare :: Expr
+rectSquare = lam "r" $ defAbs $ caseRect "r" ("p1", "p2") $
+  casePoint "p1" ("p1x", "p1y") $ casePoint "p2" ("p2x", "p2y") $
+    app "abs" $ ("p1x" - "p2x") * ("p1y" - "p2y")
+  where
+    defAbs = let_ "abs" (lam "a" $ if_ ("a" `gte` 0) "a" (negate "a"))
+
+insideCircle2 :: Expr
+insideCircle2 = lam "c" $ lam "p" $ caseCircle "c" ("center", "rad") $
+  casePoint (addPoint "center" (negatePoint "p")) ("ax", "ay") $
+    app3 insideCircle "rad" "ax" "ay"
+
+----------------------------------------------------------
+-- tests
+
+tests :: TestTree
+tests = testGroup "lambda calculus with numbers and booleans"
+  [ check "int expr"        intT                            intExpr1
+  , check "bool expr"       boolT                           boolExpr1
+  , check "int fun"         (intT ~> intT)                  intFun1
+  , check "square dist fun" (intT ~> intT ~> intT)          squareDist
+  , check "inside circle"   (intT ~> intT ~> intT ~> boolT) insideCircle
+  , check "factorial"       (intT ~> intT)                  fact
+  , check "gcd"             (intT ~> intT ~> intT)          gcd'
+  , fails "Fail mismatch 1" failExpr1
+  , fails "Fail mismatch 2" failExpr2
+  , fails "Fail missing var" failExpr3
+  , check "add points"      (pointT ~> pointT ~> pointT)    addPointLam
+  , check "negate point"    (pointT ~> pointT)              negatePointLam
+  , check "rect square"     (rectT ~> intT)                 rectSquare
+  , check "inside circle 2" (circleT ~> pointT ~> boolT)    insideCircle2
+  ]
+  where
+    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)
+
diff --git a/test/TM/SKI.hs b/test/TM/SKI.hs
new file mode 100644
--- /dev/null
+++ b/test/TM/SKI.hs
@@ -0,0 +1,58 @@
+{-# LANGUAGE EmptyDataDeriving #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeFamilies      #-}
+-- | Tests with type-inference for SKI-combinators
+module TM.SKI (tests) where
+
+import Data.Text (Text)
+import Test.Tasty
+import Test.Tasty.HUnit
+
+import Type.Check.HM
+
+tests :: TestTree
+tests = testGroup "infer"
+  [ testCase "SKI:I"
+  $ Right (var "a" --> var "a") @=? (inferType mempty termI)
+  , testCase "SKI:K"
+  $ Right (var "a" --> (var "b" --> var "a")) @=? (inferType mempty termK)
+  , testCase "let-chain-case"
+  $ Right (var "a" --> var "a") @=? (inferType mempty termLetChain)
+  , testCase "let-rec-chain-case"
+  $ Right (var "a" --> var "a") @=? (inferType mempty termLetRecChain)
+  ]
+  where
+    a --> b = arrowT () a b
+    var     = varT ()
+
+----------------------------------------------------------------
+data NoPrim
+  deriving (Show)
+
+data TestLang
+
+instance Lang TestLang where
+  type Src  TestLang = ()
+  type Var  TestLang = Text
+  type Prim TestLang = NoPrim
+  getPrimType _ = error "No primops"
+
+-- I combinator
+termI,termK :: Term NoPrim () Text
+termI = lamE () "x" $ varE () "x"
+termK = lamE () "x" $ lamE () "y" $ varE () "x"
+
+termLetChain :: Term NoPrim () Text
+termLetChain = lamE () "x" $ letE ()
+  (Bind () "a" $ varE () "x")
+    (letE ()
+      (Bind () "b" $ varE () "a")
+      (varE () "b"))
+
+termLetRecChain :: Term NoPrim () Text
+termLetRecChain = lamE () "x" $ letRecE ()
+  [ Bind () "a" $ varE () "x"
+  , Bind () "b" $ varE () "a"
+  ]
+  (varE () "b")
+