Algebraic data types + higher kinded System F

• add user definable algebraic data types
• allow nested pattern matching on algebraic data types
• use type safe de Bruijn indices internally
• use System F as internal calculus
• add higher kinded polymorphism and polymorphic recursion