Do you have a (more or less) formal description of the type system?