[Agda] hot computer churns codata

[Conor McBride]

Friends

I'm trying to typecheck a file and my left leg is about to burst into
flames. I attach the file.

It's an extensional universe construction with coinductive families.
It goes wild when I try to prove that an unfold is equal to its
unfolding (where "equal" means bisimilar, in a coinductively defined
way). There's only the one corecursive definition in the whole piece:

codata Co (T : Set) : Set where
   [_] : T -> Co T

! : forall {T} -> Co T -> T
! [ t ] = t

data M (I : Set)(S : I -> Set)(P : (i : I) -> S i -> Set)
          (r : (i : I)(s : S i) -> P i s -> I)(i : I) : Set where
   edon : (s : S i) -> ((p : P i s) -> Co (M I S P r (r i s p))) -> M  
I S P r i

unfold : forall {I S P r}
          (C : I -> Set)
          (s : (i : I) -> C i -> S i)
          (m : (i : I)(c : C i)(p : P i (s i c)) -> C (r i (s i c) p))  
->
          (i : I) -> C i -> M I S P r i
unfold C s m i c = edon (s i c) \ p -> [ unfold C s m _ (m i c p) ]

Everything else gets done with unfold. Am I doing it wrong?

I notice that ~ isn't special any more.

Of course, maybe my computer is just puny.

Confused...

Conor


-------------- next part --------------
A non-text attachment was scrubbed...
Name: MTypes.agda
Type: application/octet-stream
Size: 9620 bytes
Desc: not available
Url : https://lists.chalmers.se/mailman/private/agda/attachments/20090519/381bb7f3/MTypes.obj
-------------- next part --------------