{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1993-1998


A ``lint'' pass to check for Core correctness.
See Note [Core Lint guarantee].
-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}

module CoreLint (
    lintCoreBindings, lintUnfolding,
    lintPassResult, lintInteractiveExpr, lintExpr,
    lintAnnots, lintTypes,

    -- ** Debug output
    endPass, endPassIO,
    dumpPassResult,
    CoreLint.dumpIfSet,
 ) where

#include "HsVersions.h"

import GhcPrelude

import CoreSyn
import CoreFVs
import CoreUtils
import CoreStats   ( coreBindsStats )
import CoreMonad
import Bag
import Literal
import DataCon
import TysWiredIn
import TysPrim
import TcType ( isFloatingTy )
import Var
import VarEnv
import VarSet
import Name
import Id
import IdInfo
import PprCore
import ErrUtils
import Coercion
import SrcLoc
import Type
import RepType
import TyCoRep       -- checks validity of types/coercions
import TyCoSubst
import TyCoFVs
import TyCoPpr ( pprTyVar )
import TyCon
import CoAxiom
import BasicTypes
import ErrUtils as Err
import ListSetOps
import PrelNames
import Outputable
import FastString
import Util
import InstEnv     ( instanceDFunId )
import OptCoercion ( checkAxInstCo )
import CoreArity ( typeArity )
import Demand ( splitStrictSig, isBotRes )

import HscTypes
import DynFlags
import Control.Monad
import qualified Control.Monad.Fail as MonadFail
import MonadUtils
import Data.Foldable      ( toList )
import Data.List.NonEmpty ( NonEmpty )
import Data.Maybe
import Pair
import qualified GHC.LanguageExtensions as LangExt

{-
Note [Core Lint guarantee]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Core Lint is the type-checker for Core. Using it, we get the following guarantee:

If all of:
1. Core Lint passes,
2. there are no unsafe coercions (i.e. UnsafeCoerceProv),
3. all plugin-supplied coercions (i.e. PluginProv) are valid, and
4. all case-matches are complete
then running the compiled program will not seg-fault, assuming no bugs downstream
(e.g. in the code generator). This guarantee is quite powerful, in that it allows us
to decouple the safety of the resulting program from the type inference algorithm.

However, do note point (4) above. Core Lint does not check for incomplete case-matches;
see Note [Case expression invariants] in CoreSyn, invariant (4). As explained there,
an incomplete case-match might slip by Core Lint and cause trouble at runtime.

Note [GHC Formalism]
~~~~~~~~~~~~~~~~~~~~
This file implements the type-checking algorithm for System FC, the "official"
name of the Core language. Type safety of FC is heart of the claim that
executables produced by GHC do not have segmentation faults. Thus, it is
useful to be able to reason about System FC independently of reading the code.
To this purpose, there is a document core-spec.pdf built in docs/core-spec that
contains a formalism of the types and functions dealt with here. If you change
just about anything in this file or you change other types/functions throughout
the Core language (all signposted to this note), you should update that
formalism. See docs/core-spec/README for more info about how to do so.

Note [check vs lint]
~~~~~~~~~~~~~~~~~~~~
This file implements both a type checking algorithm and also general sanity
checking. For example, the "sanity checking" checks for TyConApp on the left
of an AppTy, which should never happen. These sanity checks don't really
affect any notion of type soundness. Yet, it is convenient to do the sanity
checks at the same time as the type checks. So, we use the following naming
convention:

- Functions that begin with 'lint'... are involved in type checking. These
  functions might also do some sanity checking.

- Functions that begin with 'check'... are *not* involved in type checking.
  They exist only for sanity checking.

Issues surrounding variable naming, shadowing, and such are considered *not*
to be part of type checking, as the formalism omits these details.

Summary of checks
~~~~~~~~~~~~~~~~~
Checks that a set of core bindings is well-formed.  The PprStyle and String
just control what we print in the event of an error.  The Bool value
indicates whether we have done any specialisation yet (in which case we do
some extra checks).

We check for
        (a) type errors
        (b) Out-of-scope type variables
        (c) Out-of-scope local variables
        (d) Ill-kinded types
        (e) Incorrect unsafe coercions

If we have done specialisation the we check that there are
        (a) No top-level bindings of primitive (unboxed type)

Outstanding issues:

    -- Things are *not* OK if:
    --
    --  * Unsaturated type app before specialisation has been done;
    --
    --  * Oversaturated type app after specialisation (eta reduction
    --   may well be happening...);


Note [Linting function types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As described in Note [Representation of function types], all saturated
applications of funTyCon are represented with the FunTy constructor. We check
this invariant in lintType.

Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
In the desugarer, it's very very convenient to be able to say (in effect)
        let a = Type Int in <body>
That is, use a type let.   See Note [Type let] in CoreSyn.

However, when linting <body> we need to remember that a=Int, else we might
reject a correct program.  So we carry a type substitution (in this example
[a -> Int]) and apply this substitution before comparing types.  The functin
        lintInTy :: Type -> LintM (Type, Kind)
returns a substituted type.

When we encounter a binder (like x::a) we must apply the substitution
to the type of the binding variable.  lintBinders does this.

For Ids, the type-substituted Id is added to the in_scope set (which
itself is part of the TCvSubst we are carrying down), and when we
find an occurrence of an Id, we fetch it from the in-scope set.

Note [Bad unsafe coercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~
For discussion see https://gitlab.haskell.org/ghc/ghc/wikis/bad-unsafe-coercions
Linter introduces additional rules that checks improper coercion between
different types, called bad coercions. Following coercions are forbidden:

  (a) coercions between boxed and unboxed values;
  (b) coercions between unlifted values of the different sizes, here
      active size is checked, i.e. size of the actual value but not
      the space allocated for value;
  (c) coercions between floating and integral boxed values, this check
      is not yet supported for unboxed tuples, as no semantics were
      specified for that;
  (d) coercions from / to vector type
  (e) If types are unboxed tuples then tuple (# A_1,..,A_n #) can be
      coerced to (# B_1,..,B_m #) if n=m and for each pair A_i, B_i rules
      (a-e) holds.

Note [Join points]
~~~~~~~~~~~~~~~~~~
We check the rules listed in Note [Invariants on join points] in CoreSyn. The
only one that causes any difficulty is the first: All occurrences must be tail
calls. To this end, along with the in-scope set, we remember in le_joins the
subset of in-scope Ids that are valid join ids. For example:

  join j x = ... in
  case e of
    A -> jump j y -- good
    B -> case (jump j z) of -- BAD
           C -> join h = jump j w in ... -- good
           D -> let x = jump j v in ... -- BAD

A join point remains valid in case branches, so when checking the A
branch, j is still valid. When we check the scrutinee of the inner
case, however, we set le_joins to empty, and catch the
error. Similarly, join points can occur free in RHSes of other join
points but not the RHSes of value bindings (thunks and functions).

************************************************************************
*                                                                      *
                 Beginning and ending passes
*                                                                      *
************************************************************************

These functions are not CoreM monad stuff, but they probably ought to
be, and it makes a convenient place for them.  They print out stuff
before and after core passes, and do Core Lint when necessary.
-}

endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
endPass CoreToDo
pass CoreProgram
binds [CoreRule]
rules
  = do { HscEnv
hsc_env <- CoreM HscEnv
getHscEnv
       ; PrintUnqualified
print_unqual <- CoreM PrintUnqualified
getPrintUnqualified
       ; IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ HscEnv
-> PrintUnqualified
-> CoreToDo
-> CoreProgram
-> [CoreRule]
-> IO ()
endPassIO HscEnv
hsc_env PrintUnqualified
print_unqual CoreToDo
pass CoreProgram
binds [CoreRule]
rules }

endPassIO :: HscEnv -> PrintUnqualified
          -> CoreToDo -> CoreProgram -> [CoreRule] -> IO ()
-- Used by the IO-is CorePrep too
endPassIO :: HscEnv
-> PrintUnqualified
-> CoreToDo
-> CoreProgram
-> [CoreRule]
-> IO ()
endPassIO HscEnv
hsc_env PrintUnqualified
print_unqual CoreToDo
pass CoreProgram
binds [CoreRule]
rules
  = do { DynFlags
-> PrintUnqualified
-> Maybe DumpFlag
-> SDoc
-> SDoc
-> CoreProgram
-> [CoreRule]
-> IO ()
dumpPassResult DynFlags
dflags PrintUnqualified
print_unqual Maybe DumpFlag
mb_flag
                        (CoreToDo -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreToDo
pass) (CoreToDo -> SDoc
pprPassDetails CoreToDo
pass) CoreProgram
binds [CoreRule]
rules
       ; HscEnv -> CoreToDo -> CoreProgram -> IO ()
lintPassResult HscEnv
hsc_env CoreToDo
pass CoreProgram
binds }
  where
    dflags :: DynFlags
dflags  = HscEnv -> DynFlags
hsc_dflags HscEnv
hsc_env
    mb_flag :: Maybe DumpFlag
mb_flag = case CoreToDo -> Maybe DumpFlag
coreDumpFlag CoreToDo
pass of
                Just DumpFlag
flag | DumpFlag -> DynFlags -> Bool
dopt DumpFlag
flag DynFlags
dflags                    -> DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
flag
                          | DumpFlag -> DynFlags -> Bool
dopt DumpFlag
Opt_D_verbose_core2core DynFlags
dflags -> DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
flag
                Maybe DumpFlag
_ -> Maybe DumpFlag
forall a. Maybe a
Nothing

dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
dumpIfSet DynFlags
dflags Bool
dump_me CoreToDo
pass SDoc
extra_info SDoc
doc
  = DynFlags -> Bool -> String -> SDoc -> IO ()
Err.dumpIfSet DynFlags
dflags Bool
dump_me (DynFlags -> SDoc -> String
showSDoc DynFlags
dflags (CoreToDo -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreToDo
pass SDoc -> SDoc -> SDoc
<+> SDoc
extra_info)) SDoc
doc

dumpPassResult :: DynFlags
               -> PrintUnqualified
               -> Maybe DumpFlag        -- Just df => show details in a file whose
                                        --            name is specified by df
               -> SDoc                  -- Header
               -> SDoc                  -- Extra info to appear after header
               -> CoreProgram -> [CoreRule]
               -> IO ()
dumpPassResult :: DynFlags
-> PrintUnqualified
-> Maybe DumpFlag
-> SDoc
-> SDoc
-> CoreProgram
-> [CoreRule]
-> IO ()
dumpPassResult DynFlags
dflags PrintUnqualified
unqual Maybe DumpFlag
mb_flag SDoc
hdr SDoc
extra_info CoreProgram
binds [CoreRule]
rules
  = do { Maybe DumpFlag -> (DumpFlag -> IO ()) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Maybe DumpFlag
mb_flag ((DumpFlag -> IO ()) -> IO ()) -> (DumpFlag -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \DumpFlag
flag ->
           DynFlags -> PrintUnqualified -> DumpFlag -> String -> SDoc -> IO ()
Err.dumpSDoc DynFlags
dflags PrintUnqualified
unqual DumpFlag
flag (DynFlags -> SDoc -> String
showSDoc DynFlags
dflags SDoc
hdr) SDoc
dump_doc

         -- Report result size
         -- This has the side effect of forcing the intermediate to be evaluated
         -- if it's not already forced by a -ddump flag.
       ; DynFlags -> Int -> SDoc -> IO ()
Err.debugTraceMsg DynFlags
dflags Int
2 SDoc
size_doc
       }

  where
    size_doc :: SDoc
size_doc = [SDoc] -> SDoc
sep [String -> SDoc
text String
"Result size of" SDoc -> SDoc -> SDoc
<+> SDoc
hdr, Int -> SDoc -> SDoc
nest Int
2 (SDoc
equals SDoc -> SDoc -> SDoc
<+> CoreStats -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoreProgram -> CoreStats
coreBindsStats CoreProgram
binds))]

    dump_doc :: SDoc
dump_doc  = [SDoc] -> SDoc
vcat [ Int -> SDoc -> SDoc
nest Int
2 SDoc
extra_info
                     , SDoc
size_doc
                     , SDoc
blankLine
                     , CoreProgram -> SDoc
pprCoreBindingsWithSize CoreProgram
binds
                     , Bool -> SDoc -> SDoc
ppUnless ([CoreRule] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoreRule]
rules) SDoc
pp_rules ]
    pp_rules :: SDoc
pp_rules = [SDoc] -> SDoc
vcat [ SDoc
blankLine
                    , String -> SDoc
text String
"------ Local rules for imported ids --------"
                    , [CoreRule] -> SDoc
pprRules [CoreRule]
rules ]

coreDumpFlag :: CoreToDo -> Maybe DumpFlag
coreDumpFlag :: CoreToDo -> Maybe DumpFlag
coreDumpFlag (CoreDoSimplify {})      = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag (CoreDoPluginPass {})    = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag CoreToDo
CoreDoFloatInwards       = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag (CoreDoFloatOutwards {}) = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag CoreToDo
CoreLiberateCase         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag CoreToDo
CoreDoStaticArgs         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag CoreToDo
CoreDoCallArity          = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_call_arity
coreDumpFlag CoreToDo
CoreDoExitify            = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_exitify
coreDumpFlag CoreToDo
CoreDoStrictness         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_stranal
coreDumpFlag CoreToDo
CoreDoWorkerWrapper      = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_worker_wrapper
coreDumpFlag CoreToDo
CoreDoSpecialising       = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_spec
coreDumpFlag CoreToDo
CoreDoSpecConstr         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_spec
coreDumpFlag CoreToDo
CoreCSE                  = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_cse
coreDumpFlag CoreToDo
CoreDesugar              = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_ds_preopt
coreDumpFlag CoreToDo
CoreDesugarOpt           = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_ds
coreDumpFlag CoreToDo
CoreTidy                 = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_simpl
coreDumpFlag CoreToDo
CorePrep                 = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_prep
coreDumpFlag CoreToDo
CoreOccurAnal            = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_occur_anal

coreDumpFlag CoreToDo
CoreDoPrintCore          = Maybe DumpFlag
forall a. Maybe a
Nothing
coreDumpFlag (CoreDoRuleCheck {})     = Maybe DumpFlag
forall a. Maybe a
Nothing
coreDumpFlag CoreToDo
CoreDoNothing            = Maybe DumpFlag
forall a. Maybe a
Nothing
coreDumpFlag (CoreDoPasses {})        = Maybe DumpFlag
forall a. Maybe a
Nothing

{-
************************************************************************
*                                                                      *
                 Top-level interfaces
*                                                                      *
************************************************************************
-}

lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
lintPassResult HscEnv
hsc_env CoreToDo
pass CoreProgram
binds
  | Bool -> Bool
not (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DoCoreLinting DynFlags
dflags)
  = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise
  = do { let (Bag SDoc
warns, Bag SDoc
errs) = DynFlags
-> CoreToDo -> [Var] -> CoreProgram -> (Bag SDoc, Bag SDoc)
lintCoreBindings DynFlags
dflags CoreToDo
pass (HscEnv -> [Var]
interactiveInScope HscEnv
hsc_env) CoreProgram
binds
       ; DynFlags -> String -> IO ()
Err.showPass DynFlags
dflags (String
"Core Linted result of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DynFlags -> CoreToDo -> String
forall a. Outputable a => DynFlags -> a -> String
showPpr DynFlags
dflags CoreToDo
pass)
       ; DynFlags
-> CoreToDo -> Bag SDoc -> Bag SDoc -> CoreProgram -> IO ()
displayLintResults DynFlags
dflags CoreToDo
pass Bag SDoc
warns Bag SDoc
errs CoreProgram
binds  }
  where
    dflags :: DynFlags
dflags = HscEnv -> DynFlags
hsc_dflags HscEnv
hsc_env

displayLintResults :: DynFlags -> CoreToDo
                   -> Bag Err.MsgDoc -> Bag Err.MsgDoc -> CoreProgram
                   -> IO ()
displayLintResults :: DynFlags
-> CoreToDo -> Bag SDoc -> Bag SDoc -> CoreProgram -> IO ()
displayLintResults DynFlags
dflags CoreToDo
pass Bag SDoc
warns Bag SDoc
errs CoreProgram
binds
  | Bool -> Bool
not (Bag SDoc -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag SDoc
errs)
  = do { DynFlags
-> WarnReason -> Severity -> SrcSpan -> PprStyle -> SDoc -> IO ()
putLogMsg DynFlags
dflags WarnReason
NoReason Severity
Err.SevDump SrcSpan
noSrcSpan
           (DynFlags -> PprStyle
defaultDumpStyle DynFlags
dflags)
           ([SDoc] -> SDoc
vcat [ String -> SDoc -> SDoc
lint_banner String
"errors" (CoreToDo -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreToDo
pass), Bag SDoc -> SDoc
Err.pprMessageBag Bag SDoc
errs
                 , String -> SDoc
text String
"*** Offending Program ***"
                 , CoreProgram -> SDoc
forall b. OutputableBndr b => [Bind b] -> SDoc
pprCoreBindings CoreProgram
binds
                 , String -> SDoc
text String
"*** End of Offense ***" ])
       ; DynFlags -> Int -> IO ()
Err.ghcExit DynFlags
dflags Int
1 }

  | Bool -> Bool
not (Bag SDoc -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag SDoc
warns)
  , Bool -> Bool
not (DynFlags -> Bool
hasNoDebugOutput DynFlags
dflags)
  , CoreToDo -> Bool
showLintWarnings CoreToDo
pass
  -- If the Core linter encounters an error, output to stderr instead of
  -- stdout (#13342)
  = DynFlags
-> WarnReason -> Severity -> SrcSpan -> PprStyle -> SDoc -> IO ()
putLogMsg DynFlags
dflags WarnReason
NoReason Severity
Err.SevInfo SrcSpan
noSrcSpan
        (DynFlags -> PprStyle
defaultDumpStyle DynFlags
dflags)
        (String -> SDoc -> SDoc
lint_banner String
"warnings" (CoreToDo -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreToDo
pass) SDoc -> SDoc -> SDoc
$$ Bag SDoc -> SDoc
Err.pprMessageBag ((SDoc -> SDoc) -> Bag SDoc -> Bag SDoc
forall a b. (a -> b) -> Bag a -> Bag b
mapBag (SDoc -> SDoc -> SDoc
$$ SDoc
blankLine) Bag SDoc
warns))

  | Bool
otherwise = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where

lint_banner :: String -> SDoc -> SDoc
lint_banner :: String -> SDoc -> SDoc
lint_banner String
string SDoc
pass = String -> SDoc
text String
"*** Core Lint"      SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
string
                          SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
": in result of" SDoc -> SDoc -> SDoc
<+> SDoc
pass
                          SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"***"

showLintWarnings :: CoreToDo -> Bool
-- Disable Lint warnings on the first simplifier pass, because
-- there may be some INLINE knots still tied, which is tiresomely noisy
showLintWarnings :: CoreToDo -> Bool
showLintWarnings (CoreDoSimplify Int
_ (SimplMode { sm_phase :: SimplMode -> CompilerPhase
sm_phase = CompilerPhase
InitialPhase })) = Bool
False
showLintWarnings CoreToDo
_ = Bool
True

lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
lintInteractiveExpr String
what HscEnv
hsc_env CoreExpr
expr
  | Bool -> Bool
not (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DoCoreLinting DynFlags
dflags)
  = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Just SDoc
err <- DynFlags -> [Var] -> CoreExpr -> Maybe SDoc
lintExpr DynFlags
dflags (HscEnv -> [Var]
interactiveInScope HscEnv
hsc_env) CoreExpr
expr
  = do { SDoc -> IO ()
display_lint_err SDoc
err
       ; DynFlags -> Int -> IO ()
Err.ghcExit DynFlags
dflags Int
1 }
  | Bool
otherwise
  = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    dflags :: DynFlags
dflags = HscEnv -> DynFlags
hsc_dflags HscEnv
hsc_env

    display_lint_err :: SDoc -> IO ()
display_lint_err SDoc
err
      = do { DynFlags
-> WarnReason -> Severity -> SrcSpan -> PprStyle -> SDoc -> IO ()
putLogMsg DynFlags
dflags WarnReason
NoReason Severity
Err.SevDump
               SrcSpan
noSrcSpan (DynFlags -> PprStyle
defaultDumpStyle DynFlags
dflags)
               ([SDoc] -> SDoc
vcat [ String -> SDoc -> SDoc
lint_banner String
"errors" (String -> SDoc
text String
what)
                     , SDoc
err
                     , String -> SDoc
text String
"*** Offending Program ***"
                     , CoreExpr -> SDoc
forall b. OutputableBndr b => Expr b -> SDoc
pprCoreExpr CoreExpr
expr
                     , String -> SDoc
text String
"*** End of Offense ***" ])
           ; DynFlags -> Int -> IO ()
Err.ghcExit DynFlags
dflags Int
1 }

interactiveInScope :: HscEnv -> [Var]
-- In GHCi we may lint expressions, or bindings arising from 'deriving'
-- clauses, that mention variables bound in the interactive context.
-- These are Local things (see Note [Interactively-bound Ids in GHCi] in HscTypes).
-- So we have to tell Lint about them, lest it reports them as out of scope.
--
-- We do this by find local-named things that may appear free in interactive
-- context.  This function is pretty revolting and quite possibly not quite right.
-- When we are not in GHCi, the interactive context (hsc_IC hsc_env) is empty
-- so this is a (cheap) no-op.
--
-- See #8215 for an example
interactiveInScope :: HscEnv -> [Var]
interactiveInScope HscEnv
hsc_env
  = [Var]
tyvars [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
ids
  where
    -- C.f. TcRnDriver.setInteractiveContext, Desugar.deSugarExpr
    ictxt :: InteractiveContext
ictxt                   = HscEnv -> InteractiveContext
hsc_IC HscEnv
hsc_env
    ([ClsInst]
cls_insts, [FamInst]
_fam_insts) = InteractiveContext -> ([ClsInst], [FamInst])
ic_instances InteractiveContext
ictxt
    te1 :: TypeEnv
te1    = [TyThing] -> TypeEnv
mkTypeEnvWithImplicits (InteractiveContext -> [TyThing]
ic_tythings InteractiveContext
ictxt)
    te :: TypeEnv
te     = TypeEnv -> [Var] -> TypeEnv
extendTypeEnvWithIds TypeEnv
te1 ((ClsInst -> Var) -> [ClsInst] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map ClsInst -> Var
instanceDFunId [ClsInst]
cls_insts)
    ids :: [Var]
ids    = TypeEnv -> [Var]
typeEnvIds TypeEnv
te
    tyvars :: [Var]
tyvars = [Type] -> [Var]
tyCoVarsOfTypesList ([Type] -> [Var]) -> [Type] -> [Var]
forall a b. (a -> b) -> a -> b
$ (Var -> Type) -> [Var] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Type
idType [Var]
ids
              -- Why the type variables?  How can the top level envt have free tyvars?
              -- I think it's because of the GHCi debugger, which can bind variables
              --   f :: [t] -> [t]
              -- where t is a RuntimeUnk (see TcType)

-- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee].
lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
--   Returns (warnings, errors)
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoreBindings :: DynFlags
-> CoreToDo -> [Var] -> CoreProgram -> (Bag SDoc, Bag SDoc)
lintCoreBindings DynFlags
dflags CoreToDo
pass [Var]
local_in_scope CoreProgram
binds
  = DynFlags
-> LintFlags -> InScopeSet -> LintM [()] -> (Bag SDoc, Bag SDoc)
forall a.
DynFlags
-> LintFlags -> InScopeSet -> LintM a -> (Bag SDoc, Bag SDoc)
initL DynFlags
dflags LintFlags
flags InScopeSet
in_scope_set (LintM [()] -> (Bag SDoc, Bag SDoc))
-> LintM [()] -> (Bag SDoc, Bag SDoc)
forall a b. (a -> b) -> a -> b
$
    LintLocInfo -> LintM [()] -> LintM [()]
forall a. LintLocInfo -> LintM a -> LintM a
addLoc LintLocInfo
TopLevelBindings         (LintM [()] -> LintM [()]) -> LintM [()] -> LintM [()]
forall a b. (a -> b) -> a -> b
$
    TopLevelFlag -> [Var] -> LintM [()] -> LintM [()]
forall a. TopLevelFlag -> [Var] -> LintM a -> LintM a
lintLetBndrs TopLevelFlag
TopLevel [Var]
binders   (LintM [()] -> LintM [()]) -> LintM [()] -> LintM [()]
forall a b. (a -> b) -> a -> b
$
        -- Put all the top-level binders in scope at the start
        -- This is because transformation rules can bring something
        -- into use 'unexpectedly'
    do { Bool -> SDoc -> LintM ()
checkL ([NonEmpty Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NonEmpty Var]
dups) ([NonEmpty Var] -> SDoc
dupVars [NonEmpty Var]
dups)
       ; Bool -> SDoc -> LintM ()
checkL ([NonEmpty Name] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NonEmpty Name]
ext_dups) ([NonEmpty Name] -> SDoc
dupExtVars [NonEmpty Name]
ext_dups)
       ; (Bind Var -> LintM ()) -> CoreProgram -> LintM [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Bind Var -> LintM ()
lint_bind CoreProgram
binds }
  where
    in_scope_set :: InScopeSet
in_scope_set = VarSet -> InScopeSet
mkInScopeSet ([Var] -> VarSet
mkVarSet [Var]
local_in_scope)

    flags :: LintFlags
flags = LintFlags
defaultLintFlags
               { lf_check_global_ids :: Bool
lf_check_global_ids = Bool
check_globals
               , lf_check_inline_loop_breakers :: Bool
lf_check_inline_loop_breakers = Bool
check_lbs
               , lf_check_static_ptrs :: StaticPtrCheck
lf_check_static_ptrs = StaticPtrCheck
check_static_ptrs }

    -- See Note [Checking for global Ids]
    check_globals :: Bool
check_globals = case CoreToDo
pass of
                      CoreToDo
CoreTidy -> Bool
False
                      CoreToDo
CorePrep -> Bool
False
                      CoreToDo
_        -> Bool
True

    -- See Note [Checking for INLINE loop breakers]
    check_lbs :: Bool
check_lbs = case CoreToDo
pass of
                      CoreToDo
CoreDesugar    -> Bool
False
                      CoreToDo
CoreDesugarOpt -> Bool
False
                      CoreToDo
_              -> Bool
True

    -- See Note [Checking StaticPtrs]
    check_static_ptrs :: StaticPtrCheck
check_static_ptrs | Bool -> Bool
not (Extension -> DynFlags -> Bool
xopt Extension
LangExt.StaticPointers DynFlags
dflags) = StaticPtrCheck
AllowAnywhere
                      | Bool
otherwise = case CoreToDo
pass of
                          CoreDoFloatOutwards FloatOutSwitches
_ -> StaticPtrCheck
AllowAtTopLevel
                          CoreToDo
CoreTidy              -> StaticPtrCheck
RejectEverywhere
                          CoreToDo
CorePrep              -> StaticPtrCheck
AllowAtTopLevel
                          CoreToDo
_                     -> StaticPtrCheck
AllowAnywhere

    binders :: [Var]
binders = CoreProgram -> [Var]
forall b. [Bind b] -> [b]
bindersOfBinds CoreProgram
binds
    ([Var]
_, [NonEmpty Var]
dups) = (Var -> Var -> Ordering) -> [Var] -> ([Var], [NonEmpty Var])
forall a. (a -> a -> Ordering) -> [a] -> ([a], [NonEmpty a])
removeDups Var -> Var -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [Var]
binders

    -- dups_ext checks for names with different uniques
    -- but but the same External name M.n.  We don't
    -- allow this at top level:
    --    M.n{r3}  = ...
    --    M.n{r29} = ...
    -- because they both get the same linker symbol
    ext_dups :: [NonEmpty Name]
ext_dups = ([Name], [NonEmpty Name]) -> [NonEmpty Name]
forall a b. (a, b) -> b
snd ((Name -> Name -> Ordering) -> [Name] -> ([Name], [NonEmpty Name])
forall a. (a -> a -> Ordering) -> [a] -> ([a], [NonEmpty a])
removeDups Name -> Name -> Ordering
ord_ext ((Var -> Name) -> [Var] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map Var -> Name
Var.varName [Var]
binders))
    ord_ext :: Name -> Name -> Ordering
ord_ext Name
n1 Name
n2 | Just Module
m1 <- Name -> Maybe Module
nameModule_maybe Name
n1
                  , Just Module
m2 <- Name -> Maybe Module
nameModule_maybe Name
n2
                  = (Module, OccName) -> (Module, OccName) -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Module
m1, Name -> OccName
nameOccName Name
n1) (Module
m2, Name -> OccName
nameOccName Name
n2)
                  | Bool
otherwise = Ordering
LT

    -- If you edit this function, you may need to update the GHC formalism
    -- See Note [GHC Formalism]
    lint_bind :: Bind Var -> LintM ()
lint_bind (Rec [(Var, CoreExpr)]
prs)         = ((Var, CoreExpr) -> LintM ()) -> [(Var, CoreExpr)] -> LintM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TopLevelFlag -> RecFlag -> (Var, CoreExpr) -> LintM ()
lintSingleBinding TopLevelFlag
TopLevel RecFlag
Recursive) [(Var, CoreExpr)]
prs
    lint_bind (NonRec Var
bndr CoreExpr
rhs) = TopLevelFlag -> RecFlag -> (Var, CoreExpr) -> LintM ()
lintSingleBinding TopLevelFlag
TopLevel RecFlag
NonRecursive (Var
bndr,CoreExpr
rhs)

{-
************************************************************************
*                                                                      *
\subsection[lintUnfolding]{lintUnfolding}
*                                                                      *
************************************************************************

Note [Linting Unfoldings from Interfaces]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

We use this to check all top-level unfoldings that come in from interfaces
(it is very painful to catch errors otherwise).

We do not need to call lintUnfolding on unfoldings that are nested within
top-level unfoldings; they are linted when we lint the top-level unfolding;
hence the `TopLevelFlag` on `tcPragExpr` in TcIface.

-}

lintUnfolding :: DynFlags
              -> SrcLoc
              -> VarSet         -- Treat these as in scope
              -> CoreExpr
              -> Maybe MsgDoc   -- Nothing => OK

lintUnfolding :: DynFlags -> SrcLoc -> VarSet -> CoreExpr -> Maybe SDoc
lintUnfolding DynFlags
dflags SrcLoc
locn VarSet
vars CoreExpr
expr
  | Bag SDoc -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag SDoc
errs = Maybe SDoc
forall a. Maybe a
Nothing
  | Bool
otherwise       = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (Bag SDoc -> SDoc
pprMessageBag Bag SDoc
errs)
  where
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet VarSet
vars
    (Bag SDoc
_warns, Bag SDoc
errs) = DynFlags
-> LintFlags -> InScopeSet -> LintM Type -> (Bag SDoc, Bag SDoc)
forall a.
DynFlags
-> LintFlags -> InScopeSet -> LintM a -> (Bag SDoc, Bag SDoc)
initL DynFlags
dflags LintFlags
defaultLintFlags InScopeSet
in_scope LintM Type
linter
    linter :: LintM Type
linter = LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (SrcLoc -> LintLocInfo
ImportedUnfolding SrcLoc
locn) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
             CoreExpr -> LintM Type
lintCoreExpr CoreExpr
expr

lintExpr :: DynFlags
         -> [Var]               -- Treat these as in scope
         -> CoreExpr
         -> Maybe MsgDoc        -- Nothing => OK

lintExpr :: DynFlags -> [Var] -> CoreExpr -> Maybe SDoc
lintExpr DynFlags
dflags [Var]
vars CoreExpr
expr
  | Bag SDoc -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag SDoc
errs = Maybe SDoc
forall a. Maybe a
Nothing
  | Bool
otherwise       = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (Bag SDoc -> SDoc
pprMessageBag Bag SDoc
errs)
  where
    in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet ([Var] -> VarSet
mkVarSet [Var]
vars)
    (Bag SDoc
_warns, Bag SDoc
errs) = DynFlags
-> LintFlags -> InScopeSet -> LintM Type -> (Bag SDoc, Bag SDoc)
forall a.
DynFlags
-> LintFlags -> InScopeSet -> LintM a -> (Bag SDoc, Bag SDoc)
initL DynFlags
dflags LintFlags
defaultLintFlags InScopeSet
in_scope LintM Type
linter
    linter :: LintM Type
linter = LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc LintLocInfo
TopLevelBindings (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
             CoreExpr -> LintM Type
lintCoreExpr CoreExpr
expr

{-
************************************************************************
*                                                                      *
\subsection[lintCoreBinding]{lintCoreBinding}
*                                                                      *
************************************************************************

Check a core binding, returning the list of variables bound.
-}

lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintSingleBinding :: TopLevelFlag -> RecFlag -> (Var, CoreExpr) -> LintM ()
lintSingleBinding TopLevelFlag
top_lvl_flag RecFlag
rec_flag (Var
binder,CoreExpr
rhs)
  = LintLocInfo -> LintM () -> LintM ()
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
RhsOf Var
binder) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
         -- Check the rhs
    do { Type
ty <- Var -> CoreExpr -> LintM Type
lintRhs Var
binder CoreExpr
rhs
       ; Type
binder_ty <- Type -> LintM Type
applySubstTy (Var -> Type
idType Var
binder)
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
binder_ty Type
ty (Var -> SDoc -> Type -> SDoc
mkRhsMsg Var
binder (String -> SDoc
text String
"RHS") Type
ty)

       -- If the binding is for a CoVar, the RHS should be (Coercion co)
       -- See Note [CoreSyn type and coercion invariant] in CoreSyn
       ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Var -> Bool
isCoVar Var
binder) Bool -> Bool -> Bool
|| CoreExpr -> Bool
forall b. Expr b -> Bool
isCoArg CoreExpr
rhs)
                (Var -> CoreExpr -> SDoc
mkLetErr Var
binder CoreExpr
rhs)

       -- Check that it's not levity-polymorphic
       -- Do this first, because otherwise isUnliftedType panics
       -- Annoyingly, this duplicates the test in lintIdBdr,
       -- because for non-rec lets we call lintSingleBinding first
       ; Bool -> SDoc -> LintM ()
checkL (Var -> Bool
isJoinId Var
binder Bool -> Bool -> Bool
|| Bool -> Bool
not (Type -> Bool
isTypeLevPoly Type
binder_ty))
                (Var -> SDoc -> SDoc
badBndrTyMsg Var
binder (String -> SDoc
text String
"levity-polymorphic"))

        -- Check the let/app invariant
        -- See Note [CoreSyn let/app invariant] in CoreSyn
       ; Bool -> SDoc -> LintM ()
checkL ( Var -> Bool
isJoinId Var
binder
               Bool -> Bool -> Bool
|| Bool -> Bool
not (HasDebugCallStack => Type -> Bool
Type -> Bool
isUnliftedType Type
binder_ty)
               Bool -> Bool -> Bool
|| (RecFlag -> Bool
isNonRec RecFlag
rec_flag Bool -> Bool -> Bool
&& CoreExpr -> Bool
exprOkForSpeculation CoreExpr
rhs)
               Bool -> Bool -> Bool
|| CoreExpr -> Bool
exprIsTickedString CoreExpr
rhs)
           (Var -> SDoc -> SDoc
badBndrTyMsg Var
binder (String -> SDoc
text String
"unlifted"))

        -- Check that if the binder is top-level or recursive, it's not
        -- demanded. Primitive string literals are exempt as there is no
        -- computation to perform, see Note [CoreSyn top-level string literals].
       ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Var -> Bool
isStrictId Var
binder)
            Bool -> Bool -> Bool
