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"))
230 ; checkL (not (var `hasKey` wildCardKey))
231 (ptext (sLit "Occurence of a wild-card binder") <+> ppr var)
232 -- See Note [WildCard binders] in SimplEnv
235 ; var' <- lookupIdInScope var
236 ; return (idType var') }
238 lintCoreExpr (Lit lit)
239 = return (literalType lit)
241 lintCoreExpr (Cast expr co)
242 = do { expr_ty <- lintCoreExpr expr
243 ; co' <- applySubst co
244 ; (from_ty, to_ty) <- lintCoercion co'
245 ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
248 lintCoreExpr (Note _ expr)
251 lintCoreExpr (Let (NonRec tv (Type ty)) body)
253 = -- See Note [Linting type lets]
254 do { ty' <- addLoc (RhsOf tv) $ lintInTy ty
255 ; lintTyBndr tv $ \ tv' ->
256 addLoc (BodyOfLetRec [tv]) $
257 extendSubstL tv' ty' $ do
259 -- Now extend the substitution so we
260 -- take advantage of it in the body
261 ; lintCoreExpr body } }
264 = do { co <- applySubst ty
265 ; (s1,s2) <- addLoc (RhsOf tv) $ lintCoercion co
266 ; lintTyBndr tv $ \ tv' ->
267 addLoc (BodyOfLetRec [tv]) $ do
268 { let (t1,t2) = coVarKind tv'
269 ; checkTys s1 t1 (mkTyVarLetErr tv ty)
270 ; checkTys s2 t2 (mkTyVarLetErr tv ty)
271 ; lintCoreExpr body } }
274 = failWithL (mkTyVarLetErr tv ty) -- Not quite accurate
276 lintCoreExpr (Let (NonRec bndr rhs) body)
277 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
278 ; addLoc (BodyOfLetRec [bndr])
279 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
281 lintCoreExpr (Let (Rec pairs) body)
282 = lintAndScopeIds bndrs $ \_ ->
283 do { checkL (null dups) (dupVars dups)
284 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
285 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
287 bndrs = map fst pairs
288 (_, dups) = removeDups compare bndrs
290 lintCoreExpr e@(App fun arg)
291 = do { fun_ty <- lintCoreExpr fun
292 ; addLoc (AnExpr e) $
293 lintCoreArg fun_ty arg }
295 lintCoreExpr (Lam var expr)
296 = addLoc (LambdaBodyOf var) $
297 lintBinders [var] $ \ vars' ->
298 do { let [var'] = vars'
299 ; body_ty <- lintCoreExpr expr
301 return (mkFunTy (idType var') body_ty)
303 return (mkForAllTy var' body_ty)
305 -- The applySubst is needed to apply the subst to var
307 lintCoreExpr e@(Case scrut var alt_ty alts) =
308 -- Check the scrutinee
309 do { scrut_ty <- lintCoreExpr scrut
310 ; alt_ty <- lintInTy alt_ty
311 ; var_ty <- lintInTy (idType var)
313 ; let mb_tc_app = splitTyConApp_maybe (idType var)
318 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
319 null (tyConDataCons tycon) ->
320 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
321 -- This can legitimately happen for type families
323 _otherwise -> return ()
325 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
327 ; subst <- getTvSubst
328 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
330 -- If the binder is an unboxed tuple type, don't put it in scope
331 ; let scope = if (isUnboxedTupleType (idType var)) then
333 else lintAndScopeId var
335 do { -- Check the alternatives
336 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
337 ; checkCaseAlts e scrut_ty alts
342 lintCoreExpr (Type ty)
343 = do { ty' <- lintInTy ty
344 ; return (typeKind ty') }
347 %************************************************************************
349 \subsection[lintCoreArgs]{lintCoreArgs}
351 %************************************************************************
353 The basic version of these functions checks that the argument is a
354 subtype of the required type, as one would expect.
357 lintCoreArg :: OutType -> CoreArg -> LintM OutType
358 lintCoreArg fun_ty (Type arg_ty)
359 = do { arg_ty' <- applySubst arg_ty
360 ; lintTyApp fun_ty arg_ty' }
362 lintCoreArg fun_ty arg
363 = do { arg_ty <- lintCoreExpr arg
364 ; lintValApp arg fun_ty arg_ty }
367 lintAltBinders :: OutType -- Scrutinee type
368 -> OutType -- Constructor type
369 -> [OutVar] -- Binders
371 lintAltBinders scrut_ty con_ty []
372 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
373 lintAltBinders scrut_ty con_ty (bndr:bndrs)
375 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
376 ; lintAltBinders scrut_ty con_ty' bndrs }
378 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
379 ; lintAltBinders scrut_ty con_ty' bndrs }
382 lintTyApp :: OutType -> OutType -> LintM OutType
383 lintTyApp fun_ty arg_ty
384 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
385 = do { checkKinds tyvar arg_ty
386 ; if isCoVar tyvar then
387 return body_ty -- Co-vars don't appear in body_ty!
389 return (substTyWith [tyvar] [arg_ty] body_ty) }
391 = failWithL (mkTyAppMsg fun_ty arg_ty)
394 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
395 lintValApp arg fun_ty arg_ty
396 | Just (arg,res) <- splitFunTy_maybe fun_ty
397 = do { checkTys arg arg_ty err1
402 err1 = mkAppMsg fun_ty arg_ty arg
403 err2 = mkNonFunAppMsg fun_ty arg_ty arg
407 checkKinds :: OutVar -> OutType -> LintM ()
408 -- Both args have had substitution applied
409 checkKinds tyvar arg_ty
410 -- Arg type might be boxed for a function with an uncommitted
411 -- tyvar; notably this is used so that we can give
412 -- error :: forall a:*. String -> a
413 -- and then apply it to both boxed and unboxed types.
414 | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
415 ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
416 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
417 | otherwise = do { arg_kind <- lintType arg_ty
418 ; unless (arg_kind `isSubKind` tyvar_kind)
419 (addErrL (mkKindErrMsg tyvar arg_ty)) }
421 tyvar_kind = tyVarKind tyvar
422 (s1,t1) = coVarKind tyvar
424 checkDeadIdOcc :: Id -> LintM ()
425 -- Occurrences of an Id should never be dead....
426 -- except when we are checking a case pattern
428 | isDeadOcc (idOccInfo id)
429 = do { in_case <- inCasePat
431 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
437 %************************************************************************
439 \subsection[lintCoreAlts]{lintCoreAlts}
441 %************************************************************************
444 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
445 -- a) Check that the alts are non-empty
446 -- b1) Check that the DEFAULT comes first, if it exists
447 -- b2) Check that the others are in increasing order
448 -- c) Check that there's a default for infinite types
449 -- NB: Algebraic cases are not necessarily exhaustive, because
450 -- the simplifer correctly eliminates case that can't
454 = addErrL (mkNullAltsMsg e)
456 checkCaseAlts e ty alts =
457 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
458 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
459 ; checkL (isJust maybe_deflt || not is_infinite_ty)
460 (nonExhaustiveAltsMsg e) }
462 (con_alts, maybe_deflt) = findDefault alts
464 -- Check that successive alternatives have increasing tags
465 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
466 increasing_tag _ = True
468 non_deflt (DEFAULT, _, _) = False
471 is_infinite_ty = case splitTyConApp_maybe ty of
473 Just (tycon, _) -> isPrimTyCon tycon
477 checkAltExpr :: CoreExpr -> OutType -> LintM ()
478 checkAltExpr expr ann_ty
479 = do { actual_ty <- lintCoreExpr expr
480 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
482 lintCoreAlt :: OutType -- Type of scrutinee
483 -> OutType -- Type of the alternative
487 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
488 do { checkL (null args) (mkDefaultArgsMsg args)
489 ; checkAltExpr rhs alt_ty }
491 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
492 do { checkL (null args) (mkDefaultArgsMsg args)
493 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
494 ; checkAltExpr rhs alt_ty }
496 lit_ty = literalType lit
498 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
499 | isNewTyCon (dataConTyCon con)
500 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
501 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
502 = addLoc (CaseAlt alt) $ do
503 { -- First instantiate the universally quantified
504 -- type variables of the data constructor
505 -- We've already check
506 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
507 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
509 -- And now bring the new binders into scope
510 ; lintBinders args $ \ args' -> do
511 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
512 ; checkAltExpr rhs alt_ty } }
514 | otherwise -- Scrut-ty is wrong shape
515 = addErrL (mkBadAltMsg scrut_ty alt)
518 %************************************************************************
520 \subsection[lint-types]{Types}
522 %************************************************************************
525 -- When we lint binders, we (one at a time and in order):
526 -- 1. Lint var types or kinds (possibly substituting)
527 -- 2. Add the binder to the in scope set, and if its a coercion var,
528 -- we may extend the substitution to reflect its (possibly) new kind
529 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
530 lintBinders [] linterF = linterF []
531 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
532 lintBinders vars $ \ vars' ->
535 lintBinder :: Var -> (Var -> LintM a) -> LintM a
536 lintBinder var linterF
537 | isId var = lintIdBndr var linterF
538 | otherwise = lintTyBndr var linterF
540 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
541 lintTyBndr tv thing_inside
542 = do { subst <- getTvSubst
543 ; let (subst', tv') = substTyVarBndr subst tv
545 ; updateTvSubst subst' (thing_inside tv') }
547 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
548 -- Do substitution on the type of a binder and add the var with this
549 -- new type to the in-scope set of the second argument
550 -- ToDo: lint its rules
552 lintIdBndr id linterF
553 = do { checkL (not (isUnboxedTupleType (idType id)))
554 (mkUnboxedTupleMsg id)
555 -- No variable can be bound to an unboxed tuple.
556 ; lintAndScopeId id $ \id' -> linterF id' }
558 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
559 lintAndScopeIds ids linterF
563 go (id:ids) = lintAndScopeId id $ \id ->
564 lintAndScopeIds ids $ \ids ->
567 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
568 lintAndScopeId id linterF
569 = do { ty <- lintInTy (idType id)
570 ; let id' = setIdType id ty
571 ; addInScopeVar id' $ (linterF id') }
575 %************************************************************************
577 \subsection[lint-monad]{The Lint monad}
579 %************************************************************************
582 lintInTy :: InType -> LintM OutType
583 -- Check the type, and apply the substitution to it
584 -- See Note [Linting type lets]
585 -- ToDo: check the kind structure of the type
587 = addLoc (InType ty) $
588 do { ty' <- applySubst ty
593 lintKind :: Kind -> LintM ()
594 -- Check well-formedness of kinds: *, *->*, etc
595 lintKind (TyConApp tc [])
596 | getUnique tc `elem` kindKeys
598 lintKind (FunTy k1 k2)
599 = lintKind k1 >> lintKind k2
601 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
604 lintTyBndrKind :: OutTyVar -> LintM ()
606 | isCoVar tv = lintCoVarKind tv
607 | otherwise = lintKind (tyVarKind tv)
610 lintCoVarKind :: OutCoVar -> LintM ()
611 -- Check the kind of a coercion binder
613 = do { (ty1,ty2) <- lintSplitCoVar tv
616 ; unless (k1 `eqKind` k2)
617 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
618 , nest 2 (quotes (ppr tv))
622 lintSplitCoVar :: CoVar -> LintM (Type,Type)
624 = case coVarKind_maybe cv of
626 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
627 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
630 lintCoercion, lintCoercion' :: OutType -> LintM (OutType, OutType)
631 -- Check the kind of a coercion term, returning the kind
633 = addLoc (InCoercion co) $ lintCoercion' co
635 lintCoercion' ty@(TyVarTy tv)
636 = do { checkTyVarInScope tv
637 ; if isCoVar tv then return (coVarKind tv)
638 else return (ty, ty) }
640 lintCoercion' ty@(AppTy ty1 ty2)
641 = do { (s1,t1) <- lintCoercion ty1
642 ; (s2,t2) <- lintCoercion ty2
643 ; check_co_app ty (typeKind s1) [s2]
644 ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
646 lintCoercion' ty@(FunTy ty1 ty2)
647 = do { (s1,t1) <- lintCoercion ty1
648 ; (s2,t2) <- lintCoercion ty2
649 ; check_co_app ty (tyConKind funTyCon) [s1, s2]
650 ; return (FunTy s1 s2, FunTy t1 t2) }
652 lintCoercion' ty@(TyConApp tc tys)
653 | Just (ar, desc) <- isCoercionTyCon_maybe tc
654 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
655 ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
656 ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
657 ; check_co_app ty (typeKind s) ss
658 ; return (mkAppTys s ss, mkAppTys t ts) }
660 | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
664 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
665 ; check_co_app ty (tyConKind tc) ss
666 ; return (TyConApp tc ss, TyConApp tc ts) }
668 lintCoercion' ty@(PredTy (ClassP cls tys))
669 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
670 ; check_co_app ty (tyConKind (classTyCon cls)) ss
671 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
673 lintCoercion' (PredTy (IParam n p_ty))
674 = do { (s,t) <- lintCoercion p_ty
675 ; return (PredTy (IParam n s), PredTy (IParam n t)) }
677 lintCoercion' ty@(PredTy (EqPred {}))
678 = failWithL (badEq ty)
680 lintCoercion' (ForAllTy tv ty)
682 = do { (co1, co2) <- lintSplitCoVar tv
683 ; (s1,t1) <- lintCoercion co1
684 ; (s2,t2) <- lintCoercion co2
685 ; (sr,tr) <- lintCoercion ty
686 ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
689 = do { lintKind (tyVarKind tv)
690 ; (s,t) <- addInScopeVar tv (lintCoercion ty)
691 ; return (ForAllTy tv s, ForAllTy tv t) }
693 badCo :: Coercion -> LintM a
694 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
697 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
698 -- Always called with correct number of coercion arguments
699 -- First arg is just for error message
700 lintCoTyConApp _ CoLeft (co:_) = lintLR fst co
701 lintCoTyConApp _ CoRight (co:_) = lintLR snd co
702 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co
703 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co
704 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
706 lintCoTyConApp _ CoSym (co:_)
707 = do { (ty1,ty2) <- lintCoercion co
710 lintCoTyConApp co CoTrans (co1:co2:_)
711 = do { (ty1a, ty1b) <- lintCoercion co1
712 ; (ty2a, ty2b) <- lintCoercion co2
713 ; checkL (ty1b `coreEqType` ty2a)
714 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
715 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
716 ; return (ty1a, ty2b) }
718 lintCoTyConApp _ CoInst (co:arg_ty:_)
719 = do { co_tys <- lintCoercion co
720 ; arg_kind <- lintType arg_ty
721 ; case decompInst_maybe co_tys of
722 Just ((tv1,tv2), (ty1,ty2))
723 | arg_kind `isSubKind` tyVarKind tv1
724 -> return (substTyWith [tv1] [arg_ty] ty1,
725 substTyWith [tv2] [arg_ty] ty2)
727 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
728 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
730 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
731 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
732 = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
733 ; sequence_ (zipWith checkKinds tvs tys1)
734 ; return (substTyWith tvs tys1 lhs_ty,
735 substTyWith tvs tys2 rhs_ty) }
737 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
738 = do { _ <- lintType ty1
739 ; _ <- lintType ty2 -- Ignore kinds; it's unsafe!
742 lintCoTyConApp _ _ _ = panic "lintCoTyConApp" -- Called with wrong number of coercion args
745 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
747 = do { (ty1,ty2) <- lintCoercion co
748 ; case decompLR_maybe (ty1,ty2) of
749 Just res -> return (sel res)
750 Nothing -> failWithL (ptext (sLit "Bad argument of left/right")) }
753 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
755 = do { (ty1,ty2) <- lintCoercion co
756 ; case decompCsel_maybe (ty1,ty2) of
757 Just res -> return (sel res)
758 Nothing -> failWithL (ptext (sLit "Bad argument of csel")) }
761 lintType :: OutType -> LintM Kind
762 lintType (TyVarTy tv)
763 = do { checkTyVarInScope tv
764 ; return (tyVarKind tv) }
766 lintType ty@(AppTy t1 t2)
767 = do { k1 <- lintType t1
768 ; lint_ty_app ty k1 [t2] }
770 lintType ty@(FunTy t1 t2)
771 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
773 lintType ty@(TyConApp tc tys)
775 = lint_ty_app ty (tyConKind tc) tys
777 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
779 lintType (ForAllTy tv ty)
780 = do { lintTyBndrKind tv
781 ; addInScopeVar tv (lintType ty) }
783 lintType ty@(PredTy (ClassP cls tys))
784 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
786 lintType (PredTy (IParam _ p_ty))
789 lintType ty@(PredTy (EqPred {}))
790 = failWithL (badEq ty)
793 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
795 = do { ks <- mapM lintType tys
796 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
799 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
800 check_co_app ty k tys
801 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
806 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
807 lint_kind_app doc kfn ks = go kfn ks
809 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
810 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
811 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
813 go kfn [] = return kfn
814 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
815 Nothing -> failWithL fail_msg
816 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
820 badEq :: Type -> SDoc
821 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
825 %************************************************************************
827 \subsection[lint-monad]{The Lint monad}
829 %************************************************************************
834 [LintLocInfo] -> -- Locations
835 TvSubst -> -- Current type substitution; we also use this
836 -- to keep track of all the variables in scope,
837 -- both Ids and TyVars
838 WarnsAndErrs -> -- Error and warning messages so far
839 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
841 type WarnsAndErrs = (Bag Message, Bag Message)
843 {- Note [Type substitution]
844 ~~~~~~~~~~~~~~~~~~~~~~~~
845 Why do we need a type substitution? Consider
846 /\(a:*). \(x:a). /\(a:*). id a x
847 This is ill typed, because (renaming variables) it is really
848 /\(a:*). \(x:a). /\(b:*). id b x
849 Hence, when checking an application, we can't naively compare x's type
850 (at its binding site) with its expected type (at a use site). So we
851 rename type binders as we go, maintaining a substitution.
853 The same substitution also supports let-type, current expressed as
855 Here we substitute 'ty' for 'a' in 'body', on the fly.
858 instance Monad LintM where
859 return x = LintM (\ _ _ errs -> (Just x, errs))
860 fail err = failWithL (text err)
861 m >>= k = LintM (\ loc subst errs ->
862 let (res, errs') = unLintM m loc subst errs in
864 Just r -> unLintM (k r) loc subst errs'
865 Nothing -> (Nothing, errs'))
868 = RhsOf Id -- The variable bound
869 | LambdaBodyOf Id -- The lambda-binder
870 | BodyOfLetRec [Id] -- One of the binders
871 | CaseAlt CoreAlt -- Case alternative
872 | CasePat CoreAlt -- The *pattern* of the case alternative
873 | AnExpr CoreExpr -- Some expression
874 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
876 | InType Type -- Inside a type
877 | InCoercion Coercion -- Inside a type
882 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
884 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
889 checkL :: Bool -> Message -> LintM ()
890 checkL True _ = return ()
891 checkL False msg = failWithL msg
893 failWithL :: Message -> LintM a
894 failWithL msg = LintM $ \ loc subst (warns,errs) ->
895 (Nothing, (warns, addMsg subst errs msg loc))
897 addErrL :: Message -> LintM ()
898 addErrL msg = LintM $ \ loc subst (warns,errs) ->
899 (Just (), (warns, addMsg subst errs msg loc))
901 addWarnL :: Message -> LintM ()
902 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
903 (Just (), (addMsg subst warns msg loc, errs))
905 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
906 addMsg subst msgs msg locs
907 = ASSERT( notNull locs )
908 msgs `snocBag` mk_msg msg
910 (loc, cxt1) = dumpLoc (head locs)
911 cxts = [snd (dumpLoc loc) | loc <- locs]
912 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
913 ptext (sLit "Substitution:") <+> ppr subst
916 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
918 addLoc :: LintLocInfo -> LintM a -> LintM a
920 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
922 inCasePat :: LintM Bool -- A slight hack; see the unique call site
923 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
925 is_case_pat (CasePat {} : _) = True
926 is_case_pat _other = False
928 addInScopeVars :: [Var] -> LintM a -> LintM a
929 addInScopeVars vars m
930 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
932 addInScopeVar :: Var -> LintM a -> LintM a
934 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
936 updateTvSubst :: TvSubst -> LintM a -> LintM a
937 updateTvSubst subst' m =
938 LintM (\ loc _ errs -> unLintM m loc subst' errs)
940 getTvSubst :: LintM TvSubst
941 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
943 applySubst :: Type -> LintM Type
944 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
946 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
948 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
952 lookupIdInScope :: Id -> LintM Id
954 | not (mustHaveLocalBinding id)
955 = return id -- An imported Id
957 = do { subst <- getTvSubst
958 ; case lookupInScope (getTvInScope subst) id of
960 Nothing -> do { addErrL out_of_scope
963 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
966 oneTupleDataConId :: Id -- Should not happen
967 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
969 checkBndrIdInScope :: Var -> Var -> LintM ()
970 checkBndrIdInScope binder id
971 = checkInScope msg id
973 msg = ptext (sLit "is out of scope inside info for") <+>
976 checkTyVarInScope :: TyVar -> LintM ()
977 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
979 checkInScope :: SDoc -> Var -> LintM ()
980 checkInScope loc_msg var =
981 do { subst <- getTvSubst
982 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
983 (hsep [ppr var, loc_msg]) }
985 checkTys :: OutType -> OutType -> Message -> LintM ()
986 -- check ty2 is subtype of ty1 (ie, has same structure but usage
987 -- annotations need only be consistent, not equal)
988 -- Assumes ty1,ty2 are have alrady had the substitution applied
989 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
992 %************************************************************************
994 \subsection{Error messages}
996 %************************************************************************
999 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
1002 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
1004 dumpLoc (LambdaBodyOf b)
1005 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
1007 dumpLoc (BodyOfLetRec [])
1008 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
1010 dumpLoc (BodyOfLetRec bs@(_:_))
1011 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
1014 = (noSrcLoc, text "In the expression:" <+> ppr e)
1016 dumpLoc (CaseAlt (con, args, _))
1017 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1019 dumpLoc (CasePat (con, args, _))
1020 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1022 dumpLoc (ImportedUnfolding locn)
1023 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1024 dumpLoc TopLevelBindings
1027 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1028 dumpLoc (InCoercion ty)
1029 = (noSrcLoc, text "In the coercion" <+> quotes (ppr ty))
1031 pp_binders :: [Var] -> SDoc
1032 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1034 pp_binder :: Var -> SDoc
1035 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1036 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1040 ------------------------------------------------------
1041 -- Messages for case expressions
1043 mkNullAltsMsg :: CoreExpr -> Message
1045 = hang (text "Case expression with no alternatives:")
1048 mkDefaultArgsMsg :: [Var] -> Message
1049 mkDefaultArgsMsg args
1050 = hang (text "DEFAULT case with binders")
1053 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1054 mkCaseAltMsg e ty1 ty2
1055 = hang (text "Type of case alternatives not the same as the annotation on case:")
1056 4 (vcat [ppr ty1, ppr ty2, ppr e])
1058 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1059 mkScrutMsg var var_ty scrut_ty subst
1060 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1061 text "Result binder type:" <+> ppr var_ty,--(idType var),
1062 text "Scrutinee type:" <+> ppr scrut_ty,
1063 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1065 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1067 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1068 mkNonIncreasingAltsMsg e
1069 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1071 nonExhaustiveAltsMsg :: CoreExpr -> Message
1072 nonExhaustiveAltsMsg e
1073 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1075 mkBadConMsg :: TyCon -> DataCon -> Message
1076 mkBadConMsg tycon datacon
1078 text "In a case alternative, data constructor isn't in scrutinee type:",
1079 text "Scrutinee type constructor:" <+> ppr tycon,
1080 text "Data con:" <+> ppr datacon
1083 mkBadPatMsg :: Type -> Type -> Message
1084 mkBadPatMsg con_result_ty scrut_ty
1086 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1087 text "Pattern result type:" <+> ppr con_result_ty,
1088 text "Scrutinee type:" <+> ppr scrut_ty
1091 mkBadAltMsg :: Type -> CoreAlt -> Message
1092 mkBadAltMsg scrut_ty alt
1093 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1094 text "Scrutinee type:" <+> ppr scrut_ty,
1095 text "Alternative:" <+> pprCoreAlt alt ]
1097 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1098 mkNewTyDataConAltMsg scrut_ty alt
1099 = vcat [ text "Data alternative for newtype datacon",
1100 text "Scrutinee type:" <+> ppr scrut_ty,
1101 text "Alternative:" <+> pprCoreAlt alt ]
1104 ------------------------------------------------------
1105 -- Other error messages
1107 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1108 mkAppMsg fun_ty arg_ty arg
1109 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1110 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1111 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1112 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1114 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1115 mkNonFunAppMsg fun_ty arg_ty arg
1116 = vcat [ptext (sLit "Non-function type in function position"),
1117 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1118 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1119 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1121 mkTyVarLetErr :: TyVar -> Type -> Message
1122 mkTyVarLetErr tyvar ty
1123 = vcat [ptext (sLit "Bad `let' binding for type or coercion variable:"),
1124 hang (ptext (sLit "Type/coercion variable:"))
1125 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1126 hang (ptext (sLit "Arg type/coercion:"))
1129 mkKindErrMsg :: TyVar -> Type -> Message
1130 mkKindErrMsg tyvar arg_ty
1131 = vcat [ptext (sLit "Kinds don't match in type application:"),
1132 hang (ptext (sLit "Type variable:"))
1133 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1134 hang (ptext (sLit "Arg type:"))
1135 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1137 mkCoAppErrMsg :: TyVar -> Type -> Message
1138 mkCoAppErrMsg tyvar arg_ty
1139 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1140 hang (ptext (sLit "Coercion variable:"))
1141 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1142 hang (ptext (sLit "Arg coercion:"))
1143 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1145 mkTyAppMsg :: Type -> Type -> Message
1146 mkTyAppMsg ty arg_ty
1147 = vcat [text "Illegal type application:",
1148 hang (ptext (sLit "Exp type:"))
1149 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1150 hang (ptext (sLit "Arg type:"))
1151 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1153 mkRhsMsg :: Id -> Type -> Message
1156 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1158 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1159 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1161 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1162 mkRhsPrimMsg binder _rhs
1163 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1165 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1168 mkStrictMsg :: Id -> Message
1170 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1172 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1175 mkArityMsg :: Id -> Message
1177 = vcat [hsep [ptext (sLit "Demand type has "),
1178 ppr (dmdTypeDepth dmd_ty),
1179 ptext (sLit " arguments, rhs has "),
1180 ppr (idArity binder),
1181 ptext (sLit "arguments, "),
1183 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1186 where (StrictSig dmd_ty) = idStrictness binder
1188 mkUnboxedTupleMsg :: Id -> Message
1189 mkUnboxedTupleMsg binder
1190 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1191 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1193 mkCastErr :: Type -> Type -> Message
1194 mkCastErr from_ty expr_ty
1195 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1196 ptext (sLit "From-type:") <+> ppr from_ty,
1197 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1200 dupVars :: [[Var]] -> Message
1202 = hang (ptext (sLit "Duplicate variables brought into scope"))
1205 dupExtVars :: [[Name]] -> Message
1207 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))