[Agda] parsing reports

[Serge D. Mechveliani]

On Mon, Jan 28, 2013 at 03:32:11PM +0100, Nils Anders Danielsson wrote:
> On 2013-01-01 13:38, Serge D. Mechveliani wrote:
> >A minor note on	 Agda-2.3.2 MAlonzo:
> >
> >when a type constructor is not in scope, the type checker reports
> >"could not parse this expression ...",
> >-- without explaining the reason any more precisely.
> >Why the checker does not report, say,  "... not in scope" ?
> >For example,
> >
> >   open import Data.Maybe using (Maybe)   -- `just' is forgotten
> >
> >   f : Maybe Bool -> Bool
> >   f (just _) = true
> >   f _        = false
> >
> >causes       "could not parse (just _)"
> >rather than  "not in scope:  just"
> >
> >For the examples with a complex expression this leads to difficulty in
> >finding the source of this kind of error.
> 
> In many cases it is hard to determine what the problem is. Let me modify
> your example:
> 
>   f : Maybe Bool -> Bool
>   f (just x) = true
>   f _        = false
> 
> The problem could be that "just" is not in scope, but it could also be
> that "_x" is not in scope.
> 

Respectively, a natural report is:
"Line ...
 Cannot parse  (just x).
 Possible reasons:
 1) "just" is an operator being not in scope,  
 2) "_x" is an operator being not in scope
"  
(only 2-3 probable reasons to print).
Seeing "1)", the programmer guesses to import "just".

But suppose that in 99% cases it occurs that the printed reasons are 
not relevant ...
One needs to estimate, how often the reported reasons will occur
relevant.
I am not so sure about this.

Regards,

------
Sergei