|| (RecFlag -> Bool
isNonRec RecFlag
rec_flag Bool -> Bool -> Bool
&& Bool -> Bool
not (TopLevelFlag -> Bool
isTopLevel TopLevelFlag
top_lvl_flag))
            Bool -> Bool -> Bool
|| CoreExpr -> Bool
exprIsTickedString CoreExpr
rhs)
           (Var -> SDoc
mkStrictMsg Var
binder)

        -- Check that if the binder is at the top level and has type Addr#,
        -- that it is a string literal, see
        -- Note [CoreSyn top-level string literals].
       ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (TopLevelFlag -> Bool
isTopLevel TopLevelFlag
top_lvl_flag Bool -> Bool -> Bool
&& Type
binder_ty Type -> Type -> Bool
`eqType` Type
addrPrimTy)
                 Bool -> Bool -> Bool
|| CoreExpr -> Bool
exprIsTickedString CoreExpr
rhs)
           (Var -> SDoc
mkTopNonLitStrMsg Var
binder)

       ; LintFlags
flags <- LintM LintFlags
getLintFlags

         -- Check that a join-point binder has a valid type
         -- NB: lintIdBinder has checked that it is not top-level bound
       ; case Var -> Maybe Int
isJoinId_maybe Var
binder of
            Maybe Int
Nothing    -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just Int
arity ->  Bool -> SDoc -> LintM ()
checkL (Int -> Type -> Bool
isValidJoinPointType Int
arity Type
binder_ty)
                                  (Var -> Type -> SDoc
mkInvalidJoinPointMsg Var
binder Type
binder_ty)

       ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (LintFlags -> Bool
lf_check_inline_loop_breakers LintFlags
flags
               Bool -> Bool -> Bool
&& Unfolding -> Bool
isStableUnfolding (Var -> Unfolding
realIdUnfolding Var
binder)
               Bool -> Bool -> Bool
&& OccInfo -> Bool
isStrongLoopBreaker (Var -> OccInfo
idOccInfo Var
binder)
               Bool -> Bool -> Bool
&& InlinePragma -> Bool
isInlinePragma (Var -> InlinePragma
idInlinePragma Var
binder))
              (SDoc -> LintM ()
addWarnL (String -> SDoc
text String
"INLINE binder is (non-rule) loop breaker:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder))
              -- Only non-rule loop breakers inhibit inlining

       -- We used to check that the dmdTypeDepth of a demand signature never
       -- exceeds idArity, but that is an unnecessary complication, see
       -- Note [idArity varies independently of dmdTypeDepth] in DmdAnal

       -- Check that the binder's arity is within the bounds imposed by
       -- the type and the strictness signature. See Note [exprArity invariant]
       -- and Note [Trimming arity]
       ; Bool -> SDoc -> LintM ()
checkL (Type -> [OneShotInfo]
typeArity (Var -> Type
idType Var
binder) [OneShotInfo] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` Var -> Int
idArity Var
binder)
           (String -> SDoc
text String
"idArity" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Int
idArity Var
binder) SDoc -> SDoc -> SDoc
<+>
           String -> SDoc
text String
"exceeds typeArity" SDoc -> SDoc -> SDoc
<+>
           Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([OneShotInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Type -> [OneShotInfo]
typeArity (Var -> Type
idType Var
binder))) SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+>
           Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder)

       ; case StrictSig -> ([Demand], DmdResult)
splitStrictSig (Var -> StrictSig
idStrictness Var
binder) of
           ([Demand]
demands, DmdResult
result_info) | DmdResult -> Bool
isBotRes DmdResult
result_info ->
             Bool -> SDoc -> LintM ()
checkL ([Demand]
demands [Demand] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthAtLeast` Var -> Int
idArity Var
binder)
               (String -> SDoc
text String
"idArity" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Int
idArity Var
binder) SDoc -> SDoc -> SDoc
<+>
               String -> SDoc
text String
"exceeds arity imposed by the strictness signature" SDoc -> SDoc -> SDoc
<+>
               StrictSig -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> StrictSig
idStrictness Var
binder) SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+>
               Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder)
           ([Demand], DmdResult)
_ -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

       ; (CoreRule -> LintM ()) -> [CoreRule] -> LintM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Var -> Type -> CoreRule -> LintM ()
lintCoreRule Var
binder Type
binder_ty) (Var -> [CoreRule]
idCoreRules Var
binder)

       ; LintLocInfo -> LintM () -> LintM ()
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
UnfoldingOf Var
binder) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
         Var -> Type -> Unfolding -> LintM ()
lintIdUnfolding Var
binder Type
binder_ty (Var -> Unfolding
idUnfolding Var
binder) }

        -- We should check the unfolding, if any, but this is tricky because
        -- the unfolding is a SimplifiableCoreExpr. Give up for now.

-- | Checks the RHS of bindings. It only differs from 'lintCoreExpr'
-- in that it doesn't reject occurrences of the function 'makeStatic' when they
-- appear at the top level and @lf_check_static_ptrs == AllowAtTopLevel@, and
-- for join points, it skips the outer lambdas that take arguments to the
-- join point.
--
-- See Note [Checking StaticPtrs].
lintRhs :: Id -> CoreExpr -> LintM OutType
lintRhs :: Var -> CoreExpr -> LintM Type
lintRhs Var
bndr CoreExpr
rhs
    | Just Int
arity <- Var -> Maybe Int
isJoinId_maybe Var
bndr
    = Int -> Int -> Bool -> CoreExpr -> LintM Type
lint_join_lams Int
arity Int
arity Bool
True CoreExpr
rhs
    | AlwaysTailCalled Int
arity <- OccInfo -> TailCallInfo
tailCallInfo (Var -> OccInfo
idOccInfo Var
bndr)
    = Int -> Int -> Bool -> CoreExpr -> LintM Type
lint_join_lams Int
arity Int
arity Bool
False CoreExpr
rhs
  where
    lint_join_lams :: Int -> Int -> Bool -> CoreExpr -> LintM Type
lint_join_lams Int
0 Int
_ Bool
_ CoreExpr
rhs
      = CoreExpr -> LintM Type
lintCoreExpr CoreExpr
rhs

    lint_join_lams Int
n Int
tot Bool
enforce (Lam Var
var CoreExpr
expr)
      = LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
LambdaBodyOf Var
var) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
        BindingSite -> Var -> (Var -> LintM Type) -> LintM Type
forall a. BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
LambdaBind Var
var ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \ Var
var' ->
        do { Type
body_ty <- Int -> Int -> Bool -> CoreExpr -> LintM Type
lint_join_lams (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
tot Bool
enforce CoreExpr
expr
           ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> LintM Type) -> Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ Var -> Type -> Type
mkLamType Var
var' Type
body_ty }

    lint_join_lams Int
n Int
tot Bool
True CoreExpr
_other
      = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> LintM Type) -> SDoc -> LintM Type
forall a b. (a -> b) -> a -> b
$ Var -> Int -> Int -> CoreExpr -> SDoc
mkBadJoinArityMsg Var
bndr Int
tot (Int
totInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
n) CoreExpr
rhs
    lint_join_lams Int
_ Int
_ Bool
False CoreExpr
rhs
      = LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> LintM Type
lintCoreExpr CoreExpr
rhs
          -- Future join point, not yet eta-expanded
          -- Body is not a tail position

-- Allow applications of the data constructor @StaticPtr@ at the top
-- but produce errors otherwise.
lintRhs Var
_bndr CoreExpr
rhs = (LintFlags -> StaticPtrCheck)
-> LintM LintFlags -> LintM StaticPtrCheck
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LintFlags -> StaticPtrCheck
lf_check_static_ptrs LintM LintFlags
getLintFlags LintM StaticPtrCheck
-> (StaticPtrCheck -> LintM Type) -> LintM Type
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StaticPtrCheck -> LintM Type
go
  where
    -- Allow occurrences of 'makeStatic' at the top-level but produce errors
    -- otherwise.
    go :: StaticPtrCheck -> LintM Type
go StaticPtrCheck
AllowAtTopLevel
      | ([Var]
binders0, CoreExpr
rhs') <- CoreExpr -> ([Var], CoreExpr)
collectTyBinders CoreExpr
rhs
      , Just (CoreExpr
fun, Type
t, CoreExpr
info, CoreExpr
e) <- CoreExpr -> Maybe (CoreExpr, Type, CoreExpr, CoreExpr)
collectMakeStaticArgs CoreExpr
rhs'
      = LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
        (Var -> LintM Type -> LintM Type)
-> LintM Type -> [Var] -> LintM Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
        -- imitate @lintCoreExpr (Lam ...)@
        (\Var
var LintM Type
loopBinders ->
          LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
LambdaBodyOf Var
var) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
            BindingSite -> Var -> (Var -> LintM Type) -> LintM Type
forall a. BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
LambdaBind Var
var ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \Var
var' ->
              do { Type
body_ty <- LintM Type
loopBinders
                 ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> LintM Type) -> Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ Var -> Type -> Type
mkLamType Var
var' Type
body_ty }
        )
        -- imitate @lintCoreExpr (App ...)@
        (do Type
fun_ty <- CoreExpr -> LintM Type
lintCoreExpr CoreExpr
fun
            Type -> [CoreExpr] -> LintM Type
lintCoreArgs Type
fun_ty [Type -> CoreExpr
forall b. Type -> Expr b
Type Type
t, CoreExpr
info, CoreExpr
e]
        )
        [Var]
binders0
    go StaticPtrCheck
_ = LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> LintM Type
lintCoreExpr CoreExpr
rhs

lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
lintIdUnfolding :: Var -> Type -> Unfolding -> LintM ()
lintIdUnfolding Var
bndr Type
bndr_ty Unfolding
uf
  | Unfolding -> Bool
isStableUnfolding Unfolding
uf
  , Just CoreExpr
rhs <- Unfolding -> Maybe CoreExpr
maybeUnfoldingTemplate Unfolding
uf
  = do { Type
ty <- Var -> CoreExpr -> LintM Type
lintRhs Var
bndr CoreExpr
rhs
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
bndr_ty Type
ty (Var -> SDoc -> Type -> SDoc
mkRhsMsg Var
bndr (String -> SDoc
text String
"unfolding") Type
ty) }
lintIdUnfolding  Var
_ Type
_ Unfolding
_
  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()       -- Do not Lint unstable unfoldings, because that leads
                    -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars

{-
Note [Checking for INLINE loop breakers]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It's very suspicious if a strong loop breaker is marked INLINE.

However, the desugarer generates instance methods with INLINE pragmas
that form a mutually recursive group.  Only after a round of
simplification are they unravelled.  So we suppress the test for
the desugarer.

************************************************************************
*                                                                      *
\subsection[lintCoreExpr]{lintCoreExpr}
*                                                                      *
************************************************************************
-}

-- For OutType, OutKind, the substitution has been applied,
--                       but has not been linted yet

type LintedType  = Type -- Substitution applied, and type is linted
type LintedKind  = Kind

lintCoreExpr :: CoreExpr -> LintM OutType
-- The returned type has the substitution from the monad
-- already applied to it:
--      lintCoreExpr e subst = exprType (subst e)
--
-- The returned "type" can be a kind, if the expression is (Type ty)

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoreExpr :: CoreExpr -> LintM Type
lintCoreExpr (Var Var
var)
  = Var -> Int -> LintM Type
lintVarOcc Var
var Int
0

lintCoreExpr (Lit Literal
lit)
  = Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> Type
literalType Literal
lit)

lintCoreExpr (Cast CoreExpr
expr Coercion
co)
  = do { Type
expr_ty <- LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> LintM Type
lintCoreExpr CoreExpr
expr
       ; Coercion
co' <- Coercion -> LintM Coercion
applySubstCo Coercion
co
       ; (Type
_, Type
k2, Type
from_ty, Type
to_ty, Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co'
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k2 (String -> SDoc
text String
"target of cast" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co))
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co' Role
Representational Role
r
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
from_ty Type
expr_ty (CoreExpr -> Coercion -> Type -> Type -> SDoc
mkCastErr CoreExpr
expr Coercion
co' Type
from_ty Type
expr_ty)
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
to_ty }

lintCoreExpr (Tick Tickish Var
tickish CoreExpr
expr)
  = do case Tickish Var
tickish of
         Breakpoint Int
_ [Var]
ids -> [Var] -> (Var -> LintM Var) -> LintM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var]
ids ((Var -> LintM Var) -> LintM ()) -> (Var -> LintM Var) -> LintM ()
forall a b. (a -> b) -> a -> b
$ \Var
id -> do
                               Var -> LintM ()
checkDeadIdOcc Var
id
                               Var -> LintM Var
lookupIdInScope Var
id
         Tickish Var
_                -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       Bool -> LintM Type -> LintM Type
forall a. Bool -> LintM a -> LintM a
markAllJoinsBadIf Bool
block_joins (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> LintM Type
lintCoreExpr CoreExpr
expr
  where
    block_joins :: Bool
block_joins = Bool -> Bool
not (Tickish Var
tickish Tickish Var -> TickishScoping -> Bool
forall id. Tickish id -> TickishScoping -> Bool
`tickishScopesLike` TickishScoping
SoftScope)
      -- TODO Consider whether this is the correct rule. It is consistent with
      -- the simplifier's behaviour - cost-centre-scoped ticks become part of
      -- the continuation, and thus they behave like part of an evaluation
      -- context, but soft-scoped and non-scoped ticks simply wrap the result
      -- (see Simplify.simplTick).

lintCoreExpr (Let (NonRec Var
tv (Type Type
ty)) CoreExpr
body)
  | Var -> Bool
isTyVar Var
tv
  =     -- See Note [Linting type lets]
    do  { Type
ty' <- Type -> LintM Type
applySubstTy Type
ty
        ; Var -> (Var -> LintM Type) -> LintM Type
forall a. Var -> (Var -> LintM a) -> LintM a
lintTyBndr Var
tv              ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \ Var
tv' ->
    do  { LintLocInfo -> LintM () -> LintM ()
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
RhsOf Var
tv) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$ Var -> Type -> LintM ()
lintTyKind Var
tv' Type
ty'
                -- Now extend the substitution so we
                -- take advantage of it in the body
        ; Var -> Type -> LintM Type -> LintM Type
forall a. Var -> Type -> LintM a -> LintM a
extendSubstL Var
tv Type
ty'        (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
          LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc ([Var] -> LintLocInfo
BodyOfLetRec [Var
tv]) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
          CoreExpr -> LintM Type
lintCoreExpr CoreExpr
body } }

lintCoreExpr (Let (NonRec Var
bndr CoreExpr
rhs) CoreExpr
body)
  | Var -> Bool
