Improve the desugaring of -XStrict
[ghc.git] / compiler / typecheck / TcBinds.hs
index fb89416..0995f6b 100644 (file)
@@ -7,9 +7,10 @@
 
 {-# LANGUAGE CPP, RankNTypes, ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
-                 tcValBinds, tcHsBootSigs, tcPolyCheck,
+                 tcHsBootSigs, tcPolyCheck,
                  tcVectDecls, addTypecheckedBinds,
                  chooseInferredQuantifiers,
                  badBootDeclErr ) where
@@ -18,7 +19,10 @@ import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
 import {-# SOURCE #-} TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl
                                , tcPatSynBuilderBind )
+import CoreSyn (Tickish (..))
+import CostCentre (mkUserCC)
 import DynFlags
+import FastString
 import HsSyn
 import HscTypes( isHsBootOrSig )
 import TcSigs
@@ -30,12 +34,11 @@ import TcEvidence
 import TcHsType
 import TcPat
 import TcMType
-import Inst( deeplyInstantiate )
 import FamInstEnv( normaliseType )
 import FamInst( tcGetFamInstEnvs )
 import TyCon
 import TcType
-import Type( mkStrLitTy, tidyOpenType, TyVarBinder, mkTyVarBinder )
+import Type( mkStrLitTy, tidyOpenType, splitTyConApp_maybe)
 import TysPrim
 import TysWiredIn( cTupleTyConName )
 import Id
@@ -55,10 +58,13 @@ import Maybes
 import Util
 import BasicTypes
 import Outputable
-import PrelNames( gHC_PRIM, ipClassName )
+import PrelNames( ipClassName )
 import TcValidity (checkValidType)
+import Unique (getUnique)
 import UniqFM
+import UniqSet
 import qualified GHC.LanguageExtensions as LangExt
+import ConLike
 
 import Control.Monad
 
@@ -70,7 +76,7 @@ import Control.Monad
 *                                                                      *
 ********************************************************************* -}
 
-addTypecheckedBinds :: TcGblEnv -> [LHsBinds Id] -> TcGblEnv
+addTypecheckedBinds :: TcGblEnv -> [LHsBinds GhcTc] -> TcGblEnv
 addTypecheckedBinds tcg_env binds
   | isHsBootOrSig (tcg_src tcg_env) = tcg_env
     -- Do not add the code for record-selector bindings
@@ -171,7 +177,8 @@ Then we get
                                fm
 -}
 
-tcTopBinds :: [(RecFlag, LHsBinds Name)] -> [LSig Name] -> TcM (TcGblEnv, TcLclEnv)
+tcTopBinds :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
+           -> TcM (TcGblEnv, TcLclEnv)
 -- The TcGblEnv contains the new tcg_binds and tcg_spects
 -- The TcLclEnv has an extended type envt for the new bindings
 tcTopBinds binds sigs
@@ -182,14 +189,122 @@ tcTopBinds binds sigs
                ; return (gbl, lcl) }
         ; specs <- tcImpPrags sigs   -- SPECIALISE prags for imported Ids
 
