Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC Commits: c64cca1e by mangoiv at 2026-02-03T15:59:29-05:00 ExplicitLevelImports: check staging for types just like for values Previously, imported types were entirely exempted from staging checks as the implicit stage persistance assumed to be all imported types to be well staged. ExplicitLevelImports' change specification, however, does not do such an exemption. Thus we want to introduce such a check, just like we have for values. ExplicitLevelImports does not, however, talk about local names - from its perspective, we could theoretically keep treating locally introduced types specially - e.g. an ill-staged used in a quote would only emit a warning, not an error. To allow for a potential future migration away from such wrinkles as the staging check in notFound (see Note [Out of scope might be a staging error]) we consistently do the strict staging check that we also do for value if ExplicitLevelImports is on. Closes #26098 - - - - - 11 changed files: - compiler/GHC/Rename/HsType.hs - compiler/GHC/Rename/Splice.hs-boot - + testsuite/tests/th/T26098A_quote.hs - + testsuite/tests/th/T26098A_splice.hs - + testsuite/tests/th/T26098_local.hs - + testsuite/tests/th/T26098_local.stderr - + testsuite/tests/th/T26098_quote.hs - + testsuite/tests/th/T26098_quote.stderr - + testsuite/tests/th/T26098_splice.hs - + testsuite/tests/th/T26098_splice.stderr - testsuite/tests/th/all.T Changes: ===================================== compiler/GHC/Rename/HsType.hs ===================================== @@ -1,4 +1,5 @@ {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE MultiWayIf #-} {- (c) The GRASP/AQUA Project, Glasgow University, 1992-1998 @@ -42,7 +43,7 @@ module GHC.Rename.HsType ( import GHC.Prelude -import {-# SOURCE #-} GHC.Rename.Splice( rnSpliceType, checkThLocalTyName ) +import {-# SOURCE #-} GHC.Rename.Splice( rnSpliceType, checkThLocalTyName, checkThLocalNameNoLift ) import GHC.Core.TyCo.FVs ( tyCoVarsOfTypeList ) import GHC.Core.TyCon ( isKindName ) @@ -537,10 +538,18 @@ rnHsTyKi env tv@(HsTyVar _ ip (L loc rdr_name)) -- of PolyKinds (see #14710) ; name <- rnTyVar env rdr_name ; this_mod <- getModule - ; when (nameIsLocalOrFrom this_mod name) $ - checkThLocalTyName name + ; explicit_level_imports <- xoptM LangExt.ExplicitLevelImports + ; let loc_name_with_rdr = L loc $ WithUserRdr rdr_name name + ; if | explicit_level_imports + -- See Note [Strict level checks with ExplicitLevelImports] + -> checkThLocalNameNoLift loc_name_with_rdr + + | nameIsLocalOrFrom this_mod name + -> checkThLocalTyName name + + | otherwise -> pure () ; checkPromotedDataConName env tv Prefix ip name - ; return (HsTyVar noAnn ip (L loc $ WithUserRdr rdr_name name), unitFV name) } + ; return (HsTyVar noAnn ip loc_name_with_rdr, unitFV name) } rnHsTyKi env ty@(HsOpTy _ prom ty1 l_op ty2) = setSrcSpan (getLocA l_op) $ @@ -685,6 +694,37 @@ rnHsTyLit tyLit@(HsNumTy x i) = do pure (HsNumTy x i) rnHsTyLit (HsCharTy x c) = pure (HsCharTy x c) +{- +Note [Strict level checks with ExplicitLevelImports] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Since the proposed change specification of `ExplicitLevelImports` [1] talks about +all identifiers as if they were created equally in the context of TemplateHaskell, +we want to adhere to that specification and at the same time use this unique +chance of being able to guard the "correct" behaviour behind an extension, without +breaking too many users. That is why, if ExplicitLevelImports is on, we +- do not allow non-well-levelled types to be imported +- do not allow locally defined type names to be used in an ill-levelled way, more + most importantly, we do not allow locally defined names to be used in quotes. + +When doing level checks, we historically have been glancing over some +not-well-levelled programs - e.g. the following program was historically +accepted from the perspective of the stage restriction: + +type T = ExpQ +x = $(_ :: T) + +However, when type-checking the splice `$(_ :: T)`, we found that `T` +had not yet been made part of the type-checking environment - we would +insert an ad-hoc check in `notFound` which would report the staging error. + +See Note [Out of scope might be a staging error] + +This is obviously not very rigorous - our "specification" of a program +being well-staged becomes "if the type checker needs the thing to be in scope +and it is not, the program is not well-staged, otherwise it is". + +[1]: https://github.com/ghc-proposals/ghc-proposals/blob/8e4d0e9340c04b904373f9df... +-} rnHsMultAnnWith :: (LocatedA (mult GhcPs) -> RnM (LocatedA (mult GhcRn), FreeVars)) -> HsMultAnnOf (LocatedA (mult GhcPs)) GhcPs ===================================== compiler/GHC/Rename/Splice.hs-boot ===================================== @@ -16,3 +16,5 @@ rnSpliceDecl :: SpliceDecl GhcPs -> RnM (SpliceDecl GhcRn, FreeVars) rnTopSpliceDecls :: HsUntypedSplice GhcPs -> RnM ([LHsDecl GhcPs], FreeVars) checkThLocalTyName :: Name -> RnM () + +checkThLocalNameNoLift :: LIdOccP GhcRn -> RnM () ===================================== testsuite/tests/th/T26098A_quote.hs ===================================== @@ -0,0 +1,4 @@ +module T26098A_quote where + +data T = MkT + ===================================== testsuite/tests/th/T26098A_splice.hs ===================================== @@ -0,0 +1,7 @@ +module T26098A_splice where + +import Language.Haskell.TH + +data T = MkT + +type Foo = ExpQ ===================================== testsuite/tests/th/T26098_local.hs ===================================== @@ -0,0 +1,32 @@ +{-# LANGUAGE ExplicitLevelImports #-} +module T26098_local where + +import Language.Haskell.TH +import Data.Char +import Data.Proxy + +tardy :: forall a. Proxy a -> IO Type +tardy _ = [t| a |] + +tardy2 :: forall a. Proxy a -> IO Exp +tardy2 _ = [| id @a |] + +tardy3 :: forall a. Proxy a -> Code IO (a -> a) +tardy3 _ = [|| id @a ||] + +main :: IO () +main = do + tardy (Proxy @Int) >>= putStrLn . filt . show + tardy2 (Proxy @Int) >>= putStrLn . filt . show + examineCode (tardy3 (Proxy @Int)) >>= putStrLn . filt . show . unType + +-- ad-hoc filter uniques, a_12313 -> a +filt :: String -> String +filt = go where + go [] = [] + go ('_' : rest) = go (dropWhile isDigit rest) + go (c:cs) = c : go cs + +type T = ExpQ + +blup = $(3 :: T) ===================================== testsuite/tests/th/T26098_local.stderr ===================================== @@ -0,0 +1,16 @@ +T26098_local.hs:9:15: error: [GHC-28914] + • Level error: ‘a’ is bound at level 0 but used at level 1 + • In the Template Haskell quotation: [t| a |] + +T26098_local.hs:12:19: error: [GHC-28914] + • Level error: ‘a’ is bound at level 0 but used at level 1 + • In the Template Haskell quotation: [| id @a |] + +T26098_local.hs:15:20: error: [GHC-28914] + • Level error: ‘a’ is bound at level 0 but used at level 1 + • In the Template Haskell typed quotation: [|| id @a ||] + +T26098_local.hs:32:15: error: [GHC-28914] + • Level error: ‘T’ is bound at level 0 but used at level -1 + • In the untyped splice: $(3 :: T) + ===================================== testsuite/tests/th/T26098_quote.hs ===================================== @@ -0,0 +1,12 @@ +{-# LANGUAGE ExplicitLevelImports, DataKinds, TemplateHaskell #-} +module T26098_quote where + +import splice T26098A_quote +import T26098A_quote +import Language.Haskell.TH + +c :: Q Type +c = [t|T|] + +d :: Q Type +d = [t|'MkT|] ===================================== testsuite/tests/th/T26098_quote.stderr ===================================== @@ -0,0 +1,14 @@ +T26098_quote.hs:9:8: error: [GHC-28914] + • Level error: ‘T’ is bound at levels {-1, 0} but used at level 1 + • Available from the imports: + • imported from ‘T26098A_quote’ at T26098_quote.hs:5:1-20 + • imported from ‘T26098A_quote’ at -1 at T26098_quote.hs:4:1-27 + • In the Template Haskell quotation: [t| T |] + +T26098_quote.hs:12:8: error: [GHC-28914] + • Level error: ‘MkT’ is bound at levels {-1, 0} but used at level 1 + • Available from the imports: + • imported from ‘T26098A_quote’ at T26098_quote.hs:5:1-20 + • imported from ‘T26098A_quote’ at -1 at T26098_quote.hs:4:1-27 + • In the Template Haskell quotation: [t| 'MkT |] + ===================================== testsuite/tests/th/T26098_splice.hs ===================================== @@ -0,0 +1,9 @@ +{-# LANGUAGE ExplicitLevelImports, TemplateHaskell #-} +module T26098_splice where + +import T26098A_splice +import quote T26098A_splice + +import splice Prelude + +x = $(undefined :: Foo) ===================================== testsuite/tests/th/T26098_splice.stderr ===================================== @@ -0,0 +1,7 @@ +T26098_splice.hs:9:20: error: [GHC-28914] + • Level error: ‘Foo’ is bound at levels {0, 1} but used at level -1 + • Available from the imports: + • imported from ‘T26098A_splice’ at 1 at T26098_splice.hs:5:1-27 + • imported from ‘T26098A_splice’ at T26098_splice.hs:4:1-21 + • In the untyped splice: $(undefined :: Foo) + ===================================== testsuite/tests/th/all.T ===================================== @@ -624,6 +624,9 @@ test('T24997', normal, compile_and_run, ['']) test('T25256', normal, compile_and_run, ['']) test('T24572a', normal, compile, ['']) test('T24572b', normal, compile_fail, ['']) +test('T26098_splice', [extra_files(['T26098A_splice.hs'])], multimod_compile_fail, ['T26098_splice', '-v0 ' + config.ghc_th_way_flags]) +test('T26098_quote', [extra_files(['T26098A_quote.hs'])], multimod_compile_fail, ['T26098_quote', '-v0 ' + config.ghc_th_way_flags]) +test('T26098_local', normal, compile_fail, ['']) test('T24572c', normal, compile_fail, ['']) test('T26568', normal, compile_fail, ['']) test('T24572d', normal, compile, ['']) View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c64cca1ef667751c02ce2eb4141349e6... -- View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/c64cca1ef667751c02ce2eb4141349e6... You're receiving this email because of your account on gitlab.haskell.org.