Add valid refinement substitution suggestions for typed holes
[ghc.git] / compiler / typecheck / TcRnDriver.hs
index 6c800f4..85535e1 100644 (file)
@@ -12,9 +12,9 @@ https://ghc.haskell.org/trac/ghc/wiki/Commentary/Compiler/TypeChecker
 {-# LANGUAGE NondecreasingIndentation #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
 
 module TcRnDriver (
-#ifdef GHCI
         tcRnStmt, tcRnExpr, TcRnExprMode(..), tcRnType,
         tcRnImportDecls,
         tcRnLookupRdrName,
@@ -22,7 +22,6 @@ module TcRnDriver (
         tcRnDeclsi,
         isGHCiMonad,
         runTcInteractive,    -- Used by GHC API clients (Trac #8878)
-#endif
         tcRnLookupName,
         tcRnGetInfo,
         tcRnModule, tcRnModuleTcRnM,
@@ -36,39 +35,48 @@ module TcRnDriver (
         tcRnMergeSignatures,
         instantiateSignature,
         tcRnInstantiateSignature,
+        loadUnqualIfaces,
         -- More private...
         badReexportedBootThing,
         checkBootDeclM,
         missingBootThing,
     ) where
 
-#ifdef GHCI
+import GhcPrelude
+
 import {-# SOURCE #-} TcSplice ( finishTH )
 import RnSplice ( rnTopSpliceDecls, traceSplice, SpliceInfo(..) )
 import IfaceEnv( externaliseName )
 import TcHsType
 import TcMatches
 import Inst( deeplyInstantiate )
+import TcUnify( checkConstraints )
 import RnTypes
 import RnExpr
+import RnUtils ( HsDocContext(..) )
+import RnFixity ( lookupFixityRn )
 import MkId
 import TidyPgm    ( globaliseAndTidyId )
 import TysWiredIn ( unitTy, mkListTy )
+#if defined(GHCI)
 import DynamicLoading ( loadPlugins )
 import Plugins ( tcPlugin )
 #endif
 
 import DynFlags
-import StaticFlags
 import HsSyn
+import IfaceSyn ( ShowSub(..), showToHeader )
+import IfaceType( ShowForAllFlag(..) )
 import PrelNames
+import PrelInfo
 import RdrName
 import TcHsSyn
 import TcExpr
 import TcRnMonad
 import TcRnExports
 import TcEvidence
-import PprTyThing( pprTyThing )
+import qualified BooleanFormula as BF
+import PprTyThing( pprTyThingInContext )
 import MkIface( tyThingToIfaceDecl )
 import Coercion( pprCoAxiom )
 import CoreFVs( orphNamesOfFamInst )
@@ -98,7 +106,7 @@ import ErrUtils
 import Id
 import VarEnv
 import Module
-import UniqDFM
+import UniqFM
 import Name
 import NameEnv
 import NameSet
@@ -115,7 +123,7 @@ import Class
 import BasicTypes hiding( SuccessFlag(..) )
 import CoAxiom
 import Annotations
-import Data.List ( sortBy )
+import Data.List ( sortBy, sort )
 import Data.Ord
 import FastString
 import Maybes
@@ -123,6 +131,9 @@ import Util
 import Bag
 import Inst (tcGetInsts)
 import qualified GHC.LanguageExtensions as LangExt
+import Data.Data ( Data )
+import HsDumpAst
+import qualified Data.Set as S
 
 import Control.Monad
 
@@ -151,6 +162,7 @@ tcRnModule hsc_env hsc_src save_rn_syntax
               (const ()) $
    initTc hsc_env hsc_src save_rn_syntax this_mod real_loc $
           withTcPlugins hsc_env $
+
           tcRnModuleTcRnM hsc_env hsc_src parsedModule pair
 
   | otherwise
@@ -229,7 +241,7 @@ tcRnModuleTcRnM hsc_env hsc_src
 
           -- If the whole module is warned about or deprecated
           -- (via mod_deprec) record that in tcg_warns. If we do thereby add
-          -- a WarnAll, it will override any subseqent depracations added to tcg_warns
+          -- a WarnAll, it will override any subsequent deprecations added to tcg_warns
         let { tcg_env1 = case mod_deprec of
                          Just (L _ txt) -> tcg_env { tcg_warns = WarnAll txt }
                          Nothing        -> tcg_env
@@ -238,7 +250,7 @@ tcRnModuleTcRnM hsc_env hsc_src
         setGblEnv tcg_env1 $ do {
 
                 -- Rename and type check the declarations
-        traceRn (text "rn1a") ;
+        traceRn "rn1a" empty ;
         tcg_env <- if isHsBootOrSig hsc_src then
                         tcRnHsBootDecls hsc_src local_decls
                    else
@@ -247,11 +259,11 @@ tcRnModuleTcRnM hsc_env hsc_src
         setGblEnv tcg_env               $ do {
 
                 -- Process the export list
-        traceRn (text "rn4a: before exports");
+        traceRn "rn4a: before exports" empty;
         tcg_env <- tcRnExports explicit_mod_hdr export_ies tcg_env ;
-        traceRn (text "rn4b: after exports") ;
+        traceRn "rn4b: after exports" empty ;
 
-                -- Check that main is exported (must be after rnExports)
+                -- Check that main is exported (must be after tcRnExports)
         checkMainExported tcg_env ;
 
         -- Compare the hi-boot iface (if any) with the real thing
@@ -269,6 +281,9 @@ tcRnModuleTcRnM hsc_env hsc_src
         tcg_env <- return (tcg_env { tcg_doc_hdr = maybe_doc_hdr }) ;
 
                 -- Report unused names
+                -- Do this /after/ type inference, so that when reporting
+                -- a function with no type signature we can give the
+                -- inferred type
         reportUnusedNames export_ies tcg_env ;
 
                 -- add extra source files to tcg_dependent_files
@@ -291,12 +306,12 @@ implicitPreludeWarn
 ************************************************************************
 -}
 
-tcRnImports :: HscEnv -> [LImportDecl RdrName] -> TcM TcGblEnv
+tcRnImports :: HscEnv -> [LImportDecl GhcPs] -> TcM TcGblEnv
 tcRnImports hsc_env import_decls
   = do  { (rn_imports, rdr_env, imports, hpc_info) <- rnImports import_decls ;
 
         ; this_mod <- getModule
-        ; let { dep_mods :: DModuleNameEnv (ModuleName, IsBootInterface)
+        ; let { dep_mods :: ModuleNameEnv (ModuleName, IsBootInterface)
               ; dep_mods = imp_dep_mods imports
 
                 -- We want instance declarations from all home-package
@@ -307,7 +322,7 @@ tcRnImports hsc_env import_decls
                 -- modules batch (@--make@) compiled before this one, but
                 -- which are not below this one.
               ; want_instances :: ModuleName -> Bool
-              ; want_instances mod = mod `elemUDFM` dep_mods
+              ; want_instances mod = mod `elemUFM` dep_mods
                                    && mod /= moduleName this_mod
               ; (home_insts, home_fam_insts) = hptInstances hsc_env
                                                             want_instances
@@ -316,7 +331,7 @@ tcRnImports hsc_env import_decls
                 -- Record boot-file info in the EPS, so that it's
                 -- visible to loadHiBootInterface in tcRnSrcDecls,
                 -- and any other incrementally-performed imports
-        ; updateEps_ (\eps -> eps { eps_is_boot = udfmToUfm dep_mods }) ;
+        ; updateEps_ (\eps -> eps { eps_is_boot = dep_mods }) ;
 
                 -- Update the gbl env
         ; updGblEnv ( \ gbl ->
@@ -330,26 +345,33 @@ tcRnImports hsc_env import_decls
               tcg_hpc          = hpc_info
             }) $ do {
 
-        ; traceRn (text "rn1" <+> ppr (imp_dep_mods imports))
+        ; traceRn "rn1" (ppr (imp_dep_mods imports))
                 -- Fail if there are any errors so far
                 -- The error printing (if needed) takes advantage
                 -- of the tcg_env we have now set
 --      ; traceIf (text "rdr_env: " <+> ppr rdr_env)
         ; failIfErrsM
 
-                -- Load any orphan-module and family instance-module
-                -- interfaces, so that their rules and instance decls will be
-                -- found.  But filter out a self hs-boot: these instances
-                -- will be checked when we define them locally.
+                -- Load any orphan-module (including orphan family
+                -- instance-module) interfaces, so that their rules and
+                -- instance decls will be found.  But filter out a
+                -- self hs-boot: these instances will be checked when
+                -- we define them locally.
+                -- (We don't need to load non-orphan family instance
+                -- modules until we either try to use the instances they
+                -- define, or define our own family instances, at which
+                -- point we need to check them for consistency.)
         ; loadModuleInterfaces (text "Loading orphan modules")
                                (filter (/= this_mod) (imp_orphs imports))
 
-                -- Check type-family consistency
-        ; traceRn (text "rn1: checking family instance consistency")
+                -- Check type-family consistency between imports.
+                -- See Note [The type family instance consistency story]
+        ; traceRn "rn1: checking family instance consistency {" empty
         ; let { dir_imp_mods = moduleEnvKeys
                              . imp_mods
                              $ imports }
-        ; checkFamInstConsistency (imp_finsts imports) dir_imp_mods ;
+        ; checkFamInstConsistency dir_imp_mods
+        ; traceRn "rn1: } checking family instance consistency" empty
 
         ; getGblEnv } }
 
@@ -362,32 +384,21 @@ tcRnImports hsc_env import_decls
 -}
 
 tcRnSrcDecls :: Bool  -- False => no 'module M(..) where' header at all
-             -> [LHsDecl RdrName]               -- Declarations
+             -> [LHsDecl GhcPs]               -- Declarations
              -> TcM TcGblEnv
 tcRnSrcDecls explicit_mod_hdr decls
  = do { -- Do all the declarations
-      ; ((tcg_env, tcl_env), lie) <- captureConstraints $
-              do { envs <- tc_rn_src_decls decls
-                 ; (tcg_env, tcl_env) <- setEnvs envs run_th_modfinalizers
+      ; ((tcg_env, tcl_env), lie) <- captureTopConstraints $
+              do { (tcg_env, tcl_env) <- tc_rn_src_decls decls
 
                    -- Check for the 'main' declaration
-                   -- Must do this inside the captureConstraints
+                   -- Must do this inside the captureTopConstraints
                  ; tcg_env <- setEnvs (tcg_env, tcl_env) $
                               checkMain explicit_mod_hdr
                  ; return (tcg_env, tcl_env) }
 
-        -- Emit Typeable bindings
-      ; tcg_env <- setGblEnv tcg_env mkTypeableBinds
-
       ; setEnvs (tcg_env, tcl_env) $ do {
 
-#ifdef GHCI
-      ; finishTH
-#endif /* GHCI */
-
-        -- wanted constraints from static forms
-      ; stWC <- tcg_static_wc <$> getGblEnv >>= readTcRef
-
              --         Simplify constraints
              --
              -- We do this after checkMain, so that we use the type info
@@ -398,7 +409,18 @@ tcRnSrcDecls explicit_mod_hdr decls
              --  * the local env exposes the local Ids to simplifyTop,
              --    so that we get better error messages (monomorphism restriction)
       ; new_ev_binds <- {-# SCC "simplifyTop" #-}
-                        simplifyTop (andWC stWC lie)
+                        simplifyTop lie
+
+        -- Emit Typeable bindings
+      ; tcg_env <- mkTypeableBinds
+
+        -- Finalizers must run after constraints are simplified, or some types
+        -- might not be complete when using reify (see #12777).
+      ; (tcg_env, tcl_env) <- setGblEnv tcg_env run_th_modfinalizers
+      ; setEnvs (tcg_env, tcl_env) $ do {
+
+      ; finishTH
+
       ; traceTc "Tc9" empty
 
       ; failIfErrsM     -- Don't zonk if there have been errors
@@ -434,9 +456,9 @@ tcRnSrcDecls explicit_mod_hdr decls
 
       ; setGlobalTypeEnv tcg_env' final_type_env
 
+   }
    } }
 
-#ifdef GHCI
 -- | Runs TH finalizers and renames and typechecks the top-level declarations
 -- that they could introduce.
 run_th_modfinalizers :: TcM (TcGblEnv, TcLclEnv)
@@ -447,17 +469,23 @@ run_th_modfinalizers = do
   then getEnvs
   else do
     writeTcRef th_modfinalizers_var []
-    sequence_ th_modfinalizers
-    -- Finalizers can add top-level declarations with addTopDecls.
-    envs <- tc_rn_src_decls []
-    -- addTopDecls can add declarations which add new finalizers.
-    setEnvs envs run_th_modfinalizers
-#else
-run_th_modfinalizers :: TcM (TcGblEnv, TcLclEnv)
-run_th_modfinalizers = getEnvs
-#endif /* GHCI */
-
-tc_rn_src_decls :: [LHsDecl RdrName]
+    (envs, lie) <- captureTopConstraints $ do
+      sequence_ th_modfinalizers
+      -- Finalizers can add top-level declarations with addTopDecls.
+      tc_rn_src_decls []
+    setEnvs envs $ do
+      -- Subsequent rounds of finalizers run after any new constraints are
+      -- simplified, or some types might not be complete when using reify
+      -- (see #12777).
+      new_ev_binds <- {-# SCC "simplifyTop2" #-}
+                      simplifyTop lie
+      updGblEnv (\tcg_env ->
+        tcg_env { tcg_ev_binds = tcg_ev_binds tcg_env `unionBags` new_ev_binds }
+        )
+        -- addTopDecls can add declarations which add new finalizers.
+        run_th_modfinalizers
+
+tc_rn_src_decls :: [LHsDecl GhcPs]
                 -> TcM (TcGblEnv, TcLclEnv)
 -- Loops around dealing with each top level inter-splice group
 -- in turn, until it's dealt with the entire module
@@ -470,7 +498,6 @@ tc_rn_src_decls ds
       ; (tcg_env, rn_decls) <- rnTopSrcDecls first_group
                 -- rnTopSrcDecls fails if there are any errors
 
-#ifdef GHCI
         -- Get TH-generated top-level declarations and make sure they don't
         -- contain any splices since we don't handle that at the moment
         --
@@ -503,7 +530,6 @@ tc_rn_src_decls ds
 
                     ; return (tcg_env, appendGroups rn_decls th_rn_decls)
                     }
-#endif /* GHCI */
 
       -- Type check all declarations
       ; (tcg_env, tcl_env) <- setGblEnv tcg_env $
@@ -514,12 +540,6 @@ tc_rn_src_decls ds
         case group_tail of
           { Nothing -> return (tcg_env, tcl_env)
 
-#ifndef GHCI
-            -- There shouldn't be a splice
-          ; Just (SpliceDecl {}, _) ->
-            failWithTc (text "Can't do a top-level splice; need a bootstrapped compiler")
-          }
-#else
             -- If there's a splice, we must carry on
           ; Just (SpliceDecl (L loc splice) _, rest_ds) ->
             do { recordTopLevelSpliceLoc loc
@@ -533,7 +553,6 @@ tc_rn_src_decls ds
                  tc_rn_src_decls (spliced_decls ++ rest_ds)
                }
           }
-#endif /* GHCI */
       }
 
 {-
@@ -545,7 +564,7 @@ tc_rn_src_decls ds
 ************************************************************************
 -}
 
-tcRnHsBootDecls :: HscSource -> [LHsDecl RdrName] -> TcM TcGblEnv
+tcRnHsBootDecls :: HscSource -> [LHsDecl GhcPs] -> TcM TcGblEnv
 tcRnHsBootDecls hsc_src decls
    = do { (first_group, group_tail) <- findSplice decls
 
@@ -561,7 +580,7 @@ tcRnHsBootDecls hsc_src decls
               <- rnTopSrcDecls first_group
         -- The empty list is for extra dependencies coming from .hs-boot files
         -- See Note [Extra dependencies from .hs-boot files] in RnSource
-        ; (gbl_env, lie) <- captureConstraints $ setGblEnv tcg_env $ do {
+        ; (gbl_env, lie) <- captureTopConstraints $ setGblEnv tcg_env $ do {
 
 
                 -- Check for illegal declarations
@@ -579,6 +598,10 @@ tcRnHsBootDecls hsc_src decls
              <- tcTyClsInstDecls tycl_decls deriv_decls val_binds
         ; setGblEnv tcg_env     $ do {
 
+        -- Emit Typeable bindings
+        ; tcg_env <- mkTypeableBinds
+        ; setGblEnv tcg_env $ do {
+
                 -- Typecheck value declarations
         ; traceTc "Tc5" empty
         ; val_ids <- tcHsBootSigs val_binds val_sigs
@@ -598,7 +621,7 @@ tcRnHsBootDecls hsc_src decls
               }
 
         ; setGlobalTypeEnv gbl_env type_env2
-   }}
+   }}}
    ; traceTc "boot" (ppr lie); return gbl_env }
 
 badBootDecl :: HscSource -> String -> Located decl -> TcM ()
@@ -907,9 +930,13 @@ checkBootTyCon is_boot tc1 tc2
            check (eqTypeX env op_ty1 op_ty2)
                  (text "The types of" <+> pname1 <+>
                   text "are different") `andThenCheck`
-           check (eqMaybeBy eqDM def_meth1 def_meth2)
-                 (text "The default methods associated with" <+> pname1 <+>
-                  text "are different")
+           if is_boot
+               then check (eqMaybeBy eqDM def_meth1 def_meth2)
+                          (text "The default methods associated with" <+> pname1 <+>
+                           text "are different")
+               else check (subDM op_ty1 def_meth1 def_meth2)
+                          (text "The default methods associated with" <+> pname1 <+>
+                           text "are not compatible")
          where
           name1 = idName id1
           name2 = idName id2
@@ -929,6 +956,26 @@ checkBootTyCon is_boot tc1 tc2
        eqDM (_, GenericDM t1) (_, GenericDM t2) = eqTypeX env t1 t2
        eqDM _ _ = False
 
+       -- NB: first argument is from hsig, second is from real impl.
+       -- Order of pattern matching matters.
+       subDM _ Nothing _ = True
+       subDM _ _ Nothing = False
+       -- If the hsig wrote:
+       --
+       --   f :: a -> a
+       --   default f :: a -> a
+       --
+       -- this should be validly implementable using an old-fashioned
+       -- vanilla default method.
+       subDM t1 (Just (_, GenericDM t2)) (Just (_, VanillaDM))
+        = eqTypeX env t1 t2
+       -- This case can occur when merging signatures
+       subDM t1 (Just (_, VanillaDM)) (Just (_, GenericDM t2))
+        = eqTypeX env t1 t2
+       subDM _ (Just (_, VanillaDM)) (Just (_, VanillaDM)) = True
+       subDM _ (Just (_, GenericDM t1)) (Just (_, GenericDM t2))
+        = eqTypeX env t1 t2
+
        -- Ignore the location of the defaults
        eqATDef Nothing             Nothing             = True
        eqATDef (Just (ty1, _loc1)) (Just (ty2, _loc2)) = eqTypeX env ty1 ty2
@@ -938,100 +985,35 @@ checkBootTyCon is_boot tc1 tc2
          eqListBy (eqTypeX env) (mkTyVarTys as1) (mkTyVarTys as2) &&
          eqListBy (eqTypeX env) (mkTyVarTys bs1) (mkTyVarTys bs2)
     in
-    check (roles1 == roles2) roles_msg `andThenCheck`
+    checkRoles roles1 roles2 `andThenCheck`
           -- Checks kind of class
     check (eqListBy eqFD clas_fds1 clas_fds2)
           (text "The functional dependencies do not match") `andThenCheck`
-    checkUnless (null sc_theta1 && null op_stuff1 && null ats1) $
-                     -- Above tests for an "abstract" class.
-                     -- This is duplicated in 'isAbstractIfaceDecl'
-                     -- and also below near
-                     -- Note [Constraint synonym implements abstract class]
+    checkUnless (isAbstractTyCon tc1) $
     check (eqListBy (eqTypeX env) sc_theta1 sc_theta2)
           (text "The class constraints do not match") `andThenCheck`
     checkListBy eqSig op_stuff1 op_stuff2 (text "methods") `andThenCheck`
-    checkListBy eqAT ats1 ats2 (text "associated types")
+    checkListBy eqAT ats1 ats2 (text "associated types") `andThenCheck`
+    check (classMinimalDef c1 `BF.implies` classMinimalDef c2)
+        (text "The MINIMAL pragmas are not compatible")
 
   | Just syn_rhs1 <- synTyConRhs_maybe tc1
   , Just syn_rhs2 <- synTyConRhs_maybe tc2
   , Just env <- eqVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
   = ASSERT(tc1 == tc2)
-    check (roles1 == roles2) roles_msg `andThenCheck`
+    checkRoles roles1 roles2 `andThenCheck`
     check (eqTypeX env syn_rhs1 syn_rhs2) empty   -- nothing interesting to say
 
-  -- A skolem abstract TyCon can be implemented using a type synonym, but ONLY
-  -- if the type synonym is nullary and has no type family applications.
-  -- This arises from two properties of skolem abstract data:
-  --
-  --    For any T (with some number of paramaters),
-  --
-  --    1. T is a valid type (it is "curryable"), and
-  --
-  --    2. T is valid in an instance head (no type families).
-  --
-  -- See also 'HowAbstract' and Note [Skolem abstract data].
-  --
-  | isSkolemAbstractTyCon tc1
+  -- This allows abstract 'data T a' to be implemented using 'type T = ...'
+  -- and abstract 'class K a' to be implement using 'type K = ...'
+  -- See Note [Synonyms implement abstract data]
+  | not is_boot -- don't support for hs-boot yet
+  , isAbstractTyCon tc1
   , Just (tvs, ty) <- synTyConDefn_maybe tc2
   , Just (tc2', args) <- tcSplitTyConApp_maybe ty
-  = check (null (tcTyFamInsts ty))
-          (text "Illegal type family application in implementation of abstract data.")
-            `andThenCheck`
-    check (null tvs)
-          (text "Illegal parameterized type synonym in implementation of abstract data." $$
-           text "(Try eta reducing your type synonym so that it is nullary.)")
-            `andThenCheck`
-    -- Don't report roles errors unless the type synonym is nullary
-    checkUnless (not (null tvs)) $
-        ASSERT( null roles2 )
-        -- If we have something like:
-        --
-        --  signature H where
-        --      data T a
-        --  module H where
-        --      data K a b = ...
-        --      type T = K Int
-        --
-        -- we need to drop the first role of K when comparing!
-        check (roles1 == drop (length args) (tyConRoles tc2')) roles_msg
-
-  -- Note [Constraint synonym implements abstract class]
-  -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-  -- This clause allows an abstract class to be implemented with a constraint
-  -- synonym. For instance, consider a signature requiring an abstract class,
-  --
-  --     signature ASig where
-  --         class K a
-  --
-  -- Since K has no methods (i.e. is abstract), the module implementing this
-  -- signature may want to implement it using a constraint synonym of another
-  -- class,
-  --
-  --     module AnImpl where
-  --         class SomeClass a where ...
-  --         type K a = SomeClass a
-  --
-  -- This was originally requested in #12679.  For now, we only allow this
-  -- in hsig files (@not is_boot@).
-
-  | not is_boot
-  , Just c1 <- tyConClass_maybe tc1
-  , let (_, _clas_fds1, sc_theta1, _, ats1, op_stuff1)
-          = classExtraBigSig c1
-  -- Is it abstract?
-  , null sc_theta1 && null op_stuff1 && null ats1
-  , Just (tvs, ty) <- synTyConDefn_maybe tc2
-  = -- The synonym may or may not be eta-expanded, so we need to
-    -- massage it into the correct form before checking if roles
-    -- match.
-    if length tvs == length roles1
-        then check (roles1 == roles2) roles_msg
-        else case tcSplitTyConApp_maybe ty of
-                Just (tc2', args) ->
-                    check (roles1 == drop (length args) (tyConRoles tc2') ++ roles2)
-                          roles_msg
-                Nothing -> Just roles_msg
-    -- TODO: We really should check if the fundeps are satisfied, but
+  = checkSynAbsData tvs ty tc2' args
+    -- TODO: When it's a synonym implementing a class, we really
+    -- should check if the fundeps are satisfied, but
     -- there is not an obvious way to do this for a constraint synonym.
     -- So for now, let it all through (it won't cause segfaults, anyway).
     -- Tracked at #12704.
@@ -1041,24 +1023,31 @@ checkBootTyCon is_boot tc1 tc2
   = ASSERT(tc1 == tc2)
     let eqFamFlav OpenSynFamilyTyCon   OpenSynFamilyTyCon = True
         eqFamFlav (DataFamilyTyCon {}) (DataFamilyTyCon {}) = True
+        -- This case only happens for hsig merging:
+        eqFamFlav AbstractClosedSynFamilyTyCon AbstractClosedSynFamilyTyCon = True
         eqFamFlav AbstractClosedSynFamilyTyCon (ClosedSynFamilyTyCon {}) = True
         eqFamFlav (ClosedSynFamilyTyCon {}) AbstractClosedSynFamilyTyCon = True
         eqFamFlav (ClosedSynFamilyTyCon ax1) (ClosedSynFamilyTyCon ax2)
             = eqClosedFamilyAx ax1 ax2
         eqFamFlav (BuiltInSynFamTyCon {}) (BuiltInSynFamTyCon {}) = tc1 == tc2
         eqFamFlav _ _ = False
-        injInfo1 = familyTyConInjectivityInfo tc1
-        injInfo2 = familyTyConInjectivityInfo tc2
+        injInfo1 = tyConInjectivityInfo tc1
+        injInfo2 = tyConInjectivityInfo tc2
     in
     -- check equality of roles, family flavours and injectivity annotations
-    check (roles1 == roles2) roles_msg `andThenCheck`
-    check (eqFamFlav fam_flav1 fam_flav2) empty `andThenCheck`
-    check (injInfo1 == injInfo2) empty
+    -- (NB: Type family roles are always nominal. But the check is
+    -- harmless enough.)
+    checkRoles roles1 roles2 `andThenCheck`
+    check (eqFamFlav fam_flav1 fam_flav2)
+        (whenPprDebug $
+            text "Family flavours" <+> ppr fam_flav1 <+> text "and" <+> ppr fam_flav2 <+>
+            text "do not match") `andThenCheck`
+    check (injInfo1 == injInfo2) (text "Injectivities do not match")
 
   | isAlgTyCon tc1 && isAlgTyCon tc2
   , Just env <- eqVarBndrs emptyRnEnv2 (tyConTyVars tc1) (tyConTyVars tc2)
   = ASSERT(tc1 == tc2)
-    check (roles1 == roles2) roles_msg `andThenCheck`
+    checkRoles roles1 roles2 `andThenCheck`
     check (eqListBy (eqTypeX env)
                      (tyConStupidTheta tc1) (tyConStupidTheta tc2))
           (text "The datatype contexts do not match") `andThenCheck`
@@ -1066,13 +1055,129 @@ checkBootTyCon is_boot tc1 tc2
 
   | otherwise = Just empty   -- two very different types -- should be obvious
   where
-    roles1 = tyConRoles tc1
+    roles1 = tyConRoles tc1 -- the abstract one
     roles2 = tyConRoles tc2
     roles_msg = text "The roles do not match." $$
                 (text "Roles on abstract types default to" <+>
                  quotes (text "representational") <+> text "in boot files.")
 
-    eqAlgRhs _ (AbstractTyCon _) _rhs2
+    roles_subtype_msg = text "The roles are not compatible:" $$
+                        text "Main module:" <+> ppr roles2 $$
+                        text "Hsig file:" <+> ppr roles1
+
+    checkRoles r1 r2
+      | is_boot || isInjectiveTyCon tc1 Representational -- See Note [Role subtyping]
+      = check (r1 == r2) roles_msg
+      | otherwise = check (r2 `rolesSubtypeOf` r1) roles_subtype_msg
+
+    -- Note [Role subtyping]
+    -- ~~~~~~~~~~~~~~~~~~~~~
+    -- In the current formulation of roles, role subtyping is only OK if the
+    -- "abstract" TyCon was not representationally injective.  Among the most
+    -- notable examples of non representationally injective TyCons are abstract
+    -- data, which can be implemented via newtypes (which are not
+    -- representationally injective).  The key example is
+    -- in this example from #13140:
+    --
+    --      -- In an hsig file
+    --      data T a -- abstract!
+    --      type role T nominal
+    --
+    --      -- Elsewhere
+    --      foo :: Coercible (T a) (T b) => a -> b
+    --      foo x = x
+    --
+    -- We must NOT allow foo to typecheck, because if we instantiate
+    -- T with a concrete data type with a phantom role would cause
+    -- Coercible (T a) (T b) to be provable.  Fortunately, if T is not
+    -- representationally injective, we cannot make the inference that a ~N b if
+    -- T a ~R T b.
+    --
+    -- Unconditional role subtyping would be possible if we setup
+    -- an extra set of roles saying when we can project out coercions
+    -- (we call these proj-roles); then it would NOT be valid to instantiate T
+    -- with a data type at phantom since the proj-role subtyping check
+    -- would fail.  See #13140 for more details.
+    --
+    -- One consequence of this is we get no role subtyping for non-abstract
+    -- data types in signatures. Suppose you have:
+    --
+    --      signature A where
+    --          type role T nominal
+    --          data T a = MkT
+    --
+    -- If you write this, we'll treat T as injective, and make inferences
+    -- like T a ~R T b ==> a ~N b (mkNthCo).  But if we can
+    -- subsequently replace T with one at phantom role, we would then be able to
+    -- infer things like T Int ~R T Bool which is bad news.
+    --
+    -- We could allow role subtyping here if we didn't treat *any* data types
+    -- defined in signatures as injective.  But this would be a bit surprising,
+    -- replacing a data type in a module with one in a signature could cause
+    -- your code to stop typechecking (whereas if you made the type abstract,
+    -- it is more understandable that the type checker knows less).
+    --
+    -- It would have been best if this was purely a question of defaults
+    -- (i.e., a user could explicitly ask for one behavior or another) but
+    -- the current role system isn't expressive enough to do this.
+    -- Having explict proj-roles would solve this problem.
+
+    rolesSubtypeOf [] [] = True
+    -- NB: this relation is the OPPOSITE of the subroling relation
+    rolesSubtypeOf (x:xs) (y:ys) = x >= y && rolesSubtypeOf xs ys
+    rolesSubtypeOf _ _ = False
+
+    -- Note [Synonyms implement abstract data]
+    -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    -- An abstract data type or class can be implemented using a type synonym,
+    -- but ONLY if the type synonym is nullary and has no type family
+    -- applications.  This arises from two properties of skolem abstract data:
+    --
+    --    For any T (with some number of paramaters),
+    --
+    --    1. T is a valid type (it is "curryable"), and
+    --
+    --    2. T is valid in an instance head (no type families).
+    --
+    -- See also 'HowAbstract' and Note [Skolem abstract data].
+
+    -- | Given @type T tvs = ty@, where @ty@ decomposes into @tc2' args@,
+    -- check that this synonym is an acceptable implementation of @tc1@.
+    -- See Note [Synonyms implement abstract data]
+    checkSynAbsData :: [TyVar] -> Type -> TyCon -> [Type] -> Maybe SDoc
+    checkSynAbsData tvs ty tc2' args =
+        check (null (tcTyFamInsts ty))
+              (text "Illegal type family application in implementation of abstract data.")
+                `andThenCheck`
+        check (null tvs)
+              (text "Illegal parameterized type synonym in implementation of abstract data." $$
+               text "(Try eta reducing your type synonym so that it is nullary.)")
+                `andThenCheck`
+        -- Don't report roles errors unless the type synonym is nullary
+        checkUnless (not (null tvs)) $
+            ASSERT( null roles2 )
+            -- If we have something like:
+            --
+            --  signature H where
+            --      data T a
+            --  module H where
+            --      data K a b = ...
+            --      type T = K Int
+            --
+            -- we need to drop the first role of K when comparing!
+            checkRoles roles1 (drop (length args) (tyConRoles tc2'))
+{-
+        -- Hypothetically, if we were allow to non-nullary type synonyms, here
+        -- is how you would check the roles
+        if length tvs == length roles1
+            then checkRoles roles1 roles2
+            else case tcSplitTyConApp_maybe ty of
+                    Just (tc2', args) ->
+                        checkRoles roles1 (drop (length args) (tyConRoles tc2') ++ roles2)
+                    Nothing -> Just roles_msg
+-}
+
+    eqAlgRhs _ AbstractTyCon _rhs2
       = checkSuccess -- rhs2 is guaranteed to be injective, since it's an AlgTyCon
     eqAlgRhs _  tc1@DataTyCon{} tc2@DataTyCon{} =
         checkListBy eqCon (data_cons tc1) (data_cons tc2) (text "constructors")
@@ -1136,9 +1241,9 @@ missingBootThing is_boot name what
     <+> text "file, but not"
     <+> text what <+> text "the module"
 
-badReexportedBootThing :: Bool -> Name -> Name -> SDoc
-badReexportedBootThing is_boot name name'
-  = withPprStyle (mkUserStyle alwaysQualify AllTheWay) $ vcat
+badReexportedBootThing :: DynFlags -> Bool -> Name -> Name -> SDoc
+badReexportedBootThing dflags is_boot name name'
+  = withPprStyle (mkUserStyle dflags alwaysQualify AllTheWay) $ vcat
         [ text "The" <+> (if is_boot then text "hs-boot" else text "hsig")
            <+> text "file (re)exports" <+> quotes (ppr name)
         , text "but the implementing module exports a different identifier" <+> quotes (ppr name')
@@ -1146,17 +1251,33 @@ badReexportedBootThing is_boot name name'
 
 bootMisMatch :: Bool -> SDoc -> TyThing -> TyThing -> SDoc
 bootMisMatch is_boot extra_info real_thing boot_thing
-  = vcat [ppr real_thing <+>
-          text "has conflicting definitions in the module",
-          text "and its" <+>
-            (if is_boot then text "hs-boot file"
-                       else text "hsig file"),
-          text "Main module:" <+> PprTyThing.pprTyThing real_thing,
-          (if is_boot
-            then text "Boot file:  "
-            else text "Hsig file: ")
-            <+> PprTyThing.pprTyThing boot_thing,
-          extra_info]
+  = pprBootMisMatch is_boot extra_info real_thing real_doc boot_doc
+  where
+    to_doc
+      = pprTyThingInContext $ showToHeader { ss_forall =
+                                              if is_boot
+                                                then ShowForAllMust
+                                                else ShowForAllWhen }
+
+    real_doc = to_doc real_thing
+    boot_doc = to_doc boot_thing
+
+    pprBootMisMatch :: Bool -> SDoc -> TyThing -> SDoc -> SDoc -> SDoc
+    pprBootMisMatch is_boot extra_info real_thing real_doc boot_doc
+      = vcat
+          [ ppr real_thing <+>
+            text "has conflicting definitions in the module",
+            text "and its" <+>
+              (if is_boot
+                then text "hs-boot file"
+                else text "hsig file"),
+            text "Main module:" <+> real_doc,
+              (if is_boot
+                then text "Boot file:  "
+                else text "Hsig file: ")
+                <+> boot_doc,
+            extra_info
+          ]
 
 instMisMatch :: Bool -> ClsInst -> SDoc
 instMisMatch is_boot inst
@@ -1173,13 +1294,13 @@ instMisMatch is_boot inst
 ************************************************************************
 -}
 
-rnTopSrcDecls :: HsGroup RdrName -> TcM (TcGblEnv, HsGroup Name)
+rnTopSrcDecls :: HsGroup GhcPs -> TcM (TcGblEnv, HsGroup GhcRn)
 -- Fails if there are any errors
 rnTopSrcDecls group
  = do { -- Rename the source decls
-        traceRn (text "rn12") ;
+        traceRn "rn12" empty ;
         (tcg_env, rn_decls) <- checkNoErrs $ rnSrcDecls group ;
-        traceRn (text "rn13") ;
+        traceRn "rn13" empty ;
 
         -- save the renamed syntax, if we want it
         let { tcg_env'
@@ -1189,11 +1310,11 @@ rnTopSrcDecls group
                    = tcg_env };
 
                 -- Dump trace of renaming part
-        rnDump (ppr rn_decls) ;
+        rnDump rn_decls ;
         return (tcg_env', rn_decls)
    }
 
-tcTopSrcDecls :: HsGroup Name -> TcM (TcGblEnv, TcLclEnv)
+tcTopSrcDecls :: HsGroup GhcRn -> TcM (TcGblEnv, TcLclEnv)
 tcTopSrcDecls (HsGroup { hs_tyclds = tycl_decls,
                          hs_derivds = deriv_decls,
                          hs_fords  = foreign_decls,
@@ -1370,31 +1491,31 @@ tcPreludeClashWarn warnFlag name = do
     --   c) Prelude is imported hiding the name in question. Issue no warnings.
     --   d) Qualified import of Prelude, no warnings.
     importedViaPrelude :: Name
-                       -> [ImportDecl Name]
+                       -> [ImportDecl GhcRn]
                        -> Bool
     importedViaPrelude name = any importViaPrelude
       where
-        isPrelude :: ImportDecl Name -> Bool
+        isPrelude :: ImportDecl GhcRn -> Bool
         isPrelude imp = unLoc (ideclName imp) == pRELUDE_NAME
 
         -- Implicit (Prelude) import?
-        isImplicit :: ImportDecl Name -> Bool
+        isImplicit :: ImportDecl GhcRn -> Bool
         isImplicit = ideclImplicit
 
         -- Unqualified import?
-        isUnqualified :: ImportDecl Name -> Bool
+        isUnqualified :: ImportDecl GhcRn -> Bool
         isUnqualified = not . ideclQualified
 
         -- List of explicitly imported (or hidden) Names from a single import.
         --   Nothing -> No explicit imports
         --   Just (False, <names>) -> Explicit import list of <names>
         --   Just (True , <names>) -> Explicit hiding of <names>
-        importListOf :: ImportDecl Name -> Maybe (Bool, [Name])
+        importListOf :: ImportDecl GhcRn -> Maybe (Bool, [Name])
         importListOf = fmap toImportList . ideclHiding
           where
             toImportList (h, loc) = (h, map (ieName . unLoc) (unLoc loc))
 
-        isExplicit :: ImportDecl Name -> Bool
+        isExplicit :: ImportDecl GhcRn -> Bool
         isExplicit x = case importListOf x of
             Nothing -> False
             Just (False, explicit)
@@ -1404,7 +1525,7 @@ tcPreludeClashWarn warnFlag name = do
 
         -- Check whether the given name would be imported (unqualified) from
         -- an import declaration.
-        importViaPrelude :: ImportDecl Name -> Bool
+        importViaPrelude :: ImportDecl GhcRn -> Bool
         importViaPrelude x = isPrelude x
                           && isUnqualified x
                           && (isImplicit x || isExplicit x)
@@ -1483,13 +1604,15 @@ tcMissingParentClassWarn warnFlag isName shouldName
 
 
 ---------------------------
-tcTyClsInstDecls :: [TyClGroup Name]
-                 -> [LDerivDecl Name]
-                 -> [(RecFlag, LHsBinds Name)]
+tcTyClsInstDecls :: [TyClGroup GhcRn]
+                 -> [LDerivDecl GhcRn]
+                 -> [(RecFlag, LHsBinds GhcRn)]
                  -> TcM (TcGblEnv,            -- The full inst env
-                         [InstInfo Name],     -- Source-code instance decls to process;
-                                              -- contains all dfuns for this module
-                          HsValBinds Name)    -- Supporting bindings for derived instances
+                         [InstInfo GhcRn],    -- Source-code instance decls to
+                                              -- process; contains all dfuns for
+                                              -- this module
+                          HsValBinds GhcRn)   -- Supporting bindings for derived
+                                              -- instances
 
 tcTyClsInstDecls tycl_decls deriv_decls binds
  = tcAddDataFamConPlaceholders (tycl_decls >>= group_instds) $
@@ -1544,14 +1667,16 @@ check_main dflags tcg_env explicit_mod_hdr
              Just main_name -> do
 
         { traceTc "checkMain found" (ppr main_mod <+> ppr main_fn)
-        ; let loc = srcLocSpan (getSrcLoc main_name)
+        ; let loc       = srcLocSpan (getSrcLoc main_name)
         ; ioTyCon <- tcLookupTyCon ioTyConName
         ; res_ty <- newFlexiTyVarTy liftedTypeKind
-        ; main_expr
-                <- addErrCtxt mainCtxt    $
-                   tcMonoExpr (L loc (HsVar (L loc main_name)))
-                                            (mkCheckExpType $
-                                             mkTyConApp ioTyCon [res_ty])
+        ; let io_ty = mkTyConApp ioTyCon [res_ty]
+              skol_info = SigSkol (FunSigCtxt main_name False) io_ty []
+        ; (ev_binds, main_expr)
+               <- checkConstraints skol_info [] [] $
+                  addErrCtxt mainCtxt    $
+                  tcMonoExpr (L loc (HsVar (L loc main_name)))
+                             (mkCheckExpType io_ty)
 
                 -- See Note [Root-main Id]
                 -- Construct the binding
@@ -1563,7 +1688,8 @@ check_main dflags tcg_env explicit_mod_hdr
               ; root_main_id = Id.mkExportedVanillaId root_main_name
                                                       (mkTyConApp ioTyCon [res_ty])
               ; co  = mkWpTyApps [res_ty]
-              ; rhs = nlHsApp (mkLHsWrap co (nlHsVar run_main_id)) main_expr
+              ; rhs = mkHsDictLet ev_binds $
+                      nlHsApp (mkLHsWrap co (nlHsVar run_main_id)) main_expr
               ; main_bind = mkVarBind root_main_id rhs }
 
         ; return (tcg_env { tcg_main  = Just main_name,
@@ -1654,14 +1780,19 @@ runTcInteractive hsc_env thing_inside
                       vcat (map ppr [ local_gres | gres <- occEnvElts (ic_rn_gbl_env icxt)
                                                  , let local_gres = filter isLocalGRE gres
                                                  , not (null local_gres) ]) ]
-       ; let getOrphans m = fmap (\iface -> mi_module iface
+
+       ; let getOrphans m mb_pkg = fmap (\iface -> mi_module iface
                                           : dep_orphs (mi_deps iface))
                                  (loadSrcInterface (text "runTcInteractive") m
-                                                   False Nothing)
+                                                   False mb_pkg)
+
        ; orphs <- fmap concat . forM (ic_imports icxt) $ \i ->
             case i of
-                IIModule n -> getOrphans n
-                IIDecl i -> getOrphans (unLoc (ideclName i))
+                IIModule n -> getOrphans n Nothing
+                IIDecl i ->
+                  let mb_pkg = sl_fs <$> ideclPkgQual i in
+                  getOrphans (unLoc (ideclName i)) mb_pkg
+
        ; let imports = emptyImportAvails {
                             imp_orphs = orphs
                         }
@@ -1719,7 +1850,7 @@ runTcInteractive hsc_env thing_inside
 
 {- Note [Initialising the type environment for GHCi]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Most of the the Ids in ic_things, defined by the user in 'let' stmts,
+Most of the Ids in ic_things, defined by the user in 'let' stmts,
 have closed types. E.g.
    ghci> let foo x y = x && not y
 
@@ -1746,14 +1877,13 @@ lead to duplicate "perhaps you meant..." suggestions (e.g. T5564).
 We don't bother with the tcl_th_bndrs environment either.
 -}
 
-#ifdef GHCI
 -- | The returned [Id] is the list of new Ids bound by this statement. It can
 -- be used to extend the InteractiveContext via extendInteractiveContext.
 --
 -- The returned TypecheckedHsExpr is of type IO [ () ], a list of the bound
 -- values, coerced to ().
-tcRnStmt :: HscEnv -> GhciLStmt RdrName
-         -> IO (Messages, Maybe ([Id], LHsExpr Id, FixityEnv))
+tcRnStmt :: HscEnv -> GhciLStmt GhcPs
+         -> IO (Messages, Maybe ([Id], LHsExpr GhcTc, FixityEnv))
 tcRnStmt hsc_env rdr_stmt
   = runTcInteractive hsc_env $ do {
 
@@ -1762,6 +1892,9 @@ tcRnStmt hsc_env rdr_stmt
     zonked_expr <- zonkTopLExpr tc_expr ;
     zonked_ids  <- zonkTopBndrs bound_ids ;
 
+    failIfErrsM ;  -- we can't do the next step if there are levity polymorphism errors
+                   -- test case: ghci/scripts/T13202{,a}
+
         -- None of the Ids should be of unboxed type, because we
         -- cast them all to HValues in the end!
     mapM_ bad_unboxed (filter (isUnliftedType . idType) zonked_ids) ;
@@ -1825,7 +1958,7 @@ Here is the grand plan, implemented in tcUserStmt
 -}
 
 -- | A plan is an attempt to lift some code into the IO monad.
-type PlanResult = ([Id], LHsExpr Id)
+type PlanResult = ([Id], LHsExpr GhcTc)
 type Plan = TcM PlanResult
 
 -- | Try the plans in order. If one fails (by raising an exn), try the next.
@@ -1833,7 +1966,7 @@ type Plan = TcM PlanResult
 runPlans :: [Plan] -> TcM PlanResult
 runPlans []     = panic "runPlans"
 runPlans [p]    = p
-runPlans (p:ps) = tryTcLIE_ (runPlans ps) p
+runPlans (p:ps) = tryTcDiscardingErrs (runPlans ps) p
 
 -- | Typecheck (and 'lift') a stmt entered by the user in GHCi into the
 -- GHCi 'environment'.
@@ -1843,7 +1976,7 @@ runPlans (p:ps) = tryTcLIE_ (runPlans ps) p
 -- in GHCi] in HscTypes for more details. We do this lifting by trying
 -- different ways ('plans') of lifting the code into the IO monad and
 -- type checking each plan until one succeeds.
-tcUserStmt :: GhciLStmt RdrName -> TcM (PlanResult, FixityEnv)
+tcUserStmt :: GhciLStmt GhcPs -> TcM (PlanResult, FixityEnv)
 
 -- An expression typed at the prompt is treated very specially
 tcUserStmt (L loc (BodyStmt expr _ _ _))
@@ -1853,7 +1986,7 @@ tcUserStmt (L loc (BodyStmt expr _ _ _))
         ; uniq <- newUnique
         ; interPrintName <- getInteractivePrintName
         ; let fresh_it  = itName uniq loc
-              matches   = [mkMatch (FunRhs (L loc fresh_it) Prefix) [] rn_expr
+              matches   = [mkMatch (mkPrefixFunRhs (L loc fresh_it)) [] rn_expr
                                    (noLoc emptyLocalBinds)]
               -- [it = expr]
               the_bind  = L loc $ (mkTopFunBind FromSource (L loc fresh_it) matches) { bind_fvs = fvs }
@@ -1877,24 +2010,30 @@ tcUserStmt (L loc (BodyStmt expr _ _ _))
                                            (mkRnSyntaxExpr thenIOName)
                                                   noSyntaxExpr placeHolderType
 
-        -- The plans are:
-        --   A. [it <- e; print it]     but not if it::()
-        --   B. [it <- e]
-        --   C. [let it = e; print it]
-        --
-        -- Ensure that type errors don't get deferred when type checking the
-        -- naked expression. Deferring type errors here is unhelpful because the
-        -- expression gets evaluated right away anyway. It also would potentially
-        -- emit two redundant type-error warnings, one from each plan.
-        ; plan <- unsetGOptM Opt_DeferTypeErrors $
-                  unsetGOptM Opt_DeferTypedHoles $ runPlans [
+              -- NewA
+              no_it_a = L loc $ BodyStmt (nlHsApps bindIOName
+                                       [rn_expr , nlHsVar interPrintName])
+                                       (mkRnSyntaxExpr thenIOName)
+                                       noSyntaxExpr placeHolderType
+
+              no_it_b = L loc $ BodyStmt (rn_expr)
+                                       (mkRnSyntaxExpr thenIOName)
+                                       noSyntaxExpr placeHolderType
+
+              no_it_c = L loc $ BodyStmt (nlHsApp (nlHsVar interPrintName) rn_expr)
+                                       (mkRnSyntaxExpr thenIOName)
+                                       noSyntaxExpr placeHolderType
+
+              -- See Note [GHCi Plans]
+
+              it_plans = [
                     -- Plan A
                     do { stuff@([it_id], _) <- tcGhciStmts [bind_stmt, print_it]
                        ; it_ty <- zonkTcType (idType it_id)
                        ; when (isUnitTy $ it_ty) failM
                        ; return stuff },
 
-                        -- Plan B; a naked bind statment
+                        -- Plan B; a naked bind statement
                     tcGhciStmts [bind_stmt],
 
                         -- Plan C; check that the let-binding is typeable all by itself.
@@ -1906,6 +2045,25 @@ tcUserStmt (L loc (BodyStmt expr _ _ _))
                                 --- checkNoErrs defeats the error recovery of let-bindings
                        ; tcGhciStmts [let_stmt, print_it] } ]
 
+              -- Plans where we don't bind "it"
+              no_it_plans = [
+                    tcGhciStmts [no_it_a] ,
+                    tcGhciStmts [no_it_b] ,
+                    tcGhciStmts [no_it_c] ]
+
+
+        -- Ensure that type errors don't get deferred when type checking the
+        -- naked expression. Deferring type errors here is unhelpful because the
+        -- expression gets evaluated right away anyway. It also would potentially
+        -- emit two redundant type-error warnings, one from each plan.
+        ; generate_it <- goptM Opt_NoIt
+        ; plan <- unsetGOptM Opt_DeferTypeErrors $
+                  unsetGOptM Opt_DeferTypedHoles $
+                    runPlans $ if generate_it
+                                 then no_it_plans
+                                 else it_plans
+
+
         ; fix_env <- getFixityEnv
         ; return (plan, fix_env) }
 
@@ -1915,8 +2073,8 @@ tcUserStmt rdr_stmt@(L loc _)
              fix_env <- getFixityEnv
              return (fix_env, emptyFVs)
             -- Don't try to typecheck if the renamer fails!
-       ; traceRn (text "tcRnStmt" <+> vcat [ppr rdr_stmt, ppr rn_stmt, ppr fvs])
-       ; rnDump (ppr rn_stmt) ;
+       ; traceRn "tcRnStmt" (vcat [ppr rdr_stmt, ppr rn_stmt, ppr fvs])
+       ; rnDump rn_stmt ;
 
        ; ghciStep <- getGhciStepIO
        ; let gi_stmt
@@ -1947,9 +2105,30 @@ tcUserStmt rdr_stmt@(L loc _)
                                     (mkRnSyntaxExpr thenIOName) noSyntaxExpr
                                     placeHolderType
 
+{-
+Note [GHCi Plans]
+
+When a user types an expression in the repl we try to print it in three different
+ways. Also, depending on whether -fno-it is set, we bind a variable called `it`
+which can be used to refer to the result of the expression subsequently in the repl.
+
+The normal plans are :
+  A. [it <- e; print e]     but not if it::()
+  B. [it <- e]
+  C. [let it = e; print it]
+
+When -fno-it is set, the plans are:
+  A. [e >>= print]
+  B. [e]
+  C. [let it = e in print it]
+
+The reason for -fno-it is explained in #14336. `it` can lead to the repl
+leaking memory as it is repeatedly queried.
+-}
+
 -- | Typecheck the statements given and then return the results of the
 -- statement in the form 'IO [()]'.
-tcGhciStmts :: [GhciLStmt Name] -> TcM PlanResult
+tcGhciStmts :: [GhciLStmt GhcRn] -> TcM PlanResult
 tcGhciStmts stmts
  = do { ioTyCon <- tcLookupTyCon ioTyConName ;
         ret_id  <- tcLookupId returnIOName ;            -- return @ IO
@@ -1963,18 +2142,15 @@ tcGhciStmts stmts
 
         -- OK, we're ready to typecheck the stmts
         traceTc "TcRnDriver.tcGhciStmts: tc stmts" empty ;
-        ((tc_stmts, ids), lie) <- captureConstraints $
+        ((tc_stmts, ids), lie) <- captureTopConstraints $
                                   tc_io_stmts $ \ _ ->
                                   mapM tcLookupId names  ;
                         -- Look up the names right in the middle,
                         -- where they will all be in scope
 
-        -- wanted constraints from static forms
-        stWC <- tcg_static_wc <$> getGblEnv >>= readTcRef ;
-
         -- Simplify the context
         traceTc "TcRnDriver.tcGhciStmts: simplify ctxt" empty ;
-        const_binds <- checkNoErrs (simplifyInteractive (andWC stWC lie)) ;
+        const_binds <- checkNoErrs (simplifyInteractive lie) ;
                 -- checkNoErrs ensures that the plan fails if context redn fails
 
         traceTc "TcRnDriver.tcGhciStmts: done" empty ;
@@ -1993,7 +2169,7 @@ tcGhciStmts stmts
                        (noLoc $ ExplicitList unitTy Nothing (map mk_item ids)) ;
             mk_item id = let ty_args = [idType id, unitTy] in
                          nlHsApp (nlHsTyApp unsafeCoerceId
-                                   (map (getRuntimeRep "tcGhciStmts") ty_args ++ ty_args))
+                                   (map getRuntimeRep ty_args ++ ty_args))
                                  (nlHsVar id) ;
             stmts = tc_stmts ++ [noLoc (mkLastStmt ret_expr)]
         } ;
@@ -2002,7 +2178,7 @@ tcGhciStmts stmts
     }
 
 -- | Generate a typed ghciStepIO expression (ghciStep :: Ty a -> IO a)
-getGhciStepIO :: TcM (LHsExpr Name)
+getGhciStepIO :: TcM (LHsExpr GhcRn)
 getGhciStepIO = do
     ghciTy <- getGHCiMonad
     a_tv <- newName (mkTyVarOccFS (fsLit "a"))
@@ -2012,7 +2188,7 @@ getGhciStepIO = do
         step_ty = noLoc $ HsForAllTy { hst_bndrs = [noLoc $ UserTyVar (noLoc a_tv)]
                                      , hst_body  = nlHsFunTy ghciM ioM }
 
-        stepTy :: LHsSigWcType Name
+        stepTy :: LHsSigWcType GhcRn
         stepTy = mkEmptyWildCardBndrs (mkEmptyImplicitBndrs step_ty)
 
     return (noLoc $ ExprWithTySig (nlHsVar ghciStepIoMName) stepTy)
@@ -2042,7 +2218,7 @@ data TcRnExprMode = TM_Inst    -- ^ Instantiate the type fully (:type)
 -- | tcRnExpr just finds the type of an expression
 tcRnExpr :: HscEnv
          -> TcRnExprMode
-         -> LHsExpr RdrName
+         -> LHsExpr GhcPs
          -> IO (Messages, Maybe Type)
 tcRnExpr hsc_env mode rdr_expr
   = runTcInteractive hsc_env $
@@ -2055,7 +2231,7 @@ tcRnExpr hsc_env mode rdr_expr
         -- it might have a rank-2 type (e.g. :t runST)
     uniq <- newUnique ;
     let { fresh_it  = itName uniq (getLoc rdr_expr)
-        ; orig = exprCtOrigin (unLoc rn_expr) } ;
+        ; orig = lexprCtOrigin rn_expr } ;
     (tclvl, lie, res_ty)
           <- pushLevelAndCaptureConstraints $
              do { (_tc_expr, expr_ty) <- tcInferSigma rn_expr
@@ -2064,19 +2240,17 @@ tcRnExpr hsc_env mode rdr_expr
                   else return expr_ty } ;
 
     -- Generalise
-    ((qtvs, dicts, _), lie_top) <- captureConstraints $
-                                   {-# SCC "simplifyInfer" #-}
-                                   simplifyInfer tclvl
+    ((qtvs, dicts, _, _), lie_top) <- captureTopConstraints $
+                                      {-# SCC "simplifyInfer" #-}
+                                      simplifyInfer tclvl
                                                  infer_mode
                                                  []    {- No sig vars -}
                                                  [(fresh_it, res_ty)]
                                                  lie ;
-    -- Wanted constraints from static forms
-    stWC <- tcg_static_wc <$> getGblEnv >>= readTcRef ;
 
     -- Ignore the dictionary bindings
     _ <- perhaps_disable_default_warnings $
-         simplifyInteractive (andWC stWC lie_top) ;
+         simplifyInteractive lie_top ;
 
     let { all_expr_ty = mkInvForAllTys qtvs (mkLamTypes dicts res_ty) } ;
     ty <- zonkTcType all_expr_ty ;
@@ -2090,7 +2264,7 @@ tcRnExpr hsc_env mode rdr_expr
     return (snd (normaliseType fam_envs Nominal ty))
     }
   where
-    -- See Note [Deeply instantiate in :type]
+    -- See Note [TcRnExprMode]
     (inst, infer_mode, perhaps_disable_default_warnings) = case mode of
       TM_Inst    -> (True,  NoRestrictions, id)
       TM_NoInst  -> (False, NoRestrictions, id)
@@ -2098,7 +2272,7 @@ tcRnExpr hsc_env mode rdr_expr
 
 --------------------------
 tcRnImportDecls :: HscEnv
-                -> [LImportDecl RdrName]
+                -> [LImportDecl GhcPs]
                 -> IO (Messages, Maybe GlobalRdrEnv)
 -- Find the new chunk of GlobalRdrEnv created by this list of import
 -- decls.  In contract tcRnImports *extends* the TcGblEnv.
@@ -2113,7 +2287,7 @@ tcRnImportDecls hsc_env import_decls
 -- tcRnType just finds the kind of a type
 tcRnType :: HscEnv
          -> Bool        -- Normalise the returned type
-         -> LHsType RdrName
+         -> LHsType GhcPs
          -> IO (Messages, Maybe (Type, Kind))
 tcRnType hsc_env normalise rdr_type
   = runTcInteractive hsc_env $
@@ -2130,7 +2304,7 @@ tcRnType hsc_env normalise rdr_type
        ; traceTc "tcRnType" (vcat [ppr wcs, ppr rn_type])
        ; (ty, kind) <- solveEqualities $
                        tcWildCardBinders wcs  $ \ _ ->
-                       tcLHsType rn_type
+                       tcLHsTypeUnsaturated rn_type
 
        -- Do kind generalisation; see Note [Kind-generalise in tcRnType]
        ; kvs <- kindGeneralize kind
@@ -2237,7 +2411,7 @@ tcRnDeclsi exists to allow class, data, and other declarations in GHCi.
 -}
 
 tcRnDeclsi :: HscEnv
-           -> [LHsDecl RdrName]
+           -> [LHsDecl GhcPs]
            -> IO (Messages, Maybe TcGblEnv)
 tcRnDeclsi hsc_env local_decls
   = runTcInteractive hsc_env $
@@ -2248,7 +2422,6 @@ externaliseAndTidyId this_mod id
   = do { name' <- externaliseName this_mod (idName id)
        ; return (globaliseAndTidyId (setIdName id name')) }
 
-#endif /* GHCi */
 
 {-
 ************************************************************************
@@ -2258,7 +2431,6 @@ externaliseAndTidyId this_mod id
 ************************************************************************
 -}
 
-#ifdef GHCI
 -- | ASSUMES that the module is either in the 'HomePackageTable' or is
 -- a package module with an interface on disk.  If neither of these is
 -- true, then the result will be an error indicating the interface
@@ -2282,7 +2454,6 @@ tcRnLookupRdrName hsc_env (L loc rdr_name)
        ; let names = concat names_s
        ; when (null names) (addErrTc (text "Not in scope:" <+> quotes (ppr rdr_name)))
        ; return names }
-#endif
 
 tcRnLookupName :: HscEnv -> Name -> IO (Messages, Maybe TyThing)
 tcRnLookupName hsc_env name
@@ -2303,7 +2474,8 @@ tcRnLookupName' name = do
 
 tcRnGetInfo :: HscEnv
             -> Name
-            -> IO (Messages, Maybe (TyThing, Fixity, [ClsInst], [FamInst]))
+            -> IO ( Messages
+                  , Maybe (TyThing, Fixity, [ClsInst], [FamInst], SDoc))
 
 -- Used to implement :info in GHCi
 --
@@ -2323,8 +2495,17 @@ tcRnGetInfo hsc_env name
        ; thing  <- tcRnLookupName' name
        ; fixity <- lookupFixityRn name
        ; (cls_insts, fam_insts) <- lookupInsts thing
-       ; return (thing, fixity, cls_insts, fam_insts) }
+       ; let info = lookupKnownNameInfo name
+       ; return (thing, fixity, cls_insts, fam_insts, info) }
 
+
+-- Lookup all class and family instances for a type constructor.
+--
+-- This function filters all instances in the type environment, so there
+-- is a lot of duplicated work if it is called many times in the same
+-- type environment. If this becomes a problem, the NameEnv computed
+-- in GHC.getNameToInstancesIndex could be cached in TcM and both functions
+-- could be changed to consult that index.
 lookupInsts :: TyThing -> TcM ([ClsInst],[FamInst])
 lookupInsts (ATyCon tc)
   = do  { InstEnvs { ie_global = pkg_ie, ie_local = home_ie, ie_visible = vis_mods } <- tcGetInstEnvs
@@ -2378,9 +2559,9 @@ loadUnqualIfaces hsc_env ictxt
 ************************************************************************
 -}
 
-rnDump :: SDoc -> TcRn ()
+rnDump :: (Outputable a, Data a) => a -> TcRn ()
 -- Dump, with a banner, if -ddump-rn
-rnDump doc = do { traceOptTcRn Opt_D_dump_rn (mkDumpDoc "Renamer" doc) }
+rnDump rn = do { traceOptTcRn Opt_D_dump_rn (mkDumpDoc "Renamer" (ppr rn)) }
 
 tcDump :: TcGblEnv -> TcRn ()
 tcDump env
@@ -2391,13 +2572,17 @@ tcDump env
              (printForUserTcRn short_dump) ;
 
         -- Dump bindings if -ddump-tc
-        traceOptTcRn Opt_D_dump_tc (mkDumpDoc "Typechecker" full_dump)
+        traceOptTcRn Opt_D_dump_tc (mkDumpDoc "Typechecker" full_dump);
+
+        -- Dump bindings as an hsSyn AST if -ddump-tc-ast
+        traceOptTcRn Opt_D_dump_tc_ast (mkDumpDoc "Typechecker" ast_dump)
    }
   where
     short_dump = pprTcGblEnv env
     full_dump  = pprLHsBinds (tcg_binds env)
         -- NB: foreign x-d's have undefined's in their types;
         --     hence can't show the tc_fords
+    ast_dump = showAstData NoBlankSrcSpan (tcg_binds env)
 
 -- It's unpleasant having both pprModGuts and pprModDetails here
 pprTcGblEnv :: TcGblEnv -> SDoc
@@ -2414,38 +2599,40 @@ pprTcGblEnv (TcGblEnv { tcg_type_env  = type_env,
          , vcat (map ppr rules)
          , vcat (map ppr vects)
          , text "Dependent modules:" <+>
-                pprUDFM (imp_dep_mods imports) ppr
+                pprUFM (imp_dep_mods imports) (ppr . sort)
          , text "Dependent packages:" <+>
-                ppr (sortBy compare $ imp_dep_pkgs imports)]
-  where         -- The use of sortBy is just to reduce unnecessary
+                ppr (S.toList $ imp_dep_pkgs imports)]
+  where         -- The use of sort is just to reduce unnecessary
                 -- wobbling in testsuite output
 
 ppr_types :: TypeEnv -> SDoc
-ppr_types type_env
-  = text "TYPE SIGNATURES" $$ nest 2 (ppr_sigs ids)
-  where
+ppr_types type_env = getPprDebug $ \dbg ->
+  let
     ids = [id | id <- typeEnvIds type_env, want_sig id]
-    want_sig id | opt_PprStyle_Debug
+    want_sig id | dbg
                 = True
                 | otherwise
                 = isExternalName (idName id) &&
                   (not (isDerivedOccName (getOccName id)))
         -- Top-level user-defined things have External names.
         -- Suppress internally-generated things unless -dppr-debug
+  in
+  text "TYPE SIGNATURES" $$ nest 2 (ppr_sigs ids)
 
 ppr_tycons :: [FamInst] -> TypeEnv -> SDoc
-ppr_tycons fam_insts type_env
-  = vcat [ text "TYPE CONSTRUCTORS"
-         ,   nest 2 (ppr_tydecls tycons)
-         , text "COERCION AXIOMS"
-         ,   nest 2 (vcat (map pprCoAxiom (typeEnvCoAxioms type_env))) ]
-  where
+ppr_tycons fam_insts type_env = getPprDebug $ \dbg ->
+  let
     fi_tycons = famInstsRepTyCons fam_insts
     tycons = [tycon | tycon <- typeEnvTyCons type_env, want_tycon tycon]
-    want_tycon tycon | opt_PprStyle_Debug = True
-                     | otherwise          = not (isImplicitTyCon tycon) &&
-                                            isExternalName (tyConName tycon) &&
-                                            not (tycon `elem` fi_tycons)
+    want_tycon tycon | dbg        = True
+                     | otherwise  = not (isImplicitTyCon tycon) &&
+                                    isExternalName (tyConName tycon) &&
+                                    not (tycon `elem` fi_tycons)
+  in
+  vcat [ text "TYPE CONSTRUCTORS"
+       ,   nest 2 (ppr_tydecls tycons)
+       , text "COERCION AXIOMS"
+       ,   nest 2 (vcat (map pprCoAxiom (typeEnvCoAxioms type_env))) ]
 
 ppr_insts :: [ClsInst] -> SDoc
 ppr_insts []     = empty
@@ -2470,7 +2657,7 @@ ppr_tydecls tycons
   = vcat [ ppr (tyThingToIfaceDecl (ATyCon tc))
          | tc <- sortBy (comparing getOccName) tycons ]
     -- The Outputable instance for IfaceDecl uses
-    -- showAll, which is what we want here, whereas
+    -- showToIface, which is what we want here, whereas
     -- pprTyThing uses ShowSome.
 
 {-
@@ -2502,7 +2689,7 @@ withTcPlugins hsc_env m =
        return (solve s, stop s)
 
 loadTcPlugins :: HscEnv -> IO [TcPlugin]
-#ifndef GHCI
+#if !defined(GHCI)
 loadTcPlugins _ = return []
 #else
 loadTcPlugins hsc_env =