-        ; let { tcg_env' = tcg_env { tcg_imp_specs = specs ++ tcg_imp_specs tcg_env }
+        ; complete_matches <- setEnvs (tcg_env, tcl_env) $ tcCompleteSigs sigs
+        ; traceTc "complete_matches" (ppr binds $$ ppr sigs)
+        ; traceTc "complete_matches" (ppr complete_matches)
+
+        ; let { tcg_env' = tcg_env { tcg_imp_specs
+                                      = specs ++ tcg_imp_specs tcg_env
+                                   , tcg_complete_matches
+                                      = complete_matches
+                                          ++ tcg_complete_matches tcg_env }
                            `addTypecheckedBinds` map snd binds' }
 
         ; return (tcg_env', tcl_env) }
         -- The top level bindings are flattened into a giant
         -- implicitly-mutually-recursive LHsBinds
 
-tcRecSelBinds :: HsValBinds Name -> TcM TcGblEnv
+
+-- Note [Typechecking Complete Matches]
+-- Much like when a user bundled a pattern synonym, the result types of
+-- all the constructors in the match pragma must be consistent.
+--
+-- If we allowed pragmas with inconsistent types then it would be
+-- impossible to ever match every constructor in the list and so
+-- the pragma would be useless.
+
+
+
+
+
+-- This is only used in `tcCompleteSig`. We fold over all the conlikes,
+-- this accumulator keeps track of the first `ConLike` with a concrete
+-- return type. After fixing the return type, all other constructors with
+-- a fixed return type must agree with this.
+--
+-- The fields of `Fixed` cache the first conlike and its return type so
+-- that that we can compare all the other conlikes to it. The conlike is
+-- stored for error messages.
+--
+-- `Nothing` in the case that the type is fixed by a type signature
+data CompleteSigType = AcceptAny | Fixed (Maybe ConLike) TyCon
+
+tcCompleteSigs  :: [LSig GhcRn] -> TcM [CompleteMatch]
+tcCompleteSigs sigs =
+  let
+      doOne :: Sig GhcRn -> TcM (Maybe CompleteMatch)
+      doOne c@(CompleteMatchSig _ lns mtc)
+        = fmap Just $ do
+           addErrCtxt (text "In" <+> ppr c) $
+            case mtc of
+              Nothing -> infer_complete_match
+              Just tc -> check_complete_match tc
+        where
+
+          checkCLTypes acc = foldM checkCLType (acc, []) (unLoc lns)
+
+          infer_complete_match = do
+            (res, cls) <- checkCLTypes AcceptAny
+            case res of
+              AcceptAny -> failWithTc ambiguousError
+              Fixed _ tc  -> return $ mkMatch cls tc
+
+          check_complete_match tc_name = do
+            ty_con <- tcLookupLocatedTyCon tc_name
+            (_, cls) <- checkCLTypes (Fixed Nothing ty_con)
+            return $ mkMatch cls ty_con
+
+          mkMatch :: [ConLike] -> TyCon -> CompleteMatch
+          mkMatch cls ty_con = CompleteMatch {
+            completeMatchConLikes = map conLikeName cls,
+            completeMatchTyCon = tyConName ty_con
+            }
+      doOne _ = return Nothing
+
+      ambiguousError :: SDoc
+      ambiguousError =
+        text "A type signature must be provided for a set of polymorphic"
+          <+> text "pattern synonyms."
+
+
+      -- See note [Typechecking Complete Matches]
+      checkCLType :: (CompleteSigType, [ConLike]) -> Located Name
+                  -> TcM (CompleteSigType, [ConLike])
+      checkCLType (cst, cs) n = do
+        cl <- addLocM tcLookupConLike n
+        let   (_,_,_,_,_,_, res_ty) = conLikeFullSig cl
+              res_ty_con = fst <$> splitTyConApp_maybe res_ty
+        case (cst, res_ty_con) of
+          (AcceptAny, Nothing) -> return (AcceptAny, cl:cs)
+          (AcceptAny, Just tc) -> return (Fixed (Just cl) tc, cl:cs)
+          (Fixed mfcl tc, Nothing)  -> return (Fixed mfcl tc, cl:cs)
+          (Fixed mfcl tc, Just tc') ->
+            if tc == tc'
+              then return (Fixed mfcl tc, cl:cs)
+              else case mfcl of
+                     Nothing ->
+                      addErrCtxt (text "In" <+> ppr cl) $
+                        failWithTc typeSigErrMsg
+                     Just cl -> failWithTc (errMsg cl)
+             where
+              typeSigErrMsg :: SDoc
+              typeSigErrMsg =
+                text "Couldn't match expected type"
+                      <+> quotes (ppr tc)
+                      <+> text "with"
+                      <+> quotes (ppr tc')
+
+              errMsg :: ConLike -> SDoc
+              errMsg fcl =
+                text "Cannot form a group of complete patterns from patterns"
+                  <+> quotes (ppr fcl) <+> text "and" <+> quotes (ppr cl)
+                  <+> text "as they match different type constructors"
+                  <+> parens (quotes (ppr tc)
+                               <+> text "resp."
+                               <+> quotes (ppr tc'))
+  in  mapMaybeM (addLocM doOne) sigs
+
+tcRecSelBinds :: HsValBinds GhcRn -> TcM TcGblEnv
 tcRecSelBinds (ValBindsOut binds sigs)
   = tcExtendGlobalValEnv [sel_id | L _ (IdSig sel_id) <- sigs] $
     do { (rec_sel_binds, tcg_env) <- discardWarnings $
@@ -198,7 +313,7 @@ tcRecSelBinds (ValBindsOut binds sigs)
        ; return tcg_env' }
 tcRecSelBinds (ValBindsIn {}) = panic "tcRecSelBinds"
 
-tcHsBootSigs :: [(RecFlag, LHsBinds Name)] -> [LSig Name] -> TcM [Id]
+tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
 -- A hs-boot file has only one BindGroup, and it only has type
 -- signatures in it.  The renamer checked all this
 tcHsBootSigs binds sigs
@@ -208,8 +323,7 @@ tcHsBootSigs binds sigs
     tc_boot_sig (TypeSig lnames hs_ty) = mapM f lnames
       where
         f (L _ name)
-          = do { sigma_ty <- solveEqualities $
-                             tcHsSigWcType (FunSigCtxt name False) hs_ty
+          = do { sigma_ty <- tcHsSigWcType (FunSigCtxt name False) hs_ty
                ; return (mkVanillaGlobal name sigma_ty) }
         -- Notice that we make GlobalIds, not LocalIds
     tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
@@ -218,8 +332,8 @@ badBootDeclErr :: MsgDoc
 badBootDeclErr = text "Illegal declarations in an hs-boot file"
 
 ------------------------
-tcLocalBinds :: HsLocalBinds Name -> TcM thing
-             -> TcM (HsLocalBinds TcId, thing)
+tcLocalBinds :: HsLocalBinds GhcRn -> TcM thing
+             -> TcM (HsLocalBinds GhcTcId, thing)
 
 tcLocalBinds EmptyLocalBinds thing_inside
   = do  { thing <- thing_inside
@@ -259,7 +373,7 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
 
     -- Coerces a `t` into a dictionry for `IP "x" t`.
     -- co : t -> IP "x" t
-    toDict ipClass x ty = HsWrap $ mkWpCastR $
+    toDict ipClass x ty = mkHsWrap $ mkWpCastR $
                           wrapIP $ mkClassPred ipClass [x,ty]
 
 {- Note [Implicit parameter untouchables]
@@ -275,59 +389,12 @@ time by defaulting.  No no no.
 
 However [Oct 10] this is all handled automatically by the
 untouchable-range idea.
-
-Note [Inlining and hs-boot files]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider this example (Trac #10083):
-
-    ---------- RSR.hs-boot ------------
-    module RSR where
-      data RSR
-      eqRSR :: RSR -> RSR -> Bool
-
-    ---------- SR.hs ------------
-    module SR where
-      import {-# SOURCE #-} RSR
-      data SR = MkSR RSR
-      eqSR (MkSR r1) (MkSR r2) = eqRSR r1 r2
-
-    ---------- RSR.hs ------------
-    module RSR where
-      import SR
-      data RSR = MkRSR SR -- deriving( Eq )
-      eqRSR (MkRSR s1) (MkRSR s2) = (eqSR s1 s2)
-      foo x y = not (eqRSR x y)
-
-When compiling RSR we get this code
-
-    RSR.eqRSR :: RSR -> RSR -> Bool
-    RSR.eqRSR = \ (ds1 :: RSR.RSR) (ds2 :: RSR.RSR) ->
-                case ds1 of _ { RSR.MkRSR s1 ->
-                case ds2 of _ { RSR.MkRSR s2 ->
-                SR.eqSR s1 s2 }}
-
-    RSR.foo :: RSR -> RSR -> Bool
-    RSR.foo = \ (x :: RSR) (y :: RSR) -> not (RSR.eqRSR x y)
-
-Now, when optimising foo:
-    Inline eqRSR (small, non-rec)
-    Inline eqSR  (small, non-rec)
-but the result of inlining eqSR from SR is another call to eqRSR, so
-everything repeats.  Neither eqSR nor eqRSR are (apparently) loop
-breakers.
-
-Solution: when compiling RSR, add a NOINLINE pragma to every function
-exported by the boot-file for RSR (if it exists).
-
-ALAS: doing so makes the boostrappted GHC itself slower by 8% overall
-      (on Trac #9872a-d, and T1969.  So I un-did this change, and
-      parked it for now.  Sigh.
 -}
 
 tcValBinds :: TopLevelFlag
-           -> [(RecFlag, LHsBinds Name)] -> [LSig Name]
+           -> [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
            -> TcM thing
-           -> TcM ([(RecFlag, LHsBinds TcId)], thing)
+           -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
 
 tcValBinds top_lvl binds sigs thing_inside
   = do  { let patsyns = getPatSynBinds binds
@@ -336,28 +403,17 @@ tcValBinds top_lvl binds sigs thing_inside
         ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
                                 tcTySigs sigs
 
-        ; _self_boot <- tcSelfBootInfo
         ; let prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
 
--- -------  See Note [Inlining and hs-boot files] (change parked) --------
---              prag_fn | isTopLevel top_lvl   -- See Note [Inlining and hs-boot files]
---                      , SelfBoot { sb_ids = boot_id_names } <- self_boot
---                      = foldNameSet add_no_inl prag_fn1 boot_id_names
---                      | otherwise
---                      = prag_fn1
---              add_no_inl boot_id_name prag_fn
---                = extendPragEnv prag_fn (boot_id_name, no_inl_sig boot_id_name)
---              no_inl_sig name = L boot_loc (InlineSig (L boot_loc name) neverInlinePragma)
---              boot_loc = mkGeneralSrcSpan (fsLit "The hs-boot file for this module")
-
                 -- Extend the envt right away with all the Ids
                 -- declared with complete type signatures
                 -- Do not extend the TcIdBinderStack; instead
                 -- we extend it on a per-rhs basis in tcExtendForRhs
-        ; tcExtendLetEnvIds top_lvl [(idName id, id) | id <- poly_ids] $ do
+        ; tcExtendSigIds top_lvl poly_ids $ do
             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
                    { thing <- thing_inside
                      -- See Note [Pattern synonym builders don't yield dependencies]
+                     --     in RnBinds
                    ; patsyn_builders <- mapM tcPatSynBuilderBind patsyns
                    ; let extra_binds = [ (NonRecursive, builder) | builder <- patsyn_builders ]
                    ; return (extra_binds, thing) }
@@ -365,8 +421,8 @@ tcValBinds top_lvl binds sigs thing_inside
 
 ------------------------
 tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
-             -> [(RecFlag, LHsBinds Name)] -> TcM thing
-             -> TcM ([(RecFlag, LHsBinds TcId)], thing)
+             -> [(RecFlag, LHsBinds GhcRn)] -> TcM thing
+             -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
 -- Typecheck a whole lot of value bindings,
 -- one strongly-connected component at a time
 -- Here a "strongly connected component" has the strightforward
@@ -379,7 +435,8 @@ tcBindGroups _ _ _ [] thing_inside
 
 tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
   = do  { -- See Note [Closed binder groups]
-          closed <- isClosedBndrGroup $ snd group
+          type_env <- getLclTypeEnv
+        ; let closed = isClosedBndrGroup type_env (snd group)
         ; (group', (groups', thing))
                 <- tc_group top_lvl sig_fn prag_fn group closed $
                    tcBindGroups top_lvl sig_fn prag_fn groups thing_inside
@@ -405,8 +462,8 @@ tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
 ------------------------
 tc_group :: forall thing.
             TopLevelFlag -> TcSigFun -> TcPragEnv
-         -> (RecFlag, LHsBinds Name) -> IsGroupClosed -> TcM thing
-         -> TcM ([(RecFlag, LHsBinds TcId)], thing)
+         -> (RecFlag, LHsBinds GhcRn) -> IsGroupClosed -> TcM thing
+         -> TcM ([(RecFlag, LHsBinds GhcTcId)], thing)
 
 -- Typecheck one strongly-connected component of the original program.
 -- We get a list of groups back, because there may
@@ -440,13 +497,14 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
     isPatSyn PatSynBind{} = True
     isPatSyn _ = False
 
-    sccs :: [SCC (LHsBind Name)]
-    sccs = stronglyConnCompFromEdgedVertices (mkEdges sig_fn binds)
+    sccs :: [SCC (LHsBind GhcRn)]
+    sccs = stronglyConnCompFromEdgedVerticesUniq (mkEdges sig_fn binds)
 
-    go :: [SCC (LHsBind Name)] -> TcM (LHsBinds TcId, thing)
+    go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTcId, thing)
     go (scc:sccs) = do  { (binds1, ids1) <- tc_scc scc
-                        ; (binds2, thing) <- tcExtendLetEnv top_lvl closed ids1
-                                                            (go sccs)
+                        ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn
+                                                            closed ids1 $
+                                             go sccs
                         ; return (binds1 `unionBags` binds2, thing) }
     go []         = do  { thing <- thing_inside; return (emptyBag, thing) }
 
@@ -454,9 +512,9 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
     tc_scc (CyclicSCC binds) = tc_sub_group Recursive    binds
 
     tc_sub_group rec_tc binds =
-      tcPolyBinds top_lvl sig_fn prag_fn Recursive rec_tc closed binds
+      tcPolyBinds sig_fn prag_fn Recursive rec_tc closed binds
 
-recursivePatSynErr :: OutputableBndr name => LHsBinds name -> TcM a
+recursivePatSynErr :: OutputableBndrId name => LHsBinds name -> TcM a
 recursivePatSynErr binds
   = failWithTc $
     hang (text "Recursive pattern synonym definition with following bindings:")
@@ -468,8 +526,8 @@ recursivePatSynErr binds
 
 tc_single :: forall thing.
             TopLevelFlag -> TcSigFun -> TcPragEnv
-          -> LHsBind Name -> IsGroupClosed -> TcM thing
-          -> TcM (LHsBinds TcId, thing)
+          -> LHsBind GhcRn -> IsGroupClosed -> TcM thing
+          -> TcM (LHsBinds GhcTcId, thing)
 tc_single _top_lvl sig_fn _prag_fn
           (L _ (PatSynBind psb@PSB{ psb_id = L _ name }))
           _ thing_inside
@@ -478,28 +536,28 @@ tc_single _top_lvl sig_fn _prag_fn
        ; return (aux_binds, thing)
        }
   where
-    tc_pat_syn_decl :: TcM (LHsBinds TcId, TcGblEnv)
+    tc_pat_syn_decl :: TcM (LHsBinds GhcTcId, TcGblEnv)
     tc_pat_syn_decl = case sig_fn name of
         Nothing                 -> tcInferPatSynDecl psb
         Just (TcPatSynSig tpsi) -> tcCheckPatSynDecl psb tpsi
         Just                 _  -> panic "tc_single"
 
 tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
-  = do { (binds1, ids) <- tcPolyBinds top_lvl sig_fn prag_fn
+  = do { (binds1, ids) <- tcPolyBinds sig_fn prag_fn
                                       NonRecursive NonRecursive
                                       closed
                                       [lbind]
-       ; thing <- tcExtendLetEnv top_lvl closed ids thing_inside
+       ; thing <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside
        ; return (binds1, thing) }
 
 ------------------------
 type BKey = Int -- Just number off the bindings
 
-mkEdges :: TcSigFun -> LHsBinds Name -> [Node BKey (LHsBind Name)]
+mkEdges :: TcSigFun -> LHsBinds GhcRn -> [Node BKey (LHsBind GhcRn)]
 -- See Note [Polymorphic recursion] in HsBinds.
 mkEdges sig_fn binds
-  = [ (bind, key, [key | n <- nonDetEltsUFM (bind_fvs (unLoc bind)),
-                         Just key <- [lookupNameEnv key_map n], no_sig n ])
+  = [ DigraphNode bind key [key | n <- nonDetEltsUniqSet (bind_fvs (unLoc bind)),
+                         Just key <- [lookupNameEnv key_map n], no_sig n ]
     | (bind, key) <- keyd_binds
     ]
     -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
@@ -507,7 +565,7 @@ mkEdges sig_fn binds
     -- as explained in Note [Deterministic SCC] in Digraph.
   where
     no_sig :: Name -> Bool
-    no_sig n = noCompleteSig (sig_fn n)
+    no_sig n = not (hasCompleteSig sig_fn n)
 
     keyd_binds = bagToList binds `zip` [0::BKey ..]
 
@@ -516,13 +574,13 @@ mkEdges sig_fn binds
                                      , bndr <- collectHsBindBinders bind ]
 
 ------------------------
-tcPolyBinds :: TopLevelFlag -> TcSigFun -> TcPragEnv
+tcPolyBinds :: TcSigFun -> TcPragEnv
             -> RecFlag         -- Whether the group is really recursive
             -> RecFlag         -- Whether it's recursive after breaking
                                -- dependencies based on type signatures
             -> IsGroupClosed   -- Whether the group is closed
-            -> [LHsBind Name]  -- None are PatSynBind
-            -> TcM (LHsBinds TcId, [TcId])
+            -> [LHsBind GhcRn]  -- None are PatSynBind
+            -> TcM (LHsBinds GhcTcId, [TcId])
 
 -- Typechecks a single bunch of values bindings all together,
 -- and generalises them.  The bunch may be only part of a recursive
@@ -535,7 +593,7 @@ tcPolyBinds :: TopLevelFlag -> TcSigFun -> TcPragEnv
 -- Knows nothing about the scope of the bindings
 -- None of the bindings are pattern synonyms
 
-tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list
+tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list
   = setSrcSpan loc                              $
     recoverM (recoveryCode binder_names sig_fn) $ do
         -- Set up main recover; take advantage of any type sigs
@@ -545,15 +603,11 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list
     ; dflags   <- getDynFlags
     ; let plan = decideGeneralisationPlan dflags bind_list closed sig_fn
     ; traceTc "Generalisation plan" (ppr plan)
-    ; result@(tc_binds, poly_ids) <- case plan of
+    ; result@(_, poly_ids) <- case plan of
          NoGen              -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
          InferGen mn        -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list
          CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind
 
-        -- Check whether strict bindings are ok
-        -- These must be non-recursive etc, and are not generalised
-        -- They desugar to a case expression in the end
-    ; checkStrictBinds top_lvl rec_group bind_list tc_binds poly_ids
     ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group
                                             , vcat [ppr id <+> ppr (idType id) | id <- poly_ids]
                                           ])
@@ -570,7 +624,7 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc closed bind_list
 -- If typechecking the binds fails, then return with each
 -- signature-less binder given type (forall a.a), to minimise
 -- subsequent error messages
-recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds TcId, [Id])
+recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds GhcTcId, [Id])
 recoveryCode binder_names sig_fn
   = do  { traceTc "tcBindsWithSigs: error recovery" (ppr binder_names)
         ; let poly_ids = map mk_dummy binder_names
@@ -596,8 +650,8 @@ tcPolyNoGen     -- No generalisation whatsoever
   :: RecFlag       -- Whether it's recursive after breaking
                    -- dependencies based on type signatures
   -> TcPragEnv -> TcSigFun
-  -> [LHsBind Name]
-  -> TcM (LHsBinds TcId, [TcId])
+  -> [LHsBind GhcRn]
+  -> TcM (LHsBinds GhcTcId, [TcId])
 
 tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
   = do { (binds', mono_infos) <- tcMonoBinds rec_tc tc_sig_fn
@@ -607,11 +661,8 @@ tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
        ; return (binds', mono_ids') }
   where
     tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id })
-      = do { mono_ty' <- zonkTcType (idType mono_id)
-             -- Zonk, mainly to expose unboxed types to checkStrictBinds
-           ; let mono_id' = setIdType mono_id mono_ty'
-           ; _specs <- tcSpecPrags mono_id' (lookupPragEnv prag_fn name)
-           ; return mono_id' }
+      = do { _specs <- tcSpecPrags mono_id (lookupPragEnv prag_fn name)
+           ; return mono_id }
            -- NB: tcPrags generates error messages for
            --     specialisation pragmas for non-overloaded sigs
            -- Indeed that is why we call it here!
@@ -626,8 +677,8 @@ tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
 
 tcPolyCheck :: TcPragEnv
             -> TcIdSigInfo     -- Must be a complete signature
-            -> LHsBind Name    -- Must be a FunBind
-            -> TcM (LHsBinds TcId, [TcId])
+            -> LHsBind GhcRn   -- Must be a FunBind
+            -> TcM (LHsBinds GhcTcId, [TcId])
 -- There is just one binding,
 --   it is a Funbind
 --   it has a complete type signature,
@@ -639,13 +690,13 @@ tcPolyCheck prag_fn
                             , fun_matches = matches }))
   = setSrcSpan sig_loc $
     do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
-       ; (tv_prs, theta, tau) <- tcInstType (tcInstSigTyVars sig_loc) poly_id
+       ; (tv_prs, theta, tau) <- tcInstType tcInstSkolTyVars poly_id
                 -- See Note [Instantiate sig with fresh variables]
 
        ; mono_name <- newNameAt (nameOccName name) nm_loc
        ; ev_vars   <- newEvVars theta
        ; let mono_id   = mkLocalId mono_name tau
-             skol_info = SigSkol ctxt (mkPhiTy theta tau)
+             skol_info = SigSkol ctxt (idType poly_id) tv_prs
              skol_tvs  = map snd tv_prs
 
        ; (ev_binds, (co_fn, matches'))
@@ -659,25 +710,48 @@ tcPolyCheck prag_fn
        ; spec_prags <- tcSpecPrags poly_id prag_sigs
        ; poly_id    <- addInlinePrags poly_id prag_sigs
 
+       ; mod <- getModule
        ; let bind' = FunBind { fun_id      = L nm_loc mono_id
                              , fun_matches = matches'
                              , fun_co_fn   = co_fn
                              , bind_fvs    = placeHolderNamesTc
-                             , fun_tick    = [] }
+                             , fun_tick    = funBindTicks nm_loc mono_id mod prag_sigs }
+
+             export = ABE { abe_wrap = idHsWrapper
+                          , abe_poly  = poly_id
+                          , abe_mono  = mono_id
+                          , abe_prags = SpecPrags spec_prags }
 
-             abs_bind = L loc $ AbsBindsSig
-                        { abs_sig_export  = poly_id
-                        , abs_tvs         = skol_tvs
-                        , abs_ev_vars     = ev_vars
-                        , abs_sig_prags   = SpecPrags spec_prags
-                        , abs_sig_ev_bind = ev_binds
-                        , abs_sig_bind    = L loc bind' }
+             abs_bind = L loc $
+                        AbsBinds { abs_tvs      = skol_tvs
+                                 , abs_ev_vars  = ev_vars
+                                 , abs_ev_binds = [ev_binds]
+                                 , abs_exports  = [export]
+                                 , abs_binds    = unitBag (L loc bind')
+                                 , abs_sig      = True }
 
        ; return (unitBag abs_bind, [poly_id]) }
 
 tcPolyCheck _prag_fn sig bind
   = pprPanic "tcPolyCheck" (ppr sig $$ ppr bind)
 
+funBindTicks :: SrcSpan -> TcId -> Module -> [LSig GhcRn]
+             -> [Tickish TcId]
+funBindTicks loc fun_id mod sigs
+  | (mb_cc_str : _) <- [ cc_name | L _ (SCCFunSig _ _ cc_name) <- sigs ]
+      -- this can only be a singleton list, as duplicate pragmas are rejected
+      -- by the renamer
+  , let cc_str
+          | Just cc_str <- mb_cc_str
+          = sl_fs $ unLoc cc_str
+          | otherwise
+          = getOccFS (Var.varName fun_id)
+        cc_name = moduleNameFS (moduleName mod) `appendFS` consFS '.' cc_str
+        cc = mkUserCC cc_name mod loc (getUnique fun_id)
+  = [ProfNote cc True True]
+  | otherwise
+  = []
+
 {- Note [Instantiate sig with fresh variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 It's vital to instantiate a type signature with fresh variables.
@@ -703,33 +777,35 @@ tcPolyInfer
                    -- dependencies based on type signatures
   -> TcPragEnv -> TcSigFun
   -> Bool         -- True <=> apply the monomorphism restriction
-  -> [LHsBind Name]
-  -> TcM (LHsBinds TcId, [TcId])
+  -> [LHsBind GhcRn]
+  -> TcM (LHsBinds GhcTcId, [TcId])
 tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
   = do { (tclvl, wanted, (binds', mono_infos))
              <- pushLevelAndCaptureConstraints  $
                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
 
-       ; let name_taus = [ (mbi_poly_name info, idType (mbi_mono_id info))
-                         | info <- mono_infos ]
-             sigs      = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ]
+       ; let name_taus  = [ (mbi_poly_name info, idType (mbi_mono_id info))
+                          | info <- mono_infos ]
+             sigs       = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ]
+             infer_mode = if mono then ApplyMR else NoRestrictions
 
        ; mapM_ (checkOverloadedSig mono) sigs
 
        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
-       ; (qtvs, givens, ev_binds)
-                 <- simplifyInfer tclvl mono sigs name_taus wanted
+       ; (qtvs, givens, ev_binds, insoluble)
+                 <- simplifyInfer tclvl infer_mode sigs name_taus wanted
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
-                    mapM (mkExport prag_fn qtvs inferred_theta) mono_infos
+                    mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos
 
        ; loc <- getSrcSpanM
        ; let poly_ids = map abe_poly exports
              abs_bind = L loc $
                         AbsBinds { abs_tvs = qtvs
                                  , abs_ev_vars = givens, abs_ev_binds = [ev_binds]
-                                 , abs_exports = exports, abs_binds = binds' }
+                                 , abs_exports = exports, abs_binds = binds'
+                                 , abs_sig = False }
 
        ; traceTc "Binding:" (ppr (poly_ids `zip` map idType poly_ids))
        ; return (unitBag abs_bind, poly_ids) }
@@ -737,9 +813,11 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
 
 --------------
 mkExport :: TcPragEnv
+         -> Bool                        -- True <=> there was an insoluble type error
+                                        --          when typechecking the bindings
          -> [TyVar] -> TcThetaType      -- Both already zonked
          -> MonoBindInfo
-         -> TcM (ABExport Id)
+         -> TcM (ABExport GhcTc)
 -- Only called for generalisation plan InferGen, not by CheckGen or NoGen
 --
 -- mkExport generates exports with
@@ -753,32 +831,32 @@ mkExport :: TcPragEnv
 
 -- Pre-condition: the qtvs and theta are already zonked
 
-mkExport prag_fn qtvs theta
+mkExport prag_fn insoluble qtvs theta
          mono_info@(MBI { mbi_poly_name = poly_name
                         , mbi_sig       = mb_sig
                         , mbi_mono_id   = mono_id })
   = do  { mono_ty <- zonkTcType (idType mono_id)
-        ; poly_id <- mkInferredPolyId qtvs theta poly_name mb_sig mono_ty
+        ; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty
 
         -- NB: poly_id has a zonked type
         ; poly_id <- addInlinePrags poly_id prag_sigs
         ; spec_prags <- tcSpecPrags poly_id prag_sigs
                 -- tcPrags requires a zonked poly_id
 
-        -- See Note [Impedence matching]
+        -- See Note [Impedance matching]
         -- NB: we have already done checkValidType, including an ambiguity check,
         --     on the type; either when we checked the sig or in mkInferredPolyId
         ; let poly_ty     = idType poly_id
-              sel_poly_ty = mkInvSigmaTy qtvs theta mono_ty
+              sel_poly_ty = mkInfSigmaTy qtvs theta mono_ty
                 -- This type is just going into tcSubType,
-                -- so Inv vs. Spec doesn't matter
+                -- so Inferred vs. Specified doesn't matter
 
         ; wrap <- if sel_poly_ty `eqType` poly_ty  -- NB: eqType ignores visibility
                   then return idHsWrapper  -- Fast path; also avoids complaint when we infer
-                                           -- an ambiguouse type and have AllowAmbiguousType
+                                           -- an ambiguous type and have AllowAmbiguousType
                                            -- e..g infer  x :: forall a. F a -> Int
-                  else addErrCtxtM (mk_impedence_match_msg mono_info sel_poly_ty poly_ty) $
-                       tcSubType_NC sig_ctxt sel_poly_ty (mkCheckExpType poly_ty)
+                  else addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $
+                       tcSubType_NC sig_ctxt sel_poly_ty poly_ty
 
         ; warn_missing_sigs <- woptM Opt_WarnMissingLocalSignatures
         ; when warn_missing_sigs $
@@ -786,24 +864,26 @@ mkExport prag_fn qtvs theta
 
         ; return (ABE { abe_wrap = wrap
                         -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => mono_ty)
-                      , abe_poly = poly_id
-                      , abe_mono = mono_id
-                      , abe_prags = SpecPrags spec_prags}) }
+                      , abe_poly  = poly_id
+                      , abe_mono  = mono_id
+                      , abe_prags = SpecPrags spec_prags }) }
   where
     prag_sigs = lookupPragEnv prag_fn poly_name
     sig_ctxt  = InfSigCtxt poly_name
 
-mkInferredPolyId :: [TyVar] -> TcThetaType
+mkInferredPolyId :: Bool  -- True <=> there was an insoluble error when
+                          --          checking the binding group for this Id
+                 -> [TyVar] -> TcThetaType
                  -> Name -> Maybe TcIdSigInst -> TcType
                  -> TcM TcId
-mkInferredPolyId qtvs inferred_theta poly_name mb_sig_inst mono_ty
+mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
   | Just (TISI { sig_inst_sig = sig })  <- mb_sig_inst
   , CompleteSig { sig_bndr = poly_id } <- sig
   = return poly_id
 
   | otherwise  -- Either no type sig or partial type sig
   = checkNoErrs $  -- The checkNoErrs ensures that if the type is ambiguous
-                   -- we don't carry on to the impedence matching, and generate
+                   -- we don't carry on to the impedance matching, and generate
                    -- a duplicate ambiguity error.  There is a similar
                    -- checkNoErrs for complete type signatures too.
     do { fam_envs <- tcGetFamInstEnvs
@@ -824,9 +904,13 @@ mkInferredPolyId qtvs inferred_theta poly_name mb_sig_inst mono_ty
 
        ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
                                           , ppr inferred_poly_ty])
-       ; addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
+       ; unless insoluble $
+         addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
          checkValidType (InfSigCtxt poly_name) inferred_poly_ty
          -- See Note [Validity of inferred types]
+         -- If we found an insoluble error in the function definition, don't
+         -- do this check; otherwise (Trac #14000) we may report an ambiguity
+         -- error for a rather bogus type.
 
        ; return (mkLocalIdOrCoVar poly_name inferred_poly_ty) }
 
@@ -841,7 +925,7 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
     do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
                         -- Include kind variables!  Trac #7916
              my_theta = pickCapturedPreds free_tvs inferred_theta
-             binders  = [ mkTyVarBinder Invisible tv
+             binders  = [ mkTyVarBinder Inferred tv
                         | tv <- qtvs
                         , tv `elemVarSet` free_tvs ]
        ; return (binders, my_theta) }
@@ -856,13 +940,21 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
        ; let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
                                         `unionVarSet` tau_tvs)
        ; traceTc "ciq" (vcat [ ppr sig, ppr annotated_theta, ppr free_tvs])
-       ; return (mk_binders free_tvs, annotated_theta) }
+       ; psig_qtvs <- mk_psig_qtvs annotated_tvs
+       ; return (mk_final_qtvs psig_qtvs free_tvs, annotated_theta) }
 
   | Just wc_var <- wcx
   = do { annotated_theta <- zonkTcTypes annotated_theta
-       ; let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
-                                        `unionVarSet` tau_tvs)
-             my_theta = pickCapturedPreds free_tvs inferred_theta
+       ; let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs)
+                          -- growThetaVars just like the no-type-sig case
+                          -- Omitting this caused #12844
+             seed_tvs = tyCoVarsOfTypes annotated_theta  -- These are put there
+                        `unionVarSet` tau_tvs            --       by the user
+
+       ; psig_qtvs <- mk_psig_qtvs annotated_tvs
+       ; let my_qtvs  = mk_final_qtvs psig_qtvs free_tvs
+             keep_me  = psig_qtvs `unionVarSet` free_tvs
+             my_theta = pickCapturedPreds keep_me inferred_theta
 
        -- Report the inferred constraints for an extra-constraints wildcard/hole as
        -- an error message, unless the PartialTypeSignatures flag is enabled. In this
@@ -878,30 +970,35 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                  , ppr annotated_theta, ppr inferred_theta
                  , ppr inferred_diff ]
 
-       ; return (mk_binders free_tvs, my_theta) }
+       ; return (my_qtvs, my_theta) }
 
   | otherwise  -- A complete type signature is dealt with in mkInferredPolyId
   = pprPanic "chooseInferredQuantifiers" (ppr sig)
 
   where
