abel_nf: PANIC at Lean.isLevelMVarAssignable Lean.MetavarContext:412:14: unknown universe metavariable

[eric-wieser]

import Mathlib.Tactic

theorem foo (n : ℕ) (h₀ : 0 < n) :
    (∏ x ∈ Finset.Ico 1 (n + 1), x * (x + 1) : ℤ) ∣
      ∏ x ∈ Finset.Ico 1 (n + 1), 1 := by
  induction id h₀ with
  | refl => sorry
  | @step a b c => abel_nf at c

gives

PANIC at Lean.isLevelMVarAssignable Lean.MetavarContext:412:14: unknown universe metavariable

[digama0]

minimized

import Mathlib.Tactic.Abel

axiom F (s : Nat) (f : Nat → Nat) : Nat
axiom G (a b : Nat) : Nat
@[congr] axiom F_congr {s₁ s₂ : Nat} {f : Nat → Nat} (h : s₁ = s₂) : F s₁ f = F s₂ f 

-- invalid occurrence of universe level 'u_1' at '_example'
example (n : ℕ) : F (G 1 (n + 1)) (fun x => x) ≤ F (G 1 (n + 1)) id := by
  abel_nf
  sorry

This is minimal under lots of surprising things, for example G 0 and G 2 do not give the error, only G 1 does.

[digama0]

The bug seems to be somewhere in simp, it's rolling back the universe metavariable context after a custom pre method assigns some metavariables and returns an expression depending on those metavariables.

[eric-wieser]

Thanks for the minimization! If this is a simp bug, then I suppose it's possible that leanprover-community/aesop#153 is also a simp bug?

[digama0]

Yes, I think that is the same bug. I've minimized it to something mathlib-free and will report it shortly.

[euprunin]

@digama0 Is there any tool available that can help reduce a small test case relying on mathlib to a minimal version that doesn't depend on mathlib, or is it typically done manually?