diff --git a/src/GF/Command/Commands.hs b/src/GF/Command/Commands.hs
index 07d710e0a..65f64ef11 100644
--- a/src/GF/Command/Commands.hs
+++ b/src/GF/Command/Commands.hs
@@ -32,6 +32,7 @@ import GF.Command.TreeOperations ---- temporary place for typecheck and compute
 import GF.Data.Operations
 import GF.Text.Coding
 
+import Data.List
 import Data.Maybe
 import qualified Data.Map as Map
 import System.Cmd
@@ -283,7 +284,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
           _ | isOpt "changes" opts -> changesMsg
           _ | isOpt "coding" opts -> codingMsg
           _ | isOpt "license" opts -> licenseMsg
-          [t] -> let co = getCommandOp (showExpr t) in 
+          [t] -> let co = getCommandOp (showExpr [] t) in 
                  case lookCommand co (allCommands cod env) of   ---- new map ??!!
                    Just info -> commandHelp True (co,info)
                    _ -> "command not found"
@@ -615,23 +616,29 @@ allCommands cod env@(pgf, mos) = Map.fromList [
        ],
      exec = \opts arg -> do
        case arg of
-         [EVar id] -> case Map.lookup id (funs (abstract pgf)) of
+         [EFun id] -> case Map.lookup id (funs (abstract pgf)) of
                         Just (ty,_,eqs) -> return $ fromString $
-                                              render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 ty $$
+                                              render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 [] ty $$
                                                       if null eqs
                                                         then empty
-                                                        else text "def" <+> vcat [text (prCId id) <+> hsep (map (ppPatt 9) patts) <+> char '=' <+> ppExpr 0 res | Equ patts res <- eqs])
+                                                        else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts
+                                                                                  in text (prCId id) <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs])
                         Nothing         -> case Map.lookup id (cats (abstract pgf)) of
                                              Just hyps -> do return $ fromString $
-                                                                render (text "cat" <+> text (prCId id) <+> hsep (map ppHypo hyps) $$
+                                                                render (text "cat" <+> text (prCId id) <+> hsep (snd (mapAccumL ppHypo [] hyps)) $$
                                                                         if null (functionsToCat pgf id)
                                                                           then empty
                                                                           else space $$
-                                                                               text "fun" <+> vcat [text (prCId fid) <+> colon <+> ppType 0 ty 
+                                                                               text "fun" <+> vcat [text (prCId fid) <+> colon <+> ppType 0 [] ty 
                                                                                                        | (fid,ty) <- functionsToCat pgf id])
                                              Nothing   -> do putStrLn "unknown identifier"
                                                              return void
-         _           -> do putStrLn "a single identifier is expected from the command"
+         [e]         -> case inferExpr pgf e of
+                          Left tcErr   -> error $ render (ppTcError tcErr)
+                          Right (e,ty) -> do putStrLn ("Expression: "++showExpr [] e)
+                                             putStrLn ("Type:       "++showType [] ty)
+                                             return void
+         _           -> do putStrLn "a single identifier or expression is expected from the command"
                            return void
      })
   ]
