Improvements to error messages (#96)

Fixes #94. Fixes
#95.

Error on #94 is now:
```
Error: /space/ajreynol/ethos/tc-fail.eo:11.54: Type checking application failed when applying la_generic
Children: [(! 1 :decimal), (! 1 :decimal)]
Message: Incorrect arity for la_generic, which expects 1 arguments and 0 premises but 2 arguments and 0 premises were provided
```
Error on #95 is now:
```
Error: /space/ajreynol/ethos/tc-fail2.eo:6.3: Failed to bind symbol rule, since the symbol has already been defined

src/expr_parser.cpp

@@ -1338,7 +1338,8 @@ void ExprParser::bind(const std::string& name, Expr& e)
   if (!d_state.bind(name, e))
   {
     std::stringstream ss;
-    ss << "Failed to bind symbol " << name;
+    ss << "Failed to bind symbol " << name
+       << ", since the symbol has already been defined";
     d_lex.parseError(ss.str());
   }
 }
@@ -1376,8 +1377,10 @@ Expr ExprParser::typeCheckApp(std::vector<Expr>& children)
     std::stringstream ss;
     d_state.getTypeChecker().getTypeApp(children, &ss);
     std::stringstream msg;
-    msg << "Type checking application failed:" << std::endl;
-    msg << "Children: " << children << std::endl;
+    msg << "Type checking application failed when applying " << children[0]
+        << std::endl;
+    msg << "Children: "
+        << std::vector<Expr>(children.begin() + 1, children.end()) << std::endl;
     msg << "Message: " << ss.str() << std::endl;
     d_lex.parseError(msg.str());
   }

src/type_checker.cpp

@@ -369,9 +369,34 @@ Expr TypeChecker::getTypeAppInternal(std::vector<ExprValue*>& children,
     // incorrect arity
     if (out)
     {
-      (*out) << "Incorrect arity for " << Expr(hd)
-             << ", #argTypes=" << hdtypes.size()
-             << " #children=" << children.size();
+      (*out) << "Incorrect arity for " << Expr(hd);
+      if (hdtypes[hdtypes.size() - 1]->getKind() == Kind::PROOF_TYPE)
+      {
+        // proof rule can give more information, partioned into args/premises
+        size_t npIndex1 = hdtypes.size() - 1;
+        while (npIndex1 > 0
+               && hdtypes[npIndex1 - 1]->getKind() == Kind::PROOF_TYPE)
+        {
+          npIndex1--;
+        }
+        size_t npIndex2 = children.size() - 1;
+        while (npIndex2 > 0
+               && d_state.lookupType(children[npIndex2 - 1])->getKind()
+                      == Kind::PROOF_TYPE)
+        {
+          npIndex2--;
+        }
+        (*out) << ", which expects " << npIndex1 << " arguments and "
+               << (hdtypes.size() - 1 - npIndex1) << " premises but "
+               << npIndex2 << " arguments and "
+               << (children.size() - 1 - npIndex2) << " premises were provided";
+      }
+      else
+      {
+        (*out) << ", which expects " << (hdtypes.size() - 1)
+               << " arguments but " << (children.size() - 1)
+               << " were provided";
+      }
     }
     return d_null;
   }