3 % (c) The University of Glasgow 2006
4 % (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
7 A ``lint'' pass to check for Core correctness
10 module CoreLint ( lintCoreBindings, lintUnfolding ) where
12 #include "HsVersions.h"
47 %************************************************************************
49 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
51 %************************************************************************
53 Checks that a set of core bindings is well-formed. The PprStyle and String
54 just control what we print in the event of an error. The Bool value
55 indicates whether we have done any specialisation yet (in which case we do
60 (b) Out-of-scope type variables
61 (c) Out-of-scope local variables
64 If we have done specialisation the we check that there are
65 (a) No top-level bindings of primitive (unboxed type)
70 -- Things are *not* OK if:
72 -- * Unsaturated type app before specialisation has been done;
74 -- * Oversaturated type app after specialisation (eta reduction
75 -- may well be happening...);
78 Note [Linting type lets]
79 ~~~~~~~~~~~~~~~~~~~~~~~~
80 In the desugarer, it's very very convenient to be able to say (in effect)
81 let a = Type Int in <body>
82 That is, use a type let. See Note [Type let] in CoreSyn.
84 However, when linting <body> we need to remember that a=Int, else we might
85 reject a correct program. So we carry a type substitution (in this example
86 [a -> Int]) and apply this substitution before comparing types. The functin
87 lintInTy :: Type -> LintM Type
88 returns a substituted type; that's the only reason it returns anything.
90 When we encounter a binder (like x::a) we must apply the substitution
91 to the type of the binding variable. lintBinders does this.
93 For Ids, the type-substituted Id is added to the in_scope set (which
94 itself is part of the TvSubst we are carrying down), and when we
95 find an occurence of an Id, we fetch it from the in-scope set.
99 lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
101 lintCoreBindings dflags _whoDunnit _binds
102 | not (dopt Opt_DoCoreLinting dflags)
105 lintCoreBindings dflags whoDunnit binds
107 = do { showPass dflags ("Core Linted result of " ++ whoDunnit)
108 ; unless (isEmptyBag warns || opt_NoDebugOutput) $ printDump $
109 (banner "warnings" $$ displayMessageBag warns)
113 = do { printDump (vcat [ banner "errors", displayMessageBag errs
114 , ptext (sLit "*** Offending Program ***")
115 , pprCoreBindings binds
116 , ptext (sLit "*** End of Offense ***") ])
120 (warns, errs) = initL (lint_binds binds)
122 -- Put all the top-level binders in scope at the start
123 -- This is because transformation rules can bring something
124 -- into use 'unexpectedly'
125 lint_binds binds = addLoc TopLevelBindings $
126 addInScopeVars (bindersOfBinds binds) $
129 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
130 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
132 banner string = ptext (sLit "*** Core Lint") <+> text string
133 <+> ptext (sLit ": in result of") <+> text whoDunnit
134 <+> ptext (sLit "***")
136 displayMessageBag :: Bag Message -> SDoc
137 displayMessageBag msgs = vcat (punctuate blankLine (bagToList msgs))
140 %************************************************************************
142 \subsection[lintUnfolding]{lintUnfolding}
144 %************************************************************************
146 We use this to check all unfoldings that come in from interfaces
147 (it is very painful to catch errors otherwise):
150 lintUnfolding :: SrcLoc
151 -> [Var] -- Treat these as in scope
153 -> Maybe Message -- Nothing => OK
155 lintUnfolding locn vars expr
156 | isEmptyBag errs = Nothing
157 | otherwise = Just (displayMessageBag errs)
159 (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
160 addInScopeVars vars $
164 %************************************************************************
166 \subsection[lintCoreBinding]{lintCoreBinding}
168 %************************************************************************
170 Check a core binding, returning the list of variables bound.
173 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
174 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
175 = addLoc (RhsOf binder) $
177 do { ty <- lintCoreExpr rhs
178 ; lintBinder binder -- Check match to RHS type
179 ; binder_ty <- applySubst binder_ty
180 ; checkTys binder_ty ty (mkRhsMsg binder ty)
181 -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
182 ; checkL (not (isUnLiftedType binder_ty)
183 || (isNonRec rec_flag && exprOkForSpeculation rhs))
184 (mkRhsPrimMsg binder rhs)
185 -- Check that if the binder is top-level or recursive, it's not demanded
186 ; checkL (not (isStrictId binder)
187 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
189 -- Check whether binder's specialisations contain any out-of-scope variables
190 ; mapM_ (checkBndrIdInScope binder) bndr_vars
192 ; when (isLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
193 (addWarnL (ptext (sLit "INLINE binder is loop breaker:") <+> ppr binder))
195 -- Check whether arity and demand type are consistent (only if demand analysis
197 ; checkL (case maybeDmdTy of
198 Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
200 (mkArityMsg binder) }
202 -- We should check the unfolding, if any, but this is tricky because
203 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
205 binder_ty = idType binder
206 maybeDmdTy = idNewStrictness_maybe binder
207 bndr_vars = varSetElems (idFreeVars binder)
208 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
209 | otherwise = return ()
212 %************************************************************************
214 \subsection[lintCoreExpr]{lintCoreExpr}
216 %************************************************************************
219 type InType = Type -- Substitution not yet applied
223 type OutType = Type -- Substitution has been applied to this
225 type OutTyVar = TyVar
226 type OutCoVar = CoVar
228 lintCoreExpr :: CoreExpr -> LintM OutType
229 -- The returned type has the substitution from the monad
230 -- already applied to it:
231 -- lintCoreExpr e subst = exprType (subst e)
233 -- The returned "type" can be a kind, if the expression is (Type ty)
235 lintCoreExpr (Var var)
236 = do { checkL (not (var == oneTupleDataConId))
237 (ptext (sLit "Illegal one-tuple"))
240 ; var' <- lookupIdInScope var
241 ; return (idType var')
244 lintCoreExpr (Lit lit)
245 = return (literalType lit)
247 lintCoreExpr (Cast expr co)
248 = do { expr_ty <- lintCoreExpr expr
249 ; co' <- applySubst co
250 ; (from_ty, to_ty) <- lintCoercion co'
251 ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
254 lintCoreExpr (Note _ expr)
257 lintCoreExpr (Let (NonRec tv (Type ty)) body)
258 = -- See Note [Type let] in CoreSyn
259 do { checkL (isTyVar tv) (mkKindErrMsg tv ty) -- Not quite accurate
261 ; lintTyBndr tv $ \ tv' ->
262 addLoc (BodyOfLetRec [tv]) $
263 extendSubstL tv' ty' $ do
265 -- Now extend the substitution so we
266 -- take advantage of it in the body
267 ; lintCoreExpr body } }
269 lintCoreExpr (Let (NonRec bndr rhs) body)
270 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
271 ; addLoc (BodyOfLetRec [bndr])
272 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
274 lintCoreExpr (Let (Rec pairs) body)
275 = lintAndScopeIds bndrs $ \_ ->
276 do { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
277 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
279 bndrs = map fst pairs
281 lintCoreExpr e@(App fun arg)
282 = do { fun_ty <- lintCoreExpr fun
283 ; addLoc (AnExpr e) $
284 lintCoreArg fun_ty arg }
286 lintCoreExpr (Lam var expr)
287 = addLoc (LambdaBodyOf var) $
288 lintBinders [var] $ \[var'] ->
289 do { body_ty <- lintCoreExpr expr
291 return (mkFunTy (idType var') body_ty)
293 return (mkForAllTy var' body_ty)
295 -- The applySubst is needed to apply the subst to var
297 lintCoreExpr e@(Case scrut var alt_ty alts) =
298 -- Check the scrutinee
299 do { scrut_ty <- lintCoreExpr scrut
300 ; alt_ty <- lintInTy alt_ty
301 ; var_ty <- lintInTy (idType var)
303 ; let mb_tc_app = splitTyConApp_maybe (idType var)
308 not (isOpenTyCon tycon) &&
309 null (tyConDataCons tycon) ->
310 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
311 -- This can legitimately happen for type families
313 _otherwise -> return ()
315 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
317 ; subst <- getTvSubst
318 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
320 -- If the binder is an unboxed tuple type, don't put it in scope
321 ; let scope = if (isUnboxedTupleType (idType var)) then
323 else lintAndScopeId var
325 do { -- Check the alternatives
326 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
327 ; checkCaseAlts e scrut_ty alts
332 lintCoreExpr (Type ty)
333 = do { ty' <- lintInTy ty
334 ; return (typeKind ty') }
337 %************************************************************************
339 \subsection[lintCoreArgs]{lintCoreArgs}
341 %************************************************************************
343 The basic version of these functions checks that the argument is a
344 subtype of the required type, as one would expect.
347 lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
348 lintCoreArg :: OutType -> CoreArg -> LintM OutType
349 -- First argument has already had substitution applied to it
353 lintCoreArgs ty [] = return ty
354 lintCoreArgs ty (a : args) =
355 do { res <- lintCoreArg ty a
356 ; lintCoreArgs res args }
358 lintCoreArg fun_ty (Type arg_ty)
359 | Just (tyvar,body) <- splitForAllTy_maybe fun_ty
360 = do { arg_ty' <- applySubst arg_ty
361 ; checkKinds tyvar arg_ty'
362 ; if isCoVar tyvar then
363 return body -- Co-vars don't appear in body!
365 return (substTyWith [tyvar] [arg_ty'] body) }
367 = failWithL (mkTyAppMsg fun_ty arg_ty)
369 lintCoreArg fun_ty arg
370 -- Make sure function type matches argument
371 = do { arg_ty <- lintCoreExpr arg
372 ; let err1 = mkAppMsg fun_ty arg_ty arg
373 err2 = mkNonFunAppMsg fun_ty arg_ty arg
374 ; case splitFunTy_maybe fun_ty of
376 do { checkTys arg arg_ty err1
378 _ -> failWithL err2 }
382 checkKinds :: Var -> OutType -> LintM ()
383 -- Both args have had substitution applied
384 checkKinds tyvar arg_ty
385 -- Arg type might be boxed for a function with an uncommitted
386 -- tyvar; notably this is used so that we can give
387 -- error :: forall a:*. String -> a
388 -- and then apply it to both boxed and unboxed types.
389 | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
390 ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
391 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
392 | otherwise = do { arg_kind <- lintType arg_ty
393 ; unless (arg_kind `isSubKind` tyvar_kind)
394 (addErrL (mkKindErrMsg tyvar arg_ty)) }
396 tyvar_kind = tyVarKind tyvar
397 (s1,t1) = coVarKind tyvar
399 checkDeadIdOcc :: Id -> LintM ()
400 -- Occurrences of an Id should never be dead....
401 -- except when we are checking a case pattern
403 | isDeadOcc (idOccInfo id)
404 = do { in_case <- inCasePat
406 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
412 %************************************************************************
414 \subsection[lintCoreAlts]{lintCoreAlts}
416 %************************************************************************
419 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
420 -- a) Check that the alts are non-empty
421 -- b1) Check that the DEFAULT comes first, if it exists
422 -- b2) Check that the others are in increasing order
423 -- c) Check that there's a default for infinite types
424 -- NB: Algebraic cases are not necessarily exhaustive, because
425 -- the simplifer correctly eliminates case that can't
429 = addErrL (mkNullAltsMsg e)
431 checkCaseAlts e ty alts =
432 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
433 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
434 ; checkL (isJust maybe_deflt || not is_infinite_ty)
435 (nonExhaustiveAltsMsg e) }
437 (con_alts, maybe_deflt) = findDefault alts
439 -- Check that successive alternatives have increasing tags
440 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
441 increasing_tag _ = True
443 non_deflt (DEFAULT, _, _) = False
446 is_infinite_ty = case splitTyConApp_maybe ty of
448 Just (tycon, _) -> isPrimTyCon tycon
452 checkAltExpr :: CoreExpr -> OutType -> LintM ()
453 checkAltExpr expr ann_ty
454 = do { actual_ty <- lintCoreExpr expr
455 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
457 lintCoreAlt :: OutType -- Type of scrutinee
458 -> OutType -- Type of the alternative
462 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
463 do { checkL (null args) (mkDefaultArgsMsg args)
464 ; checkAltExpr rhs alt_ty }
466 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
467 do { checkL (null args) (mkDefaultArgsMsg args)
468 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
469 ; checkAltExpr rhs alt_ty }
471 lit_ty = literalType lit
473 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
474 | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
475 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
476 = addLoc (CaseAlt alt) $ do
477 { -- First instantiate the universally quantified
478 -- type variables of the data constructor
479 -- We've already check
480 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
481 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
483 -- And now bring the new binders into scope
484 ; lintBinders args $ \ args -> do
485 { addLoc (CasePat alt) $ do
486 { -- Check the pattern
487 -- Scrutinee type must be a tycon applicn; checked by caller
488 -- This code is remarkably compact considering what it does!
489 -- NB: args must be in scope here so that the lintCoreArgs
491 -- NB: relies on existential type args coming *after*
492 -- ordinary type args
493 ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
494 ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
497 ; checkAltExpr rhs alt_ty } }
499 | otherwise -- Scrut-ty is wrong shape
500 = addErrL (mkBadAltMsg scrut_ty alt)
503 %************************************************************************
505 \subsection[lint-types]{Types}
507 %************************************************************************
510 -- When we lint binders, we (one at a time and in order):
511 -- 1. Lint var types or kinds (possibly substituting)
512 -- 2. Add the binder to the in scope set, and if its a coercion var,
513 -- we may extend the substitution to reflect its (possibly) new kind
514 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
515 lintBinders [] linterF = linterF []
516 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
517 lintBinders vars $ \ vars' ->
520 lintBinder :: Var -> (Var -> LintM a) -> LintM a
521 lintBinder var linterF
522 | isId var = lintIdBndr var linterF
523 | otherwise = lintTyBndr var linterF
525 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
526 lintTyBndr tv thing_inside
527 = do { subst <- getTvSubst
528 ; let (subst', tv') = substTyVarBndr subst tv
530 ; updateTvSubst subst' (thing_inside tv') }
532 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
533 -- Do substitution on the type of a binder and add the var with this
534 -- new type to the in-scope set of the second argument
535 -- ToDo: lint its rules
537 lintIdBndr id linterF
538 = do { checkL (not (isUnboxedTupleType (idType id)))
539 (mkUnboxedTupleMsg id)
540 -- No variable can be bound to an unboxed tuple.
541 ; lintAndScopeId id $ \id' -> linterF id' }
543 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
544 lintAndScopeIds ids linterF
548 go (id:ids) = lintAndScopeId id $ \id ->
549 lintAndScopeIds ids $ \ids ->
552 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
553 lintAndScopeId id linterF
554 = do { ty <- lintInTy (idType id)
555 ; let id' = setIdType id ty
556 ; addInScopeVar id' $ (linterF id') }
560 %************************************************************************
562 \subsection[lint-monad]{The Lint monad}
564 %************************************************************************
567 lintInTy :: InType -> LintM OutType
568 -- Check the type, and apply the substitution to it
569 -- See Note [Linting type lets]
570 -- ToDo: check the kind structure of the type
572 = addLoc (InType ty) $
573 do { ty' <- applySubst ty
578 lintKind :: Kind -> LintM ()
579 -- Check well-formedness of kinds: *, *->*, etc
580 lintKind (TyConApp tc [])
581 | getUnique tc `elem` kindKeys
583 lintKind (FunTy k1 k2)
584 = lintKind k1 >> lintKind k2
586 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
589 lintTyBndrKind :: OutTyVar -> LintM ()
591 | isCoVar tv = lintCoVarKind tv
592 | otherwise = lintKind (tyVarKind tv)
595 lintCoVarKind :: OutCoVar -> LintM ()
596 -- Check the kind of a coercion binder
598 = do { (ty1,ty2) <- lintSplitCoVar tv
601 ; unless (k1 `eqKind` k2)
602 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
603 , nest 2 (quotes (ppr tv))
607 lintSplitCoVar :: CoVar -> LintM (Type,Type)
609 = case coVarKind_maybe cv of
611 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
612 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
615 lintCoercion :: OutType -> LintM (OutType, OutType)
616 -- Check the kind of a coercion term, returning the kind
617 lintCoercion ty@(TyVarTy tv)
618 = do { checkTyVarInScope tv
619 ; if isCoVar tv then return (coVarKind tv)
620 else return (ty, ty) }
622 lintCoercion ty@(AppTy ty1 ty2)
623 = do { (s1,t1) <- lintCoercion ty1
624 ; (s2,t2) <- lintCoercion ty2
625 ; check_co_app ty (typeKind s1) [s2]
626 ; return (AppTy s1 s2, AppTy t1 t2) }
628 lintCoercion ty@(FunTy ty1 ty2)
629 = do { (s1,t1) <- lintCoercion ty1
630 ; (s2,t2) <- lintCoercion ty2
631 ; check_co_app ty (tyConKind funTyCon) [s1, s2]
632 ; return (FunTy s1 s2, FunTy t1 t2) }
634 lintCoercion ty@(TyConApp tc tys)
635 | Just (ar, rule) <- isCoercionTyCon_maybe tc
636 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
637 ; (s,t) <- rule lintType lintCoercion
639 ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
640 ; check_co_app ty (typeKind s) ss
641 ; return (mkAppTys s ss, mkAppTys t ts) }
643 | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
647 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
648 ; check_co_app ty (tyConKind tc) ss
649 ; return (TyConApp tc ss, TyConApp tc ts) }
651 lintCoercion ty@(PredTy (ClassP cls tys))
652 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
653 ; check_co_app ty (tyConKind (classTyCon cls)) ss
654 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
656 lintCoercion (PredTy (IParam n p_ty))
657 = do { (s,t) <- lintCoercion p_ty
658 ; return (PredTy (IParam n s), PredTy (IParam n t)) }
660 lintCoercion ty@(PredTy (EqPred {}))
661 = failWithL (badEq ty)
663 lintCoercion (ForAllTy tv ty)
665 = do { (co1, co2) <- lintSplitCoVar tv
666 ; (s1,t1) <- lintCoercion co1
667 ; (s2,t2) <- lintCoercion co2
668 ; (sr,tr) <- lintCoercion ty
669 ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
672 = do { lintKind (tyVarKind tv)
673 ; (s,t) <- addInScopeVar tv (lintCoercion ty)
674 ; return (ForAllTy tv s, ForAllTy tv t) }
676 badCo :: Coercion -> LintM a
677 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
680 lintType :: OutType -> LintM Kind
681 lintType (TyVarTy tv)
682 = do { checkTyVarInScope tv
683 ; return (tyVarKind tv) }
685 lintType ty@(AppTy t1 t2)
686 = do { k1 <- lintType t1
687 ; lint_ty_app ty k1 [t2] }
689 lintType ty@(FunTy t1 t2)
690 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
692 lintType ty@(TyConApp tc tys)
694 = lint_ty_app ty (tyConKind tc) tys
696 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
698 lintType (ForAllTy tv ty)
699 = do { lintTyBndrKind tv
700 ; addInScopeVar tv (lintType ty) }
702 lintType ty@(PredTy (ClassP cls tys))
703 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
705 lintType (PredTy (IParam _ p_ty))
708 lintType ty@(PredTy (EqPred {}))
709 = failWithL (badEq ty)
712 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
714 = do { ks <- mapM lintType tys
715 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
718 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
719 check_co_app ty k tys
720 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
725 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
726 lint_kind_app doc kfn ks = go kfn ks
728 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
729 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
730 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
732 go kfn [] = return kfn
733 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
734 Nothing -> failWithL fail_msg
735 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
739 badEq :: Type -> SDoc
740 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
744 %************************************************************************
746 \subsection[lint-monad]{The Lint monad}
748 %************************************************************************
753 [LintLocInfo] -> -- Locations
754 TvSubst -> -- Current type substitution; we also use this
755 -- to keep track of all the variables in scope,
756 -- both Ids and TyVars
757 WarnsAndErrs -> -- Error and warning messages so far
758 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
760 type WarnsAndErrs = (Bag Message, Bag Message)
762 {- Note [Type substitution]
763 ~~~~~~~~~~~~~~~~~~~~~~~~
764 Why do we need a type substitution? Consider
765 /\(a:*). \(x:a). /\(a:*). id a x
766 This is ill typed, because (renaming variables) it is really
767 /\(a:*). \(x:a). /\(b:*). id b x
768 Hence, when checking an application, we can't naively compare x's type
769 (at its binding site) with its expected type (at a use site). So we
770 rename type binders as we go, maintaining a substitution.
772 The same substitution also supports let-type, current expressed as
774 Here we substitute 'ty' for 'a' in 'body', on the fly.
777 instance Monad LintM where
778 return x = LintM (\ _ _ errs -> (Just x, errs))
779 fail err = failWithL (text err)
780 m >>= k = LintM (\ loc subst errs ->
781 let (res, errs') = unLintM m loc subst errs in
783 Just r -> unLintM (k r) loc subst errs'
784 Nothing -> (Nothing, errs'))
787 = RhsOf Id -- The variable bound
788 | LambdaBodyOf Id -- The lambda-binder
789 | BodyOfLetRec [Id] -- One of the binders
790 | CaseAlt CoreAlt -- Case alternative
791 | CasePat CoreAlt -- The *pattern* of the case alternative
792 | AnExpr CoreExpr -- Some expression
793 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
795 | InType Type -- Inside a type
800 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
802 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
807 checkL :: Bool -> Message -> LintM ()
808 checkL True _ = return ()
809 checkL False msg = failWithL msg
811 failWithL :: Message -> LintM a
812 failWithL msg = LintM $ \ loc subst (warns,errs) ->
813 (Nothing, (warns, addMsg subst errs msg loc))
815 addErrL :: Message -> LintM ()
816 addErrL msg = LintM $ \ loc subst (warns,errs) ->
817 (Just (), (warns, addMsg subst errs msg loc))
819 addWarnL :: Message -> LintM ()
820 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
821 (Just (), (addMsg subst warns msg loc, errs))
823 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
824 addMsg subst msgs msg locs
825 = ASSERT( notNull locs )
826 msgs `snocBag` mk_msg msg
828 (loc, cxt1) = dumpLoc (head locs)
829 cxts = [snd (dumpLoc loc) | loc <- locs]
830 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
831 ptext (sLit "Substitution:") <+> ppr subst
834 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
836 addLoc :: LintLocInfo -> LintM a -> LintM a
838 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
840 inCasePat :: LintM Bool -- A slight hack; see the unique call site
841 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
843 is_case_pat (CasePat {} : _) = True
844 is_case_pat _other = False
846 addInScopeVars :: [Var] -> LintM a -> LintM a
847 addInScopeVars vars m
849 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
851 = failWithL (dupVars dups)
853 (_, dups) = removeDups compare vars
855 addInScopeVar :: Var -> LintM a -> LintM a
857 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
859 updateTvSubst :: TvSubst -> LintM a -> LintM a
860 updateTvSubst subst' m =
861 LintM (\ loc _ errs -> unLintM m loc subst' errs)
863 getTvSubst :: LintM TvSubst
864 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
866 applySubst :: Type -> LintM Type
867 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
869 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
871 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
875 lookupIdInScope :: Id -> LintM Id
877 | not (mustHaveLocalBinding id)
878 = return id -- An imported Id
880 = do { subst <- getTvSubst
881 ; case lookupInScope (getTvInScope subst) id of
883 Nothing -> do { addErrL out_of_scope
886 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
889 oneTupleDataConId :: Id -- Should not happen
890 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
892 checkBndrIdInScope :: Var -> Var -> LintM ()
893 checkBndrIdInScope binder id
894 = checkInScope msg id
896 msg = ptext (sLit "is out of scope inside info for") <+>
899 checkTyVarInScope :: TyVar -> LintM ()
900 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
902 checkInScope :: SDoc -> Var -> LintM ()
903 checkInScope loc_msg var =
904 do { subst <- getTvSubst
905 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
906 (hsep [ppr var, loc_msg]) }
908 checkTys :: Type -> Type -> Message -> LintM ()
909 -- check ty2 is subtype of ty1 (ie, has same structure but usage
910 -- annotations need only be consistent, not equal)
911 -- Assumes ty1,ty2 are have alrady had the substitution applied
912 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
915 %************************************************************************
917 \subsection{Error messages}
919 %************************************************************************
922 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
925 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
927 dumpLoc (LambdaBodyOf b)
928 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
930 dumpLoc (BodyOfLetRec [])
931 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
933 dumpLoc (BodyOfLetRec bs@(_:_))
934 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
937 = (noSrcLoc, text "In the expression:" <+> ppr e)
939 dumpLoc (CaseAlt (con, args, _))
940 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
942 dumpLoc (CasePat (con, args, _))
943 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
945 dumpLoc (ImportedUnfolding locn)
946 = (locn, brackets (ptext (sLit "in an imported unfolding")))
947 dumpLoc TopLevelBindings
950 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
952 pp_binders :: [Var] -> SDoc
953 pp_binders bs = sep (punctuate comma (map pp_binder bs))
955 pp_binder :: Var -> SDoc
956 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
957 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
961 ------------------------------------------------------
962 -- Messages for case expressions
964 mkNullAltsMsg :: CoreExpr -> Message
966 = hang (text "Case expression with no alternatives:")
969 mkDefaultArgsMsg :: [Var] -> Message
970 mkDefaultArgsMsg args
971 = hang (text "DEFAULT case with binders")
974 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
975 mkCaseAltMsg e ty1 ty2
976 = hang (text "Type of case alternatives not the same as the annotation on case:")
977 4 (vcat [ppr ty1, ppr ty2, ppr e])
979 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
980 mkScrutMsg var var_ty scrut_ty subst
981 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
982 text "Result binder type:" <+> ppr var_ty,--(idType var),
983 text "Scrutinee type:" <+> ppr scrut_ty,
984 hsep [ptext (sLit "Current TV subst"), ppr subst]]
986 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
988 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
989 mkNonIncreasingAltsMsg e
990 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
992 nonExhaustiveAltsMsg :: CoreExpr -> Message
993 nonExhaustiveAltsMsg e
994 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
996 mkBadConMsg :: TyCon -> DataCon -> Message
997 mkBadConMsg tycon datacon
999 text "In a case alternative, data constructor isn't in scrutinee type:",
1000 text "Scrutinee type constructor:" <+> ppr tycon,
1001 text "Data con:" <+> ppr datacon
1004 mkBadPatMsg :: Type -> Type -> Message
1005 mkBadPatMsg con_result_ty scrut_ty
1007 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1008 text "Pattern result type:" <+> ppr con_result_ty,
1009 text "Scrutinee type:" <+> ppr scrut_ty
1012 mkBadAltMsg :: Type -> CoreAlt -> Message
1013 mkBadAltMsg scrut_ty alt
1014 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1015 text "Scrutinee type:" <+> ppr scrut_ty,
1016 text "Alternative:" <+> pprCoreAlt alt ]
1018 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1019 mkNewTyDataConAltMsg scrut_ty alt
1020 = vcat [ text "Data alternative for newtype datacon",
1021 text "Scrutinee type:" <+> ppr scrut_ty,
1022 text "Alternative:" <+> pprCoreAlt alt ]
1025 ------------------------------------------------------
1026 -- Other error messages
1028 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1029 mkAppMsg fun_ty arg_ty arg
1030 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1031 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1032 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1033 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1035 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1036 mkNonFunAppMsg fun_ty arg_ty arg
1037 = vcat [ptext (sLit "Non-function type in function position"),
1038 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1039 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1040 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1042 mkKindErrMsg :: TyVar -> Type -> Message
1043 mkKindErrMsg tyvar arg_ty
1044 = vcat [ptext (sLit "Kinds don't match in type application:"),
1045 hang (ptext (sLit "Type variable:"))
1046 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1047 hang (ptext (sLit "Arg type:"))
1048 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1050 mkCoAppErrMsg :: TyVar -> Type -> Message
1051 mkCoAppErrMsg tyvar arg_ty
1052 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1053 hang (ptext (sLit "Coercion variable:"))
1054 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1055 hang (ptext (sLit "Arg coercion:"))
1056 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1058 mkTyAppMsg :: Type -> Type -> Message
1059 mkTyAppMsg ty arg_ty
1060 = vcat [text "Illegal type application:",
1061 hang (ptext (sLit "Exp type:"))
1062 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1063 hang (ptext (sLit "Arg type:"))
1064 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1066 mkRhsMsg :: Id -> Type -> Message
1069 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1071 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1072 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1074 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1075 mkRhsPrimMsg binder _rhs
1076 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1078 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1081 mkStrictMsg :: Id -> Message
1083 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1085 hsep [ptext (sLit "Binder's demand info:"), ppr (idNewDemandInfo binder)]
1088 mkArityMsg :: Id -> Message
1090 = vcat [hsep [ptext (sLit "Demand type has "),
1091 ppr (dmdTypeDepth dmd_ty),
1092 ptext (sLit " arguments, rhs has "),
1093 ppr (idArity binder),
1094 ptext (sLit "arguments, "),
1096 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1099 where (StrictSig dmd_ty) = idNewStrictness binder
1101 mkUnboxedTupleMsg :: Id -> Message
1102 mkUnboxedTupleMsg binder
1103 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1104 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1106 mkCastErr :: Type -> Type -> Message
1107 mkCastErr from_ty expr_ty
1108 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1109 ptext (sLit "From-type:") <+> ppr from_ty,
1110 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1113 dupVars :: [[Var]] -> Message
1115 = hang (ptext (sLit "Duplicate variables brought into scope"))