@@ -689,7 +696,9 @@ allCommands cod env@(pgf, mos) = Map.fromList [
    optType opts = 
      let str = valStrOpts "cat" (prCId $ lookStartCat pgf) opts
      in case readType str of
-          Just ty -> ty
+          Just ty -> case checkType pgf ty of
+                       Left tcErr -> error $ render (ppTcError tcErr)
+                       Right ty   -> ty
           Nothing -> error ("Can't parse '"++str++"' as type")
    optComm opts = valStrOpts "command" "" opts
    optViewFormat opts = valStrOpts "format" "png" opts
@@ -710,10 +719,10 @@ allCommands cod env@(pgf, mos) = Map.fromList [
 
    returnFromExprs es = return $ case es of
      [] -> ([], "no trees found")
-     _  -> (es,unlines (map showExpr es))
+     _  -> (es,unlines (map (showExpr []) es))
 
    prGrammar opts
-     | isOpt "cats"     opts = return $ fromString $ unwords $ map showType $ categories pgf
+     | isOpt "cats"     opts = return $ fromString $ unwords $ map (showType []) $ categories pgf
      | isOpt "fullform" opts = return $ fromString $ concatMap (prFullFormLexicon . morpho) $ optLangs opts
      | isOpt "missing"  opts = return $ fromString $ unlines $ [unwords (prCId la:":": map prCId cs) | 
                                                                   la <- optLangs opts, let cs = missingLins pgf la]
@@ -739,7 +748,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
 
    showAsString t = case t of
      ELit (LStr s) -> s
-     _ -> "\n" ++ showExpr t  --- newline needed in other cases than the first
+     _ -> "\n" ++ showExpr [] t  --- newline needed in other cases than the first
 
 stringOpOptions = sort $ [
        ("bind","bind tokens separated by Prelude.BIND, i.e. &+"),
diff --git a/src/GF/Command/Interpreter.hs b/src/GF/Command/Interpreter.hs
index 23b928ed6..2ace4cde6 100644
--- a/src/GF/Command/Interpreter.hs
+++ b/src/GF/Command/Interpreter.hs
@@ -12,14 +12,13 @@ import GF.Command.Abstract
 import GF.Command.Parse
 import PGF
 import PGF.Data
-import PGF.Macros
 import PGF.Morphology
 import GF.System.Signal
 import GF.Infra.UseIO
 import GF.Infra.Option
 
-import GF.Data.ErrM ----
-
+import Text.PrettyPrint
+import Control.Monad.Error
 import qualified Data.Map as Map
 
 data CommandEnv = CommandEnv {
@@ -43,12 +42,6 @@ interpretCommandLine enc env line =
   case readCommandLine line of
     Just []    -> return ()
     Just pipes -> mapM_ (interpretPipe enc env) pipes
-{-
-    Just pipes -> do res <- runInterruptibly (mapM_ (interpretPipe enc env) pipes)
-                     case res of
-                       Left ex -> putStrLnFlush $ enc (show ex)
-                       Right x -> return x
--}
     Nothing    -> putStrLnFlush "command not parsed"
 
 interpretPipe enc env cs = do
@@ -60,12 +53,15 @@ interpretPipe enc env cs = do
    intercs (trees,_) (c:cs) = do
      treess2 <- interc trees c
      intercs treess2 cs
-   interc es comm@(Command co _ arg) = case co of
+   interc es comm@(Command co opts arg) = case co of
      '%':f -> case Map.lookup f (commandmacros env) of
-       Just css -> do
-         mapM_ (interpretPipe enc env) (appLine (getCommandArg env arg es) css) 
-         return ([],[]) ---- return ?
-       _ -> do
+       Just css ->
+         case getCommandTrees env arg es of
+           Right es -> do mapM_ (interpretPipe enc env) (appLine es css) 
+                          return ([],[])
+           Left msg -> do putStrLn ('\n':msg)
+                          return ([],[])
+       Nothing  -> do
          putStrLn $ "command macro " ++ co ++ " not interpreted"
          return ([],[])
      _ -> interpret enc env es comm
@@ -82,43 +78,53 @@ appCommand xs c@(Command i os arg) = case arg of
     EApp e1 e2 -> EApp (app e1) (app e2)
     ELit l     -> ELit l
     EMeta i    -> xs !! i
-    EVar x     -> EVar x
+    EFun x     -> EFun x
 
 -- return the trees to be sent in pipe, and the output possibly printed
 interpret :: (String -> String) -> CommandEnv -> [Expr] -> Command -> IO CommandOutput
-interpret enc env trees0 comm = case lookCommand co comms of
-    Just info -> do
-      checkOpts info
-      tss@(_,s) <- exec info opts trees
-      optTrace $ enc s
-      return tss
-    _ -> do
-      putStrLn $ "command " ++ co ++ " not interpreted"
-      return ([],[])
- where
-   optTrace = if isOpt "tr" opts then putStrLn else const (return ()) 
-   (co,opts,trees) = getCommand env comm trees0
-   comms = commands env
-   checkOpts info = 
-     case
-       [o | OOpt  o   <- opts, notElem o ("tr" : map fst (options info))] ++
-       [o | OFlag o _ <- opts, notElem o (map fst (flags info))]
-      of
-        []  -> return () 
-        [o] -> putStrLn $ "option not interpreted: " ++ o
-        os  -> putStrLn $ "options not interpreted: " ++ unwords os
+interpret enc env trees comm = 
+  case getCommand env trees comm of
+    Left  msg               -> do putStrLn ('\n':msg)
+                                  return ([],[])
+    Right (info,opts,trees) -> do tss@(_,s) <- exec info opts trees
+                                  if isOpt "tr" opts
+                                    then putStrLn (enc s)
+                                    else return ()
+                                  return tss
 
 -- analyse command parse tree to a uniform datastructure, normalizing comm name
 --- the env is needed for macro lookup
-getCommand :: CommandEnv -> Command -> [Expr] -> (String,[Option],[Expr])
-getCommand env co@(Command c opts arg) ts = 
-  (getCommandOp c,opts,getCommandArg env arg ts) 
+getCommand :: CommandEnv -> [Expr] -> Command -> Either String (CommandInfo,[Option],[Expr])
+getCommand env es co@(Command c opts arg) = do
+  info <- getCommandInfo  env c
+  checkOpts info opts
+  es   <- getCommandTrees env arg es
+  return (info,opts,es)
 
-getCommandArg :: CommandEnv -> Argument -> [Expr] -> [Expr]
-getCommandArg env a ts = case a of
-  AMacro m -> case Map.lookup m (expmacros env) of
-    Just t -> [t]
-    _ -> [] 
-  AExpr t -> [t] -- ignore piped
-  ANoArg  -> ts  -- use piped
+getCommandInfo :: CommandEnv -> String -> Either String CommandInfo
+getCommandInfo env cmd = 
+  case lookCommand (getCommandOp cmd) (commands env) of
+    Just info -> return info
+    Nothing   -> fail $ "command " ++ cmd ++ " not interpreted"
 
+checkOpts :: CommandInfo -> [Option] -> Either String ()
+checkOpts info opts = 
+  case
+    [o | OOpt  o   <- opts, notElem o ("tr" : map fst (options info))] ++
+    [o | OFlag o _ <- opts, notElem o (map fst (flags info))]
+  of
+    []  -> return () 
+    [o] -> fail $ "option not interpreted: " ++ o
+    os  -> fail $ "options not interpreted: " ++ unwords os
+
+getCommandTrees :: CommandEnv -> Argument -> [Expr] -> Either String [Expr]
+getCommandTrees env a es =
+  case a of
+    AMacro m -> case Map.lookup m (expmacros env) of
+                  Just e -> return [e]
+                  _      -> return [] 
+    AExpr e -> case inferExpr (multigrammar env) e of
+                 Left tcErr   -> fail $ render (ppTcError tcErr)
+                 Right (e,ty) -> return [e] -- ignore piped
+    ANoArg  -> return es  -- use piped
+  
diff --git a/src/GF/Command/TreeOperations.hs b/src/GF/Command/TreeOperations.hs
index 262ce35b5..45f927afc 100644
--- a/src/GF/Command/TreeOperations.hs
+++ b/src/GF/Command/TreeOperations.hs
@@ -20,9 +20,7 @@ allTreeOps pgf = [
    ("paraphrase",("paraphrase by using semantic definitions (def)",
       map tree2expr . nub . concatMap (paraphrase pgf . expr2tree))),
    ("smallest",("sort trees from smallest to largest, in number of nodes",
-      smallest)),
-   ("typecheck",("type check and solve metavariables; reject if incorrect",
-      concatMap (typecheck pgf)))
+      smallest))
   ]
 
 smallest :: [Expr] -> [Expr]
@@ -31,35 +29,3 @@ smallest = sortBy (\t u -> compare (size t) (size u)) where
     EAbs _ e -> size e + 1
     EApp e1 e2 -> size e1 + size e2 + 1
     _ -> 1
-
-{-
-toTree :: G.Term -> Tree
-toTree t = case M.termForm t of
-  Ok (xx,f,aa) -> Abs xx (Fun f (map toTree aa))
-
-fromTree :: Tree -> G.Term
-fromTree t = case t of
-  Abs xx b -> M.mkAbs xx (fromTree b)
-  Var x    -> M.vr x
-  Fun f ts -> M.mkApp f (map fromTree ts)
--}
-
-{-
-data Tree = 
-   Abs [CId] Tree                   -- ^ lambda abstraction. The list of variables is non-empty
- | Var CId                          -- ^ variable
- | Fun CId [Tree]                   -- ^ function application
- | Lit Literal                      -- ^ literal
- | Meta Int                         -- ^ meta variable
-
-data Literal = 
-   LStr String                      -- ^ string constant
- | LInt Integer                     -- ^ integer constant
- | LFlt Double                      -- ^ floating point constant
-
-mkType :: A.Type -> C.Type
-mkType t = case GM.typeForm t of
-  Ok (hyps,(_,cat),args) -> C.DTyp (mkContext hyps) (i2i cat) (map mkExp args)
-
-mkExp :: A.Term -> C.Expr
--}
diff --git a/src/GF/Compile/GFCCtoProlog.hs b/src/GF/Compile/GFCCtoProlog.hs
index dca6465fa..3e30dccc3 100644
--- a/src/GF/Compile/GFCCtoProlog.hs
+++ b/src/GF/Compile/GFCCtoProlog.hs
@@ -68,7 +68,7 @@ plAbstract (name, Abstr aflags funs cats _catfuns) =
 plCat :: (CId, [Hypo]) -> String
 plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) 
     where ((_,subst), hypos') = alphaConvert emptyEnv hypos
-          args = reverse [EVar x | (_,x) <- subst]
+          args = reverse [EFun x | (_,x) <- subst]
           typ = DTyp hypos' cat args
 
 plFun :: (CId, (Type, Int, [Equation])) -> String
@@ -119,7 +119,7 @@ instance PLPrint Hypo where
     plp (HypV var typ) = plOper ":" (plp var) (plp typ)
 
 instance PLPrint Expr where
-    plp (EVar x)    = plp x
+    plp (EFun x)    = plp x
     plp (EAbs x e)  = plOper "^" (plp x) (plp e)
     plp (EApp e e') = plOper " * " (plp e) (plp e')
     plp (ELit lit)  = plp lit
@@ -279,7 +279,7 @@ instance AlphaConvert Expr where
     alphaConvert env (EApp e1 e2) = (env'', EApp e1' e2')
         where (env',  e1') = alphaConvert env  e1
               (env'', e2') = alphaConvert env' e2
-    alphaConvert env expr@(EVar i) = (env, maybe expr EVar (lookup i (snd env)))
+    alphaConvert env expr@(EFun i) = (env, maybe expr EFun (lookup i (snd env)))
     alphaConvert env expr = (env, expr)
 
 -- pattern variables are not alpha converted
diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs
index d7e46df3e..115f3e319 100644
--- a/src/GF/Compile/GrammarToGFCC.hs
+++ b/src/GF/Compile/GrammarToGFCC.hs
@@ -70,17 +70,17 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
   gflags = Map.empty
   aflags = Map.fromList [(mkCId f,x) | (f,x) <- optionsPGF (M.flags abm)]
 
-  mkDef (Just eqs) = [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs]
+  mkDef (Just eqs) = [C.Equ ps' (mkExp scope' e) | (ps,e) <- eqs, let (scope',ps') = mapAccumL mkPatt [] ps]
   mkDef Nothing    = []
   
   mkArrity (Just a) = a
   mkArrity Nothing  = 0
 
   -- concretes
-  lfuns = [(f', (mkType ty, mkArrity ma, mkDef pty)) | 
+  lfuns = [(f', (mkType [] ty, mkArrity ma, mkDef pty)) | 
              (f,AbsFun (Just ty) ma pty) <- tree2list (M.jments abm), let f' = i2i f]
   funs = Map.fromAscList lfuns
-  lcats = [(i2i c, mkContext cont) |
+  lcats = [(i2i c, snd (mkContext [] cont)) |
                 (c,AbsCat (Just cont) _) <- tree2list (M.jments abm)]
   cats = Map.fromAscList lcats
   catfuns = Map.fromList 
@@ -118,36 +118,45 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
 i2i :: Ident -> CId
 i2i = CId . ident2bs
 
-mkType :: A.Type -> C.Type
-mkType t = case GM.typeForm t of
-  Ok (hyps,(_,cat),args) -> C.DTyp (mkContext hyps) (i2i cat) (map mkExp args)
+mkType :: [Ident] -> A.Type -> C.Type
+mkType scope t =
+  case GM.typeForm t of
+    Ok (hyps,(_,cat),args) -> let (scope',hyps') = mkContext scope hyps
+                              in C.DTyp hyps' (i2i cat) (map (mkExp scope') args)
 
-mkExp :: A.Term -> C.Expr
-mkExp t = case GM.termForm t of
-    Ok (xs,c,args) -> mkAbs xs (mkApp c (map mkExp args))
+mkExp :: [Ident] -> A.Term -> C.Expr
+mkExp scope t = case GM.termForm t of
+    Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
   where
     mkAbs xs t = foldr (C.EAbs . i2i) t xs
-    mkApp c args = case c of
-      Q _ c    -> foldl C.EApp (C.EVar (i2i c)) args
-      QC _ c   -> foldl C.EApp (C.EVar (i2i c)) args
-      Vr x     -> C.EVar (i2i x)
+    mkApp scope c args = case c of
+      Q _ c    -> foldl C.EApp (C.EFun (i2i c)) args
+      QC _ c   -> foldl C.EApp (C.EFun (i2i c)) args
+      Vr x     -> case lookup x (zip scope [0..]) of
+                    Just i  -> foldl C.EApp (C.EVar  i) args
+                    Nothing -> foldl C.EApp (C.EMeta 0) args
       EInt i   -> C.ELit (C.LInt i)
       EFloat f -> C.ELit (C.LFlt f)
       K s      -> C.ELit (C.LStr s)
       Meta (MetaSymb i) -> C.EMeta i
       _        -> C.EMeta 0
 
-mkPatt p = case p of
-  A.PP _ c ps -> C.PApp (i2i c) (map mkPatt ps)
-  A.PV x      -> C.PVar (i2i x)
-  A.PW        -> C.PWild
-  A.PInt i    -> C.PLit (C.LInt i)
-  A.PFloat f  -> C.PLit (C.LFlt f)
-  A.PString s -> C.PLit (C.LStr s)
+mkPatt scope p = 
+  case p of
+    A.PP _ c ps -> let (scope',ps') = mapAccumL mkPatt scope ps
+                   in (scope',C.PApp (i2i c) ps')
+    A.PV x      -> (x:scope,C.PVar (i2i x))
+    A.PW        -> (  scope,C.PWild)
+    A.PInt i    -> (  scope,C.PLit (C.LInt i))
+    A.PFloat f  -> (  scope,C.PLit (C.LFlt f))
+    A.PString s -> (  scope,C.PLit (C.LStr s))
 
 
-mkContext :: A.Context -> [C.Hypo]
-mkContext hyps = [(if x == identW then C.Hyp else C.HypV (i2i x)) (mkType ty) | (x,ty) <- hyps]
+mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
+mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
+                                                   in if x == identW
+                                                        then (  scope,C.Hyp          ty')
+                                                        else (x:scope,C.HypV (i2i x) ty')) scope hyps 
 
 mkTerm :: Term -> C.Term
 mkTerm tr = case tr of
diff --git a/src/PGF.hs b/src/PGF.hs
index 8ac936e70..45da170d9 100644
--- a/src/PGF.hs
+++ b/src/PGF.hs
@@ -9,7 +9,7 @@
 -- load and interpret grammars compiled in Portable Grammar Format (PGF).
 -- The PGF format is produced as a final output from the GF compiler.
 -- The API is meant to be used for embedding GF grammars in Haskell 
--- programs.
+-- programs
 -------------------------------------------------
 
 module PGF(
@@ -51,7 +51,11 @@ module PGF(
            parse, canParse, parseAllLang, parseAll,
            
            -- ** Evaluation
-           tree2expr, expr2tree, PGF.compute, paraphrase, typecheck,
+           tree2expr, expr2tree, PGF.compute, paraphrase,
+           
+           -- ** Type Checking
+           checkType, checkExpr, inferExpr,
+           ppTcError, TcError(..),
            
            -- ** Word Completion (Incremental Parsing)
            complete,
@@ -80,6 +84,7 @@ import GF.Data.Utilities (replace)
 
 import Data.Char
 import qualified Data.Map as Map
+import qualified Data.IntMap as IntMap
 import Data.Maybe
 import Data.Binary
 import System.Random (newStdGen)
@@ -307,4 +312,4 @@ complete pgf from typ input =
 
 -- | Converts an expression to normal form
 compute :: PGF -> Expr -> Expr
-compute pgf = PGF.Data.normalForm (funs (abstract pgf))
+compute pgf = PGF.Data.normalForm (funs (abstract pgf)) 0 []
diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs
index bd896817f..87d61d1bc 100644
--- a/src/PGF/Binary.hs
+++ b/src/PGF/Binary.hs
@@ -104,20 +104,24 @@ instance Binary Term where
 instance Binary Expr where
   put (EAbs x exp)    = putWord8 0 >> put (x,exp)
   put (EApp e1 e2)    = putWord8 1 >> put (e1,e2)
-  put (EVar   x)      = putWord8 2 >> put x
-  put (ELit (LStr s)) = putWord8 3 >> put s
-  put (ELit (LFlt d)) = putWord8 4 >> put d
-  put (ELit (LInt i)) = putWord8 5 >> put i
-  put (EMeta i)       = putWord8 6 >> put i
+  put (ELit (LStr s)) = putWord8 2 >> put s
+  put (ELit (LFlt d)) = putWord8 3 >> put d
+  put (ELit (LInt i)) = putWord8 4 >> put i
+  put (EMeta i)       = putWord8 5 >> put i
+  put (EFun  f)       = putWord8 6 >> put f
+  put (EVar  i)       = putWord8 7 >> put i
+  put (ETyped e ty)   = putWord8 8 >> put (e,ty)
   get = do tag <- getWord8
            case tag of
              0 -> liftM2 EAbs get get
              1 -> liftM2 EApp get get
-             2 -> liftM  EVar get
-             3 -> liftM  (ELit . LStr) get
-             4 -> liftM  (ELit . LFlt) get
-             5 -> liftM  (ELit . LInt) get
-             6 -> liftM  EMeta get
+             2 -> liftM  (ELit . LStr) get
+             3 -> liftM  (ELit . LFlt) get
+             4 -> liftM  (ELit . LInt) get
+             5 -> liftM  EMeta get
+             6 -> liftM  EFun get
+             7 -> liftM  EVar get
+             8 -> liftM2 ETyped get get
              _ -> decodingError
 
 instance Binary Patt where
diff --git a/src/PGF/Expr.hs b/src/PGF/Expr.hs
index c22fa8a08..62a97698a 100644
--- a/src/PGF/Expr.hs
+++ b/src/PGF/Expr.hs
@@ -7,12 +7,12 @@ module PGF.Expr(Tree(..), Literal(..),
                 tree2expr, expr2tree, normalForm,
 
                 -- needed in the typechecker
-                Value(..), Env, eval, apply, eqValue,
+                Value(..), Env, Funs, eval, apply,
 
                 MetaId,
 
                 -- helpers
-                pStr,pFactor,
+                pStr,pFactor,freshName,ppMeta
                ) where
 
 import PGF.CId
@@ -20,16 +20,17 @@ import PGF.Type
 
 import Data.Char
 import Data.Maybe
+import Data.List as List
+import Data.Map as Map hiding (showTree)
 import Control.Monad
 import qualified Text.PrettyPrint as PP
 import qualified Text.ParserCombinators.ReadP as RP
-import qualified Data.Map as Map
 
 data Literal = 
    LStr String                      -- ^ string constant
  | LInt Integer                     -- ^ integer constant
  | LFlt Double                      -- ^ floating point constant
- deriving (Eq,Ord)
+ deriving (Eq,Ord,Show)
 
 type MetaId = Int
 
@@ -52,9 +53,10 @@ data Expr =
  | EApp Expr Expr                   -- ^ application
  | ELit Literal                     -- ^ literal
  | EMeta  {-# UNPACK #-} !MetaId    -- ^ meta variable
- | EVar   CId                       -- ^ variable or function reference
- | EPi CId Expr Expr                -- ^ dependent function type
-  deriving (Eq,Ord)
+ | EFun   CId                       -- ^ function or data constructor
+ | EVar   {-# UNPACK #-} !Int       -- ^ variable with de Bruijn index
+ | ETyped Expr Type
+  deriving (Eq,Ord,Show)
 
 -- | The pattern is used to define equations in the abstract syntax of the grammar.
 data Patt =
@@ -94,12 +96,12 @@ readExpr s = case [x | (x,cs) <- RP.readP_to_S pExpr s, all isSpace cs] of
                [x] -> Just x
                _   -> Nothing
 
--- | renders expression as 'String'
-showExpr :: Expr -> String
-showExpr = PP.render . ppExpr 0
-
-instance Show Expr where
-    showsPrec i x = showString (PP.render (ppExpr i x))
+-- | renders expression as 'String'. The list
+-- of identifiers is the list of all free variables
+-- in the expression in order reverse to the order
+-- of binding.
+showExpr :: [CId] -> Expr -> String
+showExpr vars = PP.render . ppExpr 0 vars
 
 instance Read Expr where
     readsPrec _ = RP.readP_to_S pExpr
@@ -124,24 +126,31 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
                   return (Fun f ts)
 
 pExpr :: RP.ReadP Expr
-pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
+pExpr = pExpr0 >>= optTyped
   where
+    pExpr0  = RP.skipSpaces >> (pAbs RP.<++ pTerm)
+
     pTerm   =       fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces)
 
     pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))
-              e  <- pExpr
+              e  <- pExpr0
               return (foldr EAbs e xs)
 
-pFactor =       fmap EVar  pCId
+    optTyped e = do RP.skipSpaces
+                    RP.char ':'
+                    RP.skipSpaces
+                    ty <- pType
+                    return (ETyped e ty)
+                 RP.<++
+                 return e 
+                 
+pFactor =       fmap EFun  pCId
         RP.<++  fmap ELit  pLit
         RP.<++  fmap EMeta pMeta
         RP.<++  RP.between (RP.char '(') (RP.char ')') pExpr
 
 pMeta = do RP.char '?'
-           cs <- RP.look
-           case cs of
-             (c:_) | isDigit c -> fmap read (RP.munch1 isDigit)
-             _                 -> return 0
+           return 0
 
 pLit :: RP.ReadP Literal
 pLit = pNum RP.<++ liftM LStr pStr
@@ -161,35 +170,37 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
 -----------------------------------------------------
 
 ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
-                                        PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>
+                                        PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) xs)) PP.<+>
                                         PP.text "->" PP.<+>
                                         ppTree 0 t)
 ppTree d (Fun f []) = PP.text (prCId f)
-ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (map (ppTree 1) ts))
+ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (List.map (ppTree 1) ts))
 ppTree d (Lit l)    = ppLit l
 ppTree d (Meta n)   = ppMeta n
 ppTree d (Var id)   = PP.text (prCId id)
 
 
-ppExpr :: Int -> Expr -> PP.Doc
-ppExpr d (EAbs x e)   = let (xs,e1) = getVars (EAbs x e)
-                        in ppParens (d > 0) (PP.char '\\' PP.<>
-                                             PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>
-                                             PP.text "->" PP.<+>
-                                             ppExpr 0 e1)
-                        where
-                          getVars (EAbs x e) = let (xs,e1) = getVars e in (x:xs,e1)
-                          getVars e          = ([],e)
-ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2))
-ppExpr d (ELit l)     = ppLit l
-ppExpr d (EMeta n)    = ppMeta n
-ppExpr d (EVar f)     = PP.text (prCId f)
-ppExpr d (EPi x e1 e2)= PP.parens (PP.text (prCId x) PP.<+> PP.colon PP.<+> ppExpr 0 e1) PP.<+> PP.text "->" PP.<+> ppExpr 0 e2
+ppExpr :: Int -> [CId] -> Expr -> PP.Doc
+ppExpr d scope (EAbs x e)   = let (xs,e1) = getVars [x] e
+                              in ppParens (d > 1) (PP.char '\\' PP.<>
+                                                   PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) (reverse xs))) PP.<+>
+                                                   PP.text "->" PP.<+>
+                                                   ppExpr 1 (xs++scope) e1)
+                              where
+                                getVars xs (EAbs x e) = getVars (freshName x xs:xs) e
+                                getVars xs e          = (xs,e)
+ppExpr d scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 scope e1) PP.<+> (ppExpr 4 scope e2))
+ppExpr d scope (ELit l)     = ppLit l
+ppExpr d scope (EMeta n)    = ppMeta n
+ppExpr d scope (EFun f)     = PP.text (prCId f)
+ppExpr d scope (EVar i)     = PP.text (prCId (scope !! i))
+ppExpr d scope (ETyped e ty)= ppParens (d > 0) (ppExpr 0 scope e PP.<+> PP.colon PP.<+> ppType 0 scope ty)
 
-ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps))
-ppPatt d (PLit l)    = ppLit l
-ppPatt d (PVar f)    = PP.text (prCId f)
-ppPatt d PWild       = PP.char '_'
+ppPatt d scope (PApp f ps) = let (scope',ds) = mapAccumL (ppPatt 2) scope ps
+                             in (scope',ppParens (not (List.null ps) && d > 1) (PP.text (prCId f) PP.<+> PP.hsep ds))
+ppPatt d scope (PLit l)    = (scope,ppLit l)
+ppPatt d scope (PVar f)    = (scope,PP.text (prCId f))
+ppPatt d scope PWild       = (scope,PP.char '_')
 
 ppLit (LStr s) = PP.text (show s)
 ppLit (LInt n) = PP.integer n
@@ -203,6 +214,12 @@ ppMeta n
 ppParens True  = PP.parens
 ppParens False = id
 
+freshName :: CId -> [CId] -> CId
+freshName x xs = loop 1 x
+  where
+    loop i y
+      | elem y xs = loop (i+1) (mkCId (show x++"'"++show i))
+      | otherwise = y
 
 -----------------------------------------------------
 -- Conversion Expr <-> Tree
@@ -211,33 +228,38 @@ ppParens False = id
 -- | Converts a tree to expression. The conversion
 -- is always total, every tree is a valid expression.
 tree2expr :: Tree -> Expr
-tree2expr (Fun x ts) = foldl EApp (EVar x) (map tree2expr ts) 
-tree2expr (Lit l)    = ELit l
-tree2expr (Meta n)   = EMeta n
-tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs
-tree2expr (Var x)    = EVar x
+tree2expr = tree2expr []
+  where
+    tree2expr ys (Fun x ts) = foldl EApp (EFun x) (List.map (tree2expr ys) ts) 
+    tree2expr ys (Lit l)    = ELit l
+    tree2expr ys (Meta n)   = EMeta n
+    tree2expr ys (Abs xs t) = foldr EAbs (tree2expr (reverse xs++ys) t) xs
+    tree2expr ys (Var x)    = case List.lookup x (zip ys [0..]) of
+                                Just i  -> EVar i
+                                Nothing -> error "unknown variable"
 
 -- | Converts an expression to tree. The conversion is only partial.
 -- Variables and meta variables of function type and beta redexes are not allowed.
 expr2tree :: Expr -> Tree
 expr2tree e = abs [] [] e
   where
-    abs ys xs (EAbs x e) = abs ys (x:xs) e
-    abs ys xs e          = case xs of
-                             [] -> app ys [] e
-                             xs -> Abs (reverse xs) (app (xs++ys) [] e)
+    abs ys xs (EAbs x e)      = abs ys (x:xs) e
+    abs ys xs (ETyped e _)    = abs ys xs e
+    abs ys xs e               = case xs of
+                                  [] -> app ys [] e
+                                  xs -> Abs (reverse xs) (app (xs++ys) [] e)
 
-    app xs as (EApp e1 e2)   = app xs ((abs xs [] e2) : as) e1
+    app xs as (EApp e1 e2)    = app xs ((abs xs [] e2) : as) e1
     app xs as (ELit l)
-               | null as     = Lit l
-               | otherwise   = error "literal of function type encountered"
+               | List.null as = Lit l
+               | otherwise    = error "literal of function type encountered"
     app xs as (EMeta n)
-               | null as     = Meta n
-               | otherwise   = error "meta variables of function type are not allowed in trees"
-    app xs as (EAbs x e)     = error "beta redexes are not allowed in trees"
-    app xs as (EVar x)
-               | x `elem` xs = Var x
-               | otherwise   = Fun x as
+               | List.null as = Meta n
+               | otherwise    = error "meta variables of function type are not allowed in trees"
+    app xs as (EAbs x e)      = error "beta redexes are not allowed in trees"
+    app xs as (EVar i)        = Var (xs !! i)
+    app xs as (EFun f)        = Fun f as
+    app xs as (ETyped e _)    = app xs as e
 
 
 -----------------------------------------------------
@@ -245,109 +267,84 @@ expr2tree e = abs [] [] e
 -----------------------------------------------------
 
 -- | Compute an expression to normal form
-normalForm :: Funs -> Expr -> Expr
-normalForm funs e = value2expr 0 (eval funs Map.empty e)
+normalForm :: Funs -> Int -> Env -> Expr -> Expr
+normalForm funs k env e = value2expr k (eval funs env e)
   where
-    value2expr i (VApp f vs)               = foldl EApp (EVar f)       (map (value2expr i) vs)
-    value2expr i (VGen j vs)               = foldl EApp (EVar (var j)) (map (value2expr i) vs)
-    value2expr i (VMeta j vs)              = foldl EApp (EMeta j)      (map (value2expr i) vs)
-    value2expr i (VSusp j vs k)            = value2expr i (k (VGen j vs))
+    value2expr i (VApp f vs)               = foldl EApp (EFun f)       (List.map (value2expr i) vs)
+    value2expr i (VGen j vs)               = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs)
+    value2expr i (VMeta j env vs)          = foldl EApp (EMeta j)      (List.map (value2expr i) vs)
+    value2expr i (VSusp j env vs k)        = value2expr i (k (VGen j vs))
     value2expr i (VLit l)                  = ELit l
-    value2expr i (VClosure env (EAbs x e)) = EAbs (var i) (value2expr (i+1) (eval funs (Map.insert x (VGen i []) env) e))
-
-    var i = mkCId ('v':show i)
-
-    ret [] t = t
-    ret xs t = Abs (reverse xs) t
+    value2expr i (VClosure env (EAbs x e)) = EAbs x (value2expr (i+1) (eval funs ((VGen i []):env) e))
 
 data Value
   = VApp CId [Value]
   | VLit Literal
-  | VMeta {-# UNPACK #-} !MetaId [Value]
-  | VGen  {-# UNPACK #-} !MetaId [Value]
-  | VSusp {-# UNPACK #-} !MetaId [Value] (Value -> Value)
+  | VMeta {-# UNPACK #-} !MetaId Env [Value]
+  | VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value)
+  | VGen  {-# UNPACK #-} !Int [Value]
   | VClosure Env Expr
 
 type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun
-type Env  = Map.Map CId Value
+type Env  = [Value]
 
 eval :: Funs -> Env -> Expr -> Value
-eval funs env (EVar x)     = case Map.lookup x env of
-                               Just v  -> v
-                               Nothing -> case Map.lookup x funs of
-                                            Just (_,a,eqs) -> if a == 0
-                                                                then case eqs of
-                                                                       Equ [] e : _ -> eval funs Map.empty e
-                                                                       _            -> VApp x []
-                                                                else VApp x []
-                                            Nothing        -> error ("unknown variable "++prCId x)
+eval funs env (EVar i)     = env !! i
+eval funs env (EFun f)     = case Map.lookup f funs of
+                              Just (_,a,eqs) -> if a == 0
+                                                  then case eqs of
+                                                         Equ [] e : _ -> eval funs [] e
+                                                         _            -> VApp f []
+                                                  else VApp f []
+                              Nothing        -> error ("unknown function "++prCId f)
 eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
 eval funs env (EAbs x e)   = VClosure env (EAbs x e)
-eval funs env (EMeta k)    = VMeta k []
+eval funs env (EMeta i)    = VMeta i env []
 eval funs env (ELit l)     = VLit l
-eval funs env (EPi x e1 e2)= VClosure env (EPi x e1 e2)
+eval funs env (ETyped e _) = eval funs env e
 
 apply :: Funs -> Env -> Expr -> [Value] -> Value
 apply funs env e            []     = eval funs env e
-apply funs env (EVar x)     vs     = case Map.lookup x env of
-                                       Just v  -> applyValue funs env v vs
-                                       Nothing -> case Map.lookup x funs of
-                                                    Just (_,a,eqs) -> if a <= length vs
-                                                                        then let (as,vs') = splitAt a vs
-                                                                             in match funs x eqs as vs'
-                                                                        else VApp x vs
-                                                    Nothing        -> error ("unknown variable "++prCId x)
+apply funs env (EVar i)     vs     = applyValue funs (env !! i) vs
+apply funs env (EFun f)     vs     = case Map.lookup f funs of
+                                       Just (_,a,eqs) -> if a <= length vs
+                                                           then let (as,vs') = splitAt a vs
+                                                                in match funs f eqs as vs'
+                                                           else VApp f vs
+                                       Nothing      -> error ("unknown function "++prCId f)
 apply funs env (EApp e1 e2) vs     = apply funs env e1 (eval funs env e2 : vs)
-apply funs env (EAbs x e)   (v:vs) = apply funs (Map.insert x v env) e vs
-apply funs env (EMeta k)    vs     = VMeta k vs
+apply funs env (EAbs x e)   (v:vs) = apply funs (v:env) e vs
+apply funs env (EMeta i)    vs     = VMeta i env vs
 apply funs env (ELit l)     vs     = error "literal of function type"
+apply funs env (ETyped e _) vs     = apply funs env e vs
 
-applyValue funs env (VApp f  vs0)             vs     = apply funs env (EVar f) (vs0++vs)
-applyValue funs env (VLit _)                  vs     = error "literal of function type"
-applyValue funs env (VMeta i vs0)             vs     = VMeta i (vs0++vs)
-applyValue funs env (VGen  i vs0)             vs     = VGen  i (vs0++vs)
-applyValue funs env (VSusp i vs0 k)           vs     = VSusp i vs0 (\v -> applyValue funs env (k v) vs)
-applyValue funs _   (VClosure env (EAbs x e)) (v:vs) = apply funs (Map.insert x v env) e vs
+applyValue funs v                         []     = v
+applyValue funs (VApp f  vs0)             vs     = apply funs [] (EFun f) (vs0++vs)
+applyValue funs (VLit _)                  vs     = error "literal of function type"
+applyValue funs (VMeta i env vs0)         vs     = VMeta i env (vs0++vs)
+applyValue funs (VGen  i vs0)             vs     = VGen  i (vs0++vs)
+applyValue funs (VSusp i env vs0 k)       vs     = VSusp i env vs0 (\v -> applyValue funs (k v) vs)
+applyValue funs (VClosure env (EAbs x e)) (v:vs) = apply funs (v:env) e vs
 
 -----------------------------------------------------
 -- Pattern matching
 -----------------------------------------------------
 
 match :: Funs -> CId -> [Equation] -> [Value] -> [Value] -> Value
-match funs f eqs as0 vs0 =
+match sig f eqs as0 vs0 =
   case eqs of
     []               -> VApp f (as0++vs0)
-    (Equ ps res):eqs -> tryMatches eqs ps as0 res Map.empty
+    (Equ ps res):eqs -> tryMatches eqs ps as0 res []
   where
-    tryMatches eqs []     []     res env = apply funs env res vs0
+    tryMatches eqs []     []     res env = apply sig env res vs0
     tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env
       where
-        tryMatch (PVar x     ) (v           ) env            = tryMatches eqs  ps        as  res (Map.insert x v env)
-        tryMatch (PWild      ) (_           ) env            = tryMatches eqs  ps        as  res env
-        tryMatch (p          ) (VMeta i vs  ) env            = VSusp i vs (\v -> tryMatch p v env)
-        tryMatch (p          ) (VGen  i vs  ) env            = VApp f (as0++vs0)
-        tryMatch (p          ) (VSusp i vs k) env            = VSusp i vs (\v -> tryMatch p (k v) env)
-        tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
-        tryMatch (PLit l1    ) (VLit l2     ) env | l1 == l2 = tryMatches eqs  ps        as  res env
-        tryMatch _             _              env            = match funs f eqs as0 vs0
-
-
------------------------------------------------------
--- Equality checking
------------------------------------------------------
-
-eqValue :: Funs -> Int -> Value -> Value -> [(Value,Value)]
-eqValue funs k v1 v2 =
-  case (whnf v1,whnf v2) of
-    (VApp f1 vs1, VApp f2 vs2) | f1 == f2  -> concat (zipWith (eqValue funs k) vs1 vs2)
-    (VLit l1,     VLit l2    ) | l1 == l2  -> []
-    (VMeta i vs1, VMeta j vs2) | i  == j   -> concat (zipWith (eqValue funs k) vs1 vs2)
-    (VGen  i vs1, VGen  j vs2) | i  == j   -> concat (zipWith (eqValue funs k) vs1 vs2)
-    (VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
-      let v = VGen k []
-      in eqValue funs (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)
-    _                                      -> [(v1,v2)]
-  where
-    whnf (VClosure env e) = eval funs env e   -- should be removed when the typechecker is improved
-    whnf v                = v
+        tryMatch (PVar x     ) (v                ) env            = tryMatches eqs  ps        as  res (v:env)
+        tryMatch (PWild      ) (_                ) env            = tryMatches eqs  ps        as  res env
+        tryMatch (p          ) (VMeta i envi vs  ) env            = VSusp i envi vs (\v -> tryMatch p v env)
+        tryMatch (p          ) (VGen  i vs       ) env            = VApp f (as0++vs0)
+        tryMatch (p          ) (VSusp i envi vs k) env            = VSusp i envi vs (\v -> tryMatch p (k v) env)
+        tryMatch (PApp f1 ps1) (VApp f2 vs2      ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
+        tryMatch (PLit l1    ) (VLit l2          ) env | l1 == l2 = tryMatches eqs  ps        as  res env
+        tryMatch _             _                   env            = match sig f eqs as0 vs0
 
diff --git a/src/PGF/Expr.hs-boot b/src/PGF/Expr.hs-boot
index 0369be173..21f5f7ef1 100644
--- a/src/PGF/Expr.hs-boot
+++ b/src/PGF/Expr.hs-boot
@@ -1,13 +1,17 @@
 module PGF.Expr where
 
+import PGF.CId
 import qualified Text.PrettyPrint as PP
 import qualified Text.ParserCombinators.ReadP as RP
 
 data Expr
 
-instance Eq  Expr
-instance Ord Expr
+instance Eq   Expr
+instance Ord  Expr
+instance Show Expr
 
 pFactor :: RP.ReadP Expr
 
-ppExpr :: Int -> Expr -> PP.Doc
+ppExpr :: Int -> [CId] -> Expr -> PP.Doc
+
+freshName :: CId -> [CId] -> CId
\ No newline at end of file
diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs
index a899e84c2..5ddad6ef0 100644
--- a/src/PGF/Type.hs
+++ b/src/PGF/Type.hs
@@ -5,22 +5,22 @@ module PGF.Type ( Type(..), Hypo(..),
 import PGF.CId
 import {-# SOURCE #-} PGF.Expr
 import Data.Char
+import Data.List
 import qualified Text.PrettyPrint as PP
 import qualified Text.ParserCombinators.ReadP as RP
 import Control.Monad
-import Debug.Trace
 
 -- | To read a type from a 'String', use 'read' or 'readType'.
 data Type =
    DTyp [Hypo] CId [Expr]
-  deriving (Eq,Ord)
+  deriving (Eq,Ord,Show)
 
 -- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis
 data Hypo =
     Hyp      Type      -- ^ hypothesis without bound variable like in A -> B
   | HypV CId Type      -- ^ hypothesis with bound variable like in (x : A) -> B x
   | HypI CId Type      -- ^ hypothesis with bound implicit variable like in {x : A} -> B x
-  deriving (Eq,Ord)
+  deriving (Eq,Ord,Show)
 
 -- | Reads a 'Type' from a 'String'.
 readType :: String -> Maybe Type
@@ -28,15 +28,12 @@ readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of
                [x] -> Just x
                _   -> Nothing
 
-instance Show Type where
-    showsPrec i x = showString (PP.render (ppType i x))
-
-instance Read Type where
-    readsPrec _ = RP.readP_to_S pType
-
--- | renders type as 'String'
-showType :: Type -> String
-showType = PP.render . ppType 0
+-- | renders type as 'String'. The list
+-- of identifiers is the list of all free variables
+-- in the expression in order reverse to the order
+-- of binding.
+showType :: [CId] -> Type -> String
+showType vars = PP.render . ppType 0 vars
 
 pType :: RP.ReadP Type
 pType = do
@@ -72,17 +69,19 @@ pType = do
       args <- RP.sepBy pFactor RP.skipSpaces
       return (cat, args)
 
-ppType :: Int -> Type -> PP.Doc
-ppType d (DTyp ctxt cat args)
-  | null ctxt = ppRes cat args
-  | otherwise = ppParens (d > 0) (foldr ppCtxt (ppRes cat args) ctxt)
+ppType :: Int -> [CId] -> Type -> PP.Doc
+ppType d scope (DTyp hyps cat args)
+  | null hyps = ppRes scope cat args
+  | otherwise = let (scope',hdocs) = mapAccumL ppHypo scope hyps
+                in ppParens (d > 0) (foldr (\hdoc doc -> hdoc PP.<+> PP.text "->" PP.<+> doc) (ppRes scope' cat args) hdocs)
   where
-    ppCtxt hyp doc = ppHypo hyp PP.<+> PP.text "->" PP.<+> doc
-    ppRes cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 2) es)
+    ppRes scope cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 4 scope) es)
 
-ppHypo (Hyp    typ) = ppType 1 typ
-ppHypo (HypV x typ) = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
-ppHypo (HypI x typ) = PP.braces (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
+ppHypo scope (Hyp    typ) = (  scope,ppType 1 scope typ)
+ppHypo scope (HypV x typ) = let y = freshName x scope
+                            in (y:scope,PP.parens (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
+ppHypo scope (HypI x typ) = let y = freshName x scope
+                            in (y:scope,PP.braces (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
 
 ppParens :: Bool -> PP.Doc -> PP.Doc
 ppParens True  = PP.parens
diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs
index 3fba99302..ddccc2e70 100644
--- a/src/PGF/TypeCheck.hs
+++ b/src/PGF/TypeCheck.hs
@@ -1,201 +1,463 @@
 ----------------------------------------------------------------------
 -- |
--- Module      : TypeCheck
--- Maintainer  : AR
+-- Module      : PGF.TypeCheck
+-- Maintainer  : Krasimir Angelov
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- type checking in abstract syntax with dependent types.
+-- Type checking in abstract syntax with dependent types.
+-- The type checker also performs renaming and checking for unknown
+-- functions. The variable references are replaced by de Bruijn indices.
 --
--- modified from src GF TC
 -----------------------------------------------------------------------------
 
-module PGF.TypeCheck (
-		   typecheck
-		  ) where
+module PGF.TypeCheck (checkType, checkExpr, inferExpr,
+
+                      ppTcError, TcError(..)
+                     ) where
 
 import PGF.Data
-import PGF.Macros (lookDef,isData)
 import PGF.Expr
+import PGF.Macros (typeOfHypo)
 import PGF.CId
 
-import GF.Data.ErrM
-import qualified Data.Map as Map
-import Control.Monad (liftM2,foldM)
-import Data.List (partition,sort,groupBy)
+import Data.Map as Map
+import Data.IntMap as IntMap
+import Data.Maybe as Maybe
+import Data.List as List
+import Control.Monad
+import Text.PrettyPrint
 
-import Debug.Trace
+-----------------------------------------------------
+-- The Scope
+-----------------------------------------------------
 
-typecheck :: PGF -> Expr -> [Expr]
-typecheck pgf e = case inferExpr pgf (newMetas e) of
-  Ok e  -> [e]
-  Bad s -> trace s []
+data    TType = TTyp Env Type
+newtype Scope = Scope [(CId,TType)]
 
-inferExpr :: PGF -> Expr -> Err Expr
-inferExpr pgf e = case infer pgf emptyTCEnv e of
-  Ok (e,_,cs) -> let (ms,cs2) = splitConstraints pgf cs in case cs2 of
-    [] -> trace (prConstraints cs ++"\n"++ show ms) $ Ok (metaSubst ms e)
-    _  -> Bad ("Error in tree " ++ showExpr e ++ " :\n  " ++ prConstraints cs2)
-  Bad s -> Bad s
+emptyScope = Scope []
 
-infer :: PGF -> TCEnv -> Expr -> Err (Expr, Value, [(Value,Value)])
-infer pgf tenv@(k,rho,gamma) e = case e of
-   EVar x -> do
-     ty <- lookupEVar pgf tenv x
-     return (e,ty,[])
+addScopedVar :: CId -> TType -> Scope -> Scope
+addScopedVar x tty (Scope gamma) = Scope ((x,tty):gamma)
 
---   EInt i -> return (AInt i, valAbsInt, [])
---   EFloat i -> return (AFloat i, valAbsFloat, [])
---   K i -> return (AStr i, valAbsString, [])
+-- | returns the type and the De Bruijn index of a local variable
+lookupVar :: CId -> Scope -> Maybe (Int,TType)
+lookupVar x (Scope gamma) = listToMaybe [(i,tty) | ((y,tty),i) <- zip gamma [0..], x == y]
 
-   EApp f t -> do
-    (f',typ,csf) <- infer pgf tenv f 
-    case typ of
-      VClosure env (EPi x a b) -> do
-        (a',csa) <- checkExp pgf tenv t (VClosure env a)
-	let b' = eval (getFunEnv (abstract pgf)) (eins x (VClosure rho t) env) b
-	return $ (EApp f' a', b', csf ++ csa)
-      _ -> Bad ("function type expected for function " ++ show f)
-   _ -> Bad ("cannot infer type of expression" ++ show e)
+-- | returns the type and the name of a local variable
+getVar :: Int -> Scope -> (CId,TType)
+getVar i (Scope gamma) = gamma !! i
 
+scopeEnv :: Scope -> Env
+scopeEnv (Scope gamma) = let n = length gamma
+                         in [VGen (n-i-1) [] | i <- [0..n-1]]
 
-checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
-checkExp pgf tenv@(k,rho,gamma) e typ = do
-  let v = VGen k []
-  case e of
-    EMeta m -> return $ (e,[])
-    EAbs x t -> case typ of
-      VClosure env (EPi y a b) -> do
-	let a' = eval (getFunEnv (abstract pgf)) env a
-	(t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t 
-                            (VClosure (eins y v env) b)
-	return (EAbs x t', cs)
-      _ -> Bad ("function type expected for " ++ show e)
-    _ -> checkInferExp pgf tenv e typ
+scopeVars :: Scope -> [CId]
+scopeVars (Scope gamma) = List.map fst gamma
 
-getFunEnv abs = Map.union (funs abs) (Map.map (\hypos -> (DTyp hypos cidType [],0,[])) (cats abs))
+scopeSize :: Scope -> Int
+scopeSize (Scope gamma) = length gamma
+
+-----------------------------------------------------
+-- The Monad
+-----------------------------------------------------
+
+type MetaStore = IntMap MetaValue
+data MetaValue
+  = MUnbound Scope [Expr -> TcM ()]
+  | MBound   Expr
+  | MGuarded Expr  [Expr -> TcM ()] {-# UNPACK #-} !Int   -- the Int is the number of constraints that have to be solved 
+                                                          -- to unlock this meta variable
+
+newtype TcM a = TcM {unTcM :: Abstr -> MetaId -> MetaStore -> TcResult a}
+data TcResult a
+  = Ok {-# UNPACK #-} !MetaId MetaStore a
+  | Fail TcError
+
+instance Monad TcM where
+  return x = TcM (\abstr metaid ms -> Ok metaid ms x)
+  f >>= g  = TcM (\abstr metaid ms -> case unTcM f abstr metaid ms of
+                                        Ok metaid ms x   -> unTcM (g x) abstr metaid ms
+                                        Fail e           -> Fail e)
+
+instance Functor TcM where
+  fmap f x = TcM (\abstr metaid ms -> case unTcM x abstr metaid ms of
+                                        Ok metaid ms x   -> Ok metaid ms (f x)
+                                        Fail e           -> Fail e)
+
+lookupCatHyps :: CId -> TcM [Hypo]
+lookupCatHyps cat = TcM (\abstr metaid ms -> case Map.lookup cat (cats abstr) of
+                                               Just hyps -> Ok metaid ms hyps
+                                               Nothing   -> Fail (UnknownCat cat))
+
+lookupFunType :: CId -> TcM TType
+lookupFunType fun = TcM (\abstr metaid ms -> case Map.lookup fun (funs abstr) of
+                                               Just (ty,_,_) -> Ok metaid ms (TTyp [] ty)
+                                               Nothing       -> Fail (UnknownFun fun))
+
+newMeta :: Scope -> TcM MetaId
+newMeta scope = TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MUnbound scope []) ms) metaid)
+
+newGuardedMeta :: Scope -> Expr -> TcM MetaId
+newGuardedMeta scope e = getFuns >>= \funs -> TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
+
+getMeta :: MetaId -> TcM MetaValue
+getMeta i = TcM (\abstr metaid ms -> Ok metaid ms $! case IntMap.lookup i ms of
+                                                       Just mv  -> mv)
+setMeta :: MetaId -> MetaValue -> TcM ()
+setMeta i mv = TcM (\abstr metaid ms -> Ok metaid (IntMap.insert i mv ms) ())
+
+tcError :: TcError -> TcM a
+tcError e = TcM (\abstr metaid ms -> Fail e)
+
+getFuns :: TcM Funs
+getFuns = TcM (\abstr metaid ms -> Ok metaid ms (funs abstr))
+
+addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM ()
+addConstraint i j env vs c = do
+  funs <- getFuns
+  mv   <- getMeta j
+  case mv of
+    MUnbound scope cs           -> addRef >> setMeta j (MUnbound scope ((\e -> release >> c (apply funs env e vs)) : cs))
+    MBound   e                  -> c (apply funs env e vs)
+    MGuarded e cs x | x == 0    -> c (apply funs env e vs)
+                    | otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c (apply funs env e vs)) : cs) x)
   where
-    cidType = mkCId "Type"
+    addRef  = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
+                                         Just (MGuarded e cs x) -> Ok metaid (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
 
-checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
-checkInferExp pgf tenv@(k,_,_) e typ = do
-  (e',w,cs1) <- infer pgf tenv e
-  let cs2 = eqValue (getFunEnv (abstract pgf)) k w typ
-  return (e',cs1 ++ cs2)
-      
-lookupEVar :: PGF -> TCEnv -> CId -> Err Value
-lookupEVar pgf (_,g,_) x = case Map.lookup x g of
-  Just v -> return v
-  _ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . (\(a,b,c) -> a)) $ 
-         Map.lookup x (funs (abstract pgf))
+    release = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
+                                         Just (MGuarded e cs x) -> if x == 1
+                                                                     then unTcM (sequence_ [c e | c <- cs]) abstr metaid (IntMap.insert i (MGuarded e [] 0) ms)
+                                                                     else Ok metaid (IntMap.insert i (MGuarded e cs (x-1)) ms) ())
 
-type2expr :: Type -> Expr
-type2expr (DTyp hyps cat es) = 
-  foldr (uncurry EPi) (foldl EApp (EVar cat) es) [toPair h | h <- hyps]
+-----------------------------------------------------
+-- Type errors
+-----------------------------------------------------
+
+data TcError
+  = UnknownCat      CId
+  | UnknownFun      CId
+  | WrongCatArgs    Scope Type CId  Int Int
+  | TypeMismatch    Scope Expr Type Type
+  | NotFunType      Scope Expr Type
+  | CannotInferType Scope Expr
+  | UnresolvedMetaVars Scope Expr [MetaId]
+
+ppTcError :: TcError -> Doc
+ppTcError (UnknownCat cat)                = text "Category" <+> text (prCId cat) <+> text "is not in scope"
+ppTcError (UnknownFun fun)                = text "Function" <+> text (prCId fun) <+> text "is not in scope"
+ppTcError (WrongCatArgs scope ty cat m n) =
+   text "Category" <+> text (prCId cat) <+> text "should have" <+> int m <+> text "argument(s), but has been given" <+> int n $$
+   text "In the type:" <+> ppType 0 (scopeVars scope) ty
+ppTcError (TypeMismatch scope e ty1 ty2)  = text "Couldn't match expected type" <+> ppType 0 (scopeVars scope) ty1 $$
+                                            text "       against inferred type" <+> ppType 0 (scopeVars scope) ty2 $$
+                                            text "In the expression:" <+> ppExpr 0 (scopeVars scope) e
+ppTcError (NotFunType scope e ty)         = text "A function type is expected for the expression" <+> ppExpr 0 (scopeVars scope) e <+> text "instead of type" <+> ppType 0 (scopeVars scope) ty
+ppTcError (CannotInferType scope e)       = text "Cannot infer the type of expression" <+> ppExpr 0 (scopeVars scope) e
+ppTcError (UnresolvedMetaVars scope e xs) = text "Meta variable(s)" <+> fsep (List.map ppMeta xs) <+> text "should be resolved" $$
+                                            text "in the expression:" <+> ppExpr 0 (scopeVars scope) e
+
+-----------------------------------------------------
+-- checkType
+-----------------------------------------------------
+
+checkType :: PGF -> Type -> Either TcError Type
+checkType pgf ty = 
+  case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) 0 IntMap.empty of
+    Ok _ ms ty  -> Right ty
+    Fail err    -> Left  err
+
+tcType :: Scope -> Type -> TcM Type
+tcType scope ty@(DTyp hyps cat es) = do
+  (scope,hyps) <- tcHypos scope hyps
+  c_hyps <- lookupCatHyps cat
+  let m = length es
+      n = length c_hyps
+  if m == n
+    then do (delta,es) <- tcHypoExprs scope [] (zip es c_hyps)
+            return (DTyp hyps cat es)
+    else tcError (WrongCatArgs scope ty cat n m)
+
+tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo])
+tcHypos scope []     = return (scope,[])
+tcHypos scope (h:hs) = do
+  (scope,h ) <- tcHypo  scope h
+  (scope,hs) <- tcHypos scope hs
+  return (scope,h:hs)
+
+tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
+tcHypo scope (Hyp    ty) = do
+  ty <- tcType scope ty
+  return (scope,Hyp ty)
+tcHypo scope (HypV x ty) = do
+  ty <- tcType scope ty
+  return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,HypV x ty)
+
+tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr])
+tcHypoExprs scope delta []         = return (delta,[])
+tcHypoExprs scope delta ((e,h):xs) = do
+  (delta,e ) <- tcHypoExpr scope delta e h
+  (delta,es) <- tcHypoExprs scope delta xs
+  return (delta,e:es)
+
+tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr)
+tcHypoExpr scope delta e (Hyp    ty) = do
+  e  <- tcExpr scope e (TTyp delta ty)
+  return (delta,e)
+tcHypoExpr scope delta e (HypV x ty) = do
+  e  <- tcExpr scope e (TTyp delta ty)
+  funs <- getFuns
+  return (eval funs (scopeEnv scope) e:delta,e)
+
+
+-----------------------------------------------------
+-- checkExpr
+-----------------------------------------------------
+
+checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
+checkExpr pgf e ty =
+  case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
+                 e <- refineExpr e
+                 checkResolvedMetaStore emptyScope e
+                 return e) (abstract pgf) 0 IntMap.empty of
+    Ok _ ms e  -> Right e
+    Fail err   -> Left err
+
+tcExpr :: Scope -> Expr -> TType -> TcM Expr
+tcExpr scope e0@(EAbs x e) tty =
+  case tty of
+    TTyp delta (DTyp (h:hs) c es) -> do e <- case h of
+                                               Hyp    ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
+                                                                   e (TTyp delta (DTyp hs c es))
+                                               HypV y ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
+                                                                   e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
+                                        return (EAbs x e)
+    _                             -> do ty <- evalType (scopeSize scope) tty
+                                        tcError (NotFunType scope e0 ty)
+tcExpr scope (EMeta _) tty = do
+  i <- newMeta scope
+  return (EMeta i)
+tcExpr scope e0        tty = do
+  (e0,tty0) <- infExpr scope e0
+  i <- newGuardedMeta scope e0
+  eqType scope (scopeSize scope) i tty tty0
+  return (EMeta i)
+
+
+-----------------------------------------------------
+-- inferExpr
+-----------------------------------------------------
+
+inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
+inferExpr pgf e =
+  case unTcM (do (e,tty) <- infExpr emptyScope e
+                 e <- refineExpr e
+                 checkResolvedMetaStore emptyScope e
+                 ty <- evalType 0 tty
+                 return (e,ty)) (abstract pgf) 1 IntMap.empty of
+    Ok _ ms (e,ty) -> Right (e,ty)
+    Fail err       -> Left err
+
+infExpr :: Scope -> Expr -> TcM (Expr,TType)
+infExpr scope e0@(EApp e1 e2) = do
+  (e1,tty1) <- infExpr scope e1
+  case tty1 of
+    (TTyp delta1 (DTyp (h:hs) c es)) -> do (delta1,e2) <- tcHypoExpr scope delta1 e2 h
+                                           return (EApp e1 e2,TTyp delta1 (DTyp hs c es))
+    _                                -> do ty1 <- evalType (scopeSize scope) tty1
+                                           tcError (NotFunType scope e1 ty1)
+infExpr scope e0@(EFun x) = do
+  case lookupVar x scope of
+    Just (i,tty) -> return (EVar i,tty)
+    Nothing      -> do tty <- lookupFunType x
+                       return (e0,tty)
+infExpr scope e0@(EVar i) = do
+  return (e0,snd (getVar i scope))
+infExpr scope e0@(ELit l) = do
+  let cat = case l of
+              LStr _ -> mkCId "String"
+              LInt _ -> mkCId "Int"
+              LFlt _ -> mkCId "Float"
+  return (e0,TTyp [] (DTyp [] cat []))
+infExpr scope (ETyped e ty) = do
+  ty <- tcType scope ty
+  e  <- tcExpr scope e (TTyp (scopeEnv scope) ty)
+  return (ETyped e ty,TTyp (scopeEnv scope) ty)
+infExpr scope e = tcError (CannotInferType scope e)
+
+-----------------------------------------------------
+-- eqType
+-----------------------------------------------------
+
+eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM ()
+eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 ty2@(DTyp hyps2 cat2 es2))
+  | cat1 == cat2 = do (k,delta1,delta2) <- eqHyps k delta1 hyps1 delta2 hyps2
+                      sequence_ [eqExpr k delta1 e1 delta2 e2 | (e1,e2) <- zip es1 es2]
+  | otherwise    = raiseTypeMatchError
   where
-    toPair (Hyp    t) = (wildCId, type2expr t)
-    toPair (HypV x t) = (x,       type2expr t)
+    raiseTypeMatchError = do ty1 <- evalType k tty1
+                             ty2 <- evalType k tty2
+                             e   <- refineExpr (EMeta i0)
+                             tcError (TypeMismatch scope e ty1 ty2)
 
-type TCEnv = (Int,Env,Env)
+    eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env)
+    eqHyps k delta1 []                 delta2 []                 =
+      return (k,delta1,delta2)
+    eqHyps k delta1 (Hyp    ty1 : h1s) delta2 (Hyp    ty2 : h2s) = do
+      eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
+      (k,delta1,delta2) <- eqHyps k delta1 h1s delta2 h2s
+      return (k,delta1,delta2)
+    eqHyps k delta1 (HypV x ty1 : h1s) delta2 (HypV y ty2 : h2s) = do
+      eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
+      (k,delta1,delta2) <- eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
+      return (k,delta1,delta2)
+    eqHyps k delta1               h1s  delta2               h2s  = raiseTypeMatchError
 
-eempty = Map.empty
-eins = Map.insert
+    eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
+    eqExpr k env1 e1 env2 e2 = do
+      funs <- getFuns
+      eqValue k (eval funs env1 e1) (eval funs env2 e2)
 
-emptyTCEnv :: TCEnv
-emptyTCEnv = (0,eempty,eempty)
+    eqValue :: Int -> Value -> Value -> TcM ()
+    eqValue k v1 v2 = do
+      v1 <- deRef v1
+      v2 <- deRef v2
+      eqValue' k v1 v2
+
+    deRef v@(VMeta i env vs) = do
+      mv   <- getMeta i
+      funs <- getFuns
+      case mv of
+        MBound   e                 -> deRef (apply funs env e vs)
+        MGuarded e _ x | x == 0    -> deRef (apply funs env e vs)
+                       | otherwise -> return v
+        MUnbound _ _               -> return v
+    deRef v = return v
+
+    eqValue' k (VSusp i env vs1 c)          v2                           = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2)
+    eqValue' k v1                           (VSusp i env vs2 c)          = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2))
+    eqValue' k (VMeta i env1 vs1)           (VMeta j env2 vs2) | i  == j = zipWithM_ (eqValue k) vs1 vs2
+    eqValue' k (VMeta i env1 vs1)           v2                           = do (MUnbound scopei cs) <- getMeta i
+                                                                              e2 <- mkLam i scopei env1 vs1 v2
+                                                                              sequence_ [c e2 | c <- cs]
+                                                                              setMeta i (MBound e2)
+    eqValue' k v1                           (VMeta i env2 vs2)           = do (MUnbound scopei cs) <- getMeta i
+                                                                              e1 <- mkLam i scopei env2 vs2 v1
+                                                                              sequence_ [c e1 | c <- cs]
+                                                                              setMeta i (MBound e1)
+    eqValue' k (VApp f1 vs1)                (VApp f2 vs2) | f1 == f2     = zipWithM_ (eqValue k) vs1 vs2
+    eqValue' k (VLit l1)                    (VLit l2    ) | l1 == l2     = return ()
+    eqValue' k (VGen  i vs1)                (VGen  j vs2) | i  == j      = zipWithM_ (eqValue k) vs1 vs2
+    eqValue' k (VClosure env1 (EAbs x1 e1)) (VClosure env2 (EAbs x2 e2)) = let v = VGen k []
+                                                                           in eqExpr (k+1) (v:env1) e1 (v:env2) e2
+    eqValue' k v1                           v2                           = raiseTypeMatchError
+
+    mkLam i scope env vs0 v = do
+      let k  = scopeSize scope
+          vs  = reverse (take k env) ++ vs0
+          xs  = nub [i | VGen i [] <- vs]
+      if length vs == length xs
+        then return ()
+        else raiseTypeMatchError
+      v <- occurCheck i k xs v
+      funs <- getFuns
+      return (addLam vs0 (value2expr funs (length xs) v))
+      where
+        addLam []     e = e
+        addLam (v:vs) e = EAbs var (addLam vs e)
+
+        var = mkCId "v"
+
+    occurCheck i0 k xs (VApp f vs)      = do vs <- mapM (occurCheck i0 k xs) vs
+                                             return (VApp f vs)
+    occurCheck i0 k xs (VLit l)         = return (VLit l)
+    occurCheck i0 k xs (VMeta i env vs) = do if i == i0
+                                               then raiseTypeMatchError
+                                               else return ()
+                                             mv <- getMeta i
+                                             funs <- getFuns
+                                             case mv of
+                                               MBound   e                               -> occurCheck i0 k xs (apply funs env e vs)
+                                               MGuarded e _ _                           -> occurCheck i0 k xs (apply funs env e vs)
+                                               MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
+                                                                 | otherwise            -> do vs <- mapM (occurCheck i0 k xs) vs
+                                                                                              return (VMeta i env vs)
+    occurCheck i0 k xs (VSusp i env vs cnt) = do addConstraint i0 i env vs (\v -> occurCheck i0 k xs (cnt v) >> return ())
+                                                 return (VSusp i env vs cnt)
+    occurCheck i0 k xs (VGen  i vs)     = case List.findIndex (==i) xs of
+                                            Just i  -> do vs <- mapM (occurCheck i0 k xs) vs
+                                                          return (VGen i vs)
+                                            Nothing -> raiseTypeMatchError
+    occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env
+                                             return (VClosure env e)
 
 
--- this is not given in Expr
-prValue = showExpr . value2expr
+-----------------------------------------------------------
+-- check for meta variables that still have to be resolved
+-----------------------------------------------------------
 
-value2expr v = case v of
-  VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
-  VMeta i vs -> foldl EApp (EMeta i) (map value2expr vs)
-  VClosure g e -> e ----
-  VLit l -> ELit l
+checkResolvedMetaStore :: Scope -> Expr -> TcM ()
+checkResolvedMetaStore scope e = TcM (\abstr metaid ms -> 
+  let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
+  in if List.null xs
+       then Ok metaid ms ()
+       else Fail (UnresolvedMetaVars scope e xs))
+  where
+    isResolved (MUnbound _ [])   = True
+    isResolved (MGuarded  _ _ _) = True
+    isResolved (MBound    _)     = True
+    isResolved _                 = False
 
-prConstraints :: [(Value,Value)] -> String
-prConstraints cs = unwords 
-  ["(" ++ prValue v ++ " <> " ++ prValue w ++ ")" | (v,w) <- cs]
+-----------------------------------------------------
+-- evalType
+-----------------------------------------------------
 
--- work more on this: unification, compute,...
-
-{-
-splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
-splitConstraints pgf = mkSplit . partition isSubst . regroup . map reorder . map reduce where
-  reorder (v,w) = case w of
-    VMeta _ _ -> (w,v)
-    _ -> (v,w)
-
-  reduce (v,w) = (whnf v,whnf w)
-
-  whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e   -- should be removed when the typechecker is improved
-  whnf v                = v
-
-  regroup = groupBy (\x y -> fst x == fst y) . sort
-
-  isSubst cs@((v,u):_) = case v of
-    VMeta _ _ -> all ((==u) . snd) cs
-    _ -> False
-  mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i _,v):_ <- ms], concat cs)
--}
-
-splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
-splitConstraints pgf = mkSplit . unifyAll [] . map reduce where
-  reduce (v,w) = (whnf v,whnf w)
-
-  whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e -- should be removed when the typechecker is improved
-  whnf v                = v
-  mkSplit (ms,cs) = ([(i,value2expr v) | (i,v) <- ms], cs)
-
-  unifyAll g [] = (g, [])
-  unifyAll g ((a@(s, t)) : l) =
-    let (g1, c) = unifyAll g l
-    in case unify s t g1 of
-         Just g2  -> (g2, c)
-         _        -> (g1, a : c)
-
-  unify e1 e2 g = case (e1, e2) of 
-    (VMeta s _, t) -> do
-      let tg = substMetas g t
-      let sg = maybe e1 id (lookup s g)
-      if null (eqValue (funs (abstract pgf)) 0 sg e1) then extend s tg g else unify sg tg g 
-    (t, VMeta _ _) -> unify e2 e1 g
-    (VApp c as, VApp d bs) | c == d -> 
-       foldM (\ h (a,b) -> unify a b h) g (zip as bs)
-    _ -> Nothing
-
-  extend s t g = case t of
-    VMeta u _ | u == s -> return g  
-    _ | occCheck s t   -> Nothing
-    _                  -> return ((s, t) : g) 
-
-  substMetas subst trm = case trm of
-    VMeta s _ -> maybe trm id (lookup s subst)
-    VApp c vs -> VApp c (map (substMetas subst) vs)
-    _ -> trm
-
-  occCheck s u = case u of
-    VMeta t _ -> s == t
-    VApp c as -> any (occCheck s) as
-    _         -> False
+evalType :: Int -> TType -> TcM Type
+evalType k (TTyp delta ty) = do funs <- getFuns
+                                refineType (evalTy funs k delta ty)
+  where
+    evalTy sig k delta (DTyp hyps cat es) = 
+      let ((k1,delta1),hyps1) = mapAccumL (evalHypo sig) (k,delta) hyps
+      in DTyp hyps1 cat (List.map (normalForm sig k1 delta1) es)
+    
+    evalHypo sig (k,delta) (Hyp    ty) = ((k,              delta),Hyp    (evalTy sig k delta ty))
+    evalHypo sig (k,delta) (HypV x ty) = ((k+1,(VGen k []):delta),HypV x (evalTy sig k delta ty))
+    evalHypo sig (k,delta) (HypI x ty) = ((k+1,(VGen k []):delta),HypI x (evalTy sig k delta ty))
 
 
-metaSubst :: [(Int,Expr)] -> Expr -> Expr
-metaSubst vs exp = case exp of
-  EApp u v  -> EApp (subst u) (subst v)
-  EMeta i   -> maybe exp id $ lookup i vs
-  EPi x a b -> EPi x (subst a) (subst b)
-  EAbs x b  -> EAbs x (subst b)
-  _ -> exp
- where
-  subst = metaSubst vs
+-----------------------------------------------------
+-- refinement
+-----------------------------------------------------
 
---- use composOp and state monad...
-newMetas :: Expr -> Expr
-newMetas = fst . metas 0 where
-  metas i exp = case exp of
-    EAbs x e -> let (f,j) = metas i e in (EAbs x f, j)
-    EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k)
-    EMeta _  -> (EMeta i, i+1)
-    _        -> (exp,i)
+refineExpr :: Expr -> TcM Expr
+refineExpr e = TcM (\abstr metaid ms -> Ok metaid ms (refineExpr_ ms e))
+
+refineExpr_ ms e = refine e
+  where
+    refine (EAbs x e)    = EAbs x (refine e)
+    refine (EApp e1 e2)  = EApp (refine e1) (refine e2)
+    refine (ELit l)      = ELit l
+    refine (EMeta i)     = case IntMap.lookup i ms of
+                             Just (MBound   e    ) -> refine e
+                             Just (MGuarded e _ _) -> refine e
+                             _                     -> EMeta i
+    refine (EFun f)      = EFun f
+    refine (EVar i)      = EVar i
+    refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty)
+
+refineType :: Type -> TcM Type
+refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
+
+refineType_ ms (DTyp hyps cat es) = DTyp (List.map (refineHypo_ ms) hyps) cat (List.map (refineExpr_ ms) es)
+
+refineHypo_ ms (Hyp    ty) = Hyp    (refineType_ ms ty)
+refineHypo_ ms (HypV x ty) = HypV x (refineType_ ms ty)
+refineHypo_ ms (HypI x ty) = HypI x (refineType_ ms ty)
+
+value2expr sig i (VApp f vs)               = foldl EApp (EFun f)           (List.map (value2expr sig i) vs)
+value2expr sig i (VGen j vs)               = foldl EApp (EVar (i-j-1))     (List.map (value2expr sig i) vs)
+value2expr sig i (VMeta j env vs)          = foldl EApp (EMeta j) (List.map (value2expr sig i) vs)
+value2expr sig i (VSusp j env vs k)        = value2expr sig i (k (VGen j vs))
+value2expr sig i (VLit l)                  = ELit l
+value2expr sig i (VClosure env (EAbs x e)) = EAbs x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
diff --git a/testsuite/runtime/eval/Test.gf b/testsuite/runtime/eval/Test.gf
index 71a7dc2c2..a0131d767 100644
--- a/testsuite/runtime/eval/Test.gf
+++ b/testsuite/runtime/eval/Test.gf
@@ -14,7 +14,7 @@ def g0 = g2 ;
 fun g3 : Int -> (Int -> Int) ;
 def g3 3 = g ;
 
-fun const : Int -> Int -> Int ;
+fun const : Float -> String -> Float ;
 def const x _ = x ;
 
 cat Nat ;
diff --git a/testsuite/runtime/eval/eval.gfs b/testsuite/runtime/eval/eval.gfs
index dd1cede9c..557bb9f90 100644
--- a/testsuite/runtime/eval/eval.gfs
+++ b/testsuite/runtime/eval/eval.gfs
@@ -1,34 +1,30 @@
 i testsuite/runtime/eval/Test.gf
 
-pt -compute \x -> x 1
-pt -compute ? 1
-pt -compute (\x -> x 1) ?
-pt -compute unknown_var
-pt -compute unknown_var 1
-pt -compute 1 2
+pt -compute \x -> x 1 : (Int->Int)->Int
+pt -compute (? : Int -> Int) 1
+pt -compute (\x -> x 1 : (Int->Int)->Int) ?
 pt -compute f 1 2
-pt -compute \x -> x
-pt -compute ?666
+pt -compute \x -> x : Nat -> Nat
+pt -compute ? : String
 pt -compute f
-pt -compute (\x -> x 2) (f 1)
-pt -compute (\x -> x 2) 1
+pt -compute (\x -> x 2 : (Int->Int)->Int) (f 1)
 pt -compute g 1
 pt -compute g 0
-pt -compute \x -> g x
+pt -compute \x -> g x : Int -> Int
 pt -compute g ?
-pt -compute (\x -> x 5) (g2 1)
-pt -compute (\x -> x 3) (\x -> x)
+pt -compute (\x -> x 5 : (Int->Int)->Int) (g2 1)
+pt -compute (\x -> x 3 : (Int->Int)->Int) (\x -> x)
 pt -compute g0
-pt -compute (\x -> x 3.2) (\x -> f x)
-pt -compute g0 2.3
-pt -compute g0 ((\x -> f x) 0) 1
+pt -compute (\x -> x 32 : (Int -> Int -> Int) -> Int -> Int) (\x -> f x : Int -> Int -> Int)
+pt -compute g0 23
 pt -compute const 3.14 "pi"
 pt -compute dec (succ (succ zero))
 pt -compute dec (succ ?)
-pt -compute \x -> dec x
+pt -compute \x -> dec x : Nat -> Nat
 pt -compute dec ?
-pt -compute (\f -> f 0) (g3 ?)
+pt -compute (\f -> f 0 : (Int -> Int) -> Int) (g3 ?)
 pt -compute g (g2 ? 0)
 pt -compute plus (succ zero) (succ zero)
 pt -compute dec2 0 (succ zero)
+pt -compute dec2 0 err
 pt -compute plus err (succ zero)
\ No newline at end of file
diff --git a/testsuite/runtime/eval/eval.gfs.gold b/testsuite/runtime/eval/eval.gfs.gold
index 861c8534c..1c6282f27 100644
--- a/testsuite/runtime/eval/eval.gfs.gold
+++ b/testsuite/runtime/eval/eval.gfs.gold
@@ -1,30 +1,26 @@
-\v0 -> v0 1

+\x -> x 1

 

-? 1

+?1 1

 

-? 1

+?3 1

 

-unknown variable unknown_var

-unknown variable unknown_var

-literal of function type

 f 1 2

 

-\v0 -> v0

+\x -> x

 

-?666

+?1

 

 f

 

 f 1 2

 

-literal of function type

 2

 

 g 0

 

-\v0 -> g v0

+\x -> g x

 

-g ?

+g ?1

 

 5

 

@@ -32,29 +28,29 @@ g ?
 

 g2

 

-f 3.2

+f 32

 

-g2 2.3

-

-g2 (f 0) 1

+g2 23

 

 3.14

 

 succ zero

 

-?

+?1

 

-\v0 -> dec v0

+\x -> dec x

 

-dec ?

+dec ?1

 

-g3 ? 0

+g3 ?3 0

 

-g (g2 ? 0)

+g (g2 ?1 0)

 

 succ (succ zero)

 

 zero

 

+dec2 0 err

+

 succ err

 

diff --git a/testsuite/runtime/paraphrase/lambda.gfs.gold b/testsuite/runtime/paraphrase/lambda.gfs.gold
index 0d8f027d6..5735dc175 100644
--- a/testsuite/runtime/paraphrase/lambda.gfs.gold
+++ b/testsuite/runtime/paraphrase/lambda.gfs.gold
@@ -1,10 +1,10 @@
-\v0 -> v0

+\x -> x

 

 1

 

-\v0 -> v0

+\x -> x

 

-\v0 -> 2

+\x -> 2

 

 1

 

diff --git a/testsuite/runtime/typecheck/Test.gf b/testsuite/runtime/typecheck/Test.gf
new file mode 100644
index 000000000..8ef0e03cf
--- /dev/null
+++ b/testsuite/runtime/typecheck/Test.gf
@@ -0,0 +1,37 @@
+abstract Test = {
+
+cat Nat ;
+data zero : Nat ;
+     succ : Nat -> Nat ;
+
+fun plus : Nat -> Nat -> Nat ;
+def plus zero     n = n ;
+    plus (succ m) n = plus m (succ n) ;
+
+cat Vector Nat ;
+fun vector : (n : Nat) -> Vector n ;
+
+fun append : (m,n : Nat) -> Vector m -> Vector n -> Vector (plus m n) ;
+fun diff   : (m,n : Nat) -> Vector (plus m n) -> Vector m -> Vector n ;
+
+cat Morph (Nat -> Nat) ;
+fun mkMorph : (f : Nat -> Nat) -> Morph f ;
+fun mkMorph2 : (f : Nat -> Nat) -> Vector (f zero) -> Morph f ;
+fun idMorph : Morph (\x -> x) -> Nat ;
+
+fun f0 : (n : Nat)        -> ((m : Nat) -> Vector n)     -> Int ;
+fun f1 : (n : Nat -> Nat) -> ((m : Nat) -> Vector (n m)) -> Int ;
+
+fun cmpVector : (n : Nat) -> Vector n -> Vector n -> Int ;
+
+fun g : ((n : Nat) -> Vector n) -> Int ;
+
+cat U (n,m : Nat) ;
+fun u0 : (n : Nat) -> U n n ;
+fun u1 : (n : Nat) -> U n (succ n) ;
+fun h  : (n : Nat) -> U n n -> Int ;
+
+-- fun u2 : (n : Nat) -> U (plus n zero) zero ;
+-- fun h2 : (f : Nat -> Nat) -> ((n : Nat) -> U (f n) (f zero)) -> Int ;
+
+}
\ No newline at end of file
diff --git a/testsuite/runtime/typecheck/typecheck.gfs b/testsuite/runtime/typecheck/typecheck.gfs
new file mode 100644
index 000000000..b1231a75d
--- /dev/null
+++ b/testsuite/runtime/typecheck/typecheck.gfs
@@ -0,0 +1,30 @@
+i testsuite/runtime/typecheck/Test.gf
+
+ai succ "0"
+ai succ : Int 0
+ai 1 2
+ai (\x -> x 2 : (Int->Int)->Int) 1
+ai unknown_fun
+ai 0 : unknown_cat
+ai \x -> x
+ai \x -> x : Int
+ai append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero))
+ai \m,n -> vector (plus m n) : (m,n : Nat) -> Vector (plus m n)
+ai mkMorph (\x -> succ zero)
+ai idMorph (mkMorph (\x -> x))
+ai idMorph (mkMorph (\x -> succ zero))
+ai append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero)
+ai \n,v1,n,v2 -> append ? ? v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)
+ai \n -> (\v1,v2 -> eqVector n v1 v2 : Vector ? -> Vector ? -> EQ) (vector ?) : (n : Nat) -> Vector n -> EQ
+ai (\v1,v2 -> cmpVector ? v1 v2 : Vector ? -> Vector ? -> Int) (vector ?) 
+ai f0 ? vector
+ai f1 ? vector
+ai f1 ? (\x -> vector (succ x))
+ai mkMorph (\x -> cmpVector ? (vector x) (vector (succ x)))
+ai g (\n -> vector (succ n))
+ai h ? (u0 ?)
+ai h ? (u1 ?)
+ai cmpVector (succ (succ zero)) (vector (succ (succ zero))) (append ? (succ zero) (vector ?) (vector (succ zero)))
+ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ (succ zero)))))) (vector (succ (succ (succ zero))))
+ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ zero))))) (vector (succ (succ (succ zero))))
+ai idMorph (mkMorph2 (\x -> ?) (vector zero))
\ No newline at end of file
diff --git a/testsuite/runtime/typecheck/typecheck.gfs.gold b/testsuite/runtime/typecheck/typecheck.gfs.gold
new file mode 100644
index 000000000..ca0412fb8
--- /dev/null
+++ b/testsuite/runtime/typecheck/typecheck.gfs.gold
@@ -0,0 +1,102 @@
+

