[Agda] Agda compiler optimizations

[agda newb]

Hello, i'm really new to agda and dependently typed languages but i'm really impressed by it.
Just want to suggest something like "optimization trade" idea - you give proofs to compiler and compiler gives you optimizations.
In dependently typed languges it should be easy to provide proofs for various things, set of these things includes proofs for various optimizations
which can be safely performed on proven code.
E.g:
Prove that you natural numbers definition can't go out of certain bounds,
write something like this {#- OPTIMIZATION NO_BIGINT MyNat #-} and compiler will throw away bigint support for numbers.
That bigint example is quite silly but i think it can help to get the idea i'm trying share.

What do you think about it?