= tc1 == tc2 && tcEqTyConAppArgs args1 args2

 tcEqTyConAppArgs :: [Type] -> [Type] -> Bool

 tcEqTyConAppArgs args1 args2

   = and (zipWith tcEqTypeNoKindCheck args1 args2)

     -- No kind check necessary: if both arguments are well typed, then

 can reduce to Double. So, it had better be the case that (F blah blah) can

 reduce to Double, no matter what (blah) is!

 * When we attempt to unify (G Float) ~ Int, we return MaybeApart..

 * When we later encounter (G Float) ~ Bool, we apply the family substitution,

   very much as we apply the conventional [tyvar :-> type] substitution

   `uVarOrFam`.

   So (G Float ~ Bool) becomes (Int ~ Bool) which is SurelyApart.  Bingo.

    alternative path.  So `noMatchableGivenDicts` must return False;

    so `mightMatchLater` must return False; so when um_bind_fam_fun returns

    `DontBindMe`, the unifier must return `SurelyApart`, not `MaybeApart`.  See

 (ATF6) When /matching/ can we ever have a type-family application on the LHS, in

    the template?  You might think not, because type-class-instance and

 (ATF12) There is a horrid exception for the injectivity check. See (UR1) in

   in Note [Specification of unification].

 SIDE NOTE.  The paper "Closed type families with overlapping equations"

 http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/axioms-extended.pdf

 tries to achieve the same effect with a standard yes/no unifier, by "flattening"

     a a   ~    (Var A) (Var B)

 is SurelyApart, so the first equation definitely doesn't match and we can try the

 second, which does.  END OF SIDE NOTE.

 -}

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

 -- Why saturated?  See (ATF4) in Note [Apartness and type families]

 uVarOrFam env ty1 ty2 kco

   = do { substs <- getSubstEnvs

        ; go NotSwapped substs ty1 ty2 kco }

   where

     -- `go` takes two bites at the cherry; if the first one fails

     -- E.g.    a ~ F p q

     --         Starts with: go a (F p q)

     --         if `a` not bindable, swap to: go (F p q) a

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

     -- The sequence of tests is very similar to go_tv

       | Just ty1' <- lookupVarEnv (um_tv_env substs) tv1'

       = -- We already have a substitution for tv1

         if | um_unif env                          -> unify_ty env ty1' ty2 kco

       where

         tv1'            = umRnOccL env tv1

         ty2_fvs         = tyCoVarsOfType ty2

         rhs             = ty2 `mkCastTy` mkSymCo kco

                           -- tv1' is not forall-bound, but tv1 can still differ

                           -- from tv1; see Note [Cloning the template binders]

                           -- in GHC.Core.Rules.  So give tv1' to um_bind_tv_fun.

                         | otherwise

                         = False

           -- Occurs check, only when unifying

           -- see Note [Infinitary substitutions]

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

     -- Invariant: ty2 is not a TyVarTy

       -- If we are under a forall, just give up and return MaybeApart

       -- see (ATF3) in Note [Apartness and type families]

       | not (isEmptyVarSet (um_foralls env))

       -- Check for equality  F tys1 ~ F tys2

       | Just (tc2, tys2) <- isSatFamApp ty2

       , tc1 == tc2

       -- Now check if we can bind the (F tys) to the RHS

       -- This can happen even when matching: see (ATF7)

       | BindMe <- um_bind_fam_fun env tc1 tys1 rhs

       -- Swap in case of (F a b) ~ (G c d e)

       -- Maybe um_bind_fam_fun is False of (F a b) but true of (G c d e)

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

     -- go_fam_fam: LHS and RHS are both saturated type-family applications,

     --             for the same type-family F

        -- Decompose (F tys1 ~ F tys2): (ATF9)

        -- Use injectivity information of F: (ATF10)

        -- But first bind the type-fam if poss: (ATF11)

        bind_fam_if_poss

          | not (um_unif env)  -- Not when matching (ATF11-1)

          = return ()

          | BindMe <- um_bind_fam_fun env tc tys1 rhs1

          | otherwise

          = return ()

        rhs2 = mkTyConApp tc tys1 `mkCastTy` kco

   where

 Suppose we try to unify (forall cv. t1) ~ (forall cv. t2).

 See Note [ForAllTy] in GHC.Core.TyCo.Rep.

 module GHC.Tc.Gen.App

        ( tcApp

        , tcExprPrag ) where

 import {-# SOURCE #-} GHC.Tc.Gen.Expr( tcPolyExpr )

 -}

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

 *                                                                      *

               Typechecking n-ary applications

 A "head" has three special cases (for which we can infer a polytype

 using tcInferAppHead_maybe); otherwise is just any old expression (for

 There is no special treatment for HsHole (HsVar ...), HsOverLit, etc, because

 we can't get a polytype from them.

        -- Step 2: Infer the type of `fun`, the head of the application

        ; (tc_fun, fun_sigma) <- tcInferAppHead fun

        ; let tc_head = (tc_fun, fun_ctxt)

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

        ; do_ql <- wantQuickLook rn_fun

        ; (inst_args, app_res_rho)

               <- setQLInstLevel do_ql $  -- See (TCAPP1) and (TCAPP2) in

                                          -- Note [tcApp: typechecking applications]

        ; case do_ql of

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

                                                    app_res_rho exp_res_ty

                          -- Step 4.2: typecheck the  arguments

                        ; tc_args <- tcValArgs NoQL inst_args

                          -- Step 4.3: wrap up

                        ; finishApp tc_head tc_args app_res_rho res_wrap }

                          -- Step 5.1: Take a quick look at the result type

                        ; quickLookResultType app_res_rho exp_res_ty

                          -- Step 5.2: typecheck the arguments, and monomorphise

                          --           any un-unified instantiation variables

                        ; tc_args <- tcValArgs DoQL inst_args

                          --           QuickLook instantiation variables in `app_res_rho`

                        ; app_res_rho <- liftZonkM $ zonkTcType app_res_rho

                          -- Step 5.4: subsumption check against the expected type

                        ; res_wrap <- checkResultTy rn_expr tc_head inst_args

                          -- Step 5.5: wrap up

                        ; finishApp tc_head tc_args app_res_rho res_wrap } }

               -> (HsExpr GhcTc, AppCtxt)  -- Head

               -> [HsExprArg p]            -- Arguments, just error messages

               -> TcRhoType  -- Inferred type of the application; zonked to

               -> ExpRhoType -- Expected type; this is deeply skolemised

               -> TcM HsWrapper

 checkResultTy rn_expr _fun _inst_args app_res_rho (Infer inf_res)

 checkResultTy rn_expr (tc_fun, fun_ctxt) inst_args app_res_rho (Check res_ty)

 -- Unify with expected type from the context

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

 tcInstFun :: QLFlag

                     --           so may return a sigma-type

                     --    |-inst returns a rho-type

           -> (HsExpr GhcTc, AppCtxt)

           -> TcSigmaType -> [HsExprArg 'TcpRn]

           -> TcM ( [HsExprArg 'TcpInst]

 -- This crucial function implements the |-inst judgement in Fig 4, plus the

 -- modification in Fig 5, of the QL paper:

 -- "A quick look at impredicativity" (ICFP'20).

           _               -> False

     inst_fun :: [HsExprArg 'TcpRn] -> ForAllTyFlag -> Bool

     inst_fun [] | inst_final  = isInvisibleForAllTyFlag

                 | otherwise   = const False

     inst_fun (EValArg {} : _) = isInvisibleForAllTyFlag

     inst_fun _                = isInferredForAllTyFlag

     do  { mult <- newMultiplicityVar

         ; ((co_fn, matches'), rhs_ty')

                  -- a fixed runtime rep. See #23176

                tcExtendBinderStack [TcIdBndr_ExpType name exp_ty NotTopLevel] $

                  -- We extend the error context even for a non-recursive

   = addErrCtxt (PatMonoBindsCtxt pat grhss) $

     do { mult <- tcMultAnnOnPatBind mult_ann

                           -- a fixed runtime rep. See #23176

                              tcGRHSsPat mult grhss exp_ty

             -- See Note [Typechecking pattern bindings]

         ; ((pat', nosig_mbis), pat_ty)

             <- addErrCtxt (PatMonoBindsCtxt pat grhss) $

                tcLetPat inst_sig_fun no_gen pat (Scaled mult exp_ty) $

                  -- The above inferred type get an unrestricted multiplicity. It may be

                  -- worth it to try and find a finer-grained multiplicity here

        ( tcCheckPolyExpr, tcCheckPolyExprNC,

          tcCheckMonoExpr, tcCheckMonoExprNC,

          tcMonoExpr, tcMonoExprNC,

          tcPolyLExpr, tcPolyExpr, tcExpr, tcPolyLExprSig,

          tcSyntaxOp, tcSyntaxOpGen, SyntaxOpType(..), synKnownType,

          tcCheckId,

 *                                                                      *

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

 tcInferRho, tcInferRhoNC :: LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)

 -- Infer a *rho*-type. The return type is always instantiated.

     addExprCtxt expr $  -- Note [Error contexts in generated code]

        ; return (L loc expr', rho) }

        ; return (L loc expr', rho) }

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

          ; return (Missing (Scaled mult arg_ty), arg_ty) }

   tc_infer_tup_arg i (Present x lexpr@(L l expr))

     = do { (expr', arg_ty) <- case boxity of

              Boxed   -> do { arg_ty <- newFlexiTyVarTy liftedTypeKind

                            ; L _ expr' <- tcCheckPolyExpr lexpr arg_ty

                            ; return (expr', arg_ty) }

 module GHC.Tc.Gen.Expr where

 import GHC.Hs              ( HsExpr, LHsExpr, SyntaxExprRn

                            , SyntaxExprTc )

                            , ExpType, ExpRhoType, ExpSigmaType )

 import GHC.Tc.Types        ( TcM )

 import GHC.Tc.Types.BasicTypes( TcCompleteSig )

 tcInferRho, tcInferRhoNC ::

           LHsExpr GhcRn -> TcM (LHsExpr GhcTc, TcRhoType)

 tcSyntaxOp :: CtOrigin

            -> SyntaxExprRn

            -> [SyntaxOpType]           -- ^ shape of syntax operator arguments

     do { mb_tc_fun <- tcInferAppHead_maybe fun

        ; case mb_tc_fun of

             Just (fun', fun_sigma) -> return (fun', fun_sigma)

 tcInferAppHead_maybe :: HsExpr GhcRn

                      -> TcM (Maybe (HsExpr GhcTc, TcSigmaType))

 -- | Infer the kind of a type and desugar. This is the "up" type-checker,

 -- as described in Note [Bidirectional type checking]

 tc_infer_hs_type :: TcTyMode -> HsType GhcRn -> TcM (TcType, TcKind)

 tc_infer_hs_type mode rn_ty

 {-

 Note [Typechecking HsCoreTys]

 checkExpKind _rn_ty ty ki (Infer cell) = do

   -- NB: do not instantiate.

   -- See Note [Do not always instantiate eagerly in types]

   pure (ty `mkCastTy` co)

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

         ; tcExtendIdEnv tup_ids $ do

         { ((stmts', (ret_op', tup_rets)), stmts_ty)

                    tcStmtsAndThen ctxt tcDoStmt stmts exp_ty $ \ inner_res_ty ->

                    do { tup_rets <- zipWithM tcCheckId tup_names

                                       (map mkCheckExpType tup_elt_tys)

                       ; return (ret_op', tup_rets) }

         ; ((_, mfix_op'), mfix_res_ty)

                tcSyntaxOp DoOrigin mfix_op

                           [synKnownType (mkVisFunTyMany tup_ty stmts_ty)] exp_ty $

                \ _ _ -> return ()

 tcApplicativeStmts ctxt pairs rhs_ty thing_inside

  = do { body_ty <- newFlexiTyVarTy liftedTypeKind

       ; let arity = length pairs

       ; exp_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind

       ; pat_tys <- replicateM arity $ newFlexiTyVarTy liftedTypeKind

       ; let fun_ty = mkVisFunTysMany pat_tys body_ty

 import GHC.Prelude

 import GHC.Hs

 import GHC.Hs.Syn.Type

            -> TcM a

            -> TcM ((LPat GhcTc, a), TcSigmaTypeFRR)

 tcInferPat frr_orig ctxt pat thing_inside

     tc_lpat (unrestricted exp_ty) penv pat thing_inside

  where

     penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt, pe_orig = PatOrigin }

          -- restriction need to be put in place, if any, for linear view

          -- patterns to desugar to type-correct Core.

          -- Expression must be a function

         ; let herald = ExpectedFunTyViewPat $ unLoc expr

         ; (expr_wrap1, Scaled _mult inf_arg_ty, inf_res_sigma)

                -- See Note [View patterns and polymorphism]

          -- Check that overall pattern is more polymorphic than arg type

         ; expr_wrap2 <- tc_sub_type penv (scaledThing pat_ty) inf_arg_ty

         ; pat_ty <- readExpType h_pat_ty

         ; let expr_wrap2' = mkWpFun expr_wrap2 idHsWrapper

                               (Scaled w pat_ty) inf_res_sigma

               expr_wrap = expr_wrap2' <.> expr_wrap1

         ; return $ (ViewPat pat_ty (mkLHsWrap expr_wrap expr') pat', res) }

 {- Note [View patterns and polymorphism]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

    pair :: forall a. Bool -> a -> forall b. b -> (a,b)

    f :: Int -> blah

 The expression (pair True) should have type

     pair True :: Int -> forall b. b -> (Int,b)

 so that it is ready to consume the incoming Int. It should be an

 Then, when taking that arrow apart we want to get a *sigma* type

 (forall b. b->(Int,b)), because that's what we want to bind 'x' to.

 Fortunately that's what matchActualFunTy returns anyway.

 -}

 -- Type signatures in patterns

                                      penv pats thing_inside

         ; pat_ty <- readExpType (scaledThing pat_ty)

         ; return (mkHsWrapPat coi

   TuplePat _ pats boxity -> do

         { let arity = length pats

 import GHC.Tc.Utils.Unify( checkConstraints, tcSubTypeSigma )

 import GHC.Tc.Zonk.Type

 import GHC.Tc.Gen.Expr

 import GHC.Tc.Utils.Monad

 import GHC.Tc.Gen.Export

 import GHC.Tc.Types.Evidence

     failIfErrsM ;

     -- Typecheck the expression

           <- captureTopConstraints $

              pushTcLevelM          $

     -- Generalise

     uniq <- newUnique ;

 (<.>) :: HsWrapper -> HsWrapper -> HsWrapper

 WpHole    <.> c         = c

 c         <.> WpHole    = c

   -- If we can represent the HsWrapper as a cast, try to do so: this may avoid

   -- unnecessary eta-expansion (see 'mkWpFun').

 c1        <.> c2        = c1 `WpCompose` c2

 -- | Smart constructor to create a 'WpFun' 'HsWrapper', which avoids introducing

   -- Expected types

   ExpType(..), ExpSigmaType, ExpRhoType,

   mkCheckExpType, newInferExpType, newInferExpTypeFRR,

   readExpType, readExpType_maybe, readScaledExpType,

   expTypeToType, scaledExpTypeToType,

   checkingExpType_maybe, checkingExpType,

 -- actual data definition is in GHC.Tc.Utils.TcType

   = do { th_lvl <- getThLevel