Empty parentheses after with are parsed as Unit

[spcfox]

Steps to Reproduce

The argument after with is written in parentheses. But if you leave them empty, they themselves will be parsed as Unit.

f : ()
f with ()
  f | x = x

Expected Behavior

Parsing error

Observed Behavior

Successful compilation

[spcfox]

This is because the parser for with uses bracketedExpr, which can parse Unit

Idris2/src/Idris/Parser.idr

Lines 436 to 437 in 82ea4b1

	<|> do b <- bounds (continueWith indents ")")
	pure (PUnit (boundToFC fname (mergeBounds s b)))

[spcfox]

Other syntactic constructs with parentheses are also parsed

g : (Bool, Bool)
g with (True, False)
  g | x = x

-- Not parser error
failing "Can't solve constraint between: ?x = ?x and ?p True"
  h : (b : Bool ** b = True)
  h with (True ** Refl)
    h | x = x

k : Type
k with (b : Bool ** b = True)
  k | x = x

[buzden]

Wow, didn't know that despite using with clauses a lot. This syntax seems irregular, but, maybe, it's not bad that we may omit double parens.