CoreLint.hs 101 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

A ``lint'' pass to check for Core correctness
Austin Seipp's avatar
Austin Seipp committed
7
-}
8

9
{-# LANGUAGE CPP #-}
Ian Lynagh's avatar
Ian Lynagh committed
10

11 12
module CoreLint (
    lintCoreBindings, lintUnfolding,
13
    lintPassResult, lintInteractiveExpr, lintExpr,
Ryan Scott's avatar
Ryan Scott committed
14
    lintAnnots, lintTypes,
15 16

    -- ** Debug output
17
    endPass, endPassIO,
18
    dumpPassResult,
19 20
    CoreLint.dumpIfSet,
 ) where
21

22
#include "HsVersions.h"
23

24 25
import GhcPrelude

26
import CoreSyn
Simon Marlow's avatar
Simon Marlow committed
27 28
import CoreFVs
import CoreUtils
29
import CoreStats   ( coreBindsStats )
30
import CoreMonad
31
import Bag
Simon Marlow's avatar
Simon Marlow committed
32 33 34
import Literal
import DataCon
import TysWiredIn
35
import TysPrim
Ben Gamari's avatar
Ben Gamari committed
36
import TcType ( isFloatingTy )
Simon Marlow's avatar
Simon Marlow committed
37 38
import Var
import VarEnv
39
import VarSet
Simon Marlow's avatar
Simon Marlow committed
40
import Name
41
import Id
lukemaurer's avatar
lukemaurer committed
42
import IdInfo
43
import PprCore
Simon Marlow's avatar
Simon Marlow committed
44
import ErrUtils
batterseapower's avatar
batterseapower committed
45
import Coercion
Simon Marlow's avatar
Simon Marlow committed
46
import SrcLoc
47
import Kind
Simon Marlow's avatar
Simon Marlow committed
48
import Type
49
import RepType
50
import TyCoRep       -- checks validity of types/coercions
Simon Marlow's avatar
Simon Marlow committed
51
import TyCon
52
import CoAxiom
Simon Marlow's avatar
Simon Marlow committed
53
import BasicTypes
54
import ErrUtils as Err
55
import ListSetOps
56
import PrelNames
57
import Outputable
58
import FastString
59
import Util
60
import InstEnv     ( instanceDFunId )
eir@cis.upenn.edu's avatar
eir@cis.upenn.edu committed
61
import OptCoercion ( checkAxInstCo )
Peter Wortmann's avatar
Peter Wortmann committed
62
import UniqSupply
63 64
import CoreArity ( typeArity )
import Demand ( splitStrictSig, isBotRes )
65 66 67

import HscTypes
import DynFlags
68
import Control.Monad
quchen's avatar
quchen committed
69
import qualified Control.Monad.Fail as MonadFail
70
import MonadUtils
71 72
import Data.Foldable      ( toList )
import Data.List.NonEmpty ( NonEmpty )
Simon Marlow's avatar
Simon Marlow committed
73
import Data.Maybe
74
import Pair
75
import qualified GHC.LanguageExtensions as LangExt
76

Austin Seipp's avatar
Austin Seipp committed
77
{-
78 79 80 81 82 83
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.
84
To this purpose, there is a document core-spec.pdf built in docs/core-spec that
85 86 87 88 89
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.

90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
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.

108 109
Summary of checks
~~~~~~~~~~~~~~~~~
110 111 112 113 114 115
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
116 117 118 119
        (a) type errors
        (b) Out-of-scope type variables
        (c) Out-of-scope local variables
        (d) Ill-kinded types
120
        (e) Incorrect unsafe coercions
121 122

If we have done specialisation the we check that there are
123
        (a) No top-level bindings of primitive (unboxed type)
124 125 126 127 128

Outstanding issues:

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

134

135 136 137 138 139 140
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.

141 142
Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
143
In the desugarer, it's very very convenient to be able to say (in effect)
144
        let a = Type Int in <body>
145 146 147
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
148
reject a correct program.  So we carry a type substitution (in this example
149
[a -> Int]) and apply this substitution before comparing types.  The functin
150 151
        lintInTy :: Type -> LintM (Type, Kind)
returns a substituted type.
152 153 154 155

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

156
For Ids, the type-substituted Id is added to the in_scope set (which
157
itself is part of the TCvSubst we are carrying down), and when we
Gabor Greif's avatar
Gabor Greif committed
158
find an occurrence of an Id, we fetch it from the in-scope set.
159

160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177
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.

lukemaurer's avatar
lukemaurer committed
178 179 180 181
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
182 183
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
184 185 186 187 188 189 190 191

  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

192 193 194 195 196
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
197

198 199 200 201 202 203 204
************************************************************************
*                                                                      *
                 Beginning and ending passes
*                                                                      *
************************************************************************

These functions are not CoreM monad stuff, but they probably ought to
205 206
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
207
-}
208

209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
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
242 243 244 245 246 247 248 249
  = do { forM_ mb_flag $ \flag ->
           Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) 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.
       ; Err.debugTraceMsg dflags 2 size_doc
       }
