CoreLint.hs 80.9 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,
Peter Wortmann's avatar
Peter Wortmann committed
14
    lintAnnots,
15
16

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

22
#include "HsVersions.h"
23
24

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

import HscTypes
import DynFlags
64
import Control.Monad
quchen's avatar
quchen committed
65
66
67
#if __GLASGOW_HASKELL__ > 710
import qualified Control.Monad.Fail as MonadFail
#endif
68
import MonadUtils
69
import Data.Function (fix)
Simon Marlow's avatar
Simon Marlow committed
70
import Data.Maybe
71
import Pair
72
import qualified GHC.LanguageExtensions as LangExt
73

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

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

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

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

Outstanding issues:

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

131

132
133
Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
134
In the desugarer, it's very very convenient to be able to say (in effect)
135
        let a = Type Int in <body>
136
137
138
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
139
reject a correct program.  So we carry a type substitution (in this example
140
[a -> Int]) and apply this substitution before comparing types.  The functin
141
142
        lintInTy :: Type -> LintM (Type, Kind)
returns a substituted type.
143
144
145
146

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

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

151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
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.

170
171
172
173
174
175
176
177
178
************************************************************************
*                                                                      *
                 Beginning and ending passes
*                                                                      *
************************************************************************

These functions are not CoreM monad stuff, but they probably ought to
be, and it makes a conveneint place.  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
179
-}
180

181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
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
  | Just flag <- mb_flag
  = Err.dumpSDoc dflags unqual flag (showSDoc dflags hdr) dump_doc

  | otherwise
  = Err.debugTraceMsg dflags 2 size_doc
          -- Report result size
          -- This has the side effect of forcing the intermediate to be evaluated

  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
228
                     , pprCoreBindingsWithSize binds
229
230
                     , ppUnless (null rules) pp_rules ]
    pp_rules = vcat [ blankLine
231
                    , text "------ Local rules for imported ids --------"
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
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
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
coreDumpFlag CoreDoVectorisation      = Just Opt_D_dump_vect
coreDumpFlag CoreDesugar              = Just Opt_D_dump_ds
coreDumpFlag CoreDesugarOpt           = Just Opt_D_dump_ds
coreDumpFlag CoreTidy                 = Just Opt_D_dump_simpl
coreDumpFlag CorePrep                 = Just Opt_D_dump_prep

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
271
  = do { let (warns, errs) = lintCoreBindings dflags pass (interactiveInScope hsc_env) binds
272
273
274
275
276
277
278
279
280
281
       ; 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)
282
  = do { log_action dflags dflags NoReason Err.SevDump noSrcSpan defaultDumpStyle
283
           (vcat [ lint_banner "errors" (ppr pass), Err.pprMessageBag errs
284
                 , text "*** Offending Program ***"
285
                 , pprCoreBindings binds
286
                 , text "*** End of Offense ***" ])
287
288
289
290
291
       ; Err.ghcExit dflags 1 }

  | not (isEmptyBag warns)
  , not opt_NoDebugOutput
  , showLintWarnings pass
292
  = log_action dflags dflags NoReason Err.SevDump noSrcSpan defaultDumpStyle
293
294
295
296
297
298
        (lint_banner "warnings" (ppr pass) $$ Err.pprMessageBag warns)

  | otherwise = return ()
  where

lint_banner :: String -> SDoc -> SDoc
299
300
301
lint_banner string pass = text "*** Core Lint"      <+> text string
                          <+> text ": in result of" <+> pass
                          <+> text "***"
302
303
304
305
306
307
308
309
310
311
312

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 ()
313
  | Just err <- lintExpr dflags (interactiveInScope hsc_env) expr
314
315
316
317
318
319
320
321
  = do { display_lint_err err
       ; Err.ghcExit dflags 1 }
  | otherwise
  = return ()
  where
    dflags = hsc_dflags hsc_env

    display_lint_err err
322
323
      = do { log_action dflags dflags NoReason Err.SevDump
               noSrcSpan defaultDumpStyle
324
325
               (vcat [ lint_banner "errors" (text what)
                     , err
326
                     , text "*** Offending Program ***"
327
                     , pprCoreExpr expr
328
                     , text "*** End of Offense ***" ])
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
           ; 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
344
  = tyvars ++ ids
345
346
347
348
349
350
351
  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
352
    tyvars = tyCoVarsOfTypesList $ map idType ids
353
354
355
356
357
              -- 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)

358
lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc, Bag MsgDoc)
359
--   Returns (warnings, errors)
360
361
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
362
363
lintCoreBindings dflags pass local_in_scope binds
  = initL dflags flags $
364
365
366
    addLoc TopLevelBindings        $
    addInScopeVars local_in_scope  $
    addInScopeVars binders         $
367
368
369
        -- Put all the top-level binders in scope at the start
        -- This is because transformation rules can bring something
        -- into use 'unexpectedly'
370
371
372
373
    do { checkL (null dups) (dupVars dups)
       ; checkL (null ext_dups) (dupExtVars ext_dups)
       ; mapM lint_bind binds }
  where
374
    flags = LF { lf_check_global_ids = check_globals
375
376
               , lf_check_inline_loop_breakers = check_lbs
               , lf_check_static_ptrs = check_static_ptrs }
377
378
379
380
381
382
383

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

384
385
386
387
388
389
    -- See Note [Checking for INLINE loop breakers]
    check_lbs = case pass of
                      CoreDesugar    -> False
                      CoreDesugarOpt -> False
                      _              -> True

390
391
392
393
394
395
396
397
    -- See Note [Checking StaticPtrs]
    check_static_ptrs = xopt LangExt.StaticPointers dflags &&
                        case pass of
                          CoreDoFloatOutwards _ -> True
                          CoreTidy              -> True
                          CorePrep              -> True
                          _                     -> False

398
399
400
401
402
403
404
405
    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
406
    -- because they both get the same linker symbol
407
408
409
410
411
    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
412

413
414
    -- If you edit this function, you may need to update the GHC formalism
    -- See Note [GHC Formalism]
415
    lint_bind (Rec prs)         = mapM_ (lintSingleBinding TopLevel Recursive) prs
416
    lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
417

Austin Seipp's avatar
Austin Seipp committed
418
419
420
{-
************************************************************************
*                                                                      *
421
\subsection[lintUnfolding]{lintUnfolding}
Austin Seipp's avatar
Austin Seipp committed
422
423
*                                                                      *
************************************************************************
424

425
426
We use this to check all unfoldings that come in from interfaces
(it is very painful to catch errors otherwise):
Austin Seipp's avatar
Austin Seipp committed
427
-}
428

429
430
lintUnfolding :: DynFlags
              -> SrcLoc
431
432
433
              -> [Var]          -- Treat these as in scope
              -> CoreExpr
              -> Maybe MsgDoc   -- Nothing => OK
434

435
lintUnfolding dflags locn vars expr
436
  | isEmptyBag errs = Nothing
437
  | otherwise       = Just (pprMessageBag errs)
438
  where
439
    (_warns, errs) = initL dflags defaultLintFlags linter
440
441
442
    linter = addLoc (ImportedUnfolding locn) $
             addInScopeVars vars             $
             lintCoreExpr expr
443

444
445
lintExpr :: DynFlags
         -> [Var]               -- Treat these as in scope
446
447
         -> CoreExpr
         -> Maybe MsgDoc        -- Nothing => OK
448

449
lintExpr dflags vars expr
450
451
452
  | isEmptyBag errs = Nothing
  | otherwise       = Just (pprMessageBag errs)
  where
453
    (_warns, errs) = initL dflags defaultLintFlags linter
454
455
456
    linter = addLoc TopLevelBindings $
             addInScopeVars vars     $
             lintCoreExpr expr
457

Austin Seipp's avatar
Austin Seipp committed
458
459
460
{-
************************************************************************
*                                                                      *
461
\subsection[lintCoreBinding]{lintCoreBinding}
Austin Seipp's avatar
Austin Seipp committed
462
463
*                                                                      *
************************************************************************
464

465
Check a core binding, returning the list of variables bound.
Austin Seipp's avatar
Austin Seipp committed
466
-}
467

twanvl's avatar
twanvl committed
468
lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
469
470
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
471
lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
472
  = addLoc (RhsOf binder) $
473
         -- Check the rhs
