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

Question

TL;DR: Can I say, "K-rule in Agda enables people to match $ \forall a.a \equiv a $ with $ 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 $ 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 $ 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 $ 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?