[Agda] acyclicity of constructors

[Conor McBride]

Hi Nisse

On 30 Jun 2008, at 14:25, Nils Anders Danielsson wrote:

> On Sun, Jun 29, 2008 at 5:15 AM, Dan Licata <drl at cs.cmu.edu> wrote:
>>
>> [What exactly does != mean here?  I'm assuming it's (the failure of)
>>  unification-modulo-definitional-equality.]
>
> Yes.
>
>> Actually, the corresponding situation for CoNat is puzzling to  
>> me.  As
>> far as I can tell, in Agda right now, you can neither prove nor  
>> refute
>> (Id n (S n)) for CoNat.
>
> You can prove it for n = omega:

[..]

> And for finite n, with
>
>   data Finite : CoNat -> Set where
>     Z : Finite Z
>     S : forall {i} (n : Finite i) -> Finite (S i)
>
> you can prove the negation.

Ah, but that's not the key question anyway, because
pattern matching relies on Ginger-unification, where
you're trying to find necessary substitutions, forced
by the equations, not Fred-unification where you're
looking for sufficient substituions to satisfy them.
Locally more pertinent is

   (n : CoNat) -> Id n (S n) -> Id n omega

which should hold observationally, but seems likely to
be another "Monster from the Id".

OK. Enough movies already.

All the best

Conor