[Agda] Re: Help debugging

[Nils Anders Danielsson]

On 2009-05-07 04:55, Stefan Monnier wrote:
> In my case, the code started with a variable in place of "inHere" and it
> "worked",

Except that parts of the type signature were highlighted with the
"unsolved metavariable" colour, right?

> and then I used case-split at which point the problem appeared.

If I do that I get the error "Panic: CantSplit foo.inHere", which is
certainly not very helpful.

Ulf, is it possible to switch to a more helpful error message? Perhaps
something like the following:

  Unable to split <variable>.
  The constructor <constructor> is not accepted because
    <the type error you get if you write the constructor manually>,
  but on the other hand it is not possible to omit the constructor,
  because
    <the error you get from the completeness checker if you omit the
    constructor>.

> Great, thanks.  Any hope to see the error message improved so that
> I could have figured out that this was the problem?
> E.g. it seems this error should be signalled right at the
> type-declaration line
> 
>   problem : ∀{Δ τ Δ' t} → (P' : Extend (Δ :: τ) Δ') → t ∈ Δ' → ℕ
> 
> before Agda even tries to process the function's definition.

Agda does warn about the problem with t, but warnings are not displayed
if an error is encountered. Perhaps that should be changed. (Some
warnings cannot currently be computed unless the code is more or less
correct, though: the termination checker only runs after the core part
of the type checker has finished.)

Could the error in the type signature have been turned into an error?
Sometimes an unsolved metavariable becomes solved when a hole is filled
or a new definition is added, so in general I do not think we should
treat unsolved metavariables as errors (during the development of a
file). However, in this case I doubt that it is possible to fix the
problem without changing existing code, and in that case it would be
more helpful with a proper error message.

I have raised a couple of feature requests on the bug tracker.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.