[Agda] command line type checker vs interactive

[Sergei Meshveliani]

Kahl,

thank you for your advices.  
You write on On Wed, 2015-12-30 at 10:49 :

> Sergei,
> 
> > I mean to report explicitly _all_ the places which are highlighted
> > yellow in the interactive checker (mainly they are related to "unsolved
> > metas").
> > 
> > [...]
> >
> > 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).
> 
> A real error like this is, in the interactive view,
> often surrounded by unresolved metas that Agda
> didn't even try to resolve before it encountered the error ---
> I doubt that it would be useful to report those.
>> [..]

Anyway: there are examples in which it is much easier to find the place
responsible for an error by using the interactive type checker.
And on other examples the two checkers are equally useful in searching
the responsible place.
And I am asking for the command line type checker which is equally
useful in searching the responsible place in all examples.


> No matter whether interactively or using the command line,
> I recommend that you comment out the error location
> and everything after it,
> and try to typecheck the remaining module to see whether
> there are real unsolved metas.
> 

This does not work. The fragment is 

   let ...
 
       e1 :  (asd ε) ∙' Q  =' Q  
       e1 =  UpMonoid.ε∙ asdUpMonoid Q       
   in
   a

, where `a' is dummy, does not use the values inside this let-in.  

The error report is for the line of  "e1 = ".
If  e1  is commented out, then the program is type-checked.

Regards,

------
Sergei