Panic in fun_prop

Stream: mathlib4

[Attila Gáspár]

In the following example, fun_prop causes a PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:381:22: loose bvar in expression instead of failing:

import Mathlib.Tactic.FunProp

@[fun_prop]
axiom A {α β : Type} (f : α → β) : Prop

axiom f : Unit → Unit

@[fun_prop]
axiom x : (∀ g : Unit → Unit, A g) → A f

theorem y : A f := by
  fun_prop

[Kim Morrison]

@Tomas Skrivan may be the relevant person to help?

[Tomas Skrivan]

It should definitely not panic, and with a quick look I couldn't figure out why it is happening.

Also on my recent refactor of fun_prop it does not throw anymore but it might be some time before I finish it. Is this blocking you from doing some work and you need a fix? or is this just something you have encountered?

[Attila Gáspár]

While I was experimenting with measurability, I found that fun_prop gives this error when it tries to use docs#Multiset.aestronglyMeasurable_prod. I've made PR #31001 to fix the panic, but unfortunately it doesn't make aestronglyMeasurable_prod usable by fun_prop. But so far it hasn't caused any issues, so it's not urgent.