-lintCoreArg :: Bool -> CoreExpr -> Type -> CoreArg -> LintM (Maybe Type)
-
-lintCoreArg _ e ty (LitArg lit)
- = -- Make sure function type matches argument
- case (getFunTy_maybe ty) of
- Just (arg,res) | (literalType lit `eqTy` arg) -> returnL(Just res)
- _ -> addErrL (mkAppMsg ty (literalType lit) e) `seqL` returnL Nothing
-
-lintCoreArg _ e ty (VarArg v)
- = -- Make sure variable is bound
- checkInScope v `seqL`
- -- Make sure function type matches argument
- case (getFunTy_maybe ty) of
- Just (arg,res) | (idType v `eqTy` arg) -> returnL(Just res)
- _ -> addErrL (mkAppMsg ty (idType v) e) `seqL` returnL Nothing
-
-lintCoreArg checkTyApp e ty a@(TyArg arg_ty)
- = -- TODO: Check that ty is well-kinded and has no unbound tyvars
- checkIfSpecDoneL (not (isPrimType arg_ty)) (mkSpecTyAppMsg a)
- `seqL`
- case (getForAllTy_maybe ty) of
- Just (tyvar,body) | (getTyVarKind tyvar == getTypeKind arg_ty) ->
- returnL(Just(instantiateTy [(tyvar,arg_ty)] body))
- _ -> addErrL (mkTyAppMsg ty arg_ty e) `seqL` returnL Nothing
-
-lintCoreArg _ e ty (UsageArg u)
- = -- TODO: Check that usage has no unbound usage variables
- case (getForAllUsageTy ty) of
- Just (uvar,bounds,body) ->
- -- TODO Check argument satisfies bounds
- returnL(Just(panic "lintCoreArg:instantiateUsage uvar u body"))
- _ -> addErrL (mkUsageAppMsg ty u e) `seqL` returnL Nothing
+checkCaseAlts :: CoreExpr -> Type -> [CoreAlt] -> LintM ()
+-- a) Check that the alts are non-empty
+-- b) Check that the DEFAULT comes first, if it exists
+-- 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
+-- possibly match.
+
+checkCaseAlts e ty []
+ = addErrL (mkNullAltsMsg e)
+
+checkCaseAlts e ty alts =
+ do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
+ ; checkL (isJust maybe_deflt || not is_infinite_ty)
+ (nonExhaustiveAltsMsg e) }
+ where
+ (con_alts, maybe_deflt) = findDefault alts
+
+ non_deflt (DEFAULT, _, _) = False
+ non_deflt alt = True
+
+ is_infinite_ty = case splitTyConApp_maybe ty of
+ Nothing -> False
+ Just (tycon, tycon_arg_tys) -> isPrimTyCon tycon
+\end{code}
+
+\begin{code}
+checkAltExpr :: CoreExpr -> Type -> LintM ()
+checkAltExpr expr ty
+ = do { actual_ty <- lintCoreExpr expr
+ ; ty' <- applySubst ty
+ ; checkTys actual_ty ty' (mkCaseAltMsg expr actual_ty ty') }
+
+lintCoreAlt :: Type -- Type of scrutinee
+ -> Type -- Type of the alternative
+ -> CoreAlt
+ -> LintM ()
+
+lintCoreAlt scrut_ty alt_ty alt@(DEFAULT, args, rhs) =
+ do { checkL (null args) (mkDefaultArgsMsg args)
+ ; checkAltExpr rhs alt_ty }
+
+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)
+ ; checkAltExpr rhs alt_ty }
+ where
+ lit_ty = literalType lit
+
+lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
+ | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty,
+ tycon == dataConTyCon con
+ = addLoc (CaseAlt alt) $
+ addInScopeVars args $ -- Put the args in scope before lintBinder,
+ -- because the Ids mention the type variables
+ if isVanillaDataCon con then
+ do { mapM lintBinder args
+ -- FIX! Add check that all args are Ids.
+ -- 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_type <- lintTyApps (dataConRepType con) tycon_arg_tys
+ -- Can just map Var as we know that this is a vanilla datacon
+ ; con_result_ty <- lintCoreArgs con_type (map Var args)
+ ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
+ -- Check the RHS
+ ; checkAltExpr rhs alt_ty }
+
+ 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 $
+ 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
+ } } }
+
+ | otherwise -- Scrut-ty is wrong shape
+ = addErrL (mkBadAltMsg scrut_ty alt)