Read on Twitter
Has anyone done used bidirectionally typed IRs for compilation before? If you have dependent types (or some sort of parametric polymorphism), does that mean you have to re-implement an evaluator for each type-directed compiler pass?
Eg. I'm doing a compilation pass from my bidirectional PTS-style core language to a stratified language, but I need to know the types of function arguments to do so: https://twitter.com/brendanzab/status/1278860210770079744. I'm guessing I might need to re-evaluate types to figure that out?
Not sure if @pigworker has any ideas - I was trying to go down the route of a bidirectionally typed IR based on what I read in “The types who say ‘ni’” 
: https://twitter.com/brendanzab/status/1163979356030558209
: https://twitter.com/brendanzab/status/1163979356030558209
So, in some detective work going back into my prior state of mind, it seems like this thread is where I got scared off from using readback in my elaborator, which actually seems quite similar to what McBride is talking about in the above quote: https://twitter.com/brendanzab/status/1120190725184872448
Apparently, according to @ollfredo, using ‘glued evaluation’ might help here by allowing you to “read back terms smaller (close to the surface term they came from)”. This is implemented in smalltt and sixty:
• https://github.com/AndrasKovacs/smalltt/
• https://github.com/ollef/sixty/
• https://github.com/AndrasKovacs/smalltt/
• https://github.com/ollef/sixty/
If I understand correctly, this explains why @ollfredo can readback parameter types to core terms during elaboration without needing to worry about term-size blowup (which is what I was trying to avoid): https://github.com/ollef/sixty/blob/f840ec29b0820f25e246671c6253263324f04078/src/Elaboration.hs#L796
