-- Andreas, 2017-11-14, issue #2849, reported by laMudri

-- Internal error, regression introduced by new pattern Internal.AbsurdP

{-# OPTIONS --allow-unsolved-metas #-}

-- {-# OPTIONS -v tc.with.strip:30 #-}

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

-- WAS (2.5.3): Internal error

-- OK error:
-- Failed to solve the following constraints:
--   Is empty: P b

-- This could also succeed, but somehow the rewrite does not
-- apply to the IsEmpty constraint generated by the absurd pattern.
-- The rewrite should be happening before the absurd pattern split.
