Minimized from an issue originally reported on Zulip. Explicit coercion arrows seem to badly interact with the infix% term elaborator, causing nonassignable metavariables to be created which cause unification to go on a wild goose chase of definition unfolding:
def dontUnfoldMe (x : Int) : Nat → List Bool → Nat
| 0, _ => 0
| n+1, l => dontUnfoldMe x n (true::l) + dontUnfoldMe x n (false::l)
theorem dontUnfoldMe_eq (x) : ∀ n l, dontUnfoldMe x n l = 0
| 0, _ => rfl
| n+1, l => by rw [dontUnfoldMe, dontUnfoldMe_eq x n, dontUnfoldMe_eq x n]
example (a : Int) (n : Nat) : dontUnfoldMe (a * n) 14 [] = 0 :=
dontUnfoldMe_eq (a * n) 14 [] -- fast
example (a : Int) (n : Nat) : dontUnfoldMe (a * n) 14 [] = 0 :=
dontUnfoldMe_eq (a * ↑n) 14 [] -- slow
Here dontUnfoldMe is written such that it exponentially blows up if you unfold it. The Meta.isDefEq trace looks like this:
[] 💥 dontUnfoldMe (a * ?m.1656) 14 [] =?= dontUnfoldMe (a * Int.ofNat n) 14 [] ▼
[] ❌ a * ?m.1656 =?= a * Int.ofNat n ▼
[] ✅ a =?= a
[] ❌ ?m.1656 =?= Int.ofNat n ▼
[] ?m.1656 [nonassignable] =?= Int.ofNat n [nonassignable]
[] ❌ instHMul.1 a ?m.1656 =?= instHMul.1 a (Int.ofNat n) ▼
[] ❌ Mul.mul a ?m.1656 =?= Mul.mul a (Int.ofNat n) ▼
[] ✅ a =?= a
[] ❌ ?m.1656 =?= Int.ofNat n ▼
[] ?m.1656 [nonassignable] =?= Int.ofNat n [nonassignable]
[] ❌ Int.instMulInt.1 a ?m.1656 =?= Int.instMulInt.1 a (Int.ofNat n) ▼
[] ❌ Int.mul a ?m.1656 =?= Int.mul a (Int.ofNat n) ▶
[] 💥 dontUnfoldMe (a * ?m.1656) 13 [true] +
dontUnfoldMe (a * ?m.1656) 13
[false] =?= dontUnfoldMe (a * Int.ofNat n) 13 [true] + dontUnfoldMe (a * Int.ofNat n) 13 [false] ▶
Minimized from an issue originally reported on Zulip. Explicit coercion arrows seem to badly interact with the
infix%term elaborator, causing nonassignable metavariables to be created which cause unification to go on a wild goose chase of definition unfolding:Here
dontUnfoldMeis written such that it exponentially blows up if you unfold it. TheMeta.isDefEqtrace looks like this: