Commit 257c13d8 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari
Browse files

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
parent 8fa688a8
......@@ -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
......
......@@ -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)
......
{-# LANGUAGE LiberalTypeSynonyms #-}
{-# LANGUAGE TypeFamilies #-}
module T15057 where
type T f = f Int
type S a = a -> a
type family TF a
type instance TF Int = T S
-- Ensure that -dcore-lint doesn't trip up on this unsaturated use
-- of the type synonym S
......@@ -273,3 +273,4 @@ test('T14162', normal, compile, [''])
test('T14237', normal, compile, [''])
test('T14554', normal, compile, [''])
test('T14680', normal, compile, [''])
test('T15057', normal, compile, [''])
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