RE: panic: addImpDecls

| Is this preparatory work visible at all? Or still under wraps? Could
| you explain the idea in a little more detail? Is this only for
"closed"
| declarations and expressions?

It's not secret; it's just not implemented! 

Briefly the deal is this.  Currently the type checker typechecks
brackets, but throws the translated (type-annotated) term away.  The
desugarer translates the original un-annotated term.  It'd be better to
keep the translated term, so the desugarer could (if THSyntax supported
types somehow) have access to the types.  But the translated term is
slightly mixed up: there are type abstractions and applications (easy to
discard), but AbsBinds (the translation of a binding group) is a bit
more of a problem.  Anyway, it seems like the right way to go.  Just
need to find time to do it.

Simon