This one is also going to benefit from the `Hole` refactoring. I wonder whether the subtyping check (or the corresponding function) is going to be necessary at all (apart from the implementation of Hole).