Support type annotations on LHS of a monadic bind `<-` about idris2

[joelberkeley]

Those appear to me to all agree with how let bindings work (which is a very good thing, as having subtly different syntax for each would be a recipe for confusion)

[joelberkeley]

OK thanks. I'd only suggest parsing what can be parsed currently in let, even using the same parser code if possible

[dunhamsteve]

I've coded this up and the type annotations are working fine, but I need to drop the multiplicities on the pattern matching version. We can still have quantities on bare variables.

There are two problems with quantities on patterns. One is that the syntax is breaking existing code (CI fails). E.g. Network.Socket.Data does:

nullPtr p = do 0 <- primIO  $ prim__idrnet_isNull p

which no longer parses because 0 is getting eaten as a quantity.

The second issue is that it won't work at all in the current Idris (this is issue #2513). You can see that while the syntax is accepted for let, it's not functioning correctly. E.g. y is unerased in the hole in this code:

blah : Maybe Nat -> Nat
blah x = let 0 (Just y) = x | Nothing => 0 in ?hole

Issue #2513 is fixed in PR #2535 which we closed pending new core. I'm happy to revive that work separately, if and when we're ready to merge it.

But the type annotations and quantities on variables do work. I can PR this after backing off the pattern quantities. I'll leave the previous commit in the branch history.

[buzden]

It also needs to be thought how this feature would interplay with pattern matching and shortcut alternatives:

do (a, b) : (X, Y) <- foo
   1 (c, d, e) : (A, B, C) <- bar
   5 : Nat <- baz
     | 6 => unbaz
     | _ => unbaf
   unfoo

[dunhamsteve]

I don't think the 5 example is consistent with the current behavior of let. Because of parsing for multiplicities, let will give a parse error for:

let 5 := ...

and

let 5 : Nat := ...

but accepts:

let (5) := ...

The parser for multiplicity could be tweaked to only have this behavior for 0 and 1, but it might rule out having other multiplicities in the future.

[joelberkeley]

what about let 5 : Nat =?

[dunhamsteve]

Currently that is a parse error:

1: Couldn't parse declaration.

src.Temp:12:13--12:14
 08 | --      then S (countFst (x :: zs) | zs) 
 09 | --      else countFst (x :: zs) | zs
 10 | 
 11 | foo : Nat -> Nat
 12 | foo x = let 5 : Nat = x | _ => 42 in 6
                  ^
... (6 others)

If you put parens around the 5, it parses, because the parser for multiplicity doesn't see the number.

[dunhamsteve]

Because of this - it maybe parses a number and then decides its an error if there is a number there that is not 0 or 1. Arguably correct if we plan to support other numbers someday?

  multiplicity : OriginDesc -> EmptyRule RigCount
  multiplicity fname
      = case !(optional $ decorate fname Keyword intLit) of
          (Just 0) => pure erased
          (Just 1) => pure linear
          Nothing => pure top
          _ => fail "Invalid multiplicity (must be 0 or 1)"

If we do want a bare 5 to work, this would have to change to succeed without consuming anything for integers other than 0 or 1.

[buzden]

Arguably correct if we plan to support other numbers someday?

Maybe, but someday we will have support of whole expressions for quantities, and this will anyway cause similar problems on the next level