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 NewDemand
+import Demand
import CoreSyn
import CoreFVs
import CoreUtils
+import Pair
import Bag
import Literal
import DataCon
import VarSet
import Name
import Id
-import IdInfo
import PprCore
import ErrUtils
import SrcLoc
+import Kind
import Type
+import TypeRep
import Coercion
import TyCon
+import Class
import BasicTypes
import StaticFlags
import ListSetOps
-import DynFlags
+import PrelNames
import Outputable
import FastString
import Util
+import Control.Monad
import Data.Maybe
+import Data.Traversable (traverse)
\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}
%* *
%************************************************************************
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
+ lintInTy :: Type -> LintM Type
returns a substituted type; that's the only reason it returns anything.
When we encounter a binder (like x::a) we must apply the substitution
\begin{code}
-lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
-
-lintCoreBindings dflags _whoDunnit _binds
- | not (dopt Opt_DoCoreLinting dflags)
- = 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
- where
+lintCoreBindings :: [CoreBind] -> (Bag Message, Bag Message)
+-- Returns (warnings, errors)
+lintCoreBindings binds
+ = initL $
+ addLoc TopLevelBindings $
+ addInScopeVars binders $
-- Put all the top-level binders in scope at the start
-- This is because transformation rules can bring something
-- into use 'unexpectedly'
- lint_binds binds = addLoc TopLevelBindings $
- addInScopeVars (bindersOfBinds binds) $
- mapM lint_bind binds
+ do { checkL (null dups) (dupVars dups)
+ ; checkL (null ext_dups) (dupExtVars ext_dups)
+ ; mapM lint_bind binds }
+ where
+ binders = bindersOfBinds binds
+ (_, dups) = removeDups compare binders
+
+ -- dups_ext checks for names with different uniques
+ -- but but the same External name M.n. We don't
+ -- allow this at top level:
+ -- M.n{r3} = ...
+ -- M.n{r29} = ...
+ -- becuase they both get the same linker symbol
+ ext_dups = snd (removeDups ord_ext (map Var.varName binders))
+ ord_ext n1 n2 | Just m1 <- nameModule_maybe n1
+ , Just m2 <- nameModule_maybe n2
+ = compare (m1, nameOccName n1) (m2, nameOccName n2)
+ | otherwise = LT
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 ***")
- ]
\end{code}
%************************************************************************
-> Maybe Message -- Nothing => OK
lintUnfolding locn vars expr
- = initL (addLoc (ImportedUnfolding locn) $
- addInScopeVars vars $
- lintCoreExpr expr)
+ | isEmptyBag errs = Nothing
+ | otherwise = Just (pprMessageBag errs)
+ where
+ (_warns, errs) = initL (addLoc (ImportedUnfolding locn) $
+ addInScopeVars vars $
+ lintCoreExpr expr)
\end{code}
%************************************************************************
-- Check the rhs
do { ty <- lintCoreExpr rhs
; lintBinder binder -- Check match to RHS type
- ; binder_ty <- applySubst binder_ty
+ ; binder_ty <- applySubstTy binder_ty
; checkTys binder_ty ty (mkRhsMsg binder ty)
-- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
; checkL (not (isUnLiftedType binder_ty)
-- Check whether binder's specialisations contain any out-of-scope variables
; mapM_ (checkBndrIdInScope binder) bndr_vars
+ ; when (isNonRuleLoopBreaker (idOccInfo binder) && isInlinePragma (idInlinePragma binder))
+ (addWarnL (ptext (sLit "INLINE binder is (non-rule) loop breaker:") <+> ppr binder))
+ -- Only non-rule loop breakers inhibit inlining
+
-- Check whether arity and demand type are consistent (only if demand analysis
-- already happened)
; checkL (case maybeDmdTy of
-- the unfolding is a SimplifiableCoreExpr. Give up for now.
where
binder_ty = idType binder
- maybeDmdTy = idNewStrictness_maybe binder
- bndr_vars = varSetElems (idFreeVars binder `unionVarSet` wkr_vars)
- wkr_vars | workerExists wkr_info = unitVarSet (workerId wkr_info)
- | otherwise = emptyVarSet
- wkr_info = idWorkerInfo binder
+ maybeDmdTy = idStrictness_maybe binder
+ bndr_vars = varSetElems (idFreeVars binder)
lintBinder var | isId var = lintIdBndr var $ \_ -> (return ())
| otherwise = return ()
\end{code}
%************************************************************************
\begin{code}
-type InType = Type -- Substitution not yet applied
-type OutType = Type -- Substitution has been applied to this
+type InType = Type -- Substitution not yet applied
+type InCoercion = Coercion
+type InVar = Var
+type InTyVar = TyVar
+
+type OutType = Type -- Substitution has been applied to this
+type OutCoercion = Coercion
+type OutVar = Var
+type OutTyVar = TyVar
lintCoreExpr :: CoreExpr -> LintM OutType
-- The returned type has the substitution from the monad
= do { checkL (not (var == oneTupleDataConId))
(ptext (sLit "Illegal one-tuple"))
- ; checkDeadIdOcc var
+ ; checkL (isId var && not (isCoVar var))
+ (ptext (sLit "Non term variable") <+> ppr var)
+
+ ; checkDeadIdOcc var
; var' <- lookupIdInScope var
- ; return (idType var')
- }
+ ; return (idType var') }
lintCoreExpr (Lit lit)
= return (literalType lit)
---lintCoreExpr (Note (Coerce to_ty from_ty) expr)
--- = do { expr_ty <- lintCoreExpr expr
--- ; to_ty <- lintTy to_ty
--- ; from_ty <- lintTy from_ty
--- ; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
--- ; return to_ty }
-
lintCoreExpr (Cast expr co)
= do { expr_ty <- lintCoreExpr expr
- ; co' <- lintTy co
- ; let (from_ty, to_ty) = coercionKind co'
+ ; co' <- applySubstCo co
+ ; (from_ty, to_ty) <- lintCoercion co'
; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
; return to_ty }
= 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'
+ | isTyVar tv
+ = -- See Note [Linting type lets]
+ do { ty' <- addLoc (RhsOf tv) $ lintInTy ty
+ ; lintTyBndr tv $ \ tv' ->
+ addLoc (BodyOfLetRec [tv]) $
+ extendSubstL tv' ty' $ do
+ { checkTyKind 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 body } }
lintCoreExpr (Let (NonRec bndr rhs) body)
+ | isId bndr
= do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
- ; addLoc (BodyOfLetRec [bndr])
+ ; addLoc (BodyOfLetRec [bndr])
(lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
+ | otherwise
+ = failWithL (mkLetErr bndr rhs) -- Not quite accurate
+
lintCoreExpr (Let (Rec pairs) body)
= lintAndScopeIds bndrs $ \_ ->
- do { mapM (lintSingleBinding NotTopLevel Recursive) pairs
+ do { checkL (null dups) (dupVars dups)
+ ; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
where
bndrs = map fst pairs
+ (_, dups) = removeDups compare bndrs
lintCoreExpr e@(App fun arg)
= do { fun_ty <- lintCoreExpr fun
lintCoreExpr (Lam var expr)
= addLoc (LambdaBodyOf var) $
- lintBinders [var] $ \[var'] ->
- do { body_ty <- lintCoreExpr expr
+ lintBinders [var] $ \ vars' ->
+ do { let [var'] = vars'
+ ; body_ty <- lintCoreExpr expr
; if isId var' then
return (mkFunTy (idType var') body_ty)
else
return (mkForAllTy var' body_ty)
}
- -- The applySubst is needed to apply the subst to var
+ -- The applySubstTy is needed to apply the subst to var
lintCoreExpr e@(Case scrut var alt_ty alts) =
-- Check the scrutinee
do { scrut_ty <- lintCoreExpr scrut
- ; alt_ty <- lintTy alt_ty
- ; var_ty <- lintTy (idType var)
+ ; alt_ty <- lintInTy alt_ty
+ ; var_ty <- lintInTy (idType var)
; let mb_tc_app = splitTyConApp_maybe (idType var)
; case mb_tc_app of
Just (tycon, _)
| debugIsOn &&
isAlgTyCon tycon &&
- not (isOpenTyCon tycon) &&
+ not (isFamilyTyCon tycon || isAbstractTyCon tycon) &&
null (tyConDataCons tycon) ->
pprTrace "Lint warning: case binder's type has no constructors" (ppr var <+> ppr (idType var))
-- This can legitimately happen for type families
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 (Type ty)
- = do { ty' <- lintTy ty
+ = do { ty' <- lintInTy ty
; return (typeKind ty') }
+
+lintCoreExpr (Coercion co)
+ = do { co' <- lintInCo co
+ ; let Pair ty1 ty2 = coercionKind co'
+ ; return (mkPredTy $ EqPred ty1 ty2) }
\end{code}
%************************************************************************
subtype of the required type, as one would expect.
\begin{code}
-lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
-lintCoreArg :: OutType -> CoreArg -> LintM OutType
--- First argument has already had substitution applied to it
-\end{code}
+lintCoreArg :: OutType -> CoreArg -> LintM OutType
+lintCoreArg fun_ty (Type arg_ty)
+ = do { arg_ty' <- applySubstTy arg_ty
+ ; lintTyApp fun_ty arg_ty' }
+
+lintCoreArg fun_ty arg
+ = do { arg_ty <- lintCoreExpr arg
+ ; lintValApp arg fun_ty arg_ty }
+
+-----------------
+lintAltBinders :: OutType -- Scrutinee type
+ -> OutType -- Constructor type
+ -> [OutVar] -- Binders
+ -> LintM ()
+lintAltBinders scrut_ty con_ty []
+ = checkTys con_ty scrut_ty (mkBadPatMsg con_ty scrut_ty)
+lintAltBinders scrut_ty con_ty (bndr:bndrs)
+ | isTyVar bndr
+ = do { con_ty' <- lintTyApp con_ty (mkTyVarTy bndr)
+ ; lintAltBinders scrut_ty con_ty' bndrs }
+ | otherwise
+ = do { con_ty' <- lintValApp (Var bndr) con_ty (idType bndr)
+ ; lintAltBinders scrut_ty con_ty' bndrs }
-\begin{code}
-lintCoreArgs ty [] = return ty
-lintCoreArgs ty (a : args) =
- do { res <- lintCoreArg ty a
- ; lintCoreArgs res args }
-
-lintCoreArg fun_ty (Type arg_ty) =
- do { arg_ty <- lintTy arg_ty
- ; lintTyApp fun_ty arg_ty }
-
-lintCoreArg fun_ty arg =
- -- Make sure function type matches argument
- do { arg_ty <- lintCoreExpr arg
- ; let err1 = mkAppMsg fun_ty arg_ty arg
- err2 = mkNonFunAppMsg fun_ty arg_ty arg
- ; case splitFunTy_maybe fun_ty of
- Just (arg,res) ->
- do { checkTys arg arg_ty err1
- ; return res }
- _ -> addErrL err2 }
+-----------------
+lintTyApp :: OutType -> OutType -> LintM OutType
+lintTyApp fun_ty arg_ty
+ | Just (tyvar,body_ty) <- splitForAllTy_maybe fun_ty
+ , isTyVar tyvar
+ = do { checkTyKind tyvar arg_ty
+ ; return (substTyWith [tyvar] [arg_ty] body_ty) }
+
+ | otherwise
+ = failWithL (mkTyAppMsg fun_ty arg_ty)
+
+-----------------
+lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
+lintValApp arg fun_ty arg_ty
+ | Just (arg,res) <- splitFunTy_maybe fun_ty
+ = do { checkTys arg arg_ty err1
+ ; return res }
+ | otherwise
+ = failWithL err2
+ where
+ err1 = mkAppMsg fun_ty arg_ty arg
+ err2 = mkNonFunAppMsg fun_ty arg_ty arg
\end{code}
\begin{code}
+checkTyKind :: OutTyVar -> OutType -> LintM ()
-- 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)
-
- Just (tyvar,body)
- -> do { checkL (isTyVar tyvar) (mkTyAppMsg ty arg_ty)
- ; checkKinds tyvar arg_ty
- ; return (substTyWith [tyvar] [arg_ty] body) }
-
-checkKinds :: Var -> Type -> LintM ()
-checkKinds tyvar arg_ty
+checkTyKind tyvar arg_ty
-- Arg type might be boxed for a function with an uncommitted
-- 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)
+ = do { arg_kind <- lintType arg_ty
+ ; 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
+
+-- Check that the kinds of a type variable and a coercion match, that
+-- is, if tv :: k then co :: t1 ~ t2 where t1 :: k and t2 :: k.
+checkTyCoKind :: TyVar -> OutCoercion -> LintM (OutType, OutType)
+checkTyCoKind tv co
+ = do { (t1,t2) <- lintCoercion co
+ ; k1 <- lintType t1
+ ; k2 <- lintType t2
+ ; unless ((k1 `isSubKind` tyvar_kind) && (k2 `isSubKind` tyvar_kind))
+ (addErrL (mkTyCoAppErrMsg tv co))
+ ; return (t1,t2) }
+ where
+ tyvar_kind = tyVarKind tv
+
+checkTyCoKinds :: [TyVar] -> [OutCoercion] -> LintM [(OutType, OutType)]
+checkTyCoKinds = zipWithM checkTyCoKind
checkDeadIdOcc :: Id -> LintM ()
-- Occurrences of an Id should never be dead....
lit_ty = literalType lit
lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
- | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
+ | isNewTyCon (dataConTyCon con)
+ = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
| Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
= addLoc (CaseAlt alt) $ do
{ -- First instantiate the universally quantified
; 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 con_payload_ty (varsToCoreExprs args)
- ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
- }
- -- Check the RHS
+ ; lintBinders args $ \ args' -> do
+ { addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
; checkAltExpr rhs alt_ty } }
| otherwise -- Scrut-ty is wrong shape
lintBinder :: Var -> (Var -> LintM a) -> LintM a
lintBinder var linterF
- | isTyVar var = lint_ty_bndr
- | otherwise = lintIdBndr var linterF
- where
- lint_ty_bndr = do { lintTy (tyVarKind var)
- ; subst <- getTvSubst
- ; let (subst', tv') = substTyVarBndr subst var
- ; updateTvSubst subst' (linterF tv') }
+ | isId var = lintIdBndr var linterF
+ | otherwise = lintTyBndr var linterF
-lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
+lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
+lintTyBndr tv thing_inside
+ = do { subst <- getTvSubst
+ ; let (subst', tv') = Type.substTyVarBndr subst tv
+ ; lintTyBndrKind tv'
+ ; updateTvSubst subst' (thing_inside tv') }
+
+lintIdBndr :: Id -> (Id -> LintM a) -> LintM a
-- Do substitution on the type of a binder and add the var with this
-- new type to the in-scope set of the second argument
-- ToDo: lint its rules
+
lintIdBndr id linterF
= do { checkL (not (isUnboxedTupleType (idType id)))
(mkUnboxedTupleMsg id)
-- No variable can be bound to an unboxed tuple.
- ; lintAndScopeId id $ \id' -> linterF id'
- }
+ ; lintAndScopeId id $ \id' -> linterF id' }
lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
lintAndScopeIds ids linterF
= go ids
where
go [] = linterF []
- go (id:ids) = do { lintAndScopeId id $ \id ->
- lintAndScopeIds ids $ \ids ->
- linterF (id:ids) }
+ go (id:ids) = lintAndScopeId id $ \id ->
+ lintAndScopeIds ids $ \ids ->
+ linterF (id:ids)
-lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
+lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
lintAndScopeId id linterF
- = do { ty <- lintTy (idType id)
+ = do { ty <- lintInTy (idType id)
; let id' = setIdType id ty
- ; addInScopeVars [id'] $ (linterF id')
- }
+ ; addInScopeVar id' $ (linterF id') }
+\end{code}
+
-lintTy :: InType -> LintM OutType
+%************************************************************************
+%* *
+\subsection[lint-monad]{The Lint monad}
+%* *
+%************************************************************************
+
+\begin{code}
+lintInTy :: 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
- ; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
+lintInTy ty
+ = addLoc (InType ty) $
+ do { ty' <- applySubstTy ty
+ ; _ <- lintType ty'
; return ty' }
-\end{code}
+lintInCo :: InCoercion -> LintM OutCoercion
+-- Check the coercion, and apply the substitution to it
+-- See Note [Linting type lets]
+lintInCo co
+ = addLoc (InCo co) $
+ do { co' <- applySubstCo co
+ ; _ <- lintCoercion co'
+ ; return co' }
+
+-------------------
+lintKind :: Kind -> LintM ()
+-- Check well-formedness of kinds: *, *->*, etc
+lintKind (TyConApp tc [])
+ | getUnique tc `elem` kindKeys
+ = return ()
+lintKind (FunTy k1 k2)
+ = lintKind k1 >> lintKind k2
+lintKind kind
+ = addErrL (hang (ptext (sLit "Malformed kind:")) 2 (quotes (ppr kind)))
+
+-------------------
+lintTyBndrKind :: OutTyVar -> LintM ()
+lintTyBndrKind tv = lintKind (tyVarKind tv)
+
+-------------------
+lintCoercion :: OutCoercion -> LintM (OutType, OutType)
+-- Check the kind of a coercion term, returning the kind
+lintCoercion (Refl ty)
+ = do { ty' <- lintInTy ty
+ ; return (ty', ty') }
+
+lintCoercion co@(TyConAppCo tc cos)
+ = do { (ss,ts) <- mapAndUnzipM lintCoercion cos
+ ; check_co_app co (tyConKind tc) ss
+ ; return (mkTyConApp tc ss, mkTyConApp tc ts) }
+
+lintCoercion co@(AppCo co1 co2)
+ = do { (s1,t1) <- lintCoercion co1
+ ; (s2,t2) <- lintCoercion co2
+ ; check_co_app co (typeKind s1) [s2]
+ ; return (mkAppTy s1 s2, mkAppTy t1 t2) }
+
+lintCoercion (ForAllCo v co)
+ = do { lintKind (tyVarKind v)
+ ; (s,t) <- addInScopeVar v (lintCoercion co)
+ ; return (ForAllTy v s, ForAllTy v t) }
+
+lintCoercion (CoVarCo cv)
+ = do { checkTyCoVarInScope cv
+ ; return (coVarKind cv) }
+
+lintCoercion (AxiomInstCo (CoAxiom { co_ax_tvs = tvs
+ , co_ax_lhs = lhs
+ , co_ax_rhs = rhs })
+ cos)
+ = do { (tys1, tys2) <- liftM unzip (checkTyCoKinds tvs cos)
+ ; return (substTyWith tvs tys1 lhs,
+ substTyWith tvs tys2 rhs) }
+
+lintCoercion (UnsafeCo ty1 ty2)
+ = do { ty1' <- lintInTy ty1
+ ; ty2' <- lintInTy ty2
+ ; return (ty1', ty2') }
+
+lintCoercion (SymCo co)
+ = do { (ty1, ty2) <- lintCoercion co
+ ; return (ty2, ty1) }
+
+lintCoercion co@(TransCo co1 co2)
+ = do { (ty1a, ty1b) <- lintCoercion co1
+ ; (ty2a, ty2b) <- lintCoercion co2
+ ; checkL (ty1b `eqType` ty2a)
+ (hang (ptext (sLit "Trans coercion mis-match:") <+> ppr co)
+ 2 (vcat [ppr ty1a, ppr ty1b, ppr ty2a, ppr ty2b]))
+ ; return (ty1a, ty2b) }
+
+lintCoercion the_co@(NthCo d co)
+ = do { (s,t) <- lintCoercion co
+ ; sn <- checkTcApp the_co d s
+ ; tn <- checkTcApp the_co d t
+ ; return (sn, tn) }
+
+lintCoercion (InstCo co arg_ty)
+ = do { co_tys <- lintCoercion co
+ ; arg_kind <- lintType arg_ty
+ ; case splitForAllTy_maybe `traverse` toPair co_tys of
+ Just (Pair (tv1,ty1) (tv2,ty2))
+ | arg_kind `isSubKind` tyVarKind tv1
+ -> return (substTyWith [tv1] [arg_ty] ty1,
+ substTyWith [tv2] [arg_ty] ty2)
+ | otherwise
+ -> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
+ Nothing -> failWithL (ptext (sLit "Bad argument of inst")) }
+
+----------
+checkTcApp :: Coercion -> Int -> Type -> LintM Type
+checkTcApp co n ty
+ | Just (_, tys) <- splitTyConApp_maybe ty
+ , n < length tys
+ = return (tys !! n)
+ | otherwise
+ = failWithL (hang (ptext (sLit "Bad getNth:") <+> ppr co)
+ 2 (ptext (sLit "Offending type:") <+> ppr ty))
+
+-------------------
+lintType :: OutType -> LintM Kind
+lintType (TyVarTy tv)
+ = do { checkTyCoVarInScope tv
+ ; return (tyVarKind tv) }
+
+lintType ty@(AppTy t1 t2)
+ = do { k1 <- lintType t1
+ ; lint_ty_app ty k1 [t2] }
+
+lintType ty@(FunTy t1 t2)
+ = lint_ty_app ty (tyConKind funTyCon) [t1,t2]
+
+lintType ty@(TyConApp tc tys)
+ | tyConHasKind tc
+ = lint_ty_app ty (tyConKind tc) tys
+ | otherwise
+ = failWithL (hang (ptext (sLit "Malformed type:")) 2 (ppr ty))
+
+lintType (ForAllTy tv ty)
+ = do { lintTyBndrKind tv
+ ; addInScopeVar tv (lintType ty) }
+
+lintType ty@(PredTy (ClassP cls tys))
+ = lint_ty_app ty (tyConKind (classTyCon cls)) tys
+
+lintType (PredTy (IParam _ p_ty))
+ = lintType p_ty
+
+lintType ty@(PredTy (EqPred t1 t2))
+ = do { k1 <- lintType t1
+ ; k2 <- lintType t2
+ ; unless (k1 `eqKind` k2)
+ (addErrL (sep [ ptext (sLit "Kind mis-match in equality predicate:")
+ , nest 2 (ppr ty) ]))
+ ; return unliftedTypeKind }
+
+----------------
+lint_ty_app :: Type -> Kind -> [OutType] -> LintM Kind
+lint_ty_app ty k tys
+ = do { ks <- mapM lintType tys
+ ; lint_kind_app (ptext (sLit "type") <+> quotes (ppr ty)) k ks }
+
+----------------
+check_co_app :: Coercion -> Kind -> [OutType] -> LintM ()
+check_co_app ty k tys
+ = do { _ <- lint_kind_app (ptext (sLit "coercion") <+> quotes (ppr ty))
+ k (map typeKind tys)
+ ; return () }
+
+----------------
+lint_kind_app :: SDoc -> Kind -> [Kind] -> LintM Kind
+lint_kind_app doc kfn ks = go kfn ks
+ where
+ fail_msg = vcat [hang (ptext (sLit "Kind application error in")) 2 doc,
+ nest 2 (ptext (sLit "Function kind =") <+> ppr kfn),
+ nest 2 (ptext (sLit "Arg kinds =") <+> ppr ks)]
+
+ go kfn [] = return kfn
+ go kfn (k:ks) = case splitKindFunTy_maybe kfn of
+ Nothing -> failWithL fail_msg
+ Just (kfa, kfb) -> do { unless (k `isSubKind` kfa)
+ (addErrL fail_msg)
+ ; go kfb ks }
+\end{code}
%************************************************************************
%* *
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
| AnExpr CoreExpr -- Some expression
| ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
| TopLevelBindings
+ | InType Type -- Inside a type
+ | InCo Coercion -- Inside a coercion
\end{code}
\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
-addErrL :: Message -> LintM a
-addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
+failWithL :: Message -> LintM a
+failWithL msg = LintM $ \ loc subst (warns,errs) ->
+ (Nothing, (warns, addMsg subst errs msg loc))
-addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
-addErr subst errs_so_far msg locs
+addErrL :: Message -> LintM ()
+addErrL msg = LintM $ \ loc subst (warns,errs) ->
+ (Just (), (warns, addMsg subst errs msg loc))
+
+addWarnL :: Message -> LintM ()
+addWarnL msg = LintM $ \ loc subst (warns,errs) ->
+ (Just (), (addMsg subst warns msg loc, errs))
+
+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]
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)
- where
- (_, dups) = removeDups compare vars
+ = LintM (\ loc subst errs -> unLintM m loc (extendTvInScopeList subst vars) errs)
+
+addInScopeVar :: Var -> LintM a -> LintM a
+addInScopeVar var m
+ = LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst var) errs)
updateTvSubst :: TvSubst -> LintM a -> LintM a
updateTvSubst subst' m =
getTvSubst :: LintM TvSubst
getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
-applySubst :: Type -> LintM Type
-applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
+applySubstTy :: Type -> LintM Type
+applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
+
+applySubstCo :: Coercion -> LintM Coercion
+applySubstCo co = do { subst <- getTvSubst; return (substCo (tvCvSubst subst) co) }
extendSubstL :: TyVar -> Type -> LintM a -> LintM a
extendSubstL tv ty m
- = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
+ = LintM (\ loc subst errs -> unLintM m loc (Type.extendTvSubst subst tv ty) errs)
\end{code}
\begin{code}
msg = ptext (sLit "is out of scope inside info for") <+>
ppr binder
-checkTyVarInScope :: TyVar -> LintM ()
-checkTyVarInScope tv = checkInScope (ptext (sLit "is out of scope")) tv
+checkTyCoVarInScope :: TyCoVar -> LintM ()
+checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
checkInScope :: SDoc -> Var -> LintM ()
checkInScope loc_msg var =
; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
(hsep [ppr var, loc_msg]) }
-checkTys :: Type -> Type -> Message -> LintM ()
+checkTys :: OutType -> OutType -> Message -> LintM ()
-- check ty2 is subtype of ty1 (ie, has same structure but usage
-- annotations need only be consistent, not equal)
-- Assumes ty1,ty2 are have alrady had the substitution applied
-checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
+checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
\end{code}
%************************************************************************
= (locn, brackets (ptext (sLit "in an imported unfolding")))
dumpLoc TopLevelBindings
= (noSrcLoc, empty)
+dumpLoc (InType ty)
+ = (noSrcLoc, text "In the type" <+> quotes (ppr ty))
+dumpLoc (InCo co)
+ = (noSrcLoc, text "In the coercion" <+> quotes (ppr co))
pp_binders :: [Var] -> SDoc
pp_binders bs = sep (punctuate comma (map pp_binder bs))
hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
hang (ptext (sLit "Arg:")) 4 (ppr arg)]
-mkKindErrMsg :: TyVar -> Type -> Message
-mkKindErrMsg tyvar arg_ty
- = vcat [ptext (sLit "Kinds don't match in type application:"),
- hang (ptext (sLit "Type variable:"))
+mkLetErr :: TyVar -> CoreExpr -> Message
+mkLetErr bndr rhs
+ = vcat [ptext (sLit "Bad `let' binding:"),
+ hang (ptext (sLit "Variable:"))
+ 4 (ppr bndr <+> dcolon <+> ppr (varType bndr)),
+ hang (ptext (sLit "Rhs:"))
+ 4 (ppr rhs)]
+
+mkTyCoAppErrMsg :: TyVar -> Coercion -> Message
+mkTyCoAppErrMsg tyvar arg_co
+ = vcat [ptext (sLit "Kinds don't match in lifted coercion application:"),
+ hang (ptext (sLit "Type variable:"))
4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
- hang (ptext (sLit "Arg type:"))
- 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
+ hang (ptext (sLit "Arg coercion:"))
+ 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
mkTyAppMsg :: Type -> Type -> Message
mkTyAppMsg ty arg_ty
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)]
+ hsep [ptext (sLit "Binder's demand info:"), ppr (idDemandInfo binder)]
]
+
+mkKindErrMsg :: TyVar -> Type -> Message
+mkKindErrMsg tyvar arg_ty
+ = vcat [ptext (sLit "Kinds don't match in type application:"),
+ hang (ptext (sLit "Type variable:"))
+ 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
+ hang (ptext (sLit "Arg type:"))
+ 4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
+
mkArityMsg :: Id -> Message
mkArityMsg binder
= vcat [hsep [ptext (sLit "Demand type has "),
hsep [ptext (sLit "Binder's strictness signature:"), ppr dmd_ty]
]
- where (StrictSig dmd_ty) = idNewStrictness binder
+ where (StrictSig dmd_ty) = idStrictness binder
mkUnboxedTupleMsg :: Id -> Message
mkUnboxedTupleMsg binder
dupVars vars
= hang (ptext (sLit "Duplicate variables brought into scope"))
2 (ppr vars)
+
+dupExtVars :: [[Name]] -> Message
+dupExtVars vars
+ = hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
+ 2 (ppr vars)
\end{code}
+
+-------------- DEAD CODE -------------------
+
+-------------------
+checkCoKind :: CoVar -> OutCoercion -> LintM ()
+-- Both args have had substitution applied
+checkCoKind covar arg_co
+ = do { (s2,t2) <- lintCoercion arg_co
+ ; unless (s1 `eqType` s2 && t1 `coreEqType` t2)
+ (addErrL (mkCoAppErrMsg covar arg_co)) }
+ where
+ (s1,t1) = coVarKind covar
+
+lintCoVarKind :: OutCoVar -> LintM ()
+-- Check the kind of a coercion binder
+lintCoVarKind tv
+ = do { (ty1,ty2) <- lintSplitCoVar tv
+ ; lintEqType ty1 ty2
+
+
+-------------------
+lintSplitCoVar :: CoVar -> LintM (Type,Type)
+lintSplitCoVar cv
+ = case coVarKind_maybe cv of
+ Just ts -> return ts
+ Nothing -> failWithL (sep [ ptext (sLit "Coercion variable with non-equality kind:")
+ , nest 2 (ppr cv <+> dcolon <+> ppr (tyVarKind cv))])
+
+mkCoVarLetErr :: CoVar -> Coercion -> Message
+mkCoVarLetErr covar co
+ = vcat [ptext (sLit "Bad `let' binding for coercion variable:"),
+ hang (ptext (sLit "Coercion variable:"))
+ 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
+ hang (ptext (sLit "Arg coercion:"))
+ 4 (ppr co)]
+
+mkCoAppErrMsg :: CoVar -> Coercion -> Message
+mkCoAppErrMsg covar arg_co
+ = vcat [ptext (sLit "Kinds don't match in coercion application:"),
+ hang (ptext (sLit "Coercion variable:"))
+ 4 (ppr covar <+> dcolon <+> ppr (coVarKind covar)),
+ hang (ptext (sLit "Arg coercion:"))
+ 4 (ppr arg_co <+> dcolon <+> pprEqPred (coercionKind arg_co))]
+
+
+mkCoAppMsg :: Type -> Coercion -> Message
+mkCoAppMsg ty arg_co
+ = vcat [text "Illegal type application:",
+ hang (ptext (sLit "exp type:"))
+ 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
+ hang (ptext (sLit "arg type:"))
+ 4 (ppr arg_co <+> dcolon <+> ppr (coercionKind arg_co))]
+
projects / ghc-hetmet.git / blobdiff