Literal match does not respect first-match semantics

[jespercockx]

When the first clause is blocked on a literal pattern and a later clause is blocked on a constructor, Agda splits first on the constructor. This causes the first clause to not hold as a definitional equality. For example:

open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.Equality

postulate
  A B : Set
  b : B

f : List A → Char → B
f _ 'a' = b
f [] _  = b
f _  _  = b

test : ∀ xs → f xs 'a' ≡ b
test _ = refl

Error message:

f xs 'a' != b of type B
when checking that the expression refl has type f xs 'a' ≡ b

The problem is that the current coverage checker postpones all splits on literals until there are no other splits left.

[jespercockx]

As usual, this can be exploited to violate subject reduction:

open import Agda.Builtin.List
open import Agda.Builtin.Char
open import Agda.Builtin.Equality

postulate
  A B : Set
  b : B

record R : Set where
  field
    f  : List A → Char → B
    pf : ∀ xs → f xs 'a' ≡ b
open R

foo : R
foo .f _ 'a' = b
foo .f [] _  = b
foo .f _  _  = b
foo .pf xs   = refl

illtyped : (xs : List A) → foo .f xs 'a' ≡ b
illtyped xs = foo .pf xs
-- normalizes to 'refl', but giving 'refl' directly is rejected.