%
+% (c) The University of Glasgow 2006
% (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
%
-\section[CoreLint]{A ``lint'' pass to check for Core correctness}
+
+A ``lint'' pass to check for Core correctness
\begin{code}
+{-# OPTIONS -w #-}
+-- The above warning supression flag is a temporary kludge.
+-- While working on this module you are encouraged to remove it and fix
+-- any warnings in the module. See
+-- http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
+-- for details
+
module CoreLint (
lintCoreBindings,
lintUnfolding,
#include "HsVersions.h"
+import NewDemand
import CoreSyn
-import CoreFVs ( idFreeVars )
-import CoreUtils ( findDefault, exprOkForSpeculation, coreBindsSize )
+import CoreFVs
+import CoreUtils
import Bag
-import Literal ( literalType )
-import DataCon ( dataConRepType, dataConTyCon, dataConWorkId )
-import TysWiredIn ( tupleCon )
-import Var ( Var, Id, TyVar, isCoVar, idType, tyVarKind,
- mustHaveLocalBinding, setTyVarKind, setIdType )
-import VarEnv ( lookupInScope )
+import Literal
+import DataCon
+import TysWiredIn
+import Var
+import VarEnv
import VarSet
-import Name ( getSrcLoc )
+import Name
+import Id
import PprCore
-import ErrUtils ( dumpIfSet_core, ghcExit, Message, showPass,
- mkLocMessage, debugTraceMsg )
-import SrcLoc ( SrcLoc, noSrcLoc, mkSrcSpan )
-import Type ( Type, tyVarsOfType, coreEqType,
- splitFunTy_maybe, mkTyVarTys,
- splitForAllTy_maybe, splitTyConApp_maybe,
- isUnLiftedType, typeKind, mkForAllTy, mkFunTy,
- isUnboxedTupleType, isSubKind,
- substTyWith, emptyTvSubst, extendTvInScope,
- TvSubst, TvSubstEnv, mkTvSubst, setTvSubstEnv, substTy,
- extendTvSubst, composeTvSubst, substTyVarBndr, isInScope,
- getTvSubstEnv, getTvInScope, mkTyVarTy )
-import Coercion ( Coercion, coercionKind, coercionKindPredTy )
-import TyCon ( isPrimTyCon, isNewTyCon )
-import BasicTypes ( RecFlag(..), Boxity(..), isNonRec )
-import StaticFlags ( opt_PprStyle_Debug )
-import DynFlags ( DynFlags, DynFlag(..), dopt )
+import ErrUtils
+import SrcLoc
+import Type
+import Coercion
+import TyCon
+import BasicTypes
+import StaticFlags
+import DynFlags
import Outputable
-
-#ifdef DEBUG
-import Util ( notNull )
-#endif
-
-import Maybe
-
+import Util
+import Data.Maybe
\end{code}
%************************************************************************
lint_binds binds = addInScopeVars (bindersOfBinds binds) $
mapM lint_bind binds
- lint_bind (Rec prs) = mapM_ (lintSingleBinding Recursive) prs
- lint_bind (NonRec bndr rhs) = lintSingleBinding NonRecursive (bndr,rhs)
+ 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 ++ " ***"),
Check a core binding, returning the list of variables bound.
\begin{code}
-lintSingleBinding rec_flag (binder,rhs)
+lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
= addLoc (RhsOf binder) $
-- Check the rhs
do { ty <- lintCoreExpr rhs
; checkL (not (isUnLiftedType binder_ty)
|| (isNonRec rec_flag && exprOkForSpeculation rhs))
(mkRhsPrimMsg binder rhs)
+ -- Check that if the binder is top-level or recursive, it's not demanded
+ ; checkL (not (isStrictId binder)
+ || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
+ (mkStrictMsg binder)
-- Check whether binder's specialisations contain any out-of-scope variables
- ; mapM_ (checkBndrIdInScope binder) bndr_vars }
+ ; mapM_ (checkBndrIdInScope binder) bndr_vars
+
+ -- Check whether arity and demand type are consistent (only if demand analysis
+ -- already happened)
+ ; checkL (case maybeDmdTy of
+ Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
+ Nothing -> True)
+ (mkArityMsg binder) }
-- We should check the unfolding, if any, but this is tricky because
- -- the unfolding is a SimplifiableCoreExpr. Give up for now.
- where
- binder_ty = idType binder
- bndr_vars = varSetElems (idFreeVars binder)
+ -- the unfolding is a SimplifiableCoreExpr. Give up for now.
+ where
+ binder_ty = idType binder
+ maybeDmdTy = idNewStrictness_maybe binder
+ bndr_vars = varSetElems (idFreeVars binder)
lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
| otherwise = return ()
\end{code}
= lintCoreExpr expr
lintCoreExpr (Let (NonRec bndr rhs) body)
- = do { lintSingleBinding NonRecursive (bndr,rhs)
+ = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
; addLoc (BodyOfLetRec [bndr])
(lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
lintCoreExpr (Let (Rec pairs) body)
= lintAndScopeIds bndrs $ \_ ->
- do { mapM (lintSingleBinding Recursive) pairs
+ do { mapM (lintSingleBinding NotTopLevel Recursive) pairs
; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
where
bndrs = map fst pairs
else lintAndScopeId var
; scope $ \_ ->
do { -- Check the alternatives
- checkCaseAlts e scrut_ty alts
- ; 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
subtype of the required type, as one would expect.
\begin{code}
-lintCoreArgs :: Type -> [CoreArg] -> LintM Type
-lintCoreArg :: Type -> CoreArg -> LintM Type
+lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
+lintCoreArg :: OutType -> CoreArg -> LintM OutType
-- First argument has already had substitution applied to it
\end{code}
\begin{code}
-- Both args have had substitution applied
+lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp ty arg_ty
= case splitForAllTy_maybe ty of
Nothing -> addErrL (mkTyAppMsg ty arg_ty)
; checkKinds tyvar arg_ty
; return (substTyWith [tyvar] [arg_ty] body) }
-lintTyApps fun_ty [] = return fun_ty
-
-lintTyApps fun_ty (arg_ty : arg_tys) =
- do { fun_ty' <- lintTyApp fun_ty arg_ty
- ; lintTyApps fun_ty' arg_tys }
-
checkKinds tyvar arg_ty
-- Arg type might be boxed for a function with an uncommitted
-- tyvar; notably this is used so that we can give
lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
| isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
| Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
- = lintBinders args $ \ args ->
-
- do { addLoc (CasePat alt) $ do
- { -- Check the pattern
+ = addLoc (CaseAlt alt) $ do
+ { -- First instantiate the universally quantified
+ -- type variables of the data constructor
+ -- We've already check
+ checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
+ ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
+
+ -- And now bring the new binders into scope
+ ; lintBinders args $ \ args -> do
+ { addLoc (CasePat alt) $ do
+ { -- Check the pattern
-- Scrutinee type must be a tycon applicn; checked by caller
-- This code is remarkably compact considering what it does!
-- NB: args must be in scope here so that the lintCoreArgs line works.
-- NB: relies on existential type args coming *after* ordinary type args
- ; con_result_ty <- lintCoreArgs (dataConRepType con)
- (map Type tycon_arg_tys ++ varsToCoreExprs args)
+ ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
}
-- Check the RHS
- ; checkAltExpr rhs alt_ty }
+ ; checkAltExpr rhs alt_ty } }
| otherwise -- Scrut-ty is wrong shape
= addErrL (mkBadAltMsg scrut_ty alt)
lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
lintAndScopeId id linterF
= do { ty <- lintTy (idType id)
- ; let id' = setIdType id ty
+ ; let id' = Var.setIdType id ty
; addInScopeVars [id'] $ (linterF id')
}
Bag Message -> -- Error messages so far
(Maybe a, Bag Message) } -- Result and error messages (if any)
+{- Note [Type substitution]
+ ~~~~~~~~~~~~~~~~~~~~~~~~
+Why do we need a type substitution? Consider
+ /\(a:*). \(x:a). /\(a:*). id a x
+This is ill typed, because (renaming variables) it is really
+ /\(a:*). \(x:a). /\(b:*). id b x
+Hence, when checking an application, we can't naively compare x's type
+(at its binding site) with its expected type (at a use site). So we
+rename type binders as we go, maintaining a substitution.
+
+The same substitution also supports let-type, current expressed as
+ (/\(a:*). body) ty
+Here we substitute 'ty' for 'a' in 'body', on the fly.
+-}
+
instance Monad LintM where
return x = LintM (\ loc subst errs -> (Just x, errs))
fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
text "Scrutinee type:" <+> ppr scrut_ty,
hsep [ptext SLIT("Current TV subst"), ppr subst]]
-
mkNonDefltMsg e
= hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
mkNonIncreasingAltsMsg e
nonExhaustiveAltsMsg e
= hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
+mkBadConMsg :: TyCon -> DataCon -> Message
+mkBadConMsg tycon datacon
+ = vcat [
+ text "In a case alternative, data constructor isn't in scrutinee type:",
+ text "Scrutinee type constructor:" <+> ppr tycon,
+ text "Data con:" <+> ppr datacon
+ ]
+
mkBadPatMsg :: Type -> Type -> Message
mkBadPatMsg con_result_ty scrut_ty
= vcat [
hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
]
+mkStrictMsg :: Id -> Message
+mkStrictMsg binder
+ = vcat [hsep [ptext SLIT("Recursive or top-level binder has strict demand info:"),
+ ppr binder],
+ hsep [ptext SLIT("Binder's demand info:"), ppr (idNewDemandInfo binder)]
+ ]
+
+mkArityMsg :: Id -> Message
+mkArityMsg binder
+ = vcat [hsep [ptext SLIT("Demand type has "),
+ ppr (dmdTypeDepth dmd_ty),
+ ptext SLIT(" arguments, rhs has "),
+ ppr (idArity binder),
+ ptext SLIT("arguments, "),
+ ppr binder],
+ hsep [ptext SLIT("Binder's strictness signature:"), ppr dmd_ty]
+
+ ]
+ where (StrictSig dmd_ty) = idNewStrictness binder
+
mkUnboxedTupleMsg :: Id -> Message
mkUnboxedTupleMsg binder
= vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],