@zyang (cc, @AndrasKovacs) Thank you for the interesting blog post! It really helped me to understand the optimizations that NbE applies. After reading the original blog post I also tried thinking about ways to simplify nf7 and I worked out one alternative (https://github.com/DDOtten/NbE-cached/blob/main/NbE.hs). I implemented a further variation (`nf8` at the end of the file) that avoids the need for the `forceShifts` function. This change is based on storing the number of shifts at the root of the cached normal forms: instead of storing a ~TmS with lazy weakenings we store a ~Tm and the number of shifts that need to be applied to the normal form for this specific occurrence. I hope the computational complexity of `nf8` is the same as `nf7`, since both have to traverse every cached normal form once per occurrence to apply the needed shifts (which depend on the number of additional binders encountered before substituting this occurrence), but I have not worked this out in detail yet. I did compare the output and performance of (both the original and newly updated) `nf7` and `nf8` on the original adversarial example and two new large adversarial examples, and they match, with `nf8` being slightly faster on my computer. However, a more detailed analysis of computational behavior is needed, so please let me know if I made any mistakes!