isId Var
bndr
  = do  { TopLevelFlag -> RecFlag -> (Var, CoreExpr) -> LintM ()
lintSingleBinding TopLevelFlag
NotTopLevel RecFlag
NonRecursive (Var
bndr,CoreExpr
rhs)
        ; LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc ([Var] -> LintLocInfo
BodyOfLetRec [Var
bndr])
                 (BindingSite -> Var -> (Var -> LintM Type) -> LintM Type
forall a. BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
LetBind Var
bndr ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \Var
_ ->
                  [Var] -> LintM Type -> LintM Type
forall a. [Var] -> LintM a -> LintM a
addGoodJoins [Var
bndr] (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
                  CoreExpr -> LintM Type
lintCoreExpr CoreExpr
body) }

  | Bool
otherwise
  = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (Var -> CoreExpr -> SDoc
mkLetErr Var
bndr CoreExpr
rhs)       -- Not quite accurate

lintCoreExpr e :: CoreExpr
e@(Let (Rec [(Var, CoreExpr)]
pairs) CoreExpr
body)
  = TopLevelFlag -> [Var] -> LintM Type -> LintM Type
forall a. TopLevelFlag -> [Var] -> LintM a -> LintM a
lintLetBndrs TopLevelFlag
NotTopLevel [Var]
bndrs (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
    [Var] -> LintM Type -> LintM Type
forall a. [Var] -> LintM a -> LintM a
addGoodJoins [Var]
bndrs             (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
    do  { -- Check that the list of pairs is non-empty
          Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not ([(Var, CoreExpr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Var, CoreExpr)]
pairs)) (CoreExpr -> SDoc
emptyRec CoreExpr
e)

          -- Check that there are no duplicated binders
        ; Bool -> SDoc -> LintM ()
checkL ([NonEmpty Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NonEmpty Var]
dups) ([NonEmpty Var] -> SDoc
dupVars [NonEmpty Var]
dups)

          -- Check that either all the binders are joins, or none
        ; Bool -> SDoc -> LintM ()
checkL ((Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Var -> Bool
isJoinId [Var]
bndrs Bool -> Bool -> Bool
|| (Var -> Bool) -> [Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool -> Bool
not (Bool -> Bool) -> (Var -> Bool) -> Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Bool
isJoinId) [Var]
bndrs) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
            [Var] -> SDoc
mkInconsistentRecMsg [Var]
bndrs

        ; ((Var, CoreExpr) -> LintM ()) -> [(Var, CoreExpr)] -> LintM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (TopLevelFlag -> RecFlag -> (Var, CoreExpr) -> LintM ()
lintSingleBinding TopLevelFlag
NotTopLevel RecFlag
Recursive) [(Var, CoreExpr)]
pairs
        ; LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc ([Var] -> LintLocInfo
BodyOfLetRec [Var]
bndrs) (CoreExpr -> LintM Type
lintCoreExpr CoreExpr
body) }
  where
    bndrs :: [Var]
bndrs = ((Var, CoreExpr) -> Var) -> [(Var, CoreExpr)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, CoreExpr) -> Var
forall a b. (a, b) -> a
fst [(Var, CoreExpr)]
pairs
    ([Var]
_, [NonEmpty Var]
dups) = (Var -> Var -> Ordering) -> [Var] -> ([Var], [NonEmpty Var])
forall a. (a -> a -> Ordering) -> [a] -> ([a], [NonEmpty a])
removeDups Var -> Var -> Ordering
forall a. Ord a => a -> a -> Ordering
compare [Var]
bndrs

lintCoreExpr e :: CoreExpr
e@(App CoreExpr
_ CoreExpr
_)
  = do { Type
fun_ty <- CoreExpr -> Int -> LintM Type
lintCoreFun CoreExpr
fun ([CoreExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CoreExpr]
args)
       ; Type -> [CoreExpr] -> LintM Type
lintCoreArgs Type
fun_ty [CoreExpr]
args }
  where
    (CoreExpr
fun, [CoreExpr]
args) = CoreExpr -> (CoreExpr, [CoreExpr])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e

lintCoreExpr (Lam Var
var CoreExpr
expr)
  = LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
LambdaBodyOf Var
var) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
    LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
    BindingSite -> Var -> (Var -> LintM Type) -> LintM Type
forall a. BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
LambdaBind Var
var ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \ Var
var' ->
    do { Type
body_ty <- CoreExpr -> LintM Type
lintCoreExpr CoreExpr
expr
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> LintM Type) -> Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ Var -> Type -> Type
mkLamType Var
var' Type
body_ty }

lintCoreExpr (Case CoreExpr
scrut Var
var Type
alt_ty [Alt Var]
alts)
  = CoreExpr -> Var -> Type -> [Alt Var] -> LintM Type
lintCaseExpr CoreExpr
scrut Var
var Type
alt_ty [Alt Var]
alts

-- This case can't happen; linting types in expressions gets routed through
-- lintCoreArgs
lintCoreExpr (Type Type
ty)
  = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Type found as expression" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)

lintCoreExpr (Coercion Coercion
co)
  = do { (Type
k1, Type
k2, Type
ty1, Type
ty2, Role
role) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintInCo Coercion
co
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Role -> Type -> Type -> Type -> Type -> Type
mkHeteroCoercionType Role
role Type
k1 Type
k2 Type
ty1 Type
ty2) }

----------------------
lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed
            -> LintM Type -- returns type of the *variable*
lintVarOcc :: Var -> Int -> LintM Type
lintVarOcc Var
var Int
nargs
  = do  { Bool -> SDoc -> LintM ()
checkL (Var -> Bool
isNonCoVarId Var
var)
                 (String -> SDoc
text String
"Non term variable" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var)
                 -- See CoreSyn Note [Variable occurrences in Core]

        -- Cneck that the type of the occurrence is the same
        -- as the type of the binding site
        ; Type
ty   <- Type -> LintM Type
applySubstTy (Var -> Type
idType Var
var)
        ; Var
var' <- Var -> LintM Var
lookupIdInScope Var
var
        ; let ty' :: Type
ty' = Var -> Type
idType Var
var'
        ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
ty Type
ty' (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$ Var -> Var -> Type -> Type -> SDoc
mkBndrOccTypeMismatchMsg Var
var' Var
var Type
ty' Type
ty

          -- Check for a nested occurrence of the StaticPtr constructor.
          -- See Note [Checking StaticPtrs].
        ; LintFlags
lf <- LintM LintFlags
getLintFlags
        ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0 Bool -> Bool -> Bool
&& LintFlags -> StaticPtrCheck
lf_check_static_ptrs LintFlags
lf StaticPtrCheck -> StaticPtrCheck -> Bool
forall a. Eq a => a -> a -> Bool
/= StaticPtrCheck
AllowAnywhere) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
            Bool -> SDoc -> LintM ()
checkL (Var -> Name
idName Var
var Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
/= Name
makeStaticName) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
              String -> SDoc
text String
"Found makeStatic nested in an expression"

        ; Var -> LintM ()
checkDeadIdOcc Var
var
        ; Var -> Int -> LintM ()
checkJoinOcc Var
var Int
nargs

        ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type
idType Var
var') }

lintCoreFun :: CoreExpr
            -> Int        -- Number of arguments (type or val) being passed
            -> LintM Type -- Returns type of the *function*
lintCoreFun :: CoreExpr -> Int -> LintM Type
lintCoreFun (Var Var
var) Int
nargs
  = Var -> Int -> LintM Type
lintVarOcc Var
var Int
nargs

lintCoreFun (Lam Var
var CoreExpr
body) Int
nargs
  -- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; see
  -- Note [Beta redexes]
  | Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0
  = LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
LambdaBodyOf Var
var) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
    BindingSite -> Var -> (Var -> LintM Type) -> LintM Type
forall a. BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
LambdaBind Var
var ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \ Var
var' ->
    do { Type
body_ty <- CoreExpr -> Int -> LintM Type
lintCoreFun CoreExpr
body (Int
nargs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> LintM Type) -> Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ Var -> Type -> Type
mkLamType Var
var' Type
body_ty }

lintCoreFun CoreExpr
expr Int
nargs
  = Bool -> LintM Type -> LintM Type
forall a. Bool -> LintM a -> LintM a
markAllJoinsBadIf (Int
nargs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
      -- See Note [Join points are less general than the paper]
    CoreExpr -> LintM Type
lintCoreExpr CoreExpr
expr

------------------
checkDeadIdOcc :: Id -> LintM ()
-- Occurrences of an Id should never be dead....
-- except when we are checking a case pattern
checkDeadIdOcc :: Var -> LintM ()
checkDeadIdOcc Var
id
  | OccInfo -> Bool
isDeadOcc (Var -> OccInfo
idOccInfo Var
id)
  = do { Bool
in_case <- LintM Bool
inCasePat
       ; Bool -> SDoc -> LintM ()
checkL Bool
in_case
                (String -> SDoc
text String
"Occurrence of a dead Id" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
id) }
  | Bool
otherwise
  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

------------------
checkJoinOcc :: Id -> JoinArity -> LintM ()
-- Check that if the occurrence is a JoinId, then so is the
-- binding site, and it's a valid join Id
checkJoinOcc :: Var -> Int -> LintM ()
checkJoinOcc Var
var Int
n_args
  | Just Int
join_arity_occ <- Var -> Maybe Int
isJoinId_maybe Var
var
  = do { Maybe Int
mb_join_arity_bndr <- Var -> LintM (Maybe Int)
lookupJoinId Var
var
       ; case Maybe Int
mb_join_arity_bndr of {
           Maybe Int
Nothing -> -- Binder is not a join point
                      SDoc -> LintM ()
addErrL (Var -> SDoc
invalidJoinOcc Var
var) ;

           Just Int
join_arity_bndr ->

    do { Bool -> SDoc -> LintM ()
checkL (Int
join_arity_bndr Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
join_arity_occ) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
           -- Arity differs at binding site and occurrence
         Var -> Int -> Int -> SDoc
mkJoinBndrOccMismatchMsg Var
var Int
join_arity_bndr Int
join_arity_occ

       ; Bool -> SDoc -> LintM ()
checkL (Int
n_args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
join_arity_occ) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
           -- Arity doesn't match #args
         Var -> Int -> Int -> SDoc
mkBadJumpMsg Var
var Int
join_arity_occ Int
n_args } } }

  | Bool
otherwise
  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{-
Note [No alternatives lint check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Case expressions with no alternatives are odd beasts, and it would seem
like they would worth be looking at in the linter (cf #10180). We
used to check two things:

* exprIsHNF is false: it would *seem* to be terribly wrong if
  the scrutinee was already in head normal form.

* exprIsBottom is true: we should be able to see why GHC believes the
  scrutinee is diverging for sure.

It was already known that the second test was not entirely reliable.
Unfortunately (#13990), the first test turned out not to be reliable
either. Getting the checks right turns out to be somewhat complicated.

For example, suppose we have (comment 8)

  data T a where
    TInt :: T Int

  absurdTBool :: T Bool -> a
  absurdTBool v = case v of

  data Foo = Foo !(T Bool)

  absurdFoo :: Foo -> a
  absurdFoo (Foo x) = absurdTBool x

GHC initially accepts the empty case because of the GADT conditions. But then
we inline absurdTBool, getting

  absurdFoo (Foo x) = case x of

x is in normal form (because the Foo constructor is strict) but the
case is empty. To avoid this problem, GHC would have to recognize
that matching on Foo x is already absurd, which is not so easy.

More generally, we don't really know all the ways that GHC can
lose track of why an expression is bottom, so we shouldn't make too
much fuss when that happens.


Note [Beta redexes]
~~~~~~~~~~~~~~~~~~~
Consider:

  join j @x y z = ... in
  (\@x y z -> jump j @x y z) @t e1 e2

This is clearly ill-typed, since the jump is inside both an application and a
lambda, either of which is enough to disqualify it as a tail call (see Note
[Invariants on join points] in CoreSyn). However, strictly from a
lambda-calculus perspective, the term doesn't go wrong---after the two beta
reductions, the jump *is* a tail call and everything is fine.

Why would we want to allow this when we have let? One reason is that a compound
beta redex (that is, one with more than one argument) has different scoping
rules: naively reducing the above example using lets will capture any free
occurrence of y in e2. More fundamentally, type lets are tricky; many passes,
such as Float Out, tacitly assume that the incoming program's type lets have
all been dealt with by the simplifier. Thus we don't want to let-bind any types
in, say, CoreSubst.simpleOptPgm, which in some circumstances can run immediately
before Float Out.

All that said, currently CoreSubst.simpleOptPgm is the only thing using this
loophole, doing so to avoid re-traversing large functions (beta-reducing a type
lambda without introducing a type let requires a substitution). TODO: Improve
simpleOptPgm so that we can forget all this ever happened.

************************************************************************
*                                                                      *
\subsection[lintCoreArgs]{lintCoreArgs}
*                                                                      *
************************************************************************

The basic version of these functions checks that the argument is a
subtype of the required type, as one would expect.
-}


lintCoreArgs  :: OutType -> [CoreArg] -> LintM OutType
lintCoreArgs :: Type -> [CoreExpr] -> LintM Type
lintCoreArgs Type
fun_ty [CoreExpr]
args = (Type -> CoreExpr -> LintM Type)
-> Type -> [CoreExpr] -> LintM Type
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM Type -> CoreExpr -> LintM Type
lintCoreArg Type
fun_ty [CoreExpr]
args

lintCoreArg  :: OutType -> CoreArg -> LintM OutType
lintCoreArg :: Type -> CoreExpr -> LintM Type
lintCoreArg Type
fun_ty (Type Type
arg_ty)
  = do { Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Type -> Bool
isCoercionTy Type
arg_ty))
                (String -> SDoc
text String
"Unnecessary coercion-to-type injection:"
                  SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_ty)
       ; Type
arg_ty' <- Type -> LintM Type
applySubstTy Type
arg_ty
       ; Type -> Type -> LintM Type
lintTyApp Type
fun_ty Type
arg_ty' }

lintCoreArg Type
fun_ty CoreExpr
arg
  = do { Type
arg_ty <- LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> LintM Type
lintCoreExpr CoreExpr
arg
           -- See Note [Levity polymorphism invariants] in CoreSyn
       ; Bool -> SDoc -> LintM ()
lintL (Bool -> Bool
not (Type -> Bool
isTypeLevPoly Type
arg_ty))
           (String -> SDoc
text String
"Levity-polymorphic argument:" SDoc -> SDoc -> SDoc
<+>
             (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
arg SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
arg_ty))))
          -- check for levity polymorphism first, because otherwise isUnliftedType panics

       ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (HasDebugCallStack => Type -> Bool
Type -> Bool
isUnliftedType Type
arg_ty) Bool -> Bool -> Bool
|| CoreExpr -> Bool
exprOkForSpeculation CoreExpr
arg)
                (CoreExpr -> SDoc
mkLetAppMsg CoreExpr
arg)
       ; CoreExpr -> Type -> Type -> LintM Type
lintValApp CoreExpr
arg Type
fun_ty Type
arg_ty }

-----------------
lintAltBinders :: OutType     -- Scrutinee type
               -> OutType     -- Constructor type
               -> [OutVar]    -- Binders
               -> LintM ()
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintAltBinders :: Type -> Type -> [Var] -> LintM ()
lintAltBinders Type
scrut_ty Type
con_ty []
  = Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
con_ty Type
scrut_ty (Type -> Type -> SDoc
mkBadPatMsg Type
con_ty Type
scrut_ty)
lintAltBinders Type
scrut_ty Type
con_ty (Var
bndr:[Var]
bndrs)
  | Var -> Bool
isTyVar Var
bndr
  = do { Type
con_ty' <- Type -> Type -> LintM Type
lintTyApp Type
con_ty (Var -> Type
mkTyVarTy Var
bndr)
       ; Type -> Type -> [Var] -> LintM ()
lintAltBinders Type
scrut_ty Type
con_ty' [Var]
bndrs }
  | Bool
otherwise
  = do { Type
con_ty' <- CoreExpr -> Type -> Type -> LintM Type
lintValApp (Var -> CoreExpr
forall b. Var -> Expr b
Var Var
bndr) Type
con_ty (Var -> Type
idType Var
bndr)
       ; Type -> Type -> [Var] -> LintM ()
lintAltBinders Type
scrut_ty Type
con_ty' [Var]
bndrs }

-----------------
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp :: Type -> Type -> LintM Type
lintTyApp Type
fun_ty Type
arg_ty
  | Just (Var
tv,Type
body_ty) <- Type -> Maybe (Var, Type)
splitForAllTy_maybe Type
fun_ty
  = do  { Var -> Type -> LintM ()
lintTyKind Var
tv Type
arg_ty
        ; InScopeSet
in_scope <- LintM InScopeSet
getInScope
        -- substTy needs the set of tyvars in scope to avoid generating
        -- uniques that are already in scope.
        -- See Note [The substitution invariant] in TyCoSubst
        ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (InScopeSet -> [Var] -> [Type] -> Type -> Type
substTyWithInScope InScopeSet
in_scope [Var
tv] [Type
arg_ty] Type
body_ty) }

  | Bool
otherwise
  = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (Type -> Type -> SDoc
mkTyAppMsg Type
fun_ty Type
arg_ty)

-----------------
lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
lintValApp :: CoreExpr -> Type -> Type -> LintM Type
lintValApp CoreExpr
arg Type
fun_ty Type
arg_ty
  | Just (Type
arg,Type
res) <- Type -> Maybe (Type, Type)
splitFunTy_maybe Type
fun_ty
  = do { Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
arg Type
arg_ty SDoc
err1
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
res }
  | Bool
otherwise
  = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL SDoc
err2
  where
    err1 :: SDoc
err1 = Type -> Type -> CoreExpr -> SDoc
mkAppMsg       Type
fun_ty Type
arg_ty CoreExpr
arg
    err2 :: SDoc
err2 = Type -> Type -> CoreExpr -> SDoc
mkNonFunAppMsg Type
fun_ty Type
arg_ty CoreExpr
arg

lintTyKind :: OutTyVar -> OutType -> LintM ()
-- Both args have had substitution applied

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintTyKind :: Var -> Type -> LintM ()
lintTyKind Var
tyvar Type
arg_ty
        -- Arg type might be boxed for a function with an uncommitted
        -- tyvar; notably this is used so that we can give
        --      error :: forall a:*. String -> a
        -- and then apply it to both boxed and unboxed types.
  = do { Type
arg_kind <- Type -> LintM Type
lintType Type
arg_ty
       ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
arg_kind Type -> Type -> Bool
`eqType` Type
tyvar_kind)
                (SDoc -> LintM ()
addErrL (Var -> Type -> SDoc
mkKindErrMsg Var
tyvar Type
arg_ty SDoc -> SDoc -> SDoc
$$ (String -> SDoc
text String
"Linted Arg kind:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_kind))) }
  where
    tyvar_kind :: Type
tyvar_kind = Var -> Type
tyVarKind Var
tyvar

{-
************************************************************************
*                                                                      *
\subsection[lintCoreAlts]{lintCoreAlts}
*                                                                      *
************************************************************************
-}

lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM OutType
lintCaseExpr :: CoreExpr -> Var -> Type -> [Alt Var] -> LintM Type
lintCaseExpr CoreExpr
scrut Var
var Type
alt_ty [Alt Var]
alts =
  do { let e :: CoreExpr
e = CoreExpr -> Var -> Type -> [Alt Var] -> CoreExpr
forall b. Expr b -> b -> Type -> [Alt b] -> Expr b
Case CoreExpr
scrut Var
var Type
alt_ty [Alt Var]
alts   -- Just for error messages

     -- Check the scrutinee
     ; Type
scrut_ty <- LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> LintM Type
lintCoreExpr CoreExpr
scrut
          -- See Note [Join points are less general than the paper]
          -- in CoreSyn

     ; (Type
alt_ty, Type
_) <- LintLocInfo -> LintM (Type, Type) -> LintM (Type, Type)
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (CoreExpr -> LintLocInfo
CaseTy CoreExpr
scrut) (LintM (Type, Type) -> LintM (Type, Type))
-> LintM (Type, Type) -> LintM (Type, Type)
forall a b. (a -> b) -> a -> b
$
                      Type -> LintM (Type, Type)
lintInTy Type
alt_ty
     ; (Type
var_ty, Type
_) <- LintLocInfo -> LintM (Type, Type) -> LintM (Type, Type)
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
IdTy Var
var) (LintM (Type, Type) -> LintM (Type, Type))
-> LintM (Type, Type) -> LintM (Type, Type)
forall a b. (a -> b) -> a -> b
$
                      Type -> LintM (Type, Type)
lintInTy (Var -> Type
idType Var
var)

     -- We used to try to check whether a case expression with no
     -- alternatives was legitimate, but this didn't work.
     -- See Note [No alternatives lint check] for details.

     -- Check that the scrutinee is not a floating-point type
     -- if there are any literal alternatives
     -- See CoreSyn Note [Case expression invariants] item (5)
     -- See Note [Rules for floating-point comparisons] in PrelRules
     ; let isLitPat :: (AltCon, b, c) -> Bool
isLitPat (LitAlt Literal
_, b
_ , c
_) = Bool
True
           isLitPat (AltCon, b, c)
_                 = Bool
False
     ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Bool
isFloatingTy Type
scrut_ty Bool -> Bool -> Bool
&& (Alt Var -> Bool) -> [Alt Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Alt Var -> Bool
forall b c. (AltCon, b, c) -> Bool
isLitPat [Alt Var]
alts)
         (PtrString -> SDoc
ptext (String -> PtrString
sLit (String -> PtrString) -> String -> PtrString
forall a b. (a -> b) -> a -> b
$ String
"Lint warning: Scrutinising floating-point " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                        String
"expression with literal pattern in case " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                        String
"analysis (see #9238).")
          SDoc -> SDoc -> SDoc
$$ String -> SDoc
text String
"scrut" SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
scrut)

     ; case Type -> Maybe TyCon
tyConAppTyCon_maybe (Var -> Type
idType Var
var) of
         Just TyCon
tycon
              | Bool
debugIsOn
              , TyCon -> Bool
isAlgTyCon TyCon
tycon
              , Bool -> Bool
not (TyCon -> Bool
isAbstractTyCon TyCon
tycon)
              , [DataCon] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (TyCon -> [DataCon]
tyConDataCons TyCon
tycon)
              , Bool -> Bool
not (CoreExpr -> Bool
exprIsBottom CoreExpr
scrut)
              -> String -> SDoc -> LintM () -> LintM ()
forall a. String -> SDoc -> a -> a
pprTrace String
"Lint warning: case binder's type has no constructors" (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
idType Var
var))
                        -- This can legitimately happen for type families
                      (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$ () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
         Maybe TyCon
_otherwise -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

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

     ; TCvSubst
subst <- LintM TCvSubst
getTCvSubst
     ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
var_ty Type
scrut_ty (Var -> Type -> Type -> TCvSubst -> SDoc
mkScrutMsg Var
var Type
var_ty Type
scrut_ty TCvSubst
subst)
       -- See CoreSyn Note [Case expression invariants] item (7)

     ; BindingSite -> Var -> (Var -> LintM Type) -> LintM Type
forall a. BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
CaseBind Var
var ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \Var
_ ->
       do { -- Check the alternatives
            (Alt Var -> LintM ()) -> [Alt Var] -> LintM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Type -> Type -> Alt Var -> LintM ()
lintCoreAlt Type
scrut_ty Type
alt_ty) [Alt Var]
alts
          ; CoreExpr -> Type -> [Alt Var] -> LintM ()
checkCaseAlts CoreExpr
e Type
scrut_ty [Alt Var]
alts
          ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
alt_ty } }

checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
-- 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
-- c) Check that there's a default for infinite types
-- NB: Algebraic cases are not necessarily exhaustive, because
--     the simplifier correctly eliminates case that can't
--     possibly match.

checkCaseAlts :: CoreExpr -> Type -> [Alt Var] -> LintM ()
checkCaseAlts CoreExpr
e Type
ty [Alt Var]
alts =
  do { Bool -> SDoc -> LintM ()
checkL ((Alt Var -> Bool) -> [Alt Var] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Alt Var -> Bool
forall b c. (AltCon, b, c) -> Bool
non_deflt [Alt Var]
con_alts) (CoreExpr -> SDoc
mkNonDefltMsg CoreExpr
e)
         -- See CoreSyn Note [Case expression invariants] item (2)

     ; Bool -> SDoc -> LintM ()
checkL ([Alt Var] -> Bool
forall a b. [(AltCon, a, b)] -> Bool
increasing_tag [Alt Var]
con_alts) (CoreExpr -> SDoc
mkNonIncreasingAltsMsg CoreExpr
e)
         -- See CoreSyn Note [Case expression invariants] item (3)

          -- For types Int#, Word# with an infinite (well, large!) number of
          -- possible values, there should usually be a DEFAULT case
          -- But (see Note [Empty case alternatives] in CoreSyn) it's ok to
          -- have *no* case alternatives.
          -- In effect, this is a kind of partial test. I suppose it's possible
          -- that we might *know* that 'x' was 1 or 2, in which case
          --   case x of { 1 -> e1; 2 -> e2 }
          -- would be fine.
     ; Bool -> SDoc -> LintM ()
checkL (Maybe CoreExpr -> Bool
forall a. Maybe a -> Bool
isJust Maybe CoreExpr
maybe_deflt Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
is_infinite_ty Bool -> Bool -> Bool
|| [Alt Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Alt Var]
alts)
              (CoreExpr -> SDoc
nonExhaustiveAltsMsg CoreExpr
e) }
  where
    ([Alt Var]
con_alts, Maybe CoreExpr
maybe_deflt) = [Alt Var] -> ([Alt Var], Maybe CoreExpr)
forall a b. [(AltCon, [a], b)] -> ([(AltCon, [a], b)], Maybe b)
findDefault [Alt Var]
alts

        -- Check that successive alternatives have strictly increasing tags
    increasing_tag :: [(AltCon, a, b)] -> Bool
increasing_tag ((AltCon, a, b)
alt1 : rest :: [(AltCon, a, b)]
rest@( (AltCon, a, b)
alt2 : [(AltCon, a, b)]
_)) = (AltCon, a, b)
alt1 (AltCon, a, b) -> (AltCon, a, b) -> Bool
forall a b. (AltCon, a, b) -> (AltCon, a, b) -> Bool
`ltAlt` (AltCon, a, b)
alt2 Bool -> Bool -> Bool
&& [(AltCon, a, b)] -> Bool
increasing_tag [(AltCon, a, b)]
rest
    increasing_tag [(AltCon, a, b)]
_                         = Bool
True

    non_deflt :: (AltCon, b, c) -> Bool
non_deflt (AltCon
DEFAULT, b
_, c
_) = Bool
False
    non_deflt (AltCon, b, c)
_               = Bool
True

    is_infinite_ty :: Bool
is_infinite_ty = case Type -> Maybe TyCon
tyConAppTyCon_maybe Type
ty of
                        Maybe TyCon
Nothing    -> Bool
False
                        Just TyCon
tycon -> TyCon -> Bool
isPrimTyCon TyCon
tycon

lintAltExpr :: CoreExpr -> OutType -> LintM ()
lintAltExpr :: CoreExpr -> Type -> LintM ()
lintAltExpr CoreExpr
expr Type
ann_ty
  = do { Type
actual_ty <- CoreExpr -> LintM Type
lintCoreExpr CoreExpr
expr
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
actual_ty Type
ann_ty (CoreExpr -> Type -> Type -> SDoc
mkCaseAltMsg CoreExpr
expr Type
actual_ty Type
ann_ty) }
         -- See CoreSyn Note [Case expression invariants] item (6)

lintCoreAlt :: OutType          -- Type of scrutinee
            -> OutType          -- Type of the alternative
            -> CoreAlt
            -> LintM ()
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoreAlt :: Type -> Type -> Alt Var -> LintM ()
lintCoreAlt Type
_ Type
alt_ty (AltCon
DEFAULT, [Var]
args, CoreExpr
rhs) =
  do { Bool -> SDoc -> LintM ()
lintL ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
args) ([Var] -> SDoc
mkDefaultArgsMsg [Var]
args)
     ; CoreExpr -> Type -> LintM ()
lintAltExpr CoreExpr
rhs Type
alt_ty }

lintCoreAlt Type
scrut_ty Type
alt_ty (LitAlt Literal
lit, [Var]
args, CoreExpr
rhs)
  | Literal -> Bool
litIsLifted Literal
lit
  = SDoc -> LintM ()
