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)
720 | tc `hasKey` eqPredPrimTyConKey -- See Note [The (~) TyCon] in TysPrim
721 = lint_eq_pred ty tys
723 = lint_ty_app ty (tyConKind tc) tys
725 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
727 lintType (ForAllTy tv ty)
728 = do { lintTyBndrKind tv
729 ; addInScopeVar tv (lintType ty) }
731 lintType ty@(PredTy (ClassP cls tys))
732 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
734 lintType (PredTy (IParam _ p_ty))
737 lintType ty@(PredTy (EqPred t1 t2))
738 = do { k1 <- lintType t1
740 ; unless (k1 `eqKind` k2)
741 (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:")
742 , nest 2 (ppr ty) ]))
743 ; return unliftedTypeKind }
746 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
748 = do { ks <- mapM lintType tys
749 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
751 lint_eq_pred :: Type -> [OutType] -> LintM Kind
752 lint_eq_pred ty arg_tys
753 | [ty1,ty2] <- arg_tys
754 = do { k1 <- lintType ty1
756 ; checkL (k1 `eqKind` k2)
757 (ptext (sLit "Mismatched arg kinds:") <+> ppr ty)
758 ; return unliftedTypeKind }
760 = failWithL (ptext (sLit "Unsaturated (~) type") <+> ppr ty)
763 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
764 check_co_app ty k tys
765 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
770 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
771 lint_kind_app doc kfn ks = go kfn ks
773 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
774 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
775 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
777 go kfn [] = return kfn
778 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
779 Nothing -> failWithL fail_msg
780 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
785 %************************************************************************
787 \subsection[lint-monad]{The Lint monad}
789 %************************************************************************
794 [LintLocInfo] -> -- Locations
795 TvSubst -> -- Current type substitution; we also use this
796 -- to keep track of all the variables in scope,
797 -- both Ids and TyVars
798 WarnsAndErrs -> -- Error and warning messages so far
799 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
801 type WarnsAndErrs = (Bag Message, Bag Message)
803 {- Note [Type substitution]
804 ~~~~~~~~~~~~~~~~~~~~~~~~
805 Why do we need a type substitution? Consider
806 /\(a:*). \(x:a). /\(a:*). id a x
807 This is ill typed, because (renaming variables) it is really
808 /\(a:*). \(x:a). /\(b:*). id b x
809 Hence, when checking an application, we can't naively compare x's type
810 (at its binding site) with its expected type (at a use site). So we
811 rename type binders as we go, maintaining a substitution.
813 The same substitution also supports let-type, current expressed as
815 Here we substitute 'ty' for 'a' in 'body', on the fly.
818 instance Monad LintM where
819 return x = LintM (\ _ _ errs -> (Just x, errs))
820 fail err = failWithL (text err)
821 m >>= k = LintM (\ loc subst errs ->
822 let (res, errs') = unLintM m loc subst errs in
824 Just r -> unLintM (k r) loc subst errs'
825 Nothing -> (Nothing, errs'))
828 = RhsOf Id -- The variable bound
829 | LambdaBodyOf Id -- The lambda-binder
830 | BodyOfLetRec [Id] -- One of the binders
831 | CaseAlt CoreAlt -- Case alternative
832 | CasePat CoreAlt -- The *pattern* of the case alternative
833 | AnExpr CoreExpr -- Some expression
834 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
836 | InType Type -- Inside a type
837 | InCo Coercion -- Inside a coercion
842 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
844 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
849 checkL :: Bool -> Message -> LintM ()
850 checkL True _ = return ()
851 checkL False msg = failWithL msg
853 failWithL :: Message -> LintM a
854 failWithL msg = LintM $ \ loc subst (warns,errs) ->
855 (Nothing, (warns, addMsg subst errs msg loc))
857 addErrL :: Message -> LintM ()
858 addErrL msg = LintM $ \ loc subst (warns,errs) ->
859 (Just (), (warns, addMsg subst errs msg loc))
861 addWarnL :: Message -> LintM ()
862 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
863 (Just (), (addMsg subst warns msg loc, errs))
865 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
866 addMsg subst msgs msg locs
867 = ASSERT( notNull locs )
868 msgs `snocBag` mk_msg msg
870 (loc, cxt1) = dumpLoc (head locs)
871 cxts = [snd (dumpLoc loc) | loc <- locs]
872 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
873 ptext (sLit "Substitution:") <+> ppr subst
876 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
878 addLoc :: LintLocInfo -> LintM a -> LintM a
880 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
882 inCasePat :: LintM Bool -- A slight hack; see the unique call site
883 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
885 is_case_pat (CasePat {} : _) = True
886 is_case_pat _other = False
888 addInScopeVars :: [Var] -> LintM a -> LintM a
889 addInScopeVars vars m
890 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
892 addInScopeVar :: Var -> LintM a -> LintM a
894 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
896 updateTvSubst :: TvSubst -> LintM a -> LintM a
897 updateTvSubst subst' m =
898 LintM (\ loc _ errs -> unLintM m loc subst' errs)
900 getTvSubst :: LintM TvSubst
901 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
903 applySubstTy :: Type -> LintM Type
904 applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
906 applySubstCo :: Coercion -> LintM Coercion
907 applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
909 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
911 = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs)
915 lookupIdInScope :: Id -> LintM Id
917 | not (mustHaveLocalBinding id)
918 = return id -- An imported Id
920 = do { subst <- getTvSubst
921 ; case lookupInScope (getTvInScope subst) id of
923 Nothing -> do { addErrL out_of_scope
926 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
929 oneTupleDataConId :: Id -- Should not happen
930 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
932 checkBndrIdInScope :: Var -> Var -> LintM ()
933 checkBndrIdInScope binder id
934 = checkInScope msg id
936 msg = ptext (sLit "is out of scope inside info for") <+>
939 checkTyCoVarInScope :: TyCoVar -> LintM ()
940 checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
942 checkInScope :: SDoc -> Var -> LintM ()
943 checkInScope loc_msg var =
944 do { subst <- getTvSubst
945 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
946 (hsep [ppr var, loc_msg]) }
948 checkTys :: OutType -> OutType -> Message -> LintM ()
949 -- check ty2 is subtype of ty1 (ie, has same structure but usage
950 -- annotations need only be consistent, not equal)
951 -- Assumes ty1,ty2 are have alrady had the substitution applied
952 checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
955 %************************************************************************
957 \subsection{Error messages}
959 %************************************************************************
962 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
965 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
967 dumpLoc (LambdaBodyOf b)
968 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
970 dumpLoc (BodyOfLetRec [])
971 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
973 dumpLoc (BodyOfLetRec bs@(_:_))
974 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
977 = (noSrcLoc, text "In the expression:" <+> ppr e)
979 dumpLoc (CaseAlt (con, args, _))
980 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
982 dumpLoc (CasePat (con, args, _))
983 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
985 dumpLoc (ImportedUnfolding locn)
986 = (locn, brackets (ptext (sLit "in an imported unfolding")))
987 dumpLoc TopLevelBindings
990 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
992 = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
994 pp_binders :: [Var] -> SDoc
995 pp_binders bs = sep (punctuate comma (map pp_binder bs))
997 pp_binder :: Var -> SDoc
998 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
999 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1003 ------------------------------------------------------
1004 -- Messages for case expressions
1006 mkNullAltsMsg :: CoreExpr -> Message
1008 = hang (text "Case expression with no alternatives:")
1011 mkDefaultArgsMsg :: [Var] -> Message
1012 mkDefaultArgsMsg args
1013 = hang (text "DEFAULT case with binders")
1016 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1017 mkCaseAltMsg e ty1 ty2
1018 = hang (text "Type of case alternatives not the same as the annotation on case:")
1019 4 (vcat [ppr ty1, ppr ty2, ppr e])
1021 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1022 mkScrutMsg var var_ty scrut_ty subst
1023 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1024 text "Result binder type:" <+> ppr var_ty,--(idType var),
1025 text "Scrutinee type:" <+> ppr scrut_ty,
1026 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1028 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1030 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1031 mkNonIncreasingAltsMsg e
1032 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1034 nonExhaustiveAltsMsg :: CoreExpr -> Message
1035 nonExhaustiveAltsMsg e
1036 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1038 mkBadConMsg :: TyCon -> DataCon -> Message
1039 mkBadConMsg tycon datacon
1041 text "In a case alternative, data constructor isn't in scrutinee type:",
1042 text "Scrutinee type constructor:" <+> ppr tycon,
1043 text "Data con:" <+> ppr datacon
1046 mkBadPatMsg :: Type -> Type -> Message
1047 mkBadPatMsg con_result_ty scrut_ty
1049 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1050 text "Pattern result type:" <+> ppr con_result_ty,
1051 text "Scrutinee type:" <+> ppr scrut_ty
1054 mkBadAltMsg :: Type -> CoreAlt -> Message
1055 mkBadAltMsg scrut_ty alt
1056 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1057 text "Scrutinee type:" <+> ppr scrut_ty,
1058 text "Alternative:" <+> pprCoreAlt alt ]
1060 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1061 mkNewTyDataConAltMsg scrut_ty alt
1062 = vcat [ text "Data alternative for newtype datacon",
1063 text "Scrutinee type:" <+> ppr scrut_ty,
1064 text "Alternative:" <+> pprCoreAlt alt ]
1067 ------------------------------------------------------
1068 -- Other error messages
1070 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1071 mkAppMsg fun_ty arg_ty arg
1072 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1073 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1074 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1075 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1077 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1078 mkNonFunAppMsg fun_ty arg_ty arg
1079 = vcat [ptext (sLit "Non-function type in function position"),
1080 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1081 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1082 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1084 mkLetErr :: TyVar -> CoreExpr -> Message
1086 = vcat [ptext (sLit "Bad `let' binding:"),
1087 hang (ptext (sLit "Variable:"))
1088 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
1089 hang (ptext (sLit "Rhs:"))
1092 mkTyCoAppErrMsg :: TyVar -> Coercion -> Message
1093 mkTyCoAppErrMsg tyvar arg_co
1094 = vcat [ptext (sLit "Kinds don't match in lifted coercion application:"),
1095 hang (ptext (sLit "Type variable:"))
1096 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1097 hang (ptext (sLit "Arg coercion:"))
1098 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1100 mkTyAppMsg :: Type -> Type -> Message
1101 mkTyAppMsg ty arg_ty
1102 = vcat [text "Illegal type application:",
1103 hang (ptext (sLit "Exp type:"))
1104 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1105 hang (ptext (sLit "Arg type:"))
1106 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1108 mkRhsMsg :: Id -> Type -> Message
1111 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1113 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1114 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1116 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1117 mkRhsPrimMsg binder _rhs
1118 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1120 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1123 mkStrictMsg :: Id -> Message
1125 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1127 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1131 mkKindErrMsg :: TyVar -> Type -> Message
1132 mkKindErrMsg tyvar arg_ty
1133 = vcat [ptext (sLit "Kinds don't match in type application:"),
1134 hang (ptext (sLit "Type variable:"))
1135 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1136 hang (ptext (sLit "Arg type:"))
1137 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1139 mkArityMsg :: Id -> Message
1141 = vcat [hsep [ptext (sLit "Demand type has "),
1142 ppr (dmdTypeDepth dmd_ty),
1143 ptext (sLit " arguments, rhs has "),
1144 ppr (idArity binder),
1145 ptext (sLit "arguments, "),
1147 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1150 where (StrictSig dmd_ty) = idStrictness binder
1152 mkUnboxedTupleMsg :: Id -> Message
1153 mkUnboxedTupleMsg binder
1154 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1155 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1157 mkCastErr :: Type -> Type -> Message
1158 mkCastErr from_ty expr_ty
1159 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1160 ptext (sLit "From-type:") <+> ppr from_ty,
1161 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1164 dupVars :: [[Var]] -> Message
1166 = hang (ptext (sLit "Duplicate variables brought into scope"))
1169 dupExtVars :: [[Name]] -> Message
1171 = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
1175 -------------- DEAD CODE -------------------
1178 checkCoKind :: CoVar -> OutCoercion -> LintM ()
1179 -- Both args have had substitution applied
1180 checkCoKind covar arg_co
1181 = do { (s2,t2) <- lintCoercion arg_co
1182 ; unless (s1 `eqType` s2 && t1 `coreEqType` t2)
1183 (addErrL (mkCoAppErrMsg covar arg_co)) }
1185 (s1,t1) = coVarKind covar
1187 lintCoVarKind :: OutCoVar -> LintM ()
1188 -- Check the kind of a coercion binder
1190 = do { (ty1,ty2) <- lintSplitCoVar tv
1191 ; lintEqType ty1 ty2
1195 lintSplitCoVar :: CoVar -> LintM (Type,Type)
1197 = case coVarKind_maybe cv of
1198 Just ts -> return ts
1199 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
1200 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
1202 mkCoVarLetErr :: CoVar -> Coercion -> Message
1203 mkCoVarLetErr covar co
1204 = vcat [ptext (sLit "Bad `let' binding for coercion variable:"),
1205 hang (ptext (sLit "Coercion variable:"))
1206 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1207 hang (ptext (sLit "Arg coercion:"))
1210 mkCoAppErrMsg :: CoVar -> Coercion -> Message
1211 mkCoAppErrMsg covar arg_co
1212 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1213 hang (ptext (sLit "Coercion variable:"))
1214 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
1215 hang (ptext (sLit "Arg coercion:"))
1216 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
1219 mkCoAppMsg :: Type -> Coercion -> Message
1220 mkCoAppMsg ty arg_co
1221 = vcat [text "Illegal type application:",
1222 hang (ptext (sLit "exp type:"))
1223 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1224 hang (ptext (sLit "arg type:"))
1225 4 (ppr arg_co <+> dcolon <+> ppr (coercionKind arg_co))]