never executed always true always false
    1 
    2 {-# LANGUAGE FlexibleContexts #-}
    3 {-# LANGUAGE DisambiguateRecordFields #-}
    4 
    5 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
    6 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
    7 
    8 {-
    9 (c) The University of Glasgow 2006
   10 (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
   11 
   12 -}
   13 
   14 module GHC.Tc.Utils.Instantiate (
   15      topSkolemise,
   16      topInstantiate,
   17      instantiateSigma,
   18      instCall, instDFunType, instStupidTheta, instTyVarsWith,
   19      newWanted, newWanteds,
   20 
   21      tcInstType, tcInstTypeBndrs,
   22      tcInstSkolTyVars, tcInstSkolTyVarsX, tcInstSkolTyVarsAt,
   23      tcSkolDFunType, tcSuperSkolTyVars, tcInstSuperSkolTyVarsX,
   24 
   25      freshenTyVarBndrs, freshenCoVarBndrsX,
   26 
   27      tcInstInvisibleTyBindersN, tcInstInvisibleTyBinders, tcInstInvisibleTyBinder,
   28 
   29      newOverloadedLit, mkOverLit,
   30 
   31      newClsInst,
   32      tcGetInsts, tcGetInstEnvs, getOverlapFlag,
   33      tcExtendLocalInstEnv,
   34      instCallConstraints, newMethodFromName,
   35      tcSyntaxName,
   36 
   37      -- Simple functions over evidence variables
   38      tyCoVarsOfWC,
   39      tyCoVarsOfCt, tyCoVarsOfCts,
   40   ) where
   41 
   42 import GHC.Prelude
   43 
   44 import GHC.Driver.Session
   45 import GHC.Driver.Env
   46 
   47 import GHC.Builtin.Types  ( heqDataCon, eqDataCon, integerTyConName )
   48 import GHC.Builtin.Names
   49 
   50 import GHC.Hs
   51 import GHC.Hs.Syn.Type   ( hsLitType )
   52 
   53 import GHC.Core.InstEnv
   54 import GHC.Core.Predicate
   55 import GHC.Core ( Expr(..), isOrphan ) -- For the Coercion constructor
   56 import GHC.Core.Type
   57 import GHC.Core.Multiplicity
   58 import GHC.Core.TyCo.Rep
   59 import GHC.Core.TyCo.Ppr ( debugPprType )
   60 import GHC.Core.Class( Class )
   61 import GHC.Core.DataCon
   62 
   63 import {-# SOURCE #-}   GHC.Tc.Gen.Expr( tcCheckPolyExpr, tcSyntaxOp )
   64 import {-# SOURCE #-}   GHC.Tc.Utils.Unify( unifyType, unifyKind )
   65 import GHC.Tc.Utils.Zonk
   66 import GHC.Tc.Utils.Monad
   67 import GHC.Tc.Types.Constraint
   68 import GHC.Tc.Types.Origin
   69 import GHC.Tc.Utils.Env
   70 import GHC.Tc.Types.Evidence
   71 import GHC.Tc.Instance.FunDeps
   72 import GHC.Tc.Utils.Concrete
   73 import GHC.Tc.Utils.TcMType
   74 import GHC.Tc.Utils.TcType
   75 import GHC.Tc.Errors.Types
   76 
   77 import GHC.Types.Id.Make( mkDictFunId )
   78 import GHC.Types.Basic ( TypeOrKind(..), Arity )
   79 import GHC.Types.Error
   80 import GHC.Types.SourceText
   81 import GHC.Types.SrcLoc as SrcLoc
   82 import GHC.Types.Var.Env
   83 import GHC.Types.Var.Set
   84 import GHC.Types.Id
   85 import GHC.Types.Name
   86 import GHC.Types.Var
   87 import qualified GHC.LanguageExtensions as LangExt
   88 
   89 import GHC.Utils.Misc
   90 import GHC.Utils.Panic
   91 import GHC.Utils.Panic.Plain
   92 import GHC.Utils.Outputable
   93 
   94 import GHC.Unit.State
   95 import GHC.Unit.External
   96 
   97 import Data.List ( mapAccumL )
   98 import qualified Data.List.NonEmpty as NE
   99 import Control.Monad( when, unless, void )
  100 import Data.Function ( on )
  101 
  102 {-
  103 ************************************************************************
  104 *                                                                      *
  105                 Creating and emittind constraints
  106 *                                                                      *
  107 ************************************************************************
  108 -}
  109 
  110 newMethodFromName
  111   :: CtOrigin              -- ^ why do we need this?
  112   -> Name                  -- ^ name of the method
  113   -> [TcRhoType]           -- ^ types with which to instantiate the class
  114   -> TcM (HsExpr GhcTc)
  115 -- ^ Used when 'Name' is the wired-in name for a wired-in class method,
  116 -- so the caller knows its type for sure, which should be of form
  117 --
  118 -- > forall a. C a => <blah>
  119 --
  120 -- 'newMethodFromName' is supposed to instantiate just the outer
  121 -- type variable and constraint
  122 
  123 newMethodFromName origin name ty_args
  124   = do { id <- tcLookupId name
  125               -- Use tcLookupId not tcLookupGlobalId; the method is almost
  126               -- always a class op, but with -XRebindableSyntax GHC is
  127               -- meant to find whatever thing is in scope, and that may
  128               -- be an ordinary function.
  129 
  130        ; let ty = piResultTys (idType id) ty_args
  131              (theta, _caller_knows_this) = tcSplitPhiTy ty
  132        ; wrap <- assert (not (isForAllTy ty) && isSingleton theta) $
  133                  instCall origin ty_args theta
  134 
  135        ; return (mkHsWrap wrap (HsVar noExtField (noLocA id))) }
  136 
  137 {-
  138 ************************************************************************
  139 *                                                                      *
  140          Instantiation and skolemisation
  141 *                                                                      *
  142 ************************************************************************
  143 
  144 Note [Skolemisation]
  145 ~~~~~~~~~~~~~~~~~~~~
  146 topSkolemise decomposes and skolemises a type, returning a type
  147 with no top level foralls or (=>)
  148 
  149 Examples:
  150 
  151   topSkolemise (forall a. Ord a => a -> a)
  152     =  ( wp, [a], [d:Ord a], a->a )
  153     where wp = /\a. \(d:Ord a). <hole> a d
  154 
  155   topSkolemise  (forall a. Ord a => forall b. Eq b => a->b->b)
  156     =  ( wp, [a,b], [d1:Ord a,d2:Eq b], a->b->b )
  157     where wp = /\a.\(d1:Ord a)./\b.\(d2:Ord b). <hole> a d1 b d2
  158 
  159 This second example is the reason for the recursive 'go'
  160 function in topSkolemise: we must remove successive layers
  161 of foralls and (=>).
  162 
  163 In general,
  164   if      topSkolemise ty = (wrap, tvs, evs, rho)
  165     and   e :: rho
  166   then    wrap e :: ty
  167     and   'wrap' binds {tvs, evs}
  168 
  169 -}
  170 
  171 topSkolemise :: TcSigmaType
  172              -> TcM ( HsWrapper
  173                     , [(Name,TyVar)]     -- All skolemised variables
  174                     , [EvVar]            -- All "given"s
  175                     , TcRhoType )
  176 -- See Note [Skolemisation]
  177 topSkolemise ty
  178   = go init_subst idHsWrapper [] [] ty
  179   where
  180     init_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
  181 
  182     -- Why recursive?  See Note [Skolemisation]
  183     go subst wrap tv_prs ev_vars ty
  184       | (tvs, theta, inner_ty) <- tcSplitSigmaTy ty
  185       , not (null tvs && null theta)
  186       = do { (subst', tvs1) <- tcInstSkolTyVarsX subst tvs
  187            ; ev_vars1       <- newEvVars (substTheta subst' theta)
  188            ; go subst'
  189                 (wrap <.> mkWpTyLams tvs1 <.> mkWpLams ev_vars1)
  190                 (tv_prs ++ (map tyVarName tvs `zip` tvs1))
  191                 (ev_vars ++ ev_vars1)
  192                 inner_ty }
  193 
  194       | otherwise
  195       = return (wrap, tv_prs, ev_vars, substTy subst ty)
  196         -- substTy is a quick no-op on an empty substitution
  197 
  198 topInstantiate ::CtOrigin -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
  199 -- Instantiate outer invisible binders (both Inferred and Specified)
  200 -- If    top_instantiate ty = (wrap, inner_ty)
  201 -- then  wrap :: inner_ty "->" ty
  202 -- NB: returns a type with no (=>),
  203 --     and no invisible forall at the top
  204 topInstantiate orig sigma
  205   | (tvs,   body1) <- tcSplitSomeForAllTyVars isInvisibleArgFlag sigma
  206   , (theta, body2) <- tcSplitPhiTy body1
  207   , not (null tvs && null theta)
  208   = do { (_, wrap1, body3) <- instantiateSigma orig tvs theta body2
  209 
  210        -- Loop, to account for types like
  211        --       forall a. Num a => forall b. Ord b => ...
  212        ; (wrap2, body4) <- topInstantiate orig body3
  213 
  214        ; return (wrap2 <.> wrap1, body4) }
  215 
  216   | otherwise = return (idHsWrapper, sigma)
  217 
  218 instantiateSigma :: CtOrigin -> [TyVar] -> TcThetaType -> TcSigmaType
  219                  -> TcM ([TcTyVar], HsWrapper, TcSigmaType)
  220 -- (instantiate orig tvs theta ty)
  221 -- instantiates the the type variables tvs, emits the (instantiated)
  222 -- constraints theta, and returns the (instantiated) type ty
  223 instantiateSigma orig tvs theta body_ty
  224   = do { (subst, inst_tvs) <- mapAccumLM newMetaTyVarX empty_subst tvs
  225        ; let inst_theta  = substTheta subst theta
  226              inst_body   = substTy subst body_ty
  227              inst_tv_tys = mkTyVarTys inst_tvs
  228 
  229        ; wrap <- instCall orig inst_tv_tys inst_theta
  230        ; traceTc "Instantiating"
  231                  (vcat [ text "origin" <+> pprCtOrigin orig
  232                        , text "tvs"   <+> ppr tvs
  233                        , text "theta" <+> ppr theta
  234                        , text "type" <+> debugPprType body_ty
  235                        , text "with" <+> vcat (map debugPprType inst_tv_tys)
  236                        , text "theta:" <+>  ppr inst_theta ])
  237 
  238       ; return (inst_tvs, wrap, inst_body) }
  239   where
  240     free_tvs = tyCoVarsOfType body_ty `unionVarSet` tyCoVarsOfTypes theta
  241     in_scope = mkInScopeSet (free_tvs `delVarSetList` tvs)
  242     empty_subst = mkEmptyTCvSubst in_scope
  243 
  244 instTyVarsWith :: CtOrigin -> [TyVar] -> [TcType] -> TcM TCvSubst
  245 -- Use this when you want to instantiate (forall a b c. ty) with
  246 -- types [ta, tb, tc], but when the kinds of 'a' and 'ta' might
  247 -- not yet match (perhaps because there are unsolved constraints; #14154)
  248 -- If they don't match, emit a kind-equality to promise that they will
  249 -- eventually do so, and thus make a kind-homongeneous substitution.
  250 instTyVarsWith orig tvs tys
  251   = go emptyTCvSubst tvs tys
  252   where
  253     go subst [] []
  254       = return subst
  255     go subst (tv:tvs) (ty:tys)
  256       | tv_kind `tcEqType` ty_kind
  257       = go (extendTvSubstAndInScope subst tv ty) tvs tys
  258       | otherwise
  259       = do { co <- emitWantedEq orig KindLevel Nominal ty_kind tv_kind
  260            ; go (extendTvSubstAndInScope subst tv (ty `mkCastTy` co)) tvs tys }
  261       where
  262         tv_kind = substTy subst (tyVarKind tv)
  263         ty_kind = tcTypeKind ty
  264 
  265     go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
  266 
  267 
  268 {-
  269 ************************************************************************
  270 *                                                                      *
  271             Instantiating a call
  272 *                                                                      *
  273 ************************************************************************
  274 
  275 Note [Handling boxed equality]
  276 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  277 The solver deals entirely in terms of unboxed (primitive) equality.
  278 There should never be a boxed Wanted equality. Ever. But, what if
  279 we are calling `foo :: forall a. (F a ~ Bool) => ...`? That equality
  280 is boxed, so naive treatment here would emit a boxed Wanted equality.
  281 
  282 So we simply check for this case and make the right boxing of evidence.
  283 
  284 -}
  285 
  286 ----------------
  287 instCall :: CtOrigin -> [TcType] -> TcThetaType -> TcM HsWrapper
  288 -- Instantiate the constraints of a call
  289 --      (instCall o tys theta)
  290 -- (a) Makes fresh dictionaries as necessary for the constraints (theta)
  291 -- (b) Throws these dictionaries into the LIE
  292 -- (c) Returns an HsWrapper ([.] tys dicts)
  293 
  294 instCall orig tys theta
  295   = do  { dict_app <- instCallConstraints orig theta
  296         ; return (dict_app <.> mkWpTyApps tys) }
  297 
  298 ----------------
  299 instCallConstraints :: CtOrigin -> TcThetaType -> TcM HsWrapper
  300 -- Instantiates the TcTheta, puts all constraints thereby generated
  301 -- into the LIE, and returns a HsWrapper to enclose the call site.
  302 
  303 instCallConstraints orig preds
  304   | null preds
  305   = return idHsWrapper
  306   | otherwise
  307   = do { evs <- mapM go preds
  308        ; traceTc "instCallConstraints" (ppr evs)
  309        ; return (mkWpEvApps evs) }
  310   where
  311     go :: TcPredType -> TcM EvTerm
  312     go pred
  313      | Just (Nominal, ty1, ty2) <- getEqPredTys_maybe pred -- Try short-cut #1
  314      = do  { co <- unifyType Nothing ty1 ty2
  315            ; return (evCoercion co) }
  316 
  317        -- Try short-cut #2
  318      | Just (tc, args@[_, _, ty1, ty2]) <- splitTyConApp_maybe pred
  319      , tc `hasKey` heqTyConKey
  320      = do { co <- unifyType Nothing ty1 ty2
  321           ; return (evDFunApp (dataConWrapId heqDataCon) args [Coercion co]) }
  322 
  323      | otherwise
  324      = emitWanted orig pred
  325 
  326 instDFunType :: DFunId -> [DFunInstType]
  327              -> TcM ( [TcType]      -- instantiated argument types
  328                     , TcThetaType ) -- instantiated constraint
  329 -- See Note [DFunInstType: instantiating types] in GHC.Core.InstEnv
  330 instDFunType dfun_id dfun_inst_tys
  331   = do { (subst, inst_tys) <- go empty_subst dfun_tvs dfun_inst_tys
  332        ; return (inst_tys, substTheta subst dfun_theta) }
  333   where
  334     dfun_ty = idType dfun_id
  335     (dfun_tvs, dfun_theta, _) = tcSplitSigmaTy dfun_ty
  336     empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType dfun_ty))
  337                   -- With quantified constraints, the
  338                   -- type of a dfun may not be closed
  339 
  340     go :: TCvSubst -> [TyVar] -> [DFunInstType] -> TcM (TCvSubst, [TcType])
  341     go subst [] [] = return (subst, [])
  342     go subst (tv:tvs) (Just ty : mb_tys)
  343       = do { (subst', tys) <- go (extendTvSubstAndInScope subst tv ty)
  344                                  tvs
  345                                  mb_tys
  346            ; return (subst', ty : tys) }
  347     go subst (tv:tvs) (Nothing : mb_tys)
  348       = do { (subst', tv') <- newMetaTyVarX subst tv
  349            ; (subst'', tys) <- go subst' tvs mb_tys
  350            ; return (subst'', mkTyVarTy tv' : tys) }
  351     go _ _ _ = pprPanic "instDFunTypes" (ppr dfun_id $$ ppr dfun_inst_tys)
  352 
  353 ----------------
  354 instStupidTheta :: CtOrigin -> TcThetaType -> TcM ()
  355 -- Similar to instCall, but only emit the constraints in the LIE
  356 -- Used exclusively for the 'stupid theta' of a data constructor
  357 instStupidTheta orig theta
  358   = do  { _co <- instCallConstraints orig theta -- Discard the coercion
  359         ; return () }
  360 
  361 
  362 {- *********************************************************************
  363 *                                                                      *
  364          Instantiating Kinds
  365 *                                                                      *
  366 ********************************************************************* -}
  367 
  368 -- | Given ty::forall k1 k2. k, instantiate all the invisible forall-binders
  369 --   returning ty @kk1 @kk2 :: k[kk1/k1, kk2/k1]
  370 tcInstInvisibleTyBinders :: TcType -> TcKind -> TcM (TcType, TcKind)
  371 tcInstInvisibleTyBinders ty kind
  372   = do { (extra_args, kind') <- tcInstInvisibleTyBindersN n_invis kind
  373        ; return (mkAppTys ty extra_args, kind') }
  374   where
  375     n_invis = invisibleTyBndrCount kind
  376 
  377 tcInstInvisibleTyBindersN :: Int -> TcKind -> TcM ([TcType], TcKind)
  378 tcInstInvisibleTyBindersN 0 kind
  379   = return ([], kind)
  380 tcInstInvisibleTyBindersN n ty
  381   = go n empty_subst ty
  382   where
  383     empty_subst = mkEmptyTCvSubst (mkInScopeSet (tyCoVarsOfType ty))
  384 
  385     go n subst kind
  386       | n > 0
  387       , Just (bndr, body) <- tcSplitPiTy_maybe kind
  388       , isInvisibleBinder bndr
  389       = do { (subst', arg) <- tcInstInvisibleTyBinder subst bndr
  390            ; (args, inner_ty) <- go (n-1) subst' body
  391            ; return (arg:args, inner_ty) }
  392       | otherwise
  393       = return ([], substTy subst kind)
  394 
  395 -- | Used only in *types*
  396 tcInstInvisibleTyBinder :: TCvSubst -> TyBinder -> TcM (TCvSubst, TcType)
  397 tcInstInvisibleTyBinder subst (Named (Bndr tv _))
  398   = do { (subst', tv') <- newMetaTyVarX subst tv
  399        ; return (subst', mkTyVarTy tv') }
  400 
  401 tcInstInvisibleTyBinder subst (Anon af ty)
  402   | Just (mk, k1, k2) <- get_eq_tys_maybe (substTy subst (scaledThing ty))
  403     -- Equality is the *only* constraint currently handled in types.
  404     -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
  405   = assert (af == InvisArg) $
  406     do { co <- unifyKind Nothing k1 k2
  407        ; arg' <- mk co
  408        ; return (subst, arg') }
  409 
  410   | otherwise  -- This should never happen
  411                -- See GHC.Core.TyCo.Rep Note [Constraints in kinds]
  412   = pprPanic "tcInvisibleTyBinder" (ppr ty)
  413 
  414 -------------------------------
  415 get_eq_tys_maybe :: Type
  416                  -> Maybe ( Coercion -> TcM Type
  417                              -- given a coercion proving t1 ~# t2, produce the
  418                              -- right instantiation for the TyBinder at hand
  419                           , Type  -- t1
  420                           , Type  -- t2
  421                           )
  422 -- See Note [Constraints in kinds] in GHC.Core.TyCo.Rep
  423 get_eq_tys_maybe ty
  424   -- Lifted heterogeneous equality (~~)
  425   | Just (tc, [_, _, k1, k2]) <- splitTyConApp_maybe ty
  426   , tc `hasKey` heqTyConKey
  427   = Just (\co -> mkHEqBoxTy co k1 k2, k1, k2)
  428 
  429   -- Lifted homogeneous equality (~)
  430   | Just (tc, [_, k1, k2]) <- splitTyConApp_maybe ty
  431   , tc `hasKey` eqTyConKey
  432   = Just (\co -> mkEqBoxTy co k1 k2, k1, k2)
  433 
  434   | otherwise
  435   = Nothing
  436 
  437 -- | This takes @a ~# b@ and returns @a ~~ b@.
  438 mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
  439 -- monadic just for convenience with mkEqBoxTy
  440 mkHEqBoxTy co ty1 ty2
  441   = return $
  442     mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
  443   where k1 = tcTypeKind ty1
  444         k2 = tcTypeKind ty2
  445 
  446 -- | This takes @a ~# b@ and returns @a ~ b@.
  447 mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
  448 mkEqBoxTy co ty1 ty2
  449   = return $
  450     mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
  451   where k = tcTypeKind ty1
  452 
  453 {- *********************************************************************
  454 *                                                                      *
  455         SkolemTvs (immutable)
  456 *                                                                      *
  457 ********************************************************************* -}
  458 
  459 tcInstType :: ([TyVar] -> TcM (TCvSubst, [TcTyVar]))
  460                    -- ^ How to instantiate the type variables
  461            -> Id                                           -- ^ Type to instantiate
  462            -> TcM ([(Name, TcTyVar)], TcThetaType, TcType) -- ^ Result
  463                 -- (type vars, preds (incl equalities), rho)
  464 tcInstType inst_tyvars id
  465   | null tyvars   -- There may be overloading despite no type variables;
  466                   --      (?x :: Int) => Int -> Int
  467   = return ([], theta, tau)
  468   | otherwise
  469   = do { (subst, tyvars') <- inst_tyvars tyvars
  470        ; let tv_prs  = map tyVarName tyvars `zip` tyvars'
  471              subst'  = extendTCvInScopeSet subst (tyCoVarsOfType rho)
  472        ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
  473   where
  474     (tyvars, rho) = tcSplitForAllInvisTyVars (idType id)
  475     (theta, tau)  = tcSplitPhiTy rho
  476 
  477 tcInstTypeBndrs :: Id -> TcM ([(Name, InvisTVBinder)], TcThetaType, TcType)
  478                      -- (type vars, preds (incl equalities), rho)
  479 -- Instantiate the binders of a type signature with TyVarTvs
  480 tcInstTypeBndrs id
  481   | null tyvars   -- There may be overloading despite no type variables;
  482                   --      (?x :: Int) => Int -> Int
  483   = return ([], theta, tau)
  484   | otherwise
  485   = do { (subst, tyvars') <- mapAccumLM inst_invis_bndr emptyTCvSubst tyvars
  486        ; let tv_prs  = map (tyVarName . binderVar) tyvars `zip` tyvars'
  487              subst'  = extendTCvInScopeSet subst (tyCoVarsOfType rho)
  488        ; return (tv_prs, substTheta subst' theta, substTy subst' tau) }
  489   where
  490     (tyvars, rho) = splitForAllInvisTVBinders (idType id)
  491     (theta, tau)  = tcSplitPhiTy rho
  492 
  493     inst_invis_bndr :: TCvSubst -> InvisTVBinder
  494                     -> TcM (TCvSubst, InvisTVBinder)
  495     inst_invis_bndr subst (Bndr tv spec)
  496       = do { (subst', tv') <- newMetaTyVarTyVarX subst tv
  497            ; return (subst', Bndr tv' spec) }
  498 
  499 tcSkolDFunType :: DFunId -> TcM ([TcTyVar], TcThetaType, TcType)
  500 -- Instantiate a type signature with skolem constants.
  501 -- This freshens the names, but no need to do so
  502 tcSkolDFunType dfun
  503   = do { (tv_prs, theta, tau) <- tcInstType tcInstSuperSkolTyVars dfun
  504        ; return (map snd tv_prs, theta, tau) }
  505 
  506 tcSuperSkolTyVars :: [TyVar] -> (TCvSubst, [TcTyVar])
  507 -- Make skolem constants, but do *not* give them new names, as above
  508 -- Moreover, make them "super skolems"; see comments with superSkolemTv
  509 -- see Note [Kind substitution when instantiating]
  510 -- Precondition: tyvars should be ordered by scoping
  511 tcSuperSkolTyVars = mapAccumL tcSuperSkolTyVar emptyTCvSubst
  512 
  513 tcSuperSkolTyVar :: TCvSubst -> TyVar -> (TCvSubst, TcTyVar)
  514 tcSuperSkolTyVar subst tv
  515   = (extendTvSubstWithClone subst tv new_tv, new_tv)
  516   where
  517     kind   = substTyUnchecked subst (tyVarKind tv)
  518     new_tv = mkTcTyVar (tyVarName tv) kind superSkolemTv
  519 
  520 -- | Given a list of @['TyVar']@, skolemize the type variables,
  521 -- returning a substitution mapping the original tyvars to the
  522 -- skolems, and the list of newly bound skolems.
  523 tcInstSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
  524 -- See Note [Skolemising type variables]
  525 tcInstSkolTyVars = tcInstSkolTyVarsX emptyTCvSubst
  526 
  527 tcInstSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
  528 -- See Note [Skolemising type variables]
  529 tcInstSkolTyVarsX = tcInstSkolTyVarsPushLevel False
  530 
  531 tcInstSuperSkolTyVars :: [TyVar] -> TcM (TCvSubst, [TcTyVar])
  532 -- See Note [Skolemising type variables]
  533 -- This version freshens the names and creates "super skolems";
  534 -- see comments around superSkolemTv.
  535 tcInstSuperSkolTyVars = tcInstSuperSkolTyVarsX emptyTCvSubst
  536 
  537 tcInstSuperSkolTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
  538 -- See Note [Skolemising type variables]
  539 -- This version freshens the names and creates "super skolems";
  540 -- see comments around superSkolemTv.
  541 tcInstSuperSkolTyVarsX subst = tcInstSkolTyVarsPushLevel True subst
  542 
  543 tcInstSkolTyVarsPushLevel :: Bool  -- True <=> make "super skolem"
  544                           -> TCvSubst -> [TyVar]
  545                           -> TcM (TCvSubst, [TcTyVar])
  546 -- Skolemise one level deeper, hence pushTcLevel
  547 -- See Note [Skolemising type variables]
  548 tcInstSkolTyVarsPushLevel overlappable subst tvs
  549   = do { tc_lvl <- getTcLevel
  550        -- Do not retain the whole TcLclEnv
  551        ; let !pushed_lvl = pushTcLevel tc_lvl
  552        ; tcInstSkolTyVarsAt pushed_lvl overlappable subst tvs }
  553 
  554 tcInstSkolTyVarsAt :: TcLevel -> Bool
  555                    -> TCvSubst -> [TyVar]
  556                    -> TcM (TCvSubst, [TcTyVar])
  557 tcInstSkolTyVarsAt lvl overlappable subst tvs
  558   = freshenTyCoVarsX new_skol_tv subst tvs
  559   where
  560     details = SkolemTv lvl overlappable
  561     new_skol_tv name kind = mkTcTyVar name kind details
  562 
  563 ------------------
  564 freshenTyVarBndrs :: [TyVar] -> TcM (TCvSubst, [TyVar])
  565 -- ^ Give fresh uniques to a bunch of TyVars, but they stay
  566 --   as TyVars, rather than becoming TcTyVars
  567 -- Used in 'GHC.Tc.Instance.Family.newFamInst', and 'GHC.Tc.Utils.Instantiate.newClsInst'
  568 freshenTyVarBndrs = freshenTyCoVars mkTyVar
  569 
  570 freshenCoVarBndrsX :: TCvSubst -> [CoVar] -> TcM (TCvSubst, [CoVar])
  571 -- ^ Give fresh uniques to a bunch of CoVars
  572 -- Used in "GHC.Tc.Instance.Family.newFamInst"
  573 freshenCoVarBndrsX subst = freshenTyCoVarsX mkCoVar subst
  574 
  575 ------------------
  576 freshenTyCoVars :: (Name -> Kind -> TyCoVar)
  577                 -> [TyVar] -> TcM (TCvSubst, [TyCoVar])
  578 freshenTyCoVars mk_tcv = freshenTyCoVarsX mk_tcv emptyTCvSubst
  579 
  580 freshenTyCoVarsX :: (Name -> Kind -> TyCoVar)
  581                  -> TCvSubst -> [TyCoVar]
  582                  -> TcM (TCvSubst, [TyCoVar])
  583 freshenTyCoVarsX mk_tcv = mapAccumLM (freshenTyCoVarX mk_tcv)
  584 
  585 freshenTyCoVarX :: (Name -> Kind -> TyCoVar)
  586                 -> TCvSubst -> TyCoVar -> TcM (TCvSubst, TyCoVar)
  587 -- This a complete freshening operation:
  588 -- the skolems have a fresh unique, and a location from the monad
  589 -- See Note [Skolemising type variables]
  590 freshenTyCoVarX mk_tcv subst tycovar
  591   = do { loc  <- getSrcSpanM
  592        ; uniq <- newUnique
  593        ; let old_name = tyVarName tycovar
  594              -- Force so we don't retain reference to the old name and id
  595              -- See (#19619) for more discussion
  596              !old_occ_name = getOccName old_name
  597              new_name = mkInternalName uniq old_occ_name loc
  598              new_kind = substTyUnchecked subst (tyVarKind tycovar)
  599              new_tcv  = mk_tcv new_name new_kind
  600              subst1   = extendTCvSubstWithClone subst tycovar new_tcv
  601        ; return (subst1, new_tcv) }
  602 
  603 {- Note [Skolemising type variables]
  604 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  605 The tcInstSkolTyVars family of functions instantiate a list of TyVars
  606 to fresh skolem TcTyVars. Important notes:
  607 
  608 a) Level allocation. We generally skolemise /before/ calling
  609    pushLevelAndCaptureConstraints.  So we want their level to the level
  610    of the soon-to-be-created implication, which has a level ONE HIGHER
  611    than the current level.  Hence the pushTcLevel.  It feels like a
  612    slight hack.
  613 
  614 b) The [TyVar] should be ordered (kind vars first)
  615    See Note [Kind substitution when instantiating]
  616 
  617 c) Clone the variable to give a fresh unique.  This is essential.
  618    Consider (tc160)
  619        type Foo x = forall a. a -> x
  620    And typecheck the expression
  621        (e :: Foo (Foo ())
  622    We will skolemise the signature, but after expanding synonyms it
  623    looks like
  624         forall a. a -> forall a. a -> x
  625    We don't want to make two big-lambdas with the same unique!
  626 
  627 d) We retain locations. Because the location of the variable is the correct
  628    location to report in errors (e.g. in the signature). We don't want the
  629    location to change to the body of the function, which does *not* explicitly
  630    bind the variable.
  631 
  632 e) The resulting skolems are
  633         non-overlappable for tcInstSkolTyVars,
  634    but overlappable for tcInstSuperSkolTyVars
  635    See GHC.Tc.Deriv.Infer Note [Overlap and deriving] for an example
  636    of where this matters.
  637 
  638 Note [Kind substitution when instantiating]
  639 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  640 When we instantiate a bunch of kind and type variables, first we
  641 expect them to be topologically sorted.
  642 Then we have to instantiate the kind variables, build a substitution
  643 from old variables to the new variables, then instantiate the type
  644 variables substituting the original kind.
  645 
  646 Exemple: If we want to instantiate
  647   [(k1 :: *), (k2 :: *), (a :: k1 -> k2), (b :: k1)]
  648 we want
  649   [(?k1 :: *), (?k2 :: *), (?a :: ?k1 -> ?k2), (?b :: ?k1)]
  650 instead of the bogus
  651   [(?k1 :: *), (?k2 :: *), (?a :: k1 -> k2), (?b :: k1)]
  652 -}
  653 
  654 {- *********************************************************************
  655 *                                                                      *
  656                 Literals
  657 *                                                                      *
  658 ********************************************************************* -}
  659 
  660 {-
  661 In newOverloadedLit we convert directly to an Int or Integer if we
  662 know that's what we want.  This may save some time, by not
  663 temporarily generating overloaded literals, but it won't catch all
  664 cases (the rest are caught in lookupInst).
  665 
  666 -}
  667 
  668 newOverloadedLit :: HsOverLit GhcRn
  669                  -> ExpRhoType
  670                  -> TcM (HsOverLit GhcTc)
  671 newOverloadedLit lit res_ty
  672   = do { mb_lit' <- tcShortCutLit lit res_ty
  673        ; case mb_lit' of
  674             Just lit' -> return lit'
  675             Nothing   -> newNonTrivialOverloadedLit lit res_ty }
  676 
  677 -- Does not handle things that 'shortCutLit' can handle. See also
  678 -- newOverloadedLit in GHC.Tc.Utils.Unify
  679 newNonTrivialOverloadedLit :: HsOverLit GhcRn
  680                            -> ExpRhoType
  681                            -> TcM (HsOverLit GhcTc)
  682 newNonTrivialOverloadedLit
  683   lit@(OverLit { ol_val = val, ol_ext = OverLitRn rebindable (L _ meth_name) })
  684   res_ty
  685   = do  { hs_lit <- mkOverLit val
  686         ; let lit_ty = hsLitType hs_lit
  687         ; (_, fi') <- tcSyntaxOp orig (mkRnSyntaxExpr meth_name)
  688                                       [synKnownType lit_ty] res_ty $
  689                       \_ _ -> return ()
  690         ; let L _ witness = nlHsSyntaxApps fi' [nlHsLit hs_lit]
  691         ; res_ty <- readExpType res_ty
  692         ; return (lit { ol_ext = OverLitTc { ol_rebindable = rebindable
  693                                            , ol_witness = witness
  694                                            , ol_type = res_ty } }) }
  695   where
  696     orig = LiteralOrigin lit
  697 
  698 ------------
  699 mkOverLit ::OverLitVal -> TcM (HsLit GhcTc)
  700 mkOverLit (HsIntegral i)
  701   = do  { integer_ty <- tcMetaTy integerTyConName
  702         ; return (HsInteger (il_text i)
  703                             (il_value i) integer_ty) }
  704 
  705 mkOverLit (HsFractional r)
  706   = do  { rat_ty <- tcMetaTy rationalTyConName
  707         ; return (HsRat noExtField r rat_ty) }
  708 
  709 mkOverLit (HsIsString src s) = return (HsString src s)
  710 
  711 {-
  712 ************************************************************************
  713 *                                                                      *
  714                 Re-mappable syntax
  715 
  716      Used only for arrow syntax -- find a way to nuke this
  717 *                                                                      *
  718 ************************************************************************
  719 
  720 Suppose we are doing the -XRebindableSyntax thing, and we encounter
  721 a do-expression.  We have to find (>>) in the current environment, which is
  722 done by the rename. Then we have to check that it has the same type as
  723 Control.Monad.(>>).  Or, more precisely, a compatible type. One 'customer' had
  724 this:
  725 
  726   (>>) :: HB m n mn => m a -> n b -> mn b
  727 
  728 So the idea is to generate a local binding for (>>), thus:
  729 
  730         let then72 :: forall a b. m a -> m b -> m b
  731             then72 = ...something involving the user's (>>)...
  732         in
  733         ...the do-expression...
  734 
  735 Now the do-expression can proceed using then72, which has exactly
  736 the expected type.
  737 
  738 In fact tcSyntaxName just generates the RHS for then72, because we only
  739 want an actual binding in the do-expression case. For literals, we can
  740 just use the expression inline.
  741 -}
  742 
  743 tcSyntaxName :: CtOrigin
  744              -> TcType                  -- ^ Type to instantiate it at
  745              -> (Name, HsExpr GhcRn)    -- ^ (Standard name, user name)
  746              -> TcM (Name, HsExpr GhcTc)
  747                                         -- ^ (Standard name, suitable expression)
  748 -- USED ONLY FOR CmdTop (sigh) ***
  749 -- See Note [CmdSyntaxTable] in "GHC.Hs.Expr"
  750 
  751 tcSyntaxName orig ty (std_nm, HsVar _ (L _ user_nm))
  752   | std_nm == user_nm
  753   = do rhs <- newMethodFromName orig std_nm [ty]
  754        return (std_nm, rhs)
  755 
  756 tcSyntaxName orig ty (std_nm, user_nm_expr) = do
  757     std_id <- tcLookupId std_nm
  758     let
  759         ([tv], _, tau) = tcSplitSigmaTy (idType std_id)
  760         sigma1         = substTyWith [tv] [ty] tau
  761         -- Actually, the "tau-type" might be a sigma-type in the
  762         -- case of locally-polymorphic methods.
  763 
  764     span <- getSrcSpanM
  765     addErrCtxtM (syntaxNameCtxt user_nm_expr orig sigma1 span) $ do
  766 
  767         -- Check that the user-supplied thing has the
  768         -- same type as the standard one.
  769         -- Tiresome jiggling because tcCheckSigma takes a located expression
  770      expr <- tcCheckPolyExpr (L (noAnnSrcSpan span) user_nm_expr) sigma1
  771      hasFixedRuntimeRepRes std_nm user_nm_expr sigma1
  772      return (std_nm, unLoc expr)
  773 
  774 syntaxNameCtxt :: HsExpr GhcRn -> CtOrigin -> Type -> SrcSpan -> TidyEnv
  775                -> TcRn (TidyEnv, SDoc)
  776 syntaxNameCtxt name orig ty loc tidy_env = return (tidy_env, msg)
  777   where
  778     msg = vcat [ text "When checking that" <+> quotes (ppr name)
  779                           <+> text "(needed by a syntactic construct)"
  780                , nest 2 (text "has the required type:"
  781                          <+> ppr (tidyType tidy_env ty))
  782                , nest 2 (sep [ppr orig, text "at" <+> ppr loc])]
  783 
  784 {-
  785 ************************************************************************
  786 *                                                                      *
  787                 FixedRuntimeRep
  788 *                                                                      *
  789 ************************************************************************
  790 -}
  791 
  792 -- | Check that the result type of an expression has a fixed runtime representation.
  793 --
  794 -- Used only for arrow operations such as 'arr', 'first', etc.
  795 hasFixedRuntimeRepRes :: Name -> HsExpr GhcRn -> TcSigmaType -> TcM ()
  796 hasFixedRuntimeRepRes std_nm user_expr ty = mapM_ do_check mb_arity
  797   where
  798    do_check :: Arity -> TcM ()
  799    do_check arity =
  800      let res_ty = nTimes arity (snd . splitPiTy) ty
  801      in void $ hasFixedRuntimeRep (FRRArrow $ ArrowFun user_expr) res_ty
  802    mb_arity :: Maybe Arity
  803    mb_arity -- arity of the arrow operation, counting type-level arguments
  804      | std_nm == arrAName     -- result used as an argument in, e.g., do_premap
  805      = Just 3
  806      | std_nm == composeAName -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
  807      = Just 5
  808      | std_nm == firstAName   -- result used as an argument in, e.g., dsCmdStmt/BodyStmt
  809      = Just 4
  810      | std_nm == appAName     -- result used as an argument in, e.g., dsCmd/HsCmdArrApp/HsHigherOrderApp
  811      = Just 2
  812      | std_nm == choiceAName  -- result used as an argument in, e.g., HsCmdIf
  813      = Just 5
  814      | std_nm == loopAName    -- result used as an argument in, e.g., HsCmdIf
  815      = Just 4
  816      | otherwise
  817      = Nothing
  818 
  819 {-
  820 ************************************************************************
  821 *                                                                      *
  822                 Instances
  823 *                                                                      *
  824 ************************************************************************
  825 -}
  826 
  827 getOverlapFlag :: Maybe OverlapMode -> TcM OverlapFlag
  828 -- Construct the OverlapFlag from the global module flags,
  829 -- but if the overlap_mode argument is (Just m),
  830 --     set the OverlapMode to 'm'
  831 getOverlapFlag overlap_mode
  832   = do  { dflags <- getDynFlags
  833         ; let overlap_ok    = xopt LangExt.OverlappingInstances dflags
  834               incoherent_ok = xopt LangExt.IncoherentInstances  dflags
  835               use x = OverlapFlag { isSafeOverlap = safeLanguageOn dflags
  836                                   , overlapMode   = x }
  837               default_oflag | incoherent_ok = use (Incoherent NoSourceText)
  838                             | overlap_ok    = use (Overlaps NoSourceText)
  839                             | otherwise     = use (NoOverlap NoSourceText)
  840 
  841               final_oflag = setOverlapModeMaybe default_oflag overlap_mode
  842         ; return final_oflag }
  843 
  844 tcGetInsts :: TcM [ClsInst]
  845 -- Gets the local class instances.
  846 tcGetInsts = fmap tcg_insts getGblEnv
  847 
  848 newClsInst :: Maybe OverlapMode -> Name -> [TyVar] -> ThetaType
  849            -> Class -> [Type] -> TcM ClsInst
  850 newClsInst overlap_mode dfun_name tvs theta clas tys
  851   = do { (subst, tvs') <- freshenTyVarBndrs tvs
  852              -- Be sure to freshen those type variables,
  853              -- so they are sure not to appear in any lookup
  854        ; let tys' = substTys subst tys
  855 
  856              dfun = mkDictFunId dfun_name tvs theta clas tys
  857              -- The dfun uses the original 'tvs' because
  858              -- (a) they don't need to be fresh
  859              -- (b) they may be mentioned in the ib_binds field of
  860              --     an InstInfo, and in GHC.Tc.Utils.Env.pprInstInfoDetails it's
  861              --     helpful to use the same names
  862 
  863        ; oflag <- getOverlapFlag overlap_mode
  864        ; let inst = mkLocalInstance dfun oflag tvs' clas tys'
  865        ; when (isOrphan (is_orphan inst)) $
  866           addDiagnostic (TcRnOrphanInstance inst)
  867        ; return inst }
  868 
  869 tcExtendLocalInstEnv :: [ClsInst] -> TcM a -> TcM a
  870   -- Add new locally-defined instances
  871 tcExtendLocalInstEnv dfuns thing_inside
  872  = do { traceDFuns dfuns
  873       ; env <- getGblEnv
  874       -- Force the access to the TcgEnv so it isn't retained.
  875       -- During auditing it is much easier to observe in -hi profiles if
  876       -- there are a very small number of TcGblEnv. Keeping a TcGblEnv
  877       -- alive is quite dangerous because it contains reference to many
  878       -- large data structures.
  879       ; let !init_inst_env = tcg_inst_env env
  880             !init_insts = tcg_insts env
  881       ; (inst_env', cls_insts') <- foldlM addLocalInst
  882                                           (init_inst_env, init_insts)
  883                                           dfuns
  884       ; let env' = env { tcg_insts    = cls_insts'
  885                        , tcg_inst_env = inst_env' }
  886       ; setGblEnv env' thing_inside }
  887 
  888 addLocalInst :: (InstEnv, [ClsInst]) -> ClsInst -> TcM (InstEnv, [ClsInst])
  889 -- Check that the proposed new instance is OK,
  890 -- and then add it to the home inst env
  891 -- If overwrite_inst, then we can overwrite a direct match
  892 addLocalInst (home_ie, my_insts) ispec
  893    = do {
  894              -- Load imported instances, so that we report
  895              -- duplicates correctly
  896 
  897              -- 'matches'  are existing instance declarations that are less
  898              --            specific than the new one
  899              -- 'dups'     are those 'matches' that are equal to the new one
  900          ; isGHCi <- getIsGHCi
  901          ; eps    <- getEps
  902          ; tcg_env <- getGblEnv
  903 
  904            -- In GHCi, we *override* any identical instances
  905            -- that are also defined in the interactive context
  906            -- See Note [Override identical instances in GHCi]
  907          ; let home_ie'
  908                  | isGHCi    = deleteFromInstEnv home_ie ispec
  909                  | otherwise = home_ie
  910 
  911                global_ie = eps_inst_env eps
  912                inst_envs = InstEnvs { ie_global  = global_ie
  913                                     , ie_local   = home_ie'
  914                                     , ie_visible = tcVisibleOrphanMods tcg_env }
  915 
  916              -- Check for inconsistent functional dependencies
  917          ; let inconsistent_ispecs = checkFunDeps inst_envs ispec
  918          ; unless (null inconsistent_ispecs) $
  919            funDepErr ispec inconsistent_ispecs
  920 
  921              -- Check for duplicate instance decls.
  922          ; let (_tvs, cls, tys) = instanceHead ispec
  923                (matches, _, _)  = lookupInstEnv False inst_envs cls tys
  924                dups             = filter (identicalClsInstHead ispec) (map fst matches)
  925          ; unless (null dups) $
  926            dupInstErr ispec (head dups)
  927 
  928          ; return (extendInstEnv home_ie' ispec, ispec : my_insts) }
  929 
  930 {-
  931 Note [Signature files and type class instances]
  932 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  933 Instances in signature files do not have an effect when compiling:
  934 when you compile a signature against an implementation, you will
  935 see the instances WHETHER OR NOT the instance is declared in
  936 the file (this is because the signatures go in the EPS and we
  937 can't filter them out easily.)  This is also why we cannot
  938 place the instance in the hi file: it would show up as a duplicate,
  939 and we don't have instance reexports anyway.
  940 
  941 However, you might find them useful when typechecking against
  942 a signature: the instance is a way of indicating to GHC that
  943 some instance exists, in case downstream code uses it.
  944 
  945 Implementing this is a little tricky.  Consider the following
  946 situation (sigof03):
  947 
  948  module A where
  949      instance C T where ...
  950 
  951  module ASig where
  952      instance C T
  953 
  954 When compiling ASig, A.hi is loaded, which brings its instances
  955 into the EPS.  When we process the instance declaration in ASig,
  956 we should ignore it for the purpose of doing a duplicate check,
  957 since it's not actually a duplicate. But don't skip the check
  958 entirely, we still want this to fail (tcfail221):
  959 
  960  module ASig where
  961      instance C T
  962      instance C T
  963 
  964 Note that in some situations, the interface containing the type
  965 class instances may not have been loaded yet at all.  The usual
  966 situation when A imports another module which provides the
  967 instances (sigof02m):
  968 
  969  module A(module B) where
  970      import B
  971 
  972 See also Note [Signature lazy interface loading].  We can't
  973 rely on this, however, since sometimes we'll have spurious
  974 type class instances in the EPS, see #9422 (sigof02dm)
  975 
  976 ************************************************************************
  977 *                                                                      *
  978         Errors and tracing
  979 *                                                                      *
  980 ************************************************************************
  981 -}
  982 
  983 traceDFuns :: [ClsInst] -> TcRn ()
  984 traceDFuns ispecs
  985   = traceTc "Adding instances:" (vcat (map pp ispecs))
  986   where
  987     pp ispec = hang (ppr (instanceDFunId ispec) <+> colon)
  988                   2 (ppr ispec)
  989         -- Print the dfun name itself too
  990 
  991 funDepErr :: ClsInst -> [ClsInst] -> TcRn ()
  992 funDepErr ispec ispecs
  993   = addClsInstsErr TcRnFunDepConflict (ispec NE.:| ispecs)
  994 
  995 dupInstErr :: ClsInst -> ClsInst -> TcRn ()
  996 dupInstErr ispec dup_ispec
  997   = addClsInstsErr TcRnDupInstanceDecls (ispec NE.:| [dup_ispec])
  998 
  999 addClsInstsErr :: (UnitState -> NE.NonEmpty ClsInst -> TcRnMessage)
 1000                -> NE.NonEmpty ClsInst
 1001                -> TcRn ()
 1002 addClsInstsErr mkErr ispecs = do
 1003    unit_state <- hsc_units <$> getTopEnv
 1004    setSrcSpan (getSrcSpan (NE.head sorted)) $
 1005       addErr $ mkErr unit_state sorted
 1006  where
 1007    sorted = NE.sortBy (SrcLoc.leftmost_smallest `on` getSrcSpan) ispecs
 1008    -- The sortBy just arranges that instances are displayed in order
 1009    -- of source location, which reduced wobbling in error messages,
 1010    -- and is better for users