Add type annotations to monadic bind #3327

[dunhamsteve]

Description

This PR implements most of the proposal in #3327. With this change we can optionally provide a type annotation in a monadic bind, following the syntax of the same in a let statement:

test1 = do
  x : Nat <- foo
  printLn x

and with pattern matching

test6 = do
  Just x : Maybe Nat <- bar
    | Nothing => pure ()
  printLn x

The discussion in #3327 (and on discord) mentions support for declaring multiplicities on the binds like in let statements. This is implemented when binding a variable name, but not for a pattern matching bind. The syntax for pattern quantities would have broken existing code and would not function correctly because of issues related to #2513 (ICase does not have a quantity).

Should this change go in the CHANGELOG?

• [x] If this is a fix, user-facing change, a compiler change, or a new paper implementation, I have updated CHANGELOG_NEXT.md (and potentially also CONTRIBUTORS.md).