Major overhaul of the type system. Existential types are now simply implicit GADTs, with actual value constructors introduced in expressions and eliminated in patterns. Disjunction in constraints is defined more generally, without guards. Pruning of disjuncts `prune_cn` has no role in inference (just to display the pruned constraint).