diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-04-19 20:47:48 -0400 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2018-04-19 20:48:10 -0400 |
commit | 257c13d86db0a9ed540287127fd1c79abacf857e (patch) | |
tree | 888828144d01e11d0c9a89182023f6847f87d1fb /compiler | |
parent | 8fa688a84f4e4d86096710edd1f0d19bac3eea90 (diff) | |
download | haskell-257c13d86db0a9ed540287127fd1c79abacf857e.tar.gz |
Lint types in newFamInst
We weren't linting the types used in `newFamInst`, which
might have been why #15012 went undiscovered for so long. Let's fix
that.
One has to be surprisingly careful with expanding type synonyms in
`lintType`, since in the offending program (simplified):
```lang=haskell
type FakeOut a = Int
type family TF a
type instance TF Int = FakeOut a
```
If one expands type synonyms, then `FakeOut a` will expand to
`Int`, which masks the issue (that `a` is unbound). I added an
extra Lint flag to configure whether type synonyms should be
expanded or not in Lint, and disabled this when calling `lintTypes`
from `newFamInst`.
As evidence that this works, I ran it on the offending program
from #15012, and voilà:
```
$ ghc3/inplace/bin/ghc-stage2 Bug.hs -dcore-lint
[1 of 1] Compiling Foo ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
(GHC version 8.5.20180417 for x86_64-unknown-linux):
Core Lint error
<no location info>: warning:
In the type ‘... (Rec0 (FakeOut b_a1Qt))))’
@ b_a1Qt is out of scope
```
Test Plan: make test TEST=T15057
Reviewers: simonpj, goldfire, bgamari
Reviewed By: bgamari
Subscribers: thomie, carter
GHC Trac Issues: #15057
Differential Revision: https://phabricator.haskell.org/D4611
Diffstat (limited to 'compiler')
-rw-r--r-- | compiler/coreSyn/CoreLint.hs | 112 | ||||
-rw-r--r-- | compiler/typecheck/FamInst.hs | 16 |
2 files changed, 97 insertions, 31 deletions
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs index 78902dfea4..812e1ed281 100644 --- a/compiler/coreSyn/CoreLint.hs +++ b/compiler/coreSyn/CoreLint.hs @@ -11,7 +11,7 @@ A ``lint'' pass to check for Core correctness module CoreLint ( lintCoreBindings, lintUnfolding, lintPassResult, lintInteractiveExpr, lintExpr, - lintAnnots, + lintAnnots, lintTypes, -- ** Debug output endPass, endPassIO, @@ -407,7 +407,8 @@ lintCoreBindings dflags pass local_in_scope binds where in_scope_set = mkInScopeSet (mkVarSet local_in_scope) - flags = LF { lf_check_global_ids = check_globals + flags = defaultLintFlags + { lf_check_global_ids = check_globals , lf_check_inline_loop_breakers = check_lbs , lf_check_static_ptrs = check_static_ptrs } @@ -1275,6 +1276,21 @@ lintIdBndr top_lvl bind_site id linterF %************************************************************************ -} +lintTypes :: DynFlags + -> Bool -- Should type synonyms be expanded? + -- See Note [Linting type synonym applications] + -> TyCoVarSet -- Treat these as in scope + -> [Type] + -> Maybe MsgDoc -- Nothing => OK +lintTypes dflags expand_ts vars tys + | isEmptyBag errs = Nothing + | otherwise = Just (pprMessageBag errs) + where + in_scope = mkInScopeSet vars + lint_flags = defaultLintFlags { lf_expand_type_synonyms = expand_ts } + (_warns, errs) = initL dflags lint_flags in_scope linter + linter = mapM_ lintInTy tys + lintInTy :: InType -> LintM (LintedType, LintedKind) -- Types only, not kinds -- Check the type, and apply the substitution to it @@ -1311,26 +1327,36 @@ lintType ty@(AppTy t1 t2) ; lint_ty_app ty k1 [(t2,k2)] } lintType ty@(TyConApp tc tys) - | Just ty' <- coreView ty - = lintType ty' -- Expand type synonyms, so that we do not bogusly complain - -- about un-saturated type synonyms - - -- We should never see a saturated application of funTyCon; such applications - -- should be represented with the FunTy constructor. See Note [Linting - -- function types] and Note [Representation of function types]. - | isFunTyCon tc - , tys `lengthIs` 4 - = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty)) - - | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc - -- Also type synonyms and type families - , tys `lengthLessThan` tyConArity tc - = failWithL (hang (text "Un-saturated type application") 2 (ppr ty)) - - | otherwise - = do { checkTyCon tc - ; ks <- mapM lintType tys - ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) } + = do { expand_ts <- lf_expand_type_synonyms <$> getLintFlags + ; lint_tc_app expand_ts } + where + lint_tc_app :: Bool -> LintM LintedKind + lint_tc_app expand_ts + | expand_ts, Just ty' <- coreView ty + = lintType ty' -- Expand type synonyms, so that we do not bogusly + -- complain about un-saturated type synonyms. + -- See Note [Linting type synonym applications] + + -- We should never see a saturated application of funTyCon; such + -- applications should be represented with the FunTy constructor. + -- See Note [Linting function types] and + -- Note [Representation of function types]. + | isFunTyCon tc + , tys `lengthIs` 4 + = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty)) + + -- Only check if a type synonym application is unsatured if we have + -- made an effort to expand previously encountered type synonyms. + -- See Note [Linting type synonym applications] + | (expand_ts && isTypeSynonymTyCon tc) || isTypeFamilyTyCon tc + -- Also type synonyms and type families + , tys `lengthLessThan` tyConArity tc + = failWithL (hang (text "Un-saturated type application") 2 (ppr ty)) + + | otherwise + = do { checkTyCon tc + ; ks <- mapM lintType tys + ; lint_ty_app ty (tyConKind tc) (tys `zip` ks) } -- arrows can related *unlifted* kinds, so this has to be separate from -- a dependent forall. @@ -1417,31 +1443,32 @@ lint_app :: SDoc -> LintedKind -> [(LintedType,LintedKind)] -> LintM Kind -- See Note [GHC Formalism] lint_app doc kfn kas = do { in_scope <- getInScope + ; expand_ts <- lf_expand_type_synonyms <$> getLintFlags -- We need the in_scope set to satisfy the invariant in -- Note [The substitution invariant] in TyCoRep - ; foldlM (go_app in_scope) kfn kas } + ; foldlM (go_app expand_ts in_scope) kfn kas } where fail_msg extra = vcat [ hang (text "Kind application error in") 2 doc , nest 2 (text "Function kind =" <+> ppr kfn) , nest 2 (text "Arg kinds =" <+> ppr kas) , extra ] - go_app in_scope kfn tka - | Just kfn' <- coreView kfn - = go_app in_scope kfn' tka + go_app expand_ts in_scope kfn tka + | expand_ts, Just kfn' <- coreView kfn + = go_app expand_ts in_scope kfn' tka - go_app _ (FunTy kfa kfb) tka@(_,ka) + go_app _ _ (FunTy kfa kfb) tka@(_,ka) = do { unless (ka `eqType` kfa) $ addErrL (fail_msg (text "Fun:" <+> (ppr kfa $$ ppr tka))) ; return kfb } - go_app in_scope (ForAllTy (TvBndr kv _vis) kfn) tka@(ta,ka) + go_app _ in_scope (ForAllTy (TvBndr kv _vis) kfn) tka@(ta,ka) = do { let kv_kind = tyVarKind kv ; unless (ka `eqType` kv_kind) $ addErrL (fail_msg (text "Forall:" <+> (ppr kv $$ ppr kv_kind $$ ppr tka))) ; return (substTyWithInScope in_scope [kv] [ta] kfn) } - go_app _ kfn ka + go_app _ _ kfn ka = failWithL (fail_msg (text "Not a fun:" <+> (ppr kfn $$ ppr ka))) {- ********************************************************************* @@ -1912,6 +1939,8 @@ data LintFlags , lf_check_inline_loop_breakers :: Bool -- See Note [Checking for INLINE loop breakers] , lf_check_static_ptrs :: StaticPtrCheck -- ^ See Note [Checking StaticPtrs] + , lf_expand_type_synonyms :: Bool + -- ^ See Note [Linting type synonym applications] } -- See Note [Checking StaticPtrs] @@ -1928,6 +1957,7 @@ defaultLintFlags :: LintFlags defaultLintFlags = LF { lf_check_global_ids = False , lf_check_inline_loop_breakers = True , lf_check_static_ptrs = AllowAnywhere + , lf_expand_type_synonyms = True } newtype LintM a = @@ -1972,6 +2002,30 @@ rename type binders as we go, maintaining a substitution. The same substitution also supports let-type, current expressed as (/\(a:*). body) ty Here we substitute 'ty' for 'a' in 'body', on the fly. + +Note [Linting type synonym applications] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Most of the time when linting types, one will want to expand type synonyms. +This is because there's a separate lint check for unsaturated applications of +type constructors, so the following code (which is permitted with +LiberalTypeSynonyms) would fail to lint: + + type T f = f Int + type S a = a -> a + type Z = T S + +On the other hand, expanding type synonyms can sometimes mask other problems. +For instance, in the following code (#15012): + + type FakeOut a = Int + type family TF a + type instance TF Int = FakeOut a + +The TF Int instance is ill-formed, since `a` is unbound. However, lintType +normally wouldn't catch this, since it would expand `FakeOut a` to `Int`, +which prevents Lint from knowing about `a` in the first place. As a result, +Lint allows configuring whether one should expand type synonyms or not, +depending on the situation. -} instance Functor LintM where diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs index 956a412baf..4fe1430762 100644 --- a/compiler/typecheck/FamInst.hs +++ b/compiler/typecheck/FamInst.hs @@ -19,6 +19,7 @@ import HscTypes import FamInstEnv import InstEnv( roughMatchTcs ) import Coercion +import CoreLint import TcEvidence import LoadIface import TcRnMonad @@ -160,13 +161,24 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc }) ASSERT2( lhs_kind `eqType` rhs_kind, text "kind" <+> pp_ax $$ ppr lhs_kind $$ ppr rhs_kind ) do { (subst, tvs') <- freshenTyVarBndrs tvs ; (subst, cvs') <- freshenCoVarBndrsX subst cvs + ; dflags <- getDynFlags + ; let lhs' = substTys subst lhs + rhs' = substTy subst rhs + tcv_set' = mkVarSet (tvs' ++ cvs') + ; when (gopt Opt_DoCoreLinting dflags) $ + -- Check that the types involved in this instance are well formed. + -- Do /not/ expand type synonyms, for the reasons discussed in + -- Note [Linting type synonym applications]. + case lintTypes dflags False tcv_set' (rhs':lhs') of + Nothing -> pure () + Just fail_msg -> pprPanic "Core Lint error" fail_msg ; return (FamInst { fi_fam = tyConName fam_tc , fi_flavor = flavor , fi_tcs = roughMatchTcs lhs , fi_tvs = tvs' , fi_cvs = cvs' - , fi_tys = substTys subst lhs - , fi_rhs = substTy subst rhs + , fi_tys = lhs' + , fi_rhs = rhs' , fi_axiom = axiom }) } where lhs_kind = typeKind (mkTyConApp fam_tc lhs) |