A ``lint'' pass to check for Core correctness
\begin{code}
-module CoreLint (
- lintCoreBindings,
- lintUnfolding,
- showPass, endPass, endPassIf, endIteration
- ) where
+module CoreLint ( lintCoreBindings, lintUnfolding ) where
#include "HsVersions.h"
import Outputable
import FastString
import Util
+import Control.Monad
import Data.Maybe
\end{code}
%************************************************************************
%* *
-\subsection{End pass}
-%* *
-%************************************************************************
-
-@showPass@ and @endPass@ don't really belong here, but it makes a convenient
-place for them. They print out stuff before and after core passes,
-and do Core Lint when necessary.
-
-\begin{code}
-endPass :: DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
-endPass = dumpAndLint dumpIfSet_core
-
-endPassIf :: Bool -> DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
-endPassIf cond = dumpAndLint (dumpIf_core cond)
-
-endIteration :: DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
-endIteration = dumpAndLint dumpIfSet_dyn
-
-dumpAndLint :: (DynFlags -> DynFlag -> String -> SDoc -> IO ())
- -> DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
-dumpAndLint dump dflags pass_name dump_flag binds
- = do
- -- Report result size if required
- -- This has the side effect of forcing the intermediate to be evaluated
- debugTraceMsg dflags 2 $
- (text " Result size =" <+> int (coreBindsSize binds))
-
- -- Report verbosely, if required
- dump dflags dump_flag pass_name (pprCoreBindings binds)
-
- -- Type check
- lintCoreBindings dflags pass_name binds
-
- return binds
-\end{code}
-
-
-%************************************************************************
-%* *
\subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
%* *
%************************************************************************
-- may well be happening...);
-Note [Type lets]
-~~~~~~~~~~~~~~~~
+Note [Linting type lets]
+~~~~~~~~~~~~~~~~~~~~~~~~
In the desugarer, it's very very convenient to be able to say (in effect)
- let a = Int in <body>
-That is, use a type let. (See notes just below for why we want this.)
-
-We don't have type lets in Core, so the desugarer uses type lambda
- (/\a. <body>) Int
-However, in the lambda form, we'd get lint errors from:
- (/\a. let x::a = 4 in <body>) Int
-because (x::a) doesn't look compatible with (4::Int).
-
-So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
-as it were. It carries a type substitution (in this example [a -> Int])
-and applies this substitution before comparing types. The functin
+ let a = Type Int in <body>
+That is, use a type let. See Note [Type let] in CoreSyn.
+
+However, when linting <body> we need to remember that a=Int, else we might
+reject a correct program. So we carry a type substitution (in this example
+[a -> Int]) and apply this substitution before comparing types. The functin
lintTy :: Type -> LintM Type
returns a substituted type; that's the only reason it returns anything.
find an occurence of an Id, we fetch it from the in-scope set.
-Why we need type let
-~~~~~~~~~~~~~~~~~~~~
-It's needed when dealing with desugarer output for GADTs. Consider
- data T = forall a. T a (a->Int) Bool
- f :: T -> ... ->
- f (T x f True) = <e1>
- f (T y g False) = <e2>
-After desugaring we get
- f t b = case t of
- T a (x::a) (f::a->Int) (b:Bool) ->
- case b of
- True -> <e1>
- False -> (/\b. let y=x; g=f in <e2>) a
-And for a reason I now forget, the ...<e2>... can mention a; so
-we want Lint to know that b=a. Ugh.
-
-I tried quite hard to make the necessity for this go away, by changing the
-desugarer, but the fundamental problem is this:
-
- T a (x::a) (y::Int) -> let fail::a = ...
- in (/\b. ...(case ... of
- True -> x::b
- False -> fail)
- ) a
-Now the inner case look as though it has incompatible branches.
-
-
\begin{code}
lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
= return ()
lintCoreBindings dflags whoDunnit binds
- = case (initL (lint_binds binds)) of
- Nothing -> showPass dflags ("Core Linted result of " ++ whoDunnit)
- Just bad_news -> printDump (display bad_news) >>
- ghcExit dflags 1
+ | isEmptyBag errs
+ = do { showPass dflags ("Core Linted result of " ++ whoDunnit)
+ ; unless (isEmptyBag warns) $ printDump $
+ (banner "warnings" $$ displayMessageBag warns)
+ ; return () }
+
+ | otherwise
+ = do { printDump (vcat [ banner "errors", displayMessageBag errs
+ , ptext (sLit "*** Offending Program ***")
+ , pprCoreBindings binds
+ , ptext (sLit "*** End of Offense ***") ])
+
+ ; ghcExit dflags 1 }
where
+ (warns, errs) = initL (lint_binds binds)
+
-- Put all the top-level binders in scope at the start
-- This is because transformation rules can bring something
-- into use 'unexpectedly'
lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
- display bad_news
- = vcat [ text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
- bad_news,
- ptext (sLit "*** Offending Program ***"),
- pprCoreBindings binds,
- ptext (sLit "*** End of Offense ***")
- ]
+ banner string = ptext (sLit "*** Core Lint") <+> text string
+ <+> ptext (sLit ": in result of") <+> text whoDunnit
+ <+> ptext (sLit "***")
+
+displayMessageBag :: Bag Message -> SDoc
+displayMessageBag msgs = vcat (punctuate blankLine (bagToList msgs))
\end{code}
%************************************************************************
-> Maybe Message -- Nothing => OK
lintUnfolding locn vars expr
- = initL (addLoc (ImportedUnfolding locn) $
- addInScopeVars vars $
- lintCoreExpr expr)
+ | isEmptyBag errs = Nothing
+ | otherwise = Just (displayMessageBag errs)
+ where
+ (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
+ addInScopeVars vars $
+ lintCoreExpr expr)
\end{code}
%************************************************************************
-- Check whether binder's specialisations contain any out-of-scope variables
; mapM_ (checkBndrIdInScope binder) bndr_vars
+ ; when (isLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
+ (addWarnL (ptext (sLit "INLINE binder is loop breaker:") <+> ppr binder))
+
-- Check whether arity and demand type are consistent (only if demand analysis
-- already happened)
; checkL (case maybeDmdTy of
-- The returned type has the substitution from the monad
-- already applied to it:
-- lintCoreExpr e subst = exprType (subst e)
+--
+-- The returned "type" can be a kind, if the expression is (Type ty)
lintCoreExpr (Var var)
= do { checkL (not (var == oneTupleDataConId))
(ptext (sLit "Illegal one-tuple"))
+
+ ; checkDeadIdOcc var
; var' <- lookupIdInScope var
; return (idType var')
}
lintCoreExpr (Note _ expr)
= lintCoreExpr expr
+lintCoreExpr (Let (NonRec tv (Type ty)) body)
+ = -- See Note [Type let] in CoreSyn
+ do { checkL (isTyVar tv) (mkKindErrMsg tv ty) -- Not quite accurate
+ ; ty' <- lintTy ty
+ ; kind' <- lintTy (tyVarKind tv)
+ ; let tv' = setTyVarKind tv kind'
+ ; checkKinds tv' ty'
+ -- Now extend the substitution so we
+ -- take advantage of it in the body
+ ; addLoc (BodyOfLetRec [tv]) $
+ addInScopeVars [tv'] $
+ extendSubstL tv' ty' $
+ lintCoreExpr body }
+
lintCoreExpr (Let (NonRec bndr rhs) body)
= do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
; addLoc (BodyOfLetRec [bndr])
lintCoreExpr (Let (Rec pairs) body)
= lintAndScopeIds bndrs $ \_ ->
- do { mapM (lintSingleBinding NotTopLevel Recursive) pairs
+ do { mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
where
bndrs = map fst pairs
-lintCoreExpr e@(App fun (Type ty))
--- See Note [Type let] above
- = addLoc (AnExpr e) $
- go fun [ty]
- where
- go (App fun (Type ty)) tys
- = do { go fun (ty:tys) }
- go (Lam tv body) (ty:tys)
- = do { checkL (isTyVar tv) (mkKindErrMsg tv ty) -- Not quite accurate
- ; ty' <- lintTy ty
- ; let kind = tyVarKind tv
- ; kind' <- lintTy kind
- ; let tv' = setTyVarKind tv kind'
- ; checkKinds tv' ty'
- -- Now extend the substitution so we
- -- take advantage of it in the body
- ; addInScopeVars [tv'] $
- extendSubstL tv' ty' $
- go body tys }
- go fun tys
- = do { fun_ty <- lintCoreExpr fun
- ; lintCoreArgs fun_ty (map Type tys) }
-
lintCoreExpr e@(App fun arg)
= do { fun_ty <- lintCoreExpr fun
; addLoc (AnExpr e) $
Just (tycon, _)
| debugIsOn &&
isAlgTyCon tycon &&
+ not (isOpenTyCon tycon) &&
null (tyConDataCons tycon) ->
- pprTrace "case binder's type has no constructors" (ppr e)
+ pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
+ -- This can legitimately happen for type families
$ return ()
_otherwise -> return ()
else lintAndScopeId var
; scope $ \_ ->
do { -- Check the alternatives
- mapM (lintCoreAlt scrut_ty alt_ty) alts
+ mapM_ (lintCoreAlt scrut_ty alt_ty) alts
; checkCaseAlts e scrut_ty alts
; return alt_ty } }
where
pass_var f = f var
-lintCoreExpr e@(Type _)
- = addErrL (mkStrangeTyMsg e)
+lintCoreExpr (Type ty)
+ = do { ty' <- lintTy ty
+ ; return (typeKind ty') }
\end{code}
%************************************************************************
Just (arg,res) ->
do { checkTys arg arg_ty err1
; return res }
- _ -> addErrL err2 }
+ _ -> failWithL err2 }
\end{code}
\begin{code}
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp ty arg_ty
= case splitForAllTy_maybe ty of
- Nothing -> addErrL (mkTyAppMsg ty arg_ty)
+ Nothing -> failWithL (mkTyAppMsg ty arg_ty)
Just (tyvar,body)
-> do { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
-- tyvar; notably this is used so that we can give
-- error :: forall a:*. String -> a
-- and then apply it to both boxed and unboxed types.
- = checkL (arg_kind `isSubKind` tyvar_kind)
- (mkKindErrMsg tyvar arg_ty)
+ | isCoVar tyvar = unless (s1 `coreEqType` s2 && t1 `coreEqType` t2)
+ (addErrL (mkCoAppErrMsg tyvar arg_ty))
+ | otherwise = unless (arg_kind `isSubKind` tyvar_kind)
+ (addErrL (mkKindErrMsg tyvar arg_ty))
where
tyvar_kind = tyVarKind tyvar
- arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
- | otherwise = typeKind arg_ty
+ arg_kind = typeKind arg_ty
+ (s1,t1) = coVarKind tyvar
+ (s2,t2) = coercionKind arg_ty
+
+checkDeadIdOcc :: Id -> LintM ()
+-- Occurrences of an Id should never be dead....
+-- except when we are checking a case pattern
+checkDeadIdOcc id
+ | isDeadOcc (idOccInfo id)
+ = do { in_case <- inCasePat
+ ; checkL in_case
+ (ptext (sLit "Occurrence of a dead Id") <+> ppr id) }
+ | otherwise
+ = return ()
\end{code}
| isTyVar var = lint_ty_bndr
| otherwise = lintIdBndr var linterF
where
- lint_ty_bndr = do { lintTy (tyVarKind var)
+ lint_ty_bndr = do { _ <- lintTy (tyVarKind var)
; subst <- getTvSubst
; let (subst', tv') = substTyVarBndr subst var
; updateTvSubst subst' (linterF tv') }
lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
lintAndScopeId id linterF
= do { ty <- lintTy (idType id)
- ; let id' = Var.setIdType id ty
+ ; let id' = setIdType id ty
; addInScopeVars [id'] $ (linterF id')
}
lintTy :: InType -> LintM OutType
-- Check the type, and apply the substitution to it
+-- See Note [Linting type lets]
-- ToDo: check the kind structure of the type
lintTy ty
= do { ty' <- applySubst ty
TvSubst -> -- Current type substitution; we also use this
-- to keep track of all the variables in scope,
-- both Ids and TyVars
- Bag Message -> -- Error messages so far
- (Maybe a, Bag Message) } -- Result and error messages (if any)
+ WarnsAndErrs -> -- Error and warning messages so far
+ (Maybe a, WarnsAndErrs) } -- Result and messages (if any)
+
+type WarnsAndErrs = (Bag Message, Bag Message)
{- Note [Type substitution]
~~~~~~~~~~~~~~~~~~~~~~~~
instance Monad LintM where
return x = LintM (\ _ _ errs -> (Just x, errs))
- fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
+ fail err = failWithL (text err)
m >>= k = LintM (\ loc subst errs ->
let (res, errs') = unLintM m loc subst errs in
case res of
| LambdaBodyOf Id -- The lambda-binder
| BodyOfLetRec [Id] -- One of the binders
| CaseAlt CoreAlt -- Case alternative
- | CasePat CoreAlt -- *Pattern* of the case alternative
+ | CasePat CoreAlt -- The *pattern* of the case alternative
| AnExpr CoreExpr -- Some expression
| ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
| TopLevelBindings
\begin{code}
-initL :: LintM a -> Maybe Message {- errors -}
+initL :: LintM a -> WarnsAndErrs -- Errors and warnings
initL m
- = case unLintM m [] emptyTvSubst emptyBag of
- (_, errs) | isEmptyBag errs -> Nothing
- | otherwise -> Just (vcat (punctuate (text "") (bagToList errs)))
+ = case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
+ (_, errs) -> errs
\end{code}
\begin{code}
checkL :: Bool -> Message -> LintM ()
checkL True _ = return ()
-checkL False msg = addErrL msg
+checkL False msg = failWithL msg
+
+failWithL :: Message -> LintM a
+failWithL msg = LintM $ \ loc subst (warns,errs) ->
+ (Nothing, (warns, addMsg subst errs msg loc))
+
+addErrL :: Message -> LintM ()
+addErrL msg = LintM $ \ loc subst (warns,errs) ->
+ (Just (), (warns, addMsg subst errs msg loc))
-addErrL :: Message -> LintM a
-addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
+addWarnL :: Message -> LintM ()
+addWarnL msg = LintM $ \ loc subst (warns,errs) ->
+ (Just (), (addMsg subst warns msg loc, errs))
-addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
-addErr subst errs_so_far msg locs
+addMsg :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
+addMsg subst msgs msg locs
= ASSERT( notNull locs )
- errs_so_far `snocBag` mk_msg msg
+ msgs `snocBag` mk_msg msg
where
(loc, cxt1) = dumpLoc (head locs)
cxts = [snd (dumpLoc loc) | loc <- locs]
addLoc extra_loc m =
LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
+inCasePat :: LintM Bool -- A slight hack; see the unique call site
+inCasePat = LintM $ \ loc _ errs -> (Just (is_case_pat loc), errs)
+ where
+ is_case_pat (CasePat {} : _) = True
+ is_case_pat _other = False
+
addInScopeVars :: [Var] -> LintM a -> LintM a
addInScopeVars vars m
| null dups
= LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
| otherwise
- = addErrL (dupVars dups)
+ = failWithL (dupVars dups)
where
(_, dups) = removeDups compare vars
hang (ptext (sLit "Arg type:"))
4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
+mkCoAppErrMsg :: TyVar -> Type -> Message
+mkCoAppErrMsg tyvar arg_ty
+ = vcat [ptext (sLit "Kinds don't match in coercion application:"),
+ hang (ptext (sLit "Coercion variable:"))
+ 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
+ hang (ptext (sLit "Arg coercion:"))
+ 4 (ppr arg_ty <+> dcolon <+> pprEqPred (coercionKind arg_ty))]
+
mkTyAppMsg :: Type -> Type -> Message
mkTyAppMsg ty arg_ty
= vcat [text "Illegal type application:",
dupVars vars
= hang (ptext (sLit "Duplicate variables brought into scope"))
2 (ppr vars)
-
-mkStrangeTyMsg :: CoreExpr -> Message
-mkStrangeTyMsg e
- = ptext (sLit "Type where expression expected:") <+> ppr e
\end{code}
projects / ghc-hetmet.git / blobdiff