250 251 252 253 254 255 256

  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
257
                     , pprCoreBindingsWithSize binds
258 259
                     , ppUnless (null rules) pp_rules ]
    pp_rules = vcat [ blankLine
260
                    , text "------ Local rules for imported ids --------"
261 262 263 264 265 266 267 268 269 270
                    , 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
271
coreDumpFlag CoreDoExitify            = Just Opt_D_dump_exitify
272 273 274 275 276
coreDumpFlag CoreDoStrictness         = Just Opt_D_dump_stranal
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
277
coreDumpFlag CoreDesugar              = Just Opt_D_dump_ds_preopt
278 279 280
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
281
coreDumpFlag CoreOccurAnal            = Just Opt_D_dump_occur_anal
282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300

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
301
  = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
302 303 304 305 306 307 308 309 310 311
       ; 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
312
  = do { putLogMsg dflags NoReason Err.SevDump noSrcSpan
Sylvain Henry's avatar
Sylvain Henry committed
313
           (defaultDumpStyle dflags)
314
           (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
315
                 , text "*** Offending Program ***"
316
                 , pprCoreBindings binds
317
                 , text "*** End of Offense ***" ])
318 319 320
       ; Err.ghcExit dflags 1 }

  | not (isEmptyBag warns)
Sylvain Henry's avatar
Sylvain Henry committed
321
  , not (hasNoDebugOutput dflags)
322
  , showLintWarnings pass
