diff --git a/src/binding.c b/src/binding.c
index 9fc23c2..b9c9c9c 100644
--- a/src/binding.c
+++ b/src/binding.c
@@ -7,6 +7,7 @@
 #include "binding.h"
 #include "warshall.h"
 #include "memory.h"
+#include "debug.h"
 
 /*
  * Idea is the ev_from *has to* precede the ev_to
@@ -203,7 +204,13 @@ binding_add (int run_from, int ev_from, int run_to, int ev_to)
   Binding b;
 
   b = binding_create (run_from, ev_from, run_to, ev_to);
-  eprintf ("Adding binding (%i,%i) --->> (%i,%i)\n",run_from, ev_from, run_to, ev_to);
+#ifdef DEBUG
+  if (DEBUGL (5))
+    {
+      eprintf ("Adding binding (%i,%i) --->> (%i,%i)\n", run_from, ev_from,
+	       run_to, ev_to);
+    }
+#endif
   sys->bindings = list_insert (sys->bindings, b);
 
   /*
diff --git a/src/compiler.c b/src/compiler.c
index aa8840d..fd3fbee 100644
--- a/src/compiler.c
+++ b/src/compiler.c
@@ -701,8 +701,11 @@ protocolCompile (Symbol prots, Tac tc, Tac tcroles)
     {
       if (sys->engine == ARACHNE_ENGINE)
 	{
-	  pr->rolenames =
-	    termlistAppend (pr->rolenames, levelVar (tcroles->t1.sym));
+	  Term rolename;
+
+	  rolename = levelVar (tcroles->t1.sym);
+	  rolename->stype = termlistAdd (NULL, TERM_Agent);
+	  pr->rolenames = termlistAppend (pr->rolenames, rolename);
 	}
       else
 	{
diff --git a/src/mgu.c b/src/mgu.c
index 4af4332..bcdbc12 100644
--- a/src/mgu.c
+++ b/src/mgu.c
@@ -14,6 +14,85 @@
    New version yields a termlist with substituted variables, which can later be reset to NULL.
 */
 
+//! Global constant. If true, typed checking
+int welltyped = 1;
+
+void
+showSubst (Term t)
+{
+#ifdef DEBUG
+  if (!DEBUGL (5))
+    return;
+
+  indent ();
+  printf ("Substituting ");
+  termPrint (t);
+  printf (", typed ");
+  termlistPrint (t->stype);
+  if (realTermLeaf (t->subst))
+    {
+      printf ("->");
+      termlistPrint (t->subst->stype);
+    }
+  else
+    {
+      printf (", composite term");
+    }
+  if (t->type != VARIABLE)
+    {
+      printf (" (bound roleconstant)");
+    }
+  printf ("\n");
+#endif
+}
+
+//! See if a substitution is valid
+__inline__ int
+goodsubst (Term tvar, Term tsubst)
+{
+  if (tvar->stype == NULL || (!welltyped))
+    {
+      return 1;
+    }
+  else
+    {
+      /**
+       * Check if each type of the substitution is allowed in the variable
+       */
+      if (!realTermLeaf (tsubst))
+	{
+	  // Typed var cannot match with non-leaf
+	  return 0;
+	}
+      else
+	{
+	  // It's a leaf, but what type?
+	  if (termlistContained (tvar->stype, tsubst->stype))
+	    {
+	      return 1;
+	    }
+	  else
+	    {
+#ifdef DEBUG
+	      if (DEBUGL (5))
+		{
+		  eprintf ("Substitution fails on ");
+		  termPrint (tvar);
+		  eprintf (" -/-> ");
+		  termPrint (tsubst);
+		  eprintf (", because type: \n");
+		  termlistPrint (tvar->stype);
+		  eprintf (" does not contain ");
+		  termlistPrint (tsubst->stype);
+		  eprintf ("\n");
+		}
+#endif
+	      return 0;
+	    }
+	}
+    }
+}
+
 //! Undo all substitutions in a list of variables.
 /**
  * The termlist should contain only variables.
@@ -43,34 +122,6 @@ termMguTerm (Term t1, Term t2)
   if (t1 == t2)
     return NULL;
 
-#ifdef DEBUG
-  void showSubst (Term t)
-  {
-    if (!DEBUGL (5))
-      return;
-
-    indent ();
-    printf ("Substituting ");
-    termPrint (t);
-    printf (", typed ");
-    termlistPrint (t->stype);
-    if (realTermLeaf (t->subst))
-      {
-	printf ("->");
-	termlistPrint (t->subst->stype);
-      }
-    else
-      {
-	printf (", composite term");
-      }
-    if (t->type != VARIABLE)
-      {
-	printf (" (bound roleconstant)");
-      }
-    printf ("\n");
-  }
-#endif
-
   if (!(hasTermVariable (t1) || hasTermVariable (t2)))
     {
       if (isTermEqual (t1, t2))
@@ -86,7 +137,7 @@ termMguTerm (Term t1, Term t2)
   /* symmetrical tests for single variable */
   if (realTermVariable (t1))
     {
-      if (termOccurs (t2, t1))
+      if (termOccurs (t2, t1) || !goodsubst (t1, t2))
 	return MGUFAIL;
       else
 	{
@@ -99,7 +150,7 @@ termMguTerm (Term t1, Term t2)
     }
   if (realTermVariable (t2))
     {
-      if (termOccurs (t1, t2))
+      if (termOccurs (t1, t2) || !goodsubst (t2, t1))
 	return MGUFAIL;
       else
 	{
@@ -265,4 +316,3 @@ termMguSubTerm (Term t1, Term t2, int (*iterator) (),
     }
   return flag;
 }
-
diff --git a/src/system.c b/src/system.c
index ba7f622..f71f14f 100644
--- a/src/system.c
+++ b/src/system.c
@@ -597,6 +597,7 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	      // Make new var for this run
 	      newt = makeTermType (VARIABLE, newt->left.symb, rid);
 	      artefacts = termlistAdd (artefacts, newt);
+	      newt->stype = oldt->stype;
 	      // Copy substitution
 	      newt->subst = oldt->subst;
 	      // Remove any old substitution! It is now propagated!
@@ -604,7 +605,9 @@ roleInstance (const System sys, const Protocol protocol, const Role role,
 	    }
 	  // Add to agent list, possibly
 	  if (inTermlist (protocol->rolenames, oldt))
-	    runs[rid].agents = termlistAdd (runs[rid].agents, newt);
+	    {
+	      runs[rid].agents = termlistAdd (runs[rid].agents, newt);
+	    }
 	  fromlist = termlistAdd (fromlist, oldt);
 	  tolist = termlistAdd (tolist, newt);
 
diff --git a/src/term.c b/src/term.c
index 2520220..7928e83 100644
--- a/src/term.c
+++ b/src/term.c
@@ -297,7 +297,7 @@ termPrint (Term term)
       return;
     }
 #ifdef DEBUG
-  if (!DEBUGL (1))
+  if (!DEBUGL (4))
     {
       term = deVar (term);
     }