forall a. SDoc -> LintM a
failWithL SDoc
integerScrutinisedMsg
  | Bool
otherwise
  = do { Bool -> SDoc -> LintM ()
lintL ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
args) ([Var] -> SDoc
mkDefaultArgsMsg [Var]
args)
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
lit_ty Type
scrut_ty (Type -> Type -> SDoc
mkBadPatMsg Type
lit_ty Type
scrut_ty)
       ; CoreExpr -> Type -> LintM ()
lintAltExpr CoreExpr
rhs Type
alt_ty }
  where
    lit_ty :: Type
lit_ty = Literal -> Type
literalType Literal
lit

lintCoreAlt Type
scrut_ty Type
alt_ty alt :: Alt Var
alt@(DataAlt DataCon
con, [Var]
args, CoreExpr
rhs)
  | TyCon -> Bool
isNewTyCon (DataCon -> TyCon
dataConTyCon DataCon
con)
  = SDoc -> LintM ()
addErrL (Type -> Alt Var -> SDoc
mkNewTyDataConAltMsg Type
scrut_ty Alt Var
alt)
  | Just (TyCon
tycon, [Type]
tycon_arg_tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
scrut_ty
  = LintLocInfo -> LintM () -> LintM ()
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Alt Var -> LintLocInfo
CaseAlt Alt Var
alt) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$  do
    {   -- First instantiate the universally quantified
        -- type variables of the data constructor
        -- We've already check
      Bool -> SDoc -> LintM ()
lintL (TyCon
tycon TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== DataCon -> TyCon
dataConTyCon DataCon
con) (TyCon -> DataCon -> SDoc
mkBadConMsg TyCon
tycon DataCon
con)
    ; let con_payload_ty :: Type
con_payload_ty = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (DataCon -> Type
dataConRepType DataCon
con) [Type]
tycon_arg_tys

        -- And now bring the new binders into scope
    ; BindingSite -> [Var] -> ([Var] -> LintM ()) -> LintM ()
forall a. BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders BindingSite
CasePatBind [Var]
args (([Var] -> LintM ()) -> LintM ())
-> ([Var] -> LintM ()) -> LintM ()
forall a b. (a -> b) -> a -> b
$ \ [Var]
args' -> do
    { LintLocInfo -> LintM () -> LintM ()
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Alt Var -> LintLocInfo
CasePat Alt Var
alt) (Type -> Type -> [Var] -> LintM ()
lintAltBinders Type
scrut_ty Type
con_payload_ty [Var]
args')
    ; CoreExpr -> Type -> LintM ()
lintAltExpr CoreExpr
rhs Type
alt_ty } }

  | Bool
otherwise   -- Scrut-ty is wrong shape
  = SDoc -> LintM ()
addErrL (Type -> Alt Var -> SDoc
mkBadAltMsg Type
scrut_ty Alt Var
alt)

{-
************************************************************************
*                                                                      *
\subsection[lint-types]{Types}
*                                                                      *
************************************************************************
-}

-- When we lint binders, we (one at a time and in order):
--  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
lintBinders :: BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders :: BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders BindingSite
_    []         [Var] -> LintM a
linterF = [Var] -> LintM a
linterF []
lintBinders BindingSite
site (Var
var:[Var]
vars) [Var] -> LintM a
linterF = BindingSite -> Var -> (Var -> LintM a) -> LintM a
forall a. BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
site Var
var ((Var -> LintM a) -> LintM a) -> (Var -> LintM a) -> LintM a
forall a b. (a -> b) -> a -> b
$ \Var
var' ->
                                      BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
forall a. BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders BindingSite
site [Var]
vars (([Var] -> LintM a) -> LintM a) -> ([Var] -> LintM a) -> LintM a
forall a b. (a -> b) -> a -> b
$ \ [Var]
vars' ->
                                      [Var] -> LintM a
linterF (Var
var'Var -> [Var] -> [Var]
forall a. a -> [a] -> [a]
:[Var]
vars')

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintBinder :: BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder :: BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder BindingSite
site Var
var Var -> LintM a
linterF
  | Var -> Bool
isTyVar Var
var = Var -> (Var -> LintM a) -> LintM a
forall a. Var -> (Var -> LintM a) -> LintM a
lintTyBndr                  Var
var Var -> LintM a
linterF
  | Var -> Bool
isCoVar Var
var = Var -> (Var -> LintM a) -> LintM a
forall a. Var -> (Var -> LintM a) -> LintM a
lintCoBndr                  Var
var Var -> LintM a
linterF
  | Bool
otherwise   = TopLevelFlag -> BindingSite -> Var -> (Var -> LintM a) -> LintM a
forall a.
TopLevelFlag -> BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintIdBndr TopLevelFlag
NotTopLevel BindingSite
site Var
var Var -> LintM a
linterF

lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
lintTyBndr :: Var -> (Var -> LintM a) -> LintM a
lintTyBndr Var
tv Var -> LintM a
thing_inside
  = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; let (TCvSubst
subst', Var
tv') = HasCallStack => TCvSubst -> Var -> (TCvSubst, Var)
TCvSubst -> Var -> (TCvSubst, Var)
substTyVarBndr TCvSubst
subst Var
tv
       ; Type -> LintM ()
lintKind (Var -> Type
varType Var
tv')
       ; TCvSubst -> LintM a -> LintM a
forall a. TCvSubst -> LintM a -> LintM a
updateTCvSubst TCvSubst
subst' (Var -> LintM a
thing_inside Var
tv') }

lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
lintCoBndr :: Var -> (Var -> LintM a) -> LintM a
lintCoBndr Var
cv Var -> LintM a
thing_inside
  = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; let (TCvSubst
subst', Var
cv') = HasCallStack => TCvSubst -> Var -> (TCvSubst, Var)
TCvSubst -> Var -> (TCvSubst, Var)
substCoVarBndr TCvSubst
subst Var
cv
       ; Type -> LintM ()
lintKind (Var -> Type
varType Var
cv')
       ; Bool -> SDoc -> LintM ()
lintL (Type -> Bool
isCoVarType (Var -> Type
varType Var
cv'))
               (String -> SDoc
text String
"CoVar with non-coercion type:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
pprTyVar Var
cv)
       ; TCvSubst -> LintM a -> LintM a
forall a. TCvSubst -> LintM a -> LintM a
updateTCvSubst TCvSubst
subst' (Var -> LintM a
thing_inside Var
cv') }

lintLetBndrs :: TopLevelFlag -> [Var] -> LintM a -> LintM a
lintLetBndrs :: TopLevelFlag -> [Var] -> LintM a -> LintM a
lintLetBndrs TopLevelFlag
top_lvl [Var]
ids LintM a
linterF
  = [Var] -> LintM a
go [Var]
ids
  where
    go :: [Var] -> LintM a
go []       = LintM a
linterF
    go (Var
id:[Var]
ids) = TopLevelFlag -> BindingSite -> Var -> (Var -> LintM a) -> LintM a
forall a.
TopLevelFlag -> BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintIdBndr TopLevelFlag
top_lvl BindingSite
LetBind Var
id  ((Var -> LintM a) -> LintM a) -> (Var -> LintM a) -> LintM a
forall a b. (a -> b) -> a -> b
$ \Var
_ ->
                  [Var] -> LintM a
go [Var]
ids

lintIdBndr :: TopLevelFlag -> BindingSite
           -> InVar -> (OutVar -> LintM a) -> LintM a
-- 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
lintIdBndr :: TopLevelFlag -> BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintIdBndr TopLevelFlag
top_lvl BindingSite
bind_site Var
id Var -> LintM a
linterF
  = ASSERT2( isId id, ppr id )
    do { LintFlags
flags <- LintM LintFlags
getLintFlags
       ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (LintFlags -> Bool
lf_check_global_ids LintFlags
flags) Bool -> Bool -> Bool
|| Var -> Bool
isLocalId Var
id)
                (String -> SDoc
text String
"Non-local Id binder" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
id)
                -- See Note [Checking for global Ids]

       -- Check that if the binder is nested, it is not marked as exported
       ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Var -> Bool
isExportedId Var
id) Bool -> Bool -> Bool
|| Bool
is_top_lvl)
           (Var -> SDoc
mkNonTopExportedMsg Var
id)

       -- Check that if the binder is nested, it does not have an external name
       ; Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Name -> Bool
isExternalName (Var -> Name
Var.varName Var
id)) Bool -> Bool -> Bool
|| Bool
is_top_lvl)
           (Var -> SDoc
mkNonTopExternalNameMsg Var
id)

       ; (Type
ty, Type
k) <- LintLocInfo -> LintM (Type, Type) -> LintM (Type, Type)
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Var -> LintLocInfo
IdTy Var
id) (LintM (Type, Type) -> LintM (Type, Type))
-> LintM (Type, Type) -> LintM (Type, Type)
forall a b. (a -> b) -> a -> b
$
                    Type -> LintM (Type, Type)
lintInTy (Var -> Type
idType Var
id)

          -- See Note [Levity polymorphism invariants] in CoreSyn
       ; Bool -> SDoc -> LintM ()
lintL (Var -> Bool
isJoinId Var
id Bool -> Bool -> Bool
|| Bool -> Bool
not (Type -> Bool
isKindLevPoly Type
k))
           (String -> SDoc
text String
"Levity-polymorphic binder:" SDoc -> SDoc -> SDoc
<+>
                 (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
id SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k)))

       -- Check that a join-id is a not-top-level let-binding
       ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var -> Bool
isJoinId Var
id) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
         Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not Bool
is_top_lvl Bool -> Bool -> Bool
&& Bool
is_let_bind) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
         Var -> SDoc
mkBadJoinBindMsg Var
id

       -- Check that the Id does not have type (t1 ~# t2) or (t1 ~R# t2);
       -- if so, it should be a CoVar, and checked by lintCoVarBndr
       ; Bool -> SDoc -> LintM ()
lintL (Bool -> Bool
not (Type -> Bool
isCoVarType Type
ty))
               (String -> SDoc
text String
"Non-CoVar has coercion type" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
id SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)

       ; let id' :: Var
id' = Var -> Type -> Var
setIdType Var
id Type
ty
       ; Var -> LintM a -> LintM a
forall a. Var -> LintM a -> LintM a
addInScopeVar Var
id' (LintM a -> LintM a) -> LintM a -> LintM a
forall a b. (a -> b) -> a -> b
$ (Var -> LintM a
linterF Var
id') }
  where
    is_top_lvl :: Bool
is_top_lvl = TopLevelFlag -> Bool
isTopLevel TopLevelFlag
top_lvl
    is_let_bind :: Bool
is_let_bind = case BindingSite
bind_site of
                    BindingSite
LetBind -> Bool
True
                    BindingSite
_       -> Bool
False

{-
%************************************************************************
%*                                                                      *
             Types
%*                                                                      *
%************************************************************************
-}

lintTypes :: DynFlags
          -> [TyCoVar]   -- Treat these as in scope
          -> [Type]
          -> Maybe MsgDoc -- Nothing => OK
lintTypes :: DynFlags -> [Var] -> [Type] -> Maybe SDoc
lintTypes DynFlags
dflags [Var]
vars [Type]
tys
  | Bag SDoc -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag SDoc
errs = Maybe SDoc
forall a. Maybe a
Nothing
  | Bool
otherwise       = SDoc -> Maybe SDoc
forall a. a -> Maybe a
Just (Bag SDoc -> SDoc
pprMessageBag Bag SDoc
errs)
  where
    in_scope :: InScopeSet
in_scope = InScopeSet
emptyInScopeSet
    (Bag SDoc
_warns, Bag SDoc
errs) = DynFlags
-> LintFlags -> InScopeSet -> LintM () -> (Bag SDoc, Bag SDoc)
forall a.
DynFlags
-> LintFlags -> InScopeSet -> LintM a -> (Bag SDoc, Bag SDoc)
initL DynFlags
dflags LintFlags
defaultLintFlags InScopeSet
in_scope LintM ()
linter
    linter :: LintM ()
linter = BindingSite -> [Var] -> ([Var] -> LintM ()) -> LintM ()
forall a. BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders BindingSite
LambdaBind [Var]
vars (([Var] -> LintM ()) -> LintM ())
-> ([Var] -> LintM ()) -> LintM ()
forall a b. (a -> b) -> a -> b
$ \[Var]
_ ->
             (Type -> LintM (Type, Type)) -> [Type] -> LintM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Type -> LintM (Type, Type)
lintInTy [Type]
tys

lintInTy :: InType -> LintM (LintedType, LintedKind)
-- Types only, not kinds
-- Check the type, and apply the substitution to it
-- See Note [Linting type lets]
lintInTy :: Type -> LintM (Type, Type)
lintInTy Type
ty
  = LintLocInfo -> LintM (Type, Type) -> LintM (Type, Type)
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Type -> LintLocInfo
InType Type
ty) (LintM (Type, Type) -> LintM (Type, Type))
-> LintM (Type, Type) -> LintM (Type, Type)
forall a b. (a -> b) -> a -> b
$
    do  { Type
ty' <- Type -> LintM Type
applySubstTy Type
ty
        ; Type
k  <- Type -> LintM Type
lintType Type
ty'
        ; Type -> LintM ()
lintKind Type
k  -- The kind returned by lintType is already
                      -- a LintedKind but we also want to check that
                      -- k :: *, which lintKind does
        ; (Type, Type) -> LintM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ty', Type
k) }

checkTyCon :: TyCon -> LintM ()
checkTyCon :: TyCon -> LintM ()
checkTyCon TyCon
tc
  = Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (TyCon -> Bool
isTcTyCon TyCon
tc)) (String -> SDoc
text String
"Found TcTyCon:" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc)

-------------------
lintType :: OutType -> LintM LintedKind
-- The returned Kind has itself been linted

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintType :: Type -> LintM Type
lintType (TyVarTy Var
tv)
  = do { Bool -> SDoc -> LintM ()
checkL (Var -> Bool
isTyVar Var
tv) (Var -> SDoc
mkBadTyVarMsg Var
tv)
       ; Var -> LintM ()
lintTyCoVarInScope Var
tv
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Type
tyVarKind Var
tv) }
         -- We checked its kind when we added it to the envt

lintType ty :: Type
ty@(AppTy Type
t1 Type
t2)
  | TyConApp {} <- Type
t1
  = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> LintM Type) -> SDoc -> LintM Type
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"TyConApp to the left of AppTy:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
  | Bool
otherwise
  = do { Type
k1 <- Type -> LintM Type
lintType Type
t1
       ; Type
k2 <- Type -> LintM Type
lintType Type
t2
       ; Type -> Type -> [(Type, Type)] -> LintM Type
lint_ty_app Type
ty Type
k1 [(Type
t2,Type
k2)] }

lintType ty :: Type
ty@(TyConApp TyCon
tc [Type]
tys)
  | TyCon -> Bool
isTypeSynonymTyCon TyCon
tc Bool -> Bool -> Bool
|| TyCon -> Bool
isTypeFamilyTyCon TyCon
tc
  = do { Bool
report_unsat <- LintFlags -> Bool
lf_report_unsat_syns (LintFlags -> Bool) -> LintM LintFlags -> LintM Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LintM LintFlags
getLintFlags
       ; Bool -> Type -> TyCon -> [Type] -> LintM Type
lintTySynFamApp Bool
report_unsat Type
ty TyCon
tc [Type]
tys }

  | TyCon -> Bool
isFunTyCon TyCon
tc
  , [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Int
4
    -- We should never see a saturated application of funTyCon; such
    -- applications should be represented with the FunTy constructor.
    -- See Note [Linting function types] and
    -- Note [Representation of function types].
  = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Saturated application of (->)") Int
2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty))

  | Bool
otherwise  -- Data types, data families, primitive types
  = do { TyCon -> LintM ()
checkTyCon TyCon
tc
       ; [Type]
ks <- (Type -> LintM Type) -> [Type] -> LintM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> LintM Type
lintType [Type]
tys
       ; Type -> Type -> [(Type, Type)] -> LintM Type
lint_ty_app Type
ty (TyCon -> Type
tyConKind TyCon
tc) ([Type]
tys [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Type]
ks) }

-- arrows can related *unlifted* kinds, so this has to be separate from
-- a dependent forall.
lintType ty :: Type
ty@(FunTy AnonArgFlag
_ Type
t1 Type
t2)
  = do { Type
k1 <- Type -> LintM Type
lintType Type
t1
       ; Type
k2 <- Type -> LintM Type
lintType Type
t2
       ; SDoc -> Type -> Type -> LintM Type
lintArrow (String -> SDoc
text String
"type or kind" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)) Type
k1 Type
k2 }

lintType t :: Type
t@(ForAllTy (Bndr Var
tv ArgFlag
_vis) Type
ty)
  -- forall over types
  | Var -> Bool
isTyVar Var
tv
  = Var -> (Var -> LintM Type) -> LintM Type
forall a. Var -> (Var -> LintM a) -> LintM a
lintTyBndr Var
tv ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \Var
tv' ->
    do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k (String -> SDoc
text String
"the body of forall:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)
       ; case [Var] -> Type -> Maybe Type
occCheckExpand [Var
tv'] Type
k of  -- See Note [Stupid type synonyms]
           Just Type
k' -> Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
k'
           Maybe Type
Nothing -> SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Variable escape in forall:")
                                    Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t
                                            , String -> SDoc
text String
"kind:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k ]))
    }

lintType t :: Type
t@(ForAllTy (Bndr Var
cv ArgFlag
_vis) Type
ty)
  -- forall over coercions
  = do { Bool -> SDoc -> LintM ()
lintL (Var -> Bool
isCoVar Var
cv)
               (String -> SDoc
text String
"Non-Tyvar or Non-Covar bound in type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)
       ; Bool -> SDoc -> LintM ()
lintL (Var
cv Var -> VarSet -> Bool
`elemVarSet` Type -> VarSet
tyCoVarsOfType Type
ty)
               (String -> SDoc
text String
"Covar does not occur in the body:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)
       ; Var -> (Var -> LintM Type) -> LintM Type
forall a. Var -> (Var -> LintM a) -> LintM a
lintCoBndr Var
cv ((Var -> LintM Type) -> LintM Type)
-> (Var -> LintM Type) -> LintM Type
forall a b. (a -> b) -> a -> b
$ \Var
_ ->
    do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k (String -> SDoc
text String
"the body of forall:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
liftedTypeKind
           -- We don't check variable escape here. Namely, k could refer to cv'
           -- See Note [NthCo and newtypes] in TyCoRep
    }}

lintType ty :: Type
ty@(LitTy TyLit
l) = TyLit -> LintM ()
lintTyLit TyLit
l LintM () -> LintM Type -> LintM Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty)

lintType (CastTy Type
ty Coercion
co)
  = do { Type
k1 <- Type -> LintM Type
lintType Type
ty
       ; (Type
k1', Type
k2) <- Coercion -> LintM (Type, Type)
lintStarCoercion Coercion
co
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
k1 Type
k1' (Type -> Coercion -> Type -> Type -> SDoc
mkCastTyErr Type
ty Coercion
co Type
k1' Type
k1)
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
k2 }

lintType (CoercionTy Coercion
co)
  = do { (Type
k1, Type
k2, Type
ty1, Type
ty2, Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> LintM Type) -> Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Type -> Type -> Type -> Type
mkHeteroCoercionType Role
r Type
k1 Type
k2 Type
ty1 Type
ty2 }

{- Note [Stupid type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#14939)
   type Alg cls ob = ob
   f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b

Here 'cls' appears free in b's kind, which would usually be illegal
(because in (forall a. ty), ty's kind should not mention 'a'). But
#in this case (Alg cls *) = *, so all is well.  Currently we allow
this, and make Lint expand synonyms where necessary to make it so.

c.f. TcUnify.occCheckExpand and CoreUtils.coreAltsType which deal
with the same problem. A single systematic solution eludes me.
-}

-----------------
lintTySynFamApp :: Bool -> Type -> TyCon -> [Type] -> LintM LintedKind
-- The TyCon is a type synonym or a type family (not a data family)
-- See Note [Linting type synonym applications]
-- c.f. TcValidity.check_syn_tc_app
lintTySynFamApp :: Bool -> Type -> TyCon -> [Type] -> LintM Type
lintTySynFamApp Bool
report_unsat Type
ty TyCon
tc [Type]
tys
  | Bool
report_unsat   -- Report unsaturated only if report_unsat is on
  , [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthLessThan` TyCon -> Int
tyConArity TyCon
tc
  = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Un-saturated type application") Int
2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty))

  -- Deal with type synonyms
  | Just ([(Var, Type)]
tenv, Type
rhs, [Type]
tys') <- TyCon -> [Type] -> Maybe ([(Var, Type)], Type, [Type])
forall tyco. TyCon -> [tyco] -> Maybe ([(Var, tyco)], Type, [tyco])
expandSynTyCon_maybe TyCon
tc [Type]
tys
  , let expanded_ty :: Type
expanded_ty = Type -> [Type] -> Type
mkAppTys (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy ([(Var, Type)] -> TCvSubst
mkTvSubstPrs [(Var, Type)]
tenv) Type
rhs) [Type]
tys'
  = do { -- Kind-check the argument types, but without reporting
         -- un-saturated type families/synonyms
         [Type]
ks <- Bool -> LintM [Type] -> LintM [Type]
forall a. Bool -> LintM a -> LintM a
setReportUnsat Bool
False ((Type -> LintM Type) -> [Type] -> LintM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> LintM Type
lintType [Type]
tys)

       ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
report_unsat (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
         do { Type
_ <- Type -> LintM Type
lintType Type
expanded_ty
            ; () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return () }

       ; Type -> Type -> [(Type, Type)] -> LintM Type
lint_ty_app Type
ty (TyCon -> Type
tyConKind TyCon
tc) ([Type]
tys [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Type]
ks) }

  -- Otherwise this must be a type family
  | Bool
otherwise
  = do { [Type]
ks <- (Type -> LintM Type) -> [Type] -> LintM [Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Type -> LintM Type
lintType [Type]
tys
       ; Type -> Type -> [(Type, Type)] -> LintM Type
lint_ty_app Type
ty (TyCon -> Type
tyConKind TyCon
tc) ([Type]
tys [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Type]
ks) }

-----------------
lintKind :: OutKind -> LintM ()
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintKind :: Type -> LintM ()
lintKind Type
k = do { Type
sk <- Type -> LintM Type
lintType Type
k
                ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type -> Bool
classifiesTypeWithValues Type
sk)
                         (SDoc -> LintM ()
addErrL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Ill-kinded kind:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k)
                                      Int
2 (String -> SDoc
text String
"has kind:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
sk))) }

-----------------
-- Confirms that a type is really *, #, Constraint etc
checkValueKind :: OutKind -> SDoc -> LintM ()
checkValueKind :: Type -> SDoc -> LintM ()
checkValueKind Type
k SDoc
doc
  = Bool -> SDoc -> LintM ()
lintL (Type -> Bool
classifiesTypeWithValues Type
k)
          (String -> SDoc
text String
"Non-*-like kind when *-like expected:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k SDoc -> SDoc -> SDoc
$$
           String -> SDoc
text String
"when checking" SDoc -> SDoc -> SDoc
<+> SDoc
doc)

-----------------
lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintArrow :: SDoc -> Type -> Type -> LintM Type
lintArrow SDoc
what Type
k1 Type
k2   -- Eg lintArrow "type or kind `blah'" k1 k2
                       -- or lintarrow "coercion `blah'" k1 k2
  = do { Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type -> Bool
classifiesTypeWithValues Type
k1) (SDoc -> LintM ()
addErrL (SDoc -> Type -> SDoc
forall a. Outputable a => SDoc -> a -> SDoc
msg (String -> SDoc
text String
"argument") Type
k1))
       ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type -> Bool
classifiesTypeWithValues Type
k2) (SDoc -> LintM ()
addErrL (SDoc -> Type -> SDoc
forall a. Outputable a => SDoc -> a -> SDoc
msg (String -> SDoc
text String
"result")   Type
k2))
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
liftedTypeKind }
  where
    msg :: SDoc -> a -> SDoc
msg SDoc
ar a
k
      = [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Ill-kinded" SDoc -> SDoc -> SDoc
<+> SDoc
ar)
                  Int
2 (String -> SDoc
text String
"in" SDoc -> SDoc -> SDoc
<+> SDoc
what)
             , SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"kind:" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
k ]

-----------------
lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
lint_ty_app :: Type -> Type -> [(Type, Type)] -> LintM Type
lint_ty_app Type
ty Type
k [(Type, Type)]
tys
  = SDoc -> Type -> [(Type, Type)] -> LintM Type
lint_app (String -> SDoc
text String
"type" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)) Type
k [(Type, Type)]
tys

----------------
lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
lint_co_app :: Coercion -> Type -> [(Type, Type)] -> LintM Type
lint_co_app Coercion
ty Type
k [(Type, Type)]
tys
  = SDoc -> Type -> [(Type, Type)] -> LintM Type
lint_app (String -> SDoc
text String
"coercion" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
ty)) Type
k [(Type, Type)]
tys

----------------
lintTyLit :: TyLit -> LintM ()
lintTyLit :: TyLit -> LintM ()
lintTyLit (NumTyLit Integer
n)
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0    = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  | Bool
otherwise = SDoc -> LintM ()
forall a. SDoc -> LintM a
failWithL SDoc
msg
    where msg :: SDoc
msg = String -> SDoc
text String
"Negative type literal:" SDoc -> SDoc -> SDoc
<+> Integer -> SDoc
integer Integer
n
lintTyLit (StrTyLit FastString
_) = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()

lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
-- (lint_app d fun_kind arg_tys)
--    We have an application (f arg_ty1 .. arg_tyn),
--    where f :: fun_kind
-- Takes care of linting the OutTypes

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lint_app :: SDoc -> Type -> [(Type, Type)] -> LintM Type
lint_app SDoc
doc Type
kfn [(Type, Type)]
kas
    = do { InScopeSet
in_scope <- LintM InScopeSet
getInScope
         -- We need the in_scope set to satisfy the invariant in
         -- Note [The substitution invariant] in TyCoSubst
         ; (Type -> (Type, Type) -> LintM Type)
-> Type -> [(Type, Type)] -> LintM Type
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (InScopeSet -> Type -> (Type, Type) -> LintM Type
go_app InScopeSet
in_scope) Type
kfn [(Type, Type)]
kas }
  where
    fail_msg :: SDoc -> SDoc
