Synchronize ClsInst.doTyConApp with TcTypeable validity checks (#15862)
[ghc.git] / compiler / typecheck / TcBinds.hs
index 2327b6f..c8c1bc0 100644 (file)
@@ -8,19 +8,21 @@
 {-# LANGUAGE CPP, RankNTypes, ScopedTypeVariables #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE ViewPatterns #-}
 
-module TcBinds ( tcLocalBinds, tcTopBinds, tcRecSelBinds,
+module TcBinds ( tcLocalBinds, tcTopBinds, tcValBinds,
                  tcHsBootSigs, tcPolyCheck,
-                 tcVectDecls, addTypecheckedBinds,
+                 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
@@ -38,9 +40,9 @@ import FamInstEnv( normaliseType )
 import FamInst( tcGetFamInstEnvs )
 import TyCon
 import TcType
-import Type( mkStrLitTy, tidyOpenType, mkTyVarBinder, splitTyConApp_maybe)
+import Type( mkStrLitTy, tidyOpenType, splitTyConApp_maybe, mkCastTy)
 import TysPrim
-import TysWiredIn( cTupleTyConName )
+import TysWiredIn( mkBoxedTupleTy )
 import Id
 import Var
 import VarSet
@@ -51,7 +53,6 @@ import NameSet
 import NameEnv
 import SrcLoc
 import Bag
-import ListSetOps
 import ErrUtils
 import Digraph
 import Maybes
@@ -60,7 +61,6 @@ import BasicTypes
 import Outputable
 import PrelNames( ipClassName )
 import TcValidity (checkValidType)
-import Unique (getUnique)
 import UniqFM
 import UniqSet
 import qualified GHC.LanguageExtensions as LangExt
@@ -137,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
@@ -233,7 +233,7 @@ tcCompleteSigs  :: [LSig GhcRn] -> TcM [CompleteMatch]
 tcCompleteSigs sigs =
   let
       doOne :: Sig GhcRn -> TcM (Maybe CompleteMatch)
-      doOne c@(CompleteMatchSig _ lns mtc)
+      doOne c@(CompleteMatchSig _ lns mtc)
         = fmap Just $ do
            addErrCtxt (text "In" <+> ppr c) $
             case mtc of
@@ -304,15 +304,6 @@ tcCompleteSigs sigs =
                                <+> 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 $
-                                     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 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
@@ -320,9 +311,9 @@ 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)
+        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
@@ -335,16 +326,16 @@ badBootDeclErr = text "Illegal declarations in an hs-boot file"
 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
@@ -355,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 = 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
@@ -397,17 +392,16 @@ tcValBinds :: TopLevelFlag
            -> 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
         ; tcExtendSigIds top_lvl poly_ids $ do
             { (binds', (extra_binds', thing)) <- tcBindGroups top_lvl sig_fn prag_fn binds $ do
@@ -418,6 +412,9 @@ tcValBinds top_lvl binds sigs thing_inside
                    ; 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
@@ -514,33 +511,28 @@ tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
     tc_sub_group rec_tc binds =
       tcPolyBinds sig_fn prag_fn Recursive rec_tc closed binds
 
-recursivePatSynErr :: OutputableBndrId 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 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 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 sig_fn prag_fn
@@ -564,13 +556,17 @@ mkEdges sig_fn binds
     -- 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 = 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 ]
 
 ------------------------
@@ -638,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
 
 {- *********************************************************************
 *                                                                      *
@@ -686,8 +688,8 @@ 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 tcInstSkolTyVars poly_id
@@ -701,29 +703,37 @@ tcPolyCheck prag_fn
 
        ; (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]) }
 
@@ -731,9 +741,9 @@ tcPolyCheck _prag_fn sig bind
   = pprPanic "tcPolyCheck" (ppr sig $$ ppr bind)
 
 funBindTicks :: SrcSpan -> TcId -> Module -> [LSig GhcRn]
-             -> [Tickish TcId]
+             -> 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
@@ -742,10 +752,12 @@ funBindTicks loc fun_id mod sigs
           | 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]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -787,8 +799,9 @@ 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, insoluble)
+       ; (qtvs, givens, ev_binds, residual, insoluble)
                  <- simplifyInfer tclvl infer_mode sigs name_taus wanted
