Without K

New in version 2.2.10.

The option --without-K makes pattern matching more restricted. If the option is activated, then Agda only accepts certain case splits.

Changed in version 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)].

New in version 2.4.2.

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 is on by default.

New in version 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.

See issues #1023, #1264, #1292.