are you certain about that? my understanding was that witness terms are indeed passed at runtime especially for non-total functions