Merge branch 'master' of http://darcs.haskell.org/ghc

10 files changed, 235 insertions, 126 deletions

diff --git a/compiler/basicTypes/BasicTypes.lhs b/compiler/basicTypes/BasicTypes.lhs
index a4fb5590a2..3501291557 100644
--- a/compiler/basicTypes/BasicTypes.lhs
+++ b/compiler/basicTypes/BasicTypes.lhs
@@ -686,7 +686,8 @@ data InlineSpec   -- What the user's INLINE pragama looked like
   = Inline
   | Inlinable
   | NoInline
-  | EmptyInlineSpec
+  | EmptyInlineSpec  -- Used in a place-holder InlinePragma in SpecPrag or IdInfo,
+                     -- where there isn't any real inline pragma at all
   deriving( Eq, Data, Typeable, Show )
 	-- Show needed for Lexer.x
 \end{code}
diff --git a/compiler/coreSyn/MkCore.lhs b/compiler/coreSyn/MkCore.lhs
index 4cc199853b..c6fc2be21f 100644
--- a/compiler/coreSyn/MkCore.lhs
+++ b/compiler/coreSyn/MkCore.lhs
@@ -53,7 +53,8 @@ module MkCore (
     	mkRuntimeErrorApp, mkImpossibleExpr, errorIds,
     	rEC_CON_ERROR_ID, iRREFUT_PAT_ERROR_ID, rUNTIME_ERROR_ID,
     	nON_EXHAUSTIVE_GUARDS_ERROR_ID, nO_METHOD_BINDING_ERROR_ID,
-    	pAT_ERROR_ID, eRROR_ID, rEC_SEL_ERROR_ID, aBSENT_ERROR_ID
+    	pAT_ERROR_ID, eRROR_ID, rEC_SEL_ERROR_ID, aBSENT_ERROR_ID,
+        uNDEFINED_ID, undefinedName
     ) where
 
 #include "HsVersions.h"
@@ -659,6 +660,9 @@ errorIds
                   -- import its type from the interface file; we just get
                   -- the Id defined here.  Which has an 'open-tyvar' type.
 
+      uNDEFINED_ID,   -- Ditto for 'undefined'. The big deal is to give it
+                      -- an 'open-tyvar' type.
+
       rUNTIME_ERROR_ID,
       iRREFUT_PAT_ERROR_ID,
       nON_EXHAUSTIVE_GUARDS_ERROR_ID,
@@ -700,7 +704,7 @@ nON_EXHAUSTIVE_GUARDS_ERROR_ID  = mkRuntimeErrorId nonExhaustiveGuardsErrorName
 aBSENT_ERROR_ID                 = mkRuntimeErrorId absentErrorName
 
 mkRuntimeErrorId :: Name -> Id
-mkRuntimeErrorId name = pc_bottoming_Id name runtimeErrorTy
+mkRuntimeErrorId name = pc_bottoming_Id1 name runtimeErrorTy
 
 runtimeErrorTy :: Type
 -- The runtime error Ids take a UTF8-encoded string as argument
@@ -712,15 +716,33 @@ errorName :: Name
 errorName = mkWiredInIdName gHC_ERR (fsLit "error") errorIdKey eRROR_ID
 
 eRROR_ID :: Id
-eRROR_ID = pc_bottoming_Id errorName errorTy
+eRROR_ID = pc_bottoming_Id1 errorName errorTy
 
-errorTy  :: Type
+errorTy  :: Type   -- See Note [Error and friends have an "open-tyvar" forall]
 errorTy  = mkSigmaTy [openAlphaTyVar] [] (mkFunTys [mkListTy charTy] openAlphaTy)
-    -- Notice the openAlphaTyVar.  It says that "error" can be applied
-    -- to unboxed as well as boxed types.  This is OK because it never
-    -- returns, so the return type is irrelevant.
+
+undefinedName :: Name
+undefinedName = mkWiredInIdName gHC_ERR (fsLit "undefined") undefinedKey uNDEFINED_ID
+
+uNDEFINED_ID :: Id
+uNDEFINED_ID = pc_bottoming_Id0 undefinedName undefinedTy
+
+undefinedTy  :: Type   -- See Note [Error and friends have an "open-tyvar" forall]
+undefinedTy  = mkSigmaTy [openAlphaTyVar] [] openAlphaTy
 \end{code}
 
+Note [Error and friends have an "open-tyvar" forall]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+'error' and 'undefined' have types 
+        error     :: forall (a::OpenKind). String -> a
+        undefined :: forall (a::OpenKind). a
+Notice the 'OpenKind' (manifested as openAlphaTyVar in the code). This ensures that
+"error" can be instantiated at 
+  * unboxed as well as boxed types
+  * polymorphic types
+This is OK because it never returns, so the return type is irrelevant.
+See Note [OpenTypeKind accepts foralls] in TcUnify.
+
 
 %************************************************************************
 %*                                                                      *
