Why does Epigram colors Branches brown?

[Serguey Zefirov]

     (   X : *    !        ( X : * ;  subs : List (Tup X (Bush X)) !
data !------------!  where !---------------------------------------!
     ! Bush X : * )        !        Branches subs : Bush X         )

Tup is a tuple, List is a list.

[Wouter Swierstra]

Hi Serguey,

>     (   X : *    !        ( X : * ;  subs : List (Tup X (Bush X)) !
> data !------------!  where !---------------------------------------!
>     ! Bush X : * )        !        Branches subs : Bush X         )
>
> Tup is a tuple, List is a list.

This is a limitation in Epigram's current treatment of data types. If  
recursive occurrences of Bush occur within other types (like List or  
Tup in your example), Epigram cannot tell that the data type is  
strictly positive. You can find more about this in Peter Morris's  
thesis:

http://www.cs.nott.ac.uk/~pwm/thesis.pdf

I'm not entirely sure what's going on in your other question regarding  
implicit arguments.

In the meantime, I'd recommend you have a look at Agda:

http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.HomePage

At the moment, it's much better supported than Epigram and has a very  
similar type theory. It can handle things like you Bush data type, for  
example.

Hope this helps,

   Wouter