Case splitting inserts one with pattern too much (regression in 2.6.2)

[andreasabel]

Case splitting (C-c C-c) in last goal produces in 2.6.2

  ... | join rs₄' rs₂' | join r₃ r₄ = ?
-- Unexpected with patterns | join r₃ r₄

while in 2.6.1 it correctly gives:

  ... | join r₃ r₄ = {!!}

Code:

module NewmansLemma {ℓ} {A : Set ℓ} (let Rel = A → A → Set ℓ) (R : Rel) where

variable
  a a₁ a₂ a' : A
  b b₁ b₂ b' : A
  c c₁ c₂ c' : A
  r r₁ r₂ r' : R a b
  s s₁ s₂ s' : R a b

-- Reflexive transitive closure

data R* : Rel where
  nil   : R* a a
  cons  : R  a b → R* b c → R* a c

-- Joinable elements

data Joinable : Rel where
  join : (r₁ : R* a₁ a) (r₂ : R* a₂ a) → Joinable a₁ a₂

-- (Locally) confluent

LocConfl = λ a → ∀ {a₁ a₂} → R  a a₁ → R  a a₂ → Joinable a₁ a₂
Confl    = λ a → ∀ {a₁ a₂} → R* a a₁ → R* a a₂ → Joinable a₁ a₂

-- Accessible elements

data Acc : A → Set ℓ where
  acc : (∀{b} (r : R a b) → Acc b) → Acc a

-- Wellfoundedness

WF = ∀ a → Acc a

module Newman (lc : ∀{a} → LocConfl a) where

  newman : Acc a → Confl a
  newman (acc h) nil nil = join nil nil
  newman (acc h) nil (cons r rs) = join (cons r rs) nil
  newman (acc h) (cons r rs) nil = join nil (cons r rs)
  newman (acc h) (cons r₁ rs₁) (cons r₂ rs₂) with lc r₁ r₂
  ... | join rs₃ rs₄ with newman (h r₁) rs₁ rs₃ | newman (h r₂) rs₄ rs₂
  ... | join rs₁' rs₃' | join rs₄' rs₂' with newman {!!} rs₃' rs₄'
  ... | z = {!z!}

[UlfNorell]

Shrunk example:

data ⊤ : Set where
  tt : ⊤

f : ⊤ → ⊤
f tt = tt

foo : ⊤ → ⊤
foo t with f t
... | x with f t
... | y with f t
... | z = {!z!}
-- ... | y | tt = ?  -- <- result

Adding more nested withs adds more incorrect pattens (always including everything from y and onwards)

[UlfNorell]

Bisection points to 86b3223 (@jespercockx)

[andreasabel]

@jespercockx : Maybe this is not too hard to fix (?). Would be nice to get it into 2.6.2.1.

[jespercockx]

I have just found a fix, PR incoming...

[andreasabel]

Picked onto 2.6.2.1.