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?

• 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).

[gallais]

Isn't it bizarre that we are using desugarDo to elaborate the type?
Does it even make sense to have an effectful function returning a type here?

[dunhamsteve]

Yeah, that struck me as odd, but I followed the pattern of DoLet and DoLetPat. It looks like they were changed from a full desugar to desugarDo in ee063a5 to propagate the do namespace.

[gallais]

Right, I think that should be reverted.
Unless @Russoul has a motivation for it.

[dunhamsteve]

I'll let you guys sort out what is wanted here. It looks like desugar simply calls desugarDo with a namespace of Nothing.

[dunhamsteve]

Yeah I think the function name threw me off, but either looks fine. The difference seems to be what namespace ends up on comprehensions, which I wouldn't expect to appear in types.

What did you want to revert? Is it just changing the otherty elaborations to desugar or more of #1700?