@@ -729,9 +751,9 @@ errorTy  = mkSigmaTy [openAlphaTyVar] [] (mkFunTys [mkListTy charTy] openAlphaTy
 %************************************************************************
 
 \begin{code}
-pc_bottoming_Id :: Name -> Type -> Id
+pc_bottoming_Id1 :: Name -> Type -> Id
 -- Function of arity 1, which diverges after being given one argument
-pc_bottoming_Id name ty
+pc_bottoming_Id1 name ty
  = mkVanillaGlobalWithInfo name ty bottoming_info
  where
     bottoming_info = vanillaIdInfo `setStrictnessInfo`    strict_sig
@@ -749,5 +771,13 @@ pc_bottoming_Id name ty
 
     strict_sig = mkStrictSig (mkTopDmdType [evalDmd] botRes)
     -- These "bottom" out, no matter what their arguments
+
+pc_bottoming_Id0 :: Name -> Type -> Id
+-- Same but arity zero
+pc_bottoming_Id0 name ty
+ = mkVanillaGlobalWithInfo name ty bottoming_info
+ where
+    bottoming_info = vanillaIdInfo `setStrictnessInfo` strict_sig
+    strict_sig = mkStrictSig (mkTopDmdType [] botRes)
 \end{code}
 
diff --git a/compiler/hsSyn/HsBinds.lhs b/compiler/hsSyn/HsBinds.lhs
index 10724bc757..cb2538f574 100644
--- a/compiler/hsSyn/HsBinds.lhs
+++ b/compiler/hsSyn/HsBinds.lhs
@@ -615,7 +615,7 @@ hsSigDoc (TypeSig {})           = ptext (sLit "type signature")
 hsSigDoc (GenericSig {})        = ptext (sLit "default type signature")
 hsSigDoc (IdSig {})             = ptext (sLit "id signature")
 hsSigDoc (SpecSig {})           = ptext (sLit "SPECIALISE pragma")
-hsSigDoc (InlineSig {})         = ptext (sLit "INLINE pragma")
+hsSigDoc (InlineSig _ prag)     = ppr (inlinePragmaSpec prag) <+> ptext (sLit "pragma")
 hsSigDoc (SpecInstSig {})       = ptext (sLit "SPECIALISE instance pragma")
 hsSigDoc (FixSig {})            = ptext (sLit "fixity declaration")
 \end{code}
diff --git a/compiler/hsSyn/HsTypes.lhs b/compiler/hsSyn/HsTypes.lhs
index a95630d74b..eeed5cdbfb 100644
--- a/compiler/hsSyn/HsTypes.lhs
+++ b/compiler/hsSyn/HsTypes.lhs
@@ -447,6 +447,7 @@ hsLTyVarLocNames qtvs = map hsLTyVarLocName (hsQTvBndrs qtvs)
 \begin{code}
 splitHsAppTys :: LHsType n -> [LHsType n] -> (LHsType n, [LHsType n])
 splitHsAppTys (L _ (HsAppTy f a)) as = splitHsAppTys f (a:as)
+splitHsAppTys (L _ (HsParTy f))   as = splitHsAppTys f as
 splitHsAppTys f                   as = (f,as)
 
 mkHsAppTys :: OutputableBndr n => LHsType n -> [LHsType n] -> HsType n
diff --git a/compiler/prelude/PrelNames.lhs b/compiler/prelude/PrelNames.lhs
index 19acf488e0..09835fb34e 100644
--- a/compiler/prelude/PrelNames.lhs
+++ b/compiler/prelude/PrelNames.lhs
@@ -798,10 +798,6 @@ stringTyConName         = tcQual  gHC_BASE (fsLit "String") stringTyConKey
 inlineIdName :: Name
 inlineIdName            = varQual gHC_MAGIC (fsLit "inline") inlineIdKey
 
--- The 'undefined' function. Used by supercompilation.
-undefinedName :: Name
-undefinedName = varQual gHC_ERR (fsLit "undefined") undefinedKey
-
 -- Base classes (Eq, Ord, Functor)
 fmapName, eqClassName, eqName, ordClassName, geName, functorClassName :: Name
 eqClassName       = clsQual  gHC_CLASSES (fsLit "Eq")      eqClassKey
@@ -1689,7 +1685,6 @@ checkDotnetResNameIdKey       = mkPreludeMiscIdUnique 154
 
 undefinedKey :: Unique
 undefinedKey                  = mkPreludeMiscIdUnique 155
-
 \end{code}
 
 Certain class operations from Prelude classes.  They get their own
diff --git a/compiler/specialise/SpecConstr.lhs b/compiler/specialise/SpecConstr.lhs
index f8eeab7936..c1486d30c7 100644
--- a/compiler/specialise/SpecConstr.lhs
+++ b/compiler/specialise/SpecConstr.lhs
@@ -132,7 +132,7 @@ because now t is allocated by the caller, then r and s are passed to the
 recursive call, which allocates the (r,s) pair again.
 
 This happens if
-  (a) the argument p is used in other than a case-scrutinsation way.
+  (a) the argument p is used in other than a case-scrutinisation way.
   (b) the argument to the call is not a 'fresh' tuple; you have to
         look into its unfolding to see that it's a tuple
 
@@ -394,6 +394,22 @@ use the calls in the un-specialised RHS as seeds.  We call these
 "boring call patterns", and callsToPats reports if it finds any of these.
 
 
+Note [Top-level recursive groups]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+If all the bindings in a top-level recursive group are not exported,
+all the calls are in the rest of the top-level bindings.
+This means we can specialise with those call patterns instead of with the RHSs
+of the recursive group.
+
+To get the call usage information, we work backwards through the top-level bindings
+so we see the usage before we get to the binding of the function.
+Before we can collect the usage though, we go through all the bindings and add them
+to the environment. This is necessary because usage is only tracked for functions
+in the environment.
+
+The actual seeding of the specialisation is very similar to Note [Local recursive group].
+
+
 Note [Do not specialise diverging functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Specialising a function that just diverges is a waste of code.
@@ -402,7 +418,7 @@ Furthermore, it broke GHC (simpl014) thus:
    f = \x. case x of (a,b) -> f x
 If we specialise f we get
    f = \x. case x of (a,b) -> fspec a b
-But fspec doesn't have decent strictnes info.  As it happened,
+But fspec doesn't have decent strictness info.  As it happened,
 (f x) :: IO t, so the state hack applied and we eta expanded fspec,
 and hence f.  But now f's strictness is less than its arity, which
 breaks an invariant.
@@ -451,7 +467,7 @@ foldl_loop. Note that
 This is all quite ugly; we ought to come up with a better design.
 
 ForceSpecConstr arguments are spotted in scExpr' and scTopBinds which then set
-sc_force to True when calling specLoop. This flag does three things:
+sc_force to True when calling specLoop. This flag does four things:
   * Ignore specConstrThreshold, to specialise functions of arbitrary size
         (see scTopBind)
   * Ignore specConstrCount, to make arbitrary numbers of specialisations
@@ -459,7 +475,7 @@ sc_force to True when calling specLoop. This flag does three things:
   * Specialise even for arguments that are not scrutinised in the loop
         (see argToPat; Trac #4488)
   * Only specialise on recursive types a finite number of times
-        (see is_too_recursive; Trac #5550)
+        (see is_too_recursive; Trac #5550; Note [Limit recursive specialisation])
 
 This flag is inherited for nested non-recursive bindings (which are likely to
 be join points and hence should be fully specialised) but reset for nested
@@ -507,6 +523,39 @@ Without the SPEC, if 'loop' were strict, the case would move out
 and we'd see loop applied to a pair. But if 'loop' isn't strict
 this doesn't look like a specialisable call.
 
+Note [Limit recursive specialisation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It is possible for ForceSpecConstr to cause an infinite loop of specialisation.
+Because there is no limit on the number of specialisations, a recursive call with
+a recursive constructor as an argument (for example, list cons) will generate
+a specialisation for that constructor. If the resulting specialisation also
+contains a recursive call with the constructor, this could proceed indefinitely.
+
+For example, if ForceSpecConstr is on:
+  loop :: [Int] -> [Int] -> [Int]
+  loop z []         = z
+  loop z (x:xs)     = loop (x:z) xs
+this example will create a specialisation for the pattern
+  loop (a:b) c      = loop' a b c
+
+  loop' a b []      = (a:b)
+  loop' a b (x:xs)  = loop (x:(a:b)) xs
+and a new pattern is found:
+  loop (a:(b:c)) d  = loop'' a b c d
+which can continue indefinitely.
+
+Roman's suggestion to fix this was to stop after a couple of times on recursive types,
+but still specialising on non-recursive types as much as possible.
+
+To implement this, we count the number of recursive constructors in each
+function argument. If the maximum is greater than the specConstrRecursive limit,
+do not specialise on that pattern.
+
+This is only necessary when ForceSpecConstr is on: otherwise the specConstrCount
+will force termination anyway.
+
+See Trac #5550.
+
 Note [NoSpecConstr]
 ~~~~~~~~~~~~~~~~~~~
 The ignoreDataCon stuff allows you to say
@@ -605,13 +654,22 @@ specConstrProgram guts
       dflags <- getDynFlags
       us     <- getUniqueSupplyM
       annos  <- getFirstAnnotations deserializeWithData guts
-      let binds' = fst $ initUs us (go (initScEnv dflags annos) (mg_binds guts))
+      let binds' = reverse $ fst $ initUs us $ do
+                    -- Note [Top-level recursive groups]
+                    (env, binds) <- goEnv (initScEnv dflags annos) (mg_binds guts)
+                    go env nullUsage (reverse binds)
+
       return (guts { mg_binds = binds' })
   where
-    go _   []           = return []
-    go env (bind:binds) = do (env', bind') <- scTopBind env bind
-                             binds' <- go env' binds
-                             return (bind' : binds')
+    goEnv env []            = return (env, [])
+    goEnv env (bind:binds)  = do (env', bind')   <- scTopBindEnv env bind
+                                 (env'', binds') <- goEnv env' binds
+                                 return (env'', bind' : binds')
+
+    go _   _   []           = return []
+    go env usg (bind:binds) = do (usg', bind') <- scTopBind env usg bind
+                                 binds' <- go env usg' binds
+                                 return (bind' : binds')
 \end{code}
 
 
@@ -912,7 +970,7 @@ Note [Avoiding exponential blowup]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The sc_count field of the ScEnv says how many times we are prepared to
 duplicate a single function.  But we must take care with recursive
-specialiations.  Consider
+specialisations.  Consider
 
         let $j1 = let $j2 = let $j3 = ...
                             in
@@ -1225,38 +1283,62 @@ mkVarUsage env fn args
             | otherwise = evalScrutOcc
 
 ----------------------
-scTopBind :: ScEnv -> CoreBind -> UniqSM (ScEnv, CoreBind)
-scTopBind env (Rec prs)
+scTopBindEnv :: ScEnv -> CoreBind -> UniqSM (ScEnv, CoreBind)
+scTopBindEnv env (Rec prs)
+  = do  { let (rhs_env1,bndrs') = extendRecBndrs env bndrs
+              rhs_env2          = extendHowBound rhs_env1 bndrs RecFun
+
+              prs'              = zip bndrs' rhss
+        ; return (rhs_env2, Rec prs') }
+  where
+    (bndrs,rhss) = unzip prs
+
+scTopBindEnv env (NonRec bndr rhs)
+  = do  { let (env1, bndr') = extendBndr env bndr
+              env2          = extendValEnv env1 bndr' (isValue (sc_vals env) rhs)
+        ; return (env2, NonRec bndr' rhs) }
+
+----------------------
+scTopBind :: ScEnv -> ScUsage -> CoreBind -> UniqSM (ScUsage, CoreBind)
+
+{-
+scTopBind _ usage _
+  | pprTrace "scTopBind_usage" (ppr (scu_calls usage)) False
+  = error "false"
+-}
+ 
+scTopBind env usage (Rec prs)
   | Just threshold <- sc_size env
   , not force_spec
   , not (all (couldBeSmallEnoughToInline (sc_dflags env) threshold) rhss)
                 -- No specialisation
-  = do  { let (rhs_env,bndrs') = extendRecBndrs env bndrs
-        ; (_, rhss') <- mapAndUnzipM (scExpr rhs_env) rhss
-        ; return (rhs_env, Rec (bndrs' `zip` rhss')) }
+  = do  { (rhs_usgs, rhss')   <- mapAndUnzipM (scExpr env) rhss
+        ; return (usage `combineUsage` (combineUsages rhs_usgs), Rec (bndrs `zip` rhss')) }
   | otherwise   -- Do specialisation
-  = do  { let (rhs_env1,bndrs') = extendRecBndrs env bndrs
-              rhs_env2          = extendHowBound rhs_env1 bndrs' RecFun
+  = do  { (rhs_usgs, rhs_infos) <- mapAndUnzipM (scRecRhs env) (bndrs `zip` rhss)
+        -- ; pprTrace "scTopBind" (ppr bndrs $$ ppr (map (lookupVarEnv (scu_calls usage)) bndrs)) (return ())
 
-        ; (rhs_usgs, rhs_infos) <- mapAndUnzipM (scRecRhs rhs_env2) (bndrs' `zip` rhss)
-        ; let rhs_usg = combineUsages rhs_usgs
+        -- Note [Top-level recursive groups]
+        ; let (usg,rest) = if   all (not . isExportedId) bndrs
+                           then -- pprTrace "scTopBind-T" (ppr bndrs $$ ppr (map (fmap (map snd) . lookupVarEnv (scu_calls usage)) bndrs))
+                                ( usage
+                                , [SI [] 0 (Just us) | us <- rhs_usgs] )
+                           else ( combineUsages rhs_usgs
+                                , [SI [] 0 Nothing   | _  <- rhs_usgs] )
 
-        ; (_, specs) <- specLoop (scForce rhs_env2 force_spec)
-                                 (scu_calls rhs_usg) rhs_infos nullUsage
-                                 [SI [] 0 Nothing | _ <- bndrs]
+        ; (usage', specs) <- specLoop (scForce env force_spec)
+                                 (scu_calls usg) rhs_infos nullUsage rest
 
-        ; return (rhs_env1,  -- For the body of the letrec, delete the RecFun business
+        ; return (usage `combineUsage` usage',
                   Rec (concat (zipWith specInfoBinds rhs_infos specs))) }
   where
     (bndrs,rhss) = unzip prs
     force_spec   = any (forceSpecBndr env) bndrs
       -- Note [Forcing specialisation]
 
-scTopBind env (NonRec bndr rhs)
-  = do  { (_, rhs') <- scExpr env rhs
-        ; let (env1, bndr') = extendBndr env bndr
-              env2          = extendValEnv env1 bndr' (isValue (sc_vals env) rhs')
-        ; return (env2, NonRec bndr' rhs') }
+scTopBind env usage (NonRec bndr rhs)
+  = do  { (rhs_usg', rhs') <- scExpr env rhs
+        ; return (usage `combineUsage` rhs_usg', NonRec bndr rhs') }
 
 ----------------------
 scRecRhs :: ScEnv -> (OutId, InExpr) -> UniqSM (ScUsage, RhsInfo)
@@ -1282,6 +1364,7 @@ specInfoBinds (RI fn new_rhs _ _ _) (SI specs _ _)
               -- And now the original binding
   where
     rules = [r | OS _ r _ _ <- specs]
+
 \end{code}
 
 
@@ -1589,6 +1672,7 @@ is_too_recursive :: ScEnv -> (CallPat, ValueEnv) -> Bool
     -- filter out if there are more than the maximum.
     -- This is only necessary if ForceSpecConstr is in effect:
     -- otherwise specConstrCount will cause specialisation to terminate.
+    -- See Note [Limit recursive specialisation]
 is_too_recursive env ((_,exprs), val_env)
  = sc_force env && maximum (map go exprs) > sc_recursive env
  where
@@ -1617,7 +1701,7 @@ callToPats env bndr_occs (con_env, args)
         ; let pat_fvs       = varSetElems (exprsFreeVars pats)
               in_scope_vars = getInScopeVars in_scope
               qvars         = filterOut (`elemVarSet` in_scope_vars) pat_fvs
-                -- Quantify over variables that are not in sccpe
+                -- Quantify over variables that are not in scope
                 -- at the call site
                 -- See Note [Free type variables of the qvar types]
                 -- See Note [Shadowing] at the top
diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index 3ced71334e..c992faa416 100644
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -325,9 +325,10 @@ tc_group top_lvl sig_fn prag_fn (NonRecursive, binds) thing_inside
        ; return ( [(NonRecursive, binds1)], thing) }
 
 tc_group top_lvl sig_fn prag_fn (Recursive, binds) thing_inside
-  =     -- To maximise polymorphism (assumes -XRelaxedPolyRec), we do a new 
+  =     -- To maximise polymorphism, we do a new 
         -- strongly-connected-component analysis, this time omitting 
         -- any references to variables with type signatures.
+        -- (This used to be optional, but isn't now.)
     do  { traceTc "tc_group rec" (pprLHsBinds binds)
         ; (binds1, _ids, thing) <- go sccs
              -- Here is where we should do bindInstsOfLocalFuns
@@ -1006,7 +1007,12 @@ type MonoBindInfo = (Name, Maybe TcSigInfo, TcId)
 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind
 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_infix = inf, fun_matches = matches })
   | Just sig <- sig_fn name
-  = do  { mono_id <- newSigLetBndr no_gen name sig
+  = ASSERT2( case no_gen of { LetLclBndr -> True; LetGblBndr {} -> False }
+           , ppr name )  -- { f :: ty; f x = e } is always done via CheckGen
+                         -- which gives rise to LetLclBndr.  It wouldn't make
+                         -- sense to have a *polymorphic* function Id at this point
+    do  { mono_name <- newLocalName name
+        ; let mono_id = mkLocalId mono_name (sig_tau sig)
         ; return (TcFunBind (name, Just sig, mono_id) nm_loc inf matches) }
   | otherwise
   = do  { mono_ty <- newFlexiTyVarTy openTypeKind
@@ -1098,17 +1104,6 @@ However, we do *not* support this
         f :: forall a. a->a
         (f,g) = e
 
-  - For multiple function bindings, unless Opt_RelaxedPolyRec is on
-        f :: forall a. a -> a
-        f = g
-        g :: forall b. b -> b
-        g = ...f...
-    Reason: we use mutable variables for 'a' and 'b', since they may
-    unify to each other, and that means the scoped type variable would
-    not stand for a completely rigid variable.
-
-    Currently, we simply make Opt_ScopedTypeVariables imply Opt_RelaxedPolyRec
-
 Note [More instantiated than scoped]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 There may be more instantiated type variables than lexically-scoped 
diff --git a/compiler/typecheck/TcHsType.lhs b/compiler/typecheck/TcHsType.lhs
index 703ab95d57..dd0155e5e4 100644
--- a/compiler/typecheck/TcHsType.lhs
+++ b/compiler/typecheck/TcHsType.lhs
@@ -387,6 +387,9 @@ tc_hs_type hs_ty@(HsAppTy ty1 ty2) exp_kind
        ; arg_tys' <- tcCheckApps hs_ty fun_ty fun_kind arg_tys exp_kind
        ; return (mkNakedAppTys fun_ty' arg_tys') }
          -- mkNakedAppTys: see Note [Zonking inside the knot]
+         -- This looks fragile; how do we *know* that fun_ty isn't 
+         -- a TyConApp, say (which is never supposed to appear in the
+         -- function position of an AppTy)?
   where
     (fun_ty, arg_tys) = splitHsAppTys ty1 [ty2]
 
diff --git a/compiler/typecheck/TcPat.lhs b/compiler/typecheck/TcPat.lhs
index f4759659d6..fd9acee346 100644
--- a/compiler/typecheck/TcPat.lhs
+++ b/compiler/typecheck/TcPat.lhs
@@ -15,7 +15,7 @@ TcPat: Typechecking patterns
 
 module TcPat ( tcLetPat, TcSigFun, TcSigInfo(..), TcPragFun 
              , LetBndrSpec(..), addInlinePrags, warnPrags
-             , tcPat, tcPats, newNoSigLetBndr, newSigLetBndr
+             , tcPat, tcPats, newNoSigLetBndr
 	     , addDataConStupidTheta, badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"
@@ -112,8 +112,8 @@ data PatCtxt
   = LamPat   -- Used for lambdas, case etc
        (HsMatchContext Name) 
 
-  | LetPat   -- Used only for let(rec) bindings
-    	     -- See Note [Let binders]
+  | LetPat   -- Used only for let(rec) pattern bindings
+    	     -- See Note [Typing patterns in pattern bindings]
        TcSigFun        -- Tells type sig if any
        LetBndrSpec     -- True <=> no generalisation of this let
 
@@ -121,8 +121,10 @@ data LetBndrSpec
   = LetLclBndr		  -- The binder is just a local one;
     			  -- an AbsBinds will provide the global version
 
-  | LetGblBndr TcPragFun  -- There isn't going to be an AbsBinds;
-    	       		  -- here is the inline-pragma information
+  | LetGblBndr TcPragFun  -- Genrealisation plan is NoGen, so there isn't going 
+                          -- to be an AbsBinds; So we must bind the global version
+                          -- of the binder right away.  
+    	       		  -- Oh, and dhhere is the inline-pragma information
 
 makeLazy :: PatEnv -> PatEnv
 makeLazy penv = penv { pe_lazy = True }
@@ -177,15 +179,6 @@ if the original function had a signature like
 But that's ok: tcMatchesFun (called by tcRhs) can deal with that
 It happens, too!  See Note [Polymorphic methods] in TcClassDcl.
 
-Note [Let binders]
-~~~~~~~~~~~~~~~~~~
-eg   x :: Int
-     y :: Bool
-     (x,y) = e
-
-...more notes to add here..
-
-
 Note [Existential check]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 Lazy patterns can't bind existentials.  They arise in two ways:
@@ -215,13 +208,17 @@ tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (TcCoercion, TcId)
 -- Then coi : pat_ty ~ typeof(xp)
 --
 tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty
-  | Just sig <- lookup_sig bndr_name
-  = do { bndr_id <- newSigLetBndr no_gen bndr_name sig
+          -- See Note [Typing patterns in pattern bindings]
+  | LetGblBndr prags <- no_gen
+  , Just sig <- lookup_sig bndr_name
+  = do { bndr_id <- addInlinePrags (sig_id sig) (prags bndr_name)
+       ; traceTc "tcPatBndr(gbl,sig)" (ppr bndr_id $$ ppr (idType bndr_id)) 
        ; co <- unifyPatType (idType bndr_id) pat_ty
        ; return (co, bndr_id) }
       
-  | otherwise
+  | otherwise 
   = do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty
+       ; traceTc "tcPatBndr(no-sig)" (ppr bndr_id $$ ppr (idType bndr_id))
        ; return (mkTcReflCo pat_ty, bndr_id) }
 
 tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
@@ -229,20 +226,12 @@ tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
        ; return (mkTcReflCo pat_ty, bndr) }
 
 ------------
-newSigLetBndr :: LetBndrSpec -> Name -> TcSigInfo -> TcM TcId
-newSigLetBndr LetLclBndr name sig
-  = do { mono_name <- newLocalName name
-       ; mkLocalBinder mono_name (sig_tau sig) }
-newSigLetBndr (LetGblBndr prags) name sig
-  = addInlinePrags (sig_id sig) (prags name)
-
-------------
 newNoSigLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
--- In the polymorphic case (no_gen = False), generate a "monomorphic version" 
+-- In the polymorphic case (no_gen = LetLclBndr), generate a "monomorphic version" 
 --    of the Id; the original name will be bound to the polymorphic version
 --    by the AbsBinds
--- In the monomorphic case there is no AbsBinds, and we use the original
---    name directly
+-- In the monomorphic case (no_gen = LetBglBndr) there is no AbsBinds, and we 
+--    use the original name directly
 newNoSigLetBndr LetLclBndr name ty 
   =do  { mono_name <- newLocalName name
        ; mkLocalBinder mono_name ty }
@@ -280,16 +269,34 @@ mkLocalBinder name ty
   = return (Id.mkLocalId name ty)
 \end{code}
 
-Note [Polymorphism and pattern bindings]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When is_mono holds we are not generalising
-But the signature can still be polymorphic!
-     data T = MkT (forall a. a->a)
+Note [Typing patterns in pattern bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we are typing a pattern binding
+    pat = rhs
+Then the PatCtxt will be (LetPat sig_fn let_bndr_spec).
+
+There can still be signatures for the binders:
+     data T = MkT (forall a. a->a) Int
      x :: forall a. a->a
-     MkT x = <rhs>
-So the no_gen flag decides whether the pattern-bound variables should
-have exactly the type in the type signature (when not generalising) or
-the instantiated version (when generalising)
+     y :: Int
+     MkT x y = <rhs>
+
+Two cases, dealt with by the LetPat case of tcPatBndr
+
+ * If we are generalising (generalisation plan is InferGen or
+   CheckGen), then the let_bndr_spec will be LetLclBndr.  In that case
+   we want to bind a cloned, local version of the variable, with the
+   type given by the pattern context, *not* by the signature (even if
+   there is one; see Trac #7268). The mkExport part of the
+   generalisation step will do the checking and impedence matching
+   against the signature.
+
+ * If for some some reason we are not generalising (plan = NoGen), the
+   LetBndrSpec will be LetGblBndr.  In that case we must bind the
+   global version of the Id, and do so with precisely the type given
+   in the signature.  (Then we unify with the type from the pattern
+   context type.
+
 
 %************************************************************************
 %*									*
diff --git a/compiler/typecheck/TcSplice.lhs b/compiler/typecheck/TcSplice.lhs
index 7d51d4b937..d20c6ff59c 100644
--- a/compiler/typecheck/TcSplice.lhs
+++ b/compiler/typecheck/TcSplice.lhs
@@ -1010,38 +1010,28 @@ reifyInstances :: TH.Name -> [TH.Type] -> TcM [TH.Dec]
 reifyInstances th_nm th_tys
    = addErrCtxt (ptext (sLit "In the argument of reifyInstances:")
                  <+> ppr_th th_nm <+> sep (map ppr_th th_tys)) $
-     do { thing <- getThing th_nm
-        ; case thing of
-            AGlobal (ATyCon tc)
-              | Just cls <- tyConClass_maybe tc
-              -> do { tys <- tc_types (classTyCon cls) th_tys
-                    ; inst_envs <- tcGetInstEnvs
-                    ; let (matches, unifies, _) = lookupInstEnv inst_envs cls tys
-                    ; mapM reifyClassInstance (map fst matches ++ unifies) }
-              | otherwise
-              -> do { tys <- tc_types tc th_tys
-                    ; inst_envs <- tcGetFamInstEnvs
-                    ; let matches = lookupFamInstEnv inst_envs tc tys
-                    ; mapM (reifyFamilyInstance . fim_instance) matches }
-            _ -> bale_out (ppr_th th_nm <+> ptext (sLit "is not a class or type constructor"))
-        }
+     do { loc <- getSrcSpanM
+        ; rdr_ty <- cvt loc (mkThAppTs (TH.ConT th_nm) th_tys)
+        ; (rn_ty, _fvs) <- checkNoErrs $ rnLHsType doc rdr_ty   -- Rename  to HsType Name
+                         -- checkNoErrs: see Note [Renamer errors]
+        ; (ty, _kind)  <- tcLHsType rn_ty
+
+        ; case splitTyConApp_maybe ty of   -- This expands any type synonyms
+            Just (tc, tys)                 -- See Trac #7910
+               | Just cls <- tyConClass_maybe tc
+               -> do { inst_envs <- tcGetInstEnvs
+                     ; let (matches, unifies, _) = lookupInstEnv inst_envs cls tys
+                     ; mapM reifyClassInstance (map fst matches ++ unifies) }
+               | isFamilyTyCon tc
+               -> do { inst_envs <- tcGetFamInstEnvs
+                     ; let matches = lookupFamInstEnv inst_envs tc tys
+                     ; mapM (reifyFamilyInstance . fim_instance) matches }
+            _  -> bale_out (hang (ptext (sLit "reifyInstances:") <+> quotes (ppr ty)) 
+                               2 (ptext (sLit "is not a class constraint or type family application"))) }
   where
     doc = ClassInstanceCtx
     bale_out msg = failWithTc msg
 
-    tc_types :: TyCon -> [TH.Type] -> TcM [Type]
-    tc_types tc th_tys
-      = do { let tc_arity = tyConArity tc
-           ; when (length th_tys /= tc_arity)
-                  (bale_out (ptext (sLit "Wrong number of types (expected")
-                             <+> int tc_arity <> rparen))
-           ; loc <- getSrcSpanM
-           ; rdr_tys <- mapM (cvt loc) th_tys    -- Convert to HsType RdrName
-           ; (rn_tys, _fvs) <- checkNoErrs $ rnLHsTypes doc rdr_tys   -- Rename  to HsType Name
-                         -- checkNoErrs: see Note [Renamer errors]
-           ; (tys, _res_k)  <- tcInferApps tc (tyConKind tc) rn_tys
-           ; return tys }
-
     cvt :: SrcSpan -> TH.Type -> TcM (LHsType RdrName)
     cvt loc th_ty = case convertToHsType loc th_ty of
                       Left msg -> failWithTc msg
@@ -1305,7 +1295,7 @@ reifyClassInstance :: ClsInst -> TcM TH.Dec
 reifyClassInstance i
   = do { cxt <- reifyCxt (drop n_silent theta)
        ; thtypes <- reifyTypes types
-       ; let head_ty = foldl TH.AppT (TH.ConT (reifyName cls)) thtypes
+       ; let head_ty = mkThAppTs (TH.ConT (reifyName cls)) thtypes
        ; return $ (TH.InstanceD cxt head_ty []) }
   where
      (_tvs, theta, cls, types) = tcSplitDFunTy (idType dfun)
@@ -1386,7 +1376,7 @@ reifyKind  ki
 
 reify_kc_app :: TyCon -> [TypeRep.Kind] -> TcM TH.Kind
 reify_kc_app kc kis
-  = fmap (foldl TH.AppT r_kc) (mapM reifyKind kis)
+  = fmap (mkThAppTs r_kc) (mapM reifyKind kis)
   where
     r_kc | Just tc <- isPromotedTyCon_maybe kc
          , isTupleTyCon tc          = TH.TupleT (tyConArity kc)
@@ -1418,7 +1408,7 @@ reifyTyVars = mapM reifyTyVar . filter isTypeVar
 reify_tc_app :: TyCon -> [TypeRep.Type] -> TcM TH.Type
 reify_tc_app tc tys
   = do { tys' <- reifyTypes (removeKinds (tyConKind tc) tys)
-       ; return (foldl TH.AppT r_tc tys') }
+       ; return (mkThAppTs r_tc tys') }
   where
     arity = tyConArity tc
     r_tc | isTupleTyCon tc            = if isPromotedDataCon tc
@@ -1495,6 +1485,9 @@ reifyStrict HsStrict                      = TH.IsStrict
 reifyStrict (HsUnpack {})                 = TH.Unpacked
 
 ------------------------------
+mkThAppTs :: TH.Type -> [TH.Type] -> TH.Type
+mkThAppTs fun_ty arg_tys = foldl TH.AppT fun_ty arg_tys
+
 noTH :: LitString -> SDoc -> TcM a
 noTH s d = failWithTc (hsep [ptext (sLit "Can't represent") <+> ptext s <+>
                                 ptext (sLit "in Template Haskell:"),