fix(kernel/normalizer): equality between semantic attachments

Given a heterogenous equality:  a == b
The normalizer will only reduce it if a and b are objects of the same kind.
Now, 1 == true is not reduced to false anymore.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

doc/lean/expr.md

@@ -69,18 +69,17 @@ eval 1 == 2
 eval 2 == 2
 ```
 
-Since we can compare elements of different types, the following expression is type correct and evaluates to `false`.
+Since we can compare elements of different types, the following
+expression is type correct, but Lean normalizer/evaluator will *not*
+reduce it.
 
 ```lean
-eval 1 == true
+eval 2 == true
 ```
 
-This is consistent with the set theoretic semantics used in Lean, where the interpretation of all expressions are sets.
-The interpretation of heterogeneous equality is just set equality in the Lean seamtics.
-
 We strongly discourage users from directly using heterogeneous equality. The main problem is that it is very easy to
-write expressions that are false like the one above. The expression `t = s` is a homogeneous equality.
-It expects `t` and `s` to have the same type. Thus, the expression `1 = true` is type incorrect in Lean.
+write nonsensical expressions like the one above. The expression `t = s` is a homogeneous equality.
+It expects `t` and `s` to have the same type. Thus, the expression `2 = true` is type incorrect in Lean.
 The symbol `=` is just notation. Internally, homogeneous equality is defined as:
 
 ```

src/kernel/normalizer.cpp

@@ -312,7 +312,7 @@ class normalizer::imp {
         case expr_kind::Eq: {
             expr new_lhs = normalize(eq_lhs(a), s, k);
             expr new_rhs = normalize(eq_rhs(a), s, k);
-            if (is_value(new_lhs) && is_value(new_rhs) && !is_closure(new_lhs) && !is_closure(new_rhs)) {
+            if (is_value(new_lhs) && is_value(new_rhs) && !is_closure(new_lhs) && !is_closure(new_rhs) && typeid(to_value(new_lhs)) == typeid(to_value(new_rhs))) {
                 r = mk_bool_value(new_lhs == new_rhs);
             } else {
                 r = mk_eq(new_lhs, new_rhs);

tests/lean/eq4.lean

@@ -0,0 +1,8 @@
+import Int
+eval 1 == true
+eval 1 == 1.0
+eval 1 == nat_to_int 1
+eval true == 1.0
+eval Nat::add == 1
+eval Nat::add == Nat::mul
+eval Int::add == Int::mul

tests/lean/eq4.lean.expected.out

@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'Int'
+1 == ⊤
+1 == 1
+1 == 1
+⊤ == 1
+Nat::add == 1
+Nat::add == Nat::mul
+Int::add == Int::mul