hack to fix alpha equivalence

thorin/check.cpp

@@ -14,7 +14,7 @@ const Def* infer_type_level(World& world, Defs defs) {
         } else if (auto type = def->type()->isa<Type>()) {
             level = std::max(level, as_lit(type->level()));
         } else {
-            err(def->loc(), "'{}' used as a type but is in fact a term", def);
+            err(def->loc(), "'{}' : '{}' used as a type but is in fact a term", def, def->type());
         }
     }
     return world.type(world.lit_univ(level));

thorin/error.cpp

@@ -1,5 +1,9 @@
 #include "thorin/error.h"
 
+#include <cstdio>
+
+#include <sstream>
+
 #include "thorin/lam.h"
 
 #include "thorin/util/print.h"
@@ -28,6 +32,16 @@ void ErrorHandler::index_out_of_range(const Def* arity, nat_t index, const Def*
 
 void ErrorHandler::ill_typed_app(const Def* callee, const Def* arg, const Def* dbg) {
     Debug d(dbg ? dbg : arg->dbg());
+    // TODO: remove hack
+    // hack to at least accept cases that are syntactically equal
+    auto dom_type = callee->type()->as<Pi>()->dom();
+    auto arg_type = arg->type();
+    std::stringstream dom_type_str;
+    std::stringstream arg_type_str;
+    dom_type_str << dom_type;
+    arg_type_str << arg_type;
+    if (dom_type_str.str() == arg_type_str.str()) return;
+    // original error
     err(d.loc, "cannot pass argument \n  '{}' of type \n  '{}' to \n  '{}' of domain \n  '{}'", arg, arg->type(),
         callee, callee->type()->as<Pi>()->dom());
 }