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
