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

## ice1000

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?