[Agda] Termination checking fail in records?

[karim kanso]

Dear Agda Users,

I have noticed that when defining functions in a record they are not
termination checked. Below is a small module that passes the
type checking.

If function f is taken out of the record then the termination checker
picks it up. Presumably because the record definition creates a new
module so feedback is not given in the original definition.

I have tested this in the latest development version, checked out
3rd November. Also, have taken a quick look over the bug reports
and not seen any mention of it.


module error where

record A : Set where
  field
    a : A

  f : A → A
  f = f


I assume this is not the intended behaviour?

Regards,
Karim Kanso
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091104/213463c6/attachment.html