Lint.hs 113 KB
Newer Older
Austin Seipp's avatar
Austin Seipp committed
1 2 3
{-
(c) The University of Glasgow 2006
(c) The GRASP/AQUA Project, Glasgow University, 1993-1998
4

Simon Marlow's avatar
Simon Marlow committed
5

6 7
A ``lint'' pass to check for Core correctness.
See Note [Core Lint guarantee].
Austin Seipp's avatar
Austin Seipp committed
8
-}
9

10
{-# LANGUAGE CPP #-}
11
{-# LANGUAGE DeriveFunctor #-}
Ian Lynagh's avatar
Ian Lynagh committed
12

Sylvain Henry's avatar
Sylvain Henry committed
13
module GHC.Core.Lint (
14
    lintCoreBindings, lintUnfolding,
15
    lintPassResult, lintInteractiveExpr, lintExpr,
Ryan Scott's avatar
Ryan Scott committed
16
    lintAnnots, lintTypes,
17 18

    -- ** Debug output
19
    endPass, endPassIO,
20
    dumpPassResult,
Sylvain Henry's avatar
Sylvain Henry committed
21
    GHC.Core.Lint.dumpIfSet,
22
 ) where
23

24
#include "HsVersions.h"
25

26 27
import GhcPrelude

Sylvain Henry's avatar
Sylvain Henry committed
28 29 30 31
import GHC.Core
import GHC.Core.FVs
import GHC.Core.Utils
import GHC.Core.Stats ( coreBindsStats )
32
import GHC.Core.Op.Monad
33
import Bag
Simon Marlow's avatar
Simon Marlow committed
34
import Literal
Sylvain Henry's avatar
Sylvain Henry committed
35
import GHC.Core.DataCon
Simon Marlow's avatar
Simon Marlow committed
36
import TysWiredIn
37
import TysPrim
Ben Gamari's avatar
Ben Gamari committed
38
import TcType ( isFloatingTy )
Simon Marlow's avatar
Simon Marlow committed
39 40
import Var
import VarEnv
41
import VarSet
Simon Peyton Jones's avatar
Simon Peyton Jones committed
42
import UniqSet( nonDetEltsUniqSet )
Simon Marlow's avatar
Simon Marlow committed
43
import Name
44
import Id
lukemaurer's avatar
lukemaurer committed
45
import IdInfo
Sylvain Henry's avatar
Sylvain Henry committed
46
import GHC.Core.Ppr
Simon Marlow's avatar
Simon Marlow committed
47
import ErrUtils
Sylvain Henry's avatar
Sylvain Henry committed
48
import GHC.Core.Coercion
Simon Marlow's avatar
Simon Marlow committed
49
import SrcLoc
Sylvain Henry's avatar
Sylvain Henry committed
50
import GHC.Core.Type as Type
51
import GHC.Types.RepType
Sylvain Henry's avatar
Sylvain Henry committed
52 53 54 55 56 57
import GHC.Core.TyCo.Rep   -- checks validity of types/coercions
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr ( pprTyVar )
import GHC.Core.TyCon as TyCon
import GHC.Core.Coercion.Axiom
Simon Marlow's avatar
Simon Marlow committed
58
import BasicTypes
59
import ErrUtils as Err
60
import ListSetOps
61
import PrelNames
62
import Outputable
63
import FastString
64
import Util
Sylvain Henry's avatar
Sylvain Henry committed
65 66 67
import GHC.Core.InstEnv      ( instanceDFunId )
import GHC.Core.Coercion.Opt ( checkAxInstCo )
import GHC.Core.Arity        ( typeArity )
68
import Demand ( splitStrictSig, isBotDiv )
69

Sylvain Henry's avatar
Sylvain Henry committed
70 71
import GHC.Driver.Types
import GHC.Driver.Session
72
import Control.Monad
quchen's avatar
quchen committed
73
import qualified Control.Monad.Fail as MonadFail
74
import MonadUtils
75 76
import Data.Foldable      ( toList )
import Data.List.NonEmpty ( NonEmpty )
Simon Peyton Jones's avatar
Simon Peyton Jones committed
77
import Data.List          ( partition )
Simon Marlow's avatar
Simon Marlow committed
78
import Data.Maybe
79
import Pair
80
import qualified GHC.LanguageExtensions as LangExt
81

Austin Seipp's avatar
Austin Seipp committed
82
{-
83 84 85 86 87 88
Note [Core Lint guarantee]
~~~~~~~~~~~~~~~~~~~~~~~~~~
Core Lint is the type-checker for Core. Using it, we get the following guarantee:

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

However, do note point (4) above. Core Lint does not check for incomplete case-matches;
Sylvain Henry's avatar
Sylvain Henry committed
97
see Note [Case expression invariants] in GHC.Core, invariant (4). As explained there,
98 99
an incomplete case-match might slip by Core Lint and cause trouble at runtime.

100 101 102 103 104 105
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.
106
To this purpose, there is a document core-spec.pdf built in docs/core-spec that
107 108 109 110 111
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.

112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129
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.

130 131
Summary of checks
~~~~~~~~~~~~~~~~~
132 133 134 135 136 137
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
138 139 140 141
        (a) type errors
        (b) Out-of-scope type variables
        (c) Out-of-scope local variables
        (d) Ill-kinded types
142
        (e) Incorrect unsafe coercions
143 144

If we have done specialisation the we check that there are
145
        (a) No top-level bindings of primitive (unboxed type)
146 147 148 149 150

Outstanding issues:

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

156

157 158 159 160 161 162
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.

163 164
Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
165
In the desugarer, it's very very convenient to be able to say (in effect)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
166 167 168 169
        let a = Type Bool in
        let x::a = True in <body>
That is, use a type let.   See Note [Type let] in CoreSyn.
One place it is used is in mkWwArgs; see Note [Join points and beta-redexes]
170
in GHC.Core.Op.WorkWrap.Lib.  (Maybe there are other "clients" of this feature; I'm not sure).
171

Simon Peyton Jones's avatar
Simon Peyton Jones committed
172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187
* Hence 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 -> Bool]) and apply this substitution before
  comparing types. In effect, in Lint, type equality is always
  equality-moduolo-le-subst.  This is in the le_subst field of
  LintEnv.  But nota bene:

  (SI1) The le_subst substitution is applied to types and coercions only

  (SI2) The result of that substitution is used only to check for type
        equality, to check well-typed-ness, /but is then discarded/.
        The result of substittion does not outlive the CoreLint pass.

  (SI3) The InScopeSet of le_subst includes only TyVar and CoVar binders.

* The function
188
        lintInTy :: Type -> LintM (Type, Kind)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
189 190 191 192 193 194 195 196 197 198 199
  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.

* Clearly we need to clone tyvar binders as we go.

* But take care (#17590)! We must also clone CoVar binders:
    let a = TYPE (ty |> cv)
    in \cv -> blah
  blindly substituting for `a` might capture `cv`.
200

Simon Peyton Jones's avatar
Simon Peyton Jones committed
201 202 203 204 205 206
* Alas, when cloning a coercion variable we might choose a unique
  that happens to clash with an inner Id, thus
      \cv_66 -> let wild_X7 = blah in blah
  We decide to clone `cv_66` becuase it's already in scope.  Fine,
  choose a new unique.  Aha, X7 looks good.  So we check the lambda
  body with le_subst of [cv_66 :-> cv_X7]
207

Simon Peyton Jones's avatar
Simon Peyton Jones committed
208 209 210 211 212 213 214 215 216 217 218 219
  This is all fine, even though we use the same unique as wild_X7.
  As (SI2) says, we do /not/ return a new lambda
     (\cv_X7 -> let wild_X7 = blah in ...)
  We simply use the le_subst subsitution in types/coercions only, when
  checking for equality.

* We still need to check that Id occurrences are bound by some
  enclosing binding.  We do /not/ use the InScopeSet for the le_subst
  for this purpose -- it contains only TyCoVars.  Instead we have a separate
  le_ids for the in-scope Id binders.

Sigh.  We might want to explore getting rid of type-let!
220

221 222
Note [Bad unsafe coercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~
223
For discussion see https://gitlab.haskell.org/ghc/ghc/wikis/bad-unsafe-coercions
224 225 226 227 228 229 230 231 232 233 234 235 236 237 238
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.

lukemaurer's avatar
lukemaurer committed
239 240
Note [Join points]
~~~~~~~~~~~~~~~~~~
Sylvain Henry's avatar
Sylvain Henry committed
241
We check the rules listed in Note [Invariants on join points] in GHC.Core. The
lukemaurer's avatar
lukemaurer committed
242
only one that causes any difficulty is the first: All occurrences must be tail
243 244
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:
lukemaurer's avatar
lukemaurer committed
245 246 247 248 249 250 251 252

  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

253 254 255 256 257
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).
lukemaurer's avatar
lukemaurer committed
258

259 260 261 262 263 264 265
************************************************************************
*                                                                      *
                 Beginning and ending passes
*                                                                      *
************************************************************************

These functions are not CoreM monad stuff, but they probably ought to
266 267
be, and it makes a convenient place for them.  They print out stuff
before and after core passes, and do Core Lint when necessary.
Austin Seipp's avatar
Austin Seipp committed
268
-}
269

270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
endPass :: CoreToDo -> CoreProgram -> [CoreRule] -> CoreM ()
endPass pass binds rules
  = do { hsc_env <- getHscEnv
       ; print_unqual <- getPrintUnqualified
       ; liftIO $ endPassIO hsc_env print_unqual pass binds rules }

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

dumpIfSet :: DynFlags -> Bool -> CoreToDo -> SDoc -> SDoc -> IO ()
dumpIfSet dflags dump_me pass extra_info doc
  = Err.dumpIfSet dflags dump_me (showSDoc dflags (ppr pass <+> extra_info)) 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 dflags unqual mb_flag hdr extra_info binds rules
Sylvain Henry's avatar
Sylvain Henry committed
303 304 305 306
  = do { forM_ mb_flag $ \flag -> do
           let sty = mkDumpStyle dflags unqual
           dumpAction dflags sty (dumpOptionsFromFlag flag)
              (showSDoc dflags hdr) FormatCore dump_doc
307 308 309 310 311 312

         -- 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.
       ; Err.debugTraceMsg dflags 2 size_doc
       }
313 314 315 316 317 318 319

  where
    size_doc = sep [text "Result size of" <+> hdr, nest 2 (equals <+> ppr (coreBindsStats binds))]

    dump_doc  = vcat [ nest 2 extra_info
                     , size_doc
                     , blankLine
320
                     , pprCoreBindingsWithSize binds
321 322
                     , ppUnless (null rules) pp_rules ]
    pp_rules = vcat [ blankLine
323
                    , text "------ Local rules for imported ids --------"
324 325 326 327 328 329 330 331 332 333
                    , pprRules rules ]

coreDumpFlag :: CoreToDo -> Maybe DumpFlag
coreDumpFlag (CoreDoSimplify {})      = Just Opt_D_verbose_core2core
coreDumpFlag (CoreDoPluginPass {})    = Just Opt_D_verbose_core2core
coreDumpFlag CoreDoFloatInwards       = Just Opt_D_verbose_core2core
coreDumpFlag (CoreDoFloatOutwards {}) = Just Opt_D_verbose_core2core
coreDumpFlag CoreLiberateCase         = Just Opt_D_verbose_core2core
coreDumpFlag CoreDoStaticArgs         = Just Opt_D_verbose_core2core
coreDumpFlag CoreDoCallArity          = Just Opt_D_dump_call_arity
334
coreDumpFlag CoreDoExitify            = Just Opt_D_dump_exitify
335 336
coreDumpFlag CoreDoDemand             = Just Opt_D_dump_stranal
coreDumpFlag CoreDoCpr                = Just Opt_D_dump_cpranal
337 338 339 340
coreDumpFlag CoreDoWorkerWrapper      = Just Opt_D_dump_worker_wrapper
coreDumpFlag CoreDoSpecialising       = Just Opt_D_dump_spec
coreDumpFlag CoreDoSpecConstr         = Just Opt_D_dump_spec
coreDumpFlag CoreCSE                  = Just Opt_D_dump_cse
Simon Peyton Jones's avatar
Simon Peyton Jones committed
341
coreDumpFlag CoreDesugar              = Just Opt_D_dump_ds_preopt
342 343 344
coreDumpFlag CoreDesugarOpt           = Just Opt_D_dump_ds
coreDumpFlag CoreTidy                 = Just Opt_D_dump_simpl
coreDumpFlag CorePrep                 = Just Opt_D_dump_prep
lukemaurer's avatar
lukemaurer committed
345
coreDumpFlag CoreOccurAnal            = Just Opt_D_dump_occur_anal
346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364

coreDumpFlag CoreDoPrintCore          = Nothing
coreDumpFlag (CoreDoRuleCheck {})     = Nothing
coreDumpFlag CoreDoNothing            = Nothing
coreDumpFlag (CoreDoPasses {})        = Nothing

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

lintPassResult :: HscEnv -> CoreToDo -> CoreProgram -> IO ()
lintPassResult hsc_env pass binds
  | not (gopt Opt_DoCoreLinting dflags)
  = return ()
  | otherwise
365
  = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
366 367 368 369 370 371 372 373 374 375
       ; Err.showPass dflags ("Core Linted result of " ++ showPpr dflags pass)
       ; displayLintResults dflags pass warns errs binds  }
  where
    dflags = hsc_dflags hsc_env

displayLintResults :: DynFlags -> CoreToDo
                   -> Bag Err.MsgDoc -> Bag Err.MsgDoc -> CoreProgram
                   -> IO ()
displayLintResults dflags pass warns errs binds
  | not (isEmptyBag errs)
Ben Gamari's avatar
Ben Gamari committed
376
  = do { putLogMsg dflags NoReason Err.SevDump noSrcSpan
Sylvain Henry's avatar
Sylvain Henry committed
377
           (defaultDumpStyle dflags)
378
           (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
379
                 , text "*** Offending Program ***"
380
                 , pprCoreBindings binds
381
                 , text "*** End of Offense ***" ])
382 383 384
       ; Err.ghcExit dflags 1 }

  | not (isEmptyBag warns)
