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


A ``lint'' pass to check for Core correctness
-}

{-# LANGUAGE CPP #-}

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 Kind
import Type
import RepType
import TyCoRep       -- checks validity of types/coercions
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 UniqSupply
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 [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://ghc.haskell.org/trac/ghc/wiki/BadUnsafeCoercions
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 pass :: CoreToDo
pass binds :: CoreProgram
binds rules :: [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 hsc_env :: HscEnv
hsc_env print_unqual :: PrintUnqualified
print_unqual pass :: CoreToDo
pass binds :: CoreProgram
binds rules :: [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 flag :: 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
forall a. Maybe a
Nothing

dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
dumpIfSet dflags :: DynFlags
dflags dump_me :: Bool
dump_me pass :: CoreToDo
pass extra_info :: SDoc
extra_info doc :: 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 dflags :: DynFlags
dflags unqual :: PrintUnqualified
unqual mb_flag :: Maybe DumpFlag
mb_flag hdr :: SDoc
hdr extra_info :: SDoc
extra_info binds :: CoreProgram
binds rules :: [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
$ \flag :: 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 2 SDoc
size_doc
       }

  where
    size_doc :: SDoc
size_doc = [SDoc] -> SDoc
sep [String -> SDoc
text "Result size of" SDoc -> SDoc -> SDoc
<+> SDoc
hdr, Int -> SDoc -> SDoc
nest 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 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 "------ 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 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 CoreLiberateCase         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag CoreDoStaticArgs         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_verbose_core2core
coreDumpFlag CoreDoCallArity          = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_call_arity
coreDumpFlag CoreDoExitify            = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_exitify
coreDumpFlag CoreDoStrictness         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_stranal
coreDumpFlag CoreDoWorkerWrapper      = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_worker_wrapper
coreDumpFlag CoreDoSpecialising       = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_spec
coreDumpFlag CoreDoSpecConstr         = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_spec
coreDumpFlag CoreCSE                  = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_cse
coreDumpFlag CoreDesugar              = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_ds_preopt
coreDumpFlag CoreDesugarOpt           = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_ds
coreDumpFlag CoreTidy                 = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_simpl
coreDumpFlag CorePrep                 = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_prep
coreDumpFlag CoreOccurAnal            = DumpFlag -> Maybe DumpFlag
forall a. a -> Maybe a
Just DumpFlag
Opt_D_dump_occur_anal

coreDumpFlag CoreDoPrintCore          = Maybe DumpFlag
forall a. Maybe a
Nothing
coreDumpFlag (CoreDoRuleCheck {})     = Maybe DumpFlag
forall a. Maybe a
Nothing
coreDumpFlag 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 hsc_env :: HscEnv
hsc_env pass :: CoreToDo
pass binds :: 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 (warns :: Bag SDoc
warns, errs :: 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 ("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 dflags :: DynFlags
dflags pass :: CoreToDo
pass warns :: Bag SDoc
warns errs :: Bag SDoc
errs binds :: 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 "errors" (CoreToDo -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreToDo
pass), Bag SDoc -> SDoc
Err.pprMessageBag Bag SDoc
errs
                 , String -> SDoc
text "*** Offending Program ***"
                 , CoreProgram -> SDoc
forall b. OutputableBndr b => [Bind b] -> SDoc
pprCoreBindings CoreProgram
binds
                 , String -> SDoc
text "*** End of Offense ***" ])
       ; DynFlags -> Int -> IO ()
Err.ghcExit DynFlags
dflags 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 "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
string pass :: SDoc
pass = String -> SDoc
text "*** Core Lint"      SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
string
                          SDoc -> SDoc -> SDoc
<+> String -> SDoc
text ": in result of" SDoc -> SDoc -> SDoc
<+> SDoc
pass
                          SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "***"

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 _ (SimplMode { sm_phase :: SimplMode -> CompilerPhase
sm_phase = CompilerPhase
InitialPhase })) = Bool
False
showLintWarnings _ = Bool
True

lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
lintInteractiveExpr what :: String
what hsc_env :: HscEnv
hsc_env expr :: 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 err :: 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 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 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 "errors" (String -> SDoc
text String
what)
                     , SDoc
err
                     , String -> SDoc
text "*** Offending Program ***"
                     , CoreExpr -> SDoc
forall b. OutputableBndr b => Expr b -> SDoc
pprCoreExpr CoreExpr
expr
                     , String -> SDoc
text "*** End of Offense ***" ])
           ; DynFlags -> Int -> IO ()
Err.ghcExit DynFlags
dflags 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 Trac #8215 for an example
interactiveInScope :: HscEnv -> [Var]
interactiveInScope hsc_env :: 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
    (cls_insts :: [ClsInst]
cls_insts, _fam_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)

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 dflags :: DynFlags
dflags pass :: CoreToDo
pass local_in_scope :: [Var]
local_in_scope binds :: 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
                      CoreTidy -> Bool
False
                      CorePrep -> Bool
False
                      _        -> Bool
True

    -- See Note [Checking for INLINE loop breakers]
    check_lbs :: Bool
check_lbs = case CoreToDo
pass of
                      CoreDesugar    -> Bool
False
                      CoreDesugarOpt -> Bool
False
                      _              -> 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 _ -> StaticPtrCheck
AllowAtTopLevel
                          CoreTidy              -> StaticPtrCheck
RejectEverywhere
                          CorePrep              -> StaticPtrCheck
AllowAtTopLevel
                          _                     -> StaticPtrCheck
AllowAnywhere

    binders :: [Var]
binders = CoreProgram -> [Var]
forall b. [Bind b] -> [b]
bindersOfBinds CoreProgram
binds
    (_, dups :: [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 n1 :: Name
n1 n2 :: Name
n2 | Just m1 :: Module
m1 <- Name -> Maybe Module
nameModule_maybe Name
n1
                  , Just m2 :: 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 prs :: [(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 bndr :: Var
bndr rhs :: 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 dflags :: DynFlags
dflags locn :: SrcLoc
locn vars :: VarSet
vars expr :: 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
    (_warns :: Bag SDoc
_warns, errs :: 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 dflags :: DynFlags
dflags vars :: [Var]
vars expr :: 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)
    (_warns :: Bag SDoc
_warns, errs :: 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 top_lvl_flag :: TopLevelFlag
top_lvl_flag rec_flag :: RecFlag
rec_flag (binder :: Var
binder,rhs :: 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 "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 "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 "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
            Nothing    -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            Just arity :: 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 "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

      -- Check whether arity and demand type are consistent (only if demand analysis
      -- already happened)
      --
      -- Note (Apr 2014): this is actually ok.  See Note [Demand analysis for trivial right-hand sides]
      --                  in DmdAnal.  After eta-expansion in CorePrep the rhs is no longer trivial.
      --       ; let dmdTy = idStrictness binder
      --       ; checkL (case dmdTy of
      --                  StrictSig dmd_ty -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs)
      --           (mkArityMsg binder)

       -- 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 "idArity" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Int
idArity Var
binder) SDoc -> SDoc -> SDoc
<+>
           String -> SDoc
text "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
           (demands :: [Demand]
demands, result_info :: 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 "idArity" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Int
idArity Var
binder) SDoc -> SDoc -> SDoc
<+>
               String -> SDoc
text "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)
           _ -> () -> 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 bndr :: Var
bndr rhs :: CoreExpr
rhs
    | Just arity :: 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 arity :: 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 0 _ _ rhs :: CoreExpr
rhs
      = CoreExpr -> LintM Type
lintCoreExpr CoreExpr
rhs

    lint_join_lams n :: Int
n tot :: Int
tot enforce :: Bool
enforce (Lam var :: Var
var expr :: 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
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
-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 n :: Int
n tot :: Int
tot True _other :: 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 _ _ False rhs :: 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 _bndr :: Var
_bndr rhs :: 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 AllowAtTopLevel
      | (binders0 :: [Var]
binders0, rhs' :: CoreExpr
rhs') <- CoreExpr -> ([Var], CoreExpr)
collectTyBinders CoreExpr
rhs
      , Just (fun :: CoreExpr
fun, t :: Type
t, info :: CoreExpr
info, e :: 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
var loopBinders :: 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
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
            LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (CoreExpr -> LintLocInfo
AnExpr CoreExpr
rhs') (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$ 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 _ = 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 bndr :: Var
bndr bndr_ty :: Type
bndr_ty uf :: Unfolding
uf
  | Unfolding -> Bool
isStableUnfolding Unfolding
uf
  , Just rhs :: 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 "unfolding") Type
ty) }
lintIdUnfolding  _ _ _
  = () -> 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)
  = Var -> Int -> LintM Type
lintVarOcc Var
var 0

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

lintCoreExpr (Cast expr :: CoreExpr
expr co :: 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
       ; (_, k2 :: Type
k2, from_ty :: Type
from_ty, to_ty :: Type
to_ty, r :: Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co'
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k2 (String -> SDoc
text "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 :: Tickish Var
tickish expr :: CoreExpr
expr)
  = do case Tickish Var
tickish of
         Breakpoint _ ids :: [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
$ \id :: Var
id -> do
                               Var -> LintM ()
checkDeadIdOcc Var
id
                               Var -> LintM Var
lookupIdInScope Var
id
         _                -> () -> 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 tv :: Var
tv (Type ty :: Type
ty)) body :: 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
$ \ tv' :: 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 bndr :: Var
bndr rhs :: CoreExpr
rhs) body :: 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] -> 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 pairs :: [(Var, CoreExpr)]
pairs) body :: 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
    (_, dups :: [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 _ _)
  = LintLocInfo -> LintM Type -> LintM Type
forall a. LintLocInfo -> LintM a -> LintM a
addLoc (CoreExpr -> LintLocInfo
AnExpr CoreExpr
e) (LintM Type -> LintM Type) -> LintM Type -> LintM Type
forall a b. (a -> b) -> a -> b
$
    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
    (fun :: CoreExpr
fun, args :: [CoreExpr]
args) = CoreExpr -> (CoreExpr, [CoreExpr])
forall b. Expr b -> (Expr b, [Expr b])
collectArgs CoreExpr
e

lintCoreExpr (Lam var :: Var
var expr :: 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
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 e :: CoreExpr
e@(Case scrut :: CoreExpr
scrut var :: Var
var alt_ty :: Type
alt_ty alts :: [Alt Var]
alts) =
       -- Check the scrutinee
  do { 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

     ; (alt_ty :: Type
alt_ty, _) <- Type -> LintM (Type, Type)
lintInTy Type
alt_ty
     ; (var_ty :: Type
var_ty, _) <- 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.

     -- See Note [Rules for floating-point comparisons] in PrelRules
     ; let isLitPat :: (AltCon, b, c) -> Bool
isLitPat (LitAlt _, _ , _) = Bool
True
           isLitPat _                 = 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
$ "Lint warning: Scrutinising floating-point " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                        "expression with literal pattern in case " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                        "analysis (see Trac #9238).")
          SDoc -> SDoc -> SDoc
$$ String -> SDoc
text "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
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 "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 ()
         _otherwise :: 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)

     ; 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
$ \_ ->
       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 } }

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

lintCoreExpr (Coercion co :: Coercion
co)
  = do { (k1 :: Type
k1, k2 :: Type
k2, ty1 :: Type
ty1, ty2 :: Type
ty2, role :: 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
var nargs :: Int
nargs
  = do  { Bool -> SDoc -> LintM ()
checkL (Var -> Bool
isNonCoVarId Var
var)
                 (String -> SDoc
text "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
/= 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 "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
var) nargs :: Int
nargs
  = Var -> Int -> LintM Type
lintVarOcc Var
var Int
nargs

lintCoreFun (Lam var :: Var
var body :: CoreExpr
body) nargs :: 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
/= 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
var' ->
    do { Type
body_ty <- CoreExpr -> Int -> LintM Type
lintCoreFun CoreExpr
body (Int
nargs Int -> Int -> Int
forall a. Num a => a -> a -> a
- 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 expr :: CoreExpr
expr nargs :: 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
/= 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 id :: 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 "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
var n_args :: Int
n_args
  | Just join_arity_occ :: 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 {
           Nothing -> -- Binder is not a join point
                      SDoc -> LintM ()
addErrL (Var -> SDoc
invalidJoinOcc Var
var) ;

           Just join_arity_bndr :: 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 Trac #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 (Trac #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 fun_ty :: Type
fun_ty args :: [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 fun_ty :: Type
fun_ty (Type arg_ty :: Type
arg_ty)
  = do { Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (Type -> Bool
isCoercionTy Type
arg_ty))
                (String -> SDoc
text "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 fun_ty :: Type
fun_ty arg :: 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 "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 scrut_ty :: Type
scrut_ty con_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 scrut_ty :: Type
scrut_ty con_ty :: Type
con_ty (bndr :: Var
bndr:bndrs :: [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 fun_ty :: Type
fun_ty arg_ty :: Type
arg_ty
  | Just (tv :: Var
tv,body_ty :: 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 TyCoRep
        ; 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 arg :: CoreExpr
arg fun_ty :: Type
fun_ty arg_ty :: Type
arg_ty
  | Just (arg :: Type
arg,res :: 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 tyvar :: Var
tyvar arg_ty :: 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 "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}
*                                                                      *
************************************************************************
-}

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 e :: CoreExpr
e ty :: Type
ty alts :: [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)
     ; 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)

          -- 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
    (con_alts :: [Alt Var]
con_alts, maybe_deflt :: 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 (alt1 :: (AltCon, a, b)
alt1 : rest :: [(AltCon, a, b)]
rest@( alt2 :: (AltCon, a, b)
alt2 : _)) = (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 _                         = Bool
True

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

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

lintAltExpr :: CoreExpr -> OutType -> LintM ()
lintAltExpr :: CoreExpr -> Type -> LintM ()
lintAltExpr expr :: CoreExpr
expr ann_ty :: 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) }

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 _ alt_ty :: Type
alt_ty (DEFAULT, args :: [Var]
args, rhs :: 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 scrut_ty :: Type
scrut_ty alt_ty :: Type
alt_ty (LitAlt lit :: Literal
lit, args :: [Var]
args, rhs :: 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 scrut_ty :: Type
scrut_ty alt_ty :: Type
alt_ty alt :: Alt Var
alt@(DataAlt con :: DataCon
con, args :: [Var]
args, rhs :: 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
tycon, tycon_arg_tys :: [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
$ \ args' :: [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 _    []         linterF :: [Var] -> LintM a
linterF = [Var] -> LintM a
linterF []
lintBinders site :: BindingSite
site (var :: Var
var:vars :: [Var]
vars) linterF :: [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
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
$ \ vars' :: [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 site :: BindingSite
site var :: Var
var linterF :: 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 tv :: Var
tv thing_inside :: Var -> LintM a
thing_inside
  = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; let (subst' :: TCvSubst
subst', tv' :: 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 cv :: Var
cv thing_inside :: Var -> LintM a
thing_inside
  = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; let (subst' :: TCvSubst
subst', cv' :: 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 "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 top_lvl :: TopLevelFlag
top_lvl ids :: [Var]
ids linterF :: LintM a
linterF
  = [Var] -> LintM a
go [Var]
ids
  where
    go :: [Var] -> LintM a
go []       = LintM a
linterF
    go (id :: Var
id:ids :: [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] -> 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 top_lvl :: TopLevelFlag
top_lvl bind_site :: BindingSite
bind_site id :: Var
id linterF :: 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 "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)

       ; (ty :: Type
ty, k :: Type
k) <- 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 "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 "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
                    LetBind -> Bool
True
                    _       -> Bool
False

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

lintTypes :: DynFlags
          -> [TyCoVar]   -- Treat these as in scope
          -> [Type]
          -> Maybe MsgDoc -- Nothing => OK
lintTypes :: DynFlags -> [Var] -> [Type] -> Maybe SDoc
lintTypes dflags :: DynFlags
dflags vars :: [Var]
vars tys :: [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
    (_warns :: Bag SDoc
_warns, errs :: 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
$ \_ ->
             (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 ty :: 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 tc :: TyCon
tc
  = Bool -> SDoc -> LintM ()
checkL (Bool -> Bool
not (TyCon -> Bool
isTcTyCon TyCon
tc)) (String -> SDoc
text "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 tv :: 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 t1 :: Type
t1 t2 :: 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 "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 tc :: TyCon
tc tys :: [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` 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 "Saturated application of (->)") 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 t1 :: Type
t1 t2 :: 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 "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 tv :: Var
tv _vis :: ArgFlag
_vis) ty :: 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
$ \tv' :: Var
tv' ->
    do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k (String -> SDoc
text "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 k' :: Type
k' -> Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
k'
           Nothing -> SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Variable escape in forall:")
                                    2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text "type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t
                                            , String -> SDoc
text "kind:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k ]))
    }

lintType t :: Type
t@(ForAllTy (Bndr cv :: Var
cv _vis :: ArgFlag
_vis) ty :: Type
ty)
  -- forall over coercions
  = do { Bool -> SDoc -> LintM ()
lintL (Var -> Bool
isCoVar Var
cv)
               (String -> SDoc
text "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 "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
$ \_ ->
    do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k (String -> SDoc
text "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 l :: 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 ty :: Type
ty co :: Coercion
co)
  = do { Type
k1 <- Type -> LintM Type
lintType Type
ty
       ; (k1' :: Type
k1', k2 :: 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 co :: Coercion
co)
  = do { (k1 :: Type
k1, k2 :: Type
k2, ty1 :: Type
ty1, ty2 :: Type
ty2, r :: 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 (Trac #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 report_unsat :: Bool
report_unsat ty :: Type
ty tc :: TyCon
tc tys :: [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 "Un-saturated type application") 2 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty))

  -- Deal with type synonyms
  | Just (tenv :: [(Var, Type)]
tenv, rhs :: Type
rhs, tys' :: [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 k :: 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 "Ill-kinded kind:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
k)
                                      2 (String -> SDoc
text "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 k :: Type
k doc :: SDoc
doc
  = Bool -> SDoc -> LintM ()
lintL (Type -> Bool
classifiesTypeWithValues Type
k)
          (String -> SDoc
text "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 "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 what :: SDoc
what k1 :: Type
k1 k2 :: 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 "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 "result")   Type
k2))
       ; Type -> LintM Type
forall (m :: * -> *) a. Monad m => a -> m a
return Type
liftedTypeKind }
  where
    msg :: SDoc -> a -> SDoc
msg ar :: SDoc
ar k :: a
k
      = [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Ill-kinded" SDoc -> SDoc -> SDoc
<+> SDoc
ar)
                  2 (String -> SDoc
text "in" SDoc -> SDoc -> SDoc
<+> SDoc
what)
             , SDoc
what SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "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 ty :: Type
ty k :: Type
k tys :: [(Type, Type)]
tys
  = SDoc -> Type -> [(Type, Type)] -> LintM Type
lint_app (String -> SDoc
text "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 ty :: Coercion
ty k :: Type
k tys :: [(Type, Type)]
tys
  = SDoc -> Type -> [(Type, Type)] -> LintM Type
lint_app (String -> SDoc
text "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 n :: Integer
n)
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= 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 "Negative type literal:" SDoc -> SDoc -> SDoc
<+> Integer -> SDoc
integer Integer
n
lintTyLit (StrTyLit _) = () -> 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 doc :: SDoc
doc kfn :: Type
kfn kas :: [(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 TyCoRep
         ; (Type -> (Type, Type) -> LintM Type)
-> Type -> [(Type, Type)] -> LintM Type
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m a) -> a -> [b] -> m a
foldlM (InScopeSet -> Type -> (Type, Type) -> LintM Type
go_app InScopeSet
in_scope) Type
kfn [(Type, Type)]
kas }
  where
    fail_msg :: SDoc -> SDoc
fail_msg extra :: SDoc
extra = [SDoc] -> SDoc
vcat [ SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Kind application error in") 2 SDoc
doc
                          , Int -> SDoc -> SDoc
nest 2 (String -> SDoc
text "Function kind =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
kfn)
                          , Int -> SDoc -> SDoc
nest 2 (String -> SDoc
text "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 in_scope :: InScopeSet
in_scope kfn :: Type
kfn tka :: (Type, Type)
tka
      | Just kfn' :: 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 _ (FunTy kfa :: Type
kfa kfb :: Type
kfb) tka :: (Type, Type)
tka@(_,ka :: 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 "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 in_scope :: InScopeSet
in_scope (ForAllTy (Bndr kv :: Var
kv _vis :: ArgFlag
_vis) kfn :: Type
kfn) tka :: (Type, Type)
tka@(ta :: Type
ta,ka :: 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 "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 _ kfn :: Type
kfn ka :: (Type, Type)
ka
       = SDoc -> LintM Type
forall a. SDoc -> LintM a
failWithL (SDoc -> SDoc
fail_msg (String -> SDoc
text "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 _ _ (BuiltinRule {})
  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- Don't bother

lintCoreRule fun :: Var
fun fun_ty :: Type
fun_ty rule :: CoreRule
rule@(Rule { ru_name :: CoreRule -> RuleName
ru_name = RuleName
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
$ \ _ ->
    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 join_arity :: 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 }
                     _ -> 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 "lhs type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
lhs_ty
                            , String -> SDoc
text "rhs type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs_ty
                            , String -> SDoc
text "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 "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 "Rule" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
doubleQuotes (RuleName -> SDoc
ftext RuleName
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 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
Trac #10602, SpecConstr stupidly constructed a rule like

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

But simplExpr collapses those coercions into one.  (Indeed in
Trac #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 (Trac #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 co :: 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 g :: Coercion
g
  = do { (k1 :: Type
k1, k2 :: Type
k2, t1 :: Type
t1, t2 :: Type
t2, r :: Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
g
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k1 (String -> SDoc
text "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 "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 ty :: 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 r :: Role
r ty :: Type
ty 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 r :: Role
r ty :: Type
ty (MCo co :: Coercion
co))
  = do { Type
k <- Type -> LintM Type
lintType Type
ty
       ; (_, _, k1 :: Type
k1, k2 :: Type
k2, r' :: 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 "GRefl coercion kind mis-match:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
                   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 r :: Role
r tc :: TyCon
tc cos :: [Coercion]
cos)
  | TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
funTyConKey
  , [_rep1 :: Coercion
_rep1,_rep2 :: Coercion
_rep2,_co1 :: Coercion
_co1,_co2 :: Coercion
_co2] <- [Coercion]
cos
  = do { SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text "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 "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
       ; (k's :: [Type]
k's, ks :: [Type]
ks, ss :: [Type]
ss, ts :: [Type]
ts, rs :: [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 co1 :: Coercion
co1 co2 :: Coercion
co2)
  | TyConAppCo {} <- Coercion
co1
  = SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text "TyConAppCo to the left of AppCo:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
  | Just (TyConApp {}, _) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co1
  = SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text "Refl (TyConApp ...) to the left of AppCo:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
  | Bool
otherwise
  = do { (k1 :: Type
k1,  k2 :: Type
k2,  s1 :: Type
s1, s2 :: Type
s2, r1 :: Role
r1) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co1
       ; (k'1 :: Type
k'1, k'2 :: Type
k'2, t1 :: Type
t1, t2 :: Type
t2, r2 :: 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 "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 tv1 :: Var
tv1 kind_co :: Coercion
kind_co co :: Coercion
co)
  -- forall over types
  | Var -> Bool
isTyVar Var
tv1
  = do { (_, k2 :: 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 {
       ; (k3 :: Type
k3, k4 :: Type
k4, t1 :: Type
t1, t2 :: Type
t2, r :: 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]
                     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 cv1 :: Var
cv1 kind_co :: Coercion
kind_co 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 "Covar can only appear in Refl and GRefl: " SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
       ; (_, k2 :: 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 {
       ; (k3 :: Type
k3, k4 :: Type
k4, t1 :: Type
t1, t2 :: Type
t2, r :: Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; Type -> SDoc -> LintM ()
checkValueKind Type
k3 (String -> SDoc
text "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 "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 2 Coercion
kind_co'
             eta2 :: Coercion
eta2  = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r2 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]
                     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 r :: Role
r co1 :: Coercion
co1 co2 :: Coercion
co2)
  = do { (k1 :: Type
k1,k'1 :: Type
k'1,s1 :: Type
s1,t1 :: Type
t1,r1 :: Role
r1) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co1
       ; (k2 :: Type
k2,k'2 :: Type
k'2,s2 :: Type
s2,t2 :: Type
t2,r2 :: Role
r2) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co2
       ; Type
k <- SDoc -> Type -> Type -> LintM Type
lintArrow (String -> SDoc
text "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 "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
mkFunTy Type
s1 Type
s2, Type -> Type -> Type
mkFunTy Type
t1 Type
t2, Role
r) }

lintCoercion (CoVarCo cv :: 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 "Bad CoVarCo:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
cv)
                  2 (String -> SDoc
text "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 prov :: UnivCoProvenance
prov r :: Role
r ty1 :: Type
ty1 ty2 :: Type
ty2)
  = do { Type
k1 <- Type -> LintM Type
lintType Type
ty1
       ; Type
k2 <- Type -> LintM Type
lintType Type
ty2
       ; case UnivCoProvenance
prov of
           UnsafeCoerceProv -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- no extra checks

           PhantomProv kco :: 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 kco :: 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 _     -> () -> 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 s :: String
s = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text (String -> SDoc) -> String -> SDoc
forall a b. (a -> b) -> a -> b
$ "Unsafe coercion: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
                     2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text "From:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1
                             , String -> SDoc
text "  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 t1 :: Type
t1 t2 :: Type
t2
       = do { Bool -> SDoc -> LintM ()
checkWarnL (Bool -> Bool
not Bool
lev_poly1)
                         (String -> SDoc
report "left-hand type is levity-polymorphic")
            ; Bool -> SDoc -> LintM ()
checkWarnL (Bool -> Bool
not Bool
lev_poly2)
                         (String -> SDoc
report "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 "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 rep1 :: PrimRep
rep1 rep2 :: 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 "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 "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
                Nothing    -> SDoc -> LintM ()
addWarnL (String -> SDoc
report "between vector types")
                Just False -> SDoc -> LintM ()
addWarnL (String -> SDoc
report "between float and integral values")
                _          -> () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
            }

     check_kinds :: Coercion -> Type -> Type -> LintM ()
check_kinds kco :: Coercion
kco k1 :: Type
k1 k2 :: Type
k2 = do { (k1' :: Type
k1', k2' :: 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 co :: Coercion
co)
  = do { (k1 :: Type
k1, k2 :: Type
k2, ty1 :: Type
ty1, ty2 :: Type
ty2, r :: 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 co1 :: Coercion
co1 co2 :: Coercion
co2)
  = do { (k1a :: Type
k1a, _k1b :: Type
_k1b, ty1a :: Type
ty1a, ty1b :: Type
ty1b, r1 :: Role
r1) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co1
       ; (_k2a :: Type
_k2a, k2b :: Type
k2b, ty2a :: Type
ty2a, ty2b :: Type
ty2b, r2 :: 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 "Trans coercion mis-match:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
                   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 r0 :: Role
r0 n :: Int
n co :: Coercion
co)
  = do { (_, _, s :: Type
s, t :: Type
t, r :: 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 (tcv_s :: Var
tcv_s, _ty_s :: Type
_ty_s), Just (tcv_t :: Var
tcv_t, _ty_t :: Type
_ty_t))
             -- works for both tyvar and covar
             | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 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

         ; _ -> 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 (tc_s :: TyCon
tc_s, tys_s :: [Type]
tys_s), Just (tc_t :: TyCon
tc_t, tys_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

         ; _ -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Bad getNth:")
                              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 lr :: LeftOrRight
lr co :: Coercion
co)
  = do { (_,_,s :: Type
s,t :: Type
t,r :: 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 s_pr :: (Type, Type)
s_pr, Just t_pr :: (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

           _ -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Bad LRCo:")
                              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 co :: Coercion
co arg :: Coercion
arg)
  = do { (k3 :: Type
k3, k4 :: Type
k4, t1' :: Type
t1',t2' :: Type
t2', r :: Role
r) <- Coercion -> LintM (Type, Type, Type, Type, Role)
lintCoercion Coercion
co
       ; (k1' :: Type
k1',k2' :: Type
k2',s1 :: Type
s1,s2 :: Type
s2, r' :: 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 (tv1 :: Var
tv1,t1 :: Type
t1), Just (tv2 :: Var
tv2,t2 :: 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 "Kind mis-match in inst coercion")
         ; _ -> case (Type -> Maybe (Var, Type)
splitForAllTy_co_maybe Type
t1', Type -> Maybe (Var, Type)
splitForAllTy_co_maybe Type
t2') of
         -- forall over covar
         { (Just (cv1 :: Var
cv1, t1 :: Type
t1), Just (cv2 :: Var
cv2, t2 :: 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 s1' :: Coercion
s1' <- Type
s1
             , CoercionTy s2' :: 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 "Kind mis-match in inst coercion")
         ; _ -> SDoc -> LintM (Type, Type, Type, Type, Role)
forall a. SDoc -> LintM a
failWithL (String -> SDoc
text "Bad argument of inst") }}}

lintCoercion co :: Coercion
co@(AxiomInstCo con :: CoAxiom Branched
con ind :: Int
ind cos :: [Coercion]
cos)
  = do { Bool -> LintM () -> LintM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (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 "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 "lengths")
       ; TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; let empty_subst :: TCvSubst
empty_subst = TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst
       ; (subst_l :: TCvSubst
subst_l, subst_r :: TCvSubst
subst_r) <- ((TCvSubst, TCvSubst)
 -> (Var, Role, Coercion) -> LintM (TCvSubst, TCvSubst))
-> (TCvSubst, TCvSubst)
-> [(Var, Role, Coercion)]
-> LintM (TCvSubst, TCvSubst)
forall (m :: * -> *) a b.
Monad m =>
(a -> b -> m a) -> a -> [b] -> m a
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 bad_branch :: CoAxBranch
bad_branch -> SDoc -> LintM ()
bad_ax (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "inconsistent with" SDoc -> SDoc -> SDoc
<+>
                                       TyCon -> CoAxBranch -> SDoc
pprCoAxBranch TyCon
fam_tc CoAxBranch
bad_branch
           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 what :: SDoc
what = SDoc -> LintM ()
addErrL (SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text  "Bad axiom application" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
parens SDoc
what)
                        2 (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co))

    check_ki :: (TCvSubst, TCvSubst)
-> (Var, Role, Coercion) -> LintM (TCvSubst, TCvSubst)
check_ki (subst_l :: TCvSubst
subst_l, subst_r :: TCvSubst
subst_r) (ktv :: Var
ktv, role :: Role
role, arg :: Coercion
arg)
      = do { (k' :: Type
k', k'' :: Type
k'', s' :: Type
s', t' :: Type
t', r :: 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 "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 "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 co :: Coercion
co)
  = do { (k1 :: Type
k1, k2 :: Type
k2, _, _, _) <- 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 co' :: Coercion
co')
  = do { (k1 :: Type
k1,k2 :: Type
k2,s :: Type
s,t :: Type
t,r :: 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 co :: CoAxiomRule
co cs :: [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 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 | (_,_,l :: Type
l,r :: Type
r,_) <- [(Type, Type, Type, Type, Role)]
eqs ] of
           Nothing -> String -> [SDoc] -> LintM (Type, Type, Type, Type, Role)
forall a. String -> [SDoc] -> LintM a
err "Malformed use of AxiomRuleCo" [ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
this ]
           Just (Pair l :: Type
l r :: 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 m :: String
m xs :: [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) 2 (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat (String -> SDoc
text "Rule:" SDoc -> SDoc -> SDoc
<+> RuleName -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoAxiomRule -> RuleName
coaxrName CoAxiomRule
co) SDoc -> [SDoc] -> [SDoc]
forall a. a -> [a] -> [a]
: [SDoc]
xs)

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

lintCoercion (HoleCo h :: CoercionHole
h)
  = do { SDoc -> LintM ()
addErrL (SDoc -> LintM ()) -> SDoc -> LintM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc
text "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 cv :: 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 "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 ->           -- Error and warning messages so far
            (Maybe a, WarnsAndErrs) } -- Result and messages (if any)

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 Trac #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 (Trac #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 Functor LintM where
      fmap :: (a -> b) -> LintM a -> LintM b
fmap = (a -> b) -> LintM a -> LintM b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Applicative LintM where
      pure :: a -> LintM a
pure x :: 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
$ \ _ errs :: (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
  m :: LintM a
m >>= :: LintM a -> (a -> LintM b) -> LintM b
>>= k :: 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 (\ env :: LintEnv
env errs :: (Bag SDoc, Bag SDoc)
errs ->
                       let (res :: Maybe a
res, errs' :: (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 r :: 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'
                           Nothing -> (Maybe b
forall a. Maybe a
Nothing, (Bag SDoc, Bag SDoc)
errs'))

instance MonadFail.MonadFail LintM where
    fail :: String -> LintM a
fail err :: 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 (\ e :: LintEnv
e errs :: (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
  | 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    -- Errors and warnings
initL :: DynFlags
-> LintFlags -> InScopeSet -> LintM a -> (Bag SDoc, Bag SDoc)
initL dflags :: DynFlags
dflags flags :: LintFlags
flags in_scope :: InScopeSet
in_scope m :: 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
      (_, errs :: (Bag SDoc, Bag SDoc)
errs) -> (Bag SDoc, Bag SDoc)
errs
  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 ru :: Bool
ru thing_inside :: 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
$ \ env :: LintEnv
env errs :: (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
$ \ env :: LintEnv
env errs :: (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 True  _   = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkL False msg :: 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 True   _  = () -> LintM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
checkWarnL False msg :: SDoc
msg = SDoc -> LintM ()
addWarnL SDoc
msg

failWithL :: MsgDoc -> LintM a
failWithL :: SDoc -> LintM a
failWithL msg :: 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
$ \ env :: LintEnv
env (warns :: Bag SDoc
warns,errs :: Bag SDoc
errs) ->
                (Maybe a
forall a. Maybe a
Nothing, (Bag SDoc
warns, LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg LintEnv
env Bag SDoc
errs SDoc
msg))

addErrL :: MsgDoc -> LintM ()
addErrL :: SDoc -> LintM ()
addErrL msg :: 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
$ \ env :: LintEnv
env (warns :: Bag SDoc
warns,errs :: Bag SDoc
errs) ->
              (() -> Maybe ()
forall a. a -> Maybe a
Just (), (Bag SDoc
warns, LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg LintEnv
env Bag SDoc
errs SDoc
msg))

addWarnL :: MsgDoc -> LintM ()
addWarnL :: SDoc -> LintM ()
addWarnL msg :: 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
$ \ env :: LintEnv
env (warns :: Bag SDoc
warns,errs :: Bag SDoc
errs) ->
              (() -> Maybe ()
forall a. a -> Maybe a
Just (), (LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg LintEnv
env Bag SDoc
warns SDoc
msg, Bag SDoc
errs))

addMsg :: LintEnv ->  Bag MsgDoc -> MsgDoc -> Bag MsgDoc
addMsg :: LintEnv -> Bag SDoc -> SDoc -> Bag SDoc
addMsg env :: LintEnv
env msgs :: Bag SDoc
msgs msg :: SDoc
msg
  = ASSERT( notNull locs )
    Bag SDoc
msgs Bag SDoc -> SDoc -> Bag SDoc
forall a. Bag a -> a -> Bag a
`snocBag` SDoc -> SDoc
mk_msg SDoc
msg
  where
   locs :: [LintLocInfo]
locs = LintEnv -> [LintLocInfo]
le_loc LintEnv
env
   (loc :: SrcLoc
loc, cxt1 :: SDoc
cxt1) = LintLocInfo -> (SrcLoc, SDoc)
dumpLoc ([LintLocInfo] -> LintLocInfo
forall a. [a] -> a
head [LintLocInfo]
locs)
   cxts :: [SDoc]
cxts        = [(SrcLoc, SDoc) -> SDoc
forall a b. (a, b) -> b
snd (LintLocInfo -> (SrcLoc, SDoc)
dumpLoc LintLocInfo
loc) | LintLocInfo
loc <- [LintLocInfo]
locs]
   context :: SDoc
context     = SDoc -> SDoc -> SDoc
ifPprDebug ([SDoc] -> SDoc
vcat ([SDoc] -> [SDoc]
forall a. [a] -> [a]
reverse [SDoc]
cxts) SDoc -> SDoc -> SDoc
$$ SDoc
cxt1 SDoc -> SDoc -> SDoc
$$
                             String -> SDoc
text "Substitution:" SDoc -> SDoc -> SDoc
<+> TCvSubst -> SDoc
forall a. Outputable a => a -> SDoc
ppr (LintEnv -> TCvSubst
le_subst LintEnv
env))
                            SDoc
cxt1

   mk_msg :: SDoc -> SDoc
mk_msg msg :: SDoc
msg = Severity -> SrcSpan -> SDoc -> SDoc
mkLocMessage Severity
SevWarning (SrcLoc -> SrcLoc -> SrcSpan
mkSrcSpan SrcLoc
loc SrcLoc
loc) (SDoc
context SDoc -> SDoc -> SDoc
$$ SDoc
msg)

addLoc :: LintLocInfo -> LintM a -> LintM a
addLoc :: LintLocInfo -> LintM a -> LintM a
addLoc extra_loc :: LintLocInfo
extra_loc m :: 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
$ \ env :: LintEnv
env errs :: (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
$ \ env :: LintEnv
env errs :: (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 {} : _ }) = Bool
True
    is_case_pat _other :: LintEnv
_other                           = Bool
False

addInScopeVar :: Var -> LintM a -> LintM a
addInScopeVar :: Var -> LintM a -> LintM a
addInScopeVar var :: Var
var m :: 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
$ \ env :: LintEnv
env errs :: (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 tv :: Var
tv ty :: Type
ty m :: 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
$ \ env :: LintEnv
env errs :: (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 subst' :: TCvSubst
subst' m :: 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
$ \ env :: LintEnv
env errs :: (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 m :: 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
$ \ env :: LintEnv
env errs :: (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 True  m :: LintM a
m = LintM a -> LintM a
forall a. LintM a -> LintM a
markAllJoinsBad LintM a
m
markAllJoinsBadIf False m :: LintM a
m = LintM a
m

addGoodJoins :: [Var] -> LintM a -> LintM a
addGoodJoins :: [Var] -> LintM a -> LintM a
addGoodJoins vars :: [Var]
vars thing_inside :: 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
$ \ env :: LintEnv
env errs :: (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 env :: 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 (\ env :: LintEnv
env errs :: (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 (\ env :: LintEnv
env errs :: (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 (\ env :: LintEnv
env errs :: (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 ty :: 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 co :: 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 id_occ :: 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 id_bnd :: 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 }
           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 "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 "Occurrence is GlobalId, but binding is LocalId")
                            2 (BindingSite -> Var -> SDoc
forall a. OutputableBndr a => BindingSite -> a -> SDoc
pprBndr BindingSite
LetBind Var
id_occ)
    bad_global :: Var -> Bool
bad_global id_bnd :: 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 id :: Var
id
  = do { VarSet
join_set <- LintM VarSet
getValidJoins
       ; case VarSet -> Var -> Maybe Var
lookupVarSet VarSet
join_set Var
id of
            Just id' :: Var
id' -> Maybe Int -> LintM (Maybe Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Var -> Maybe Int
isJoinId_maybe Var
id')
            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
var
  = do { TCvSubst
subst <- LintM TCvSubst
getTCvSubst
       ; Bool -> SDoc -> LintM ()
lintL (Var
var Var -> TCvSubst -> Bool
`isInScope` TCvSubst
subst)
               (BindingSite -> Var -> SDoc
forall a. OutputableBndr a => BindingSite -> a -> SDoc
pprBndr BindingSite
LetBind Var
var SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "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 ty1 :: Type
ty1 ty2 :: Type
ty2 msg :: 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 co :: thing
co r1 :: Role
r1 r2 :: Role
r2
  = Bool -> SDoc -> LintM ()
lintL (Role
r1 Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
r2)
          (String -> SDoc
text "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 "got" SDoc -> SDoc -> SDoc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r2 SDoc -> SDoc -> SDoc
$$
           String -> SDoc
text "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 v :: Var
v)
  = (Var -> SrcLoc
forall a. NamedThing a => a -> SrcLoc
getSrcLoc Var
v, SDoc -> SDoc
brackets (String -> SDoc
text "RHS of" SDoc -> SDoc -> SDoc
<+> [Var] -> SDoc
pp_binders [Var
v]))

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

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

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

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

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

dumpLoc (CaseAlt (con :: AltCon
con, args :: [Var]
args, _))
  = (SrcLoc
noSrcLoc, String -> SDoc
text "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 (con :: AltCon
con, args :: [Var]
args, _))
  = (SrcLoc
noSrcLoc, String -> SDoc
text "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 (ImportedUnfolding locn :: SrcLoc
locn)
  = (SrcLoc
locn, SDoc -> SDoc
brackets (String -> SDoc
text "in an imported unfolding"))
dumpLoc TopLevelBindings
  = (SrcLoc
noSrcLoc, SDoc
Outputable.empty)
dumpLoc (InType ty :: Type
ty)
  = (SrcLoc
noSrcLoc, String -> SDoc
text "In the type" SDoc -> SDoc -> SDoc
<+> SDoc -> SDoc
quotes (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty))
dumpLoc (InCo co :: Coercion
co)
  = (SrcLoc
noSrcLoc, String -> SDoc
text "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 bs :: [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 b :: 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 args :: [Var]
args
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "DEFAULT case with binders")
         4 ([Var] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [Var]
args)

mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
mkCaseAltMsg :: CoreExpr -> Type -> Type -> SDoc
mkCaseAltMsg e :: CoreExpr
e ty1 :: Type
ty1 ty2 :: Type
ty2
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Type of case alternatives not the same as the annotation on case:")
         4 ([SDoc] -> SDoc
vcat [ String -> SDoc
text "Actual type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1,
                   String -> SDoc
text "Annotation on case:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2,
                   String -> SDoc
text "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
var var_ty :: Type
var_ty scrut_ty :: Type
scrut_ty subst :: TCvSubst
subst
  = [SDoc] -> SDoc
vcat [String -> SDoc
text "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 "Result binder type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
var_ty,--(idType var),
          String -> SDoc
text "Scrutinee type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
scrut_ty,
     [SDoc] -> SDoc
hsep [String -> SDoc
text "Current TCv subst", TCvSubst -> SDoc
forall a. Outputable a => a -> SDoc
ppr TCvSubst
subst]]

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

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

mkBadConMsg :: TyCon -> DataCon -> MsgDoc
mkBadConMsg :: TyCon -> DataCon -> SDoc
mkBadConMsg tycon :: TyCon
tycon datacon :: DataCon
datacon
  = [SDoc] -> SDoc
vcat [
        String -> SDoc
text "In a case alternative, data constructor isn't in scrutinee type:",
        String -> SDoc
text "Scrutinee type constructor:" SDoc -> SDoc -> SDoc
<+> TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tycon,
        String -> SDoc
text "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 con_result_ty :: Type
con_result_ty scrut_ty :: Type
scrut_ty
  = [SDoc] -> SDoc
vcat [
        String -> SDoc
text "In a case alternative, pattern result type doesn't match scrutinee type:",
        String -> SDoc
text "Pattern result type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
con_result_ty,
        String -> SDoc
text "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 "In a LitAlt, the literal is lifted (probably Integer)"

mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
mkBadAltMsg :: Type -> Alt Var -> SDoc
mkBadAltMsg scrut_ty :: Type
scrut_ty alt :: Alt Var
alt
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Data alternative when scrutinee is not a tycon application",
           String -> SDoc
text "Scrutinee type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
scrut_ty,
           String -> SDoc
text "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 scrut_ty :: Type
scrut_ty alt :: Alt Var
alt
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Data alternative for newtype datacon",
           String -> SDoc
text "Scrutinee type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
scrut_ty,
           String -> SDoc
text "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 fun_ty :: Type
fun_ty arg_ty :: Type
arg_ty arg :: CoreExpr
arg
  = [SDoc] -> SDoc
vcat [String -> SDoc
text "Argument value doesn't match argument type:",
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Fun type:") 4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
fun_ty),
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Arg type:") 4 (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
arg_ty),
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Arg:") 4 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
arg)]

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

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

mkTyAppMsg :: Type -> Type -> MsgDoc
mkTyAppMsg :: Type -> Type -> SDoc
mkTyAppMsg ty :: Type
ty arg_ty :: Type
arg_ty
  = [SDoc] -> SDoc
vcat [String -> SDoc
text "Illegal type application:",
              SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Exp type:")
                 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 "Arg type:")
                 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 e :: CoreExpr
e = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Empty Rec binding:") 2 (CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
e)

mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
mkRhsMsg :: Var -> SDoc -> Type -> SDoc
mkRhsMsg binder :: Var
binder what :: SDoc
what ty :: Type
ty
  = [SDoc] -> SDoc
vcat
    [[SDoc] -> SDoc
hsep [String -> SDoc
text "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 "Binder's type:", Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Var -> Type
idType Var
binder)],
     [SDoc] -> SDoc
hsep [String -> SDoc
text "Rhs type:", Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty]]

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

badBndrTyMsg :: Id -> SDoc -> MsgDoc
badBndrTyMsg :: Var -> SDoc -> SDoc
badBndrTyMsg binder :: Var
binder what :: SDoc
what
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "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 "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 binder :: Var
binder
  = [SDoc] -> SDoc
vcat [[SDoc] -> SDoc
hsep [String -> SDoc
text "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 "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 binder :: Var
binder
  = [SDoc] -> SDoc
hsep [String -> SDoc
text "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 binder :: Var
binder
  = [SDoc] -> SDoc
hsep [String -> SDoc
text "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 binder :: Var
binder
  = [SDoc] -> SDoc
hsep [String -> SDoc
text "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 tyvar :: Var
tyvar arg_ty :: Type
arg_ty
  = [SDoc] -> SDoc
vcat [String -> SDoc
text "Kinds don't match in type application:",
          SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Type variable:")
                 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 "Arg type:")
                 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))]

{- Not needed now
mkArityMsg :: Id -> MsgDoc
mkArityMsg binder
  = vcat [hsep [text "Demand type has",
                ppr (dmdTypeDepth dmd_ty),
                text "arguments, rhs has",
                ppr (idArity binder),
                text "arguments,",
                ppr binder],
              hsep [text "Binder's strictness signature:", ppr dmd_ty]

         ]
           where (StrictSig dmd_ty) = idStrictness binder
-}
mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> SDoc
mkCastErr expr :: CoreExpr
expr = String -> String -> SDoc -> Coercion -> Type -> Type -> SDoc
mk_cast_err "expression" "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 ty :: Type
ty = String -> String -> SDoc -> Coercion -> Type -> Type -> SDoc
mk_cast_err "type" "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 thing_str :: String
thing_str co_str :: String
co_str pp_thing :: SDoc
pp_thing co :: Coercion
co from_ty :: Type
from_ty thing_ty :: Type
thing_ty
  = [SDoc] -> SDoc
vcat [SDoc
from_msg SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "of Cast differs from" SDoc -> SDoc -> SDoc
<+> SDoc
co_msg
            SDoc -> SDoc -> SDoc
<+> String -> SDoc
text "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 "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 "Actual" SDoc -> SDoc -> SDoc
<+> SDoc
enclosed_msg SDoc -> SDoc -> SDoc
<> SDoc
colon SDoc -> SDoc -> SDoc
<+> SDoc
pp_thing,
          String -> SDoc
text "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 "From-" SDoc -> SDoc -> SDoc
<> SDoc
co_msg
    enclosed_msg :: SDoc
enclosed_msg = String -> SDoc
text "enclosed" SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
thing_str

mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
mkBadUnivCoMsg :: LeftOrRight -> Coercion -> SDoc
mkBadUnivCoMsg lr :: LeftOrRight
lr co :: Coercion
co
  = String -> SDoc
text "Kind mismatch on the" SDoc -> SDoc -> SDoc
<+> LeftOrRight -> SDoc
pprLeftOrRight LeftOrRight
lr SDoc -> SDoc -> SDoc
<+>
    String -> SDoc
text "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 ty :: Type
ty co :: Coercion
co
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Found a non-coercion in a proof-irrelevance UnivCo:")
       2 ([SDoc] -> SDoc
vcat [ String -> SDoc
text "type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty
               , String -> SDoc
text "co:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co ])

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

mkInvalidJoinPointMsg :: Var -> Type -> SDoc
mkInvalidJoinPointMsg :: Var -> Type -> SDoc
mkInvalidJoinPointMsg var :: Var
var ty :: Type
ty
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Join point has invalid type:")
        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
var ar :: Int
ar nlams :: Int
nlams rhs :: CoreExpr
rhs
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Join point has too few lambdas",
           String -> SDoc
text "Join var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var,
           String -> SDoc
text "Join arity:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
ar,
           String -> SDoc
text "Number of lambdas:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
nlams,
           String -> SDoc
text "Rhs = " SDoc -> SDoc -> SDoc
<+> CoreExpr -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreExpr
rhs
           ]

invalidJoinOcc :: Var -> SDoc
invalidJoinOcc :: Var -> SDoc
invalidJoinOcc var :: Var
var
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Invalid occurrence of a join variable:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var
         , String -> SDoc
text "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
var ar :: Int
ar nargs :: Int
nargs
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Join point invoked with wrong number of arguments",
           String -> SDoc
text "Join var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
var,
           String -> SDoc
text "Join arity:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
ar,
           String -> SDoc
text "Number of arguments:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
int Int
nargs ]

mkInconsistentRecMsg :: [Var] -> SDoc
mkInconsistentRecMsg :: [Var] -> SDoc
mkInconsistentRecMsg bndrs :: [Var]
bndrs
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Recursive let binders mix values and join points",
           String -> SDoc
text "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 bndr :: 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 bndr :: Var
bndr join_arity_bndr :: Int
join_arity_bndr join_arity_occ :: Int
join_arity_occ
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Mismatch in join point arity between binder and occurrence"
         , String -> SDoc
text "Var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr
         , String -> SDoc
text "Arity at binding site:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
join_arity_bndr
         , String -> SDoc
text "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 bndr :: Var
bndr var :: Var
var bndr_ty :: Type
bndr_ty var_ty :: Type
var_ty
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Mismatch in type between binder and occurrence"
         , String -> SDoc
text "Var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr
         , String -> SDoc
text "Binder type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
bndr_ty
         , String -> SDoc
text "Occurrence type:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
var_ty
         , String -> SDoc
text "  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 bndr :: Var
bndr join_arity :: Int
join_arity rule :: CoreRule
rule
  = [SDoc] -> SDoc
vcat [ String -> SDoc
text "Join point has rule with wrong number of arguments"
         , String -> SDoc
text "Var:" SDoc -> SDoc -> SDoc
<+> Var -> SDoc
forall a. Outputable a => a -> SDoc
ppr Var
bndr
         , String -> SDoc
text "Join arity:" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
join_arity
         , String -> SDoc
text "Rule:" SDoc -> SDoc -> SDoc
<+> CoreRule -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoreRule
rule ]

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

dupVars :: [NonEmpty Var] -> MsgDoc
dupVars :: [NonEmpty Var] -> SDoc
dupVars vars :: [NonEmpty Var]
vars
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Duplicate variables brought into scope")
       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 vars :: [NonEmpty Name]
vars
  = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text "Duplicate top-level variables with the same qualified name")
       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 pname :: SDoc
pname pass :: ModGuts -> CoreM ModGuts
pass guts :: 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 "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 "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 "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'
        (diffs :: [SDoc]
diffs,_) = 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 "warning" SDoc
pname
      , String -> SDoc
text "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 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 pass :: ModGuts -> CoreM ModGuts
pass guts :: ModGuts
guts = do
  -- Remove debug flag from environment.
  DynFlags
dflags <- CoreM DynFlags
forall (m :: * -> *). HasDynFlags m => m DynFlags
getDynFlags
  let removeFlag :: HscEnv -> HscEnv
removeFlag env :: HscEnv
env = HscEnv
env{ hsc_dflags :: DynFlags
hsc_dflags = DynFlags
dflags{ debugLevel :: Int
debugLevel = 0} }
      withoutFlag :: CoreM a -> CoreM (a, SimplCount)
withoutFlag corem :: CoreM a
corem =
        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
-> UniqSupply
-> Module
-> ModuleSet
-> PrintUnqualified
-> SrcSpan
-> CoreM a
-> IO (a, SimplCount)
forall a.
HscEnv
-> RuleBase
-> UniqSupply
-> Module
-> ModuleSet
-> PrintUnqualified
-> SrcSpan
-> CoreM a
-> IO (a, SimplCount)
runCoreM (HscEnv
 -> RuleBase
 -> UniqSupply
 -> Module
 -> ModuleSet
 -> PrintUnqualified
 -> SrcSpan
 -> CoreM a
 -> IO (a, SimplCount))
-> CoreM HscEnv
-> CoreM
     (RuleBase
      -> UniqSupply
      -> 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
   -> UniqSupply
   -> Module
   -> ModuleSet
   -> PrintUnqualified
   -> SrcSpan
   -> CoreM a
   -> IO (a, SimplCount))
-> CoreM RuleBase
-> CoreM
     (UniqSupply
      -> 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
  (UniqSupply
   -> Module
   -> ModuleSet
   -> PrintUnqualified
   -> SrcSpan
   -> CoreM a
   -> IO (a, SimplCount))
-> CoreM UniqSupply
-> CoreM
     (Module
      -> ModuleSet
      -> PrintUnqualified
      -> SrcSpan
      -> CoreM a
      -> IO (a, SimplCount))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*>
                                CoreM UniqSupply
forall (m :: * -> *). MonadUnique m => m UniqSupply
getUniqueSupplyM 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 :: Bind Var
bind = case Bind Var
bind of
        Rec bs :: [(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 (\(b :: Var
b,e :: CoreExpr
e) -> (Var
b, CoreExpr -> CoreExpr
forall b. Expr b -> Expr b
nukeTicks CoreExpr
e)) [(Var, CoreExpr)]
bs
        NonRec b :: Var
b e :: 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)