Commit c12a2ec5 authored by Simon Peyton Jones's avatar Simon Peyton Jones Committed by Marge Bot

Fix Lint

Ticket #17590 pointed out a bug in the way the linter dealt with
type lets, exposed by the new uniqAway story.

The fix is described in Note [Linting type lets]. I ended up
putting the in-scope Ids in a different env field, le_ids,
rather than (as before) sneaking them into the TCvSubst.

Surprisingly tiresome, but done.

Metric Decrease:
    hie002
parent 7f25557a
Pipeline #16695 canceled with stages
......@@ -39,6 +39,7 @@ import TcType ( isFloatingTy )
import Var
import VarEnv
import VarSet
import UniqSet( nonDetEltsUniqSet )
import Name
import Id
import IdInfo
......@@ -73,6 +74,7 @@ import qualified Control.Monad.Fail as MonadFail
import MonadUtils
import Data.Foldable ( toList )
import Data.List.NonEmpty ( NonEmpty )
import Data.List ( partition )
import Data.Maybe
import Pair
import qualified GHC.LanguageExtensions as LangExt
......@@ -161,21 +163,60 @@ this invariant in lintType.
Note [Linting type lets]
~~~~~~~~~~~~~~~~~~~~~~~~
In the desugarer, it's very very convenient to be able to say (in effect)
let a = Type Int in <body>
That is, use a type let. See Note [Type let] in GHC.Core.
let a = Type Bool in
let x::a = True in <body>
That is, use a type let. See Note [Type let] in CoreSyn.
One place it is used is in mkWwArgs; see Note [Join points and beta-redexes]
in WwLib. (Maybe there are other "clients" of this feature; I'm not sure).
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 function
* Hence 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 -> Bool]) and apply this substitution before
comparing types. In effect, in Lint, type equality is always
equality-moduolo-le-subst. This is in the le_subst field of
LintEnv. But nota bene:
(SI1) The le_subst substitution is applied to types and coercions only
(SI2) The result of that substitution is used only to check for type
equality, to check well-typed-ness, /but is then discarded/.
The result of substittion does not outlive the CoreLint pass.
(SI3) The InScopeSet of le_subst includes only TyVar and CoVar binders.
* The function
lintInTy :: Type -> LintM (Type, Kind)
returns a substituted type.
returns a substituted type.
* When we encounter a binder (like x::a) we must apply the substitution
to the type of the binding variable. lintBinders does this.
* Clearly we need to clone tyvar binders as we go.
* But take care (#17590)! We must also clone CoVar binders:
let a = TYPE (ty |> cv)
in \cv -> blah
blindly substituting for `a` might capture `cv`.
When we encounter a binder (like x::a) we must apply the substitution
to the type of the binding variable. lintBinders does this.
* Alas, when cloning a coercion variable we might choose a unique
that happens to clash with an inner Id, thus
\cv_66 -> let wild_X7 = blah in blah
We decide to clone `cv_66` becuase it's already in scope. Fine,
choose a new unique. Aha, X7 looks good. So we check the lambda
body with le_subst of [cv_66 :-> cv_X7]
For Ids, the type-substituted Id is added to the in_scope set (which
itself is part of the TCvSubst we are carrying down), and when we
find an occurrence of an Id, we fetch it from the in-scope set.
This is all fine, even though we use the same unique as wild_X7.
As (SI2) says, we do /not/ return a new lambda
(\cv_X7 -> let wild_X7 = blah in ...)
We simply use the le_subst subsitution in types/coercions only, when
checking for equality.
* We still need to check that Id occurrences are bound by some
enclosing binding. We do /not/ use the InScopeSet for the le_subst
for this purpose -- it contains only TyCoVars. Instead we have a separate
le_ids for the in-scope Id binders.
Sigh. We might want to explore getting rid of type-let!
Note [Bad unsafe coercion]
~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -418,9 +459,9 @@ lintCoreBindings :: DynFlags -> CoreToDo -> [Var] -> CoreProgram -> (Bag MsgDoc,
-- If you edit this function, you may need to update the GHC formalism
-- See Note [GHC Formalism]
lintCoreBindings dflags pass local_in_scope binds
= initL dflags flags in_scope_set $
addLoc TopLevelBindings $
lintLetBndrs TopLevel binders $
= 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'
......@@ -428,8 +469,6 @@ lintCoreBindings dflags pass local_in_scope binds
; checkL (null ext_dups) (dupExtVars ext_dups)
; mapM lint_bind binds }
where
in_scope_set = mkInScopeSet (mkVarSet local_in_scope)
flags = defaultLintFlags
{ lf_check_global_ids = check_globals
, lf_check_inline_loop_breakers = check_lbs
......@@ -501,12 +540,12 @@ lintUnfolding :: Bool -- True <=> is a compulsory unfolding
-> CoreExpr
-> Maybe MsgDoc -- Nothing => OK
lintUnfolding is_compulsory dflags locn vars expr
lintUnfolding is_compulsory dflags locn var_set expr
| isEmptyBag errs = Nothing
| otherwise = Just (pprMessageBag errs)
where
in_scope = mkInScopeSet vars
(_warns, errs) = initL dflags defaultLintFlags in_scope $
vars = nonDetEltsUniqSet var_set
(_warns, errs) = initL dflags defaultLintFlags vars $
if is_compulsory
-- See Note [Checking for levity polymorphism]
then noLPChecks linter
......@@ -523,8 +562,7 @@ lintExpr dflags vars expr
| isEmptyBag errs = Nothing
| otherwise = Just (pprMessageBag errs)
where
in_scope = mkInScopeSet (mkVarSet vars)
(_warns, errs) = initL dflags defaultLintFlags in_scope linter
(_warns, errs) = initL dflags defaultLintFlags vars linter
linter = addLoc TopLevelBindings $
lintCoreExpr expr
......@@ -776,7 +814,7 @@ lintCoreExpr (Let (NonRec tv (Type ty)) body)
do { addLoc (RhsOf tv) $ lintTyKind tv' ty'
-- Now extend the substitution so we
-- take advantage of it in the body
; extendSubstL tv ty' $
; extendTvSubstL tv ty' $
addLoc (BodyOfLetRec [tv]) $
lintCoreExpr body } }
......@@ -1296,13 +1334,14 @@ lintIdBndr top_lvl bind_site id linterF
; checkL (not (isExternalName (Var.varName id)) || is_top_lvl)
(mkNonTopExternalNameMsg id)
; (ty, k) <- addLoc (IdTy id) $
lintInTy (idType 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 ty <+> dcolon <+> ppr k)))
(ppr id <+> dcolon <+> parens (ppr id_ty <+> dcolon <+> ppr k)))
-- Check that a join-id is a not-top-level let-binding
; when (isJoinId id) $
......@@ -1311,11 +1350,10 @@ lintIdBndr top_lvl bind_site id linterF
-- Check that the Id does not have type (t1 ~# t2) or (t1 ~R# t2);
-- if so, it should be a CoVar, and checked by lintCoVarBndr
; lintL (not (isCoVarType ty))
(text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr ty)
; lintL (not (isCoVarType id_ty))
(text "Non-CoVar has coercion type" <+> ppr id <+> dcolon <+> ppr id_ty)
; let id' = setIdType id ty
; addInScopeVar id' $ (linterF id') }
; addInScopeId id' $ (linterF id') }
where
is_top_lvl = isTopLevel top_lvl
is_let_bind = case bind_site of
......@@ -1338,8 +1376,7 @@ lintTypes dflags vars tys
| isEmptyBag errs = Nothing
| otherwise = Just (pprMessageBag errs)
where
in_scope = emptyInScopeSet
(_warns, errs) = initL dflags defaultLintFlags in_scope linter
(_warns, errs) = initL dflags defaultLintFlags vars linter
linter = lintBinders LambdaBind vars $ \_ ->
mapM_ lintInTy tys
......@@ -1368,8 +1405,8 @@ lintType :: OutType -> LintM LintedKind
-- See Note [GHC Formalism]
lintType (TyVarTy tv)
= do { checkL (isTyVar tv) (mkBadTyVarMsg tv)
; lintTyCoVarInScope tv
; return (tyVarKind tv) }
; tv' <- lintTyCoVarInScope tv
; return (tyVarKind tv') }
-- We checked its kind when we added it to the envt
lintType ty@(AppTy t1 t2)
......@@ -1759,7 +1796,7 @@ lintCoercion (ForAllCo tv1 kind_co co)
| isTyVar tv1
= do { (_, k2) <- lintStarCoercion kind_co
; let tv2 = setTyVarKind tv1 k2
; addInScopeVar tv1 $
; addInScopeTyCoVar tv1 $
do {
; (k3, k4, t1, t2, r) <- lintCoercion co
; in_scope <- getInScope
......@@ -1783,7 +1820,7 @@ lintCoercion (ForAllCo cv1 kind_co co)
(text "Covar can only appear in Refl and GRefl: " <+> ppr co)
; (_, k2) <- lintStarCoercion kind_co
; let cv2 = setVarType cv1 k2
; addInScopeVar cv1 $
; addInScopeTyCoVar cv1 $
do {
; (k3, k4, t1, t2, r) <- lintCoercion co
; checkValueKind k3 (text "the body of a ForAllCo over covar:" <+> ppr co)
......@@ -1823,9 +1860,8 @@ lintCoercion (CoVarCo cv)
= failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
2 (text "With offending type:" <+> ppr (varType cv)))
| otherwise
= do { lintTyCoVarInScope cv
; cv' <- lookupIdInScope cv
; lintUnliftedCoVar cv
= do { cv' <- lintTyCoVarInScope cv
; lintUnliftedCoVar cv'
; return $ coVarKindsTypesRole cv' }
-- See Note [Bad unsafe coercion]
......@@ -2091,10 +2127,14 @@ data LintEnv
= LE { le_flags :: LintFlags -- Linting the result of this pass
, le_loc :: [LintLocInfo] -- Locations
, le_subst :: TCvSubst -- Current type substitution
, le_subst :: TCvSubst -- Current TyCo substitution
-- See Note [Linting type lets]
-- /Only/ substitutes for type variables;
-- but might clone CoVars
-- We also use le_subst to keep track of
-- /all variables/ in scope, both Ids and TyVars
-- in-scope TyVars and CoVars
, le_ids :: IdSet -- In-scope Ids
, le_joins :: IdSet -- Join points in scope that are valid
-- A subset of the InScopeSet in le_subst
-- See Note [Join points]
......@@ -2240,17 +2280,19 @@ data LintLocInfo
| InType Type -- Inside a type
| InCo Coercion -- Inside a coercion
initL :: DynFlags -> LintFlags -> InScopeSet
initL :: DynFlags -> LintFlags -> [Var]
-> LintM a -> WarnsAndErrs -- Warnings and errors
initL dflags flags in_scope m
initL dflags flags vars m
= case unLintM m env (emptyBag, emptyBag) of
(Just _, errs) -> errs
(Nothing, errs@(_, e)) | not (isEmptyBag e) -> errs
| otherwise -> pprPanic ("Bug in Lint: a failure occurred " ++
"without reporting an error message") empty
where
(tcvs, ids) = partition isTyCoVar vars
env = LE { le_flags = flags
, le_subst = mkEmptyTCvSubst in_scope
, le_subst = mkEmptyTCvSubst (mkInScopeSet (mkVarSet tcvs))
, le_ids = mkVarSet ids
, le_joins = emptyVarSet
, le_loc = []
, le_dynflags = dflags }
......@@ -2330,15 +2372,22 @@ inCasePat = LintM $ \ env errs -> (Just (is_case_pat env), errs)
is_case_pat (LE { le_loc = CasePat {} : _ }) = True
is_case_pat _other = False
addInScopeVar :: Var -> LintM a -> LintM a
addInScopeVar var m
addInScopeTyCoVar :: Var -> LintM a -> LintM a
addInScopeTyCoVar var m
= LintM $ \ env errs ->
unLintM m (env { le_subst = extendTCvInScope (le_subst env) var
, le_joins = delVarSet (le_joins env) var
}) errs
unLintM m (env { le_subst = extendTCvInScope (le_subst env) var }) errs
extendSubstL :: TyVar -> Type -> LintM a -> LintM a
extendSubstL tv ty m
addInScopeId :: Id -> LintM a -> LintM a
addInScopeId id m
= LintM $ \ env errs ->
unLintM m (env { le_ids = extendVarSet (le_ids env) id
, le_joins = delVarSet (le_joins env) id }) errs
getInScopeIds :: LintM IdSet
getInScopeIds = LintM (\env errs -> (Just (le_ids env), errs))
extendTvSubstL :: TyVar -> Type -> LintM a -> LintM a
extendTvSubstL tv ty m
= LintM $ \ env errs ->
unLintM m (env { le_subst = Type.extendTvSubst (le_subst env) tv ty }) errs
......@@ -2378,8 +2427,8 @@ applySubstCo co = do { subst <- getTCvSubst; return (substCo subst co) }
lookupIdInScope :: Id -> LintM Id
lookupIdInScope id_occ
= do { subst <- getTCvSubst
; case lookupInScope (getTCvInScope subst) id_occ of
= do { in_scope_ids <- getInScopeIds
; case lookupVarSet in_scope_ids id_occ of
Just id_bnd -> do { checkL (not (bad_global id_bnd)) global_in_scope
; return id_bnd }
Nothing -> do { checkL (not is_local) local_out_of_scope
......@@ -2411,12 +2460,14 @@ lookupJoinId id
Just id' -> return (isJoinId_maybe id')
Nothing -> return Nothing }
lintTyCoVarInScope :: TyCoVar -> LintM ()
lintTyCoVarInScope :: TyCoVar -> LintM TyCoVar
lintTyCoVarInScope var
= do { subst <- getTCvSubst
; lintL (var `isInScope` subst)
(hang (text "The variable" <+> pprBndr LetBind var)
2 (text "is out of scope")) }
; case lookupInScope (getTCvInScope subst) var of
Just var' -> return var'
Nothing -> failWithL $
hang (text "The TyCo variable" <+> pprBndr LetBind var)
2 (text "is out of scope") }
ensureEqTys :: OutType -> OutType -> MsgDoc -> LintM ()
-- check ty2 is subtype of ty1 (ie, has same structure but usage
......
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeOperators #-}
module Codec.Picture.Metadata where
import Control.DeepSeq( NFData( .. ) )
import Data.Typeable( (:~:)( Refl ) )
import Data.Word( Word16 )
data ExifTag
= TagPhotometricInterpretation
| TagUnknown !Word16
deriving Eq
data ExifData = ExifNone
data Keys a where
Exif :: !ExifTag -> Keys ExifData
Unknown :: !String -> Keys Value
data Value
data Elem k =
forall a. (Show a, NFData a) => !(k a) :=> a
keyEq :: Keys a -> Keys b -> Maybe (a :~: b)
keyEq a b = case (a, b) of
(Unknown v1, Unknown v2) | v1 == v2 -> Just Refl
(Exif t1, Exif t2) | t1 == t2 -> Just Refl
_ -> Nothing
newtype Metadatas = Metadatas { getMetadatas :: [Elem Keys] }
lookup :: Keys a -> Metadatas -> Maybe a
lookup k = go . getMetadatas where
go [] = Nothing
go ((k2 :=> v) : rest) = case keyEq k k2 of
Nothing -> go rest
Just Refl -> Just v
......@@ -312,6 +312,7 @@ test('T17409',
normal,
makefile_test, ['T17409'])
test('T17429', normal, compile, ['-dcore-lint -O2'])
test('T17590', normal, compile, ['-dcore-lint -O2'])
test('T17722', normal, multimod_compile, ['T17722B', '-dcore-lint -O2 -v0'])
test('T17724', normal, compile, ['-dcore-lint -O2'])
test('T17787', [ grep_errmsg(r'foo') ], compile, ['-ddump-simpl -dsuppress-uniques'])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment