compiler/typecheck/TcBinds.hs

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