323 324
  -- If the Core linter encounters an error, output to stderr instead of
  -- stdout (#13342)
Ben Gamari's avatar
Ben Gamari committed
325
  = putLogMsg dflags NoReason Err.SevInfo noSrcSpan
Sylvain Henry's avatar
Sylvain Henry committed
326
        (defaultDumpStyle dflags)
327
        (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag (mapBag ($$ blankLine) warns))
328 329 330 331 332

  | otherwise = return ()
  where

lint_banner :: String -> SDoc -> SDoc
333 334 335
lint_banner string pass = text "*** Core Lint"      <+> text string
                          <+> text ": in result of" <+> pass
                          <+> text "***"
336 337 338 339 340 341 342 343 344 345 346

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 ()
347
  | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
348 349 350 351 352 353 354 355
  = 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
356
      = do { putLogMsg dflags NoReason Err.SevDump
Sylvain Henry's avatar
Sylvain Henry committed
357
               noSrcSpan (defaultDumpStyle dflags)
358 359
               (vcat [ lint_banner "errors" (text what)
                     , err
360
                     , text "*** Offending Program ***"
361
                     , pprCoreExpr expr
362
                     , text "*** End of Offense ***" ])
363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
           ; 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.
-- 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 hsc_env
niteria's avatar
niteria committed
378
  = tyvars ++ ids
379 380 381 382 383 384 385
  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
386
    tyvars = tyCoVarsOfTypesList $ map idType ids
387 388 389 390 391
              -- 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)

392
lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
393
--   Returns (warnings, errors)
394 395
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
396
lintCoreBindings dflags pass local_in_scope binds
397 398
  = initL dflags flags in_scope_set $
    addLoc TopLevelBindings         $
399
    lintLetBndrs TopLevel binders   $
400 401 402
        -- Put all the top-level binders in scope at the start
        -- This is because transformation rules can bring something
        -- into use 'unexpectedly'
403 404 405 406
    do { checkL (null dups) (dupVars dups)
       ; checkL (null ext_dups) (dupExtVars ext_dups)
       ; mapM lint_bind binds }
  where
407 408
    in_scope_set = mkInScopeSet (mkVarSet local_in_scope)

Ryan Scott's avatar
Ryan Scott committed
409 410
    flags = defaultLintFlags
               { lf_check_global_ids = check_globals
411 412
               , lf_check_inline_loop_breakers = check_lbs
               , lf_check_static_ptrs = check_static_ptrs }
413 414 415 416 417 418 419

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

420 421 422 423 424 425
    -- See Note [Checking for INLINE loop breakers]
    check_lbs = case pass of
                      CoreDesugar    -> False
                      CoreDesugarOpt -> False
                      _              -> True

426
    -- See Note [Checking StaticPtrs]
427 428 429 430 431 432
    check_static_ptrs | not (xopt LangExt.StaticPointers dflags) = AllowAnywhere
                      | otherwise = case pass of
                          CoreDoFloatOutwards _ -> AllowAtTopLevel
                          CoreTidy              -> RejectEverywhere
                          CorePrep              -> AllowAtTopLevel
                          _                     -> AllowAnywhere
433

434 435 436 437 438 439 440 441
    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
442
    -- because they both get the same linker symbol
443 444 445 446 447
    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
448

449 450
    -- If you edit this function, you may need to update the GHC formalism
    -- See Note [GHC Formalism]
451
    lint_bind (Rec prs)         = mapM_ (lintSingleBinding TopLevel Recursive) prs
452
    lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
453

Austin Seipp's avatar
Austin Seipp committed
454 455 456
{-
************************************************************************
*                                                                      *
457
\subsection[lintUnfolding]{lintUnfolding}
Austin Seipp's avatar
Austin Seipp committed
458 459
*                                                                      *
************************************************************************
460

461 462 463 464 465 466 467 468 469 470
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.

Austin Seipp's avatar
Austin Seipp committed
471
-}
472

473 474
lintUnfolding :: DynFlags
              -> SrcLoc
niteria's avatar
niteria committed
475
              -> VarSet         -- Treat these as in scope
476 477
              -> CoreExpr
              -> Maybe MsgDoc   -- Nothing => OK
478

479
lintUnfolding dflags locn vars expr
480
  | isEmptyBag errs = Nothing
481
  | otherwise       = Just (pprMessageBag errs)
482
  where
483 484
    in_scope = mkInScopeSet vars
    (_warns, errs) = initL dflags defaultLintFlags in_scope linter
485 486
    linter = addLoc (ImportedUnfolding locn) $
             lintCoreExpr expr
487

488 489
lintExpr :: DynFlags
         -> [Var]               -- Treat these as in scope
490 491
         -> CoreExpr
         -> Maybe MsgDoc        -- Nothing => OK
492

493
lintExpr dflags vars expr
494 495 496
  | isEmptyBag errs = Nothing
  | otherwise       = Just (pprMessageBag errs)
  where
497 498
    in_scope = mkInScopeSet (mkVarSet vars)
    (_warns, errs) = initL dflags defaultLintFlags in_scope linter
499 500
    linter = addLoc TopLevelBindings $
             lintCoreExpr expr
501

Austin Seipp's avatar
Austin Seipp committed
502 503 504
{-
************************************************************************
*                                                                      *
505
\subsection[lintCoreBinding]{lintCoreBinding}
Austin Seipp's avatar
Austin Seipp committed
506 507
*                                                                      *
************************************************************************
508

509
Check a core binding, returning the list of variables bound.
Austin Seipp's avatar
Austin Seipp committed
510
-}
511

twanvl's avatar
twanvl committed
512
lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
513 514
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
515
lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
516
  = addLoc (RhsOf binder) $
517
         -- Check the rhs
lukemaurer's avatar
lukemaurer committed
518
    do { ty <- lintRhs binder rhs
Simon Peyton Jones's avatar
Simon Peyton Jones committed
519
       ; binder_ty <- applySubstTy (idType binder)
520
       ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
521

522 523 524 525 526 527 528
       -- 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"))

529 530
        -- Check the let/app invariant
        -- See Note [CoreSyn let/app invariant] in CoreSyn
531 532 533
       ; checkL ( isJoinId binder
               || not (isUnliftedType binder_ty)
               || (isNonRec rec_flag && exprOkForSpeculation rhs)
534
               || exprIsTickedString rhs)
535
           (badBndrTyMsg binder (text "unlifted"))
536

537 538 539
        -- 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].
540
       ; checkL (not (isStrictId binder)
541
            || (isNonRec rec_flag && not (isTopLevel top_lvl_flag))
542
            || exprIsTickedString rhs)
543
           (mkStrictMsg binder)
544

545 546 547 548
        -- 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].
       ; checkL (not (isTopLevel top_lvl_flag && binder_ty `eqType` addrPrimTy)
549
                 || exprIsTickedString rhs)
