fix issue #74

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:

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)
 

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>)

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>