Consider the stage of typeable evidence when checking stage restrictionwip/t21547

We were considering all Typeable evidence to be "BuiltinInstance"s which
meant the stage restriction was going unchecked. In-fact, typeable has
evidence and so we need to apply the stage restriction.

This is
complicated by the fact we don't generate typeable evidence and the
corresponding DFunIds until after typechecking is concluded so we
introcue a new `InstanceWhat` constructor, BuiltinTypeableInstance which
records whether the evidence is going to be local or not.

Fixes #21547

7 files changed, 130 insertions, 21 deletions

diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index df7046c4fd..50a13ba901 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -33,6 +33,7 @@ import GHC.Types.SafeHaskell
 import GHC.Types.Name   ( Name, pprDefinedAt )
 import GHC.Types.Var.Env ( VarEnv )
 import GHC.Types.Id
+import GHC.Types.Var
 
 import GHC.Core.Predicate
 import GHC.Core.InstEnv
@@ -96,13 +97,22 @@ data ClsInstResult
 
   | NotSure      -- Multiple matches and/or one or more unifiers
 
-data InstanceWhat
-  = BuiltinInstance
-  | BuiltinEqInstance   -- A built-in "equality instance"; see the
-                        -- GHC.Tc.Solver.InertSet Note [Solved dictionaries]
-  | LocalInstance
-  | TopLevInstance { iw_dfun_id   :: DFunId
-                   , iw_safe_over :: SafeOverlapping }
+data InstanceWhat  -- How did we solve this constraint?
+  = BuiltinEqInstance    -- Built-in solver for (t1 ~ t2), (t1 ~~ t2), Coercible t1 t2
+                         -- See GHC.Tc.Solver.InertSet Note [Solved dictionaries]
+
+  | BuiltinTypeableInstance TyCon   -- Built-in solver for Typeable (T t1 .. tn)
+                         -- See Note [Well-staged instance evidence]
+
+  | BuiltinInstance      -- Built-in solver for (C t1 .. tn) where C is
+                         --   KnownNat, .. etc (classes with no top-level evidence)
+
+  | LocalInstance        -- Solved by a quantified constraint
+                         -- See GHC.Tc.Solver.InertSet Note [Solved dictionaries]
+
+  | TopLevInstance       -- Solved by a top-level instance decl
+      { iw_dfun_id   :: DFunId
+      , iw_safe_over :: SafeOverlapping }
 
 instance Outputable ClsInstResult where
   ppr NoInstance = text "NoInstance"
@@ -113,6 +123,7 @@ instance Outputable ClsInstResult where
 
 instance Outputable InstanceWhat where
   ppr BuiltinInstance   = text "a built-in instance"
+  ppr BuiltinTypeableInstance {} = text "a built-in typeable instance"
   ppr BuiltinEqInstance = text "a built-in equality instance"
   ppr LocalInstance     = text "a locally-quantified instance"
   ppr (TopLevInstance { iw_dfun_id = dfun })
@@ -127,6 +138,7 @@ instanceReturnsDictCon :: InstanceWhat -> Bool
 -- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
 instanceReturnsDictCon (TopLevInstance {}) = True
 instanceReturnsDictCon BuiltinInstance     = True
+instanceReturnsDictCon BuiltinTypeableInstance {} = True
 instanceReturnsDictCon BuiltinEqInstance   = False
 instanceReturnsDictCon LocalInstance       = False
 
@@ -462,9 +474,10 @@ doFunTy clas ty mult arg_ty ret_ty
 doTyConApp :: Class -> Type -> TyCon -> [Kind] -> TcM ClsInstResult
 doTyConApp clas ty tc kind_args
   | tyConIsTypeable tc
-  = return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args)
-                     , cir_mk_ev     = mk_ev
-                     , cir_what      = BuiltinInstance }
+  = do
+     return $ OneInst { cir_new_theta = (map (mk_typeable_pred clas) kind_args)
+                      , cir_mk_ev     = mk_ev
+                      , cir_what      = BuiltinTypeableInstance tc }
   | otherwise
   = return NoInstance
   where
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index bac38d8f0a..7323585dc2 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -2216,7 +2216,7 @@ chooseInstance work_item lookup_res
   = pprPanic "chooseInstance" (ppr work_item $$ ppr lookup_res)
 
 checkInstanceOK :: CtLoc -> InstanceWhat -> TcPredType -> TcS CtLoc
--- Check that it's OK to use this insstance:
+-- Check that it's OK to use this instance:
 --    (a) the use is well staged in the Template Haskell sense
 -- Returns the CtLoc to used for sub-goals
 -- Probably also want to call checkReductionDepth
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 26af2ff689..8721068b8c 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -150,7 +150,7 @@ import GHC.Types.Error ( mkPlainError, noHints )
 
 import GHC.Types.Name
 import GHC.Types.TyThing
-import GHC.Unit.Module ( HasModule, getModule )
+import GHC.Unit.Module ( HasModule, getModule, extractModule )
 import GHC.Types.Name.Reader ( GlobalRdrEnv, GlobalRdrElt )
 import qualified GHC.Rename.Env as TcM
 import GHC.Types.Var
@@ -1385,18 +1385,84 @@ checkWellStagedDFun :: CtLoc -> InstanceWhat -> PredType -> TcS ()
 -- Here we can't use the equality function from the instance in the splice
 
 checkWellStagedDFun loc what pred
