I was trying to prove K (with without-K) using J to see what goes wrong when we try to do that

that's all well and good, but in the process of playing around I noticed that agda refuses to match with refl any term (that I tried) of type Id A x x (saying something along the lines of "can't unify x1 ≟ x1")

for example, agda refuses to case split on p in the following example:

data 1 : Type where
 * : 1
test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 1
test {l} {A} x p = ?

but the following snippet is fine

data 1 : Type where
 * : 1
test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 1
test {l} {A} x p = J {A = A} {x = x} (λ y path -> 1) {y = x} p *

isn't using J here like this essentially the same as case-splitting on p and assuming it to be refl. If yes, then why does agda refuse to split on p in the earlier example.

for reference the type of the J rule being used is this:

J : {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b)
 {y : A} (p : x ≡ y) → B x refl → B y p

I was trying to prove K (with without-K) using J to see what goes wrong when we try to do that.

That's all well and good, but in the process of playing around I noticed that agda refuses to match with refl any term (that I tried) of type Id A x x (saying something along the lines of "can't unify x1 ≟ x1").

For example, agda refuses to case split on p in the following example:

data 1 : Type where
 * : 1
test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 1
test {l} {A} x p = ?

but the following snippet is fine:

data 1 : Type where
 * : 1
test : {l : Level} {A : Type l} -> (x : A) -> (p : x ≡ x) -> 1
test {l} {A} x p = J {A = A} {x = x} (λ y path -> 1) {y = x} p *

Isn't using J here like this essentially the same as case-splitting on p and assuming it to be refl? If yes, then why does agda refuse to split on p in the earlier example?

For reference the type of the J rule being used is this:

J : {A : Set a} {x : A} (B : (y : A) → x ≡ y → Set b)
 {y : A} (p : x ≡ y) → B x refl → B y p