Sylvain Henry's avatar
Sylvain Henry committed
385
  , not (hasNoDebugOutput dflags)
386
  , showLintWarnings pass
387 388
  -- If the Core linter encounters an error, output to stderr instead of
  -- stdout (#13342)
Ben Gamari's avatar
Ben Gamari committed
389
  = putLogMsg dflags NoReason Err.SevInfo noSrcSpan
Sylvain Henry's avatar
Sylvain Henry committed
390
        (defaultDumpStyle dflags)
391
        (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag (mapBag ($$ blankLine) warns))
392 393 394 395 396

  | otherwise = return ()
  where

lint_banner :: String -> SDoc -> SDoc
397 398 399
lint_banner string pass = text "*** Core Lint"      <+> text string
                          <+> text ": in result of" <+> pass
                          <+> text "***"
400 401 402 403 404 405 406 407 408 409 410

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

lintInteractiveExpr :: String -> HscEnv -> CoreExpr -> IO ()
lintInteractiveExpr what hsc_env expr
  | not (gopt Opt_DoCoreLinting dflags)
  = return ()
411
  | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
412 413 414 415 416 417 418 419
  = do { display_lint_err err
       ; Err.ghcExit dflags 1 }
  | otherwise
  = return ()
  where
    dflags = hsc_dflags hsc_env

    display_lint_err err
Ben Gamari's avatar
Ben Gamari committed
420
      = do { putLogMsg dflags NoReason Err.SevDump
Sylvain Henry's avatar
Sylvain Henry committed
421
               noSrcSpan (defaultDumpStyle dflags)
422 423
               (vcat [ lint_banner "errors" (text what)
                     , err
424
                     , text "*** Offending Program ***"
425
                     , pprCoreExpr expr
426
                     , text "*** End of Offense ***" ])
427 428 429 430 431
           ; Err.ghcExit 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.
Sylvain Henry's avatar
Sylvain Henry committed
432
-- These are Local things (see Note [Interactively-bound Ids in GHCi] in GHC.Driver.Types).
433 434 435 436 437 438 439
-- 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.
--
440
-- See #8215 for an example
441
interactiveInScope hsc_env
niteria's avatar
niteria committed
442
  = tyvars ++ ids
443 444 445 446 447 448 449
  where
    -- C.f. TcRnDriver.setInteractiveContext, Desugar.deSugarExpr
    ictxt                   = hsc_IC hsc_env
    (cls_insts, _fam_insts) = ic_instances ictxt
    te1    = mkTypeEnvWithImplicits (ic_tythings ictxt)
    te     = extendTypeEnvWithIds te1 (map instanceDFunId cls_insts)
    ids    = typeEnvIds te
niteria's avatar
niteria committed
450
    tyvars = tyCoVarsOfTypesList $ map idType ids
451 452 453 454 455
              -- 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)

456
-- | Type-check a 'CoreProgram'. See Note [Core Lint guarantee].
457
lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
458
--   Returns (warnings, errors)
459 460
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
461
lintCoreBindings dflags pass local_in_scope binds
Simon Peyton Jones's avatar
Simon Peyton Jones committed
462 463 464
  = initL dflags flags local_in_scope $
    addLoc TopLevelBindings           $
    lintLetBndrs TopLevel binders     $
465 466 467
        -- Put all the top-level binders in scope at the start
        -- This is because transformation rules can bring something
        -- into use 'unexpectedly'
468 469 470 471
    do { checkL (null dups) (dupVars dups)
       ; checkL (null ext_dups) (dupExtVars ext_dups)
       ; mapM lint_bind binds }
  where
Ryan Scott's avatar
Ryan Scott committed
472 473
    flags = defaultLintFlags
               { lf_check_global_ids = check_globals
474 475
               , lf_check_inline_loop_breakers = check_lbs
               , lf_check_static_ptrs = check_static_ptrs }
476 477 478 479 480 481 482

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

483 484 485 486 487 488
    -- See Note [Checking for INLINE loop breakers]
    check_lbs = case pass of
                      CoreDesugar    -> False
                      CoreDesugarOpt -> False
                      _              -> True

489
    -- See Note [Checking StaticPtrs]
490 491 492 493 494 495
    check_static_ptrs | not (xopt LangExt.StaticPointers dflags) = AllowAnywhere
                      | otherwise = case pass of
                          CoreDoFloatOutwards _ -> AllowAtTopLevel
                          CoreTidy              -> RejectEverywhere
                          CorePrep              -> AllowAtTopLevel
                          _                     -> AllowAnywhere
496

497 498 499 500 501 502 503 504
    binders = bindersOfBinds binds
    (_, dups) = removeDups compare 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} = ...
