[Agda-dev] without K and termination

[John Leo]

Hi everyone,

Recently I created a simple slow set implementation using a list, and ran
into some unexpected behavior when I tried to invoke without-K. In the code
below (which uses the standard library), the first two "ok" variations are
fine, but the original "insert" fails the termination checker. If without-K
is turned off everything passes. This seems to be some strange interplay
between records, with clauses, and without-K, but I don't know if this is a
bug or just some subtlety that I don't understand. Please let me know what
you think, and if it's a bug I'm happy to file it. Agda version
is 2.6.0-b754131.

John

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

module WithoutKTermination where

open import Data.List                             using (List; []; _∷_)
open import Relation.Binary.Core                  using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary                      using (yes; no)

record ListSet (A : Set) : Set where
  constructor listSet
  field
    set : List A
    eq  : Decidable {A = A} _≡_
open ListSet

insertOk : {A : Set} → A → ListSet A → ListSet A
insertOk a (listSet []      e) = listSet (a ∷ []) e
insertOk a (listSet (b ∷ l) e) = listSet (b ∷ set (insertOk a (listSet l
e))) e

insertOk2 : {A : Set} → Decidable {A = A} _≡_ → A → List A → List A
insertOk2 e a [] = a ∷ []
insertOk2 e a (b ∷ l) with e a b
insertOk2 e a l@(b ∷ _) | yes p = l
insertOk2 e a (b ∷ l)   | no ¬p = b ∷ (insertOk2 e a l)

insert : {A : Set} → A → ListSet A → ListSet A
insert a (listSet []      e) = listSet (a ∷ []) e
insert a (listSet (b ∷ l) e) with e a b
insert a (listSet l@(b ∷ _) e) | yes p = listSet l e
insert a (listSet   (b ∷ l) e) | no ¬p = listSet (b ∷ set (insert a
(listSet l e))) e
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180316/f7df251d/attachment.html>