[Agda] Fixing inferExpr panic

[Nicolas Pouillard]

On Mon, 11 Apr 2011 12:28:51 -0400, David Haguenauer <haguenad at iro.umontreal.ca> wrote:
> Hi,
> 
> I altered agda to add some sort of an unquote construct. To make sure
> that the resulting expression is well-typed, I call inferExpr (this
> forces me to convert my Internal.Term `unq' back to the Abstract.Expr
> type using `reify', since that's what inferExpr expects):

We (with Simon Foster and Karim Kanso) had a code sprint at the Agda meeting this
week. One of the goals was to lay the path for better reflection and meta-programming
in Agda. We actually made such an unquote construct today. While this is still work
in progress we have a working basic version by now. I hope you will it tomorrow in the
main Agda repository.

Cheers,

-- 
Nicolas Pouillard
http://nicolaspouillard.fr