[Agda] Agda's copatterns incompatible with initial algebras

[Dmitriy Traytel]

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)