[Agda] Fixing inferExpr panic

[David Haguenauer]

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):

    unq <- unquoteTerm evd
    unqExpr <- reify unq
    (vunq, tunq) <- inferExpr unqExpr

However, this results in a panic message at runtime (whereas the
unchecked code works fine if it happens to be well-typed):

    Panic: unbound variable Setw
    when checking that the expression Setw has type _60

(Where `w' is actually a lowercase omega.)

Is there something obvious I'm missing? Could somebody point me to a
way to solve any mistake it is I'm making?

-- 
Thanks,
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/cb52069d/attachment.bin