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

4 files changed, 109 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)
diff --git a/testsuite/tests/indexed-types/should_compile/T15057.hs b/testsuite/tests/indexed-types/should_compile/T15057.hs
new file mode 100644
index 0000000000..b21d3e37f9
--- /dev/null
+++ b/testsuite/tests/indexed-types/should_compile/T15057.hs
@@ -0,0 +1,11 @@
+{-# 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
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 8e89ecfd78..1a5e5d4f5c 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -273,3 +273,4 @@ test('T14162', normal, compile, [''])
 test('T14237', normal, compile, [''])
 test('T14554', normal, compile, [''])
 test('T14680', normal, compile, [''])
+test('T15057', normal, compile, [''])