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 (isNonRuleLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
193 (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
194 -- Only non-rule loop breakers inhibit inlining
196 -- Check whether arity and demand type are consistent (only if demand analysis
198 ; checkL (case maybeDmdTy of
199 Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
201 (mkArityMsg binder) }
203 -- We should check the unfolding, if any, but this is tricky because
204 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
206 binder_ty = idType binder
207 maybeDmdTy = idStrictness_maybe binder
208 bndr_vars = varSetElems (idFreeVars binder)
209 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
210 | otherwise = return ()
213 %************************************************************************
215 \subsection[lintCoreExpr]{lintCoreExpr}
217 %************************************************************************
220 type InType = Type -- Substitution not yet applied
224 type OutType = Type -- Substitution has been applied to this
226 type OutTyVar = TyVar
227 type OutCoVar = CoVar
229 lintCoreExpr :: CoreExpr -> LintM OutType
230 -- The returned type has the substitution from the monad
231 -- already applied to it:
232 -- lintCoreExpr e subst = exprType (subst e)
234 -- The returned "type" can be a kind, if the expression is (Type ty)
236 lintCoreExpr (Var var)
237 = do { checkL (not (var == oneTupleDataConId))
238 (ptext (sLit "Illegal one-tuple"))
241 ; var' <- lookupIdInScope var
242 ; return (idType var')
245 lintCoreExpr (Lit lit)
246 = return (literalType lit)
248 lintCoreExpr (Cast expr co)
249 = do { expr_ty <- lintCoreExpr expr
250 ; co' <- applySubst co
251 ; (from_ty, to_ty) <- lintCoercion co'
252 ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
255 lintCoreExpr (Note _ expr)
258 lintCoreExpr (Let (NonRec tv (Type ty)) body)
259 = -- See Note [Type let] in CoreSyn
260 do { checkL (isTyVar tv) (mkKindErrMsg tv ty) -- Not quite accurate
262 ; lintTyBndr tv $ \ tv' ->
263 addLoc (BodyOfLetRec [tv]) $
264 extendSubstL tv' ty' $ do
266 -- Now extend the substitution so we
267 -- take advantage of it in the body
268 ; lintCoreExpr body } }
270 lintCoreExpr (Let (NonRec bndr rhs) body)
271 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
272 ; addLoc (BodyOfLetRec [bndr])
273 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
275 lintCoreExpr (Let (Rec pairs) body)
276 = lintAndScopeIds bndrs $ \_ ->
277 do { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
278 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
280 bndrs = map fst pairs
282 lintCoreExpr e@(App fun arg)
283 = do { fun_ty <- lintCoreExpr fun
284 ; addLoc (AnExpr e) $
285 lintCoreArg fun_ty arg }
287 lintCoreExpr (Lam var expr)
288 = addLoc (LambdaBodyOf var) $
289 lintBinders [var] $ \[var'] ->
290 do { body_ty <- lintCoreExpr expr
292 return (mkFunTy (idType var') body_ty)
294 return (mkForAllTy var' body_ty)
296 -- The applySubst is needed to apply the subst to var
298 lintCoreExpr e@(Case scrut var alt_ty alts) =
299 -- Check the scrutinee
300 do { scrut_ty <- lintCoreExpr scrut
301 ; alt_ty <- lintInTy alt_ty
302 ; var_ty <- lintInTy (idType var)
304 ; let mb_tc_app = splitTyConApp_maybe (idType var)
309 not (isOpenTyCon tycon) &&
310 null (tyConDataCons tycon) ->
311 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
312 -- This can legitimately happen for type families
314 _otherwise -> return ()
316 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
318 ; subst <- getTvSubst
319 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
321 -- If the binder is an unboxed tuple type, don't put it in scope
322 ; let scope = if (isUnboxedTupleType (idType var)) then
324 else lintAndScopeId var
326 do { -- Check the alternatives
327 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
328 ; checkCaseAlts e scrut_ty alts
333 lintCoreExpr (Type ty)
334 = do { ty' <- lintInTy ty
335 ; return (typeKind ty') }
338 %************************************************************************
340 \subsection[lintCoreArgs]{lintCoreArgs}
342 %************************************************************************
344 The basic version of these functions checks that the argument is a
345 subtype of the required type, as one would expect.
348 lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
349 lintCoreArg :: OutType -> CoreArg -> LintM OutType
350 -- First argument has already had substitution applied to it
354 lintCoreArgs ty [] = return ty
355 lintCoreArgs ty (a : args) =
356 do { res <- lintCoreArg ty a
357 ; lintCoreArgs res args }
359 lintCoreArg fun_ty (Type arg_ty)
360 | Just (tyvar,body) <- splitForAllTy_maybe fun_ty
361 = do { arg_ty' <- applySubst arg_ty
362 ; checkKinds tyvar arg_ty'
363 ; if isCoVar tyvar then
364 return body -- Co-vars don't appear in body!
366 return (substTyWith [tyvar] [arg_ty'] body) }
368 = failWithL (mkTyAppMsg fun_ty arg_ty)
370 lintCoreArg fun_ty arg
371 -- Make sure function type matches argument
372 = do { arg_ty <- lintCoreExpr arg
373 ; let err1 = mkAppMsg fun_ty arg_ty arg
374 err2 = mkNonFunAppMsg fun_ty arg_ty arg
375 ; case splitFunTy_maybe fun_ty of
377 do { checkTys arg arg_ty err1
379 _ -> failWithL err2 }
383 checkKinds :: Var -> OutType -> LintM ()
384 -- Both args have had substitution applied
385 checkKinds tyvar arg_ty
386 -- Arg type might be boxed for a function with an uncommitted
387 -- tyvar; notably this is used so that we can give
388 -- error :: forall a:*. String -> a
389 -- and then apply it to both boxed and unboxed types.
390 | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
391 ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
392 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
393 | otherwise = do { arg_kind <- lintType arg_ty
394 ; unless (arg_kind `isSubKind` tyvar_kind)
395 (addErrL (mkKindErrMsg tyvar arg_ty)) }
397 tyvar_kind = tyVarKind tyvar
398 (s1,t1) = coVarKind tyvar
400 checkDeadIdOcc :: Id -> LintM ()
401 -- Occurrences of an Id should never be dead....
402 -- except when we are checking a case pattern
404 | isDeadOcc (idOccInfo id)
405 = do { in_case <- inCasePat
407 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
413 %************************************************************************
415 \subsection[lintCoreAlts]{lintCoreAlts}
417 %************************************************************************
420 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
421 -- a) Check that the alts are non-empty
422 -- b1) Check that the DEFAULT comes first, if it exists
423 -- b2) Check that the others are in increasing order
424 -- c) Check that there's a default for infinite types
425 -- NB: Algebraic cases are not necessarily exhaustive, because
426 -- the simplifer correctly eliminates case that can't
430 = addErrL (mkNullAltsMsg e)
432 checkCaseAlts e ty alts =
433 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
434 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
435 ; checkL (isJust maybe_deflt || not is_infinite_ty)
436 (nonExhaustiveAltsMsg e) }
438 (con_alts, maybe_deflt) = findDefault alts
440 -- Check that successive alternatives have increasing tags
441 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
442 increasing_tag _ = True
444 non_deflt (DEFAULT, _, _) = False
447 is_infinite_ty = case splitTyConApp_maybe ty of
449 Just (tycon, _) -> isPrimTyCon tycon
453 checkAltExpr :: CoreExpr -> OutType -> LintM ()
454 checkAltExpr expr ann_ty
455 = do { actual_ty <- lintCoreExpr expr
456 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
458 lintCoreAlt :: OutType -- Type of scrutinee
459 -> OutType -- Type of the alternative
463 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
464 do { checkL (null args) (mkDefaultArgsMsg args)
465 ; checkAltExpr rhs alt_ty }
467 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
468 do { checkL (null args) (mkDefaultArgsMsg args)
469 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
470 ; checkAltExpr rhs alt_ty }
472 lit_ty = literalType lit
474 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
475 | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
476 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
477 = addLoc (CaseAlt alt) $ do
478 { -- First instantiate the universally quantified
479 -- type variables of the data constructor
480 -- We've already check
481 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
482 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
484 -- And now bring the new binders into scope
485 ; lintBinders args $ \ args -> do
486 { addLoc (CasePat alt) $ do
487 { -- Check the pattern
488 -- Scrutinee type must be a tycon applicn; checked by caller
489 -- This code is remarkably compact considering what it does!
490 -- NB: args must be in scope here so that the lintCoreArgs
492 -- NB: relies on existential type args coming *after*
493 -- ordinary type args
494 ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
495 ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
498 ; checkAltExpr rhs alt_ty } }
500 | otherwise -- Scrut-ty is wrong shape
501 = addErrL (mkBadAltMsg scrut_ty alt)
504 %************************************************************************
506 \subsection[lint-types]{Types}
508 %************************************************************************
511 -- When we lint binders, we (one at a time and in order):
512 -- 1. Lint var types or kinds (possibly substituting)
513 -- 2. Add the binder to the in scope set, and if its a coercion var,
514 -- we may extend the substitution to reflect its (possibly) new kind
515 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
516 lintBinders [] linterF = linterF []
517 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
518 lintBinders vars $ \ vars' ->
521 lintBinder :: Var -> (Var -> LintM a) -> LintM a
522 lintBinder var linterF
523 | isId var = lintIdBndr var linterF
524 | otherwise = lintTyBndr var linterF
526 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
527 lintTyBndr tv thing_inside
528 = do { subst <- getTvSubst
529 ; let (subst', tv') = substTyVarBndr subst tv
531 ; updateTvSubst subst' (thing_inside tv') }
533 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
534 -- Do substitution on the type of a binder and add the var with this
535 -- new type to the in-scope set of the second argument
536 -- ToDo: lint its rules
538 lintIdBndr id linterF
539 = do { checkL (not (isUnboxedTupleType (idType id)))
540 (mkUnboxedTupleMsg id)
541 -- No variable can be bound to an unboxed tuple.
542 ; lintAndScopeId id $ \id' -> linterF id' }
544 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
545 lintAndScopeIds ids linterF
549 go (id:ids) = lintAndScopeId id $ \id ->
550 lintAndScopeIds ids $ \ids ->
553 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
554 lintAndScopeId id linterF
555 = do { ty <- lintInTy (idType id)
556 ; let id' = setIdType id ty
557 ; addInScopeVar id' $ (linterF id') }
561 %************************************************************************
563 \subsection[lint-monad]{The Lint monad}
565 %************************************************************************
568 lintInTy :: InType -> LintM OutType
569 -- Check the type, and apply the substitution to it
570 -- See Note [Linting type lets]
571 -- ToDo: check the kind structure of the type
573 = addLoc (InType ty) $
574 do { ty' <- applySubst ty
579 lintKind :: Kind -> LintM ()
580 -- Check well-formedness of kinds: *, *->*, etc
581 lintKind (TyConApp tc [])
582 | getUnique tc `elem` kindKeys
584 lintKind (FunTy k1 k2)
585 = lintKind k1 >> lintKind k2
587 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
590 lintTyBndrKind :: OutTyVar -> LintM ()
592 | isCoVar tv = lintCoVarKind tv
593 | otherwise = lintKind (tyVarKind tv)
596 lintCoVarKind :: OutCoVar -> LintM ()
597 -- Check the kind of a coercion binder
599 = do { (ty1,ty2) <- lintSplitCoVar tv
602 ; unless (k1 `eqKind` k2)
603 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
604 , nest 2 (quotes (ppr tv))
608 lintSplitCoVar :: CoVar -> LintM (Type,Type)
610 = case coVarKind_maybe cv of
612 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
613 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
616 lintCoercion :: OutType -> LintM (OutType, OutType)
617 -- Check the kind of a coercion term, returning the kind
618 lintCoercion ty@(TyVarTy tv)
619 = do { checkTyVarInScope tv
620 ; if isCoVar tv then return (coVarKind tv)
621 else return (ty, ty) }
623 lintCoercion ty@(AppTy ty1 ty2)
624 = do { (s1,t1) <- lintCoercion ty1
625 ; (s2,t2) <- lintCoercion ty2
626 ; check_co_app ty (typeKind s1) [s2]
627 ; return (AppTy s1 s2, AppTy t1 t2) }
629 lintCoercion ty@(FunTy ty1 ty2)
630 = do { (s1,t1) <- lintCoercion ty1
631 ; (s2,t2) <- lintCoercion ty2
632 ; check_co_app ty (tyConKind funTyCon) [s1, s2]
633 ; return (FunTy s1 s2, FunTy t1 t2) }
635 lintCoercion ty@(TyConApp tc tys)
636 | Just (ar, desc) <- isCoercionTyCon_maybe tc
637 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
638 ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
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 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
681 -- Always called with correct number of coercion arguments
682 -- First arg is just for error message
683 lintCoTyConApp _ CoLeft (co:_) = lintLR fst co
684 lintCoTyConApp _ CoRight (co:_) = lintLR snd co
685 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co
686 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co
687 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
689 lintCoTyConApp _ CoSym (co:_)
690 = do { (ty1,ty2) <- lintCoercion co
693 lintCoTyConApp co CoTrans (co1:co2:_)
694 = do { (ty1a, ty1b) <- lintCoercion co1
695 ; (ty2a, ty2b) <- lintCoercion co2
696 ; checkL (ty1b `coreEqType` ty2a)
697 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
698 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
699 ; return (ty1a, ty2b) }
701 lintCoTyConApp _ CoInst (co:arg_ty:_)
702 = do { co_tys <- lintCoercion co
703 ; arg_kind <- lintType arg_ty
704 ; case decompInst_maybe co_tys of
705 Just ((tv1,tv2), (ty1,ty2))
706 | arg_kind `isSubKind` tyVarKind tv1
707 -> return (substTyWith [tv1] [arg_ty] ty1,
708 substTyWith [tv2] [arg_ty] ty2)
710 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
711 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
713 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
714 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
715 = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
716 ; sequence_ (zipWith checkKinds tvs tys1)
717 ; return (substTyWith tvs tys1 lhs_ty,
718 substTyWith tvs tys2 rhs_ty) }
720 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
721 = do { _ <- lintType ty1
722 ; _ <- lintType ty2 -- Ignore kinds; it's unsafe!
725 lintCoTyConApp _ _ _ = panic "lintCoTyConApp" -- Called with wrong number of coercion args
728 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
730 = do { (ty1,ty2) <- lintCoercion co
731 ; case decompLR_maybe (ty1,ty2) of
732 Just res -> return (sel res)
733 Nothing -> failWithL (ptext (sLit "Bad argument of left/right")) }
736 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
738 = do { (ty1,ty2) <- lintCoercion co
739 ; case decompCsel_maybe (ty1,ty2) of
740 Just res -> return (sel res)
741 Nothing -> failWithL (ptext (sLit "Bad argument of csel")) }
744 lintType :: OutType -> LintM Kind
745 lintType (TyVarTy tv)
746 = do { checkTyVarInScope tv
747 ; return (tyVarKind tv) }
749 lintType ty@(AppTy t1 t2)
750 = do { k1 <- lintType t1
751 ; lint_ty_app ty k1 [t2] }
753 lintType ty@(FunTy t1 t2)
754 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
756 lintType ty@(TyConApp tc tys)
758 = lint_ty_app ty (tyConKind tc) tys
760 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
762 lintType (ForAllTy tv ty)
763 = do { lintTyBndrKind tv
764 ; addInScopeVar tv (lintType ty) }
766 lintType ty@(PredTy (ClassP cls tys))
767 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
769 lintType (PredTy (IParam _ p_ty))
772 lintType ty@(PredTy (EqPred {}))
773 = failWithL (badEq ty)
776 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
778 = do { ks <- mapM lintType tys
779 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
782 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
783 check_co_app ty k tys
784 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
789 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
790 lint_kind_app doc kfn ks = go kfn ks
792 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
793 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
794 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
796 go kfn [] = return kfn
797 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
798 Nothing -> failWithL fail_msg
799 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
803 badEq :: Type -> SDoc
804 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
808 %************************************************************************
810 \subsection[lint-monad]{The Lint monad}
812 %************************************************************************
817 [LintLocInfo] -> -- Locations
818 TvSubst -> -- Current type substitution; we also use this
819 -- to keep track of all the variables in scope,
820 -- both Ids and TyVars
821 WarnsAndErrs -> -- Error and warning messages so far
822 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
824 type WarnsAndErrs = (Bag Message, Bag Message)
826 {- Note [Type substitution]
827 ~~~~~~~~~~~~~~~~~~~~~~~~
828 Why do we need a type substitution? Consider
829 /\(a:*). \(x:a). /\(a:*). id a x
830 This is ill typed, because (renaming variables) it is really
831 /\(a:*). \(x:a). /\(b:*). id b x
832 Hence, when checking an application, we can't naively compare x's type
833 (at its binding site) with its expected type (at a use site). So we
834 rename type binders as we go, maintaining a substitution.
836 The same substitution also supports let-type, current expressed as
838 Here we substitute 'ty' for 'a' in 'body', on the fly.
841 instance Monad LintM where
842 return x = LintM (\ _ _ errs -> (Just x, errs))
843 fail err = failWithL (text err)
844 m >>= k = LintM (\ loc subst errs ->
845 let (res, errs') = unLintM m loc subst errs in
847 Just r -> unLintM (k r) loc subst errs'
848 Nothing -> (Nothing, errs'))
851 = RhsOf Id -- The variable bound
852 | LambdaBodyOf Id -- The lambda-binder
853 | BodyOfLetRec [Id] -- One of the binders
854 | CaseAlt CoreAlt -- Case alternative
855 | CasePat CoreAlt -- The *pattern* of the case alternative
856 | AnExpr CoreExpr -- Some expression
857 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
859 | InType Type -- Inside a type
864 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
866 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
871 checkL :: Bool -> Message -> LintM ()
872 checkL True _ = return ()
873 checkL False msg = failWithL msg
875 failWithL :: Message -> LintM a
876 failWithL msg = LintM $ \ loc subst (warns,errs) ->
877 (Nothing, (warns, addMsg subst errs msg loc))
879 addErrL :: Message -> LintM ()
880 addErrL msg = LintM $ \ loc subst (warns,errs) ->
881 (Just (), (warns, addMsg subst errs msg loc))
883 addWarnL :: Message -> LintM ()
884 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
885 (Just (), (addMsg subst warns msg loc, errs))
887 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
888 addMsg subst msgs msg locs
889 = ASSERT( notNull locs )
890 msgs `snocBag` mk_msg msg
892 (loc, cxt1) = dumpLoc (head locs)
893 cxts = [snd (dumpLoc loc) | loc <- locs]
894 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
895 ptext (sLit "Substitution:") <+> ppr subst
898 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
900 addLoc :: LintLocInfo -> LintM a -> LintM a
902 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
904 inCasePat :: LintM Bool -- A slight hack; see the unique call site
905 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
907 is_case_pat (CasePat {} : _) = True
908 is_case_pat _other = False
910 addInScopeVars :: [Var] -> LintM a -> LintM a
911 addInScopeVars vars m
913 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
915 = failWithL (dupVars dups)
917 (_, dups) = removeDups compare vars
919 addInScopeVar :: Var -> LintM a -> LintM a
921 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
923 updateTvSubst :: TvSubst -> LintM a -> LintM a
924 updateTvSubst subst' m =
925 LintM (\ loc _ errs -> unLintM m loc subst' errs)
927 getTvSubst :: LintM TvSubst
928 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
930 applySubst :: Type -> LintM Type
931 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
933 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
935 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
939 lookupIdInScope :: Id -> LintM Id
941 | not (mustHaveLocalBinding id)
942 = return id -- An imported Id
944 = do { subst <- getTvSubst
945 ; case lookupInScope (getTvInScope subst) id of
947 Nothing -> do { addErrL out_of_scope
950 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
953 oneTupleDataConId :: Id -- Should not happen
954 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
956 checkBndrIdInScope :: Var -> Var -> LintM ()
957 checkBndrIdInScope binder id
958 = checkInScope msg id
960 msg = ptext (sLit "is out of scope inside info for") <+>
963 checkTyVarInScope :: TyVar -> LintM ()
964 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
966 checkInScope :: SDoc -> Var -> LintM ()
967 checkInScope loc_msg var =
968 do { subst <- getTvSubst
969 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
970 (hsep [ppr var, loc_msg]) }
972 checkTys :: Type -> Type -> Message -> LintM ()
973 -- check ty2 is subtype of ty1 (ie, has same structure but usage
974 -- annotations need only be consistent, not equal)
975 -- Assumes ty1,ty2 are have alrady had the substitution applied
976 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
979 %************************************************************************
981 \subsection{Error messages}
983 %************************************************************************
986 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
989 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
991 dumpLoc (LambdaBodyOf b)
992 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
994 dumpLoc (BodyOfLetRec [])
995 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
997 dumpLoc (BodyOfLetRec bs@(_:_))
998 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1001 = (noSrcLoc, text "In the expression:" <+> ppr e)
1003 dumpLoc (CaseAlt (con, args, _))
1004 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1006 dumpLoc (CasePat (con, args, _))
1007 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1009 dumpLoc (ImportedUnfolding locn)
1010 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1011 dumpLoc TopLevelBindings
1014 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1016 pp_binders :: [Var] -> SDoc
1017 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1019 pp_binder :: Var -> SDoc
1020 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1021 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1025 ------------------------------------------------------
1026 -- Messages for case expressions
1028 mkNullAltsMsg :: CoreExpr -> Message
1030 = hang (text "Case expression with no alternatives:")
1033 mkDefaultArgsMsg :: [Var] -> Message
1034 mkDefaultArgsMsg args
1035 = hang (text "DEFAULT case with binders")
1038 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1039 mkCaseAltMsg e ty1 ty2
1040 = hang (text "Type of case alternatives not the same as the annotation on case:")
1041 4 (vcat [ppr ty1, ppr ty2, ppr e])
1043 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1044 mkScrutMsg var var_ty scrut_ty subst
1045 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1046 text "Result binder type:" <+> ppr var_ty,--(idType var),
1047 text "Scrutinee type:" <+> ppr scrut_ty,
1048 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1050 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1052 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1053 mkNonIncreasingAltsMsg e
1054 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1056 nonExhaustiveAltsMsg :: CoreExpr -> Message
1057 nonExhaustiveAltsMsg e
1058 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1060 mkBadConMsg :: TyCon -> DataCon -> Message
1061 mkBadConMsg tycon datacon
1063 text "In a case alternative, data constructor isn't in scrutinee type:",
1064 text "Scrutinee type constructor:" <+> ppr tycon,
1065 text "Data con:" <+> ppr datacon
1068 mkBadPatMsg :: Type -> Type -> Message
1069 mkBadPatMsg con_result_ty scrut_ty
1071 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1072 text "Pattern result type:" <+> ppr con_result_ty,
1073 text "Scrutinee type:" <+> ppr scrut_ty
1076 mkBadAltMsg :: Type -> CoreAlt -> Message
1077 mkBadAltMsg scrut_ty alt
1078 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1079 text "Scrutinee type:" <+> ppr scrut_ty,
1080 text "Alternative:" <+> pprCoreAlt alt ]
1082 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1083 mkNewTyDataConAltMsg scrut_ty alt
1084 = vcat [ text "Data alternative for newtype datacon",
1085 text "Scrutinee type:" <+> ppr scrut_ty,
1086 text "Alternative:" <+> pprCoreAlt alt ]
1089 ------------------------------------------------------
1090 -- Other error messages
1092 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1093 mkAppMsg fun_ty arg_ty arg
1094 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1095 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1096 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1097 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1099 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1100 mkNonFunAppMsg fun_ty arg_ty arg
1101 = vcat [ptext (sLit "Non-function type in function position"),
1102 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1103 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1104 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1106 mkKindErrMsg :: TyVar -> Type -> Message
1107 mkKindErrMsg tyvar arg_ty
1108 = vcat [ptext (sLit "Kinds don't match in type application:"),
1109 hang (ptext (sLit "Type variable:"))
1110 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1111 hang (ptext (sLit "Arg type:"))
1112 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1114 mkCoAppErrMsg :: TyVar -> Type -> Message
1115 mkCoAppErrMsg tyvar arg_ty
1116 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1117 hang (ptext (sLit "Coercion variable:"))
1118 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1119 hang (ptext (sLit "Arg coercion:"))
1120 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1122 mkTyAppMsg :: Type -> Type -> Message
1123 mkTyAppMsg ty arg_ty
1124 = vcat [text "Illegal type application:",
1125 hang (ptext (sLit "Exp type:"))
1126 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1127 hang (ptext (sLit "Arg type:"))
1128 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1130 mkRhsMsg :: Id -> Type -> Message
1133 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1135 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1136 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1138 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1139 mkRhsPrimMsg binder _rhs
1140 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1142 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1145 mkStrictMsg :: Id -> Message
1147 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1149 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1152 mkArityMsg :: Id -> Message
1154 = vcat [hsep [ptext (sLit "Demand type has "),
1155 ppr (dmdTypeDepth dmd_ty),
1156 ptext (sLit " arguments, rhs has "),
1157 ppr (idArity binder),
1158 ptext (sLit "arguments, "),
1160 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1163 where (StrictSig dmd_ty) = idStrictness binder
1165 mkUnboxedTupleMsg :: Id -> Message
1166 mkUnboxedTupleMsg binder
1167 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1168 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1170 mkCastErr :: Type -> Type -> Message
1171 mkCastErr from_ty expr_ty
1172 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1173 ptext (sLit "From-type:") <+> ppr from_ty,
1174 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1177 dupVars :: [[Var]] -> Message
1179 = hang (ptext (sLit "Duplicate variables brought into scope"))