Improve error message for type checking applications (#101)

Fixes #97.
cvc5 · Dec 4, 2024 · 5c9f7cc · 5c9f7cc
1 parent bf71098
commit 5c9f7cc
Showing 1 changed file with 21 additions and 5 deletions.
diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -447,11 +447,27 @@ Expr TypeChecker::getTypeAppInternal(std::vector<ExprValue*>& children,
     {
       if (out)
       {
-        (*out) << "Unexpected argument type " << i << " of " << Expr(hd)
-              << std::endl;
-        (*out) << "  LHS " << evaluate(hdtypes[i], ctx) << ", from "
-              << Expr(hdtypes[i]) << std::endl;
-        (*out) << "  RHS " << Expr(ctypes[i]) << std::endl;
+        ExprValue* hdto = hdtypes[i];
+        if (hdtypes[i]->getKind() == Kind::QUOTE_TYPE)
+        {
+          (*out) << "Unexpected child #" << i << std::endl;
+          (*out) << "  Term: " << Expr(children[i + 1]) << std::endl;
+          (*out) << "  Expected pattern: ";
+          hdto = hdto->d_children[0];
+        }
+        else
+        {
+          (*out) << "Unexpected type of child #" << i << std::endl;
+          (*out) << "  Term: " << Expr(children[i + 1]) << std::endl;
+          (*out) << "  Has type: " << Expr(ctypes[i]) << std::endl;
+          (*out) << "  Expected type: ";
+        }
+        (*out) << Expr(hdt);
+        if (hdto != hdt)
+        {
+          (*out) << ", from " << Expr(hdto);
+        }
+        (*out) << std::endl;
         (*out) << "  Context " << ctx << std::endl;
       }
       return d_null;