+Couldn't match expected type Nat

+       against inferred type String

+In the expression: "0"

+

+

+Category Int should have 0 argument(s), but has been given 1

+In the type: Int 0

+

+

+A function type is expected for the expression 1 instead of type Int

+

+

+Couldn't match expected type Int -> Int

+       against inferred type Int

+In the expression: 1

+

+

+Function unknown_fun is not in scope

+

+

+Category unknown_cat is not in scope

+

+

+Cannot infer the type of expression \x -> x

+

+

+A function type is expected for the expression \x -> x instead of type Int

+

+Expression: append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero))

+Type:       Vector (plus (succ (succ zero)) (succ zero))

+

+Expression: \m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)

+Type:       (m : Nat) -> (n : Nat) -> Vector (plus m n)

+

+Expression: mkMorph (\x -> succ zero)

+Type:       Morph (\x -> succ zero)

+

+Expression: idMorph (mkMorph (\x -> x))

+Type:       Nat

+

+

+Couldn't match expected type Morph (\x -> x)

+       against inferred type Morph (\x -> succ zero)

+In the expression: mkMorph (\x -> succ zero)

+

+Expression: append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero)

+Type:       Vector zero -> Vector (succ zero) -> Vector (succ zero)

+

+Expression: \n, v1, n'1, v2 -> append n n'1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)

