Allow pattern-matching in let-bindings

[AshleyYakeley]

Currently we have to do this:

f: P *: Q;
let
p: P = f >- fn (p,_) => p;
q: Q = f >- fn (_,q) => q;
in expr;

It would be nice to be able to do something like:

let
(p,q) = f;
in expr;

The problem is that : in pattern-matching now has two different meanings. Consider

g = fn y => let
x: T = y;
in x;

Does g have type T -> T or D(T) -> T?

[AshleyYakeley]

• Option 1: : always means dynamic checking, don't worry about it.
• Option 2: : means static checking, introduce a new syntax for dynamic checking.

[AshleyYakeley]

If option 2, then :? is the obvious syntax.

[AshleyYakeley]

Done.