It seems that we don't refine the set of levels a name is available from based on its qualification, e.g. the following is allowed: ```hs import quote Data.Maybe qualified as Q import Data.Maybe qualified as Z import splice Data.Maybe qualified as S foo = S.isJust ``` Here we determine that `isJust` is available at levels `{-1,0,1}` and accept this program, even though `S.isJust` specifically refers to the splice import, so that it should be unavailable at level 0. I didn't see any discussion of the interaction of qualified names with level checks in [the ExplicitLevelImports GHC proposal](https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0682-explicit-level-imports.rst), so I assume this is simply an oversight of the implementation.