-         , nest 2 (hang (text "fits the type of its context:") 2 pp_res_ty) ]

-    where

-      -- Zonking will have turned Infer into Check

-      pp_res_ty = case res_ty of

-                    Check ty -> ppr ty

-                    Infer ir -> text "OOPS" <+> ppr ir

-  FunResCtxt fun n_val_args res_fun res_env n_fun n_env

-checkResultTy rn_expr (tc_fun, _) _ app_res_rho (Infer inf_res)

-  = do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun

-       ; fillInferResult ds_flag (exprCtOrigin rn_expr) app_res_rho inf_res

-       }

-

-checkResultTy rn_expr (tc_fun, fun_loc) inst_args app_res_rho (Check res_ty)

--- Unify with expected type from the context

--- See Note [Unify with expected type before typechecking arguments]

---

--- Match up app_res_rho: the result type of rn_expr

---     with res_ty:  the expected result type

- = perhaps_add_res_ty_ctxt $

-   do { ds_flag <- getDeepSubsumptionFlag_DataConHead tc_fun

-      ; traceTc "checkResultTy {" $

-          vcat [ text "tc_fun:" <+> ppr tc_fun

-               , text "app_res_rho:" <+> ppr app_res_rho

-               , text "res_ty:"  <+> ppr res_ty

-               , text "ds_flag:" <+> ppr ds_flag ]

-      ; case ds_flag of

-          Shallow -> -- No deep subsumption

-             -- app_res_rho and res_ty are both rho-types,

-             -- so with simple subsumption we can just unify them

-             -- No need to zonk; the unifier does that

-             do { co <- unifyExprType rn_expr app_res_rho res_ty

-                ; traceTc "checkResultTy 1 }" (ppr co)

-                ; return (mkWpCastN co) }

-

-          Deep ds_reason ->   -- Deep subsumption

-             -- Even though both app_res_rho and res_ty are rho-types,

-             -- they may have nested polymorphism, so if deep subsumption

-             -- is on we must call tcSubType.

-             do { wrap <- tcSubTypeDS tc_fun ds_reason rn_expr app_res_rho res_ty

-                ; traceTc "checkResultTy 2 }" $

-                   vcat [ text "app_res_rho:" <+> ppr app_res_rho

-                        , text "res_ty:" <+> ppr res_ty

-                        , text "wrap:" <+> ppr wrap

-                        ]

-                ; return wrap } }

-      = addFunResCtxt tc_fun inst_args app_res_rho (mkCheckExpType res_ty) $

-       ; if tooComplicatedForQuickLook rn_fun_arg

-    do { (fun_ue, (tc_fun_arg_head, fun_sigma_arg_head)) <- tcCollectingUsage $ tcInferExprSigma rn_fun_arg

-tooComplicatedForQuickLook :: HsExpr GhcRn -> Bool

-tooComplicatedForQuickLook expr

-      HsVar {}              -> False

-      ExprWithTySig {}      -> False

-      XExpr (HsRecSelRn {}) -> False

-      HsOverLit {}          -> False

-      _ -> True  -- Too complicated

---   - HsVar           lone variables, to ensure that they can get an

---                     impredicative instantiation (via Quick Look

---                     driven by res_ty (in checking mode)).

---   - ExprWithTySig   (e :: type)

---   - HsRecSel        overloaded record fields

---   - ExpandedThingRn renamer/pre-typechecker expansions

---   - HsOverLit       overloaded literals

-tcExpr e@(HsVar _ v_rn) res_ty

-  = do { (v_tc, sigma_ty) <- tcInferId v_rn

-       ; traceTc "tcExpr:HsVar" (ppr v_tc <+> dcolon <+> ppr sigma_ty $$ ppr res_ty)

-       ; tcWrapResult e v_tc sigma_ty res_ty }

-

-tcExpr e@(ExprWithTySig _ e_rn e_ty) res_ty

-  = do { (e_tc, sigma_ty) <- tcExprWithSig e_rn e_ty

-       ; tcWrapResult e e_tc sigma_ty res_ty }

-

-tcExpr e@(XExpr(HsRecSelRn f)) res_ty

-  = do { (e_tc, sigma_ty) <- tcInferRecSelId f

-       ; tcWrapResult e e_tc sigma_ty res_ty }

-

-tcExpr (XExpr (ExpandedThingRn hse)) res_ty = tcHsExpansion hse res_ty

-

-tcExpr e@(HsApp {})              res_ty = tcApp e res_ty

-tcExpr e@(OpApp {})              res_ty = tcApp e res_ty

-tcExpr e@(HsAppType {})          res_ty = tcApp e res_ty

-       ; tcWrapResultMono expr expr' act_res_ty res_ty }

-        ; ret <- tcWrapResultMono expr expr' actual_res_ty res_ty

-

-        ; return ret }

