_Originally posted by @nicolasstucki in https://github.com/lampepfl/dotty/pull/11269#discussion_r567776495_