import CoreSyn
import CoreFVs ( idFreeVars )
-import CoreUtils ( findDefault, exprOkForSpeculation, coreBindsSize, mkPiType )
+import CoreUtils ( findDefault, exprOkForSpeculation, coreBindsSize )
import Unify ( coreRefineTys )
import Bag
import Literal ( literalType )
-import DataCon ( dataConRepType, isVanillaDataCon, dataConTyCon, dataConResTy, dataConWorkId )
+import DataCon ( dataConRepType, isVanillaDataCon, dataConTyCon, dataConWorkId )
import TysWiredIn ( tupleCon )
import Var ( Var, Id, TyVar, idType, tyVarKind, mustHaveLocalBinding )
import VarSet
import Type ( Type, tyVarsOfType, coreEqType,
splitFunTy_maybe, mkTyVarTys,
splitForAllTy_maybe, splitTyConApp_maybe,
- isUnLiftedType, typeKind,
+ isUnLiftedType, typeKind, mkForAllTy, mkFunTy,
isUnboxedTupleType, isSubKind,
substTyWith, emptyTvSubst, extendTvInScope,
- TvSubst, TvSubstEnv, setTvSubstEnv, substTy,
- extendTvSubst, isInScope )
+ TvSubst, TvSubstEnv, mkTvSubst, setTvSubstEnv, substTy,
+ extendTvSubst, composeTvSubst, isInScope,
+ getTvSubstEnv, getTvInScope )
import TyCon ( isPrimTyCon )
import BasicTypes ( RecFlag(..), Boxity(..), isNonRec )
import CmdLineOpts
%************************************************************************
\begin{code}
+type InType = Type -- Substitution not yet applied
+type OutType = Type -- Substitution has been applied to this
-lintCoreExpr :: CoreExpr -> LintM Type
+lintCoreExpr :: CoreExpr -> LintM OutType
-- The returned type has the substitution from the monad
-- already applied to it:
-- lintCoreExpr e subst = exprType (subst e)
lintCoreExpr (Lam var expr)
= addLoc (LambdaBodyOf var) $
- do { lintBinder var
- ; ty <- addInScopeVars [var] $
- lintCoreExpr expr
- ; applySubst (mkPiType var ty) }
+ do { body_ty <- addInScopeVars [var] $
+ lintCoreExpr expr
+ ; if isId var then do
+ { var_ty <- lintId var
+ ; return (mkFunTy var_ty body_ty) }
+ else
+ return (mkForAllTy var body_ty)
+ }
-- The applySubst is needed to apply the subst to var
lintCoreExpr e@(Case scrut var alt_ty alts) =
%************************************************************************
\begin{code}
-checkCaseAlts :: CoreExpr -> Type -> [CoreAlt] -> LintM ()
+checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
-- a) Check that the alts are non-empty
--- b) Check that the DEFAULT comes first, if it exists
+-- b1) Check that the DEFAULT comes first, if it exists
+-- b2) Check that the others are in increasing order
-- c) Check that there's a default for infinite types
-- NB: Algebraic cases are not necessarily exhaustive, because
-- the simplifer correctly eliminates case that can't
checkCaseAlts e ty alts =
do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
+ ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
; checkL (isJust maybe_deflt || not is_infinite_ty)
(nonExhaustiveAltsMsg e) }
where
(con_alts, maybe_deflt) = findDefault alts
+ -- Check that successive alternatives have increasing tags
+ increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
+ increasing_tag other = True
+
non_deflt (DEFAULT, _, _) = False
non_deflt alt = True
\end{code}
\begin{code}
-checkAltExpr :: CoreExpr -> Type -> LintM ()
-checkAltExpr expr ty
+checkAltExpr :: CoreExpr -> OutType -> LintM ()
+checkAltExpr expr ann_ty
= do { actual_ty <- lintCoreExpr expr
- ; ty' <- applySubst ty
- ; checkTys actual_ty ty' (mkCaseAltMsg expr actual_ty ty') }
+ ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
-lintCoreAlt :: Type -- Type of scrutinee; a fixed point of
- -- the substitution
- -> Type -- Type of the alternative
+lintCoreAlt :: OutType -- Type of scrutinee
+ -> OutType -- Type of the alternative
-> CoreAlt
-> LintM ()
lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) =
do { checkL (null args) (mkDefaultArgsMsg args)
- ; checkTys lit_ty scrut_ty
- (mkBadPatMsg lit_ty scrut_ty)
+ ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)
; checkAltExpr rhs alt_ty }
where
lit_ty = literalType lit
else -- GADT
do { let (tvs,ids) = span isTyVar args
- pat_res_ty = dataConResTy con (mkTyVarTys tvs)
-
; subst <- getTvSubst
- ; case coreRefineTys tvs subst pat_res_ty scrut_ty of {
- Nothing -> return () ; -- Alternative is dead code
- Just senv -> updateTvSubstEnv senv $
+ ; let in_scope = getTvInScope subst
+ subst_env = getTvSubstEnv subst
+ ; case coreRefineTys in_scope con tvs scrut_ty of {
+ Nothing -> return () ; -- Alternative is dead code
+ Just (refine, _) -> updateTvSubstEnv (composeTvSubst in_scope refine subst_env) $
do { tvs' <- mapM lintTy (mkTyVarTys tvs)
; con_type <- lintTyApps (dataConRepType con) tvs'
; mapM lintBinder ids -- Lint Ids in the refined world
; lintCoreArgs con_type (map Var ids)
- ; checkAltExpr rhs alt_ty
+ ; let refined_alt_ty = substTy (mkTvSubst in_scope refine) alt_ty
+ -- alt_ty is already an OutType, so don't re-apply
+ -- the current substitution. But we must apply the
+ -- refinement so that the check in checkAltExpr is ok
+ ; checkAltExpr rhs refined_alt_ty
} } }
| otherwise -- Scrut-ty is wrong shape
lintBinder var | isId var = lintId var >> return ()
| otherwise = return ()
-lintId :: Var -> LintM Type
+lintId :: Var -> LintM OutType
-- ToDo: lint its rules
lintId id
= do { checkL (not (isUnboxedTupleType (idType id)))
-- No variable can be bound to an unboxed tuple.
; lintTy (idType id) }
-lintTy :: Type -> LintM Type
+lintTy :: InType -> LintM OutType
-- Check the type, and apply the substitution to it
-- ToDo: check the kind structure of the type
lintTy ty
addInScopeVars vars m =
LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
--- gaw 2004
updateTvSubstEnv :: TvSubstEnv -> LintM a -> LintM a
updateTvSubstEnv substenv m =
LintM (\ loc subst errs -> unLintM m loc (setTvSubstEnv subst substenv) errs)
mkNonDefltMsg e
= hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
+mkNonIncreasingAltsMsg e
+ = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
nonExhaustiveAltsMsg :: CoreExpr -> Message
nonExhaustiveAltsMsg e
projects / ghc-hetmet.git / blobdiff