550 551
           (mkTopNonLitStrMsg binder)

552
       ; flags <- getLintFlags
lukemaurer's avatar
lukemaurer committed
553

554 555 556 557 558 559
         -- 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
560

561
       ; when (lf_check_inline_loop_breakers flags
562
               && isStableUnfolding (realIdUnfolding binder)
563 564
               && isStrongLoopBreaker (idOccInfo binder)
               && isInlinePragma (idInlinePragma binder))
565
              (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder))
566
              -- Only non-rule loop breakers inhibit inlining
567

568 569
      -- Check whether arity and demand type are consistent (only if demand analysis
      -- already happened)
570 571 572 573 574 575 576
      --
      -- 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)
577

578 579 580
       -- 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]
581
       ; checkL (typeArity (idType binder) `lengthAtLeast` idArity binder)
582 583
           (text "idArity" <+> ppr (idArity binder) <+>
           text "exceeds typeArity" <+>
584 585 586 587 588
           ppr (length (typeArity (idType binder))) <> colon <+>
           ppr binder)

       ; case splitStrictSig (idStrictness binder) of
           (demands, result_info) | isBotRes result_info ->
589
             checkL (demands `lengthAtLeast` idArity binder)
590 591
               (text "idArity" <+> ppr (idArity binder) <+>
               text "exceeds arity imposed by the strictness signature" <+>
592 593 594 595
               ppr (idStrictness binder) <> colon <+>
               ppr binder)
           _ -> return ()

lukemaurer's avatar
lukemaurer committed
596
       ; mapM_ (lintCoreRule binder binder_ty) (idCoreRules binder)
Simon Peyton Jones's avatar
Simon Peyton Jones committed
597 598 599

       ; addLoc (UnfoldingOf binder) $
         lintIdUnfolding binder binder_ty (idUnfolding binder) }
600 601 602

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

lukemaurer's avatar
lukemaurer committed
604
-- | Checks the RHS of bindings. It only differs from 'lintCoreExpr'
605
-- in that it doesn't reject occurrences of the function 'makeStatic' when they
lukemaurer's avatar
lukemaurer committed
606 607 608
-- 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.
609 610
--
-- See Note [Checking StaticPtrs].
lukemaurer's avatar
lukemaurer committed
611 612 613 614 615 616 617 618 619
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
620

lukemaurer's avatar
lukemaurer committed
621 622
    lint_join_lams n tot enforce (Lam var expr)
      = addLoc (LambdaBodyOf var) $
623
        lintBinder LambdaBind var $ \ var' ->
