3 % (c) The University of Glasgow 2006
4 % (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
7 A ``lint'' pass to check for Core correctness
10 module CoreLint ( lintCoreBindings, lintUnfolding ) where
12 #include "HsVersions.h"
46 %************************************************************************
48 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
50 %************************************************************************
52 Checks that a set of core bindings is well-formed. The PprStyle and String
53 just control what we print in the event of an error. The Bool value
54 indicates whether we have done any specialisation yet (in which case we do
59 (b) Out-of-scope type variables
60 (c) Out-of-scope local variables
63 If we have done specialisation the we check that there are
64 (a) No top-level bindings of primitive (unboxed type)
69 -- Things are *not* OK if:
71 -- * Unsaturated type app before specialisation has been done;
73 -- * Oversaturated type app after specialisation (eta reduction
74 -- may well be happening...);
77 Note [Linting type lets]
78 ~~~~~~~~~~~~~~~~~~~~~~~~
79 In the desugarer, it's very very convenient to be able to say (in effect)
80 let a = Type Int in <body>
81 That is, use a type let. See Note [Type let] in CoreSyn.
83 However, when linting <body> we need to remember that a=Int, else we might
84 reject a correct program. So we carry a type substitution (in this example
85 [a -> Int]) and apply this substitution before comparing types. The functin
86 lintInTy :: Type -> LintM Type
87 returns a substituted type; that's the only reason it returns anything.
89 When we encounter a binder (like x::a) we must apply the substitution
90 to the type of the binding variable. lintBinders does this.
92 For Ids, the type-substituted Id is added to the in_scope set (which
93 itself is part of the TvSubst we are carrying down), and when we
94 find an occurence of an Id, we fetch it from the in-scope set.
98 lintCoreBindings :: [CoreBind] -> (Bag Message, Bag Message)
99 -- Returns (warnings, errors)
100 lintCoreBindings binds
101 = initL (lint_binds binds)
103 -- Put all the top-level binders in scope at the start
104 -- This is because transformation rules can bring something
105 -- into use 'unexpectedly'
106 lint_binds binds = addLoc TopLevelBindings $
107 addInScopeVars (bindersOfBinds binds) $
110 lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
111 lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
114 %************************************************************************
116 \subsection[lintUnfolding]{lintUnfolding}
118 %************************************************************************
120 We use this to check all unfoldings that come in from interfaces
121 (it is very painful to catch errors otherwise):
124 lintUnfolding :: SrcLoc
125 -> [Var] -- Treat these as in scope
127 -> Maybe Message -- Nothing => OK
129 lintUnfolding locn vars expr
130 | isEmptyBag errs = Nothing
131 | otherwise = Just (pprMessageBag errs)
133 (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
134 addInScopeVars vars $
138 %************************************************************************
140 \subsection[lintCoreBinding]{lintCoreBinding}
142 %************************************************************************
144 Check a core binding, returning the list of variables bound.
147 lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
148 lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
149 = addLoc (RhsOf binder) $
151 do { ty <- lintCoreExpr rhs
152 ; lintBinder binder -- Check match to RHS type
153 ; binder_ty <- applySubst binder_ty
154 ; checkTys binder_ty ty (mkRhsMsg binder ty)
155 -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
156 ; checkL (not (isUnLiftedType binder_ty)
157 || (isNonRec rec_flag && exprOkForSpeculation rhs))
158 (mkRhsPrimMsg binder rhs)
159 -- Check that if the binder is top-level or recursive, it's not demanded
160 ; checkL (not (isStrictId binder)
161 || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
163 -- Check whether binder's specialisations contain any out-of-scope variables
164 ; mapM_ (checkBndrIdInScope binder) bndr_vars
166 ; when (isNonRuleLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
167 (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
168 -- Only non-rule loop breakers inhibit inlining
170 -- Check whether arity and demand type are consistent (only if demand analysis
172 ; checkL (case maybeDmdTy of
173 Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
175 (mkArityMsg binder) }
177 -- We should check the unfolding, if any, but this is tricky because
178 -- the unfolding is a SimplifiableCoreExpr. Give up for now.
180 binder_ty = idType binder
181 maybeDmdTy = idStrictness_maybe binder
182 bndr_vars = varSetElems (idFreeVars binder)
183 lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
184 | otherwise = return ()
187 %************************************************************************
189 \subsection[lintCoreExpr]{lintCoreExpr}
191 %************************************************************************
194 type InType = Type -- Substitution not yet applied
198 type OutType = Type -- Substitution has been applied to this
200 type OutTyVar = TyVar
201 type OutCoVar = CoVar
203 lintCoreExpr :: CoreExpr -> LintM OutType
204 -- The returned type has the substitution from the monad
205 -- already applied to it:
206 -- lintCoreExpr e subst = exprType (subst e)
208 -- The returned "type" can be a kind, if the expression is (Type ty)
210 lintCoreExpr (Var var)
211 = do { checkL (not (var == oneTupleDataConId))
212 (ptext (sLit "Illegal one-tuple"))
215 ; var' <- lookupIdInScope var
216 ; return (idType var')
219 lintCoreExpr (Lit lit)
220 = return (literalType lit)
222 lintCoreExpr (Cast expr co)
223 = do { expr_ty <- lintCoreExpr expr
224 ; co' <- applySubst co
225 ; (from_ty, to_ty) <- lintCoercion co'
226 ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
229 lintCoreExpr (Note _ expr)
232 lintCoreExpr (Let (NonRec tv (Type ty)) body)
233 = -- See Note [Type let] in CoreSyn
234 do { checkL (isTyVar tv) (mkKindErrMsg tv ty) -- Not quite accurate
236 ; lintTyBndr tv $ \ tv' ->
237 addLoc (BodyOfLetRec [tv]) $
238 extendSubstL tv' ty' $ do
240 -- Now extend the substitution so we
241 -- take advantage of it in the body
242 ; lintCoreExpr body } }
244 lintCoreExpr (Let (NonRec bndr rhs) body)
245 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
246 ; addLoc (BodyOfLetRec [bndr])
247 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
249 lintCoreExpr (Let (Rec pairs) body)
250 = lintAndScopeIds bndrs $ \_ ->
251 do { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
252 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
254 bndrs = map fst pairs
256 lintCoreExpr e@(App fun arg)
257 = do { fun_ty <- lintCoreExpr fun
258 ; addLoc (AnExpr e) $
259 lintCoreArg fun_ty arg }
261 lintCoreExpr (Lam var expr)
262 = addLoc (LambdaBodyOf var) $
263 lintBinders [var] $ \[var'] ->
264 do { body_ty <- lintCoreExpr expr
266 return (mkFunTy (idType var') body_ty)
268 return (mkForAllTy var' body_ty)
270 -- The applySubst is needed to apply the subst to var
272 lintCoreExpr e@(Case scrut var alt_ty alts) =
273 -- Check the scrutinee
274 do { scrut_ty <- lintCoreExpr scrut
275 ; alt_ty <- lintInTy alt_ty
276 ; var_ty <- lintInTy (idType var)
278 ; let mb_tc_app = splitTyConApp_maybe (idType var)
283 not (isOpenTyCon tycon) &&
284 null (tyConDataCons tycon) ->
285 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
286 -- This can legitimately happen for type families
288 _otherwise -> return ()
290 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
292 ; subst <- getTvSubst
293 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
295 -- If the binder is an unboxed tuple type, don't put it in scope
296 ; let scope = if (isUnboxedTupleType (idType var)) then
298 else lintAndScopeId var
300 do { -- Check the alternatives
301 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
302 ; checkCaseAlts e scrut_ty alts
307 lintCoreExpr (Type ty)
308 = do { ty' <- lintInTy ty
309 ; return (typeKind ty') }
312 %************************************************************************
314 \subsection[lintCoreArgs]{lintCoreArgs}
316 %************************************************************************
318 The basic version of these functions checks that the argument is a
319 subtype of the required type, as one would expect.
322 lintCoreArg :: OutType -> CoreArg -> LintM OutType
323 lintCoreArg fun_ty (Type arg_ty)
324 = do { arg_ty' <- applySubst arg_ty
325 ; lintTyApp fun_ty arg_ty' }
327 lintCoreArg fun_ty arg
328 = do { arg_ty <- lintCoreExpr arg
329 ; lintValApp arg fun_ty arg_ty }
332 lintAltBinders :: OutType -- Scrutinee type
333 -> OutType -- Constructor type
334 -> [OutVar] -- Binders
336 lintAltBinders scrut_ty con_ty []
337 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
338 lintAltBinders scrut_ty con_ty (bndr:bndrs)
340 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
341 ; lintAltBinders scrut_ty con_ty' bndrs }
343 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
344 ; lintAltBinders scrut_ty con_ty' bndrs }
347 lintTyApp :: OutType -> OutType -> LintM OutType
348 lintTyApp fun_ty arg_ty
349 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
350 = do { checkKinds tyvar arg_ty
351 ; if isCoVar tyvar then
352 return body_ty -- Co-vars don't appear in body_ty!
354 return (substTyWith [tyvar] [arg_ty] body_ty) }
356 = failWithL (mkTyAppMsg fun_ty arg_ty)
359 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
360 lintValApp arg fun_ty arg_ty
361 | Just (arg,res) <- splitFunTy_maybe fun_ty
362 = do { checkTys arg arg_ty err1
367 err1 = mkAppMsg fun_ty arg_ty arg
368 err2 = mkNonFunAppMsg fun_ty arg_ty arg
372 checkKinds :: Var -> OutType -> LintM ()
373 -- Both args have had substitution applied
374 checkKinds tyvar arg_ty
375 -- Arg type might be boxed for a function with an uncommitted
376 -- tyvar; notably this is used so that we can give
377 -- error :: forall a:*. String -> a
378 -- and then apply it to both boxed and unboxed types.
379 | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
380 ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
381 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
382 | otherwise = do { arg_kind <- lintType arg_ty
383 ; unless (arg_kind `isSubKind` tyvar_kind)
384 (addErrL (mkKindErrMsg tyvar arg_ty)) }
386 tyvar_kind = tyVarKind tyvar
387 (s1,t1) = coVarKind tyvar
389 checkDeadIdOcc :: Id -> LintM ()
390 -- Occurrences of an Id should never be dead....
391 -- except when we are checking a case pattern
393 | isDeadOcc (idOccInfo id)
394 = do { in_case <- inCasePat
396 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
402 %************************************************************************
404 \subsection[lintCoreAlts]{lintCoreAlts}
406 %************************************************************************
409 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
410 -- a) Check that the alts are non-empty
411 -- b1) Check that the DEFAULT comes first, if it exists
412 -- b2) Check that the others are in increasing order
413 -- c) Check that there's a default for infinite types
414 -- NB: Algebraic cases are not necessarily exhaustive, because
415 -- the simplifer correctly eliminates case that can't
419 = addErrL (mkNullAltsMsg e)
421 checkCaseAlts e ty alts =
422 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
423 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
424 ; checkL (isJust maybe_deflt || not is_infinite_ty)
425 (nonExhaustiveAltsMsg e) }
427 (con_alts, maybe_deflt) = findDefault alts
429 -- Check that successive alternatives have increasing tags
430 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
431 increasing_tag _ = True
433 non_deflt (DEFAULT, _, _) = False
436 is_infinite_ty = case splitTyConApp_maybe ty of
438 Just (tycon, _) -> isPrimTyCon tycon
442 checkAltExpr :: CoreExpr -> OutType -> LintM ()
443 checkAltExpr expr ann_ty
444 = do { actual_ty <- lintCoreExpr expr
445 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
447 lintCoreAlt :: OutType -- Type of scrutinee
448 -> OutType -- Type of the alternative
452 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
453 do { checkL (null args) (mkDefaultArgsMsg args)
454 ; checkAltExpr rhs alt_ty }
456 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
457 do { checkL (null args) (mkDefaultArgsMsg args)
458 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
459 ; checkAltExpr rhs alt_ty }
461 lit_ty = literalType lit
463 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
464 | isNewTyCon (dataConTyCon con)
465 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
466 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
467 = addLoc (CaseAlt alt) $ do
468 { -- First instantiate the universally quantified
469 -- type variables of the data constructor
470 -- We've already check
471 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
472 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
474 -- And now bring the new binders into scope
475 ; lintBinders args $ \ args' -> do
476 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
477 ; checkAltExpr rhs alt_ty } }
479 | otherwise -- Scrut-ty is wrong shape
480 = addErrL (mkBadAltMsg scrut_ty alt)
483 %************************************************************************
485 \subsection[lint-types]{Types}
487 %************************************************************************
490 -- When we lint binders, we (one at a time and in order):
491 -- 1. Lint var types or kinds (possibly substituting)
492 -- 2. Add the binder to the in scope set, and if its a coercion var,
493 -- we may extend the substitution to reflect its (possibly) new kind
494 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
495 lintBinders [] linterF = linterF []
496 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
497 lintBinders vars $ \ vars' ->
500 lintBinder :: Var -> (Var -> LintM a) -> LintM a
501 lintBinder var linterF
502 | isId var = lintIdBndr var linterF
503 | otherwise = lintTyBndr var linterF
505 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
506 lintTyBndr tv thing_inside
507 = do { subst <- getTvSubst
508 ; let (subst', tv') = substTyVarBndr subst tv
510 ; updateTvSubst subst' (thing_inside tv') }
512 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
513 -- Do substitution on the type of a binder and add the var with this
514 -- new type to the in-scope set of the second argument
515 -- ToDo: lint its rules
517 lintIdBndr id linterF
518 = do { checkL (not (isUnboxedTupleType (idType id)))
519 (mkUnboxedTupleMsg id)
520 -- No variable can be bound to an unboxed tuple.
521 ; lintAndScopeId id $ \id' -> linterF id' }
523 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
524 lintAndScopeIds ids linterF
528 go (id:ids) = lintAndScopeId id $ \id ->
529 lintAndScopeIds ids $ \ids ->
532 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
533 lintAndScopeId id linterF
534 = do { ty <- lintInTy (idType id)
535 ; let id' = setIdType id ty
536 ; addInScopeVar id' $ (linterF id') }
540 %************************************************************************
542 \subsection[lint-monad]{The Lint monad}
544 %************************************************************************
547 lintInTy :: InType -> LintM OutType
548 -- Check the type, and apply the substitution to it
549 -- See Note [Linting type lets]
550 -- ToDo: check the kind structure of the type
552 = addLoc (InType ty) $
553 do { ty' <- applySubst ty
558 lintKind :: Kind -> LintM ()
559 -- Check well-formedness of kinds: *, *->*, etc
560 lintKind (TyConApp tc [])
561 | getUnique tc `elem` kindKeys
563 lintKind (FunTy k1 k2)
564 = lintKind k1 >> lintKind k2
566 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
569 lintTyBndrKind :: OutTyVar -> LintM ()
571 | isCoVar tv = lintCoVarKind tv
572 | otherwise = lintKind (tyVarKind tv)
575 lintCoVarKind :: OutCoVar -> LintM ()
576 -- Check the kind of a coercion binder
578 = do { (ty1,ty2) <- lintSplitCoVar tv
581 ; unless (k1 `eqKind` k2)
582 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
583 , nest 2 (quotes (ppr tv))
587 lintSplitCoVar :: CoVar -> LintM (Type,Type)
589 = case coVarKind_maybe cv of
591 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
592 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
595 lintCoercion :: OutType -> LintM (OutType, OutType)
596 -- Check the kind of a coercion term, returning the kind
597 lintCoercion ty@(TyVarTy tv)
598 = do { checkTyVarInScope tv
599 ; if isCoVar tv then return (coVarKind tv)
600 else return (ty, ty) }
602 lintCoercion ty@(AppTy ty1 ty2)
603 = do { (s1,t1) <- lintCoercion ty1
604 ; (s2,t2) <- lintCoercion ty2
605 ; check_co_app ty (typeKind s1) [s2]
606 ; return (AppTy s1 s2, AppTy t1 t2) }
608 lintCoercion ty@(FunTy ty1 ty2)
609 = do { (s1,t1) <- lintCoercion ty1
610 ; (s2,t2) <- lintCoercion ty2
611 ; check_co_app ty (tyConKind funTyCon) [s1, s2]
612 ; return (FunTy s1 s2, FunTy t1 t2) }
614 lintCoercion ty@(TyConApp tc tys)
615 | Just (ar, desc) <- isCoercionTyCon_maybe tc
616 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
617 ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
618 ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
619 ; check_co_app ty (typeKind s) ss
620 ; return (mkAppTys s ss, mkAppTys t ts) }
622 | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
626 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
627 ; check_co_app ty (tyConKind tc) ss
628 ; return (TyConApp tc ss, TyConApp tc ts) }
630 lintCoercion ty@(PredTy (ClassP cls tys))
631 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
632 ; check_co_app ty (tyConKind (classTyCon cls)) ss
633 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
635 lintCoercion (PredTy (IParam n p_ty))
636 = do { (s,t) <- lintCoercion p_ty
637 ; return (PredTy (IParam n s), PredTy (IParam n t)) }
639 lintCoercion ty@(PredTy (EqPred {}))
640 = failWithL (badEq ty)
642 lintCoercion (ForAllTy tv ty)
644 = do { (co1, co2) <- lintSplitCoVar tv
645 ; (s1,t1) <- lintCoercion co1
646 ; (s2,t2) <- lintCoercion co2
647 ; (sr,tr) <- lintCoercion ty
648 ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
651 = do { lintKind (tyVarKind tv)
652 ; (s,t) <- addInScopeVar tv (lintCoercion ty)
653 ; return (ForAllTy tv s, ForAllTy tv t) }
655 badCo :: Coercion -> LintM a
656 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
659 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
660 -- Always called with correct number of coercion arguments
661 -- First arg is just for error message
662 lintCoTyConApp _ CoLeft (co:_) = lintLR fst co
663 lintCoTyConApp _ CoRight (co:_) = lintLR snd co
664 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co
665 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co
666 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
668 lintCoTyConApp _ CoSym (co:_)
669 = do { (ty1,ty2) <- lintCoercion co
672 lintCoTyConApp co CoTrans (co1:co2:_)
673 = do { (ty1a, ty1b) <- lintCoercion co1
674 ; (ty2a, ty2b) <- lintCoercion co2
675 ; checkL (ty1b `coreEqType` ty2a)
676 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
677 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
678 ; return (ty1a, ty2b) }
680 lintCoTyConApp _ CoInst (co:arg_ty:_)
681 = do { co_tys <- lintCoercion co
682 ; arg_kind <- lintType arg_ty
683 ; case decompInst_maybe co_tys of
684 Just ((tv1,tv2), (ty1,ty2))
685 | arg_kind `isSubKind` tyVarKind tv1
686 -> return (substTyWith [tv1] [arg_ty] ty1,
687 substTyWith [tv2] [arg_ty] ty2)
689 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
690 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
692 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
693 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
694 = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
695 ; sequence_ (zipWith checkKinds tvs tys1)
696 ; return (substTyWith tvs tys1 lhs_ty,
697 substTyWith tvs tys2 rhs_ty) }
699 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
700 = do { _ <- lintType ty1
701 ; _ <- lintType ty2 -- Ignore kinds; it's unsafe!
704 lintCoTyConApp _ _ _ = panic "lintCoTyConApp" -- Called with wrong number of coercion args
707 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
709 = do { (ty1,ty2) <- lintCoercion co
710 ; case decompLR_maybe (ty1,ty2) of
711 Just res -> return (sel res)
712 Nothing -> failWithL (ptext (sLit "Bad argument of left/right")) }
715 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
717 = do { (ty1,ty2) <- lintCoercion co
718 ; case decompCsel_maybe (ty1,ty2) of
719 Just res -> return (sel res)
720 Nothing -> failWithL (ptext (sLit "Bad argument of csel")) }
723 lintType :: OutType -> LintM Kind
724 lintType (TyVarTy tv)
725 = do { checkTyVarInScope tv
726 ; return (tyVarKind tv) }
728 lintType ty@(AppTy t1 t2)
729 = do { k1 <- lintType t1
730 ; lint_ty_app ty k1 [t2] }
732 lintType ty@(FunTy t1 t2)
733 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
735 lintType ty@(TyConApp tc tys)
737 = lint_ty_app ty (tyConKind tc) tys
739 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
741 lintType (ForAllTy tv ty)
742 = do { lintTyBndrKind tv
743 ; addInScopeVar tv (lintType ty) }
745 lintType ty@(PredTy (ClassP cls tys))
746 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
748 lintType (PredTy (IParam _ p_ty))
751 lintType ty@(PredTy (EqPred {}))
752 = failWithL (badEq ty)
755 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
757 = do { ks <- mapM lintType tys
758 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
761 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
762 check_co_app ty k tys
763 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
768 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
769 lint_kind_app doc kfn ks = go kfn ks
771 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
772 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
773 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
775 go kfn [] = return kfn
776 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
777 Nothing -> failWithL fail_msg
778 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
782 badEq :: Type -> SDoc
783 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
787 %************************************************************************
789 \subsection[lint-monad]{The Lint monad}
791 %************************************************************************
796 [LintLocInfo] -> -- Locations
797 TvSubst -> -- Current type substitution; we also use this
798 -- to keep track of all the variables in scope,
799 -- both Ids and TyVars
800 WarnsAndErrs -> -- Error and warning messages so far
801 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
803 type WarnsAndErrs = (Bag Message, Bag Message)
805 {- Note [Type substitution]
806 ~~~~~~~~~~~~~~~~~~~~~~~~
807 Why do we need a type substitution? Consider
808 /\(a:*). \(x:a). /\(a:*). id a x
809 This is ill typed, because (renaming variables) it is really
810 /\(a:*). \(x:a). /\(b:*). id b x
811 Hence, when checking an application, we can't naively compare x's type
812 (at its binding site) with its expected type (at a use site). So we
813 rename type binders as we go, maintaining a substitution.
815 The same substitution also supports let-type, current expressed as
817 Here we substitute 'ty' for 'a' in 'body', on the fly.
820 instance Monad LintM where
821 return x = LintM (\ _ _ errs -> (Just x, errs))
822 fail err = failWithL (text err)
823 m >>= k = LintM (\ loc subst errs ->
824 let (res, errs') = unLintM m loc subst errs in
826 Just r -> unLintM (k r) loc subst errs'
827 Nothing -> (Nothing, errs'))
830 = RhsOf Id -- The variable bound
831 | LambdaBodyOf Id -- The lambda-binder
832 | BodyOfLetRec [Id] -- One of the binders
833 | CaseAlt CoreAlt -- Case alternative
834 | CasePat CoreAlt -- The *pattern* of the case alternative
835 | AnExpr CoreExpr -- Some expression
836 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
838 | InType Type -- Inside a type
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
892 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
894 = failWithL (dupVars dups)
896 (_, dups) = removeDups compare vars
898 addInScopeVar :: Var -> LintM a -> LintM a
900 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
902 updateTvSubst :: TvSubst -> LintM a -> LintM a
903 updateTvSubst subst' m =
904 LintM (\ loc _ errs -> unLintM m loc subst' errs)
906 getTvSubst :: LintM TvSubst
907 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
909 applySubst :: Type -> LintM Type
910 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
912 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
914 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
918 lookupIdInScope :: Id -> LintM Id
920 | not (mustHaveLocalBinding id)
921 = return id -- An imported Id
923 = do { subst <- getTvSubst
924 ; case lookupInScope (getTvInScope subst) id of
926 Nothing -> do { addErrL out_of_scope
929 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
932 oneTupleDataConId :: Id -- Should not happen
933 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
935 checkBndrIdInScope :: Var -> Var -> LintM ()
936 checkBndrIdInScope binder id
937 = checkInScope msg id
939 msg = ptext (sLit "is out of scope inside info for") <+>
942 checkTyVarInScope :: TyVar -> LintM ()
943 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
945 checkInScope :: SDoc -> Var -> LintM ()
946 checkInScope loc_msg var =
947 do { subst <- getTvSubst
948 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
949 (hsep [ppr var, loc_msg]) }
951 checkTys :: OutType -> OutType -> Message -> LintM ()
952 -- check ty2 is subtype of ty1 (ie, has same structure but usage
953 -- annotations need only be consistent, not equal)
954 -- Assumes ty1,ty2 are have alrady had the substitution applied
955 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
958 %************************************************************************
960 \subsection{Error messages}
962 %************************************************************************
965 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
968 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
970 dumpLoc (LambdaBodyOf b)
971 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
973 dumpLoc (BodyOfLetRec [])
974 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
976 dumpLoc (BodyOfLetRec bs@(_:_))
977 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
980 = (noSrcLoc, text "In the expression:" <+> ppr e)
982 dumpLoc (CaseAlt (con, args, _))
983 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
985 dumpLoc (CasePat (con, args, _))
986 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
988 dumpLoc (ImportedUnfolding locn)
989 = (locn, brackets (ptext (sLit "in an imported unfolding")))
990 dumpLoc TopLevelBindings
993 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
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 mkKindErrMsg :: TyVar -> Type -> Message
1086 mkKindErrMsg tyvar arg_ty
1087 = vcat [ptext (sLit "Kinds don't match in type application:"),
1088 hang (ptext (sLit "Type variable:"))
1089 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1090 hang (ptext (sLit "Arg type:"))
1091 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1093 mkCoAppErrMsg :: TyVar -> Type -> Message
1094 mkCoAppErrMsg tyvar arg_ty
1095 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1096 hang (ptext (sLit "Coercion variable:"))
1097 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1098 hang (ptext (sLit "Arg coercion:"))
1099 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
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)]
1131 mkArityMsg :: Id -> Message
1133 = vcat [hsep [ptext (sLit "Demand type has "),
1134 ppr (dmdTypeDepth dmd_ty),
1135 ptext (sLit " arguments, rhs has "),
1136 ppr (idArity binder),
1137 ptext (sLit "arguments, "),
1139 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1142 where (StrictSig dmd_ty) = idStrictness binder
1144 mkUnboxedTupleMsg :: Id -> Message
1145 mkUnboxedTupleMsg binder
1146 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1147 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1149 mkCastErr :: Type -> Type -> Message
1150 mkCastErr from_ty expr_ty
1151 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1152 ptext (sLit "From-type:") <+> ppr from_ty,
1153 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1156 dupVars :: [[Var]] -> Message
1158 = hang (ptext (sLit "Duplicate variables brought into scope"))