Optionally include a measure of work size in -ddump-timings.

Currently -ddump-timings is quite handy to measure the time/allocations for certain phases.

However it's hard to judge if a growth in time/allocations stems from the compiler processing a larger work load or from us processing it less efficiently.

So I would like to have a flag like -ddump-timings-extra which produces a bit more information.

In particular instead of emitting this info:

Simplifier [Agda.Syntax.Parser.Lexer]: alloc=124670096 time=52.135
Simplifier [Agda.Syntax.Parser.Lexer]: alloc=122955936 time=51.450

I would like to include info about the core size. For example emit something like:

Simplifier [Agda.Syntax.Parser.Lexer]: alloc=124670096 time=52.135 size={total=50, terms=20, types=30, coercions=0}
Simplifier [Agda.Syntax.Parser.Lexer]: alloc=122955936 time=51.450 size={total=60, terms=20, types=30, coercions=10}

We could do so by changing withTiming to something like:

withTiming :: MonadIO m
           => Logger
           -> SDoc         -- ^ The name of the phase
           -> (a -> ())    -- ^ A function to force the result
                           -- (often either @const ()@ or 'rnf')
           -> (a -> SDoc)  -- ^ A function to output a representation of the size of the result (e.g. core size)
           -> m a          -- ^ The body of the phase to be timed
           -> m a