Gabor Greif's avatar
typos  
Gabor Greif committed
505
    -- because they both get the same linker symbol
506 507 508 509 510
    ext_dups = snd (removeDups ord_ext (map Var.varName binders))
    ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
                  , Just m2 <- nameModule_maybe n2
                  = compare (m1, nameOccName n1) (m2, nameOccName n2)
                  | otherwise = LT
511

512 513
    -- If you edit this function, you may need to update the GHC formalism
    -- See Note [GHC Formalism]
514
    lint_bind (Rec prs)         = mapM_ (lintSingleBinding TopLevel Recursive) prs
515
    lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
516

Austin Seipp's avatar
Austin Seipp committed
517 518 519
{-
************************************************************************
*                                                                      *
520
\subsection[lintUnfolding]{lintUnfolding}
Austin Seipp's avatar
Austin Seipp committed
521 522
*                                                                      *
************************************************************************
523

524 525 526 527 528 529 530 531
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;
532
hence the `TopLevelFlag` on `tcPragExpr` in GHC.IfaceToCore.
533

Austin Seipp's avatar
Austin Seipp committed
534
-}
535

536 537
lintUnfolding :: Bool           -- True <=> is a compulsory unfolding
              -> DynFlags
538
              -> SrcLoc
niteria's avatar
niteria committed
539
              -> VarSet         -- Treat these as in scope
