[Agda] Fixing inferExpr panic

[David Haguenauer]

Hi Andreas,

* Andreas Abel <andreas.abel at ifi.lmu.de>, 2011-04-11 23:58:27 Mon:
> in general, converting internal to abstract syntax only happens for 
> printing purposes.  There are exceptions, like in the implementation of 
> "with", and these cause problems.

Yes, it did seem to me that the backwards conversion was meant for
very specific purposes, and, as such, limited. Thanks for confirming
that feeling.

> Set\omega is an internal construct which does not have a 100% 
> correspondence in abstract syntax, since the user can never write it. 

In the meantime, I solved my immediate problem by not mistakenly
introducing Set\omega while unquoting...

> Instead of reification, a second type checker which works on Internal 
> syntax would be better.  It would not be so hard to implement, since 
> Internal syntax is much leaner than Abstract.

Oh, that sounds like a great idea, that will lead to a more robust
long-time solution than relying on dubious calls to `reify'.

-- 
Thanks a lot,
David Haguenauer
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 254 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110411/ae35d6b9/attachment.bin