474
    do { ty <- lintRhs rhs
475
       ; lintBinder binder -- Check match to RHS type
Simon Peyton Jones's avatar
Simon Peyton Jones committed
476
       ; binder_ty <- applySubstTy (idType binder)
477
       ; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
478

479
480
        -- Check the let/app invariant
        -- See Note [CoreSyn let/app invariant] in CoreSyn
481
       ; checkL (not (isUnliftedType binder_ty)
482
            || (isNonRec rec_flag && exprOkForSpeculation rhs))
483
           (mkRhsPrimMsg binder rhs)
484

485
486
487
488
        -- Check that if the binder is top-level or recursive, it's not demanded
       ; checkL (not (isStrictId binder)
            || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
           (mkStrictMsg binder)
489

490
491
492
        -- Check that if the binder is local, it is not marked as exported
       ; checkL (not (isExportedId binder) || isTopLevel top_lvl_flag)
           (mkNonTopExportedMsg binder)
493

494
495
496
        -- Check that if the binder is local, it does not have an external name
       ; checkL (not (isExternalName (Var.varName binder)) || isTopLevel top_lvl_flag)
           (mkNonTopExternalNameMsg binder)
497

498
499
500
501
       ; flags <- getLintFlags
       ; when (lf_check_inline_loop_breakers flags
               && isStrongLoopBreaker (idOccInfo binder)
               && isInlinePragma (idInlinePragma binder))
502
              (addWarnL (text "INLINE binder is (non-rule) loop breaker:" <+> ppr binder))
503
              -- Only non-rule loop breakers inhibit inlining
504

505
506
      -- Check whether arity and demand type are consistent (only if demand analysis
      -- already happened)
507
508
509
510
511
512
513
      --
      -- 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)
514

515
516
517
518
       -- 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]
       ; checkL (idArity binder <= length (typeArity (idType binder)))
519
520
           (text "idArity" <+> ppr (idArity binder) <+>
           text "exceeds typeArity" <+>
521
522
523
524
525
526
           ppr (length (typeArity (idType binder))) <> colon <+>
           ppr binder)

       ; case splitStrictSig (idStrictness binder) of
           (demands, result_info) | isBotRes result_info ->
             checkL (idArity binder <= length demands)
527
528
               (text "idArity" <+> ppr (idArity binder) <+>
               text "exceeds arity imposed by the strictness signature" <+>
529
530
531
532
               ppr (idStrictness binder) <> colon <+>
               ppr binder)
           _ -> return ()

Simon Peyton Jones's avatar
Simon Peyton Jones committed
533
       ; mapM_ (lintCoreRule binder_ty) (idCoreRules binder)
534
       ; lintIdUnfolding binder binder_ty (idUnfolding binder) }
535
536
537

        -- We should check the unfolding, if any, but this is tricky because
        -- the unfolding is a SimplifiableCoreExpr. Give up for now.
538
   where
539
540
    -- If you edit this function, you may need to update the GHC formalism
    -- See Note [GHC Formalism]
541
    lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
542
                   | otherwise = return ()
543

