To me, a lot of the more interesting areas of type research basically involve embedding logic into types. So types for sequencing of operations, types that cons

To me, a lot of the more interesting areas of type research basically involve embedding logic into types. So types for sequencing of operations, types that constrain the data in them, etc. Those are awesome in that they enable static analysis to detect more sorts of logic errors in a digestible way, but my impression is that they end up encoding constraints in the type system that are then harder to change as the demands on the system evolve.