[Agda] Record definition being in scope during type checking can cause Agda to hang

[Nils Anders Danielsson]

On 2010-10-01 15:09, Iain Lane wrote:
> record Tailspin : Set where
>   field
>     Kaboom : Tailspin
>   test : Tailspin
>   test = ?

I think the problem here is that you are using a recursive record type.
Such types are not really supported, but for some reason they are not
disallowed, maybe to allow experiments with coinductive records:

   record Stream (A : Set) : Set where
     constructor _∷_
     field
       head : A
       tail : ∞ (Stream A)

--
/NAD