More

src/kind.cpp

@@ -119,6 +119,7 @@ std::string kindToTerm(Kind k)
     case Kind::LAMBDA: ss << "lambda"; break;
     case Kind::PROGRAM: ss << "program"; break;
     case Kind::AS: ss << "eo::as"; break;
+    case Kind::AS_RETURN: ss << "as"; break;
     case Kind::PARAMETERIZED: ss << "eo::_"; break;
     // operations on literals
     default:

src/state.cpp

@@ -925,12 +925,13 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
       Trace("overload") << "...type arg for ambiguous constructor" << std::endl;
       return mkExpr(Kind::APPLY_OPAQUE, {children[0], children[1]});
     }
-    // note we don't support other uses of `as` for symbol disambiguation yet
+    // note we don't support other uses of `as` for symbol disambiguation yet,
+    // we fallthrough and construct the bogus term of kind AS_RETURN.
   }
   else if (k==Kind::AS)
   {
-    // if it has 2 children, process it, otherwise we make the bogus term
-    // below
+    // if it has 2 children, process it, otherwise we make the bogus term of
+    // kind AS below
     if (vchildren.size()==2)
     {
       Trace("overload") << "process eo::as " << children[0] << " " << children[1] << std::endl;

src/type_checker.cpp

@@ -298,11 +298,12 @@ Expr TypeChecker::getTypeInternal(ExprValue* e, std::ostream* out)
     }
       break;
     case Kind::AS:
+    case Kind::AS_RETURN:
     {
       // constructing an application of AS means the type was incorrect.
       if (out)
       {
-        (*out) << "Encountered bad type for eo::as";
+        (*out) << "Encountered bad type for " << kindToTerm(k);
       }
       return d_null;
     }