[ project ] merge PRs #2017 and #2022

Closing #2017 in favour of re-raising an issue to sort out "new notions of finiteness" building on earlier work of @Saransh-cpp and @laMudri and going all the way back to #863 ...