540 541
              -> CoreExpr
              -> Maybe MsgDoc   -- Nothing => OK
542

Simon Peyton Jones's avatar
Simon Peyton Jones committed
543
lintUnfolding is_compulsory dflags locn var_set expr
544
  | isEmptyBag errs = Nothing
545
  | otherwise       = Just (pprMessageBag errs)
546
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
547 548
    vars = nonDetEltsUniqSet var_set
    (_warns, errs) = initL dflags defaultLintFlags vars $
549 550 551 552
                     if is_compulsory
                       -- See Note [Checking for levity polymorphism]
                     then noLPChecks linter
                     else linter
553 554
    linter = addLoc (ImportedUnfolding locn) $
             lintCoreExpr expr
555

556 557
lintExpr :: DynFlags
         -> [Var]               -- Treat these as in scope
558 559
         -> CoreExpr
         -> Maybe MsgDoc        -- Nothing => OK
560

561
lintExpr dflags vars expr
562 563 564
  | isEmptyBag errs = Nothing
  | otherwise       = Just (pprMessageBag errs)
  where
Simon Peyton Jones's avatar
Simon Peyton Jones committed
565
    (_warns, errs) = initL dflags defaultLintFlags vars linter
566 567
    linter = addLoc TopLevelBindings $
             lintCoreExpr expr
568

Austin Seipp's avatar
Austin Seipp committed
569 570 571
{-
************************************************************************
*                                                                      *
572
\subsection[lintCoreBinding]{lintCoreBinding}
Austin Seipp's avatar
Austin Seipp committed
573 574
*                                                                      *
************************************************************************
575

576
Check a core binding, returning the list of variables bound.
Austin Seipp's avatar
Austin Seipp committed
577
-}
578

twanvl's avatar
twanvl committed
579
lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
580 581
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
582
lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
583
  = addLoc (RhsOf binder) $
584
         -- Check the rhs
lukemaurer's avatar
lukemaurer committed
585
    do { ty <- lintRhs binder rhs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
586
       ; binder_ty <- applySubstTy (idType binder)
587
       ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
588

589
       -- If the binding is for a CoVar, the RHS should be (Coercion co)
Sylvain Henry's avatar
Sylvain Henry committed
590
       -- See Note [Core type and coercion invariant] in GHC.Core
591 592 593
       ; checkL (not (isCoVar binder) || isCoArg rhs)
                (mkLetErr binder rhs)

594 595 596 597 598 599 600
       -- 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
       ; checkL (isJoinId binder || not (isTypeLevPoly binder_ty))
                (badBndrTyMsg binder (text "levity-polymorphic"))

601
        -- Check the let/app invariant
Sylvain Henry's avatar
Sylvain Henry committed
602
        -- See Note [Core let/app invariant] in GHC.Core
603 604 605
       ; checkL ( isJoinId binder
               || not (isUnliftedType binder_ty)
               || (isNonRec rec_flag && exprOkForSpeculation rhs)
606
               || exprIsTickedString rhs)
607
           (badBndrTyMsg binder (text "unlifted"))
608

609 610
        -- Check that if the binder is top-level or recursive, it's not
        -- demanded. Primitive string literals are exempt as there is no
Sylvain Henry's avatar
Sylvain Henry committed
611
        -- computation to perform, see Note [Core top-level string literals].
612
       ; checkL (not (isStrictId binder)
613
            || (isNonRec rec_flag && not (isTopLevel top_lvl_flag))
614
            || exprIsTickedString rhs)
615
           (mkStrictMsg binder)
616

617 618
        -- Check that if the binder is at the top level and has type Addr#,
        -- that it is a string literal, see
Sylvain Henry's avatar
Sylvain Henry committed
619
        -- Note [Core top-level string literals].
620
       ; checkL (not (isTopLevel top_lvl_flag && binder_ty `eqType` addrPrimTy)
621
                 || exprIsTickedString rhs)
622 623
           (mkTopNonLitStrMsg binder)

624
       ; flags <- getLintFlags
lukemaurer's avatar
lukemaurer committed
625

626 627 628 629 630 631
         -- Check that a join-point binder has a valid type
         -- NB: lintIdBinder has checked that it is not top-level bound
       ; case isJoinId_maybe binder of
            Nothing    -> return ()
            Just arity ->  checkL (isValidJoinPointType arity binder_ty)
                                  (mkInvalidJoinPointMsg binder binder_ty)
lukemaurer's avatar
lukemaurer committed
632

633
       ; when (lf_check_inline_loop_breakers flags
634
               && isStableUnfolding (realIdUnfolding binder)
635 636
               && isStrongLoopBreaker (idOccInfo binder)
               && isInlinePragma (idInlinePragma binder))
637
              (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder))
638
              -- Only non-rule loop breakers inhibit inlining
639

640 641
       -- We used to check that the dmdTypeDepth of a demand signature never
       -- exceeds idArity, but that is an unnecessary complication, see
642
       -- Note [idArity varies independently of dmdTypeDepth] in GHC.Core.Op.DmdAnal
643

644 645 646
       -- 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]
647
       ; checkL (typeArity (idType binder) `lengthAtLeast` idArity binder)
648 649
           (text "idArity" <+> ppr (idArity binder) <+>
           text "exceeds typeArity" <+>
650 651 652 653
           ppr (length (typeArity (idType binder))) <> colon <+>
           ppr binder)

       ; case splitStrictSig (idStrictness binder) of
654
           (demands, result_info) | isBotDiv result_info ->
655
             checkL (demands `lengthAtLeast` idArity binder)
656 657
               (text "idArity" <+> ppr (idArity binder) <+>
               text "exceeds arity imposed by the strictness signature" <+>
658 659 660 661
               ppr (idStrictness binder) <> colon <+>
               ppr binder)
           _ -> return ()

lukemaurer's avatar
lukemaurer committed
662
       ; mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
663 664 665

       ; addLoc (UnfoldingOf binder) $
         lintIdUnfolding binder binder_ty (idUnfolding binder) }
666 667 668

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

lukemaurer's avatar
lukemaurer committed
670
-- | Checks the RHS of bindings. It only differs from 'lintCoreExpr'
671
-- in that it doesn't reject occurrences of the function 'makeStatic' when they
lukemaurer's avatar
lukemaurer committed
672 673 674
-- 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.
675 676
--
-- See Note [Checking StaticPtrs].
lukemaurer's avatar
lukemaurer committed
677 678 679 680 681 682 683 684 685
lintRhs :: Id -> CoreExpr -> LintM OutType
lintRhs bndr rhs
    | Just arity <- isJoinId_maybe bndr
    = lint_join_lams arity arity True rhs
    | AlwaysTailCalled arity <- tailCallInfo (idOccInfo bndr)
    = lint_join_lams arity arity False rhs
  where
    lint_join_lams 0 _ _ rhs
      = lintCoreExpr rhs
