All saturated applications of funTyCon are represented with the FunTy constructor.

 See Note [Function type constructors and FunTy] in GHC.Builtin.Types.Prim

 Note [Bad unsafe coercion]

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

 -- Let

 lintRecBindings :: TopLevelFlag -> [(Id, CoreExpr)]

 lintRecBindings top_lvl pairs thing_inside

        ; return (a, ues) }

   where

     (bndrs, rhss) = unzip pairs

            ; lintLetBind top_lvl Recursive bndr' rhs rhs_ty

            ; return ue }

 lintLetBody loc bndrs body

   = do { (body_ty, body_ue) <- addLoc loc (lintCoreExpr body)

        ; mapM_ (lintJoinBndrType body_ty) bndrs

        ; return (body_ty, body_ue) }

 -- Binder's type, and the RHS, have already been linted

 -- This function checks other invariants

 lintLetBind top_lvl rec_flag binder rhs rhs_ty

 -- join point.

 --

 -- See Note [Checking StaticPtrs].

 -- NB: the Id can be Linted or not -- it's only used for

 --     its OccInfo and join-pointer-hood

 lintRhs bndr rhs

   where

     -- Allow occurrences of 'makeStatic' at the top-level but produce errors

     -- otherwise.

     go AllowAtTopLevel

       | (binders0, rhs') <- collectTyBinders rhs

       , Just (fun, t, info, e) <- collectMakeStaticArgs rhs'

 -- | Lint the RHS of a join point with expected join arity of @n@ (see Note

 -- [Join points] in "GHC.Core").

 lintJoinLams join_arity enforce rhs

   = go join_arity rhs

   where

 ************************************************************************

 -}

 -- If you edit this function, you may need to update the GHC formalism

 -- See Note [GHC Formalism]

        ; lintCoercion co

        ; lintRole co Representational (coercionRole co)

        ; checkValueType (typeKind to_ty) $

          text "target of cast" <+> quotes (ppr co)

        ; ensureEqTys from_ty expr_ty (mkCastErr expr co from_ty expr_ty)

 lintCoreExpr (Let (NonRec tv (Type ty)) body)

   | isTyVar tv

   =     -- See Note [Linting type lets]

                 -- Now extend the substitution so we

                 -- take advantage of it in the body

           lintCoreExpr body } }

 lintCoreExpr (Let (NonRec bndr rhs) body)

           -- See Note [Multiplicity of let binders] in Var

          -- Now lint the binder

   | otherwise

   = failWithL (mkLetErr bndr rhs)       -- Not quite accurate

           -- See Note [Multiplicity of let binders] in Var

         ; ((body_type, body_ue), ues) <-

         ; return (body_type, body_ue  `addUE` scaleUE ManyTy (foldr1WithDefault zeroUE addUE ues)) }

   where

     bndrs = map fst pairs

     -- N.B. we may have an over-saturated application of the form:

     --   runRW (\s -> \x -> ...) y

   , ty_arg1 : ty_arg2 : cont_arg : rest <- args

              lint_rw_cont expr@(Lam _ _) mult fun_ue

                 = do { (arg_ty, arg_ue) <- lintJoinLams 1 (Just fun) expr

                      ; let app_ue = addUE fun_ue (scaleUE mult arg_ue)

 lintCoreExpr (Coercion co)

   -- See Note [Coercions in terms]

   = do { addLoc (InCo co) $ lintCoercion co

        ; return (ty, zeroUE) }

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

                  -- See GHC.Core Note [Variable occurrences in Core]

           -- Check for a nested occurrence of the StaticPtr constructor.

           -- See Note [Checking StaticPtrs].

         ; when (nargs /= 0) $

           text "Found makeStatic nested in an expression"

              Nothing -> return ()

              Just dc -> checkTypeDataConOcc "expression" dc

 lintCoreFun :: CoreExpr

             -> Int                       -- Number of arguments (type or val) being passed

 lintCoreFun (Var var) nargs

   = lintIdOcc var nargs

 lintLambda :: Var -> LintM (Type, UsageEnv) -> LintM (Type, UsageEnv)

 lintLambda var lintBody =

     addLoc (LambdaBodyOf var) $

     do { (body_ty, ue) <- lintBody

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

 checkDeadIdOcc :: Id -> LintM ()

 -- Occurrences of an Id should never be dead....

   = return ()

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

                  -> LintM ()

 -- Checks that the return type of a join Id matches the body

 -- E.g. join j x = rhs in body

 -- Takes the functions type and arguments as argument.

 -- Returns the *result* of applying the function to arguments.

 -- e.g. f :: Int -> Bool -> Int would return `Int` as result type.

 lintCoreArgs (fun_ty, fun_ue) args

   = lintApp (text "expression")

               lintTyArg lintValArg fun_ty args fun_ue

 -- Type argument

 lintTyArg (Type arg_ty)

   = do { checkL (not (isCoercionTy arg_ty))

                 (text "Unnecessary coercion-to-type injection:"

                   <+> ppr arg_ty)

 lintTyArg arg

   = failWithL (hang (text "Expected type argument but found") 2 (ppr arg))

 lintValArg arg mult fun_ue

   = do { (arg_ty, arg_ue) <- markAllJoinsBad $ lintCoreExpr arg

            -- See Note [Representation polymorphism invariants] in GHC.Core

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

 lintAltBinders :: UsageEnv

                -> Var         -- Case binder

                -> [(Mult, OutVar)]    -- Binders

                -> LintM UsageEnv

 -- If you edit this function, you may need to update the GHC formalism

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

 lintTyApp fun_ty arg_ty

   | Just (tv,body_ty) <- splitForAllTyVar_maybe fun_ty

   = do  { lintTyKind tv arg_ty

 -- | @lintValApp arg fun_ty arg_ty@ lints an application of @fun arg@

 -- where @fun :: fun_ty@ and @arg :: arg_ty@, returning the type of the

 -- application.

 lintValApp arg fun_ty arg_ty fun_ue arg_ue

   | Just (_, w, arg_ty', res_ty') <- splitFunTy_maybe fun_ty

   = do { ensureEqTys arg_ty' arg_ty (mkAppMsg arg_ty' arg_ty arg)

   where

     err2 = mkNonFunAppMsg fun_ty arg_ty arg

 -- Both args have had substitution applied

 -- If you edit this function, you may need to update the GHC formalism

 ************************************************************************

 -}

 lintCaseExpr scrut case_bndr alt_ty alts

   = do { let e = Case scrut case_bndr alt_ty alts   -- Just for error messages

        -- Check the scrutinee

             -- See Note [Join points are less general than the paper]

             -- in GHC.Core

        -- Lint the case-binder. Must do this after linting the scrutinee

        -- because the case-binder isn't in scope in the scrutineex

       -- Don't use lintIdBndr on case_bndr, because unboxed tuple is legitimate

          -- See GHC.Core Note [Case expression invariants] item (7)

        ; -- Check the alternatives

        ; let case_ue = (scaleUE scrut_mult scrut_ue) `addUE` supUEs alt_ues

 -- a) Check that the alts are non-empty

 -- b1) Check that the DEFAULT comes first, if it exists

 -- b2) Check that the others are in increasing order

     is_lit_alt (Alt (LitAlt _) _  _) = True

     is_lit_alt _                     = False

 lintAltExpr expr ann_ty

   = do { (actual_ty, ue) <- lintCoreExpr expr

        ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty)

        ; return ue }

          -- See GHC.Core Note [Case expression invariants] item (6)

             -> Mult          -- Multiplicity of scrutinee

             -> CoreAlt

             -> LintM UsageEnv

 -- If you edit this function, you may need to update the GHC formalism

           ; multiplicities = map binderMult $ fst $ splitPiTys con_payload_ty }

         -- And now bring the new binders into scope

       { rhs_ue <- lintAltExpr rhs alt_ty

       ; rhs_ue' <- addLoc (CasePat alt) $

                    lintAltBinders rhs_ue case_bndr scrut_ty con_payload_ty

       ; return $ deleteUE rhs_ue' case_bndr

       }

    }

 --  1. Lint var types or kinds (possibly substituting)

 --  2. Add the binder to the in scope set, and if its a coercion var,

 --     we may extend the substitution to reflect its (possibly) new kind

 -- If you edit this function, you may need to update the GHC formalism

 -- See Note [GHC Formalism]

 lintBinder site var linterF

   | isTyCoVar var = lintTyCoBndr var linterF

   | otherwise     = lintIdBndr NotTopLevel site var linterF

 lintTyCoBndr tcv thing_inside

          -- See (FORALL1) and (FORALL2) in GHC.Core.Type

        ; if (isTyVar tcv)

          then -- Check that in (forall (a:ki). blah) we have ki:Type

               hang (text "TyVar whose kind does not have kind Type:")

          else -- Check that in (forall (cv::ty). blah),

               -- then ty looks like (t1 ~# t2)

               text "CoVar with non-coercion type:" <+> pprTyVar tcv

 lintIdBndrs top_lvl ids thing_inside

   = go ids thing_inside

   where

 lintIdBndr :: TopLevelFlag -> BindingSite

 -- Do substitution on the type of a binder and add the var with this

 -- new type to the in-scope set of the second argument

 -- ToDo: lint its rules

        ; lintL (not (bind_site == LambdaBind && isEvaldUnfolding (idUnfolding id)))

                 (text "Lambda binder with value or OtherCon unfolding.")

   where

     id_ty = idType id

 {- Note [Linting types and coercions]

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

 Notice that

 Neither returns anything.

 If you need the kind of the type, then do `typeKind` and then apply

 Note: you might wonder if we should apply the same logic to expressions.

 Why do we have

 Partly inertia; but also taking the type of an expresison involve looking

 down a deep chain of let's, whereas that is not true of taking the kind

 of a type.  It'd be worth an experiment though.

 Historical note: in the olden days we had

 often discarded, or used only to get its kind.

 I also experimented with

 but that too was slower.  It is also much simpler to return ()!  If we

 return the kind we have to duplicate the logic in `typeKind`; and it is

 much worse for coercions.

 -}

 -- Types only, not kinds

 -- Check the type, and apply the substitution to it

 -- See Note [Linting type lets]

 lintValueType ty

   = addLoc (InType ty) $

         ; lintL (isTYPEorCONSTRAINT sk) $

           hang (text "Ill-kinded type:" <+> ppr ty)

 checkTyCon :: TyCon -> LintM ()

 checkTyCon tc

   = checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)

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

 -- See Note [Linting types and coercions]

 --

 -- If you edit this function, you may need to update the GHC formalism

   = failWithL (mkBadTyVarMsg tv)

   | otherwise

 lintType ty@(AppTy t1 t2)

   | TyConApp {} <- t1

   | otherwise

   = do { let (fun_ty, arg_tys) = collect t1 [t2]

        ; lintType fun_ty

        ; lint_ty_app ty fun_kind arg_tys }

   where

     collect (AppTy f a) as = collect f (a:as)

 lintType ty@(ForAllTy {})

   = go [] ty

   where

     -- Loop, collecting the forall-binders

     go tcvs ty@(ForAllTy (Bndr tcv _) body_ty)

       | not (isTyCoVar tcv)

       = failWithL (text "Non-TyVar or Non-CoVar bound in type:" <+> ppr ty)

       | otherwise

         do { -- See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]

              -- Suspicious because it works on InTyCoVar; c.f. ForAllCo

              when (isCoVar tcv) $

              lintL (anyFreeVarsOfType (== tcv) body_ty) $

              text "Covar does not occur in the body:" <+> (ppr tcv $$ ppr body_ty)

     go tcvs body_ty

       = do { lintType body_ty

 lintType (CastTy ty co)

   = do { lintType ty

        ; co_lk <- lintStarCoercion co

        ; ensureEqTys ty_kind co_lk (mkCastTyErr ty co ty_kind co_lk) }

 lintType (CoercionTy co) = lintCoercion co

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

 -- Do the checks for the body of a forall-type

 lintForAllBody tcvs body_ty

   = do { -- For type variables, check for skolem escape

          -- See Note [Phantom type variables in kinds] in GHC.Core.Type

          -- The kind of (forall cv. th) is liftedTypeKind, so no

          -- need to check for skolem-escape in the CoVar case

        ; case occCheckExpand tcvs body_kind of

            Just {} -> return ()

            Nothing -> failWithL $

        ; checkValueType body_kind (text "the body of forall:" <+> ppr body_ty) }

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

 -- The TyCon is a type synonym or a type family (not a data family)

 -- See Note [Linting type synonym applications]

 -- c.f. GHC.Tc.Validity.check_syn_tc_app

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

 -- Confirms that a kind is really TYPE r or Constraint

 checkValueType kind doc

   = lintL (isTYPEorCONSTRAINT kind)

           (text "Non-Type-like kind when Type-like expected:" <+> ppr kind $$

            text "when checking" <+> doc)

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

 -- If you edit this function, you may need to update the GHC formalism

 -- See Note [GHC Formalism]

 lintArrow what af t1 t2 tw  -- Eg lintArrow "type or kind `blah'" k1 k2 kw

                             -- or lintArrow "coercion `blah'" k1 k2 kw

        ; unless (isTYPEorCONSTRAINT k1) (report (text "argument")     t1 k1)

        ; unless (isTYPEorCONSTRAINT k2) (report (text "result")       t2 k2)

        ; unless (isMultiplicityTy kw)   (report (text "multiplicity") tw kw)

 lintTyLit (CharTyLit _) = return ()

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

 lint_ty_app ty = lint_tyco_app (text "type" <+> quotes (ppr ty))

 lint_co_app co = lint_tyco_app (text "coercion" <+> quotes (ppr co))

 lint_tyco_app msg fun_kind arg_tys

     -- See Note [Avoiding compiler perf traps when constructing error messages.]