fail_msg SDoc
extra = [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Kind application error in") Int
2 SDoc
doc
                          , Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"Function kind =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
kfn)
                          , Int -> SDoc -> SDoc
nest Int
2 (String -> SDoc
text String
"Arg kinds =" SDoc -> SDoc -> SDoc
<+> [(Type, Type)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(Type, Type)]
kas)
                          , SDoc
extra ]

    go_app :: InScopeSet -> Type -> (Type, Type) -> LintM Type
go_app InScopeSet
in_scope Type
kfn (Type, Type)
tka
      | Just Type
kfn' <- Type -> Maybe Type
coreView Type
kfn
      = InScopeSet -> Type -> (Type, Type) -> LintM Type
go_app InScopeSet
in_scope Type
kfn' (Type, Type)
tka

    go_app InScopeSet
_ (FunTy AnonArgFlag
_ Type
kfa Type
kfb) tka :: (Type, Type)
tka@(Type
_,Type
ka)
      = do { Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
ka Type -> Type -> Bool
`eqType` Type
kfa) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
             SDoc -> LintM ()
addErrL (SDoc -> SDoc
fail_msg (String -> SDoc
text String
"Fun:" SDoc -> SDoc -> SDoc
<+> (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
kfa SDoc -> SDoc -> SDoc
$$ (Type, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type, Type)
tka)))
           ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
kfb }

    go_app InScopeSet
in_scope (ForAllTy (Bndr Var
kv ArgFlag
_vis) Type
kfn) tka :: (Type, Type)
tka@(Type
ta,Type
ka)
      = do { let kv_kind :: Type
kv_kind = Var -> Type
varType Var
kv
           ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
ka Type -> Type -> Bool
`eqType` Type
kv_kind) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
             SDoc -> LintM ()
addErrL (SDoc -> SDoc
fail_msg (String -> SDoc
text String
"Forall:" SDoc -> SDoc -> SDoc
<+> (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
kv SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
kv_kind SDoc -> SDoc -> SDoc
$$ (Type, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type, Type)
tka)))
           ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> LintM Type) -> Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (TCvSubst -> Var -> Type -> TCvSubst
extendTCvSubst (InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope) Var
kv Type
ta) Type
kfn }

    go_app InScopeSet
_ Type
kfn (Type, Type)
ka
       = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> SDoc
fail_msg (String -> SDoc
text String
"Not a fun:" SDoc -> SDoc -> SDoc
<+> (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
kfn SDoc -> SDoc -> SDoc
$$ (Type, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type, Type)
ka)))

{- *********************************************************************
*                                                                      *
        Linting rules
*                                                                      *
********************************************************************* -}

lintCoreRule :: OutVar -> OutType -> CoreRule -> LintM ()
lintCoreRule :: Var -> Type -> CoreRule -> LintM ()
lintCoreRule Var
_ Type
_ (BuiltinRule {})
  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- Don't bother

lintCoreRule Var
fun Type
fun_ty rule :: CoreRule
rule@(Rule { ru_name :: CoreRule -> FastString
ru_name = FastString
name, ru_bndrs :: CoreRule -> [Var]
ru_bndrs = [Var]
bndrs
                                   , ru_args :: CoreRule -> [CoreExpr]
ru_args = [CoreExpr]
args, ru_rhs :: CoreRule -> CoreExpr
ru_rhs = CoreExpr
rhs })
  = BindingSite -> [Var] -> ([Var] -> LintM ()) -> LintM ()
forall a. BindingSite -> [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders BindingSite
LambdaBind [Var]
bndrs (([Var] -> LintM ()) -> LintM ())
-> ([Var] -> LintM ()) -> LintM ()
forall a b. (a -> b) -> a -> b
$ \ [Var]
_ ->
    do { Type
lhs_ty <- Type -> [CoreExpr] -> LintM Type
lintCoreArgs Type
fun_ty [CoreExpr]
args
       ; Type
rhs_ty <- case Var -> Maybe Int
isJoinId_maybe Var
fun of
                     Just Int
join_arity
                       -> do { Bool -> SDoc -> LintM ()
checkL ([CoreExpr]
args [CoreExpr] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthIs` Int
join_arity) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
                                Var -> Int -> CoreRule -> SDoc
mkBadJoinPointRuleMsg Var
fun Int
join_arity CoreRule
rule
                               -- See Note [Rules for join points]
                             ; CoreExpr -> LintM Type
lintCoreExpr CoreExpr
rhs }
                     Maybe Int
_ -> LintM Type -> LintM Type
forall a. LintM a -> LintM a
markAllJoinsBad (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ CoreExpr -> LintM Type
lintCoreExpr CoreExpr
rhs
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
lhs_ty Type
rhs_ty (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
         (SDoc
rule_doc SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"lhs type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
lhs_ty
                            , String -> SDoc
text String
"rhs type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs_ty
                            , String -> SDoc
text String
"fun_ty:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fun_ty ])
       ; let bad_bndrs :: [Var]
bad_bndrs = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
is_bad_bndr [Var]
bndrs

       ; Bool -> SDoc -> LintM ()
checkL ([Var] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Var]
bad_bndrs)
                (SDoc
rule_doc SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"unbound" SDoc -> SDoc -> SDoc
<+> [Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
bad_bndrs)
            -- See Note [Linting rules]
    }
  where
    rule_doc :: SDoc
rule_doc = String -> SDoc
text String
"Rule" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
doubleQuotes (FastString -> SDoc
ftext FastString
name) SDoc -> SDoc -> SDoc
<> SDoc
colon

    lhs_fvs :: VarSet
lhs_fvs = [CoreExpr] -> VarSet
exprsFreeVars [CoreExpr]
args
    rhs_fvs :: VarSet
rhs_fvs = CoreExpr -> VarSet
exprFreeVars CoreExpr
rhs

    is_bad_bndr :: Var -> Bool
    -- See Note [Unbound RULE binders] in Rules
    is_bad_bndr :: Var -> Bool
is_bad_bndr Var
bndr = Bool -> Bool
not (Var
bndr Var -> VarSet -> Bool
`elemVarSet` VarSet
lhs_fvs)
                    Bool -> Bool -> Bool
&& Var
bndr Var -> VarSet -> Bool
`elemVarSet` VarSet
rhs_fvs
                    Bool -> Bool -> Bool
&& Maybe Coercion -> Bool
forall a. Maybe a -> Bool
isNothing (Var -> Maybe Coercion
isReflCoVar_maybe Var
bndr)


{- Note [Linting rules]
~~~~~~~~~~~~~~~~~~~~~~~
It's very bad if simplifying a rule means that one of the template
variables (ru_bndrs) that /is/ mentioned on the RHS becomes
not-mentioned in the LHS (ru_args).  How can that happen?  Well, in
#10602, SpecConstr stupidly constructed a rule like

  forall x,c1,c2.
     f (x |> c1 |> c2) = ....

But simplExpr collapses those coercions into one.  (Indeed in
#10602, it collapsed to the identity and was removed altogether.)

We don't have a great story for what to do here, but at least
this check will nail it.

NB (#11643): it's possible that a variable listed in the
binders becomes not-mentioned on both LHS and RHS.  Here's a silly
example:
   RULE forall x y. f (g x y) = g (x+1) (y-1)
And suppose worker/wrapper decides that 'x' is Absent.  Then
we'll end up with
   RULE forall x y. f ($gw y) = $gw (x+1)
This seems sufficiently obscure that there isn't enough payoff to
try to trim the forall'd binder list.

Note [Rules for join points]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~

A join point cannot be partially applied. However, the left-hand side of a rule
for a join point is effectively a *pattern*, not a piece of code, so there's an
argument to be made for allowing a situation like this:

  join $sj :: Int -> Int -> String
       $sj n m = ...
       j :: forall a. Eq a => a -> a -> String
       {-# RULES "SPEC j" jump j @ Int $dEq = jump $sj #-}
       j @a $dEq x y = ...

Applying this rule can't turn a well-typed program into an ill-typed one, so
conceivably we could allow it. But we can always eta-expand such an
"undersaturated" rule (see 'CoreArity.etaExpandToJoinPointRule'), and in fact
the simplifier would have to in order to deal with the RHS. So we take a
conservative view and don't allow undersaturated rules for join points. See
Note [Rules and join points] in OccurAnal for further discussion.
-}

{-
************************************************************************
*                                                                      *
         Linting coercions
*                                                                      *
************************************************************************
-}

lintInCo :: InCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
-- Check the coercion, and apply the substitution to it
-- See Note [Linting type lets]
lintInCo :: Coercion -> LintM (Type, Type, Type, Type, Role)
lintInCo Coercion
co
  = LintLocInfo
-> LintM (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (Coercion -> LintLocInfo
InCo Coercion
co) (LintM (Type, Type, Type, Type, Role)
 -> LintM (Type, Type, Type, Type, Role))
-> LintM (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a b. (a -> b) -> a -> b
$
    do  { Coercion
co' <- Coercion -> LintM Coercion
applySubstCo Coercion
co
        ; Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co' }

-- lints a coercion, confirming that its lh kind and its rh kind are both *
-- also ensures that the role is Nominal
lintStarCoercion :: OutCoercion -> LintM (LintedType, LintedType)
lintStarCoercion :: Coercion -> LintM (Type, Type)
lintStarCoercion Coercion
g
  = do { (Type
k1, Type
k2, Type
t1, Type
t2, Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
g
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k1 (String -> SDoc
text String
"the kind of the left type in" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
g)
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k2 (String -> SDoc
text String
"the kind of the right type in" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
g)
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
g Role
Nominal Role
r
       ; (Type, Type) -> LintM (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
t1, Type
t2) }

lintCoercion :: OutCoercion -> LintM (LintedKind, LintedKind, LintedType, LintedType, Role)
-- Check the kind of a coercion term, returning the kind
-- Post-condition: the returned OutTypes are lint-free
--
-- If   lintCoercion co = (k1, k2, s1, s2, r)
-- then co :: s1 ~r s2
--      s1 :: k1
--      s2 :: k2

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoercion :: Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion (Refl Type
ty)
  = do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k, Type
k, Type
ty, Type
ty, Role
Nominal) }

lintCoercion (GRefl Role
r Type
ty MCoercion
MRefl)
  = do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k, Type
k, Type
ty, Type
ty, Role
r) }

lintCoercion (GRefl Role
r Type
ty (MCo Coercion
co))
  = do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; (Type
_, Type
_, Type
k1, Type
k2, Role
r') <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
k Type
k1
               (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"GRefl coercion kind mis-match:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
                   Int
2 ([SDoc] -> SDoc
vcat [Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k1]))
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co Role
Nominal Role
r'
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k1, Type
k2, Type
ty, Type -> Coercion -> Type
mkCastTy Type
ty Coercion
co, Role
r) }

lintCoercion co :: Coercion
co@(TyConAppCo Role
r TyCon
tc [Coercion]
cos)
  | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
funTyConKey
  , [Coercion
_rep1,Coercion
_rep2,Coercion
_co1,Coercion
_co2] <- [Coercion]
cos
  = do { SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Saturated TyConAppCo (->):" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
       } -- All saturated TyConAppCos should be FunCos

  | Just {} <- TyCon -> Maybe ([Var], Type)
synTyConDefn_maybe TyCon
tc
  = SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Synonym in TyConAppCo:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)

  | Bool
otherwise
  = do { TyCon -> LintM ()
checkTyCon TyCon
tc
       ; ([Type]
k's, [Type]
ks, [Type]
ss, [Type]
ts, [Role]
rs) <- (Coercion -> LintM (Type, Type, Type, Type, Role))
-> [Coercion] -> LintM ([Type], [Type], [Type], [Type], [Role])
forall (m :: * -> *) a b c d e f.
Monad m =>
(a -> m (b, c, d, e, f)) -> [a] -> m ([b], [c], [d], [e], [f])
mapAndUnzip5M Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion [Coercion]
cos
       ; Type
k' <- Coercion -> Type -> [(Type, Type)] -> LintM Type
lint_co_app Coercion
co (TyCon -> Type
tyConKind TyCon
tc) ([Type]
ss [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Type]
k's)
       ; Type
k <- Coercion -> Type -> [(Type, Type)] -> LintM Type
lint_co_app Coercion
co (TyCon -> Type
tyConKind TyCon
tc) ([Type]
ts [Type] -> [Type] -> [(Type, Type)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Type]
ks)
       ; [()]
_ <- (Coercion -> Role -> Role -> LintM ())
-> [Coercion] -> [Role] -> [Role] -> LintM [()]
forall (m :: * -> *) a b c d.
Monad m =>
(a -> b -> c -> m d) -> [a] -> [b] -> [c] -> m [d]
zipWith3M Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole [Coercion]
cos (Role -> TyCon -> [Role]
tyConRolesX Role
r TyCon
tc) [Role]
rs
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k', Type
k, TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
ss, TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
ts, Role
r) }

lintCoercion co :: Coercion
co@(AppCo Coercion
co1 Coercion
co2)
  | TyConAppCo {} <- Coercion
co1
  = SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"TyConAppCo to the left of AppCo:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
  | Just (TyConApp {}, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co1
  = SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Refl (TyConApp ...) to the left of AppCo:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
  | Bool
otherwise
  = do { (Type
k1,  Type
k2,  Type
s1, Type
s2, Role
r1) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co1
       ; (Type
k'1, Type
k'2, Type
t1, Type
t2, Role
r2) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co2
       ; Type
k3 <- Coercion -> Type -> [(Type, Type)] -> LintM Type
lint_co_app Coercion
co Type
k1 [(Type
t1,Type
k'1)]
       ; Type
k4 <- Coercion -> Type -> [(Type, Type)] -> LintM Type
lint_co_app Coercion
co Type
k2 [(Type
t2,Type
k'2)]
       ; if Role
r1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Phantom
         then Bool -> SDoc -> LintM ()
lintL (Role
r2 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Phantom Bool -> Bool -> Bool
|| Role
r2 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal)
                     (String -> SDoc
text String
"Second argument in AppCo cannot be R:" SDoc -> SDoc -> SDoc
$$
                      Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
         else Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co Role
Nominal Role
r2
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k3, Type
k4, Type -> Type -> Type
mkAppTy Type
s1 Type
t1, Type -> Type -> Type
mkAppTy Type
s2 Type
t2, Role
r1) }

----------
lintCoercion (ForAllCo Var
tv1 Coercion
kind_co Coercion
co)
  -- forall over types
  | Var -> Bool
isTyVar Var
tv1
  = do { (Type
_, Type
k2) <- Coercion -> LintM (Type, Type)
lintStarCoercion Coercion
kind_co
       ; let tv2 :: Var
tv2 = Var -> Type -> Var
setTyVarKind Var
tv1 Type
k2
       ; Var
-> LintM (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a. Var -> LintM a -> LintM a
addInScopeVar Var
tv1 (LintM (Type, Type, Type, Type, Role)
 -> LintM (Type, Type, Type, Type, Role))
-> LintM (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a b. (a -> b) -> a -> b
$
    do {
       ; (Type
k3, Type
k4, Type
t1, Type
t2, Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; InScopeSet
in_scope <- LintM InScopeSet
getInScope
       ; let tyl :: Type
tyl = Var -> Type -> Type
mkInvForAllTy Var
tv1 Type
t1
             subst :: TCvSubst
subst = InScopeSet -> TvSubstEnv -> TCvSubst
mkTvSubst InScopeSet
in_scope (TvSubstEnv -> TCvSubst) -> TvSubstEnv -> TCvSubst
forall a b. (a -> b) -> a -> b
$
                     -- We need both the free vars of the `t2` and the
                     -- free vars of the range of the substitution in
                     -- scope. All the free vars of `t2` and `kind_co` should
                     -- already be in `in_scope`, because they've been
                     -- linted and `tv2` has the same unique as `tv1`.
                     -- See Note [The substitution invariant] in TyCoSubst.
                     Var -> Type -> TvSubstEnv
forall a. Var -> a -> VarEnv a
unitVarEnv Var
tv1 (Var -> Type
TyVarTy Var
tv2 Type -> Coercion -> Type
`mkCastTy` Coercion -> Coercion
mkSymCo Coercion
kind_co)
             tyr :: Type
tyr = Var -> Type -> Type
mkInvForAllTy Var
tv2 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                   HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
t2
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k3, Type
k4, Type
tyl, Type
tyr, Role
r) } }

lintCoercion (ForAllCo Var
cv1 Coercion
kind_co Coercion
co)
  -- forall over coercions
  = ASSERT( isCoVar cv1 )
    do { Bool -> SDoc -> LintM ()
lintL (Var -> Coercion -> Bool
almostDevoidCoVarOfCo Var
cv1 Coercion
co)
               (String -> SDoc
text String
"Covar can only appear in Refl and GRefl: " SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
       ; (Type
_, Type
k2) <- Coercion -> LintM (Type, Type)
lintStarCoercion Coercion
kind_co
       ; let cv2 :: Var
cv2 = Var -> Type -> Var
setVarType Var
cv1 Type
k2
       ; Var
-> LintM (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a. Var -> LintM a -> LintM a
addInScopeVar Var
cv1 (LintM (Type, Type, Type, Type, Role)
 -> LintM (Type, Type, Type, Type, Role))
-> LintM (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a b. (a -> b) -> a -> b
$
    do {
       ; (Type
k3, Type
k4, Type
t1, Type
t2, Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k3 (String -> SDoc
text String
"the body of a ForAllCo over covar:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k4 (String -> SDoc
text String
"the body of a ForAllCo over covar:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
           -- See Note [Weird typing rule for ForAllTy] in Type
       ; InScopeSet
in_scope <- LintM InScopeSet
getInScope
       ; let tyl :: Type
tyl   = Var -> Type -> Type
mkTyCoInvForAllTy Var
cv1 Type
t1
             r2 :: Role
r2    = Var -> Role
coVarRole Var
cv1
             kind_co' :: Coercion
kind_co' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r2 Role
Nominal Coercion
kind_co
             eta1 :: Coercion
eta1  = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r2 Int
2 Coercion
kind_co'
             eta2 :: Coercion
eta2  = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r2 Int
3 Coercion
kind_co'
             subst :: TCvSubst
subst = InScopeSet -> CvSubstEnv -> TCvSubst
mkCvSubst InScopeSet
in_scope (CvSubstEnv -> TCvSubst) -> CvSubstEnv -> TCvSubst
forall a b. (a -> b) -> a -> b
$
                     -- We need both the free vars of the `t2` and the
                     -- free vars of the range of the substitution in
                     -- scope. All the free vars of `t2` and `kind_co` should
                     -- already be in `in_scope`, because they've been
                     -- linted and `cv2` has the same unique as `cv1`.
                     -- See Note [The substitution invariant] in TyCoSubst.
                     Var -> Coercion -> CvSubstEnv
forall a. Var -> a -> VarEnv a
unitVarEnv Var
cv1 (Coercion
eta1 Coercion -> Coercion -> Coercion
`mkTransCo` (Var -> Coercion
mkCoVarCo Var
cv2)
                                          Coercion -> Coercion -> Coercion
`mkTransCo` (Coercion -> Coercion
mkSymCo Coercion
eta2))
             tyr :: Type
tyr = Var -> Type -> Type
mkTyCoInvForAllTy Var
cv2 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                   HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
t2
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
liftedTypeKind, Type
liftedTypeKind, Type
tyl, Type
tyr, Role
r) } }
                   -- See Note [Weird typing rule for ForAllTy] in Type

lintCoercion co :: Coercion
co@(FunCo Role
r Coercion
co1 Coercion
co2)
  = do { (Type
k1,Type
k'1,Type
s1,Type
t1,Role
r1) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co1
       ; (Type
k2,Type
k'2,Type
s2,Type
t2,Role
r2) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co2
       ; Type
k <- SDoc -> Type -> Type -> LintM Type
lintArrow (String -> SDoc
text String
"coercion" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)) Type
k1 Type
k2
       ; Type
k' <- SDoc -> Type -> Type -> LintM Type
lintArrow (String -> SDoc
text String
"coercion" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)) Type
k'1 Type
k'2
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co1 Role
r Role
r1
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co2 Role
r Role
r2
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k, Type
k', Type -> Type -> Type
mkVisFunTy Type
s1 Type
s2, Type -> Type -> Type
mkVisFunTy Type
t1 Type
t2, Role
r) }

lintCoercion (CoVarCo Var
cv)
  | Bool -> Bool
not (Var -> Bool
isCoVar Var
cv)
  = SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Bad CoVarCo:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
cv)
                  Int
2 (String -> SDoc
text String
"With offending type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
cv)))
  | Bool
otherwise
  = do { Var -> LintM ()
lintTyCoVarInScope Var
cv
       ; Var
cv' <- Var -> LintM Var
lookupIdInScope Var
cv
       ; Var -> LintM ()
lintUnliftedCoVar Var
cv
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type, Type, Type, Role)
 -> LintM (Type, Type, Type, Type, Role))
-> (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Var -> (Type, Type, Type, Type, Role)
Var -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole Var
cv' }

-- See Note [Bad unsafe coercion]
lintCoercion co :: Coercion
co@(UnivCo UnivCoProvenance
prov Role
r Type
ty1 Type
ty2)
  = do { Type
k1 <- Type -> LintM Type
lintType Type
ty1
       ; Type
k2 <- Type -> LintM Type
lintType Type
ty2
       ; case UnivCoProvenance
prov of
           UnivCoProvenance
UnsafeCoerceProv -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- no extra checks

           PhantomProv Coercion
kco    -> do { Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co Role
Phantom Role
r
                                    ; Coercion -> Type -> Type -> LintM ()
check_kinds Coercion
kco Type
k1 Type
k2 }

           ProofIrrelProv Coercion
kco -> do { Bool -> SDoc -> LintM ()
lintL (Type -> Bool
isCoercionTy Type
ty1) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
                                          Type -> Coercion -> SDoc
mkBadProofIrrelMsg Type
ty1 Coercion
co
                                    ; Bool -> SDoc -> LintM ()
lintL (Type -> Bool
isCoercionTy Type
ty2) (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$
                                          Type -> Coercion -> SDoc
mkBadProofIrrelMsg Type
ty2 Coercion
co
                                    ; Coercion -> Type -> Type -> LintM ()
check_kinds Coercion
kco Type
k1 Type
k2 }

           PluginProv String
_     -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- no extra checks

       ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
/= Role
Phantom Bool -> Bool -> Bool
&& Type -> Bool
classifiesTypeWithValues Type
k1
                            Bool -> Bool -> Bool
&& Type -> Bool
classifiesTypeWithValues Type
k2)
              (Type -> Type -> LintM ()
checkTypes Type
ty1 Type
ty2)
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k1, Type
k2, Type
ty1, Type
ty2, Role
r) }
   where
     report :: String -> SDoc
report String
s = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text (String -> SDoc) -> String -> SDoc
forall a b. (a -> b) -> a -> b
$ String
"Unsafe coercion: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
                     Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"From:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1
                             , String -> SDoc
text String
"  To:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2])
     isUnBoxed :: PrimRep -> Bool
     isUnBoxed :: PrimRep -> Bool
isUnBoxed = Bool -> Bool
not (Bool -> Bool) -> (PrimRep -> Bool) -> PrimRep -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimRep -> Bool
isGcPtrRep

       -- see #9122 for discussion of these checks
     checkTypes :: Type -> Type -> LintM ()
checkTypes Type
t1 Type
t2
       = do { Bool -> SDoc -> LintM ()
checkWarnL (Bool -> Bool
not Bool
lev_poly1)
                         (String -> SDoc
report String
"left-hand type is levity-polymorphic")
            ; Bool -> SDoc -> LintM ()
checkWarnL (Bool -> Bool
not Bool
lev_poly2)
                         (String -> SDoc
report String
"right-hand type is levity-polymorphic")
            ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (Bool
lev_poly1 Bool -> Bool -> Bool
|| Bool
lev_poly2)) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
              do { Bool -> SDoc -> LintM ()
checkWarnL ([PrimRep]
reps1 [PrimRep] -> [PrimRep] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [PrimRep]
reps2)
                              (String -> SDoc
report String
"between values with different # of reps")
                 ; (PrimRep -> PrimRep -> LintM ())
-> [PrimRep] -> [PrimRep] -> LintM ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ PrimRep -> PrimRep -> LintM ()
validateCoercion [PrimRep]
reps1 [PrimRep]
reps2 }}
       where
         lev_poly1 :: Bool
lev_poly1 = Type -> Bool
isTypeLevPoly Type
t1
         lev_poly2 :: Bool
lev_poly2 = Type -> Bool
isTypeLevPoly Type
t2

         -- don't look at these unless lev_poly1/2 are False
         -- Otherwise, we get #13458
         reps1 :: [PrimRep]
reps1 = HasDebugCallStack => Type -> [PrimRep]
Type -> [PrimRep]
typePrimRep Type
t1
         reps2 :: [PrimRep]
reps2 = HasDebugCallStack => Type -> [PrimRep]
Type -> [PrimRep]
typePrimRep Type
t2

     validateCoercion :: PrimRep -> PrimRep -> LintM ()
     validateCoercion :: PrimRep -> PrimRep -> LintM ()
validateCoercion PrimRep
rep1 PrimRep
rep2
       = do { DynFlags
dflags <- LintM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
            ; Bool -> SDoc -> LintM ()
checkWarnL (PrimRep -> Bool
isUnBoxed PrimRep
rep1 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== PrimRep -> Bool
isUnBoxed PrimRep
rep2)
                         (String -> SDoc
report String
"between unboxed and boxed value")
            ; Bool -> SDoc -> LintM ()
checkWarnL (DynFlags -> PrimRep -> Int
TyCon.primRepSizeB DynFlags
dflags PrimRep
rep1
                           Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== DynFlags -> PrimRep -> Int
TyCon.primRepSizeB DynFlags
dflags PrimRep
rep2)
                         (String -> SDoc
report String
"between unboxed values of different size")
            ; let fl :: Maybe Bool
fl = (Bool -> Bool -> Bool) -> Maybe Bool -> Maybe Bool -> Maybe Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) (PrimRep -> Maybe Bool
TyCon.primRepIsFloat PrimRep
rep1)
                                   (PrimRep -> Maybe Bool
TyCon.primRepIsFloat PrimRep
rep2)
            ; case Maybe Bool
fl of
                Maybe Bool
Nothing    -> SDoc -> LintM ()
addWarnL (String -> SDoc
report String
"between vector types")
                Just Bool
False -> SDoc -> LintM ()
addWarnL (String -> SDoc
report String
"between float and integral values")
                Maybe Bool
_          -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            }

     check_kinds :: Coercion -> Type -> Type -> LintM ()
check_kinds Coercion
kco Type
k1 Type
k2 = do { (Type
k1', Type
k2') <- Coercion -> LintM (Type, Type)
lintStarCoercion Coercion
kco
                                ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
k1 Type
k1' (LeftOrRight -> Coercion -> SDoc
mkBadUnivCoMsg LeftOrRight
CLeft  Coercion
co)
                                ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
k2 Type
k2' (LeftOrRight -> Coercion -> SDoc
mkBadUnivCoMsg LeftOrRight
CRight Coercion
co) }


lintCoercion (SymCo Coercion
co)
  = do { (Type
k1, Type
k2, Type
ty1, Type
ty2, Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k2, Type
k1, Type
ty2, Type
ty1, Role
r) }

lintCoercion co :: Coercion
co@(TransCo Coercion
co1 Coercion
co2)
  = do { (Type
k1a, Type
_k1b, Type
ty1a, Type
ty1b, Role
r1) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co1
       ; (Type
_k2a, Type
k2b, Type
ty2a, Type
ty2b, Role
r2) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co2
       ; Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
ty1b Type
ty2a
               (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Trans coercion mis-match:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
                   Int
2 ([SDoc] -> SDoc
vcat [Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1a, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1b, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2a, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2b]))
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co Role
r1 Role
r2
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k1a, Type
k2b, Type
ty1a, Type
ty2b, Role
r1) }

lintCoercion the_co :: Coercion
the_co@(NthCo Role
r0 Int
n Coercion
co)
  = do { (Type
_, Type
_, Type
s, Type
t, Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; case (Type -> Maybe (Var, Type)
splitForAllTy_maybe Type
s, Type -> Maybe (Var, Type)
splitForAllTy_maybe Type
t) of
         { (Just (Var
tcv_s, Type
_ty_s), Just (Var
tcv_t, Type
_ty_t))
             -- works for both tyvar and covar
             | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
             ,  (Type -> Bool
isForAllTy_ty Type
s Bool -> Bool -> Bool
&& Type -> Bool
isForAllTy_ty Type
t)
             Bool -> Bool -> Bool
|| (Type -> Bool
isForAllTy_co Type
s Bool -> Bool -> Bool
&& Type -> Bool
isForAllTy_co Type
t)
             -> do { Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
the_co Role
Nominal Role
r0
                   ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ks, Type
kt, Type
ts, Type
tt, Role
r0) }
             where
               ts :: Type
ts = Var -> Type
varType Var
tcv_s
               tt :: Type
tt = Var -> Type
varType Var
tcv_t
               ks :: Type
ks = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ts
               kt :: Type
kt = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
tt

         ; (Maybe (Var, Type), Maybe (Var, Type))
_ -> case (HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
s, HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
t) of
         { (Just (TyCon
tc_s, [Type]
tys_s), Just (TyCon
tc_t, [Type]
tys_t))
             | TyCon
tc_s TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc_t
             , TyCon -> Role -> Bool
isInjectiveTyCon TyCon
tc_s Role
r
                 -- see Note [NthCo and newtypes] in TyCoRep
             , [Type]
tys_s [Type] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` [Type]
tys_t
             , [Type]
tys_s [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
n
             -> do { Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
the_co Role
tr Role
r0
                   ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ks, Type
kt, Type
ts, Type
tt, Role
r0) }
             where
               ts :: Type
ts = [Type] -> Int -> Type
forall a. Outputable a => [a] -> Int -> a
getNth [Type]
tys_s Int
n
               tt :: Type
tt = [Type] -> Int -> Type
forall a. Outputable a => [a] -> Int -> a
getNth [Type]
tys_t Int
n
               tr :: Role
tr = Role -> TyCon -> Int -> Role
nthRole Role
r TyCon
tc_s Int
n
               ks :: Type
ks = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ts
               kt :: Type
kt = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
tt

         ; (Maybe (TyCon, [Type]), Maybe (TyCon, [Type]))
_ -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Bad getNth:")
                              Int
2 (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
the_co SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
s SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)) }}}

