Pattern matching and GADTs