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] $ \[var'] ->
276 do { body_ty <- lintCoreExpr expr
278 return (mkFunTy (idType var') body_ty)
280 return (mkForAllTy var' body_ty)
282 -- The applySubst is needed to apply the subst to var
284 lintCoreExpr e@(Case scrut var alt_ty alts) =
285 -- Check the scrutinee
286 do { scrut_ty <- lintCoreExpr scrut
287 ; alt_ty <- lintInTy alt_ty
288 ; var_ty <- lintInTy (idType var)
290 ; let mb_tc_app = splitTyConApp_maybe (idType var)
295 not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
296 null (tyConDataCons tycon) ->
297 pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
298 -- This can legitimately happen for type families
300 _otherwise -> return ()
302 -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
304 ; subst <- getTvSubst
305 ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
307 -- If the binder is an unboxed tuple type, don't put it in scope
308 ; let scope = if (isUnboxedTupleType (idType var)) then
310 else lintAndScopeId var
312 do { -- Check the alternatives
313 mapM_ (lintCoreAlt scrut_ty alt_ty) alts
314 ; checkCaseAlts e scrut_ty alts
319 lintCoreExpr (Type ty)
320 = do { ty' <- lintInTy ty
321 ; return (typeKind ty') }
324 %************************************************************************
326 \subsection[lintCoreArgs]{lintCoreArgs}
328 %************************************************************************
330 The basic version of these functions checks that the argument is a
331 subtype of the required type, as one would expect.
334 lintCoreArg :: OutType -> CoreArg -> LintM OutType
335 lintCoreArg fun_ty (Type arg_ty)
336 = do { arg_ty' <- applySubst arg_ty
337 ; lintTyApp fun_ty arg_ty' }
339 lintCoreArg fun_ty arg
340 = do { arg_ty <- lintCoreExpr arg
341 ; lintValApp arg fun_ty arg_ty }
344 lintAltBinders :: OutType -- Scrutinee type
345 -> OutType -- Constructor type
346 -> [OutVar] -- Binders
348 lintAltBinders scrut_ty con_ty []
349 = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
350 lintAltBinders scrut_ty con_ty (bndr:bndrs)
352 = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
353 ; lintAltBinders scrut_ty con_ty' bndrs }
355 = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
356 ; lintAltBinders scrut_ty con_ty' bndrs }
359 lintTyApp :: OutType -> OutType -> LintM OutType
360 lintTyApp fun_ty arg_ty
361 | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
362 = do { checkKinds tyvar arg_ty
363 ; if isCoVar tyvar then
364 return body_ty -- Co-vars don't appear in body_ty!
366 return (substTyWith [tyvar] [arg_ty] body_ty) }
368 = failWithL (mkTyAppMsg fun_ty arg_ty)
371 lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
372 lintValApp arg fun_ty arg_ty
373 | Just (arg,res) <- splitFunTy_maybe fun_ty
374 = do { checkTys arg arg_ty err1
379 err1 = mkAppMsg fun_ty arg_ty arg
380 err2 = mkNonFunAppMsg fun_ty arg_ty arg
384 checkKinds :: OutVar -> OutType -> LintM ()
385 -- Both args have had substitution applied
386 checkKinds tyvar arg_ty
387 -- Arg type might be boxed for a function with an uncommitted
388 -- tyvar; notably this is used so that we can give
389 -- error :: forall a:*. String -> a
390 -- and then apply it to both boxed and unboxed types.
391 | isCoVar tyvar = do { (s2,t2) <- lintCoercion arg_ty
392 ; unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
393 (addErrL (mkCoAppErrMsg tyvar arg_ty)) }
394 | otherwise = do { arg_kind <- lintType arg_ty
395 ; unless (arg_kind `isSubKind` tyvar_kind)
396 (addErrL (mkKindErrMsg tyvar arg_ty)) }
398 tyvar_kind = tyVarKind tyvar
399 (s1,t1) = coVarKind tyvar
401 checkDeadIdOcc :: Id -> LintM ()
402 -- Occurrences of an Id should never be dead....
403 -- except when we are checking a case pattern
405 | isDeadOcc (idOccInfo id)
406 = do { in_case <- inCasePat
408 (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
414 %************************************************************************
416 \subsection[lintCoreAlts]{lintCoreAlts}
418 %************************************************************************
421 checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
422 -- a) Check that the alts are non-empty
423 -- b1) Check that the DEFAULT comes first, if it exists
424 -- b2) Check that the others are in increasing order
425 -- c) Check that there's a default for infinite types
426 -- NB: Algebraic cases are not necessarily exhaustive, because
427 -- the simplifer correctly eliminates case that can't
431 = addErrL (mkNullAltsMsg e)
433 checkCaseAlts e ty alts =
434 do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
435 ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
436 ; checkL (isJust maybe_deflt || not is_infinite_ty)
437 (nonExhaustiveAltsMsg e) }
439 (con_alts, maybe_deflt) = findDefault alts
441 -- Check that successive alternatives have increasing tags
442 increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
443 increasing_tag _ = True
445 non_deflt (DEFAULT, _, _) = False
448 is_infinite_ty = case splitTyConApp_maybe ty of
450 Just (tycon, _) -> isPrimTyCon tycon
454 checkAltExpr :: CoreExpr -> OutType -> LintM ()
455 checkAltExpr expr ann_ty
456 = do { actual_ty <- lintCoreExpr expr
457 ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
459 lintCoreAlt :: OutType -- Type of scrutinee
460 -> OutType -- Type of the alternative
464 lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
465 do { checkL (null args) (mkDefaultArgsMsg args)
466 ; checkAltExpr rhs alt_ty }
468 lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs) =
469 do { checkL (null args) (mkDefaultArgsMsg args)
470 ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
471 ; checkAltExpr rhs alt_ty }
473 lit_ty = literalType lit
475 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
476 | isNewTyCon (dataConTyCon con)
477 = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
478 | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
479 = addLoc (CaseAlt alt) $ do
480 { -- First instantiate the universally quantified
481 -- type variables of the data constructor
482 -- We've already check
483 checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
484 ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
486 -- And now bring the new binders into scope
487 ; lintBinders args $ \ args' -> do
488 { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
489 ; checkAltExpr rhs alt_ty } }
491 | otherwise -- Scrut-ty is wrong shape
492 = addErrL (mkBadAltMsg scrut_ty alt)
495 %************************************************************************
497 \subsection[lint-types]{Types}
499 %************************************************************************
502 -- When we lint binders, we (one at a time and in order):
503 -- 1. Lint var types or kinds (possibly substituting)
504 -- 2. Add the binder to the in scope set, and if its a coercion var,
505 -- we may extend the substitution to reflect its (possibly) new kind
506 lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
507 lintBinders [] linterF = linterF []
508 lintBinders (var:vars) linterF = lintBinder var $ \var' ->
509 lintBinders vars $ \ vars' ->
512 lintBinder :: Var -> (Var -> LintM a) -> LintM a
513 lintBinder var linterF
514 | isId var = lintIdBndr var linterF
515 | otherwise = lintTyBndr var linterF
517 lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
518 lintTyBndr tv thing_inside
519 = do { subst <- getTvSubst
520 ; let (subst', tv') = substTyVarBndr subst tv
522 ; updateTvSubst subst' (thing_inside tv') }
524 lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
525 -- Do substitution on the type of a binder and add the var with this
526 -- new type to the in-scope set of the second argument
527 -- ToDo: lint its rules
529 lintIdBndr id linterF
530 = do { checkL (not (isUnboxedTupleType (idType id)))
531 (mkUnboxedTupleMsg id)
532 -- No variable can be bound to an unboxed tuple.
533 ; lintAndScopeId id $ \id' -> linterF id' }
535 lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
536 lintAndScopeIds ids linterF
540 go (id:ids) = lintAndScopeId id $ \id ->
541 lintAndScopeIds ids $ \ids ->
544 lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
545 lintAndScopeId id linterF
546 = do { ty <- lintInTy (idType id)
547 ; let id' = setIdType id ty
548 ; addInScopeVar id' $ (linterF id') }
552 %************************************************************************
554 \subsection[lint-monad]{The Lint monad}
556 %************************************************************************
559 lintInTy :: InType -> LintM OutType
560 -- Check the type, and apply the substitution to it
561 -- See Note [Linting type lets]
562 -- ToDo: check the kind structure of the type
564 = addLoc (InType ty) $
565 do { ty' <- applySubst ty
570 lintKind :: Kind -> LintM ()
571 -- Check well-formedness of kinds: *, *->*, etc
572 lintKind (TyConApp tc [])
573 | getUnique tc `elem` kindKeys
575 lintKind (FunTy k1 k2)
576 = lintKind k1 >> lintKind k2
578 = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
581 lintTyBndrKind :: OutTyVar -> LintM ()
583 | isCoVar tv = lintCoVarKind tv
584 | otherwise = lintKind (tyVarKind tv)
587 lintCoVarKind :: OutCoVar -> LintM ()
588 -- Check the kind of a coercion binder
590 = do { (ty1,ty2) <- lintSplitCoVar tv
593 ; unless (k1 `eqKind` k2)
594 (addErrL (sep [ ptext (sLit "Kind mis-match in coercion kind of:")
595 , nest 2 (quotes (ppr tv))
599 lintSplitCoVar :: CoVar -> LintM (Type,Type)
601 = case coVarKind_maybe cv of
603 Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
604 , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
607 lintCoercion, lintCoercion' :: OutType -> LintM (OutType, OutType)
608 -- Check the kind of a coercion term, returning the kind
610 = addLoc (InCoercion co) $ lintCoercion' co
612 lintCoercion' ty@(TyVarTy tv)
613 = do { checkTyVarInScope tv
614 ; if isCoVar tv then return (coVarKind tv)
615 else return (ty, ty) }
617 lintCoercion' ty@(AppTy ty1 ty2)
618 = do { (s1,t1) <- lintCoercion ty1
619 ; (s2,t2) <- lintCoercion ty2
620 ; check_co_app ty (typeKind s1) [s2]
621 ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
623 lintCoercion' ty@(FunTy ty1 ty2)
624 = do { (s1,t1) <- lintCoercion ty1
625 ; (s2,t2) <- lintCoercion ty2
626 ; check_co_app ty (tyConKind funTyCon) [s1, s2]
627 ; return (FunTy s1 s2, FunTy t1 t2) }
629 lintCoercion' ty@(TyConApp tc tys)
630 | Just (ar, desc) <- isCoercionTyCon_maybe tc
631 = do { unless (tys `lengthAtLeast` ar) (badCo ty)
632 ; (s,t) <- lintCoTyConApp ty desc (take ar tys)
633 ; (ss,ts) <- mapAndUnzipM lintCoercion (drop ar tys)
634 ; check_co_app ty (typeKind s) ss
635 ; return (mkAppTys s ss, mkAppTys t ts) }
637 | not (tyConHasKind tc) -- Just something bizarre like SuperKindTyCon
641 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
642 ; check_co_app ty (tyConKind tc) ss
643 ; return (TyConApp tc ss, TyConApp tc ts) }
645 lintCoercion' ty@(PredTy (ClassP cls tys))
646 = do { (ss,ts) <- mapAndUnzipM lintCoercion tys
647 ; check_co_app ty (tyConKind (classTyCon cls)) ss
648 ; return (PredTy (ClassP cls ss), PredTy (ClassP cls ts)) }
650 lintCoercion' (PredTy (IParam n p_ty))
651 = do { (s,t) <- lintCoercion p_ty
652 ; return (PredTy (IParam n s), PredTy (IParam n t)) }
654 lintCoercion' ty@(PredTy (EqPred {}))
655 = failWithL (badEq ty)
657 lintCoercion' (ForAllTy tv ty)
659 = do { (co1, co2) <- lintSplitCoVar tv
660 ; (s1,t1) <- lintCoercion co1
661 ; (s2,t2) <- lintCoercion co2
662 ; (sr,tr) <- lintCoercion ty
663 ; return (mkCoPredTy s1 s2 sr, mkCoPredTy t1 t2 tr) }
666 = do { lintKind (tyVarKind tv)
667 ; (s,t) <- addInScopeVar tv (lintCoercion ty)
668 ; return (ForAllTy tv s, ForAllTy tv t) }
670 badCo :: Coercion -> LintM a
671 badCo co = failWithL (hang (ptext (sLit "Ill-kinded coercion term:")) 2 (ppr co))
674 lintCoTyConApp :: Coercion -> CoTyConDesc -> [Coercion] -> LintM (Type,Type)
675 -- Always called with correct number of coercion arguments
676 -- First arg is just for error message
677 lintCoTyConApp _ CoLeft (co:_) = lintLR fst co
678 lintCoTyConApp _ CoRight (co:_) = lintLR snd co
679 lintCoTyConApp _ CoCsel1 (co:_) = lintCsel fstOf3 co
680 lintCoTyConApp _ CoCsel2 (co:_) = lintCsel sndOf3 co
681 lintCoTyConApp _ CoCselR (co:_) = lintCsel thirdOf3 co
683 lintCoTyConApp _ CoSym (co:_)
684 = do { (ty1,ty2) <- lintCoercion co
687 lintCoTyConApp co CoTrans (co1:co2:_)
688 = do { (ty1a, ty1b) <- lintCoercion co1
689 ; (ty2a, ty2b) <- lintCoercion co2
690 ; checkL (ty1b `coreEqType` ty2a)
691 (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
692 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
693 ; return (ty1a, ty2b) }
695 lintCoTyConApp _ CoInst (co:arg_ty:_)
696 = do { co_tys <- lintCoercion co
697 ; arg_kind <- lintType arg_ty
698 ; case decompInst_maybe co_tys of
699 Just ((tv1,tv2), (ty1,ty2))
700 | arg_kind `isSubKind` tyVarKind tv1
701 -> return (substTyWith [tv1] [arg_ty] ty1,
702 substTyWith [tv2] [arg_ty] ty2)
704 -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
705 Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
707 lintCoTyConApp _ (CoAxiom { co_ax_tvs = tvs
708 , co_ax_lhs = lhs_ty, co_ax_rhs = rhs_ty }) cos
709 = do { (tys1, tys2) <- mapAndUnzipM lintCoercion cos
710 ; sequence_ (zipWith checkKinds tvs tys1)
711 ; return (substTyWith tvs tys1 lhs_ty,
712 substTyWith tvs tys2 rhs_ty) }
714 lintCoTyConApp _ CoUnsafe (ty1:ty2:_)
715 = do { _ <- lintType ty1
716 ; _ <- lintType ty2 -- Ignore kinds; it's unsafe!
719 lintCoTyConApp _ _ _ = panic "lintCoTyConApp" -- Called with wrong number of coercion args
722 lintLR :: (forall a. (a,a)->a) -> Coercion -> LintM (Type,Type)
724 = do { (ty1,ty2) <- lintCoercion co
725 ; case decompLR_maybe (ty1,ty2) of
726 Just res -> return (sel res)
727 Nothing -> failWithL (ptext (sLit "Bad argument of left/right")) }
730 lintCsel :: (forall a. (a,a,a)->a) -> Coercion -> LintM (Type,Type)
732 = do { (ty1,ty2) <- lintCoercion co
733 ; case decompCsel_maybe (ty1,ty2) of
734 Just res -> return (sel res)
735 Nothing -> failWithL (ptext (sLit "Bad argument of csel")) }
738 lintType :: OutType -> LintM Kind
739 lintType (TyVarTy tv)
740 = do { checkTyVarInScope tv
741 ; return (tyVarKind tv) }
743 lintType ty@(AppTy t1 t2)
744 = do { k1 <- lintType t1
745 ; lint_ty_app ty k1 [t2] }
747 lintType ty@(FunTy t1 t2)
748 = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
750 lintType ty@(TyConApp tc tys)
752 = lint_ty_app ty (tyConKind tc) tys
754 = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
756 lintType (ForAllTy tv ty)
757 = do { lintTyBndrKind tv
758 ; addInScopeVar tv (lintType ty) }
760 lintType ty@(PredTy (ClassP cls tys))
761 = lint_ty_app ty (tyConKind (classTyCon cls)) tys
763 lintType (PredTy (IParam _ p_ty))
766 lintType ty@(PredTy (EqPred {}))
767 = failWithL (badEq ty)
770 lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
772 = do { ks <- mapM lintType tys
773 ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
776 check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
777 check_co_app ty k tys
778 = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
783 lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
784 lint_kind_app doc kfn ks = go kfn ks
786 fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
787 nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
788 nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
790 go kfn [] = return kfn
791 go kfn (k:ks) = case splitKindFunTy_maybe kfn of
792 Nothing -> failWithL fail_msg
793 Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
797 badEq :: Type -> SDoc
798 badEq ty = hang (ptext (sLit "Unexpected equality predicate:"))
802 %************************************************************************
804 \subsection[lint-monad]{The Lint monad}
806 %************************************************************************
811 [LintLocInfo] -> -- Locations
812 TvSubst -> -- Current type substitution; we also use this
813 -- to keep track of all the variables in scope,
814 -- both Ids and TyVars
815 WarnsAndErrs -> -- Error and warning messages so far
816 (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
818 type WarnsAndErrs = (Bag Message, Bag Message)
820 {- Note [Type substitution]
821 ~~~~~~~~~~~~~~~~~~~~~~~~
822 Why do we need a type substitution? Consider
823 /\(a:*). \(x:a). /\(a:*). id a x
824 This is ill typed, because (renaming variables) it is really
825 /\(a:*). \(x:a). /\(b:*). id b x
826 Hence, when checking an application, we can't naively compare x's type
827 (at its binding site) with its expected type (at a use site). So we
828 rename type binders as we go, maintaining a substitution.
830 The same substitution also supports let-type, current expressed as
832 Here we substitute 'ty' for 'a' in 'body', on the fly.
835 instance Monad LintM where
836 return x = LintM (\ _ _ errs -> (Just x, errs))
837 fail err = failWithL (text err)
838 m >>= k = LintM (\ loc subst errs ->
839 let (res, errs') = unLintM m loc subst errs in
841 Just r -> unLintM (k r) loc subst errs'
842 Nothing -> (Nothing, errs'))
845 = RhsOf Id -- The variable bound
846 | LambdaBodyOf Id -- The lambda-binder
847 | BodyOfLetRec [Id] -- One of the binders
848 | CaseAlt CoreAlt -- Case alternative
849 | CasePat CoreAlt -- The *pattern* of the case alternative
850 | AnExpr CoreExpr -- Some expression
851 | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
853 | InType Type -- Inside a type
854 | InCoercion Coercion -- Inside a type
859 initL :: LintM a -> WarnsAndErrs -- Errors and warnings
861 = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
866 checkL :: Bool -> Message -> LintM ()
867 checkL True _ = return ()
868 checkL False msg = failWithL msg
870 failWithL :: Message -> LintM a
871 failWithL msg = LintM $ \ loc subst (warns,errs) ->
872 (Nothing, (warns, addMsg subst errs msg loc))
874 addErrL :: Message -> LintM ()
875 addErrL msg = LintM $ \ loc subst (warns,errs) ->
876 (Just (), (warns, addMsg subst errs msg loc))
878 addWarnL :: Message -> LintM ()
879 addWarnL msg = LintM $ \ loc subst (warns,errs) ->
880 (Just (), (addMsg subst warns msg loc, errs))
882 addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
883 addMsg subst msgs msg locs
884 = ASSERT( notNull locs )
885 msgs `snocBag` mk_msg msg
887 (loc, cxt1) = dumpLoc (head locs)
888 cxts = [snd (dumpLoc loc) | loc <- locs]
889 context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
890 ptext (sLit "Substitution:") <+> ppr subst
893 mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
895 addLoc :: LintLocInfo -> LintM a -> LintM a
897 LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
899 inCasePat :: LintM Bool -- A slight hack; see the unique call site
900 inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
902 is_case_pat (CasePat {} : _) = True
903 is_case_pat _other = False
905 addInScopeVars :: [Var] -> LintM a -> LintM a
906 addInScopeVars vars m
908 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
910 = failWithL (dupVars dups)
912 (_, dups) = removeDups compare vars
914 addInScopeVar :: Var -> LintM a -> LintM a
916 = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
918 updateTvSubst :: TvSubst -> LintM a -> LintM a
919 updateTvSubst subst' m =
920 LintM (\ loc _ errs -> unLintM m loc subst' errs)
922 getTvSubst :: LintM TvSubst
923 getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
925 applySubst :: Type -> LintM Type
926 applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
928 extendSubstL :: TyVar -> Type -> LintM a -> LintM a
930 = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
934 lookupIdInScope :: Id -> LintM Id
936 | not (mustHaveLocalBinding id)
937 = return id -- An imported Id
939 = do { subst <- getTvSubst
940 ; case lookupInScope (getTvInScope subst) id of
942 Nothing -> do { addErrL out_of_scope
945 out_of_scope = ppr id <+> ptext (sLit "is out of scope")
948 oneTupleDataConId :: Id -- Should not happen
949 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
951 checkBndrIdInScope :: Var -> Var -> LintM ()
952 checkBndrIdInScope binder id
953 = checkInScope msg id
955 msg = ptext (sLit "is out of scope inside info for") <+>
958 checkTyVarInScope :: TyVar -> LintM ()
959 checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
961 checkInScope :: SDoc -> Var -> LintM ()
962 checkInScope loc_msg var =
963 do { subst <- getTvSubst
964 ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
965 (hsep [ppr var, loc_msg]) }
967 checkTys :: OutType -> OutType -> Message -> LintM ()
968 -- check ty2 is subtype of ty1 (ie, has same structure but usage
969 -- annotations need only be consistent, not equal)
970 -- Assumes ty1,ty2 are have alrady had the substitution applied
971 checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
974 %************************************************************************
976 \subsection{Error messages}
978 %************************************************************************
981 dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
984 = (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
986 dumpLoc (LambdaBodyOf b)
987 = (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
989 dumpLoc (BodyOfLetRec [])
990 = (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
992 dumpLoc (BodyOfLetRec bs@(_:_))
993 = ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
996 = (noSrcLoc, text "In the expression:" <+> ppr e)
998 dumpLoc (CaseAlt (con, args, _))
999 = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
1001 dumpLoc (CasePat (con, args, _))
1002 = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
1004 dumpLoc (ImportedUnfolding locn)
1005 = (locn, brackets (ptext (sLit "in an imported unfolding")))
1006 dumpLoc TopLevelBindings
1009 = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
1010 dumpLoc (InCoercion ty)
1011 = (noSrcLoc, text "In the coercion" <+> quotes (ppr ty))
1013 pp_binders :: [Var] -> SDoc
1014 pp_binders bs = sep (punctuate comma (map pp_binder bs))
1016 pp_binder :: Var -> SDoc
1017 pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
1018 | otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
1022 ------------------------------------------------------
1023 -- Messages for case expressions
1025 mkNullAltsMsg :: CoreExpr -> Message
1027 = hang (text "Case expression with no alternatives:")
1030 mkDefaultArgsMsg :: [Var] -> Message
1031 mkDefaultArgsMsg args
1032 = hang (text "DEFAULT case with binders")
1035 mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
1036 mkCaseAltMsg e ty1 ty2
1037 = hang (text "Type of case alternatives not the same as the annotation on case:")
1038 4 (vcat [ppr ty1, ppr ty2, ppr e])
1040 mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
1041 mkScrutMsg var var_ty scrut_ty subst
1042 = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
1043 text "Result binder type:" <+> ppr var_ty,--(idType var),
1044 text "Scrutinee type:" <+> ppr scrut_ty,
1045 hsep [ptext (sLit "Current TV subst"), ppr subst]]
1047 mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> Message
1049 = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
1050 mkNonIncreasingAltsMsg e
1051 = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
1053 nonExhaustiveAltsMsg :: CoreExpr -> Message
1054 nonExhaustiveAltsMsg e
1055 = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
1057 mkBadConMsg :: TyCon -> DataCon -> Message
1058 mkBadConMsg tycon datacon
1060 text "In a case alternative, data constructor isn't in scrutinee type:",
1061 text "Scrutinee type constructor:" <+> ppr tycon,
1062 text "Data con:" <+> ppr datacon
1065 mkBadPatMsg :: Type -> Type -> Message
1066 mkBadPatMsg con_result_ty scrut_ty
1068 text "In a case alternative, pattern result type doesn't match scrutinee type:",
1069 text "Pattern result type:" <+> ppr con_result_ty,
1070 text "Scrutinee type:" <+> ppr scrut_ty
1073 mkBadAltMsg :: Type -> CoreAlt -> Message
1074 mkBadAltMsg scrut_ty alt
1075 = vcat [ text "Data alternative when scrutinee is not a tycon application",
1076 text "Scrutinee type:" <+> ppr scrut_ty,
1077 text "Alternative:" <+> pprCoreAlt alt ]
1079 mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
1080 mkNewTyDataConAltMsg scrut_ty alt
1081 = vcat [ text "Data alternative for newtype datacon",
1082 text "Scrutinee type:" <+> ppr scrut_ty,
1083 text "Alternative:" <+> pprCoreAlt alt ]
1086 ------------------------------------------------------
1087 -- Other error messages
1089 mkAppMsg :: Type -> Type -> CoreExpr -> Message
1090 mkAppMsg fun_ty arg_ty arg
1091 = vcat [ptext (sLit "Argument value doesn't match argument type:"),
1092 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1093 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1094 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1096 mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
1097 mkNonFunAppMsg fun_ty arg_ty arg
1098 = vcat [ptext (sLit "Non-function type in function position"),
1099 hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
1100 hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
1101 hang (ptext (sLit "Arg:")) 4 (ppr arg)]
1103 mkTyVarLetErr :: TyVar -> Type -> Message
1104 mkTyVarLetErr tyvar ty
1105 = vcat [ptext (sLit "Bad `let' binding for type or coercion variable:"),
1106 hang (ptext (sLit "Type/coercion variable:"))
1107 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1108 hang (ptext (sLit "Arg type/coercion:"))
1111 mkKindErrMsg :: TyVar -> Type -> Message
1112 mkKindErrMsg tyvar arg_ty
1113 = vcat [ptext (sLit "Kinds don't match in type application:"),
1114 hang (ptext (sLit "Type variable:"))
1115 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1116 hang (ptext (sLit "Arg type:"))
1117 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1119 mkCoAppErrMsg :: TyVar -> Type -> Message
1120 mkCoAppErrMsg tyvar arg_ty
1121 = vcat [ptext (sLit "Kinds don't match in coercion application:"),
1122 hang (ptext (sLit "Coercion variable:"))
1123 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
1124 hang (ptext (sLit "Arg coercion:"))
1125 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
1127 mkTyAppMsg :: Type -> Type -> Message
1128 mkTyAppMsg ty arg_ty
1129 = vcat [text "Illegal type application:",
1130 hang (ptext (sLit "Exp type:"))
1131 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
1132 hang (ptext (sLit "Arg type:"))
1133 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
1135 mkRhsMsg :: Id -> Type -> Message
1138 [hsep [ptext (sLit "The type of this binder doesn't match the type of its RHS:"),
1140 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
1141 hsep [ptext (sLit "Rhs type:"), ppr ty]]
1143 mkRhsPrimMsg :: Id -> CoreExpr -> Message
1144 mkRhsPrimMsg binder _rhs
1145 = vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
1147 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
1150 mkStrictMsg :: Id -> Message
1152 = vcat [hsep [ptext (sLit "Recursive or top-level binder has strict demand info:"),
1154 hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
1157 mkArityMsg :: Id -> Message
1159 = vcat [hsep [ptext (sLit "Demand type has "),
1160 ppr (dmdTypeDepth dmd_ty),
1161 ptext (sLit " arguments, rhs has "),
1162 ppr (idArity binder),
1163 ptext (sLit "arguments, "),
1165 hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
1168 where (StrictSig dmd_ty) = idStrictness binder
1170 mkUnboxedTupleMsg :: Id -> Message
1171 mkUnboxedTupleMsg binder
1172 = vcat [hsep [ptext (sLit "A variable has unboxed tuple type:"), ppr binder],
1173 hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]]
1175 mkCastErr :: Type -> Type -> Message
1176 mkCastErr from_ty expr_ty
1177 = vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
1178 ptext (sLit "From-type:") <+> ppr from_ty,
1179 ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty
1182 dupVars :: [[Var]] -> Message
1184 = hang (ptext (sLit "Duplicate variables brought into scope"))