What does it mean if we disable K-rule in Agda?

TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ \mathit{refl} $"?

In https://agda.readthedocs.io/en/v2.5.4.1/language/without-k.html#without-k, K-rule is introduced as an implicit rule and it's defaultly enabled. If I understand it correctly, it means parameter of type $ \forall a.a \equiv a $ can be matched with $ \mathit{refl} $. If we disable K-rule, what will happen? What kind of codes is it going to prevent me writing? Because we can always construct $ \forall a . a \equiv a $, even without K, we can always get an instance of $ T $ by passing $ \mathit{refl} $ to any functions with type $ \forall a.a \equiv a \rightarrow T $.

Agda's doc has given me an example which indeed shows a circumstance that can only work with K:

K : {A : Set} {x : A} (P : x ≡ x → Set) →
    P refl → (x≡x : x ≡ x) → P x≡x
K P p refl = p

In this code, if we can pattern match x≡x with refl, P refl can be trivially equivalent to P x≡x (but without K, we can't).

So does that mean: "K enables people to match $ \forall a.a \equiv a $ with $ \mathit{refl} $"? I didn't find the answer on the Agda doc.

If we disable K, will the semantic of Agda's equality type (CH-ISO) change?

Axiom K is related to "Uniqueness of Identity Proofs", which says is that any two proofs of equality are themselves equal to each other (i.e. are both Refl). Agda doesn't include K as an axiom, but it (and UIP) can be proved as a theorem using Agda's dependent pattern matching.

Axiom K is inconsistent with homotopy type theory, where the univalence axiom provides ways of constructing equalities other than refl. For example, if there are two functions that are pointwise equal, univalence asserts that there is an equality term equating them, but it cannot be refl if the functions have different implementations.

All removing K from Agda does is add restrictions to pattern matching, making fewer matches typecheck. The runtime semantics are unchanged, and no new programs typecheck.

For some excellent introductions on the subject, I recommend:

Pattern Matching without K

Unifiers as Equivalences

Both of these have more detailed versions in JFP if you have access to a subscription.

StackExchange Computer Science Q#98339, answer score: 3