lintCoercion the_co :: Coercion
the_co@(LRCo LeftOrRight
lr Coercion
co)
  = do { (Type
_,Type
_,Type
s,Type
t,Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co Role
Nominal Role
r
       ; case (Type -> Maybe (Type, Type)
splitAppTy_maybe Type
s, Type -> Maybe (Type, Type)
splitAppTy_maybe Type
t) of
           (Just (Type, Type)
s_pr, Just (Type, Type)
t_pr)
             -> (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
ks_pick, Type
kt_pick, Type
s_pick, Type
t_pick, Role
Nominal)
             where
               s_pick :: Type
s_pick  = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
lr (Type, Type)
s_pr
               t_pick :: Type
t_pick  = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
lr (Type, Type)
t_pr
               ks_pick :: Type
ks_pick = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
s_pick
               kt_pick :: Type
kt_pick = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
t_pick

           (Maybe (Type, Type), Maybe (Type, Type))
_ -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Bad LRCo:")
                              Int
2 (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
the_co SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
s SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)) }

lintCoercion (InstCo Coercion
co Coercion
arg)
  = do { (Type
k3, Type
k4, Type
t1',Type
t2', Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; (Type
k1',Type
k2',Type
s1,Type
s2, Role
r') <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
arg
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
arg Role
Nominal Role
r'
       ; InScopeSet
in_scope <- LintM InScopeSet
getInScope
       ; case (Type -> Maybe (Var, Type)
splitForAllTy_ty_maybe Type
t1', Type -> Maybe (Var, Type)
splitForAllTy_ty_maybe Type
t2') of
         -- forall over tvar
         { (Just (Var
tv1,Type
t1), Just (Var
tv2,Type
t2))
             | Type
k1' Type -> Type -> Bool
`eqType` Var -> Type
tyVarKind Var
tv1
             , Type
k2' Type -> Type -> Bool
`eqType` Var -> Type
tyVarKind Var
tv2
             -> (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k3, Type
k4,
                        InScopeSet -> [Var] -> [Type] -> Type -> Type
substTyWithInScope InScopeSet
in_scope [Var
tv1] [Type
s1] Type
t1,
                        InScopeSet -> [Var] -> [Type] -> Type -> Type
substTyWithInScope InScopeSet
in_scope [Var
tv2] [Type
s2] Type
t2, Role
r)
             | Bool
otherwise
             -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Kind mis-match in inst coercion")
         ; (Maybe (Var, Type), Maybe (Var, Type))
_ -> case (Type -> Maybe (Var, Type)
splitForAllTy_co_maybe Type
t1', Type -> Maybe (Var, Type)
splitForAllTy_co_maybe Type
t2') of
         -- forall over covar
         { (Just (Var
cv1, Type
t1), Just (Var
cv2, Type
t2))
             | Type
k1' Type -> Type -> Bool
`eqType` Var -> Type
varType Var
cv1
             , Type
k2' Type -> Type -> Bool
`eqType` Var -> Type
varType Var
cv2
             , CoercionTy Coercion
s1' <- Type
s1
             , CoercionTy Coercion
s2' <- Type
s2
             -> do { (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type, Type, Type, Type, Role)
 -> LintM (Type, Type, Type, Type, Role))
-> (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall a b. (a -> b) -> a -> b
$
                       (Type
liftedTypeKind, Type
liftedTypeKind
                          -- See Note [Weird typing rule for ForAllTy] in Type
                       , HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (InScopeSet -> CvSubstEnv -> TCvSubst
mkCvSubst InScopeSet
in_scope (CvSubstEnv -> TCvSubst) -> CvSubstEnv -> TCvSubst
forall a b. (a -> b) -> a -> b
$ Var -> Coercion -> CvSubstEnv
forall a. Var -> a -> VarEnv a
unitVarEnv Var
cv1 Coercion
s1') Type
t1
                       , HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (InScopeSet -> CvSubstEnv -> TCvSubst
mkCvSubst InScopeSet
in_scope (CvSubstEnv -> TCvSubst) -> CvSubstEnv -> TCvSubst
forall a b. (a -> b) -> a -> b
$ Var -> Coercion -> CvSubstEnv
forall a. Var -> a -> VarEnv a
unitVarEnv Var
cv2 Coercion
s2') Type
t2
                       , Role
r) }
             | Bool
otherwise
             -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Kind mis-match in inst coercion")
         ; (Maybe (Var, Type), Maybe (Var, Type))
_ -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Bad argument of inst") }}}

lintCoercion co :: Coercion
co@(AxiomInstCo CoAxiom Branched
con Int
ind [Coercion]
cos)
  = do { Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
ind Bool -> Bool -> Bool
&& Int
ind Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Branches Branched -> Int
forall (br :: BranchFlag). Branches br -> Int
numBranches (CoAxiom Branched -> Branches Branched
forall (br :: BranchFlag). CoAxiom br -> Branches br
coAxiomBranches CoAxiom Branched
con))
                (SDoc -> LintM ()
bad_ax (String -> SDoc
text String
"index out of range"))
       ; let CoAxBranch { cab_tvs :: CoAxBranch -> [Var]
cab_tvs   = [Var]
ktvs
                        , cab_cvs :: CoAxBranch -> [Var]
cab_cvs   = [Var]
cvs
                        , cab_roles :: CoAxBranch -> [Role]
cab_roles = [Role]
roles
                        , cab_lhs :: CoAxBranch -> [Type]
cab_lhs   = [Type]
lhs
                        , cab_rhs :: CoAxBranch -> Type
cab_rhs   = Type
rhs } = CoAxiom Branched -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom Branched
con Int
ind
       ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Coercion]
cos [Coercion] -> [Var] -> Bool
forall a b. [a] -> [b] -> Bool
`equalLength` ([Var]
ktvs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
cvs)) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
           SDoc -> LintM ()
bad_ax (String -> SDoc
text String
"lengths")
       ; TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; let empty_subst :: TCvSubst
empty_subst = TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst
       ; (TCvSubst
subst_l, TCvSubst
subst_r) <- ((TCvSubst, TCvSubst)
 -> (Var, Role, Coercion) -> LintM (TCvSubst, TCvSubst))
-> (TCvSubst, TCvSubst)
-> [(Var, Role, Coercion)]
-> LintM (TCvSubst, TCvSubst)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (TCvSubst, TCvSubst)
-> (Var, Role, Coercion) -> LintM (TCvSubst, TCvSubst)
check_ki
                                      (TCvSubst
empty_subst, TCvSubst
empty_subst)
                                      ([Var] -> [Role] -> [Coercion] -> [(Var, Role, Coercion)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 ([Var]
ktvs [Var] -> [Var] -> [Var]
forall a. [a] -> [a] -> [a]
++ [Var]
cvs) [Role]
roles [Coercion]
cos)
       ; let lhs' :: [Type]
lhs' = HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys TCvSubst
subst_l [Type]
lhs
             rhs' :: Type
rhs' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy  TCvSubst
subst_r Type
rhs
             fam_tc :: TyCon
fam_tc = CoAxiom Branched -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom Branched
con
       ; case Coercion -> Maybe CoAxBranch
checkAxInstCo Coercion
co of
           Just CoAxBranch
bad_branch -> SDoc -> LintM ()
bad_ax (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"inconsistent with" SDoc -> SDoc -> SDoc
<+>
                                       TyCon -> CoAxBranch -> SDoc
pprCoAxBranch TyCon
fam_tc CoAxBranch
bad_branch
           Maybe CoAxBranch
Nothing -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
       ; let s2 :: Type
s2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc [Type]
lhs'
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
s2, HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
rhs', Type
s2, Type
rhs', CoAxiom Branched -> Role
forall (br :: BranchFlag). CoAxiom br -> Role
coAxiomRole CoAxiom Branched
con) }
  where
    bad_ax :: SDoc -> LintM ()
bad_ax SDoc
what = SDoc -> LintM ()
addErrL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text  String
"Bad axiom application" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens SDoc
what)
                        Int
2 (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co))

    check_ki :: (TCvSubst, TCvSubst)
-> (Var, Role, Coercion) -> LintM (TCvSubst, TCvSubst)
check_ki (TCvSubst
subst_l, TCvSubst
subst_r) (Var
ktv, Role
role, Coercion
arg)
      = do { (Type
k', Type
k'', Type
s', Type
t', Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
arg
           ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
arg Role
role Role
r
           ; let ktv_kind_l :: Type
ktv_kind_l = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst_l (Var -> Type
tyVarKind Var
ktv)
                 ktv_kind_r :: Type
ktv_kind_r = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst_r (Var -> Type
tyVarKind Var
ktv)
           ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
k' Type -> Type -> Bool
`eqType` Type
ktv_kind_l)
                    (SDoc -> LintM ()
bad_ax (String -> SDoc
text String
"check_ki1" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k', Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
ktv, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ktv_kind_l ] ))
           ; Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Type
k'' Type -> Type -> Bool
`eqType` Type
ktv_kind_r)
                    (SDoc -> LintM ()
bad_ax (String -> SDoc
text String
"check_ki2" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
vcat [ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k'', Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
ktv, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ktv_kind_r ] ))
           ; (TCvSubst, TCvSubst) -> LintM (TCvSubst, TCvSubst)
forall (m :: * -> *) a. Monad m => a -> m a
return (TCvSubst -> Var -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst_l Var
ktv Type
s',
                     TCvSubst -> Var -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst_r Var
ktv Type
t') }

lintCoercion (KindCo Coercion
co)
  = do { (Type
k1, Type
k2, Type
_, Type
_, Role
_) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
liftedTypeKind, Type
liftedTypeKind, Type
k1, Type
k2, Role
Nominal) }

lintCoercion (SubCo Coercion
co')
  = do { (Type
k1,Type
k2,Type
s,Type
t,Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co'
       ; Coercion -> Role -> Role -> LintM ()
forall thing. Outputable thing => thing -> Role -> Role -> LintM ()
lintRole Coercion
co' Role
Nominal Role
r
       ; (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
k1,Type
k2,Type
s,Type
t,Role
Representational) }

lintCoercion this :: Coercion
this@(AxiomRuleCo CoAxiomRule
co [Coercion]
cs)
  = do { [(Type, Type, Type, Type, Role)]
eqs <- (Coercion -> LintM (Type, Type, Type, Type, Role))
-> [Coercion] -> LintM [(Type, Type, Type, Type, Role)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion [Coercion]
cs
       ; Int -> [Role] -> [(Type, Type, Type, Type, Role)] -> LintM ()
forall a a b c d.
(Eq a, Outputable a) =>
Int -> [a] -> [(a, b, c, d, a)] -> LintM ()
lintRoles Int
0 (CoAxiomRule -> [Role]
coaxrAsmpRoles CoAxiomRule
co) [(Type, Type, Type, Type, Role)]
eqs
       ; case CoAxiomRule -> [TypeEqn] -> Maybe TypeEqn
coaxrProves CoAxiomRule
co [ Type -> Type -> TypeEqn
forall a. a -> a -> Pair a
Pair Type
l Type
r | (Type
_,Type
_,Type
l,Type
r,Role
_) <- [(Type, Type, Type, Type, Role)]
eqs ] of
           Maybe TypeEqn
Nothing -> String -> [SDoc] -> LintM (Type, Type, Type, Type, Role)
forall a. String -> [SDoc] -> LintM a
err String
"Malformed use of AxiomRuleCo" [ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
this ]
           Just (Pair Type
l Type
r) ->
             (Type, Type, Type, Type, Role)
-> LintM (Type, Type, Type, Type, Role)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
l, HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
r, Type
l, Type
r, CoAxiomRule -> Role
coaxrRole CoAxiomRule
co) }
  where
  err :: String -> [SDoc] -> LintM a
err String
m [SDoc]
xs  = SDoc -> LintM a
forall a. SDoc -> LintM a
failWithL (SDoc -> LintM a) -> SDoc -> LintM a
forall a b. (a -> b) -> a -> b
$
                SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
m) Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat (String -> SDoc
text String
"Rule:" SDoc -> SDoc -> SDoc
<+> FastString -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoAxiomRule -> FastString
coaxrName CoAxiomRule
co) SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: [SDoc]
xs)

  lintRoles :: Int -> [a] -> [(a, b, c, d, a)] -> LintM ()
lintRoles Int
n (a
e : [a]
es) ((a
_,b
_,c
_,d
_,a
r) : [(a, b, c, d, a)]
rs)
    | a
e a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
r    = Int -> [a] -> [(a, b, c, d, a)] -> LintM ()
lintRoles (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [a]
es [(a, b, c, d, a)]
rs
    | Bool
otherwise = String -> [SDoc] -> LintM ()
forall a. String -> [SDoc] -> LintM a
err String
"Argument roles mismatch"
                      [ String -> SDoc
text String
"In argument:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
                      , String -> SDoc
text String
"Expected:" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
e
                      , String -> SDoc
text String
"Found:" SDoc -> SDoc -> SDoc
<+> a -> SDoc
forall a. Outputable a => a -> SDoc
ppr a
r ]
  lintRoles Int
_ [] []  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  lintRoles Int
n [] [(a, b, c, d, a)]
rs  = String -> [SDoc] -> LintM ()
forall a. String -> [SDoc] -> LintM a
err String
"Too many coercion arguments"
                          [ String -> SDoc
text String
"Expected:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n
                          , String -> SDoc
text String
"Provided:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(a, b, c, d, a)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(a, b, c, d, a)]
rs) ]

  lintRoles Int
n [a]
es []  = String -> [SDoc] -> LintM ()
forall a. String -> [SDoc] -> LintM a
err String
"Not enough coercion arguments"
                          [ String -> SDoc
text String
"Expected:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
es)
                          , String -> SDoc
text String
"Provided:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
n ]

lintCoercion (HoleCo CoercionHole
h)
  = do { SDoc -> LintM ()
addErrL (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text String
"Unfilled coercion hole:" SDoc -> SDoc -> SDoc
<+> CoercionHole -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoercionHole
h
       ; Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion (Var -> Coercion
CoVarCo (CoercionHole -> Var
coHoleCoVar CoercionHole
h)) }


----------
lintUnliftedCoVar :: CoVar -> LintM ()
lintUnliftedCoVar :: Var -> LintM ()
lintUnliftedCoVar Var
cv
  = Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not (HasDebugCallStack => Type -> Bool
Type -> Bool
isUnliftedType (Var -> Type
coVarKind Var
cv))) (LintM () -> LintM ()) -> LintM () -> LintM ()
forall a b. (a -> b) -> a -> b
$
    SDoc -> LintM ()
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
"Bad lifted equality:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
cv
                 SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
coVarKind Var
cv))

{-
************************************************************************
*                                                                      *
\subsection[lint-monad]{The Lint monad}
*                                                                      *
************************************************************************
-}

-- If you edit this type, you may need to update the GHC formalism
-- See Note [GHC Formalism]
data LintEnv
  = LE { LintEnv -> LintFlags
le_flags :: LintFlags       -- Linting the result of this pass
       , LintEnv -> [LintLocInfo]
le_loc   :: [LintLocInfo]   -- Locations

       , LintEnv -> TCvSubst
le_subst :: TCvSubst  -- Current type substitution
                               -- We also use le_subst to keep track of
                               -- /all variables/ in scope, both Ids and TyVars

       , LintEnv -> VarSet
le_joins :: IdSet     -- Join points in scope that are valid
                               -- A subset of the InScopeSet in le_subst
                               -- See Note [Join points]

       , LintEnv -> DynFlags
le_dynflags :: DynFlags     -- DynamicFlags
       }

data LintFlags
  = LF { LintFlags -> Bool
lf_check_global_ids           :: Bool -- See Note [Checking for global Ids]
       , LintFlags -> Bool
lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers]
       , LintFlags -> StaticPtrCheck
lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs]
       , LintFlags -> Bool
lf_report_unsat_syns :: Bool -- ^ See Note [Linting type synonym applications]
    }

-- See Note [Checking StaticPtrs]
data StaticPtrCheck
    = AllowAnywhere
        -- ^ Allow 'makeStatic' to occur anywhere.
    | AllowAtTopLevel
        -- ^ Allow 'makeStatic' calls at the top-level only.
    | RejectEverywhere
        -- ^ Reject any 'makeStatic' occurrence.
  deriving StaticPtrCheck -> StaticPtrCheck -> Bool
(StaticPtrCheck -> StaticPtrCheck -> Bool)
-> (StaticPtrCheck -> StaticPtrCheck -> Bool) -> Eq StaticPtrCheck
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: StaticPtrCheck -> StaticPtrCheck -> Bool
$c/= :: StaticPtrCheck -> StaticPtrCheck -> Bool
== :: StaticPtrCheck -> StaticPtrCheck -> Bool
$c== :: StaticPtrCheck -> StaticPtrCheck -> Bool
Eq

defaultLintFlags :: LintFlags
defaultLintFlags :: LintFlags
defaultLintFlags = LF :: Bool -> Bool -> StaticPtrCheck -> Bool -> LintFlags
LF { lf_check_global_ids :: Bool
lf_check_global_ids = Bool
False
                      , lf_check_inline_loop_breakers :: Bool
lf_check_inline_loop_breakers = Bool
True
                      , lf_check_static_ptrs :: StaticPtrCheck
lf_check_static_ptrs = StaticPtrCheck
AllowAnywhere
                      , lf_report_unsat_syns :: Bool
lf_report_unsat_syns = Bool
True
                      }

newtype LintM a =
   LintM { LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM ::
            LintEnv ->
            WarnsAndErrs ->           -- Warning and error messages so far
            (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
   deriving (a -> LintM b -> LintM a
(a -> b) -> LintM a -> LintM b
(forall a b. (a -> b) -> LintM a -> LintM b)
-> (forall a b. a -> LintM b -> LintM a) -> Functor LintM
forall a b. a -> LintM b -> LintM a
forall a b. (a -> b) -> LintM a -> LintM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> LintM b -> LintM a
$c<$ :: forall a b. a -> LintM b -> LintM a
fmap :: (a -> b) -> LintM a -> LintM b
$cfmap :: forall a b. (a -> b) -> LintM a -> LintM b
Functor)

type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)

{- Note [Checking for global Ids]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Before CoreTidy, all locally-bound Ids must be LocalIds, even
top-level ones. See Note [Exported LocalIds] and #9857.

Note [Checking StaticPtrs]
~~~~~~~~~~~~~~~~~~~~~~~~~~
See Note [Grand plan for static forms] in StaticPtrTable for an overview.

Every occurrence of the function 'makeStatic' should be moved to the
top level by the FloatOut pass.  It's vital that we don't have nested
'makeStatic' occurrences after CorePrep, because we populate the Static
Pointer Table from the top-level bindings. See SimplCore Note [Grand
plan for static forms].

The linter checks that no occurrence is left behind, nested within an
expression. The check is enabled only after the FloatOut, CorePrep,
and CoreTidy passes and only if the module uses the StaticPointers
language extension. Checking more often doesn't help since the condition
doesn't hold until after the first FloatOut pass.

Note [Type substitution]
~~~~~~~~~~~~~~~~~~~~~~~~
Why do we need a type substitution?  Consider
        /\(a:*). \(x:a). /\(a:*). id a x
This is ill typed, because (renaming variables) it is really
        /\(a:*). \(x:a). /\(b:*). id b x
Hence, when checking an application, we can't naively compare x's type
(at its binding site) with its expected type (at a use site).  So we
rename type binders as we go, maintaining a substitution.

The same substitution also supports let-type, current expressed as
        (/\(a:*). body) ty
Here we substitute 'ty' for 'a' in 'body', on the fly.

Note [Linting type synonym applications]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When linting a type-synonym, or type-family, application
  S ty1 .. tyn
we behave as follows (#15057, #T15664):

* If lf_report_unsat_syns = True, and S has arity < n,
  complain about an unsaturated type synonym or type family

* Switch off lf_report_unsat_syns, and lint ty1 .. tyn.

  Reason: catch out of scope variables or other ill-kinded gubbins,
  even if S discards that argument entirely. E.g. (#15012):
     type FakeOut a = Int
     type family TF a
     type instance TF Int = FakeOut a
  Here 'a' is out of scope; but if we expand FakeOut, we conceal
  that out-of-scope error.

  Reason for switching off lf_report_unsat_syns: with
  LiberalTypeSynonyms, GHC allows unsaturated synonyms provided they
  are saturated when the type is expanded. Example
     type T f = f Int
     type S a = a -> a
     type Z = T S
  In Z's RHS, S appears unsaturated, but it is saturated when T is expanded.

* If lf_report_unsat_syns is on, expand the synonym application and
  lint the result.  Reason: want to check that synonyms are saturated
  when the type is expanded.
-}

instance Applicative LintM where
      pure :: a -> LintM a
pure a
x = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
_ (Bag SDoc, Bag SDoc)
errs -> (a -> Maybe a
forall a. a -> Maybe a
Just a
x, (Bag SDoc, Bag SDoc)
errs)
      <*> :: LintM (a -> b) -> LintM a -> LintM b
(<*>) = LintM (a -> b) -> LintM a -> LintM b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Monad LintM where
#if !MIN_VERSION_base(4,13,0)
  fail = MonadFail.fail
#endif
  LintM a
m >>= :: LintM a -> (a -> LintM b) -> LintM b
>>= a -> LintM b
k  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe b, (Bag SDoc, Bag SDoc)))
-> LintM b
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM (\ LintEnv
env (Bag SDoc, Bag SDoc)
errs ->
                       let (Maybe a
res, (Bag SDoc, Bag SDoc)
errs') = LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
m LintEnv
env (Bag SDoc, Bag SDoc)
errs in
                         case Maybe a
res of
                           Just a
r -> LintM b
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe b, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM (a -> LintM b
k a
r) LintEnv
env (Bag SDoc, Bag SDoc)
errs'
                           Maybe a
Nothing -> (Maybe b
forall a. Maybe a
Nothing, (Bag SDoc, Bag SDoc)
errs'))

instance MonadFail.MonadFail LintM where
    fail :: String -> LintM a
fail String
err = SDoc -> LintM a
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text String
err)

instance HasDynFlags LintM where
  getDynFlags :: LintM DynFlags
getDynFlags = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe DynFlags, (Bag SDoc, Bag SDoc)))
-> LintM DynFlags
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM (\ LintEnv
e (Bag SDoc, Bag SDoc)
errs -> (DynFlags -> Maybe DynFlags
forall a. a -> Maybe a
Just (LintEnv -> DynFlags
le_dynflags LintEnv
e), (Bag SDoc, Bag SDoc)
errs))

data LintLocInfo
  = RhsOf Id            -- The variable bound
  | LambdaBodyOf Id     -- The lambda-binder
  | UnfoldingOf Id      -- Unfolding of a binder
  | BodyOfLetRec [Id]   -- One of the binders
  | CaseAlt CoreAlt     -- Case alternative
  | CasePat CoreAlt     -- The *pattern* of the case alternative
  | CaseTy CoreExpr     -- The type field of a case expression
                        -- with this scrutinee
  | IdTy Id             -- The type field of an Id binder
  | AnExpr CoreExpr     -- Some expression
  | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
  | TopLevelBindings
  | InType Type         -- Inside a type
  | InCo   Coercion     -- Inside a coercion

initL :: DynFlags -> LintFlags -> InScopeSet
       -> LintM a -> WarnsAndErrs    -- Warnings and errors
initL :: DynFlags
-> LintFlags -> InScopeSet -> LintM a -> (Bag SDoc, Bag SDoc)
initL DynFlags
dflags LintFlags
flags InScopeSet
in_scope LintM a
m
  = case LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
m LintEnv
env (Bag SDoc
forall a. Bag a
emptyBag, Bag SDoc
forall a. Bag a
emptyBag) of
      (Just a
_, (Bag SDoc, Bag SDoc)
errs) -> (Bag SDoc, Bag SDoc)
errs
      (Maybe a
Nothing, errs :: (Bag SDoc, Bag SDoc)
errs@(Bag SDoc
_, Bag SDoc
e)) | Bool -> Bool
not (Bag SDoc -> Bool
forall a. Bag a -> Bool
isEmptyBag Bag SDoc
e) -> (Bag SDoc, Bag SDoc)
errs
                             | Bool
otherwise -> String -> SDoc -> (Bag SDoc, Bag SDoc)
forall a. HasCallStack => String -> SDoc -> a
pprPanic (String
"Bug in Lint: a failure occurred " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                                                      String
"without reporting an error message") SDoc
empty
  where
    env :: LintEnv
env = LE :: LintFlags
-> [LintLocInfo] -> TCvSubst -> VarSet -> DynFlags -> LintEnv
LE { le_flags :: LintFlags
le_flags = LintFlags
flags
             , le_subst :: TCvSubst
le_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope
             , le_joins :: VarSet
le_joins = VarSet
emptyVarSet
             , le_loc :: [LintLocInfo]
le_loc = []
             , le_dynflags :: DynFlags
le_dynflags = DynFlags
dflags }

setReportUnsat :: Bool -> LintM a -> LintM a
-- Switch off lf_report_unsat_syns
setReportUnsat :: Bool -> LintM a -> LintM a
setReportUnsat Bool
ru LintM a
thing_inside
  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs ->
    let env' :: LintEnv
env' = LintEnv
env { le_flags :: LintFlags
le_flags = (LintEnv -> LintFlags
le_flags LintEnv
env) { lf_report_unsat_syns :: Bool
lf_report_unsat_syns = Bool
ru } }
    in LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
thing_inside LintEnv
env' (Bag SDoc, Bag SDoc)
errs

getLintFlags :: LintM LintFlags
getLintFlags :: LintM LintFlags
getLintFlags = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe LintFlags, (Bag SDoc, Bag SDoc)))
-> LintM LintFlags
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe LintFlags, (Bag SDoc, Bag SDoc)))
 -> LintM LintFlags)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe LintFlags, (Bag SDoc, Bag SDoc)))
