[Agda] parsing reports

[Nils Anders Danielsson]

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.

-- 
/NAD