| 1. The docs say that annotations can only be applied to top-level | binders/declarations. We’ve found it *very* helpful to annotate nested | binders in some cases to reduce the inference burden (it’s also | extremely helpful for debugging the code/spec). Is this restriction in | place because of the aforementioned issue of not serializing the | GlobalRdrEnv? If so, could the restriction be lifted with the caveat | that annotations on nested binders will *not* be exported? I think that | would be sufficient for us as long as we can get a hold of the Core | before any sort of inlining happens. I think the main awkwardness is that there's no very convenient way to attach the annotation to a nested binder. For built in things like strictness it's all kept in the IdInfo. You could imagine a kind of extensible IdInfo, with a field of [Dynamic], being the annotations. To look up, find the Dynamic with the expected type (e.g. LiquidHaskellSpec). Not very hard, I think, but still work. | 2. The docs say that you can only annotate binders that are declared in | the same module. We’ve similarly found it useful to be able to *assume* | stronger types for certain imported functions, though this is of course | unsound. Could we also lift the same-module restriction, again with the | caveat that the annotations will *not* be exported? I don’t think that would be hard to lift. | I still think that a Template Haskell-based approach could be really | nice without requiring any changes to GHC (beyond the profiling issue | we’ve run into). That sounds good, but I can't really say more because I don't understand what "a Template-Haskell-based approach" really is. I'd be happy to have a Skype call about it, with Ranjit and Niki, if you wanted. Simon