lukemaurer's avatar
lukemaurer committed
624 625
        do { body_ty <- lint_join_lams (n-1) tot enforce expr
           ; return $ mkLamType var' body_ty }
626

lukemaurer's avatar
lukemaurer committed
627
    lint_join_lams n tot True _other
Simon Peyton Jones's avatar
Simon Peyton Jones committed
628
      = failWithL $ mkBadJoinArityMsg bndr tot (tot-n) rhs
lukemaurer's avatar
lukemaurer committed
629 630 631 632 633 634 635 636
    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
637 638 639 640 641 642
  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
643 644
      = markAllJoinsBad $
        foldr
645
        -- imitate @lintCoreExpr (Lam ...)@
646 647
        (\var loopBinders ->
          addLoc (LambdaBodyOf var) $
648
            lintBinder LambdaBind var $ \var' ->
649 650 651
              do { body_ty <- loopBinders
                 ; return $ mkLamType var' body_ty }
        )
652
        -- imitate @lintCoreExpr (App ...)@
653 654 655 656
        (do fun_ty <- lintCoreExpr fun
            addLoc (AnExpr rhs') $ lintCoreArgs fun_ty [Type t, info, e]
        )
        binders0
lukemaurer's avatar
lukemaurer committed
657
    go _ = markAllJoinsBad $ lintCoreExpr rhs
658

659 660 661
lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
  | isStableSource src
lukemaurer's avatar
lukemaurer committed
662
  = do { ty <- lintRhs bndr rhs
663
       ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
Simon Peyton Jones's avatar
Simon Peyton Jones committed
664 665 666

lintIdUnfolding bndr bndr_ty (DFunUnfolding { df_con = con, df_bndrs = bndrs
                                            , df_args = args })
667
  = do { ty <- lintBinders LambdaBind bndrs $ \ bndrs' ->
Simon Peyton Jones's avatar
Simon Peyton Jones committed
668 669 670 671
               do { res_ty <- lintCoreArgs (dataConRepType con) args
                  ; return (mkLamTypes bndrs' res_ty) }
       ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "dfun unfolding") ty) }

672
lintIdUnfolding  _ _ _
Gabor Greif's avatar
Gabor Greif committed
673
  = return ()       -- Do not Lint unstable unfoldings, because that leads
Simon Peyton Jones's avatar
Simon Peyton Jones committed
674
                    -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
675

Austin Seipp's avatar
Austin Seipp committed
676
{-
677 678 679 680 681
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
682
that form a mutually recursive group.  Only after a round of
683 684 685
simplification are they unravelled.  So we suppress the test for
the desugarer.

Austin Seipp's avatar
Austin Seipp committed
686 687
************************************************************************
*                                                                      *
688
\subsection[lintCoreExpr]{lintCoreExpr}
Austin Seipp's avatar
Austin Seipp committed
689 690 691
*                                                                      *
************************************************************************
-}
692

693 694
-- For OutType, OutKind, the substitution has been applied,
--                       but has not been linted yet
695 696

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

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

706 707
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
708
lintCoreExpr (Var var)
709
  = lintVarOcc var 0
710

711 712
lintCoreExpr (Lit lit)
  = return (literalType lit)
713

714
lintCoreExpr (Cast expr co)
lukemaurer's avatar
lukemaurer committed
715
  = do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr
716
       ; co' <- applySubstCo co
717 718
       ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
       ; lintL (classifiesTypeWithValues k2)
719
               (text "Target of cast not # or *:" <+> ppr co)
720 721
       ; lintRole co' Representational r
       ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
722
       ; return to_ty }
723

lukemaurer's avatar
lukemaurer committed
724 725 726 727 728 729 730 731 732 733 734 735 736 737
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).
738

739
lintCoreExpr (Let (NonRec tv (Type ty)) body)
740
  | isTyVar tv
741 742 743
  =     -- See Note [Linting type lets]
    do  { ty' <- applySubstTy ty
        ; lintTyBndr tv              $ \ tv' ->
744
    do  { addLoc (RhsOf tv) $ lintTyKind tv' ty'
745 746
                -- Now extend the substitution so we
                -- take advantage of it in the body
lukemaurer's avatar
lukemaurer committed
747
        ; extendSubstL tv ty'        $
748
          addLoc (BodyOfLetRec [tv]) $
749
          lintCoreExpr body } }
750

751
lintCoreExpr (Let (NonRec bndr rhs) body)
752
  | isId bndr
753 754
  = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
        ; addLoc (BodyOfLetRec [bndr])
755
                 (lintIdBndr NotTopLevel LetBind bndr $ \_ ->
756 757
                  addGoodJoins [bndr] $
                  lintCoreExpr body) }
758

759
  | otherwise
760
  = failWithL (mkLetErr bndr rhs)       -- Not quite accurate
761

762 763
lintCoreExpr e@(Let (Rec pairs) body)
  = lintLetBndrs NotTopLevel bndrs $
764
    addGoodJoins bndrs             $
765 766 767 768 769 770 771
    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
772 773
        ; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $
            mkInconsistentRecMsg bndrs
774

775 776
        ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
        ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
777 778
  where
    bndrs = map fst pairs
779
    (_, dups) = removeDups compare bndrs
780

batterseapower's avatar
batterseapower committed
781
lintCoreExpr e@(App _ _)
lukemaurer's avatar
lukemaurer committed
782 783 784
  = addLoc (AnExpr e) $
    do { fun_ty <- lintCoreFun fun (length args)
       ; lintCoreArgs fun_ty args }
batterseapower's avatar
batterseapower committed
785 786
  where
    (fun, args) = collectArgs e
787 788

lintCoreExpr (Lam var expr)
789
  = addLoc (LambdaBodyOf var) $
lukemaurer's avatar
lukemaurer committed
790
    markAllJoinsBad $
791
    lintBinder LambdaBind var $ \ var' ->
792
    do { body_ty <- lintCoreExpr expr
793
       ; return $ mkLamType var' body_ty }
794 795 796

lintCoreExpr e@(Case scrut var alt_ty alts) =
       -- Check the scrutinee
797
  do { let scrut_diverges = exprIsBottom scrut
lukemaurer's avatar
lukemaurer committed
798
     ; scrut_ty <- markAllJoinsBad $ lintCoreExpr scrut
799 800
     ; (alt_ty, _) <- lintInTy alt_ty
     ; (var_ty, _) <- lintInTy (idType var)
801

802 803 804
     -- 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.
805

Ben Gamari's avatar
Ben Gamari committed
806 807 808 809 810 811 812 813 814
     -- See Note [Rules for floating-point comparisons] in PrelRules
     ; let isLitPat (LitAlt _, _ , _) = True
           isLitPat _                 = False
     ; checkL (not $ isFloatingTy scrut_ty && any isLitPat alts)
         (ptext (sLit $ "Lint warning: Scrutinising floating-point " ++
                        "expression with literal pattern in case " ++
                        "analysis (see Trac #9238).")
          $$ text "scrut" <+> ppr scrut)

815
     ; case tyConAppTyCon_maybe (idType var) of
816
         Just tycon
817 818 819 820 821 822
              | debugIsOn
              , isAlgTyCon tycon
              , not (isAbstractTyCon tycon)
              , null (tyConDataCons tycon)
              , not scrut_diverges
              -> pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
823
                        -- This can legitimately happen for type families
824 825 826
                      $ return ()
         _otherwise -> return ()

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

829 830
     ; subst <- getTCvSubst
     ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
831

832
     ; lintIdBndr NotTopLevel CaseBind var $ \_ ->
833
       do { -- Check the alternatives
834
            mapM_ (lintCoreAlt scrut_ty alt_ty) alts
835
          ; checkCaseAlts e scrut_ty alts
836
          ; return alt_ty } }
837

838 839
-- This case can't happen; linting types in expressions gets routed through
-- lintCoreArgs
840
lintCoreExpr (Type ty)
841
  = failWithL (text "Type found as expression" <+> ppr ty)
842 843

lintCoreExpr (Coercion co)
844 845
  = do { (k1, k2, ty1, ty2, role) <- lintInCo co
       ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
846

847 848
----------------------
lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed
lukemaurer's avatar
lukemaurer committed
849
            -> LintM Type -- returns type of the *variable*
850
lintVarOcc var nargs
lukemaurer's avatar
lukemaurer committed
851 852 853
  = do  { checkL (isNonCoVarId var)
                 (text "Non term variable" <+> ppr var)

854 855 856 857 858 859 860
        -- Cneck that the type of the occurrence is the same
        -- 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
861 862
          -- Check for a nested occurrence of the StaticPtr constructor.
          -- See Note [Checking StaticPtrs].
863
        ; lf <- getLintFlags
lukemaurer's avatar
lukemaurer committed
864 865 866 867 868
        ; when (nargs /= 0 && lf_check_static_ptrs lf /= AllowAnywhere) $
            checkL (idName var /= makeStaticName) $
              text "Found makeStatic nested in an expression"

        ; checkDeadIdOcc var
869 870
        ; checkJoinOcc var nargs

lukemaurer's avatar
lukemaurer committed
871 872
        ; return (idType var') }

873 874 875
lintCoreFun :: CoreExpr
            -> Int        -- Number of arguments (type or val) being passed
            -> LintM Type -- Returns type of the *function*
lukemaurer's avatar
lukemaurer committed
876
lintCoreFun (Var var) nargs
877 878
  = lintVarOcc var nargs

lukemaurer's avatar
lukemaurer committed
879 880 881 882 883
lintCoreFun (Lam var body) nargs
  -- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; see
  -- Note [Beta redexes]
  | nargs /= 0
  = addLoc (LambdaBodyOf var) $
884
    lintBinder LambdaBind var $ \ var' ->
lukemaurer's avatar
lukemaurer committed
885 886
    do { body_ty <- lintCoreFun body (nargs - 1)
       ; return $ mkLamType var' body_ty }
887

lukemaurer's avatar
lukemaurer committed
888 889 890 891
lintCoreFun expr nargs
  = markAllJoinsBadIf (nargs /= 0) $
    lintCoreExpr expr

892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927
------------------
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
928
{-
929 930
Note [No alternatives lint check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
931 932 933
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:
934

935 936
* exprIsHNF is false: it would *seem* to be terribly wrong if
  the scrutinee was already in head normal form.
937 938 939 940

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

941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970
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.

971

lukemaurer's avatar
lukemaurer committed
972 973 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
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.

Austin Seipp's avatar
Austin Seipp committed
999 1000
************************************************************************
*                                                                      *
1001
\subsection[lintCoreArgs]{lintCoreArgs}
Austin Seipp's avatar
Austin Seipp committed
1002 1003
*                                                                      *
************************************************************************
1004

1005 1006
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
1007
-}
1008

Simon Peyton Jones's avatar
Simon Peyton Jones committed
1009 1010 1011 1012

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

1013
lintCoreArg  :: OutType -> CoreArg -> LintM OutType
1014
lintCoreArg fun_ty (Type arg_ty)
1015
  = do { checkL (not (isCoercionTy arg_ty))
1016
                (text "Unnecessary coercion-to-type injection:"
1017 1018
                  <+> ppr arg_ty)
       ; arg_ty' <- applySubstTy arg_ty
1019
       ; lintTyApp fun_ty arg_ty' }
1020 1021

lintCoreArg fun_ty arg
lukemaurer's avatar
lukemaurer committed
1022
  = do { arg_ty <- markAllJoinsBad $ lintCoreExpr arg
1023 1024 1025 1026 1027 1028
           -- See Note [Levity polymorphism invariants] in CoreSyn
       ; lintL (not (isTypeLevPoly arg_ty))
           (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

1029
       ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
1030
                (mkLetAppMsg arg)
1031
       ; lintValApp arg fun_ty arg_ty }
1032 1033 1034

-----------------
lintAltBinders :: OutType     -- Scrutinee type
1035
               -> OutType     -- Constructor type
1036 1037
               -> [OutVar]    -- Binders
               -> LintM ()
1038 1039
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
1040
lintAltBinders scrut_ty con_ty []
1041
  = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
1042
lintAltBinders scrut_ty con_ty (bndr:bndrs)
1043
  | isTyVar bndr
1044 1045 1046 1047
  = 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)
1048
       ; lintAltBinders scrut_ty con_ty' bndrs }
1049 1050 1051 1052

-----------------
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp fun_ty arg_ty
1053 1054
  | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
  = do  { lintTyKind tv arg_ty
1055 1056 1057
        ; in_scope <- getInScope
        -- substTy needs the set of tyvars in scope to avoid generating
        -- uniques that are already in scope.
1058
        -- See Note [The substitution invariant] in TyCoRep
1059
        ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
1060

1061 1062
  | otherwise
  = failWithL (mkTyAppMsg fun_ty arg_ty)
1063

1064 1065 1066 1067
-----------------
lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
lintValApp arg fun_ty arg_ty
  | Just (arg,res) <- splitFunTy_maybe fun_ty
1068
  = do { ensureEqTys arg arg_ty err1
1069 1070 1071 1072 1073 1074
       ; return res }
  | otherwise
  = failWithL err2
  where
    err1 = mkAppMsg       fun_ty arg_ty arg
    err2 = mkNonFunAppMsg fun_ty arg_ty arg
1075

1076
lintTyKind :: OutTyVar -> OutType -> LintM ()
1077
-- Both args have had substitution applied
1078 1079 1080

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
1081
lintTyKind tyvar arg_ty
1082 1083 1084 1085
        -- 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.
1086
  = do { arg_kind <- lintType arg_ty
1087
       ; unless (arg_kind `eqType` tyvar_kind)
Ben Gamari's avatar
Ben Gamari committed
1088
                (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))) }