Explore the possibility of putting all type annotations in patterns

[thufschmitt]

So instead of λp:τ.e, we would get λp.e, but with p containing − mandatory − type matching.

For example, x:τ would be the pattern matching on values of type τ