-             ; tcWrapResultMono expr expr' ds_res_ty res_ty

-             }

-        }

-import {-# SOURCE #-} GHC.Tc.Gen.Splice( getUntypedSpliceBody )

-

-import GHC.Utils.Panic

-As per Note [Polymorphisation of linear fields] in

-GHC.Core.Multiplicity, when we use a data constructor as a term, we want to

-consider its field to have polymorphic multiplicities. That is,

-Note [Data constructors are linear by default] says:

-addFunResCtxt :: HsExpr GhcTc -> [HsExprArg p]

-  = do { env_tv  <- newFlexiTyVarTy liftedTypeKind

-       ; dumping <- doptM Opt_D_dump_tc_trace

-       ; msg <- mk_msg dumping env_tv

-       ; addErrCtxt msg thing_inside }

-  where

-    mk_msg dumping env_tv

-      = do { mb_env_ty <- readExpType_maybe env_ty

-                     -- by the time the message is rendered, the ExpType

-                     -- will be filled in (except if we're debugging)

-           ; env'     <- case mb_env_ty of

-                           Just env_ty -> return env_ty

-                           Nothing     -> do { massert dumping; return env_tv }

-           ; let -- See Note [Splitting nested sigma types in mismatched

-                 --           function types]

-                 (_, _, fun_tau) = tcSplitNestedSigmaTys fun_res_ty

-                 (_, _, env_tau) = tcSplitNestedSigmaTys env'

-                     -- env_ty is an ExpRhoTy, but with simple subsumption it

-                     -- is not deeply skolemised, so still use tcSplitNestedSigmaTys

-                 (args_fun, res_fun) = tcSplitFunTys fun_tau

-                 (args_env, res_env) = tcSplitFunTys env_tau

-                 info =

-                  FunResCtxt fun (count isValArg args) res_fun res_env

-                    (length args_fun) (length args_env)

-           ; return info }

-

-  | FunResCtxt !(HsExpr GhcTc) !Int !Type !Type !Int !Int

-  mkCheckExpType,

-  tcWrapResult, tcWrapResultO, tcWrapResultMono,

-  tcSubType, tcSubTypeSigma, tcSubTypePat, tcSubTypeDS, tcSubTypeHoleFit,

-  addSubTypeCtxt,

-  tcSubTypeAmbiguity, tcSubMult,

-import GHC.Types.Id( idType, isDataConId )

-import GHC.Types.SrcLoc (unLoc, GenLocated (..))

-fillInferResult :: DeepSubsumptionFlag -> CtOrigin -> TcType -> InferResult -> TcM HsWrapper

--- | A version of 'tcWrapResult' to use when the actual type is a

--- rho-type, so nothing to instantiate; just go straight to unify.

--- It means we don't need to pass in a CtOrigin.

-tcWrapResultMono :: HasDebugCallStack

-                 => HsExpr GhcRn -> HsExpr GhcTc

-                 -> TcRhoType   -- ^ Actual; a rho-type, not a sigma-type

-                 -> ExpRhoType  -- ^ Expected

-                 -> TcM (HsExpr GhcTc)

-tcWrapResultMono rn_expr expr act_ty res_ty

-  = do { co <- tcSubTypeMono rn_expr act_ty res_ty

-       ; return (mkHsWrapCo co expr) }

-tcSubTypePat inst_orig ctxt (Check ty_actual) ty_expected

-  = tc_sub_type unifyTypeET inst_orig ctxt ty_actual ty_expected

-

-tcSubTypePat _ _ (Infer inf_res) ty_expected

-  = do { co <- fillInferResultNoInst ty_expected inf_res

-               -- In patterns we do not instantatiate

-

-       ; return (mkWpCastN (mkSymCo co)) }

-

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

--- | A subtype check that performs deep subsumption.

--- See also 'tcSubTypeMono', for when no instantiation is required.

-tcSubTypeDS :: HsExpr GhcTc -- ^ App head (for error messages only)

-            -> DeepSubsumptionDepth

-            -> HsExpr GhcRn

-            -> TcRhoType   -- ^ Actual type; a rho-type, not a sigma-type

-            -> TcRhoType   -- ^ Expected type

-                           -- DeepSubsumption <=> when checking, this type

-                           --                     is deeply skolemised

-            -> TcM HsWrapper

--- Only one call site, in GHC.Tc.Gen.App.checkResultTy

-tcSubTypeDS tc_fun ds_depth rn_expr act_rho exp_rho

-  = do { wrap <- tc_sub_type_deep (Just tc_fun, Top) ds_depth

-                   (unifyExprType rn_expr)

-                   (exprCtOrigin rn_expr)

-                   GenSigCtxt act_rho exp_rho

-       ; return (mkWpSubType wrap) }

-

-  = case res_ty of

-      Check ty_expected -> tc_sub_type (unifyType m_thing) inst_orig ctxt

-                                       ty_actual ty_expected

-      Infer inf_res ->

-        do { ds_flag <- getDeepSubsumptionFlag

-           ; fillInferResult ds_flag inst_orig ty_actual inf_res }

-  = tc_sub_type (unifyType Nothing) orig ctxt ty_actual ty_expected

-tcSubTypeHoleFit ds_flag orig cand_ty hole_ty =

-  tc_sub_type_ds (Nothing, Top) ds_flag (unifyType Nothing)

-    orig (ExprSigCtxt NoRRC) cand_ty hole_ty

-  = tc_sub_type_ds (Nothing, Top)

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

-tc_sub_type :: (TcType -> TcType -> TcM TcCoercionN)  -- How to unify

-            -> CtOrigin       -- Used when instantiating

-            -> UserTypeCtxt   -- Used when skolemising

-            -> TcSigmaType    -- Actual; a sigma-type

-            -> TcSigmaType    -- Expected; also a sigma-type

-            -> TcM HsWrapper

--- Checks that actual_ty is more polymorphic than expected_ty

--- If wrap = tc_sub_type t1 t2

---    => wrap :: t1 ~~> t2

---

--- The "how to unify argument" is always a call to `uType TypeLevel orig`,

--- but with different ways of constructing the CtOrigin `orig` from

--- the argument types and context.

-

-tc_sub_type unify inst_orig ctxt ty_actual ty_expected

-  = do { ds_flag <- getDeepSubsumptionFlag

-       ; wrap <- tc_sub_type_ds (Nothing, Top) ds_flag unify inst_orig ctxt ty_actual ty_expected

--- tc_sub_type_ds is the main subsumption worker function

--- It takes an explicit DeepSubsumptionFlag

-4. In GHC.Tc.Gen.App.tcApp we call tcSubTypeDS to match the result

-   type. Without deep subsumption, tcSubTypeMono would be sufficent.

-  do { ds <- xoptM LangExt.DeepSubsumption

-     ; if ds

-getDeepSubsumptionFlag_DataConHead app_head =

-  do { user_ds <- xoptM LangExt.DeepSubsumption

-     ; traceTc "getDeepSubsumptionFlag_DataConHead" (ppr app_head)

-     ; return $

-         if | user_ds

-            -> Deep DeepSub

-            | otherwise

-            -> go app_head

-     }

-    go :: HsExpr GhcTc -> DeepSubsumptionFlag

-    go app_head

-     | XExpr (ConLikeTc (RealDataCon {})) <- app_head

-     = Deep TopSub

-     | XExpr (ExpandedThingTc (HSE _ (L _ f))) <- app_head

-     = go f

-     | XExpr (WrapExpr _ f) <- app_head

-     = go f

-     | HsVar _ f <- app_head

-     , isDataConId (unLoc f)

-     = Deep TopSub

-     | HsApp _ f _ <- app_head

-     = go (unLoc f)

-     | HsAppType _ f _ <- app_head

-     = go (unLoc f)

-     | OpApp _ _ f _ <- app_head

-     = go (unLoc f)

-     | HsPar _ f <- app_head

-     = go (unLoc f)

-     | otherwise

-     = Shallow

-

-  = go init_subst ty

-           ; arg_tys <- traverse oneToMeta arg_tys

-    oneToMeta (Scaled OneTy ty)

-      = do { mu <- newMultiplicityVar

-           ; return $ Scaled mu ty }

-    oneToMeta ty = return ty

-zonkTidyHsCtxt env (FunResCtxt e i1 ty1 ty2 i2 i3) = do

-  (env', ty1') <- zonkTidyTcType env ty1

-  (env', ty2') <- zonkTidyTcType env' ty2

-  return $ (env', FunResCtxt e i1 ty1' ty2' i2 i3)

-  (env', res_ty') <-

-    case res_ty of

-      Check ty -> zonkTidyTcType env' ty

-      Infer (IR {ir_ref = ref}) -> do -- inlining readExpTyp_maybe to avoid module dep loops

-        mb_ty <- liftIO $ readIORef ref

-        case mb_ty of

-          Nothing -> error "zonkTidyHsCtxt PatSigErrCtxt"

-          Just ty -> zonkTidyTcType env' ty

-  return (env', PatSigErrCtxt sig_ty' (Check res_ty'))