[Agda] command line type checker vs interactive

[Sergei Meshveliani]

Dear Agda developers,

Is it possible to agree the command line type checker reports with such
of interactive one?
I mean to report explicitly _all_ the places which are highlighted
yellow in the interactive checker (mainly they are related to "unsolved
metas").

The matter is that 
1) some programs are much more difficult (practically impossible) to 
   debug when using a command line checker than in the interactive one, 
2) generally, it is desirable to have a working command line type 
   checker, in particular, because setting agda mode in emacs may 
   present problems.

For example, I do not find what is wrong in the program of 

http://www.botik.ru/pub/local/Mechveliani/agdaNotes/bug-dec28-2015.zip

(It is not large: 12 Kb archive.  See README.agda there).

This ids for  Development Agda of December 18 (ghc-7.8.3).
It reports
"Expected a visible argument, but found a hidden argument ...",
which report looks like a bug in Agda (see README.agda).

And I suspect that the interactive checker may (if I manage to install
it) highlight earlier some "unsolved metas" place which is not reported
by the command line type checker. 

Probably, I shall try more with setting a mode for emacs.
But I think that, anyway, a workable command line type checker is quite
necessary.

Regards,

------
Sergei