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 import Data.Traversable (traverse)
49 %************************************************************************
51 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
53 %************************************************************************
55 Checks that a set of core bindings is well-formed. The PprStyle and String
56 just control what we print in the event of an error. The Bool value
57 indicates whether we have done any specialisation yet (in which case we do
62 (b) Out-of-scope type variables
63 (c) Out-of-scope local variables
66 If we have done specialisation the we check that there are
67 (a) No top-level bindings of primitive (unboxed type)
72 -- Things are *not* OK if:
74 -- * Unsaturated type app before specialisation has been done;
76 -- * Oversaturated type app after specialisation (eta reduction
77 -- may well be happening...);
80 Note [Linting type lets]
81 ~~~~~~~~~~~~~~~~~~~~~~~~
82 In the desugarer, it's very very convenient to be able to say (in effect)
83 let a = Type Int in <body>
84 That is, use a type let. See Note [Type let] in CoreSyn.
86 However, when linting <body> we need to remember that a=Int, else we might
87 reject a correct program. So we carry a type substitution (in this example
88 [a -> Int]) and apply this substitution before comparing types. The functin
89 lintInTy :: Type -> LintM Type
90 returns a substituted type; that's the only reason it returns anything.
92 When we encounter a binder (like x::a) we must apply the substitution
93 to the type of the binding variable. lintBinders does this.
95 For Ids, the type-substituted Id is added to the in_scope set (which
96 itself is part of the TvSubst we are carrying down), and when we
97 find an occurence of an Id, we fetch it from the in-scope set.
101 lintCoreBindings :: [CoreBind] -> (Bag Message, Bag Message)
102 -- Returns (warnings, errors)
103 lintCoreBindings binds
105 addLoc TopLevelBindings $
106 addInScopeVars binders $
107 -- Put all the top-level binders in scope at the start
108 -- This is because transformation rules can bring something
109 -- into use 'unexpectedly'
110 do { checkL (null dups) (dupVars dups)
111 ; checkL (null ext_dups) (dupExtVars ext_dups)
112 ; mapM lint_bind binds }
114 binders = bindersOfBinds binds
115 (_, dups) = removeDups compare binders
117 -- dups_ext checks for names with different uniques
118 -- but but the same External name M.n. We don't
119 -- allow this at top level:
122 -- becuase they both get the same linker symbol
123 ext_dups = snd (removeDups ord_ext (map Var.varName binders))
124 ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
125 , Just m2 <- nameModule_maybe n2
126 = compare (m1, nameOccName n1) (m2, nameOccName n2)
129 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
130 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
133 %************************************************************************
135 \subsection[lintUnfolding]{lintUnfolding}
137 %************************************************************************
139 We use this to check all unfoldings that come in from interfaces
140 (it is very painful to catch errors otherwise):
143 lintUnfolding :: SrcLoc
144 -> [Var] -- Treat these as in scope
146 -> Maybe Message -- Nothing => OK
148 lintUnfolding locn vars expr
149 | isEmptyBag errs = Nothing
150 | otherwise = Just (pprMessageBag errs)
152 (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
153 addInScopeVars vars $
157 %************************************************************************
159 \subsection[lintCoreBinding]{lintCoreBinding}
161 %************************************************************************
163 Check a core binding, returning the list of variables bound.
166 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
167 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
168 = addLoc (RhsOf binder) $
170 do { ty <- lintCoreExpr rhs
171 ; lintBinder binder -- Check match to RHS type
172 ; binder_ty <- applySubstTy binder_ty
173 ; checkTys binder_ty ty (mkRhsMsg binder ty)
174 -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
175 ; checkL (not (isUnLiftedType binder_ty)
176 || (isNonRec rec_flag && exprOkForSpeculation rhs))
177 (mkRhsPrimMsg binder rhs)
178 -- Check that if the binder is top-level or recursive, it's not demanded
179 ; checkL (not (isStrictId binder)
180 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
182 -- Check whether binder's specialisations contain any out-of-scope variables
183 ; mapM_ (checkBndrIdInScope binder) bndr_vars
185 ; when (isNonRuleLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
186 (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
187 -- Only non-rule loop breakers inhibit inlining
189 -- Check whether arity and demand type are consistent (only if demand analysis
191 ; checkL (case maybeDmdTy of
192 Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
194 (mkArityMsg binder) }
196 -- We should check the unfolding, if any, but this is tricky because
197 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
199 binder_ty = idType binder
200 maybeDmdTy = idStrictness_maybe binder
201 bndr_vars = varSetElems (idFreeVars binder)
202 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
203 | otherwise = return ()
206 %************************************************************************
208 \subsection[lintCoreExpr]{lintCoreExpr}
210 %************************************************************************
213 type InType = Type -- Substitution not yet applied
214 type InCoercion = Coercion
218 type OutType = Type -- Substitution has been applied to this
219 type OutCoercion = Coercion
221 type OutTyVar = TyVar
223 lintCoreExpr :: CoreExpr -> LintM OutType
224 -- The returned type has the substitution from the monad
225 -- already applied to it:
226 -- lintCoreExpr e subst = exprType (subst e)
228 -- The returned "type" can be a kind, if the expression is (Type ty)
230 lintCoreExpr (Var var)
231 = do { checkL (not (var == oneTupleDataConId))
232 (ptext (sLit "Illegal one-tuple"))
234 ; checkL (isId var && not (isCoVar var))
235 (ptext (sLit "Non term variable") <+> ppr var)
238 ; var' <- lookupIdInScope var
239 ; return (idType var') }
241 lintCoreExpr (Lit lit)
242 = return (literalType lit)
244 lintCoreExpr (Cast expr co)
245 = do { expr_ty <- lintCoreExpr expr
246 ; co' <- applySubstCo co
247 ; (from_ty, to_ty) <- lintCoercion co'
248 ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
251 lintCoreExpr (Note _ expr)
254 lintCoreExpr (Let (NonRec tv (Type ty)) body)
256 = -- See Note [Linting type lets]
257 do { ty' <- addLoc (RhsOf tv) $ lintInTy ty
258 ; lintTyBndr tv $ \ tv' ->
259 addLoc (BodyOfLetRec [tv]) $
260 extendSubstL tv' ty' $ do
261 { checkTyKind tv' ty'
262 -- Now extend the substitution so we
263 -- take advantage of it in the body
264 ; lintCoreExpr body } }
266 lintCoreExpr (Let (NonRec bndr rhs) body)
268 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
269 ; addLoc (BodyOfLetRec [bndr])
270 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
273 = failWithL (mkLetErr bndr rhs) -- Not quite accurate
275 lintCoreExpr (Let (Rec pairs) body)
276 = lintAndScopeIds bndrs $ \_ ->
277 do { checkL (null dups) (dupVars dups)
278 ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
279 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
281 bndrs = map fst pairs
282 (_, dups) = removeDups compare bndrs
284 lintCoreExpr e@(App fun arg)
285 = do { fun_ty <- lintCoreExpr fun
286 ; addLoc (AnExpr e) $
287 lintCoreArg fun_ty arg }
289 lintCoreExpr (Lam var expr)
290 = addLoc (LambdaBodyOf var) $
291 lintBinders [var] $ \ vars' ->
292 do { let [var'] = vars'
293 ; body_ty <- lintCoreExpr expr
295 return (mkFunTy (idType var') body_ty)
297 return (mkForAllTy var' body_ty)
299 -- The applySubstTy is needed to apply the subst to var
301 lintCoreExpr e@(Case scrut var alt_ty alts) =
302 -- Check the scrutinee
303 do { scrut_ty <- lintCoreExpr scrut
304 ; alt_ty <- lintInTy alt_ty
305 ; var_ty <- lintInTy (idType var)
307 ; let mb_tc_app = splitTyConApp_maybe (idType var)
312 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
313 null (tyConDataCons tycon) ->
314 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
315 -- This can legitimately happen for type families
317 _otherwise -> return ()
319 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
321 ; subst <- getTvSubst
322 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
324 -- If the binder is an unboxed tuple type, don't put it in scope
325 ; let scope = if (isUnboxedTupleType (idType var)) then
327 else lintAndScopeId var
329 do { -- Check the alternatives
330 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
331 ; checkCaseAlts e scrut_ty alts
336 lintCoreExpr (Type ty)
337 = do { ty' <- lintInTy ty
338 ; return (typeKind ty') }
340 lintCoreExpr (Coercion co)
341 = do { co' <- lintInCo co
342 ; let Pair ty1 ty2 = coercionKind co'
343 ; return (mkPredTy $ EqPred ty1 ty2) }
346 %************************************************************************
348 \subsection[lintCoreArgs]{lintCoreArgs}
350 %************************************************************************
352 The basic version of these functions checks that the argument is a
353 subtype of the required type, as one would expect.
356 lintCoreArg :: OutType -> CoreArg -> LintM OutType
357 lintCoreArg fun_ty (Type arg_ty)
358 = do { arg_ty' <- applySubstTy arg_ty
359 ; lintTyApp fun_ty arg_ty' }
361 lintCoreArg fun_ty arg
362 = do { arg_ty <- lintCoreExpr arg
363 ; lintValApp arg fun_ty arg_ty }
366 lintAltBinders :: OutType -- Scrutinee type
367 -> OutType -- Constructor type
368 -> [OutVar] -- Binders
370 lintAltBinders scrut_ty con_ty []
371 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
372 lintAltBinders scrut_ty con_ty (bndr:bndrs)
374 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
375 ; lintAltBinders scrut_ty con_ty' bndrs }
377 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
378 ; lintAltBinders scrut_ty con_ty' bndrs }
381 lintTyApp :: OutType -> OutType -> LintM OutType
382 lintTyApp fun_ty arg_ty
383 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
385 = do { checkTyKind tyvar arg_ty
386 ; return (substTyWith [tyvar] [arg_ty] body_ty) }
389 = failWithL (mkTyAppMsg fun_ty arg_ty)
392 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
393 lintValApp arg fun_ty arg_ty
394 | Just (arg,res) <- splitFunTy_maybe fun_ty
395 = do { checkTys arg arg_ty err1
400 err1 = mkAppMsg fun_ty arg_ty arg
401 err2 = mkNonFunAppMsg fun_ty arg_ty arg
405 checkTyKind :: OutTyVar -> OutType -> LintM ()
406 -- Both args have had substitution applied
407 checkTyKind tyvar arg_ty
408 -- Arg type might be boxed for a function with an uncommitted
409 -- tyvar; notably this is used so that we can give
410 -- error :: forall a:*. String -> a
411 -- and then apply it to both boxed and unboxed types.
412 = do { arg_kind <- lintType arg_ty
413 ; unless (arg_kind `isSubKind` tyvar_kind)
414 (addErrL (mkKindErrMsg tyvar arg_ty)) }
416 tyvar_kind = tyVarKind tyvar
418 -- Check that the kinds of a type variable and a coercion match, that
419 -- is, if tv :: k then co :: t1 ~ t2 where t1 :: k and t2 :: k.
420 checkTyCoKind :: TyVar -> OutCoercion -> LintM (OutType, OutType)
422 = do { (t1,t2) <- lintCoercion co
425 ; unless ((k1 `isSubKind` tyvar_kind) && (k2 `isSubKind` tyvar_kind))
426 (addErrL (mkTyCoAppErrMsg tv co))
429 tyvar_kind = tyVarKind tv
431 checkTyCoKinds :: [TyVar] -> [OutCoercion] -> LintM [(OutType, OutType)]
432 checkTyCoKinds = zipWithM checkTyCoKind
434 checkDeadIdOcc :: Id -> LintM ()
435 -- Occurrences of an Id should never be dead....
436 -- except when we are checking a case pattern
438 | isDeadOcc (idOccInfo id)
439 = do { in_case <- inCasePat
441 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
447 %************************************************************************
449 \subsection[lintCoreAlts]{lintCoreAlts}
451 %************************************************************************
454 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
455 -- a) Check that the alts are non-empty
456 -- b1) Check that the DEFAULT comes first, if it exists
457 -- b2) Check that the others are in increasing order
458 -- c) Check that there's a default for infinite types
459 -- NB: Algebraic cases are not necessarily exhaustive, because
460 -- the simplifer correctly eliminates case that can't
464 = addErrL (mkNullAltsMsg e)
466 checkCaseAlts e ty alts =
467 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
468 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
469 ; checkL (isJust maybe_deflt || not is_infinite_ty)
470 (nonExhaustiveAltsMsg e) }
472 (con_alts, maybe_deflt) = findDefault alts
474 -- Check that successive alternatives have increasing tags
475 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
476 increasing_tag _ = True
478 non_deflt (DEFAULT, _, _) = False
481 is_infinite_ty = case splitTyConApp_maybe ty of
483 Just (tycon, _) -> isPrimTyCon tycon
487 checkAltExpr :: CoreExpr -> OutType -> LintM ()
488 checkAltExpr expr ann_ty
489 = do { actual_ty <- lintCoreExpr expr
490 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
492 lintCoreAlt :: OutType -- Type of scrutinee
493 -> OutType -- Type of the alternative
497 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
498 do { checkL (null args) (mkDefaultArgsMsg args)
499 ; checkAltExpr rhs alt_ty }
501 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
502 do { checkL (null args) (mkDefaultArgsMsg args)
503 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
504 ; checkAltExpr rhs alt_ty }
506 lit_ty = literalType lit
508 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
509 | isNewTyCon (dataConTyCon con)
510 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
511 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
512 = addLoc (CaseAlt alt) $ do
513 { -- First instantiate the universally quantified
514 -- type variables of the data constructor
515 -- We've already check
516 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
517 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
519 -- And now bring the new binders into scope
520 ; lintBinders args $ \ args' -> do
521 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
522 ; checkAltExpr rhs alt_ty } }
524 | otherwise -- Scrut-ty is wrong shape
525 = addErrL (mkBadAltMsg scrut_ty alt)
528 %************************************************************************
530 \subsection[lint-types]{Types}
532 %************************************************************************
535 -- When we lint binders, we (one at a time and in order):
536 -- 1. Lint var types or kinds (possibly substituting)
537 -- 2. Add the binder to the in scope set, and if its a coercion var,
538 -- we may extend the substitution to reflect its (possibly) new kind
539 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
540 lintBinders [] linterF = linterF []
541 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
542 lintBinders vars $ \ vars' ->
545 lintBinder :: Var -> (Var -> LintM a) -> LintM a
546 lintBinder var linterF
547 | isId var = lintIdBndr var linterF
548 | otherwise = lintTyBndr var linterF
550 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
551 lintTyBndr tv thing_inside
552 = do { subst <- getTvSubst
553 ; let (subst', tv') = Type.substTyVarBndr subst tv
555 ; updateTvSubst subst' (thing_inside tv') }
557 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
558 -- Do substitution on the type of a binder and add the var with this
559 -- new type to the in-scope set of the second argument
560 -- ToDo: lint its rules
562 lintIdBndr id linterF
563 = do { checkL (not (isUnboxedTupleType (idType id)))
564 (mkUnboxedTupleMsg id)
565 -- No variable can be bound to an unboxed tuple.
566 ; lintAndScopeId id $ \id' -> linterF id' }
568 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
569 lintAndScopeIds ids linterF
573 go (id:ids) = lintAndScopeId id $ \id ->
574 lintAndScopeIds ids $ \ids ->
577 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
578 lintAndScopeId id linterF
579 = do { ty <- lintInTy (idType id)
580 ; let id' = setIdType id ty
581 ; addInScopeVar id' $ (linterF id') }
585 %************************************************************************
587 \subsection[lint-monad]{The Lint monad}
589 %************************************************************************
592 lintInTy :: InType -> LintM OutType
593 -- Check the type, and apply the substitution to it
594 -- See Note [Linting type lets]
595 -- ToDo: check the kind structure of the type
597 = addLoc (InType ty) $
598 do { ty' <- applySubstTy ty
602 lintInCo :: InCoercion -> LintM OutCoercion
603 -- Check the coercion, and apply the substitution to it
604 -- See Note [Linting type lets]
607 do { co' <- applySubstCo co
608 ; _ <- lintCoercion co'
612 lintKind :: Kind -> LintM ()
613 -- Check well-formedness of kinds: *, *->*, etc
614 lintKind (TyConApp tc [])
615 | getUnique tc `elem` kindKeys
617 lintKind (FunTy k1 k2)
618 = lintKind k1 >> lintKind k2
620 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
623 lintTyBndrKind :: OutTyVar -> LintM ()
624 lintTyBndrKind tv = lintKind (tyVarKind tv)
627 lintCoercion :: OutCoercion -> LintM (OutType, OutType)
628 -- Check the kind of a coercion term, returning the kind
629 lintCoercion (Refl ty)
630 = do { ty' <- lintInTy ty
631 ; return (ty', ty') }
633 lintCoercion co@(TyConAppCo tc cos)
634 = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
635 ; check_co_app co (tyConKind tc) ss
636 ; return (mkTyConApp tc ss, mkTyConApp tc ts) }
638 lintCoercion co@(AppCo co1 co2)
639 = do { (s1,t1) <- lintCoercion co1
640 ; (s2,t2) <- lintCoercion co2
641 ; check_co_app co (typeKind s1) [s2]
642 ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
644 lintCoercion (ForAllCo v co)
645 = do { lintKind (tyVarKind v)
646 ; (s,t) <- addInScopeVar v (lintCoercion co)
647 ; return (ForAllTy v s, ForAllTy v t) }
649 lintCoercion co@(PredCo (ClassP cls cos))
650 = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
651 ; check_co_app co (tyConKind (classTyCon cls)) ss
652 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
654 lintCoercion (PredCo (IParam ip co))
655 = do { (s,t) <- lintCoercion co
656 ; return (PredTy (IParam ip s), PredTy (IParam ip t)) }
658 lintCoercion (PredCo (EqPred c1 c2))
659 = do { (s1,t1) <- lintCoercion c1
660 ; (s2,t2) <- lintCoercion c2
661 ; return (PredTy (EqPred s1 s2), PredTy (EqPred t1 t2)) }
663 lintCoercion (CoVarCo cv)
664 = do { checkTyCoVarInScope cv
665 ; return (coVarKind cv) }
667 lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = tvs
671 = do { (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs cos)
672 ; return (substTyWith tvs tys1 lhs,
673 substTyWith tvs tys2 rhs) }
675 lintCoercion (UnsafeCo ty1 ty2)
676 = do { ty1' <- lintInTy ty1
677 ; ty2' <- lintInTy ty2
678 ; return (ty1', ty2') }
680 lintCoercion (SymCo co)
681 = do { (ty1, ty2) <- lintCoercion co
682 ; return (ty2, ty1) }
684 lintCoercion co@(TransCo co1 co2)
685 = do { (ty1a, ty1b) <- lintCoercion co1
686 ; (ty2a, ty2b) <- lintCoercion co2
687 ; checkL (ty1b `eqType` ty2a)
688 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
689 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
690 ; return (ty1a, ty2b) }
692 lintCoercion the_co@(NthCo d co)
693 = do { (s,t) <- lintCoercion co
694 ; sn <- checkTcApp the_co d s
695 ; tn <- checkTcApp the_co d t
698 lintCoercion (InstCo co arg_ty)
699 = do { co_tys <- lintCoercion co
700 ; arg_kind <- lintType arg_ty
701 ; case splitForAllTy_maybe `traverse` toPair co_tys of
702 Just (Pair (tv1,ty1) (tv2,ty2))
703 | arg_kind `isSubKind` tyVarKind tv1
704 -> return (substTyWith [tv1] [arg_ty] ty1,
705 substTyWith [tv2] [arg_ty] ty2)
707 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
708 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
711 checkTcApp :: Coercion -> Int -> Type -> LintM Type
713 | Just (_, tys) <- splitTyConApp_maybe ty
717 = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co)
718 2 (ptext (sLit "Offending type:") <+> ppr ty))
721 lintType :: OutType -> LintM Kind
722 lintType (TyVarTy tv)
723 = do { checkTyCoVarInScope tv
724 ; return (tyVarKind tv) }
726 lintType ty@(AppTy t1 t2)
727 = do { k1 <- lintType t1
728 ; lint_ty_app ty k1 [t2] }
730 lintType ty@(FunTy t1 t2)
731 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
733 lintType ty@(TyConApp tc tys)
735 = lint_ty_app ty (tyConKind tc) tys
737 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
739 lintType (ForAllTy tv ty)
740 = do { lintTyBndrKind tv
741 ; addInScopeVar tv (lintType ty) }
743 lintType ty@(PredTy (ClassP cls tys))
744 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
746 lintType (PredTy (IParam _ p_ty))
749 lintType ty@(PredTy (EqPred t1 t2))
750 = do { k1 <- lintType t1
752 ; unless (k1 `eqKind` k2)
753 (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:")
754 , nest 2 (ppr ty) ]))
755 ; return unliftedTypeKind }
758 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
760 = do { ks <- mapM lintType tys
761 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
764 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
765 check_co_app ty k tys
766 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
771 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
772 lint_kind_app doc kfn ks = go kfn ks
774 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
775 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
776 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
778 go kfn [] = return kfn
779 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
780 Nothing -> failWithL fail_msg
781 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
786 %************************************************************************
788 \subsection[lint-monad]{The Lint monad}
790 %************************************************************************
795 [LintLocInfo] -> -- Locations
796 TvSubst -> -- Current type substitution; we also use this
797 -- to keep track of all the variables in scope,
798 -- both Ids and TyVars
799 WarnsAndErrs -> -- Error and warning messages so far
800 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
802 type WarnsAndErrs = (Bag Message, Bag Message)
804 {- Note [Type substitution]
805 ~~~~~~~~~~~~~~~~~~~~~~~~
806 Why do we need a type substitution? Consider
807 /\(a:*). \(x:a). /\(a:*). id a x
808 This is ill typed, because (renaming variables) it is really
809 /\(a:*). \(x:a). /\(b:*). id b x
810 Hence, when checking an application, we can't naively compare x's type
811 (at its binding site) with its expected type (at a use site). So we
812 rename type binders as we go, maintaining a substitution.
814 The same substitution also supports let-type, current expressed as
816 Here we substitute 'ty' for 'a' in 'body', on the fly.
819 instance Monad LintM where
820 return x = LintM (\ _ _ errs -> (Just x, errs))
821 fail err = failWithL (text err)
822 m >>= k = LintM (\ loc subst errs ->
823 let (res, errs') = unLintM m loc subst errs in
825 Just r -> unLintM (k r) loc subst errs'
826 Nothing -> (Nothing, errs'))
829 = RhsOf Id -- The variable bound
830 | LambdaBodyOf Id -- The lambda-binder
831 | BodyOfLetRec [Id] -- One of the binders
832 | CaseAlt CoreAlt -- Case alternative
833 | CasePat CoreAlt -- The *pattern* of the case alternative
834 | AnExpr CoreExpr -- Some expression
835 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
837 | InType Type -- Inside a type
838 | InCo Coercion -- Inside a coercion
843 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
845 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
850 checkL :: Bool -> Message -> LintM ()
851 checkL True _ = return ()
852 checkL False msg = failWithL msg
854 failWithL :: Message -> LintM a
855 failWithL msg = LintM $ \ loc subst (warns,errs) ->
856 (Nothing, (warns, addMsg subst errs msg loc))
858 addErrL :: Message -> LintM ()
859 addErrL msg = LintM $ \ loc subst (warns,errs) ->
860 (Just (), (warns, addMsg subst errs msg loc))
862 addWarnL :: Message -> LintM ()
863 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
864 (Just (), (addMsg subst warns msg loc, errs))
866 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
867 addMsg subst msgs msg locs
868 = ASSERT( notNull locs )
869 msgs `snocBag` mk_msg msg
871 (loc, cxt1) = dumpLoc (head locs)
872 cxts = [snd (dumpLoc loc) | loc <- locs]
873 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
874 ptext (sLit "Substitution:") <+> ppr subst
877 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
879 addLoc :: LintLocInfo -> LintM a -> LintM a
881 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
883 inCasePat :: LintM Bool -- A slight hack; see the unique call site
884 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
886 is_case_pat (CasePat {} : _) = True
887 is_case_pat _other = False
889 addInScopeVars :: [Var] -> LintM a -> LintM a
890 addInScopeVars vars m
891 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
893 addInScopeVar :: Var -> LintM a -> LintM a
895 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
897 updateTvSubst :: TvSubst -> LintM a -> LintM a
898 updateTvSubst subst' m =
899 LintM (\ loc _ errs -> unLintM m loc subst' errs)
901 getTvSubst :: LintM TvSubst
902 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
904 applySubstTy :: Type -> LintM Type
905 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
907 applySubstCo :: Coercion -> LintM Coercion
908 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
910 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
912 = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs)
916 lookupIdInScope :: Id -> LintM Id
918 | not (mustHaveLocalBinding id)
919 = return id -- An imported Id
921 = do { subst <- getTvSubst
922 ; case lookupInScope (getTvInScope subst) id of
924 Nothing -> do { addErrL out_of_scope
927 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
930 oneTupleDataConId :: Id -- Should not happen
931 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
933 checkBndrIdInScope :: Var -> Var -> LintM ()
934 checkBndrIdInScope binder id
935 = checkInScope msg id
937 msg = ptext (sLit "is out of scope inside info for") <+>
940 checkTyCoVarInScope :: TyCoVar -> LintM ()
941 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
943 checkInScope :: SDoc -> Var -> LintM ()
944 checkInScope loc_msg var =
945 do { subst <- getTvSubst
946 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
947 (hsep [ppr var, loc_msg]) }
949 checkTys :: OutType -> OutType -> Message -> LintM ()
950 -- check ty2 is subtype of ty1 (ie, has same structure but usage
951 -- annotations need only be consistent, not equal)
952 -- Assumes ty1,ty2 are have alrady had the substitution applied
953 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
956 %************************************************************************
958 \subsection{Error messages}
960 %************************************************************************
963 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
966 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
968 dumpLoc (LambdaBodyOf b)
969 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
971 dumpLoc (BodyOfLetRec [])
972 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
974 dumpLoc (BodyOfLetRec bs@(_:_))
975 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
978 = (noSrcLoc, text "In the expression:" <+> ppr e)
980 dumpLoc (CaseAlt (con, args, _))
981 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
983 dumpLoc (CasePat (con, args, _))
984 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
986 dumpLoc (ImportedUnfolding locn)
987 = (locn, brackets (ptext (sLit "in an imported unfolding")))
988 dumpLoc TopLevelBindings
991 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
993 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
995 pp_binders :: [Var] -> SDoc
996 pp_binders bs = sep (punctuate comma (map pp_binder bs))
998 pp_binder :: Var -> SDoc
999 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1000 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1004 ------------------------------------------------------
1005 -- Messages for case expressions
1007 mkNullAltsMsg :: CoreExpr -> Message
1009 = hang (text "Case expression with no alternatives:")
1012 mkDefaultArgsMsg :: [Var] -> Message
1013 mkDefaultArgsMsg args
1014 = hang (text "DEFAULT case with binders")
1017 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1018 mkCaseAltMsg e ty1 ty2
1019 = hang (text "Type of case alternatives not the same as the annotation on case:")
1020 4 (vcat [ppr ty1, ppr ty2, ppr e])
1022 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1023 mkScrutMsg var var_ty scrut_ty subst
1024 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1025 text "Result binder type:" <+> ppr var_ty,--(idType var),
1026 text "Scrutinee type:" <+> ppr scrut_ty,
1027 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1029 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1031 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1032 mkNonIncreasingAltsMsg e
1033 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1035 nonExhaustiveAltsMsg :: CoreExpr -> Message
1036 nonExhaustiveAltsMsg e
1037 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1039 mkBadConMsg :: TyCon -> DataCon -> Message
1040 mkBadConMsg tycon datacon
1042 text "In a case alternative, data constructor isn't in scrutinee type:",
1043 text "Scrutinee type constructor:" <+> ppr tycon,
1044 text "Data con:" <+> ppr datacon
1047 mkBadPatMsg :: Type -> Type -> Message
1048 mkBadPatMsg con_result_ty scrut_ty
1050 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1051 text "Pattern result type:" <+> ppr con_result_ty,
1052 text "Scrutinee type:" <+> ppr scrut_ty
1055 mkBadAltMsg :: Type -> CoreAlt -> Message
1056 mkBadAltMsg scrut_ty alt
1057 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1058 text "Scrutinee type:" <+> ppr scrut_ty,
1059 text "Alternative:" <+> pprCoreAlt alt ]
1061 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1062 mkNewTyDataConAltMsg scrut_ty alt
1063 = vcat [ text "Data alternative for newtype datacon",
1064 text "Scrutinee type:" <+> ppr scrut_ty,
1065 text "Alternative:" <+> pprCoreAlt alt ]
1068 ------------------------------------------------------
1069 -- Other error messages
1071 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1072 mkAppMsg fun_ty arg_ty arg
1073 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1074 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1075 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1076 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1078 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1079 mkNonFunAppMsg fun_ty arg_ty arg
1080 = vcat [ptext (sLit "Non-function type in function position"),
1081 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1082 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1083 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1085 mkLetErr :: TyVar -> CoreExpr -> Message
1087 = vcat [ptext (sLit "Bad `let' binding:"),
1088 hang (ptext (sLit "Variable:"))
1089 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1090 hang (ptext (sLit "Rhs:"))
1093 mkTyCoAppErrMsg :: TyVar -> Coercion -> Message
1094 mkTyCoAppErrMsg tyvar arg_co
1095 = vcat [ptext (sLit "Kinds don't match in lifted coercion application:"),
1096 hang (ptext (sLit "Type variable:"))
1097 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1098 hang (ptext (sLit "Arg coercion:"))
1099 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1101 mkTyAppMsg :: Type -> Type -> Message
1102 mkTyAppMsg ty arg_ty
1103 = vcat [text "Illegal type application:",
1104 hang (ptext (sLit "Exp type:"))
1105 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1106 hang (ptext (sLit "Arg type:"))
1107 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1109 mkRhsMsg :: Id -> Type -> Message
1112 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1114 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1115 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1117 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1118 mkRhsPrimMsg binder _rhs
1119 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1121 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1124 mkStrictMsg :: Id -> Message
1126 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1128 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1132 mkKindErrMsg :: TyVar -> Type -> Message
1133 mkKindErrMsg tyvar arg_ty
1134 = vcat [ptext (sLit "Kinds don't match in type application:"),
1135 hang (ptext (sLit "Type variable:"))
1136 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1137 hang (ptext (sLit "Arg type:"))
1138 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1140 mkArityMsg :: Id -> Message
1142 = vcat [hsep [ptext (sLit "Demand type has "),
1143 ppr (dmdTypeDepth dmd_ty),
1144 ptext (sLit " arguments, rhs has "),
1145 ppr (idArity binder),
1146 ptext (sLit "arguments, "),
1148 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1151 where (StrictSig dmd_ty) = idStrictness binder
1153 mkUnboxedTupleMsg :: Id -> Message
1154 mkUnboxedTupleMsg binder
1155 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1156 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1158 mkCastErr :: Type -> Type -> Message
1159 mkCastErr from_ty expr_ty
1160 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1161 ptext (sLit "From-type:") <+> ppr from_ty,
1162 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1165 dupVars :: [[Var]] -> Message
1167 = hang (ptext (sLit "Duplicate variables brought into scope"))
1170 dupExtVars :: [[Name]] -> Message
1172 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1176 -------------- DEAD CODE -------------------
1179 checkCoKind :: CoVar -> OutCoercion -> LintM ()
1180 -- Both args have had substitution applied
1181 checkCoKind covar arg_co
1182 = do { (s2,t2) <- lintCoercion arg_co
1183 ; unless (s1 `eqType` s2 && t1 `coreEqType` t2)
1184 (addErrL (mkCoAppErrMsg covar arg_co)) }
1186 (s1,t1) = coVarKind covar
1188 lintCoVarKind :: OutCoVar -> LintM ()
1189 -- Check the kind of a coercion binder
1191 = do { (ty1,ty2) <- lintSplitCoVar tv
1192 ; lintEqType ty1 ty2
1196 lintSplitCoVar :: CoVar -> LintM (Type,Type)
1198 = case coVarKind_maybe cv of
1199 Just ts -> return ts
1200 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
1201 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
1203 mkCoVarLetErr :: CoVar -> Coercion -> Message
1204 mkCoVarLetErr covar co
1205 = vcat [ptext (sLit "Bad `let' binding for coercion variable:"),
1206 hang (ptext (sLit "Coercion variable:"))
1207 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1208 hang (ptext (sLit "Arg coercion:"))
1211 mkCoAppErrMsg :: CoVar -> Coercion -> Message
1212 mkCoAppErrMsg covar arg_co
1213 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1214 hang (ptext (sLit "Coercion variable:"))
1215 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1216 hang (ptext (sLit "Arg coercion:"))
1217 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1220 mkCoAppMsg :: Type -> Coercion -> Message
1221 mkCoAppMsg ty arg_co
1222 = vcat [text "Illegal type application:",
1223 hang (ptext (sLit "exp type:"))
1224 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1225 hang (ptext (sLit "arg type:"))
1226 4 (ppr arg_co <+> dcolon <+> ppr (coercionKind arg_co))]