This all seems to be solidifying nicely. From my perspective, I didn't really like the original proposal, but am now in favor of where it has evolved -- with all imports declared at the top, and then adding `import ...` to the syntax of local declarations. I'm not sure where the trouble around instances comes from in this idea, though. Even if a module is imported qualified, all of its instances are available anywhere, and I don't see that changing here. As Edward said, this would just be a small change in the renamer.