fix(library/type_context): do not unify (1 : ℕ) with (1 : ℤ) (#376)

Fixes #362.

src/library/type_context.cpp

@@ -3102,8 +3102,6 @@ lbool type_context_old::try_numeral_eq_numeral(expr const & t, expr const & s) {
     if (!n1) return l_undef;
     optional<mpz> n2 = eval_num(s);
     if (!n2) return l_undef;
-    if (!is_nat_type(whnf(infer(t))))
-        return l_undef;
     if (*n1 != *n2)
         return l_false;
     else if (to_small_num(t) && to_small_num(s))
@@ -3117,6 +3115,9 @@ lbool type_context_old::try_nat_offset_cnstrs(expr const & t, expr const & s) {
     /* We should not use this feature when transparency_mode is none.
        See issue #1295 */
     if (m_transparency_mode == transparency_mode::None) return l_undef;
+    // Only special-case natural numbers, see https://github.com/leanprover-community/lean/issues/362
+    if (!is_nat_type(whnf(infer(t))) || !is_nat_type(whnf(infer(s))))
+        return l_undef;
     lbool r;
     r = try_offset_eq_offset(t, s);
     if (r != l_undef) return r;

tests/lean/run/362c.lean

@@ -0,0 +1,2 @@
+open tactic
+#eval success_if_fail $ unify `(1 : ℕ) `(1 : ℤ)

tests/lean/widget/widget4.input.expected.out

@@ -1,3 +1,3 @@
 {"msgs":[{"caption":"","file_name":"widget4.lean","pos_col":0,"pos_line":3,"severity":"information","text":"(widget)","widget":{"column":0,"id":3,"line":3}}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
-{"response":"ok","seq_num":1,"widget":{"column":0,"html":{"c":[{"a":{"className":"list pl0"},"c":[{"a":{"className":"lh-copy"},"c":[{"a":{"className":"goal-goals"},"c":["expected type:"],"t":"strong"}],"t":"li"},{"a":{"className":"lh-copy"},"c":[{"c":[{"a":{"className":"list pl0 font-code","key":"419198192"},"c":[{"a":{"key":"_mlocal._fresh.10.70"},"c":[{"a":{"className":"goal-vdash b"},"c":["⊢ "],"t":"span"},{"c":[{"c":[{"a":{"className":"expr","key":"695702567"},"c":[{"a":{"className":"expr-boundary","key":"[]"},"c":[{"a":{"key":"true"},"c":["true"],"e":{"onClick":{"h":2,"r":[6,5,4,3]},"onMouseEnter":{"h":1,"r":[6,5,4,3]}},"t":"span"}],"t":"span"}],"e":{"onMouseLeave":{"h":0,"r":[6,5,4,3]}},"t":"span"}]}]}],"t":"li"}],"t":"ul"}]}],"t":"li"}],"t":"ul"}]},"id":3,"line":3}}
+{"response":"ok","seq_num":1,"widget":{"column":0,"html":{"c":[{"a":{"className":"list pl0"},"c":[{"a":{"className":"lh-copy"},"c":[{"a":{"className":"goal-goals"},"c":["expected type:"],"t":"strong"}],"t":"li"},{"a":{"className":"lh-copy"},"c":[{"c":[{"a":{"className":"list pl0 font-code","key":"417262892"},"c":[{"a":{"key":"_mlocal._fresh.10.100"},"c":[{"a":{"className":"goal-vdash b"},"c":["⊢ "],"t":"span"},{"c":[{"c":[{"a":{"className":"expr","key":"695702567"},"c":[{"a":{"className":"expr-boundary","key":"[]"},"c":[{"a":{"key":"true"},"c":["true"],"e":{"onClick":{"h":2,"r":[6,5,4,3]},"onMouseEnter":{"h":1,"r":[6,5,4,3]}},"t":"span"}],"t":"span"}],"e":{"onMouseLeave":{"h":0,"r":[6,5,4,3]}},"t":"span"}]}]}],"t":"li"}],"t":"ul"}]}],"t":"li"}],"t":"ul"}]},"id":3,"line":3}}