Improvements for `Text.Pretty`

[gallais]

Currently http://agda.github.io/agda-stdlib/Text.Pretty.html suffers from various limitations:

1. Performance: _<>_ only filters the invalid results, it does not discard the dominated ones. This doesn't prevent combinatorial explosion (we've been experiencing issues with this on my Haskell port of the Agda port in https://github.com/msp-strath/TypOs). Cf. the call to bestsOn here in the original lib.

2. Any result is better than no result: we do guarantee that the result will fit in the tapewidth... at the cost of never returning anything if no layout will fit! It would be better for the toplevel Doc to be a sum type of either a List1 of candidates that fit or a single document that does not fit.

3. Support for annotations & configuration (it's all worked out in this Doc.Internal module and just needs porting)