686

lukemaurer's avatar
lukemaurer committed
687
    lint_join_lams n tot enforce (Lam var expr)
688
      = lintLambda var $ lint_join_lams (n-1) tot enforce expr
689

lukemaurer's avatar
lukemaurer committed
690
    lint_join_lams n tot True _other
Simon Peyton Jones's avatar
Simon Peyton Jones committed
691
      = failWithL $ mkBadJoinArityMsg bndr tot (tot-n) rhs
lukemaurer's avatar
lukemaurer committed
692 693 694 695 696 697 698 699
    lint_join_lams _ _ False rhs
      = markAllJoinsBad $ lintCoreExpr 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 rhs = fmap lf_check_static_ptrs getLintFlags >>= go
700 701 702 703 704 705
  where
    -- Allow occurrences of 'makeStatic' at the top-level but produce errors
    -- otherwise.
    go AllowAtTopLevel
      | (binders0, rhs') <- collectTyBinders rhs
      , Just (fun, t, info, e) <- collectMakeStaticArgs rhs'
lukemaurer's avatar
lukemaurer committed
706 707
      = markAllJoinsBad $
        foldr
708
        -- imitate @lintCoreExpr (Lam ...)@
709
        lintLambda
710
        -- imitate @lintCoreExpr (App ...)@
711
        (do fun_ty <- lintCoreExpr fun
Simon Peyton Jones's avatar
Simon Peyton Jones committed
712
            lintCoreArgs fun_ty [Type t, info, e]
713 714
        )
        binders0
lukemaurer's avatar
lukemaurer committed
715
    go _ = markAllJoinsBad $ lintCoreExpr rhs
716

717
lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
Matthew Pickering's avatar
Matthew Pickering committed
718 719 720
lintIdUnfolding bndr bndr_ty uf
  | isStableUnfolding uf
  , Just rhs <- maybeUnfoldingTemplate uf
721 722 723 724
  = do { ty <- if isCompulsoryUnfolding uf
               then noLPChecks $ lintRhs bndr rhs
                     -- See Note [Checking for levity polymorphism]
               else lintRhs bndr rhs
725
       ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
726
lintIdUnfolding  _ _ _
Gabor Greif's avatar
Gabor Greif committed
727
  = return ()       -- Do not Lint unstable unfoldings, because that leads
Sylvain Henry's avatar
Sylvain Henry committed
728
                    -- to exponential behaviour; c.f. GHC.Core.FVs.idUnfoldingVars
729

Austin Seipp's avatar
Austin Seipp committed
730
{-
731 732 733 734 735
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
Gabor Greif's avatar
Gabor Greif committed
736
that form a mutually recursive group.  Only after a round of
737 738 739
simplification are they unravelled.  So we suppress the test for
the desugarer.

740 741 742
Note [Checking for levity polymorphism]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
We ordinarily want to check for bad levity polymorphism. See
Sylvain Henry's avatar
Sylvain Henry committed
743
Note [Levity polymorphism invariants] in GHC.Core. However, we do *not*
744 745 746 747 748 749 750 751 752 753 754 755 756
want to do this in a compulsory unfolding. Compulsory unfoldings arise
only internally, for things like newtype wrappers, dictionaries, and
(notably) unsafeCoerce#. These might legitimately be levity-polymorphic;
indeed levity-polyorphic unfoldings are a primary reason for the
very existence of compulsory unfoldings (we can't compile code for
the original, levity-poly, binding).

It is vitally important that we do levity-polymorphism checks *after*
performing the unfolding, but not beforehand. This is all safe because
we will check any unfolding after it has been unfolded; checking the
unfolding beforehand is merely an optimization, and one that actively
hurts us here.

Austin Seipp's avatar
Austin Seipp committed
757 758
************************************************************************
*                                                                      *
759
\subsection[lintCoreExpr]{lintCoreExpr}
Austin Seipp's avatar
Austin Seipp committed
760 761 762
*                                                                      *
************************************************************************
-}
763

764 765
-- For OutType, OutKind, the substitution has been applied,
--                       but has not been linted yet
766 767

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

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

777 778
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
779
lintCoreExpr (Var var)
780
  = lintVarOcc var 0
781

782 783
lintCoreExpr (Lit lit)
  = return (literalType lit)
784

785
lintCoreExpr (Cast expr co)
lukemaurer's avatar
lukemaurer committed
786
  = do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr
787
       ; co' <- applySubstCo co
788
       ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
789
       ; checkValueKind k2 (text "target of cast" <+> quotes (ppr co))
790 791
       ; lintRole co' Representational r
       ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
792
       ; return to_ty }
793

lukemaurer's avatar
lukemaurer committed
794 795 796 797 798 799 800 801 802 803 804 805 806 807
lintCoreExpr (Tick tickish expr)
  = do case tickish of
         Breakpoint _ ids -> forM_ ids $ \id -> do
                               checkDeadIdOcc id
                               lookupIdInScope id
         _                -> return ()
       markAllJoinsBadIf block_joins $ lintCoreExpr expr
  where
    block_joins = not (tickish `tickishScopesLike` 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).
808

809
lintCoreExpr (Let (NonRec tv (Type ty)) body)
810
  | isTyVar tv
811 812 813
  =     -- See Note [Linting type lets]
    do  { ty' <- applySubstTy ty
        ; lintTyBndr tv              $ \ tv' ->
814
    do  { addLoc (RhsOf tv) $ lintTyKind tv' ty'
815 816
                -- Now extend the substitution so we
                -- take advantage of it in the body
Simon Peyton Jones's avatar
Simon Peyton Jones committed
817
        ; extendTvSubstL tv ty'        $
818
          addLoc (BodyOfLetRec [tv]) $
819
          lintCoreExpr body } }
820

821
lintCoreExpr (Let (NonRec bndr rhs) body)
822
  | isId bndr
823 824
  = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
        ; addLoc (BodyOfLetRec [bndr])
825
                 (lintBinder LetBind bndr $ \_ ->
826 827
                  addGoodJoins [bndr] $
                  lintCoreExpr body) }
