{-# LANGUAGE FlexibleContexts    #-}

 {-# LANGUAGE GADTs               #-}

 {-# LANGUAGE MultiWayIf          #-}

 {-# LANGUAGE ScopedTypeVariables #-}

 {-# LANGUAGE TypeFamilies        #-}

 {-# LANGUAGE UndecidableInstances #-} -- Wrinkle in Note [Trees That Grow]

 import GHC.Core.Type

 import GHC.Core.Coercion

 import GHC.Builtin.PrimOps( tagToEnumKey )

 import GHC.Builtin.Names

 import GHC.Types.Var.Env  ( emptyTidyEnv, mkInScopeSet )

 import GHC.Data.Maybe

 import GHC.Utils.Misc

 import GHC.Utils.Outputable as Outputable

        -- Step 3: Instantiate the function type (taking a quick look at args)

        ; do_ql <- wantQuickLook rn_fun

        ; (inst_args, app_res_rho)

        ; case do_ql of

             NoQL -> do { traceTc "tcApp:NoQL" (ppr rn_fun $$ ppr app_res_rho)

                          -- Step 5.5: wrap up

                        ; finishApp tc_head tc_args app_res_rho res_wrap } }

 quickLookResultType :: TcRhoType -> ExpRhoType -> TcM ()

 -- This function implements the shaded bit of rule APP-Downarrow in

 -- Fig 5 of the QL paper: "A quick look at impredicativity" (ICFP'20).

                 -- addHeadCtxt: important for the class constraints

                 -- that may be emitted from instantiating fun_sigma

                 addHeadCtxt fun_ctxt $

                   -- See Note [Representation-polymorphism checking built-ins]

                   -- in GHC.Tc.Utils.Concrete.

                   -- NB: we are doing this even when "acc" is not empty,

         --     not defer in any way, because this is a QL instantiation variable.

         -- It's easier just to do the job directly here.

         do { arg_tys <- zipWithM new_arg_ty (leadingValArgs args) [pos..]

            ; let fun_ty' = mkScaledFunTys arg_tys res_ty

            -- Fill in kappa := nu_1 -> .. -> nu_n -> res_nu

     new_arg_ty :: LHsExpr GhcRn -> Int -> TcM (Scaled TcType)

     -- Make a fresh nus for each argument in rule IVAR

     new_arg_ty (L _ arg) i

                        FRRExpectedFunTy (ExpectedFunTyArg (HsExprTcThing tc_fun) arg) i

                -- Following matchActualFunTy, we create nu_i :: TYPE kappa_i[conc],

                -- thereby ensuring that the arguments have concrete runtime representations

                -- mult_ty: e need variables for argument multiplicities (#18731)

                -- Otherwise, 'undefined x' wouldn't be linear in x

 {- *********************************************************************

 *                                                                      *

               Instantiating fresh type variables

 *                                                                      *

 ********************************************************************* -}

 getTcLevelQL DoQL = return QLInstVar

 getTcLevelQL NoQL = getTcLevel

                  -> ConcreteTyVars -- ^ concreteness information

                  -> [TyVar]

                  -> TcThetaType -> TcSigmaType

 -- (instantiate orig tvs theta ty)

 -- instantiates the type variables tvs, emits the (instantiated)

 -- constraints theta, and returns the (instantiated) type ty

        ; let inst_theta  = substTheta subst theta

              inst_body   = substTy subst body_ty

                        , text "tvs"   <+> ppr tvs

                        , text "theta" <+> ppr theta

                        , text "type" <+> debugPprType body_ty

                        , text "theta:" <+> ppr inst_theta ])

       ; return (wrap, inst_body) }

                --                We just want an accurate free-var set

     empty_subst = mkEmptySubst in_scope

            ; return (new_subst, new_tv) }

     get_info :: Subst -> TyVar -> TcM MetaInfo

       -- Is this a type variable that must be instantiated to a concrete type?

       -- If so, create a ConcreteTv metavariable instead of a plain TauTv.

       -- See Note [Representation-polymorphism checking built-ins]

       --     in GHC.Tc.Utils.Concrete.

       | Just conc_orig0 <- lookupNameEnv concs (tyVarName tv)

       , let conc_orig = substConcreteTvOrigin final_subst body_ty conc_orig0

                         -- See Note [substConcreteTvOrigin].

       -- The vastly common case

       | otherwise

 import GHC.Types.Var.Env

 import GHC.Types.Id

 import GHC.Types.Name

 import GHC.Types.Name.Reader (WithUserRdr(..))

 import GHC.Types.Var

 import qualified GHC.LanguageExtensions as LangExt

                        , text "tvs"   <+> ppr tvs

                        , text "theta" <+> ppr theta

                        , text "type" <+> debugPprType body_ty

                        , text "theta:" <+> ppr inst_theta ])

       ; return (wrap2 <.> wrap1, inner_body) }

   newOpenBoxedTypeKind,

   newMetaKindVar, newMetaKindVars,

   newMetaTyVarTyAtLevel, newConcreteTyVarTyAtLevel, substConcreteTvOrigin,

   cloneMetaTyVar, cloneMetaTyVarWithInfo,

   newCycleBreakerTyVar,

   newMetaTyVars, newMetaTyVarX, newMetaTyVarsX, newMetaTyVarBndrsX,

   newMetaTyVarTyVarX,

   newTyVarTyVar, cloneTyVarTyVar,

   newPatTyVar, newSkolemTyVar, newWildCardX,

   --------------------------------

 variables only refer to other type variables, but this restriction was

 dropped, and ScopedTypeVariables can now refer to full types (GHC

 Proposal 29).

 -}

 newMetaTyVarName :: FastString -> TcM Name

 newMetaTyVarName str

   = newSysName (mkTyVarOccFS str)

 cloneMetaTyVarName :: Name -> TcM Name

 cloneMetaTyVarName name

   = newSysName (nameOccName name)

 metaInfoToTyVarName :: MetaInfo -> FastString

 metaInfoToTyVarName  meta_info =

                  -> FastString -> TcKind -> TcM TcTyVar

 newConcreteTyVar reason fs kind

   = assertPpr (isConcreteType kind) assert_msg $

   where

     assert_msg = text "newConcreteTyVar: non-concrete kind" <+> ppr kind

 newPatTyVar :: Name -> Kind -> TcM TcTyVar

 newPatTyVar name kind

   = do { details <- newMetaDetails TauTv

 -- in GHC.Tc.Utils.Concrete.

 newOpenFlexiFRRTyVar :: FixedRuntimeRepContext -> TcM TcTyVar

 newOpenFlexiFRRTyVar frr_ctxt

                           FixedRuntimeRepOrigin

                             { frr_context = frr_ctxt

                             , frr_type    = mkTyVarTy tv }

 -- | See 'newOpenFlexiFRRTyVar'.

 newOpenFlexiFRRTyVarTy :: FixedRuntimeRepContext -> TcM TcType