[Agda] Agda's copatterns incompatible with initial algebras

Dmitriy Traytel traytel at in.tum.de
Wed Jun 18 21:07:09 CEST 2014

```Dear Agda developers,

today, I was able to prove false in Agda using copatterns and sized
types only (attached). Is my assumption, that those two extensions are
supposed to work together properly, correct?

Especially, the definition of "wit" that refers to itself in order to
produce its own head looks fishy. I would have expected that something
would prevent me from doing this.

This is my first proof in Agda, so please apologize if the example is
not as simplified as possible. The proof (and this email's title) is
based on the examples that exhibit the incompatibility of sized types
and the "musical coinduction" from [1] (of course replacing the "musical
coinduction" by copatterns).

Or am I doing something completely wrong?

Cheers,
Dmitriy

[1] https://lists.chalmers.se/pipermail/agda/2011/003337.html
-------------- next part --------------
{-# OPTIONS --sized-types --copatterns #-}
module False where

open import Size

record Stream (A : Set) : Set where
coinductive
field
shd : A
stl : Stream A
open Stream public

map : ? {A B : Set} ? (A ? B) ? Stream A ? Stream B
shd (map f a) = f (shd a)
stl (map f a) = map f (stl a)

data Mu-Stream : Size ? Set where
inn : ? {i} ? Stream (Mu-Stream i) ? Mu-Stream (? i)

iter : ? {A} ? (Stream A ? A) ? ? {i} ? Mu-Stream i ? A
iter s (inn t) = s (map (iter s) t)

wit : Stream (Mu-Stream ?)
shd wit = inn wit
stl wit = wit

data ? : Set where

false : ?
false = iter shd (inn wit)
```