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 :: OutType -> [CoreArg] -> LintM OutType
 373 lintCoreArg  :: OutType -> CoreArg   -> LintM OutType
 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 :: OutType -> OutType -> LintM OutType
 402 lintTyApp ty arg_ty
 403   = case splitForAllTy_maybe ty of
 404       Nothing -> addErrL (mkTyAppMsg ty arg_ty)
 405
 406       Just (tyvar,body)
 407         -> do   { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
 408                 ; checkKinds tyvar arg_ty
 409                 ; return (substTyWith [tyvar] [arg_ty] body) }
 410
 411 checkKinds tyvar arg_ty
 412         -- Arg type might be boxed for a function with an uncommitted
 413         -- tyvar; notably this is used so that we can give
 414         --      error :: forall a:*. String -> a
 415         -- and then apply it to both boxed and unboxed types.
 416   = checkL (arg_kind `isSubKind` tyvar_kind)
 417            (mkKindErrMsg tyvar arg_ty)
 418   where
 419     tyvar_kind = tyVarKind tyvar
 420     arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
 421              | otherwise     = typeKind arg_ty
 422 \end{code}
 423
 424
 425 %************************************************************************
 426 %*                                                                      *
 427 \subsection[lintCoreAlts]{lintCoreAlts}
 428 %*                                                                      *
 429 %************************************************************************
 430
 431 \begin{code}
 432 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
 433 -- a) Check that the alts are non-empty
 434 -- b1) Check that the DEFAULT comes first, if it exists
 435 -- b2) Check that the others are in increasing order
 436 -- c) Check that there's a default for infinite types
 437 -- NB: Algebraic cases are not necessarily exhaustive, because
 438 --     the simplifer correctly eliminates case that can't
 439 --     possibly match.
 440
 441 checkCaseAlts e ty []
 442   = addErrL (mkNullAltsMsg e)
 443
 444 checkCaseAlts e ty alts =
 445   do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
 446      ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
 447      ; checkL (isJust maybe_deflt || not is_infinite_ty)
 448            (nonExhaustiveAltsMsg e) }
 449   where
 450     (con_alts, maybe_deflt) = findDefault alts
 451
 452         -- Check that successive alternatives have increasing tags
 453     increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
 454     increasing_tag other                     = True
 455
 456     non_deflt (DEFAULT, _, _) = False
 457     non_deflt alt             = True
 458
 459     is_infinite_ty = case splitTyConApp_maybe ty of
 460                         Nothing                     -> False
 461                         Just (tycon, tycon_arg_tys) -> isPrimTyCon tycon
 462 \end{code}
 463
 464 \begin{code}
 465 checkAltExpr :: CoreExpr -> OutType -> LintM ()
 466 checkAltExpr expr ann_ty
 467   = do { actual_ty <- lintCoreExpr expr
 468        ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
 469
 470 lintCoreAlt :: OutType          -- Type of scrutinee
 471             -> OutType          -- Type of the alternative
 472             -> CoreAlt
 473             -> LintM ()
 474
 475 lintCoreAlt scrut_ty alt_ty alt@(DEFAULT, args, rhs) =
 476   do { checkL (null args) (mkDefaultArgsMsg args)
 477      ; checkAltExpr rhs alt_ty }
 478
 479 lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) =
 480   do { checkL (null args) (mkDefaultArgsMsg args)
 481      ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
 482      ; checkAltExpr rhs alt_ty }
 483   where
 484     lit_ty = literalType lit
 485
 486 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
 487   | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
 488   | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
 489   = addLoc (CaseAlt alt) $  do
 490     {   -- First instantiate the universally quantified
 491         -- type variables of the data constructor
 492         -- We've already check
 493       checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
 494     ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
 495
 496         -- And now bring the new binders into scope
 497     ; lintBinders args $ \ args -> do
 498     { addLoc (CasePat alt) $ do
 499           {    -- Check the pattern
 500                  -- Scrutinee type must be a tycon applicn; checked by caller
 501                  -- This code is remarkably compact considering what it does!
 502                  -- NB: args must be in scope here so that the lintCoreArgs line works.
 503                  -- NB: relies on existential type args coming *after* ordinary type args
 504
 505           ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
 506           ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
 507           }
 508                -- Check the RHS
 509     ; checkAltExpr rhs alt_ty } }
 510
 511   | otherwise   -- Scrut-ty is wrong shape
 512   = addErrL (mkBadAltMsg scrut_ty alt)
 513 \end{code}
 514
 515 %************************************************************************
 516 %*                                                                      *
 517 \subsection[lint-types]{Types}
 518 %*                                                                      *
 519 %************************************************************************
 520
 521 \begin{code}
 522 -- When we lint binders, we (one at a time and in order):
 523 --  1. Lint var types or kinds (possibly substituting)
 524 --  2. Add the binder to the in scope set, and if its a coercion var,
 525 --     we may extend the substitution to reflect its (possibly) new kind
 526 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
 527 lintBinders [] linterF = linterF []
 528 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
 529                                  lintBinders vars $ \ vars' ->
 530                                  linterF (var':vars')
 531
 532 lintBinder :: Var -> (Var -> LintM a) -> LintM a
 533 lintBinder var linterF
 534   | isTyVar var = lint_ty_bndr
 535   | otherwise   = lintIdBndr var linterF
 536   where
 537     lint_ty_bndr = do { lintTy (tyVarKind var)
 538                       ; subst <- getTvSubst
 539                       ; let (subst', tv') = substTyVarBndr subst var
 540                       ; updateTvSubst subst' (linterF tv') }
 541
 542 lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
 543 -- Do substitution on the type of a binder and add the var with this
 544 -- new type to the in-scope set of the second argument
 545 -- ToDo: lint its rules
 546 lintIdBndr id linterF
 547   = do  { checkL (not (isUnboxedTupleType (idType id)))
 548                  (mkUnboxedTupleMsg id)
 549                 -- No variable can be bound to an unboxed tuple.
 550         ; lintAndScopeId id $ \id' -> linterF id'
 551         }
 552
 553 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
 554 lintAndScopeIds ids linterF
 555   = go ids
 556   where
 557     go []       = linterF []
 558     go (id:ids) = do { lintAndScopeId id $ \id ->
 559                            lintAndScopeIds ids $ \ids ->
 560                            linterF (id:ids) }
 561
 562 lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
 563 lintAndScopeId id linterF
 564   = do { ty <- lintTy (idType id)
 565        ; let id' = setIdType id ty
 566        ; addInScopeVars [id'] $ (linterF id')
 567        }
 568
 569 lintTy :: InType -> LintM OutType
 570 -- Check the type, and apply the substitution to it
 571 -- ToDo: check the kind structure of the type
 572 lintTy ty
 573   = do  { ty' <- applySubst ty
 574         ; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
 575         ; return ty' }
 576 \end{code}
 577
 578
 579 %************************************************************************
 580 %*                                                                      *
 581 \subsection[lint-monad]{The Lint monad}
 582 %*                                                                      *
 583 %************************************************************************
 584
 585 \begin{code}
 586 newtype LintM a =
 587    LintM { unLintM ::
 588             [LintLocInfo] ->         -- Locations
 589             TvSubst ->               -- Current type substitution; we also use this
 590                                      -- to keep track of all the variables in scope,
 591                                      -- both Ids and TyVars
 592             Bag Message ->           -- Error messages so far
 593             (Maybe a, Bag Message) } -- Result and error messages (if any)
 594
 595 {-      Note [Type substitution]
 596         ~~~~~~~~~~~~~~~~~~~~~~~~
 597 Why do we need a type substitution?  Consider
 598         /\(a:*). \(x:a). /\(a:*). id a x
 599 This is ill typed, because (renaming variables) it is really
 600         /\(a:*). \(x:a). /\(b:*). id b x
 601 Hence, when checking an application, we can't naively compare x's type
 602 (at its binding site) with its expected type (at a use site).  So we
 603 rename type binders as we go, maintaining a substitution.
 604
 605 The same substitution also supports let-type, current expressed as
 606         (/\(a:*). body) ty
 607 Here we substitute 'ty' for 'a' in 'body', on the fly.
 608 -}
 609
 610 instance Monad LintM where
 611   return x = LintM (\ loc subst errs -> (Just x, errs))
 612   fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
 613   m >>= k  = LintM (\ loc subst errs ->
 614                        let (res, errs') = unLintM m loc subst errs in
 615                          case res of
 616                            Just r -> unLintM (k r) loc subst errs'
 617                            Nothing -> (Nothing, errs'))
 618
 619 data LintLocInfo
 620   = RhsOf Id            -- The variable bound
 621   | LambdaBodyOf Id     -- The lambda-binder
 622   | BodyOfLetRec [Id]   -- One of the binders
 623   | CaseAlt CoreAlt     -- Case alternative
 624   | CasePat CoreAlt     -- *Pattern* of the case alternative
 625   | AnExpr CoreExpr     -- Some expression
 626   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 627 \end{code}
 628
 629
 630 \begin{code}
 631 initL :: LintM a -> Maybe Message {- errors -}
 632 initL m
 633   = case unLintM m [] emptyTvSubst emptyBag of
 634       (_, errs) | isEmptyBag errs -> Nothing
 635                 | otherwise       -> Just (vcat (punctuate (text "") (bagToList errs)))
 636 \end{code}
 637
 638 \begin{code}
 639 checkL :: Bool -> Message -> LintM ()
 640 checkL True  msg = return ()
 641 checkL False msg = addErrL msg
 642
 643 addErrL :: Message -> LintM a
 644 addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
 645
 646 addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
 647 addErr subst errs_so_far msg locs
 648   = ASSERT( notNull locs )
 649     errs_so_far `snocBag` mk_msg msg
 650   where
 651    (loc, cxt1) = dumpLoc (head locs)
 652    cxts        = [snd (dumpLoc loc) | loc <- locs]
 653    context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
 654                                       ptext SLIT("Substitution:") <+> ppr subst
 655                | otherwise          = cxt1
 656
 657    mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 658
 659 addLoc :: LintLocInfo -> LintM a -> LintM a
 660 addLoc extra_loc m =
 661   LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
 662
 663 addInScopeVars :: [Var] -> LintM a -> LintM a
 664 addInScopeVars vars m =
 665   LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
 666
 667 updateTvSubst :: TvSubst -> LintM a -> LintM a
 668 updateTvSubst subst' m =
 669   LintM (\ loc subst errs -> unLintM m loc subst' errs)
 670
 671 getTvSubst :: LintM TvSubst
 672 getTvSubst = LintM (\ loc subst errs -> (Just subst, errs))
 673
 674 applySubst :: Type -> LintM Type
 675 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
 676
 677 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
 678 extendSubstL tv ty m
 679   = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
 680 \end{code}
 681
 682 \begin{code}
 683 lookupIdInScope :: Id -> LintM Id
 684 lookupIdInScope id
 685   | not (mustHaveLocalBinding id)
 686   = return id   -- An imported Id
 687   | otherwise
 688   = do  { subst <- getTvSubst
 689         ; case lookupInScope (getTvInScope subst) id of
 690                 Just v  -> return v
 691                 Nothing -> do { addErrL out_of_scope
 692                               ; return id } }
 693   where
 694     out_of_scope = ppr id <+> ptext SLIT("is out of scope")
 695
 696
 697 oneTupleDataConId :: Id -- Should not happen
 698 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
 699
 700 checkBndrIdInScope :: Var -> Var -> LintM ()
 701 checkBndrIdInScope binder id
 702   = checkInScope msg id
 703     where
 704      msg = ptext SLIT("is out of scope inside info for") <+>
 705            ppr binder
 706
 707 checkTyVarInScope :: TyVar -> LintM ()
 708 checkTyVarInScope tv = checkInScope (ptext SLIT("is out of scope")) tv
 709
 710 checkInScope :: SDoc -> Var -> LintM ()
 711 checkInScope loc_msg var =
 712  do { subst <- getTvSubst
 713     ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
 714              (hsep [ppr var, loc_msg]) }
 715
 716 checkTys :: Type -> Type -> Message -> LintM ()
 717 -- check ty2 is subtype of ty1 (ie, has same structure but usage
 718 -- annotations need only be consistent, not equal)
 719 -- Assumes ty1,ty2 are have alrady had the substitution applied
 720 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
 721 \end{code}
 722
 723 %************************************************************************
 724 %*                                                                      *
 725 \subsection{Error messages}
 726 %*                                                                      *
 727 %************************************************************************
 728
 729 \begin{code}
 730 dumpLoc (RhsOf v)
 731   = (getSrcLoc v, brackets (ptext SLIT("RHS of") <+> pp_binders [v]))
 732
 733 dumpLoc (LambdaBodyOf b)
 734   = (getSrcLoc b, brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b))
 735
 736 dumpLoc (BodyOfLetRec [])
 737   = (noSrcLoc, brackets (ptext SLIT("In body of a letrec with no binders")))
 738
 739 dumpLoc (BodyOfLetRec bs@(_:_))
 740   = ( getSrcLoc (head bs), brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs))
 741
 742 dumpLoc (AnExpr e)
 743   = (noSrcLoc, text "In the expression:" <+> ppr e)
 744
 745 dumpLoc (CaseAlt (con, args, rhs))
 746   = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
 747
 748 dumpLoc (CasePat (con, args, rhs))
 749   = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 750
 751 dumpLoc (ImportedUnfolding locn)
 752   = (locn, brackets (ptext SLIT("in an imported unfolding")))
 753
 754 pp_binders :: [Var] -> SDoc
 755 pp_binders bs = sep (punctuate comma (map pp_binder bs))
 756
 757 pp_binder :: Var -> SDoc
 758 pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
 759             | isTyVar b = hsep [ppr b, dcolon, ppr (tyVarKind b)]
 760 \end{code}
 761
 762 \begin{code}
 763 ------------------------------------------------------
 764 --      Messages for case expressions
 765
 766 mkNullAltsMsg :: CoreExpr -> Message
 767 mkNullAltsMsg e
 768   = hang (text "Case expression with no alternatives:")
 769          4 (ppr e)
 770
 771 mkDefaultArgsMsg :: [Var] -> Message
 772 mkDefaultArgsMsg args
 773   = hang (text "DEFAULT case with binders")
 774          4 (ppr args)
 775
 776 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
 777 mkCaseAltMsg e ty1 ty2
 778   = hang (text "Type of case alternatives not the same as the annotation on case:")
 779          4 (vcat [ppr ty1, ppr ty2, ppr e])
 780
 781 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
 782 mkScrutMsg var var_ty scrut_ty subst
 783   = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
 784           text "Result binder type:" <+> ppr var_ty,--(idType var),
 785           text "Scrutinee type:" <+> ppr scrut_ty,
 786      hsep [ptext SLIT("Current TV subst"), ppr subst]]
 787
 788 mkNonDefltMsg e
 789   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
 790 mkNonIncreasingAltsMsg e
 791   = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
 792
 793 nonExhaustiveAltsMsg :: CoreExpr -> Message
 794 nonExhaustiveAltsMsg e
 795   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
 796
 797 mkBadConMsg :: TyCon -> DataCon -> Message
 798 mkBadConMsg tycon datacon
 799   = vcat [
 800         text "In a case alternative, data constructor isn't in scrutinee type:",
 801         text "Scrutinee type constructor:" <+> ppr tycon,
 802         text "Data con:" <+> ppr datacon
 803     ]
 804
 805 mkBadPatMsg :: Type -> Type -> Message
 806 mkBadPatMsg con_result_ty scrut_ty
 807   = vcat [
 808         text "In a case alternative, pattern result type doesn't match scrutinee type:",
 809         text "Pattern result type:" <+> ppr con_result_ty,
 810         text "Scrutinee type:" <+> ppr scrut_ty
 811     ]
 812
 813 mkBadAltMsg :: Type -> CoreAlt -> Message
 814 mkBadAltMsg scrut_ty alt
 815   = vcat [ text "Data alternative when scrutinee is not a tycon application",
 816            text "Scrutinee type:" <+> ppr scrut_ty,
 817            text "Alternative:" <+> pprCoreAlt alt ]
 818
 819 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
 820 mkNewTyDataConAltMsg scrut_ty alt
 821   = vcat [ text "Data alternative for newtype datacon",
 822            text "Scrutinee type:" <+> ppr scrut_ty,
 823            text "Alternative:" <+> pprCoreAlt alt ]
 824
 825
 826 ------------------------------------------------------
 827 --      Other error messages
 828
 829 mkAppMsg :: Type -> Type -> CoreExpr -> Message
 830 mkAppMsg fun_ty arg_ty arg
 831   = vcat [ptext SLIT("Argument value doesn't match argument type:"),
 832               hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
 833               hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
 834               hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 835
 836 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
 837 mkNonFunAppMsg fun_ty arg_ty arg
 838   = vcat [ptext SLIT("Non-function type in function position"),
 839               hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
 840               hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
 841               hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 842
 843 mkKindErrMsg :: TyVar -> Type -> Message
 844 mkKindErrMsg tyvar arg_ty
 845   = vcat [ptext SLIT("Kinds don't match in type application:"),
 846           hang (ptext SLIT("Type variable:"))
 847                  4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
 848           hang (ptext SLIT("Arg type:"))
 849                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 850
 851 mkTyAppMsg :: Type -> Type -> Message
 852 mkTyAppMsg ty arg_ty
 853   = vcat [text "Illegal type application:",
 854               hang (ptext SLIT("Exp type:"))
 855                  4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
 856               hang (ptext SLIT("Arg type:"))
 857                  4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
 858
 859 mkRhsMsg :: Id -> Type -> Message
 860 mkRhsMsg binder ty
 861   = vcat
 862     [hsep [ptext SLIT("The type of this binder doesn't match the type of its RHS:"),
 863             ppr binder],
 864      hsep [ptext SLIT("Binder's type:"), ppr (idType binder)],
 865      hsep [ptext SLIT("Rhs type:"), ppr ty]]
 866
 867 mkRhsPrimMsg :: Id -> CoreExpr -> Message
 868 mkRhsPrimMsg binder rhs
 869   = vcat [hsep [ptext SLIT("The type of this binder is primitive:"),
 870                      ppr binder],
 871               hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
 872              ]
 873
 874 mkUnboxedTupleMsg :: Id -> Message
 875 mkUnboxedTupleMsg binder
 876   = vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],
 877           hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]]
 878
 879 mkCastErr from_ty expr_ty
 880   = vcat [ptext SLIT("From-type of Cast differs from type of enclosed expression"),
 881           ptext SLIT("From-type:") <+> ppr from_ty,
 882           ptext SLIT("Type of enclosed expr:") <+> ppr expr_ty
 883     ]
 884
 885 mkStrangeTyMsg e
 886   = ptext SLIT("Type where expression expected:") <+> ppr e
 887 \end{code}