never executed always true always false
    1 
    2 {-# LANGUAGE FlexibleContexts    #-}
    3 {-# LANGUAGE RankNTypes          #-}
    4 {-# LANGUAGE ScopedTypeVariables #-}
    5 {-# LANGUAGE TypeApplications    #-}
    6 {-# LANGUAGE TypeFamilies        #-}
    7 
    8 {-
    9 (c) The University of Glasgow 2006
   10 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   11 
   12 -}
   13 
   14 module GHC.Tc.Gen.Bind
   15    ( tcLocalBinds
   16    , tcTopBinds
   17    , tcValBinds
   18    , tcHsBootSigs
   19    , tcPolyCheck
   20    , chooseInferredQuantifiers
   21    )
   22 where
   23 
   24 import GHC.Prelude
   25 
   26 import {-# SOURCE #-} GHC.Tc.Gen.Match ( tcGRHSsPat, tcMatchesFun )
   27 import {-# SOURCE #-} GHC.Tc.Gen.Expr  ( tcCheckMonoExpr )
   28 import {-# SOURCE #-} GHC.Tc.TyCl.PatSyn ( tcPatSynDecl, tcPatSynBuilderBind )
   29 
   30 import GHC.Types.Tickish (CoreTickish, GenTickish (..))
   31 import GHC.Types.CostCentre (mkUserCC, CCFlavour(DeclCC))
   32 import GHC.Driver.Session
   33 import GHC.Data.FastString
   34 import GHC.Hs
   35 import GHC.Tc.Errors.Types
   36 import GHC.Tc.Gen.Sig
   37 import GHC.Tc.Utils.Concrete ( hasFixedRuntimeRep )
   38 import GHC.Tc.Utils.Monad
   39 import GHC.Tc.Types.Origin
   40 import GHC.Tc.Utils.Env
   41 import GHC.Tc.Utils.Unify
   42 import GHC.Tc.Solver
   43 import GHC.Tc.Types.Evidence
   44 import GHC.Tc.Gen.HsType
   45 import GHC.Tc.Gen.Pat
   46 import GHC.Tc.Utils.TcMType
   47 import GHC.Core.Reduction ( Reduction(..) )
   48 import GHC.Core.Multiplicity
   49 import GHC.Core.FamInstEnv( normaliseType )
   50 import GHC.Tc.Instance.Family( tcGetFamInstEnvs )
   51 import GHC.Tc.Utils.TcType
   52 import GHC.Core.Type (mkStrLitTy, tidyOpenType, mkCastTy)
   53 import GHC.Builtin.Types ( mkBoxedTupleTy )
   54 import GHC.Builtin.Types.Prim
   55 import GHC.Types.SourceText
   56 import GHC.Types.Id
   57 import GHC.Types.Var as Var
   58 import GHC.Types.Var.Set
   59 import GHC.Types.Var.Env( TidyEnv )
   60 import GHC.Unit.Module
   61 import GHC.Types.Name
   62 import GHC.Types.Name.Set
   63 import GHC.Types.Name.Env
   64 import GHC.Types.SrcLoc
   65 import GHC.Data.Bag
   66 import GHC.Utils.Error
   67 import GHC.Data.Graph.Directed
   68 import GHC.Data.Maybe
   69 import GHC.Utils.Misc
   70 import GHC.Types.Basic
   71 import GHC.Types.CompleteMatch
   72 import GHC.Utils.Outputable as Outputable
   73 import GHC.Utils.Panic
   74 import GHC.Builtin.Names( ipClassName )
   75 import GHC.Tc.Validity (checkValidType)
   76 import GHC.Types.Unique.FM
   77 import GHC.Types.Unique.DSet
   78 import GHC.Types.Unique.Set
   79 import qualified GHC.LanguageExtensions as LangExt
   80 
   81 import Control.Monad
   82 import Data.Foldable (find)
   83 
   84 {-
   85 ************************************************************************
   86 *                                                                      *
   87 \subsection{Type-checking bindings}
   88 *                                                                      *
   89 ************************************************************************
   90 
   91 @tcBindsAndThen@ typechecks a @HsBinds@.  The "and then" part is because
   92 it needs to know something about the {\em usage} of the things bound,
   93 so that it can create specialisations of them.  So @tcBindsAndThen@
   94 takes a function which, given an extended environment, E, typechecks
   95 the scope of the bindings returning a typechecked thing and (most
   96 important) an LIE.  It is this LIE which is then used as the basis for
   97 specialising the things bound.
   98 
   99 @tcBindsAndThen@ also takes a "combiner" which glues together the
  100 bindings and the "thing" to make a new "thing".
  101 
  102 The real work is done by @tcBindWithSigsAndThen@.
  103 
  104 Recursive and non-recursive binds are handled in essentially the same
  105 way: because of uniques there are no scoping issues left.  The only
  106 difference is that non-recursive bindings can bind primitive values.
  107 
  108 Even for non-recursive binding groups we add typings for each binder
  109 to the LVE for the following reason.  When each individual binding is
  110 checked the type of its LHS is unified with that of its RHS; and
  111 type-checking the LHS of course requires that the binder is in scope.
  112 
  113 At the top-level the LIE is sure to contain nothing but constant
  114 dictionaries, which we resolve at the module level.
  115 
  116 Note [Polymorphic recursion]
  117 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  118 The game plan for polymorphic recursion in the code above is
  119 
  120         * Bind any variable for which we have a type signature
  121           to an Id with a polymorphic type.  Then when type-checking
  122           the RHSs we'll make a full polymorphic call.
  123 
  124 This fine, but if you aren't a bit careful you end up with a horrendous
  125 amount of partial application and (worse) a huge space leak. For example:
  126 
  127         f :: Eq a => [a] -> [a]
  128         f xs = ...f...
  129 
  130 If we don't take care, after typechecking we get
  131 
  132         f = /\a -> \d::Eq a -> let f' = f a d
  133                                in
  134                                \ys:[a] -> ...f'...
  135 
  136 Notice the stupid construction of (f a d), which is of course
  137 identical to the function we're executing.  In this case, the
  138 polymorphic recursion isn't being used (but that's a very common case).
  139 This can lead to a massive space leak, from the following top-level defn
  140 (post-typechecking)
  141 
  142         ff :: [Int] -> [Int]
  143         ff = f Int dEqInt
  144 
  145 Now (f dEqInt) evaluates to a lambda that has f' as a free variable; but
  146 f' is another thunk which evaluates to the same thing... and you end
  147 up with a chain of identical values all hung onto by the CAF ff.
  148 
  149         ff = f Int dEqInt
  150 
  151            = let f' = f Int dEqInt in \ys. ...f'...
  152 
  153            = let f' = let f' = f Int dEqInt in \ys. ...f'...
  154                       in \ys. ...f'...
  155 
  156 Etc.
  157 
  158 NOTE: a bit of arity analysis would push the (f a d) inside the (\ys...),
  159 which would make the space leak go away in this case
  160 
  161 Solution: when typechecking the RHSs we always have in hand the
  162 *monomorphic* Ids for each binding.  So we just need to make sure that
  163 if (Method f a d) shows up in the constraints emerging from (...f...)
  164 we just use the monomorphic Id.  We achieve this by adding monomorphic Ids
  165 to the "givens" when simplifying constraints.  That's what the "lies_avail"
  166 is doing.
  167 
  168 Then we get
  169 
  170         f = /\a -> \d::Eq a -> letrec
  171                                  fm = \ys:[a] -> ...fm...
  172                                in
  173                                fm
  174 -}
  175 
  176 tcTopBinds :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
  177            -> TcM (TcGblEnv, TcLclEnv)
  178 -- The TcGblEnv contains the new tcg_binds and tcg_spects
  179 -- The TcLclEnv has an extended type envt for the new bindings
  180 tcTopBinds binds sigs
  181   = do  { -- Pattern synonym bindings populate the global environment
  182           (binds', (tcg_env, tcl_env)) <- tcValBinds TopLevel binds sigs $
  183             do { gbl <- getGblEnv
  184                ; lcl <- getLclEnv
  185                ; return (gbl, lcl) }
  186         ; specs <- tcImpPrags sigs   -- SPECIALISE prags for imported Ids
  187 
  188         ; complete_matches <- setEnvs (tcg_env, tcl_env) $ tcCompleteSigs sigs
  189         ; traceTc "complete_matches" (ppr binds $$ ppr sigs)
  190         ; traceTc "complete_matches" (ppr complete_matches)
  191 
  192         ; let { tcg_env' = tcg_env { tcg_imp_specs
  193                                       = specs ++ tcg_imp_specs tcg_env
  194                                    , tcg_complete_matches
  195                                       = complete_matches
  196                                           ++ tcg_complete_matches tcg_env }
  197                            `addTypecheckedBinds` map snd binds' }
  198 
  199         ; return (tcg_env', tcl_env) }
  200         -- The top level bindings are flattened into a giant
  201         -- implicitly-mutually-recursive LHsBinds
  202 
  203 tcCompleteSigs  :: [LSig GhcRn] -> TcM [CompleteMatch]
  204 tcCompleteSigs sigs =
  205   let
  206       doOne :: LSig GhcRn -> TcM (Maybe CompleteMatch)
  207       -- We don't need to "type-check" COMPLETE signatures anymore; if their
  208       -- combinations are invalid it will be found so at match sites.
  209       -- There it is also where we consider if the type of the pattern match is
  210       -- compatible with the result type constructor 'mb_tc'.
  211       doOne (L loc c@(CompleteMatchSig _ext _src_txt (L _ ns) mb_tc_nm))
  212         = fmap Just $ setSrcSpanA loc $ addErrCtxt (text "In" <+> ppr c) $ do
  213             cls   <- mkUniqDSet <$> mapM (addLocMA tcLookupConLike) ns
  214             mb_tc <- traverse @Maybe tcLookupLocatedTyCon mb_tc_nm
  215             pure CompleteMatch { cmConLikes = cls, cmResultTyCon = mb_tc }
  216       doOne _ = return Nothing
  217 
  218   -- For some reason I haven't investigated further, the signatures come in
  219   -- backwards wrt. declaration order. So we reverse them here, because it makes
  220   -- a difference for incomplete match suggestions.
  221   in mapMaybeM doOne $ reverse sigs
  222 
  223 tcHsBootSigs :: [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn] -> TcM [Id]
  224 -- A hs-boot file has only one BindGroup, and it only has type
  225 -- signatures in it.  The renamer checked all this
  226 tcHsBootSigs binds sigs
  227   = do  { checkTc (null binds) TcRnIllegalHsBootFileDecl
  228         ; concatMapM (addLocMA tc_boot_sig) (filter isTypeLSig sigs) }
  229   where
  230     tc_boot_sig (TypeSig _ lnames hs_ty) = mapM f lnames
  231       where
  232         f (L _ name)
  233           = do { sigma_ty <- tcHsSigWcType (FunSigCtxt name NoRRC) hs_ty
  234                ; return (mkVanillaGlobal name sigma_ty) }
  235         -- Notice that we make GlobalIds, not LocalIds
  236     tc_boot_sig s = pprPanic "tcHsBootSigs/tc_boot_sig" (ppr s)
  237 
  238 ------------------------
  239 tcLocalBinds :: HsLocalBinds GhcRn -> TcM thing
  240              -> TcM (HsLocalBinds GhcTc, thing)
  241 
  242 tcLocalBinds (EmptyLocalBinds x) thing_inside
  243   = do  { thing <- thing_inside
  244         ; return (EmptyLocalBinds x, thing) }
  245 
  246 tcLocalBinds (HsValBinds x (XValBindsLR (NValBinds binds sigs))) thing_inside
  247   = do  { (binds', thing) <- tcValBinds NotTopLevel binds sigs thing_inside
  248         ; return (HsValBinds x (XValBindsLR (NValBinds binds' sigs)), thing) }
  249 tcLocalBinds (HsValBinds _ (ValBinds {})) _ = panic "tcLocalBinds"
  250 
  251 tcLocalBinds (HsIPBinds x (IPBinds _ ip_binds)) thing_inside
  252   = do  { ipClass <- tcLookupClass ipClassName
  253         ; (given_ips, ip_binds') <-
  254             mapAndUnzipM (wrapLocSndMA (tc_ip_bind ipClass)) ip_binds
  255 
  256         -- If the binding binds ?x = E, we  must now
  257         -- discharge any ?x constraints in expr_lie
  258         -- See Note [Implicit parameter untouchables]
  259         ; (ev_binds, result) <- checkConstraints (IPSkol ips)
  260                                   [] given_ips thing_inside
  261 
  262         ; return (HsIPBinds x (IPBinds ev_binds ip_binds') , result) }
  263   where
  264     ips = [ip | (L _ (IPBind _ (Left (L _ ip)) _)) <- ip_binds]
  265 
  266         -- I wonder if we should do these one at a time
  267         -- Consider     ?x = 4
  268         --              ?y = ?x + 1
  269     tc_ip_bind ipClass (IPBind _ (Left (L _ ip)) expr)
  270        = do { ty <- newOpenFlexiTyVarTy
  271             ; let p = mkStrLitTy $ hsIPNameFS ip
  272             ; ip_id <- newDict ipClass [ p, ty ]
  273             ; expr' <- tcCheckMonoExpr expr ty
  274             ; let d = toDict ipClass p ty `fmap` expr'
  275             ; return (ip_id, (IPBind noAnn (Right ip_id) d)) }
  276     tc_ip_bind _ (IPBind _ (Right {}) _) = panic "tc_ip_bind"
  277 
  278     -- Coerces a `t` into a dictionary for `IP "x" t`.
  279     -- co : t -> IP "x" t
  280     toDict ipClass x ty = mkHsWrap $ mkWpCastR $
  281                           wrapIP $ mkClassPred ipClass [x,ty]
  282 
  283 {- Note [Implicit parameter untouchables]
  284 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  285 We add the type variables in the types of the implicit parameters
  286 as untouchables, not so much because we really must not unify them,
  287 but rather because we otherwise end up with constraints like this
  288     Num alpha, Implic { wanted = alpha ~ Int }
  289 The constraint solver solves alpha~Int by unification, but then
  290 doesn't float that solved constraint out (it's not an unsolved
  291 wanted).  Result disaster: the (Num alpha) is again solved, this
  292 time by defaulting.  No no no.
  293 
  294 However [Oct 10] this is all handled automatically by the
  295 untouchable-range idea.
  296 -}
  297 
  298 tcValBinds :: TopLevelFlag
  299            -> [(RecFlag, LHsBinds GhcRn)] -> [LSig GhcRn]
  300            -> TcM thing
  301            -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
  302 
  303 tcValBinds top_lvl binds sigs thing_inside
  304   = do  {   -- Typecheck the signatures
  305             -- It's easier to do so now, once for all the SCCs together
  306             -- because a single signature  f,g :: <type>
  307             -- might relate to more than one SCC
  308           (poly_ids, sig_fn) <- tcAddPatSynPlaceholders patsyns $
  309                                 tcTySigs sigs
  310 
  311         -- Extend the envt right away with all the Ids
  312         --   declared with complete type signatures
  313         -- Do not extend the TcBinderStack; instead
  314         --   we extend it on a per-rhs basis in tcExtendForRhs
  315         --   See Note [Relevant bindings and the binder stack]
  316         --
  317         -- For the moment, let bindings and top-level bindings introduce
  318         -- only unrestricted variables.
  319         ; tcExtendSigIds top_lvl poly_ids $
  320      do { (binds', (extra_binds', thing))
  321               <- tcBindGroups top_lvl sig_fn prag_fn binds $
  322                  do { thing <- thing_inside
  323                        -- See Note [Pattern synonym builders don't yield dependencies]
  324                        --     in GHC.Rename.Bind
  325                     ; patsyn_builders <- mapM (tcPatSynBuilderBind prag_fn) patsyns
  326                     ; let extra_binds = [ (NonRecursive, builder)
  327                                         | builder <- patsyn_builders ]
  328                     ; return (extra_binds, thing) }
  329         ; return (binds' ++ extra_binds', thing) }}
  330   where
  331     patsyns = getPatSynBinds binds
  332     prag_fn = mkPragEnv sigs (foldr (unionBags . snd) emptyBag binds)
  333 
  334 ------------------------
  335 tcBindGroups :: TopLevelFlag -> TcSigFun -> TcPragEnv
  336              -> [(RecFlag, LHsBinds GhcRn)] -> TcM thing
  337              -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
  338 -- Typecheck a whole lot of value bindings,
  339 -- one strongly-connected component at a time
  340 -- Here a "strongly connected component" has the straightforward
  341 -- meaning of a group of bindings that mention each other,
  342 -- ignoring type signatures (that part comes later)
  343 
  344 tcBindGroups _ _ _ [] thing_inside
  345   = do  { thing <- thing_inside
  346         ; return ([], thing) }
  347 
  348 tcBindGroups top_lvl sig_fn prag_fn (group : groups) thing_inside
  349   = do  { -- See Note [Closed binder groups]
  350           type_env <- getLclTypeEnv
  351         ; let closed = isClosedBndrGroup type_env (snd group)
  352         ; (group', (groups', thing))
  353                 <- tc_group top_lvl sig_fn prag_fn group closed $
  354                    tcBindGroups top_lvl sig_fn prag_fn groups thing_inside
  355         ; return (group' ++ groups', thing) }
  356 
  357 -- Note [Closed binder groups]
  358 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~
  359 --
  360 --  A mutually recursive group is "closed" if all of the free variables of
  361 --  the bindings are closed. For example
  362 --
  363 -- >  h = \x -> let f = ...g...
  364 -- >                g = ....f...x...
  365 -- >             in ...
  366 --
  367 -- Here @g@ is not closed because it mentions @x@; and hence neither is @f@
  368 -- closed.
  369 --
  370 -- So we need to compute closed-ness on each strongly connected components,
  371 -- before we sub-divide it based on what type signatures it has.
  372 --
  373 
  374 ------------------------
  375 tc_group :: forall thing.
  376             TopLevelFlag -> TcSigFun -> TcPragEnv
  377          -> (RecFlag, LHsBinds GhcRn) -> IsGroupClosed -> TcM thing
  378          -> TcM ([(RecFlag, LHsBinds GhcTc)], thing)
  379 
  380 -- Typecheck one strongly-connected component of the original program.
  381 -- We get a list of groups back, because there may
  382 -- be specialisations etc as well
  383 
  384 tc_group top_lvl sig_fn prag_fn (NonRecursive, binds) closed thing_inside
  385         -- A single non-recursive binding
  386         -- We want to keep non-recursive things non-recursive
  387         -- so that we desugar unlifted bindings correctly
  388   = do { let bind = case bagToList binds of
  389                  [bind] -> bind
  390                  []     -> panic "tc_group: empty list of binds"
  391                  _      -> panic "tc_group: NonRecursive binds is not a singleton bag"
  392        ; (bind', thing) <- tc_single top_lvl sig_fn prag_fn bind closed
  393                                      thing_inside
  394        ; return ( [(NonRecursive, bind')], thing) }
  395 
  396 tc_group top_lvl sig_fn prag_fn (Recursive, binds) closed thing_inside
  397   =     -- To maximise polymorphism, we do a new
  398         -- strongly-connected-component analysis, this time omitting
  399         -- any references to variables with type signatures.
  400         -- (This used to be optional, but isn't now.)
  401         -- See Note [Polymorphic recursion] in "GHC.Hs.Binds".
  402     do  { traceTc "tc_group rec" (pprLHsBinds binds)
  403         ; whenIsJust mbFirstPatSyn $ \lpat_syn ->
  404             recursivePatSynErr (locA $ getLoc lpat_syn) binds
  405         ; (binds1, thing) <- go sccs
  406         ; return ([(Recursive, binds1)], thing) }
  407                 -- Rec them all together
  408   where
  409     mbFirstPatSyn = find (isPatSyn . unLoc) binds
  410     isPatSyn PatSynBind{} = True
  411     isPatSyn _ = False
  412 
  413     sccs :: [SCC (LHsBind GhcRn)]
  414     sccs = stronglyConnCompFromEdgedVerticesUniq (mkEdges sig_fn binds)
  415 
  416     go :: [SCC (LHsBind GhcRn)] -> TcM (LHsBinds GhcTc, thing)
  417     go (scc:sccs) = do  { (binds1, ids1) <- tc_scc scc
  418                          -- recursive bindings must be unrestricted
  419                          -- (the ids added to the environment here are the name of the recursive definitions).
  420                         ; (binds2, thing) <- tcExtendLetEnv top_lvl sig_fn closed ids1
  421                                                             (go sccs)
  422                         ; return (binds1 `unionBags` binds2, thing) }
  423     go []         = do  { thing <- thing_inside; return (emptyBag, thing) }
  424 
  425     tc_scc (AcyclicSCC bind) = tc_sub_group NonRecursive [bind]
  426     tc_scc (CyclicSCC binds) = tc_sub_group Recursive    binds
  427 
  428     tc_sub_group rec_tc binds =
  429       tcPolyBinds sig_fn prag_fn Recursive rec_tc closed binds
  430 
  431 recursivePatSynErr
  432   :: SrcSpan -- ^ The location of the first pattern synonym binding
  433              --   (for error reporting)
  434   -> LHsBinds GhcRn
  435   -> TcM a
  436 recursivePatSynErr loc binds
  437   = failAt loc $ TcRnRecursivePatternSynonym binds
  438 
  439 tc_single :: forall thing.
  440             TopLevelFlag -> TcSigFun -> TcPragEnv
  441           -> LHsBind GhcRn -> IsGroupClosed -> TcM thing
  442           -> TcM (LHsBinds GhcTc, thing)
  443 tc_single _top_lvl sig_fn prag_fn
  444           (L _ (PatSynBind _ psb@PSB{ psb_id = L _ name }))
  445           _ thing_inside
  446   = do { (aux_binds, tcg_env) <- tcPatSynDecl psb (sig_fn name) prag_fn
  447        ; thing <- setGblEnv tcg_env thing_inside
  448        ; return (aux_binds, thing)
  449        }
  450 
  451 tc_single top_lvl sig_fn prag_fn lbind closed thing_inside
  452   = do { (binds1, ids) <- tcPolyBinds sig_fn prag_fn
  453                                       NonRecursive NonRecursive
  454                                       closed
  455                                       [lbind]
  456          -- since we are defining a non-recursive binding, it is not necessary here
  457          -- to define an unrestricted binding. But we do so until toplevel linear bindings are supported.
  458        ; thing <- tcExtendLetEnv top_lvl sig_fn closed ids thing_inside
  459        ; return (binds1, thing) }
  460 
  461 ------------------------
  462 type BKey = Int -- Just number off the bindings
  463 
  464 mkEdges :: TcSigFun -> LHsBinds GhcRn -> [Node BKey (LHsBind GhcRn)]
  465 -- See Note [Polymorphic recursion] in "GHC.Hs.Binds".
  466 mkEdges sig_fn binds
  467   = [ DigraphNode bind key [key | n <- nonDetEltsUniqSet (bind_fvs (unLoc bind)),
  468                          Just key <- [lookupNameEnv key_map n], no_sig n ]
  469     | (bind, key) <- keyd_binds
  470     ]
  471     -- It's OK to use nonDetEltsUFM here as stronglyConnCompFromEdgedVertices
  472     -- is still deterministic even if the edges are in nondeterministic order
  473     -- as explained in Note [Deterministic SCC] in GHC.Data.Graph.Directed.
  474   where
  475     bind_fvs (FunBind { fun_ext = fvs }) = fvs
  476     bind_fvs (PatBind { pat_ext = fvs }) = fvs
  477     bind_fvs _                           = emptyNameSet
  478 
  479     no_sig :: Name -> Bool
  480     no_sig n = not (hasCompleteSig sig_fn n)
  481 
  482     keyd_binds = bagToList binds `zip` [0::BKey ..]
  483 
  484     key_map :: NameEnv BKey     -- Which binding it comes from
  485     key_map = mkNameEnv [(bndr, key) | (L _ bind, key) <- keyd_binds
  486                                      , bndr <- collectHsBindBinders CollNoDictBinders bind ]
  487 
  488 ------------------------
  489 tcPolyBinds :: TcSigFun -> TcPragEnv
  490             -> RecFlag         -- Whether the group is really recursive
  491             -> RecFlag         -- Whether it's recursive after breaking
  492                                -- dependencies based on type signatures
  493             -> IsGroupClosed   -- Whether the group is closed
  494             -> [LHsBind GhcRn]  -- None are PatSynBind
  495             -> TcM (LHsBinds GhcTc, [TcId])
  496 
  497 -- Typechecks a single bunch of values bindings all together,
  498 -- and generalises them.  The bunch may be only part of a recursive
  499 -- group, because we use type signatures to maximise polymorphism
  500 --
  501 -- Returns a list because the input may be a single non-recursive binding,
  502 -- in which case the dependency order of the resulting bindings is
  503 -- important.
  504 --
  505 -- Knows nothing about the scope of the bindings
  506 -- None of the bindings are pattern synonyms
  507 
  508 tcPolyBinds sig_fn prag_fn rec_group rec_tc closed bind_list
  509   = setSrcSpan loc                              $
  510     recoverM (recoveryCode binder_names sig_fn) $ do
  511         -- Set up main recover; take advantage of any type sigs
  512 
  513     { traceTc "------------------------------------------------" Outputable.empty
  514     ; traceTc "Bindings for {" (ppr binder_names)
  515     ; dflags   <- getDynFlags
  516     ; let plan = decideGeneralisationPlan dflags bind_list closed sig_fn
  517     ; traceTc "Generalisation plan" (ppr plan)
  518     ; result@(_, poly_ids) <- case plan of
  519          NoGen              -> tcPolyNoGen rec_tc prag_fn sig_fn bind_list
  520          InferGen mn        -> tcPolyInfer rec_tc prag_fn sig_fn mn bind_list
  521          CheckGen lbind sig -> tcPolyCheck prag_fn sig lbind
  522 
  523     ; _concrete_evs <-
  524         mapM (\ poly_id ->
  525           hasFixedRuntimeRep (FRRBinder $ idName poly_id) (idType poly_id))
  526           poly_ids
  527 
  528     ; traceTc "} End of bindings for" (vcat [ ppr binder_names, ppr rec_group
  529                                             , vcat [ppr id <+> ppr (idType id) | id <- poly_ids]
  530                                           ])
  531 
  532     ; return result }
  533   where
  534     binder_names = collectHsBindListBinders CollNoDictBinders bind_list
  535     loc = foldr1 combineSrcSpans (map (locA . getLoc) bind_list)
  536          -- The mbinds have been dependency analysed and
  537          -- may no longer be adjacent; so find the narrowest
  538          -- span that includes them all
  539 
  540 --------------
  541 -- If typechecking the binds fails, then return with each
  542 -- signature-less binder given type (forall a.a), to minimise
  543 -- subsequent error messages
  544 recoveryCode :: [Name] -> TcSigFun -> TcM (LHsBinds GhcTc, [Id])
  545 recoveryCode binder_names sig_fn
  546   = do  { traceTc "tcBindsWithSigs: error recovery" (ppr binder_names)
  547         ; let poly_ids = map mk_dummy binder_names
  548         ; return (emptyBag, poly_ids) }
  549   where
  550     mk_dummy name
  551       | Just sig <- sig_fn name
  552       , Just poly_id <- completeSigPolyId_maybe sig
  553       = poly_id
  554       | otherwise
  555       = mkLocalId name Many forall_a_a
  556 
  557 forall_a_a :: TcType
  558 -- At one point I had (forall r (a :: TYPE r). a), but of course
  559 -- that type is ill-formed: its mentions 'r' which escapes r's scope.
  560 -- Another alternative would be (forall (a :: TYPE kappa). a), where
  561 -- kappa is a unification variable. But I don't think we need that
  562 -- complication here. I'm going to just use (forall (a::*). a).
  563 -- See #15276
  564 forall_a_a = mkSpecForAllTys [alphaTyVar] alphaTy
  565 
  566 {- *********************************************************************
  567 *                                                                      *
  568                          tcPolyNoGen
  569 *                                                                      *
  570 ********************************************************************* -}
  571 
  572 tcPolyNoGen     -- No generalisation whatsoever
  573   :: RecFlag       -- Whether it's recursive after breaking
  574                    -- dependencies based on type signatures
  575   -> TcPragEnv -> TcSigFun
  576   -> [LHsBind GhcRn]
  577   -> TcM (LHsBinds GhcTc, [TcId])
  578 
  579 tcPolyNoGen rec_tc prag_fn tc_sig_fn bind_list
  580   = do { (binds', mono_infos) <- tcMonoBinds rec_tc tc_sig_fn
  581                                              (LetGblBndr prag_fn)
  582                                              bind_list
  583        ; mono_ids' <- mapM tc_mono_info mono_infos
  584        ; return (binds', mono_ids') }
  585   where
  586     tc_mono_info (MBI { mbi_poly_name = name, mbi_mono_id = mono_id })
  587       = do { _specs <- tcSpecPrags mono_id (lookupPragEnv prag_fn name)
  588            ; return mono_id }
  589            -- NB: tcPrags generates error messages for
  590            --     specialisation pragmas for non-overloaded sigs
  591            -- Indeed that is why we call it here!
  592            -- So we can safely ignore _specs
  593 
  594 
  595 {- *********************************************************************
  596 *                                                                      *
  597                          tcPolyCheck
  598 *                                                                      *
  599 ********************************************************************* -}
  600 
  601 tcPolyCheck :: TcPragEnv
  602             -> TcIdSigInfo     -- Must be a complete signature
  603             -> LHsBind GhcRn   -- Must be a FunBind
  604             -> TcM (LHsBinds GhcTc, [TcId])
  605 -- There is just one binding,
  606 --   it is a FunBind
  607 --   it has a complete type signature,
  608 tcPolyCheck prag_fn
  609             (CompleteSig { sig_bndr  = poly_id
  610                          , sig_ctxt  = ctxt
  611                          , sig_loc   = sig_loc })
  612             (L bind_loc (FunBind { fun_id = L nm_loc name
  613                                  , fun_matches = matches }))
  614   = do { traceTc "tcPolyCheck" (ppr poly_id $$ ppr sig_loc)
  615 
  616        ; mono_name <- newNameAt (nameOccName name) (locA nm_loc)
  617        ; (wrap_gen, (wrap_res, matches'))
  618              <- setSrcSpan sig_loc $ -- Sets the binding location for the skolems
  619                 tcSkolemiseScoped ctxt (idType poly_id) $ \rho_ty ->
  620                 -- Unwraps multiple layers; e.g
  621                 --    f :: forall a. Eq a => forall b. Ord b => blah
  622                 -- NB: tcSkolemise makes fresh type variables
  623                 -- See Note [Instantiate sig with fresh variables]
  624 
  625                 let mono_id = mkLocalId mono_name (varMult poly_id) rho_ty in
  626                 tcExtendBinderStack [TcIdBndr mono_id NotTopLevel] $
  627                 -- Why mono_id in the BinderStack?
  628                 --    See Note [Relevant bindings and the binder stack]
  629 
  630                 setSrcSpanA bind_loc $
  631                 tcMatchesFun (L nm_loc mono_id) matches
  632                              (mkCheckExpType rho_ty)
  633 
  634        -- We make a funny AbsBinds, abstracting over nothing,
  635        -- just so we have somewhere to put the SpecPrags.
  636        -- Otherwise we could just use the FunBind
  637        -- Hence poly_id2 is just a clone of poly_id;
  638        -- We re-use mono-name, but we could equally well use a fresh one
  639 
  640        ; let prag_sigs = lookupPragEnv prag_fn name
  641              poly_id2  = mkLocalId mono_name (idMult poly_id) (idType poly_id)
  642        ; spec_prags <- tcSpecPrags    poly_id prag_sigs
  643        ; poly_id    <- addInlinePrags poly_id prag_sigs
  644 
  645        ; mod <- getModule
  646        ; tick <- funBindTicks (locA nm_loc) poly_id mod prag_sigs
  647 
  648        ; let bind' = FunBind { fun_id      = L nm_loc poly_id2
  649                              , fun_matches = matches'
  650                              , fun_ext     = wrap_gen <.> wrap_res
  651                              , fun_tick    = tick }
  652 
  653              export = ABE { abe_ext   = noExtField
  654                           , abe_wrap  = idHsWrapper
  655                           , abe_poly  = poly_id
  656                           , abe_mono  = poly_id2
  657                           , abe_prags = SpecPrags spec_prags }
  658 
  659              abs_bind = L bind_loc $
  660                         AbsBinds { abs_ext      = noExtField
  661                                  , abs_tvs      = []
  662                                  , abs_ev_vars  = []
  663                                  , abs_ev_binds = []
  664                                  , abs_exports  = [export]
  665                                  , abs_binds    = unitBag (L bind_loc bind')
  666                                  , abs_sig      = True }
  667 
  668        ; return (unitBag abs_bind, [poly_id]) }
  669 
  670 tcPolyCheck _prag_fn sig bind
  671   = pprPanic "tcPolyCheck" (ppr sig $$ ppr bind)
  672 
  673 funBindTicks :: SrcSpan -> TcId -> Module -> [LSig GhcRn]
  674              -> TcM [CoreTickish]
  675 funBindTicks loc fun_id mod sigs
  676   | (mb_cc_str : _) <- [ cc_name | L _ (SCCFunSig _ _ _ cc_name) <- sigs ]
  677       -- this can only be a singleton list, as duplicate pragmas are rejected
  678       -- by the renamer
  679   , let cc_str
  680           | Just cc_str <- mb_cc_str
  681           = sl_fs $ unLoc cc_str
  682           | otherwise
  683           = getOccFS (Var.varName fun_id)
  684         cc_name = moduleNameFS (moduleName mod) `appendFS` consFS '.' cc_str
  685   = do
  686       flavour <- DeclCC <$> getCCIndexTcM cc_name
  687       let cc = mkUserCC cc_name mod loc flavour
  688       return [ProfNote cc True True]
  689   | otherwise
  690   = return []
  691 
  692 {- Note [Instantiate sig with fresh variables]
  693 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  694 It's vital to instantiate a type signature with fresh variables.
  695 For example:
  696       type T = forall a. [a] -> [a]
  697       f :: T;
  698       f = g where { g :: T; g = <rhs> }
  699 
  700  We must not use the same 'a' from the defn of T at both places!!
  701 (Instantiation is only necessary because of type synonyms.  Otherwise,
  702 it's all cool; each signature has distinct type variables from the renamer.)
  703 -}
  704 
  705 
  706 {- *********************************************************************
  707 *                                                                      *
  708                          tcPolyInfer
  709 *                                                                      *
  710 ********************************************************************* -}
  711 
  712 tcPolyInfer
  713   :: RecFlag       -- Whether it's recursive after breaking
  714                    -- dependencies based on type signatures
  715   -> TcPragEnv -> TcSigFun
  716   -> Bool         -- True <=> apply the monomorphism restriction
  717   -> [LHsBind GhcRn]
  718   -> TcM (LHsBinds GhcTc, [TcId])
  719 tcPolyInfer rec_tc prag_fn tc_sig_fn mono bind_list
  720   = do { (tclvl, wanted, (binds', mono_infos))
  721              <- pushLevelAndCaptureConstraints  $
  722                 tcMonoBinds rec_tc tc_sig_fn LetLclBndr bind_list
  723 
  724        ; let name_taus  = [ (mbi_poly_name info, idType (mbi_mono_id info))
  725                           | info <- mono_infos ]
  726              sigs       = [ sig | MBI { mbi_sig = Just sig } <- mono_infos ]
  727              infer_mode = if mono then ApplyMR else NoRestrictions
  728 
  729        ; mapM_ (checkOverloadedSig mono) sigs
  730 
  731        ; traceTc "simplifyInfer call" (ppr tclvl $$ ppr name_taus $$ ppr wanted)
  732        ; (qtvs, givens, ev_binds, insoluble)
  733                  <- simplifyInfer tclvl infer_mode sigs name_taus wanted
  734 
  735        ; let inferred_theta = map evVarPred givens
  736        ; exports <- checkNoErrs $
  737                     mapM (mkExport prag_fn insoluble qtvs inferred_theta) mono_infos
  738 
  739        ; loc <- getSrcSpanM
  740        ; let poly_ids = map abe_poly exports
  741              abs_bind = L (noAnnSrcSpan loc) $
  742                         AbsBinds { abs_ext = noExtField
  743                                  , abs_tvs = qtvs
  744                                  , abs_ev_vars = givens, abs_ev_binds = [ev_binds]
  745                                  , abs_exports = exports, abs_binds = binds'
  746                                  , abs_sig = False }
  747 
  748        ; traceTc "Binding:" (ppr (poly_ids `zip` map idType poly_ids))
  749        ; return (unitBag abs_bind, poly_ids) }
  750          -- poly_ids are guaranteed zonked by mkExport
  751 
  752 --------------
  753 mkExport :: TcPragEnv
  754          -> Bool                        -- True <=> there was an insoluble type error
  755                                         --          when typechecking the bindings
  756          -> [TyVar] -> TcThetaType      -- Both already zonked
  757          -> MonoBindInfo
  758          -> TcM (ABExport GhcTc)
  759 -- Only called for generalisation plan InferGen, not by CheckGen or NoGen
  760 --
  761 -- mkExport generates exports with
  762 --      zonked type variables,
  763 --      zonked poly_ids
  764 -- The former is just because no further unifications will change
  765 -- the quantified type variables, so we can fix their final form
  766 -- right now.
  767 -- The latter is needed because the poly_ids are used to extend the
  768 -- type environment; see the invariant on GHC.Tc.Utils.Env.tcExtendIdEnv
  769 
  770 -- Pre-condition: the qtvs and theta are already zonked
  771 
  772 mkExport prag_fn insoluble qtvs theta
  773          mono_info@(MBI { mbi_poly_name = poly_name
  774                         , mbi_sig       = mb_sig
  775                         , mbi_mono_id   = mono_id })
  776   = do  { mono_ty <- zonkTcType (idType mono_id)
  777         ; poly_id <- mkInferredPolyId insoluble qtvs theta poly_name mb_sig mono_ty
  778 
  779         -- NB: poly_id has a zonked type
  780         ; poly_id <- addInlinePrags poly_id prag_sigs
  781         ; spec_prags <- tcSpecPrags poly_id prag_sigs
  782                 -- tcPrags requires a zonked poly_id
  783 
  784         -- See Note [Impedance matching]
  785         -- NB: we have already done checkValidType, including an ambiguity check,
  786         --     on the type; either when we checked the sig or in mkInferredPolyId
  787         ; let poly_ty     = idType poly_id
  788               sel_poly_ty = mkInfSigmaTy qtvs theta mono_ty
  789                 -- This type is just going into tcSubType,
  790                 -- so Inferred vs. Specified doesn't matter
  791 
  792         ; wrap <- if sel_poly_ty `eqType` poly_ty  -- NB: eqType ignores visibility
  793                   then return idHsWrapper  -- Fast path; also avoids complaint when we infer
  794                                            -- an ambiguous type and have AllowAmbiguousType
  795                                            -- e..g infer  x :: forall a. F a -> Int
  796                   else addErrCtxtM (mk_impedance_match_msg mono_info sel_poly_ty poly_ty) $
  797                        tcSubTypeSigma sig_ctxt sel_poly_ty poly_ty
  798 
  799         ; localSigWarn poly_id mb_sig
  800 
  801         ; return (ABE { abe_ext = noExtField
  802                       , abe_wrap = wrap
  803                         -- abe_wrap :: idType poly_id ~ (forall qtvs. theta => mono_ty)
  804                       , abe_poly  = poly_id
  805                       , abe_mono  = mono_id
  806                       , abe_prags = SpecPrags spec_prags }) }
  807   where
  808     prag_sigs = lookupPragEnv prag_fn poly_name
  809     sig_ctxt  = InfSigCtxt poly_name
  810 
  811 mkInferredPolyId :: Bool  -- True <=> there was an insoluble error when
  812                           --          checking the binding group for this Id
  813                  -> [TyVar] -> TcThetaType
  814                  -> Name -> Maybe TcIdSigInst -> TcType
  815                  -> TcM TcId
  816 mkInferredPolyId insoluble qtvs inferred_theta poly_name mb_sig_inst mono_ty
  817   | Just (TISI { sig_inst_sig = sig })  <- mb_sig_inst
  818   , CompleteSig { sig_bndr = poly_id } <- sig
  819   = return poly_id
  820 
  821   | otherwise  -- Either no type sig or partial type sig
  822   = checkNoErrs $  -- The checkNoErrs ensures that if the type is ambiguous
  823                    -- we don't carry on to the impedance matching, and generate
  824                    -- a duplicate ambiguity error.  There is a similar
  825                    -- checkNoErrs for complete type signatures too.
  826     do { fam_envs <- tcGetFamInstEnvs
  827        ; let mono_ty' = reductionReducedType $ normaliseType fam_envs Nominal mono_ty
  828                -- Unification may not have normalised the type,
  829                -- so do it here to make it as uncomplicated as possible.
  830                -- Example: f :: [F Int] -> Bool
  831                -- should be rewritten to f :: [Char] -> Bool, if possible
  832                --
  833                -- We can discard the coercion _co, because we'll reconstruct
  834                -- it in the call to tcSubType below
  835 
  836        ; (binders, theta') <- chooseInferredQuantifiers inferred_theta
  837                                 (tyCoVarsOfType mono_ty') qtvs mb_sig_inst
  838 
  839        ; let inferred_poly_ty = mkInvisForAllTys binders (mkPhiTy theta' mono_ty')
  840 
  841        ; traceTc "mkInferredPolyId" (vcat [ppr poly_name, ppr qtvs, ppr theta'
  842                                           , ppr inferred_poly_ty])
  843        ; unless insoluble $
  844          addErrCtxtM (mk_inf_msg poly_name inferred_poly_ty) $
  845          checkValidType (InfSigCtxt poly_name) inferred_poly_ty
  846          -- See Note [Validity of inferred types]
  847          -- If we found an insoluble error in the function definition, don't
  848          -- do this check; otherwise (#14000) we may report an ambiguity
  849          -- error for a rather bogus type.
  850 
  851        ; return (mkLocalId poly_name Many inferred_poly_ty) }
  852 
  853 
  854 chooseInferredQuantifiers :: TcThetaType   -- inferred
  855                           -> TcTyVarSet    -- tvs free in tau type
  856                           -> [TcTyVar]     -- inferred quantified tvs
  857                           -> Maybe TcIdSigInst
  858                           -> TcM ([InvisTVBinder], TcThetaType)
  859 chooseInferredQuantifiers inferred_theta tau_tvs qtvs Nothing
  860   = -- No type signature (partial or complete) for this binder,
  861     do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta tau_tvs)
  862                         -- Include kind variables!  #7916
  863              my_theta = pickCapturedPreds free_tvs inferred_theta
  864              binders  = [ mkTyVarBinder InferredSpec tv
  865                         | tv <- qtvs
  866                         , tv `elemVarSet` free_tvs ]
  867        ; return (binders, my_theta) }
  868 
  869 chooseInferredQuantifiers inferred_theta tau_tvs qtvs
  870                           (Just (TISI { sig_inst_sig   = sig  -- Always PartialSig
  871                                       , sig_inst_wcx   = wcx
  872                                       , sig_inst_theta = annotated_theta
  873                                       , sig_inst_skols = annotated_tvs }))
  874   = -- Choose quantifiers for a partial type signature
  875     do { let (psig_qtv_nms, psig_qtv_bndrs) = unzip annotated_tvs
  876        ; psig_qtv_bndrs <- mapM zonkInvisTVBinder psig_qtv_bndrs
  877        ; let psig_qtvs    = map binderVar psig_qtv_bndrs
  878              psig_qtv_set = mkVarSet psig_qtvs
  879              psig_qtv_prs = psig_qtv_nms `zip` psig_qtvs
  880 
  881 
  882             -- Check whether the quantified variables of the
  883             -- partial signature have been unified together
  884             -- See Note [Quantified variables in partial type signatures]
  885        ; mapM_ report_dup_tyvar_tv_err  (findDupTyVarTvs psig_qtv_prs)
  886 
  887             -- Check whether a quantified variable of the partial type
  888             -- signature is not actually quantified.  How can that happen?
  889             -- See Note [Quantification and partial signatures] Wrinkle 4
  890             --     in GHC.Tc.Solver
  891        ; mapM_ report_mono_sig_tv_err [ n | (n,tv) <- psig_qtv_prs
  892                                           , not (tv `elem` qtvs) ]
  893 
  894        ; annotated_theta      <- zonkTcTypes annotated_theta
  895        ; (free_tvs, my_theta) <- choose_psig_context psig_qtv_set annotated_theta wcx
  896 
  897        ; let keep_me    = free_tvs `unionVarSet` psig_qtv_set
  898              final_qtvs = [ mkTyVarBinder vis tv
  899                           | tv <- qtvs -- Pulling from qtvs maintains original order
  900                           , tv `elemVarSet` keep_me
  901                           , let vis = case lookupVarBndr tv psig_qtv_bndrs of
  902                                   Just spec -> spec
  903                                   Nothing   -> InferredSpec ]
  904 
  905        ; return (final_qtvs, my_theta) }
  906   where
  907     report_dup_tyvar_tv_err (n1,n2)
  908       | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
  909       = addErrTc (TcRnPartialTypeSigTyVarMismatch n1 n2 fn_name hs_ty)
  910       | otherwise -- Can't happen; by now we know it's a partial sig
  911       = pprPanic "report_tyvar_tv_err" (ppr sig)
  912 
  913     report_mono_sig_tv_err n
  914       | PartialSig { psig_name = fn_name, psig_hs_ty = hs_ty } <- sig
  915       = addErrTc (TcRnPartialTypeSigBadQuantifier n fn_name hs_ty)
  916       | otherwise -- Can't happen; by now we know it's a partial sig
  917       = pprPanic "report_mono_sig_tv_err" (ppr sig)
  918 
  919     choose_psig_context :: VarSet -> TcThetaType -> Maybe TcType
  920                         -> TcM (VarSet, TcThetaType)
  921     choose_psig_context _ annotated_theta Nothing
  922       = do { let free_tvs = closeOverKinds (tyCoVarsOfTypes annotated_theta
  923                                             `unionVarSet` tau_tvs)
  924            ; return (free_tvs, annotated_theta) }
  925 
  926     choose_psig_context psig_qtvs annotated_theta (Just wc_var_ty)
  927       = do { let free_tvs = closeOverKinds (growThetaTyVars inferred_theta seed_tvs)
  928                             -- growThetaVars just like the no-type-sig case
  929                             -- Omitting this caused #12844
  930                  seed_tvs = tyCoVarsOfTypes annotated_theta  -- These are put there
  931                             `unionVarSet` tau_tvs            --       by the user
  932 
  933            ; let keep_me  = psig_qtvs `unionVarSet` free_tvs
  934                  my_theta = pickCapturedPreds keep_me inferred_theta
  935 
  936            -- Fill in the extra-constraints wildcard hole with inferred_theta,
  937            -- so that the Hole constraint we have already emitted
  938            -- (in tcHsPartialSigType) can report what filled it in.
  939            -- NB: my_theta already includes all the annotated constraints
  940            ; diff_theta <- findInferredDiff annotated_theta my_theta
  941 
  942            ; case tcGetCastedTyVar_maybe wc_var_ty of
  943                -- We know that wc_co must have type kind(wc_var) ~ Constraint, as it
  944                -- comes from the checkExpectedKind in GHC.Tc.Gen.HsType.tcAnonWildCardOcc.
  945                -- So, to make the kinds work out, we reverse the cast here.
  946                Just (wc_var, wc_co) -> writeMetaTyVar wc_var (mk_ctuple diff_theta
  947                                                               `mkCastTy` mkTcSymCo wc_co)
  948                Nothing              -> pprPanic "chooseInferredQuantifiers 1" (ppr wc_var_ty)
  949 
  950            ; traceTc "completeTheta" $
  951                 vcat [ ppr sig
  952                      , text "annotated_theta:" <+> ppr annotated_theta
  953                      , text "inferred_theta:" <+> ppr inferred_theta
  954                      , text "my_theta:" <+> ppr my_theta
  955                      , text "diff_theta:" <+> ppr diff_theta ]
  956            ; return (free_tvs, annotated_theta ++ diff_theta) }
  957              -- Return (annotated_theta ++ diff_theta)
  958              -- See Note [Extra-constraints wildcards]
  959 
  960     mk_ctuple preds = mkBoxedTupleTy preds
  961        -- Hack alert!  See GHC.Tc.Gen.HsType:
  962        -- Note [Extra-constraint holes in partial type signatures]
  963 
  964 mk_impedance_match_msg :: MonoBindInfo
  965                        -> TcType -> TcType
  966                        -> TidyEnv -> TcM (TidyEnv, SDoc)
  967 -- This is a rare but rather awkward error messages
  968 mk_impedance_match_msg (MBI { mbi_poly_name = name, mbi_sig = mb_sig })
  969                        inf_ty sig_ty tidy_env
  970  = do { (tidy_env1, inf_ty) <- zonkTidyTcType tidy_env  inf_ty
  971       ; (tidy_env2, sig_ty) <- zonkTidyTcType tidy_env1 sig_ty
  972       ; let msg = vcat [ text "When checking that the inferred type"
  973                        , nest 2 $ ppr name <+> dcolon <+> ppr inf_ty
  974                        , text "is as general as its" <+> what <+> text "signature"
  975                        , nest 2 $ ppr name <+> dcolon <+> ppr sig_ty ]
  976       ; return (tidy_env2, msg) }
  977   where
  978     what = case mb_sig of
  979              Nothing                     -> text "inferred"
  980              Just sig | isPartialSig sig -> text "(partial)"
  981                       | otherwise        -> empty
  982 
  983 
  984 mk_inf_msg :: Name -> TcType -> TidyEnv -> TcM (TidyEnv, SDoc)
  985 mk_inf_msg poly_name poly_ty tidy_env
  986  = do { (tidy_env1, poly_ty) <- zonkTidyTcType tidy_env poly_ty
  987       ; let msg = vcat [ text "When checking the inferred type"
  988                        , nest 2 $ ppr poly_name <+> dcolon <+> ppr poly_ty ]
  989       ; return (tidy_env1, msg) }
  990 
  991 
  992 -- | Warn the user about polymorphic local binders that lack type signatures.
  993 localSigWarn :: Id -> Maybe TcIdSigInst -> TcM ()
  994 localSigWarn id mb_sig
  995   | Just _ <- mb_sig               = return ()
  996   | not (isSigmaTy (idType id))    = return ()
  997   | otherwise                      = warnMissingSignatures id
  998 
  999 warnMissingSignatures :: Id -> TcM ()
 1000 warnMissingSignatures id
 1001   = do  { env0 <- tcInitTidyEnv
 1002         ; let (env1, tidy_ty) = tidyOpenType env0 (idType id)
 1003         ; let dia = TcRnPolymorphicBinderMissingSig (idName id) tidy_ty
 1004         ; addDiagnosticTcM (env1, dia) }
 1005 
 1006 checkOverloadedSig :: Bool -> TcIdSigInst -> TcM ()
 1007 -- Example:
 1008 --   f :: Eq a => a -> a
 1009 --   K f = e
 1010 -- The MR applies, but the signature is overloaded, and it's
 1011 -- best to complain about this directly
 1012 -- c.f #11339
 1013 checkOverloadedSig monomorphism_restriction_applies sig
 1014   | not (null (sig_inst_theta sig))
 1015   , monomorphism_restriction_applies
 1016   , let orig_sig = sig_inst_sig sig
 1017   = setSrcSpan (sig_loc orig_sig) $
 1018     failWith $ TcRnOverloadedSig orig_sig
 1019   | otherwise
 1020   = return ()
 1021 
 1022 {- Note [Partial type signatures and generalisation]
 1023 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1024 If /any/ of the signatures in the group is a partial type signature
 1025    f :: _ -> Int
 1026 then we *always* use the InferGen plan, and hence tcPolyInfer.
 1027 We do this even for a local binding with -XMonoLocalBinds, when
 1028 we normally use NoGen.
 1029 
 1030 Reasons:
 1031   * The TcSigInfo for 'f' has a unification variable for the '_',
 1032     whose TcLevel is one level deeper than the current level.
 1033     (See pushTcLevelM in tcTySig.)  But NoGen doesn't increase
 1034     the TcLevel like InferGen, so we lose the level invariant.
 1035 
 1036   * The signature might be   f :: forall a. _ -> a
 1037     so it really is polymorphic.  It's not clear what it would
 1038     mean to use NoGen on this, and indeed the ASSERT in tcLhs,
 1039     in the (Just sig) case, checks that if there is a signature
 1040     then we are using LetLclBndr, and hence a nested AbsBinds with
 1041     increased TcLevel
 1042 
 1043 It might be possible to fix these difficulties somehow, but there
 1044 doesn't seem much point.  Indeed, adding a partial type signature is a
 1045 way to get per-binding inferred generalisation.
 1046 
 1047 We apply the MR if /all/ of the partial signatures lack a context.
 1048 In particular (#11016):
 1049    f2 :: (?loc :: Int) => _
 1050    f2 = ?loc
 1051 It's stupid to apply the MR here.  This test includes an extra-constraints
 1052 wildcard; that is, we don't apply the MR if you write
 1053    f3 :: _ => blah
 1054 
 1055 Note [Quantified variables in partial type signatures]
 1056 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1057 Consider
 1058   f :: forall a. a -> a -> _
 1059   f x y = g x y
 1060   g :: forall b. b -> b -> _
 1061   g x y = [x, y]
 1062 
 1063 Here, 'f' and 'g' are mutually recursive, and we end up unifying 'a' and 'b'
 1064 together, which is fine.  So we bind 'a' and 'b' to TyVarTvs, which can then
 1065 unify with each other.
 1066 
 1067 But now consider:
 1068   f :: forall a b. a -> b -> _
 1069   f x y = [x, y]
 1070 
 1071 We want to get an error from this, because 'a' and 'b' get unified.
 1072 So we make a test, one per partial signature, to check that the
 1073 explicitly-quantified type variables have not been unified together.
 1074 #14449 showed this up.
 1075 
 1076 Note [Extra-constraints wildcards]
 1077 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1078 Consider this from #18646
 1079     class Foo x where
 1080       foo :: x
 1081 
 1082     bar :: (Foo (), _) => f ()
 1083     bar = pure foo
 1084 
 1085 We get [W] Foo (), [W] Applicative f.   When we do pickCapturedPreds in
 1086 choose_psig_context, we'll discard Foo ()!  Usually would not quantify over
 1087 such (closed) predicates.  So my_theta will be (Applicative f). But we really
 1088 do want to quantify over (Foo ()) -- it was speicfied by the programmer.
 1089 Solution: always return annotated_theta (user-specified) plus the extra piece
 1090 diff_theta.
 1091 
 1092 Note [Validity of inferred types]
 1093 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1094 We need to check inferred type for validity, in case it uses language
 1095 extensions that are not turned on.  The principle is that if the user
 1096 simply adds the inferred type to the program source, it'll compile fine.
 1097 See #8883.
 1098 
 1099 Examples that might fail:
 1100  - the type might be ambiguous
 1101 
 1102  - an inferred theta that requires type equalities e.g. (F a ~ G b)
 1103                                 or multi-parameter type classes
 1104  - an inferred type that includes unboxed tuples
 1105 
 1106 
 1107 Note [Impedance matching]
 1108 ~~~~~~~~~~~~~~~~~~~~~~~~~
 1109 Consider
 1110    f 0 x = x
 1111    f n x = g [] (not x)
 1112 
 1113    g [] y = f 10 y
 1114    g _  y = f 9  y
 1115 
 1116 After typechecking we'll get
 1117   f_mono_ty :: a -> Bool -> Bool
 1118   g_mono_ty :: [b] -> Bool -> Bool
 1119 with constraints
 1120   (Eq a, Num a)
 1121 
 1122 Note that f is polymorphic in 'a' and g in 'b'; and these are not linked.
 1123 The types we really want for f and g are
 1124    f :: forall a. (Eq a, Num a) => a -> Bool -> Bool
 1125    g :: forall b. [b] -> Bool -> Bool
 1126 
 1127 We can get these by "impedance matching":
 1128    tuple :: forall a b. (Eq a, Num a) => (a -> Bool -> Bool, [b] -> Bool -> Bool)
 1129    tuple a b d1 d1 = let ...bind f_mono, g_mono in (f_mono, g_mono)
 1130 
 1131    f a d1 d2 = case tuple a Any d1 d2 of (f, g) -> f
 1132    g b = case tuple Integer b dEqInteger dNumInteger of (f,g) -> g
 1133 
 1134 Suppose the shared quantified tyvars are qtvs and constraints theta.
 1135 Then we want to check that
 1136      forall qtvs. theta => f_mono_ty   is more polymorphic than   f's polytype
 1137 and the proof is the impedance matcher.
 1138 
 1139 Notice that the impedance matcher may do defaulting.  See #7173.
 1140 
 1141 It also cleverly does an ambiguity check; for example, rejecting
 1142    f :: F a -> F a
 1143 where F is a non-injective type function.
 1144 -}
 1145 
 1146 
 1147 {-
 1148 Note [SPECIALISE pragmas]
 1149 ~~~~~~~~~~~~~~~~~~~~~~~~~
 1150 There is no point in a SPECIALISE pragma for a non-overloaded function:
 1151    reverse :: [a] -> [a]
 1152    {-# SPECIALISE reverse :: [Int] -> [Int] #-}
 1153 
 1154 But SPECIALISE INLINE *can* make sense for GADTS:
 1155    data Arr e where
 1156      ArrInt :: !Int -> ByteArray# -> Arr Int
 1157      ArrPair :: !Int -> Arr e1 -> Arr e2 -> Arr (e1, e2)
 1158 
 1159    (!:) :: Arr e -> Int -> e
 1160    {-# SPECIALISE INLINE (!:) :: Arr Int -> Int -> Int #-}
 1161    {-# SPECIALISE INLINE (!:) :: Arr (a, b) -> Int -> (a, b) #-}
 1162    (ArrInt _ ba)     !: (I# i) = I# (indexIntArray# ba i)
 1163    (ArrPair _ a1 a2) !: i      = (a1 !: i, a2 !: i)
 1164 
 1165 When (!:) is specialised it becomes non-recursive, and can usefully
 1166 be inlined.  Scary!  So we only warn for SPECIALISE *without* INLINE
 1167 for a non-overloaded function.
 1168 
 1169 ************************************************************************
 1170 *                                                                      *
 1171                          tcMonoBinds
 1172 *                                                                      *
 1173 ************************************************************************
 1174 
 1175 @tcMonoBinds@ deals with a perhaps-recursive group of HsBinds.
 1176 The signatures have been dealt with already.
 1177 -}
 1178 
 1179 data MonoBindInfo = MBI { mbi_poly_name :: Name
 1180                         , mbi_sig       :: Maybe TcIdSigInst
 1181                         , mbi_mono_id   :: TcId }
 1182 
 1183 tcMonoBinds :: RecFlag  -- Whether the binding is recursive for typechecking purposes
 1184                         -- i.e. the binders are mentioned in their RHSs, and
 1185                         --      we are not rescued by a type signature
 1186             -> TcSigFun -> LetBndrSpec
 1187             -> [LHsBind GhcRn]
 1188             -> TcM (LHsBinds GhcTc, [MonoBindInfo])
 1189 
 1190 -- SPECIAL CASE 1: see Note [Special case for non-recursive function bindings]
 1191 tcMonoBinds is_rec sig_fn no_gen
 1192            [ L b_loc (FunBind { fun_id = L nm_loc name
 1193                               , fun_matches = matches })]
 1194                              -- Single function binding,
 1195   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
 1196   , Nothing <- sig_fn name   -- ...with no type signature
 1197   = setSrcSpanA b_loc    $
 1198     do  { ((co_fn, matches'), mono_id, _) <- fixM $ \ ~(_, _, rhs_ty) ->
 1199                                           -- See Note [fixM for rhs_ty in tcMonoBinds]
 1200             do  { mono_id <- newLetBndr no_gen name Many rhs_ty
 1201                 ; (matches', rhs_ty')
 1202                     <- tcInfer $ \ exp_ty ->
 1203                        tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $
 1204                           -- We extend the error context even for a non-recursive
 1205                           -- function so that in type error messages we show the
 1206                           -- type of the thing whose rhs we are type checking
 1207                        tcMatchesFun (L nm_loc mono_id) matches exp_ty
 1208                 ; return (matches', mono_id, rhs_ty')
 1209                 }
 1210 
 1211         ; return (unitBag $ L b_loc $
 1212                      FunBind { fun_id = L nm_loc mono_id,
 1213                                fun_matches = matches',
 1214                                fun_ext = co_fn, fun_tick = [] },
 1215                   [MBI { mbi_poly_name = name
 1216                        , mbi_sig       = Nothing
 1217                        , mbi_mono_id   = mono_id }]) }
 1218 
 1219 -- SPECIAL CASE 2: see Note [Special case for non-recursive pattern bindings]
 1220 tcMonoBinds is_rec sig_fn no_gen
 1221            [L b_loc (PatBind { pat_lhs = pat, pat_rhs = grhss })]
 1222   | NonRecursive <- is_rec   -- ...binder isn't mentioned in RHS
 1223   , all (isNothing . sig_fn) bndrs
 1224   = addErrCtxt (patMonoBindsCtxt pat grhss) $
 1225     do { (grhss', pat_ty) <- tcInfer $ \ exp_ty ->
 1226                              tcGRHSsPat grhss exp_ty
 1227 
 1228        ; let exp_pat_ty :: Scaled ExpSigmaType
 1229              exp_pat_ty = unrestricted (mkCheckExpType pat_ty)
 1230        ; (pat', mbis) <- tcLetPat (const Nothing) no_gen pat exp_pat_ty $
 1231                          mapM lookupMBI bndrs
 1232 
 1233        ; return ( unitBag $ L b_loc $
 1234                      PatBind { pat_lhs = pat', pat_rhs = grhss'
 1235                              , pat_ext = pat_ty, pat_ticks = ([],[]) }
 1236 
 1237                 , mbis ) }
 1238   where
 1239     bndrs = collectPatBinders CollNoDictBinders pat
 1240 
 1241 -- GENERAL CASE
 1242 tcMonoBinds _ sig_fn no_gen binds
 1243   = do  { tc_binds <- mapM (wrapLocMA (tcLhs sig_fn no_gen)) binds
 1244 
 1245         -- Bring the monomorphic Ids, into scope for the RHSs
 1246         ; let mono_infos = getMonoBindInfo tc_binds
 1247               rhs_id_env = [ (name, mono_id)
 1248                            | MBI { mbi_poly_name = name
 1249                                  , mbi_sig       = mb_sig
 1250                                  , mbi_mono_id   = mono_id } <- mono_infos
 1251                            , case mb_sig of
 1252                                Just sig -> isPartialSig sig
 1253                                Nothing  -> True ]
 1254                 -- A monomorphic binding for each term variable that lacks
 1255                 -- a complete type sig.  (Ones with a sig are already in scope.)
 1256 
 1257         ; traceTc "tcMonoBinds" $ vcat [ ppr n <+> ppr id <+> ppr (idType id)
 1258                                        | (n,id) <- rhs_id_env]
 1259         ; binds' <- tcExtendRecIds rhs_id_env $
 1260                     mapM (wrapLocMA tcRhs) tc_binds
 1261 
 1262         ; return (listToBag binds', mono_infos) }
 1263 
 1264 {- Note [Special case for non-recursive function bindings]
 1265 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1266 In the special case of
 1267 * A non-recursive FunBind
 1268 * With no type signature
 1269 we infer the type of the right hand side first (it may have a
 1270 higher-rank type) and *then* make the monomorphic Id for the LHS e.g.
 1271    f = \(x::forall a. a->a) -> <body>
 1272 
 1273 We want to infer a higher-rank type for f
 1274 
 1275 Note [Special case for non-recursive pattern bindings]
 1276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1277 In the special case of
 1278 * A pattern binding
 1279 * With no type signature for any of the binders
 1280 we can /infer/ the type of the RHS, and /check/ the pattern
 1281 against that type.  For example (#18323)
 1282 
 1283   ids :: [forall a. a -> a]
 1284   combine :: (forall a . [a] -> a) -> [forall a. a -> a]
 1285           -> ((forall a . [a] -> a), [forall a. a -> a])
 1286 
 1287   (x,y) = combine head ids
 1288 
 1289 with -XImpredicativeTypes we can infer a good type for
 1290 (combine head ids), and use that to tell us the polymorphic
 1291 types of x and y.
 1292 
 1293 We don't need to check -XImpredicativeTypes beucase without it
 1294 these types like [forall a. a->a] are illegal anyway, so this
 1295 special case code only really has an effect if -XImpredicativeTypes
 1296 is on.  Small exception:
 1297   (x) = e
 1298 is currently treated as a pattern binding so, even absent
 1299 -XImpredicativeTypes, we will get a small improvement in behaviour.
 1300 But I don't think it's worth an extension flag.
 1301 
 1302 Why do we require no type signatures on /any/ of the binders?
 1303 Consider
 1304    x :: forall a. a->a
 1305    y :: forall a. a->a
 1306    (x,y) = (id,id)
 1307 
 1308 Here we should /check/ the RHS with expected type
 1309   (forall a. a->a, forall a. a->a).
 1310 
 1311 If we have no signatures, we can the approach of this Note
 1312 to /infer/ the type of the RHS.
 1313 
 1314 But what if we have some signatures, but not all? Say this:
 1315   p :: forall a. a->a
 1316   (p,q) = (id,  (\(x::forall b. b->b). x True))
 1317 
 1318 Here we want to push p's signature inwards, i.e. /checking/, to
 1319 correctly elaborate 'id'. But we want to /infer/ q's higher rank
 1320 type.  There seems to be no way to do this.  So currently we only
 1321 switch to inference when we have no signature for any of the binders.
 1322 
 1323 Note [fixM for rhs_ty in tcMonoBinds]
 1324 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1325 In order to create mono_id we need rhs_ty but we don't have it yet,
 1326 we only get it from tcMatchesFun later (which needs mono_id to put
 1327 into HsMatchContext for pretty printing). To solve this, create
 1328 a thunk of rhs_ty with fixM that we fill in later.
 1329 
 1330 This is fine only because neither newLetBndr or tcMatchesFun look
 1331 at the varType field of the Id. tcMatchesFun only looks at idName
 1332 of mono_id.
 1333 
 1334 Also see #20415 for the bigger picture of why tcMatchesFun needs
 1335 mono_id in the first place.
 1336 -}
 1337 
 1338 
 1339 ------------------------
 1340 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
 1341 -- we typecheck the RHSs.  Basically what we are doing is this: for each binder:
 1342 --      if there's a signature for it, use the instantiated signature type
 1343 --      otherwise invent a type variable
 1344 -- You see that quite directly in the FunBind case.
 1345 --
 1346 -- But there's a complication for pattern bindings:
 1347 --      data T = MkT (forall a. a->a)
 1348 --      MkT f = e
 1349 -- Here we can guess a type variable for the entire LHS (which will be refined to T)
 1350 -- but we want to get (f::forall a. a->a) as the RHS environment.
 1351 -- The simplest way to do this is to typecheck the pattern, and then look up the
 1352 -- bound mono-ids.  Then we want to retain the typechecked pattern to avoid re-doing
 1353 -- it; hence the TcMonoBind data type in which the LHS is done but the RHS isn't
 1354 
 1355 data TcMonoBind         -- Half completed; LHS done, RHS not done
 1356   = TcFunBind  MonoBindInfo  SrcSpan (MatchGroup GhcRn (LHsExpr GhcRn))
 1357   | TcPatBind [MonoBindInfo] (LPat GhcTc) (GRHSs GhcRn (LHsExpr GhcRn))
 1358               TcSigmaType
 1359 
 1360 tcLhs :: TcSigFun -> LetBndrSpec -> HsBind GhcRn -> TcM TcMonoBind
 1361 -- Only called with plan InferGen (LetBndrSpec = LetLclBndr)
 1362 --                    or NoGen    (LetBndrSpec = LetGblBndr)
 1363 -- CheckGen is used only for functions with a complete type signature,
 1364 --          and tcPolyCheck doesn't use tcMonoBinds at all
 1365 
 1366 tcLhs sig_fn no_gen (FunBind { fun_id = L nm_loc name
 1367                              , fun_matches = matches })
 1368   | Just (TcIdSig sig) <- sig_fn name
 1369   = -- There is a type signature.
 1370     -- It must be partial; if complete we'd be in tcPolyCheck!
 1371     --    e.g.   f :: _ -> _
 1372     --           f x = ...g...
 1373     --           Just g = ...f...
 1374     -- Hence always typechecked with InferGen
 1375     do { mono_info <- tcLhsSigId no_gen (name, sig)
 1376        ; return (TcFunBind mono_info (locA nm_loc) matches) }
 1377 
 1378   | otherwise  -- No type signature
 1379   = do { mono_ty <- newOpenFlexiTyVarTy
 1380        ; mono_id <- newLetBndr no_gen name Many mono_ty
 1381           -- This ^ generates a binder with Many multiplicity because all
 1382           -- let/where-binders are unrestricted. When we introduce linear let
 1383           -- binders, we will need to retrieve the multiplicity information.
 1384        ; let mono_info = MBI { mbi_poly_name = name
 1385                              , mbi_sig       = Nothing
 1386                              , mbi_mono_id   = mono_id }
 1387        ; return (TcFunBind mono_info (locA nm_loc) matches) }
 1388 
 1389 tcLhs sig_fn no_gen (PatBind { pat_lhs = pat, pat_rhs = grhss })
 1390   = -- See Note [Typechecking pattern bindings]
 1391     do  { sig_mbis <- mapM (tcLhsSigId no_gen) sig_names
 1392 
 1393         ; let inst_sig_fun = lookupNameEnv $ mkNameEnv $
 1394                              [ (mbi_poly_name mbi, mbi_mono_id mbi)
 1395                              | mbi <- sig_mbis ]
 1396 
 1397             -- See Note [Existentials in pattern bindings]
 1398         ; ((pat', nosig_mbis), pat_ty)
 1399             <- addErrCtxt (patMonoBindsCtxt pat grhss) $
 1400                tcInfer $ \ exp_ty ->
 1401                tcLetPat inst_sig_fun no_gen pat (unrestricted exp_ty) $
 1402                  -- The above inferred type get an unrestricted multiplicity. It may be
 1403                  -- worth it to try and find a finer-grained multiplicity here
 1404                  -- if examples warrant it.
 1405                mapM lookupMBI nosig_names
 1406 
 1407         ; let mbis = sig_mbis ++ nosig_mbis
 1408 
 1409         ; traceTc "tcLhs" (vcat [ ppr id <+> dcolon <+> ppr (idType id)
 1410                                 | mbi <- mbis, let id = mbi_mono_id mbi ]
 1411                            $$ ppr no_gen)
 1412 
 1413         ; return (TcPatBind mbis pat' grhss pat_ty) }
 1414   where
 1415     bndr_names = collectPatBinders CollNoDictBinders pat
 1416     (nosig_names, sig_names) = partitionWith find_sig bndr_names
 1417 
 1418     find_sig :: Name -> Either Name (Name, TcIdSigInfo)
 1419     find_sig name = case sig_fn name of
 1420                       Just (TcIdSig sig) -> Right (name, sig)
 1421                       _                  -> Left name
 1422 
 1423 tcLhs _ _ other_bind = pprPanic "tcLhs" (ppr other_bind)
 1424         -- AbsBind, VarBind impossible
 1425 
 1426 lookupMBI :: Name -> TcM MonoBindInfo
 1427 -- After typechecking the pattern, look up the binder
 1428 -- names that lack a signature, which the pattern has brought
 1429 -- into scope.
 1430 lookupMBI name
 1431   = do { mono_id <- tcLookupId name
 1432        ; return (MBI { mbi_poly_name = name
 1433                      , mbi_sig       = Nothing
 1434                      , mbi_mono_id   = mono_id }) }
 1435 
 1436 -------------------
 1437 tcLhsSigId :: LetBndrSpec -> (Name, TcIdSigInfo) -> TcM MonoBindInfo
 1438 tcLhsSigId no_gen (name, sig)
 1439   = do { inst_sig <- tcInstSig sig
 1440        ; mono_id <- newSigLetBndr no_gen name inst_sig
 1441        ; return (MBI { mbi_poly_name = name
 1442                      , mbi_sig       = Just inst_sig
 1443                      , mbi_mono_id   = mono_id }) }
 1444 
 1445 ------------
 1446 newSigLetBndr :: LetBndrSpec -> Name -> TcIdSigInst -> TcM TcId
 1447 newSigLetBndr (LetGblBndr prags) name (TISI { sig_inst_sig = id_sig })
 1448   | CompleteSig { sig_bndr = poly_id } <- id_sig
 1449   = addInlinePrags poly_id (lookupPragEnv prags name)
 1450 newSigLetBndr no_gen name (TISI { sig_inst_tau = tau })
 1451   = newLetBndr no_gen name Many tau
 1452     -- Binders with a signature are currently always of multiplicity
 1453     -- Many. Because they come either from toplevel, let, or where
 1454     -- declarations. Which are all unrestricted currently.
 1455 
 1456 -------------------
 1457 tcRhs :: TcMonoBind -> TcM (HsBind GhcTc)
 1458 tcRhs (TcFunBind info@(MBI { mbi_sig = mb_sig, mbi_mono_id = mono_id })
 1459                  loc matches)
 1460   = tcExtendIdBinderStackForRhs [info]  $
 1461     tcExtendTyVarEnvForRhs mb_sig       $
 1462     do  { traceTc "tcRhs: fun bind" (ppr mono_id $$ ppr (idType mono_id))
 1463         ; (co_fn, matches') <- tcMatchesFun (L (noAnnSrcSpan loc) mono_id)
 1464                                  matches (mkCheckExpType $ idType mono_id)
 1465         ; return ( FunBind { fun_id = L (noAnnSrcSpan loc) mono_id
 1466                            , fun_matches = matches'
 1467                            , fun_ext = co_fn
 1468                            , fun_tick = [] } ) }
 1469 
 1470 tcRhs (TcPatBind infos pat' grhss pat_ty)
 1471   = -- When we are doing pattern bindings we *don't* bring any scoped
 1472     -- type variables into scope unlike function bindings
 1473     -- Wny not?  They are not completely rigid.
 1474     -- That's why we have the special case for a single FunBind in tcMonoBinds
 1475     tcExtendIdBinderStackForRhs infos        $
 1476     do  { traceTc "tcRhs: pat bind" (ppr pat' $$ ppr pat_ty)
 1477         ; grhss' <- addErrCtxt (patMonoBindsCtxt pat' grhss) $
 1478                     tcGRHSsPat grhss (mkCheckExpType pat_ty)
 1479 
 1480         ; return ( PatBind { pat_lhs = pat', pat_rhs = grhss'
 1481                            , pat_ext = pat_ty
 1482                            , pat_ticks = ([],[]) } )}
 1483 
 1484 tcExtendTyVarEnvForRhs :: Maybe TcIdSigInst -> TcM a -> TcM a
 1485 tcExtendTyVarEnvForRhs Nothing thing_inside
 1486   = thing_inside
 1487 tcExtendTyVarEnvForRhs (Just sig) thing_inside
 1488   = tcExtendTyVarEnvFromSig sig thing_inside
 1489 
 1490 tcExtendTyVarEnvFromSig :: TcIdSigInst -> TcM a -> TcM a
 1491 tcExtendTyVarEnvFromSig sig_inst thing_inside
 1492   | TISI { sig_inst_skols = skol_prs, sig_inst_wcs = wcs } <- sig_inst
 1493   = tcExtendNameTyVarEnv wcs $
 1494     tcExtendNameTyVarEnv (mapSnd binderVar skol_prs) $
 1495     thing_inside
 1496 
 1497 tcExtendIdBinderStackForRhs :: [MonoBindInfo] -> TcM a -> TcM a
 1498 -- See Note [Relevant bindings and the binder stack]
 1499 tcExtendIdBinderStackForRhs infos thing_inside
 1500   = tcExtendBinderStack [ TcIdBndr mono_id NotTopLevel
 1501                         | MBI { mbi_mono_id = mono_id } <- infos ]
 1502                         thing_inside
 1503     -- NotTopLevel: it's a monomorphic binding
 1504 
 1505 ---------------------
 1506 getMonoBindInfo :: [LocatedA TcMonoBind] -> [MonoBindInfo]
 1507 getMonoBindInfo tc_binds
 1508   = foldr (get_info . unLoc) [] tc_binds
 1509   where
 1510     get_info (TcFunBind info _ _)    rest = info : rest
 1511     get_info (TcPatBind infos _ _ _) rest = infos ++ rest
 1512 
 1513 
 1514 {- Note [Relevant bindings and the binder stack]
 1515 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1516 When typecking a binding we extend the TcBinderStack for the RHS of
 1517 the binding, with the /monomorphic/ Id.  That way, if we have, say
 1518     f = \x -> blah
 1519 and something goes wrong in 'blah', we get a "relevant binding"
 1520 looking like  f :: alpha -> beta
 1521 This applies if 'f' has a type signature too:
 1522    f :: forall a. [a] -> [a]
 1523    f x = True
 1524 We can't unify True with [a], and a relevant binding is f :: [a] -> [a]
 1525 If we had the *polymorphic* version of f in the TcBinderStack, it
 1526 would not be reported as relevant, because its type is closed.
 1527 (See TcErrors.relevantBindings.)
 1528 
 1529 Note [Typechecking pattern bindings]
 1530 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1531 Look at:
 1532    - typecheck/should_compile/ExPat
 1533    - #12427, typecheck/should_compile/T12427{a,b}
 1534 
 1535   data T where
 1536     MkT :: Integral a => a -> Int -> T
 1537 
 1538 and suppose t :: T.  Which of these pattern bindings are ok?
 1539 
 1540   E1. let { MkT p _ = t } in <body>
 1541 
 1542   E2. let { MkT _ q = t } in <body>
 1543 
 1544   E3. let { MkT (toInteger -> r) _ = t } in <body>
 1545 
 1546 * (E1) is clearly wrong because the existential 'a' escapes.
 1547   What type could 'p' possibly have?
 1548 
 1549 * (E2) is fine, despite the existential pattern, because
 1550   q::Int, and nothing escapes.
 1551 
 1552 * Even (E3) is fine.  The existential pattern binds a dictionary
 1553   for (Integral a) which the view pattern can use to convert the
 1554   a-valued field to an Integer, so r :: Integer.
 1555 
 1556 An easy way to see all three is to imagine the desugaring.
 1557 For (E2) it would look like
 1558     let q = case t of MkT _ q' -> q'
 1559     in <body>
 1560 
 1561 
 1562 We typecheck pattern bindings as follows.  First tcLhs does this:
 1563 
 1564   1. Take each type signature q :: ty, partial or complete, and
 1565      instantiate it (with tcLhsSigId) to get a MonoBindInfo.  This
 1566      gives us a fresh "mono_id" qm :: instantiate(ty), where qm has
 1567      a fresh name.
 1568 
 1569      Any fresh unification variables in instantiate(ty) born here, not
 1570      deep under implications as would happen if we allocated them when
 1571      we encountered q during tcPat.
 1572 
 1573   2. Build a little environment mapping "q" -> "qm" for those Ids
 1574      with signatures (inst_sig_fun)
 1575 
 1576   3. Invoke tcLetPat to typecheck the pattern.
 1577 
 1578      - We pass in the current TcLevel.  This is captured by
 1579        GHC.Tc.Gen.Pat.tcLetPat, and put into the pc_lvl field of PatCtxt, in
 1580        PatEnv.
 1581 
 1582      - When tcPat finds an existential constructor, it binds fresh
 1583        type variables and dictionaries as usual, increments the TcLevel,
 1584        and emits an implication constraint.
 1585 
 1586      - When we come to a binder (GHC.Tc.Gen.Pat.tcPatBndr), it looks it up
 1587        in the little environment (the pc_sig_fn field of PatCtxt).
 1588 
 1589          Success => There was a type signature, so just use it,
 1590                     checking compatibility with the expected type.
 1591 
 1592          Failure => No type signature.
 1593              Infer case: (happens only outside any constructor pattern)
 1594                          use a unification variable
 1595                          at the outer level pc_lvl
 1596 
 1597              Check case: use promoteTcType to promote the type
 1598                          to the outer level pc_lvl.  This is the
 1599                          place where we emit a constraint that'll blow
 1600                          up if existential capture takes place
 1601 
 1602        Result: the type of the binder is always at pc_lvl. This is
 1603        crucial.
 1604 
 1605   4. Throughout, when we are making up an Id for the pattern-bound variables
 1606      (newLetBndr), we have two cases:
 1607 
 1608      - If we are generalising (generalisation plan is InferGen or
 1609        CheckGen), then the let_bndr_spec will be LetLclBndr.  In that case
 1610        we want to bind a cloned, local version of the variable, with the
 1611        type given by the pattern context, *not* by the signature (even if
 1612        there is one; see #7268). The mkExport part of the
 1613        generalisation step will do the checking and impedance matching
 1614        against the signature.
 1615 
 1616      - If for some reason we are not generalising (plan = NoGen), the
 1617        LetBndrSpec will be LetGblBndr.  In that case we must bind the
 1618        global version of the Id, and do so with precisely the type given
 1619        in the signature.  (Then we unify with the type from the pattern
 1620        context type.)
 1621 
 1622 
 1623 And that's it!  The implication constraints check for the skolem
 1624 escape.  It's quite simple and neat, and more expressive than before
 1625 e.g. GHC 8.0 rejects (E2) and (E3).
 1626 
 1627 Example for (E1), starting at level 1.  We generate
 1628      p :: beta:1, with constraints (forall:3 a. Integral a => a ~ beta)
 1629 The (a~beta) can't float (because of the 'a'), nor be solved (because
 1630 beta is untouchable.)
 1631 
 1632 Example for (E2), we generate
 1633      q :: beta:1, with constraint (forall:3 a. Integral a => Int ~ beta)
 1634 The beta is untouchable, but floats out of the constraint and can
 1635 be solved absolutely fine.
 1636 
 1637 
 1638 ************************************************************************
 1639 *                                                                      *
 1640                 Generalisation
 1641 *                                                                      *
 1642 ********************************************************************* -}
 1643 
 1644 data GeneralisationPlan
 1645   = NoGen               -- No generalisation, no AbsBinds
 1646 
 1647   | InferGen            -- Implicit generalisation; there is an AbsBinds
 1648        Bool             --   True <=> apply the MR; generalise only unconstrained type vars
 1649 
 1650   | CheckGen (LHsBind GhcRn) TcIdSigInfo
 1651                         -- One FunBind with a signature
 1652                         -- Explicit generalisation
 1653 
 1654 -- A consequence of the no-AbsBinds choice (NoGen) is that there is
 1655 -- no "polymorphic Id" and "monmomorphic Id"; there is just the one
 1656 
 1657 instance Outputable GeneralisationPlan where
 1658   ppr NoGen          = text "NoGen"
 1659   ppr (InferGen b)   = text "InferGen" <+> ppr b
 1660   ppr (CheckGen _ s) = text "CheckGen" <+> ppr s
 1661 
 1662 decideGeneralisationPlan
 1663    :: DynFlags -> [LHsBind GhcRn] -> IsGroupClosed -> TcSigFun
 1664    -> GeneralisationPlan
 1665 decideGeneralisationPlan dflags lbinds closed sig_fn
 1666   | has_partial_sigs                         = InferGen (and partial_sig_mrs)
 1667   | Just (bind, sig) <- one_funbind_with_sig = CheckGen bind sig
 1668   | do_not_generalise closed                 = NoGen
 1669   | otherwise                                = InferGen mono_restriction
 1670   where
 1671     binds = map unLoc lbinds
 1672 
 1673     partial_sig_mrs :: [Bool]
 1674     -- One for each partial signature (so empty => no partial sigs)
 1675     -- The Bool is True if the signature has no constraint context
 1676     --      so we should apply the MR
 1677     -- See Note [Partial type signatures and generalisation]
 1678     partial_sig_mrs
 1679       = [ null $ fromMaybeContext mtheta
 1680         | TcIdSig (PartialSig { psig_hs_ty = hs_ty })
 1681             <- mapMaybe sig_fn (collectHsBindListBinders CollNoDictBinders lbinds)
 1682         , let (mtheta, _) = splitLHsQualTy (hsSigWcType hs_ty) ]
 1683 
 1684     has_partial_sigs   = not (null partial_sig_mrs)
 1685 
 1686     mono_restriction  = xopt LangExt.MonomorphismRestriction dflags
 1687                      && any restricted binds
 1688 
 1689     do_not_generalise (IsGroupClosed _ True) = False
 1690         -- The 'True' means that all of the group's
 1691         -- free vars have ClosedTypeId=True; so we can ignore
 1692         -- -XMonoLocalBinds, and generalise anyway
 1693     do_not_generalise _ = xopt LangExt.MonoLocalBinds dflags
 1694 
 1695     -- With OutsideIn, all nested bindings are monomorphic
 1696     -- except a single function binding with a signature
 1697     one_funbind_with_sig
 1698       | [lbind@(L _ (FunBind { fun_id = v }))] <- lbinds
 1699       , Just (TcIdSig sig) <- sig_fn (unLoc v)
 1700       = Just (lbind, sig)
 1701       | otherwise
 1702       = Nothing
 1703 
 1704     -- The Haskell 98 monomorphism restriction
 1705     restricted (PatBind {})                              = True
 1706     restricted (VarBind { var_id = v })                  = no_sig v
 1707     restricted (FunBind { fun_id = v, fun_matches = m }) = restricted_match m
 1708                                                            && no_sig (unLoc v)
 1709     restricted b = pprPanic "isRestrictedGroup/unrestricted" (ppr b)
 1710 
 1711     restricted_match mg = matchGroupArity mg == 0
 1712         -- No args => like a pattern binding
 1713         -- Some args => a function binding
 1714 
 1715     no_sig n = not (hasCompleteSig sig_fn n)
 1716 
 1717 isClosedBndrGroup :: TcTypeEnv -> Bag (LHsBind GhcRn) -> IsGroupClosed
 1718 isClosedBndrGroup type_env binds
 1719   = IsGroupClosed fv_env type_closed
 1720   where
 1721     type_closed = allUFM (nameSetAll is_closed_type_id) fv_env
 1722 
 1723     fv_env :: NameEnv NameSet
 1724     fv_env = mkNameEnv $ concatMap (bindFvs . unLoc) binds
 1725 
 1726     bindFvs :: HsBindLR GhcRn GhcRn -> [(Name, NameSet)]
 1727     bindFvs (FunBind { fun_id = L _ f
 1728                      , fun_ext = fvs })
 1729        = let open_fvs = get_open_fvs fvs
 1730          in [(f, open_fvs)]
 1731     bindFvs (PatBind { pat_lhs = pat, pat_ext = fvs })
 1732        = let open_fvs = get_open_fvs fvs
 1733          in [(b, open_fvs) | b <- collectPatBinders CollNoDictBinders pat]
 1734     bindFvs _
 1735        = []
 1736 
 1737     get_open_fvs fvs = filterNameSet (not . is_closed) fvs
 1738 
 1739     is_closed :: Name -> ClosedTypeId
 1740     is_closed name
 1741       | Just thing <- lookupNameEnv type_env name
 1742       = case thing of
 1743           AGlobal {}                     -> True
 1744           ATcId { tct_info = ClosedLet } -> True
 1745           _                              -> False
 1746 
 1747       | otherwise
 1748       = True  -- The free-var set for a top level binding mentions
 1749 
 1750 
 1751     is_closed_type_id :: Name -> Bool
 1752     -- We're already removed Global and ClosedLet Ids
 1753     is_closed_type_id name
 1754       | Just thing <- lookupNameEnv type_env name
 1755       = case thing of
 1756           ATcId { tct_info = NonClosedLet _ cl } -> cl
 1757           ATcId { tct_info = NotLetBound }       -> False
 1758           ATyVar {}                              -> False
 1759                -- In-scope type variables are not closed!
 1760           _ -> pprPanic "is_closed_id" (ppr name)
 1761 
 1762       | otherwise
 1763       = True   -- The free-var set for a top level binding mentions
 1764                -- imported things too, so that we can report unused imports
 1765                -- These won't be in the local type env.
 1766                -- Ditto class method etc from the current module
 1767 
 1768 
 1769 {- *********************************************************************
 1770 *                                                                      *
 1771                Error contexts and messages
 1772 *                                                                      *
 1773 ********************************************************************* -}
 1774 
 1775 -- This one is called on LHS, when pat and grhss are both Name
 1776 -- and on RHS, when pat is TcId and grhss is still Name
 1777 patMonoBindsCtxt :: (OutputableBndrId p)
 1778                  => LPat (GhcPass p) -> GRHSs GhcRn (LHsExpr GhcRn) -> SDoc
 1779 patMonoBindsCtxt pat grhss
 1780   = hang (text "In a pattern binding:") 2 (pprPatBind pat grhss)