[Agda] Termination problem with --without-K

[Jacques Carette]

[Probably related to (closed) issue 1214]

{-# OPTIONS --without-K #-}

open import Data.List
open import Data.Nat
open import Data.Bool

module Sort (A : Set) ( _≤_ : A → A → Bool) where
insert : A → List A → List A
insert x [] = []
insert x (y ∷ ys) with x ≤ y
... | true = x ∷ y ∷ ys
... | false = y ∷ insert x ys

This is reproducible in 2.4.0.2. [And note that the above code is 
essentially verbatim from code on the Agda wiki]

Should I open a new bug?

Jacques