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, rule) <- isCoercionTyCon_maybe tc
637 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
638 ; (s,t) <- rule lintType lintCoercion
640 ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
641 ; check_co_app ty (typeKind s) ss
642 ; return (mkAppTys s ss, mkAppTys t ts) }
644 | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
648 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
649 ; check_co_app ty (tyConKind tc) ss
650 ; return (TyConApp tc ss, TyConApp tc ts) }
652 lintCoercion ty@(PredTy (ClassP cls tys))
653 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
654 ; check_co_app ty (tyConKind (classTyCon cls)) ss
655 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
657 lintCoercion (PredTy (IParam n p_ty))
658 = do { (s,t) <- lintCoercion p_ty
659 ; return (PredTy (IParam n s), PredTy (IParam n t)) }
661 lintCoercion ty@(PredTy (EqPred {}))
662 = failWithL (badEq ty)
664 lintCoercion (ForAllTy tv ty)
666 = do { (co1, co2) <- lintSplitCoVar tv
667 ; (s1,t1) <- lintCoercion co1
668 ; (s2,t2) <- lintCoercion co2
669 ; (sr,tr) <- lintCoercion ty
670 ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
673 = do { lintKind (tyVarKind tv)
674 ; (s,t) <- addInScopeVar tv (lintCoercion ty)
675 ; return (ForAllTy tv s, ForAllTy tv t) }
677 badCo :: Coercion -> LintM a
678 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
681 lintType :: OutType -> LintM Kind
682 lintType (TyVarTy tv)
683 = do { checkTyVarInScope tv
684 ; return (tyVarKind tv) }
686 lintType ty@(AppTy t1 t2)
687 = do { k1 <- lintType t1
688 ; lint_ty_app ty k1 [t2] }
690 lintType ty@(FunTy t1 t2)
691 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
693 lintType ty@(TyConApp tc tys)
695 = lint_ty_app ty (tyConKind tc) tys
697 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
699 lintType (ForAllTy tv ty)
700 = do { lintTyBndrKind tv
701 ; addInScopeVar tv (lintType ty) }
703 lintType ty@(PredTy (ClassP cls tys))
704 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
706 lintType (PredTy (IParam _ p_ty))
709 lintType ty@(PredTy (EqPred {}))
710 = failWithL (badEq ty)
713 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
715 = do { ks <- mapM lintType tys
716 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
719 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
720 check_co_app ty k tys
721 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
726 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
727 lint_kind_app doc kfn ks = go kfn ks
729 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
730 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
731 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
733 go kfn [] = return kfn
734 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
735 Nothing -> failWithL fail_msg
736 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
740 badEq :: Type -> SDoc
741 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
745 %************************************************************************
747 \subsection[lint-monad]{The Lint monad}
749 %************************************************************************
754 [LintLocInfo] -> -- Locations
755 TvSubst -> -- Current type substitution; we also use this
756 -- to keep track of all the variables in scope,
757 -- both Ids and TyVars
758 WarnsAndErrs -> -- Error and warning messages so far
759 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
761 type WarnsAndErrs = (Bag Message, Bag Message)
763 {- Note [Type substitution]
764 ~~~~~~~~~~~~~~~~~~~~~~~~
765 Why do we need a type substitution? Consider
766 /\(a:*). \(x:a). /\(a:*). id a x
767 This is ill typed, because (renaming variables) it is really
768 /\(a:*). \(x:a). /\(b:*). id b x
769 Hence, when checking an application, we can't naively compare x's type
770 (at its binding site) with its expected type (at a use site). So we
771 rename type binders as we go, maintaining a substitution.
773 The same substitution also supports let-type, current expressed as
775 Here we substitute 'ty' for 'a' in 'body', on the fly.
778 instance Monad LintM where
779 return x = LintM (\ _ _ errs -> (Just x, errs))
780 fail err = failWithL (text err)
781 m >>= k = LintM (\ loc subst errs ->
782 let (res, errs') = unLintM m loc subst errs in
784 Just r -> unLintM (k r) loc subst errs'
785 Nothing -> (Nothing, errs'))
788 = RhsOf Id -- The variable bound
789 | LambdaBodyOf Id -- The lambda-binder
790 | BodyOfLetRec [Id] -- One of the binders
791 | CaseAlt CoreAlt -- Case alternative
792 | CasePat CoreAlt -- The *pattern* of the case alternative
793 | AnExpr CoreExpr -- Some expression
794 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
796 | InType Type -- Inside a type
801 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
803 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
808 checkL :: Bool -> Message -> LintM ()
809 checkL True _ = return ()
810 checkL False msg = failWithL msg
812 failWithL :: Message -> LintM a
813 failWithL msg = LintM $ \ loc subst (warns,errs) ->
814 (Nothing, (warns, addMsg subst errs msg loc))
816 addErrL :: Message -> LintM ()
817 addErrL msg = LintM $ \ loc subst (warns,errs) ->
818 (Just (), (warns, addMsg subst errs msg loc))
820 addWarnL :: Message -> LintM ()
821 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
822 (Just (), (addMsg subst warns msg loc, errs))
824 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
825 addMsg subst msgs msg locs
826 = ASSERT( notNull locs )
827 msgs `snocBag` mk_msg msg
829 (loc, cxt1) = dumpLoc (head locs)
830 cxts = [snd (dumpLoc loc) | loc <- locs]
831 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
832 ptext (sLit "Substitution:") <+> ppr subst
835 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
837 addLoc :: LintLocInfo -> LintM a -> LintM a
839 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
841 inCasePat :: LintM Bool -- A slight hack; see the unique call site
842 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
844 is_case_pat (CasePat {} : _) = True
845 is_case_pat _other = False
847 addInScopeVars :: [Var] -> LintM a -> LintM a
848 addInScopeVars vars m
850 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
852 = failWithL (dupVars dups)
854 (_, dups) = removeDups compare vars
856 addInScopeVar :: Var -> LintM a -> LintM a
858 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
860 updateTvSubst :: TvSubst -> LintM a -> LintM a
861 updateTvSubst subst' m =
862 LintM (\ loc _ errs -> unLintM m loc subst' errs)
864 getTvSubst :: LintM TvSubst
865 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
867 applySubst :: Type -> LintM Type
868 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
870 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
872 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
876 lookupIdInScope :: Id -> LintM Id
878 | not (mustHaveLocalBinding id)
879 = return id -- An imported Id
881 = do { subst <- getTvSubst
882 ; case lookupInScope (getTvInScope subst) id of
884 Nothing -> do { addErrL out_of_scope
887 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
890 oneTupleDataConId :: Id -- Should not happen
891 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
893 checkBndrIdInScope :: Var -> Var -> LintM ()
894 checkBndrIdInScope binder id
895 = checkInScope msg id
897 msg = ptext (sLit "is out of scope inside info for") <+>
900 checkTyVarInScope :: TyVar -> LintM ()
901 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
903 checkInScope :: SDoc -> Var -> LintM ()
904 checkInScope loc_msg var =
905 do { subst <- getTvSubst
906 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
907 (hsep [ppr var, loc_msg]) }
909 checkTys :: Type -> Type -> Message -> LintM ()
910 -- check ty2 is subtype of ty1 (ie, has same structure but usage
911 -- annotations need only be consistent, not equal)
912 -- Assumes ty1,ty2 are have alrady had the substitution applied
913 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
916 %************************************************************************
918 \subsection{Error messages}
920 %************************************************************************
923 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
926 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
928 dumpLoc (LambdaBodyOf b)
929 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
931 dumpLoc (BodyOfLetRec [])
932 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
934 dumpLoc (BodyOfLetRec bs@(_:_))
935 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
938 = (noSrcLoc, text "In the expression:" <+> ppr e)
940 dumpLoc (CaseAlt (con, args, _))
941 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
943 dumpLoc (CasePat (con, args, _))
944 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
946 dumpLoc (ImportedUnfolding locn)
947 = (locn, brackets (ptext (sLit "in an imported unfolding")))
948 dumpLoc TopLevelBindings
951 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
953 pp_binders :: [Var] -> SDoc
954 pp_binders bs = sep (punctuate comma (map pp_binder bs))
956 pp_binder :: Var -> SDoc
957 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
958 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
962 ------------------------------------------------------
963 -- Messages for case expressions
965 mkNullAltsMsg :: CoreExpr -> Message
967 = hang (text "Case expression with no alternatives:")
970 mkDefaultArgsMsg :: [Var] -> Message
971 mkDefaultArgsMsg args
972 = hang (text "DEFAULT case with binders")
975 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
976 mkCaseAltMsg e ty1 ty2
977 = hang (text "Type of case alternatives not the same as the annotation on case:")
978 4 (vcat [ppr ty1, ppr ty2, ppr e])
980 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
981 mkScrutMsg var var_ty scrut_ty subst
982 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
983 text "Result binder type:" <+> ppr var_ty,--(idType var),
984 text "Scrutinee type:" <+> ppr scrut_ty,
985 hsep [ptext (sLit "Current TV subst"), ppr subst]]
987 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
989 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
990 mkNonIncreasingAltsMsg e
991 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
993 nonExhaustiveAltsMsg :: CoreExpr -> Message
994 nonExhaustiveAltsMsg e
995 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
997 mkBadConMsg :: TyCon -> DataCon -> Message
998 mkBadConMsg tycon datacon
1000 text "In a case alternative, data constructor isn't in scrutinee type:",
1001 text "Scrutinee type constructor:" <+> ppr tycon,
1002 text "Data con:" <+> ppr datacon
1005 mkBadPatMsg :: Type -> Type -> Message
1006 mkBadPatMsg con_result_ty scrut_ty
1008 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1009 text "Pattern result type:" <+> ppr con_result_ty,
1010 text "Scrutinee type:" <+> ppr scrut_ty
1013 mkBadAltMsg :: Type -> CoreAlt -> Message
1014 mkBadAltMsg scrut_ty alt
1015 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1016 text "Scrutinee type:" <+> ppr scrut_ty,
1017 text "Alternative:" <+> pprCoreAlt alt ]
1019 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1020 mkNewTyDataConAltMsg scrut_ty alt
1021 = vcat [ text "Data alternative for newtype datacon",
1022 text "Scrutinee type:" <+> ppr scrut_ty,
1023 text "Alternative:" <+> pprCoreAlt alt ]
1026 ------------------------------------------------------
1027 -- Other error messages
1029 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1030 mkAppMsg fun_ty arg_ty arg
1031 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1032 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1033 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1034 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1036 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1037 mkNonFunAppMsg fun_ty arg_ty arg
1038 = vcat [ptext (sLit "Non-function type in function position"),
1039 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1040 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1041 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1043 mkKindErrMsg :: TyVar -> Type -> Message
1044 mkKindErrMsg tyvar arg_ty
1045 = vcat [ptext (sLit "Kinds don't match in type application:"),
1046 hang (ptext (sLit "Type variable:"))
1047 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1048 hang (ptext (sLit "Arg type:"))
1049 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1051 mkCoAppErrMsg :: TyVar -> Type -> Message
1052 mkCoAppErrMsg tyvar arg_ty
1053 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1054 hang (ptext (sLit "Coercion variable:"))
1055 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1056 hang (ptext (sLit "Arg coercion:"))
1057 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1059 mkTyAppMsg :: Type -> Type -> Message
1060 mkTyAppMsg ty arg_ty
1061 = vcat [text "Illegal type application:",
1062 hang (ptext (sLit "Exp type:"))
1063 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1064 hang (ptext (sLit "Arg type:"))
1065 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1067 mkRhsMsg :: Id -> Type -> Message
1070 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1072 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1073 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1075 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1076 mkRhsPrimMsg binder _rhs
1077 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1079 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1082 mkStrictMsg :: Id -> Message
1084 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1086 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1089 mkArityMsg :: Id -> Message
1091 = vcat [hsep [ptext (sLit "Demand type has "),
1092 ppr (dmdTypeDepth dmd_ty),
1093 ptext (sLit " arguments, rhs has "),
1094 ppr (idArity binder),
1095 ptext (sLit "arguments, "),
1097 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1100 where (StrictSig dmd_ty) = idStrictness binder
1102 mkUnboxedTupleMsg :: Id -> Message
1103 mkUnboxedTupleMsg binder
1104 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1105 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1107 mkCastErr :: Type -> Type -> Message
1108 mkCastErr from_ty expr_ty
1109 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1110 ptext (sLit "From-type:") <+> ppr from_ty,
1111 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1114 dupVars :: [[Var]] -> Message
1116 = hang (ptext (sLit "Duplicate variables brought into scope"))