| 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