[Agda] Type declaration might lead to non-termination?

[takeyama]

Dear Lionel,

Thank you very much for your adoption of Agda, and I am sorry for the
delayed response.

  > 1)
  > ...
  > Hmm... What should I understand from this message? It is a type
  > declaration! What can be unsafe about it?

Probably nothing is wrong in the type declaration.   The error message

   At: XXX
   The call: f
   might lead to non-termination.

should have been written

   At: XXX
   The function f [whose definition starts at XXX] might not terminate.


  > 2) Given this definition:
  > ...
  >  1) I couldn't find the right syntax to do that. A suggestion?

If you mean some sort of let-definition, it is not recommended.

  >  2) This would make the definition of P much less readable; is there
  >     another solution?

How about this?

P_CONS(F::Set)::Set = data P_cons(f::F)
mutual
  PASet::Type = data
    PASet_cons (I::Set)(f::I->PASet)(N::(i::I)-> (P (f i)))
  P(X::PASet) :: Set =
    case X of (PASet_cons I f N)-> P_CONS((xi::I)-> P(f xi))

(The reason P_CONS is defined separately is that "data expression" should
always be explicitly named.)

Best Wishes,

Makoto
-- 
Makoto Takeyama
AIST/CVS (National Institute of Advanced Industrial Science and Technology /
          Research Center for Verification and Semantics)
tel: +81-6-4863-5019   fax: +81-6-4863-5052