[Agda] Testing new Haskell functions

[Simon Foster]

Hi,

What's the best way to test out Haskell functions manipulating Agda  
Terms? For instance, I've written a few instances of FromTerm for  
appropriate Haskell types and I'd like to check if my instances work.

Testing a function on a type is easy, as I can just create an  
interaction point with the type I want and then pull the Expr out of  
the state. However, if I want to use a term, like a vector for  
instance, I can't figure out how to parse this on the *ghci*  
commandline. Running parseExprIn (from BasicOps) with the expression I  
want using ioTCM_ mostly fails (ioTCM_ doesn't seem to return type- 
checking errors at the moment). For instance if I do parseExprIn ii  
noRange "[]", I correctly get the corresponding Vector expression, but  
if I try to parse "zero ∷ []" I get a failure (zero is in scope in  
the loaded module with the given interaction point and this expression  
can be deduced from Agda).

Is there a better/easier way to do this?

Thanks,

-Si.