-    spec_tv_set = mkVarSet $ map snd annotated_tvs
-    mk_binders free_tvs
+    mk_final_qtvs psig_qtvs free_tvs
       = [ mkTyVarBinder vis tv
-        | tv <- qtvs
-        , tv `elemVarSet` free_tvs
-        , let vis | tv `elemVarSet` spec_tv_set = Specified
-                  | otherwise                   = Invisible ]
-                          -- Pulling from qtvs maintains original order
+        | tv <- qtvs -- Pulling from qtvs maintains original order
+        , tv `elemVarSet` keep_me
+        , let vis | tv `elemVarSet` psig_qtvs = Specified
+                  | otherwise                 = Inferred ]
+      where
+        keep_me = free_tvs `unionVarSet` psig_qtvs
 
     mk_ctuple [pred] = return pred
     mk_ctuple preds  = do { tc <- tcLookupTyCon (cTupleTyConName (length preds))
                           ; return (mkTyConApp tc preds) }
 
-mk_impedence_match_msg :: MonoBindInfo
+    mk_psig_qtvs :: [(Name,TcTyVar)] -> TcM TcTyVarSet
+    mk_psig_qtvs annotated_tvs
+       = do { psig_qtvs <- mapM (zonkTcTyVarToTyVar . snd) annotated_tvs
+            ; return (mkVarSet psig_qtvs) }
+
+mk_impedance_match_msg :: MonoBindInfo
                        -> TcType -> TcType
                        -> TidyEnv -> TcM (TidyEnv, SDoc)
 -- This is a rare but rather awkward error messages
