Internal error at absurd pattern followed by rewrite

[laMudri]

Trying to check the following file leads to the error:

An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/With.hs:464

module _ where

data _≡_ {a} {A : Set a} (x : A) : A → Set a where
  instance refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}

data ⊥ : Set where

data Bool : Set where
  true false : Bool

data _≤_ : Bool → Bool → Set where
  false≤ : ∀ x → false ≤ x
  ≤-refl : ∀ x → x ≤ x

postulate _∨_ : Bool → Bool → Bool

lemma : ∀ x y → (x ∨ y) ≡ false → true ≤ (x ∨ y) → ⊥
lemma x y eq le with le
... | () rewrite eq

Replacing the absurd pattern by a variable and splitting that via agda-mode also causes an error. It seems to act as if the rewrite were actually expanded into a with on the previous line and the corresponding patterns on the current line. This leaves ... | () | .false | refl, but because there is no extra with on the previous line, the checker complains about there being unexpected with patterns.

[laMudri]

The same internal error is given when checking this definition in place of lemma.

bar : true ≤ false → ⊥
bar () rewrite refl {x = true}

Meanwhile, the following produces a genuine error message.

foo : forall x -> x ≤ false → x ≡ true → ⊥
foo _ () eq rewrite eq

.x ≤ false should be empty, but the following constructor patterns
are valid:
  false≤ ._
  ≤-refl ._
when checking that the clause foo _ () eq rewrite eq has type
(x : Bool) → x ≤ false → x ≡ true → ⊥

[andreasabel]

It seems to be a rewrite issue, since the with version actually works:

open import Agda.Builtin.Equality

data ⊥ : Set where

data Bool : Set where
  true false : Bool

data P : Bool → Set where
  pt : P true

postulate
  b : Bool
  eq : b ≡ false

works : P b → ⊥
works p with b | eq
works () | .false | refl

test : P b → ⊥
test () rewrite eq

[andreasabel]

Agda 2.5.2 still says:

Failed to solve the following constraints:
  Is empty: P b

It seems that this internal error was introduced in the refactoring that added AbsurdP, @jespercockx ?

[andreasabel]

I fixed the internal error and restored the unsolved constraints error.

However, we might want to process absurd patterns after the rewrite. Then this would succeed, like the with version.
@jespercockx : maybe something for your refactoring.