-> LintM LintFlags
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> (LintFlags -> Maybe LintFlags
forall a. a -> Maybe a
Just (LintEnv -> LintFlags
le_flags LintEnv
env), (Bag SDoc, Bag SDoc)
errs)

checkL :: Bool -> MsgDoc -> LintM ()
checkL :: Bool -> SDoc -> LintM ()
checkL Bool
True  SDoc
_   = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkL Bool
False SDoc
msg = SDoc -> LintM ()
forall a. SDoc -> LintM a
failWithL SDoc
msg

-- like checkL, but relevant to type checking
lintL :: Bool -> MsgDoc -> LintM ()
lintL :: Bool -> SDoc -> LintM ()
lintL = Bool -> SDoc -> LintM ()
checkL

checkWarnL :: Bool -> MsgDoc -> LintM ()
checkWarnL :: Bool -> SDoc -> LintM ()
checkWarnL Bool
True   SDoc
_  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkWarnL Bool
False SDoc
msg = SDoc -> LintM ()
addWarnL SDoc
msg

failWithL :: MsgDoc -> LintM a
failWithL :: SDoc -> LintM a
failWithL SDoc
msg = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc
warns,Bag SDoc
errs) ->
                (Maybe a
forall a. Maybe a
Nothing, (Bag SDoc
warns, Bool -> LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg Bool
True LintEnv
env Bag SDoc
errs SDoc
msg))

addErrL :: MsgDoc -> LintM ()
addErrL :: SDoc -> LintM ()
addErrL SDoc
msg = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe (), (Bag SDoc, Bag SDoc)))
-> LintM ()
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe (), (Bag SDoc, Bag SDoc)))
 -> LintM ())
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe (), (Bag SDoc, Bag SDoc)))
-> LintM ()
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc
warns,Bag SDoc
errs) ->
              (() -> Maybe ()
forall a. a -> Maybe a
Just (), (Bag SDoc
warns, Bool -> LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg Bool
True LintEnv
env Bag SDoc
errs SDoc
msg))

addWarnL :: MsgDoc -> LintM ()
addWarnL :: SDoc -> LintM ()
addWarnL SDoc
msg = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe (), (Bag SDoc, Bag SDoc)))
-> LintM ()
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe (), (Bag SDoc, Bag SDoc)))
 -> LintM ())
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe (), (Bag SDoc, Bag SDoc)))
-> LintM ()
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc
warns,Bag SDoc
errs) ->
              (() -> Maybe ()
forall a. a -> Maybe a
Just (), (Bool -> LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg Bool
False LintEnv
env Bag SDoc
warns SDoc
msg, Bag SDoc
errs))

addMsg :: Bool -> LintEnv ->  Bag MsgDoc -> MsgDoc -> Bag MsgDoc
addMsg :: Bool -> LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg Bool
is_error LintEnv
env Bag SDoc
msgs SDoc
msg
  = ASSERT( notNull loc_msgs )
    Bag SDoc
msgs Bag SDoc -> SDoc -> Bag SDoc
forall a. Bag a -> a -> Bag a
`snocBag` SDoc -> SDoc
mk_msg SDoc
msg
  where
   loc_msgs :: [(SrcLoc, SDoc)]  -- Innermost first
   loc_msgs :: [(SrcLoc, SDoc)]
loc_msgs = (LintLocInfo -> (SrcLoc, SDoc))
-> [LintLocInfo] -> [(SrcLoc, SDoc)]
forall a b. (a -> b) -> [a] -> [b]
map LintLocInfo -> (SrcLoc, SDoc)
dumpLoc (LintEnv -> [LintLocInfo]
le_loc LintEnv
env)

   cxt_doc :: SDoc
cxt_doc = [SDoc] -> SDoc
vcat [ [SDoc] -> SDoc
vcat ([SDoc] -> SDoc) -> [SDoc] -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> [SDoc]
forall a. [a] -> [a]
reverse ([SDoc] -> [SDoc]) -> [SDoc] -> [SDoc]
forall a b. (a -> b) -> a -> b
$ ((SrcLoc, SDoc) -> SDoc) -> [(SrcLoc, SDoc)] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (SrcLoc, SDoc) -> SDoc
forall a b. (a, b) -> b
snd [(SrcLoc, SDoc)]
loc_msgs
                  , String -> SDoc
text String
"Substitution:" SDoc -> SDoc -> SDoc
<+> TCvSubst -> SDoc
forall a. Outputable a => a -> SDoc
ppr (LintEnv -> TCvSubst
le_subst LintEnv
env) ]
   context :: SDoc
context | Bool
is_error  = SDoc
cxt_doc
           | Bool
otherwise = SDoc -> SDoc
whenPprDebug SDoc
cxt_doc
     -- Print voluminous info for Lint errors
     -- but not for warnings

   msg_span :: SrcSpan
msg_span = case [ SrcSpan
span | (SrcLoc
loc,SDoc
_) <- [(SrcLoc, SDoc)]
loc_msgs
                          , let span :: SrcSpan
span = SrcLoc -> SrcSpan
srcLocSpan SrcLoc
loc
                          , SrcSpan -> Bool
isGoodSrcSpan SrcSpan
span ] of
               []    -> SrcSpan
noSrcSpan
               (SrcSpan
s:[SrcSpan]
_) -> SrcSpan
s
   mk_msg :: SDoc -> SDoc
mk_msg SDoc
msg = Severity -> SrcSpan -> SDoc -> SDoc
mkLocMessage Severity
SevWarning SrcSpan
msg_span
                             (SDoc
msg SDoc -> SDoc -> SDoc
$$ SDoc
context)

addLoc :: LintLocInfo -> LintM a -> LintM a
addLoc :: LintLocInfo -> LintM a -> LintM a
addLoc LintLocInfo
extra_loc LintM a
m
  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs ->
    LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
m (LintEnv
env { le_loc :: [LintLocInfo]
le_loc = LintLocInfo
extra_loc LintLocInfo -> [LintLocInfo] -> [LintLocInfo]
forall a. a -> [a] -> [a]
: LintEnv -> [LintLocInfo]
le_loc LintEnv
env }) (Bag SDoc, Bag SDoc)
errs

inCasePat :: LintM Bool         -- A slight hack; see the unique call site
inCasePat :: LintM Bool
inCasePat = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe Bool, (Bag SDoc, Bag SDoc)))
-> LintM Bool
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe Bool, (Bag SDoc, Bag SDoc)))
 -> LintM Bool)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe Bool, (Bag SDoc, Bag SDoc)))
-> LintM Bool
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> (Bool -> Maybe Bool
forall a. a -> Maybe a
Just (LintEnv -> Bool
is_case_pat LintEnv
env), (Bag SDoc, Bag SDoc)
errs)
  where
    is_case_pat :: LintEnv -> Bool
is_case_pat (LE { le_loc :: LintEnv -> [LintLocInfo]
le_loc = CasePat {} : [LintLocInfo]
_ }) = Bool
True
    is_case_pat LintEnv
_other                           = Bool
False

addInScopeVar :: Var -> LintM a -> LintM a
addInScopeVar :: Var -> LintM a -> LintM a
addInScopeVar Var
var LintM a
m
  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs ->
    LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
m (LintEnv
env { le_subst :: TCvSubst
le_subst = TCvSubst -> Var -> TCvSubst
extendTCvInScope (LintEnv -> TCvSubst
le_subst LintEnv
env) Var
var
                   , le_joins :: VarSet
le_joins = VarSet -> Var -> VarSet
delVarSet        (LintEnv -> VarSet
le_joins LintEnv
env) Var
var
               }) (Bag SDoc, Bag SDoc)
errs

extendSubstL :: TyVar -> Type -> LintM a -> LintM a
extendSubstL :: Var -> Type -> LintM a -> LintM a
extendSubstL Var
tv Type
ty LintM a
m
  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs ->
    LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
m (LintEnv
env { le_subst :: TCvSubst
le_subst = TCvSubst -> Var -> Type -> TCvSubst
Type.extendTvSubst (LintEnv -> TCvSubst
le_subst LintEnv
env) Var
tv Type
ty }) (Bag SDoc, Bag SDoc)
errs

updateTCvSubst :: TCvSubst -> LintM a -> LintM a
updateTCvSubst :: TCvSubst -> LintM a -> LintM a
updateTCvSubst TCvSubst
subst' LintM a
m
  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
m (LintEnv
env { le_subst :: TCvSubst
le_subst = TCvSubst
subst' }) (Bag SDoc, Bag SDoc)
errs

markAllJoinsBad :: LintM a -> LintM a
markAllJoinsBad :: LintM a -> LintM a
markAllJoinsBad LintM a
m
  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
m (LintEnv
env { le_joins :: VarSet
le_joins = VarSet
emptyVarSet }) (Bag SDoc, Bag SDoc)
errs

markAllJoinsBadIf :: Bool -> LintM a -> LintM a
markAllJoinsBadIf :: Bool -> LintM a -> LintM a
markAllJoinsBadIf Bool
True  LintM a
m = LintM a -> LintM a
forall a. LintM a -> LintM a
markAllJoinsBad LintM a
m
markAllJoinsBadIf Bool
False LintM a
m = LintM a
m

addGoodJoins :: [Var] -> LintM a -> LintM a
addGoodJoins :: [Var] -> LintM a -> LintM a
addGoodJoins [Var]
vars LintM a
thing_inside
  = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM ((LintEnv
  -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
 -> LintM a)
-> (LintEnv
    -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
forall a b. (a -> b) -> a -> b
$ \ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
forall a.
LintM a
-> LintEnv
-> (Bag SDoc, Bag SDoc)
-> (Maybe a, (Bag SDoc, Bag SDoc))
unLintM LintM a
thing_inside (LintEnv -> LintEnv
add_joins LintEnv
env) (Bag SDoc, Bag SDoc)
errs
  where
    add_joins :: LintEnv -> LintEnv
add_joins LintEnv
env = LintEnv
env { le_joins :: VarSet
le_joins = LintEnv -> VarSet
le_joins LintEnv
env VarSet -> [Var] -> VarSet
`extendVarSetList` [Var]
join_ids }
    join_ids :: [Var]
join_ids = (Var -> Bool) -> [Var] -> [Var]
forall a. (a -> Bool) -> [a] -> [a]
filter Var -> Bool
isJoinId [Var]
vars

getValidJoins :: LintM IdSet
getValidJoins :: LintM VarSet
getValidJoins = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe VarSet, (Bag SDoc, Bag SDoc)))
-> LintM VarSet
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM (\ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> (VarSet -> Maybe VarSet
forall a. a -> Maybe a
Just (LintEnv -> VarSet
le_joins LintEnv
env), (Bag SDoc, Bag SDoc)
errs))

getTCvSubst :: LintM TCvSubst
getTCvSubst :: LintM TCvSubst
getTCvSubst = (LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe TCvSubst, (Bag SDoc, Bag SDoc)))
-> LintM TCvSubst
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM (\ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> (TCvSubst -> Maybe TCvSubst
forall a. a -> Maybe a
Just (LintEnv -> TCvSubst
le_subst LintEnv
env), (Bag SDoc, Bag SDoc)
errs))

getInScope :: LintM InScopeSet
getInScope :: LintM InScopeSet
getInScope = (LintEnv
 -> (Bag SDoc, Bag SDoc)
 -> (Maybe InScopeSet, (Bag SDoc, Bag SDoc)))
-> LintM InScopeSet
forall a.
(LintEnv
 -> (Bag SDoc, Bag SDoc) -> (Maybe a, (Bag SDoc, Bag SDoc)))
-> LintM a
LintM (\ LintEnv
env (Bag SDoc, Bag SDoc)
errs -> (InScopeSet -> Maybe InScopeSet
forall a. a -> Maybe a
Just (TCvSubst -> InScopeSet
getTCvInScope (TCvSubst -> InScopeSet) -> TCvSubst -> InScopeSet
forall a b. (a -> b) -> a -> b
$ LintEnv -> TCvSubst
le_subst LintEnv
env), (Bag SDoc, Bag SDoc)
errs))

applySubstTy :: InType -> LintM OutType
applySubstTy :: Type -> LintM Type
applySubstTy Type
ty = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
ty) }

applySubstCo :: InCoercion -> LintM OutCoercion
applySubstCo :: Coercion -> LintM Coercion
applySubstCo Coercion
co = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst; Coercion -> LintM Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return (HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo TCvSubst
subst Coercion
co) }

lookupIdInScope :: Id -> LintM Id
lookupIdInScope :: Var -> LintM Var
lookupIdInScope Var
id_occ
  = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; case InScopeSet -> Var -> Maybe Var
lookupInScope (TCvSubst -> InScopeSet
getTCvInScope TCvSubst
subst) Var
id_occ of
           Just Var
id_bnd  -> do { Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Var -> Bool
bad_global Var
id_bnd)) SDoc
global_in_scope
                              ; Var -> LintM Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
id_bnd }
           Maybe Var
Nothing -> do { Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not Bool
is_local) SDoc
local_out_of_scope
                         ; Var -> LintM Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
id_occ } }
  where
    is_local :: Bool
is_local = Var -> Bool
mustHaveLocalBinding Var
id_occ
    local_out_of_scope :: SDoc
local_out_of_scope = String -> SDoc
text String
"Out of scope:" SDoc -> SDoc -> SDoc
<+> BindingSite -> Var -> SDoc
forall a. OutputableBndr a => BindingSite -> a -> SDoc
pprBndr BindingSite
LetBind Var
id_occ
    global_in_scope :: SDoc
global_in_scope    = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Occurrence is GlobalId, but binding is LocalId")
                            Int
2 (BindingSite -> Var -> SDoc
forall a. OutputableBndr a => BindingSite -> a -> SDoc
pprBndr BindingSite
LetBind Var
id_occ)
    bad_global :: Var -> Bool
bad_global Var
id_bnd = Var -> Bool
isGlobalId Var
id_occ
                     Bool -> Bool -> Bool
&& Var -> Bool
isLocalId Var
id_bnd
                     Bool -> Bool -> Bool
&& Bool -> Bool
not (Name -> Bool
isWiredInName (Var -> Name
idName Var
id_occ))
       -- 'bad_global' checks for the case where an /occurrence/ is
       -- a GlobalId, but there is an enclosing binding fora a LocalId.
       -- NB: the in-scope variables are mostly LocalIds, checked by lintIdBndr,
       --     but GHCi adds GlobalIds from the interactive context.  These
       --     are fine; hence the test (isLocalId id == isLocalId v)
       -- NB: when compiling Control.Exception.Base, things like absentError
       --     are defined locally, but appear in expressions as (global)
       --     wired-in Ids after worker/wrapper
       --     So we simply disable the test in this case

lookupJoinId :: Id -> LintM (Maybe JoinArity)
-- Look up an Id which should be a join point, valid here
-- If so, return its arity, if not return Nothing
lookupJoinId :: Var -> LintM (Maybe Int)
lookupJoinId Var
id
  = do { VarSet
join_set <- LintM VarSet
getValidJoins
       ; case VarSet -> Var -> Maybe Var
lookupVarSet VarSet
join_set Var
id of
            Just Var
id' -> Maybe Int -> LintM (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Maybe Int
isJoinId_maybe Var
id')
            Maybe Var
Nothing  -> Maybe Int -> LintM (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Int
forall a. Maybe a
Nothing }

lintTyCoVarInScope :: TyCoVar -> LintM ()
lintTyCoVarInScope :: Var -> LintM ()
lintTyCoVarInScope Var
var
  = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; Bool -> SDoc -> LintM ()
lintL (Var
var Var -> TCvSubst -> Bool
`isInScope` TCvSubst
subst)
               (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"The variable" SDoc -> SDoc -> SDoc
<+> BindingSite -> Var -> SDoc
forall a. OutputableBndr a => BindingSite -> a -> SDoc
pprBndr BindingSite
LetBind Var
var)
                   Int
2 (String -> SDoc
text String
"is out of scope")) }

ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
-- check ty2 is subtype of ty1 (ie, has same structure but usage
-- annotations need only be consistent, not equal)
-- Assumes ty1,ty2 are have already had the substitution applied
ensureEqTys :: Type -> Type -> SDoc -> LintM ()
ensureEqTys Type
ty1 Type
ty2 SDoc
msg = Bool -> SDoc -> LintM ()
lintL (Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2) SDoc
msg

lintRole :: Outputable thing
          => thing     -- where the role appeared
          -> Role      -- expected
          -> Role      -- actual
          -> LintM ()
lintRole :: thing -> Role -> Role -> LintM ()
lintRole thing
co Role
r1 Role
r2
  = Bool -> SDoc -> LintM ()
lintL (Role
r1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
r2)
          (String -> SDoc
text String
"Role incompatibility: expected" SDoc -> SDoc -> SDoc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r1 SDoc -> SDoc -> SDoc
<> SDoc
comma SDoc -> SDoc -> SDoc
<+>
           String -> SDoc
text String
"got" SDoc -> SDoc -> SDoc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r2 SDoc -> SDoc -> SDoc
$$
           String -> SDoc
text String
"in" SDoc -> SDoc -> SDoc
<+> thing -> SDoc
forall a. Outputable a => a -> SDoc
ppr thing
co)

{-
************************************************************************
*                                                                      *
\subsection{Error messages}
*                                                                      *
************************************************************************
-}

dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)

dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
dumpLoc (RhsOf Var
v)
  = (Var -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Var
v, String -> SDoc
text String
"In the RHS of" SDoc -> SDoc -> SDoc
<+> [Var] -> SDoc
pp_binders [Var
v])

dumpLoc (LambdaBodyOf Var
b)
  = (Var -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Var
b, String -> SDoc
text String
"In the body of lambda with binder" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
pp_binder Var
b)

dumpLoc (UnfoldingOf Var
b)
  = (Var -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Var
b, String -> SDoc
text String
"In the unfolding of" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
pp_binder Var
b)

dumpLoc (BodyOfLetRec [])
  = (SrcLoc
noSrcLoc, String -> SDoc
text String
"In body of a letrec with no binders")

dumpLoc (BodyOfLetRec bs :: [Var]
bs@(Var
_:[Var]
_))
  = ( Var -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc ([Var] -> Var
forall a. [a] -> a
head [Var]
bs), String -> SDoc
text String
"In the body of letrec with binders" SDoc -> SDoc -> SDoc
<+> [Var] -> SDoc
pp_binders [Var]
bs)

dumpLoc (AnExpr CoreExpr
e)
  = (SrcLoc
noSrcLoc, String -> SDoc
text String
"In the expression:" SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)

dumpLoc (CaseAlt (AltCon
con, [Var]
args, CoreExpr
_))
  = (SrcLoc
noSrcLoc, String -> SDoc
text String
"In a case alternative:" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (AltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr AltCon
con SDoc -> SDoc -> SDoc
<+> [Var] -> SDoc
pp_binders [Var]
args))

dumpLoc (CasePat (AltCon
con, [Var]
args, CoreExpr
_))
  = (SrcLoc
noSrcLoc, String -> SDoc
text String
"In the pattern of a case alternative:" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens (AltCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr AltCon
con SDoc -> SDoc -> SDoc
<+> [Var] -> SDoc
pp_binders [Var]
args))

dumpLoc (CaseTy CoreExpr
scrut)
  = (SrcLoc
noSrcLoc, SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"In the result-type of a case with scrutinee:")
                  Int
2 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
scrut))

dumpLoc (IdTy Var
b)
  = (Var -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Var
b, String -> SDoc
text String
"In the type of a binder:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
b)

dumpLoc (ImportedUnfolding SrcLoc
locn)
  = (SrcLoc
locn, String -> SDoc
text String
"In an imported unfolding")
dumpLoc LintLocInfo
TopLevelBindings
  = (SrcLoc
noSrcLoc, SDoc
Outputable.empty)
dumpLoc (InType Type
ty)
  = (SrcLoc
noSrcLoc, String -> SDoc
text String
"In the type" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty))
dumpLoc (InCo Coercion
co)
  = (SrcLoc
noSrcLoc, String -> SDoc
text String
"In the coercion" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co))

pp_binders :: [Var] -> SDoc
pp_binders :: [Var] -> SDoc
pp_binders [Var]
bs = [SDoc] -> SDoc
sep (SDoc -> [SDoc] -> [SDoc]
punctuate SDoc
comma ((Var -> SDoc) -> [Var] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Var -> SDoc
pp_binder [Var]
bs))

pp_binder :: Var -> SDoc
pp_binder :: Var -> SDoc
pp_binder Var
b | Var -> Bool
isId Var
b    = [SDoc] -> SDoc
hsep [Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
b, SDoc
dcolon, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
idType Var
b)]
            | Bool
otherwise = [SDoc] -> SDoc
hsep [Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
b, SDoc
dcolon, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
tyVarKind Var
b)]

------------------------------------------------------
--      Messages for case expressions

mkDefaultArgsMsg :: [Var] -> MsgDoc
mkDefaultArgsMsg :: [Var] -> SDoc
mkDefaultArgsMsg [Var]
args
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"DEFAULT case with binders")
         Int
4 ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
args)

mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
mkCaseAltMsg :: CoreExpr -> Type -> Type -> SDoc
mkCaseAltMsg CoreExpr
e Type
ty1 Type
ty2
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Type of case alternatives not the same as the annotation on case:")
         Int
4 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Actual type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1,
                   String -> SDoc
text String
"Annotation on case:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2,
                   String -> SDoc
text String
"Alt Rhs:" SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e ])

mkScrutMsg :: Id -> Type -> Type -> TCvSubst -> MsgDoc
mkScrutMsg :: Var -> Type -> Type -> TCvSubst -> SDoc
mkScrutMsg Var
var Type
var_ty Type
scrut_ty TCvSubst
subst
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
"Result binder in case doesn't match scrutinee:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var,
          String -> SDoc
text String
"Result binder type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
var_ty,--(idType var),
          String -> SDoc
text String
"Scrutinee type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
scrut_ty,
     [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Current TCv subst", TCvSubst -> SDoc
forall a. Outputable a => a -> SDoc
ppr TCvSubst
subst]]

mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
mkNonDefltMsg :: CoreExpr -> SDoc
mkNonDefltMsg CoreExpr
e
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Case expression with DEFAULT not at the beginning") Int
4 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)
mkNonIncreasingAltsMsg :: CoreExpr -> SDoc
mkNonIncreasingAltsMsg CoreExpr
e
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Case expression with badly-ordered alternatives") Int
4 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)