-  | TopLevInstance { iw_dfun_id = dfun_id } <- what
-  , let bind_lvl = TcM.topIdLvl dfun_id
-  , bind_lvl > impLevel
-  = wrapTcS $ TcM.setCtLocM loc $
-    do { use_stage <- TcM.getStage
-       ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
-
-  | otherwise
-  = return ()    -- Fast path for common case
+  = do
+      mbind_lvl <- checkWellStagedInstanceWhat what
+      case mbind_lvl of
+        Just bind_lvl | bind_lvl > impLevel ->
+          wrapTcS $ TcM.setCtLocM loc $ do
+              { use_stage <- TcM.getStage
+              ; TcM.checkWellStaged pp_thing bind_lvl (thLevel use_stage) }
+        _ ->
+          return ()
   where
     pp_thing = text "instance for" <+> quotes (ppr pred)
 
+-- | Returns the ThLevel of evidence for the solved constraint (if it has evidence)
+-- See Note [Well-staged instance evidence]
+checkWellStagedInstanceWhat :: InstanceWhat -> TcS (Maybe ThLevel)
+checkWellStagedInstanceWhat what
+  | TopLevInstance { iw_dfun_id = dfun_id } <- what
+    = return $ Just (TcM.topIdLvl dfun_id)
+  | BuiltinTypeableInstance tc <- what
+    = do
+        cur_mod <- extractModule <$> getGblEnv
+        return $ Just (if nameIsLocalOrFrom cur_mod (tyConName tc)
+                        then outerLevel
+                        else impLevel)
+  | otherwise = return Nothing
+
+{-
+Note [Well-staged instance evidence]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Evidence for instances must obey the same level restrictions as normal bindings.
+In particular, it is forbidden to use an instance in a top-level splice in the
+module which the instance is defined. This is because the evidence is bound at
+the top-level and top-level definitions are forbidden from being using in top-level splices in
+the same module.
+
+For example, suppose you have a function..  foo :: Show a => Code Q a -> Code Q ()
+then the following program is disallowed,
+
+```
+data T a = T a deriving (Show)
+
+main :: IO ()
+main =
+  let x = $$(foo [|| T () ||])
+  in return ()
+```
+
+because the `foo` function (used in a top-level splice) requires `Show T` evidence,
+which is defined at the top-level and therefore fails with an error that we have violated
+the stage restriction.
+
+```
+Main.hs:12:14: error:
+    • GHC stage restriction:
+        instance for ‘Show
+                        (T ())’ is used in a top-level splice, quasi-quote, or annotation,
+        and must be imported, not defined locally
+    • In the expression: foo [|| T () ||]
+      In the Template Haskell splice $$(foo [|| T () ||])
+      In the expression: $$(foo [|| T () ||])
+   |
+12 |   let x = $$(foo [|| T () ||])
+   |
+```
+
+Solving a `Typeable (T t1 ...tn)` constraint generates code that relies on
+`$tcT`, the `TypeRep` for `T`; and we must check that this reference to `$tcT`
+is well staged.  It's easy to know the stage of `$tcT`: for imported TyCons it
+will be `impLevel`, and for local TyCons it will be `toplevel`.
+
+Therefore the `InstanceWhat` type had to be extended with
+a special case for `Typeable`, which recorded the TyCon the evidence was for and
+could them be used to check that we were not attempting to evidence in a stage incorrect
+manner.
+
+-}
+
 pprEq :: TcType -> TcType -> SDoc
 pprEq ty1 ty2 = pprParendType ty1 <+> char '~' <+> pprParendType ty2
 
diff --git a/testsuite/tests/th/T21547.hs b/testsuite/tests/th/T21547.hs
new file mode 100644
index 0000000000..99b9992c59
--- /dev/null
+++ b/testsuite/tests/th/T21547.hs
@@ -0,0 +1,11 @@
+{-# LANGUAGE TemplateHaskell #-}
+module T21547 where
+import T21547A
+
+data T a = T a deriving (Show)
+
+main :: IO ()
+main = do
+  let x = $$(foo [|| T () ||])
+  let y = $$(foo [|| F () ||])
+  return ()
diff --git a/testsuite/tests/th/T21547.stderr b/testsuite/tests/th/T21547.stderr
new file mode 100644
index 0000000000..a37b98aa85
--- /dev/null
+++ b/testsuite/tests/th/T21547.stderr
@@ -0,0 +1,9 @@
+
+T21547.hs:9:14: error:
+    • GHC stage restriction:
+        instance for ‘base-4.16.0.0:Data.Typeable.Internal.Typeable
+                        T’ is used in a top-level splice, quasi-quote, or annotation,
+        and must be imported, not defined locally
+    • In the expression: foo [|| T () ||]
+      In the Template Haskell splice $$(foo [|| T () ||])
+      In the expression: $$(foo [|| T () ||])
diff --git a/testsuite/tests/th/T21547A.hs b/testsuite/tests/th/T21547A.hs
new file mode 100644
index 0000000000..19b47f8987
--- /dev/null
+++ b/testsuite/tests/th/T21547A.hs
@@ -0,0 +1,9 @@
+module T21547A where
+
+import Data.Typeable
+import Language.Haskell.TH
+
+foo :: Typeable a => Code Q a -> Code Q ()
+foo = undefined
+
+data F a = F a deriving (Show)
diff --git a/testsuite/tests/th/all.T b/testsuite/tests/th/all.T
index ec79e19249..7147fa4182 100644
--- a/testsuite/tests/th/all.T
+++ b/testsuite/tests/th/all.T
@@ -543,6 +543,7 @@ test('T17820c', normal, compile_fail, [''])
 test('T17820d', normal, compile_fail, [''])
 test('T17820e', normal, compile_fail, [''])
 test('T20454', normal, compile_and_run, [''])
+test('T21547', [extra_files(['T21547A.hs'])], multimod_compile_fail, ['T21547', '-v0'])
 test('T20590', normal, compile, ['-v0 -ddump-splices -dsuppress-uniques'])
 test('T20773', only_ways(['ghci']), ghci_script, ['T20773.script'])
 test('T20884', normal, compile_fail, [''])