Universals/existentials and Typeable

Universal quantification

• Higher-rank polymorphism, RankNTypes
• (rigid, skolem) type variables (ST, STRef)

Existential types

• Natural syntax with GADTs
• ExistentialQuantification
• Instance dictionaries inside constructors

Typeable

• Typeable, TypeRep (Type.Reflection)
• Variant (aka Data.Dynamic)
• Propositional equality (:~~:, HRefl)