Splitting inside lambda using where-block causes unhandled exception

[mbrea-c]

Steps to reproduce

1. Load the following code:

open import Data.Nat using (ℕ)

fails : ℕ → ℕ
fails = 
  λ where 
  x → ?  -- fails to case split here

2. Try to case split on x at the goal

Expected result

Variable x is successfully split in cases

Actual result

The following error:

UNHANDLED EXCEPTION ErrorResult nvim_buf_set_text (ObjectArray [ObjectInt 1,ObjectString "'start' is higher than 'end'"])

Where this is used

Afaik using λ where is a common pattern when paired with case_of_ from the Function.Base module in the stdlib. Personally, I use it for type-safety proofs in large developments, where the nesting makes it harder to cleanly use with-abstractions.

Edit: Found some more related weird behaviour. In the following snippet:

open import Data.Nat using (ℕ)

works : ℕ → ℕ
works = 
  λ { 
  z → ? 
  }

fails : ℕ → ℕ
fails = 
  λ where 
  x → ? 

case splitting on x in the second goal will actually split z from the first lambda.

[isovector]

I think this will be a hard one to fix; last I checked, Agda doesn't give us the buffer range we need to change when it gives splits. If that's still the case, we'd somehow need to figure out the scope of the where block on our own :|