Synchronize ClsInst.doTyConApp with TcTypeable validity checks (#15862)
[ghc.git] / compiler / typecheck / TcBinds.hs
index 204fd5f..c8c1bc0 100644 (file)
@@ -7,19 +7,22 @@
 
 {-# LANGUAGE CPP, RankNTypes, ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
 
-module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
-                 tcValBinds, tcHsBootSigs, tcPolyCheck,
-                 tcVectDecls, addTypecheckedBinds,
+module TcBinds ( tcLocalBinds, tcTopBinds, tcValBinds,
+                 tcHsBootSigs, tcPolyCheck,
+                 addTypecheckedBinds,
                  chooseInferredQuantifiers,
                  badBootDeclErr ) where
 
+import GhcPrelude
+
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcMonoExpr )
-import {-# SOURCE #-} TcPatSyn ( tcInferPatSynDecl, tcCheckPatSynDecl
-                               , tcPatSynBuilderBind )
+import {-# SOURCE #-} TcPatSyn ( tcPatSynDecl, tcPatSynBuilderBind )
 import CoreSyn (Tickish (..))
-import CostCentre (mkUserCC)
+import CostCentre (mkUserCC, CCFlavour(DeclCC))
 import DynFlags
 import FastString
 import HsSyn
@@ -33,14 +36,13 @@ 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, mkTyVarBinder )
+import Type( mkStrLitTy, tidyOpenType, splitTyConApp_maybe, mkCastTy)
 import TysPrim
-import TysWiredIn( cTupleTyConName )
+import TysWiredIn( mkBoxedTupleTy )
 import Id
 import Var
 import VarSet
@@ -51,18 +53,18 @@ import NameSet
 import NameEnv
 import SrcLoc
 import Bag
-import ListSetOps
 import ErrUtils
 import Digraph
 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
 
@@ -74,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
@@ -135,7 +137,7 @@ If we don't take care, after typechecking we get
                                in
                                \ys:[a] -> ...f'...
 
-Notice the the stupid construction of (f a d), which is of course
+Notice the stupid construction of (f a d), which is of course
 identical to the function we're executing.  In this case, the
 polymorphic recursion isn't being used (but that's a very common case).
 This can lead to a massive space leak, from the following top-level defn
@@ -175,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
@@ -186,34 +189,132 @@ 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
-tcRecSelBinds (ValBindsOut binds sigs)
-  = tcExtendGlobalValEnv [sel_id | L _ (IdSig sel_id) <- sigs] $
-    do { (rec_sel_binds, tcg_env) <- discardWarnings $
-                                     tcValBinds TopLevel binds sigs getGblEnv
-       ; let tcg_env' = tcg_env `addTypecheckedBinds` map snd rec_sel_binds
-       ; return tcg_env' }
-tcRecSelBinds (ValBindsIn {}) = panic "tcRecSelBinds"
 
-tcHsBootSigs :: [(RecFlag, LHsBinds Name)] -> [LSig Name] -> TcM [Id]
+-- 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
+
+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
   = do  { checkTc (null binds) badBootDeclErr
         ; concat <$> mapM (addLocM tc_boot_sig) (filter isTypeLSig sigs) }
   where
-    tc_boot_sig (TypeSig lnames hs_ty) = mapM f lnames
+    tc_boot_sig (TypeSig lnames hs_ty) = mapM f lnames
       where
-        f (L _ name)
-          = do { sigma_ty <- solveEqualities $
-                             tcHsSigWcType (FunSigCtxt name False) hs_ty
+        f (dL->L _ name)
+          = 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)
@@ -222,19 +323,19 @@ 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
+tcLocalBinds (EmptyLocalBinds x) thing_inside
   = do  { thing <- thing_inside
-        ; return (EmptyLocalBinds, thing) }
+        ; return (EmptyLocalBinds x, thing) }
 
