...

I propose that haskell' include a standard syntax for invariants that the programmer wants to express.

...

The intent is not to have standardized checks on the invariants, its just to supply a common way to specify invariants to that the various strategies for checking them can all work from the same data. For example, one tool might use the invariants to generate QuickCheck properties

I think it's too early for this. As others have pointed out, it's not even clear what the semantics of these things should be. What's more, the way you write such properties depends partly on what you intend to do with them. QuickCheck properties aren't just logical properties, they're restricted to make them testable, and carry extra information to control test case generation. Other tools, like partly automated provers, may need other additional information, such as induction variables. We spent a lot of time looking for a unified property notation in the Cover project, and we didn't find one we were really happy with. The P-logic that Programmatica uses, and the preconditions that Dana Xu used in her Haskell workshop paper, are quite different from each other. We need more research on the tools that would use these annotations, before we try to fix their syntax. John