summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Peyton Jones <simonpj@microsoft.com>2019-12-20 16:27:32 +0000
committerSimon Peyton Jones <simonpj@microsoft.com>2020-03-10 23:17:04 +0000
commitc52896014bc2c8b307899d442ca309a791f66ca0 (patch)
tree0b214ba6f058abda6c85561de4c2b605108d77ad
parent3300eeacbbf7a3d1f961f809be5d236c48827b28 (diff)
downloadhaskell-wip/T17590.tar.gz
Fix Lintwip/T17590
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
Diffstat
-rw-r--r--compiler/GHC/Core/Lint.hs163
-rw-r--r--testsuite/tests/simplCore/should_compile/T17590.hs39
-rw-r--r--testsuite/tests/simplCore/should_compile/all.T1
3 files changed, 147 insertions, 56 deletions
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs
index 091e4d8571..7c774bdc67 100644
--- a/compiler/GHC/Core/Lint.hs
+++ b/compiler/GHC/Core/Lint.hs
@@ -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
diff --git a/testsuite/tests/simplCore/should_compile/T17590.hs b/testsuite/tests/simplCore/should_compile/T17590.hs
new file mode 100644
index 0000000000..4f668f32fa
--- /dev/null
+++ b/testsuite/tests/simplCore/should_compile/T17590.hs
@@ -0,0 +1,39 @@
+{-# 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
diff --git a/testsuite/tests/simplCore/should_compile/all.T b/testsuite/tests/simplCore/should_compile/all.T
index cdb2fe502b..31b7989b43 100644
--- a/testsuite/tests/simplCore/should_compile/all.T
+++ b/testsuite/tests/simplCore/should_compile/all.T
@@ -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'])
View Lorry Controller Status