Another '(kernel) declaration has metavariables' error

Stream: new members

[Egor Morozov]

Here is my setup minimized to a mwe.

import Mathlib

example (m : ℕ) : ∑ n ∈ Finset.range m with h : Even n, n = 0 := by
  conv_lhs =>
    arg 2
    intro n
    congr
  sorry

(Of course, the statement is nonsense, it's just to illustrate the issue.) I get

(kernel) declaration has metavariables '_example'

Is this error smth I should expect here or it is a bug?

[Jakub Nowak]

It's a bug I think.

[Kyle Miller]

Definitely a bug. Looking at the proof term, somehow there's a Decidable instance that's not getting synthesized. It'd be great if someone could make a mathlib-free #mwe of this. Possibly all someone needs to do is try to use conv => congr on a dependent if.

[Jakub Nowak]

Hm, I've had a mathlib free one, but I forgot to post it and I've already closed the tab with it. I'll try to do it again. .-.

[Jakub Nowak]

/--
error: unsolved goals
⊢ if h : True then True else True
---
error: (kernel) declaration has metavariables '_example'
-/
#guard_msgs in
example : if h : True then True else True := by
  conv =>
    fun
    intro h
    congr

[Jakub Nowak]

Kyle Miller said:

Possibly all someone needs to do is try to use conv => congr on a dependent if.

When I looked at it seemed that intro before congr was also needed to trigger the bug.

[Jakub Nowak]

For example, first one works, second doesn't:

example : dite True (fun h => True) h := by
  conv =>
    congr

/--
error: unsolved goals
⊢ if h : True then True else True
---
error: (kernel) declaration has metavariables '_example'
-/
#guard_msgs in
example : (fun h => dite True (fun h => True) h) h := by
  conv =>
    fun
    intro h
    congr