Error: Unsolved holes: when using _ in do block

[alexhumphreys]

Steps to Reproduce

Found on Idris 2, version 0.4.0-70ac0f410. Requires idris2 -p contrib:

module Foo

import Text.Parser

infixOp1 : Grammar state t True ()
        -> a
        -> Grammar state t True a
infixOp1 p x = do
  p -- compiles
  pure x

infixOp2 : Grammar state t True ()
        -> a
        -> Grammar state t True a
infixOp2 p x = do
  y <- p -- compiles
  pure x

infixOp3 : Grammar state t True ()
        -> a
        -> Grammar state t True a
infixOp3 p x = do
  _ <- p -- Error: Unsolved holes
  pure x

Expected Behavior

I would expect all three to compile, assuming I understood #1095 and it's ok to throw away unit types as is the case of p in infixOp1.

Observed Behavior

infixOp1 and infixOp2 compile, infixOp3 throws the following error:

"Idrall/Foo.idr" 24L, 439C written
Error: Unsolved holes:
Idrall.Foo.{c2:805} introduced at:
Idrall.Foo:23:3--23:9
 19 | infixOp3 : Grammar state t True ()
 20 |         -> a
 21 |         -> Grammar state t True a
 22 | infixOp3 p x = do
 23 |   _ <- p -- Error: Unsolved holes
        ^^^^^^
Idrall.Foo.{tok:828} introduced at:
Idrall.Foo:24:3--24:9
 20 |         -> a
 21 |         -> Grammar state t True a
 22 | infixOp3 p x = do
 23 |   _ <- p -- Error: Unsolved holes
 24 |   pure x
        ^^^^^^
Idrall.Foo.{state:829} introduced at:
Idrall.Foo:24:3--24:9
 20 |         -> a
 21 |         -> Grammar state t True a
 22 | infixOp3 p x = do
 23 |   _ <- p -- Error: Unsolved holes
 24 |   pure x
        ^^^^^^

I'm not sure why it's ok when bound to a name, but fails when bound to _. Maybe I'm doing something wrong, but at least the error message is pretty confusing...

This is a small example, but I ran into this in the wild here

[gallais]

_ is not detected as a valid variable name and so _ <- p is desugared as a pattern-matching bind.
Which means it introduces a case and then Idris has a hard time guessing what the value of the boolean
stating whether the grammar is productive should be.