diff --git a/src/runtime/c/pgf/pgf.cxx b/src/runtime/c/pgf/pgf.cxx
index 72f73df20..cd530b8f2 100644
--- a/src/runtime/c/pgf/pgf.cxx
+++ b/src/runtime/c/pgf/pgf.cxx
@@ -1249,19 +1249,21 @@ void pgf_release_phrasetable_ids(PgfPhrasetableIds *seq_ids)
 }
 
 PGF_API
-void pgf_check_expr(PgfDB *db, PgfRevision revision,
-                    PgfExpr* pe, PgfType ty,
-                    PgfMarshaller *m, PgfUnmarshaller *u,
-                    PgfExn *err)
+PgfExpr pgf_check_expr(PgfDB *db, PgfRevision revision,
+                       PgfExpr e, PgfType ty,
+                       PgfMarshaller *m, PgfUnmarshaller *u,
+                       PgfExn *err)
 {
     PGF_API_BEGIN {
         DB_scope scope(db, READER_SCOPE);
 
         ref<PgfPGF> pgf = db->revision2pgf(revision);
 
-        PgfTypechecker checker(pgf,m,u);
-        *pe = m->match_expr(&checker, *pe);
+        PgfTypechecker checker(pgf,m,u,err);
+        return checker.check_expr(e, ty);
     } PGF_API_END
+
+    return 0;
 }
 
 PGF_API
@@ -1275,31 +1277,29 @@ PgfType pgf_infer_expr(PgfDB *db, PgfRevision revision,
 
         ref<PgfPGF> pgf = db->revision2pgf(revision);
 
-        PgfTypechecker checker(pgf,m,u);
-        *pe = m->match_expr(&checker, *pe);
+        PgfTypechecker checker(pgf,m,u,err);
+        return checker.infer_expr(pe);
     } PGF_API_END
 
-    PgfText *cat = (PgfText *) alloca(sizeof(PgfText)+2);
-    cat->size = 1;
-    cat->text[0] = 'S';
-    cat->text[1] = 0;
-    return u->dtyp(0,NULL,cat,0,NULL);
+    return 0;
 }
 
 PGF_API
-void pgf_check_type(PgfDB *db, PgfRevision revision,
-                    PgfType* pty,
-                    PgfMarshaller *m, PgfUnmarshaller *u,
-                    PgfExn *err)
+PgfType pgf_check_type(PgfDB *db, PgfRevision revision,
+                       PgfType ty,
+                       PgfMarshaller *m, PgfUnmarshaller *u,
+                       PgfExn *err)
 {
     PGF_API_BEGIN {
         DB_scope scope(db, READER_SCOPE);
 
         ref<PgfPGF> pgf = db->revision2pgf(revision);
 
-        PgfTypechecker checker(pgf,m,u);
-        *pty = m->match_type(&checker, *pty);
+        PgfTypechecker checker(pgf,m,u,err);
+        return checker.check_type(ty);
     } PGF_API_END
+
+    return 0;
 }
 
 PGF_API
