This is very like the example I concocted for the relevant educational note, which was recently discussed in another thread. The note needs to be updated for the implicitly opened existentials feature (or rather, a different version needs to be written for the new diagnostics), and that should be tracked by a GitHub issue—contributions welcome!