[Agda] Fixing inferExpr panic

[Andreas Abel]

Hi David,

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.  For instance, if you use irrelevant 
arguments (new since 2.2.8), these are not present in internal syntax, 
so cannot be reified.

Set\omega is an internal construct which does not have a 100% 
correspondence in abstract syntax, since the user can never write it. 
It can be printed, though, this is why it is present in Abstract, but it 
is not well-typed.  The purpose of Set\omega is to have a limit of the 
universe hierarchy Set i, in order to give a type to

   forall i -> Set i

and folks like that.

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.

Cheers,
Andreas

On 11.04.11 6:28 PM, David Haguenauer 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):
>
>      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?

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/