ghc/compiler/typecheck/TcBinds.lhs

   1 %
   2 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   3 %
   4 \section[TcBinds]{TcBinds}
   5
   6 \begin{code}
   7 module TcBinds ( tcBindsAndThen, tcTopBinds, tcMonoBinds, tcSpecSigs ) where
   8
   9 #include "HsVersions.h"
  10
  11 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
  12 import {-# SOURCE #-} TcExpr  ( tcCheckSigma, tcCheckRho )
  13
  14 import CmdLineOpts      ( DynFlag(Opt_NoMonomorphismRestriction) )
  15 import HsSyn            ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..),
  16                           Match(..), mkMonoBind,
  17                           collectMonoBinders, andMonoBinds,
  18                           collectSigTysFromMonoBinds
  19                         )
  20 import RnHsSyn          ( RenamedHsBinds, RenamedSig, RenamedMonoBinds )
  21 import TcHsSyn          ( TcHsBinds, TcMonoBinds, TcId, zonkId, mkHsLet )
  22
  23 import TcRnMonad
  24 import Inst             ( InstOrigin(..), newDicts, newIPDict, instToId )
  25 import TcEnv            ( tcExtendLocalValEnv, tcExtendLocalValEnv2, newLocalName )
  26 import TcUnify          ( Expected(..), newHole, unifyTauTyLists, checkSigTyVarsWrt, sigCtxt )
  27 import TcSimplify       ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted,
  28                           tcSimplifyToDicts, tcSimplifyIPs )
  29 import TcHsType         ( tcHsSigType, UserTypeCtxt(..), TcSigInfo(..),
  30                           tcTySig, maybeSig, tcSigPolyId, tcSigMonoId, tcAddScopedTyVars
  31                         )
  32 import TcPat            ( tcPat, tcSubPat, tcMonoPatBndr )
  33 import TcSimplify       ( bindInstsOfLocalFuns )
  34 import TcMType          ( newTyVar, newTyVarTy, zonkTcTyVarToTyVar )
  35 import TcType           ( TcTyVar, mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType,
  36                           mkPredTy, mkForAllTy, isUnLiftedType,
  37                           unliftedTypeKind, liftedTypeKind, openTypeKind, eqKind
  38                         )
  39
  40 import CoreFVs          ( idFreeTyVars )
  41 import Id               ( mkLocalId, mkSpecPragmaId, setInlinePragma )
  42 import Var              ( idType, idName )
  43 import Name             ( Name, getSrcLoc )
  44 import NameSet
  45 import Var              ( tyVarKind )
  46 import VarSet
  47 import Bag
  48 import Util             ( isIn, equalLength )
  49 import BasicTypes       ( TopLevelFlag(..), RecFlag(..), isNonRec, isRec,
  50                           isNotTopLevel, isAlwaysActive )
  51 import FiniteMap        ( listToFM, lookupFM )
  52 import Outputable
  53 \end{code}
  54
  55
  56 %************************************************************************
  57 %*                                                                      *
  58 \subsection{Type-checking bindings}
  59 %*                                                                      *
  60 %************************************************************************
  61
  62 @tcBindsAndThen@ typechecks a @HsBinds@.  The "and then" part is because
  63 it needs to know something about the {\em usage} of the things bound,
  64 so that it can create specialisations of them.  So @tcBindsAndThen@
  65 takes a function which, given an extended environment, E, typechecks
  66 the scope of the bindings returning a typechecked thing and (most
  67 important) an LIE.  It is this LIE which is then used as the basis for
  68 specialising the things bound.
  69
  70 @tcBindsAndThen@ also takes a "combiner" which glues together the
  71 bindings and the "thing" to make a new "thing".
  72
  73 The real work is done by @tcBindWithSigsAndThen@.
  74
  75 Recursive and non-recursive binds are handled in essentially the same
  76 way: because of uniques there are no scoping issues left.  The only
  77 difference is that non-recursive bindings can bind primitive values.
  78
  79 Even for non-recursive binding groups we add typings for each binder
  80 to the LVE for the following reason.  When each individual binding is
  81 checked the type of its LHS is unified with that of its RHS; and
  82 type-checking the LHS of course requires that the binder is in scope.
  83
  84 At the top-level the LIE is sure to contain nothing but constant
  85 dictionaries, which we resolve at the module level.
  86
  87 \begin{code}
  88 tcTopBinds :: RenamedHsBinds -> TcM (TcMonoBinds, TcLclEnv)
  89         -- Note: returning the TcLclEnv is more than we really
  90         --       want.  The bit we care about is the local bindings
  91         --       and the free type variables thereof
  92 tcTopBinds binds
  93   = tc_binds_and_then TopLevel glue binds       $
  94     getLclEnv                                   `thenM` \ env ->
  95     returnM (EmptyMonoBinds, env)
  96   where
  97         -- The top level bindings are flattened into a giant
  98         -- implicitly-mutually-recursive MonoBinds
  99     glue binds1 (binds2, env) = (flatten binds1 `AndMonoBinds` binds2, env)
 100     flatten EmptyBinds          = EmptyMonoBinds
 101     flatten (b1 `ThenBinds` b2) = flatten b1 `AndMonoBinds` flatten b2
 102     flatten (MonoBind b _ _)    = b
 103         -- Can't have a IPBinds at top level
 104
 105
 106 tcBindsAndThen
 107         :: (TcHsBinds -> thing -> thing)                -- Combinator
 108         -> RenamedHsBinds
 109         -> TcM thing
 110         -> TcM thing
 111
 112 tcBindsAndThen = tc_binds_and_then NotTopLevel
 113
 114 tc_binds_and_then top_lvl combiner EmptyBinds do_next
 115   = do_next
 116 tc_binds_and_then top_lvl combiner (MonoBind EmptyMonoBinds sigs is_rec) do_next
 117   = do_next
 118
 119 tc_binds_and_then top_lvl combiner (ThenBinds b1 b2) do_next
 120   = tc_binds_and_then top_lvl combiner b1       $
 121     tc_binds_and_then top_lvl combiner b2       $
 122     do_next
 123
 124 tc_binds_and_then top_lvl combiner (IPBinds binds) do_next
 125   = getLIE do_next                      `thenM` \ (result, expr_lie) ->
 126     mapAndUnzipM tc_ip_bind binds       `thenM` \ (avail_ips, binds') ->
 127
 128         -- If the binding binds ?x = E, we  must now
 129         -- discharge any ?x constraints in expr_lie
 130     tcSimplifyIPs avail_ips expr_lie    `thenM` \ dict_binds ->
 131
 132     returnM (combiner (IPBinds binds') $
 133              combiner (mkMonoBind Recursive dict_binds) result)
 134   where
 135         -- I wonder if we should do these one at at time
 136         -- Consider     ?x = 4
 137         --              ?y = ?x + 1
 138     tc_ip_bind (ip, expr)
 139       = newTyVarTy openTypeKind         `thenM` \ ty ->
 140         getSrcLocM                      `thenM` \ loc ->
 141         newIPDict (IPBind ip) ip ty     `thenM` \ (ip', ip_inst) ->
 142         tcCheckRho expr ty              `thenM` \ expr' ->
 143         returnM (ip_inst, (ip', expr'))
 144
 145 tc_binds_and_then top_lvl combiner (MonoBind bind sigs is_rec) do_next
 146   =     -- BRING ANY SCOPED TYPE VARIABLES INTO SCOPE
 147         -- Notice that they scope over
 148         --      a) the type signatures in the binding group
 149         --      b) the bindings in the group
 150         --      c) the scope of the binding group (the "in" part)
 151       tcAddScopedTyVars (collectSigTysFromMonoBinds bind)       $
 152
 153       tcBindWithSigs top_lvl bind sigs is_rec   `thenM` \ (poly_binds, poly_ids) ->
 154
 155       case top_lvl of
 156         TopLevel        -- For the top level don't bother will all this
 157                         --  bindInstsOfLocalFuns stuff. All the top level
 158                         -- things are rec'd together anyway, so it's fine to
 159                         -- leave them to the tcSimplifyTop, and quite a bit faster too
 160                         --
 161                         -- Subtle (and ugly) point: furthermore at top level we
 162                         -- return the TcLclEnv, which contains the LIE var; we
 163                         -- don't want to return the wrong one!
 164                 -> tc_body poly_ids                     `thenM` \ (prag_binds, thing) ->
 165                    returnM (combiner (mkMonoBind Recursive (poly_binds `andMonoBinds` prag_binds))
 166                                      thing)
 167
 168         NotTopLevel     -- For nested bindings we must do teh bindInstsOfLocalFuns thing
 169                 -> getLIE (tc_body poly_ids)            `thenM` \ ((prag_binds, thing), lie) ->
 170
 171                         -- Create specialisations of functions bound here
 172                     bindInstsOfLocalFuns lie poly_ids   `thenM` \ lie_binds ->
 173
 174                         -- We want to keep non-recursive things non-recursive
 175                         -- so that we desugar unlifted bindings correctly
 176                    if isRec is_rec then
 177                      returnM (
 178                         combiner (mkMonoBind Recursive (
 179                                 poly_binds `andMonoBinds`
 180                                 lie_binds  `andMonoBinds`
 181                                 prag_binds)) thing
 182                      )
 183                    else
 184                      returnM (
 185                         combiner (mkMonoBind NonRecursive poly_binds) $
 186                         combiner (mkMonoBind NonRecursive prag_binds) $
 187                         combiner (mkMonoBind Recursive lie_binds)     $
 188                                 -- NB: the binds returned by tcSimplify and bindInstsOfLocalFuns
 189                                 -- aren't guaranteed in dependency order (though we could change
 190                                 -- that); hence the Recursive marker.
 191                         thing)
 192   where
 193     tc_body poly_ids    -- Type check the pragmas and "thing inside"
 194       =   -- Extend the environment to bind the new polymorphic Ids
 195           tcExtendLocalValEnv poly_ids  $
 196
 197           -- Build bindings and IdInfos corresponding to user pragmas
 198           tcSpecSigs sigs               `thenM` \ prag_binds ->
 199
 200           -- Now do whatever happens next, in the augmented envt
 201           do_next                       `thenM` \ thing ->
 202
 203           returnM (prag_binds, thing)
 204 \end{code}
 205
 206
 207 %************************************************************************
 208 %*                                                                      *
 209 \subsection{tcBindWithSigs}
 210 %*                                                                      *
 211 %************************************************************************
 212
 213 @tcBindWithSigs@ deals with a single binding group.  It does generalisation,
 214 so all the clever stuff is in here.
 215
 216 * binder_names and mbind must define the same set of Names
 217
 218 * The Names in tc_ty_sigs must be a subset of binder_names
 219
 220 * The Ids in tc_ty_sigs don't necessarily have to have the same name
 221   as the Name in the tc_ty_sig
 222
 223 \begin{code}
 224 tcBindWithSigs  :: TopLevelFlag
 225                 -> RenamedMonoBinds
 226                 -> [RenamedSig]
 227                 -> RecFlag
 228                 -> TcM (TcMonoBinds, [TcId])
 229
 230 tcBindWithSigs top_lvl mbind sigs is_rec
 231   =     -- TYPECHECK THE SIGNATURES
 232      recoverM (returnM []) (
 233         mappM tcTySig [sig | sig@(Sig name _ _) <- sigs]
 234      )                                          `thenM` \ tc_ty_sigs ->
 235
 236         -- SET UP THE MAIN RECOVERY; take advantage of any type sigs
 237    recoverM (
 238         -- If typechecking the binds fails, then return with each
 239         -- signature-less binder given type (forall a.a), to minimise subsequent
 240         -- error messages
 241         newTyVar liftedTypeKind         `thenM` \ alpha_tv ->
 242         let
 243           forall_a_a    = mkForAllTy alpha_tv (mkTyVarTy alpha_tv)
 244           binder_names  = collectMonoBinders mbind
 245           poly_ids      = map mk_dummy binder_names
 246           mk_dummy name = case maybeSig tc_ty_sigs name of
 247                             Just sig -> tcSigPolyId sig                 -- Signature
 248                             Nothing  -> mkLocalId name forall_a_a       -- No signature
 249         in
 250         traceTc (text "tcBindsWithSigs: error recovery" <+> ppr binder_names)   `thenM_`
 251         returnM (EmptyMonoBinds, poly_ids)
 252     )                                           $
 253
 254         -- TYPECHECK THE BINDINGS
 255     traceTc (ptext SLIT("--------------------------------------------------------"))    `thenM_`
 256     traceTc (ptext SLIT("Bindings for") <+> ppr (collectMonoBinders mbind))             `thenM_`
 257     getLIE (tcMonoBinds mbind tc_ty_sigs is_rec)        `thenM` \ ((mbind', bndr_names_w_ids), lie_req) ->
 258     let
 259         (binder_names, mono_ids) = unzip (bagToList bndr_names_w_ids)
 260         tau_tvs = foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids
 261     in
 262
 263         -- GENERALISE
 264         --      (it seems a bit crude to have to do getLIE twice,
 265         --       but I can't see a better way just now)
 266     addSrcLoc  (minimum (map getSrcLoc binder_names))           $
 267     addErrCtxt (genCtxt binder_names)                           $
 268     getLIE (generalise binder_names mbind tau_tvs lie_req tc_ty_sigs)
 269                         `thenM` \ ((tc_tyvars_to_gen, dict_binds, dict_ids), lie_free) ->
 270
 271
 272         -- ZONK THE GENERALISED TYPE VARIABLES TO REAL TyVars
 273         -- This commits any unbound kind variables to boxed kind, by unification
 274         -- It's important that the final quanfified type variables
 275         -- are fully zonked, *including boxity*, because they'll be
 276         -- included in the forall types of the polymorphic Ids.
 277         -- At calls of these Ids we'll instantiate fresh type variables from
 278         -- them, and we use their boxity then.
 279     mappM zonkTcTyVarToTyVar tc_tyvars_to_gen   `thenM` \ real_tyvars_to_gen ->
 280
 281         -- ZONK THE Ids
 282         -- It's important that the dict Ids are zonked, including the boxity set
 283         -- in the previous step, because they are later used to form the type of
 284         -- the polymorphic thing, and forall-types must be zonked so far as
 285         -- their bound variables are concerned
 286     mappM zonkId dict_ids                               `thenM` \ zonked_dict_ids ->
 287     mappM zonkId mono_ids                               `thenM` \ zonked_mono_ids ->
 288
 289         -- BUILD THE POLYMORPHIC RESULT IDs
 290     let
 291         exports  = zipWith mk_export binder_names zonked_mono_ids
 292         poly_ids = [poly_id | (_, poly_id, _) <- exports]
 293         dict_tys = map idType zonked_dict_ids
 294
 295         inlines    = mkNameSet [name | InlineSig True name _ loc <- sigs]
 296                         -- Any INLINE sig (regardless of phase control)
 297                         -- makes the RHS look small
 298         inline_phases = listToFM [(name, phase) | InlineSig _ name phase _ <- sigs,
 299                                                   not (isAlwaysActive phase)]
 300                         -- Set the IdInfo field to control the inline phase
 301                         -- AlwaysActive is the default, so don't bother with them
 302
 303         mk_export binder_name zonked_mono_id
 304           = (tyvars,
 305              attachInlinePhase inline_phases poly_id,
 306              zonked_mono_id)
 307           where
 308             (tyvars, poly_id) =
 309                 case maybeSig tc_ty_sigs binder_name of
 310                   Just (TySigInfo sig_poly_id sig_tyvars _ _ _ _ _) ->
 311                         (sig_tyvars, sig_poly_id)
 312                   Nothing -> (real_tyvars_to_gen, new_poly_id)
 313
 314             new_poly_id = mkLocalId binder_name poly_ty
 315             poly_ty = mkForAllTys real_tyvars_to_gen
 316                     $ mkFunTys dict_tys
 317                     $ idType zonked_mono_id
 318                 -- It's important to build a fully-zonked poly_ty, because
 319                 -- we'll slurp out its free type variables when extending the
 320                 -- local environment (tcExtendLocalValEnv); if it's not zonked
 321                 -- it appears to have free tyvars that aren't actually free
 322                 -- at all.
 323     in
 324
 325     traceTc (text "binding:" <+> ppr ((zonked_dict_ids, dict_binds),
 326                                       exports, map idType poly_ids)) `thenM_`
 327
 328         -- Check for an unlifted, non-overloaded group
 329         -- In that case we must make extra checks
 330     if any (isUnLiftedType . idType) zonked_mono_ids && null zonked_dict_ids
 331     then        -- Some bindings are unlifted
 332         checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind      `thenM_`
 333
 334         extendLIEs lie_req                      `thenM_`
 335         returnM (
 336             AbsBinds [] [] exports inlines mbind',
 337                 -- Do not generate even any x=y bindings
 338             poly_ids
 339         )
 340
 341     else        -- The normal case
 342     extendLIEs lie_free                         `thenM_`
 343     returnM (
 344         AbsBinds real_tyvars_to_gen
 345                  zonked_dict_ids
 346                  exports
 347                  inlines
 348                  (dict_binds `andMonoBinds` mbind'),
 349         poly_ids
 350     )
 351
 352 attachInlinePhase inline_phases bndr
 353   = case lookupFM inline_phases (idName bndr) of
 354         Just prag -> bndr `setInlinePragma` prag
 355         Nothing   -> bndr
 356
 357 -- Check that non-overloaded unlifted bindings are
 358 --      a) non-recursive,
 359 --      b) not top level,
 360 --      c) non-polymorphic
 361 --      d) not a multiple-binding group (more or less implied by (a))
 362
 363 checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind
 364   = ASSERT( not (any ((eqKind unliftedTypeKind) . tyVarKind) real_tyvars_to_gen) )
 365                 -- The instCantBeGeneralised stuff in tcSimplify should have
 366                 -- already raised an error if we're trying to generalise an
 367                 -- unboxed tyvar (NB: unboxed tyvars are always introduced
 368                 -- along with a class constraint) and it's better done there
 369                 -- because we have more precise origin information.
 370                 -- That's why we just use an ASSERT here.
 371
 372     checkTc (isNotTopLevel top_lvl)
 373             (unliftedBindErr "Top-level" mbind)         `thenM_`
 374     checkTc (isNonRec is_rec)
 375             (unliftedBindErr "Recursive" mbind)         `thenM_`
 376     checkTc (single_bind mbind)
 377             (unliftedBindErr "Multiple" mbind)          `thenM_`
 378     checkTc (null real_tyvars_to_gen)
 379             (unliftedBindErr "Polymorphic" mbind)
 380
 381   where
 382     single_bind (PatMonoBind _ _ _)   = True
 383     single_bind (FunMonoBind _ _ _ _) = True
 384     single_bind other                 = False
 385 \end{code}
 386
 387
 388 Polymorphic recursion
 389 ~~~~~~~~~~~~~~~~~~~~~
 390 The game plan for polymorphic recursion in the code above is
 391
 392         * Bind any variable for which we have a type signature
 393           to an Id with a polymorphic type.  Then when type-checking
 394           the RHSs we'll make a full polymorphic call.
 395
 396 This fine, but if you aren't a bit careful you end up with a horrendous
 397 amount of partial application and (worse) a huge space leak. For example:
 398
 399         f :: Eq a => [a] -> [a]
 400         f xs = ...f...
 401
 402 If we don't take care, after typechecking we get
 403
 404         f = /\a -> \d::Eq a -> let f' = f a d
 405                                in
 406                                \ys:[a] -> ...f'...
 407
 408 Notice the the stupid construction of (f a d), which is of course
 409 identical to the function we're executing.  In this case, the
 410 polymorphic recursion isn't being used (but that's a very common case).
 411 We'd prefer
 412
 413         f = /\a -> \d::Eq a -> letrec
 414                                  fm = \ys:[a] -> ...fm...
 415                                in
 416                                fm
 417
 418 This can lead to a massive space leak, from the following top-level defn
 419 (post-typechecking)
 420
 421         ff :: [Int] -> [Int]
 422         ff = f Int dEqInt
 423
 424 Now (f dEqInt) evaluates to a lambda that has f' as a free variable; but
 425 f' is another thunk which evaluates to the same thing... and you end
 426 up with a chain of identical values all hung onto by the CAF ff.
 427
 428         ff = f Int dEqInt
 429
 430            = let f' = f Int dEqInt in \ys. ...f'...
 431
 432            = let f' = let f' = f Int dEqInt in \ys. ...f'...
 433                       in \ys. ...f'...
 434
 435 Etc.
 436 Solution: when typechecking the RHSs we always have in hand the
 437 *monomorphic* Ids for each binding.  So we just need to make sure that
 438 if (Method f a d) shows up in the constraints emerging from (...f...)
 439 we just use the monomorphic Id.  We achieve this by adding monomorphic Ids
 440 to the "givens" when simplifying constraints.  That's what the "lies_avail"
 441 is doing.
 442
 443
 444 %************************************************************************
 445 %*                                                                      *
 446 \subsection{getTyVarsToGen}
 447 %*                                                                      *
 448 %************************************************************************
 449
 450 \begin{code}
 451 generalise binder_names mbind tau_tvs lie_req sigs =
 452
 453   -- check for -fno-monomorphism-restriction
 454   doptM Opt_NoMonomorphismRestriction           `thenM` \ no_MR ->
 455   let is_unrestricted | no_MR     = True
 456                       | otherwise = isUnRestrictedGroup tysig_names mbind
 457   in
 458
 459   if not is_unrestricted then   -- RESTRICTED CASE
 460         -- Check signature contexts are empty
 461     checkTc (all is_mono_sig sigs)
 462             (restrictedBindCtxtErr binder_names)        `thenM_`
 463
 464         -- Now simplify with exactly that set of tyvars
 465         -- We have to squash those Methods
 466     tcSimplifyRestricted doc tau_tvs lie_req            `thenM` \ (qtvs, binds) ->
 467
 468         -- Check that signature type variables are OK
 469     checkSigsTyVars qtvs sigs                           `thenM` \ final_qtvs ->
 470
 471     returnM (final_qtvs, binds, [])
 472
 473   else if null sigs then        -- UNRESTRICTED CASE, NO TYPE SIGS
 474     tcSimplifyInfer doc tau_tvs lie_req
 475
 476   else                          -- UNRESTRICTED CASE, WITH TYPE SIGS
 477         -- CHECKING CASE: Unrestricted group, there are type signatures
 478         -- Check signature contexts are identical
 479     checkSigsCtxts sigs                 `thenM` \ (sig_avails, sig_dicts) ->
 480
 481         -- Check that the needed dicts can be
 482         -- expressed in terms of the signature ones
 483     tcSimplifyInferCheck doc tau_tvs sig_avails lie_req `thenM` \ (forall_tvs, dict_binds) ->
 484
 485         -- Check that signature type variables are OK
 486     checkSigsTyVars forall_tvs sigs                     `thenM` \ final_qtvs ->
 487
 488     returnM (final_qtvs, dict_binds, sig_dicts)
 489
 490   where
 491     tysig_names = map (idName . tcSigPolyId) sigs
 492     is_mono_sig (TySigInfo _ _ theta _ _ _ _) = null theta
 493
 494     doc = ptext SLIT("type signature(s) for") <+> pprBinders binder_names
 495
 496 -----------------------
 497         -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
 498         -- The type signatures on a mutually-recursive group of definitions
 499         -- must all have the same context (or none).
 500         --
 501         -- We unify them because, with polymorphic recursion, their types
 502         -- might not otherwise be related.  This is a rather subtle issue.
 503         -- ToDo: amplify
 504 checkSigsCtxts sigs@(TySigInfo id1 sig_tvs theta1 _ _ _ src_loc : other_sigs)
 505   = addSrcLoc src_loc                   $
 506     mappM_ check_one other_sigs         `thenM_`
 507     if null theta1 then
 508         returnM ([], [])                -- Non-overloaded type signatures
 509     else
 510     newDicts SignatureOrigin theta1     `thenM` \ sig_dicts ->
 511     let
 512         -- The "sig_avails" is the stuff available.  We get that from
 513         -- the context of the type signature, BUT ALSO the lie_avail
 514         -- so that polymorphic recursion works right (see comments at end of fn)
 515         sig_avails = sig_dicts ++ sig_meths
 516     in
 517     returnM (sig_avails, map instToId sig_dicts)
 518   where
 519     sig1_dict_tys = map mkPredTy theta1
 520     sig_meths     = concat [insts | TySigInfo _ _ _ _ _ insts _ <- sigs]
 521
 522     check_one sig@(TySigInfo id _ theta _ _ _ _)
 523        = addErrCtxt (sigContextsCtxt id1 id)                    $
 524          checkTc (equalLength theta theta1) sigContextsErr      `thenM_`
 525          unifyTauTyLists sig1_dict_tys (map mkPredTy theta)
 526
 527 checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
 528 checkSigsTyVars qtvs sigs
 529   = mappM check_one sigs        `thenM` \ sig_tvs_s ->
 530     let
 531         -- Sigh.  Make sure that all the tyvars in the type sigs
 532         -- appear in the returned ty var list, which is what we are
 533         -- going to generalise over.  Reason: we occasionally get
 534         -- silly types like
 535         --      type T a = () -> ()
 536         --      f :: T a
 537         --      f () = ()
 538         -- Here, 'a' won't appear in qtvs, so we have to add it
 539
 540         sig_tvs = foldr (unionVarSet . mkVarSet) emptyVarSet sig_tvs_s
 541         all_tvs = mkVarSet qtvs `unionVarSet` sig_tvs
 542     in
 543     returnM (varSetElems all_tvs)
 544   where
 545     check_one (TySigInfo id sig_tyvars sig_theta sig_tau _ _ src_loc)
 546       = addSrcLoc src_loc                                               $
 547         addErrCtxt (ptext SLIT("When checking the type signature for")
 548                       <+> quotes (ppr id))                              $
 549         addErrCtxtM (sigCtxt id sig_tyvars sig_theta sig_tau)           $
 550         checkSigTyVarsWrt (idFreeTyVars id) sig_tyvars
 551 \end{code}
 552
 553 @getTyVarsToGen@ decides what type variables to generalise over.
 554
 555 For a "restricted group" -- see the monomorphism restriction
 556 for a definition -- we bind no dictionaries, and
 557 remove from tyvars_to_gen any constrained type variables
 558
 559 *Don't* simplify dicts at this point, because we aren't going
 560 to generalise over these dicts.  By the time we do simplify them
 561 we may well know more.  For example (this actually came up)
 562         f :: Array Int Int
 563         f x = array ... xs where xs = [1,2,3,4,5]
 564 We don't want to generate lots of (fromInt Int 1), (fromInt Int 2)
 565 stuff.  If we simplify only at the f-binding (not the xs-binding)
 566 we'll know that the literals are all Ints, and we can just produce
 567 Int literals!
 568
 569 Find all the type variables involved in overloading, the
 570 "constrained_tyvars".  These are the ones we *aren't* going to
 571 generalise.  We must be careful about doing this:
 572
 573  (a) If we fail to generalise a tyvar which is not actually
 574         constrained, then it will never, ever get bound, and lands
 575         up printed out in interface files!  Notorious example:
 576                 instance Eq a => Eq (Foo a b) where ..
 577         Here, b is not constrained, even though it looks as if it is.
 578         Another, more common, example is when there's a Method inst in
 579         the LIE, whose type might very well involve non-overloaded
 580         type variables.
 581   [NOTE: Jan 2001: I don't understand the problem here so I'm doing
 582         the simple thing instead]
 583
 584  (b) On the other hand, we mustn't generalise tyvars which are constrained,
 585         because we are going to pass on out the unmodified LIE, with those
 586         tyvars in it.  They won't be in scope if we've generalised them.
 587
 588 So we are careful, and do a complete simplification just to find the
 589 constrained tyvars. We don't use any of the results, except to
 590 find which tyvars are constrained.
 591
 592 \begin{code}
 593 isUnRestrictedGroup :: [Name]           -- Signatures given for these
 594                     -> RenamedMonoBinds
 595                     -> Bool
 596
 597 is_elem v vs = isIn "isUnResMono" v vs
 598
 599 isUnRestrictedGroup sigs (PatMonoBind other        _ _) = False
 600 isUnRestrictedGroup sigs (VarMonoBind v _)              = v `is_elem` sigs
 601 isUnRestrictedGroup sigs (FunMonoBind v _ matches _)    = isUnRestrictedMatch matches ||
 602                                                           v `is_elem` sigs
 603 isUnRestrictedGroup sigs (AndMonoBinds mb1 mb2)         = isUnRestrictedGroup sigs mb1 &&
 604                                                           isUnRestrictedGroup sigs mb2
 605 isUnRestrictedGroup sigs EmptyMonoBinds                 = True
 606
 607 isUnRestrictedMatch (Match [] _ _ : _) = False  -- No args => like a pattern binding
 608 isUnRestrictedMatch other              = True   -- Some args => a function binding
 609 \end{code}
 610
 611
 612 %************************************************************************
 613 %*                                                                      *
 614 \subsection{tcMonoBind}
 615 %*                                                                      *
 616 %************************************************************************
 617
 618 @tcMonoBinds@ deals with a single @MonoBind@.
 619 The signatures have been dealt with already.
 620
 621 \begin{code}
 622 tcMonoBinds :: RenamedMonoBinds
 623             -> [TcSigInfo] -> RecFlag
 624             -> TcM (TcMonoBinds,
 625                     Bag (Name,          -- Bound names
 626                          TcId))         -- Corresponding monomorphic bound things
 627
 628 tcMonoBinds mbinds tc_ty_sigs is_rec
 629         -- Three stages:
 630         -- 1. Check the patterns, building up an environment binding
 631         --    the variables in this group (in the recursive case)
 632         -- 2. Extend the environment
 633         -- 3. Check the RHSs
 634   = tc_mb_pats mbinds           `thenM` \ (complete_it, xve) ->
 635     tcExtendLocalValEnv2 (bagToList xve) complete_it
 636   where
 637     tc_mb_pats EmptyMonoBinds
 638       = returnM (returnM (EmptyMonoBinds, emptyBag), emptyBag)
 639
 640     tc_mb_pats (AndMonoBinds mb1 mb2)
 641       = tc_mb_pats mb1          `thenM` \ (complete_it1, xve1) ->
 642         tc_mb_pats mb2          `thenM` \ (complete_it2, xve2) ->
 643         let
 644            complete_it = complete_it1   `thenM` \ (mb1', bs1) ->
 645                          complete_it2   `thenM` \ (mb2', bs2) ->
 646                          returnM (AndMonoBinds mb1' mb2', bs1 `unionBags` bs2)
 647         in
 648         returnM (complete_it, xve1 `unionBags` xve2)
 649
 650     tc_mb_pats (FunMonoBind name inf matches locn)
 651                 -- Three cases:
 652                 --      a) Type sig supplied
 653                 --      b) No type sig and recursive
 654                 --      c) No type sig and non-recursive
 655
 656       | Just sig <- maybeSig tc_ty_sigs name
 657       = let     -- (a) There is a type signature
 658                 -- Use it for the environment extension, and check
 659                 -- the RHS has the appropriate type (with outer for-alls stripped off)
 660            mono_id = tcSigMonoId sig
 661            mono_ty = idType mono_id
 662            complete_it = addSrcLoc locn                                 $
 663                          tcMatchesFun name matches (Check mono_ty)      `thenM` \ matches' ->
 664                          returnM (FunMonoBind mono_id inf matches' locn,
 665                                   unitBag (name, mono_id))
 666         in
 667         returnM (complete_it, if isRec is_rec then unitBag (name,tcSigPolyId sig)
 668                                               else emptyBag)
 669
 670       | isRec is_rec
 671       =         -- (b) No type signature, and recursive
 672                 -- So we must use an ordinary H-M type variable
 673                 -- which means the variable gets an inferred tau-type
 674         newLocalName name               `thenM` \ mono_name ->
 675         newTyVarTy openTypeKind         `thenM` \ mono_ty ->
 676         let
 677            mono_id     = mkLocalId mono_name mono_ty
 678            complete_it = addSrcLoc locn                                 $
 679                          tcMatchesFun name matches (Check mono_ty)      `thenM` \ matches' ->
 680                          returnM (FunMonoBind mono_id inf matches' locn,
 681                                   unitBag (name, mono_id))
 682         in
 683         returnM (complete_it, unitBag (name, mono_id))
 684
 685       | otherwise       -- (c) No type signature, and non-recursive
 686       = let             -- So we can use a 'hole' type to infer a higher-rank type
 687            complete_it
 688                 = addSrcLoc locn                                $
 689                   newHole                                       `thenM` \ hole ->
 690                   tcMatchesFun name matches (Infer hole)        `thenM` \ matches' ->
 691                   readMutVar hole                               `thenM` \ fun_ty ->
 692                   newLocalName name                             `thenM` \ mono_name ->
 693                   let
 694                      mono_id = mkLocalId mono_name fun_ty
 695                   in
 696                   returnM (FunMonoBind mono_id inf matches' locn,
 697                            unitBag (name, mono_id))
 698         in
 699         returnM (complete_it, emptyBag)
 700
 701     tc_mb_pats bind@(PatMonoBind pat grhss locn)
 702       = addSrcLoc locn          $
 703
 704                 --      Now typecheck the pattern
 705                 -- We do now support binding fresh (not-already-in-scope) scoped
 706                 -- type variables in the pattern of a pattern binding.
 707                 -- For example, this is now legal:
 708                 --      (x::a, y::b) = e
 709                 -- The type variables are brought into scope in tc_binds_and_then,
 710                 -- so we don't have to do anything here.
 711
 712         newHole                                 `thenM` \ hole ->
 713         tcPat tc_pat_bndr pat (Infer hole)      `thenM` \ (pat', tvs, ids, lie_avail) ->
 714         readMutVar hole                         `thenM` \ pat_ty ->
 715
 716         -- Don't know how to deal with pattern-bound existentials yet
 717         checkTc (isEmptyBag tvs && null lie_avail)
 718                 (existentialExplode bind)       `thenM_`
 719
 720         let
 721            complete_it = addSrcLoc locn                                 $
 722                          addErrCtxt (patMonoBindsCtxt bind)             $
 723                          tcGRHSsPat grhss (Check pat_ty)        `thenM` \ grhss' ->
 724                          returnM (PatMonoBind pat' grhss' locn, ids)
 725         in
 726         returnM (complete_it, if isRec is_rec then ids else emptyBag)
 727
 728         -- tc_pat_bndr is used when dealing with a LHS binder in a pattern.
 729         -- If there was a type sig for that Id, we want to make it much
 730         -- as if that type signature had been on the binder as a SigPatIn.
 731         -- We check for a type signature; if there is one, we use the mono_id
 732         -- from the signature.  This is how we make sure the tau part of the
 733         -- signature actually matches the type of the LHS; then tc_mb_pats
 734         -- ensures the LHS and RHS have the same type
 735
 736     tc_pat_bndr name pat_ty
 737         = case maybeSig tc_ty_sigs name of
 738             Nothing  -> newLocalName name                       `thenM` \ bndr_name ->
 739                         tcMonoPatBndr bndr_name pat_ty
 740
 741             Just sig -> addSrcLoc (getSrcLoc name)              $
 742                         tcSubPat (idType mono_id) pat_ty        `thenM` \ co_fn ->
 743                         returnM (co_fn, mono_id)
 744                      where
 745                         mono_id = tcSigMonoId sig
 746 \end{code}
 747
 748
 749 %************************************************************************
 750 %*                                                                      *
 751 \subsection{SPECIALIZE pragmas}
 752 %*                                                                      *
 753 %************************************************************************
 754
 755 @tcSpecSigs@ munches up the specialisation "signatures" that arise through *user*
 756 pragmas.  It is convenient for them to appear in the @[RenamedSig]@
 757 part of a binding because then the same machinery can be used for
 758 moving them into place as is done for type signatures.
 759
 760 They look like this:
 761
 762 \begin{verbatim}
 763         f :: Ord a => [a] -> b -> b
 764         {-# SPECIALIZE f :: [Int] -> b -> b #-}
 765 \end{verbatim}
 766
 767 For this we generate:
 768 \begin{verbatim}
 769         f* = /\ b -> let d1 = ...
 770                      in f Int b d1
 771 \end{verbatim}
 772
 773 where f* is a SpecPragmaId.  The **sole** purpose of SpecPragmaIds is to
 774 retain a right-hand-side that the simplifier will otherwise discard as
 775 dead code... the simplifier has a flag that tells it not to discard
 776 SpecPragmaId bindings.
 777
 778 In this case the f* retains a call-instance of the overloaded
 779 function, f, (including appropriate dictionaries) so that the
 780 specialiser will subsequently discover that there's a call of @f@ at
 781 Int, and will create a specialisation for @f@.  After that, the
 782 binding for @f*@ can be discarded.
 783
 784 We used to have a form
 785         {-# SPECIALISE f :: <type> = g #-}
 786 which promised that g implemented f at <type>, but we do that with
 787 a RULE now:
 788         {-# SPECIALISE (f::<type) = g #-}
 789
 790 \begin{code}
 791 tcSpecSigs :: [RenamedSig] -> TcM TcMonoBinds
 792 tcSpecSigs (SpecSig name poly_ty src_loc : sigs)
 793   =     -- SPECIALISE f :: forall b. theta => tau  =  g
 794     addSrcLoc src_loc                           $
 795     addErrCtxt (valSpecSigCtxt name poly_ty)    $
 796
 797         -- Get and instantiate its alleged specialised type
 798     tcHsSigType (FunSigCtxt name) poly_ty       `thenM` \ sig_ty ->
 799
 800         -- Check that f has a more general type, and build a RHS for
 801         -- the spec-pragma-id at the same time
 802     getLIE (tcCheckSigma (HsVar name) sig_ty)   `thenM` \ (spec_expr, spec_lie) ->
 803
 804         -- Squeeze out any Methods (see comments with tcSimplifyToDicts)
 805     tcSimplifyToDicts spec_lie                  `thenM` \ spec_binds ->
 806
 807         -- Just specialise "f" by building a SpecPragmaId binding
 808         -- It is the thing that makes sure we don't prematurely
 809         -- dead-code-eliminate the binding we are really interested in.
 810     newLocalName name                   `thenM` \ spec_name ->
 811     let
 812         spec_bind = VarMonoBind (mkSpecPragmaId spec_name sig_ty)
 813                                 (mkHsLet spec_binds spec_expr)
 814     in
 815
 816         -- Do the rest and combine
 817     tcSpecSigs sigs                     `thenM` \ binds_rest ->
 818     returnM (binds_rest `andMonoBinds` spec_bind)
 819
 820 tcSpecSigs (other_sig : sigs) = tcSpecSigs sigs
 821 tcSpecSigs []                 = returnM EmptyMonoBinds
 822 \end{code}
 823
 824 %************************************************************************
 825 %*                                                                      *
 826 \subsection[TcBinds-errors]{Error contexts and messages}
 827 %*                                                                      *
 828 %************************************************************************
 829
 830
 831 \begin{code}
 832 patMonoBindsCtxt bind
 833   = hang (ptext SLIT("In a pattern binding:")) 4 (ppr bind)
 834
 835 -----------------------------------------------
 836 valSpecSigCtxt v ty
 837   = sep [ptext SLIT("In a SPECIALIZE pragma for a value:"),
 838          nest 4 (ppr v <+> dcolon <+> ppr ty)]
 839
 840 -----------------------------------------------
 841 sigContextsErr = ptext SLIT("Mismatched contexts")
 842
 843 sigContextsCtxt s1 s2
 844   = vcat [ptext SLIT("When matching the contexts of the signatures for"),
 845           nest 2 (vcat [ppr s1 <+> dcolon <+> ppr (idType s1),
 846                         ppr s2 <+> dcolon <+> ppr (idType s2)]),
 847           ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
 848
 849 -----------------------------------------------
 850 unliftedBindErr flavour mbind
 851   = hang (text flavour <+> ptext SLIT("bindings for unlifted types aren't allowed:"))
 852          4 (ppr mbind)
 853
 854 -----------------------------------------------
 855 existentialExplode mbinds
 856   = hang (vcat [text "My brain just exploded.",
 857                 text "I can't handle pattern bindings for existentially-quantified constructors.",
 858                 text "In the binding group"])
 859         4 (ppr mbinds)
 860
 861 -----------------------------------------------
 862 restrictedBindCtxtErr binder_names
 863   = hang (ptext SLIT("Illegal overloaded type signature(s)"))
 864        4 (vcat [ptext SLIT("in a binding group for") <+> pprBinders binder_names,
 865                 ptext SLIT("that falls under the monomorphism restriction")])
 866
 867 genCtxt binder_names
 868   = ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names
 869
 870 -- Used in error messages
 871 -- Use quotes for a single one; they look a bit "busy" for several
 872 pprBinders [bndr] = quotes (ppr bndr)
 873 pprBinders bndrs  = pprWithCommas ppr bndrs
 874 \end{code}