Commit a262ea49 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Significant refactor of Lint

This refactoring of Lint was triggered by #17923, which is
fixed by this patch.

The main change is this.  Instead of
   lintType :: Type -> LintM LintedKind
we now have
   lintType :: Type -> LintM LintedType

Previously, all of typeKind was effectively duplicate in lintType.
Moreover, since we have an ambient substitution, we still had to
apply the substition here and there, sometimes more than once. It
was all very tricky, in the end, and made my head hurt.

Now, lintType returns a fully linted type, with all substitutions
performed on it.  This is much simpler.

The same thing is needed for Coercions.  Instead of
  lintCoercion :: OutCoercion
               -> LintM (LintedKind, LintedKind,
                         LintedType, LintedType, Role)
we now have
  lintCoercion :: Coercion -> LintM LintedCoercion

Much simpler!  The code is shorter and less bug-prone.

There are a lot of knock on effects.  But life is now better.
parent 6d172e63
Pipeline #17180 failed with stages
in 207 minutes and 40 seconds
......@@ -8,7 +8,7 @@ See Note [Core Lint guarantee].
-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE ScopedTypeVariables, DeriveFunctor #-}
module GHC.Core.Lint (
lintCoreBindings, lintUnfolding,
......@@ -33,7 +33,6 @@ import GHC.Core.Op.Monad
import Bag
import Literal
import GHC.Core.DataCon
import TysWiredIn
import TysPrim
import TcType ( isFloatingTy )
import Var
......@@ -461,14 +460,17 @@ lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc,
lintCoreBindings dflags pass local_in_scope binds
= initL dflags flags local_in_scope $
addLoc TopLevelBindings $
lintLetBndrs TopLevel binders $
-- Put all the top-level binders in scope at the start
-- This is because transformation rules can bring something
-- into use 'unexpectedly'
do { checkL (null dups) (dupVars dups)
; checkL (null ext_dups) (dupExtVars ext_dups)
; mapM lint_bind binds }
; lintRecBindings TopLevel all_pairs $
return () }
where
all_pairs = flattenBinds binds
-- Put all the top-level binders in scope at the start
-- This is because transformation rules can bring something
-- into use 'unexpectedly'; see Note [Glomming] in OccurAnal
binders = map fst all_pairs
flags = defaultLintFlags
{ lf_check_global_ids = check_globals
, lf_check_inline_loop_breakers = check_lbs
......@@ -494,7 +496,6 @@ lintCoreBindings dflags pass local_in_scope binds
CorePrep -> AllowAtTopLevel
_ -> AllowAnywhere
binders = bindersOfBinds binds
(_, dups) = removeDups compare binders
-- dups_ext checks for names with different uniques
......@@ -509,11 +510,6 @@ lintCoreBindings dflags pass local_in_scope binds
= compare (m1, nameOccName n1) (m2, nameOccName n2)
| otherwise = LT
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lint_bind (Rec prs) = mapM_ (lintSingleBinding TopLevel Recursive) prs
lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
{-
************************************************************************
* *
......@@ -576,28 +572,32 @@ lintExpr dflags vars expr
Check a core binding, returning the list of variables bound.
-}
lintSingleBinding :: TopLevelFlag -> RecFlag -> (Id, CoreExpr) -> LintM ()
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
= addLoc (RhsOf binder) $
-- Check the rhs
do { ty <- lintRhs binder rhs
; binder_ty <- applySubstTy (idType binder)
; ensureEqTys binder_ty ty (mkRhsMsg binder (text "RHS") ty)
lintRecBindings :: TopLevelFlag -> [(Id, CoreExpr)]
-> LintM a -> LintM a
lintRecBindings top_lvl pairs thing_inside
= lintIdBndrs top_lvl bndrs $ \ bndrs' ->
do { zipWithM_ lint_pair bndrs' rhss
; thing_inside }
where
(bndrs, rhss) = unzip pairs
lint_pair bndr' rhs
= addLoc (RhsOf bndr') $
do { rhs_ty <- lintRhs bndr' rhs -- Check the rhs
; lintLetBind top_lvl Recursive bndr' rhs rhs_ty }
lintLetBind :: TopLevelFlag -> RecFlag -> LintedId
-> CoreExpr -> LintedType -> LintM ()
-- Binder's type, and the RHS, have already been linted
-- This function checks other invariants
lintLetBind top_lvl rec_flag binder rhs rhs_ty
= do { let binder_ty = idType binder
; ensureEqTys binder_ty rhs_ty (mkRhsMsg binder (text "RHS") rhs_ty)
-- If the binding is for a CoVar, the RHS should be (Coercion co)
-- See Note [Core type and coercion invariant] in GHC.Core
; checkL (not (isCoVar binder) || isCoArg rhs)
(mkLetErr binder rhs)
-- Check that it's not levity-polymorphic
-- Do this first, because otherwise isUnliftedType panics
-- Annoyingly, this duplicates the test in lintIdBdr,
-- because for non-rec lets we call lintSingleBinding first
; checkL (isJoinId binder || not (isTypeLevPoly binder_ty))
(badBndrTyMsg binder (text "levity-polymorphic"))
-- Check the let/app invariant
-- See Note [Core let/app invariant] in GHC.Core
; checkL ( isJoinId binder
......@@ -610,14 +610,14 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
-- demanded. Primitive string literals are exempt as there is no
-- computation to perform, see Note [Core top-level string literals].
; checkL (not (isStrictId binder)
|| (isNonRec rec_flag && not (isTopLevel top_lvl_flag))
|| (isNonRec rec_flag && not (isTopLevel top_lvl))
|| exprIsTickedString rhs)
(mkStrictMsg binder)
-- Check that if the binder is at the top level and has type Addr#,
-- that it is a string literal, see
-- Note [Core top-level string literals].
; checkL (not (isTopLevel top_lvl_flag && binder_ty `eqType` addrPrimTy)
; checkL (not (isTopLevel top_lvl && binder_ty `eqType` addrPrimTy)
|| exprIsTickedString rhs)
(mkTopNonLitStrMsg binder)
......@@ -674,7 +674,9 @@ lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
-- join point.
--
-- See Note [Checking StaticPtrs].
lintRhs :: Id -> CoreExpr -> LintM OutType
lintRhs :: Id -> CoreExpr -> LintM LintedType
-- NB: the Id can be Linted or not -- it's only used for
-- its OccInfo and join-pointer-hood
lintRhs bndr rhs
| Just arity <- isJoinId_maybe bndr
= lint_join_lams arity arity True rhs
......@@ -761,13 +763,14 @@ hurts us here.
************************************************************************
-}
-- For OutType, OutKind, the substitution has been applied,
-- but has not been linted yet
type LintedType = Type -- Substitution applied, and type is linted
type LintedKind = Kind
-- Linted things: substitution applied, and type is linted
type LintedType = Type
type LintedKind = Kind
type LintedCoercion = Coercion
type LintedTyCoVar = TyCoVar
type LintedId = Id
lintCoreExpr :: CoreExpr -> LintM OutType
lintCoreExpr :: CoreExpr -> LintM LintedType
-- The returned type has the substitution from the monad
-- already applied to it:
-- lintCoreExpr e subst = exprType (subst e)
......@@ -776,18 +779,20 @@ lintCoreExpr :: CoreExpr -> LintM OutType
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoreExpr (Var var)
= lintVarOcc var 0
= lintIdOcc var 0
lintCoreExpr (Lit lit)
= return (literalType lit)
lintCoreExpr (Cast expr co)
= do { expr_ty <- markAllJoinsBad $ lintCoreExpr expr
; co' <- applySubstCo co
; (_, k2, from_ty, to_ty, r) <- lintCoercion co'
; checkValueKind k2 (text "target of cast" <+> quotes (ppr co))
; lintRole co' Representational r
; co' <- lintCoercion co
; let (Pair from_ty to_ty, role) = coercionKindRole co'
; checkValueType to_ty $
text "target of cast" <+> quotes (ppr co')
; lintRole co' Representational role
; ensureEqTys from_ty expr_ty (mkCastErr expr co' from_ty expr_ty)
; return to_ty }
......@@ -809,7 +814,7 @@ lintCoreExpr (Tick tickish expr)
lintCoreExpr (Let (NonRec tv (Type ty)) body)
| isTyVar tv
= -- See Note [Linting type lets]
do { ty' <- applySubstTy ty
do { ty' <- lintType ty
; lintTyBndr tv $ \ tv' ->
do { addLoc (RhsOf tv) $ lintTyKind tv' ty'
-- Now extend the substitution so we
......@@ -820,33 +825,34 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body)
lintCoreExpr (Let (NonRec bndr rhs) body)
| isId bndr
= do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
; addLoc (BodyOfLetRec [bndr])
(lintBinder LetBind bndr $ \_ ->
addGoodJoins [bndr] $
lintCoreExpr body) }
= do { -- First Lint the RHS, before bringing the binder into scope
rhs_ty <- lintRhs bndr rhs
-- Now lint the binder
; lintBinder LetBind bndr $ \bndr' ->
do { lintLetBind NotTopLevel NonRecursive bndr' rhs rhs_ty
; addLoc (BodyOfLetRec [bndr]) (lintCoreExpr body) } }
| otherwise
= failWithL (mkLetErr bndr rhs) -- Not quite accurate
lintCoreExpr e@(Let (Rec pairs) body)
= lintLetBndrs NotTopLevel bndrs $
addGoodJoins bndrs $
do { -- Check that the list of pairs is non-empty
= do { -- Check that the list of pairs is non-empty
checkL (not (null pairs)) (emptyRec e)
-- Check that there are no duplicated binders
; let (_, dups) = removeDups compare bndrs
; checkL (null dups) (dupVars dups)
-- Check that either all the binders are joins, or none
; checkL (all isJoinId bndrs || all (not . isJoinId) bndrs) $
mkInconsistentRecMsg bndrs
mkInconsistentRecMsg bndrs
; mapM_ (lintSingleBinding NotTopLevel Recursive) pairs
; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
; lintRecBindings NotTopLevel pairs $
addLoc (BodyOfLetRec bndrs) $
lintCoreExpr body }
where
bndrs = map fst pairs
(_, dups) = removeDups compare bndrs
lintCoreExpr e@(App _ _)
= do { fun_ty <- lintCoreFun fun (length args)
......@@ -867,23 +873,35 @@ lintCoreExpr (Type ty)
= failWithL (text "Type found as expression" <+> ppr ty)
lintCoreExpr (Coercion co)
= do { (k1, k2, ty1, ty2, role) <- lintInCo co
; return (mkHeteroCoercionType role k1 k2 ty1 ty2) }
= do { co' <- addLoc (InCo co) $
lintCoercion co
; return (coercionType co') }
----------------------
lintVarOcc :: Var -> Int -- Number of arguments (type or value) being passed
-> LintM Type -- returns type of the *variable*
lintVarOcc var nargs
= do { checkL (isNonCoVarId var)
lintIdOcc :: Var -> Int -- Number of arguments (type or value) being passed
-> LintM LintedType -- returns type of the *variable*
lintIdOcc var nargs
= addLoc (OccOf var) $
do { checkL (isNonCoVarId var)
(text "Non term variable" <+> ppr var)
-- See GHC.Core Note [Variable occurrences in Core]
-- Check that the type of the occurrence is the same
-- as the type of the binding site
; ty <- applySubstTy (idType var)
; var' <- lookupIdInScope var
; let ty' = idType var'
; ensureEqTys ty ty' $ mkBndrOccTypeMismatchMsg var' var ty' ty
-- as the type of the binding site. The inScopeIds are
-- /un-substituted/, so this checks that the occurrence type
-- is identical to the binder type.
-- This makes things much easier for things like:
-- /\a. \(x::Maybe a). /\a. ...(x::Maybe a)...
-- The "::Maybe a" on the occurrence is referring to the /outer/ a.
-- If we compared /substituted/ types we'd risk comparing
-- (Maybe a) from the binding site with bogus (Maybe a1) from
-- the occurrence site. Comparing un-substituted types finesses
-- this altogether
; (bndr, linted_bndr_ty) <- lookupIdInScope var
; let occ_ty = idType var
bndr_ty = idType bndr
; ensureEqTys occ_ty bndr_ty $
mkBndrOccTypeMismatchMsg bndr var bndr_ty occ_ty
-- Check for a nested occurrence of the StaticPtr constructor.
-- See Note [Checking StaticPtrs].
......@@ -895,13 +913,13 @@ lintVarOcc var nargs
; checkDeadIdOcc var
; checkJoinOcc var nargs
; return (idType var') }
; return linted_bndr_ty }
lintCoreFun :: CoreExpr
-> Int -- Number of arguments (type or val) being passed
-> LintM Type -- Returns type of the *function*
-> Int -- Number of arguments (type or val) being passed
-> LintM LintedType -- Returns type of the *function*
lintCoreFun (Var var) nargs
= lintVarOcc var nargs
= lintIdOcc var nargs
lintCoreFun (Lam var body) nargs
-- Act like lintCoreExpr of Lam, but *don't* call markAllJoinsBad; see
......@@ -941,7 +959,9 @@ checkJoinOcc var n_args
= do { mb_join_arity_bndr <- lookupJoinId var
; case mb_join_arity_bndr of {
Nothing -> -- Binder is not a join point
addErrL (invalidJoinOcc var) ;
do { join_set <- getValidJoins
; addErrL (text "join set " <+> ppr join_set $$
invalidJoinOcc var) } ;
Just join_arity_bndr ->
......@@ -1038,15 +1058,15 @@ subtype of the required type, as one would expect.
-}
lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
lintCoreArgs :: LintedType -> [CoreArg] -> LintM LintedType
lintCoreArgs fun_ty args = foldM lintCoreArg fun_ty args
lintCoreArg :: OutType -> CoreArg -> LintM OutType
lintCoreArg :: LintedType -> CoreArg -> LintM LintedType
lintCoreArg fun_ty (Type arg_ty)
= do { checkL (not (isCoercionTy arg_ty))
(text "Unnecessary coercion-to-type injection:"
<+> ppr arg_ty)
; arg_ty' <- applySubstTy arg_ty
; arg_ty' <- lintType arg_ty
; lintTyApp fun_ty arg_ty' }
lintCoreArg fun_ty arg
......@@ -1060,11 +1080,12 @@ lintCoreArg fun_ty arg
; checkL (not (isUnliftedType arg_ty) || exprOkForSpeculation arg)
(mkLetAppMsg arg)
; lintValApp arg fun_ty arg_ty }
-----------------
lintAltBinders :: OutType -- Scrutinee type
-> OutType -- Constructor type
lintAltBinders :: LintedType -- Scrutinee type
-> LintedType -- Constructor type
-> [OutVar] -- Binders
-> LintM ()
-- If you edit this function, you may need to update the GHC formalism
......@@ -1080,7 +1101,7 @@ lintAltBinders scrut_ty con_ty (bndr:bndrs)
; lintAltBinders scrut_ty con_ty' bndrs }
-----------------
lintTyApp :: OutType -> OutType -> LintM OutType
lintTyApp :: LintedType -> LintedType -> LintM LintedType
lintTyApp fun_ty arg_ty
| Just (tv,body_ty) <- splitForAllTy_maybe fun_ty
= do { lintTyKind tv arg_ty
......@@ -1094,7 +1115,7 @@ lintTyApp fun_ty arg_ty
= failWithL (mkTyAppMsg fun_ty arg_ty)
-----------------
lintValApp :: CoreExpr -> OutType -> OutType -> LintM OutType
lintValApp :: CoreExpr -> LintedType -> LintedType -> LintM LintedType
lintValApp arg fun_ty arg_ty
| Just (arg,res) <- splitFunTy_maybe fun_ty
= do { ensureEqTys arg arg_ty err1
......@@ -1105,17 +1126,17 @@ lintValApp arg fun_ty arg_ty
err1 = mkAppMsg fun_ty arg_ty arg
err2 = mkNonFunAppMsg fun_ty arg_ty arg
lintTyKind :: OutTyVar -> OutType -> LintM ()
lintTyKind :: OutTyVar -> LintedType -> LintM ()
-- Both args have had substitution applied
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintTyKind tyvar arg_ty
= do { arg_kind <- lintType arg_ty
; unless (arg_kind `eqType` tyvar_kind)
(addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))) }
= unless (arg_kind `eqType` tyvar_kind) $
addErrL (mkKindErrMsg tyvar arg_ty $$ (text "Linted Arg kind:" <+> ppr arg_kind))
where
tyvar_kind = tyVarKind tyvar
arg_kind = typeKind arg_ty
{-
************************************************************************
......@@ -1125,7 +1146,7 @@ lintTyKind tyvar arg_ty
************************************************************************
-}
lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM OutType
lintCaseExpr :: CoreExpr -> Id -> Type -> [CoreAlt] -> LintM LintedType
lintCaseExpr scrut var alt_ty alts =
do { let e = Case scrut var alt_ty alts -- Just for error messages
......@@ -1134,10 +1155,10 @@ lintCaseExpr scrut var alt_ty alts =
-- See Note [Join points are less general than the paper]
-- in GHC.Core
; (alt_ty, _) <- addLoc (CaseTy scrut) $
lintInTy alt_ty
; (var_ty, _) <- addLoc (IdTy var) $
lintInTy (idType var)
; alt_ty <- addLoc (CaseTy scrut) $
lintValueType alt_ty
; var_ty <- addLoc (IdTy var) $
lintValueType (idType var)
-- We used to try to check whether a case expression with no
-- alternatives was legitimate, but this didn't work.
......@@ -1179,7 +1200,7 @@ lintCaseExpr scrut var alt_ty alts =
; checkCaseAlts e scrut_ty alts
; return alt_ty } }
checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
checkCaseAlts :: CoreExpr -> LintedType -> [CoreAlt] -> LintM ()
-- a) Check that the alts are non-empty
-- b1) Check that the DEFAULT comes first, if it exists
-- b2) Check that the others are in increasing order
......@@ -1219,14 +1240,14 @@ checkCaseAlts e ty alts =
Nothing -> False
Just tycon -> isPrimTyCon tycon
lintAltExpr :: CoreExpr -> OutType -> LintM ()
lintAltExpr :: CoreExpr -> LintedType -> LintM ()
lintAltExpr expr ann_ty
= do { actual_ty <- lintCoreExpr expr
; ensureEqTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
-- See GHC.Core Note [Case expression invariants] item (6)
lintCoreAlt :: OutType -- Type of scrutinee
-> OutType -- Type of the alternative
lintCoreAlt :: LintedType -- Type of scrutinee
-> LintedType -- Type of the alternative
-> CoreAlt
-> LintM ()
-- If you edit this function, you may need to update the GHC formalism
......@@ -1286,40 +1307,43 @@ lintBinders site (var:vars) linterF = lintBinder site var $ \var' ->
-- See Note [GHC Formalism]
lintBinder :: BindingSite -> Var -> (Var -> LintM a) -> LintM a
lintBinder site var linterF
| isTyVar var = lintTyBndr var linterF
| isCoVar var = lintCoBndr var linterF
| otherwise = lintIdBndr NotTopLevel site var linterF
| isTyCoVar var = lintTyCoBndr var linterF
| otherwise = lintIdBndr NotTopLevel site var linterF
lintTyBndr :: InTyVar -> (OutTyVar -> LintM a) -> LintM a
lintTyBndr tv thing_inside
= do { subst <- getTCvSubst
; let (subst', tv') = substTyVarBndr subst tv
; lintKind (varType tv')
; updateTCvSubst subst' (thing_inside tv') }
lintTyBndr :: TyVar -> (LintedTyCoVar -> LintM a) -> LintM a
lintTyBndr = lintTyCoBndr -- We could specialise it, I guess
-- lintCoBndr :: CoVar -> (LintedTyCoVar -> LintM a) -> LintM a
-- lintCoBndr = lintTyCoBndr -- We could specialise it, I guess
lintCoBndr :: InCoVar -> (OutCoVar -> LintM a) -> LintM a
lintCoBndr cv thing_inside
lintTyCoBndr :: TyCoVar -> (LintedTyCoVar -> LintM a) -> LintM a
lintTyCoBndr tcv thing_inside
= do { subst <- getTCvSubst
; let (subst', cv') = substCoVarBndr subst cv
; lintKind (varType cv')
; lintL (isCoVarType (varType cv'))
(text "CoVar with non-coercion type:" <+> pprTyVar cv)
; updateTCvSubst subst' (thing_inside cv') }
lintLetBndrs :: TopLevelFlag -> [Var] -> LintM a -> LintM a
lintLetBndrs top_lvl ids linterF
= go ids
; kind' <- lintType (varType tcv)
; let tcv' = uniqAway (getTCvInScope subst) $
setVarType tcv kind'
subst' = extendTCvSubstWithClone subst tcv tcv'
; when (isCoVar tcv) $
lintL (isCoVarType kind')
(text "CoVar with non-coercion type:" <+> pprTyVar tcv)
; updateTCvSubst subst' (thing_inside tcv') }
lintIdBndrs :: forall a. TopLevelFlag -> [Id] -> ([LintedId] -> LintM a) -> LintM a
lintIdBndrs top_lvl ids thing_inside
= go ids thing_inside
where
go [] = linterF
go (id:ids) = lintIdBndr top_lvl LetBind id $ \_ ->
go ids
go :: [Id] -> ([Id] -> LintM a) -> LintM a
go [] thing_inside = thing_inside []
go (id:ids) thing_inside = lintIdBndr top_lvl LetBind id $ \id' ->
go ids $ \ids' ->
thing_inside (id' : ids')
lintIdBndr :: TopLevelFlag -> BindingSite
-> InVar -> (OutVar -> 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 top_lvl bind_site id linterF
lintIdBndr top_lvl bind_site id thing_inside
= ASSERT2( isId id, ppr id )
do { flags <- getLintFlags
; checkL (not (lf_check_global_ids flags) || isLocalId id)
......@@ -1334,14 +1358,11 @@ lintIdBndr top_lvl bind_site id linterF
; checkL (not (isExternalName (Var.varName id)) || is_top_lvl)
(mkNonTopExternalNameMsg id)
; (id_ty, k) <- addLoc (IdTy id) $
lintInTy (idType id)
; let id' = setIdType id id_ty
-- See Note [Levity polymorphism invariants] in GHC.Core
; lintL (isJoinId id || not (lf_check_levity_poly flags) || not (isKindLevPoly k))
(text "Levity-polymorphic binder:" <+>
(ppr id <+> dcolon <+> parens (ppr id_ty <+> dcolon <+> ppr k)))
; lintL (isJoinId id || not (lf_check_levity_poly flags)
|| not (isTypeLevPoly id_ty)) $
text "Levity-polymorphic binder:" <+> ppr id <+> dcolon <+>
parens (ppr id_ty <+> dcolon <+> ppr (typeKind id_ty))
-- Check that a join-id is a not-top-level let-binding
; when (isJoinId id) $
......@@ -1353,8 +1374,13 @@ lintIdBndr top_lvl bind_site id linterF
; lintL (not (isCoVarType id_ty))
(text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr id_ty)
; addInScopeId id' $ (linterF id') }
; linted_ty <- addLoc (IdTy id) (lintValueType id_ty)
; addInScopeId id linted_ty $
thing_inside (setIdType id linted_ty) }
where
id_ty = idType id
is_top_lvl = isTopLevel top_lvl
is_let_bind = case bind_site of
LetBind -> True
......@@ -1378,45 +1404,58 @@ lintTypes dflags vars tys
where
(_warns, errs) = initL dflags defaultLintFlags vars linter
linter = lintBinders LambdaBind vars $ \_ ->
mapM_ lintInTy tys
mapM_ lintType tys
lintInTy :: InType -> LintM (LintedType, LintedKind)
lintValueType :: Type -> LintM LintedType
-- Types only, not kinds
-- Check the type, and apply the substitution to it
-- See Note [Linting type lets]
lintInTy ty
lintValueType ty
= addLoc (InType ty) $
do { ty' <- applySubstTy ty
; k <- lintType ty'
; addLoc (InKind ty' k) $
lintKind k -- The kind returned by lintType is already
-- a LintedKind but we also want to check that
-- k :: *, which lintKind does
; return (ty', k) }
do { ty' <- lintType ty
; let sk = typeKind ty'
; lintL (classifiesTypeWithValues sk) $
hang (text "Ill-kinded type:" <+> ppr ty)
2 (text "has kind:" <+> ppr sk)
; return ty' }
checkTyCon :: TyCon -> LintM ()
checkTyCon tc
= checkL (not (isTcTyCon tc)) (text "Found TcTyCon:" <+> ppr tc)
-------------------
lintType :: OutType -> LintM LintedKind
-- The returned Kind has itself been linted
lintType :: LintedType -> LintM LintedType
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintType (TyVarTy tv)
= do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
; tv' <- lintTyCoVarInScope tv
; return (tyVarKind tv') }
-- We checked its kind when we added it to the envt
| not (isTyVar tv)
= failWithL (mkBadTyVarMsg tv)
| otherwise
= do { subst <- getTCvSubst
; case lookupTyVar subst tv of
Just linted_ty -> return linted_ty
-- In GHCi we may lint an expression with a free
-- type variable. Then it won't be in the
-- substitution, but it should be in scope
Nothing | tv `isInScope` subst
-> return (TyVarTy tv)
| otherwise
-> failWithL $
hang (text "The type variable" <+> pprBndr LetBind tv)
2 (text "is out of scope")
}
lintType ty@(AppTy t1 t2)
| TyConApp {} <- t1
= failWithL $ text "TyConApp to the left of AppTy:" <+> ppr ty
| otherwise
= do { k1 <- lintType t1
; k2 <- lintType t2
; lint_ty_app ty k1 [(t2,k2)] }
= do { t1' <- lintType t1
; t2' <- lintType t2
; lint_ty_app ty (typeKind t1') [t2']
; return (AppTy t1' t2') }
lintType ty@(TyConApp tc tys)
| isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
......@@ -1433,71 +1472,72 @@ lintType ty@(TyConApp tc tys)
| otherwise -- Data types, data families, primitive types
= do { checkTyCon tc
; ks <- mapM lintType tys
; lint_ty_app ty (tyConKind tc) (tys `zip` ks) }
; tys' <- mapM lintType tys
; lint_ty_app ty (tyConKind tc) tys'
; return (TyConApp tc tys') }
-- arrows can related *unlifted* kinds, so this has to be separate from
-- a dependent forall.
lintType ty@(FunTy _ t1 t2)
= do { k1 <- lintType t1
; k2 <- lintType t2
; lintArrow (text "type or kind" <+> quotes (ppr ty)) k1 k2 }
lintType ty@(FunTy af t1 t2)
= do { t1' <- lintType t1
; t2' <- lintType t2
; lintArrow (text "type or kind" <+> quotes (ppr ty)) t1' t2'
; return (FunTy af t1' t2') }
lintType ty@(ForAllTy (Bndr tcv vis) body_ty)
| not (isTyCoVar tcv)
= failWithL (text "Non-Tyvar or Non-Covar bound in type:" <+> ppr ty)
| otherwise
= lintTyCoBndr tcv $ \tcv' ->
do { body_ty' <- lintType body_ty
; lintForAllBody tcv' body_ty'
lintType t@(ForAllTy (Bndr tv _vis) ty)
-- forall over types
| isTyVar tv
= lintTyBndr tv $ \tv' ->
do { k <- lintType ty
; checkValueKind k (text "the body of forall:" <+> ppr t)
; case occCheckExpand [tv'] k of -- See Note [Stupid type synonyms]
Just k' -> return k'
Nothing -> failWithL (hang (text "Variable escape in forall:")
2 (vcat [ text "type:" <+> ppr t
, text "kind:" <+> ppr k ]))
}
; when (isCoVar tcv) $
lintL (tcv `elemVarSet` tyCoVarsOfType body_ty) $
text "Covar does not occur in the body:" <+> (ppr tcv $$ ppr body_ty)
-- See GHC.Core.TyCo.Rep Note [Unused coercion variable in ForAllTy]
-- and cf GHC.Core.Coercion Note [Unused coercion variable in ForAllCo]
; return (ForAllTy (Bndr tcv' vis) body_ty') }
lintType t@(ForAllTy (Bndr cv _vis) ty)
-- forall over coercions
= do { lintL (isCoVar cv)
(text "Non-Tyvar or Non-Covar bound in type:" <+> ppr t)
; lintL (cv `elemVarSet` tyCoVarsOfType ty)
(text "Covar does not occur in the body:" <+> ppr t)
; lintCoBndr cv $ \_ ->
do { k <- lintType ty
; checkValueKind k (text "the body of forall:" <+> ppr t)
; return liftedTypeKind
-- We don't check variable escape here. Namely, k could refer to cv'
}}
lintType ty@(LitTy l) = lintTyLit l >> return (typeKind ty)
lintType ty@(LitTy l)
= do { lintTyLit l; return ty }
lintType (CastTy ty co)
= do { k1 <- lintType ty
; (k1', k2) <- lintStarCoercion co
; ensureEqTys k1 k1' (mkCastTyErr ty co k1' k1)
; return k2 }
= do { ty' <- lintType ty
; co' <- lintStarCoercion co
; let tyk = typeKind ty'
cok = coercionLKind co'
; ensureEqTys tyk cok (mkCastTyErr ty co tyk cok)
; return (CastTy ty' co') }
lintType (CoercionTy co)
= do { (k1, k2, ty1, ty2, r) <- lintCoercion co
; return $ mkHeteroCoercionType r k1 k2 ty1 ty2 }
{- Note [Stupid type synonyms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider (#14939)
type Alg cls ob = ob
f :: forall (cls :: * -> Constraint) (b :: Alg cls *). b
Here 'cls' appears free in b's kind, which would usually be illegal
(because in (forall a. ty), ty's kind should not mention 'a'). But
#in this case (Alg cls *) = *, so all is well. Currently we allow
this, and make Lint expand synonyms where necessary to make it so.