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') }
218 lintCoreExpr (Lit lit)
219 = return (literalType lit)
221 lintCoreExpr (Cast expr co)
222 = do { expr_ty <- lintCoreExpr expr
223 ; co' <- applySubst co
224 ; (from_ty, to_ty) <- lintCoercion co'
225 ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
228 lintCoreExpr (Note _ expr)
231 lintCoreExpr (Let (NonRec tv (Type ty)) body)
233 = -- See Note [Linting type lets]
234 do { ty' <- addLoc (RhsOf tv) $ lintInTy ty
235 ; lintTyBndr tv $ \ tv' ->
236 addLoc (BodyOfLetRec [tv]) $
237 extendSubstL tv' ty' $ do
239 -- Now extend the substitution so we
240 -- take advantage of it in the body
241 ; lintCoreExpr body } }
244 = do { co <- applySubst ty
245 ; (s1,s2) <- addLoc (RhsOf tv) $ lintCoercion co
246 ; lintTyBndr tv $ \ tv' ->
247 addLoc (BodyOfLetRec [tv]) $ do
248 { let (t1,t2) = coVarKind tv'
249 ; checkTys s1 t1 (mkTyVarLetErr tv ty)
250 ; checkTys s2 t2 (mkTyVarLetErr tv ty)
251 ; lintCoreExpr body } }
254 = failWithL (mkTyVarLetErr tv ty) -- Not quite accurate
256 lintCoreExpr (Let (NonRec bndr rhs) body)
257 = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
258 ; addLoc (BodyOfLetRec [bndr])
259 (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
261 lintCoreExpr (Let (Rec pairs) body)
262 = lintAndScopeIds bndrs $ \_ ->
263 do { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
264 ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
266 bndrs = map fst pairs
268 lintCoreExpr e@(App fun arg)
269 = do { fun_ty <- lintCoreExpr fun
270 ; addLoc (AnExpr e) $
271 lintCoreArg fun_ty arg }
273 lintCoreExpr (Lam var expr)
274 = addLoc (LambdaBodyOf var) $
275 lintBinders [var] $ \ vars' ->
276 do { let [var'] = vars'
277 ; body_ty <- lintCoreExpr expr
279 return (mkFunTy (idType var') body_ty)
281 return (mkForAllTy var' body_ty)
283 -- The applySubst is needed to apply the subst to var
285 lintCoreExpr e@(Case scrut var alt_ty alts) =
286 -- Check the scrutinee
287 do { scrut_ty <- lintCoreExpr scrut
288 ; alt_ty <- lintInTy alt_ty
289 ; var_ty <- lintInTy (idType var)
291 ; let mb_tc_app = splitTyConApp_maybe (idType var)
296 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
297 null (tyConDataCons tycon) ->
298 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
299 -- This can legitimately happen for type families
301 _otherwise -> return ()
303 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
305 ; subst <- getTvSubst
306 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
308 -- If the binder is an unboxed tuple type, don't put it in scope
309 ; let scope = if (isUnboxedTupleType (idType var)) then
311 else lintAndScopeId var
313 do { -- Check the alternatives
314 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
315 ; checkCaseAlts e scrut_ty alts
320 lintCoreExpr (Type ty)
321 = do { ty' <- lintInTy ty
322 ; return (typeKind ty') }
325 %************************************************************************
327 \subsection[lintCoreArgs]{lintCoreArgs}
329 %************************************************************************
331 The basic version of these functions checks that the argument is a
332 subtype of the required type, as one would expect.
335 lintCoreArg :: OutType -> CoreArg -> LintM OutType
336 lintCoreArg fun_ty (Type arg_ty)
337 = do { arg_ty' <- applySubst arg_ty
338 ; lintTyApp fun_ty arg_ty' }
340 lintCoreArg fun_ty arg
341 = do { arg_ty <- lintCoreExpr arg
342 ; lintValApp arg fun_ty arg_ty }
345 lintAltBinders :: OutType -- Scrutinee type
346 -> OutType -- Constructor type
347 -> [OutVar] -- Binders
349 lintAltBinders scrut_ty con_ty []
350 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
351 lintAltBinders scrut_ty con_ty (bndr:bndrs)
353 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
354 ; lintAltBinders scrut_ty con_ty' bndrs }
356 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
357 ; lintAltBinders scrut_ty con_ty' bndrs }
360 lintTyApp :: OutType -> OutType -> LintM OutType
361 lintTyApp fun_ty arg_ty
362 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
363 = do { checkKinds tyvar arg_ty
364 ; if isCoVar tyvar then
365 return body_ty -- Co-vars don't appear in body_ty!
367 return (substTyWith [tyvar] [arg_ty] body_ty) }
369 = failWithL (mkTyAppMsg fun_ty arg_ty)
372 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
373 lintValApp arg fun_ty arg_ty
374 | Just (arg,res) <- splitFunTy_maybe fun_ty
375 = do { checkTys arg arg_ty err1
380 err1 = mkAppMsg fun_ty arg_ty arg
381 err2 = mkNonFunAppMsg fun_ty arg_ty arg
385 checkKinds :: OutVar -> OutType -> LintM ()
386 -- Both args have had substitution applied
387 checkKinds tyvar arg_ty
388 -- Arg type might be boxed for a function with an uncommitted
389 -- tyvar; notably this is used so that we can give
390 -- error :: forall a:*. String -> a
391 -- and then apply it to both boxed and unboxed types.
392 | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
393 ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
394 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
395 | otherwise = do { arg_kind <- lintType arg_ty
396 ; unless (arg_kind `isSubKind` tyvar_kind)
397 (addErrL (mkKindErrMsg tyvar arg_ty)) }
399 tyvar_kind = tyVarKind tyvar
400 (s1,t1) = coVarKind tyvar
402 checkDeadIdOcc :: Id -> LintM ()
403 -- Occurrences of an Id should never be dead....
404 -- except when we are checking a case pattern
406 | isDeadOcc (idOccInfo id)
407 = do { in_case <- inCasePat
409 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
415 %************************************************************************
417 \subsection[lintCoreAlts]{lintCoreAlts}
419 %************************************************************************
422 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
423 -- a) Check that the alts are non-empty
424 -- b1) Check that the DEFAULT comes first, if it exists
425 -- b2) Check that the others are in increasing order
426 -- c) Check that there's a default for infinite types
427 -- NB: Algebraic cases are not necessarily exhaustive, because
428 -- the simplifer correctly eliminates case that can't
432 = addErrL (mkNullAltsMsg e)
434 checkCaseAlts e ty alts =
435 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
436 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
437 ; checkL (isJust maybe_deflt || not is_infinite_ty)
438 (nonExhaustiveAltsMsg e) }
440 (con_alts, maybe_deflt) = findDefault alts
442 -- Check that successive alternatives have increasing tags
443 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
444 increasing_tag _ = True
446 non_deflt (DEFAULT, _, _) = False
449 is_infinite_ty = case splitTyConApp_maybe ty of
451 Just (tycon, _) -> isPrimTyCon tycon
455 checkAltExpr :: CoreExpr -> OutType -> LintM ()
456 checkAltExpr expr ann_ty
457 = do { actual_ty <- lintCoreExpr expr
458 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
460 lintCoreAlt :: OutType -- Type of scrutinee
461 -> OutType -- Type of the alternative
465 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
466 do { checkL (null args) (mkDefaultArgsMsg args)
467 ; checkAltExpr rhs alt_ty }
469 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
470 do { checkL (null args) (mkDefaultArgsMsg args)
471 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
472 ; checkAltExpr rhs alt_ty }
474 lit_ty = literalType lit
476 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
477 | isNewTyCon (dataConTyCon con)
478 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
479 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
480 = addLoc (CaseAlt alt) $ do
481 { -- First instantiate the universally quantified
482 -- type variables of the data constructor
483 -- We've already check
484 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
485 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
487 -- And now bring the new binders into scope
488 ; lintBinders args $ \ args' -> do
489 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
490 ; checkAltExpr rhs alt_ty } }
492 | otherwise -- Scrut-ty is wrong shape
493 = addErrL (mkBadAltMsg scrut_ty alt)
496 %************************************************************************
498 \subsection[lint-types]{Types}
500 %************************************************************************
503 -- When we lint binders, we (one at a time and in order):
504 -- 1. Lint var types or kinds (possibly substituting)
505 -- 2. Add the binder to the in scope set, and if its a coercion var,
506 -- we may extend the substitution to reflect its (possibly) new kind
507 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
508 lintBinders [] linterF = linterF []
509 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
510 lintBinders vars $ \ vars' ->
513 lintBinder :: Var -> (Var -> LintM a) -> LintM a
514 lintBinder var linterF
515 | isId var = lintIdBndr var linterF
516 | otherwise = lintTyBndr var linterF
518 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
519 lintTyBndr tv thing_inside
520 = do { subst <- getTvSubst
521 ; let (subst', tv') = substTyVarBndr subst tv
523 ; updateTvSubst subst' (thing_inside tv') }
525 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
526 -- Do substitution on the type of a binder and add the var with this
527 -- new type to the in-scope set of the second argument
528 -- ToDo: lint its rules
530 lintIdBndr id linterF
531 = do { checkL (not (isUnboxedTupleType (idType id)))
532 (mkUnboxedTupleMsg id)
533 -- No variable can be bound to an unboxed tuple.
534 ; lintAndScopeId id $ \id' -> linterF id' }
536 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
537 lintAndScopeIds ids linterF
541 go (id:ids) = lintAndScopeId id $ \id ->
542 lintAndScopeIds ids $ \ids ->
545 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
546 lintAndScopeId id linterF
547 = do { ty <- lintInTy (idType id)
548 ; let id' = setIdType id ty
549 ; addInScopeVar id' $ (linterF id') }
553 %************************************************************************
555 \subsection[lint-monad]{The Lint monad}
557 %************************************************************************
560 lintInTy :: InType -> LintM OutType
561 -- Check the type, and apply the substitution to it
562 -- See Note [Linting type lets]
563 -- ToDo: check the kind structure of the type
565 = addLoc (InType ty) $
566 do { ty' <- applySubst ty
571 lintKind :: Kind -> LintM ()
572 -- Check well-formedness of kinds: *, *->*, etc
573 lintKind (TyConApp tc [])
574 | getUnique tc `elem` kindKeys
576 lintKind (FunTy k1 k2)
577 = lintKind k1 >> lintKind k2
579 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
582 lintTyBndrKind :: OutTyVar -> LintM ()
584 | isCoVar tv = lintCoVarKind tv
585 | otherwise = lintKind (tyVarKind tv)
588 lintCoVarKind :: OutCoVar -> LintM ()
589 -- Check the kind of a coercion binder
591 = do { (ty1,ty2) <- lintSplitCoVar tv
594 ; unless (k1 `eqKind` k2)
595 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
596 , nest 2 (quotes (ppr tv))
600 lintSplitCoVar :: CoVar -> LintM (Type,Type)
602 = case coVarKind_maybe cv of
604 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
605 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
608 lintCoercion, lintCoercion' :: OutType -> LintM (OutType, OutType)
609 -- Check the kind of a coercion term, returning the kind
611 = addLoc (InCoercion co) $ lintCoercion' co
613 lintCoercion' ty@(TyVarTy tv)
614 = do { checkTyVarInScope tv
615 ; if isCoVar tv then return (coVarKind tv)
616 else return (ty, ty) }
618 lintCoercion' ty@(AppTy ty1 ty2)
619 = do { (s1,t1) <- lintCoercion ty1
620 ; (s2,t2) <- lintCoercion ty2
621 ; check_co_app ty (typeKind s1) [s2]
622 ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
624 lintCoercion' ty@(FunTy ty1 ty2)
625 = do { (s1,t1) <- lintCoercion ty1
626 ; (s2,t2) <- lintCoercion ty2
627 ; check_co_app ty (tyConKind funTyCon) [s1, s2]
628 ; return (FunTy s1 s2, FunTy t1 t2) }
630 lintCoercion' ty@(TyConApp tc tys)
631 | Just (ar, desc) <- isCoercionTyCon_maybe tc
632 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
633 ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
634 ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
635 ; check_co_app ty (typeKind s) ss
636 ; return (mkAppTys s ss, mkAppTys t ts) }
638 | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
642 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
643 ; check_co_app ty (tyConKind tc) ss
644 ; return (TyConApp tc ss, TyConApp tc ts) }
646 lintCoercion' ty@(PredTy (ClassP cls tys))
647 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
648 ; check_co_app ty (tyConKind (classTyCon cls)) ss
649 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
651 lintCoercion' (PredTy (IParam n p_ty))
652 = do { (s,t) <- lintCoercion p_ty
653 ; return (PredTy (IParam n s), PredTy (IParam n t)) }
655 lintCoercion' ty@(PredTy (EqPred {}))
656 = failWithL (badEq ty)
658 lintCoercion' (ForAllTy tv ty)
660 = do { (co1, co2) <- lintSplitCoVar tv
661 ; (s1,t1) <- lintCoercion co1
662 ; (s2,t2) <- lintCoercion co2
663 ; (sr,tr) <- lintCoercion ty
664 ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
667 = do { lintKind (tyVarKind tv)
668 ; (s,t) <- addInScopeVar tv (lintCoercion ty)
669 ; return (ForAllTy tv s, ForAllTy tv t) }
671 badCo :: Coercion -> LintM a
672 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
675 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
676 -- Always called with correct number of coercion arguments
677 -- First arg is just for error message
678 lintCoTyConApp _ CoLeft (co:_) = lintLR fst co
679 lintCoTyConApp _ CoRight (co:_) = lintLR snd co
680 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co
681 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co
682 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
684 lintCoTyConApp _ CoSym (co:_)
685 = do { (ty1,ty2) <- lintCoercion co
688 lintCoTyConApp co CoTrans (co1:co2:_)
689 = do { (ty1a, ty1b) <- lintCoercion co1
690 ; (ty2a, ty2b) <- lintCoercion co2
691 ; checkL (ty1b `coreEqType` ty2a)
692 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
693 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
694 ; return (ty1a, ty2b) }
696 lintCoTyConApp _ CoInst (co:arg_ty:_)
697 = do { co_tys <- lintCoercion co
698 ; arg_kind <- lintType arg_ty
699 ; case decompInst_maybe co_tys of
700 Just ((tv1,tv2), (ty1,ty2))
701 | arg_kind `isSubKind` tyVarKind tv1
702 -> return (substTyWith [tv1] [arg_ty] ty1,
703 substTyWith [tv2] [arg_ty] ty2)
705 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
706 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
708 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
709 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
710 = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
711 ; sequence_ (zipWith checkKinds tvs tys1)
712 ; return (substTyWith tvs tys1 lhs_ty,
713 substTyWith tvs tys2 rhs_ty) }
715 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
716 = do { _ <- lintType ty1
717 ; _ <- lintType ty2 -- Ignore kinds; it's unsafe!
720 lintCoTyConApp _ _ _ = panic "lintCoTyConApp" -- Called with wrong number of coercion args
723 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
725 = do { (ty1,ty2) <- lintCoercion co
726 ; case decompLR_maybe (ty1,ty2) of
727 Just res -> return (sel res)
728 Nothing -> failWithL (ptext (sLit "Bad argument of left/right")) }
731 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
733 = do { (ty1,ty2) <- lintCoercion co
734 ; case decompCsel_maybe (ty1,ty2) of
735 Just res -> return (sel res)
736 Nothing -> failWithL (ptext (sLit "Bad argument of csel")) }
739 lintType :: OutType -> LintM Kind
740 lintType (TyVarTy tv)
741 = do { checkTyVarInScope tv
742 ; return (tyVarKind tv) }
744 lintType ty@(AppTy t1 t2)
745 = do { k1 <- lintType t1
746 ; lint_ty_app ty k1 [t2] }
748 lintType ty@(FunTy t1 t2)
749 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
751 lintType ty@(TyConApp tc tys)
753 = lint_ty_app ty (tyConKind tc) tys
755 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
757 lintType (ForAllTy tv ty)
758 = do { lintTyBndrKind tv
759 ; addInScopeVar tv (lintType ty) }
761 lintType ty@(PredTy (ClassP cls tys))
762 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
764 lintType (PredTy (IParam _ p_ty))
767 lintType ty@(PredTy (EqPred {}))
768 = failWithL (badEq ty)
771 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
773 = do { ks <- mapM lintType tys
774 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
777 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
778 check_co_app ty k tys
779 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
784 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
785 lint_kind_app doc kfn ks = go kfn ks
787 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
788 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
789 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
791 go kfn [] = return kfn
792 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
793 Nothing -> failWithL fail_msg
794 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
798 badEq :: Type -> SDoc
799 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
803 %************************************************************************
805 \subsection[lint-monad]{The Lint monad}
807 %************************************************************************
812 [LintLocInfo] -> -- Locations
813 TvSubst -> -- Current type substitution; we also use this
814 -- to keep track of all the variables in scope,
815 -- both Ids and TyVars
816 WarnsAndErrs -> -- Error and warning messages so far
817 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
819 type WarnsAndErrs = (Bag Message, Bag Message)
821 {- Note [Type substitution]
822 ~~~~~~~~~~~~~~~~~~~~~~~~
823 Why do we need a type substitution? Consider
824 /\(a:*). \(x:a). /\(a:*). id a x
825 This is ill typed, because (renaming variables) it is really
826 /\(a:*). \(x:a). /\(b:*). id b x
827 Hence, when checking an application, we can't naively compare x's type
828 (at its binding site) with its expected type (at a use site). So we
829 rename type binders as we go, maintaining a substitution.
831 The same substitution also supports let-type, current expressed as
833 Here we substitute 'ty' for 'a' in 'body', on the fly.
836 instance Monad LintM where
837 return x = LintM (\ _ _ errs -> (Just x, errs))
838 fail err = failWithL (text err)
839 m >>= k = LintM (\ loc subst errs ->
840 let (res, errs') = unLintM m loc subst errs in
842 Just r -> unLintM (k r) loc subst errs'
843 Nothing -> (Nothing, errs'))
846 = RhsOf Id -- The variable bound
847 | LambdaBodyOf Id -- The lambda-binder
848 | BodyOfLetRec [Id] -- One of the binders
849 | CaseAlt CoreAlt -- Case alternative
850 | CasePat CoreAlt -- The *pattern* of the case alternative
851 | AnExpr CoreExpr -- Some expression
852 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
854 | InType Type -- Inside a type
855 | InCoercion Coercion -- Inside a type
860 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
862 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
867 checkL :: Bool -> Message -> LintM ()
868 checkL True _ = return ()
869 checkL False msg = failWithL msg
871 failWithL :: Message -> LintM a
872 failWithL msg = LintM $ \ loc subst (warns,errs) ->
873 (Nothing, (warns, addMsg subst errs msg loc))
875 addErrL :: Message -> LintM ()
876 addErrL msg = LintM $ \ loc subst (warns,errs) ->
877 (Just (), (warns, addMsg subst errs msg loc))
879 addWarnL :: Message -> LintM ()
880 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
881 (Just (), (addMsg subst warns msg loc, errs))
883 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
884 addMsg subst msgs msg locs
885 = ASSERT( notNull locs )
886 msgs `snocBag` mk_msg msg
888 (loc, cxt1) = dumpLoc (head locs)
889 cxts = [snd (dumpLoc loc) | loc <- locs]
890 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
891 ptext (sLit "Substitution:") <+> ppr subst
894 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
896 addLoc :: LintLocInfo -> LintM a -> LintM a
898 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
900 inCasePat :: LintM Bool -- A slight hack; see the unique call site
901 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
903 is_case_pat (CasePat {} : _) = True
904 is_case_pat _other = False
906 addInScopeVars :: [Var] -> LintM a -> LintM a
907 addInScopeVars vars m
909 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
911 = failWithL (dupVars dups)
913 (_, dups) = removeDups compare vars
915 addInScopeVar :: Var -> LintM a -> LintM a
917 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
919 updateTvSubst :: TvSubst -> LintM a -> LintM a
920 updateTvSubst subst' m =
921 LintM (\ loc _ errs -> unLintM m loc subst' errs)
923 getTvSubst :: LintM TvSubst
924 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
926 applySubst :: Type -> LintM Type
927 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
929 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
931 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
935 lookupIdInScope :: Id -> LintM Id
937 | not (mustHaveLocalBinding id)
938 = return id -- An imported Id
940 = do { subst <- getTvSubst
941 ; case lookupInScope (getTvInScope subst) id of
943 Nothing -> do { addErrL out_of_scope
946 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
949 oneTupleDataConId :: Id -- Should not happen
950 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
952 checkBndrIdInScope :: Var -> Var -> LintM ()
953 checkBndrIdInScope binder id
954 = checkInScope msg id
956 msg = ptext (sLit "is out of scope inside info for") <+>
959 checkTyVarInScope :: TyVar -> LintM ()
960 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
962 checkInScope :: SDoc -> Var -> LintM ()
963 checkInScope loc_msg var =
964 do { subst <- getTvSubst
965 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
966 (hsep [ppr var, loc_msg]) }
968 checkTys :: OutType -> OutType -> Message -> LintM ()
969 -- check ty2 is subtype of ty1 (ie, has same structure but usage
970 -- annotations need only be consistent, not equal)
971 -- Assumes ty1,ty2 are have alrady had the substitution applied
972 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
975 %************************************************************************
977 \subsection{Error messages}
979 %************************************************************************
982 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
985 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
987 dumpLoc (LambdaBodyOf b)
988 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
990 dumpLoc (BodyOfLetRec [])
991 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
993 dumpLoc (BodyOfLetRec bs@(_:_))
994 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
997 = (noSrcLoc, text "In the expression:" <+> ppr e)
999 dumpLoc (CaseAlt (con, args, _))
1000 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1002 dumpLoc (CasePat (con, args, _))
1003 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1005 dumpLoc (ImportedUnfolding locn)
1006 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1007 dumpLoc TopLevelBindings
1010 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1011 dumpLoc (InCoercion ty)
1012 = (noSrcLoc, text "In the coercion" <+> quotes (ppr ty))
1014 pp_binders :: [Var] -> SDoc
1015 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1017 pp_binder :: Var -> SDoc
1018 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1019 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1023 ------------------------------------------------------
1024 -- Messages for case expressions
1026 mkNullAltsMsg :: CoreExpr -> Message
1028 = hang (text "Case expression with no alternatives:")
1031 mkDefaultArgsMsg :: [Var] -> Message
1032 mkDefaultArgsMsg args
1033 = hang (text "DEFAULT case with binders")
1036 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1037 mkCaseAltMsg e ty1 ty2
1038 = hang (text "Type of case alternatives not the same as the annotation on case:")
1039 4 (vcat [ppr ty1, ppr ty2, ppr e])
1041 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1042 mkScrutMsg var var_ty scrut_ty subst
1043 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1044 text "Result binder type:" <+> ppr var_ty,--(idType var),
1045 text "Scrutinee type:" <+> ppr scrut_ty,
1046 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1048 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1050 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1051 mkNonIncreasingAltsMsg e
1052 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1054 nonExhaustiveAltsMsg :: CoreExpr -> Message
1055 nonExhaustiveAltsMsg e
1056 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1058 mkBadConMsg :: TyCon -> DataCon -> Message
1059 mkBadConMsg tycon datacon
1061 text "In a case alternative, data constructor isn't in scrutinee type:",
1062 text "Scrutinee type constructor:" <+> ppr tycon,
1063 text "Data con:" <+> ppr datacon
1066 mkBadPatMsg :: Type -> Type -> Message
1067 mkBadPatMsg con_result_ty scrut_ty
1069 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1070 text "Pattern result type:" <+> ppr con_result_ty,
1071 text "Scrutinee type:" <+> ppr scrut_ty
1074 mkBadAltMsg :: Type -> CoreAlt -> Message
1075 mkBadAltMsg scrut_ty alt
1076 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1077 text "Scrutinee type:" <+> ppr scrut_ty,
1078 text "Alternative:" <+> pprCoreAlt alt ]
1080 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1081 mkNewTyDataConAltMsg scrut_ty alt
1082 = vcat [ text "Data alternative for newtype datacon",
1083 text "Scrutinee type:" <+> ppr scrut_ty,
1084 text "Alternative:" <+> pprCoreAlt alt ]
1087 ------------------------------------------------------
1088 -- Other error messages
1090 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1091 mkAppMsg fun_ty arg_ty arg
1092 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1093 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1094 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1095 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1097 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1098 mkNonFunAppMsg fun_ty arg_ty arg
1099 = vcat [ptext (sLit "Non-function type in function position"),
1100 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1101 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1102 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1104 mkTyVarLetErr :: TyVar -> Type -> Message
1105 mkTyVarLetErr tyvar ty
1106 = vcat [ptext (sLit "Bad `let' binding for type or coercion variable:"),
1107 hang (ptext (sLit "Type/coercion variable:"))
1108 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1109 hang (ptext (sLit "Arg type/coercion:"))
1112 mkKindErrMsg :: TyVar -> Type -> Message
1113 mkKindErrMsg tyvar arg_ty
1114 = vcat [ptext (sLit "Kinds don't match in type application:"),
1115 hang (ptext (sLit "Type variable:"))
1116 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1117 hang (ptext (sLit "Arg type:"))
1118 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1120 mkCoAppErrMsg :: TyVar -> Type -> Message
1121 mkCoAppErrMsg tyvar arg_ty
1122 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1123 hang (ptext (sLit "Coercion variable:"))
1124 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1125 hang (ptext (sLit "Arg coercion:"))
1126 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1128 mkTyAppMsg :: Type -> Type -> Message
1129 mkTyAppMsg ty arg_ty
1130 = vcat [text "Illegal type application:",
1131 hang (ptext (sLit "Exp type:"))
1132 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1133 hang (ptext (sLit "Arg type:"))
1134 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1136 mkRhsMsg :: Id -> Type -> Message
1139 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1141 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1142 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1144 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1145 mkRhsPrimMsg binder _rhs
1146 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1148 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1151 mkStrictMsg :: Id -> Message
1153 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1155 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1158 mkArityMsg :: Id -> Message
1160 = vcat [hsep [ptext (sLit "Demand type has "),
1161 ppr (dmdTypeDepth dmd_ty),
1162 ptext (sLit " arguments, rhs has "),
1163 ppr (idArity binder),
1164 ptext (sLit "arguments, "),
1166 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1169 where (StrictSig dmd_ty) = idStrictness binder
1171 mkUnboxedTupleMsg :: Id -> Message
1172 mkUnboxedTupleMsg binder
1173 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1174 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1176 mkCastErr :: Type -> Type -> Message
1177 mkCastErr from_ty expr_ty
1178 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1179 ptext (sLit "From-type:") <+> ppr from_ty,
1180 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1183 dupVars :: [[Var]] -> Message
1185 = hang (ptext (sLit "Duplicate variables brought into scope"))