828

829
  | otherwise
830
  = failWithL (mkLetErr bndr rhs)       -- Not quite accurate
831

832 833
lintCoreExpr e@(Let (Rec pairs) body)
  = lintLetBndrs NotTopLevel bndrs $
834
    addGoodJoins bndrs             $
835 836 837 838 839 840 841
    do  { -- Check that the list of pairs is non-empty
          checkL (not (null pairs)) (emptyRec e)

          -- Check that there are no duplicated binders
        ; checkL (null dups) (dupVars dups)

          -- Check that either all the binders are joins, or none
lukemaurer's avatar
lukemaurer committed
842 843
        ; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $
            mkInconsistentRecMsg bndrs
844

845 846
        ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
        ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
847 848
  where
    bndrs = map fst pairs
849
    (_, dups) = removeDups compare bndrs
850

batterseapower's avatar
batterseapower committed
851
lintCoreExpr e@(App _ _)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
852
  = do { fun_ty <- lintCoreFun fun (length args)
lukemaurer's avatar
lukemaurer committed
853
       ; lintCoreArgs fun_ty args }
batterseapower's avatar
batterseapower committed
854 855
  where
    (fun, args) = collectArgs e
856 857

lintCoreExpr (Lam var expr)
858 859
  = markAllJoinsBad $
    lintLambda var $ lintCoreExpr expr
860

861 862
lintCoreExpr (Case scrut var alt_ty alts)
  = lintCaseExpr scrut var alt_ty alts
863

864 865
-- This case can't happen; linting types in expressions gets routed through
-- lintCoreArgs
866
lintCoreExpr (Type ty)
867
  = failWithL (text "Type found as expression" <+> ppr ty)
868 869

lintCoreExpr (Coercion co)
870 871
  = do { (k1, k2, ty1, ty2, role) <- lintInCo co
       ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
872

873 874
----------------------
lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed
lukemaurer's avatar
lukemaurer committed
875
            -> LintM Type -- returns type of the *variable*
876
lintVarOcc var nargs
lukemaurer's avatar
lukemaurer committed
877 878
  = do  { checkL (isNonCoVarId var)
                 (text "Non term variable" <+> ppr var)
Sylvain Henry's avatar
Sylvain Henry committed
879
                 -- See GHC.Core Note [Variable occurrences in Core]
lukemaurer's avatar
lukemaurer committed
880

881
        -- Check that the type of the occurrence is the same
882 883 884 885 886 887
        -- as the type of the binding site
        ; ty   <- applySubstTy (idType var)
        ; var' <- lookupIdInScope var
        ; let ty' = idType var'
        ; ensureEqTys ty ty' $ mkBndrOccTypeMismatchMsg var' var ty' ty

lukemaurer's avatar
lukemaurer committed
888 889
          -- Check for a nested occurrence of the StaticPtr constructor.
          -- See Note [Checking StaticPtrs].
890
        ; lf <- getLintFlags
lukemaurer's avatar
lukemaurer committed
891 892 893 894 895
        ; when (nargs /= 0 && lf_check_static_ptrs lf /= AllowAnywhere) $
            checkL (idName var /= makeStaticName) $
              text "Found makeStatic nested in an expression"

        ; checkDeadIdOcc var
896 897
        ; checkJoinOcc var nargs

lukemaurer's avatar
lukemaurer committed
898 899
        ; return (idType var') }

900 901 902
lintCoreFun :: CoreExpr
            -> Int        -- Number of arguments (type or val) being passed
            -> LintM Type -- Returns type of the *function*
lukemaurer's avatar
lukemaurer committed
903
lintCoreFun (Var var) nargs
904 905
  = lintVarOcc var nargs

lukemaurer's avatar
lukemaurer committed
906 907 908 909
lintCoreFun (Lam var body) nargs
  -- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; see
  -- Note [Beta redexes]
  | nargs /= 0
910
  = lintLambda var $ lintCoreFun body (nargs - 1)
911

lukemaurer's avatar
lukemaurer committed
912 913
lintCoreFun expr nargs
  = markAllJoinsBadIf (nargs /= 0) $
914
      -- See Note [Join points are less general than the paper]
lukemaurer's avatar
lukemaurer committed
915
    lintCoreExpr expr
916 917 918 919 920 921 922
------------------
lintLambda :: Var -> LintM Type -> LintM Type
lintLambda var lintBody =
    addLoc (LambdaBodyOf var) $
    lintBinder LambdaBind var $ \ var' ->
      do { body_ty <- lintBody
         ; return (mkLamType var' body_ty) }
923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958
------------------
checkDeadIdOcc :: Id -> LintM ()
-- Occurrences of an Id should never be dead....
-- except when we are checking a case pattern
checkDeadIdOcc id
  | isDeadOcc (idOccInfo id)
  = do { in_case <- inCasePat
       ; checkL in_case
                (text "Occurrence of a dead Id" <+> ppr id) }
  | otherwise
  = 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 n_args
  | Just join_arity_occ <- isJoinId_maybe var
  = do { mb_join_arity_bndr <- lookupJoinId var
       ; case mb_join_arity_bndr of {
           Nothing -> -- Binder is not a join point
                      addErrL (invalidJoinOcc var) ;

           Just join_arity_bndr ->

    do { checkL (join_arity_bndr == join_arity_occ) $
           -- Arity differs at binding site and occurrence
         mkJoinBndrOccMismatchMsg var join_arity_bndr join_arity_occ

       ; checkL (n_args == join_arity_occ) $
           -- Arity doesn't match #args
         mkBadJumpMsg var join_arity_occ n_args } } }

  | otherwise
  = return ()

Austin Seipp's avatar
Austin Seipp committed
959
{-
960 961
Note [No alternatives lint check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
962
Case expressions with no alternatives are odd beasts, and it would seem
963
like they would worth be looking at in the linter (cf #10180). We
964
used to check two things:
965

966 967
* exprIsHNF is false: it would *seem* to be terribly wrong if
  the scrutinee was already in head normal form.
968 969 970 971

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

972
It was already known that the second test was not entirely reliable.
973
Unfortunately (#13990), the first test turned out not to be reliable
974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001
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.

1002

lukemaurer's avatar
lukemaurer committed
1003 1004 1005 1006 1007 1008 1009 1010 1011
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
Sylvain Henry's avatar
Sylvain Henry committed
1012
[Invariants on join points] in GHC.Core). However, strictly from a
lukemaurer's avatar
lukemaurer committed
1013 1014 1015 1016 1017 1018 1019 1020 1021
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
Sylvain Henry's avatar
Sylvain Henry committed
1022
in, say, GHC.Core.Subst.simpleOptPgm, which in some circumstances can run immediately
lukemaurer's avatar
lukemaurer committed
1023 1024
before Float Out.

Sylvain Henry's avatar
Sylvain Henry committed
1025
All that said, currently GHC.Core.Subst.simpleOptPgm is the only thing using this
lukemaurer's avatar
lukemaurer committed
1026 1027 1028 1029
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.

Austin Seipp's avatar
Austin Seipp committed
1030 1031
************************************************************************
*                                                                      *
1032
\subsection[lintCoreArgs]{lintCoreArgs}
Austin Seipp's avatar
Austin Seipp committed
1033 1034
*                                                                      *
************************************************************************
1035

1036 1037
The basic version of these functions checks that the argument is a
subtype of the required type, as one would expect.
Austin Seipp's avatar
Austin Seipp committed
1038
-}
1039

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1040 1041 1042 1043

lintCoreArgs  :: OutType -> [CoreArg] -> LintM OutType
lintCoreArgs fun_ty args = foldM lintCoreArg fun_ty args

1044
lintCoreArg  :: OutType -> CoreArg -> LintM OutType
1045
lintCoreArg fun_ty (Type arg_ty)
1046
  = do { checkL (not (isCoercionTy arg_ty))
1047
                (text "Unnecessary coercion-to-type injection:"
1048 1049
                  <+> ppr arg_ty)
       ; arg_ty' <- applySubstTy arg_ty
1050
       ; lintTyApp fun_ty arg_ty' }
1051 1052

lintCoreArg fun_ty arg
lukemaurer's avatar
lukemaurer committed
1053
  = do { arg_ty <- markAllJoinsBad $ lintCoreExpr arg
Sylvain Henry's avatar
Sylvain Henry committed
1054
           -- See Note [Levity polymorphism invariants] in GHC.Core
1055 1056
       ; flags <- getLintFlags
       ; lintL (not (lf_check_levity_poly flags) || not (isTypeLevPoly arg_ty))
1057 1058 1059 1060
           (text "Levity-polymorphic argument:" <+>
             (ppr arg <+> dcolon <+> parens (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))))
          -- check for levity polymorphism first, because otherwise isUnliftedType panics

1061
       ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
1062
                (mkLetAppMsg arg)
1063
       ; lintValApp arg fun_ty arg_ty }
1064 1065 1066

-----------------
lintAltBinders :: OutType     -- Scrutinee type
1067
               -> OutType     -- Constructor type
1068 1069
               -> [OutVar]    -- Binders
               -> LintM ()
1070 1071
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
1072
lintAltBinders scrut_ty con_ty []
1073
  = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
1074
lintAltBinders scrut_ty con_ty (bndr:bndrs)
1075
  | isTyVar bndr
1076 1077 1078 1079
  = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
       ; lintAltBinders scrut_ty con_ty' bndrs }
  | otherwise
  = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
1080
       ; lintAltBinders scrut_ty con_ty' bndrs }
1081 1082 1083 1084

-----------------
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp fun_ty arg_ty
1085 1086
  | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
  = do  { lintTyKind tv arg_ty
1087 1088 1089
        ; in_scope <- getInScope
        -- substTy needs the set of tyvars in scope to avoid generating
        -- uniques that are already in scope.
Sylvain Henry's avatar
Sylvain Henry committed
1090
        -- See Note [The substitution invariant] in GHC.Core.TyCo.Subst
1091
        ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
1092

1093 1094
  | otherwise
  = failWithL (mkTyAppMsg fun_ty arg_ty)
Simon Peyton Jones's avatar