2 % (c) The GRASP/AQUA Project, Glasgow University, 1993-1996
4 \section[CoreLint]{A ``lint'' pass to check for Core correctness}
12 #include "HsVersions.h"
14 import IO ( hPutStr, stderr )
16 import CmdLineOpts ( opt_D_show_passes, opt_DoCoreLinting )
20 import Kind ( hasMoreBoxityInfo, Kind{-instance-},
21 isTypeKind, isBoxedTypeKind {- TEMP --SOF -} )
22 import Literal ( literalType, Literal{-instance-} )
23 import Id ( idType, isBottomingId, dataConRepType, isDataCon, isNewCon, isAlgCon,
24 dataConArgTys, GenId{-instances-},
25 emptyIdSet, mkIdSet, intersectIdSets,
26 unionIdSets, elementOfIdSet, IdSet,
29 import Maybes ( catMaybes )
30 import Name ( isLocallyDefined, getSrcLoc, Name{-instance NamedThing-},
33 import ErrUtils ( doIfSet, ghcExit )
34 import PprType ( GenType, GenTyVar, TyCon )
35 import PrimOp ( primOpType, PrimOp(..) )
36 import PrimRep ( PrimRep(..) )
37 import SrcLoc ( SrcLoc )
38 import Type ( mkFunTy, splitFunTy_maybe, mkForAllTy,
40 isUnpointedType, typeKind, instantiateTy, splitSigmaTy,
41 splitAlgTyConApp_maybe, Type
43 import TyCon ( isPrimTyCon, isDataTyCon )
44 import TyVar ( TyVar, tyVarKind, mkTyVarEnv )
45 import ErrUtils ( ErrMsg )
46 import Unique ( Unique )
47 import Util ( zipEqual )
50 infixr 9 `thenL`, `seqL`, `thenMaybeL`, `seqMaybeL`
53 %************************************************************************
55 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
57 %************************************************************************
59 Checks that a set of core bindings is well-formed. The PprStyle and String
60 just control what we print in the event of an error. The Bool value
61 indicates whether we have done any specialisation yet (in which case we do
66 (b) Out-of-scope type variables
67 (c) Out-of-scope local variables
70 If we have done specialisation the we check that there are
71 (a) No top-level bindings of primitive (unboxed type)
76 -- Things are *not* OK if:
78 -- * Unsaturated type app before specialisation has been done;
80 -- * Oversaturated type app after specialisation (eta reduction
81 -- may well be happening...);
83 -- Note: checkTyApp is usually followed by a call to checkSpecTyApp.
87 lintCoreBindings :: String -> Bool -> [CoreBinding] -> IO ()
89 lintCoreBindings whoDunnit spec_done binds
90 | not opt_DoCoreLinting
93 lintCoreBindings whoDunnit spec_done binds
94 = case (initL (lint_binds binds) spec_done) of
95 Nothing -> doIfSet opt_D_show_passes
96 (hPutStr stderr ("*** Core Linted result of " ++ whoDunnit ++ "\n"))
98 Just bad_news -> printDump (display bad_news) >>
101 lint_binds [] = returnL ()
102 lint_binds (bind:binds)
103 = lintCoreBinding bind `thenL` \binders ->
104 addInScopeVars binders (lint_binds binds)
108 text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
110 ptext SLIT("*** Offending Program ***"),
111 pprCoreBindings binds,
112 ptext SLIT("*** End of Offense ***")
116 %************************************************************************
118 \subsection[lintUnfolding]{lintUnfolding}
120 %************************************************************************
122 We use this to check all unfoldings that come in from interfaces
123 (it is very painful to catch errors otherwise):
126 lintUnfolding :: SrcLoc -> CoreExpr -> Maybe CoreExpr
128 lintUnfolding locn expr
130 (initL (addLoc (ImportedUnfolding locn) (lintCoreExpr expr))
131 True{-pretend spec done-})
135 pprTrace "WARNING: Discarded bad unfolding from interface:\n"
137 ptext SLIT("*** Bad unfolding ***"),
139 ptext SLIT("*** End unfolding ***")])
143 %************************************************************************
145 \subsection[lintCoreBinding]{lintCoreBinding}
147 %************************************************************************
149 Check a core binding, returning the list of variables bound.
152 lintCoreBinding :: CoreBinding -> LintM [Id]
154 lintCoreBinding (NonRec binder rhs)
155 = lintSingleBinding (binder,rhs) `seqL` returnL [binder]
157 lintCoreBinding (Rec pairs)
158 = addInScopeVars binders (
159 mapL lintSingleBinding pairs `seqL` returnL binders
162 binders = [b | (b,_) <- pairs]
164 lintSingleBinding (binder,rhs)
165 = addLoc (RhsOf binder) (
170 -- Check match to RHS type
172 Nothing -> returnL ()
173 Just ty -> checkTys (idType binder) ty (mkRhsMsg binder ty))
176 -- Check (not isUnpointedType)
177 checkIfSpecDoneL (not (isUnpointedType (idType binder)))
178 (mkRhsPrimMsg binder rhs)
180 -- We should check the unfolding, if any, but this is tricky because
181 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
185 %************************************************************************
187 \subsection[lintCoreExpr]{lintCoreExpr}
189 %************************************************************************
192 lintCoreExpr :: CoreExpr -> LintM (Maybe Type) -- Nothing if error found
194 lintCoreExpr (Var var)
195 | isAlgCon var = returnL (Just (idType var))
196 -- Micro-hack here... Class decls generate applications of their
197 -- dictionary constructor, but don't generate a binding for the
198 -- constructor (since it would never be used). After a single round
199 -- of simplification, these dictionary constructors have been
200 -- inlined (from their UnfoldInfo) to CoCons. Just between
201 -- desugaring and simplfication, though, they appear as naked, unbound
202 -- variables as the function in an application.
203 -- The hack here simply doesn't check for out-of-scope-ness for
204 -- data constructors (at least, in a function position).
206 | otherwise = checkInScope var `seqL` returnL (Just (idType var))
208 lintCoreExpr (Lit lit) = returnL (Just (literalType lit))
209 lintCoreExpr (SCC _ expr) = lintCoreExpr expr
210 lintCoreExpr e@(Coerce coercion ty expr)
211 = lintCoercion e coercion `seqL`
212 lintCoreExpr expr `seqL` returnL (Just ty)
214 lintCoreExpr (Let binds body)
215 = lintCoreBinding binds `thenL` \binders ->
216 if (null binders) then
217 lintCoreExpr body -- Can't add a new source location
219 addLoc (BodyOfLetRec binders)
220 (addInScopeVars binders (lintCoreExpr body))
222 lintCoreExpr e@(Con con args)
223 = checkL (isDataCon con) (mkConErrMsg e) `seqL`
224 lintCoreArgs {-False-} e (dataConRepType con) args
225 -- Note: we don't check for primitive types in these arguments
227 lintCoreExpr e@(Prim op args)
228 = lintCoreArgs {-True-} e (primOpType op) args
229 -- Note: we do check for primitive types in these arguments
231 lintCoreExpr e@(App fun@(Var v) arg) | isBottomingId v
232 = lintCoreExpr fun `thenMaybeL` \ ty -> lintCoreArg {-False-} e ty arg
233 -- Note: we don't check for primitive types in argument to 'error'
235 lintCoreExpr e@(App fun arg)
236 = lintCoreExpr fun `thenMaybeL` \ty -> lintCoreArg {-True-} e ty arg
237 -- Note: we do check for primitive types in this argument
239 lintCoreExpr (Lam (ValBinder var) expr)
240 = addLoc (LambdaBodyOf var)
241 (addInScopeVars [var]
242 (lintCoreExpr expr `thenMaybeL` \ty ->
243 returnL (Just (mkFunTy (idType var) ty))))
245 lintCoreExpr (Lam (TyBinder tyvar) expr)
246 = lintCoreExpr expr `thenMaybeL` \ty ->
247 returnL (Just(mkForAllTy tyvar ty))
248 -- ToDo: Should add in-scope type variable at this point
250 lintCoreExpr e@(Case scrut alts)
251 = lintCoreExpr scrut `thenMaybeL` \ty ->
255 %************************************************************************
257 \subsection[lintCoreArgs]{lintCoreArgs}
259 %************************************************************************
261 The boolean argument indicates whether we should flag type
262 applications to primitive types as being errors.
265 lintCoreArgs :: {-Bool ->-} CoreExpr -> Type -> [CoreArg] -> LintM (Maybe Type)
267 lintCoreArgs _ ty [] = returnL (Just ty)
268 lintCoreArgs e ty (a : args)
269 = lintCoreArg e ty a `thenMaybeL` \ res ->
270 lintCoreArgs e res args
273 %************************************************************************
275 \subsection[lintCoreArg]{lintCoreArg}
277 %************************************************************************
280 lintCoreArg :: {-Bool ->-} CoreExpr -> Type -> CoreArg -> LintM (Maybe Type)
282 lintCoreArg e ty (LitArg lit)
283 = -- Make sure function type matches argument
284 case (splitFunTy_maybe ty) of
285 Just (arg,res) | (lit_ty == arg) -> returnL(Just res)
286 _ -> addErrL (mkAppMsg ty lit_ty e) `seqL` returnL Nothing
288 lit_ty = literalType lit
290 lintCoreArg e ty (VarArg v)
291 = -- Make sure variable is bound
292 checkInScope v `seqL`
293 -- Make sure function type matches argument
294 case (splitFunTy_maybe ty) of
295 Just (arg,res) | (var_ty == arg) -> returnL(Just res)
296 _ -> addErrL (mkAppMsg ty var_ty e) `seqL` returnL Nothing
300 lintCoreArg e ty a@(TyArg arg_ty)
301 = -- ToDo: Check that ty is well-kinded and has no unbound tyvars
302 case (splitForAllTy_maybe ty) of
303 Nothing -> addErrL (mkTyAppMsg SLIT("Illegal") ty arg_ty e) `seqL` returnL Nothing
307 tyvar_kind = tyVarKind tyvar
308 argty_kind = typeKind arg_ty
310 if argty_kind `hasMoreBoxityInfo` tyvar_kind
311 -- Arg type might be boxed for a function with an uncommitted
312 -- tyvar; notably this is used so that we can give
313 -- error :: forall a:*. String -> a
314 -- and then apply it to both boxed and unboxed types.
316 returnL(Just(instantiateTy (mkTyVarEnv [(tyvar,arg_ty)]) body))
318 pprTrace "lintCoreArg:kinds:" (hsep [ppr tyvar_kind, ppr argty_kind]) $
319 addErrL (mkKindErrMsg tyvar arg_ty e) `seqL` returnL Nothing
322 %************************************************************************
324 \subsection[lintCoreAlts]{lintCoreAlts}
326 %************************************************************************
329 lintCoreAlts :: CoreCaseAlts
330 -> Type -- Type of scrutinee
331 -- -> TyCon -- TyCon pinned on the case
332 -> LintM (Maybe Type) -- Type of alternatives
334 lintCoreAlts whole_alts@(AlgAlts alts deflt) ty --tycon
335 = -- Check tycon is not a primitive tycon
336 -- addErrIfL (isPrimTyCon tycon) (mkCasePrimMsg tycon)
338 -- Check we are scrutinising a proper datatype
340 -- addErrIfL (not (tyConFamilySize tycon >= 1)) (mkCaseAbstractMsg tycon)
343 `thenL` \maybe_deflt_ty ->
344 mapL (lintAlgAlt ty {-tycon-}) alts
345 `thenL` \maybe_alt_tys ->
346 -- Check the result types
347 case catMaybes (maybe_deflt_ty : maybe_alt_tys) of
348 [] -> returnL Nothing
350 (first_ty:tys) -> mapL check tys `seqL`
351 returnL (Just first_ty)
353 check ty = checkTys first_ty ty (mkCaseAltMsg whole_alts)
355 lintCoreAlts whole_alts@(PrimAlts alts deflt) ty --tycon
356 = -- Check tycon is a primitive tycon
357 -- addErrIfL (not (isPrimTyCon tycon)) (mkCaseNotPrimMsg tycon)
359 mapL (lintPrimAlt ty) alts
360 `thenL` \maybe_alt_tys ->
362 `thenL` \maybe_deflt_ty ->
363 -- Check the result types
364 case catMaybes (maybe_deflt_ty : maybe_alt_tys) of
365 [] -> returnL Nothing
367 (first_ty:tys) -> mapL check tys `seqL`
368 returnL (Just first_ty)
370 check ty = checkTys first_ty ty (mkCaseAltMsg whole_alts)
372 lintAlgAlt scrut_ty (con,args,rhs)
373 = (case splitAlgTyConApp_maybe scrut_ty of
374 Just (tycon, tys_applied, cons) | isDataTyCon tycon ->
376 arg_tys = dataConArgTys con tys_applied
378 checkL (con `elem` cons) (mkAlgAltMsg2 scrut_ty con) `seqL`
379 checkL (length arg_tys == length args) (mkAlgAltMsg3 con args)
381 mapL check (zipEqual "lintAlgAlt" arg_tys args) `seqL`
384 other -> addErrL (mkAlgAltMsg1 scrut_ty)
386 addInScopeVars args (
390 check (ty, arg) = checkTys ty (idType arg) (mkAlgAltMsg4 ty arg)
392 -- elem: yes, the elem-list here can sometimes be long-ish,
393 -- but as it's use-once, probably not worth doing anything different
394 -- We give it its own copy, so it isn't overloaded.
396 elem x (y:ys) = x==y || elem x ys
398 lintPrimAlt ty alt@(lit,rhs)
399 = checkTys (literalType lit) ty (mkPrimAltMsg alt) `seqL`
402 lintDeflt NoDefault _ = returnL Nothing
403 lintDeflt deflt@(BindDefault binder rhs) ty
404 = checkTys (idType binder) ty (mkDefltMsg deflt) `seqL`
405 addInScopeVars [binder] (lintCoreExpr rhs)
408 %************************************************************************
410 \subsection[lint-coercion]{Coercion}
412 %************************************************************************
415 lintCoercion e (CoerceIn con) = check_con e con
416 lintCoercion e (CoerceOut con) = check_con e con
418 check_con e con = checkL (isNewCon con)
423 %************************************************************************
425 \subsection[lint-monad]{The Lint monad}
427 %************************************************************************
430 type LintM a = Bool -- True <=> specialisation has been done
431 -> [LintLocInfo] -- Locations
432 -> IdSet -- Local vars in scope
433 -> Bag ErrMsg -- Error messages so far
434 -> (a, Bag ErrMsg) -- Result and error messages (if any)
437 = RhsOf Id -- The variable bound
438 | LambdaBodyOf Id -- The lambda-binder
439 | BodyOfLetRec [Id] -- One of the binders
440 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
442 instance Outputable LintLocInfo where
444 = ppr (getSrcLoc v) <> colon <+>
445 brackets (ptext SLIT("RHS of") <+> pp_binders [v])
448 = ppr (getSrcLoc b) <> colon <+>
449 brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b)
451 ppr (BodyOfLetRec bs)
452 = ppr (getSrcLoc (head bs)) <> colon <+>
453 brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs)
455 ppr (ImportedUnfolding locn)
456 = ppr locn <> colon <+>
457 brackets (ptext SLIT("in an imported unfolding"))
459 pp_binders :: [Id] -> SDoc
460 pp_binders bs = sep (punctuate comma (map pp_binder bs))
462 pp_binder :: Id -> SDoc
463 pp_binder b = hsep [ppr b, text "::", ppr (idType b)]
467 initL :: LintM a -> Bool -> Maybe ErrMsg
469 = case (m spec_done [] emptyIdSet emptyBag) of { (_, errs) ->
470 if isEmptyBag errs then
473 Just (vcat (bagToList errs))
476 returnL :: a -> LintM a
477 returnL r spec loc scope errs = (r, errs)
479 thenL :: LintM a -> (a -> LintM b) -> LintM b
480 thenL m k spec loc scope errs
481 = case m spec loc scope errs of
482 (r, errs') -> k r spec loc scope errs'
484 seqL :: LintM a -> LintM b -> LintM b
485 seqL m k spec loc scope errs
486 = case m spec loc scope errs of
487 (_, errs') -> k spec loc scope errs'
489 thenMaybeL :: LintM (Maybe a) -> (a -> LintM (Maybe b)) -> LintM (Maybe b)
490 thenMaybeL m k spec loc scope errs
491 = case m spec loc scope errs of
492 (Nothing, errs2) -> (Nothing, errs2)
493 (Just r, errs2) -> k r spec loc scope errs2
495 seqMaybeL :: LintM (Maybe a) -> LintM (Maybe b) -> LintM (Maybe b)
496 seqMaybeL m k spec loc scope errs
497 = case m spec loc scope errs of
498 (Nothing, errs2) -> (Nothing, errs2)
499 (Just _, errs2) -> k spec loc scope errs2
501 mapL :: (a -> LintM b) -> [a] -> LintM [b]
502 mapL f [] = returnL []
505 mapL f xs `thenL` \ rs ->
508 mapMaybeL :: (a -> LintM (Maybe b)) -> [a] -> LintM (Maybe [b])
509 -- Returns Nothing if anything fails
510 mapMaybeL f [] = returnL (Just [])
512 = f x `thenMaybeL` \ r ->
513 mapMaybeL f xs `thenMaybeL` \ rs ->
514 returnL (Just (r:rs))
518 checkL :: Bool -> ErrMsg -> LintM ()
519 checkL True msg spec loc scope errs = ((), errs)
520 checkL False msg spec loc scope errs = ((), addErr errs msg loc)
522 checkIfSpecDoneL :: Bool -> ErrMsg -> LintM ()
523 checkIfSpecDoneL True msg spec loc scope errs = ((), errs)
524 checkIfSpecDoneL False msg True loc scope errs = ((), addErr errs msg loc)
525 checkIfSpecDoneL False msg False loc scope errs = ((), errs)
528 = if pred then addErrL spec else returnL ()
530 addErrL :: ErrMsg -> LintM ()
531 addErrL msg spec loc scope errs = ((), addErr errs msg loc)
533 addErr :: Bag ErrMsg -> ErrMsg -> [LintLocInfo] -> Bag ErrMsg
535 addErr errs_so_far msg locs
536 = ASSERT (not (null locs))
537 errs_so_far `snocBag` (hang (ppr (head locs)) 4 msg)
539 addLoc :: LintLocInfo -> LintM a -> LintM a
540 addLoc extra_loc m spec loc scope errs
541 = m spec (extra_loc:loc) scope errs
543 addInScopeVars :: [Id] -> LintM a -> LintM a
544 addInScopeVars ids m spec loc scope errs
545 = -- We check if these "new" ids are already
546 -- in scope, i.e., we have *shadowing* going on.
547 -- For now, it's just a "trace"; we may make
548 -- a real error out of it...
550 new_set = mkIdSet ids
552 -- shadowed = scope `intersectIdSets` new_set
554 -- After adding -fliberate-case, Simon decided he likes shadowed
555 -- names after all. WDP 94/07
556 -- (if isEmptyUniqSet shadowed
558 -- else pprTrace "Shadowed vars:" (ppr (uniqSetToList shadowed))) (
559 m spec loc (scope `unionIdSets` new_set) errs
564 checkInScope :: Id -> LintM ()
565 checkInScope id spec loc scope errs
569 if isLocallyDefined id_name && not (id `elementOfIdSet` scope) then
570 ((), addErr errs (hsep [ppr id, ptext SLIT("is out of scope")]) loc)
574 checkTys :: Type -> Type -> ErrMsg -> LintM ()
575 checkTys ty1 ty2 msg spec loc scope errs
576 = if ty1 == ty2 then ((), errs) else ((), addErr errs msg loc)
581 = ($$) (ptext SLIT("Application of newtype constructor:"))
585 = ($$) (ptext SLIT("Coercion using a datatype constructor:"))
589 mkCaseAltMsg :: CoreCaseAlts -> ErrMsg
591 = ($$) (ptext SLIT("Type of case alternatives not the same:"))
594 mkCaseDataConMsg :: CoreExpr -> ErrMsg
595 mkCaseDataConMsg expr
596 = ($$) (ptext SLIT("A case scrutinee not of data constructor type:"))
599 mkCaseNotPrimMsg :: TyCon -> ErrMsg
600 mkCaseNotPrimMsg tycon
601 = ($$) (ptext SLIT("A primitive case on a non-primitive type:"))
604 mkCasePrimMsg :: TyCon -> ErrMsg
606 = ($$) (ptext SLIT("An algebraic case on a primitive type:"))
609 mkCaseAbstractMsg :: TyCon -> ErrMsg
610 mkCaseAbstractMsg tycon
611 = ($$) (ptext SLIT("An algebraic case on some weird type:"))
614 mkDefltMsg :: CoreCaseDefault -> ErrMsg
616 = ($$) (ptext SLIT("Binder in case default doesn't match type of scrutinee:"))
619 mkAppMsg :: Type -> Type -> CoreExpr -> ErrMsg
620 mkAppMsg fun arg expr
621 = vcat [ptext SLIT("Argument value doesn't match argument type:"),
622 hang (ptext SLIT("Fun type:")) 4 (ppr fun),
623 hang (ptext SLIT("Arg type:")) 4 (ppr arg),
624 hang (ptext SLIT("Expression:")) 4 (pprCoreExpr expr)]
626 mkKindErrMsg :: TyVar -> Type -> CoreExpr -> ErrMsg
627 mkKindErrMsg tyvar arg_ty expr
628 = vcat [ptext SLIT("Kinds don't match in type application:"),
629 hang (ptext SLIT("Type variable:"))
630 4 (ppr tyvar <+> ptext SLIT("::") <+> ppr (tyVarKind tyvar)),
631 hang (ptext SLIT("Arg type:"))
632 4 (ppr arg_ty <+> ptext SLIT("::") <+> ppr (typeKind arg_ty)),
633 hang (ptext SLIT("Expression:")) 4 (pprCoreExpr expr)]
635 mkTyAppMsg :: FAST_STRING -> Type -> Type -> CoreExpr -> ErrMsg
636 mkTyAppMsg msg ty arg expr
637 = vcat [hsep [ptext msg, ptext SLIT("type application:")],
638 hang (ptext SLIT("Exp type:"))
639 4 (ppr ty <+> ptext SLIT("::") <+> ppr (typeKind ty)),
640 hang (ptext SLIT("Arg type:"))
641 4 (ppr arg <+> ptext SLIT("::") <+> ppr (typeKind arg)),
642 hang (ptext SLIT("Expression:")) 4 (pprCoreExpr expr)]
644 mkAlgAltMsg1 :: Type -> ErrMsg
646 = ($$) (text "In some case statement, type of scrutinee is not a data type:")
649 mkAlgAltMsg2 :: Type -> Id -> ErrMsg
652 text "In some algebraic case alternative, constructor is not a constructor of scrutinee type:",
657 mkAlgAltMsg3 :: Id -> [Id] -> ErrMsg
658 mkAlgAltMsg3 con alts
660 text "In some algebraic case alternative, number of arguments doesn't match constructor:",
665 mkAlgAltMsg4 :: Type -> Id -> ErrMsg
668 text "In some algebraic case alternative, type of argument doesn't match data constructor:",
673 mkPrimAltMsg :: (Literal, CoreExpr) -> ErrMsg
676 (text "In a primitive case alternative, type of literal doesn't match type of scrutinee:")
679 mkRhsMsg :: Id -> Type -> ErrMsg
682 [hsep [ptext SLIT("The type of this binder doesn't match the type of its RHS:"),
684 hsep [ptext SLIT("Binder's type:"), ppr (idType binder)],
685 hsep [ptext SLIT("Rhs type:"), ppr ty]]
687 mkRhsPrimMsg :: Id -> CoreExpr -> ErrMsg
688 mkRhsPrimMsg binder rhs
689 = vcat [hsep [ptext SLIT("The type of this binder is primitive:"),
691 hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
694 mkSpecTyAppMsg :: CoreArg -> ErrMsg
697 (ptext SLIT("Unboxed types in a type application (after specialisation):"))