# Without K¶

The option `--without-K`

makes pattern matching more restricted. If
the option is activated, then Agda only accepts certain case
splits. This option was added in Agda 2.2.10.

Since Agda 2.4.0 when the option `--without-K`

is enabled, then the
unification algorithm for checking case splits cannot make use of the
deletion rule to solve equations of the form `x = x`

.

For example, the obvious implementation of the J rule is accepted:

```
J : {A : Set} (P : (x y : A) → x ≡ y → Set) →
((x : A) → P x x refl) → (x y : A) (x≡y : x ≡ y) → P x y x≡y
J P p x .x refl = p x
```

Pattern matching with the constructor `refl`

on the argument `x≡y`

causes `x`

to be unified with `y`

. The same applies to Christine
Paulin-Mohring’s version of the J rule:

```
J′ : {A : Set} {x : A} (P : (y : A) → x ≡ y → Set) →
P x refl → (y : A) (x≡y : x ≡ y) → P y x≡y
J′ P p ._ refl = p
```

On the other hand, the obvious implementation of the K rule is not accepted:

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

Pattern matching with the constructor `refl`

on the argument `x≡x`

causes `x`

to be unified with `x`

, which fails because the deletion
rule cannot be used when `--without-K`

is enabled.

For more details, see the paper Eliminating dependent pattern matching without K [Cockx, Devriese, and Piessens (2016)].

The option `--with-K`

can be used to override a global
`--without-K`

in a file, by adding a pragma
`{-# OPTIONS --with-K #-}`

. This option was added in Agda 2.4.2 and
it is on by default.

Since Agda 2.4.2 termination checking `--without-K`

restricts
structural descent to arguments ending in data types or `Size`

.
Likewise, guardedness is only tracked when result type is data or
record type:

```
data ⊥ : Set where
mutual
data WOne : Set where wrap : FOne → WOne
FOne = ⊥ → WOne
postulate iso : WOne ≡ FOne
noo : (X : Set) → (WOne ≡ X) → X → ⊥
noo .WOne refl (wrap f) = noo FOne iso f
```

`noo`

is rejected since at type `X`

the structural descent
`f < wrap f`

is discounted `--without-K`

:

```
data Pandora : Set where
C : ∞ ⊥ → Pandora
postulate foo : ⊥ ≡ Pandora
loop : (A : Set) → A ≡ Pandora → A
loop .Pandora refl = C (♯ (loop ⊥ foo))
```

`loop`

is rejected since guardedness is not tracked at type `A`

`--without-K`

.