[Agda] Maxime Dene's bug fixed

[Jesper Cockx]

>From the patch notes:

* (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.

    mutual
      data WOne : Set where wrap : FOne → WOne
      FOne = ⊥ → WOne

    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

    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.

Regarding the second question, please take a look at our ICFP paper
from this year: http://dl.acm.org/authorize?N87775.


Cheers,
Jesper


On Thu, Nov 27, 2014 at 11:03 AM, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Not long ago Maxime Denes reported a problem with Coq which lead to it
> being incompatible with univalence. Also it meant that there are programs
> definable by structural recursion which are not derivable using
> eliminators. This was also applicable to Agda even with the without-K flag
> turned on. One version of the bug in Agda (by Conor) is below.
>
> My question is: is this bug fixed in the current versions of Agda and Coq?
>
> Next question: how can we make sure that there are no other issues of this
> kind?
>
> Thorsten
>
>
> {-# OPTIONS --without-K #-}
>
> module BadWithoutK where
>
> data Zero : Set where
>
> data WOne : Set where
>   wrap : (Zero -> WOne) -> WOne
>
> data _<->_ (X : Set) : Set -> Set where
>   Refl : X <-> X
>
> postulate
>   myIso : WOne <-> (Zero -> WOne)
>
> moo : WOne -> Zero
> noo : (X : Set) -> (WOne <-> X) -> X -> Zero
>
> moo (wrap f) = noo (Zero -> WOne) myIso f
> noo .WOne Refl x = moo x
>
> bad : Zero
> bad = moo (wrap \ ())
>
>
>
> This message and any attachment are intended solely for the addressee and
> may contain confidential information. If you have received this message in
> error, please send it back to me, and immediately delete it.   Please do
> not use, copy or disclose the information contained in this message or in
> any attachment.  Any views or opinions expressed by the author of this
> email do not necessarily reflect the views of the University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141127/723e12f2/attachment-0001.html