Thanks for all infos. I'll apply that Ref-datatype from the "observable sharing" paper to my problem and see where this brings me. I'm also looking into the solution Paul Hudak presented in the "Detecting Cycles in Datastructures" thread in october.
For the problem at hand (involving the STLC), you will not be able to type omega because omega is a non-normalizing closed term and STLC has the strong normalization property. You will have to move to a more expressive calculus to type omega.
I guess the infinite omega-"type" I'm using is not a type in the same way as infinity is not a number. You cannot reach it by structural induction. Therefore the strong normalization property will not work for infinite types (or none-types if you prefer). I admit that allowing infinite types basically means moving to a more expressive calculus. Probably the best thing is to introduce the recursion operator mu explicitly and avoid the cyclic structures. I just thought it would be interesting to play around with infinite stuctures in this context. Thanks again, Tim