+Type:       (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)

+

+

+Category EQ is not in scope

+

+Expression: (\v1, v2 -> cmpVector ?7 v1 v2 : Vector ?7 -> Vector ?7 -> Int) (vector ?7)

+Type:       Vector ?7 -> Int

+

+

+Couldn't match expected type (m : Nat) -> Vector ?1

+       against inferred type (n : Nat) -> Vector n

+In the expression: vector

+

+Expression: f1 (\v -> v) vector

+Type:       Int

+

+Expression: f1 (\v -> succ v) (\x -> vector (succ x))

+Type:       Int

+

+

+Couldn't match expected type Vector x

+       against inferred type Vector (succ x)

+In the expression: vector (succ x)

+

+

+Couldn't match expected type Vector n

+       against inferred type Vector (succ n)

+In the expression: vector (succ n)

+

+Expression: h ?2 (u0 ?2)

+Type:       Int

+

+

+Couldn't match expected type U ?2 ?2

+       against inferred type U ?2 (succ ?2)

+In the expression: u1 ?2

+

+

+Meta variable(s) ?11 should be resolved

+in the expression: cmpVector (succ (succ zero)) (vector (succ (succ zero))) (append ?11 (succ zero) (vector ?11) (vector (succ zero)))

+

+Expression: diff (succ (succ (succ zero))) (succ (succ zero)) (vector (succ (succ (succ (succ (succ zero)))))) (vector (succ (succ (succ zero))))

+Type:       Vector (succ (succ zero))

+

+Couldn't match expected type Vector (plus (succ (succ (succ zero))) (succ (succ zero)))

+       against inferred type Vector (succ (succ (succ (succ zero))))

+In the expression: vector (succ (succ (succ (succ zero))))

+

+Couldn't match expected type Vector ?1

+       against inferred type Vector zero

+In the expression: vector zero

+