My last (known) issue is the MINIMAL pragma for a class definition. In Parser.y this is captured (via `name_boolformula`) as a BooleanFormula (Located RdrName) There is a problem with this from an API annotations point of view in that the constructors (mkBool,mkAnd,mkOr) are smart and try to minimise the boolean formula as it is constructed. Unfortunately this discards information in the process. I see a number of potential solutions a. Capture the original source string for the pragma, and use that for the annotations. This is a bad option. b. Introduce a new variant of BooleanFormula for the AST, and convert to use the current one when evaluating the pragma. c. Keep the BooleanFormula as it is, but do not minimise the formula on construction. I suspect that c is the best option, I do not believe the formulas constructed are particularly complex or numerous, so early optimisation is not necessary. Which is the best option? Or is there a different one? Regards Alan