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 (CoVarCo cv)
650 = do { checkTyCoVarInScope cv
651 ; return (coVarKind cv) }
653 lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = tvs
657 = do { (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs cos)
658 ; return (substTyWith tvs tys1 lhs,
659 substTyWith tvs tys2 rhs) }
661 lintCoercion (UnsafeCo ty1 ty2)
662 = do { ty1' <- lintInTy ty1
663 ; ty2' <- lintInTy ty2
664 ; return (ty1', ty2') }
666 lintCoercion (SymCo co)
667 = do { (ty1, ty2) <- lintCoercion co
668 ; return (ty2, ty1) }
670 lintCoercion co@(TransCo co1 co2)
671 = do { (ty1a, ty1b) <- lintCoercion co1
672 ; (ty2a, ty2b) <- lintCoercion co2
673 ; checkL (ty1b `eqType` ty2a)
674 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
675 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
676 ; return (ty1a, ty2b) }
678 lintCoercion the_co@(NthCo d co)
679 = do { (s,t) <- lintCoercion co
680 ; sn <- checkTcApp the_co d s
681 ; tn <- checkTcApp the_co d t
684 lintCoercion (InstCo co arg_ty)
685 = do { co_tys <- lintCoercion co
686 ; arg_kind <- lintType arg_ty
687 ; case splitForAllTy_maybe `traverse` toPair co_tys of
688 Just (Pair (tv1,ty1) (tv2,ty2))
689 | arg_kind `isSubKind` tyVarKind tv1
690 -> return (substTyWith [tv1] [arg_ty] ty1,
691 substTyWith [tv2] [arg_ty] ty2)
693 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
694 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
697 checkTcApp :: Coercion -> Int -> Type -> LintM Type
699 | Just (_, tys) <- splitTyConApp_maybe ty
703 = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co)
704 2 (ptext (sLit "Offending type:") <+> ppr ty))
707 lintType :: OutType -> LintM Kind
708 lintType (TyVarTy tv)
709 = do { checkTyCoVarInScope tv
710 ; return (tyVarKind tv) }
712 lintType ty@(AppTy t1 t2)
713 = do { k1 <- lintType t1
714 ; lint_ty_app ty k1 [t2] }
716 lintType ty@(FunTy t1 t2)
717 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
719 lintType ty@(TyConApp tc tys)
721 = lint_ty_app ty (tyConKind tc) tys
723 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
725 lintType (ForAllTy tv ty)
726 = do { lintTyBndrKind tv
727 ; addInScopeVar tv (lintType ty) }
729 lintType ty@(PredTy (ClassP cls tys))
730 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
732 lintType (PredTy (IParam _ p_ty))
735 lintType ty@(PredTy (EqPred t1 t2))
736 = do { k1 <- lintType t1
738 ; unless (k1 `eqKind` k2)
739 (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:")
740 , nest 2 (ppr ty) ]))
741 ; return unliftedTypeKind }
744 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
746 = do { ks <- mapM lintType tys
747 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
750 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
751 check_co_app ty k tys
752 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
757 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
758 lint_kind_app doc kfn ks = go kfn ks
760 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
761 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
762 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
764 go kfn [] = return kfn
765 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
766 Nothing -> failWithL fail_msg
767 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
772 %************************************************************************
774 \subsection[lint-monad]{The Lint monad}
776 %************************************************************************
781 [LintLocInfo] -> -- Locations
782 TvSubst -> -- Current type substitution; we also use this
783 -- to keep track of all the variables in scope,
784 -- both Ids and TyVars
785 WarnsAndErrs -> -- Error and warning messages so far
786 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
788 type WarnsAndErrs = (Bag Message, Bag Message)
790 {- Note [Type substitution]
791 ~~~~~~~~~~~~~~~~~~~~~~~~
792 Why do we need a type substitution? Consider
793 /\(a:*). \(x:a). /\(a:*). id a x
794 This is ill typed, because (renaming variables) it is really
795 /\(a:*). \(x:a). /\(b:*). id b x
796 Hence, when checking an application, we can't naively compare x's type
797 (at its binding site) with its expected type (at a use site). So we
798 rename type binders as we go, maintaining a substitution.
800 The same substitution also supports let-type, current expressed as
802 Here we substitute 'ty' for 'a' in 'body', on the fly.
805 instance Monad LintM where
806 return x = LintM (\ _ _ errs -> (Just x, errs))
807 fail err = failWithL (text err)
808 m >>= k = LintM (\ loc subst errs ->
809 let (res, errs') = unLintM m loc subst errs in
811 Just r -> unLintM (k r) loc subst errs'
812 Nothing -> (Nothing, errs'))
815 = RhsOf Id -- The variable bound
816 | LambdaBodyOf Id -- The lambda-binder
817 | BodyOfLetRec [Id] -- One of the binders
818 | CaseAlt CoreAlt -- Case alternative
819 | CasePat CoreAlt -- The *pattern* of the case alternative
820 | AnExpr CoreExpr -- Some expression
821 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
823 | InType Type -- Inside a type
824 | InCo Coercion -- Inside a coercion
829 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
831 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
836 checkL :: Bool -> Message -> LintM ()
837 checkL True _ = return ()
838 checkL False msg = failWithL msg
840 failWithL :: Message -> LintM a
841 failWithL msg = LintM $ \ loc subst (warns,errs) ->
842 (Nothing, (warns, addMsg subst errs msg loc))
844 addErrL :: Message -> LintM ()
845 addErrL msg = LintM $ \ loc subst (warns,errs) ->
846 (Just (), (warns, addMsg subst errs msg loc))
848 addWarnL :: Message -> LintM ()
849 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
850 (Just (), (addMsg subst warns msg loc, errs))
852 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
853 addMsg subst msgs msg locs
854 = ASSERT( notNull locs )
855 msgs `snocBag` mk_msg msg
857 (loc, cxt1) = dumpLoc (head locs)
858 cxts = [snd (dumpLoc loc) | loc <- locs]
859 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
860 ptext (sLit "Substitution:") <+> ppr subst
863 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
865 addLoc :: LintLocInfo -> LintM a -> LintM a
867 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
869 inCasePat :: LintM Bool -- A slight hack; see the unique call site
870 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
872 is_case_pat (CasePat {} : _) = True
873 is_case_pat _other = False
875 addInScopeVars :: [Var] -> LintM a -> LintM a
876 addInScopeVars vars m
877 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
879 addInScopeVar :: Var -> LintM a -> LintM a
881 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
883 updateTvSubst :: TvSubst -> LintM a -> LintM a
884 updateTvSubst subst' m =
885 LintM (\ loc _ errs -> unLintM m loc subst' errs)
887 getTvSubst :: LintM TvSubst
888 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
890 applySubstTy :: Type -> LintM Type
891 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
893 applySubstCo :: Coercion -> LintM Coercion
894 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
896 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
898 = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs)
902 lookupIdInScope :: Id -> LintM Id
904 | not (mustHaveLocalBinding id)
905 = return id -- An imported Id
907 = do { subst <- getTvSubst
908 ; case lookupInScope (getTvInScope subst) id of
910 Nothing -> do { addErrL out_of_scope
913 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
916 oneTupleDataConId :: Id -- Should not happen
917 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
919 checkBndrIdInScope :: Var -> Var -> LintM ()
920 checkBndrIdInScope binder id
921 = checkInScope msg id
923 msg = ptext (sLit "is out of scope inside info for") <+>
926 checkTyCoVarInScope :: TyCoVar -> LintM ()
927 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
929 checkInScope :: SDoc -> Var -> LintM ()
930 checkInScope loc_msg var =
931 do { subst <- getTvSubst
932 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
933 (hsep [ppr var, loc_msg]) }
935 checkTys :: OutType -> OutType -> Message -> LintM ()
936 -- check ty2 is subtype of ty1 (ie, has same structure but usage
937 -- annotations need only be consistent, not equal)
938 -- Assumes ty1,ty2 are have alrady had the substitution applied
939 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
942 %************************************************************************
944 \subsection{Error messages}
946 %************************************************************************
949 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
952 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
954 dumpLoc (LambdaBodyOf b)
955 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
957 dumpLoc (BodyOfLetRec [])
958 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
960 dumpLoc (BodyOfLetRec bs@(_:_))
961 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
964 = (noSrcLoc, text "In the expression:" <+> ppr e)
966 dumpLoc (CaseAlt (con, args, _))
967 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
969 dumpLoc (CasePat (con, args, _))
970 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
972 dumpLoc (ImportedUnfolding locn)
973 = (locn, brackets (ptext (sLit "in an imported unfolding")))
974 dumpLoc TopLevelBindings
977 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
979 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
981 pp_binders :: [Var] -> SDoc
982 pp_binders bs = sep (punctuate comma (map pp_binder bs))
984 pp_binder :: Var -> SDoc
985 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
986 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
990 ------------------------------------------------------
991 -- Messages for case expressions
993 mkNullAltsMsg :: CoreExpr -> Message
995 = hang (text "Case expression with no alternatives:")
998 mkDefaultArgsMsg :: [Var] -> Message
999 mkDefaultArgsMsg args
1000 = hang (text "DEFAULT case with binders")
1003 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1004 mkCaseAltMsg e ty1 ty2
1005 = hang (text "Type of case alternatives not the same as the annotation on case:")
1006 4 (vcat [ppr ty1, ppr ty2, ppr e])
1008 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1009 mkScrutMsg var var_ty scrut_ty subst
1010 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1011 text "Result binder type:" <+> ppr var_ty,--(idType var),
1012 text "Scrutinee type:" <+> ppr scrut_ty,
1013 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1015 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1017 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1018 mkNonIncreasingAltsMsg e
1019 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1021 nonExhaustiveAltsMsg :: CoreExpr -> Message
1022 nonExhaustiveAltsMsg e
1023 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1025 mkBadConMsg :: TyCon -> DataCon -> Message
1026 mkBadConMsg tycon datacon
1028 text "In a case alternative, data constructor isn't in scrutinee type:",
1029 text "Scrutinee type constructor:" <+> ppr tycon,
1030 text "Data con:" <+> ppr datacon
1033 mkBadPatMsg :: Type -> Type -> Message
1034 mkBadPatMsg con_result_ty scrut_ty
1036 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1037 text "Pattern result type:" <+> ppr con_result_ty,
1038 text "Scrutinee type:" <+> ppr scrut_ty
1041 mkBadAltMsg :: Type -> CoreAlt -> Message
1042 mkBadAltMsg scrut_ty alt
1043 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1044 text "Scrutinee type:" <+> ppr scrut_ty,
1045 text "Alternative:" <+> pprCoreAlt alt ]
1047 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1048 mkNewTyDataConAltMsg scrut_ty alt
1049 = vcat [ text "Data alternative for newtype datacon",
1050 text "Scrutinee type:" <+> ppr scrut_ty,
1051 text "Alternative:" <+> pprCoreAlt alt ]
1054 ------------------------------------------------------
1055 -- Other error messages
1057 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1058 mkAppMsg fun_ty arg_ty arg
1059 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1060 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1061 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1062 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1064 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1065 mkNonFunAppMsg fun_ty arg_ty arg
1066 = vcat [ptext (sLit "Non-function type in function position"),
1067 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1068 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1069 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1071 mkLetErr :: TyVar -> CoreExpr -> Message
1073 = vcat [ptext (sLit "Bad `let' binding:"),
1074 hang (ptext (sLit "Variable:"))
1075 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1076 hang (ptext (sLit "Rhs:"))
1079 mkTyCoAppErrMsg :: TyVar -> Coercion -> Message
1080 mkTyCoAppErrMsg tyvar arg_co
1081 = vcat [ptext (sLit "Kinds don't match in lifted coercion application:"),
1082 hang (ptext (sLit "Type variable:"))
1083 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1084 hang (ptext (sLit "Arg coercion:"))
1085 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1087 mkTyAppMsg :: Type -> Type -> Message
1088 mkTyAppMsg ty arg_ty
1089 = vcat [text "Illegal type application:",
1090 hang (ptext (sLit "Exp type:"))
1091 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1092 hang (ptext (sLit "Arg type:"))
1093 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1095 mkRhsMsg :: Id -> Type -> Message
1098 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1100 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1101 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1103 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1104 mkRhsPrimMsg binder _rhs
1105 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1107 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1110 mkStrictMsg :: Id -> Message
1112 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1114 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1118 mkKindErrMsg :: TyVar -> Type -> Message
1119 mkKindErrMsg tyvar arg_ty
1120 = vcat [ptext (sLit "Kinds don't match in type application:"),
1121 hang (ptext (sLit "Type variable:"))
1122 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1123 hang (ptext (sLit "Arg type:"))
1124 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1126 mkArityMsg :: Id -> Message
1128 = vcat [hsep [ptext (sLit "Demand type has "),
1129 ppr (dmdTypeDepth dmd_ty),
1130 ptext (sLit " arguments, rhs has "),
1131 ppr (idArity binder),
1132 ptext (sLit "arguments, "),
1134 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1137 where (StrictSig dmd_ty) = idStrictness binder
1139 mkUnboxedTupleMsg :: Id -> Message
1140 mkUnboxedTupleMsg binder
1141 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1142 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1144 mkCastErr :: Type -> Type -> Message
1145 mkCastErr from_ty expr_ty
1146 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1147 ptext (sLit "From-type:") <+> ppr from_ty,
1148 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1151 dupVars :: [[Var]] -> Message
1153 = hang (ptext (sLit "Duplicate variables brought into scope"))
1156 dupExtVars :: [[Name]] -> Message
1158 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1162 -------------- DEAD CODE -------------------
1165 checkCoKind :: CoVar -> OutCoercion -> LintM ()
1166 -- Both args have had substitution applied
1167 checkCoKind covar arg_co
1168 = do { (s2,t2) <- lintCoercion arg_co
1169 ; unless (s1 `eqType` s2 && t1 `coreEqType` t2)
1170 (addErrL (mkCoAppErrMsg covar arg_co)) }
1172 (s1,t1) = coVarKind covar
1174 lintCoVarKind :: OutCoVar -> LintM ()
1175 -- Check the kind of a coercion binder
1177 = do { (ty1,ty2) <- lintSplitCoVar tv
1178 ; lintEqType ty1 ty2
1182 lintSplitCoVar :: CoVar -> LintM (Type,Type)
1184 = case coVarKind_maybe cv of
1185 Just ts -> return ts
1186 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
1187 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
1189 mkCoVarLetErr :: CoVar -> Coercion -> Message
1190 mkCoVarLetErr covar co
1191 = vcat [ptext (sLit "Bad `let' binding for coercion variable:"),
1192 hang (ptext (sLit "Coercion variable:"))
1193 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1194 hang (ptext (sLit "Arg coercion:"))
1197 mkCoAppErrMsg :: CoVar -> Coercion -> Message
1198 mkCoAppErrMsg covar arg_co
1199 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1200 hang (ptext (sLit "Coercion variable:"))
1201 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1202 hang (ptext (sLit "Arg coercion:"))
1203 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1206 mkCoAppMsg :: Type -> Coercion -> Message
1207 mkCoAppMsg ty arg_co
1208 = vcat [text "Illegal type application:",
1209 hang (ptext (sLit "exp type:"))
1210 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1211 hang (ptext (sLit "arg type:"))
1212 4 (ppr arg_co <+> dcolon <+> ppr (coercionKind arg_co))]