We need to split the co_ax_tvs into kind and type variables in order
to find out the coercion kind instantiations. Those can only be Refl
since we don't have kind coercions. This is just a way to represent
kind instantiation.
We use the number of kind variables to know how to split the coercions
instantiations between kind coercions and type coercions. We lint the
kind coercions and produce the following substitution which is to be
applied in the type variables:
k_ag ~~> * -> *
%************************************************************************
%* *
\subsection[lintCoreArgs]{lintCoreArgs}
%* *
%************************************************************************
The basic version of these functions checks that the argument is a
subtype of the required type, as one would expect.
\begin{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
-> OutType
-> [OutVar]
-> 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 }
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 ()
checkTyKind tyvar arg_ty
| isSuperKind tyvar_kind
= lintKind arg_ty
| otherwise
= do { arg_kind <- lintType arg_ty
; unless (arg_kind `isSubKind` tyvar_kind)
(addErrL (mkKindErrMsg tyvar arg_ty $$ (text "xx" <+> ppr arg_kind))) }
where
tyvar_kind = tyVarKind tyvar
checkDeadIdOcc :: Id -> LintM ()
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}
%************************************************************************
%* *
\subsection[lintCoreAlts]{lintCoreAlts}
%* *
%************************************************************************
\begin{code}
checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
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 || null alts)
(nonExhaustiveAltsMsg e) }
where
(con_alts, maybe_deflt) = findDefault alts
increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
increasing_tag _ = True
non_deflt (DEFAULT, _, _) = False
non_deflt _ = True
is_infinite_ty = case tyConAppTyCon_maybe ty of
Nothing -> False
Just tycon -> isPrimTyCon tycon
\end{code}
\begin{code}
checkAltExpr :: CoreExpr -> OutType -> LintM ()
checkAltExpr expr ann_ty
= do { actual_ty <- lintCoreExpr expr
; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
lintCoreAlt :: OutType
-> OutType
-> CoreAlt
-> LintM ()
lintCoreAlt _ alt_ty (DEFAULT, args, rhs) =
do { checkL (null args) (mkDefaultArgsMsg args)
; checkAltExpr rhs alt_ty }
lintCoreAlt scrut_ty alt_ty (LitAlt lit, args, rhs)
| litIsLifted lit
= failWithL integerScrutinisedMsg
| otherwise
= 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)
| isNewTyCon (dataConTyCon con)
= addErrL (mkNewTyDataConAltMsg scrut_ty alt)
| Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
= addLoc (CaseAlt alt) $ do
{
checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
; lintBinders args $ \ args' -> do
{ addLoc (CasePat alt) (lintAltBinders scrut_ty con_payload_ty args')
; checkAltExpr rhs alt_ty } }
| otherwise
= addErrL (mkBadAltMsg scrut_ty alt)
\end{code}
%************************************************************************
%* *
\subsection[lint-types]{Types}
%* *
%************************************************************************
\begin{code}
lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
lintBinders [] linterF = linterF []
lintBinders (var:vars) linterF = lintBinder var $ \var' ->
lintBinders vars $ \ vars' ->
linterF (var':vars')
lintBinder :: Var -> (Var -> LintM a) -> LintM a
lintBinder var linterF
| isId var = lintIdBndr var linterF
| otherwise = lintTyBndr var linterF
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
lintIdBndr id linterF
= do { lintAndScopeId id $ \id' -> linterF id' }
lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
lintAndScopeIds ids linterF
= go ids
where
go [] = linterF []
go (id:ids) = lintAndScopeId id $ \id ->
lintAndScopeIds ids $ \ids ->
linterF (id:ids)
lintAndScopeId :: InVar -> (OutVar -> LintM a) -> LintM a
lintAndScopeId id linterF
= do { ty <- lintInTy (idType id)
; let id' = setIdType id ty
; addInScopeVar id' $ (linterF id') }
\end{code}
%************************************************************************
%* *
Types and kinds
%* *
%************************************************************************
We have a single linter for types and kinds. That is convenient
because sometimes it's not clear whether the thing we are looking
at is a type or a kind.
\begin{code}
lintInTy :: InType -> LintM LintedType
lintInTy ty
= addLoc (InType ty) $
do { ty' <- applySubstTy ty
; _k <- lintType ty'
; return ty' }
lintTyBndrKind :: OutTyVar -> LintM ()
lintTyBndrKind tv = lintKind (tyVarKind tv)
lintType :: OutType -> LintM LintedKind
lintType (TyVarTy tv)
= do { checkTyCoVarInScope tv
; return (tyVarKind tv) }
lintType ty@(AppTy t1 t2)
= do { k1 <- lintType t1
; k2 <- lintType t2
; lint_ty_app ty k1 [(t2,k2)] }
lintType ty@(FunTy t1 t2)
= do { k1 <- lintType t1
; k2 <- lintType t2
; lintArrow (ptext (sLit "type or kind") <+> quotes (ppr ty)) k1 k2 }
lintType ty@(TyConApp tc tys)
| Just ty' <- coreView ty
= lintType ty'
| isUnLiftedTyCon tc || isSynTyCon tc
, length tys < tyConArity tc
= failWithL (hang (ptext (sLit "Un-saturated type application")) 2 (ppr ty))
| otherwise
= do { ks <- mapM lintType tys
; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
lintType (ForAllTy tv ty)
= do { lintTyBndrKind tv
; addInScopeVar tv (lintType ty) }
lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
\end{code}
\begin{code}
lintKind :: OutKind -> LintM ()
lintKind k = do { sk <- lintType k
; unless (isSuperKind sk)
(addErrL (hang (ptext (sLit "Ill-kinded kind:") <+> ppr k)
2 (ptext (sLit "has kind:") <+> ppr sk))) }
\end{code}
\begin{code}
lintArrow :: SDoc -> LintedKind -> LintedKind -> LintM LintedKind
lintArrow what k1 k2
| isSuperKind k1
= return superKind
| otherwise
= do { unless (okArrowArgKind k1) (addErrL (msg (ptext (sLit "argument")) k1))
; unless (okArrowResultKind k2) (addErrL (msg (ptext (sLit "result")) k2))
; return liftedTypeKind }
where
msg ar k
= vcat [ hang (ptext (sLit "Ill-kinded") <+> ar)
2 (ptext (sLit "in") <+> what)
, what <+> ptext (sLit "kind:") <+> ppr k ]
lint_ty_app :: Type -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
lint_ty_app ty k tys
= lint_app (ptext (sLit "type") <+> quotes (ppr ty)) k tys
lint_co_app :: Coercion -> LintedKind -> [(LintedType,LintedKind)] -> LintM LintedKind
lint_co_app ty k tys
= lint_app (ptext (sLit "coercion") <+> quotes (ppr ty)) k tys
lintTyLit :: TyLit -> LintM ()
lintTyLit (NumTyLit n)
| n >= 0 = return ()
| otherwise = failWithL msg
where msg = ptext (sLit "Negative type literal:") <+> integer n
lintTyLit (StrTyLit _) = return ()
lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind
lint_app doc kfn kas
= foldlM go_app kfn kas
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 kas) ]
go_app kfn ka
| Just kfn' <- coreView kfn
= go_app kfn' ka
go_app (FunTy kfa kfb) (_,ka)
= do { unless (ka `isSubKind` kfa) (addErrL fail_msg)
; return kfb }
go_app (ForAllTy kv kfn) (ta,ka)
= do { unless (ka `isSubKind` tyVarKind kv) (addErrL fail_msg)
; return (substKiWith [kv] [ta] kfn) }
go_app _ _ = failWithL fail_msg
\end{code}
%************************************************************************
%* *
Linting coercions
%* *
%************************************************************************
\begin{code}
lintInCo :: InCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
lintInCo co
= addLoc (InCo co) $
do { co' <- applySubstCo co
; lintCoercion co' }
lintCoercion :: OutCoercion -> LintM (LintedKind, LintedType, LintedType, Role)
lintCoercion (Refl r ty)
= do { k <- lintType ty
; return (k, ty, ty, r) }
lintCoercion co@(TyConAppCo r tc cos)
| tc `hasKey` funTyConKey
, [co1,co2] <- cos
= do { (k1,s1,t1,r1) <- lintCoercion co1
; (k2,s2,t2,r2) <- lintCoercion co2
; rk <- lintArrow (ptext (sLit "coercion") <+> quotes (ppr co)) k1 k2
; checkRole co1 r r1
; checkRole co2 r r2
; return (rk, mkFunTy s1 s2, mkFunTy t1 t2, r) }
| Just {} <- synTyConDefn_maybe tc
= failWithL (ptext (sLit "Synonym in TyConAppCo:") <+> ppr co)
| otherwise
= do { (ks,ss,ts,rs) <- mapAndUnzip4M lintCoercion cos
; rk <- lint_co_app co (tyConKind tc) (ss `zip` ks)
; _ <- zipWith3M checkRole cos (tyConRolesX r tc) rs
; return (rk, mkTyConApp tc ss, mkTyConApp tc ts, r) }
lintCoercion co@(AppCo co1 co2)
= do { (k1,s1,t1,r1) <- lintCoercion co1
; (k2,s2,t2,r2) <- lintCoercion co2
; rk <- lint_co_app co k1 [(s2,k2)]
; if r1 == Phantom
then checkL (r2 == Phantom || r2 == Nominal)
(ptext (sLit "Second argument in AppCo cannot be R:") $$
ppr co)
else checkRole co Nominal r2
; return (rk, mkAppTy s1 s2, mkAppTy t1 t2, r1) }
lintCoercion (ForAllCo tv co)
= do { lintTyBndrKind tv
; (k, s, t, r) <- addInScopeVar tv (lintCoercion co)
; return (k, mkForAllTy tv s, mkForAllTy tv t, r) }
lintCoercion (CoVarCo cv)
| not (isCoVar cv)
= failWithL (hang (ptext (sLit "Bad CoVarCo:") <+> ppr cv)
2 (ptext (sLit "With offending type:") <+> ppr (varType cv)))
| otherwise
= do { checkTyCoVarInScope cv
; cv' <- lookupIdInScope cv
; let (s,t) = coVarKind cv'
k = typeKind s
r = coVarRole cv'
; when (isSuperKind k) $
do { checkL (r == Nominal) (hang (ptext (sLit "Non-nominal kind equality"))
2 (ppr cv))
; checkL (s `eqKind` t) (hang (ptext (sLit "Non-refl kind equality"))
2 (ppr cv)) }
; return (k, s, t, r) }
lintCoercion (UnivCo r ty1 ty2)
= do { k1 <- lintType ty1
; _k2 <- lintType ty2
; return (k1, ty1, ty2, r) }
lintCoercion (SymCo co)
= do { (k, ty1, ty2, r) <- lintCoercion co
; return (k, ty2, ty1, r) }
lintCoercion co@(TransCo co1 co2)
= do { (k1, ty1a, ty1b, r1) <- lintCoercion co1
; (_, ty2a, ty2b, r2) <- 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]))
; checkRole co r1 r2
; return (k1, ty1a, ty2b, r1) }
lintCoercion the_co@(NthCo n co)
= do { (_,s,t,r) <- lintCoercion co
; case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
(Just (tc_s, tys_s), Just (tc_t, tys_t))
| tc_s == tc_t
, tys_s `equalLength` tys_t
, n < length tys_s
-> return (ks, ts, tt, tr)
where
ts = getNth tys_s n
tt = getNth tys_t n
tr = nthRole r tc_s n
ks = typeKind ts
_ -> failWithL (hang (ptext (sLit "Bad getNth:"))
2 (ppr the_co $$ ppr s $$ ppr t)) }
lintCoercion the_co@(LRCo lr co)
= do { (_,s,t,r) <- lintCoercion co
; checkRole co Nominal r
; case (splitAppTy_maybe s, splitAppTy_maybe t) of
(Just s_pr, Just t_pr)
-> return (k, s_pick, t_pick, Nominal)
where
s_pick = pickLR lr s_pr
t_pick = pickLR lr t_pr
k = typeKind s_pick
_ -> failWithL (hang (ptext (sLit "Bad LRCo:"))
2 (ppr the_co $$ ppr s $$ ppr t)) }
lintCoercion (InstCo co arg_ty)
= do { (k,s,t,r) <- lintCoercion co
; arg_kind <- lintType arg_ty
; case (splitForAllTy_maybe s, splitForAllTy_maybe t) of
(Just (tv1,ty1), Just (tv2,ty2))
| arg_kind `isSubKind` tyVarKind tv1
-> return (k, substTyWith [tv1] [arg_ty] ty1,
substTyWith [tv2] [arg_ty] ty2, r)
| otherwise
-> failWithL (ptext (sLit "Kind mis-match in inst coercion"))
_ -> failWithL (ptext (sLit "Bad argument of inst")) }
lintCoercion co@(AxiomInstCo con ind cos)
= do { unless (0 <= ind && ind < brListLength (coAxiomBranches con))
(bad_ax (ptext (sLit "index out of range")))
; let CoAxBranch { cab_tvs = ktvs
, cab_roles = roles
, cab_lhs = lhs
, cab_rhs = rhs } = coAxiomNthBranch con ind
; unless (equalLength ktvs cos) (bad_ax (ptext (sLit "lengths")))
; in_scope <- getInScope
; let empty_subst = mkTvSubst in_scope emptyTvSubstEnv
; (subst_l, subst_r) <- foldlM check_ki
(empty_subst, empty_subst)
(zip3 ktvs roles cos)
; let lhs' = Type.substTys subst_l lhs
rhs' = Type.substTy subst_r rhs
; case checkAxInstCo co of
Just bad_branch -> bad_ax $ ptext (sLit "inconsistent with") <+> (pprCoAxBranch (coAxiomTyCon con) bad_branch)
Nothing -> return ()
; return (typeKind rhs', mkTyConApp (coAxiomTyCon con) lhs', rhs', coAxiomRole con) }
where
bad_ax what = addErrL (hang (ptext (sLit "Bad axiom application") <+> parens what)
2 (ppr co))
check_ki (subst_l, subst_r) (ktv, role, co)
= do { (k, t1, t2, r) <- lintCoercion co
; checkRole co role r
; let ktv_kind = Type.substTy subst_l (tyVarKind ktv)
; unless (k `isSubKind` ktv_kind)
(bad_ax (ptext (sLit "check_ki2") <+> vcat [ ppr co, ppr k, ppr ktv, ppr ktv_kind ] ))
; return (Type.extendTvSubst subst_l ktv t1,
Type.extendTvSubst subst_r ktv t2) }
lintCoercion co@(SubCo co')
= do { (k,s,t,r) <- lintCoercion co'
; checkRole co Nominal r
; return (k,s,t,Representational) }
lintCoercion this@(AxiomRuleCo co ts cs)
= do _ks <- mapM lintType ts
eqs <- mapM lintCoercion cs
let tyNum = length ts
case compare (coaxrTypeArity co) tyNum of
EQ -> return ()
LT -> err "Too many type arguments"
[ txt "expected" <+> int (coaxrTypeArity co)
, txt "provided" <+> int tyNum ]
GT -> err "Not enough type arguments"
[ txt "expected" <+> int (coaxrTypeArity co)
, txt "provided" <+> int tyNum ]
checkRoles 0 (coaxrAsmpRoles co) eqs
case coaxrProves co ts [ Pair l r | (_,l,r,_) <- eqs ] of
Nothing -> err "Malformed use of AxiomRuleCo" [ ppr this ]
Just (Pair l r) ->
do kL <- lintType l
kR <- lintType r
unless (eqKind kL kR)
$ err "Kind error in CoAxiomRule"
[ppr kL <+> txt "/=" <+> ppr kR]
return (kL, l, r, coaxrRole co)
where
txt = ptext . sLit
err m xs = failWithL $
hang (txt m) 2 $ vcat (txt "Rule:" <+> ppr (coaxrName co) : xs)
checkRoles n (e : es) ((_,_,_,r) : rs)
| e == r = checkRoles (n+1) es rs
| otherwise = err "Argument roles mismatch"
[ txt "In argument:" <+> int (n+1)
, txt "Expected:" <+> ppr e
, txt "Found:" <+> ppr r ]
checkRoles _ [] [] = return ()
checkRoles n [] rs = err "Too many coercion arguments"
[ txt "Expected:" <+> int n
, txt "Provided:" <+> int (n + length rs) ]
checkRoles n es [] = err "Not enough coercion arguments"
[ txt "Expected:" <+> int (n + length es)
, txt "Provided:" <+> int n ]
\end{code}
%************************************************************************
%* *
\subsection[lint-monad]{The Lint monad}
%* *
%************************************************************************
\begin{code}
newtype LintM a =
LintM { unLintM ::
[LintLocInfo] ->
TvSubst ->
WarnsAndErrs ->
(Maybe a, WarnsAndErrs) }
type WarnsAndErrs = (Bag MsgDoc, Bag MsgDoc)
instance Functor LintM where
fmap = liftM
instance Applicative LintM where
pure = return
(<*>) = ap
instance Monad LintM where
return x = LintM (\ _ _ errs -> (Just x, errs))
fail err = failWithL (text err)
m >>= k = LintM (\ loc subst errs ->
let (res, errs') = unLintM m loc subst errs in
case res of
Just r -> unLintM (k r) loc subst errs'
Nothing -> (Nothing, errs'))
data LintLocInfo
= RhsOf Id
| LambdaBodyOf Id
| BodyOfLetRec [Id]
| CaseAlt CoreAlt
| CasePat CoreAlt
| AnExpr CoreExpr
| ImportedUnfolding SrcLoc
| TopLevelBindings
| InType Type
| InCo Coercion
\end{code}
\begin{code}
initL :: LintM a -> WarnsAndErrs
initL m
= case unLintM m [] emptyTvSubst (emptyBag, emptyBag) of
(_, errs) -> errs
\end{code}
\begin{code}
checkL :: Bool -> MsgDoc -> LintM ()
checkL True _ = return ()
checkL False msg = failWithL msg
failWithL :: MsgDoc -> LintM a
failWithL msg = LintM $ \ loc subst (warns,errs) ->
(Nothing, (warns, addMsg subst errs msg loc))
addErrL :: MsgDoc -> LintM ()
addErrL msg = LintM $ \ loc subst (warns,errs) ->
(Just (), (warns, addMsg subst errs msg loc))
addWarnL :: MsgDoc -> LintM ()
addWarnL msg = LintM $ \ loc subst (warns,errs) ->
(Just (), (addMsg subst warns msg loc, errs))
addMsg :: TvSubst -> Bag MsgDoc -> MsgDoc -> [LintLocInfo] -> Bag MsgDoc
addMsg subst msgs msg locs
= ASSERT( notNull locs )
msgs `snocBag` mk_msg msg
where
(loc, cxt1) = dumpLoc (head locs)
cxts = [snd (dumpLoc loc) | loc <- locs]
context | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
ptext (sLit "Substitution:") <+> ppr subst
| otherwise = cxt1
mk_msg msg = mkLocMessage SevWarning (mkSrcSpan loc loc) (context $$ msg)
addLoc :: LintLocInfo -> LintM a -> LintM a
addLoc extra_loc m =
LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
inCasePat :: LintM Bool
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
= 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 =
LintM (\ loc _ errs -> unLintM m loc subst' errs)
getTvSubst :: LintM TvSubst
getTvSubst = LintM (\ _ subst errs -> (Just subst, errs))
getInScope :: LintM InScopeSet
getInScope = LintM (\ _ subst errs -> (Just (getTvInScope subst), errs))
applySubstTy :: InType -> LintM OutType
applySubstTy ty = do { subst <- getTvSubst; return (Type.substTy subst ty) }
applySubstCo :: InCoercion -> LintM OutCoercion
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 (Type.extendTvSubst subst tv ty) errs)
\end{code}
\begin{code}
lookupIdInScope :: Id -> LintM Id
lookupIdInScope id
| not (mustHaveLocalBinding id)
= return id
| otherwise
= do { subst <- getTvSubst
; case lookupInScope (getTvInScope subst) id of
Just v -> return v
Nothing -> do { addErrL out_of_scope
; return id } }
where
out_of_scope = pprBndr LetBind id <+> ptext (sLit "is out of scope")
oneTupleDataConId :: Id
oneTupleDataConId = dataConWorkId (tupleCon BoxedTuple 1)
checkBndrIdInScope :: Var -> Var -> LintM ()
checkBndrIdInScope binder id
= checkInScope msg id
where
msg = ptext (sLit "is out of scope inside info for") <+>
ppr binder
checkTyCoVarInScope :: Var -> LintM ()
checkTyCoVarInScope v = checkInScope (ptext (sLit "is out of scope")) v
checkInScope :: SDoc -> Var -> LintM ()
checkInScope loc_msg var =
do { subst <- getTvSubst
; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
(hsep [pprBndr LetBind var, loc_msg]) }
checkTys :: OutType -> OutType -> MsgDoc -> LintM ()
checkTys ty1 ty2 msg = checkL (ty1 `eqType` ty2) msg
checkRole :: Coercion
-> Role
-> Role
-> LintM ()
checkRole co r1 r2
= checkL (r1 == r2)
(ptext (sLit "Role incompatibility: expected") <+> ppr r1 <> comma <+>
ptext (sLit "got") <+> ppr r2 $$
ptext (sLit "in") <+> ppr co)
\end{code}
%************************************************************************
%* *
\subsection{Error messages}
%* *
%************************************************************************
\begin{code}
dumpLoc :: LintLocInfo -> (SrcLoc, SDoc)
dumpLoc (RhsOf v)
= (getSrcLoc v, brackets (ptext (sLit "RHS of") <+> pp_binders [v]))
dumpLoc (LambdaBodyOf b)
= (getSrcLoc b, brackets (ptext (sLit "in body of lambda with binder") <+> pp_binder b))
dumpLoc (BodyOfLetRec [])
= (noSrcLoc, brackets (ptext (sLit "In body of a letrec with no binders")))
dumpLoc (BodyOfLetRec bs@(_:_))
= ( getSrcLoc (head bs), brackets (ptext (sLit "in body of letrec with binders") <+> pp_binders bs))
dumpLoc (AnExpr e)
= (noSrcLoc, text "In the expression:" <+> ppr e)
dumpLoc (CaseAlt (con, args, _))
= (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
dumpLoc (CasePat (con, args, _))
= (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
dumpLoc (ImportedUnfolding locn)
= (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))
pp_binder :: Var -> SDoc
pp_binder b | isId b = hsep [ppr b, dcolon, ppr (idType b)]
| otherwise = hsep [ppr b, dcolon, ppr (tyVarKind b)]
\end{code}
\begin{code}
mkDefaultArgsMsg :: [Var] -> MsgDoc
mkDefaultArgsMsg args
= hang (text "DEFAULT case with binders")
4 (ppr args)
mkCaseAltMsg :: CoreExpr -> Type -> Type -> MsgDoc
mkCaseAltMsg e ty1 ty2
= hang (text "Type of case alternatives not the same as the annotation on case:")
4 (vcat [ppr ty1, ppr ty2, ppr e])
mkScrutMsg :: Id -> Type -> Type -> TvSubst -> MsgDoc
mkScrutMsg var var_ty scrut_ty subst
= vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
text "Result binder type:" <+> ppr var_ty,
text "Scrutinee type:" <+> ppr scrut_ty,
hsep [ptext (sLit "Current TV subst"), ppr subst]]
mkNonDefltMsg, mkNonIncreasingAltsMsg :: CoreExpr -> MsgDoc
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 -> MsgDoc
nonExhaustiveAltsMsg e
= hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
mkBadConMsg :: TyCon -> DataCon -> MsgDoc
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 -> MsgDoc
mkBadPatMsg con_result_ty scrut_ty
= vcat [
text "In a case alternative, pattern result type doesn't match scrutinee type:",
text "Pattern result type:" <+> ppr con_result_ty,
text "Scrutinee type:" <+> ppr scrut_ty
]
integerScrutinisedMsg :: MsgDoc
integerScrutinisedMsg
= text "In a LitAlt, the literal is lifted (probably Integer)"
mkBadAltMsg :: Type -> CoreAlt -> MsgDoc
mkBadAltMsg scrut_ty alt
= vcat [ text "Data alternative when scrutinee is not a tycon application",
text "Scrutinee type:" <+> ppr scrut_ty,
text "Alternative:" <+> pprCoreAlt alt ]
mkNewTyDataConAltMsg :: Type -> CoreAlt -> MsgDoc
mkNewTyDataConAltMsg scrut_ty alt
= vcat [ text "Data alternative for newtype datacon",
text "Scrutinee type:" <+> ppr scrut_ty,
text "Alternative:" <+> pprCoreAlt alt ]
mkAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
mkAppMsg fun_ty arg_ty arg
= vcat [ptext (sLit "Argument value doesn't match argument type:"),
hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
hang (ptext (sLit "Arg:")) 4 (ppr arg)]
mkNonFunAppMsg :: Type -> Type -> CoreExpr -> MsgDoc
mkNonFunAppMsg fun_ty arg_ty arg
= vcat [ptext (sLit "Non-function type in function position"),
hang (ptext (sLit "Fun type:")) 4 (ppr fun_ty),
hang (ptext (sLit "Arg type:")) 4 (ppr arg_ty),
hang (ptext (sLit "Arg:")) 4 (ppr arg)]
mkLetErr :: TyVar -> CoreExpr -> MsgDoc
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)]
mkTyAppMsg :: Type -> Type -> MsgDoc
mkTyAppMsg ty arg_ty
= 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_ty <+> dcolon <+> ppr (typeKind arg_ty))]
mkRhsMsg :: Id -> SDoc -> Type -> MsgDoc
mkRhsMsg binder what ty
= vcat
[hsep [ptext (sLit "The type of this binder doesn't match the type of its") <+> what <> colon,
ppr binder],
hsep [ptext (sLit "Binder's type:"), ppr (idType binder)],
hsep [ptext (sLit "Rhs type:"), ppr ty]]
mkRhsPrimMsg :: Id -> CoreExpr -> MsgDoc
mkRhsPrimMsg binder _rhs
= vcat [hsep [ptext (sLit "The type of this binder is primitive:"),
ppr binder],
hsep [ptext (sLit "Binder's type:"), ppr (idType binder)]
]
mkStrictMsg :: Id -> MsgDoc
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 (idDemandInfo binder)]
]
mkNonTopExportedMsg :: Id -> MsgDoc
mkNonTopExportedMsg binder
= hsep [ptext (sLit "Non-top-level binder is marked as exported:"), ppr binder]
mkNonTopExternalNameMsg :: Id -> MsgDoc
mkNonTopExternalNameMsg binder
= hsep [ptext (sLit "Non-top-level binder has an external name:"), ppr binder]
mkKindErrMsg :: TyVar -> Type -> MsgDoc
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))]
mkCastErr :: CoreExpr -> Coercion -> Type -> Type -> MsgDoc
mkCastErr expr co from_ty expr_ty
= vcat [ptext (sLit "From-type of Cast differs from type of enclosed expression"),
ptext (sLit "From-type:") <+> ppr from_ty,
ptext (sLit "Type of enclosed expr:") <+> ppr expr_ty,
ptext (sLit "Actual enclosed expr:") <+> ppr expr,
ptext (sLit "Coercion used in cast:") <+> ppr co
]
dupVars :: [[Var]] -> MsgDoc
dupVars vars
= hang (ptext (sLit "Duplicate variables brought into scope"))
2 (ppr vars)
dupExtVars :: [[Name]] -> MsgDoc
dupExtVars vars
= hang (ptext (sLit "Duplicate top-level variables with the same qualified name"))
2 (ppr vars)
\end{code}