Dear Agda developers, It will be extremely useful to have the type checker warnings (switched by the option) for unused values (types), unused import, and such (like it is in Glasgow Haskell). Regards, ------ Sergei