minor fix, and better output for type errors

2 files changed, 6 insertions, 3 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 7376b0080..b9047307d 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -209,8 +209,9 @@ bool TypeNode::isInstantiatedDatatype() const {
   }
   const Datatype& dt = (*this)[0].getConst<Datatype>();
   unsigned n = dt.getNumParameters();
+  Assert(n < getNumChildren());
   for(unsigned i = 0; i < n; ++i) {
-    if(TypeNode::fromType(dt.getParameter(i)) == (*this)[n + 1]) {
+    if(TypeNode::fromType(dt.getParameter(i)) == (*this)[i + 1]) {
       return false;
     }
   }
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index cffc95ab2..f343848d8 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -82,8 +82,10 @@ class EqualityTypeRule {
       if ( lhsType != rhsType ) {
         std::stringstream ss;
         ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage));
-        ss << "Types do not match in equation ";
-        ss << "[" << lhsType << "<>" << rhsType << "]";
+        ss << "Types do not match in equation:" << std::endl;
+        ss << "Equation: " << n << std::endl;
+        ss << "Type 1: " << lhsType << std::endl;
+        ss << "Type 2: " << rhsType << std::endl;
 
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }