Parsing first order logic

I'm translating some of John Harrison's textbook code
to Haskell. I thought I'd try Happy, Haskell's "yacc",
for parsing instead of Harrison's combinator parsers.

Since both formulas and terms can be parenthesized,
I ran into trouble with the following:

(P) meaning "the propositional variable P"
(c) meaning "the term constant c"

Then I have a reduce reduce conflict, eg. in the following cases

(P) /\ Q
(c) = 5 /\ Q

It occurred to me that even something as simple as the
following dumbed-down grammar is not LR(1) as far as I can tell:

T is "terms" and F is "Formulas"

T ::= var | ( T )
F ::= var | ( F ) | T = T

I can't think of a way to make this LR(1). In fact, it seems it's
not even LR(k), as (c) could just as easily be (f(1,2,3,...,n) = 5).
Thus I think my 'happy' experiment is a failure. Of course, with a backtracking
combinator parser this is easily remedied.