Added invariant to check that referenced declarations are in scope. This one took a while, I don't remember why forall pointer decay is involved.