[Agda] "abstract," Integer, and errors

[Sean Leather]

Hi,

I was trying to implement an equality for Integer (Z but renamed to
"Integer" on import), and I ran into a few problems.

First, I tried (using the Emacs mode) to generate the case patterns. I got
the following error:

  Panic: NotADatatype (El (Type 0) (Def Data.Integer.Integer [])).

Not understanding the error (since it appeared to me that Integer is
actually a datatype), I proceeded to write the patterns manually.

Then, I get another error:

  Could not parse the left-hand side geqInteger (:- i) _
  when scope checking the left-hand side geqInteger (:- i) _ in the
  definition of geqInteger

At first, I did not understand why this was happening. But after looking a
bit more closely at Data.Integer, I think I know. Z is annotated as
"abstract" and an abstract datatype does not reveal its constructors
according to the example Introduction.Modules.agda.

So, Z is abstract and I can't pattern match on it. I'm fine with that,
though I would like to know why this is the case.

I would also like to know how to test for equality (or even ordering) on
integers. Is something already available but not apparent to me?

Lastly, I believe the above errors could be improved upon. Ideally, I think
the compiler should know more about abstract datatypes and tell the user
when s/he is trying to access certain details that shall remain hidden.
Errors like "NotADatatype" and "Could not parse ... when scope checking" are
obscure to me.

Thanks,
Sean
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080617/76caa92e/attachment.html