failure to see definitional equality?

Stream: new members

[Scott Kovach]

I'm wondering if this is expected behavior, or if anyone could explain what's happening in the failing case:

import Mathlib.Tactic

def S (y : Nat) := {x | x < y}
def f₁        {x y : Nat} : x < y → x < y := id
def f₂ [LT α] {x y : α}   : x < y → x < y := id

variable (h : x ∈ S 0)
example := f₁ h -- ok
example : x < 0 := f₂ h -- ok
example := f₂ h -- ... has type  x ∈ S 0 : Prop but expected to have type ?m.620 < ?m.621 : Prop

why does the presence of meta variables in f₂'s type seem to prevent the definition of S from being unfolded?

[Kyle Miller]

Here are two workarounds:

example := f₂ (id h : x < 0)
example := f₂ (α := Nat) h

I was trying to make sense of the output of set_option trace.Meta.isDefEq true, and it looks like when it's solving ?m.464 < ?m.465 =?= x ∈ S 0 it can't conclude anything, and then it fails. I'm not sure it's able to defer processing until the instance problem is solved.

[Scott Kovach]

thanks, that latter workaround is more concise than what I did (change at) in my real example