Offset unification unifies non-defeq terms

[gebner]

Description

First reported at leanprover-community/mathlib3#9805 as a bug in the (mathlib) convert tactic. In mathlib we use an Additive type tag that turns e.g. a multiplicative group into an additive group by defining + as * and 0 as 1, etc. This is very useful to reuse theorems from multiplicative structures for additive ones.

It turns out that rfl is accepted by the elaborator as a proof for (0 : Nat) = (0 : Additive Nat) (which is defeq to 0 = 1 and should not be provable). The incorrect proof is of course caught by the kernel.

The root cause for this issue seems to be the offset unification module, which evaluates arithmetic expressions like 3+3 without checking that the type-class instances are the expected ones. (That is, isDefEq normalZero additiveZero returns true even though they are not defeq.)

Steps to Reproduce

def Additive (α : Type) := α

instance [OfNat α 1] : OfNat (Additive α) (nat_lit 0) := ⟨(1 : α)⟩

example : (0 : Nat) = (0 : Additive Nat) := rfl

Expected behavior: A type error should be produced when elaborating rfl.

Actual behavior: The term elaborates and produces a type-incorrect term, which is then caught by the kernel.

Versions

Nightly from Oct 30.