never executed always true always false
    1 {-
    2 (c) The University of Glasgow 2006-2012
    3 (c) The GRASP Project, Glasgow University, 1992-2002
    4 
    5 -}
    6 
    7 
    8 {-# LANGUAGE TypeFamilies #-}
    9 
   10 module GHC.Tc.Gen.Sig(
   11        TcSigInfo(..),
   12        TcIdSigInfo(..), TcIdSigInst,
   13        TcPatSynInfo(..),
   14        TcSigFun,
   15 
   16        isPartialSig, hasCompleteSig, tcIdSigName, tcSigInfoName,
   17        completeSigPolyId_maybe, isCompleteHsSig,
   18        lhsSigWcTypeContextSpan, lhsSigTypeContextSpan,
   19 
   20        tcTySigs, tcUserTypeSig, completeSigFromId,
   21        tcInstSig,
   22 
   23        TcPragEnv, emptyPragEnv, lookupPragEnv, extendPragEnv,
   24        mkPragEnv, tcSpecPrags, tcSpecWrapper, tcImpPrags, addInlinePrags
   25    ) where
   26 
   27 import GHC.Prelude
   28 
   29 import GHC.Driver.Session
   30 import GHC.Driver.Backend
   31 
   32 import GHC.Hs
   33 
   34 
   35 import GHC.Tc.Errors.Types ( FixedRuntimeRepProvenance(..), TcRnMessage(..) )
   36 import GHC.Tc.Gen.HsType
   37 import GHC.Tc.Types
   38 import GHC.Tc.Solver( pushLevelAndSolveEqualitiesX, reportUnsolvedEqualities )
   39 import GHC.Tc.Utils.Monad
   40 import GHC.Tc.Utils.TcMType ( checkTypeHasFixedRuntimeRep )
   41 import GHC.Tc.Utils.Zonk
   42 import GHC.Tc.Types.Origin
   43 import GHC.Tc.Utils.TcType
   44 import GHC.Tc.Validity ( checkValidType )
   45 import GHC.Tc.Utils.Unify( tcSkolemise, unifyType )
   46 import GHC.Tc.Utils.Instantiate( topInstantiate, tcInstTypeBndrs )
   47 import GHC.Tc.Utils.Env( tcLookupId )
   48 import GHC.Tc.Types.Evidence( HsWrapper, (<.>) )
   49 
   50 import GHC.Core( hasSomeUnfolding )
   51 import GHC.Core.Type ( mkTyVarBinders )
   52 import GHC.Core.Multiplicity
   53 
   54 import GHC.Types.Error
   55 import GHC.Types.Var ( TyVar, Specificity(..), tyVarKind, binderVars )
   56 import GHC.Types.Id  ( Id, idName, idType, setInlinePragma
   57                      , mkLocalId, realIdUnfolding )
   58 import GHC.Types.Basic
   59 import GHC.Types.Name
   60 import GHC.Types.Name.Env
   61 import GHC.Types.SrcLoc
   62 
   63 import GHC.Builtin.Names( mkUnboundName )
   64 import GHC.Unit.Module( getModule )
   65 
   66 import GHC.Utils.Misc as Utils ( singleton )
   67 import GHC.Utils.Outputable
   68 import GHC.Utils.Panic
   69 import GHC.Utils.Trace
   70 
   71 import GHC.Data.Maybe( orElse )
   72 
   73 import Data.Maybe( mapMaybe )
   74 import Control.Monad( unless )
   75 
   76 
   77 {- -------------------------------------------------------------
   78           Note [Overview of type signatures]
   79 ----------------------------------------------------------------
   80 Type signatures, including partial signatures, are jolly tricky,
   81 especially on value bindings.  Here's an overview.
   82 
   83     f :: forall a. [a] -> [a]
   84     g :: forall b. _ -> b
   85 
   86     f = ...g...
   87     g = ...f...
   88 
   89 * HsSyn: a signature in a binding starts off as a TypeSig, in
   90   type HsBinds.Sig
   91 
   92 * When starting a mutually recursive group, like f/g above, we
   93   call tcTySig on each signature in the group.
   94 
   95 * tcTySig: Sig -> TcIdSigInfo
   96   - For a /complete/ signature, like 'f' above, tcTySig kind-checks
   97     the HsType, producing a Type, and wraps it in a CompleteSig, and
   98     extend the type environment with this polymorphic 'f'.
   99 
  100   - For a /partial/signature, like 'g' above, tcTySig does nothing
  101     Instead it just wraps the pieces in a PartialSig, to be handled
  102     later.
  103 
  104 * tcInstSig: TcIdSigInfo -> TcIdSigInst
  105   In tcMonoBinds, when looking at an individual binding, we use
  106   tcInstSig to instantiate the signature forall's in the signature,
  107   and attribute that instantiated (monomorphic) type to the
  108   binder.  You can see this in GHC.Tc.Gen.Bind.tcLhsId.
  109 
  110   The instantiation does the obvious thing for complete signatures,
  111   but for /partial/ signatures it starts from the HsSyn, so it
  112   has to kind-check it etc: tcHsPartialSigType.  It's convenient
  113   to do this at the same time as instantiation, because we can
  114   make the wildcards into unification variables right away, raather
  115   than somehow quantifying over them.  And the "TcLevel" of those
  116   unification variables is correct because we are in tcMonoBinds.
  117 
  118 
  119 Note [Binding scoped type variables]
  120 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  121 The type variables *brought into lexical scope* by a type signature
  122 may be a subset of the *quantified type variables* of the signatures,
  123 for two reasons:
  124 
  125 * With kind polymorphism a signature like
  126     f :: forall f a. f a -> f a
  127   may actually give rise to
  128     f :: forall k. forall (f::k -> *) (a:k). f a -> f a
  129   So the sig_tvs will be [k,f,a], but only f,a are scoped.
  130   NB: the scoped ones are not necessarily the *initial* ones!
  131 
  132 * Even aside from kind polymorphism, there may be more instantiated
  133   type variables than lexically-scoped ones.  For example:
  134         type T a = forall b. b -> (a,b)
  135         f :: forall c. T c
  136   Here, the signature for f will have one scoped type variable, c,
  137   but two instantiated type variables, c' and b'.
  138 
  139 However, all of this only applies to the renamer.  The typechecker
  140 just puts all of them into the type environment; any lexical-scope
  141 errors were dealt with by the renamer.
  142 
  143 -}
  144 
  145 
  146 {- *********************************************************************
  147 *                                                                      *
  148              Utility functions for TcSigInfo
  149 *                                                                      *
  150 ********************************************************************* -}
  151 
  152 tcIdSigName :: TcIdSigInfo -> Name
  153 tcIdSigName (CompleteSig { sig_bndr = id }) = idName id
  154 tcIdSigName (PartialSig { psig_name = n })  = n
  155 
  156 tcSigInfoName :: TcSigInfo -> Name
  157 tcSigInfoName (TcIdSig     idsi) = tcIdSigName idsi
  158 tcSigInfoName (TcPatSynSig tpsi) = patsig_name tpsi
  159 
  160 completeSigPolyId_maybe :: TcSigInfo -> Maybe TcId
  161 completeSigPolyId_maybe sig
  162   | TcIdSig sig_info <- sig
  163   , CompleteSig { sig_bndr = id } <- sig_info = Just id
  164   | otherwise                                 = Nothing
  165 
  166 
  167 {- *********************************************************************
  168 *                                                                      *
  169                Typechecking user signatures
  170 *                                                                      *
  171 ********************************************************************* -}
  172 
  173 tcTySigs :: [LSig GhcRn] -> TcM ([TcId], TcSigFun)
  174 tcTySigs hs_sigs
  175   = checkNoErrs $
  176     do { -- Fail if any of the signatures is duff
  177          -- Hence mapAndReportM
  178          -- See Note [Fail eagerly on bad signatures]
  179          ty_sigs_s <- mapAndReportM tcTySig hs_sigs
  180 
  181        ; let ty_sigs = concat ty_sigs_s
  182              poly_ids = mapMaybe completeSigPolyId_maybe ty_sigs
  183                         -- The returned [TcId] are the ones for which we have
  184                         -- a complete type signature.
  185                         -- See Note [Complete and partial type signatures]
  186              env = mkNameEnv [(tcSigInfoName sig, sig) | sig <- ty_sigs]
  187 
  188        ; return (poly_ids, lookupNameEnv env) }
  189 
  190 tcTySig :: LSig GhcRn -> TcM [TcSigInfo]
  191 tcTySig (L _ (IdSig _ id))
  192   = do { let ctxt = FunSigCtxt (idName id) NoRRC
  193                     -- NoRRC: do not report redundant constraints
  194                     -- The user has no control over the signature!
  195              sig = completeSigFromId ctxt id
  196        ; return [TcIdSig sig] }
  197 
  198 tcTySig (L loc (TypeSig _ names sig_ty))
  199   = setSrcSpanA loc $
  200     do { sigs <- sequence [ tcUserTypeSig (locA loc) sig_ty (Just name)
  201                           | L _ name <- names ]
  202        ; return (map TcIdSig sigs) }
  203 
  204 tcTySig (L loc (PatSynSig _ names sig_ty))
  205   = setSrcSpanA loc $
  206     do { tpsigs <- sequence [ tcPatSynSig name sig_ty
  207                             | L _ name <- names ]
  208        ; return (map TcPatSynSig tpsigs) }
  209 
  210 tcTySig _ = return []
  211 
  212 
  213 tcUserTypeSig :: SrcSpan -> LHsSigWcType GhcRn -> Maybe Name
  214               -> TcM TcIdSigInfo
  215 -- A function or expression type signature
  216 -- Returns a fully quantified type signature; even the wildcards
  217 -- are quantified with ordinary skolems that should be instantiated
  218 --
  219 -- The SrcSpan is what to declare as the binding site of the
  220 -- any skolems in the signature. For function signatures we
  221 -- use the whole `f :: ty' signature; for expression signatures
  222 -- just the type part.
  223 --
  224 -- Just n  => Function type signature       name :: type
  225 -- Nothing => Expression type signature   <expr> :: type
  226 tcUserTypeSig loc hs_sig_ty mb_name
  227   | isCompleteHsSig hs_sig_ty
  228   = do { sigma_ty <- tcHsSigWcType ctxt_no_rrc hs_sig_ty
  229        ; traceTc "tcuser" (ppr sigma_ty)
  230        ; return $
  231          CompleteSig { sig_bndr  = mkLocalId name Many sigma_ty
  232                                    -- We use `Many' as the multiplicity here,
  233                                    -- as if this identifier corresponds to
  234                                    -- anything, it is a top-level
  235                                    -- definition. Which are all unrestricted in
  236                                    -- the current implementation.
  237                      , sig_ctxt  = ctxt_rrc  -- Report redundant constraints
  238                      , sig_loc   = loc } }
  239                        -- Location of the <type> in   f :: <type>
  240 
  241   -- Partial sig with wildcards
  242   | otherwise
  243   = return (PartialSig { psig_name = name, psig_hs_ty = hs_sig_ty
  244                        , sig_ctxt = ctxt_no_rrc, sig_loc = loc })
  245   where
  246     name   = case mb_name of
  247                Just n  -> n
  248                Nothing -> mkUnboundName (mkVarOcc "<expression>")
  249 
  250     ctxt_rrc    = ctxt_fn (lhsSigWcTypeContextSpan hs_sig_ty)
  251     ctxt_no_rrc = ctxt_fn NoRRC
  252 
  253     ctxt_fn :: ReportRedundantConstraints -> UserTypeCtxt
  254     ctxt_fn rcc = case mb_name of
  255                Just n  -> FunSigCtxt n rcc
  256                Nothing -> ExprSigCtxt rcc
  257 
  258 lhsSigWcTypeContextSpan :: LHsSigWcType GhcRn -> ReportRedundantConstraints
  259 -- | Find the location of the top-level context of a HsType.  For example:
  260 --
  261 -- @
  262 --   forall a b. (Eq a, Ord b) => blah
  263 --               ^^^^^^^^^^^^^
  264 -- @
  265 -- If there is none, return Nothing
  266 lhsSigWcTypeContextSpan (HsWC { hswc_body = sigType }) = lhsSigTypeContextSpan sigType
  267 
  268 lhsSigTypeContextSpan :: LHsSigType GhcRn -> ReportRedundantConstraints
  269 lhsSigTypeContextSpan (L _ HsSig { sig_body = sig_ty }) = go sig_ty
  270   where
  271     go (L _ (HsQualTy { hst_ctxt = L span _ })) = WantRRC $ locA span -- Found it!
  272     go (L _ (HsForAllTy { hst_body = hs_ty })) = go hs_ty  -- Look under foralls
  273     go (L _ (HsParTy _ hs_ty)) = go hs_ty  -- Look under parens
  274     go _ = NoRRC  -- Did not find it
  275 
  276 completeSigFromId :: UserTypeCtxt -> Id -> TcIdSigInfo
  277 -- Used for instance methods and record selectors
  278 completeSigFromId ctxt id
  279   = CompleteSig { sig_bndr = id
  280                 , sig_ctxt = ctxt
  281                 , sig_loc  = getSrcSpan id }
  282 
  283 isCompleteHsSig :: LHsSigWcType GhcRn -> Bool
  284 -- ^ If there are no wildcards, return a LHsSigWcType
  285 isCompleteHsSig (HsWC { hswc_ext = wcs, hswc_body = hs_sig_ty })
  286    = null wcs && no_anon_wc_sig_ty hs_sig_ty
  287 
  288 no_anon_wc_sig_ty :: LHsSigType GhcRn -> Bool
  289 no_anon_wc_sig_ty (L _ (HsSig{sig_bndrs = outer_bndrs, sig_body = body}))
  290   =  all no_anon_wc_tvb (hsOuterExplicitBndrs outer_bndrs)
  291   && no_anon_wc_ty body
  292 
  293 no_anon_wc_ty :: LHsType GhcRn -> Bool
  294 no_anon_wc_ty lty = go lty
  295   where
  296     go (L _ ty) = case ty of
  297       HsWildCardTy _                 -> False
  298       HsAppTy _ ty1 ty2              -> go ty1 && go ty2
  299       HsAppKindTy _ ty ki            -> go ty && go ki
  300       HsFunTy _ w ty1 ty2            -> go ty1 && go ty2 && go (arrowToHsType w)
  301       HsListTy _ ty                  -> go ty
  302       HsTupleTy _ _ tys              -> gos tys
  303       HsSumTy _ tys                  -> gos tys
  304       HsOpTy _ ty1 _ ty2             -> go ty1 && go ty2
  305       HsParTy _ ty                   -> go ty
  306       HsIParamTy _ _ ty              -> go ty
  307       HsKindSig _ ty kind            -> go ty && go kind
  308       HsDocTy _ ty _                 -> go ty
  309       HsBangTy _ _ ty                -> go ty
  310       HsRecTy _ flds                 -> gos $ map (cd_fld_type . unLoc) flds
  311       HsExplicitListTy _ _ tys       -> gos tys
  312       HsExplicitTupleTy _ tys        -> gos tys
  313       HsForAllTy { hst_tele = tele
  314                  , hst_body = ty } -> no_anon_wc_tele tele
  315                                         && go ty
  316       HsQualTy { hst_ctxt = ctxt
  317                , hst_body = ty }  -> gos (unLoc ctxt) && go ty
  318       HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)) -> go $ L noSrcSpanA ty
  319       HsSpliceTy{} -> True
  320       HsTyLit{} -> True
  321       HsTyVar{} -> True
  322       HsStarTy{} -> True
  323       XHsType{} -> True       -- HsCoreTy, which does not have any wildcard
  324 
  325     gos = all go
  326 
  327 no_anon_wc_tele :: HsForAllTelescope GhcRn -> Bool
  328 no_anon_wc_tele tele = case tele of
  329   HsForAllVis   { hsf_vis_bndrs   = ltvs } -> all no_anon_wc_tvb ltvs
  330   HsForAllInvis { hsf_invis_bndrs = ltvs } -> all no_anon_wc_tvb ltvs
  331 
  332 no_anon_wc_tvb :: LHsTyVarBndr flag GhcRn -> Bool
  333 no_anon_wc_tvb (L _ tvb) = case tvb of
  334   UserTyVar _ _ _      -> True
  335   KindedTyVar _ _ _ ki -> no_anon_wc_ty ki
  336 
  337 {- Note [Fail eagerly on bad signatures]
  338 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  339 If a type signature is wrong, fail immediately:
  340 
  341  * the type sigs may bind type variables, so proceeding without them
  342    can lead to a cascade of errors
  343 
  344  * the type signature might be ambiguous, in which case checking
  345    the code against the signature will give a very similar error
  346    to the ambiguity error.
  347 
  348 ToDo: this means we fall over if any top-level type signature in the
  349 module is wrong, because we typecheck all the signatures together
  350 (see GHC.Tc.Gen.Bind.tcValBinds).  Moreover, because of top-level
  351 captureTopConstraints, only insoluble constraints will be reported.
  352 We typecheck all signatures at the same time because a signature
  353 like   f,g :: blah   might have f and g from different SCCs.
  354 
  355 So it's a bit awkward to get better error recovery, and no one
  356 has complained!
  357 -}
  358 
  359 {- *********************************************************************
  360 *                                                                      *
  361         Type checking a pattern synonym signature
  362 *                                                                      *
  363 ************************************************************************
  364 
  365 Note [Pattern synonym signatures]
  366 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  367 Pattern synonym signatures are surprisingly tricky (see #11224 for example).
  368 In general they look like this:
  369 
  370    pattern P :: forall univ_tvs. req_theta
  371              => forall ex_tvs. prov_theta
  372              => arg1 -> .. -> argn -> res_ty
  373 
  374 For parsing and renaming we treat the signature as an ordinary LHsSigType.
  375 
  376 Once we get to type checking, we decompose it into its parts, in tcPatSynSig.
  377 
  378 * Note that 'forall univ_tvs' and 'req_theta =>'
  379         and 'forall ex_tvs'   and 'prov_theta =>'
  380   are all optional.  We gather the pieces at the top of tcPatSynSig
  381 
  382 * Initially the implicitly-bound tyvars (added by the renamer) include both
  383   universal and existential vars.
  384 
  385 * After we kind-check the pieces and convert to Types, we do kind generalisation.
  386 
  387 Note [Report unsolved equalities in tcPatSynSig]
  388 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  389 It's important that we solve /all/ the equalities in a pattern
  390 synonym signature, because we are going to zonk the signature to
  391 a Type (not a TcType), in GHC.Tc.TyCl.PatSyn.tc_patsyn_finish, and that
  392 fails if there are un-filled-in coercion variables mentioned
  393 in the type (#15694).
  394 
  395 So we solve all the equalities we can, and report any unsolved ones,
  396 rather than leaving them in the ambient constraints to be solved
  397 later.  Pattern synonyms are top-level, so there's no problem with
  398 completely solving them.
  399 -}
  400 
  401 tcPatSynSig :: Name -> LHsSigType GhcRn -> TcM TcPatSynInfo
  402 -- See Note [Pattern synonym signatures]
  403 -- See Note [Recipe for checking a signature] in GHC.Tc.Gen.HsType
  404 tcPatSynSig name sig_ty@(L _ (HsSig{sig_bndrs = hs_outer_bndrs, sig_body = hs_ty}))
  405   | (hs_req, hs_ty1) <- splitLHsQualTy hs_ty
  406   , (ex_hs_tvbndrs, hs_prov, hs_body_ty) <- splitLHsSigmaTyInvis hs_ty1
  407   = do { traceTc "tcPatSynSig 1" (ppr sig_ty)
  408 
  409        ; let skol_info = DataConSkol name
  410        ; (tclvl, wanted, (outer_bndrs, (ex_bndrs, (req, prov, body_ty))))
  411            <- pushLevelAndSolveEqualitiesX "tcPatSynSig"           $
  412                      -- See Note [solveEqualities in tcPatSynSig]
  413               tcOuterTKBndrs skol_info hs_outer_bndrs $
  414               tcExplicitTKBndrs ex_hs_tvbndrs         $
  415               do { req     <- tcHsContext hs_req
  416                  ; prov    <- tcHsContext hs_prov
  417                  ; body_ty <- tcHsOpenType hs_body_ty
  418                      -- A (literal) pattern can be unlifted;
  419                      -- e.g. pattern Zero <- 0#   (#12094)
  420                  ; return (req, prov, body_ty) }
  421 
  422        ; let implicit_tvs :: [TcTyVar]
  423              univ_bndrs   :: [TcInvisTVBinder]
  424              (implicit_tvs, univ_bndrs) = case outer_bndrs of
  425                HsOuterImplicit{hso_ximplicit = implicit_tvs} -> (implicit_tvs, [])
  426                HsOuterExplicit{hso_xexplicit = univ_bndrs}   -> ([], univ_bndrs)
  427 
  428        ; implicit_tvs <- zonkAndScopedSort implicit_tvs
  429        ; let implicit_bndrs = mkTyVarBinders SpecifiedSpec implicit_tvs
  430 
  431        -- Kind generalisation
  432        ; let ungen_patsyn_ty = build_patsyn_type implicit_bndrs univ_bndrs
  433                                                  req ex_bndrs prov body_ty
  434        ; traceTc "tcPatSynSig" (ppr ungen_patsyn_ty)
  435        ; kvs <- kindGeneralizeAll ungen_patsyn_ty
  436        ; reportUnsolvedEqualities skol_info kvs tclvl wanted
  437                -- See Note [Report unsolved equalities in tcPatSynSig]
  438 
  439        -- These are /signatures/ so we zonk to squeeze out any kind
  440        -- unification variables.  Do this after kindGeneralizeAll which may
  441        -- default kind variables to *.
  442        ; ze                   <- mkEmptyZonkEnv NoFlexi
  443        ; (ze, kv_bndrs)       <- zonkTyVarBindersX   ze (mkTyVarBinders InferredSpec kvs)
  444        ; (ze, implicit_bndrs) <- zonkTyVarBindersX   ze implicit_bndrs
  445        ; (ze, univ_bndrs)     <- zonkTyVarBindersX   ze univ_bndrs
  446        ; (ze, ex_bndrs)       <- zonkTyVarBindersX   ze ex_bndrs
  447        ; req                  <- zonkTcTypesToTypesX ze req
  448        ; prov                 <- zonkTcTypesToTypesX ze prov
  449        ; body_ty              <- zonkTcTypeToTypeX   ze body_ty
  450 
  451        -- Now do validity checking
  452        ; checkValidType ctxt $
  453          build_patsyn_type implicit_bndrs univ_bndrs req ex_bndrs prov body_ty
  454 
  455        -- Neither argument types nor the return type may be representation polymorphic.
  456        -- This is because, when creating a matcher:
  457        --   - the argument types become the the binder types (see test RepPolyPatySynArg),
  458        --   - the return type becomes the scrutinee type (see test RepPolyPatSynRes).
  459        ; let (arg_tys, res_ty) = tcSplitFunTys body_ty
  460        ; mapM_
  461            (\(Scaled _ arg_ty) -> checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigArg arg_ty)
  462            arg_tys
  463        ; checkTypeHasFixedRuntimeRep FixedRuntimeRepPatSynSigRes res_ty
  464 
  465        ; traceTc "tcTySig }" $
  466          vcat [ text "kvs"          <+> ppr_tvs (binderVars kv_bndrs)
  467               , text "implicit_tvs" <+> ppr_tvs (binderVars implicit_bndrs)
  468               , text "univ_tvs"     <+> ppr_tvs (binderVars univ_bndrs)
  469               , text "req" <+> ppr req
  470               , text "ex_tvs" <+> ppr_tvs (binderVars ex_bndrs)
  471               , text "prov" <+> ppr prov
  472               , text "body_ty" <+> ppr body_ty ]
  473        ; return (TPSI { patsig_name = name
  474                       , patsig_implicit_bndrs = kv_bndrs ++ implicit_bndrs
  475                       , patsig_univ_bndrs     = univ_bndrs
  476                       , patsig_req            = req
  477                       , patsig_ex_bndrs       = ex_bndrs
  478                       , patsig_prov           = prov
  479                       , patsig_body_ty        = body_ty }) }
  480   where
  481     ctxt = PatSynCtxt name
  482 
  483     build_patsyn_type implicit_bndrs univ_bndrs req ex_bndrs prov body
  484       = mkInvisForAllTys implicit_bndrs $
  485         mkInvisForAllTys univ_bndrs $
  486         mkPhiTy req $
  487         mkInvisForAllTys ex_bndrs $
  488         mkPhiTy prov $
  489         body
  490 
  491 ppr_tvs :: [TyVar] -> SDoc
  492 ppr_tvs tvs = braces (vcat [ ppr tv <+> dcolon <+> ppr (tyVarKind tv)
  493                            | tv <- tvs])
  494 
  495 
  496 {- *********************************************************************
  497 *                                                                      *
  498                Instantiating user signatures
  499 *                                                                      *
  500 ********************************************************************* -}
  501 
  502 
  503 tcInstSig :: TcIdSigInfo -> TcM TcIdSigInst
  504 -- Instantiate a type signature; only used with plan InferGen
  505 tcInstSig sig@(CompleteSig { sig_bndr = poly_id, sig_loc = loc })
  506   = setSrcSpan loc $  -- Set the binding site of the tyvars
  507     do { (tv_prs, theta, tau) <- tcInstTypeBndrs poly_id
  508               -- See Note [Pattern bindings and complete signatures]
  509 
  510        ; return (TISI { sig_inst_sig   = sig
  511                       , sig_inst_skols = tv_prs
  512                       , sig_inst_wcs   = []
  513                       , sig_inst_wcx   = Nothing
  514                       , sig_inst_theta = theta
  515                       , sig_inst_tau   = tau }) }
  516 
  517 tcInstSig hs_sig@(PartialSig { psig_hs_ty = hs_ty
  518                              , sig_ctxt = ctxt
  519                              , sig_loc = loc })
  520   = setSrcSpan loc $  -- Set the binding site of the tyvars
  521     do { traceTc "Staring partial sig {" (ppr hs_sig)
  522        ; (wcs, wcx, tv_prs, theta, tau) <- tcHsPartialSigType ctxt hs_ty
  523          -- See Note [Checking partial type signatures] in GHC.Tc.Gen.HsType
  524        ; let inst_sig = TISI { sig_inst_sig   = hs_sig
  525                              , sig_inst_skols = tv_prs
  526                              , sig_inst_wcs   = wcs
  527                              , sig_inst_wcx   = wcx
  528                              , sig_inst_theta = theta
  529                              , sig_inst_tau   = tau }
  530        ; traceTc "End partial sig }" (ppr inst_sig)
  531        ; return inst_sig }
  532 
  533 
  534 {- Note [Pattern bindings and complete signatures]
  535 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  536 Consider
  537       data T a = MkT a a
  538       f :: forall a. a->a
  539       g :: forall b. b->b
  540       MkT f g = MkT (\x->x) (\y->y)
  541 Here we'll infer a type from the pattern of 'T a', but if we feed in
  542 the signature types for f and g, we'll end up unifying 'a' and 'b'
  543 
  544 So we instantiate f and g's signature with TyVarTv skolems
  545 (newMetaTyVarTyVars) that can unify with each other.  If too much
  546 unification takes place, we'll find out when we do the final
  547 impedance-matching check in GHC.Tc.Gen.Bind.mkExport
  548 
  549 See Note [TyVarTv] in GHC.Tc.Utils.TcMType
  550 
  551 None of this applies to a function binding with a complete
  552 signature, which doesn't use tcInstSig.  See GHC.Tc.Gen.Bind.tcPolyCheck.
  553 -}
  554 
  555 {- *********************************************************************
  556 *                                                                      *
  557                    Pragmas and PragEnv
  558 *                                                                      *
  559 ********************************************************************* -}
  560 
  561 type TcPragEnv = NameEnv [LSig GhcRn]
  562 
  563 emptyPragEnv :: TcPragEnv
  564 emptyPragEnv = emptyNameEnv
  565 
  566 lookupPragEnv :: TcPragEnv -> Name -> [LSig GhcRn]
  567 lookupPragEnv prag_fn n = lookupNameEnv prag_fn n `orElse` []
  568 
  569 extendPragEnv :: TcPragEnv -> (Name, LSig GhcRn) -> TcPragEnv
  570 extendPragEnv prag_fn (n, sig) = extendNameEnv_Acc (:) Utils.singleton prag_fn n sig
  571 
  572 ---------------
  573 mkPragEnv :: [LSig GhcRn] -> LHsBinds GhcRn -> TcPragEnv
  574 mkPragEnv sigs binds
  575   = foldl' extendPragEnv emptyNameEnv prs
  576   where
  577     prs = mapMaybe get_sig sigs
  578 
  579     get_sig :: LSig GhcRn -> Maybe (Name, LSig GhcRn)
  580     get_sig (L l (SpecSig x lnm@(L _ nm) ty inl))
  581       = Just (nm, L l $ SpecSig   x lnm ty (add_arity nm inl))
  582     get_sig (L l (InlineSig x lnm@(L _ nm) inl))
  583       = Just (nm, L l $ InlineSig x lnm    (add_arity nm inl))
  584     get_sig (L l (SCCFunSig x st lnm@(L _ nm) str))
  585       = Just (nm, L l $ SCCFunSig x st lnm str)
  586     get_sig _ = Nothing
  587 
  588     add_arity n inl_prag   -- Adjust inl_sat field to match visible arity of function
  589       | isInlinePragma inl_prag
  590         -- add arity only for real INLINE pragmas, not INLINABLE
  591       = case lookupNameEnv ar_env n of
  592           Just ar -> inl_prag { inl_sat = Just ar }
  593           Nothing -> warnPprTrace True (text "mkPragEnv no arity" <+> ppr n) $
  594                      -- There really should be a binding for every INLINE pragma
  595                      inl_prag
  596       | otherwise
  597       = inl_prag
  598 
  599     -- ar_env maps a local to the arity of its definition
  600     ar_env :: NameEnv Arity
  601     ar_env = foldr lhsBindArity emptyNameEnv binds
  602 
  603 lhsBindArity :: LHsBind GhcRn -> NameEnv Arity -> NameEnv Arity
  604 lhsBindArity (L _ (FunBind { fun_id = id, fun_matches = ms })) env
  605   = extendNameEnv env (unLoc id) (matchGroupArity ms)
  606 lhsBindArity _ env = env        -- PatBind/VarBind
  607 
  608 
  609 -----------------
  610 addInlinePrags :: TcId -> [LSig GhcRn] -> TcM TcId
  611 addInlinePrags poly_id prags_for_me
  612   | inl@(L _ prag) : inls <- inl_prags
  613   = do { traceTc "addInlinePrag" (ppr poly_id $$ ppr prag)
  614        ; unless (null inls) (warn_multiple_inlines inl inls)
  615        ; return (poly_id `setInlinePragma` prag) }
  616   | otherwise
  617   = return poly_id
  618   where
  619     inl_prags = [L loc prag | L loc (InlineSig _ _ prag) <- prags_for_me]
  620 
  621     warn_multiple_inlines _ [] = return ()
  622 
  623     warn_multiple_inlines inl1@(L loc prag1) (inl2@(L _ prag2) : inls)
  624        | inlinePragmaActivation prag1 == inlinePragmaActivation prag2
  625        , noUserInlineSpec (inlinePragmaSpec prag1)
  626        =    -- Tiresome: inl1 is put there by virtue of being in a hs-boot loop
  627             -- and inl2 is a user NOINLINE pragma; we don't want to complain
  628          warn_multiple_inlines inl2 inls
  629        | otherwise
  630        = setSrcSpanA loc $
  631          let dia = TcRnUnknownMessage $
  632                mkPlainDiagnostic WarningWithoutFlag noHints $
  633                  (hang (text "Multiple INLINE pragmas for" <+> ppr poly_id)
  634                    2 (vcat (text "Ignoring all but the first"
  635                             : map pp_inl (inl1:inl2:inls))))
  636          in addDiagnosticTc dia
  637 
  638     pp_inl (L loc prag) = ppr prag <+> parens (ppr loc)
  639 
  640 
  641 {- *********************************************************************
  642 *                                                                      *
  643                    SPECIALISE pragmas
  644 *                                                                      *
  645 ************************************************************************
  646 
  647 Note [Handling SPECIALISE pragmas]
  648 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  649 The basic idea is this:
  650 
  651    foo :: Num a => a -> b -> a
  652    {-# SPECIALISE foo :: Int -> b -> Int #-}
  653 
  654 We check that
  655    (forall a b. Num a => a -> b -> a)
  656       is more polymorphic than
  657    forall b. Int -> b -> Int
  658 (for which we could use tcSubType, but see below), generating a HsWrapper
  659 to connect the two, something like
  660       wrap = /\b. <hole> Int b dNumInt
  661 This wrapper is put in the TcSpecPrag, in the ABExport record of
  662 the AbsBinds.
  663 
  664 
  665         f :: (Eq a, Ix b) => a -> b -> Bool
  666         {-# SPECIALISE f :: (Ix p, Ix q) => Int -> (p,q) -> Bool #-}
  667         f = <poly_rhs>
  668 
  669 From this the typechecker generates
  670 
  671     AbsBinds [ab] [d1,d2] [([ab], f, f_mono, prags)] binds
  672 
  673     SpecPrag (wrap_fn :: forall a b. (Eq a, Ix b) => XXX
  674                       -> forall p q. (Ix p, Ix q) => XXX[ Int/a, (p,q)/b ])
  675 
  676 From these we generate:
  677 
  678     Rule:       forall p, q, (dp:Ix p), (dq:Ix q).
  679                     f Int (p,q) dInt ($dfInPair dp dq) = f_spec p q dp dq
  680 
  681     Spec bind:  f_spec = wrap_fn <poly_rhs>
  682 
  683 Note that
  684 
  685   * The LHS of the rule may mention dictionary *expressions* (eg
  686     $dfIxPair dp dq), and that is essential because the dp, dq are
  687     needed on the RHS.
  688 
  689   * The RHS of f_spec, <poly_rhs> has a *copy* of 'binds', so that it
  690     can fully specialise it.
  691 
  692 From the TcSpecPrag, in GHC.HsToCore.Binds we generate a binding for f_spec and a RULE:
  693 
  694    f_spec :: Int -> b -> Int
  695    f_spec = wrap<f rhs>
  696 
  697    RULE: forall b (d:Num b). f b d = f_spec b
  698 
  699 The RULE is generated by taking apart the HsWrapper, which is a little
  700 delicate, but works.
  701 
  702 Some wrinkles
  703 
  704 1. In tcSpecWrapper, rather than calling tcSubType, we directly call
  705    skolemise/instantiate.  That is mainly because of wrinkle (2).
  706 
  707    Historical note: in the past, tcSubType did co/contra stuff, which
  708    could generate too complex a LHS for the RULE, which was another
  709    reason for not using tcSubType.  But that reason has gone away
  710    with simple subsumption (#17775).
  711 
  712 2. We need to take care with type families (#5821).  Consider
  713       type instance F Int = Bool
  714       f :: Num a => a -> F a
  715       {-# SPECIALISE foo :: Int -> Bool #-}
  716 
  717   We *could* try to generate an f_spec with precisely the declared type:
  718       f_spec :: Int -> Bool
  719       f_spec = <f rhs> Int dNumInt |> co
  720 
  721       RULE: forall d. f Int d = f_spec |> sym co
  722 
  723   but the 'co' and 'sym co' are (a) playing no useful role, and (b) are
  724   hard to generate.  At all costs we must avoid this:
  725       RULE: forall d. f Int d |> co = f_spec
  726   because the LHS will never match (indeed it's rejected in
  727   decomposeRuleLhs).
  728 
  729   So we simply do this:
  730     - Generate a constraint to check that the specialised type (after
  731       skolemisation) is equal to the instantiated function type.
  732     - But *discard* the evidence (coercion) for that constraint,
  733       so that we ultimately generate the simpler code
  734           f_spec :: Int -> F Int
  735           f_spec = <f rhs> Int dNumInt
  736 
  737           RULE: forall d. f Int d = f_spec
  738       You can see this discarding happening in tcSpecPrag
  739 
  740 3. Note that the HsWrapper can transform *any* function with the right
  741    type prefix
  742        forall ab. (Eq a, Ix b) => XXX
  743    regardless of XXX.  It's sort of polymorphic in XXX.  This is
  744    useful: we use the same wrapper to transform each of the class ops, as
  745    well as the dict.  That's what goes on in GHC.Tc.TyCl.Instance.mk_meth_spec_prags
  746 -}
  747 
  748 tcSpecPrags :: Id -> [LSig GhcRn]
  749             -> TcM [LTcSpecPrag]
  750 -- Add INLINE and SPECIALSE pragmas
  751 --    INLINE prags are added to the (polymorphic) Id directly
  752 --    SPECIALISE prags are passed to the desugarer via TcSpecPrags
  753 -- Pre-condition: the poly_id is zonked
  754 -- Reason: required by tcSubExp
  755 tcSpecPrags poly_id prag_sigs
  756   = do { traceTc "tcSpecPrags" (ppr poly_id <+> ppr spec_sigs)
  757        ; unless (null bad_sigs) warn_discarded_sigs
  758        ; pss <- mapAndRecoverM (wrapLocMA (tcSpecPrag poly_id)) spec_sigs
  759        ; return $ concatMap (\(L l ps) -> map (L (locA l)) ps) pss }
  760   where
  761     spec_sigs = filter isSpecLSig prag_sigs
  762     bad_sigs  = filter is_bad_sig prag_sigs
  763     is_bad_sig s = not (isSpecLSig s || isInlineLSig s || isSCCFunSig s)
  764 
  765     warn_discarded_sigs
  766       = let dia = TcRnUnknownMessage $
  767               mkPlainDiagnostic WarningWithoutFlag noHints $
  768                 (hang (text "Discarding unexpected pragmas for" <+> ppr poly_id)
  769                     2 (vcat (map (ppr . getLoc) bad_sigs)))
  770         in addDiagnosticTc dia
  771 
  772 --------------
  773 tcSpecPrag :: TcId -> Sig GhcRn -> TcM [TcSpecPrag]
  774 tcSpecPrag poly_id prag@(SpecSig _ fun_name hs_tys inl)
  775 -- See Note [Handling SPECIALISE pragmas]
  776 --
  777 -- The Name fun_name in the SpecSig may not be the same as that of the poly_id
  778 -- Example: SPECIALISE for a class method: the Name in the SpecSig is
  779 --          for the selector Id, but the poly_id is something like $cop
  780 -- However we want to use fun_name in the error message, since that is
  781 -- what the user wrote (#8537)
  782   = addErrCtxt (spec_ctxt prag) $
  783     do  { warnIf (not (isOverloadedTy poly_ty || isInlinePragma inl)) $
  784                  TcRnUnknownMessage $ mkPlainDiagnostic WarningWithoutFlag noHints
  785                    (text "SPECIALISE pragma for non-overloaded function"
  786                     <+> quotes (ppr fun_name))
  787                     -- Note [SPECIALISE pragmas]
  788         ; spec_prags <- mapM tc_one hs_tys
  789         ; traceTc "tcSpecPrag" (ppr poly_id $$ nest 2 (vcat (map ppr spec_prags)))
  790         ; return spec_prags }
  791   where
  792     name      = idName poly_id
  793     poly_ty   = idType poly_id
  794     spec_ctxt prag = hang (text "In the pragma:") 2 (ppr prag)
  795 
  796     tc_one hs_ty
  797       = do { spec_ty <- tcHsSigType   (FunSigCtxt name NoRRC) hs_ty
  798            ; wrap    <- tcSpecWrapper (FunSigCtxt name (lhsSigTypeContextSpan hs_ty)) poly_ty spec_ty
  799            ; return (SpecPrag poly_id wrap inl) }
  800 
  801 tcSpecPrag _ prag = pprPanic "tcSpecPrag" (ppr prag)
  802 
  803 --------------
  804 tcSpecWrapper :: UserTypeCtxt -> TcType -> TcType -> TcM HsWrapper
  805 -- A simpler variant of tcSubType, used for SPECIALISE pragmas
  806 -- See Note [Handling SPECIALISE pragmas], wrinkle 1
  807 tcSpecWrapper ctxt poly_ty spec_ty
  808   = do { (sk_wrap, inst_wrap)
  809                <- tcSkolemise ctxt spec_ty $ \ spec_tau ->
  810                   do { (inst_wrap, tau) <- topInstantiate orig poly_ty
  811                      ; _ <- unifyType Nothing spec_tau tau
  812                             -- Deliberately ignore the evidence
  813                             -- See Note [Handling SPECIALISE pragmas],
  814                             --   wrinkle (2)
  815                      ; return inst_wrap }
  816        ; return (sk_wrap <.> inst_wrap) }
  817   where
  818     orig = SpecPragOrigin ctxt
  819 
  820 --------------
  821 tcImpPrags :: [LSig GhcRn] -> TcM [LTcSpecPrag]
  822 -- SPECIALISE pragmas for imported things
  823 tcImpPrags prags
  824   = do { this_mod <- getModule
  825        ; dflags <- getDynFlags
  826        ; if (not_specialising dflags) then
  827             return []
  828          else do
  829             { pss <- mapAndRecoverM (wrapLocMA tcImpSpec)
  830                      [L loc (name,prag)
  831                              | (L loc prag@(SpecSig _ (L _ name) _ _)) <- prags
  832                              , not (nameIsLocalOrFrom this_mod name) ]
  833             ; return $ concatMap (\(L l ps) -> map (L (locA l)) ps) pss } }
  834   where
  835     -- Ignore SPECIALISE pragmas for imported things
  836     -- when we aren't specialising, or when we aren't generating
  837     -- code.  The latter happens when Haddocking the base library;
  838     -- we don't want complaints about lack of INLINABLE pragmas
  839     not_specialising dflags
  840       | not (gopt Opt_Specialise dflags) = True
  841       | otherwise = case backend dflags of
  842                       NoBackend   -> True
  843                       Interpreter -> True
  844                       _other      -> False
  845 
  846 tcImpSpec :: (Name, Sig GhcRn) -> TcM [TcSpecPrag]
  847 tcImpSpec (name, prag)
  848  = do { id <- tcLookupId name
  849       ; if hasSomeUnfolding (realIdUnfolding id)
  850            -- See Note [SPECIALISE pragmas for imported Ids]
  851         then tcSpecPrag id prag
  852         else do { let dia = TcRnUnknownMessage $
  853                         mkPlainDiagnostic WarningWithoutFlag noHints (impSpecErr name)
  854                 ; addDiagnosticTc dia
  855                 ; return [] } }
  856 
  857 impSpecErr :: Name -> SDoc
  858 impSpecErr name
  859   = hang (text "You cannot SPECIALISE" <+> quotes (ppr name))
  860        2 (vcat [ text "because its definition is not visible in this module"
  861                , text "Hint: make sure" <+> ppr mod <+> text "is compiled with -O"
  862                , text "      and that" <+> quotes (ppr name)
  863                  <+> text "has an INLINABLE pragma" ])
  864   where
  865     mod = nameModule name
  866 
  867 {- Note [SPECIALISE pragmas for imported Ids]
  868 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  869 An imported Id may or may not have an unfolding.  If not, we obviously
  870 can't specialise it here; indeed the desugar falls over (#18118).
  871 
  872 We used to test whether it had a user-specified INLINABLE pragma but,
  873 because of Note [Worker/wrapper for INLINABLE functions] in
  874 GHC.Core.Opt.WorkWrap, even an INLINABLE function may end up with
  875 a wrapper that has no pragma, just an unfolding (#19246).  So now
  876 we just test whether the function has an unfolding.
  877 
  878 There's a risk that a pragma-free function may have an unfolding now
  879 (because it is fairly small), and then gets a bit bigger, and no
  880 longer has an unfolding in the future.  But then you'll get a helpful
  881 error message suggesting an INLINABLE pragma, which you can follow.
  882 That seems enough for now.
  883 -}