simp doesn't rewrite in definitions because of unassigned metavariables

[fpvandoorn]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following code fails:

set_option trace.Meta.Tactic.simp true
def foo {ι : Type _} (n m : ι) (h h' : n = m) : ℕ := by
  simp only [id h] at h' -- no progress
  simp only [h] at h' -- works

The trace message is

[Meta.Tactic.simp.rewrite] id h:1000, has unassigned metavariables after unification 

Note that the unassigned metavariable is the universe metavariable of ι

Expected behavior: simp only [id h] should succeed, just like simp only [h] already does.

Related Issues

#4398 is basically the same issue, and #4493 didn't really fix the underlying issue.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[leodemoura]

#4398 is basically the same issue, and #4493 didn't really fix the underlying issue.

The change in #4482 is only applied to defs whose type is a Prop. This is not the case here.
We can easily remove the <- isProp condition there, and eliminate the discrepancy in the def and theorem elaborators.
See comment at #4482 for potential impact on users.

[fpvandoorn]

I don't think it's feasible to generalize universe metavariables in definitions before elaborating the value. As mentioned in #4482, that will lead to huge inconveniences.

I don't think that the rule "don't have universe metavariables around" is the right solution here. Here is a (somewhat contrived) example using theorem.

theorem bar (n m : Nat) : n = m → n = m := by
  have : ∀ (α : Type _) (x y : α), x = y → x = y := by
    intros α x y h
    simp only [id h] -- error. The proof works if you remove `id`
  exact this Nat n m

I might be completely misunderstanding why the behavior here happens, but my understanding is as follows:
My understanding of this issue is that when t is an expression (not just a name), then simp [t] will refuse to rewrite with t if t still contains universe metavariables. Maybe the check can be "no universe metavariables that are introduced by this simp" (if this can be checked cheaply)?

Feel free to mark this as low priority/wontfix, this is a low priority issue. I was surprised when I encountered it (it was within a def), so I opened an issue.

[leodemoura]

@fpvandoorn Note that the theorem bar example in your message will be rejected in the future. See #4610

[leodemoura]

I don't think that the rule "don't have universe metavariables around" is the right solution here

The motivation is simplicity.

[fpvandoorn]

Ok, this happens only rarely in Mathlib, so I think the fallout will be limited.

After that I think the only issue is in definitions.