G'day all.
Quoting Janis Voigtlaender
Maybe it is just an accidental swapping of the arguments to (.) in your implementation.
That was it, yes. Thanks for debugging my code for me. :-) (For those keeping score, it was actually the incorrect unzipping of a zipper data structure. If only I could scrap my boilerplate...)
Regarding Lennart's suggestion: I am pretty sure that it would be easy to adapt Sascha's system to omit top level quantifiers. All that should be needed would be an extra pass prior to prettyprinting, to strip off any outermost quantifiers from the data type representing free theorems.
In my case, the approach taken was to pass a Bool around the pretty printer which says whether or not to include quantifiers. (It's okay to strip quantifiers off the right-hand side of an implication if it's okay to strip quantifiers off the implication itself.)
The latter approach has advantages when it comes to producing free theorems that are faithful to the presence of _|_ and general recursion in Haskell, which is not supported by Andrew's system, as far as I can see.
That's correct. Once again, different design criteria apply. IRC has anti-flooding rules which encourage brevity rather than full-featuredness. Cheers, Andrew Bromage