@@ -1647,7 +1647,7 @@ void pgf_drop_category(PgfDB *db, PgfRevision revision,
             itor.fn       = iter_drop_cat_helper;
             itor.pgf      = pgf;
             PgfProbspace funs_by_cat =
-                probspace_delete_by_cat(pgf->abstract.funs_by_cat, &cat->name,
+                probspace_delete_by_cat(pgf->abstract.funs_by_cat, name,
                                         &itor, err);
             pgf->abstract.funs_by_cat = funs_by_cat;
             PgfAbsCat::release(cat);
diff --git a/src/runtime/c/pgf/pgf.h b/src/runtime/c/pgf/pgf.h
index 9747ecad3..cb5852529 100644
--- a/src/runtime/c/pgf/pgf.h
+++ b/src/runtime/c/pgf/pgf.h
@@ -522,10 +522,10 @@ PGF_API_DECL
 void pgf_release_phrasetable_ids(PgfPhrasetableIds *seq_ids);
 
 PGF_API_DECL
-void pgf_check_expr(PgfDB *db, PgfRevision revision,
-                    PgfExpr* pe, PgfType ty,
-                    PgfMarshaller *m, PgfUnmarshaller *u,
-                    PgfExn *err);
+PgfExpr pgf_check_expr(PgfDB *db, PgfRevision revision,
+                       PgfExpr e, PgfType ty,
+                       PgfMarshaller *m, PgfUnmarshaller *u,
+                       PgfExn *err);
 
 PGF_API_DECL
 PgfType pgf_infer_expr(PgfDB *db, PgfRevision revision,
@@ -534,10 +534,10 @@ PgfType pgf_infer_expr(PgfDB *db, PgfRevision revision,
                        PgfExn *err);
 
 PGF_API_DECL
-void pgf_check_type(PgfDB *db, PgfRevision revision,
-                    PgfType* pty,
-                    PgfMarshaller *m, PgfUnmarshaller *u,
-                    PgfExn *err);
+PgfType pgf_check_type(PgfDB *db, PgfRevision revision,
+                       PgfType ty,
+                       PgfMarshaller *m, PgfUnmarshaller *u,
+                       PgfExn *err);
 
 PGF_API_DECL
 PgfExpr pgf_generate_random(PgfDB *db, PgfRevision revision,
diff --git a/src/runtime/c/pgf/typechecker.cxx b/src/runtime/c/pgf/typechecker.cxx
index 36b3ae3d4..6d29af00b 100644
--- a/src/runtime/c/pgf/typechecker.cxx
+++ b/src/runtime/c/pgf/typechecker.cxx
@@ -1,84 +1,464 @@
+#include <stdarg.h>
 #include "data.h"
 #include "typechecker.h"
 
-PgfExpr PgfTypechecker::eabs(PgfBindType btype, PgfText *name, PgfExpr body)
+class PgfTypechecker::Unmarshaller1 : public PgfUnmarshaller {
+    virtual PgfExpr eabs(PgfBindType bind_type, PgfText *name, PgfExpr body) { return 0; }
+    virtual PgfExpr eapp(PgfExpr fun, PgfExpr arg) { return 0; }
+    virtual PgfExpr elit(PgfLiteral lit) { return 0; }
+    virtual PgfExpr emeta(PgfMetaId meta_id) { return 0; }
+    virtual PgfExpr efun(PgfText *name) { return 0; }
+    virtual PgfExpr evar(int index) { return 0; }
+    virtual PgfExpr etyped(PgfExpr expr, PgfType ty) { return 0; }
+    virtual PgfExpr eimplarg(PgfExpr expr) { return 0; }
+    virtual PgfLiteral lint(size_t size, uintmax_t *val) { return 0; }
+    virtual PgfLiteral lflt(double val) { return 0; }
+    virtual PgfLiteral lstr(PgfText *val) { return 0; }
+
+    virtual PgfType dtyp(size_t n_hypos, PgfTypeHypo *hypos,
+                         PgfText *name,
+                         size_t n_exprs, PgfExpr *exprs)
+    {
+        Type *ty = new(name) Cat;
+        while (n_hypos > 0) {
+            PgfTypeHypo *hypo = &hypos[--n_hypos];
+            ty = new(hypo->bind_type, hypo->cid, (Type*) hypo->type, ty) Pi;
+        }
+        return (PgfType) ty;
+    }
+
+    virtual void free_ref(object x) { }
+};
+
+class PgfTypechecker::Unmarshaller2 : public Unmarshaller1 {
+    PgfMarshaller *m;
+
+public:
+    Unmarshaller2(PgfMarshaller *m) {
+        this->m = m;
+    }
+
+    virtual PgfType dtyp(size_t n_hypos, PgfTypeHypo *hypos,
+                         PgfText *name,
+                         size_t n_exprs, PgfExpr *exprs)
+    {
+        Type *ty = new(name) Cat;
+        while (n_hypos > 0) {
+            PgfTypeHypo *hypo = &hypos[--n_hypos];
+            Type *arg_ty = (Type *) m->match_type(this, hypo->type);
+            ty = new(hypo->bind_type, hypo->cid, arg_ty, ty) Pi;
+        }
+        return (PgfType) ty;
+    }
+
+    virtual void free_ref(object x) { }
+};
+
+PgfType PgfTypechecker::marshall_type(Type *ty, PgfUnmarshaller *u)
 {
-    return u->eabs(btype,name,body);
+    size_t n_hypos = 0;
+    PgfTypeHypo *hypos = 0;
+    for (;;) {
+        Pi *pi = ty->is_pi();
+        if (pi) {
+            hypos = (PgfTypeHypo *) realloc(hypos, n_hypos*sizeof(PgfTypeHypo));
+            PgfTypeHypo *hypo = &hypos[n_hypos++];
+            hypo->bind_type = pi->bind_type;
+            hypo->cid = &pi->var;
+            hypo->type = marshall_type(pi->arg, u);
+            ty = pi->res;
+        }
+        Cat *cat = ty->is_cat();
+        if (cat) {
+            return u->dtyp(n_hypos,hypos,&cat->name,0,NULL);
+        }
+    }
 }
 
-PgfExpr PgfTypechecker::eapp(PgfExpr fun, PgfExpr arg)
-{
-    fun = m->match_expr(this, fun);
+PgfTypechecker::PgfTypechecker(ref<PgfPGF> gr, PgfMarshaller *m, PgfUnmarshaller *u, PgfExn* err) {
+    this->gr   = gr;
+    this->m    = m;
+    this->u    = u;
+    this->err  = err;
+};
 
-    size_t       fun_n_args = n_args;
-    ref<PgfDTyp> fun_type   = type;
-
-    arg = m->match_expr(this, arg);
-    return u->eapp(fun, arg);
+PgfTypechecker::~PgfTypechecker() {
+    while (temps.size() > 0) {
+        Type *ty = temps.back(); temps.pop_back();
+        delete(ty);
+    }
 }
 
-PgfExpr PgfTypechecker::elit(PgfLiteral lit)
-{
-    return u->elit(lit);
+PgfTypechecker::Context::Context(PgfTypechecker *tc, Type *exp_type, PgfBindType bind_type) {
+    this->tc         = tc;
+    this->bind_type  = bind_type;
+    this->exp_type   = exp_type;
+    this->inf_type   = NULL;
 }
 
-PgfExpr PgfTypechecker::emeta(PgfMetaId meta)
+PgfExpr PgfTypechecker::Context::eabs(PgfBindType btype, PgfText *name, PgfExpr body)
 {
-    return u->emeta(meta);
+    if (!checkImplArgument())
+        return 0;
+    return tc->u->eabs(btype,name,body);
 }
 
-PgfExpr PgfTypechecker::efun(PgfText *name)
+PgfExpr PgfTypechecker::Context::eapp(PgfExpr fun, PgfExpr arg)
 {
+    if (!checkImplArgument())
+        return 0;
+
+    Context fun_ctxt(tc);
+    fun = tc->m->match_expr(&fun_ctxt, fun);
+    if (fun == 0)
+        return 0;
+
+repeat:
+    Pi *pi = fun_ctxt.inf_type->is_pi();
+    if (!pi) {
+        tc->type_error("Too many arguments");
+        return 0;
+    }
+
+    Context arg_ctxt(tc,pi->arg,pi->bind_type);
+    PgfExpr new_arg = tc->m->match_expr(&arg_ctxt, arg);
+    if (new_arg == 0) {
+        if (tc->err->type == PGF_EXN_TYPE_ERROR && tc->err->code == 1) {
+            tc->err->type = PGF_EXN_NONE;
+            tc->err->code = 0;
+            tc->err->msg  = NULL;
+            PgfExpr meta = tc->u->emeta(0);
+            PgfExpr impl = tc->u->eimplarg(meta);
+            PgfExpr new_fun = tc->u->eapp(fun, impl);
+            tc->u->free_ref(fun);
+            tc->u->free_ref(impl);
+            tc->u->free_ref(meta);
+            fun = new_fun;
+            fun_ctxt.inf_type = pi->res;
+            goto repeat;
+        }
+        return 0;
+    }
+
+    PgfExpr e = tc->u->eapp(fun, new_arg);
+    free_ref(fun);
+    free_ref(new_arg);
+
+    inf_type = pi->res;
+
+    if (!unifyTypes(&e)) {
+        free_ref(fun);
+        free_ref(arg);
+        return 0;
+    }
+
+    return e;
+}
+
+PgfExpr PgfTypechecker::Context::elit(PgfLiteral lit)
+{
+    if (!checkImplArgument())
+        return 0;
+
+    lit = tc->m->match_lit(this, lit);
+    if (!lit)
+        return 0;
+
+    PgfExpr e = tc->u->elit(lit);  free_ref(lit);
+
+    if (!unifyTypes(&e))
+        return 0;
+
+    return e;
+}
+
+PgfExpr PgfTypechecker::Context::emeta(PgfMetaId meta)
+{
+    if (!checkImplArgument())
+        return 0;
+
+    if (exp_type == NULL)
+        return tc->type_error("Cannot infer the type of a meta variable");
+
+    PgfExpr e = tc->u->emeta(meta);
+
+    inf_type = exp_type;
+
+    if (!unifyTypes(&e))
+        return 0;
+
+    return e;
+}
+
+PgfExpr PgfTypechecker::Context::efun(PgfText *name)
+{
+    if (!checkImplArgument())
+        return 0;
+
     ref<PgfAbsFun> absfun =
-        namespace_lookup(gr->abstract.funs, name);
+        namespace_lookup(tc->gr->abstract.funs, name);
     if (absfun == 0)
-        throw pgf_error("Unknown function");
+        return tc->type_error("Function %s is not defined", name->text);
 
-    type   = absfun->type;
-    n_args = 0;
-    return u->efun(name);
+    Unmarshaller1 tu;
+    inf_type = (Type*) tc->db_m.match_type(&tu, absfun->type.as_object());
+    tc->temps.push_back(inf_type);
+
+    PgfExpr e = tc->u->efun(name);
+
+    if (!unifyTypes(&e)) {
+        tc->u->free_ref(e);
+        return 0;
+    }
+
+    return e;
 }
 
-PgfExpr PgfTypechecker::evar(int index)
+PgfExpr PgfTypechecker::Context::evar(int index)
 {
-    return u->evar(index);
+    if (!checkImplArgument())
+        return 0;
+
+    return tc->u->evar(index);
 }
 
-PgfExpr PgfTypechecker::etyped(PgfExpr expr, PgfType ty)
+PgfExpr PgfTypechecker::Context::etyped(PgfExpr expr, PgfType type)
 {
-    expr = m->match_expr(this, expr);
-    return u->etyped(expr,ty);
+    if (!checkImplArgument())
+        return 0;
+
+    Context type_ctxt(tc);
+    type = tc->m->match_type(&type_ctxt, type);
+    if (type == 0)
+        return 0;
+
+    Unmarshaller2 tu(tc->m);
+    Type *ty = (Type*) tc->m->match_type(&tu,type);
+
+    Context expr_ctxt(tc, ty, PGF_BIND_TYPE_EXPLICIT);
+    expr = tc->m->match_expr(&expr_ctxt, expr);
+    if (expr == 0) {
+        free_ref(type);
+        return 0;
+    }
+    inf_type = expr_ctxt.inf_type;
+
+    PgfExpr e = tc->u->etyped(expr,type);
+
+    free_ref(expr);
+    free_ref(type);
+
+    return e;
 }
 
-PgfExpr PgfTypechecker::eimplarg(PgfExpr expr)
+PgfExpr PgfTypechecker::Context::eimplarg(PgfExpr expr)
 {
-    expr = m->match_expr(this, expr);
-    return u->eimplarg(expr);
+    if (bind_type != PGF_BIND_TYPE_IMPLICIT) {
+        tc->type_error("Unexpected implicit argument");
+        return 0;
+    }
+
+    Context expr_ctxt(tc,exp_type,PGF_BIND_TYPE_EXPLICIT);
+    expr = tc->m->match_expr(&expr_ctxt, expr);
+    if (expr == 0) {
+        return 0;
+    }
+
+    inf_type = expr_ctxt.inf_type;
+
+    PgfExpr e = tc->u->eimplarg(expr);
+
+    free_ref(expr);
+
+    return e;
 }
 
-PgfLiteral PgfTypechecker::lint(size_t size, uintmax_t *v)
+PgfLiteral PgfTypechecker::Context::lint(size_t size, uintmax_t *v)
 {
-    return u->lint(size,v);
+    inf_type = new("Int") Cat;
+    tc->temps.push_back(inf_type);
+    return tc->u->lint(size,v);
 }
 
-PgfLiteral PgfTypechecker::lflt(double v)
+PgfLiteral PgfTypechecker::Context::lflt(double v)
 {
-    return u->lflt(v);
+    inf_type = new("Float") Cat;
+    tc->temps.push_back(inf_type);
+    return tc->u->lflt(v);
 }
 
-PgfLiteral PgfTypechecker::lstr(PgfText *v)
+PgfLiteral PgfTypechecker::Context::lstr(PgfText *v)
 {
-    return u->lstr(v);
+    inf_type = new("String") Cat;
+    tc->temps.push_back(inf_type);
+    return tc->u->lstr(v);
 }
 
-PgfType PgfTypechecker::dtyp(size_t n_hypos, PgfTypeHypo *hypos,
-                             PgfText *cat,
-                             size_t n_exprs, PgfExpr *exprs)
+PgfType PgfTypechecker::Context::dtyp(size_t n_hypos, PgfTypeHypo *hypos,
+                                      PgfText *cat,
+                                      size_t n_exprs, PgfExpr *exprs)
 {
-    return u->dtyp(n_hypos, hypos, cat, n_exprs, exprs);
+    ref<PgfAbsCat> abscat =
+        namespace_lookup(tc->gr->abstract.cats, cat);
+    if (abscat == 0)
+        return tc->type_error("Category %s is not defined", cat->text);
+
+    PgfType ty = 0;
+    PgfTypeHypo *new_hypos = (PgfTypeHypo *)
+        alloca(sizeof(PgfTypeHypo)*n_hypos);
+    size_t n_new_exprs = abscat->context->len;
+    PgfExpr *new_exprs = (PgfExpr *)
+        alloca(sizeof(PgfExpr)*n_new_exprs);
+
+    for (size_t i = 0; i < n_hypos; i++) {
+        new_hypos[i].bind_type = hypos[i].bind_type;
+        new_hypos[i].cid       = hypos[i].cid;
+        new_hypos[i].type      = tc->m->match_type(this, hypos[i].type);
+        if (new_hypos[i].type == 0) {
+            n_hypos = i;
+            n_new_exprs = 0;
+            goto exit;
+        }
+    }
+
+    size_t i, j;
+    for (i = 0, j = 0; i < n_new_exprs && j < n_exprs; i++) {
+        Unmarshaller1 tu;
+        PgfHypo *hypo = vector_elem(abscat->context,i);
+        Type *ty = (Type *) tc->db_m.match_type(&tu,hypo->type.as_object());
+        tc->temps.push_back(ty);
+        Context expr_ctxt(tc,ty,hypo->bind_type);
+        new_exprs[i] = tc->m->match_expr(&expr_ctxt, exprs[j]);
+        if (new_exprs[i] == 0) {
+            if (tc->err->type == PGF_EXN_TYPE_ERROR && tc->err->code == 1) {
+                tc->err->type = PGF_EXN_NONE;
+                tc->err->code = 0;
+                tc->err->msg  = NULL;
+                PgfExpr e1 = tc->u->emeta(0);
+                new_exprs[i] = tc->u->eimplarg(e1);  free_ref(e1);
+            } else {
+                n_new_exprs = i;
+                goto exit;
+            }
+        } else {
+            j++;
+        }
+    }
+
+    if (i < n_new_exprs) {
+        tc->type_error("Too few arguments to category %s - %ld expected but %ld given",
+                       cat->text,
+                       n_new_exprs,
+                       n_exprs);
+        n_new_exprs = n_exprs;
+        goto exit;
+    }
+    if (j < n_exprs) {
+        tc->type_error("Too many arguments to category %s - %ld expected but %ld given",
+                       cat->text,
+                       n_new_exprs,
+                       n_exprs);
+        goto exit;
+    }
+
+    ty = tc->u->dtyp(n_hypos, new_hypos, cat, n_new_exprs, new_exprs);
+
+exit:
+    for (size_t i = 0; i < n_hypos; i++) {
+        free_ref(new_hypos[i].type);
+    }
+    for (size_t i = 0; i < n_new_exprs; i++) {
+        free_ref(new_exprs[i]);
+    }
+    return ty;
 }
 
-void PgfTypechecker::free_ref(object x)
+void PgfTypechecker::Context::free_ref(object x)
 {
-    u->free_ref(x);
+    tc->u->free_ref(x);
+}
+
+bool PgfTypechecker::Context::checkImplArgument()
+{
+    if (bind_type == PGF_BIND_TYPE_IMPLICIT) {
+        tc->err->type = PGF_EXN_TYPE_ERROR;
+        tc->err->code = 1;
+        tc->err->msg  = "Unexpected explicit argument";
+        return false;
+    }
+    return true;
+}
+
+bool PgfTypechecker::unifyTypes(Type *ty1, Type *ty2)
+{
+    Cat *cat1 = ty1->is_cat();
+    Cat *cat2 = ty2->is_cat();
+    if (cat1 && cat2) {
+        if (textcmp(&cat1->name, &cat2->name) != 0) {
+            return type_error("Types %s and %s doesn't match", cat1->name.text, cat2->name.text);
+        }
+        return true;
+    }
+
+    Pi *pi1 = ty1->is_pi();
+    Pi *pi2 = ty2->is_pi();
+    if (pi1 && pi2) {
+        return unifyTypes(pi1->arg, pi2->arg) && unifyTypes(pi1->res, pi2->res);
+    }
+
+    return type_error("Types doesn't match");
+}
+
+bool PgfTypechecker::Context::unifyTypes(PgfExpr *e)
+{
+    if (exp_type == NULL)
+        return true;
+    return tc->unifyTypes(inf_type,exp_type);
+}
+
+bool PgfTypechecker::type_error(const char *fmt, ...)
+{
+    va_list arg_ptr;
+
+    va_start(arg_ptr, fmt);
+    size_t n_bytes = vsnprintf(NULL, 0, fmt, arg_ptr);
+    va_end(arg_ptr);
+
+    char *buffer = (char*) err->msg;
+
+    va_start(arg_ptr, fmt);
+    buffer = (char*) realloc(buffer, n_bytes+1);
+    if (buffer) {
+        vsnprintf(buffer, n_bytes+1, fmt, arg_ptr);
+        err->type = PGF_EXN_TYPE_ERROR;
+        err->code = 0;
+        err->msg  = buffer;
+    }
+    va_end(arg_ptr);
+
+    return false;
+}
+
+PgfType PgfTypechecker::infer_expr(PgfExpr *pe)
+{
+    Context ctxt(this);
+    *pe = m->match_expr(&ctxt, *pe);
+    if (*pe == 0)
+        return 0;
+    return marshall_type(ctxt.inf_type, u);
+}
+
+PgfExpr PgfTypechecker::check_expr(PgfExpr expr, PgfType type)
+{
+    Unmarshaller2 tu(m);
+    Type *ty = (Type*) m->match_type(&tu, type);
+    Context ctxt(this,ty,PGF_BIND_TYPE_EXPLICIT);
+    expr = m->match_expr(&ctxt, expr);
+    return expr;
+}
+
+PgfType PgfTypechecker::check_type(PgfType type)
+{
+    Context ctxt(this);
+    return m->match_type(&ctxt, type);
 }
diff --git a/src/runtime/c/pgf/typechecker.h b/src/runtime/c/pgf/typechecker.h
index 9b5b37413..ff1918fd5 100644
--- a/src/runtime/c/pgf/typechecker.h
+++ b/src/runtime/c/pgf/typechecker.h
@@ -1,35 +1,108 @@
 #ifndef TYPECHECKER_H
 #define TYPECHECKER_H
 
-class PGF_INTERNAL_DECL PgfTypechecker : public PgfUnmarshaller {
+class PGF_INTERNAL_DECL PgfTypechecker {
     ref<PgfPGF> gr;
-    ref<PgfDTyp> type;
-    size_t n_args;
     PgfMarshaller *m;
     PgfUnmarshaller *u;
+    PgfExn* err;
 
-public:
-    PgfTypechecker(ref<PgfPGF> gr, PgfMarshaller *m, PgfUnmarshaller *u) {
-        this->gr = gr;
-        this->m  = m;
-        this->u  = u;
+    class Unmarshaller1;
+    class Unmarshaller2;
+
+    struct Pi;
+    struct Cat;
+
+    struct Type {
+        virtual Pi  *is_pi()  { return NULL; }
+        virtual Cat *is_cat() { return NULL; }
+        virtual ~Type() {}
     };
 
-    virtual PgfExpr eabs(PgfBindType btype, PgfText *name, PgfExpr body);
-    virtual PgfExpr eapp(PgfExpr fun, PgfExpr arg);
-    virtual PgfExpr elit(PgfLiteral lit);
-    virtual PgfExpr emeta(PgfMetaId meta);
-    virtual PgfExpr efun(PgfText *name);
-    virtual PgfExpr evar(int index);
-    virtual PgfExpr etyped(PgfExpr expr, PgfType typ);
-    virtual PgfExpr eimplarg(PgfExpr expr);
-    virtual PgfLiteral lint(size_t size, uintmax_t *v);
-    virtual PgfLiteral lflt(double v);
-    virtual PgfLiteral lstr(PgfText *v);
-    virtual PgfType dtyp(size_t n_hypos, PgfTypeHypo *hypos,
-                         PgfText *cat,
-                         size_t n_exprs, PgfExpr *exprs);
-    virtual void free_ref(object x);
+    struct Pi : Type {
+        PgfBindType bind_type;
+        Type *arg, *res;
+        PgfText var;
+
+        void *operator new(size_t size, PgfBindType bind_type, PgfText *var, Type *arg, Type *res) {
+            Pi *pi = (Pi *) malloc(size+var->size+1);
+            pi->bind_type = bind_type;
+            memcpy(&pi->var, var, sizeof(PgfText)+var->size+1);
+            pi->arg = arg;
+            pi->res = res;
+            return pi;
+        }
+        virtual Pi *is_pi()  { return this; }
+
+        virtual ~Pi() {
+            delete arg;
+            delete res;
+        }
+    };
+
+    struct Cat : Type {
+        PgfText name;
+
+        void *operator new(size_t size, PgfText *name) {
+            Cat *cat = (Cat *) malloc(size+name->size+1);
+            memcpy(&cat->name, name, sizeof(PgfText)+name->size+1);
+            return cat;
+        }
+        void *operator new(size_t size, const char *name) {
+            size_t len = strlen(name);
+            Cat *cat = (Cat *) malloc(size+len+1);
+            cat->name.size = len;
+            memcpy(&cat->name.text, name, len+1);
+            return cat;
+        }
+        virtual Cat *is_cat() { return this; }
+    };
+
+    PgfType marshall_type(Type *ty, PgfUnmarshaller *u);
+    std::vector<Type*> temps;
+
+    bool unifyTypes(Type *ty1, Type *ty2);
+
+    struct Context : public PgfUnmarshaller {
+        PgfTypechecker *tc;
+
+        PgfBindType bind_type;
+        Type *exp_type;
+        Type *inf_type;
+
+        bool checkImplArgument();
+        bool unifyTypes(PgfExpr *e);
+
+    public:
+        Context(PgfTypechecker *tc, Type *exp_type = NULL, PgfBindType bind_type = PGF_BIND_TYPE_EXPLICIT);
+
+        virtual PgfExpr eabs(PgfBindType btype, PgfText *name, PgfExpr body);
+        virtual PgfExpr eapp(PgfExpr fun, PgfExpr arg);
+        virtual PgfExpr elit(PgfLiteral lit);
+        virtual PgfExpr emeta(PgfMetaId meta);
+        virtual PgfExpr efun(PgfText *name);
+        virtual PgfExpr evar(int index);
+        virtual PgfExpr etyped(PgfExpr expr, PgfType typ);
+        virtual PgfExpr eimplarg(PgfExpr expr);
+        virtual PgfLiteral lint(size_t size, uintmax_t *v);
+        virtual PgfLiteral lflt(double v);
+        virtual PgfLiteral lstr(PgfText *v);
+        virtual PgfType dtyp(size_t n_hypos, PgfTypeHypo *hypos,
+                             PgfText *cat,
+                             size_t n_exprs, PgfExpr *exprs);
+        virtual void free_ref(object x);
+    };
+
+    PgfDBMarshaller db_m;
+    bool type_error(const char *fmt, ...) __attribute__ ((format (printf, 2, 3)));
+
+public:
+    PgfTypechecker(ref<PgfPGF> gr, PgfMarshaller *m, PgfUnmarshaller *u, PgfExn* err);
+    ~PgfTypechecker();
+    
+    PgfExpr check_expr(PgfExpr expr, PgfType type);
+    PgfType infer_expr(PgfExpr *pe);
+    PgfType check_type(PgfType type);
 };
 
 #endif
diff --git a/src/runtime/haskell/PGF2.hsc b/src/runtime/haskell/PGF2.hsc
index b33ccba64..3ee193a20 100644
--- a/src/runtime/haskell/PGF2.hsc
+++ b/src/runtime/haskell/PGF2.hsc
@@ -481,7 +481,37 @@ exprProbability p e =
     withPgfExn "exprProbability" (pgf_expr_prob (a_db p) c_revision c_e marshaller)
 
 checkExpr :: PGF -> Expr -> Type -> Either String Expr
-checkExpr = error "TODO: checkExpr"
+checkExpr p e ty =
+  unsafePerformIO $
+  withForeignPtr (a_revision p) $ \c_revision ->
+  bracket (newStablePtr e) freeStablePtr $ \c_e ->
+  bracket (newStablePtr ty) freeStablePtr $ \c_ty ->
+  allocaBytes (#size PgfExn) $ \c_exn -> do
+    c_e <- pgf_check_expr (a_db p) c_revision c_e c_ty marshaller unmarshaller c_exn
+    ex_type <- (#peek PgfExn, type) c_exn :: IO (#type PgfExnType)
+    case ex_type of
+      (#const PGF_EXN_NONE) -> do
+         e  <- deRefStablePtr c_e
+         freeStablePtr c_e
+         return (Right e)
+      (#const PGF_EXN_SYSTEM_ERROR) -> do
+         errno <- (#peek PgfExn, code) c_exn
+         c_msg <- (#peek PgfExn, msg) c_exn
+         mb_fpath <- if c_msg == nullPtr
+                       then return Nothing
+                       else fmap Just (peekCString c_msg)
+         ioError (errnoToIOError "checkExpr" (Errno errno) Nothing mb_fpath)
+      (#const PGF_EXN_PGF_ERROR) -> do
+         c_msg <- (#peek PgfExn, msg) c_exn
+         msg <- peekCString c_msg
+         free c_msg
+         throwIO (PGFError "checkExpr" msg)
+      (#const PGF_EXN_TYPE_ERROR) -> do
+         c_msg <- (#peek PgfExn, msg) c_exn
+         msg <- peekCString c_msg
+         free c_msg
+         return (Left msg)
+      _ -> throwIO (PGFError "checkExpr" "An unidentified error occurred")
 
 -- | Tries to infer the type of an expression. Note that
 -- even if the expression is type correct it is not always
@@ -513,6 +543,11 @@ inferExpr p e =
                        else fmap Just (peekCString c_msg)
          ioError (errnoToIOError "inferExpr" (Errno errno) Nothing mb_fpath)
       (#const PGF_EXN_PGF_ERROR) -> do
+         c_msg <- (#peek PgfExn, msg) c_exn
+         msg <- peekCString c_msg
+         free c_msg
+         throwIO (PGFError "inferExpr" msg)
+      (#const PGF_EXN_TYPE_ERROR) -> do
          c_msg <- (#peek PgfExn, msg) c_exn
          msg <- peekCString c_msg
          free c_msg
@@ -522,7 +557,36 @@ inferExpr p e =
 -- | Check whether a type is consistent with the abstract
 -- syntax of the grammar.
 checkType :: PGF -> Type -> Either String Type
-checkType pgf ty = Right ty
+checkType p ty =
+  unsafePerformIO $
+  withForeignPtr (a_revision p) $ \c_revision ->
+  bracket (newStablePtr ty) freeStablePtr $ \c_ty ->
+  allocaBytes (#size PgfExn) $ \c_exn -> do
+    c_ty <- pgf_check_type (a_db p) c_revision c_ty marshaller unmarshaller c_exn
+    ex_type <- (#peek PgfExn, type) c_exn :: IO (#type PgfExnType)
+    case ex_type of
+      (#const PGF_EXN_NONE) -> do
+         ty <- deRefStablePtr c_ty
+         freeStablePtr c_ty
+         return (Right ty)
+      (#const PGF_EXN_SYSTEM_ERROR) -> do
+         errno <- (#peek PgfExn, code) c_exn
+         c_msg <- (#peek PgfExn, msg) c_exn
+         mb_fpath <- if c_msg == nullPtr
+                       then return Nothing
+                       else fmap Just (peekCString c_msg)
+         ioError (errnoToIOError "checkType" (Errno errno) Nothing mb_fpath)
+      (#const PGF_EXN_PGF_ERROR) -> do
+         c_msg <- (#peek PgfExn, msg) c_exn
+         msg <- peekCString c_msg
+         free c_msg
+         throwIO (PGFError "checkType" msg)
+      (#const PGF_EXN_TYPE_ERROR) -> do
+         c_msg <- (#peek PgfExn, msg) c_exn
+         msg <- peekCString c_msg
+         free c_msg
+         return (Left msg)
+      _ -> throwIO (PGFError "checkType" "An unidentified error occurred")
 
 -- | Check whether a context is consistent with the abstract
 -- syntax of the grammar.
diff --git a/src/runtime/haskell/PGF2/FFI.hsc b/src/runtime/haskell/PGF2/FFI.hsc
index 26244dece..0ef1e6f8f 100644
--- a/src/runtime/haskell/PGF2/FFI.hsc
+++ b/src/runtime/haskell/PGF2/FFI.hsc
@@ -203,11 +203,11 @@ foreign import ccall pgf_concrete_language_code :: Ptr PgfDB -> Ptr Concr -> Ptr
 
 foreign import ccall pgf_expr_prob :: Ptr PgfDB -> Ptr PGF -> StablePtr Expr -> Ptr PgfMarshaller -> Ptr PgfExn -> IO (#type prob_t)
 
-foreign import ccall pgf_check_expr :: Ptr PgfDB -> Ptr PGF -> Ptr (StablePtr Expr) -> StablePtr Type -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO ()
+foreign import ccall pgf_check_expr :: Ptr PgfDB -> Ptr PGF -> StablePtr Expr -> StablePtr Type -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Expr)
 
 foreign import ccall pgf_infer_expr :: Ptr PgfDB -> Ptr PGF -> Ptr (StablePtr Expr) -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Type)
 
-foreign import ccall pgf_check_type :: Ptr PgfDB -> Ptr PGF -> Ptr (StablePtr Type) -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO ()
+foreign import ccall pgf_check_type :: Ptr PgfDB -> Ptr PGF -> StablePtr Type -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Type)
 
 foreign import ccall pgf_generate_random :: Ptr PgfDB -> Ptr PGF -> Ptr (Ptr Concr) -> CSize -> StablePtr Type -> CSize -> Ptr Word64 -> Ptr (#type prob_t) -> Ptr PgfMarshaller -> Ptr PgfUnmarshaller -> Ptr PgfExn -> IO (StablePtr Expr)
 
diff --git a/src/runtime/haskell/pgf2.cabal b/src/runtime/haskell/pgf2.cabal
index 2cd5801a5..147a306ae 100644
--- a/src/runtime/haskell/pgf2.cabal
+++ b/src/runtime/haskell/pgf2.cabal
@@ -73,3 +73,13 @@ test-suite linearization
     HUnit >= 1.6.1.0,
     containers,
     pgf2
+
+test-suite typechecking
+  type: exitcode-stdio-1.0
+  main-is: tests/typechecking.hs
+  default-language: Haskell2010
+  build-depends:
+    base,
+    HUnit >= 1.6.1.0,
+    containers,
+    pgf2
diff --git a/src/runtime/haskell/tests/basic.gf b/src/runtime/haskell/tests/basic.gf
index 229fa320d..e47b24e39 100644
--- a/src/runtime/haskell/tests/basic.gf
+++ b/src/runtime/haskell/tests/basic.gf
@@ -11,6 +11,8 @@ cat P N ;
 fun nat : (x : N) -> P x ;
 fun ind : P z -> ((x:N) -> P x -> P (s x)) -> ((x : N) -> P x) ;
 
+fun imp : ({x},y : N) -> S ;
+
 fun intLit    : Int -> S;
 fun stringLit : String -> S;
 fun floatLit  : Float -> S;
diff --git a/src/runtime/haskell/tests/basic.hs b/src/runtime/haskell/tests/basic.hs
index a71f31e43..199ed8c28 100644
--- a/src/runtime/haskell/tests/basic.hs
+++ b/src/runtime/haskell/tests/basic.hs
@@ -15,9 +15,9 @@ main = do
     grammarTests gr =
       [TestCase (assertEqual "abstract names" "basic" (abstractName gr))
       ,TestCase (assertEqual "abstract categories" ["Float","Int","N","P","S","String"] (categories gr))
-      ,TestCase (assertEqual "abstract functions" ["c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr))
+      ,TestCase (assertEqual "abstract functions" ["c","floatLit","imp","ind","intLit","nat","s","stringLit","z"] (functions gr))
       ,TestCase (assertEqual "abstract functions by cat 1" ["s","z"] (functionsByCat gr "N"))
-      ,TestCase (assertEqual "abstract functions by cat 2" ["c","floatLit","intLit","stringLit"] (functionsByCat gr "S"))
+      ,TestCase (assertEqual "abstract functions by cat 2" ["c","floatLit","imp","intLit","stringLit"] (functionsByCat gr "S"))
       ,TestCase (assertEqual "abstract functions by cat 2" [] (functionsByCat gr "X")) -- no such category
       ,TestCase (assertBool  "type of z" (eqJust (readType "N")    (functionType gr "z")))
       ,TestCase (assertBool  "type of s" (eqJust (readType "N->N") (functionType gr "s")))
diff --git a/src/runtime/haskell/tests/basic.pgf b/src/runtime/haskell/tests/basic.pgf
index 84e8cff6c..3b643d5ef 100644
Binary files a/src/runtime/haskell/tests/basic.pgf and b/src/runtime/haskell/tests/basic.pgf differ
diff --git a/src/runtime/haskell/tests/basic.pmcfg b/src/runtime/haskell/tests/basic.pmcfg
index e6d120b28..7586bfed3 100644
--- a/src/runtime/haskell/tests/basic.pmcfg
+++ b/src/runtime/haskell/tests/basic.pmcfg
@@ -5,13 +5,14 @@ abstract basic {
   cat P N ; -- 0.693147
   cat S ; -- 0.693147
   cat String ; -- 0.693147
-  data c : N -> S ; -- 1.38629
-  fun floatLit : Float -> S ; -- 1.38629
+  data c : N -> S ; -- 1.60944
+  fun floatLit : Float -> S ; -- 1.60944
+  fun imp : ({x} : N) -> (y : N) -> S ; -- 1.60944
   fun ind : P z -> ((x : N) -> P x -> P (s x)) -> (x : N) -> P x ; -- 0.693147
-  fun intLit : Int -> S ; -- 1.38629
+  fun intLit : Int -> S ; -- 1.60944
   fun nat : (x : N) -> P x ; -- 0.693147
   data s : N -> N ; -- 0.693147
-  fun stringLit : String -> S ; -- 1.38629
+  fun stringLit : String -> S ; -- 1.60944
   data z : N ; -- 0.693147
 }
 concrete basic_cnc {
diff --git a/src/runtime/haskell/tests/transactions.hs b/src/runtime/haskell/tests/transactions.hs
index 5a9ea95e8..449991be3 100644
--- a/src/runtime/haskell/tests/transactions.hs
+++ b/src/runtime/haskell/tests/transactions.hs
@@ -41,11 +41,11 @@ main = do
 
   c <- runTestTT $
     TestList $
-      [TestCase (assertEqual "original functions" ["c","floatLit","ind","intLit","nat","s","stringLit","z"] (functions gr1))
+      [TestCase (assertEqual "original functions" ["c","floatLit","imp","ind","intLit","nat","s","stringLit","z"] (functions gr1))
       ,TestCase (assertEqual "existing function" (Left (PGFError "modifyPGF" "A function with that name already exists")) excpt1)
       ,TestCase (assertEqual "existing category" (Left (PGFError "modifyPGF" "A category with that name already exists")) excpt2)
-      ,TestCase (assertEqual "extended functions" ["c","floatLit","foo","ind","intLit","nat","s","stringLit","z"] (functions gr2))
-      ,TestCase (assertEqual "checked-out extended functions" ["c","floatLit","foo","ind","intLit","nat","s","stringLit","z"] (functions gr4))
+      ,TestCase (assertEqual "extended functions" ["c","floatLit","foo","imp","ind","intLit","nat","s","stringLit","z"] (functions gr2))
+      ,TestCase (assertEqual "checked-out extended functions" ["c","floatLit","foo","imp","ind","intLit","nat","s","stringLit","z"] (functions gr4))
       ,TestCase (assertEqual "original categories" ["Float","Int","N","P","S","String"] (categories gr1))
       ,TestCase (assertEqual "extended categories" ["Float","Int","N","P","Q","S","String"] (categories gr2))
       ,TestCase (assertEqual "Q context" (Just [(Explicit,"x",ty)]) (categoryContext gr2 "Q"))
diff --git a/src/runtime/haskell/tests/typechecking.hs b/src/runtime/haskell/tests/typechecking.hs
new file mode 100644
index 000000000..70be26bb5
--- /dev/null
+++ b/src/runtime/haskell/tests/typechecking.hs
@@ -0,0 +1,73 @@
+import Test.HUnit
+import Test.HUnit.Text
+import PGF2
+
+main = do
+  gr <- readPGF "tests/basic.pgf"
+  runTestTTAndExit $
+    TestList $
+      [TestCase (assertInference "infer fun" gr (Right "N") "z")
+      ,TestCase (assertInference "infer app" gr (Right "N") "s z")
+      ,TestCase (assertInference "infer n-args 1" gr (Left "Too many arguments") "z z")
+      ,TestCase (assertInference "infer n-args 2" gr (Left "Too many arguments") "s z z")
+      ,TestCase (assertInference "infer implarg 1" gr (Left "Unexpected implicit argument") "s {z}")
+      ,TestCase (assertInference "infer implarg 2" gr (Right "(y : N) -> S") "imp {z}")  --
+      ,TestCase (assertInference "infer implarg 3" gr (Right "S") "imp {z} z")
+      ,TestCase (assertInference "infer implarg 4" gr (Right "({x},y : N) -> S") "imp")
+      ,TestCase (assertInference' "infer implarg 4" gr (Right ("imp {?} z","S")) "imp z")
+      ,TestCase (assertInference "infer typed 1" gr (Right "N->N") "<s : N->N>")
+      ,TestCase (assertInference "infer typed 2" gr (Left "Types doesn't match") "<s : N>")
+      ,TestCase (assertInference "infer typed 3" gr (Left "Too many arguments to category N - 0 expected but 1 given") "<s : N z>")
+      ,TestCase (assertInference "infer hoas 1" gr (Left "Types doesn't match") "s s")
+      ,TestCase (assertInference "infer literal 1" gr (Right "Int") "0")
+      ,TestCase (assertInference "infer literal 2" gr (Right "Float") "3.14")
+      ,TestCase (assertInference "infer literal 3" gr (Right "String") "\"abc\"")
+      ,TestCase (assertInference "infer meta 1" gr (Left "Cannot infer the type of a meta variable") "?")
+      ,TestCase (assertInference "infer meta 2" gr (Right "N->N") "<? : N->N>")
+      ,TestCase (assertChecking "check fun" gr (Right "s") "s" "N->N")
+      ,TestCase (assertChecking "check fun" gr (Right "s z") "s z" "N")
+      ,TestCase (assertChecking "check fun" gr (Left "Types doesn't match") "s z" "N->N")
+      ,TestCase (assertType "check type 1" gr (Right "N -> N") "N -> N")
+      ,TestCase (assertType "check type 2" gr (Left "Category s is not defined") "s")
+      ,TestCase (assertType "check type 3" gr (Left "Too many arguments to category N - 0 expected but 1 given") "N z")
+      ,TestCase (assertType "check type 4" gr (Left "Too few arguments to category P - 1 expected but 0 given") "P")
+      ,TestCase (assertType "check type 5" gr (Right "P z") "P z")
+      ,TestCase (assertType "check type 6" gr (Left "Types doesn't match") "P s")
+      ,TestCase (assertType "check type 7" gr (Left "Unexpected implicit argument") "P {z}")
+      ]
+
+assertInference name gr (Left msg) e =
+  case readExpr e of
+    Just e -> assertEqual name (Left msg) (inferExpr gr e)
+    _       -> error "Reading the expression failed"
+assertInference name gr (Right ty) e =
+  case (readType ty, readExpr e) of
+    (Just ty,Just e) -> assertEqual name (Right (e,ty)) (inferExpr gr e)
+    _                -> error "Reading the type/expression failed"
+
+assertInference' name gr (Left msg) e =
+  case readExpr e of
+    Just e -> assertEqual name (Left msg) (inferExpr gr e)
+    _       -> error "Reading the expression failed"
+assertInference' name gr (Right (e1,ty)) e0 =
+  case (readExpr e1, readType ty, readExpr e0) of
+    (Just e1,Just ty,Just e0) -> assertEqual name (Right (e1,ty)) (inferExpr gr e0)
+    _                         -> error "Reading the type/expression failed"
+
+assertChecking name gr (Left msg) e ty =
+  case (readExpr e, readType ty) of
+    (Just e,Just ty) -> assertEqual name (Left msg) (checkExpr gr e ty)
+    _                -> error "Reading the expression failed"
+assertChecking name gr (Right e1) e ty =
+  case (readExpr e1, readExpr e, readType ty) of
+    (Just e1,Just e,Just ty) -> assertEqual name (Right e1) (checkExpr gr e ty)
+    _                        -> error "Reading the type/expression failed"
+
+assertType name gr (Left msg) ty =
+  case readType ty of
+    Just ty -> assertEqual name (Left msg) (checkType gr ty)
+    _       -> error "Reading the type failed"
+assertType name gr (Right ty) ty0 =
+  case (readType ty, readType ty0) of
+    (Just ty,Just ty0) -> assertEqual name (Right ty) (checkType gr ty0)
+    _                  -> error "Reading the type failed"