This paper proposes a debugging technique for functional programming languages that enables debugging of highly optimised code even if the code that actually is executed is very different from its original specification. We suggest a combination of virtual shadow stacks, uniqueness types, as well as pre- and post conditions for functions. Using this combination, we can trace bugs through function calls that may no longer exist at runtime at all. We describe how this approach is realised in the functional array language SaC and we demonstrate how we can enrich virtual stack traces with partial argument information such as array dimensionality or shape.