Eliminating conflicts of parenthesized subexpressions

[Hans Aberg]

Here is a problem I have on how to resolve a shift/reduce conflict in a
Bison grammar:

In the syntax I try to capture, an expression containing ",", "|-", and
atomic_metaformula, is called a metaformula; a subexpressions that does not
contain any of those is called an object_formula. An object_formula can be
considered a metaformula (by assuming an implicit provability "|-"), but a
metaformula can never be viewed as an object_formula.

The grammar below (simplified, as to make a small, compilable example) is
ambiguous, because of the two expansions
  metaformula -> "(" metaformula ")" -> "(" formula ")
  metaformula -> formula -> "(" formula ")
Bison chooses second one, preferring a shift over a reduction:
  metaformula -> formula .       -- reduce
  formula -> "(" formula . ")    -- shift
The shift also gives the wanted result, so one can just %expect the
conflict away. But then there remains an ambiguous grammar, which is
unsatisfactory.

So how do people generally resolve this problem? -- One solution is to
remove the rule
  metaformula: "(" metaformula ")"
replace
  object_formula: "(" object_formula ")"
with
  object_formula: "(" metaformula ")"
and the resolve it semantically in the actions by checking the type of the
cover constructed. Is that what one would generally do, or is there a way
to do it via the grammar?

%token infer_key "|-"
%token atomic_metaformula
%token atomic_formula
%token comma_key ","
%token not_key "not"
%token or_key "or"

%left ","
%nonassoc "|-"
%left "or"
%right "not"

%%

metaformula:
    atomic_metaformula
  | metaformula "," metaformula
  | metaformula "|-" metaformula
  | "(" metaformula ")"
  | object_formula
;
object_formula:
    atomic_formula
  | logic_formula
  | "(" object_formula ")"
;
logic_formula:
    "not" formula
  | formula "or" formula
  /* More stuff */
;

[The problems is the same as this: Suppose one wants to create a simple
arithmetic grammar, with relational operators such as ==, and logical
operators, in which, for numbers a, b, c, one has that a == (b + c) is
legal, but where (a == b) + c is illegal. One simple way to do this, is to
make the grammar
  E:
      number
    | E "+" E
    ...
    | E "==" E
    ...
    | "(" E ")"
  ;
with operator precedences and action type checks. But can this type
difference be directly expressed in the grammar, without action type
checks?]

  Hans Aberg