Bug with let in pattern match

Stream: general

[Rob Lewis]

@Paul-Nicolas Madelaine came across some strange behavior, which we shortened to the following:

def h : ℕ → bool
| 0 := let _ := tt in tt
| (k+1) := k = k -- fails
--| (k+1) := if k = k then tt else ff -- fails
--| (k+1) := if h : k = k then tt else ff -- succeeds

The let in the first case seems to prevent type class resolution from finding decidable (k = k) in the second. Weirdly, if you use a dependent if and name the k = k hypothesis, it succeeds. Does anyone recognize this as a known bug? Or is it something new?

[Kevin Buzzard]

That let is very weird though, right?

def h : ℕ → bool
| 0 := let hello_world := tt in tt
| (k+1) := k = k -- succeeds

[Rob Lewis]

It's not so weird, and the failure also happens with let (a, b) := (tt, tt). Does let _ := ... destruct the rhs? Maybe it has to be a pattern matching let.

[Rob Lewis]

(Yes, it seems like let _ := ... does destruct the rhs.)

[Mario Carneiro]

hm, this looks hard to diagnose without jumping into the C++

[Mario Carneiro]

Also to_bool (k = k) works, even though it's the same thing as k = k, so the error must happen before the lean magic that triggers this

[Rob Lewis]

It's not exactly high priority. I just thought I knew all the big Lean 3 bugs, but this one doesn't look familiar.

[Mario Carneiro]

I agree, I haven't seen this one

[Rob Lewis]

I'll open an issue at community Lean. Not expecting anyone to fix it, just to keep track of it.

[Patrick Massot]

Maybe we should ping Sebastian so that it also goes into his private list, in case it's still Lean 4 relevant?

[Rob Lewis]

@Sebastian Ullrich FYI, if you think this is relevant!