diff --git a/proof_checker.py b/proof_checker.py
index 9934d18..a900ef4 100644
--- a/proof_checker.py
+++ b/proof_checker.py
@@ -1958,6 +1958,9 @@ def type_synth_term(term, env, recfun, subterms):
       lhs = type_synth_term(args[0], env, recfun, subterms)
       rhs = type_check_term(args[1], lhs.typeof, env, recfun, subterms)
       ty = BoolType(loc)
+      if lhs.typeof != rhs.typeof:
+          error(loc, 'expected arguments of equality to have the same type, but\n' \
+                + '\t' + str(lhs.typeof) + ' ≠ ' + str(rhs.typeof))
       ret = Call(loc, ty, Var(loc2, ty2, name, rs), [lhs, rhs])
         
     case Call(loc, _, Var(loc2, ty2, name, rs), args) if name == recfun:
diff --git a/test-deduce.py b/test-deduce.py
index b9e160c..713711a 100644
--- a/test-deduce.py
+++ b/test-deduce.py
@@ -124,7 +124,7 @@ def test_deduce_errors(deduce_call, path):
             if os.path.isfile(path + file):
                 if file[-3:] == '.pf':
                     if not os.path.isfile(path + file + '.err'):
-                        print("Couldn't find an expected error for", path)
+                        print("Couldn't find an expected error for", path + file)
                         print("Did you mean to generate it? If so, use generate_deduce_errors")
                         exit(1)
                     
diff --git a/test/should-error/equality.pf b/test/should-error/equality.pf
new file mode 100644
index 0000000..3131370
--- /dev/null
+++ b/test/should-error/equality.pf
@@ -0,0 +1,9 @@
+union List<T> {
+  empty
+  node(T, List<T>)
+}
+
+union A { a }
+union B { b }
+
+assert not (@[]<A> = @[]<B>)
diff --git a/test/should-error/equality.pf.err b/test/should-error/equality.pf.err
new file mode 100644
index 0000000..4b0860d
--- /dev/null
+++ b/test/should-error/equality.pf.err
@@ -0,0 +1,2 @@
+./test/should-error/equality.pf:9.13-9.28: expected arguments of equality to have the same type, but
+	List<A> ≠ List<B>