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"
46 %************************************************************************
48 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
50 %************************************************************************
52 Checks that a set of core bindings is well-formed. The PprStyle and String
53 just control what we print in the event of an error. The Bool value
54 indicates whether we have done any specialisation yet (in which case we do
59 (b) Out-of-scope type variables
60 (c) Out-of-scope local variables
63 If we have done specialisation the we check that there are
64 (a) No top-level bindings of primitive (unboxed type)
69 -- Things are *not* OK if:
71 -- * Unsaturated type app before specialisation has been done;
73 -- * Oversaturated type app after specialisation (eta reduction
74 -- may well be happening...);
77 Note [Linting type lets]
78 ~~~~~~~~~~~~~~~~~~~~~~~~
79 In the desugarer, it's very very convenient to be able to say (in effect)
80 let a = Type Int in <body>
81 That is, use a type let. See Note [Type let] in CoreSyn.
83 However, when linting <body> we need to remember that a=Int, else we might
84 reject a correct program. So we carry a type substitution (in this example
85 [a -> Int]) and apply this substitution before comparing types. The functin
86 lintInTy :: Type -> LintM Type
87 returns a substituted type; that's the only reason it returns anything.
89 When we encounter a binder (like x::a) we must apply the substitution
90 to the type of the binding variable. lintBinders does this.
92 For Ids, the type-substituted Id is added to the in_scope set (which
93 itself is part of the TvSubst we are carrying down), and when we
94 find an occurence of an Id, we fetch it from the in-scope set.
98 lintCoreBindings :: [CoreBind] -> (Bag Message, Bag Message)
99 -- Returns (warnings, errors)
100 lintCoreBindings binds
102 addLoc TopLevelBindings $
103 addInScopeVars binders $
104 -- Put all the top-level binders in scope at the start
105 -- This is because transformation rules can bring something
106 -- into use 'unexpectedly'
107 do { checkL (null dups) (dupVars dups)
108 ; checkL (null ext_dups) (dupExtVars ext_dups)
109 ; mapM lint_bind binds }
111 binders = bindersOfBinds binds
112 (_, dups) = removeDups compare binders
114 -- dups_ext checks for names with different uniques
115 -- but but the same External name M.n. We don't
116 -- allow this at top level:
119 -- becuase they both get the same linker symbol
120 ext_dups = snd (removeDups ord_ext (map Var.varName binders))
121 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
122 , Just m2 <- nameModule_maybe n2
123 = compare (m1, nameOccName n1) (m2, nameOccName n2)
126 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
127 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
130 %************************************************************************
132 \subsection[lintUnfolding]{lintUnfolding}
134 %************************************************************************
136 We use this to check all unfoldings that come in from interfaces
137 (it is very painful to catch errors otherwise):
140 lintUnfolding :: SrcLoc
141 -> [Var] -- Treat these as in scope
143 -> Maybe Message -- Nothing => OK
145 lintUnfolding locn vars expr
146 | isEmptyBag errs = Nothing
147 | otherwise = Just (pprMessageBag errs)
149 (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
150 addInScopeVars vars $
154 %************************************************************************
156 \subsection[lintCoreBinding]{lintCoreBinding}
158 %************************************************************************
160 Check a core binding, returning the list of variables bound.
163 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
164 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
165 = addLoc (RhsOf binder) $
167 do { ty <- lintCoreExpr rhs
168 ; lintBinder binder -- Check match to RHS type
169 ; binder_ty <- applySubst binder_ty
170 ; checkTys binder_ty ty (mkRhsMsg binder ty)
171 -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
172 ; checkL (not (isUnLiftedType binder_ty)
173 || (isNonRec rec_flag && exprOkForSpeculation rhs))
174 (mkRhsPrimMsg binder rhs)
175 -- Check that if the binder is top-level or recursive, it's not demanded
176 ; checkL (not (isStrictId binder)
177 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
179 -- Check whether binder's specialisations contain any out-of-scope variables
180 ; mapM_ (checkBndrIdInScope binder) bndr_vars
182 ; when (isNonRuleLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
183 (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
184 -- Only non-rule loop breakers inhibit inlining
186 -- Check whether arity and demand type are consistent (only if demand analysis
188 ; checkL (case maybeDmdTy of
189 Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
191 (mkArityMsg binder) }
193 -- We should check the unfolding, if any, but this is tricky because
194 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
196 binder_ty = idType binder
197 maybeDmdTy = idStrictness_maybe binder
198 bndr_vars = varSetElems (idFreeVars binder)
199 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
200 | otherwise = return ()
203 %************************************************************************
205 \subsection[lintCoreExpr]{lintCoreExpr}
207 %************************************************************************
210 type InType = Type -- Substitution not yet applied
214 type OutType = Type -- Substitution has been applied to this
216 type OutTyVar = TyVar
217 type OutCoVar = CoVar
219 lintCoreExpr :: CoreExpr -> LintM OutType
220 -- The returned type has the substitution from the monad
221 -- already applied to it:
222 -- lintCoreExpr e subst = exprType (subst e)
224 -- The returned "type" can be a kind, if the expression is (Type ty)
226 lintCoreExpr (Var var)
227 = do { checkL (not (var == oneTupleDataConId))
228 (ptext (sLit "Illegal one-tuple"))
231 ; var' <- lookupIdInScope var
232 ; return (idType var') }
234 lintCoreExpr (Lit lit)
235 = return (literalType lit)
237 lintCoreExpr (Cast expr co)
238 = do { expr_ty <- lintCoreExpr expr
239 ; co' <- applySubst co
240 ; (from_ty, to_ty) <- lintCoercion co'
241 ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
244 lintCoreExpr (Note _ expr)
247 lintCoreExpr (Let (NonRec tv (Type ty)) body)
249 = -- See Note [Linting type lets]
250 do { ty' <- addLoc (RhsOf tv) $ lintInTy ty
251 ; lintTyBndr tv $ \ tv' ->
252 addLoc (BodyOfLetRec [tv]) $
253 extendSubstL tv' ty' $ do
255 -- Now extend the substitution so we
256 -- take advantage of it in the body
257 ; lintCoreExpr body } }
260 = do { co <- applySubst ty
261 ; (s1,s2) <- addLoc (RhsOf tv) $ lintCoercion co
262 ; lintTyBndr tv $ \ tv' ->
263 addLoc (BodyOfLetRec [tv]) $ do
264 { let (t1,t2) = coVarKind tv'
265 ; checkTys s1 t1 (mkTyVarLetErr tv ty)
266 ; checkTys s2 t2 (mkTyVarLetErr tv ty)
267 ; lintCoreExpr body } }
270 = failWithL (mkTyVarLetErr tv ty) -- Not quite accurate
272 lintCoreExpr (Let (NonRec bndr rhs) body)
273 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
274 ; addLoc (BodyOfLetRec [bndr])
275 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
277 lintCoreExpr (Let (Rec pairs) body)
278 = lintAndScopeIds bndrs $ \_ ->
279 do { checkL (null dups) (dupVars dups)
280 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
281 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
283 bndrs = map fst pairs
284 (_, dups) = removeDups compare bndrs
286 lintCoreExpr e@(App fun arg)
287 = do { fun_ty <- lintCoreExpr fun
288 ; addLoc (AnExpr e) $
289 lintCoreArg fun_ty arg }
291 lintCoreExpr (Lam var expr)
292 = addLoc (LambdaBodyOf var) $
293 lintBinders [var] $ \ vars' ->
294 do { let [var'] = vars'
295 ; body_ty <- lintCoreExpr expr
297 return (mkFunTy (idType var') body_ty)
299 return (mkForAllTy var' body_ty)
301 -- The applySubst is needed to apply the subst to var
303 lintCoreExpr e@(Case scrut var alt_ty alts) =
304 -- Check the scrutinee
305 do { scrut_ty <- lintCoreExpr scrut
306 ; alt_ty <- lintInTy alt_ty
307 ; var_ty <- lintInTy (idType var)
309 ; let mb_tc_app = splitTyConApp_maybe (idType var)
314 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
315 null (tyConDataCons tycon) ->
316 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
317 -- This can legitimately happen for type families
319 _otherwise -> return ()
321 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
323 ; subst <- getTvSubst
324 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
326 -- If the binder is an unboxed tuple type, don't put it in scope
327 ; let scope = if (isUnboxedTupleType (idType var)) then
329 else lintAndScopeId var
331 do { -- Check the alternatives
332 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
333 ; checkCaseAlts e scrut_ty alts
338 lintCoreExpr (Type ty)
339 = do { ty' <- lintInTy ty
340 ; return (typeKind ty') }
343 %************************************************************************
345 \subsection[lintCoreArgs]{lintCoreArgs}
347 %************************************************************************
349 The basic version of these functions checks that the argument is a
350 subtype of the required type, as one would expect.
353 lintCoreArg :: OutType -> CoreArg -> LintM OutType
354 lintCoreArg fun_ty (Type arg_ty)
355 = do { arg_ty' <- applySubst arg_ty
356 ; lintTyApp fun_ty arg_ty' }
358 lintCoreArg fun_ty arg
359 = do { arg_ty <- lintCoreExpr arg
360 ; lintValApp arg fun_ty arg_ty }
363 lintAltBinders :: OutType -- Scrutinee type
364 -> OutType -- Constructor type
365 -> [OutVar] -- Binders
367 lintAltBinders scrut_ty con_ty []
368 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
369 lintAltBinders scrut_ty con_ty (bndr:bndrs)
371 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
372 ; lintAltBinders scrut_ty con_ty' bndrs }
374 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
375 ; lintAltBinders scrut_ty con_ty' bndrs }
378 lintTyApp :: OutType -> OutType -> LintM OutType
379 lintTyApp fun_ty arg_ty
380 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
381 = do { checkKinds tyvar arg_ty
382 ; if isCoVar tyvar then
383 return body_ty -- Co-vars don't appear in body_ty!
385 return (substTyWith [tyvar] [arg_ty] body_ty) }
387 = failWithL (mkTyAppMsg fun_ty arg_ty)
390 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
391 lintValApp arg fun_ty arg_ty
392 | Just (arg,res) <- splitFunTy_maybe fun_ty
393 = do { checkTys arg arg_ty err1
398 err1 = mkAppMsg fun_ty arg_ty arg
399 err2 = mkNonFunAppMsg fun_ty arg_ty arg
403 checkKinds :: OutVar -> OutType -> LintM ()
404 -- Both args have had substitution applied
405 checkKinds tyvar arg_ty
406 -- Arg type might be boxed for a function with an uncommitted
407 -- tyvar; notably this is used so that we can give
408 -- error :: forall a:*. String -> a
409 -- and then apply it to both boxed and unboxed types.
410 | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
411 ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
412 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
413 | otherwise = do { arg_kind <- lintType arg_ty
414 ; unless (arg_kind `isSubKind` tyvar_kind)
415 (addErrL (mkKindErrMsg tyvar arg_ty)) }
417 tyvar_kind = tyVarKind tyvar
418 (s1,t1) = coVarKind tyvar
420 checkDeadIdOcc :: Id -> LintM ()
421 -- Occurrences of an Id should never be dead....
422 -- except when we are checking a case pattern
424 | isDeadOcc (idOccInfo id)
425 = do { in_case <- inCasePat
427 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
433 %************************************************************************
435 \subsection[lintCoreAlts]{lintCoreAlts}
437 %************************************************************************
440 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
441 -- a) Check that the alts are non-empty
442 -- b1) Check that the DEFAULT comes first, if it exists
443 -- b2) Check that the others are in increasing order
444 -- c) Check that there's a default for infinite types
445 -- NB: Algebraic cases are not necessarily exhaustive, because
446 -- the simplifer correctly eliminates case that can't
450 = addErrL (mkNullAltsMsg e)
452 checkCaseAlts e ty alts =
453 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
454 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
455 ; checkL (isJust maybe_deflt || not is_infinite_ty)
456 (nonExhaustiveAltsMsg e) }
458 (con_alts, maybe_deflt) = findDefault alts
460 -- Check that successive alternatives have increasing tags
461 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
462 increasing_tag _ = True
464 non_deflt (DEFAULT, _, _) = False
467 is_infinite_ty = case splitTyConApp_maybe ty of
469 Just (tycon, _) -> isPrimTyCon tycon
473 checkAltExpr :: CoreExpr -> OutType -> LintM ()
474 checkAltExpr expr ann_ty
475 = do { actual_ty <- lintCoreExpr expr
476 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
478 lintCoreAlt :: OutType -- Type of scrutinee
479 -> OutType -- Type of the alternative
483 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
484 do { checkL (null args) (mkDefaultArgsMsg args)
485 ; checkAltExpr rhs alt_ty }
487 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
488 do { checkL (null args) (mkDefaultArgsMsg args)
489 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
490 ; checkAltExpr rhs alt_ty }
492 lit_ty = literalType lit
494 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
495 | isNewTyCon (dataConTyCon con)
496 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
497 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
498 = addLoc (CaseAlt alt) $ do
499 { -- First instantiate the universally quantified
500 -- type variables of the data constructor
501 -- We've already check
502 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
503 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
505 -- And now bring the new binders into scope
506 ; lintBinders args $ \ args' -> do
507 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
508 ; checkAltExpr rhs alt_ty } }
510 | otherwise -- Scrut-ty is wrong shape
511 = addErrL (mkBadAltMsg scrut_ty alt)
514 %************************************************************************
516 \subsection[lint-types]{Types}
518 %************************************************************************
521 -- When we lint binders, we (one at a time and in order):
522 -- 1. Lint var types or kinds (possibly substituting)
523 -- 2. Add the binder to the in scope set, and if its a coercion var,
524 -- we may extend the substitution to reflect its (possibly) new kind
525 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
526 lintBinders [] linterF = linterF []
527 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
528 lintBinders vars $ \ vars' ->
531 lintBinder :: Var -> (Var -> LintM a) -> LintM a
532 lintBinder var linterF
533 | isId var = lintIdBndr var linterF
534 | otherwise = lintTyBndr var linterF
536 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
537 lintTyBndr tv thing_inside
538 = do { subst <- getTvSubst
539 ; let (subst', tv') = substTyVarBndr subst tv
541 ; updateTvSubst subst' (thing_inside tv') }
543 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
544 -- Do substitution on the type of a binder and add the var with this
545 -- new type to the in-scope set of the second argument
546 -- ToDo: lint its rules
548 lintIdBndr id linterF
549 = do { checkL (not (isUnboxedTupleType (idType id)))
550 (mkUnboxedTupleMsg id)
551 -- No variable can be bound to an unboxed tuple.
552 ; lintAndScopeId id $ \id' -> linterF id' }
554 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
555 lintAndScopeIds ids linterF
559 go (id:ids) = lintAndScopeId id $ \id ->
560 lintAndScopeIds ids $ \ids ->
563 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
564 lintAndScopeId id linterF
565 = do { ty <- lintInTy (idType id)
566 ; let id' = setIdType id ty
567 ; addInScopeVar id' $ (linterF id') }
571 %************************************************************************
573 \subsection[lint-monad]{The Lint monad}
575 %************************************************************************
578 lintInTy :: InType -> LintM OutType
579 -- Check the type, and apply the substitution to it
580 -- See Note [Linting type lets]
581 -- ToDo: check the kind structure of the type
583 = addLoc (InType ty) $
584 do { ty' <- applySubst ty
589 lintKind :: Kind -> LintM ()
590 -- Check well-formedness of kinds: *, *->*, etc
591 lintKind (TyConApp tc [])
592 | getUnique tc `elem` kindKeys
594 lintKind (FunTy k1 k2)
595 = lintKind k1 >> lintKind k2
597 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
600 lintTyBndrKind :: OutTyVar -> LintM ()
602 | isCoVar tv = lintCoVarKind tv
603 | otherwise = lintKind (tyVarKind tv)
606 lintCoVarKind :: OutCoVar -> LintM ()
607 -- Check the kind of a coercion binder
609 = do { (ty1,ty2) <- lintSplitCoVar tv
612 ; unless (k1 `eqKind` k2)
613 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
614 , nest 2 (quotes (ppr tv))
618 lintSplitCoVar :: CoVar -> LintM (Type,Type)
620 = case coVarKind_maybe cv of
622 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
623 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
626 lintCoercion, lintCoercion' :: OutType -> LintM (OutType, OutType)
627 -- Check the kind of a coercion term, returning the kind
629 = addLoc (InCoercion co) $ lintCoercion' co
631 lintCoercion' ty@(TyVarTy tv)
632 = do { checkTyVarInScope tv
633 ; if isCoVar tv then return (coVarKind tv)
634 else return (ty, ty) }
636 lintCoercion' ty@(AppTy ty1 ty2)
637 = do { (s1,t1) <- lintCoercion ty1
638 ; (s2,t2) <- lintCoercion ty2
639 ; check_co_app ty (typeKind s1) [s2]
640 ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
642 lintCoercion' ty@(FunTy ty1 ty2)
643 = do { (s1,t1) <- lintCoercion ty1
644 ; (s2,t2) <- lintCoercion ty2
645 ; check_co_app ty (tyConKind funTyCon) [s1, s2]
646 ; return (FunTy s1 s2, FunTy t1 t2) }
648 lintCoercion' ty@(TyConApp tc tys)
649 | Just (ar, desc) <- isCoercionTyCon_maybe tc
650 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
651 ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
652 ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
653 ; check_co_app ty (typeKind s) ss
654 ; return (mkAppTys s ss, mkAppTys t ts) }
656 | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
660 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
661 ; check_co_app ty (tyConKind tc) ss
662 ; return (TyConApp tc ss, TyConApp tc ts) }
664 lintCoercion' ty@(PredTy (ClassP cls tys))
665 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
666 ; check_co_app ty (tyConKind (classTyCon cls)) ss
667 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
669 lintCoercion' (PredTy (IParam n p_ty))
670 = do { (s,t) <- lintCoercion p_ty
671 ; return (PredTy (IParam n s), PredTy (IParam n t)) }
673 lintCoercion' ty@(PredTy (EqPred {}))
674 = failWithL (badEq ty)
676 lintCoercion' (ForAllTy tv ty)
678 = do { (co1, co2) <- lintSplitCoVar tv
679 ; (s1,t1) <- lintCoercion co1
680 ; (s2,t2) <- lintCoercion co2
681 ; (sr,tr) <- lintCoercion ty
682 ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
685 = do { lintKind (tyVarKind tv)
686 ; (s,t) <- addInScopeVar tv (lintCoercion ty)
687 ; return (ForAllTy tv s, ForAllTy tv t) }
689 badCo :: Coercion -> LintM a
690 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
693 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
694 -- Always called with correct number of coercion arguments
695 -- First arg is just for error message
696 lintCoTyConApp _ CoLeft (co:_) = lintLR fst co
697 lintCoTyConApp _ CoRight (co:_) = lintLR snd co
698 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co
699 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co
700 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
702 lintCoTyConApp _ CoSym (co:_)
703 = do { (ty1,ty2) <- lintCoercion co
706 lintCoTyConApp co CoTrans (co1:co2:_)
707 = do { (ty1a, ty1b) <- lintCoercion co1
708 ; (ty2a, ty2b) <- lintCoercion co2
709 ; checkL (ty1b `coreEqType` ty2a)
710 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
711 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
712 ; return (ty1a, ty2b) }
714 lintCoTyConApp _ CoInst (co:arg_ty:_)
715 = do { co_tys <- lintCoercion co
716 ; arg_kind <- lintType arg_ty
717 ; case decompInst_maybe co_tys of
718 Just ((tv1,tv2), (ty1,ty2))
719 | arg_kind `isSubKind` tyVarKind tv1
720 -> return (substTyWith [tv1] [arg_ty] ty1,
721 substTyWith [tv2] [arg_ty] ty2)
723 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
724 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
726 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
727 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
728 = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
729 ; sequence_ (zipWith checkKinds tvs tys1)
730 ; return (substTyWith tvs tys1 lhs_ty,
731 substTyWith tvs tys2 rhs_ty) }
733 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
734 = do { _ <- lintType ty1
735 ; _ <- lintType ty2 -- Ignore kinds; it's unsafe!
738 lintCoTyConApp _ _ _ = panic "lintCoTyConApp" -- Called with wrong number of coercion args
741 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
743 = do { (ty1,ty2) <- lintCoercion co
744 ; case decompLR_maybe (ty1,ty2) of
745 Just res -> return (sel res)
746 Nothing -> failWithL (ptext (sLit "Bad argument of left/right")) }
749 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
751 = do { (ty1,ty2) <- lintCoercion co
752 ; case decompCsel_maybe (ty1,ty2) of
753 Just res -> return (sel res)
754 Nothing -> failWithL (ptext (sLit "Bad argument of csel")) }
757 lintType :: OutType -> LintM Kind
758 lintType (TyVarTy tv)
759 = do { checkTyVarInScope tv
760 ; return (tyVarKind tv) }
762 lintType ty@(AppTy t1 t2)
763 = do { k1 <- lintType t1
764 ; lint_ty_app ty k1 [t2] }
766 lintType ty@(FunTy t1 t2)
767 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
769 lintType ty@(TyConApp tc tys)
771 = lint_ty_app ty (tyConKind tc) tys
773 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
775 lintType (ForAllTy tv ty)
776 = do { lintTyBndrKind tv
777 ; addInScopeVar tv (lintType ty) }
779 lintType ty@(PredTy (ClassP cls tys))
780 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
782 lintType (PredTy (IParam _ p_ty))
785 lintType ty@(PredTy (EqPred {}))
786 = failWithL (badEq ty)
789 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
791 = do { ks <- mapM lintType tys
792 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
795 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
796 check_co_app ty k tys
797 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
802 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
803 lint_kind_app doc kfn ks = go kfn ks
805 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
806 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
807 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
809 go kfn [] = return kfn
810 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
811 Nothing -> failWithL fail_msg
812 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
816 badEq :: Type -> SDoc
817 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
821 %************************************************************************
823 \subsection[lint-monad]{The Lint monad}
825 %************************************************************************
830 [LintLocInfo] -> -- Locations
831 TvSubst -> -- Current type substitution; we also use this
832 -- to keep track of all the variables in scope,
833 -- both Ids and TyVars
834 WarnsAndErrs -> -- Error and warning messages so far
835 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
837 type WarnsAndErrs = (Bag Message, Bag Message)
839 {- Note [Type substitution]
840 ~~~~~~~~~~~~~~~~~~~~~~~~
841 Why do we need a type substitution? Consider
842 /\(a:*). \(x:a). /\(a:*). id a x
843 This is ill typed, because (renaming variables) it is really
844 /\(a:*). \(x:a). /\(b:*). id b x
845 Hence, when checking an application, we can't naively compare x's type
846 (at its binding site) with its expected type (at a use site). So we
847 rename type binders as we go, maintaining a substitution.
849 The same substitution also supports let-type, current expressed as
851 Here we substitute 'ty' for 'a' in 'body', on the fly.
854 instance Monad LintM where
855 return x = LintM (\ _ _ errs -> (Just x, errs))
856 fail err = failWithL (text err)
857 m >>= k = LintM (\ loc subst errs ->
858 let (res, errs') = unLintM m loc subst errs in
860 Just r -> unLintM (k r) loc subst errs'
861 Nothing -> (Nothing, errs'))
864 = RhsOf Id -- The variable bound
865 | LambdaBodyOf Id -- The lambda-binder
866 | BodyOfLetRec [Id] -- One of the binders
867 | CaseAlt CoreAlt -- Case alternative
868 | CasePat CoreAlt -- The *pattern* of the case alternative
869 | AnExpr CoreExpr -- Some expression
870 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
872 | InType Type -- Inside a type
873 | InCoercion Coercion -- Inside a type
878 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
880 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
885 checkL :: Bool -> Message -> LintM ()
886 checkL True _ = return ()
887 checkL False msg = failWithL msg
889 failWithL :: Message -> LintM a
890 failWithL msg = LintM $ \ loc subst (warns,errs) ->
891 (Nothing, (warns, addMsg subst errs msg loc))
893 addErrL :: Message -> LintM ()
894 addErrL msg = LintM $ \ loc subst (warns,errs) ->
895 (Just (), (warns, addMsg subst errs msg loc))
897 addWarnL :: Message -> LintM ()
898 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
899 (Just (), (addMsg subst warns msg loc, errs))
901 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
902 addMsg subst msgs msg locs
903 = ASSERT( notNull locs )
904 msgs `snocBag` mk_msg msg
906 (loc, cxt1) = dumpLoc (head locs)
907 cxts = [snd (dumpLoc loc) | loc <- locs]
908 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
909 ptext (sLit "Substitution:") <+> ppr subst
912 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
914 addLoc :: LintLocInfo -> LintM a -> LintM a
916 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
918 inCasePat :: LintM Bool -- A slight hack; see the unique call site
919 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
921 is_case_pat (CasePat {} : _) = True
922 is_case_pat _other = False
924 addInScopeVars :: [Var] -> LintM a -> LintM a
925 addInScopeVars vars m
926 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
928 addInScopeVar :: Var -> LintM a -> LintM a
930 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
932 updateTvSubst :: TvSubst -> LintM a -> LintM a
933 updateTvSubst subst' m =
934 LintM (\ loc _ errs -> unLintM m loc subst' errs)
936 getTvSubst :: LintM TvSubst
937 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
939 applySubst :: Type -> LintM Type
940 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
942 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
944 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
948 lookupIdInScope :: Id -> LintM Id
950 | not (mustHaveLocalBinding id)
951 = return id -- An imported Id
953 = do { subst <- getTvSubst
954 ; case lookupInScope (getTvInScope subst) id of
956 Nothing -> do { addErrL out_of_scope
959 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
962 oneTupleDataConId :: Id -- Should not happen
963 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
965 checkBndrIdInScope :: Var -> Var -> LintM ()
966 checkBndrIdInScope binder id
967 = checkInScope msg id
969 msg = ptext (sLit "is out of scope inside info for") <+>
972 checkTyVarInScope :: TyVar -> LintM ()
973 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
975 checkInScope :: SDoc -> Var -> LintM ()
976 checkInScope loc_msg var =
977 do { subst <- getTvSubst
978 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
979 (hsep [ppr var, loc_msg]) }
981 checkTys :: OutType -> OutType -> Message -> LintM ()
982 -- check ty2 is subtype of ty1 (ie, has same structure but usage
983 -- annotations need only be consistent, not equal)
984 -- Assumes ty1,ty2 are have alrady had the substitution applied
985 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
988 %************************************************************************
990 \subsection{Error messages}
992 %************************************************************************
995 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
998 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1000 dumpLoc (LambdaBodyOf b)
1001 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
1003 dumpLoc (BodyOfLetRec [])
1004 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1006 dumpLoc (BodyOfLetRec bs@(_:_))
1007 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1010 = (noSrcLoc, text "In the expression:" <+> ppr e)
1012 dumpLoc (CaseAlt (con, args, _))
1013 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1015 dumpLoc (CasePat (con, args, _))
1016 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1018 dumpLoc (ImportedUnfolding locn)
1019 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1020 dumpLoc TopLevelBindings
1023 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1024 dumpLoc (InCoercion ty)
1025 = (noSrcLoc, text "In the coercion" <+> quotes (ppr ty))
1027 pp_binders :: [Var] -> SDoc
1028 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1030 pp_binder :: Var -> SDoc
1031 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1032 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1036 ------------------------------------------------------
1037 -- Messages for case expressions
1039 mkNullAltsMsg :: CoreExpr -> Message
1041 = hang (text "Case expression with no alternatives:")
1044 mkDefaultArgsMsg :: [Var] -> Message
1045 mkDefaultArgsMsg args
1046 = hang (text "DEFAULT case with binders")
1049 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1050 mkCaseAltMsg e ty1 ty2
1051 = hang (text "Type of case alternatives not the same as the annotation on case:")
1052 4 (vcat [ppr ty1, ppr ty2, ppr e])
1054 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1055 mkScrutMsg var var_ty scrut_ty subst
1056 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1057 text "Result binder type:" <+> ppr var_ty,--(idType var),
1058 text "Scrutinee type:" <+> ppr scrut_ty,
1059 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1061 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1063 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1064 mkNonIncreasingAltsMsg e
1065 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1067 nonExhaustiveAltsMsg :: CoreExpr -> Message
1068 nonExhaustiveAltsMsg e
1069 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1071 mkBadConMsg :: TyCon -> DataCon -> Message
1072 mkBadConMsg tycon datacon
1074 text "In a case alternative, data constructor isn't in scrutinee type:",
1075 text "Scrutinee type constructor:" <+> ppr tycon,
1076 text "Data con:" <+> ppr datacon
1079 mkBadPatMsg :: Type -> Type -> Message
1080 mkBadPatMsg con_result_ty scrut_ty
1082 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1083 text "Pattern result type:" <+> ppr con_result_ty,
1084 text "Scrutinee type:" <+> ppr scrut_ty
1087 mkBadAltMsg :: Type -> CoreAlt -> Message
1088 mkBadAltMsg scrut_ty alt
1089 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1090 text "Scrutinee type:" <+> ppr scrut_ty,
1091 text "Alternative:" <+> pprCoreAlt alt ]
1093 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1094 mkNewTyDataConAltMsg scrut_ty alt
1095 = vcat [ text "Data alternative for newtype datacon",
1096 text "Scrutinee type:" <+> ppr scrut_ty,
1097 text "Alternative:" <+> pprCoreAlt alt ]
1100 ------------------------------------------------------
1101 -- Other error messages
1103 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1104 mkAppMsg fun_ty arg_ty arg
1105 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1106 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1107 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1108 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1110 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1111 mkNonFunAppMsg fun_ty arg_ty arg
1112 = vcat [ptext (sLit "Non-function type in function position"),
1113 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1114 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1115 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1117 mkTyVarLetErr :: TyVar -> Type -> Message
1118 mkTyVarLetErr tyvar ty
1119 = vcat [ptext (sLit "Bad `let' binding for type or coercion variable:"),
1120 hang (ptext (sLit "Type/coercion variable:"))
1121 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1122 hang (ptext (sLit "Arg type/coercion:"))
1125 mkKindErrMsg :: TyVar -> Type -> Message
1126 mkKindErrMsg tyvar arg_ty
1127 = vcat [ptext (sLit "Kinds don't match in type application:"),
1128 hang (ptext (sLit "Type variable:"))
1129 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1130 hang (ptext (sLit "Arg type:"))
1131 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1133 mkCoAppErrMsg :: TyVar -> Type -> Message
1134 mkCoAppErrMsg tyvar arg_ty
1135 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1136 hang (ptext (sLit "Coercion variable:"))
1137 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1138 hang (ptext (sLit "Arg coercion:"))
1139 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1141 mkTyAppMsg :: Type -> Type -> Message
1142 mkTyAppMsg ty arg_ty
1143 = vcat [text "Illegal type application:",
1144 hang (ptext (sLit "Exp type:"))
1145 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1146 hang (ptext (sLit "Arg type:"))
1147 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1149 mkRhsMsg :: Id -> Type -> Message
1152 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1154 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1155 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1157 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1158 mkRhsPrimMsg binder _rhs
1159 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1161 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1164 mkStrictMsg :: Id -> Message
1166 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1168 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1171 mkArityMsg :: Id -> Message
1173 = vcat [hsep [ptext (sLit "Demand type has "),
1174 ppr (dmdTypeDepth dmd_ty),
1175 ptext (sLit " arguments, rhs has "),
1176 ppr (idArity binder),
1177 ptext (sLit "arguments, "),
1179 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1182 where (StrictSig dmd_ty) = idStrictness binder
1184 mkUnboxedTupleMsg :: Id -> Message
1185 mkUnboxedTupleMsg binder
1186 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1187 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1189 mkCastErr :: Type -> Type -> Message
1190 mkCastErr from_ty expr_ty
1191 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1192 ptext (sLit "From-type:") <+> ppr from_ty,
1193 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1196 dupVars :: [[Var]] -> Message
1198 = hang (ptext (sLit "Duplicate variables brought into scope"))
1201 dupExtVars :: [[Name]] -> Message
1203 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))