The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Bingo, Agda seems to have the same problem:

module Termination where

open import Relation.Binary.Core

data Empty : Set where

data Box : Set where
wrap : (Empty → Box) → Box

postulate
iso : (Empty → Box) ≡ Box

loop : Box -> Empty
loop (wrap x) rewrite iso = loop x

gift : Empty → Box
gift ()

bug : Empty
bug = loop (wrap gift)

However, I may be missing something due to my ignorance of Agda. It may 
be well known that the axiom I introduced is inconsistent. Forgive me if 
it is the case.

Maxime.

On 01/06/2014 01:15 PM, Maxime Dénès wrote:
> The anti-extensionality bug is indeed related to termination. More 
> precisely, it is the subterm relation used by the guard checker which 
> is not defined quite the right way on dependent pattern matching.
>
> It is not too hard to fix (we have a patch), but doing so without 
> ruling out any interesting legitimate example (dealing with recursion 
> on dependently typed data structures) is more challenging.
>
> I am also curious as to whether Agda is impacted. Let's try it :)
>
> Maxime.
>
> On 01/06/2014 12:59 PM, Altenkirch Thorsten wrote:
> > Which bug was this?
> >
> > I only saw the one which allowed you to prove anti-extensionality? But
> > this wasn't related to termination, or?
> >
> > Thorsten
> >
> > On 06/01/2014 16:54, "Cody Roux" 
> > <cody.roux AT andrew.cmu.edu>
> >  wrote:
> >
> > > Nice summary!
> > >
> > >
> > > On 01/06/2014 08:49 AM, Altenkirch Thorsten wrote:
> > > > Agda enforces termination via a termination checker which is more
> > > > flexible but I think less principled than Coq's approach.
> > > That's a bit scary given that there was an inconsistency found in
> > > the Coq termination checker just a couple of weeks ago :)
> > >
> > > BTW, has anyone tried reproducing the bug in Agda?
> > >
> > >
> > > Cody
> > 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