nonExhaustiveAltsMsg :: CoreExpr -> MsgDoc
nonExhaustiveAltsMsg :: CoreExpr -> SDoc
nonExhaustiveAltsMsg CoreExpr
e
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Case expression with non-exhaustive alternatives") Int
4 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)

mkBadConMsg :: TyCon -> DataCon -> MsgDoc
mkBadConMsg :: TyCon -> DataCon -> SDoc
mkBadConMsg TyCon
tycon DataCon
datacon
  = [SDoc] -> SDoc
vcat [
        String -> SDoc
text String
"In a case alternative, data constructor isn't in scrutinee type:",
        String -> SDoc
text String
"Scrutinee type constructor:" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon,
        String -> SDoc
text String
"Data con:" SDoc -> SDoc -> SDoc
<+> DataCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr DataCon
datacon
    ]

mkBadPatMsg :: Type -> Type -> MsgDoc
mkBadPatMsg :: Type -> Type -> SDoc
mkBadPatMsg Type
con_result_ty Type
scrut_ty
  = [SDoc] -> SDoc
vcat [
        String -> SDoc
text String
"In a case alternative, pattern result type doesn't match scrutinee type:",
        String -> SDoc
text String
"Pattern result type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
con_result_ty,
        String -> SDoc
text String
"Scrutinee type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
scrut_ty
    ]

integerScrutinisedMsg :: MsgDoc
integerScrutinisedMsg :: SDoc
integerScrutinisedMsg
  = String -> SDoc
text String
"In a LitAlt, the literal is lifted (probably Integer)"

mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
mkBadAltMsg :: Type -> Alt Var -> SDoc
mkBadAltMsg Type
scrut_ty Alt Var
alt
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Data alternative when scrutinee is not a tycon application",
           String -> SDoc
text String
"Scrutinee type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
scrut_ty,
           String -> SDoc
text String
"Alternative:" SDoc -> SDoc -> SDoc
<+> Alt Var -> SDoc
forall a. OutputableBndr a => (AltCon, [a], Expr a) -> SDoc
pprCoreAlt Alt Var
alt ]

mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
mkNewTyDataConAltMsg :: Type -> Alt Var -> SDoc
mkNewTyDataConAltMsg Type
scrut_ty Alt Var
alt
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Data alternative for newtype datacon",
           String -> SDoc
text String
"Scrutinee type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
scrut_ty,
           String -> SDoc
text String
"Alternative:" SDoc -> SDoc -> SDoc
<+> Alt Var -> SDoc
forall a. OutputableBndr a => (AltCon, [a], Expr a) -> SDoc
pprCoreAlt Alt Var
alt ]


------------------------------------------------------
--      Other error messages

mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
mkAppMsg :: Type -> Type -> CoreExpr -> SDoc
mkAppMsg Type
fun_ty Type
arg_ty CoreExpr
arg
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
"Argument value doesn't match argument type:",
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Fun type:") Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fun_ty),
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Arg type:") Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_ty),
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Arg:") Int
4 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
arg)]

mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
mkNonFunAppMsg :: Type -> Type -> CoreExpr -> SDoc
mkNonFunAppMsg Type
fun_ty Type
arg_ty CoreExpr
arg
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
"Non-function type in function position",
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Fun type:") Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fun_ty),
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Arg type:") Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_ty),
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Arg:") Int
4 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
arg)]

mkLetErr :: TyVar -> CoreExpr -> MsgDoc
mkLetErr :: Var -> CoreExpr -> SDoc
mkLetErr Var
bndr CoreExpr
rhs
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
"Bad `let' binding:",
          SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Variable:")
                 Int
4 (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
bndr)),
          SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Rhs:")
                 Int
4 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
rhs)]

mkTyAppMsg :: Type -> Type -> MsgDoc
mkTyAppMsg :: Type -> Type -> SDoc
mkTyAppMsg Type
ty Type
arg_ty
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
"Illegal type application:",
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Exp type:")
                 Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty)),
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Arg type:")
                 Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
arg_ty))]

emptyRec :: CoreExpr -> MsgDoc
emptyRec :: CoreExpr -> SDoc
emptyRec CoreExpr
e = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Empty Rec binding:") Int
2 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)

mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
mkRhsMsg :: Var -> SDoc -> Type -> SDoc
mkRhsMsg Var
binder SDoc
what Type
ty
  = [SDoc] -> SDoc
vcat
    [[SDoc] -> SDoc
hsep [String -> SDoc
text String
"The type of this binder doesn't match the type of its" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<> SDoc
colon,
            Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder],
     [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Binder's type:", Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
idType Var
binder)],
     [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Rhs type:", Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty]]

mkLetAppMsg :: CoreExpr -> MsgDoc
mkLetAppMsg :: CoreExpr -> SDoc
mkLetAppMsg CoreExpr
e
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"This argument does not satisfy the let/app invariant:")
       Int
2 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)

badBndrTyMsg :: Id -> SDoc -> MsgDoc
badBndrTyMsg :: Var -> SDoc -> SDoc
badBndrTyMsg Var
binder SDoc
what
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"The type of this binder is" SDoc -> SDoc -> SDoc
<+> SDoc
what SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder
         , String -> SDoc
text String
"Binder's type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
idType Var
binder) ]

mkStrictMsg :: Id -> MsgDoc
mkStrictMsg :: Var -> SDoc
mkStrictMsg Var
binder
  = [SDoc] -> SDoc
vcat [[SDoc] -> SDoc
hsep [String -> SDoc
text String
"Recursive or top-level binder has strict demand info:",
                     Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder],
              [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Binder's demand info:", Demand -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Demand
idDemandInfo Var
binder)]
             ]

mkNonTopExportedMsg :: Id -> MsgDoc
mkNonTopExportedMsg :: Var -> SDoc
mkNonTopExportedMsg Var
binder
  = [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Non-top-level binder is marked as exported:", Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder]

mkNonTopExternalNameMsg :: Id -> MsgDoc
mkNonTopExternalNameMsg :: Var -> SDoc
mkNonTopExternalNameMsg Var
binder
  = [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Non-top-level binder has an external name:", Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder]

mkTopNonLitStrMsg :: Id -> MsgDoc
mkTopNonLitStrMsg :: Var -> SDoc
mkTopNonLitStrMsg Var
binder
  = [SDoc] -> SDoc
hsep [String -> SDoc
text String
"Top-level Addr# binder has a non-literal rhs:", Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
binder]

mkKindErrMsg :: TyVar -> Type -> MsgDoc
mkKindErrMsg :: Var -> Type -> SDoc
mkKindErrMsg Var
tyvar Type
arg_ty
  = [SDoc] -> SDoc
vcat [String -> SDoc
text String
"Kinds don't match in type application:",
          SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Type variable:")
                 Int
4 (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tyvar SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
tyVarKind Var
tyvar)),
          SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Arg type:")
                 Int
4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_ty SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
arg_ty))]

mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> SDoc
mkCastErr CoreExpr
expr = String -> String -> SDoc -> Coercion -> Type -> Type -> SDoc
mk_cast_err String
"expression" String
"type" (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
expr)

mkCastTyErr :: Type -> Coercion -> Kind -> Kind -> MsgDoc
mkCastTyErr :: Type -> Coercion -> Type -> Type -> SDoc
mkCastTyErr Type
ty = String -> String -> SDoc -> Coercion -> Type -> Type -> SDoc
mk_cast_err String
"type" String
"kind" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)

mk_cast_err :: String -- ^ What sort of casted thing this is
                      --   (\"expression\" or \"type\").
            -> String -- ^ What sort of coercion is being used
                      --   (\"type\" or \"kind\").
            -> SDoc   -- ^ The thing being casted.
            -> Coercion -> Type -> Type -> MsgDoc
mk_cast_err :: String -> String -> SDoc -> Coercion -> Type -> Type -> SDoc
mk_cast_err String
thing_str String
co_str SDoc
pp_thing Coercion
co Type
from_ty Type
thing_ty
  = [SDoc] -> SDoc
vcat [SDoc
from_msg SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"of Cast differs from" SDoc -> SDoc -> SDoc
<+> SDoc
co_msg
            SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"of" SDoc -> SDoc -> SDoc
<+> SDoc
enclosed_msg,
          SDoc
from_msg SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
from_ty,
          String -> SDoc
text (String -> String
capitalise String
co_str) SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"of" SDoc -> SDoc -> SDoc
<+> SDoc
enclosed_msg SDoc -> SDoc -> SDoc
<> SDoc
colon
            SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
thing_ty,
          String -> SDoc
text String
"Actual" SDoc -> SDoc -> SDoc
<+> SDoc
enclosed_msg SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> SDoc
pp_thing,
          String -> SDoc
text String
"Coercion used in cast:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co
         ]
  where
    co_msg, from_msg, enclosed_msg :: SDoc
    co_msg :: SDoc
co_msg       = String -> SDoc
text String
co_str
    from_msg :: SDoc
from_msg     = String -> SDoc
text String
"From-" SDoc -> SDoc -> SDoc
<> SDoc
co_msg
    enclosed_msg :: SDoc
enclosed_msg = String -> SDoc
text String
"enclosed" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
thing_str

mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
mkBadUnivCoMsg LeftOrRight
lr Coercion
co
  = String -> SDoc
text String
"Kind mismatch on the" SDoc -> SDoc -> SDoc
<+> LeftOrRight -> SDoc
pprLeftOrRight LeftOrRight
lr SDoc -> SDoc -> SDoc
<+>
    String -> SDoc
text String
"side of a UnivCo:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co

mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
mkBadProofIrrelMsg :: Type -> Coercion -> SDoc
mkBadProofIrrelMsg Type
ty Coercion
co
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Found a non-coercion in a proof-irrelevance UnivCo:")
       Int
2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text String
"type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
               , String -> SDoc
text String
"co:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co ])

mkBadTyVarMsg :: Var -> SDoc
mkBadTyVarMsg :: Var -> SDoc
mkBadTyVarMsg Var
tv
  = String -> SDoc
text String
"Non-tyvar used in TyVarTy:"
      SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
tv SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
varType Var
tv)

mkBadJoinBindMsg :: Var -> SDoc
mkBadJoinBindMsg :: Var -> SDoc
mkBadJoinBindMsg Var
var
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Bad join point binding:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var
         , String -> SDoc
text String
"Join points can be bound only by a non-top-level let" ]

mkInvalidJoinPointMsg :: Var -> Type -> SDoc
mkInvalidJoinPointMsg :: Var -> Type -> SDoc
mkInvalidJoinPointMsg Var
var Type
ty
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Join point has invalid type:")
        Int
2 (Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var SDoc -> SDoc -> SDoc
<+> SDoc
dcolon SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)

mkBadJoinArityMsg :: Var -> Int -> Int -> CoreExpr -> SDoc
mkBadJoinArityMsg :: Var -> Int -> Int -> CoreExpr -> SDoc
mkBadJoinArityMsg Var
var Int
ar Int
nlams CoreExpr
rhs
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Join point has too few lambdas",
           String -> SDoc
text String
"Join var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var,
           String -> SDoc
text String
"Join arity:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
ar,
           String -> SDoc
text String
"Number of lambdas:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
nlams,
           String -> SDoc
text String
"Rhs = " SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
rhs
           ]

invalidJoinOcc :: Var -> SDoc
invalidJoinOcc :: Var -> SDoc
invalidJoinOcc Var
var
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Invalid occurrence of a join variable:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var
         , String -> SDoc
text String
"The binder is either not a join point, or not valid here" ]

mkBadJumpMsg :: Var -> Int -> Int -> SDoc
mkBadJumpMsg :: Var -> Int -> Int -> SDoc
mkBadJumpMsg Var
var Int
ar Int
nargs
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Join point invoked with wrong number of arguments",
           String -> SDoc
text String
"Join var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var,
           String -> SDoc
text String
"Join arity:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
ar,
           String -> SDoc
text String
"Number of arguments:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
nargs ]

mkInconsistentRecMsg :: [Var] -> SDoc
mkInconsistentRecMsg :: [Var] -> SDoc
mkInconsistentRecMsg [Var]
bndrs
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Recursive let binders mix values and join points",
           String -> SDoc
text String
"Binders:" SDoc -> SDoc -> SDoc
<+> [SDoc] -> SDoc
hsep ((Var -> SDoc) -> [Var] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Var -> SDoc
ppr_with_details [Var]
bndrs) ]
  where
    ppr_with_details :: Var -> SDoc
ppr_with_details Var
bndr = Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr SDoc -> SDoc -> SDoc
<> IdDetails -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> IdDetails
idDetails Var
bndr)

mkJoinBndrOccMismatchMsg :: Var -> JoinArity -> JoinArity -> SDoc
mkJoinBndrOccMismatchMsg :: Var -> Int -> Int -> SDoc
mkJoinBndrOccMismatchMsg Var
bndr Int
join_arity_bndr Int
join_arity_occ
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Mismatch in join point arity between binder and occurrence"
         , String -> SDoc
text String
"Var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr
         , String -> SDoc
text String
"Arity at binding site:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
join_arity_bndr
         , String -> SDoc
text String
"Arity at occurrence:  " SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
join_arity_occ ]

mkBndrOccTypeMismatchMsg :: Var -> Var -> OutType -> OutType -> SDoc
mkBndrOccTypeMismatchMsg :: Var -> Var -> Type -> Type -> SDoc
mkBndrOccTypeMismatchMsg Var
bndr Var
var Type
bndr_ty Type
var_ty
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Mismatch in type between binder and occurrence"
         , String -> SDoc
text String
"Var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr
         , String -> SDoc
text String
"Binder type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
bndr_ty
         , String -> SDoc
text String
"Occurrence type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
var_ty
         , String -> SDoc
text String
"  Before subst:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
idType Var
var) ]

mkBadJoinPointRuleMsg :: JoinId -> JoinArity -> CoreRule -> SDoc
mkBadJoinPointRuleMsg :: Var -> Int -> CoreRule -> SDoc
mkBadJoinPointRuleMsg Var
bndr Int
join_arity CoreRule
rule
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Join point has rule with wrong number of arguments"
         , String -> SDoc
text String
"Var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr
         , String -> SDoc
text String
"Join arity:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
join_arity
         , String -> SDoc
text String
"Rule:" SDoc -> SDoc -> SDoc
<+> CoreRule -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreRule
rule ]

pprLeftOrRight :: LeftOrRight -> MsgDoc
pprLeftOrRight :: LeftOrRight -> SDoc
pprLeftOrRight LeftOrRight
CLeft  = String -> SDoc
text String
"left"
pprLeftOrRight LeftOrRight
CRight = String -> SDoc
text String
"right"

dupVars :: [NonEmpty Var] -> MsgDoc
dupVars :: [NonEmpty Var] -> SDoc
dupVars [NonEmpty Var]
vars
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Duplicate variables brought into scope")
       Int
2 ([[Var]] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((NonEmpty Var -> [Var]) -> [NonEmpty Var] -> [[Var]]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty Var -> [Var]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [NonEmpty Var]
vars))

dupExtVars :: [NonEmpty Name] -> MsgDoc
dupExtVars :: [NonEmpty Name] -> SDoc
dupExtVars [NonEmpty Name]
vars
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"Duplicate top-level variables with the same qualified name")
       Int
2 ([[Name]] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((NonEmpty Name -> [Name]) -> [NonEmpty Name] -> [[Name]]
forall a b. (a -> b) -> [a] -> [b]
map NonEmpty Name -> [Name]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [NonEmpty Name]
vars))

{-
************************************************************************
*                                                                      *
\subsection{Annotation Linting}
*                                                                      *
************************************************************************
-}

-- | This checks whether a pass correctly looks through debug
-- annotations (@SourceNote@). This works a bit different from other
-- consistency checks: We check this by running the given task twice,
-- noting all differences between the results.
lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
lintAnnots :: SDoc -> (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
lintAnnots SDoc
pname ModGuts -> CoreM ModGuts
pass ModGuts
guts = do
  -- Run the pass as we normally would
  DynFlags
dflags <- CoreM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DoAnnotationLinting DynFlags
dflags) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$
    IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> String -> IO ()
Err.showPass DynFlags
dflags String
"Annotation linting - first run"
  ModGuts
nguts <- ModGuts -> CoreM ModGuts
pass ModGuts
guts
  -- If appropriate re-run it without debug annotations to make sure
  -- that they made no difference.
  Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (GeneralFlag -> DynFlags -> Bool
gopt GeneralFlag
Opt_DoAnnotationLinting DynFlags
dflags) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ do
    IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> String -> IO ()
Err.showPass DynFlags
dflags String
"Annotation linting - second run"
    ModGuts
nguts' <- (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
withoutAnnots ModGuts -> CoreM ModGuts
pass ModGuts
guts
    -- Finally compare the resulting bindings
    IO () -> CoreM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> CoreM ()) -> IO () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ DynFlags -> String -> IO ()
Err.showPass DynFlags
dflags String
"Annotation linting - comparison"
    let binds :: [(Var, CoreExpr)]
binds = CoreProgram -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (CoreProgram -> [(Var, CoreExpr)])
-> CoreProgram -> [(Var, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ ModGuts -> CoreProgram
mg_binds ModGuts
nguts
        binds' :: [(Var, CoreExpr)]
binds' = CoreProgram -> [(Var, CoreExpr)]
forall b. [Bind b] -> [(b, Expr b)]
flattenBinds (CoreProgram -> [(Var, CoreExpr)])
-> CoreProgram -> [(Var, CoreExpr)]
forall a b. (a -> b) -> a -> b
$ ModGuts -> CoreProgram
mg_binds ModGuts
nguts'
        ([SDoc]
diffs,RnEnv2
_) = Bool
-> RnEnv2
-> [(Var, CoreExpr)]
-> [(Var, CoreExpr)]
-> ([SDoc], RnEnv2)
diffBinds Bool
True (InScopeSet -> RnEnv2
mkRnEnv2 InScopeSet
emptyInScopeSet) [(Var, CoreExpr)]
binds [(Var, CoreExpr)]
binds'
    Bool -> CoreM () -> CoreM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not ([SDoc] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SDoc]
diffs)) (CoreM () -> CoreM ()) -> CoreM () -> CoreM ()
forall a b. (a -> b) -> a -> b
$ SDoc -> CoreM ()
CoreMonad.putMsg (SDoc -> CoreM ()) -> SDoc -> CoreM ()
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
      [ String -> SDoc -> SDoc
lint_banner String
"warning" SDoc
pname
      , String -> SDoc
text String
"Core changes with annotations:"
      , PprStyle -> SDoc -> SDoc
withPprStyle (DynFlags -> PprStyle
defaultDumpStyle DynFlags
dflags) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ Int -> SDoc -> SDoc
nest Int
2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat [SDoc]
diffs
      ]
  -- Return actual new guts
  ModGuts -> CoreM ModGuts
forall (m :: * -> *) a. Monad m => a -> m a
return ModGuts
nguts

-- | Run the given pass without annotations. This means that we both
-- set the debugLevel setting to 0 in the environment as well as all
-- annotations from incoming modules.
withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
withoutAnnots :: (ModGuts -> CoreM ModGuts) -> ModGuts -> CoreM ModGuts
withoutAnnots ModGuts -> CoreM ModGuts
pass ModGuts
guts = do
  -- Remove debug flag from environment.
  DynFlags
dflags <- CoreM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  let removeFlag :: HscEnv -> HscEnv
removeFlag HscEnv
env = HscEnv
env{ hsc_dflags :: DynFlags
hsc_dflags = DynFlags
dflags{ debugLevel :: Int
debugLevel = Int
0} }
      withoutFlag :: CoreM a -> CoreM (a, SimplCount)
withoutFlag CoreM a
corem =
          -- TODO: supply tag here as well ?
        IO (a, SimplCount) -> CoreM (a, SimplCount)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (a, SimplCount) -> CoreM (a, SimplCount))
-> CoreM (IO (a, SimplCount)) -> CoreM (a, SimplCount)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< HscEnv
-> RuleBase
-> Char
-> Module
-> ModuleSet
-> PrintUnqualified
-> SrcSpan
-> CoreM a
-> IO (a, SimplCount)
forall a.
HscEnv
-> RuleBase
-> Char
-> Module
-> ModuleSet
-> PrintUnqualified
-> SrcSpan
-> CoreM a
-> IO (a, SimplCount)
runCoreM (HscEnv
 -> RuleBase
 -> Char
 -> Module
 -> ModuleSet
 -> PrintUnqualified
 -> SrcSpan
 -> CoreM a
 -> IO (a, SimplCount))
-> CoreM HscEnv
-> CoreM
     (RuleBase
      -> Char
      -> Module
      -> ModuleSet
      -> PrintUnqualified
      -> SrcSpan
      -> CoreM a
      -> IO (a, SimplCount))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (HscEnv -> HscEnv) -> CoreM HscEnv -> CoreM HscEnv
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HscEnv -> HscEnv
removeFlag CoreM HscEnv
getHscEnv CoreM
  (RuleBase
   -> Char
   -> Module
   -> ModuleSet
   -> PrintUnqualified
   -> SrcSpan
   -> CoreM a
   -> IO (a, SimplCount))
-> CoreM RuleBase
-> CoreM
     (Char
      -> Module
      -> ModuleSet
      -> PrintUnqualified
      -> SrcSpan
      -> CoreM a
      -> IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreM RuleBase
getRuleBase CoreM
  (Char
   -> Module
   -> ModuleSet
   -> PrintUnqualified
   -> SrcSpan
   -> CoreM a
   -> IO (a, SimplCount))
-> CoreM Char
-> CoreM
     (Module
      -> ModuleSet
      -> PrintUnqualified
      -> SrcSpan
      -> CoreM a
      -> IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                CoreM Char
getUniqMask CoreM
  (Module
   -> ModuleSet
   -> PrintUnqualified
   -> SrcSpan
   -> CoreM a
   -> IO (a, SimplCount))
-> CoreM Module
-> CoreM
     (ModuleSet
      -> PrintUnqualified -> SrcSpan -> CoreM a -> IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreM Module
forall (m :: * -> *). HasModule m => m Module
getModule CoreM
  (ModuleSet
   -> PrintUnqualified -> SrcSpan -> CoreM a -> IO (a, SimplCount))
-> CoreM ModuleSet
-> CoreM
     (PrintUnqualified -> SrcSpan -> CoreM a -> IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                CoreM ModuleSet
getVisibleOrphanMods CoreM
  (PrintUnqualified -> SrcSpan -> CoreM a -> IO (a, SimplCount))
-> CoreM PrintUnqualified
-> CoreM (SrcSpan -> CoreM a -> IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                CoreM PrintUnqualified
getPrintUnqualified CoreM (SrcSpan -> CoreM a -> IO (a, SimplCount))
-> CoreM SrcSpan -> CoreM (CoreM a -> IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> CoreM SrcSpan
getSrcSpanM CoreM (CoreM a -> IO (a, SimplCount))
-> CoreM (CoreM a) -> CoreM (IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                CoreM a -> CoreM (CoreM a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure CoreM a
corem
  -- Nuke existing ticks in module.
  -- TODO: Ticks in unfoldings. Maybe change unfolding so it removes
  -- them in absence of debugLevel > 0.
  let nukeTicks :: Expr b -> Expr b
nukeTicks = (Tickish Var -> Bool) -> Expr b -> Expr b
forall b. (Tickish Var -> Bool) -> Expr b -> Expr b
stripTicksE (Bool -> Bool
not (Bool -> Bool) -> (Tickish Var -> Bool) -> Tickish Var -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tickish Var -> Bool
forall id. Tickish id -> Bool
tickishIsCode)
      nukeAnnotsBind :: CoreBind -> CoreBind
      nukeAnnotsBind :: Bind Var -> Bind Var
nukeAnnotsBind Bind Var
bind = case Bind Var
bind of
        Rec [(Var, CoreExpr)]
bs     -> [(Var, CoreExpr)] -> Bind Var
forall b. [(b, Expr b)] -> Bind b
Rec ([(Var, CoreExpr)] -> Bind Var) -> [(Var, CoreExpr)] -> Bind Var
forall a b. (a -> b) -> a -> b
$ ((Var, CoreExpr) -> (Var, CoreExpr))
-> [(Var, CoreExpr)] -> [(Var, CoreExpr)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Var
b,CoreExpr
e) -> (Var
b, CoreExpr -> CoreExpr
forall b. Expr b -> Expr b
nukeTicks CoreExpr
e)) [(Var, CoreExpr)]
bs
        NonRec Var
b CoreExpr
e -> Var -> CoreExpr -> Bind Var
forall b. b -> Expr b -> Bind b
NonRec Var
b (CoreExpr -> Bind Var) -> CoreExpr -> Bind Var
forall a b. (a -> b) -> a -> b
$ CoreExpr -> CoreExpr
forall b. Expr b -> Expr b
nukeTicks CoreExpr
e
      nukeAnnotsMod :: ModGuts -> ModGuts
nukeAnnotsMod mg :: ModGuts
mg@ModGuts{mg_binds :: ModGuts -> CoreProgram
mg_binds=CoreProgram
binds}
        = ModGuts
mg{mg_binds :: CoreProgram
mg_binds = (Bind Var -> Bind Var) -> CoreProgram -> CoreProgram
forall a b. (a -> b) -> [a] -> [b]
map Bind Var -> Bind Var
nukeAnnotsBind CoreProgram
binds}
  -- Perform pass with all changes applied
  ((ModGuts, SimplCount) -> ModGuts)
-> CoreM (ModGuts, SimplCount) -> CoreM ModGuts
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (ModGuts, SimplCount) -> ModGuts
forall a b. (a, b) -> a
fst (CoreM (ModGuts, SimplCount) -> CoreM ModGuts)
-> CoreM (ModGuts, SimplCount) -> CoreM ModGuts
forall a b. (a -> b) -> a -> b
$ CoreM ModGuts -> CoreM (ModGuts, SimplCount)
forall a. CoreM a -> CoreM (a, SimplCount)
withoutFlag (CoreM ModGuts -> CoreM (ModGuts, SimplCount))
-> CoreM ModGuts -> CoreM (ModGuts, SimplCount)
forall a b. (a -> b) -> a -> b
$ ModGuts -> CoreM ModGuts
pass (ModGuts -> ModGuts
nukeAnnotsMod ModGuts
guts)