-mk_impedence_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
+mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
                        inf_ty sig_ty tidy_env
  = do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env  inf_ty
       ; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty
@@ -1008,7 +1105,7 @@ Examples that might fail:
  - an inferred type that includes unboxed tuples
 
 
-Note [Impedence matching]
+Note [Impedance matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
    f 0 x = x
@@ -1053,7 +1150,7 @@ where F is a non-injective type function.
 *                                                                      *
 ********************************************************************* -}
 
-tcVectDecls :: [LVectDecl Name] -> TcM ([LVectDecl TcId])
+tcVectDecls :: [LVectDecl GhcRn] -> TcM ([LVectDecl GhcTcId])
 tcVectDecls decls
   = do { decls' <- mapM (wrapLocM tcVect) decls
        ; let ids  = [lvectDeclName decl | decl <- decls', not $ lvectInstDecl decl]
@@ -1069,7 +1166,7 @@ tcVectDecls decls
     reportVectDups _ = return ()
 
 --------------
-tcVect :: VectDecl Name -> TcM (VectDecl TcId)
+tcVect :: VectDecl GhcRn -> TcM (VectDecl GhcTcId)
 -- FIXME: We can't typecheck the expression of a vectorisation declaration against the vectorised
 --   type of the original definition as this requires internals of the vectoriser not available
 --   during type checking.  Instead, constrain the rhs of a vectorisation declaration to be a single
@@ -1154,58 +1251,6 @@ for a non-overloaded function.
 
 @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
 The signatures have been dealt with already.
-
-Note [Pattern bindings]
-~~~~~~~~~~~~~~~~~~~~~~~
-The rule for typing pattern bindings is this:
-
-    ..sigs..
-    p = e
-
-where 'p' binds v1..vn, and 'e' may mention v1..vn,
-typechecks exactly like
-
-    ..sigs..
-    x = e       -- Inferred type
-    v1 = case x of p -> v1
-    ..
-    vn = case x of p -> vn
-
-Note that
-    (f :: forall a. a -> a) = id
-should not typecheck because
-       case id of { (f :: forall a. a->a) -> f }
-will not typecheck.
-
-Note [Instantiate when inferring a type]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-  f = (*)
-As there is no incentive to instantiate the RHS, tcMonoBinds will
-produce a type of forall a. Num a => a -> a -> a for `f`. This will then go
-through simplifyInfer and such, remaining unchanged.
-
-There are two problems with this:
- 1) If the definition were `g _ = (*)`, we get a very unusual type of
-    `forall {a}. a -> forall b. Num b => b -> b -> b` for `g`. This is
-    surely confusing for users.
-
- 2) The monomorphism restriction can't work. The MR is dealt with in
-    simplifyInfer, and simplifyInfer has no way of instantiating. This
-    could perhaps be worked around, but it may be hard to know even
-    when instantiation should happen.
-
-There is an easy solution to both problems: instantiate (deeply) when
-inferring a type. So that's what we do. Note that this decision is
-user-facing.
-
-We do this deep instantiation in tcMonoBinds, in the FunBind case
-only, and only when we do not have a type signature.  Conveniently,
-the fun_co_fn field of FunBind gives a place to record the coercion.
-
-We do not need to do this
- * for PatBinds, because we don't have a function type
- * for FunBinds where we have a signature, bucause we aren't doing inference
 -}
 
 data MonoBindInfo = MBI { mbi_poly_name :: Name
@@ -1216,41 +1261,37 @@ tcMonoBinds :: RecFlag  -- Whether the binding is recursive for typechecking pur
                         -- i.e. the binders are mentioned in their RHSs, and
                         --      we are not rescued by a type signature
             -> TcSigFun -> LetBndrSpec
-            -> [LHsBind Name]
-            -> TcM (LHsBinds TcId, [MonoBindInfo])
+            -> [LHsBind GhcRn]
+            -> TcM (LHsBinds GhcTcId, [MonoBindInfo])
 tcMonoBinds is_rec sig_fn no_gen
            [ L b_loc (FunBind { fun_id = L nm_loc name,
                                 fun_matches = matches, bind_fvs = fvs })]
                              -- Single function binding,
   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
   , Nothing <- sig_fn name   -- ...with no type signature
-  =     -- In this very special case we infer the type of the
+  =     -- Note [Single function non-recursive binding special-case]
+        -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+        -- In this very special case we infer the type of the
         -- right hand side first (it may have a higher-rank type)
         -- and *then* make the monomorphic Id for the LHS
         -- e.g.         f = \(x::forall a. a->a) -> <body>
         --      We want to infer a higher-rank type for f
     setSrcSpan b_loc    $
-    do  { rhs_ty <- newOpenInferExpType
-        ; (co_fn, matches')
-            <- tcExtendIdBndrs [TcIdBndr_ExpType name rhs_ty NotTopLevel] $
+    do  { ((co_fn, matches'), rhs_ty)
+            <- tcInferInst $ \ exp_ty ->
+                  -- tcInferInst: see TcUnify,
+                  -- Note [Deep instantiation of InferResult]
+               tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $
                   -- We extend the error context even for a non-recursive
                   -- function so that in type error messages we show the
                   -- type of the thing whose rhs we are type checking
-               tcMatchesFun (L nm_loc name) matches rhs_ty
-        ; rhs_ty  <- readExpType rhs_ty
-
-        -- Deeply instantiate the inferred type
-        -- See Note [Instantiate when inferring a type]
-        ; let orig = matchesCtOrigin matches
-        ; rhs_ty <- zonkTcType rhs_ty -- NB: zonk to uncover any foralls
-        ; (inst_wrap, rhs_ty) <- addErrCtxtM (instErrCtxt name rhs_ty) $
-                                 deeplyInstantiate orig rhs_ty
+               tcMatchesFun (L nm_loc name) matches exp_ty
 
         ; mono_id <- newLetBndr no_gen name rhs_ty
         ; return (unitBag $ L b_loc $
                      FunBind { fun_id = L nm_loc mono_id,
                                fun_matches = matches', bind_fvs = fvs,
-                               fun_co_fn = inst_wrap <.> co_fn, fun_tick = [] },
+                               fun_co_fn = co_fn, fun_tick = [] },
                   [MBI { mbi_poly_name = name
                        , mbi_sig       = Nothing
                        , mbi_mono_id   = mono_id }]) }
@@ -1272,7 +1313,7 @@ tcMonoBinds _ sig_fn no_gen binds
 
         ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
                                        | (n,id) <- rhs_id_env]
-        ; binds' <- tcExtendLetEnvIds NotTopLevel rhs_id_env $
+        ; binds' <- tcExtendRecIds rhs_id_env $
                     mapM (wrapLocM tcRhs) tc_binds
 
         ; return (listToBag binds', mono_infos) }
@@ -1295,73 +1336,86 @@ tcMonoBinds _ sig_fn no_gen binds
 -- it; hence the TcMonoBind data type in which the LHS is done but the RHS isn't
 
 data TcMonoBind         -- Half completed; LHS done, RHS not done
-  = TcFunBind  MonoBindInfo  SrcSpan (MatchGroup Name (LHsExpr Name))
-  | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name (LHsExpr Name)) TcSigmaType
+  = TcFunBind  MonoBindInfo  SrcSpan (MatchGroup GhcRn (LHsExpr GhcRn))
+  | TcPatBind [MonoBindInfo] (LPat GhcTcId) (GRHSs GhcRn (LHsExpr GhcRn))
+              TcSigmaType
+
+tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
+-- Only called with plan InferGen (LetBndrSpec = LetLclBndr)
+--                    or NoGen    (LetBndrSpec = LetGblBndr)
+-- CheckGen is used only for functions with a complete type signature,
+--          and tcPolyCheck doesn't use tcMonoBinds at all
 
-tcLhs :: TcSigFun -> LetBndrSpec -> HsBind Name -> TcM TcMonoBind
 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name, fun_matches = matches })
-  = do { mono_info <- tcLhsId sig_fn no_gen name
+  | Just (TcIdSig sig) <- sig_fn name
+  = -- There is a type signature.
+    -- It must be partial; if complete we'd be in tcPolyCheck!
+    --    e.g.   f :: _ -> _
+    --           f x = ...g...
+    --           Just g = ...f...
+    -- Hence always typechecked with InferGen
+    do { mono_info <- tcLhsSigId no_gen (name, sig)
+       ; return (TcFunBind mono_info nm_loc matches) }
+
+  | otherwise  -- No type signature
+  = do { mono_ty <- newOpenFlexiTyVarTy
+       ; mono_id <- newLetBndr no_gen name mono_ty
+       ; let mono_info = MBI { mbi_poly_name = name
+                             , mbi_sig       = Nothing
+                             , mbi_mono_id   = mono_id }
        ; return (TcFunBind mono_info nm_loc matches) }
 
 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
-  = do  { let bndr_names = collectPatBinders pat
-        ; mbis <- mapM (tcLhsId sig_fn no_gen) bndr_names
-            -- See Note [Existentials in pattern bindings]
+  = -- See Note [Typechecking pattern bindings]
+    do  { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names
 
         ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $
-                             bndr_names `zip` map mbi_mono_id mbis
+                             [ (mbi_poly_name mbi, mbi_mono_id mbi)
+                             | mbi <- sig_mbis ]
+
+            -- See Note [Existentials in pattern bindings]
+        ; ((pat', nosig_mbis), pat_ty)
+            <- addErrCtxt (patMonoBindsCtxt pat grhss) $
+               tcInferNoInst $ \ exp_ty ->
+               tcLetPat inst_sig_fun no_gen pat exp_ty $
+               mapM lookup_info nosig_names
+
+        ; let mbis = sig_mbis ++ nosig_mbis
 
         ; traceTc "tcLhs" (vcat [ ppr id <+> dcolon <+> ppr (idType id)
                                 | mbi <- mbis, let id = mbi_mono_id mbi ]
                            $$ ppr no_gen)
 
-        ; ((pat', _), pat_ty) <- addErrCtxt (patMonoBindsCtxt pat grhss) $
-                                 tcInfer $ \ exp_ty ->
-                                 tcLetPat inst_sig_fun pat exp_ty $
-                                 return () -- mapM (lookup_info inst_sig_fun) bndr_names
-
         ; return (TcPatBind mbis pat' grhss pat_ty) }
+  where
+    bndr_names = collectPatBinders pat
+    (nosig_names, sig_names) = partitionWith find_sig bndr_names
+
+    find_sig :: Name -> Either Name (Name, TcIdSigInfo)
+    find_sig name = case sig_fn name of
+                      Just (TcIdSig sig) -> Right (name, sig)
+                      _                  -> Left name
+
+      -- After typechecking the pattern, look up the binder
+      -- names that lack a signature, which the pattern has brought
+      -- into scope.
+    lookup_info :: Name -> TcM MonoBindInfo
+    lookup_info name
+      = do { mono_id <- tcLookupId name
+           ; return (MBI { mbi_poly_name = name
+                         , mbi_sig       = Nothing
+                         , mbi_mono_id   = mono_id }) }
 
 tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
         -- AbsBind, VarBind impossible
 
 -------------------
-data LetBndrSpec
-  = LetLclBndr            -- We are going to generalise, and wrap in an AbsBinds
-                          -- so clone a fresh binder for the local monomorphic Id
-
-  | LetGblBndr TcPragEnv  -- Generalisation plan is NoGen, so there isn't going
-                          -- to be an AbsBinds; So we must bind the global version
-                          -- of the binder right away.
-                          -- And here is the inline-pragma information
-
-instance Outputable LetBndrSpec where
-  ppr LetLclBndr      = text "LetLclBndr"
-  ppr (LetGblBndr {}) = text "LetGblBndr"
-
-tcLhsId :: TcSigFun -> LetBndrSpec -> Name -> TcM MonoBindInfo
-tcLhsId sig_fn no_gen name
-  | Just (TcIdSig sig) <- sig_fn name
-  = -- A partial type signature on a FunBind, in a mixed group
-    --    e.g.   f :: _ -> _
-    --           f x = ...g...
-    --           Just g = ...f...
-    -- Hence always typechecked with InferGen; hence LetLclBndr
-    --
-    -- A compelete type sig on a FunBind is checked with CheckGen
-    -- and does not go via tcLhsId
-    do { inst_sig <- tcInstSig sig
-       ; the_id <- newSigLetBndr no_gen name inst_sig
+tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
+tcLhsSigId no_gen (name, sig)
+  = do { inst_sig <- tcInstSig sig
+       ; mono_id <- newSigLetBndr no_gen name inst_sig
        ; return (MBI { mbi_poly_name = name
                      , mbi_sig       = Just inst_sig
-                     , mbi_mono_id   = the_id }) }
-
-  | otherwise
-  = -- No type signature, plan InferGen (LetLclBndr) or NoGen (LetGblBndr)
-    do { mono_ty <- newOpenFlexiTyVarTy
-       ; mono_id <- newLetBndr no_gen name mono_ty
-       ; return (MBI { mbi_poly_name = name
-                     , mbi_sig       = Nothing
                      , mbi_mono_id   = mono_id }) }
 
 ------------
@@ -1372,22 +1426,8 @@ newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig })
 newSigLetBndr no_gen name (TISI { sig_inst_tau = tau })
   = newLetBndr no_gen name tau
 
-newLetBndr :: LetBndrSpec -> Name -> TcType -> TcM TcId
--- In the polymorphic case when we are going to generalise
---    (plan InferGen, 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 when we are not going to generalise
---    (plan NoGen, no_gen = LetGblBndr) there is no AbsBinds,
---    and we use the original name directly
-newLetBndr LetLclBndr name ty
-  = do { mono_name <- cloneLocalName name
-       ; return (mkLocalId mono_name ty) }
-newLetBndr (LetGblBndr prags) name ty
-  = addInlinePrags (mkLocalId name ty) (lookupPragEnv prags name)
-
 -------------------
-tcRhs :: TcMonoBind -> TcM (HsBind TcId)
+tcRhs :: TcMonoBind -> TcM (HsBind GhcTcId)
 tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
                  loc matches)
   = tcExtendIdBinderStackForRhs [info]  $
@@ -1454,9 +1494,13 @@ getMonoBindInfo tc_binds
     get_info (TcFunBind info _ _)    rest = info : rest
     get_info (TcPatBind infos _ _ _) rest = infos ++ rest
 
-{- Note [Existentials in pattern bindings]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider (typecheck/should_compile/ExPat):
+
+{- Note [Typechecking pattern bindings]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Look at:
+   - typecheck/should_compile/ExPat
+   - Trac #12427, typecheck/should_compile/T12427{a,b}
+
   data T where
     MkT :: Integral a => a -> Int -> T
 
@@ -1468,48 +1512,96 @@ and suppose t :: T.  Which of these pattern bindings are ok?
 
   E3. let { MkT (toInteger -> r) _ = t } in <body>
 
-Well (E1) is clearly wrong becuase the existential 'a' escapes.
-What type could 'p' possibly have?
+* (E1) is clearly wrong because the existential 'a' escapes.
+  What type could 'p' possibly have?
 
-But (E2) is fine, despite the existential pattern, because
-q::Int, and nothing escapes.
+* (E2) is fine, despite the existential pattern, because
+  q::Int, and nothing escapes.
 
-Even (E3) is fine.  The existential pattern binds a dictionary
-for (Integral a) which the view pattern can use to convert the
-a-valued field to an Integer, so r :: Integer.
+Even (E3) is fine.  The existential pattern binds a dictionary
+  for (Integral a) which the view pattern can use to convert the
+  a-valued field to an Integer, so r :: Integer.
 
 An easy way to see all three is to imagine the desugaring.
-For (2) it would look like
+For (E2) it would look like
     let q = case t of MkT _ q' -> q'
     in <body>
 
-We typecheck pattern bindings as follows:
-  1. In tcLhs we bind q'::alpha, for each variable q bound by the
-     pattern, where q' is a fresh name, and alpha is a fresh
-     unification variable; it will be the monomorphic verion of q that
-     we later generalise
 
-     It's very important that these fresh unification variables
-     alpha are born here, not deep under implications as would happen
-     if we allocated them when we encountered q during tcPat.
+We typecheck pattern bindings as follows.  First tcLhs does this:
+
+  1. Take each type signature q :: ty, partial or complete, and
+     instantiate it (with tcLhsSigId) to get a MonoBindInfo.  This
+     gives us a fresh "mono_id" qm :: instantiate(ty), where qm has
+     a fresh name.
+
+     Any fresh unification variables in instantiate(ty) born here, not
+     deep under implications as would happen if we allocated them when
+     we encountered q during tcPat.
+
+  2. Build a little environment mapping "q" -> "qm" for those Ids
+     with signatures (inst_sig_fun)
+
+  3. Invoke tcLetPat to typecheck the pattern.
+
+     - We pass in the current TcLevel.  This is captured by
+       TcPat.tcLetPat, and put into the pc_lvl field of PatCtxt, in
+       PatEnv.
+
+     - When tcPat finds an existential constructor, it binds fresh
+       type variables and dictionaries as usual, increments the TcLevel,
+       and emits an implication constraint.
 
-  2. Still in tcLhs, we build a little environment mappting "q" ->
-     q':alpha, and pass that to tcLetPet.
+     - When we come to a binder (TcPat.tcPatBndr), it looks it up
+       in the little environment (the pc_sig_fn field of PatCtxt).
 
-  3. Then tcLhs invokes tcLetPat to typecheck the patter as usual:
-     - When tcLetPat finds an existential constructor, it binds fresh
-       type variables and dictionaries as usual, and emits an
-       implication constraint.
+         Success => There was a type signature, so just use it,
+                    checking compatibility with the expected type.
+
+         Failure => No type sigature.
+             Infer case: (happens only outside any constructor pattern)
+                         use a unification variable
+                         at the outer level pc_lvl
+
+             Check case: use promoteTcType to promote the type
+                         to the outer level pc_lvl.  This is the
+                         place where we emit a constraint that'll blow
+                         up if existential capture takes place
+
+       Result: the type of the binder is always at pc_lvl. This is
+       crucial.
+
+  4. Throughout, when we are making up an Id for the pattern-bound variables
+     (newLetBndr), we have two cases:
+
+     - 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 impedance 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.)
 
-     - When tcLetPat finds a variable (TcPat.tcPatBndr) it looks it up
-       in the little environment, which should always succeed.  And
-       uses tcSubTypeET to connect the type of that variable with the
-       expected type of the pattern.
 
 And that's it!  The implication constraints check for the skolem
-escape.  It's quite simple and neat, and more exressive than before
+escape.  It's quite simple and neat, and more expressive than before
 e.g. GHC 8.0 rejects (E2) and (E3).
 
+Example for (E1), starting at level 1.  We generate
+     p :: beta:1, with constraints (forall:3 a. Integral a => a ~ beta)
+The (a~beta) can't float (because of the 'a'), nor be solved (because
+beta is untouchable.)
+
+Example for (E2), we generate
+     q :: beta:1, with constraint (forall:3 a. Integral a => Int ~ beta)
+The beta is untoucable, but floats out of the constraint and can
+be solved absolutely fine.
 
 ************************************************************************
 *                                                                      *
@@ -1523,9 +1615,9 @@ data GeneralisationPlan
   | InferGen            -- Implicit generalisation; there is an AbsBinds
        Bool             --   True <=> apply the MR; generalise only unconstrained type vars
 
-  | CheckGen (LHsBind Name) TcIdSigInfo
+  | CheckGen (LHsBind GhcRn) TcIdSigInfo
                         -- One FunBind with a signature
-                        -- Explicit generalisation; there is an AbsBindsSig
+                        -- Explicit generalisation
 
 -- A consequence of the no-AbsBinds choice (NoGen) is that there is
 -- no "polymorphic Id" and "monmomorphic Id"; there is just the one
@@ -1536,19 +1628,18 @@ instance Outputable GeneralisationPlan where
   ppr (CheckGen _ s) = text "CheckGen" <+> ppr s
 
 decideGeneralisationPlan
-   :: DynFlags -> [LHsBind Name] -> IsGroupClosed -> TcSigFun
+   :: DynFlags -> [LHsBind GhcRn] -> IsGroupClosed -> TcSigFun
    -> GeneralisationPlan
 decideGeneralisationPlan dflags lbinds closed sig_fn
-  | unlifted_pat_binds                       = NoGen
   | has_partial_sigs                         = InferGen (and partial_sig_mrs)
   | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig
-  | mono_local_binds closed                  = NoGen
+  | do_not_generalise closed                 = NoGen
   | otherwise                                = InferGen mono_restriction
   where
     binds = map unLoc lbinds
 
     partial_sig_mrs :: [Bool]
-    -- One for each parital signature (so empty => no partial sigs)
+    -- One for each partial signature (so empty => no partial sigs)
     -- The Bool is True if the signature has no constraint context
     --      so we should apply the MR
     -- See Note [Partial type signatures and generalisation]
@@ -1559,16 +1650,15 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
         , let (_, L _ theta, _) = splitLHsSigmaTy (hsSigWcType hs_ty) ]
 
     has_partial_sigs   = not (null partial_sig_mrs)
-    unlifted_pat_binds = any isUnliftedHsBind binds
-       -- Unlifted patterns (unboxed tuple) must not
-       -- be polymorphic, because we are going to force them
-       -- See Trac #4498, #8762
 
     mono_restriction  = xopt LangExt.MonomorphismRestriction dflags
                      && any restricted binds
 
-    mono_local_binds ClosedGroup = False
-    mono_local_binds _           = xopt LangExt.MonoLocalBinds dflags
+    do_not_generalise (IsGroupClosed _ True) = False
+        -- The 'True' means that all of the group's
+        -- free vars have ClosedTypeId=True; so we can ignore
+        -- -XMonoLocalBinds, and generalise anyway
+    do_not_generalise _ = xopt LangExt.MonoLocalBinds dflags
 
     -- With OutsideIn, all nested bindings are monomorphic
     -- except a single function binding with a signature
@@ -1584,155 +1674,61 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
     restricted (VarBind { var_id = v })                  = no_sig v
     restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
                                                            && no_sig (unLoc v)
-    restricted (PatSynBind {}) = panic "isRestrictedGroup/unrestricted PatSynBind"
-    restricted (AbsBinds {}) = panic "isRestrictedGroup/unrestricted AbsBinds"
-    restricted (AbsBindsSig {}) = panic "isRestrictedGroup/unrestricted AbsBindsSig"
+    restricted b = pprPanic "isRestrictedGroup/unrestricted" (ppr b)
 
-    restricted_match (MG { mg_alts = L _ (L _ (Match _ [] _ _) : _ )}) = True
-    restricted_match _                                                 = False
+    restricted_match mg = matchGroupArity mg == 0
         -- No args => like a pattern binding
         -- Some args => a function binding
 
-    no_sig n = noCompleteSig (sig_fn n)
+    no_sig n = not (hasCompleteSig sig_fn n)
 
-isClosedBndrGroup :: Bag (LHsBind Name) -> TcM IsGroupClosed
-isClosedBndrGroup binds = do
-    type_env <- getLclTypeEnv
-    if foldUFM (is_closed_ns type_env) True fv_env
-      then return ClosedGroup
-      else return $ NonClosedGroup fv_env
+isClosedBndrGroup :: TcTypeEnv -> Bag (LHsBind GhcRn) -> IsGroupClosed
+isClosedBndrGroup type_env binds
+  = IsGroupClosed fv_env type_closed
   where
+    type_closed = allUFM (nameSetAll is_closed_type_id) fv_env
+
     fv_env :: NameEnv NameSet
     fv_env = mkNameEnv $ concatMap (bindFvs . unLoc) binds
 
-    bindFvs :: HsBindLR Name idR -> [(Name, NameSet)]
-    bindFvs (FunBind { fun_id = f, bind_fvs = fvs })
-       = [(unLoc f, fvs)]
+    bindFvs :: HsBindLR GhcRn idR -> [(Name, NameSet)]
+    bindFvs (FunBind { fun_id = L _ f, bind_fvs = fvs })
+       = let open_fvs = filterNameSet (not . is_closed) fvs
+         in [(f, open_fvs)]
     bindFvs (PatBind { pat_lhs = pat, bind_fvs = fvs })
-       = [(b, fvs) | b <- collectPatBinders pat]
+       = let open_fvs = filterNameSet (not . is_closed) fvs
+         in [(b, open_fvs) | b <- collectPatBinders pat]
     bindFvs _
        = []
 
-    is_closed_ns :: TcTypeEnv -> NameSet -> Bool -> Bool
-    is_closed_ns type_env ns b = b && nameSetAll (is_closed_id type_env) ns
-        -- ns are the Names referred to from the RHS of this bind
-
-    is_closed_id :: TcTypeEnv -> Name -> Bool
-    -- See Note [Bindings with closed types] in TcRnTypes
-    is_closed_id type_env name
+    is_closed :: Name -> ClosedTypeId
+    is_closed name
       | Just thing <- lookupNameEnv type_env name
       = case thing of
-          ATcId { tct_info = ClosedLet } -> True  -- This is the key line
-          ATcId {}                       -> False
-          ATyVar {}                      -> False -- In-scope type variables
-          AGlobal {}                     -> True  --    are not closed!
-          _                              -> pprPanic "is_closed_id" (ppr name)
-      | otherwise
-      = True
-        -- The free-var set for a top level binding mentions
-        -- imported things too, so that we can report unused imports
-        -- These won't be in the local type env.
-        -- Ditto class method etc from the current module
+          AGlobal {}                     -> True
+          ATcId { tct_info = ClosedLet } -> True
+          _                              -> False
 
--------------------
-checkStrictBinds :: TopLevelFlag -> RecFlag
-                 -> [LHsBind Name]
-                 -> LHsBinds TcId -> [Id]
-                 -> TcM ()
--- Check that non-overloaded unlifted bindings are
---      a) non-recursive,
---      b) not top level,
---      c) not a multiple-binding group (more or less implied by (a))
-
-checkStrictBinds top_lvl rec_group orig_binds tc_binds poly_ids
-  | any_unlifted_bndr || any_strict_pat   -- This binding group must be matched strictly
-  = do  { check (isNotTopLevel top_lvl)
-                (strictBindErr "Top-level" any_unlifted_bndr orig_binds)
-        ; check (isNonRec rec_group)
-                (strictBindErr "Recursive" any_unlifted_bndr orig_binds)
-
-        ; check (all is_monomorphic (bagToList tc_binds))
-                  (polyBindErr orig_binds)
-            -- data Ptr a = Ptr Addr#
-            -- f x = let p@(Ptr y) = ... in ...
-            -- Here the binding for 'p' is polymorphic, but does
-            -- not mix with an unlifted binding for 'y'.  You should
-            -- use a bang pattern.  Trac #6078.
-
-        ; check (isSingleton orig_binds)
-                (strictBindErr "Multiple" any_unlifted_bndr orig_binds)
-
-        -- Complain about a binding that looks lazy
-        --    e.g.    let I# y = x in ...
-        -- Remember, in checkStrictBinds we are going to do strict
-        -- matching, so (for software engineering reasons) we insist
-        -- that the strictness is manifest on each binding
-        -- However, lone (unboxed) variables are ok
-        ; check (not any_pat_looks_lazy)
-                  (unliftedMustBeBang orig_binds) }
-  | otherwise
-  = traceTc "csb2" (ppr [(id, idType id) | id <- poly_ids]) >>
-    return ()
-  where
-    any_unlifted_bndr  = any is_unlifted poly_ids
-    any_strict_pat     = any (isUnliftedHsBind . unLoc) orig_binds
-    any_pat_looks_lazy = any (looksLazyPatBind . unLoc) orig_binds
-
-    is_unlifted id = case tcSplitSigmaTy (idType id) of
-                       (_, _, rho) -> isUnliftedType rho
-          -- For the is_unlifted check, we need to look inside polymorphism
-          -- and overloading.  E.g.  x = (# 1, True #)
-          -- would get type forall a. Num a => (# a, Bool #)
-          -- and we want to reject that.  See Trac #9140
-
-    is_monomorphic (L _ (AbsBinds { abs_tvs = tvs, abs_ev_vars = evs }))
-                     = null tvs && null evs
-    is_monomorphic (L _ (AbsBindsSig { abs_tvs = tvs, abs_ev_vars = evs }))
-                     = null tvs && null evs
-    is_monomorphic _ = True
-
-    check :: Bool -> MsgDoc -> TcM ()
-    -- Just like checkTc, but with a special case for module GHC.Prim:
-    --      see Note [Compiling GHC.Prim]
-    check True  _   = return ()
-    check False err = do { mod <- getModule
-                         ; checkTc (mod == gHC_PRIM) err }
-
-unliftedMustBeBang :: [LHsBind Name] -> SDoc
-unliftedMustBeBang binds
-  = hang (text "Pattern bindings containing unlifted types should use an outermost bang pattern:")
-       2 (vcat (map ppr binds))
-
-polyBindErr :: [LHsBind Name] -> SDoc
-polyBindErr binds
-  = hang (text "You can't mix polymorphic and unlifted bindings")
-       2 (vcat [vcat (map ppr binds),
-                text "Probable fix: add a type signature"])
-
-strictBindErr :: String -> Bool -> [LHsBind Name] -> SDoc
-strictBindErr flavour any_unlifted_bndr binds
-  = hang (text flavour <+> msg <+> text "aren't allowed:")
-       2 (vcat (map ppr binds))
-  where
-    msg | any_unlifted_bndr = text "bindings for unlifted types"
-        | otherwise         = text "bang-pattern or unboxed-tuple bindings"
+      | otherwise
+      = True  -- The free-var set for a top level binding mentions
 
 
-{- Note [Compiling GHC.Prim]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Module GHC.Prim has no source code: it is the host module for
-primitive, built-in functions and types.  However, for Haddock-ing
-purposes we generate (via utils/genprimopcode) a fake source file
-GHC/Prim.hs, and give it to Haddock, so that it can generate
-documentation.  It contains definitions like
-    nullAddr# :: NullAddr#
-which would normally be rejected as a top-level unlifted binding. But
-we don't want to complain, because we are only "compiling" this fake
-mdule for documentation purposes.  Hence this hacky test for gHC_PRIM
-in checkStrictBinds.
+    is_closed_type_id :: Name -> Bool
+    -- We're already removed Global and ClosedLet Ids
+    is_closed_type_id name
+      | Just thing <- lookupNameEnv type_env name
+      = case thing of
+          ATcId { tct_info = NonClosedLet _ cl } -> cl
+          ATcId { tct_info = NotLetBound }       -> False
+          ATyVar {}                              -> False
+               -- In-scope type variables are not closed!
+          _ -> pprPanic "is_closed_id" (ppr name)
 
-(We only make the test if things look wrong, so there is no cost in
-the common case.) -}
+      | otherwise
+      = True   -- The free-var set for a top level binding mentions
+               -- imported things too, so that we can report unused imports
+               -- These won't be in the local type env.
+               -- Ditto class method etc from the current module
 
 
 {- *********************************************************************
@@ -1743,21 +1739,7 @@ the common case.) -}
 
 -- This one is called on LHS, when pat and grhss are both Name
 -- and on RHS, when pat is TcId and grhss is still Name
-patMonoBindsCtxt :: (OutputableBndrId id, Outputable body)
-                 => LPat id -> GRHSs Name body -> SDoc
+patMonoBindsCtxt :: (SourceTextX p, OutputableBndrId p, Outputable body)
+                 => LPat p -> GRHSs GhcRn body -> SDoc
 patMonoBindsCtxt pat grhss
   = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss)
-
-instErrCtxt :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
-instErrCtxt name ty env
-  = do { let (env', ty') = tidyOpenType env ty
-       ; return (env', hang (text "When instantiating" <+> quotes (ppr name) <>
-                             text ", initially inferred to have" $$
-                             text "this overly-general type:")
-                          2 (ppr ty') $$
-                       extra) }
-  where
-    extra = sdocWithDynFlags $ \dflags ->
-            ppWhen (xopt LangExt.MonomorphismRestriction dflags) $
-            text "NB: This instantiation can be caused by the" <+>
-            text "monomorphism restriction."