normalizationBarrier : (input -> output) -> input -> output
Preserve a value at runtime while preventing importing modules from unfolding an expensive computation during dependent type elaboration.