This has caught a couple of things in the Idris 2 code base itself. Some tests needed partial annotations too.