I feel your pain. Not only is the API hard to use, it is a footgun, too.
Regarding exhaustivity, though, I don’t think you can hope for exhaustive pattern matches, unless you freeze the language. If you pattern-matching on user-provided code, I think you have to settle for supporting a only defined subset of code constructs, and try to give a helpful error message otherwise.
Regarding the current design of Quotes as a module with type definitions inside, one can legitimately question, as you do, whether it does not cause more problems than it solves. I’d even say that your example of
final class Logic3(using val quotes: Quotes) {
val types: Types2[quotes.type] = Types2(using quotes)
is still rather mild in terms of how complex things can get.
However, my preferred solution would be to improve usability of this sort of modular programming, as it would be useful much more broadly than just the Quotes API. There are some ideas in this thread.