compiler/coreSyn/CoreLint.lhs

   1 %
   2 % (c) The University of Glasgow 2006
   3 % (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
   4 %
   5
   6 A ``lint'' pass to check for Core correctness
   7
   8 \begin{code}
   9 module CoreLint (
  10         lintCoreBindings,
  11         lintUnfolding,
  12         showPass, endPass
  13     ) where
  14
  15 #include "HsVersions.h"
  16
  17 import CoreSyn
  18 import CoreFVs
  19 import CoreUtils
  20 import Bag
  21 import Literal
  22 import DataCon
  23 import TysWiredIn
  24 import Var
  25 import VarEnv
  26 import VarSet
  27 import Name
  28 import PprCore
  29 import ErrUtils
  30 import SrcLoc
  31 import Type
  32 import Coercion
  33 import TyCon
  34 import BasicTypes
  35 import StaticFlags
  36 import DynFlags
  37 import Outputable
  38
  39 #ifdef DEBUG
  40 import Util             ( notNull )
  41 #endif
  42
  43 import Data.Maybe
  44 \end{code}
  45
  46 %************************************************************************
  47 %*                                                                      *
  48 \subsection{End pass}
  49 %*                                                                      *
  50 %************************************************************************
  51
  52 @showPass@ and @endPass@ don't really belong here, but it makes a convenient
  53 place for them.  They print out stuff before and after core passes,
  54 and do Core Lint when necessary.
  55
  56 \begin{code}
  57 endPass :: DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
  58 endPass dflags pass_name dump_flag binds
  59   = do
  60         -- Report result size if required
  61         -- This has the side effect of forcing the intermediate to be evaluated
  62         debugTraceMsg dflags 2 $
  63                 (text "    Result size =" <+> int (coreBindsSize binds))
  64
  65         -- Report verbosely, if required
  66         dumpIfSet_core dflags dump_flag pass_name (pprCoreBindings binds)
  67
  68         -- Type check
  69         lintCoreBindings dflags pass_name binds
  70
  71         return binds
  72 \end{code}
  73
  74
  75 %************************************************************************
  76 %*                                                                      *
  77 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
  78 %*                                                                      *
  79 %************************************************************************
  80
  81 Checks that a set of core bindings is well-formed.  The PprStyle and String
  82 just control what we print in the event of an error.  The Bool value
  83 indicates whether we have done any specialisation yet (in which case we do
  84 some extra checks).
  85
  86 We check for
  87         (a) type errors
  88         (b) Out-of-scope type variables
  89         (c) Out-of-scope local variables
  90         (d) Ill-kinded types
  91
  92 If we have done specialisation the we check that there are
  93         (a) No top-level bindings of primitive (unboxed type)
  94
  95 Outstanding issues:
  96
  97     --
  98     -- Things are *not* OK if:
  99     --
 100     --  * Unsaturated type app before specialisation has been done;
 101     --
 102     --  * Oversaturated type app after specialisation (eta reduction
 103     --   may well be happening...);
 104
 105
 106 Note [Type lets]
 107 ~~~~~~~~~~~~~~~~
 108 In the desugarer, it's very very convenient to be able to say (in effect)
 109         let a = Int in <body>
 110 That is, use a type let.  (See notes just below for why we want this.)
 111
 112 We don't have type lets in Core, so the desugarer uses type lambda
 113         (/\a. <body>) Int
 114 However, in the lambda form, we'd get lint errors from:
 115         (/\a. let x::a = 4 in <body>) Int
 116 because (x::a) doesn't look compatible with (4::Int).
 117
 118 So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
 119 as it were.  It carries a type substitution (in this example [a -> Int])
 120 and applies this substitution before comparing types.  The functin
 121         lintTy :: Type -> LintM Type
 122 returns a substituted type; that's the only reason it returns anything.
 123
 124 When we encounter a binder (like x::a) we must apply the substitution
 125 to the type of the binding variable.  lintBinders does this.
 126
 127 For Ids, the type-substituted Id is added to the in_scope set (which
 128 itself is part of the TvSubst we are carrying down), and when we
 129 find an occurence of an Id, we fetch it from the in-scope set.
 130
 131
 132 Why we need type let
 133 ~~~~~~~~~~~~~~~~~~~~
 134 It's needed when dealing with desugarer output for GADTs. Consider
 135   data T = forall a. T a (a->Int) Bool
 136    f :: T -> ... ->
 137    f (T x f True)  = <e1>
 138    f (T y g False) = <e2>
 139 After desugaring we get
 140         f t b = case t of
 141                   T a (x::a) (f::a->Int) (b:Bool) ->
 142                     case b of
 143                         True -> <e1>
 144                         False -> (/\b. let y=x; g=f in <e2>) a
 145 And for a reason I now forget, the ...<e2>... can mention a; so
 146 we want Lint to know that b=a.  Ugh.
 147
 148 I tried quite hard to make the necessity for this go away, by changing the
 149 desugarer, but the fundamental problem is this:
 150
 151         T a (x::a) (y::Int) -> let fail::a = ...
 152                                in (/\b. ...(case ... of
 153                                                 True  -> x::b
 154                                                 False -> fail)
 155                                   ) a
 156 Now the inner case look as though it has incompatible branches.
 157
 158
 159 \begin{code}
 160 lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
 161
 162 lintCoreBindings dflags whoDunnit binds
 163   | not (dopt Opt_DoCoreLinting dflags)
 164   = return ()
 165
 166 lintCoreBindings dflags whoDunnit binds
 167   = case (initL (lint_binds binds)) of
 168       Nothing       -> showPass dflags ("Core Linted result of " ++ whoDunnit)
 169       Just bad_news -> printDump (display bad_news)     >>
 170                        ghcExit dflags 1
 171   where
 172         -- Put all the top-level binders in scope at the start
 173         -- This is because transformation rules can bring something
 174         -- into use 'unexpectedly'
 175     lint_binds binds = addInScopeVars (bindersOfBinds binds) $
 176                        mapM lint_bind binds
 177
 178     lint_bind (Rec prs)         = mapM_ (lintSingleBinding Recursive) prs
 179     lint_bind (NonRec bndr rhs) = lintSingleBinding NonRecursive (bndr,rhs)
 180
 181     display bad_news
 182       = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
 183                 bad_news,
 184                 ptext SLIT("*** Offending Program ***"),
 185                 pprCoreBindings binds,
 186                 ptext SLIT("*** End of Offense ***")
 187         ]
 188 \end{code}
 189
 190 %************************************************************************
 191 %*                                                                      *
 192 \subsection[lintUnfolding]{lintUnfolding}
 193 %*                                                                      *
 194 %************************************************************************
 195
 196 We use this to check all unfoldings that come in from interfaces
 197 (it is very painful to catch errors otherwise):
 198
 199 \begin{code}
 200 lintUnfolding :: SrcLoc
 201               -> [Var]          -- Treat these as in scope
 202               -> CoreExpr
 203               -> Maybe Message  -- Nothing => OK
 204
 205 lintUnfolding locn vars expr
 206   = initL (addLoc (ImportedUnfolding locn) $
 207            addInScopeVars vars             $
 208            lintCoreExpr expr)
 209 \end{code}
 210
 211 %************************************************************************
 212 %*                                                                      *
 213 \subsection[lintCoreBinding]{lintCoreBinding}
 214 %*                                                                      *
 215 %************************************************************************
 216
 217 Check a core binding, returning the list of variables bound.
 218
 219 \begin{code}
 220 lintSingleBinding rec_flag (binder,rhs)
 221   = addLoc (RhsOf binder) $
 222          -- Check the rhs
 223     do { ty <- lintCoreExpr rhs
 224        ; lintBinder binder -- Check match to RHS type
 225        ; binder_ty <- applySubst binder_ty
 226        ; checkTys binder_ty ty (mkRhsMsg binder ty)
 227         -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
 228        ; checkL (not (isUnLiftedType binder_ty)
 229             || (isNonRec rec_flag && exprOkForSpeculation rhs))
 230            (mkRhsPrimMsg binder rhs)
 231         -- Check whether binder's specialisations contain any out-of-scope variables
 232        ; mapM_ (checkBndrIdInScope binder) bndr_vars }
 233
 234         -- We should check the unfolding, if any, but this is tricky because
 235         -- the unfolding is a SimplifiableCoreExpr. Give up for now.
 236   where
 237     binder_ty = idType binder
 238     bndr_vars = varSetElems (idFreeVars binder)
 239     lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
 240                    | otherwise = return ()
 241 \end{code}
 242
 243 %************************************************************************
 244 %*                                                                      *
 245 \subsection[lintCoreExpr]{lintCoreExpr}
 246 %*                                                                      *
 247 %************************************************************************
 248
 249 \begin{code}
 250 type InType  = Type     -- Substitution not yet applied
 251 type OutType = Type     -- Substitution has been applied to this
 252
 253 lintCoreExpr :: CoreExpr -> LintM OutType
 254 -- The returned type has the substitution from the monad
 255 -- already applied to it:
 256 --      lintCoreExpr e subst = exprType (subst e)
 257
 258 lintCoreExpr (Var var)
 259   = do  { checkL (not (var == oneTupleDataConId))
 260                  (ptext SLIT("Illegal one-tuple"))
 261         ; var' <- lookupIdInScope var
 262         ; return (idType var')
 263         }
 264
 265 lintCoreExpr (Lit lit)
 266   = return (literalType lit)
 267
 268 --lintCoreExpr (Note (Coerce to_ty from_ty) expr)
 269 --  = do        { expr_ty <- lintCoreExpr expr
 270 --      ; to_ty <- lintTy to_ty
 271 --      ; from_ty <- lintTy from_ty
 272 --      ; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
 273 --      ; return to_ty }
 274
 275 lintCoreExpr (Cast expr co)
 276   = do { expr_ty <- lintCoreExpr expr
 277        ; co' <- lintTy co
 278        ; let (from_ty, to_ty) = coercionKind co'
 279        ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
 280        ; return to_ty }
 281
 282 lintCoreExpr (Note other_note expr)
 283   = lintCoreExpr expr
 284
 285 lintCoreExpr (Let (NonRec bndr rhs) body)
 286   = do  { lintSingleBinding NonRecursive (bndr,rhs)
 287         ; addLoc (BodyOfLetRec [bndr])
 288                  (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
 289
 290 lintCoreExpr (Let (Rec pairs) body)
 291   = lintAndScopeIds bndrs       $ \_ ->
 292     do  { mapM (lintSingleBinding Recursive) pairs
 293         ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
 294   where
 295     bndrs = map fst pairs
 296
 297 lintCoreExpr e@(App fun (Type ty))
 298 -- See Note [Type let] above
 299   = addLoc (AnExpr e) $
 300     go fun [ty]
 301   where
 302     go (App fun (Type ty)) tys
 303         = do { go fun (ty:tys) }
 304     go (Lam tv body) (ty:tys)
 305         = do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)        -- Not quite accurate
 306               ; ty' <- lintTy ty
 307               ; let kind = tyVarKind tv
 308               ; kind' <- lintTy kind
 309               ; let tv' = setTyVarKind tv kind'
 310               ; checkKinds tv' ty'
 311                 -- Now extend the substitution so we
 312                 -- take advantage of it in the body
 313               ; addInScopeVars [tv'] $
 314                 extendSubstL tv' ty' $
 315                 go body tys }
 316     go fun tys
 317         = do  { fun_ty <- lintCoreExpr fun
 318               ; lintCoreArgs fun_ty (map Type tys) }
 319
 320 lintCoreExpr e@(App fun arg)
 321   = do  { fun_ty <- lintCoreExpr fun
 322         ; addLoc (AnExpr e) $
 323           lintCoreArg fun_ty arg }
 324
 325 lintCoreExpr (Lam var expr)
 326   = addLoc (LambdaBodyOf var) $
 327     lintBinders [var] $ \[var'] ->
 328     do { body_ty <- lintCoreExpr expr
 329        ; if isId var' then
 330              return (mkFunTy (idType var') body_ty)
 331          else
 332              return (mkForAllTy var' body_ty)
 333        }
 334         -- The applySubst is needed to apply the subst to var
 335
 336 lintCoreExpr e@(Case scrut var alt_ty alts) =
 337        -- Check the scrutinee
 338   do { scrut_ty <- lintCoreExpr scrut
 339      ; alt_ty   <- lintTy alt_ty
 340      ; var_ty   <- lintTy (idType var)
 341         -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 342
 343      ; subst <- getTvSubst
 344      ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 345
 346      -- If the binder is an unboxed tuple type, don't put it in scope
 347      ; let scope = if (isUnboxedTupleType (idType var)) then
 348                        pass_var
 349                    else lintAndScopeId var
 350      ; scope $ \_ ->
 351        do { -- Check the alternatives
 352             checkCaseAlts e scrut_ty alts
 353           ; mapM (lintCoreAlt scrut_ty alt_ty) alts
 354           ; return alt_ty } }
 355   where
 356     pass_var f = f var
 357
 358 lintCoreExpr e@(Type ty)
 359   = addErrL (mkStrangeTyMsg e)
 360 \end{code}
 361
 362 %************************************************************************
 363 %*                                                                      *
 364 \subsection[lintCoreArgs]{lintCoreArgs}
 365 %*                                                                      *
 366 %************************************************************************
 367
 368 The basic version of these functions checks that the argument is a
 369 subtype of the required type, as one would expect.
 370
 371 \begin{code}
 372 lintCoreArgs :: Type -> [CoreArg] -> LintM Type
 373 lintCoreArg  :: Type -> CoreArg   -> LintM Type
 374 -- First argument has already had substitution applied to it
 375 \end{code}
 376
 377 \begin{code}
 378 lintCoreArgs ty [] = return ty
 379 lintCoreArgs ty (a : args) =
 380   do { res <- lintCoreArg ty a
 381      ; lintCoreArgs res args }
 382
 383 lintCoreArg fun_ty a@(Type arg_ty) =
 384   do { arg_ty <- lintTy arg_ty
 385      ; lintTyApp fun_ty arg_ty }
 386
 387 lintCoreArg fun_ty arg =
 388        -- Make sure function type matches argument
 389   do { arg_ty <- lintCoreExpr arg
 390      ; let err1 =  mkAppMsg fun_ty arg_ty arg
 391            err2 = mkNonFunAppMsg fun_ty arg_ty arg
 392      ; case splitFunTy_maybe fun_ty of
 393         Just (arg,res) ->
 394           do { checkTys arg arg_ty err1
 395              ; return res }
 396         _ -> addErrL err2 }
 397 \end{code}
 398
 399 \begin{code}
 400 -- Both args have had substitution applied
 401 lintTyApp ty arg_ty
 402   = case splitForAllTy_maybe ty of
 403       Nothing -> addErrL (mkTyAppMsg ty arg_ty)
 404
 405       Just (tyvar,body)
 406         -> do   { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
 407                 ; checkKinds tyvar arg_ty
 408                 ; return (substTyWith [tyvar] [arg_ty] body) }
 409
 410 checkKinds tyvar arg_ty
 411         -- Arg type might be boxed for a function with an uncommitted
 412         -- tyvar; notably this is used so that we can give
 413         --      error :: forall a:*. String -> a
 414         -- and then apply it to both boxed and unboxed types.
 415   = checkL (arg_kind `isSubKind` tyvar_kind)
 416            (mkKindErrMsg tyvar arg_ty)
 417   where
 418     tyvar_kind = tyVarKind tyvar
 419     arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
 420              | otherwise     = typeKind arg_ty
 421 \end{code}
 422
 423
 424 %************************************************************************
 425 %*                                                                      *
 426 \subsection[lintCoreAlts]{lintCoreAlts}
 427 %*                                                                      *
 428 %************************************************************************
 429
 430 \begin{code}
 431 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
 432 -- a) Check that the alts are non-empty
 433 -- b1) Check that the DEFAULT comes first, if it exists
 434 -- b2) Check that the others are in increasing order
 435 -- c) Check that there's a default for infinite types
 436 -- NB: Algebraic cases are not necessarily exhaustive, because
 437 --     the simplifer correctly eliminates case that can't
 438 --     possibly match.
 439
 440 checkCaseAlts e ty []
 441   = addErrL (mkNullAltsMsg e)
 442
 443 checkCaseAlts e ty alts =
 444   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
 445      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
 446      ; checkL (isJust maybe_deflt || not is_infinite_ty)
 447            (nonExhaustiveAltsMsg e) }
 448   where
 449     (con_alts, maybe_deflt) = findDefault alts
 450
 451         -- Check that successive alternatives have increasing tags
 452     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
 453     increasing_tag other                     = True
 454
 455     non_deflt (DEFAULT, _, _) = False
 456     non_deflt alt             = True
 457
 458     is_infinite_ty = case splitTyConApp_maybe ty of
 459                         Nothing                     -> False
 460                         Just (tycon, tycon_arg_tys) -> isPrimTyCon tycon
 461 \end{code}
 462
 463 \begin{code}
 464 checkAltExpr :: CoreExpr -> OutType -> LintM ()
 465 checkAltExpr expr ann_ty
 466   = do { actual_ty <- lintCoreExpr expr
 467        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
 468
 469 lintCoreAlt :: OutType          -- Type of scrutinee
 470             -> OutType          -- Type of the alternative
 471             -> CoreAlt
 472             -> LintM ()
 473
 474 lintCoreAlt scrut_ty alt_ty alt@(DEFAULT, args, rhs) =
 475   do { checkL (null args) (mkDefaultArgsMsg args)
 476      ; checkAltExpr rhs alt_ty }
 477
 478 lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) =
 479   do { checkL (null args) (mkDefaultArgsMsg args)
 480      ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
 481      ; checkAltExpr rhs alt_ty }
 482   where
 483     lit_ty = literalType lit
 484
 485 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
 486   | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
 487   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
 488   = addLoc (CaseAlt alt) $  do
 489     {   -- First instantiate the universally quantified
 490         -- type variables of the data constructor
 491       con_payload_ty <- lintCoreArgs (dataConRepType con) (map Type tycon_arg_tys)
 492
 493         -- And now bring the new binders into scope
 494     ; lintBinders args $ \ args -> do
 495     { addLoc (CasePat alt) $ do
 496           {    -- Check the pattern
 497                  -- Scrutinee type must be a tycon applicn; checked by caller
 498                  -- This code is remarkably compact considering what it does!
 499                  -- NB: args must be in scope here so that the lintCoreArgs line works.
 500                  -- NB: relies on existential type args coming *after* ordinary type args
 501
 502           ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
 503           ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
 504           }
 505                -- Check the RHS
 506     ; checkAltExpr rhs alt_ty } }
 507
 508   | otherwise   -- Scrut-ty is wrong shape
 509   = addErrL (mkBadAltMsg scrut_ty alt)
 510 \end{code}
 511
 512 %************************************************************************
 513 %*                                                                      *
 514 \subsection[lint-types]{Types}
 515 %*                                                                      *
 516 %************************************************************************
 517
 518 \begin{code}
 519 -- When we lint binders, we (one at a time and in order):
 520 --  1. Lint var types or kinds (possibly substituting)
 521 --  2. Add the binder to the in scope set, and if its a coercion var,
 522 --     we may extend the substitution to reflect its (possibly) new kind
 523 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
 524 lintBinders [] linterF = linterF []
 525 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 526                                  lintBinders vars $ \ vars' ->
 527                                  linterF (var':vars')
 528
 529 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 530 lintBinder var linterF
 531   | isTyVar var = lint_ty_bndr
 532   | otherwise   = lintIdBndr var linterF
 533   where
 534     lint_ty_bndr = do { lintTy (tyVarKind var)
 535                       ; subst <- getTvSubst
 536                       ; let (subst', tv') = substTyVarBndr subst var
 537                       ; updateTvSubst subst' (linterF tv') }
 538
 539 lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
 540 -- Do substitution on the type of a binder and add the var with this
 541 -- new type to the in-scope set of the second argument
 542 -- ToDo: lint its rules
 543 lintIdBndr id linterF
 544   = do  { checkL (not (isUnboxedTupleType (idType id)))
 545                  (mkUnboxedTupleMsg id)
 546                 -- No variable can be bound to an unboxed tuple.
 547         ; lintAndScopeId id $ \id' -> linterF id'
 548         }
 549
 550 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
 551 lintAndScopeIds ids linterF
 552   = go ids
 553   where
 554     go []       = linterF []
 555     go (id:ids) = do { lintAndScopeId id $ \id ->
 556                            lintAndScopeIds ids $ \ids ->
 557                            linterF (id:ids) }
 558
 559 lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
 560 lintAndScopeId id linterF
 561   = do { ty <- lintTy (idType id)
 562        ; let id' = setIdType id ty
 563        ; addInScopeVars [id'] $ (linterF id')
 564        }
 565
 566 lintTy :: InType -> LintM OutType
 567 -- Check the type, and apply the substitution to it
 568 -- ToDo: check the kind structure of the type
 569 lintTy ty
 570   = do  { ty' <- applySubst ty
 571         ; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
 572         ; return ty' }
 573 \end{code}
 574
 575
 576 %************************************************************************
 577 %*                                                                      *
 578 \subsection[lint-monad]{The Lint monad}
 579 %*                                                                      *
 580 %************************************************************************
 581
 582 \begin{code}
 583 newtype LintM a =
 584    LintM { unLintM ::
 585             [LintLocInfo] ->         -- Locations
 586             TvSubst ->               -- Current type substitution; we also use this
 587                                      -- to keep track of all the variables in scope,
 588                                      -- both Ids and TyVars
 589             Bag Message ->           -- Error messages so far
 590             (Maybe a, Bag Message) } -- Result and error messages (if any)
 591
 592 {-      Note [Type substitution]
 593         ~~~~~~~~~~~~~~~~~~~~~~~~
 594 Why do we need a type substitution?  Consider
 595         /\(a:*). \(x:a). /\(a:*). id a x
 596 This is ill typed, because (renaming variables) it is really
 597         /\(a:*). \(x:a). /\(b:*). id b x
 598 Hence, when checking an application, we can't naively compare x's type
 599 (at its binding site) with its expected type (at a use site).  So we
 600 rename type binders as we go, maintaining a substitution.
 601
 602 The same substitution also supports let-type, current expressed as
 603         (/\(a:*). body) ty
 604 Here we substitute 'ty' for 'a' in 'body', on the fly.
 605 -}
 606
 607 instance Monad LintM where
 608   return x = LintM (\ loc subst errs -> (Just x, errs))
 609   fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
 610   m >>= k  = LintM (\ loc subst errs ->
 611                        let (res, errs') = unLintM m loc subst errs in
 612                          case res of
 613                            Just r -> unLintM (k r) loc subst errs'
 614                            Nothing -> (Nothing, errs'))
 615
 616 data LintLocInfo
 617   = RhsOf Id            -- The variable bound
 618   | LambdaBodyOf Id     -- The lambda-binder
 619   | BodyOfLetRec [Id]   -- One of the binders
 620   | CaseAlt CoreAlt     -- Case alternative
 621   | CasePat CoreAlt     -- *Pattern* of the case alternative
 622   | AnExpr CoreExpr     -- Some expression
 623   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 624 \end{code}
 625
 626
 627 \begin{code}
 628 initL :: LintM a -> Maybe Message {- errors -}
 629 initL m
 630   = case unLintM m [] emptyTvSubst emptyBag of
 631       (_, errs) | isEmptyBag errs -> Nothing
 632                 | otherwise       -> Just (vcat (punctuate (text "") (bagToList errs)))
 633 \end{code}
 634
 635 \begin{code}
 636 checkL :: Bool -> Message -> LintM ()
 637 checkL True  msg = return ()
 638 checkL False msg = addErrL msg
 639
 640 addErrL :: Message -> LintM a
 641 addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
 642
 643 addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
 644 addErr subst errs_so_far msg locs
 645   = ASSERT( notNull locs )
 646     errs_so_far `snocBag` mk_msg msg
 647   where
 648    (loc, cxt1) = dumpLoc (head locs)
 649    cxts        = [snd (dumpLoc loc) | loc <- locs]
 650    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
 651                                       ptext SLIT("Substitution:") <+> ppr subst
 652                | otherwise          = cxt1
 653
 654    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 655
 656 addLoc :: LintLocInfo -> LintM a -> LintM a
 657 addLoc extra_loc m =
 658   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
 659
 660 addInScopeVars :: [Var] -> LintM a -> LintM a
 661 addInScopeVars vars m =
 662   LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
 663
 664 updateTvSubst :: TvSubst -> LintM a -> LintM a
 665 updateTvSubst subst' m =
 666   LintM (\ loc subst errs -> unLintM m loc subst' errs)
 667
 668 getTvSubst :: LintM TvSubst
 669 getTvSubst = LintM (\ loc subst errs -> (Just subst, errs))
 670
 671 applySubst :: Type -> LintM Type
 672 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
 673
 674 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 675 extendSubstL tv ty m
 676   = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
 677 \end{code}
 678
 679 \begin{code}
 680 lookupIdInScope :: Id -> LintM Id
 681 lookupIdInScope id
 682   | not (mustHaveLocalBinding id)
 683   = return id   -- An imported Id
 684   | otherwise
 685   = do  { subst <- getTvSubst
 686         ; case lookupInScope (getTvInScope subst) id of
 687                 Just v  -> return v
 688                 Nothing -> do { addErrL out_of_scope
 689                               ; return id } }
 690   where
 691     out_of_scope = ppr id <+> ptext SLIT("is out of scope")
 692
 693
 694 oneTupleDataConId :: Id -- Should not happen
 695 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
 696
 697 checkBndrIdInScope :: Var -> Var -> LintM ()
 698 checkBndrIdInScope binder id
 699   = checkInScope msg id
 700     where
 701      msg = ptext SLIT("is out of scope inside info for") <+>
 702            ppr binder
 703
 704 checkTyVarInScope :: TyVar -> LintM ()
 705 checkTyVarInScope tv = checkInScope (ptext SLIT("is out of scope")) tv
 706
 707 checkInScope :: SDoc -> Var -> LintM ()
 708 checkInScope loc_msg var =
 709  do { subst <- getTvSubst
 710     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
 711              (hsep [ppr var, loc_msg]) }
 712
 713 checkTys :: Type -> Type -> Message -> LintM ()
 714 -- check ty2 is subtype of ty1 (ie, has same structure but usage
 715 -- annotations need only be consistent, not equal)
 716 -- Assumes ty1,ty2 are have alrady had the substitution applied
 717 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
 718 \end{code}
 719
 720 %************************************************************************
 721 %*                                                                      *
 722 \subsection{Error messages}
 723 %*                                                                      *
 724 %************************************************************************
 725
 726 \begin{code}
 727 dumpLoc (RhsOf v)
 728   = (getSrcLoc v, brackets (ptext SLIT("RHS of") <+> pp_binders [v]))
 729
 730 dumpLoc (LambdaBodyOf b)
 731   = (getSrcLoc b, brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b))
 732
 733 dumpLoc (BodyOfLetRec [])
 734   = (noSrcLoc, brackets (ptext SLIT("In body of a letrec with no binders")))
 735
 736 dumpLoc (BodyOfLetRec bs@(_:_))
 737   = ( getSrcLoc (head bs), brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs))
 738
 739 dumpLoc (AnExpr e)
 740   = (noSrcLoc, text "In the expression:" <+> ppr e)
 741
 742 dumpLoc (CaseAlt (con, args, rhs))
 743   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
 744
 745 dumpLoc (CasePat (con, args, rhs))
 746   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 747
 748 dumpLoc (ImportedUnfolding locn)
 749   = (locn, brackets (ptext SLIT("in an imported unfolding")))
 750
 751 pp_binders :: [Var] -> SDoc
 752 pp_binders bs = sep (punctuate comma (map pp_binder bs))
 753
 754 pp_binder :: Var -> SDoc
 755 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
 756             | isTyVar b = hsep [ppr b, dcolon, ppr (tyVarKind b)]
 757 \end{code}
 758
 759 \begin{code}
 760 ------------------------------------------------------
 761 --      Messages for case expressions
 762
 763 mkNullAltsMsg :: CoreExpr -> Message
 764 mkNullAltsMsg e
 765   = hang (text "Case expression with no alternatives:")
 766          4 (ppr e)
 767
 768 mkDefaultArgsMsg :: [Var] -> Message
 769 mkDefaultArgsMsg args
 770   = hang (text "DEFAULT case with binders")
 771          4 (ppr args)
 772
 773 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
 774 mkCaseAltMsg e ty1 ty2
 775   = hang (text "Type of case alternatives not the same as the annotation on case:")
 776          4 (vcat [ppr ty1, ppr ty2, ppr e])
 777
 778 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
 779 mkScrutMsg var var_ty scrut_ty subst
 780   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
 781           text "Result binder type:" <+> ppr var_ty,--(idType var),
 782           text "Scrutinee type:" <+> ppr scrut_ty,
 783      hsep [ptext SLIT("Current TV subst"), ppr subst]]
 784
 785
 786 mkNonDefltMsg e
 787   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
 788 mkNonIncreasingAltsMsg e
 789   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
 790
 791 nonExhaustiveAltsMsg :: CoreExpr -> Message
 792 nonExhaustiveAltsMsg e
 793   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
 794
 795 mkBadPatMsg :: Type -> Type -> Message
 796 mkBadPatMsg con_result_ty scrut_ty
 797   = vcat [
 798         text "In a case alternative, pattern result type doesn't match scrutinee type:",
 799         text "Pattern result type:" <+> ppr con_result_ty,
 800         text "Scrutinee type:" <+> ppr scrut_ty
 801     ]
 802
 803 mkBadAltMsg :: Type -> CoreAlt -> Message
 804 mkBadAltMsg scrut_ty alt
 805   = vcat [ text "Data alternative when scrutinee is not a tycon application",
 806            text "Scrutinee type:" <+> ppr scrut_ty,
 807            text "Alternative:" <+> pprCoreAlt alt ]
 808
 809 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
 810 mkNewTyDataConAltMsg scrut_ty alt
 811   = vcat [ text "Data alternative for newtype datacon",
 812            text "Scrutinee type:" <+> ppr scrut_ty,
 813            text "Alternative:" <+> pprCoreAlt alt ]
 814
 815
 816 ------------------------------------------------------
 817 --      Other error messages
 818
 819 mkAppMsg :: Type -> Type -> CoreExpr -> Message
 820 mkAppMsg fun_ty arg_ty arg
 821   = vcat [ptext SLIT("Argument value doesn't match argument type:"),
 822               hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
 823               hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
 824               hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 825
 826 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
 827 mkNonFunAppMsg fun_ty arg_ty arg
 828   = vcat [ptext SLIT("Non-function type in function position"),
 829               hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
 830               hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
 831               hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 832
 833 mkKindErrMsg :: TyVar -> Type -> Message
 834 mkKindErrMsg tyvar arg_ty
 835   = vcat [ptext SLIT("Kinds don't match in type application:"),
 836           hang (ptext SLIT("Type variable:"))
 837                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
 838           hang (ptext SLIT("Arg type:"))
 839                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 840
 841 mkTyAppMsg :: Type -> Type -> Message
 842 mkTyAppMsg ty arg_ty
 843   = vcat [text "Illegal type application:",
 844               hang (ptext SLIT("Exp type:"))
 845                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
 846               hang (ptext SLIT("Arg type:"))
 847                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 848
 849 mkRhsMsg :: Id -> Type -> Message
 850 mkRhsMsg binder ty
 851   = vcat
 852     [hsep [ptext SLIT("The type of this binder doesn't match the type of its RHS:"),
 853             ppr binder],
 854      hsep [ptext SLIT("Binder's type:"), ppr (idType binder)],
 855      hsep [ptext SLIT("Rhs type:"), ppr ty]]
 856
 857 mkRhsPrimMsg :: Id -> CoreExpr -> Message
 858 mkRhsPrimMsg binder rhs
 859   = vcat [hsep [ptext SLIT("The type of this binder is primitive:"),
 860                      ppr binder],
 861               hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
 862              ]
 863
 864 mkUnboxedTupleMsg :: Id -> Message
 865 mkUnboxedTupleMsg binder
 866   = vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],
 867           hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]]
 868
 869 mkCastErr from_ty expr_ty
 870   = vcat [ptext SLIT("From-type of Cast differs from type of enclosed expression"),
 871           ptext SLIT("From-type:") <+> ppr from_ty,
 872           ptext SLIT("Type of enclosed expr:") <+> ppr expr_ty
 873     ]
 874
 875 mkStrangeTyMsg e
 876   = ptext SLIT("Type where expression expected:") <+> ppr e
 877 \end{code}