-tcLocalBinds (HsValBinds (ValBindsOut binds sigs)) thing_inside
+tcLocalBinds (HsValBinds x (XValBindsLR (NValBinds binds sigs))) thing_inside
   = do  { (binds', thing) <- tcValBinds NotTopLevel binds sigs thing_inside
-        ; return (HsValBinds (ValBindsOut binds' sigs), thing) }
-tcLocalBinds (HsValBinds (ValBindsIn {})) _ = panic "tcLocalBinds"
+        ; return (HsValBinds x (XValBindsLR (NValBinds binds' sigs)), thing) }
+tcLocalBinds (HsValBinds _ (ValBinds {})) _ = panic "tcLocalBinds"
 
-tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
+tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
   = do  { ipClass <- tcLookupClass ipClassName
         ; (given_ips, ip_binds') <-
             mapAndUnzipM (wrapLocSndM (tc_ip_bind ipClass)) ip_binds
@@ -245,27 +346,31 @@ tcLocalBinds (HsIPBinds (IPBinds ip_binds _)) thing_inside
         ; (ev_binds, result) <- checkConstraints (IPSkol ips)
                                   [] given_ips thing_inside
 
-        ; return (HsIPBinds (IPBinds ip_binds' ev_binds), result) }
+        ; return (HsIPBinds x (IPBinds ev_binds ip_binds') , result) }
   where
-    ips = [ip | L _ (IPBind (Left (L _ ip)) _) <- ip_binds]
+    ips = [ip | (dL->L _ (IPBind _ (Left (dL->L _ ip)) _)) <- ip_binds]
 
         -- I wonder if we should do these one at at time
         -- Consider     ?x = 4
         --              ?y = ?x + 1
-    tc_ip_bind ipClass (IPBind (Left (L _ ip)) expr)
+    tc_ip_bind ipClass (IPBind _ (Left (dL->L _ ip)) expr)
        = do { ty <- newOpenFlexiTyVarTy
             ; let p = mkStrLitTy $ hsIPNameFS ip
             ; ip_id <- newDict ipClass [ p, ty ]
             ; expr' <- tcMonoExpr expr (mkCheckExpType ty)
             ; let d = toDict ipClass p ty `fmap` expr'
-            ; return (ip_id, (IPBind (Right ip_id) d)) }
-    tc_ip_bind _ (IPBind (Right {}) _) = panic "tc_ip_bind"
+            ; return (ip_id, (IPBind noExt (Right ip_id) d)) }
+    tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind"
+    tc_ip_bind _ (XIPBind _) = panic "tc_ip_bind"
 
     -- 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]
 
+tcLocalBinds (HsIPBinds _ (XHsIPBinds _ )) _ = panic "tcLocalBinds"
+tcLocalBinds (XHsLocalBindsLR _)           _ = panic "tcLocalBinds"
+
 {- Note [Implicit parameter untouchables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We add the type variables in the types of the implicit parameters
@@ -282,36 +387,39 @@ untouchable-range idea.
 -}
 
 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
-
-            -- Typecheck the signature
+  = do  {   -- Typecheck the signatures
+            -- It's easier to do so now, once for all the SCCs together
+            -- because a single signature  f,g :: <type>
+            -- might relate to more than one SCC
         ; (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
                                 tcTySigs sigs
 
-        ; let prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
-
                 -- Extend the envt right away with all the Ids
                 -- declared with complete type signatures
-                -- Do not extend the TcIdBinderStack; instead
+                -- Do not extend the TcBinderStack; 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) }
             ; return (binds' ++ extra_binds', thing) }}
+  where
+    patsyns = getPatSynBinds binds
+    prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
 
 ------------------------
 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
@@ -324,7 +432,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
@@ -350,8 +459,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
@@ -385,13 +494,14 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
     isPatSyn PatSynBind{} = True
     isPatSyn _ = False
 
-    sccs :: [SCC (LHsBind Name)]
+    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) }
 
@@ -399,75 +509,74 @@ 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 (GhcPass p) =>
+                      LHsBinds (GhcPass p) -> TcM a
 recursivePatSynErr binds
   = failWithTc $
     hang (text "Recursive pattern synonym definition with following bindings:")
        2 (vcat $ map pprLBind . bagToList $ binds)
   where
     pprLoc loc  = parens (text "defined at" <+> ppr loc)
-    pprLBind (L loc bind) = pprWithCommas ppr (collectHsBindBinders bind) <+>
-                            pprLoc loc
+    pprLBind (dL->L loc bind) = pprWithCommas ppr (collectHsBindBinders bind)
+                                <+> pprLoc loc
 
 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 }))
+          (dL->L _ (PatSynBind _ psb@PSB{ psb_id = (dL->L _ name) }))
           _ thing_inside
-  = do { (aux_binds, tcg_env) <- tc_pat_syn_decl
+  = do { (aux_binds, tcg_env) <- tcPatSynDecl psb (sig_fn name)
        ; thing <- setGblEnv tcg_env thing_inside
        ; return (aux_binds, thing)
        }
-  where
-    tc_pat_syn_decl :: TcM (LHsBinds TcId, 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
     -- is still deterministic even if the edges are in nondeterministic order
     -- as explained in Note [Deterministic SCC] in Digraph.
   where
+    bind_fvs (FunBind { fun_ext = fvs }) = fvs
+    bind_fvs (PatBind { pat_ext = fvs }) = fvs
+    bind_fvs _                           = emptyNameSet
+
     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 ..]
 
     key_map :: NameEnv BKey     -- Which binding it comes from
-    key_map = mkNameEnv [(bndr, key) | (L _ bind, key) <- keyd_binds
+    key_map = mkNameEnv [(bndr, key) | (dL->L _ bind, key) <- keyd_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
@@ -480,7 +589,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
@@ -490,15 +599,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]
                                           ])
@@ -515,7 +620,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
@@ -529,7 +634,13 @@ recoveryCode binder_names sig_fn
       = mkLocalId name forall_a_a
 
 forall_a_a :: TcType
-forall_a_a = mkSpecForAllTys [runtimeRep1TyVar, openAlphaTyVar] openAlphaTy
+-- At one point I had (forall r (a :: TYPE r). a), but of course
+-- that type is ill-formed: its mentions 'r' which escapes r's scope.
+-- Another alternative would be (forall (a :: TYPE kappa). a), where
+-- kappa is a unification variable. But I don't think we need that
+-- complication here. I'm going to just use (forall (a::*). a).
+-- See #15276
+forall_a_a = mkSpecForAllTys [alphaTyVar] alphaTy
 
 {- *********************************************************************
 *                                                                      *
@@ -541,8 +652,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
@@ -552,11 +663,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!
@@ -571,8 +679,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,
@@ -580,65 +688,76 @@ tcPolyCheck prag_fn
             (CompleteSig { sig_bndr  = poly_id
                          , sig_ctxt  = ctxt
                          , sig_loc   = sig_loc })
-            (L loc (FunBind { fun_id = L nm_loc name
-                            , fun_matches = matches }))
+            (dL->L loc (FunBind { fun_id = (dL->L nm_loc name)
+                                , 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'))
             <- checkConstraints skol_info skol_tvs ev_vars $
-               tcExtendIdBndrs [TcIdBndr mono_id NotTopLevel]  $
-               tcExtendTyVarEnv2 tv_prs $
+               tcExtendBinderStack [TcIdBndr mono_id NotTopLevel]  $
+               tcExtendNameTyVarEnv tv_prs $
                setSrcSpan loc           $
-               tcMatchesFun (L nm_loc mono_name) matches (mkCheckExpType tau)
+               tcMatchesFun (cL nm_loc mono_name) matches (mkCheckExpType tau)
 
        ; let prag_sigs = lookupPragEnv prag_fn name
        ; 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
+       ; tick <- funBindTicks nm_loc mono_id mod prag_sigs
+       ; let bind' = FunBind { fun_id      = cL nm_loc mono_id
                              , fun_matches = matches'
                              , fun_co_fn   = co_fn
-                             , bind_fvs    = placeHolderNamesTc
-                             , fun_tick    = funBindTicks nm_loc mono_id mod prag_sigs }
-
-             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' }
+                             , fun_ext     = placeHolderNamesTc
+                             , fun_tick    = tick }
+
+             export = ABE { abe_ext = noExt
+                          , abe_wrap = idHsWrapper
+                          , abe_poly  = poly_id
+                          , abe_mono  = mono_id
+                          , abe_prags = SpecPrags spec_prags }
+
+             abs_bind = cL loc $
+                        AbsBinds { abs_ext = noExt
+                                 , abs_tvs      = skol_tvs
+                                 , abs_ev_vars  = ev_vars
+                                 , abs_ev_binds = [ev_binds]
+                                 , abs_exports  = [export]
+                                 , abs_binds    = unitBag (cL 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 Name] -> [Tickish TcId]
+funBindTicks :: SrcSpan -> TcId -> Module -> [LSig GhcRn]
+             -> TcM [Tickish TcId]
 funBindTicks loc fun_id mod sigs
-  | (mb_cc_str : _) <- [ cc_name | L _ (SCCFunSig _ _ cc_name) <- sigs ]
+  | (mb_cc_str : _) <- [ cc_name | (dL->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 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]
+  = do
+      flavour <- DeclCC <$> getCCIndexM cc_name
+      let cc = mkUserCC cc_name mod loc flavour
+      return [ProfNote cc True True]
   | otherwise
-  = []
+  = return []
 
 {- Note [Instantiate sig with fresh variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -665,8 +784,8 @@ 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  $
@@ -680,19 +799,22 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
        ; mapM_ (checkOverloadedSig mono) sigs
 
        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
-       ; (qtvs, givens, ev_binds)
+       ; (qtvs, givens, ev_binds, residual, insoluble)
                  <- simplifyInfer tclvl infer_mode sigs name_taus wanted
+       ; emitConstraints residual
 
        ; 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_bind = cL loc $
+                        AbsBinds { abs_ext = noExt
+                                 , 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) }
@@ -700,9 +822,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
@@ -716,19 +840,19 @@ 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
@@ -738,35 +862,38 @@ mkExport prag_fn qtvs theta
 
         ; 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 $
               localSigWarn Opt_WarnMissingLocalSignatures poly_id mb_sig
 
-        ; return (ABE { abe_wrap = wrap
+        ; return (ABE { abe_ext = noExt
+                      , 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
@@ -787,9 +914,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 (#14000) we may report an ambiguity
+         -- error for a rather bogus type.
 
        ; return (mkLocalIdOrCoVar poly_name inferred_poly_ty) }
 
@@ -802,7 +933,7 @@ chooseInferredQuantifiers :: TcThetaType   -- inferred
 chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
   = -- No type signature (partial or complete) for this binder,
     do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
-                        -- Include kind variables!  Trac #7916
+                        -- Include kind variables!  #7916
              my_theta = pickCapturedPreds free_tvs inferred_theta
              binders  = [ mkTyVarBinder Inferred tv
                         | tv <- qtvs
@@ -814,57 +945,102 @@ chooseInferredQuantifiers inferred_theta tau_tvs qtvs
                                       , sig_inst_wcx   = wcx
                                       , sig_inst_theta = annotated_theta
                                       , sig_inst_skols = annotated_tvs }))
-  | Nothing <- wcx
-  = do { annotated_theta <- zonkTcTypes annotated_theta
-       ; 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) }
-
-  | 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
-
-       -- Report the inferred constraints for an extra-constraints wildcard/hole as
-       -- an error message, unless the PartialTypeSignatures flag is enabled. In this
-       -- case, the extra inferred constraints are accepted without complaining.
-       -- NB: inferred_theta already includes all the annotated constraints
-             inferred_diff = [ pred
-                             | pred <- my_theta
-                             , all (not . (`eqType` pred)) annotated_theta ]
-       ; ctuple <- mk_ctuple inferred_diff
-       ; writeMetaTyVar wc_var ctuple
-       ; traceTc "completeTheta" $
-            vcat [ ppr sig
-                 , ppr annotated_theta, ppr inferred_theta
-                 , ppr inferred_diff ]
-
-       ; return (mk_binders free_tvs, my_theta) }
-
-  | otherwise  -- A complete type signature is dealt with in mkInferredPolyId
-  = pprPanic "chooseInferredQuantifiers" (ppr sig)
-
+  = -- Choose quantifiers for a partial type signature
+    do { psig_qtv_prs <- zonkTyVarTyVarPairs annotated_tvs
+
+            -- Check whether the quantified variables of the
+            -- partial signature have been unified together
+            -- See Note [Quantified variables in partial type signatures]
+       ; mapM_ report_dup_tyvar_tv_err  (findDupTyVarTvs psig_qtv_prs)
+
+            -- Check whether a quantified variable of the partial type
+            -- signature is not actually quantified.  How can that happen?
+            -- See Note [Quantification and partial signatures] Wrinkle 4
+            --     in TcSimplify
+       ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
+                                          , not (tv `elem` qtvs) ]
+
+       ; let psig_qtvs = mkVarSet (map snd psig_qtv_prs)
+
+       ; annotated_theta      <- zonkTcTypes annotated_theta
+       ; (free_tvs, my_theta) <- choose_psig_context psig_qtvs annotated_theta wcx
+
+       ; let keep_me    = free_tvs `unionVarSet` psig_qtvs
+             final_qtvs = [ mkTyVarBinder vis tv
+                          | tv <- qtvs -- Pulling from qtvs maintains original order
+                          , tv `elemVarSet` keep_me
+                          , let vis | tv `elemVarSet` psig_qtvs = Specified
+                                    | otherwise                 = Inferred ]
+
+       ; return (final_qtvs, my_theta) }
   where
-    spec_tv_set = mkVarSet $ map snd annotated_tvs
-    mk_binders free_tvs
-      = [ mkTyVarBinder vis tv
-        | tv <- qtvs
-        , tv `elemVarSet` free_tvs
-        , let vis | tv `elemVarSet` spec_tv_set = Specified
-                  | otherwise                   = Inferred ]
-                          -- Pulling from qtvs maintains original order
-
-    mk_ctuple [pred] = return pred
-    mk_ctuple preds  = do { tc <- tcLookupTyCon (cTupleTyConName (length preds))
-                          ; return (mkTyConApp tc preds) }
-
-mk_impedence_match_msg :: MonoBindInfo
+    report_dup_tyvar_tv_err (n1,n2)
+      | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
+      = addErrTc (hang (text "Couldn't match" <+> quotes (ppr n1)
+                        <+> text "with" <+> quotes (ppr n2))
+                     2 (hang (text "both bound by the partial type signature:")
+                           2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
+
+      | otherwise -- Can't happen; by now we know it's a partial sig
+      = pprPanic "report_tyvar_tv_err" (ppr sig)
+
+    report_mono_sig_tv_err n
+      | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
+      = addErrTc (hang (text "Can't quantify over" <+> quotes (ppr n))
+                     2 (hang (text "bound by the partial type signature:")
+                           2 (ppr fn_name <+> dcolon <+> ppr hs_ty)))
+      | otherwise -- Can't happen; by now we know it's a partial sig
+      = pprPanic "report_mono_sig_tv_err" (ppr sig)
+
+    choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType
+                        -> TcM (VarSet, TcThetaType)
+    choose_psig_context _ annotated_theta Nothing
+      = do { let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
+                                            `unionVarSet` tau_tvs)
+           ; return (free_tvs, annotated_theta) }
+
+    choose_psig_context psig_qtvs annotated_theta (Just wc_var_ty)
+      = do { 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
+
+           ; let keep_me  = psig_qtvs `unionVarSet` free_tvs
+                 my_theta = pickCapturedPreds keep_me inferred_theta
+
+           -- Fill in the extra-constraints wildcard hole with inferred_theta,
+           -- so that the Hole constraint we have already emitted
+           -- (in tcHsPartialSigType) can report what filled it in.
+           -- NB: my_theta already includes all the annotated constraints
+           ; let inferred_diff = [ pred
+                                 | pred <- my_theta
+                                 , all (not . (`eqType` pred)) annotated_theta ]
+           ; ctuple <- mk_ctuple inferred_diff
+
+           ; case tcGetCastedTyVar_maybe wc_var_ty of
+               -- We know that wc_co must have type kind(wc_var) ~ Constraint, as it
+               -- comes from the checkExpectedKind in TcHsType.tcWildCardOcc. So, to
+               -- make the kinds work out, we reverse the cast here.
+               Just (wc_var, wc_co) -> writeMetaTyVar wc_var (ctuple `mkCastTy` mkTcSymCo wc_co)
+               Nothing              -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty)
+
+           ; traceTc "completeTheta" $
+                vcat [ ppr sig
+                     , ppr annotated_theta, ppr inferred_theta
+                     , ppr inferred_diff ]
+           ; return (free_tvs, my_theta) }
+
+    mk_ctuple preds = return (mkBoxedTupleTy preds)
+       -- Hack alert!  See TcHsType:
+       -- Note [Extra-constraint holes in partial type signatures]
+
+
+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
@@ -911,7 +1087,7 @@ checkOverloadedSig :: Bool -> TcIdSigInst -> TcM ()
 --   K f = e
 -- The MR applies, but the signature is overloaded, and it's
 -- best to complain about this directly
--- c.f Trac #11339
+-- c.f #11339
 checkOverloadedSig monomorphism_restriction_applies sig
   | not (null (sig_inst_theta sig))
   , monomorphism_restriction_applies
@@ -949,13 +1125,35 @@ doesn't seem much point.  Indeed, adding a partial type signature is a
 way to get per-binding inferred generalisation.
 
 We apply the MR if /all/ of the partial signatures lack a context.
-In particular (Trac #11016):
+In particular (#11016):
    f2 :: (?loc :: Int) => _
    f2 = ?loc
 It's stupid to apply the MR here.  This test includes an extra-constraints
 wildcard; that is, we don't apply the MR if you write
    f3 :: _ => blah
 
+Note [Quantified variables in partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+  f :: forall a. a -> a -> _
+  f x y = g x y
+  g :: forall b. b -> b -> _
+  g x y = [x, y]
+
+Here, 'f' and 'g' are mutually recursive, and we end up unifying 'a' and 'b'
+together, which is fine.  So we bind 'a' and 'b' to TyVarTvs, which can then
+unify with each other.
+
+But now consider:
+  f :: forall a b. a -> b -> _
+  f x y = [x, y]
+
+We want to get an error from this, because 'a' and 'b' get unified.
+So we make a test, one per parital signature, to check that the
+explicitly-quantified type variables have not been unified together.
+#14449 showed this up.
+
+
 Note [Validity of inferred types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 We need to check inferred type for validity, in case it uses language
@@ -971,7 +1169,7 @@ Examples that might fail:
  - an inferred type that includes unboxed tuples
 
 
-Note [Impedence matching]
+Note [Impedance matching]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider
    f 0 x = x
@@ -1003,89 +1201,13 @@ Then we want to check that
      forall qtvs. theta => f_mono_ty   is more polymorphic than   f's polytype
 and the proof is the impedance matcher.
 
-Notice that the impedance matcher may do defaulting.  See Trac #7173.
+Notice that the impedance matcher may do defaulting.  See #7173.
 
 It also cleverly does an ambiguity check; for example, rejecting
    f :: F a -> F a
 where F is a non-injective type function.
 -}
 
-{- *********************************************************************
-*                                                                      *
-                         Vectorisation
-*                                                                      *
-********************************************************************* -}
-
-tcVectDecls :: [LVectDecl Name] -> TcM ([LVectDecl TcId])
-tcVectDecls decls
-  = do { decls' <- mapM (wrapLocM tcVect) decls
-       ; let ids  = [lvectDeclName decl | decl <- decls', not $ lvectInstDecl decl]
-             dups = findDupsEq (==) ids
-       ; mapM_ reportVectDups dups
-       ; traceTcConstraints "End of tcVectDecls"
-       ; return decls'
-       }
-  where
-    reportVectDups (first:_second:_more)
-      = addErrAt (getSrcSpan first) $
-          text "Duplicate vectorisation declarations for" <+> ppr first
-    reportVectDups _ = return ()
-
---------------
-tcVect :: VectDecl Name -> TcM (VectDecl TcId)
--- 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
---   identifier (this is checked in 'rnHsVectDecl').  Fix this by enabling the use of 'vectType'
---   from the vectoriser here.
-tcVect (HsVect s name rhs)
-  = addErrCtxt (vectCtxt name) $
-    do { var <- wrapLocM tcLookupId name
-       ; let L rhs_loc (HsVar (L lv rhs_var_name)) = rhs
-       ; rhs_id <- tcLookupId rhs_var_name
-       ; return $ HsVect s var (L rhs_loc (HsVar (L lv rhs_id)))
-       }
-
-tcVect (HsNoVect s name)
-  = addErrCtxt (vectCtxt name) $
-    do { var <- wrapLocM tcLookupId name
-       ; return $ HsNoVect s var
-       }
-tcVect (HsVectTypeIn _ isScalar lname rhs_name)
-  = addErrCtxt (vectCtxt lname) $
-    do { tycon <- tcLookupLocatedTyCon lname
-       ; checkTc (   not isScalar             -- either    we have a non-SCALAR declaration
-                 || isJust rhs_name           -- or        we explicitly provide a vectorised type
-                 || tyConArity tycon == 0     -- otherwise the type constructor must be nullary
-                 )
-                 scalarTyConMustBeNullary
-
-       ; rhs_tycon <- fmapMaybeM (tcLookupTyCon . unLoc) rhs_name
-       ; return $ HsVectTypeOut isScalar tycon rhs_tycon
-       }
-tcVect (HsVectTypeOut _ _ _)
-  = panic "TcBinds.tcVect: Unexpected 'HsVectTypeOut'"
-tcVect (HsVectClassIn _ lname)
-  = addErrCtxt (vectCtxt lname) $
-    do { cls <- tcLookupLocatedClass lname
-       ; return $ HsVectClassOut cls
-       }
-tcVect (HsVectClassOut _)
-  = panic "TcBinds.tcVect: Unexpected 'HsVectClassOut'"
-tcVect (HsVectInstIn linstTy)
-  = addErrCtxt (vectCtxt linstTy) $
-    do { (cls, tys) <- tcHsVectInst linstTy
-       ; inst       <- tcLookupInstance cls tys
-       ; return $ HsVectInstOut inst
-       }
-tcVect (HsVectInstOut _)
-  = panic "TcBinds.tcVect: Unexpected 'HsVectInstOut'"
-
-vectCtxt :: Outputable thing => thing -> SDoc
-vectCtxt thing = text "When checking the vectorisation declaration for" <+> ppr thing
-
-scalarTyConMustBeNullary :: MsgDoc
-scalarTyConMustBeNullary = text "VECTORISE SCALAR type constructor must be nullary"
 
 {-
 Note [SPECIALISE pragmas]
@@ -1117,58 +1239,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
@@ -1179,41 +1249,38 @@ 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 })]
+           [ dL->L b_loc (FunBind { fun_id = (dL->L nm_loc name)
+                                  , fun_matches = matches
+                                  , fun_ext = 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] in TcUnify
+               tcExtendBinderStack [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 (cL 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 = [] },
+        ; return (unitBag $ cL b_loc $
+                     FunBind { fun_id = cL nm_loc mono_id,
+                               fun_matches = matches', fun_ext = fvs,
+                               fun_co_fn = co_fn, fun_tick = [] },
                   [MBI { mbi_poly_name = name
                        , mbi_sig       = Nothing
                        , mbi_mono_id   = mono_id }]) }
@@ -1235,7 +1302,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) }
@@ -1258,73 +1325,87 @@ 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 sig_fn no_gen (FunBind { fun_id = (dL->L nm_loc name)
+                             , fun_matches = matches })
+  | 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) }
 
-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
+  | 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 }) }
 
 ------------
@@ -1335,33 +1416,19 @@ 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]  $
     tcExtendTyVarEnvForRhs mb_sig       $
     do  { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
-        ; (co_fn, matches') <- tcMatchesFun (L loc (idName mono_id))
+        ; (co_fn, matches') <- tcMatchesFun (cL loc (idName mono_id))
                                  matches (mkCheckExpType $ idType mono_id)
-        ; return ( FunBind { fun_id = L loc mono_id
+        ; return ( FunBind { fun_id = cL loc mono_id
                            , fun_matches = matches'
                            , fun_co_fn = co_fn
-                           , bind_fvs = placeHolderNamesTc
+                           , fun_ext = placeHolderNamesTc
                            , fun_tick = [] } ) }
 
 tcRhs (TcPatBind infos pat' grhss pat_ty)
@@ -1374,8 +1441,7 @@ tcRhs (TcPatBind infos pat' grhss pat_ty)
         ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
                     tcGRHSsPat grhss pat_ty
         ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
-                           , pat_rhs_ty = pat_ty
-                           , bind_fvs = placeHolderNamesTc
+                           , pat_ext = NPatBindTc placeHolderNamesTc pat_ty
                            , pat_ticks = ([],[]) } )}
 
 tcExtendTyVarEnvForRhs :: Maybe TcIdSigInst -> TcM a -> TcM a
@@ -1387,12 +1453,12 @@ tcExtendTyVarEnvForRhs (Just sig) thing_inside
 tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
 tcExtendTyVarEnvFromSig sig_inst thing_inside
   | TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
-  = tcExtendTyVarEnv2 wcs $
-    tcExtendTyVarEnv2 skol_prs $
+  = tcExtendNameTyVarEnv wcs $
+    tcExtendNameTyVarEnv skol_prs $
     thing_inside
 
 tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
--- Extend the TcIdBinderStack for the RHS of the binding, with
+-- Extend the TcBinderStack for the RHS of the binding, with
 -- the monomorphic Id.  That way, if we have, say
 --     f = \x -> blah
 -- and something goes wrong in 'blah', we get a "relevant binding"
@@ -1401,12 +1467,12 @@ tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
 --    f :: forall a. [a] -> [a]
 --    f x = True
 -- We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
--- If we had the *polymorphic* version of f in the TcIdBinderStack, it
+-- If we had the *polymorphic* version of f in the TcBinderStack, it
 -- would not be reported as relevant, because its type is closed
 tcExtendIdBinderStackForRhs infos thing_inside
-  = tcExtendIdBndrs [ TcIdBndr mono_id NotTopLevel
-                    | MBI { mbi_mono_id = mono_id } <- infos ]
-                    thing_inside
+  = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
+                        | MBI { mbi_mono_id = mono_id } <- infos ]
+                        thing_inside
     -- NotTopLevel: it's a monomorphic binding
 
 ---------------------
@@ -1417,9 +1483,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
+   - #12427, typecheck/should_compile/T12427{a,b}
+
   data T where
     MkT :: Integral a => a -> Int -> T
 
@@ -1431,48 +1501,97 @@ and suppose t :: T.  Which of these pattern bindings are ok?
 
   E3. let { MkT (toInteger -> r) _ = t } in <body>
 
-Well (E1) is clearly wrong because 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.
 
-  2. Still in tcLhs, we build a little environment mappting "q" ->
-     q':alpha, and pass that to tcLetPet.
+     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.
 
-  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.
+  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.
+
+     - When we come to a binder (TcPat.tcPatBndr), it looks it up
+       in the little environment (the pc_sig_fn field of PatCtxt).
+
+         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 #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 untouchable, but floats out of the constraint and can
+be solved absolutely fine.
+
 
 ************************************************************************
 *                                                                      *
@@ -1486,9 +1605,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
@@ -1499,19 +1618,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]
@@ -1519,24 +1637,23 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
       = [ null theta
         | TcIdSig (PartialSig { psig_hs_ty = hs_ty })
             <- mapMaybe sig_fn (collectHsBindListBinders lbinds)
-        , let (_, L _ theta, _) = splitLHsSigmaTy (hsSigWcType hs_ty) ]
+        , let (_, dL->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
     one_funbind_with_sig
-      | [lbind@(L _ (FunBind { fun_id = v }))] <- lbinds
+      | [lbind@(dL->L _ (FunBind { fun_id = v }))] <- lbinds
       , Just (TcIdSig sig) <- sig_fn (unLoc v)
       = Just (lbind, sig)
       | otherwise
@@ -1547,155 +1664,64 @@ 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 (PatBind { pat_lhs = pat, bind_fvs = fvs })
-       = [(b, fvs) | b <- collectPatBinders pat]
+    bindFvs :: HsBindLR GhcRn GhcRn -> [(Name, NameSet)]
+    bindFvs (FunBind { fun_id = (dL->L _ f)
+                     , fun_ext = fvs })
+       = let open_fvs = get_open_fvs fvs
+         in [(f, open_fvs)]
+    bindFvs (PatBind { pat_lhs = pat, pat_ext = fvs })
+       = let open_fvs = get_open_fvs 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
+    get_open_fvs fvs = filterNameSet (not . is_closed) fvs
 
-    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
 
 
 {- *********************************************************************
@@ -1706,21 +1732,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 :: (OutputableBndrId (GhcPass p), Outputable body)
+                 => LPat (GhcPass 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."