+       ; emitConstraints residual
 
        ; let inferred_theta = map evVarPred givens
        ; exports <- checkNoErrs $
@@ -796,10 +809,12 @@ tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
 
        ; 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) }
@@ -856,11 +871,12 @@ mkExport prag_fn insoluble qtvs theta
         ; 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
@@ -903,7 +919,7 @@ mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_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
+         -- do this check; otherwise (#14000) we may report an ambiguity
          -- error for a rather bogus type.
 
        ; return (mkLocalIdOrCoVar poly_name inferred_poly_ty) }
@@ -917,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
@@ -929,64 +945,96 @@ 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])
-       ; 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 (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
-       -- 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 (my_qtvs, 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
-    mk_final_qtvs psig_qtvs free_tvs
-      = [ mkTyVarBinder vis tv
-        | 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) }
+    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_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
@@ -1039,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
@@ -1077,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
@@ -1131,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 GhcRn] -> TcM ([LVectDecl GhcTcId])
-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 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
---   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]
@@ -1258,8 +1252,9 @@ tcMonoBinds :: RecFlag  -- Whether the binding is recursive for typechecking pur
             -> [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
@@ -1274,17 +1269,17 @@ tcMonoBinds is_rec sig_fn no_gen
     do  { ((co_fn, matches'), rhs_ty)
             <- tcInferInst $ \ exp_ty ->
                   -- tcInferInst: see TcUnify,
-                  -- Note [Deep instantiation of InferResult]
-               tcExtendIdBndrs [TcIdBndr_ExpType name exp_ty NotTopLevel] $
+                  -- 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 exp_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,
+        ; 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
@@ -1340,7 +1335,8 @@ tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
 -- 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 = L nm_loc name, fun_matches = matches })
+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!
@@ -1427,12 +1423,12 @@ tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
   = 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)
@@ -1445,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
@@ -1458,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"
@@ -1472,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
 
 ---------------------
@@ -1493,7 +1488,7 @@ getMonoBindInfo tc_binds
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Look at:
    - typecheck/should_compile/ExPat
-   - Trac #12427, typecheck/should_compile/T12427{a,b}
+   - #12427, typecheck/should_compile/T12427{a,b}
 
   data T where
     MkT :: Integral a => a -> Int -> T
@@ -1572,7 +1567,7 @@ We typecheck pattern bindings as follows.  First tcLhs does this:
        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
+       there is one; see #7268). The mkExport part of the
        generalisation step will do the checking and impedance matching
        against the signature.
 
@@ -1594,9 +1589,10 @@ 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
+The beta is untouchable, but floats out of the constraint and can
 be solved absolutely fine.
 
+
 ************************************************************************
 *                                                                      *
                 Generalisation
@@ -1611,7 +1607,7 @@ data GeneralisationPlan
 
   | 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
@@ -1641,7 +1637,7 @@ 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)
 
@@ -1657,7 +1653,7 @@ decideGeneralisationPlan dflags lbinds closed sig_fn
     -- 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
@@ -1685,16 +1681,19 @@ isClosedBndrGroup type_env binds
     fv_env :: NameEnv NameSet
     fv_env = mkNameEnv $ concatMap (bindFvs . unLoc) binds
 
-    bindFvs :: HsBindLR GhcRn idR -> [(Name, NameSet)]
-    bindFvs (FunBind { fun_id = L _ f, bind_fvs = fvs })
-       = let open_fvs = filterNameSet (not . is_closed) fvs
+    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, bind_fvs = fvs })
-       = let open_fvs = filterNameSet (not . is_closed) fvs
+    bindFvs (PatBind { pat_lhs = pat, pat_ext = fvs })
+       = let open_fvs = get_open_fvs fvs
          in [(b, open_fvs) | b <- collectPatBinders pat]
     bindFvs _
        = []
 
+    get_open_fvs fvs = filterNameSet (not . is_closed) fvs
+
     is_closed :: Name -> ClosedTypeId
     is_closed name
       | Just thing <- lookupNameEnv type_env name
@@ -1733,7 +1732,7 @@ isClosedBndrGroup type_env binds
 
 -- 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 :: (SourceTextX p, OutputableBndrId p, Outputable body)
-                 => LPat p -> GRHSs GhcRn 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)