Rank 2 intersection types for local definitions and conditional expressions

We introduce a rank 2 intersection type system with new typing rules for local definitions (LET-expressions and LETREC-expressions) and conditional expressions (IF-expressions and MATCH-expressions). This is a further step towards the use of intersection types in ``real'' programming languages. The technique for typing local definitions relies entirely on the principal typing property (i.e. it does not depend on particulars of rank 2 typing), so it can be applied to any system with principal typings. The technique for typing conditional expressions, which is based on the idea of introducing metrics on types to ``limit the use'' of the intersection type constructor in the types assigned to the branches of the conditionals, is instead tailored to rank 2 intersection. However, the underlying idea might be useful also for other type systems.