Code: ```haskell {-# LANGUAGE ExplicitLevelImports #-} module N where a = True ``` ```haskell {-# LANGUAGE ExplicitLevelImports, TemplateHaskell #-} module M where import N import Language.Haskell.TH.Syntax x :: Q Exp x = [| a |] ``` The code in `M` compiles. Because we didn't quote-import N, we do not have access to `a` in the quote `[|| a ||]`. The level mismatch is resolved by using lift: the definition of `x` is equivalent to `x = lift a`. Let's now change `import N` to `import splice N`. Then, unexpectedly, `x` still compiles to a lift, even though that should be a level error. Writing `x = lift a` explicitly correctly fails. In other words, GHC should check that an implicit lift goes one level up, and not just any positive amount.