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

[Lionel Elie Mamane]

Hi everyone,

I'm using agda from http://coverproject.org/Agda/IAgda.tar.gz
(labelled "2003 version" on the link on
http://coverproject.org/AgdaPage/download.html) because, as I
understood things, it is the newest one supposed to have a correct and
usable termination checker. (Or has this changed now?)


1)

What I get is that the termination checker complains on the type
declaration of a function in a mutual definition. So I have:

mutual
 f :: A -> B {- line 1 -}
 f = \(x::A) -> ... g ... f ...

 g :: A -> B {- line 4 -}
 g = \(x::A) -> ... g ... f ....

and then the termination checker complains on line 1 and 4, column 1
that the call f (g, respectively) might lead to non-termination.

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

2) Given this definition:


mutual
 PASet::Type = data
   PASet_cons (I::Set)(f::I->PASet)(N::(i::I)-> (P (f i)))
 P (x::PASet) :: Set =
       data
         P_cons (f::(xi::SIndex x)-> (P (SFun x xi))) {- line 6 -}
 SIndex::PASet -> Set =  \(X::PASet)->
                              case X of
                              (PASet_cons I f N)->
                                I
 SFun::(X::PASet)->SIndex X -> PASet =  \(X::PASet)->
                              case X of
                              (PASet_cons I f N)->
                                f


the termination checker complains:

 At: "/opt/agda/lionel/bar.agda", line 6, column 25
 The functions PASet, P, SIndex, or SFun might have a negative occurence of SIndex
 At: "/opt/agda/lionel/bar.agda", line 6, column 41
 The functions PASet, P, SIndex, or SFun might have a negative occurence of SFun


I expect I can get rid of these complaints by inlining the definitions
of SIndex and SFun in P, and doing without SIndex and SFun in the
definition, but:

 1) I couldn't find the right syntax to do that. A suggestion?

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

    Note that while this cut-down example has only one occurrence of
    SIndex and SFun in P, what I have in mind has a much more complex
    definition, with multiple occurrences of SIndex and SFun, thus a
    much greater gain in readability in having them.


Thank you by advance for your help,

-- 
Lionel