BooleanFormula implies is wrong
The current implementation looks like this:
implies :: Eq a => BooleanFormula a -> BooleanFormula a -> Bool
x `implies` Var y = x `impliesAtom` y
x `implies` And ys = all (implies x . unLoc) ys
x `implies` Or ys = any (implies x . unLoc) ys
x `implies` Parens y = x `implies` (unLoc y)
This cannot possibly be correct: this will decompose the formula A \/ B -> A \/ B in the following way
Or [Var a, Var b] `implies` Or [Var a, Var b]
Or [Var a, Var b] `implies` Var a ||
Or [Var a, Var b] `implies` Var b
But neither of the decomposed formulas are true, so GHC will never find a proof.
I didn't find a case in the typechecker where this actually mattered.