544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
-- | Checks the RHS of top-level bindings. It only differs from 'lintCoreExpr'
-- in that it doesn't reject applications of the data constructor @StaticPtr@
-- when they appear at the top level.
--
-- See Note [Checking StaticPtrs].
lintRhs :: CoreExpr -> LintM OutType
-- Allow applications of the data constructor @StaticPtr@ at the top
-- but produce errors otherwise.
lintRhs rhs
    | (binders0, rhs') <- collectTyBinders rhs
    , (fun@(Var b), args) <- collectArgs rhs'
    , Just con <- isDataConId_maybe b
    , dataConName con == staticPtrDataConName
    , length args == 5
    = flip fix binders0 $ \loopBinders binders -> case binders of
        -- imitate @lintCoreExpr (Lam ...)@
        var : vars -> addLoc (LambdaBodyOf var) $ lintBinder var $ \var' -> do
          body_ty <- loopBinders vars
          return $ mkPiType var' body_ty
        -- imitate @lintCoreExpr (App ...)@
        [] -> do
          fun_ty <- lintCoreExpr fun
          addLoc (AnExpr rhs') $ foldM lintCoreArg fun_ty args
-- Rejects applications of the data constructor @StaticPtr@ if it finds any.
lintRhs rhs = lintCoreExpr rhs

570
571
572
573
lintIdUnfolding :: Id -> Type -> Unfolding -> LintM ()
lintIdUnfolding bndr bndr_ty (CoreUnfolding { uf_tmpl = rhs, uf_src = src })
  | isStableSource src
  = do { ty <- lintCoreExpr rhs
574
       ; ensureEqTys bndr_ty ty (mkRhsMsg bndr (text "unfolding") ty) }
575
lintIdUnfolding  _ _ _
Gabor Greif's avatar
Gabor Greif committed
576
  = return ()       -- Do not Lint unstable unfoldings, because that leads
Simon Peyton Jones's avatar
Simon Peyton Jones committed
577
                    -- to exponential behaviour; c.f. CoreFVs.idUnfoldingVars
578

Austin Seipp's avatar
Austin Seipp committed
579
{-
580
581
582
583
584
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
585
that form a mutually recursive group.  Only after a round of
586
587
588
simplification are they unravelled.  So we suppress the test for
the desugarer.

Austin Seipp's avatar
Austin Seipp committed
589
590
************************************************************************
*                                                                      *
591
\subsection[lintCoreExpr]{lintCoreExpr}
Austin Seipp's avatar
Austin Seipp committed
592
593
594
*                                                                      *
************************************************************************
-}
595

596
type InType      = Type
597
598
type InCoercion  = Coercion
type InVar       = Var
599
600
type InTyVar     = Var
type InCoVar     = Var
601

602
type OutType     = Type -- Substitution has been applied to this,
603
                        -- but has not been linted yet
604
type OutKind     = Kind
605
606

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

609
610
611
612
type OutCoercion    = Coercion
type OutVar         = Var
type OutTyVar       = TyVar
type OutCoVar       = Var
613

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

621
622
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
623
lintCoreExpr (Var var)
624
  = do  { checkL (isNonCoVarId var)
625
                 (text "Non term variable" <+> ppr var)
626

627
        ; checkDeadIdOcc var
628
        ; var' <- lookupIdInScope var
simonpj@microsoft.com's avatar
simonpj@microsoft.com committed
629
        ; return (idType var') }
630

631
632
lintCoreExpr (Lit lit)
  = return (literalType lit)
633

634
635
lintCoreExpr (Cast expr co)
  = do { expr_ty <- lintCoreExpr expr
636
       ; co' <- applySubstCo co
637
638
       ; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
       ; lintL (classifiesTypeWithValues k2)
639
               (text "Target of cast not # or *:" <+> ppr co)
640
641
       ; lintRole co' Representational r
       ; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
642
       ; return to_ty }
643

644
645
646
647
648
649
650
lintCoreExpr (Tick (Breakpoint _ ids) expr)
  = do forM_ ids $ \id -> do
         checkDeadIdOcc id
         lookupIdInScope id
       lintCoreExpr expr

lintCoreExpr (Tick _other_tickish expr)
651
  = lintCoreExpr expr
652

653
lintCoreExpr (Let (NonRec tv (Type ty)) body)
654
  | isTyVar tv
655
656
657
  =     -- See Note [Linting type lets]
    do  { ty' <- applySubstTy ty
        ; lintTyBndr tv              $ \ tv' ->
658
    do  { addLoc (RhsOf tv) $ lintTyKind tv' ty'
659
660
661
662
                -- Now extend the substitution so we
                -- take advantage of it in the body
        ; extendSubstL tv' ty'       $
          addLoc (BodyOfLetRec [tv]) $
663
          lintCoreExpr body } }
664

665
lintCoreExpr (Let (NonRec bndr rhs) body)
666
  | isId bndr
667
668
669
  = do  { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
        ; addLoc (BodyOfLetRec [bndr])
                 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
670

671
  | otherwise
672
  = failWithL (mkLetErr bndr rhs)       -- Not quite accurate
673

674
675
676
677
678
lintCoreExpr (Let (Rec pairs) body)
  = lintAndScopeIds bndrs       $ \_ ->
    do  { checkL (null dups) (dupVars dups)
        ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
        ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
679
680
  where
    bndrs = map fst pairs
681
    (_, dups) = removeDups compare bndrs
682

batterseapower's avatar
batterseapower committed
683
lintCoreExpr e@(App _ _)
684
685
686
687
688
689
690
691
692
693
694
    = do lf <- getLintFlags
         -- Check for a nested occurrence of the StaticPtr constructor.
         -- See Note [Checking StaticPtrs].
         case fun of
           Var b | lf_check_static_ptrs lf
                 , Just con <- isDataConId_maybe b
                 , dataConName con == staticPtrDataConName
                 -> do
              failWithL $ text "Found StaticPtr nested in an expression: " <+>
                          ppr e
           _     -> go
batterseapower's avatar
batterseapower committed
695
  where
696
697
698
    go = do { fun_ty <- lintCoreExpr fun
            ; addLoc (AnExpr e) $ foldM lintCoreArg fun_ty args }

batterseapower's avatar
batterseapower committed
699
    (fun, args) = collectArgs e
700
701

lintCoreExpr (Lam var expr)
702
  = addLoc (LambdaBodyOf var) $
703
704
    lintBinder var $ \ var' ->
    do { body_ty <- lintCoreExpr expr
705
       ; return $ mkPiType var' body_ty }
706
707
708

lintCoreExpr e@(Case scrut var alt_ty alts) =
       -- Check the scrutinee
709
710
  do { let scrut_diverges = exprIsBottom scrut
     ; scrut_ty <- lintCoreExpr scrut
711
712
     ; (alt_ty, _) <- lintInTy alt_ty
     ; (var_ty, _) <- lintInTy (idType var)
713

714
     -- See Note [No alternatives lint check]
715
716
     ; when (null alts) $
     do { checkL (not (exprIsHNF scrut))
717
          (text "No alternatives for a case scrutinee in head-normal form:" <+> ppr scrut)
718
        ; checkL scrut_diverges
719
          (text "No alternatives for a case scrutinee not known to diverge for sure:" <+> ppr scrut)
720
        }
721

Ben Gamari's avatar
Ben Gamari committed
722
723
724
725
726
727
728
729
730
     -- 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)

731
     ; case tyConAppTyCon_maybe (idType var) of
732
         Just tycon
733
734
735
736
737
738
              | 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))
739
                        -- This can legitimately happen for type families
740
741
742
                      $ return ()
         _otherwise -> return ()

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

745
746
     ; subst <- getTCvSubst
     ; ensureEqTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
747

748
     ; lintAndScopeId var $ \_ ->
749
       do { -- Check the alternatives
750
            mapM_ (lintCoreAlt scrut_ty alt_ty) alts
751
          ; checkCaseAlts e scrut_ty alts
752
          ; return alt_ty } }
753

754
755
-- This case can't happen; linting types in expressions gets routed through
-- lintCoreArgs
756
lintCoreExpr (Type ty)
757
  = failWithL (text "Type found as expression" <+> ppr ty)
758
759

lintCoreExpr (Coercion co)
760
761
  = do { (k1, k2, ty1, ty2, role) <- lintInCo co
       ; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
762

Austin Seipp's avatar
Austin Seipp committed
763
{-
764
765
766
Note [No alternatives lint check]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Case expressions with no alternatives are odd beasts, and worth looking at
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
in the linter (cf Trac #10180).  We check two things:

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

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

In principle, the first check is redundant: exprIsBottom == True will
always imply exprIsHNF == False.  But the first check is reliable: If
exprIsHNF == True, then there definitely is a problem (exprIsHNF errs
on the right side).  If the second check triggers then it may be the
case that the compiler got smarter elsewhere, and the empty case is
correct, but that exprIsBottom is unable to see it. In particular, the
empty-type check in exprIsBottom is an approximation. Therefore, this
check is not fully reliable, and we keep both around.
783

Austin Seipp's avatar
Austin Seipp committed
784
785
************************************************************************
*                                                                      *
786
\subsection[lintCoreArgs]{lintCoreArgs}
Austin Seipp's avatar
Austin Seipp committed
787
788
*                                                                      *
************************************************************************
789

790
791
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
792
-}
793

794
lintCoreArg  :: OutType -> CoreArg -> LintM OutType
795
lintCoreArg fun_ty (Type arg_ty)
796
  = do { checkL (not (isCoercionTy arg_ty))
797
                (text "Unnecessary coercion-to-type injection:"
798
799
                  <+> ppr arg_ty)
       ; arg_ty' <- applySubstTy arg_ty
800
       ; lintTyApp fun_ty arg_ty' }
801
802

lintCoreArg fun_ty arg
803
  = do { arg_ty <- lintCoreExpr arg
804
       ; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
805
                (mkLetAppMsg arg)
806
       ; lintValApp arg fun_ty arg_ty }
807
808
809

-----------------
lintAltBinders :: OutType     -- Scrutinee type
810
               -> OutType     -- Constructor type
811
812
               -> [OutVar]    -- Binders
               -> LintM ()
813
814
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
815
lintAltBinders scrut_ty con_ty []
816
  = ensureEqTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
817
lintAltBinders scrut_ty con_ty (bndr:bndrs)
818
  | isTyVar bndr
819
820
821
822
  = 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)
823
       ; lintAltBinders scrut_ty con_ty' bndrs }
824
825
826
827

-----------------
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp fun_ty arg_ty
828
829
  | Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
  = do  { lintTyKind tv arg_ty
830
831
832
        ; in_scope <- getInScope
        -- substTy needs the set of tyvars in scope to avoid generating
        -- uniques that are already in scope.
833
        -- See Note [The substitution invariant] in TyCoRep
834
        ; return (substTyWithInScope in_scope [tv] [arg_ty] body_ty) }
835

836
837
  | otherwise
  = failWithL (mkTyAppMsg fun_ty arg_ty)
838

839
840
841
842
-----------------
lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
lintValApp arg fun_ty arg_ty
  | Just (arg,res) <- splitFunTy_maybe fun_ty
843
  = do { ensureEqTys arg arg_ty err1
844
845
846
847
848
849
       ; return res }
  | otherwise
  = failWithL err2
  where
    err1 = mkAppMsg       fun_ty arg_ty arg
    err2 = mkNonFunAppMsg fun_ty arg_ty arg
850

851
lintTyKind :: OutTyVar -> OutType -> LintM ()
852
-- Both args have had substitution applied
853
854
855

-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
856
lintTyKind tyvar arg_ty
857
858
859
860
        -- 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.
861
  = do { arg_kind <- lintType arg_ty
862
       ; unless (arg_kind `eqType` tyvar_kind)
863
                (addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
864
865
  where
    tyvar_kind = tyVarKind tyvar
866

867
868
869
870
871
872
873
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
874
                (text "Occurrence of a dead Id" <+> ppr id) }
875
876
  | otherwise
  = return ()
877

Austin Seipp's avatar
Austin Seipp committed
878
879
880
{-
************************************************************************
*                                                                      *
881
\subsection[lintCoreAlts]{lintCoreAlts}
Austin Seipp's avatar
Austin Seipp committed
882
883
884
*                                                                      *
************************************************************************
-}
885

886
checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
887
-- a) Check that the alts are non-empty
888
889
-- b1) Check that the DEFAULT comes first, if it exists
-- b2) Check that the others are in increasing order
890
891
-- c) Check that there's a default for infinite types
-- NB: Algebraic cases are not necessarily exhaustive, because
892
--     the simplifer correctly eliminates case that can't
893
894
--     possibly match.

895
checkCaseAlts e ty alts =
896
  do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
897
     ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
898
899
900
901
902
903
904
905

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

912
        -- Check that successive alternatives have increasing tags
913
    increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
twanvl's avatar
twanvl committed
914
    increasing_tag _                         = True
915

916
    non_deflt (DEFAULT, _, _) = False
twanvl's avatar
twanvl committed
917
    non_deflt _               = True
918

919
920
921
    is_infinite_ty = case tyConAppTyCon_maybe ty of
                        Nothing    -> False
                        Just tycon -> isPrimTyCon tycon
922

923
924
lintAltExpr :: CoreExpr -> OutType -> LintM ()
lintAltExpr expr ann_ty
925
  = do { actual_ty <- lintCoreExpr expr
926
       ; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
927

928
lintCoreAlt :: OutType          -- Type of scrutinee
929
            -> OutType          -- Type of the alternative
930
931
            -> CoreAlt
            -> LintM ()
932
933
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
twanvl's avatar
twanvl committed
934
lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
935
936
  do { lintL (null args) (mkDefaultArgsMsg args)
     ; lintAltExpr rhs alt_ty }
937

938
lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
939
940
  | litIsLifted lit
  = failWithL integerScrutinisedMsg
941
  | otherwise
942
943
944
  = do { lintL (null args) (mkDefaultArgsMsg args)
       ; ensureEqTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
       ; lintAltExpr rhs alt_ty }
945
946
  where
    lit_ty = literalType lit
947

948
lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
949
  | isNewTyCon (dataConTyCon con)
950
  = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
951
  | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
952
  = addLoc (CaseAlt alt) $  do
953
954
955
    {   -- First instantiate the universally quantified
        -- type variables of the data constructor
        -- We've already check
956
      lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
957
    ; let con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
958

959
        -- And now bring the new binders into scope
960
961
    ; lintBinders args $ \ args' -> do
    { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
962
    ; lintAltExpr rhs alt_ty } }
963

964
  | otherwise   -- Scrut-ty is wrong shape
965
  = addErrL (mkBadAltMsg scrut_ty alt)
966

Austin Seipp's avatar
Austin Seipp committed
967
968
969
{-
************************************************************************
*                                                                      *
970
\subsection[lint-types]{Types}
Austin Seipp's avatar
Austin Seipp committed
971
972
973
*                                                                      *
************************************************************************
-}
sof's avatar
sof committed
974

975
976
977
978
979
980