Three improvements to Template Haskell (fixes #3467)

This patch implements three significant improvements to Template Haskell.
  
Declaration-level splices with no "$" 
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
This change simply allows you to omit the "$(...)" wrapper for 
declaration-level TH splices.  An expression all by itself is
not legal, so we now treat it as a TH splice.  Thus you can now
say
	data T = T1 | T2
 	deriveMyStuff ''T

where deriveMyStuff :: Name -> Q [Dec]
This makes a much nicer interface for clients of libraries that use
TH: no scary $(deriveMyStuff ''T).

Nested top-level splices
~~~~~~~~~~~~~~~~~~~~~~~~
Previously TH would reject this, saying that splices cannot be nested:
	f x = $(g $(h 'x))
But there is no reason for this not to work.  First $(h 'x) is run,
yielding code <blah> that is spliced instead of the $(h 'x). Then (g
<blah>) is typechecked and run, yielding code that replaces the
$(g ...) splice.  

So this simply lifts the restriction.

Fix Trac #3467: non-top-level type splices
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

It appears that when I added the ability to splice types in TH
programs, I failed to pay attention to non-top-level splices -- that
is, splices inside quotatation brackets.  

This patch fixes the problem.  I had to modify HsType, so there's a
knock-on change to Haddock.

Its seems that a lot of lines of code has changed, but almost all the
new lines are comments!

General tidying up
~~~~~~~~~~~~~~~~~~
As a result of thinking all this out I re-jigged the data type ThStage,
which had far too many values before.  And I wrote a nice state transition
diagram to make it all precise; 
   see Note [Template Haskell state diagram] in TcSplice

Lots more refactoring in TcSplice, resulting in significantly less code.
(A few more lines, but actually less code -- the rest is comments.)

I think the result is significantly cleaner.

15 files changed, 480 insertions, 356 deletions

diff --git a/compiler/deSugar/DsMeta.hs b/compiler/deSugar/DsMeta.hs
index 411da4074c..162e90fa01 100644
--- a/compiler/deSugar/DsMeta.hs
+++ b/compiler/deSugar/DsMeta.hs
@@ -587,43 +587,44 @@ repTy (HsForAllTy _ tvs ctxt ty)  =
     repTForall bndrs1 ctxt1 ty1
 
 repTy (HsTyVar n)
-  | isTvOcc (nameOccName n)       = do 
-				      tv1 <- lookupTvOcc n
-				      repTvar tv1
-  | otherwise		          = do 
-				      tc1 <- lookupOcc n
-				      repNamedTyCon tc1
-repTy (HsAppTy f a)               = do 
-				      f1 <- repLTy f
-				      a1 <- repLTy a
-				      repTapp f1 a1
-repTy (HsFunTy f a)               = do 
-				      f1   <- repLTy f
-				      a1   <- repLTy a
-				      tcon <- repArrowTyCon
-				      repTapps tcon [f1, a1]
-repTy (HsListTy t)		  = do
-				      t1   <- repLTy t
-				      tcon <- repListTyCon
-				      repTapp tcon t1
-repTy (HsPArrTy t)                = do
-				      t1   <- repLTy t
-				      tcon <- repTy (HsTyVar (tyConName parrTyCon))
-				      repTapp tcon t1
-repTy (HsTupleTy _ tys)	  = do
-				      tys1 <- repLTys tys 
-				      tcon <- repTupleTyCon (length tys)
-				      repTapps tcon tys1
-repTy (HsOpTy ty1 n ty2) 	  = repLTy ((nlHsTyVar (unLoc n) `nlHsAppTy` ty1) 
-					   `nlHsAppTy` ty2)
-repTy (HsParTy t)  	       	  = repLTy t
-repTy (HsPredTy pred)             = repPredTy pred
-repTy (HsKindSig t k)             = do
-                                      t1 <- repLTy t
-                                      k1 <- repKind k
-                                      repTSig t1 k1
-repTy ty@(HsNumTy _)              = notHandled "Number types (for generics)" (ppr ty)
-repTy ty			  = notHandled "Exotic form of type" (ppr ty)
+  | isTvOcc (nameOccName n) = do 
+			        tv1 <- lookupTvOcc n
+			        repTvar tv1
+  | otherwise		    = do 
+			        tc1 <- lookupOcc n
+			        repNamedTyCon tc1
+repTy (HsAppTy f a)         = do 
+			        f1 <- repLTy f
+			        a1 <- repLTy a
+			        repTapp f1 a1
+repTy (HsFunTy f a)         = do 
+			        f1   <- repLTy f
+			        a1   <- repLTy a
+			        tcon <- repArrowTyCon
+			        repTapps tcon [f1, a1]
+repTy (HsListTy t)	    = do
+			        t1   <- repLTy t
+			        tcon <- repListTyCon
+			        repTapp tcon t1
+repTy (HsPArrTy t)          = do
+			        t1   <- repLTy t
+			        tcon <- repTy (HsTyVar (tyConName parrTyCon))
+			        repTapp tcon t1
+repTy (HsTupleTy _ tys)	    = do
+			        tys1 <- repLTys tys 
+			        tcon <- repTupleTyCon (length tys)
+			        repTapps tcon tys1
+repTy (HsOpTy ty1 n ty2)    = repLTy ((nlHsTyVar (unLoc n) `nlHsAppTy` ty1) 
+			    	   `nlHsAppTy` ty2)
+repTy (HsParTy t)  	    = repLTy t
+repTy (HsPredTy pred)       = repPredTy pred
+repTy (HsKindSig t k)       = do
+                                t1 <- repLTy t
+                                k1 <- repKind k
+                                repTSig t1 k1
+repTy (HsSpliceTy splice)   = repSplice splice
+repTy ty@(HsNumTy _)        = notHandled "Number types (for generics)" (ppr ty)
+repTy ty		    = notHandled "Exotic form of type" (ppr ty)
 
 -- represent a kind
 --
@@ -640,6 +641,21 @@ repKind ki
                                                         (ppr k)
 
 -----------------------------------------------------------------------------
+-- 		Splices
+-----------------------------------------------------------------------------
+
+repSplice :: HsSplice Name -> DsM (Core a)
+-- See Note [How brackets and nested splices are handled] in TcSplice
+-- We return a CoreExpr of any old type; the context should know
+repSplice (HsSplice n _) 
+ = do { mb_val <- dsLookupMetaEnv n
+       ; case mb_val of
+	   Just (Splice e) -> do { e' <- dsExpr e
+				 ; return (MkC e') }
+	   _ -> pprPanic "HsSplice" (ppr n) }
+			-- Should not happen; statically checked
+
+-----------------------------------------------------------------------------
 -- 		Expressions
 -----------------------------------------------------------------------------
 
@@ -742,14 +758,8 @@ repE (ArithSeq _ aseq) =
 			     ds2 <- repLE e2
 			     ds3 <- repLE e3
 			     repFromThenTo ds1 ds2 ds3
-repE (HsSpliceE (HsSplice n _)) 
-  = do { mb_val <- dsLookupMetaEnv n
-       ; case mb_val of
-		 Just (Splice e) -> do { e' <- dsExpr e
-				       ; return (MkC e') }
-		 _ -> pprPanic "HsSplice" (ppr n) }
-			-- Should not happen; statically checked
 
+repE (HsSpliceE splice)  = repSplice splice
 repE e@(PArrSeq {})      = notHandled "Parallel arrays" (ppr e)
 repE e@(HsCoreAnn {})    = notHandled "Core annotations" (ppr e)
 repE e@(HsSCC {})        = notHandled "Cost centres" (ppr e)
diff --git a/compiler/hsSyn/HsTypes.lhs b/compiler/hsSyn/HsTypes.lhs
index d3f5ce8578..797a8f28ea 100644
--- a/compiler/hsSyn/HsTypes.lhs
+++ b/compiler/hsSyn/HsTypes.lhs
@@ -159,6 +159,9 @@ data HsType name
 
   | HsDocTy             (LHsType name) LHsDocString -- A documented type
 
+  | HsSpliceTyOut       Kind		-- Used just like KindedTyVar, just between 
+					--   kcHsType and dsHsType
+
   | HsBangTy	HsBang (LHsType name)	-- Bang-style type annotations 
   | HsRecTy [ConDeclField name]	        -- Only in data type declarations
 
@@ -369,17 +372,18 @@ ppr_mono_ty ctxt_prec (HsForAllTy exp tvs ctxt ty)
   = maybeParen ctxt_prec pREC_FUN $
     sep [pprHsForAll exp tvs ctxt, ppr_mono_lty pREC_TOP ty]
 
-ppr_mono_ty _         (HsBangTy b ty)     = ppr b <> ppr ty
-ppr_mono_ty _         (HsRecTy flds)      = pprConDeclFields flds
-ppr_mono_ty _         (HsTyVar name)      = ppr name
-ppr_mono_ty ctxt_prec (HsFunTy ty1 ty2)   = ppr_fun_ty ctxt_prec ty1 ty2
-ppr_mono_ty _         (HsTupleTy con tys) = tupleParens con (interpp'SP tys)
-ppr_mono_ty _         (HsKindSig ty kind) = parens (ppr_mono_lty pREC_TOP ty <+> dcolon <+> pprKind kind)
-ppr_mono_ty _         (HsListTy ty)	  = brackets (ppr_mono_lty pREC_TOP ty)
-ppr_mono_ty _         (HsPArrTy ty)	  = pabrackets (ppr_mono_lty pREC_TOP ty)
-ppr_mono_ty _         (HsPredTy pred)     = ppr pred
-ppr_mono_ty _         (HsNumTy n)         = integer n  -- generics only
-ppr_mono_ty _         (HsSpliceTy s)      = pprSplice s
+ppr_mono_ty _    (HsBangTy b ty)     = ppr b <> ppr ty
+ppr_mono_ty _    (HsRecTy flds)      = pprConDeclFields flds
+ppr_mono_ty _    (HsTyVar name)      = ppr name
+ppr_mono_ty prec (HsFunTy ty1 ty2)   = ppr_fun_ty prec ty1 ty2
+ppr_mono_ty _    (HsTupleTy con tys) = tupleParens con (interpp'SP tys)
+ppr_mono_ty _    (HsKindSig ty kind) = parens (ppr_mono_lty pREC_TOP ty <+> dcolon <+> pprKind kind)
+ppr_mono_ty _    (HsListTy ty)	     = brackets (ppr_mono_lty pREC_TOP ty)
+ppr_mono_ty _    (HsPArrTy ty)	     = pabrackets (ppr_mono_lty pREC_TOP ty)
+ppr_mono_ty _    (HsPredTy pred)     = ppr pred
+ppr_mono_ty _    (HsNumTy n)         = integer n  -- generics only
+ppr_mono_ty _    (HsSpliceTy s)      = pprSplice s
+ppr_mono_ty _    (HsSpliceTyOut k)   = text "<splicety>" <> dcolon <> ppr k
 
 ppr_mono_ty ctxt_prec (HsAppTy fun_ty arg_ty)
   = maybeParen ctxt_prec pREC_CON $
diff --git a/compiler/parser/Lexer.x b/compiler/parser/Lexer.x
index 9a79b5b665..675b4d6fc0 100644
--- a/compiler/parser/Lexer.x
+++ b/compiler/parser/Lexer.x
@@ -542,7 +542,7 @@ data Token
   | ITprimfloat  Rational
   | ITprimdouble Rational
 
-  -- MetaHaskell extension tokens
+  -- Template Haskell extension tokens
   | ITopenExpQuote  		--  [| or [e|
   | ITopenPatQuote		--  [p|
   | ITopenDecQuote		--  [d|
diff --git a/compiler/parser/Parser.y.pp b/compiler/parser/Parser.y.pp
index 6dbb49e981..bddb2bc346 100644
--- a/compiler/parser/Parser.y.pp
+++ b/compiler/parser/Parser.y.pp
@@ -262,9 +262,9 @@ incorrect.
  '{-# SCC'	   { L _ ITscc_prag }
  '{-# GENERATED'   { L _ ITgenerated_prag }
  '{-# DEPRECATED'  { L _ ITdeprecated_prag }
- '{-# WARNING'  { L _ ITwarning_prag }
+ '{-# WARNING'     { L _ ITwarning_prag }
  '{-# UNPACK'      { L _ ITunpack_prag }
- '{-# ANN'      { L _ ITann_prag }
+ '{-# ANN'         { L _ ITann_prag }
  '#-}'		   { L _ ITclose_prag }
 
  '..'		{ L _ ITdotdot }  			-- reserved symbols
@@ -559,17 +559,17 @@ topdecl :: { OrdList (LHsDecl RdrName) }
         | stand_alone_deriving                  { unitOL (LL (DerivD (unLoc $1))) }
 	| 'default' '(' comma_types0 ')'	{ unitOL (LL $ DefD (DefaultDecl $3)) }
 	| 'foreign' fdecl			{ unitOL (LL (unLoc $2)) }
-    | '{-# DEPRECATED' deprecations '#-}' { $2 }
-    | '{-# WARNING' warnings '#-}'        { $2 }
+        | '{-# DEPRECATED' deprecations '#-}' { $2 }
+        | '{-# WARNING' warnings '#-}'        { $2 }
 	| '{-# RULES' rules '#-}'		{ $2 }
 	| annotation { unitOL $1 }
       	| decl					{ unLoc $1 }
 
 	-- Template Haskell Extension
-	| '$(' exp ')'				{ unitOL (LL $ SpliceD (SpliceDecl $2)) }
-	| TH_ID_SPLICE				{ unitOL (LL $ SpliceD (SpliceDecl $
-							L1 $ HsVar (mkUnqual varName (getTH_ID_SPLICE $1))
-						  )) }
+	-- The $(..) form is one possible form of infixexp
+	-- but we treat an arbitrary expression just as if 
+	-- it had a $(..) wrapped around it
+	| infixexp 				{ unitOL (LL $ mkTopSpliceDecl $1) } 
 
 -- Type classes
 --
diff --git a/compiler/parser/RdrHsSyn.lhs b/compiler/parser/RdrHsSyn.lhs
index cacd14c27b..03ca542149 100644
--- a/compiler/parser/RdrHsSyn.lhs
+++ b/compiler/parser/RdrHsSyn.lhs
@@ -10,7 +10,7 @@ module RdrHsSyn (
  
 	mkHsOpApp, 
 	mkHsIntegral, mkHsFractional, mkHsIsString,
-	mkHsDo, mkHsSplice,
+	mkHsDo, mkHsSplice, mkTopSpliceDecl,
         mkClassDecl, mkTyData, mkTyFamily, mkTySynonym,
         splitCon, mkInlineSpec,	
 	mkRecConstrOrUpdate, -- HsExp -> [HsFieldUpdate] -> P HsExp
@@ -128,7 +128,8 @@ extract_lty (L loc ty) acc
       HsOpTy ty1 (L loc tv) ty2 -> extract_tv loc tv (extract_lty ty1 (extract_lty ty2 acc))
       HsParTy ty               	-> extract_lty ty acc
       HsNumTy _                 -> acc
-      HsSpliceTy _             	-> acc	-- Type splices mention no type variables
+      HsSpliceTy {}           	-> acc	-- Type splices mention no type variables
+      HsSpliceTyOut {}         	-> acc	-- Type splices mention no type variables
       HsKindSig ty _            -> extract_lty ty acc
       HsForAllTy _ [] cx ty     -> extract_lctxt cx (extract_lty ty acc)
       HsForAllTy _ tvs cx ty    -> acc ++ (filter ((`notElem` locals) . unLoc) $
@@ -223,6 +224,20 @@ mkTyFamily loc flavour lhs ksig
   = do { (tc, tparams) <- checkTyClHdr lhs
        ; tyvars <- checkTyVars tparams
        ; return (L loc (TyFamily flavour tc tyvars ksig)) }
+
+mkTopSpliceDecl :: LHsExpr RdrName -> HsDecl RdrName
+-- If the user wrote
+--	$(e)
+-- then that's the splice, but if she wrote, say,
+--      f x
+-- then behave as if she'd written
+--      $(f x)
+mkTopSpliceDecl expr
+  = SpliceD (SpliceDecl expr')
+  where
+    expr' = case expr of
+              (L _ (HsSpliceE (HsSplice _ expr))) -> expr
+              _other                              -> expr
 \end{code}
 
 %************************************************************************
diff --git a/compiler/rename/RnHsSyn.lhs b/compiler/rename/RnHsSyn.lhs
index 7d78536266..5fbe7f7eed 100644
--- a/compiler/rename/RnHsSyn.lhs
+++ b/compiler/rename/RnHsSyn.lhs
@@ -68,7 +68,8 @@ extractHsTyNames ty
     get (HsRecTy flds)         = extractHsTyNames_s (map cd_fld_type flds)
     get (HsNumTy _)            = emptyNameSet
     get (HsTyVar tv)           = unitNameSet tv
-    get (HsSpliceTy _)         = emptyNameSet   -- Type splices mention no type variables
+    get (HsSpliceTy {})        = emptyNameSet   -- Type splices mention no type variables
+    get (HsSpliceTyOut {})     = emptyNameSet   -- Ditto
     get (HsKindSig ty _)       = getl ty
     get (HsForAllTy _ tvs
                     ctxt ty)   = (extractHsCtxtTyNames ctxt
diff --git a/compiler/rename/RnTypes.lhs b/compiler/rename/RnTypes.lhs
index 61c039cc22..62b778d5f8 100644
--- a/compiler/rename/RnTypes.lhs
+++ b/compiler/rename/RnTypes.lhs
@@ -191,6 +191,8 @@ rnHsType doc (HsDocTy ty haddock_doc) = do
     haddock_doc' <- rnLHsDoc haddock_doc
     return (HsDocTy ty' haddock_doc')
 
+rnHsType _ (HsSpliceTyOut {}) = panic "rnHsType"
+
 rnLHsTypes :: SDoc -> [LHsType RdrName]
            -> IOEnv (Env TcGblEnv TcLclEnv) [LHsType Name]
 rnLHsTypes doc tys = mapM (rnLHsType doc) tys
diff --git a/compiler/typecheck/Inst.lhs b/compiler/typecheck/Inst.lhs
index 4f2dfabfab..a45422adb3 100644
--- a/compiler/typecheck/Inst.lhs
+++ b/compiler/typecheck/Inst.lhs
@@ -867,7 +867,7 @@ lookupSimpleInst (Dict {tci_pred = pred, tci_loc = loc})
 
     { use_stage <- getStage
     ; checkWellStaged (ptext (sLit "instance for") <+> quotes (ppr pred))
-    		      (topIdLvl dfun_id) use_stage
+    		      (topIdLvl dfun_id) (thLevel use_stage)
 
  	-- It's possible that not all the tyvars are in
 	-- the substitution, tenv. For example:
diff --git a/compiler/typecheck/TcEnv.lhs b/compiler/typecheck/TcEnv.lhs
index df6eac119c..f9a9179cbd 100644
--- a/compiler/typecheck/TcEnv.lhs
+++ b/compiler/typecheck/TcEnv.lhs
@@ -38,7 +38,7 @@ module TcEnv(
 	tcGetGlobalTyVars,
 
 	-- Template Haskell stuff
-	checkWellStaged, spliceOK, bracketOK, tcMetaTy, thLevel, 
+	checkWellStaged, tcMetaTy, thLevel, 
 	topIdLvl, thTopLevelId, thRnBrack, isBrackStage,
 
 	-- New Ids
@@ -526,41 +526,25 @@ tcExtendRules lcl_rules thing_inside
 %************************************************************************
 
 \begin{code}
-instance Outputable ThStage where
-   ppr (Comp l)	     = text "Comp" <+> int l
-   ppr (Brack l _ _) = text "Brack" <+> int l
-   ppr (Splice l)    = text "Splice" <+> int l
-
-
-thLevel :: ThStage -> ThLevel
-thLevel (Comp l)      = l
-thLevel (Splice l)    = l
-thLevel (Brack l _ _) = l
-
-
 checkWellStaged :: SDoc		-- What the stage check is for
 		-> ThLevel 	-- Binding level (increases inside brackets)
-	        -> ThStage	-- Use stage
+	        -> ThLevel	-- Use stage
 		-> TcM ()	-- Fail if badly staged, adding an error
-checkWellStaged pp_thing bind_lvl use_stage
+checkWellStaged pp_thing bind_lvl use_lvl
   | use_lvl >= bind_lvl 	-- OK! Used later than bound
   = return ()			-- E.g.  \x -> [| $(f x) |]
 
-  | bind_lvl == topLevel	-- GHC restriction on top level splices
+  | bind_lvl == outerLevel	-- GHC restriction on top level splices
   = failWithTc $ 
     sep [ptext (sLit "GHC stage restriction:") <+>  pp_thing,
-	 nest 2 (ptext (sLit "is used in") <+> use_lvl_doc <> ptext (sLit ", and must be imported, not defined locally"))]
+	 nest 2 (vcat [ ptext (sLit "is used in a top-level splice or annotation,")
+                      , ptext (sLit ", and must be imported, not defined locally")])]
 
   | otherwise			-- Badly staged
   = failWithTc $ 		-- E.g.  \x -> $(f x)
     ptext (sLit "Stage error:") <+> pp_thing <+> 
 	hsep   [ptext (sLit "is bound at stage") <+> ppr bind_lvl,
 		ptext (sLit "but used at stage") <+> ppr use_lvl]
-  where
-    use_lvl = thLevel use_stage
-    use_lvl_doc | use_lvl == thLevel topStage    = ptext (sLit "a top-level splice")
-                | use_lvl == thLevel topAnnStage = ptext (sLit "an annotation")
-                | otherwise                      = panic "checkWellStaged"
 
 topIdLvl :: Id -> ThLevel
 -- Globals may either be imported, or may be from an earlier "chunk" 
@@ -572,19 +556,9 @@ topIdLvl :: Id -> ThLevel
 --	$( f x )
 -- By the time we are prcessing the $(f x), the binding for "x" 
 -- will be in the global env, not the local one.
-topIdLvl id | isLocalId id = topLevel
+topIdLvl id | isLocalId id = outerLevel
 	    | otherwise    = impLevel
 
--- Indicates the legal transitions on bracket( [| |] ).
-bracketOK :: ThStage -> Maybe ThLevel
-bracketOK (Brack _ _ _) = Nothing	-- Bracket illegal inside a bracket
-bracketOK stage         = Just (thLevel stage + 1)
-
--- Indicates the legal transitions on splice($).
-spliceOK :: ThStage -> Maybe ThLevel
-spliceOK (Splice _) = Nothing	-- Splice illegal inside splice
-spliceOK stage      = Just (thLevel stage - 1)
-
 tcMetaTy :: Name -> TcM Type
 -- Given the name of a Template Haskell data type, 
 -- return the type
diff --git a/compiler/typecheck/TcExpr.lhs b/compiler/typecheck/TcExpr.lhs
index 482baba4af..4ccd89c3a4 100644
--- a/compiler/typecheck/TcExpr.lhs
+++ b/compiler/typecheck/TcExpr.lhs
@@ -12,7 +12,9 @@
 --     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
 -- for details
 
-module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC, tcInferRho, tcInferRhoNC, tcSyntaxOp, addExprErrCtxt ) where
+module TcExpr ( tcPolyExpr, tcPolyExprNC, tcMonoExpr, tcMonoExprNC, 
+                tcInferRho, tcInferRhoNC, tcSyntaxOp, 
+                addExprErrCtxt ) where
 
 #include "HsVersions.h"
 
@@ -890,9 +892,10 @@ tcId orig fun_name res_ty
 tcSyntaxOp :: InstOrigin -> HsExpr Name -> TcType -> TcM (HsExpr TcId)
 -- Typecheck a syntax operator, checking that it has the specified type
 -- The operator is always a variable at this stage (i.e. renamer output)
+-- This version assumes ty is a monotype
 tcSyntaxOp orig (HsVar op) ty = tcId orig op ty
-tcSyntaxOp orig other 	   ty = pprPanic "tcSyntaxOp" (ppr other)
-
+tcSyntaxOp orig other 	   ty = pprPanic "tcSyntaxOp" (ppr other) 
+                        
 ---------------------------
 instFun :: InstOrigin
 	-> HsExpr TcId
@@ -1119,22 +1122,31 @@ lookupFun orig id_name
 
 #ifndef GHCI  /* GHCI and TH is off */
 --------------------------------------
--- thLocalId : Check for cross-stage lifting
-thLocalId orig id id_ty th_bind_lvl
+thLocalId :: InstOrigin -> Id -> TcType -> ThLevel -> TcM ()
+-- Check for cross-stage lifting
+thLocalId orig id id_ty bind_lvl
   = return ()
 
 #else	      /* GHCI and TH is on */
-thLocalId orig id id_ty th_bind_lvl 
+thLocalId orig id id_ty bind_lvl 
   = do	{ use_stage <- getStage	-- TH case
-	; case use_stage of
-	    Brack use_lvl ps_var lie_var | use_lvl > th_bind_lvl
-		  -> thBrackId orig id ps_var lie_var
-	    other -> do { checkWellStaged (quotes (ppr id)) th_bind_lvl use_stage
-			; return id }
-	}
+	; let use_lvl = thLevel use_stage
+	; checkWellStaged (quotes (ppr id)) bind_lvl use_lvl
+	; traceTc (text "thLocalId" <+> ppr id <+> ppr bind_lvl <+> ppr use_stage <+> ppr use_lvl)
+	; when (use_lvl > bind_lvl) $
+          checkCrossStageLifting orig id id_ty bind_lvl use_stage }
 
 --------------------------------------
-thBrackId orig id ps_var lie_var
+checkCrossStageLifting :: InstOrigin -> Id -> TcType -> ThLevel -> ThStage -> TcM ()
+-- We are inside brackets, and (use_lvl > bind_lvl)
+-- Now we must check whether there's a cross-stage lift to do
+-- Examples   \x -> [| x |]  
+--            [| map |]
+
+checkCrossStageLifting _ _ _ _ Comp   = return ()
+checkCrossStageLifting _ _ _ _ Splice = return ()
+
+checkCrossStageLifting orig id id_ty bind_lvl (Brack _ ps_var lie_var) 
   | thTopLevelId id
   =	-- Top-level identifiers in this module,
 	-- (which have External Names)
@@ -1146,9 +1158,10 @@ thBrackId orig id ps_var lie_var
 	-- But we do need to put f into the keep-alive
 	-- set, because after desugaring the code will
 	-- only mention f's *name*, not f itself.
-    do	{ keepAliveTc id; return id }
+    keepAliveTc id
 
-  | otherwise
+  | otherwise	-- bind_lvl = outerLevel presumably,
+		-- but the Id is not bound at top level
   = 	-- Nested identifiers, such as 'x' in
 	-- E.g. \x -> [| h x |]
 	-- We must behave as if the reference to x was
@@ -1158,8 +1171,7 @@ thBrackId orig id ps_var lie_var
 	-- If 'x' occurs many times we may get many identical
 	-- bindings of the same splice proxy, but that doesn't
 	-- matter, although it's a mite untidy.
-    do 	{ let id_ty = idType id
-	; checkTc (isTauTy id_ty) (polySpliceErr id)
+    do 	{ checkTc (isTauTy id_ty) (polySpliceErr id)
 	       -- If x is polymorphic, its occurrence sites might
 	       -- have different instantiations, so we can't use plain
 	       -- 'x' as the splice proxy name.  I don't know how to 
@@ -1183,7 +1195,7 @@ thBrackId orig id ps_var lie_var
 	; ps <- readMutVar ps_var
 	; writeMutVar ps_var ((idName id, nlHsApp (nlHsVar lift) (nlHsVar id)) : ps)
 
-	; return id }
+	; return () }
 #endif /* GHCI */
 \end{code}
 
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 91ef46fa0b..77fefc2dbc 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -415,9 +415,11 @@ kc_hs_type ty@(HsRecTy _)
 #ifdef GHCI	/* Only if bootstrapped */
 kc_hs_type (HsSpliceTy sp) = kcSpliceType sp
 #else
-kc_hs_type ty@(HsSpliceTy _) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
+kc_hs_type ty@(HsSpliceTy {}) = failWithTc (ptext (sLit "Unexpected type splice:") <+> ppr ty)
 #endif
 
+kc_hs_type (HsSpliceTyOut {}) = panic "kc_hs_type"	-- Should not happen at all
+
 -- remove the doc nodes here, no need to worry about the location since
 -- its the same for a doc node and it's child type node
 kc_hs_type (HsDocTy ty _)
@@ -612,11 +614,15 @@ ds_type (HsForAllTy _ tv_names ctxt ty)
     tau <- dsHsType ty
     return (mkSigmaTy tyvars theta tau)
 
-ds_type (HsSpliceTy {}) = panic "ds_type: HsSpliceTy"
-
 ds_type (HsDocTy ty _)  -- Remove the doc comment
   = dsHsType ty
 
+ds_type (HsSpliceTyOut kind) 
+  = do { kind' <- zonkTcKindToKind kind
+       ; newFlexiTyVarTy kind' }
+
+ds_type (HsSpliceTy {}) = panic "ds_type"
+
 dsHsTypes :: [LHsType Name] -> TcM [Type]
 dsHsTypes arg_tys = mapM dsHsType arg_tys
 \end{code}
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index cbc443f100..c011d20e69 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -22,7 +22,7 @@ module TcRnTypes(
 
 	-- Template Haskell
 	ThStage(..), topStage, topAnnStage, topSpliceStage,
-	ThLevel, impLevel, topLevel,
+	ThLevel, impLevel, outerLevel, thLevel,
 
 	-- Arrows
 	ArrowCtxt(NoArrowCtxt), newArrowScope, escapeArrowScope,
@@ -382,37 +382,55 @@ pass it inwards.
 -}
 
 ---------------------------
--- Template Haskell levels 
+-- Template Haskell stages and levels 
 ---------------------------
 
+data ThStage	-- See Note [Template Haskell state diagram] in TcSplice
+  = Splice	-- Top-level splicing
+		-- This code will be run *at compile time*;
+		--   the result replaces the splice
+		-- Binding level = 0
+ 
+  | Comp   	-- Ordinary Haskell code
+		-- Binding level = 1
+
+  | Brack  			-- Inside brackets 
+      ThStage 			--   Binding level = level(stage) + 1
+      (TcRef [PendingSplice])	--   Accumulate pending splices here
+      (TcRef LIE)		--     and type constraints here
+
+topStage, topAnnStage, topSpliceStage :: ThStage
+topStage       = Comp
+topAnnStage    = Splice
+topSpliceStage = Splice
+
+instance Outputable ThStage where
+   ppr Splice        = text "Splice"
+   ppr Comp	     = text "Comp"
+   ppr (Brack s _ _) = text "Brack" <> parens (ppr s)
+
 type ThLevel = Int	
-	-- Indicates how many levels of brackets we are inside
-	-- 	(always >= 0)
+        -- See Note [Template Haskell levels] in TcSplice
 	-- Incremented when going inside a bracket,
 	-- decremented when going inside a splice
 	-- NB: ThLevel is one greater than the 'n' in Fig 2 of the
 	--     original "Template meta-programming for Haskell" paper
 
-impLevel, topLevel :: ThLevel
-topLevel = 1	-- Things defined at top level of this module
+impLevel, outerLevel :: ThLevel
 impLevel = 0	-- Imported things; they can be used inside a top level splice
+outerLevel = 1	-- Things defined outside brackets
+-- NB: Things at level 0 are not *necessarily* imported.
+--	eg  $( \b -> ... )   here b is bound at level 0
 --
 -- For example: 
 --	f = ...
 --	g1 = $(map ...)		is OK
 --	g2 = $(f ...)		is not OK; because we havn't compiled f yet
 
-
-data ThStage
-  = Comp   ThLevel			-- Ordinary compiling, usually at level topLevel but annotations use a lower level
-  | Splice ThLevel 			-- Inside a splice
-  | Brack  ThLevel 			-- Inside brackets; 
-	   (TcRef [PendingSplice])	--   accumulate pending splices here
-	   (TcRef LIE)			--   and type constraints here
-topStage, topAnnStage, topSpliceStage :: ThStage
-topStage       = Comp topLevel
-topAnnStage    = Comp (topLevel - 1)
-topSpliceStage = Splice (topLevel - 1)	-- Stage for the body of a top-level splice
+thLevel :: ThStage -> ThLevel
+thLevel Splice        = 0
+thLevel Comp          = 1
+thLevel (Brack s _ _) = thLevel s + 1
 
 ---------------------------
 -- Arrow-notation context
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index e864b05f42..2ad5b2fefb 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -17,8 +17,6 @@ module TcSimplify (
 	tcSimplifyDeriv, tcSimplifyDefault,
 	bindInstsOfLocalFuns, 
 	
-        tcSimplifyStagedExpr,
-
         misMatchMsg
     ) where
 
@@ -3057,25 +3055,6 @@ tcSimplifyDefault theta = do
     doc = ptext (sLit "default declaration")
 \end{code}
 
-@tcSimplifyStagedExpr@ performs a simplification but does so at a new
-stage. This is used when typechecking annotations and splices.
-
-\begin{code}
-
-tcSimplifyStagedExpr :: ThStage -> TcM a -> TcM (a, TcDictBinds)
--- Type check an expression that runs at a top level stage as if
---   it were going to be spliced and then simplify it
-tcSimplifyStagedExpr stage tc_action
-  = setStage stage $ do { 
-        -- Typecheck the expression
-	  (thing', lie) <- getLIE tc_action
-	
-	-- Solve the constraints
-	; const_binds <- tcSimplifyTop lie
-	
-	; return (thing', const_binds) }
-
-\end{code}
 
 
 %************************************************************************
diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs
index 6146dfcacb..693fb2070d 100644
--- a/compiler/typecheck/TcSplice.lhs
+++ b/compiler/typecheck/TcSplice.lhs
@@ -5,6 +5,7 @@
 
 TcSplice: Template Haskell splices
 
+
 \begin{code}
 {-# OPTIONS -fno-warn-unused-imports -fno-warn-unused-binds #-}
 -- The above warning supression flag is a temporary kludge.
@@ -143,6 +144,115 @@ setInteractiveContext hsc_env icxt thing_inside
  	; thing_inside }
 \end{code}
 
+Note [How top-level splices are handled]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Top-level splices (those not inside a [| .. |] quotation bracket) are handled
+very straightforwardly:
+
+  1. tcTopSpliceExpr: typecheck the body e of the splice $(e)
+
+  2. runMetaT: desugar, compile, run it, and convert result back to
+     HsSyn RdrName (of the appropriate flavour, eg HsType RdrName,
+     HsExpr RdrName etc)
+
+  3. treat the result as if that's what you saw in the first place
+     e.g for HsType, rename and kind-check
+         for HsExpr, rename and type-check
+
+     (The last step is different for decls, becuase they can *only* be 
+      top-level: we return the result of step 2.)
+
+Note [How brackets and nested splices are handled]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Nested splices (those inside a [| .. |] quotation bracket), are treated
+quite differently. 
+
+  * After typechecking, the bracket [| |] carries
+
+     a) A mutable list of PendingSplice
+          type PendingSplice = (Name, LHsExpr Id)
+
+     b) The quoted expression e, *renamed*: (HsExpr Name)
+          The expression e has been typechecked, but the result of
+	  that typechecking is discarded.  
+
+  * The brakcet is desugared by DsMeta.dsBracket.  It 
+
+      a) Extends the ds_meta environment with the PendingSplices
+         attached to the bracket
+
+      b) Converts the quoted (HsExpr Name) to a CoreExpr that, when
+         run, will produce a suitable TH expression/type/decl.  This
+	 is why we leave the *renamed* expression attached to the bracket:
+         the quoted expression should not be decorated with all the goop
+         added by the type checker
+
+  * Each splice carries a unique Name, called a "splice point", thus
+    ${n}(e).  The name is initialised to an (Unqual "splice") when the
+    splice is created; the renamer gives it a unique.
+
+  * When the type checker type-checks a nested splice ${n}(e), it 
+	- typechecks e
+	- adds the typechecked expression (of type (HsExpr Id))
+	  as a pending splice to the enclosing bracket
+	- returns something non-committal
+    Eg for [| f ${n}(g x) |], the typechecker 
+	- attaches the typechecked term (g x) to the pending splices for n
+	  in the outer bracket
+        - returns a non-committal type \alpha.
+	Remember that the bracket discards the typechecked term altogether
+
+  * When DsMeta (used to desugar the body of the bracket) comes across
+    a splice, it looks up the splice's Name, n, in the ds_meta envt,
+    to find an (HsExpr Id) that should be substituted for the splice;
+    it just desugars it to get a CoreExpr (DsMeta.repSplice).
+
+Example: 
+    Source:	  f = [| Just $(g 3) |]
+      The [| |] part is a HsBracket
+
+    Typechecked:  f = [| Just ${s7}(g 3) |]{s7 = g Int 3}
+      The [| |] part is a HsBracketOut, containing *renamed* 
+	(not typechecked) expression
+      The "s7" is the "splice point"; the (g Int 3) part 
+	is a typechecked expression
+
+    Desugared:	  f = do { s7 <- g Int 3
+		         ; return (ConE "Data.Maybe.Just" s7) }
+
+
+Note [Template Haskell state diagram]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Here are the ThStages, s, their corresponding level numbers
+(the result of (thLevel s)), and their state transitions.  
+
+      -----------     $	     ------------   $
+      |  Comp   | ---------> |  Splice  | -----|
+      |   1     |    	     |    0     | <----|
+      -----------     	     ------------
+        ^     |       	       ^      |
+      $ |     | [||]  	     $ |      | [||]
+        |     v       	       |      v
+   --------------     	   ----------------
+   | Brack Comp |     	   | Brack Splice |
+   |     2      |     	   |      1       |
+   --------------     	   ----------------
+
+* Normal top-level declarations start in state Comp 
+       (which has level 1).
+  Annotations start in state Splice, since they are
+       treated very like a splice (only without a '$')
+
+* Code compiled in state Splice (and only such code) 
+  will be *run at compile time*, with the result replacing
+  the splice
+
+* The original paper used level -1 instead of 0, etc.
+
+* The original paper did not allow a splice within a 
+  splice, but there is no reason not to. This is the 
+  $ transition in the top right.
+
 Note [Template Haskell levels]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 * Imported things are impLevel (= 0)
@@ -152,7 +262,7 @@ Note [Template Haskell levels]
 
 * Variables are bound at the "current level"
 
-* The current level starts off at topLevel (= 1)
+* The current level starts off at outerLevel (= 1)
 
 * The level is decremented by splicing $(..)
 	       incremented by brackets [| |]
@@ -260,36 +370,27 @@ runAnnotation   _ q = pprPanic "Cant do runAnnotation without GHCi" (ppr q)
 %*									*
 %************************************************************************
 
-Note [Handling brackets]
-~~~~~~~~~~~~~~~~~~~~~~~~
-Source:		f = [| Just $(g 3) |]
-  The [| |] part is a HsBracket
-
-Typechecked:	f = [| Just ${s7}(g 3) |]{s7 = g Int 3}
-  The [| |] part is a HsBracketOut, containing *renamed* (not typechecked) expression
-  The "s7" is the "splice point"; the (g Int 3) part is a typechecked expression
-
-Desugared:	f = do { s7 <- g Int 3
-		       ; return (ConE "Data.Maybe.Just" s7) }
 
 \begin{code}
+-- See Note [How brackets and nested splices are handled]
 tcBracket brack res_ty 
   = addErrCtxt (hang (ptext (sLit "In the Template Haskell quotation"))
                    2 (ppr brack)) $
-    do { level <- getStage
-       ; case bracketOK level of {
- 	   Nothing         -> failWithTc (illegalBracket level) ;
-	   Just next_level -> do {
+    do { 	-- Check for nested brackets
+         cur_stage <- getStage
+       ; checkTc (not (isBrackStage cur_stage)) illegalBracket 
+
+	-- Brackets are desugared to code that mentions the TH package
+       ; recordThUse
 
    	-- Typecheck expr to make sure it is valid,
 	-- but throw away the results.  We'll type check
 	-- it again when we actually use it.
-          recordThUse
        ; pending_splices <- newMutVar []
        ; lie_var <- getLIEVar
 
-       ; (meta_ty, lie) <- setStage (Brack next_level pending_splices lie_var)
-                                    (getLIE (tc_bracket next_level brack))
+       ; (meta_ty, lie) <- setStage (Brack cur_stage pending_splices lie_var)
+                                    (getLIE (tc_bracket cur_stage brack))
        ; tcSimplifyBracket lie
 
 	-- Make the expected type have the right shape
@@ -297,18 +398,18 @@ tcBracket brack res_ty
 
 	-- Return the original expression, not the type-decorated one
        ; pendings <- readMutVar pending_splices
-       ; return (noLoc (HsBracketOut brack pendings)) }}}
+       ; return (noLoc (HsBracketOut brack pendings)) }
 
-tc_bracket :: ThLevel -> HsBracket Name -> TcM TcType
-tc_bracket use_lvl (VarBr name) 	-- Note [Quoting names]
+tc_bracket :: ThStage -> HsBracket Name -> TcM TcType
+tc_bracket outer_stage (VarBr name) 	-- Note [Quoting names]
   = do	{ thing <- tcLookup name
 	; case thing of
     	    AGlobal _ -> return ()
     	    ATcId { tct_level = bind_lvl, tct_id = id }
-		| thTopLevelId id	-- C.f thTopLevelId case of
-		-> keepAliveTc id 	--     TcExpr.thBrackId
+		| thTopLevelId id	-- C.f TcExpr.checkCrossStageLifting
+		-> keepAliveTc id 	 	
 		| otherwise
-		-> do { checkTc (use_lvl == bind_lvl)
+		-> do { checkTc (thLevel outer_stage + 1 == bind_lvl)
 				(quotedNameStageErr name) }
 	    _ -> pprPanic "th_bracket" (ppr name)
 
@@ -356,75 +457,77 @@ quotedNameStageErr v
 \begin{code}
 tcSpliceExpr (HsSplice name expr) res_ty
   = setSrcSpan (getLoc expr) 	$ do
-    level <- getStage
-    case spliceOK level of {
-	Nothing 	-> failWithTc (illegalSplice level) ;
-	Just next_level -> 
+    { stage <- getStage
+    ; case stage of {
+	Splice -> tcTopSplice expr res_ty ;
+	Comp   -> tcTopSplice expr res_ty ;
 
-     case level of {
-	Comp _ 		       -> do { e <- tcTopSplice expr res_ty
-				     ; return (unLoc e) } ;
-	Brack _ ps_var lie_var -> do
+	Brack pop_stage ps_var lie_var -> do
 
+        -- See Note [How brackets and nested splices are handled]
 	-- A splice inside brackets
   	-- NB: ignore res_ty, apart from zapping it to a mono-type
 	-- e.g.   [| reverse $(h 4) |]
 	-- Here (h 4) :: Q Exp
 	-- but $(h 4) :: forall a.a 	i.e. anything!
 
-      _ <- unBox res_ty
-      meta_exp_ty <- tcMetaTy expQTyConName
-      expr' <- setStage (Splice next_level) (
-                 setLIEVar lie_var    $
-                 tcMonoExpr expr meta_exp_ty
-               )
+     { _ <- unBox res_ty
+     ; meta_exp_ty <- tcMetaTy expQTyConName
+     ; expr' <- setStage pop_stage $
+                setLIEVar lie_var    $
+                tcMonoExpr expr meta_exp_ty
 
 	-- Write the pending splice into the bucket
-      ps <- readMutVar ps_var
-      writeMutVar ps_var ((name,expr') : ps)
+     ; ps <- readMutVar ps_var
+     ; writeMutVar ps_var ((name,expr') : ps)
 
-      return (panic "tcSpliceExpr")	-- The returned expression is ignored
-
-     ; Splice {} -> panic "tcSpliceExpr Splice"
-     }} 
-
--- tcTopSplice used to have this:
--- Note that we do not decrement the level (to -1) before 
--- typechecking the expression.  For example:
---	f x = $( ...$(g 3) ... )
--- The recursive call to tcMonoExpr will simply expand the 
--- inner escape before dealing with the outer one
+     ; return (panic "tcSpliceExpr")	-- The returned expression is ignored
+     }}}
 
-tcTopSplice :: LHsExpr Name -> BoxyRhoType -> TcM (LHsExpr Id)
-tcTopSplice expr res_ty = do
-    meta_exp_ty <- tcMetaTy expQTyConName
+tcTopSplice :: LHsExpr Name -> BoxyRhoType -> TcM (HsExpr Id)
+-- Note [How top-level splices are handled]
+tcTopSplice expr res_ty
+  = do { meta_exp_ty <- tcMetaTy expQTyConName
 
         -- Typecheck the expression
-    zonked_q_expr <- tcTopSpliceExpr expr meta_exp_ty
+       ; zonked_q_expr <- tcTopSpliceExpr (tcMonoExpr expr meta_exp_ty)
 
         -- Run the expression
-    traceTc (text "About to run" <+> ppr zonked_q_expr)
-    expr2 <- runMetaE convertToHsExpr zonked_q_expr
+       ; traceTc (text "About to run" <+> ppr zonked_q_expr)
+       ; expr2 <- runMetaE convertToHsExpr zonked_q_expr
 
-    traceTc (text "Got result" <+> ppr expr2)
+       ; traceTc (text "Got result" <+> ppr expr2)
 
-    showSplice "expression" expr (ppr expr2)
+       ; showSplice "expression" expr (ppr expr2)
 
         -- Rename it, but bale out if there are errors
         -- otherwise the type checker just gives more spurious errors
-    (exp3, _fvs) <- checkNoErrs (rnLExpr expr2)
-
-    tcMonoExpr exp3 res_ty
+       ; (exp3, _fvs) <- checkNoErrs (rnLExpr expr2)
 
+       ; exp4 <- tcMonoExpr exp3 res_ty
+       ; return (unLoc exp4) }
 
-tcTopSpliceExpr :: LHsExpr Name -> TcType -> TcM (LHsExpr Id)
+-------------------
+tcTopSpliceExpr :: TcM (LHsExpr Id) -> TcM (LHsExpr Id)
+-- Note [How top-level splices are handled]
 -- Type check an expression that is the body of a top-level splice
 --   (the caller will compile and run it)
-tcTopSpliceExpr expr meta_ty 
+-- Note that set the level to Splice, regardless of the original level,
+-- before typechecking the expression.  For example:
+--	f x = $( ...$(g 3) ... )
+-- The recursive call to tcMonoExpr will simply expand the 
+-- inner escape before dealing with the outer one
+
+tcTopSpliceExpr tc_action
   = checkNoErrs $  -- checkNoErrs: must not try to run the thing
                    -- if the type checker fails!
-    do { (expr', const_binds) <- tcSimplifyStagedExpr topSpliceStage $
-                                 (recordThUse >> tcMonoExpr expr meta_ty)
+    setStage Splice $ 
+    do {    -- Typecheck the expression
+         (expr', lie) <- getLIE tc_action
+        
+	-- Solve the constraints
+	; const_binds <- tcSimplifyTop lie
+	
           -- Zonk it and tie the knot of dictionary bindings
        ; zonkTopLExpr (mkHsDictLet const_binds expr') }
 \end{code}
@@ -432,43 +535,123 @@ tcTopSpliceExpr expr meta_ty
 
 %************************************************************************
 %*									*
+		Splicing a type
+%*									*
+%************************************************************************
+
+Very like splicing an expression, but we don't yet share code.
+
+\begin{code}
+kcSpliceType (HsSplice name hs_expr)
+  = setSrcSpan (getLoc hs_expr) $ do 	
+    { stage <- getStage
+    ; case stage of {
+        Splice -> kcTopSpliceType hs_expr ;
+    	Comp   -> kcTopSpliceType hs_expr ;
+
+    	Brack pop_level ps_var lie_var -> do
+	   -- See Note [How brackets and nested splices are handled]
+	   -- A splice inside brackets
+    { meta_ty <- tcMetaTy typeQTyConName
+    ; expr' <- setStage pop_level $
+    	       setLIEVar lie_var $
+    	       tcMonoExpr hs_expr meta_ty
+
+    	-- Write the pending splice into the bucket
+    ; ps <- readMutVar ps_var
+    ; writeMutVar ps_var ((name,expr') : ps)
+
+    -- e.g.   [| f (g :: Int -> $(h 4)) |]
+    -- Here (h 4) :: Q Type
+    -- but $(h 4) :: a 	i.e. any type, of any kind
+
+    -- We return a HsSpliceTyOut, which serves to convey the kind to 
+    -- the ensuing TcHsType.dsHsType, which makes up a non-committal
+    -- type variable of a suitable kind
+    ; kind <- newKindVar
+    ; return (HsSpliceTyOut kind, kind)	
+    }}}
+
+kcTopSpliceType :: LHsExpr Name -> TcM (HsType Name, TcKind)
+-- Note [How top-level splices are handled]
+kcTopSpliceType expr
+  = do	{ meta_ty <- tcMetaTy typeQTyConName
+
+	-- Typecheck the expression
+	; zonked_q_expr <- tcTopSpliceExpr (tcMonoExpr expr meta_ty)
+
+	-- Run the expression
+	; traceTc (text "About to run" <+> ppr zonked_q_expr)
+	; hs_ty2 <- runMetaT convertToHsType zonked_q_expr
+  
+	; traceTc (text "Got result" <+> ppr hs_ty2)
+
+	; showSplice "type" expr (ppr hs_ty2)
+
+	-- Rename it, but bale out if there are errors
+	-- otherwise the type checker just gives more spurious errors
+	; let doc = ptext (sLit "In the spliced type") <+> ppr hs_ty2
+	; hs_ty3 <- checkNoErrs (rnLHsType doc hs_ty2)
+
+	; (ty4, kind) <- kcLHsType hs_ty3
+        ; return (unLoc ty4, kind) }
+\end{code}
+
+%************************************************************************
+%*									*
+\subsection{Splicing an expression}
+%*									*
+%************************************************************************
+
+\begin{code}
+-- Note [How top-level splices are handled]
+-- Always at top level
+-- Type sig at top of file:
+-- 	tcSpliceDecls :: LHsExpr Name -> TcM [LHsDecl RdrName]
+tcSpliceDecls expr
+  = do	{ meta_dec_ty <- tcMetaTy decTyConName
+	; meta_q_ty <- tcMetaTy qTyConName
+	; let list_q = mkAppTy meta_q_ty (mkListTy meta_dec_ty)
+	; zonked_q_expr <- tcTopSpliceExpr (tcMonoExpr expr list_q)
+
+		-- Run the expression
+	; traceTc (text "About to run" <+> ppr zonked_q_expr)
+	; decls <- runMetaD convertToHsDecls zonked_q_expr
+
+	; traceTc (text "Got result" <+> vcat (map ppr decls))
+	; showSplice "declarations"
+	  	     expr 
+		     (ppr (getLoc expr) $$ (vcat (map ppr decls)))
+	; return decls }
+\end{code}
+
+
+%************************************************************************
+%*									*
 	Annotations
 %*									*
 %************************************************************************
 
 \begin{code}
 runAnnotation target expr = do
-    expr_ty <- newFlexiTyVarTy liftedTypeKind
-    
     -- Find the classes we want instances for in order to call toAnnotationWrapper
+    loc <- getSrcSpanM
     data_class <- tcLookupClass dataClassName
+    to_annotation_wrapper_id <- tcLookupId toAnnotationWrapperName
     
     -- Check the instances we require live in another module (we want to execute it..)
     -- and check identifiers live in other modules using TH stage checks. tcSimplifyStagedExpr
     -- also resolves the LIE constraints to detect e.g. instance ambiguity
-    ((wrapper, expr'), const_binds) <- tcSimplifyStagedExpr topAnnStage $ do
-                expr' <- tcPolyExprNC expr expr_ty
+    zonked_wrapped_expr' <- tcTopSpliceExpr $ 
+           do { (expr', expr_ty) <- tcInferRhoNC expr
+		-- We manually wrap the typechecked expression in a call to toAnnotationWrapper
                 -- By instantiating the call >here< it gets registered in the 
-		-- LIE consulted by tcSimplifyStagedExpr
+		-- LIE consulted by tcTopSpliceExpr
                 -- and hence ensures the appropriate dictionary is bound by const_binds
-                wrapper <- instCall AnnOrigin [expr_ty] [mkClassPred data_class [expr_ty]]
-                return (wrapper, expr')
-
-    -- We manually wrap the typechecked expression in a call to toAnnotationWrapper
-    loc <- getSrcSpanM
-    to_annotation_wrapper_id <- tcLookupId toAnnotationWrapperName
-    let specialised_to_annotation_wrapper_expr = L loc (HsWrap wrapper (HsVar to_annotation_wrapper_id))
-        wrapped_expr' = mkHsDictLet const_binds $
-                        L loc (HsApp specialised_to_annotation_wrapper_expr expr')
-
-    -- If we have type checking problems then potentially zonking 
-    -- (and certainly compilation) may fail. Give up NOW!
-    failIfErrsM
-
-    -- Zonk the type variables out of that raw expression. Note that
-    -- in particular we don't call recordThUse, since we don't
-    -- necessarily use any code or definitions from that package.
-    zonked_wrapped_expr' <- zonkTopLExpr wrapped_expr'
+              ; wrapper <- instCall AnnOrigin [expr_ty] [mkClassPred data_class [expr_ty]]
+              ; let specialised_to_annotation_wrapper_expr  
+                      = L loc (HsWrap wrapper (HsVar to_annotation_wrapper_id))
+              ; return (L loc (HsApp specialised_to_annotation_wrapper_expr expr')) }
 
     -- Run the appropriately wrapped expression to get the value of
     -- the annotation and its dictionaries. The return value is of
@@ -538,11 +721,10 @@ runQuasiQuote (HsQuasiQuote _name quoter q_span quote) quote_selector desc meta_
       	; let expr = L q_span $
       	             HsApp (L q_span $
       	                    HsApp (L q_span (HsVar quote_selector)) quoterExpr) quoteExpr
-      	; recordThUse
       	; meta_exp_ty <- tcMetaTy meta_ty
 
       	-- Typecheck the expression
-      	; zonked_q_expr <- tcTopSpliceExpr expr meta_exp_ty
+      	; zonked_q_expr <- tcTopSpliceExpr (tcMonoExpr expr meta_exp_ty)
 
       	-- Run the expression
       	; traceTc (text "About to run" <+> ppr zonked_q_expr)
@@ -567,97 +749,6 @@ quoteStageError quoter
 
 %************************************************************************
 %*									*
-		Splicing a type
-%*									*
-%************************************************************************
-
-Very like splicing an expression, but we don't yet share code.
-
-\begin{code}
-kcSpliceType (HsSplice name hs_expr)
-  = setSrcSpan (getLoc hs_expr) $ do 	
-	{ level <- getStage
-	; case spliceOK level of {
-		Nothing 	-> failWithTc (illegalSplice level) ;
-		Just next_level -> do 
-
-	{ case level of {
-		Comp _ 		       -> do { (t,k) <- kcTopSpliceType hs_expr 
-					     ; return (unLoc t, k) } ;
-		Brack _ ps_var lie_var -> do
-
-	{ 	-- A splice inside brackets
-	; meta_ty <- tcMetaTy typeQTyConName
-	; expr' <- setStage (Splice next_level) $
-		   setLIEVar lie_var	   	$
-		   tcMonoExpr hs_expr meta_ty
-
-		-- Write the pending splice into the bucket
-	; ps <- readMutVar ps_var
-	; writeMutVar ps_var ((name,expr') : ps)
-
-	-- e.g.   [| Int -> $(h 4) |]
-	-- Here (h 4) :: Q Type
-	-- but $(h 4) :: forall a.a 	i.e. any kind
-	; kind <- newKindVar
-	; return (panic "kcSpliceType", kind)	-- The returned type is ignored
-    }
-        ; Splice {} -> panic "kcSpliceType Splice"
-    }}}}
-
-kcTopSpliceType :: LHsExpr Name -> TcM (LHsType Name, TcKind)
-kcTopSpliceType expr
-  = do	{ meta_ty <- tcMetaTy typeQTyConName
-
-	-- Typecheck the expression
-	; zonked_q_expr <- tcTopSpliceExpr expr meta_ty
-
-	-- Run the expression
-	; traceTc (text "About to run" <+> ppr zonked_q_expr)
-	; hs_ty2 <- runMetaT convertToHsType zonked_q_expr
-  
-	; traceTc (text "Got result" <+> ppr hs_ty2)
-
-	; showSplice "type" expr (ppr hs_ty2)
-
-	-- Rename it, but bale out if there are errors
-	-- otherwise the type checker just gives more spurious errors
-	; let doc = ptext (sLit "In the spliced type") <+> ppr hs_ty2
-	; hs_ty3 <- checkNoErrs (rnLHsType doc hs_ty2)
-
-	; kcLHsType hs_ty3 }
-\end{code}
-
-%************************************************************************
-%*									*
-\subsection{Splicing an expression}
-%*									*
-%************************************************************************
-
-\begin{code}
--- Always at top level
--- Type sig at top of file:
--- 	tcSpliceDecls :: LHsExpr Name -> TcM [LHsDecl RdrName]
-tcSpliceDecls expr
-  = do	{ meta_dec_ty <- tcMetaTy decTyConName
-	; meta_q_ty <- tcMetaTy qTyConName
-	; let list_q = mkAppTy meta_q_ty (mkListTy meta_dec_ty)
-	; zonked_q_expr <- tcTopSpliceExpr expr list_q
-
-		-- Run the expression
-	; traceTc (text "About to run" <+> ppr zonked_q_expr)
-	; decls <- runMetaD convertToHsDecls zonked_q_expr
-
-	; traceTc (text "Got result" <+> vcat (map ppr decls))
-	; showSplice "declarations"
-	  	     expr 
-		     (ppr (getLoc expr) $$ (vcat (map ppr decls)))
-	; return decls }
-\end{code}
-
-
-%************************************************************************
-%*									*
 \subsection{Running an expression}
 %*									*
 %************************************************************************
@@ -836,14 +927,8 @@ showSplice what before after
 				         text "======>",
 				         nest 2 after])]) }
 
-illegalBracket :: ThStage -> SDoc
-illegalBracket level
-  = ptext (sLit "Illegal bracket at level") <+> ppr level
-
-illegalSplice :: ThStage -> SDoc
-illegalSplice level
-  = ptext (sLit "Illegal splice at level") <+> ppr level
-
+illegalBracket :: SDoc
+illegalBracket = ptext (sLit "Template Haskell brackets cannot be nested (without intervening splices)")
 #endif 	/* GHCI */
 \end{code}
 
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index bf2e9ace80..fb21918e25 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -6065,12 +6065,11 @@ Wiki page</ulink>.
 		    have type <literal>Q Exp</literal></para></listitem>
 		    <listitem><para> an type; the spliced expression must
 		    have type <literal>Q Typ</literal></para></listitem>
-		    <listitem><para> a list of top-level declarations; the spliced expression must have type <literal>Q [Dec]</literal></para></listitem>
+		    <listitem><para> a list of top-level declarations; the spliced expression 
+                    must have type <literal>Q [Dec]</literal></para></listitem>
 		    </itemizedlist>
-		</para>
 	    Inside a splice you can can only call functions defined in imported modules,
-	not functions defined elsewhere in the same module.</listitem>
-
+	not functions defined elsewhere in the same module.</para></listitem>
 
 	      <listitem><para>
 		  A expression quotation is written in Oxford brackets, thus:
@@ -6087,7 +6086,7 @@ Wiki page</ulink>.
 		  A quasi-quotation can appear in either a pattern context or an
 		  expression context and is also written in Oxford brackets:
 		  <itemizedlist>
-		    <listitem><para> <literal>[:<replaceable>varid</replaceable>| ... |]</literal>,
+		    <listitem><para> <literal>[$<replaceable>varid</replaceable>| ... |]</literal>,
                         where the "..." is an arbitrary string; a full description of the
 			quasi-quotation facility is given in <xref linkend="th-quasiquotation"/>.</para></listitem>
 		  </itemizedlist></para></listitem>
@@ -6108,6 +6107,25 @@ Wiki page</ulink>.
 	         </para>
 		</listitem>
 
+	      <listitem><para> You may omit the <literal>$(...)</literal> in a top-level declaration splice. 
+              Simply writing an expression (rather than a declaration) implies a splice.  For example, you can write
+<programlisting>
+module Foo where
+import Bar
+
+f x = x
+
+$(deriveStuff 'f)   -- Uses the $(...) notation
+
+g y = y+1
+
+deriveStuff 'g      -- Omits the $(...)
+
+h z = z-1
+</programlisting>
+            This abbreviation makes top-level declaration slices quieter and less intimidating.
+	    </para></listitem>
+
 		  
 	</itemizedlist>
 (Compared to the original paper, there are many differences of detail.