Non-primitive recursive decidability of products of modal logics with expanding domains