WIPwip/clean-refactor

14 files changed, 913 insertions, 568 deletions

diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index 269063ae65..bc59436bc4 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -56,7 +56,8 @@ import GHC.Hs
 
 import GHC.Tc.Errors.Types
 import GHC.Tc.Types.Constraint
-import {-# SOURCE #-} GHC.Tc.Types( getLclEnvLoc, lclEnvInGeneratedCode, TcTyThing )
+import {-# SOURCE #-} GHC.Tc.Types( getLclEnvLoc, lclEnvInGeneratedCode )
+import GHC.Tc.Types.TcTyThing
 import GHC.Tc.Types.Origin
 import GHC.Tc.Types.Rank (Rank(..))
 import GHC.Tc.Utils.TcType
@@ -103,7 +104,6 @@ import Data.List ( groupBy, sortBy, tails
 import Data.Ord ( comparing )
 import Data.Bifunctor
 import qualified Language.Haskell.TH as TH
-import {-# SOURCE #-} GHC.Tc.Types (pprTcTyThingCategory)
 import GHC.Iface.Errors.Types
 import GHC.Iface.Errors.Ppr
 
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 68c5ca2869..772c5fdbb8 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -124,7 +124,7 @@ module GHC.Tc.Errors.Types (
 import GHC.Prelude
 
 import GHC.Hs
-import {-# SOURCE #-} GHC.Tc.Types (TcIdSigInfo, TcTyThing)
+import GHC.Tc.Types.TcTyThing -- (TcIdSigInfo, TcTyThing)
 import {-# SOURCE #-} GHC.Tc.Errors.Hole.FitTypes (HoleFit)
 import GHC.Tc.Types.Constraint
 import GHC.Tc.Types.Evidence (EvBindsVar)
@@ -178,6 +178,10 @@ import GHC.Unit.Module.ModIface
 import GHC.Generics ( Generic )
 import GHC.Types.Name.Env (NameEnv)
 import GHC.Iface.Errors.Types
+import GHC.Tc.Errors.Types.PromotionErr
+import GHC.Tc.Types.TcIdSigInfo
+
+
 
 {-
 Note [Migrating TcM Messages]
@@ -5186,46 +5190,6 @@ discardMsg :: SDoc
 discardMsg = text "(Some bindings suppressed;" <+>
              text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
 
-data PromotionErr
-  = TyConPE          -- TyCon used in a kind before we are ready
-                     --     data T :: T -> * where ...
-  | ClassPE          -- Ditto Class
-
-  | FamDataConPE     -- Data constructor for a data family
-                     -- See Note [AFamDataCon: not promoting data family constructors]
-                     -- in GHC.Tc.Utils.Env.
-  | ConstrainedDataConPE ThetaType -- Data constructor with a context
-                                   -- See Note [No constraints in kinds] in GHC.Tc.Validity
-  | PatSynPE         -- Pattern synonyms
-                     -- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env
-
-  | RecDataConPE     -- Data constructor in a recursive loop
-                     -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
-  | TermVariablePE   -- See Note [Promoted variables in types]
-  | NoDataKindsDC    -- -XDataKinds not enabled (for a datacon)
-
-instance Outputable PromotionErr where
-  ppr ClassPE              = text "ClassPE"
-  ppr TyConPE              = text "TyConPE"
-  ppr PatSynPE             = text "PatSynPE"
-  ppr FamDataConPE         = text "FamDataConPE"
-  ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta)
-  ppr RecDataConPE         = text "RecDataConPE"
-  ppr NoDataKindsDC        = text "NoDataKindsDC"
-  ppr TermVariablePE       = text "TermVariablePE"
-
-pprPECategory :: PromotionErr -> SDoc
-pprPECategory = text . capitalise . peCategory
-
-peCategory :: PromotionErr -> String
-peCategory ClassPE              = "class"
-peCategory TyConPE              = "type constructor"
-peCategory PatSynPE             = "pattern synonym"
-peCategory FamDataConPE         = "data constructor"
-peCategory ConstrainedDataConPE{} = "data constructor"
-peCategory RecDataConPE         = "data constructor"
-peCategory NoDataKindsDC        = "data constructor"
-peCategory TermVariablePE       = "term variable"
 
 -- | Stores the information to be reported in a representation-polymorphism
 -- error message.
diff --git a/compiler/GHC/Tc/Errors/Types/PromotionErr.hs b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
new file mode 100644
index 0000000000..2de61c5aa3
--- /dev/null
+++ b/compiler/GHC/Tc/Errors/Types/PromotionErr.hs
@@ -0,0 +1,47 @@
+module GHC.Tc.Errors.Types.PromotionErr where
+
+import GHC.Prelude
+import GHC.Core.Type (ThetaType)
+import GHC.Utils.Outputable
+import GHC.Utils.Misc
+
+data PromotionErr
+  = TyConPE          -- TyCon used in a kind before we are ready
+                     --     data T :: T -> * where ...
+  | ClassPE          -- Ditto Class
+
+  | FamDataConPE     -- Data constructor for a data family
+                     -- See Note [AFamDataCon: not promoting data family constructors]
+                     -- in GHC.Tc.Utils.Env.
+  | ConstrainedDataConPE ThetaType -- Data constructor with a context
+                                   -- See Note [No constraints in kinds] in GHC.Tc.Validity
+  | PatSynPE         -- Pattern synonyms
+                     -- See Note [Don't promote pattern synonyms] in GHC.Tc.Utils.Env
+
+  | RecDataConPE     -- Data constructor in a recursive loop
+                     -- See Note [Recursion and promoting data constructors] in GHC.Tc.TyCl
+  | TermVariablePE   -- See Note [Promoted variables in types]
+  | NoDataKindsDC    -- -XDataKinds not enabled (for a datacon)
+
+instance Outputable PromotionErr where
+  ppr ClassPE              = text "ClassPE"
+  ppr TyConPE              = text "TyConPE"
+  ppr PatSynPE             = text "PatSynPE"
+  ppr FamDataConPE         = text "FamDataConPE"
+  ppr (ConstrainedDataConPE theta) = text "ConstrainedDataConPE" <+> parens (ppr theta)
+  ppr RecDataConPE         = text "RecDataConPE"
+  ppr NoDataKindsDC        = text "NoDataKindsDC"
+  ppr TermVariablePE       = text "TermVariablePE"
+
+pprPECategory :: PromotionErr -> SDoc
+pprPECategory = text . capitalise . peCategory
+
+peCategory :: PromotionErr -> String
+peCategory ClassPE              = "class"
+peCategory TyConPE              = "type constructor"
+peCategory PatSynPE             = "pattern synonym"
+peCategory FamDataConPE         = "data constructor"
+peCategory ConstrainedDataConPE{} = "data constructor"
+peCategory RecDataConPE         = "data constructor"
+peCategory NoDataKindsDC        = "data constructor"
+peCategory TermVariablePE       = "term variable"
\ No newline at end of file
diff --git a/compiler/GHC/Tc/Types.hs b/compiler/GHC/Tc/Types.hs
index a6bab74fc0..f30e891753 100644
--- a/compiler/GHC/Tc/Types.hs
+++ b/compiler/GHC/Tc/Types.hs
@@ -177,6 +177,12 @@ import qualified Language.Haskell.TH as TH
 import GHC.Driver.Env.KnotVars
 import GHC.Linker.Types
 
+import GHC.Tc.Types.TcTyThing
+import GHC.Tc.Types.TcIdSigInfo
+import GHC.Tc.Types.TH
+import GHC.Tc.Types.TcRef
+import GHC.Tc.Types.LclEnv ()
+
 -- | A 'NameShape' is a substitution on 'Name's that can be used
 -- to refine the identities of a hole while we are renaming interfaces
 -- (see "GHC.Iface.Rename").  Specifically, a 'NameShape' for
@@ -899,10 +905,6 @@ pass it inwards.
 
 -}
 
--- | Type alias for 'IORef'; the convention is we'll use this for mutable
--- bits of data in 'TcGblEnv' which are updated during typechecking and
--- returned at the end.
-type TcRef a     = IORef a
 -- ToDo: when should I refer to it as a 'TcId' instead of an 'Id'?
 type TcId        = Id
 type TcIdSet     = IdSet
@@ -969,103 +971,6 @@ removeBindingShadowing bindings = reverse $ fst $ foldl
 getPlatform :: TcRnIf a b Platform
 getPlatform = targetPlatform <$> getDynFlags
 
----------------------------
--- Template Haskell stages and levels
----------------------------
-
-data SpliceType = Typed | Untyped
-
-data ThStage    -- See Note [Template Haskell state diagram]
-                -- and Note [Template Haskell levels] in GHC.Tc.Gen.Splice
-    -- Start at:   Comp
-    -- At bracket: wrap current stage in Brack
-    -- At splice:  currently Brack: return to previous stage
-    --             currently Comp/Splice: compile and run
-  = Splice SpliceType -- Inside a top-level splice
-                      -- This code will be run *at compile time*;
-                      --   the result replaces the splice
-                      -- Binding level = 0
-
-  | RunSplice (TcRef [ForeignRef (TH.Q ())])
-      -- Set when running a splice, i.e. NOT when renaming or typechecking the
-      -- Haskell code for the splice. See Note [RunSplice ThLevel].
-      --
-      -- Contains a list of mod finalizers collected while executing the splice.
-      --
-      -- 'addModFinalizer' inserts finalizers here, and from here they are taken
-      -- to construct an @HsSpliced@ annotation for untyped splices. See Note
-      -- [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice.
-      --
-      -- For typed splices, the typechecker takes finalizers from here and
-      -- inserts them in the list of finalizers in the global environment.
-      --
-      -- See Note [Collecting modFinalizers in typed splices] in "GHC.Tc.Gen.Splice".
-
-  | Comp        -- Ordinary Haskell code
-                -- Binding level = 1
-
-  | Brack                       -- Inside brackets
-      ThStage                   --   Enclosing stage
-      PendingStuff
-
-data PendingStuff
-  = RnPendingUntyped              -- Renaming the inside of an *untyped* bracket
-      (TcRef [PendingRnSplice])   -- Pending splices in here
-
-  | RnPendingTyped                -- Renaming the inside of a *typed* bracket
-
-  | TcPending                     -- Typechecking the inside of a typed bracket
-      (TcRef [PendingTcSplice])   --   Accumulate pending splices here
-      (TcRef WantedConstraints)   --     and type constraints here
-      QuoteWrapper                -- A type variable and evidence variable
-                                  -- for the overall monad of
-                                  -- the bracket. Splices are checked
-                                  -- against this monad. The evidence
-                                  -- variable is used for desugaring
-                                  -- `lift`.
-
-
-topStage, topAnnStage, topSpliceStage :: ThStage
-topStage       = Comp
-topAnnStage    = Splice Untyped
-topSpliceStage = Splice Untyped
-
-instance Outputable ThStage where
-   ppr (Splice _)    = text "Splice"
-   ppr (RunSplice _) = text "RunSplice"
-   ppr Comp          = text "Comp"
-   ppr (Brack s _)   = text "Brack" <> parens (ppr s)
-
-type ThLevel = Int
-    -- NB: see Note [Template Haskell levels] in GHC.Tc.Gen.Splice
-    -- Incremented when going inside a bracket,
-    -- decremented when going inside a splice
-    -- NB: ThLevel is one greater than the 'n' in Fig 2 of the
-    --     original "Template meta-programming for Haskell" paper
-
-impLevel, outerLevel :: ThLevel
-impLevel = 0    -- Imported things; they can be used inside a top level splice
-outerLevel = 1  -- Things defined outside brackets
-
-thLevel :: ThStage -> ThLevel
-thLevel (Splice _)    = 0
-thLevel Comp          = 1
-thLevel (Brack s _)   = thLevel s + 1
-thLevel (RunSplice _) = panic "thLevel: called when running a splice"
-                        -- See Note [RunSplice ThLevel].
-
-{- Note [RunSplice ThLevel]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The 'RunSplice' stage is set when executing a splice, and only when running a
-splice. In particular it is not set when the splice is renamed or typechecked.
-
-'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert
-the finalizer (see Note [Delaying modFinalizers in untyped splices]), and
-'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to
-set 'RunSplice' when renaming or typechecking the splice, where 'Splice',
-'Brack' or 'Comp' are used instead.
-
--}
 
 ---------------------------
 -- Arrow-notation context
@@ -1107,234 +1012,6 @@ from further out in the ArrowCtxt that we push inwards.
 data ArrowCtxt   -- Note [Escaping the arrow scope]
   = NoArrowCtxt
   | ArrowCtxt LocalRdrEnv (TcRef WantedConstraints)
-
-
----------------------------
--- TcTyThing
----------------------------
-
--- | A typecheckable thing available in a local context.  Could be
--- 'AGlobal' 'TyThing', but also lexically scoped variables, etc.
--- See "GHC.Tc.Utils.Env" for how to retrieve a 'TyThing' given a 'Name'.
-data TcTyThing
-  = AGlobal TyThing             -- Used only in the return type of a lookup
-
-  | ATcId           -- Ids defined in this module; may not be fully zonked
-      { tct_id   :: TcId
-      , tct_info :: IdBindingInfo   -- See Note [Meaning of IdBindingInfo]
-      }
-
-  | ATyVar  Name TcTyVar   -- See Note [Type variables in the type environment]
-
-  | ATcTyCon TyCon   -- Used temporarily, during kind checking, for the
-                     -- tycons and classes in this recursive group
-                     -- The TyCon is always a TcTyCon.  Its kind
-                     -- can be a mono-kind or a poly-kind; in TcTyClsDcls see
-                     -- Note [Type checking recursive type and class declarations]
-
-  | APromotionErr PromotionErr
-
--- | Matches on either a global 'TyCon' or a 'TcTyCon'.
-tcTyThingTyCon_maybe :: TcTyThing -> Maybe TyCon
-tcTyThingTyCon_maybe (AGlobal (ATyCon tc)) = Just tc
-tcTyThingTyCon_maybe (ATcTyCon tc_tc)      = Just tc_tc
-tcTyThingTyCon_maybe _                     = Nothing
-
-instance Outputable TcTyThing where     -- Debugging only
-   ppr (AGlobal g)      = ppr g
-   ppr elt@(ATcId {})   = text "Identifier" <>
-                          brackets (ppr (tct_id elt) <> dcolon
-                                 <> ppr (varType (tct_id elt)) <> comma
-                                 <+> ppr (tct_info elt))
-   ppr (ATyVar n tv)    = text "Type variable" <+> quotes (ppr n) <+> equals <+> ppr tv
-                            <+> dcolon <+> ppr (varType tv)
-   ppr (ATcTyCon tc)    = text "ATcTyCon" <+> ppr tc <+> dcolon <+> ppr (tyConKind tc)
-   ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
-
--- | IdBindingInfo describes how an Id is bound.
---
--- It is used for the following purposes:
--- a) for static forms in 'GHC.Tc.Gen.Expr.checkClosedInStaticForm' and
--- b) to figure out when a nested binding can be generalised,
---    in 'GHC.Tc.Gen.Bind.decideGeneralisationPlan'.
---
-data IdBindingInfo -- See Note [Meaning of IdBindingInfo]
-    = NotLetBound
-    | ClosedLet
-    | NonClosedLet
-         RhsNames        -- Used for (static e) checks only
-         ClosedTypeId    -- Used for generalisation checks
-                         -- and for (static e) checks
-
--- | IsGroupClosed describes a group of mutually-recursive bindings
-data IsGroupClosed
-  = IsGroupClosed
-      (NameEnv RhsNames)  -- Free var info for the RHS of each binding in the group
-                          -- Used only for (static e) checks
-
-      ClosedTypeId        -- True <=> all the free vars of the group are
-                          --          imported or ClosedLet or
-                          --          NonClosedLet with ClosedTypeId=True.
-                          --          In particular, no tyvars, no NotLetBound
-
-type RhsNames = NameSet   -- Names of variables, mentioned on the RHS of
-                          -- a definition, that are not Global or ClosedLet
-
-type ClosedTypeId = Bool
-  -- See Note [Meaning of IdBindingInfo]
-
-{- Note [Meaning of IdBindingInfo]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-NotLetBound means that
-  the Id is not let-bound (e.g. it is bound in a
-  lambda-abstraction or in a case pattern)
-
-ClosedLet means that
-   - The Id is let-bound,
-   - Any free term variables are also Global or ClosedLet
-   - Its type has no free variables (NB: a top-level binding subject
-     to the MR might have free vars in its type)
-   These ClosedLets can definitely be floated to top level; and we
-   may need to do so for static forms.
-
-   Property:   ClosedLet
-             is equivalent to
-               NonClosedLet emptyNameSet True
-
-(NonClosedLet (fvs::RhsNames) (cl::ClosedTypeId)) means that
-   - The Id is let-bound
-
-   - The fvs::RhsNames contains the free names of the RHS,
-     excluding Global and ClosedLet ones.
-
-   - For the ClosedTypeId field see Note [Bindings with closed types: ClosedTypeId]
-
-For (static e) to be valid, we need for every 'x' free in 'e',
-that x's binding is floatable to the top level.  Specifically:
-   * x's RhsNames must be empty
-   * x's type has no free variables
-See Note [Grand plan for static forms] in "GHC.Iface.Tidy.StaticPtrTable".
-This test is made in GHC.Tc.Gen.Expr.checkClosedInStaticForm.
-Actually knowing x's RhsNames (rather than just its emptiness
-or otherwise) is just so we can produce better error messages
-
-Note [Bindings with closed types: ClosedTypeId]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-
-  f x = let g ys = map not ys
-        in ...
-
-Can we generalise 'g' under the OutsideIn algorithm?  Yes,
-because all g's free variables are top-level; that is they themselves
-have no free type variables, and it is the type variables in the
-environment that makes things tricky for OutsideIn generalisation.
-
-Here's the invariant:
-   If an Id has ClosedTypeId=True (in its IdBindingInfo), then
-   the Id's type is /definitely/ closed (has no free type variables).
-   Specifically,
-       a) The Id's actual type is closed (has no free tyvars)
-       b) Either the Id has a (closed) user-supplied type signature
-          or all its free variables are Global/ClosedLet
-             or NonClosedLet with ClosedTypeId=True.
-          In particular, none are NotLetBound.
-
-Why is (b) needed?   Consider
-    \x. (x :: Int, let y = x+1 in ...)
-Initially x::alpha.  If we happen to typecheck the 'let' before the
-(x::Int), y's type will have a free tyvar; but if the other way round
-it won't.  So we treat any let-bound variable with a free
-non-let-bound variable as not ClosedTypeId, regardless of what the
-free vars of its type actually are.
-
-But if it has a signature, all is well:
-   \x. ...(let { y::Int; y = x+1 } in
-           let { v = y+2 } in ...)...
-Here the signature on 'v' makes 'y' a ClosedTypeId, so we can
-generalise 'v'.
-
-Note that:
-
-  * A top-level binding may not have ClosedTypeId=True, if it suffers
-    from the MR
-
-  * A nested binding may be closed (eg 'g' in the example we started
-    with). Indeed, that's the point; whether a function is defined at
-    top level or nested is orthogonal to the question of whether or
-    not it is closed.
-
-  * A binding may be non-closed because it mentions a lexically scoped
-    *type variable*  Eg
-        f :: forall a. blah
-        f x = let g y = ...(y::a)...
-
-Under OutsideIn we are free to generalise an Id all of whose free
-variables have ClosedTypeId=True (or imported).  This is an extension
-compared to the JFP paper on OutsideIn, which used "top-level" as a
-proxy for "closed".  (It's not a good proxy anyway -- the MR can make
-a top-level binding with a free type variable.)
-
-Note [Type variables in the type environment]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The type environment has a binding for each lexically-scoped
-type variable that is in scope.  For example
-
-  f :: forall a. a -> a
-  f x = (x :: a)
-
-  g1 :: [a] -> a
-  g1 (ys :: [b]) = head ys :: b
-
-  g2 :: [Int] -> Int
-  g2 (ys :: [c]) = head ys :: c
-
-* The forall'd variable 'a' in the signature scopes over f's RHS.
-
-* The pattern-bound type variable 'b' in 'g1' scopes over g1's
-  RHS; note that it is bound to a skolem 'a' which is not itself
-  lexically in scope.
-
-* The pattern-bound type variable 'c' in 'g2' is bound to
-  Int; that is, pattern-bound type variables can stand for
-  arbitrary types. (see
-    GHC proposal #128 "Allow ScopedTypeVariables to refer to types"
-    https://github.com/ghc-proposals/ghc-proposals/pull/128,
-  and the paper
-    "Type variables in patterns", Haskell Symposium 2018.
-
-
-This is implemented by the constructor
-   ATyVar Name TcTyVar
-in the type environment.
-
-* The Name is the name of the original, lexically scoped type
-  variable
-
-* The TcTyVar is sometimes a skolem (like in 'f'), and sometimes
-  a unification variable (like in 'g1', 'g2').  We never zonk the
-  type environment so in the latter case it always stays as a
-  unification variable, although that variable may be later
-  unified with a type (such as Int in 'g2').
--}
-
-instance Outputable IdBindingInfo where
-  ppr NotLetBound = text "NotLetBound"
-  ppr ClosedLet = text "TopLevelLet"
-  ppr (NonClosedLet fvs closed_type) =
-    text "TopLevelLet" <+> ppr fvs <+> ppr closed_type
-
---------------
-pprTcTyThingCategory :: TcTyThing -> SDoc
-pprTcTyThingCategory = text . capitalise . tcTyThingCategory
-
-tcTyThingCategory :: TcTyThing -> String
-tcTyThingCategory (AGlobal thing)    = tyThingCategory thing
-tcTyThingCategory (ATyVar {})        = "type variable"
-tcTyThingCategory (ATcId {})         = "local identifier"
-tcTyThingCategory (ATcTyCon {})      = "local tycon"
-tcTyThingCategory (APromotionErr pe) = peCategory pe
-
 {-
 ************************************************************************
 *                                                                      *
@@ -1429,191 +1106,6 @@ instance Outputable WhereFrom where
   ppr ImportByPlugin                       = text "{- PLUGIN -}"
 
 
-{- *********************************************************************
-*                                                                      *
-                Type signatures
-*                                                                      *
-********************************************************************* -}
-
--- These data types need to be here only because
--- GHC.Tc.Solver uses them, and GHC.Tc.Solver is fairly
--- low down in the module hierarchy
-
-type TcSigFun  = Name -> Maybe TcSigInfo
-
-data TcSigInfo = TcIdSig     TcIdSigInfo
-               | TcPatSynSig TcPatSynInfo
-
-data TcIdSigInfo   -- See Note [Complete and partial type signatures]
-  = CompleteSig    -- A complete signature with no wildcards,
-                   -- so the complete polymorphic type is known.
-      { sig_bndr :: TcId          -- The polymorphic Id with that type
-
-      , sig_ctxt :: UserTypeCtxt  -- In the case of type-class default methods,
-                                  -- the Name in the FunSigCtxt is not the same
-                                  -- as the TcId; the former is 'op', while the
-                                  -- latter is '$dmop' or some such
-
-      , sig_loc  :: SrcSpan       -- Location of the type signature
-      }
-
-  | PartialSig     -- A partial type signature (i.e. includes one or more
-                   -- wildcards). In this case it doesn't make sense to give
-                   -- the polymorphic Id, because we are going to /infer/ its
-                   -- type, so we can't make the polymorphic Id ab-initio
-      { psig_name  :: Name   -- Name of the function; used when report wildcards
-      , psig_hs_ty :: LHsSigWcType GhcRn  -- The original partial signature in
-                                          -- HsSyn form
-      , sig_ctxt   :: UserTypeCtxt
-      , sig_loc    :: SrcSpan            -- Location of the type signature
-      }
-
-
-{- Note [Complete and partial type signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A type signature is partial when it contains one or more wildcards
-(= type holes).  The wildcard can either be:
-* A (type) wildcard occurring in sig_theta or sig_tau. These are
-  stored in sig_wcs.
-      f :: Bool -> _
-      g :: Eq _a => _a -> _a -> Bool
-* Or an extra-constraints wildcard, stored in sig_cts:
-      h :: (Num a, _) => a -> a
-
-A type signature is a complete type signature when there are no
-wildcards in the type signature, i.e. iff sig_wcs is empty and
-sig_extra_cts is Nothing.
--}
-
-data TcIdSigInst
-  = TISI { sig_inst_sig :: TcIdSigInfo
-
-         , sig_inst_skols :: [(Name, InvisTVBinder)]
-               -- Instantiated type and kind variables, TyVarTvs
-               -- The Name is the Name that the renamer chose;
-               --   but the TcTyVar may come from instantiating
-               --   the type and hence have a different unique.
-               -- No need to keep track of whether they are truly lexically
-               --   scoped because the renamer has named them uniquely
-               -- See Note [Binding scoped type variables] in GHC.Tc.Gen.Sig
-               --
-               -- NB: The order of sig_inst_skols is irrelevant
-               --     for a CompleteSig, but for a PartialSig see
-               --     Note [Quantified variables in partial type signatures]
-
-         , sig_inst_theta  :: TcThetaType
-               -- Instantiated theta.  In the case of a
-               -- PartialSig, sig_theta does not include
-               -- the extra-constraints wildcard
-
-         , sig_inst_tau :: TcSigmaType   -- Instantiated tau
-               -- See Note [sig_inst_tau may be polymorphic]
-
-         -- Relevant for partial signature only
-         , sig_inst_wcs   :: [(Name, TcTyVar)]
-               -- Like sig_inst_skols, but for /named/ wildcards (_a etc).
-               -- The named wildcards scope over the binding, and hence
-               -- their Names may appear in type signatures in the binding
-
-         , sig_inst_wcx   :: Maybe TcType
-               -- Extra-constraints wildcard to fill in, if any
-               -- If this exists, it is surely of the form (meta_tv |> co)
-               -- (where the co might be reflexive). This is filled in
-               -- only from the return value of GHC.Tc.Gen.HsType.tcAnonWildCardOcc
-         }
-
-{- Note [sig_inst_tau may be polymorphic]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Note that "sig_inst_tau" might actually be a polymorphic type,
-if the original function had a signature like
-   forall a. Eq a => forall b. Ord b => ....
-But that's ok: tcMatchesFun (called by tcRhs) can deal with that
-It happens, too!  See Note [Polymorphic methods] in GHC.Tc.TyCl.Class.
-
-Note [Quantified variables in partial type signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-   f :: forall a b. _ -> a -> _ -> b
-   f (x,y) p q = q
-
-Then we expect f's final type to be
-  f :: forall {x,y}. forall a b. (x,y) -> a -> b -> b
-
-Note that x,y are Inferred, and can't be use for visible type
-application (VTA).  But a,b are Specified, and remain Specified
-in the final type, so we can use VTA for them.  (Exception: if
-it turns out that a's kind mentions b we need to reorder them
-with scopedSort.)
-
-The sig_inst_skols of the TISI from a partial signature records
-that original order, and is used to get the variables of f's
-final type in the correct order.
-
-
-Note [Wildcards in partial signatures]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The wildcards in psig_wcs may stand for a type mentioning
-the universally-quantified tyvars of psig_ty
-
-E.g.  f :: forall a. _ -> a
-      f x = x
-We get sig_inst_skols = [a]
-       sig_inst_tau   = _22 -> a
-       sig_inst_wcs   = [_22]
-and _22 in the end is unified with the type 'a'
-
-Moreover the kind of a wildcard in sig_inst_wcs may mention
-the universally-quantified tyvars sig_inst_skols
-e.g.   f :: t a -> t _
-Here we get
-   sig_inst_skols = [k:*, (t::k ->*), (a::k)]
-   sig_inst_tau   = t a -> t _22
-   sig_inst_wcs   = [ _22::k ]
--}
-
-data TcPatSynInfo
-  = TPSI {
-        patsig_name           :: Name,
-        patsig_implicit_bndrs :: [InvisTVBinder], -- Implicitly-bound kind vars (Inferred) and
-                                                  -- implicitly-bound type vars (Specified)
-          -- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.TyCl.PatSyn
-        patsig_univ_bndrs     :: [InvisTVBinder], -- Bound by explicit user forall
-        patsig_req            :: TcThetaType,
-        patsig_ex_bndrs       :: [InvisTVBinder], -- Bound by explicit user forall
-        patsig_prov           :: TcThetaType,
-        patsig_body_ty        :: TcSigmaType
-    }
-
-instance Outputable TcSigInfo where
-  ppr (TcIdSig     idsi) = ppr idsi
-  ppr (TcPatSynSig tpsi) = text "TcPatSynInfo" <+> ppr tpsi
-
-instance Outputable TcIdSigInfo where
-    ppr (CompleteSig { sig_bndr = bndr })
-        = ppr bndr <+> dcolon <+> ppr (idType bndr)
-    ppr (PartialSig { psig_name = name, psig_hs_ty = hs_ty })
-        = text "psig" <+> ppr name <+> dcolon <+> ppr hs_ty
-
-instance Outputable TcIdSigInst where
-    ppr (TISI { sig_inst_sig = sig, sig_inst_skols = skols
-              , sig_inst_theta = theta, sig_inst_tau = tau })
-        = hang (ppr sig) 2 (vcat [ ppr skols, ppr theta <+> darrow <+> ppr tau ])
-
-instance Outputable TcPatSynInfo where
-    ppr (TPSI{ patsig_name = name}) = ppr name
-
-isPartialSig :: TcIdSigInst -> Bool
-isPartialSig (TISI { sig_inst_sig = PartialSig {} }) = True
-isPartialSig _                                       = False
-
--- | No signature or a partial signature
-hasCompleteSig :: TcSigFun -> Name -> Bool
-hasCompleteSig sig_fn name
-  = case sig_fn name of
-      Just (TcIdSig (CompleteSig {})) -> True
-      _                               -> False
-
-
 {-
 Constraint Solver Plugins
 -------------------------
diff --git a/compiler/GHC/Tc/Types.hs-boot b/compiler/GHC/Tc/Types.hs-boot
index 68902e98ae..7a96132e00 100644
--- a/compiler/GHC/Tc/Types.hs-boot
+++ b/compiler/GHC/Tc/Types.hs-boot
@@ -3,18 +3,11 @@ module GHC.Tc.Types where
 import GHC.Prelude
 import GHC.Tc.Utils.TcType
 import GHC.Types.SrcLoc
-import GHC.Utils.Outputable
 
 data TcLclEnv
 
 data SelfBootInfo
 
-data TcIdSigInfo
-instance Outputable TcIdSigInfo
-
-data TcTyThing
-instance Outputable TcTyThing
-
 setLclEnvTcLevel :: TcLclEnv -> TcLevel -> TcLclEnv
 getLclEnvTcLevel :: TcLclEnv -> TcLevel
 
@@ -22,4 +15,3 @@ setLclEnvLoc :: TcLclEnv -> RealSrcSpan -> TcLclEnv
 getLclEnvLoc :: TcLclEnv -> RealSrcSpan
 
 lclEnvInGeneratedCode :: TcLclEnv -> Bool
-pprTcTyThingCategory :: TcTyThing -> SDoc
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index d99f9067df..f47fb1c147 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -68,7 +68,7 @@ module GHC.Tc.Types.Constraint (
         ctLocTypeOrKind_maybe,
         ctLocDepth, bumpCtLocDepth, isGivenLoc,
         setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,
-        pprCtLoc,
+        pprCtLoc, CtLocEnv(..),
 
         -- CtEvidence
         CtEvidence(..), TcEvDest(..),
@@ -143,6 +143,7 @@ import Data.Word  ( Word8 )
 import Data.List  ( intersperse )
 
 
+
 {-
 ************************************************************************
 *                                                                      *
@@ -2417,10 +2418,12 @@ dictionaries don't appear in the original source code.
 -}
 
 data CtLoc = CtLoc { ctl_origin   :: CtOrigin
-                   , ctl_env      :: TcLclEnv
+                   , ctl_env      :: CtLocEnv
                    , ctl_t_or_k   :: Maybe TypeOrKind  -- OK if we're not sure
                    , ctl_depth    :: !SubGoalDepth }
 
+data CtLocEnv = CtLocEnv { ct_ctxt :: [()], ctl_loc :: RealSrcSpan, ctl_bndrs :: TcBinderStack, ctl_tclvl :: TcLevel }
+
   -- The TcLclEnv includes particularly
   --    source location:  tcl_loc   :: RealSrcSpan
   --    context:          tcl_ctxt  :: [ErrCtxt]
diff --git a/compiler/GHC/Tc/Types/LclEnv.hs b/compiler/GHC/Tc/Types/LclEnv.hs
new file mode 100644
index 0000000000..4f803244c7
--- /dev/null
+++ b/compiler/GHC/Tc/Types/LclEnv.hs
@@ -0,0 +1,261 @@
+module GHC.Tc.Types.LclEnv where
+
+import GHC.Prelude ( Bool, IO )
+
+
+
+import GHC.Tc.Utils.TcType ( TcLevel, ExpType )
+import GHC.Tc.Types.Constraint ( WantedConstraints )
+import GHC.Tc.Errors.Types ( TcRnMessage )
+
+import GHC.Core.Type ( TyVar )
+import GHC.Core.UsageEnv ( UsageEnv )
+
+import GHC.Types.Id         ( idName )
+import GHC.Types.Name.Reader ( LocalRdrEnv )
+import GHC.Types.Name ( Name, HasOccName(..) )
+import GHC.Types.Name.Env ( NameEnv )
+import GHC.Types.Var ( Id )
+import GHC.Types.Var.Env ( TidyEnv )
+import GHC.Types.SrcLoc ( RealSrcSpan )
+import GHC.Types.Basic ( TopLevelFlag )
+
+import GHC.Data.IOEnv ( IORef )
+
+
+import GHC.Utils.Error ( Messages, SDoc )
+import GHC.Utils.Outputable
+    ( Outputable(..), IsLine((<+>), (<>)), brackets )
+
+
+
+import GHC.Tc.Types.TcTyThing ( TcTyThing )
+import GHC.Tc.Types.TH ( ThStage, ThLevel )
+
+{-
+************************************************************************
+*                                                                      *
+                The local typechecker environment
+*                                                                      *
+************************************************************************
+
+Note [The Global-Env/Local-Env story]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+During type checking, we keep in the tcg_type_env
+        * All types and classes
+        * All Ids derived from types and classes (constructors, selectors)
+
+At the end of type checking, we zonk the local bindings,
+and as we do so we add to the tcg_type_env
+        * Locally defined top-level Ids
+
+Why?  Because they are now Ids not TcIds.  This final GlobalEnv is
+        a) fed back (via the knot) to typechecking the
+           unfoldings of interface signatures
+        b) used in the ModDetails of this module
+-}
+
+data TcLclEnv           -- Changes as we move inside an expression
+                        -- Discarded after typecheck/rename; not passed on to desugarer
+  = TcLclEnv {
+        tcl_loc        :: RealSrcSpan,     -- Source span
+        tcl_ctxt       :: [ErrCtxt],       -- Error context, innermost on top
+        tcl_in_gen_code :: Bool,           -- See Note [Rebindable syntax and HsExpansion]
+        tcl_tclvl      :: TcLevel,
+
+        tcl_th_ctxt    :: ThStage,         -- Template Haskell context
+        tcl_th_bndrs   :: ThBindEnv,       -- and binder info
+            -- The ThBindEnv records the TH binding level of in-scope Names
+            -- defined in this module (not imported)
+            -- We can't put this info in the TypeEnv because it's needed
+            -- (and extended) in the renamer, for untyped splices
+
+        tcl_arrow_ctxt :: ArrowCtxt,       -- Arrow-notation context
+
+        tcl_rdr :: LocalRdrEnv,         -- Local name envt
+                -- Maintained during renaming, of course, but also during
+                -- type checking, solely so that when renaming a Template-Haskell
+                -- splice we have the right environment for the renamer.
+                --
+                --   Does *not* include global name envt; may shadow it
+                --   Includes both ordinary variables and type variables;
+                --   they are kept distinct because tyvar have a different
+                --   occurrence constructor (Name.TvOcc)
+                -- We still need the unsullied global name env so that
+                --   we can look up record field names
+
+        tcl_env  :: TcTypeEnv,    -- The local type environment:
+                                  -- Ids and TyVars defined in this module
+
+        tcl_usage :: TcRef UsageEnv, -- Required multiplicity of bindings is accumulated here.
+
+
+        tcl_bndrs :: TcBinderStack,   -- Used for reporting relevant bindings,
+                                      -- and for tidying types
+
+        tcl_lie  :: TcRef WantedConstraints,    -- Place to accumulate type constraints
+        tcl_errs :: TcRef (Messages TcRnMessage)     -- Place to accumulate diagnostics
+    }
+
+setLclEnvTcLevel :: TcLclEnv -> TcLevel -> TcLclEnv
+setLclEnvTcLevel env lvl = env { tcl_tclvl = lvl }
+
+getLclEnvTcLevel :: TcLclEnv -> TcLevel
+getLclEnvTcLevel = tcl_tclvl
+
+setLclEnvLoc :: TcLclEnv -> RealSrcSpan -> TcLclEnv
+setLclEnvLoc env loc = env { tcl_loc = loc }
+
+getLclEnvLoc :: TcLclEnv -> RealSrcSpan
+getLclEnvLoc = tcl_loc
+
+lclEnvInGeneratedCode :: TcLclEnv -> Bool
+lclEnvInGeneratedCode = tcl_in_gen_code
+
+type ErrCtxt = (Bool, TidyEnv -> IO (TidyEnv, SDoc))
+        -- Monadic so that we have a chance
+        -- to deal with bound type variables just before error
+        -- message construction
+
+        -- Bool:  True <=> this is a landmark context; do not
+        --                 discard it when trimming for display
+
+{- TODO move these into where CtLoc is defined.
+
+
+-- These are here to avoid module loops: one might expect them
+-- in GHC.Tc.Types.Constraint, but they refer to ErrCtxt which refers to TcM.
+-- Easier to just keep these definitions here, alongside TcM.
+pushErrCtxt :: CtOrigin -> ErrCtxt -> CtLoc -> CtLoc
+pushErrCtxt o err loc@(CtLoc { ctl_env = lcl })
+  = loc { ctl_origin = o, ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
+
+pushErrCtxtSameOrigin :: ErrCtxt -> CtLoc -> CtLoc
+-- Just add information w/o updating the origin!
+pushErrCtxtSameOrigin err loc@(CtLoc { ctl_env = lcl })
+  = loc { ctl_env = lcl { tcl_ctxt = err : tcl_ctxt lcl } }
+  -}
+
+
+type TcTypeEnv = NameEnv TcTyThing
+
+type ThBindEnv = NameEnv (TopLevelFlag, ThLevel)
+   -- Domain = all Ids bound in this module (ie not imported)
+   -- The TopLevelFlag tells if the binding is syntactically top level.
+   -- We need to know this, because the cross-stage persistence story allows
+   -- cross-stage at arbitrary types if the Id is bound at top level.
+   --
+   -- Nota bene: a ThLevel of 'outerLevel' is *not* the same as being
+   -- bound at top level!  See Note [Template Haskell levels] in GHC.Tc.Gen.Splice
+
+---------------------------
+-- Arrow-notation context
+---------------------------
+
+{- Note [Escaping the arrow scope]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In arrow notation, a variable bound by a proc (or enclosed let/kappa)
+is not in scope to the left of an arrow tail (-<) or the head of (|..|).
+For example
+
+        proc x -> (e1 -< e2)
+
+Here, x is not in scope in e1, but it is in scope in e2.  This can get
+a bit complicated:
+
+        let x = 3 in
+        proc y -> (proc z -> e1) -< e2
+
+Here, x and z are in scope in e1, but y is not.
+
+We implement this by
+recording the environment when passing a proc (using newArrowScope),
+and returning to that (using escapeArrowScope) on the left of -< and the
+head of (|..|).
+
+All this can be dealt with by the *renamer*. But the type checker needs
+to be involved too.  Example (arrowfail001)
+  class Foo a where foo :: a -> ()
+  data Bar = forall a. Foo a => Bar a
+  get :: Bar -> ()
+  get = proc x -> case x of Bar a -> foo -< a
+Here the call of 'foo' gives rise to a (Foo a) constraint that should not
+be captured by the pattern match on 'Bar'.  Rather it should join the
+constraints from further out.  So we must capture the constraint bag
+from further out in the ArrowCtxt that we push inwards.
+-}
+
+data ArrowCtxt   -- Note [Escaping the arrow scope]
+  = NoArrowCtxt
+  | ArrowCtxt LocalRdrEnv (IORef WantedConstraints)
+
+
+---------------------------
+-- The TcBinderStack
+---------------------------
+
+type TcBinderStack = [TcBinder]
+   -- This is a stack of locally-bound ids and tyvars,
+   --   innermost on top
+   -- Used only in error reporting (relevantBindings in TcError),
+   --   and in tidying
+   -- We can't use the tcl_env type environment, because it doesn't
+   --   keep track of the nesting order
+
+type TcId = Id
+type TcRef = IORef
+
+data TcBinder
+  = TcIdBndr
+       TcId
+       TopLevelFlag    -- Tells whether the binding is syntactically top-level
+                       -- (The monomorphic Ids for a recursive group count
+                       --  as not-top-level for this purpose.)
+
+  | TcIdBndr_ExpType  -- Variant that allows the type to be specified as
+                      -- an ExpType
+       Name
+       ExpType
+       TopLevelFlag
+
+  | TcTvBndr          -- e.g.   case x of P (y::a) -> blah
+       Name           -- We bind the lexical name "a" to the type of y,
+       TyVar          -- which might be an utterly different (perhaps
+                      -- existential) tyvar
+
+instance Outputable TcBinder where
+   ppr (TcIdBndr id top_lvl)           = ppr id <> brackets (ppr top_lvl)
+   ppr (TcIdBndr_ExpType id _ top_lvl) = ppr id <> brackets (ppr top_lvl)
+   ppr (TcTvBndr name tv)              = ppr name <+> ppr tv
+
+instance HasOccName TcBinder where
+    occName (TcIdBndr id _)             = occName (idName id)
+    occName (TcIdBndr_ExpType name _ _) = occName name
+    occName (TcTvBndr name _)           = occName name
+
+
+{-
+************************************************************************
+*                                                                      *
+            CtLoc
+*                                                                      *
+************************************************************************
+
+The 'CtLoc' gives information about where a constraint came from.
+This is important for decent error message reporting because
+dictionaries don't appear in the original source code.
+
+-}
+
+{-
+data CtLoc = CtLoc { ctl_origin   :: CtOrigin
+                   , ctl_env      :: TcLclEnv
+                   , ctl_t_or_k   :: Maybe TypeOrKind  -- OK if we're not sure
+                   , ctl_depth    :: !SubGoalDepth }
+                   -}
+
+  -- The TcLclEnv includes particularly
+  --    source location:  tcl_loc   :: RealSrcSpan
+  --    context:          tcl_ctxt  :: [ErrCtxt]
+  --    binder stack:     tcl_bndrs :: TcBinderStack
+  --    level:            tcl_tclvl :: TcLevel
\ No newline at end of file
diff --git a/compiler/GHC/Tc/Types/TH.hs b/compiler/GHC/Tc/Types/TH.hs
new file mode 100644
index 0000000000..8e776f49b3
--- /dev/null
+++ b/compiler/GHC/Tc/Types/TH.hs
@@ -0,0 +1,108 @@
+module GHC.Tc.Types.TH where
+import GHCi.RemoteTypes
+import qualified Language.Haskell.TH as TH
+import GHC.Hs.Expr
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Evidence
+import GHC.Utils.Outputable
+import GHC.Prelude
+import GHC.Utils.Panic
+import GHC.Tc.Types.TcRef
+---------------------------
+-- Template Haskell stages and levels
+---------------------------
+
+
+data SpliceType = Typed | Untyped
+
+data ThStage    -- See Note [Template Haskell state diagram]
+                -- and Note [Template Haskell levels] in GHC.Tc.Gen.Splice
+    -- Start at:   Comp
+    -- At bracket: wrap current stage in Brack
+    -- At splice:  currently Brack: return to previous stage
+    --             currently Comp/Splice: compile and run
+  = Splice SpliceType -- Inside a top-level splice
+                      -- This code will be run *at compile time*;
+                      --   the result replaces the splice
+                      -- Binding level = 0
+
+  | RunSplice (TcRef [ForeignRef (TH.Q ())])
+      -- Set when running a splice, i.e. NOT when renaming or typechecking the
+      -- Haskell code for the splice. See Note [RunSplice ThLevel].
+      --
+      -- Contains a list of mod finalizers collected while executing the splice.
+      --
+      -- 'addModFinalizer' inserts finalizers here, and from here they are taken
+      -- to construct an @HsSpliced@ annotation for untyped splices. See Note
+      -- [Delaying modFinalizers in untyped splices] in GHC.Rename.Splice.
+      --
+      -- For typed splices, the typechecker takes finalizers from here and
+      -- inserts them in the list of finalizers in the global environment.
+      --
+      -- See Note [Collecting modFinalizers in typed splices] in "GHC.Tc.Gen.Splice".
+
+  | Comp        -- Ordinary Haskell code
+                -- Binding level = 1
+
+  | Brack                       -- Inside brackets
+      ThStage                   --   Enclosing stage
+      PendingStuff
+
+data PendingStuff
+  = RnPendingUntyped              -- Renaming the inside of an *untyped* bracket
+      (TcRef [PendingRnSplice])   -- Pending splices in here
+
+  | RnPendingTyped                -- Renaming the inside of a *typed* bracket
+
+  | TcPending                     -- Typechecking the inside of a typed bracket
+      (TcRef [PendingTcSplice])   --   Accumulate pending splices here
+      (TcRef WantedConstraints)   --     and type constraints here
+      QuoteWrapper                -- A type variable and evidence variable
+                                  -- for the overall monad of
+                                  -- the bracket. Splices are checked
+                                  -- against this monad. The evidence
+                                  -- variable is used for desugaring
+                                  -- `lift`.
+
+
+topStage, topAnnStage, topSpliceStage :: ThStage
+topStage       = Comp
+topAnnStage    = Splice Untyped
+topSpliceStage = Splice Untyped
+
+instance Outputable ThStage where
+   ppr (Splice _)    = text "Splice"
+   ppr (RunSplice _) = text "RunSplice"
+   ppr Comp          = text "Comp"
+   ppr (Brack s _)   = text "Brack" <> parens (ppr s)
+
+type ThLevel = Int
+    -- NB: see Note [Template Haskell levels] in GHC.Tc.Gen.Splice
+    -- Incremented when going inside a bracket,
+    -- decremented when going inside a splice
+    -- NB: ThLevel is one greater than the 'n' in Fig 2 of the
+    --     original "Template meta-programming for Haskell" paper
+
+impLevel, outerLevel :: ThLevel
+impLevel = 0    -- Imported things; they can be used inside a top level splice
+outerLevel = 1  -- Things defined outside brackets
+
+thLevel :: ThStage -> ThLevel
+thLevel (Splice _)    = 0
+thLevel Comp          = 1
+thLevel (Brack s _)   = thLevel s + 1
+thLevel (RunSplice _) = panic "thLevel: called when running a splice"
+                        -- See Note [RunSplice ThLevel].
+
+{- Note [RunSplice ThLevel]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The 'RunSplice' stage is set when executing a splice, and only when running a
+splice. In particular it is not set when the splice is renamed or typechecked.
+
+'RunSplice' is needed to provide a reference where 'addModFinalizer' can insert
+the finalizer (see Note [Delaying modFinalizers in untyped splices]), and
+'addModFinalizer' runs when doing Q things. Therefore, It doesn't make sense to
+set 'RunSplice' when renaming or typechecking the splice, where 'Splice',
+'Brack' or 'Comp' are used instead.
+
+-}
\ No newline at end of file
diff --git a/compiler/GHC/Tc/Types/TcIdSigInfo.hs b/compiler/GHC/Tc/Types/TcIdSigInfo.hs
new file mode 100644
index 0000000000..4b4bd265e1
--- /dev/null
+++ b/compiler/GHC/Tc/Types/TcIdSigInfo.hs
@@ -0,0 +1,209 @@
+module GHC.Tc.Types.TcIdSigInfo where
+
+import GHC.Prelude
+
+
+import GHC.Hs
+
+import GHC.Tc.Utils.TcType
+import GHC.Tc.Types.Origin
+
+
+import GHC.Types.Id         ( idType )
+import GHC.Types.Name
+import GHC.Types.Var
+import GHC.Types.SrcLoc
+
+
+
+import GHC.Utils.Outputable
+
+
+
+
+
+
+{- *********************************************************************
+*                                                                      *
+                Type signatures
+*                                                                      *
+********************************************************************* -}
+
+-- These data types need to be here only because
+-- GHC.Tc.Solver uses them, and GHC.Tc.Solver is fairly
+-- low down in the module hierarchy
+
+type TcSigFun  = Name -> Maybe TcSigInfo
+
+data TcSigInfo = TcIdSig     TcIdSigInfo
+               | TcPatSynSig TcPatSynInfo
+
+data TcIdSigInfo   -- See Note [Complete and partial type signatures]
+  = CompleteSig    -- A complete signature with no wildcards,
+                   -- so the complete polymorphic type is known.
+      { sig_bndr :: Id          -- The polymorphic Id with that type
+
+      , sig_ctxt :: UserTypeCtxt  -- In the case of type-class default methods,
+                                  -- the Name in the FunSigCtxt is not the same
+                                  -- as the TcId; the former is 'op', while the
+                                  -- latter is '$dmop' or some such
+
+      , sig_loc  :: SrcSpan       -- Location of the type signature
+      }
+
+  | PartialSig     -- A partial type signature (i.e. includes one or more
+                   -- wildcards). In this case it doesn't make sense to give
+                   -- the polymorphic Id, because we are going to /infer/ its
+                   -- type, so we can't make the polymorphic Id ab-initio
+      { psig_name  :: Name   -- Name of the function; used when report wildcards
+      , psig_hs_ty :: LHsSigWcType GhcRn  -- The original partial signature in
+                                          -- HsSyn form
+      , sig_ctxt   :: UserTypeCtxt
+      , sig_loc    :: SrcSpan            -- Location of the type signature
+      }
+
+
+{- Note [Complete and partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A type signature is partial when it contains one or more wildcards
+(= type holes).  The wildcard can either be:
+* A (type) wildcard occurring in sig_theta or sig_tau. These are
+  stored in sig_wcs.
+      f :: Bool -> _
+      g :: Eq _a => _a -> _a -> Bool
+* Or an extra-constraints wildcard, stored in sig_cts:
+      h :: (Num a, _) => a -> a
+
+A type signature is a complete type signature when there are no
+wildcards in the type signature, i.e. iff sig_wcs is empty and
+sig_extra_cts is Nothing.
+-}
+
+data TcIdSigInst
+  = TISI { sig_inst_sig :: TcIdSigInfo
+
+         , sig_inst_skols :: [(Name, InvisTVBinder)]
+               -- Instantiated type and kind variables, TyVarTvs
+               -- The Name is the Name that the renamer chose;
+               --   but the TcTyVar may come from instantiating
+               --   the type and hence have a different unique.
+               -- No need to keep track of whether they are truly lexically
+               --   scoped because the renamer has named them uniquely
+               -- See Note [Binding scoped type variables] in GHC.Tc.Gen.Sig
+               --
+               -- NB: The order of sig_inst_skols is irrelevant
+               --     for a CompleteSig, but for a PartialSig see
+               --     Note [Quantified variables in partial type signatures]
+
+         , sig_inst_theta  :: TcThetaType
+               -- Instantiated theta.  In the case of a
+               -- PartialSig, sig_theta does not include
+               -- the extra-constraints wildcard
+
+         , sig_inst_tau :: TcSigmaType   -- Instantiated tau
+               -- See Note [sig_inst_tau may be polymorphic]
+
+         -- Relevant for partial signature only
+         , sig_inst_wcs   :: [(Name, TcTyVar)]
+               -- Like sig_inst_skols, but for /named/ wildcards (_a etc).
+               -- The named wildcards scope over the binding, and hence
+               -- their Names may appear in type signatures in the binding
+
+         , sig_inst_wcx   :: Maybe TcType
+               -- Extra-constraints wildcard to fill in, if any
+               -- If this exists, it is surely of the form (meta_tv |> co)
+               -- (where the co might be reflexive). This is filled in
+               -- only from the return value of GHC.Tc.Gen.HsType.tcAnonWildCardOcc
+         }
+
+{- Note [sig_inst_tau may be polymorphic]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note that "sig_inst_tau" might actually be a polymorphic type,
+if the original function had a signature like
+   forall a. Eq a => forall b. Ord b => ....
+But that's ok: tcMatchesFun (called by tcRhs) can deal with that
+It happens, too!  See Note [Polymorphic methods] in GHC.Tc.TyCl.Class.
+
+Note [Quantified variables in partial type signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f :: forall a b. _ -> a -> _ -> b
+   f (x,y) p q = q
+
+Then we expect f's final type to be
+  f :: forall {x,y}. forall a b. (x,y) -> a -> b -> b
+
+Note that x,y are Inferred, and can't be use for visible type
+application (VTA).  But a,b are Specified, and remain Specified
+in the final type, so we can use VTA for them.  (Exception: if
+it turns out that a's kind mentions b we need to reorder them
+with scopedSort.)
+
+The sig_inst_skols of the TISI from a partial signature records
+that original order, and is used to get the variables of f's
+final type in the correct order.
+
+
+Note [Wildcards in partial signatures]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The wildcards in psig_wcs may stand for a type mentioning
+the universally-quantified tyvars of psig_ty
+
+E.g.  f :: forall a. _ -> a
+      f x = x
+We get sig_inst_skols = [a]
+       sig_inst_tau   = _22 -> a
+       sig_inst_wcs   = [_22]
+and _22 in the end is unified with the type 'a'
+
+Moreover the kind of a wildcard in sig_inst_wcs may mention
+the universally-quantified tyvars sig_inst_skols
+e.g.   f :: t a -> t _
+Here we get
+   sig_inst_skols = [k:*, (t::k ->*), (a::k)]
+   sig_inst_tau   = t a -> t _22
+   sig_inst_wcs   = [ _22::k ]
+-}
+
+data TcPatSynInfo
+  = TPSI {
+        patsig_name           :: Name,
+        patsig_implicit_bndrs :: [InvisTVBinder], -- Implicitly-bound kind vars (Inferred) and
+                                                  -- implicitly-bound type vars (Specified)
+          -- See Note [The pattern-synonym signature splitting rule] in GHC.Tc.TyCl.PatSyn
+        patsig_univ_bndrs     :: [InvisTVBinder], -- Bound by explicit user forall
+        patsig_req            :: TcThetaType,
+        patsig_ex_bndrs       :: [InvisTVBinder], -- Bound by explicit user forall
+        patsig_prov           :: TcThetaType,
+        patsig_body_ty        :: TcSigmaType
+    }
+
+instance Outputable TcSigInfo where
+  ppr (TcIdSig     idsi) = ppr idsi
+  ppr (TcPatSynSig tpsi) = text "TcPatSynInfo" <+> ppr tpsi
+
+instance Outputable TcIdSigInfo where
+    ppr (CompleteSig { sig_bndr = bndr })
+        = ppr bndr <+> dcolon <+> ppr (idType bndr)
+    ppr (PartialSig { psig_name = name, psig_hs_ty = hs_ty })
+        = text "psig" <+> ppr name <+> dcolon <+> ppr hs_ty
+
+instance Outputable TcIdSigInst where
+    ppr (TISI { sig_inst_sig = sig, sig_inst_skols = skols
+              , sig_inst_theta = theta, sig_inst_tau = tau })
+        = hang (ppr sig) 2 (vcat [ ppr skols, ppr theta <+> darrow <+> ppr tau ])
+
+instance Outputable TcPatSynInfo where
+    ppr (TPSI{ patsig_name = name}) = ppr name
+
+isPartialSig :: TcIdSigInst -> Bool
+isPartialSig (TISI { sig_inst_sig = PartialSig {} }) = True
+isPartialSig _                                       = False
+
+-- | No signature or a partial signature
+hasCompleteSig :: TcSigFun -> Name -> Bool
+hasCompleteSig sig_fn name
+  = case sig_fn name of
+      Just (TcIdSig (CompleteSig {})) -> True
+      _                               -> False
+
diff --git a/compiler/GHC/Tc/Types/TcRef.hs b/compiler/GHC/Tc/Types/TcRef.hs
new file mode 100644
index 0000000000..c6b28e6521
--- /dev/null
+++ b/compiler/GHC/Tc/Types/TcRef.hs
@@ -0,0 +1,8 @@
+module GHC.Tc.Types.TcRef where
+import Data.IORef
+
+
+-- | Type alias for 'IORef'; the convention is we'll use this for mutable
+-- bits of data in 'TcGblEnv' which are updated during typechecking and
+-- returned at the end.
+type TcRef a     = IORef a
\ No newline at end of file
diff --git a/compiler/GHC/Tc/Types/TcTyThing.hs b/compiler/GHC/Tc/Types/TcTyThing.hs
new file mode 100644
index 0000000000..5b2ad427b1
--- /dev/null
+++ b/compiler/GHC/Tc/Types/TcTyThing.hs
@@ -0,0 +1,252 @@
+module GHC.Tc.Types.TcTyThing where
+
+import GHC.Prelude
+
+
+
+import GHC.Tc.Utils.TcType
+--import GHC.Tc.Errors.Types ()
+
+import GHC.Core.Type
+import GHC.Core.TyCon  ( TyCon, tyConKind )
+
+import GHC.Types.Name
+import GHC.Types.Name.Env
+import GHC.Types.Name.Set
+import GHC.Types.Var
+import GHC.Types.TyThing
+
+
+
+import GHC.Utils.Error
+import GHC.Utils.Outputable
+import GHC.Utils.Misc
+import GHC.Tc.Errors.Types.PromotionErr (PromotionErr, peCategory)
+
+
+
+---------------------------
+-- TcTyThing
+---------------------------
+
+-- | A typecheckable thing available in a local context.  Could be
+-- 'AGlobal' 'TyThing', but also lexically scoped variables, etc.
+-- See "GHC.Tc.Utils.Env" for how to retrieve a 'TyThing' given a 'Name'.
+data TcTyThing
+  = AGlobal TyThing             -- Used only in the return type of a lookup
+
+  | ATcId           -- Ids defined in this module; may not be fully zonked
+      { tct_id   :: Id
+      , tct_info :: IdBindingInfo   -- See Note [Meaning of IdBindingInfo]
+      }
+
+  | ATyVar  Name TcTyVar   -- See Note [Type variables in the type environment]
+
+  | ATcTyCon TyCon   -- Used temporarily, during kind checking, for the
+                     -- tycons and classes in this recursive group
+                     -- The TyCon is always a TcTyCon.  Its kind
+                     -- can be a mono-kind or a poly-kind; in TcTyClsDcls see
+                     -- Note [Type checking recursive type and class declarations]
+
+  | APromotionErr PromotionErr
+
+-- | Matches on either a global 'TyCon' or a 'TcTyCon'.
+tcTyThingTyCon_maybe :: TcTyThing -> Maybe TyCon
+tcTyThingTyCon_maybe (AGlobal (ATyCon tc)) = Just tc
+tcTyThingTyCon_maybe (ATcTyCon tc_tc)      = Just tc_tc
+tcTyThingTyCon_maybe _                     = Nothing
+
+instance Outputable TcTyThing where     -- Debugging only
+   ppr (AGlobal g)      = ppr g
+   ppr elt@(ATcId {})   = text "Identifier" <>
+                          brackets (ppr (tct_id elt) <> dcolon
+                                 <> ppr (varType (tct_id elt)) <> comma
+                                 <+> ppr (tct_info elt))
+   ppr (ATyVar n tv)    = text "Type variable" <+> quotes (ppr n) <+> equals <+> ppr tv
+                            <+> dcolon <+> ppr (varType tv)
+   ppr (ATcTyCon tc)    = text "ATcTyCon" <+> ppr tc <+> dcolon <+> ppr (tyConKind tc)
+   ppr (APromotionErr err) = text "APromotionErr" <+> ppr err
+
+-- | IdBindingInfo describes how an Id is bound.
+--
+-- It is used for the following purposes:
+-- a) for static forms in 'GHC.Tc.Gen.Expr.checkClosedInStaticForm' and
+-- b) to figure out when a nested binding can be generalised,
+--    in 'GHC.Tc.Gen.Bind.decideGeneralisationPlan'.
+--
+data IdBindingInfo -- See Note [Meaning of IdBindingInfo]
+    = NotLetBound
+    | ClosedLet
+    | NonClosedLet
+         RhsNames        -- Used for (static e) checks only
+         ClosedTypeId    -- Used for generalisation checks
+                         -- and for (static e) checks
+
+-- | IsGroupClosed describes a group of mutually-recursive bindings
+data IsGroupClosed
+  = IsGroupClosed
+      (NameEnv RhsNames)  -- Free var info for the RHS of each binding in the group
+                          -- Used only for (static e) checks
+
+      ClosedTypeId        -- True <=> all the free vars of the group are
+                          --          imported or ClosedLet or
+                          --          NonClosedLet with ClosedTypeId=True.
+                          --          In particular, no tyvars, no NotLetBound
+
+type RhsNames = NameSet   -- Names of variables, mentioned on the RHS of
+                          -- a definition, that are not Global or ClosedLet
+
+type ClosedTypeId = Bool
+  -- See Note [Meaning of IdBindingInfo]
+
+{- Note [Meaning of IdBindingInfo]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+NotLetBound means that
+  the Id is not let-bound (e.g. it is bound in a
+  lambda-abstraction or in a case pattern)
+
+ClosedLet means that
+   - The Id is let-bound,
+   - Any free term variables are also Global or ClosedLet
+   - Its type has no free variables (NB: a top-level binding subject
+     to the MR might have free vars in its type)
+   These ClosedLets can definitely be floated to top level; and we
+   may need to do so for static forms.
+
+   Property:   ClosedLet
+             is equivalent to
+               NonClosedLet emptyNameSet True
+
+(NonClosedLet (fvs::RhsNames) (cl::ClosedTypeId)) means that
+   - The Id is let-bound
+
+   - The fvs::RhsNames contains the free names of the RHS,
+     excluding Global and ClosedLet ones.
+
+   - For the ClosedTypeId field see Note [Bindings with closed types: ClosedTypeId]
+
+For (static e) to be valid, we need for every 'x' free in 'e',
+that x's binding is floatable to the top level.  Specifically:
+   * x's RhsNames must be empty
+   * x's type has no free variables
+See Note [Grand plan for static forms] in "GHC.Iface.Tidy.StaticPtrTable".
+This test is made in GHC.Tc.Gen.Expr.checkClosedInStaticForm.
+Actually knowing x's RhsNames (rather than just its emptiness
+or otherwise) is just so we can produce better error messages
+
+Note [Bindings with closed types: ClosedTypeId]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+
+  f x = let g ys = map not ys
+        in ...
+
+Can we generalise 'g' under the OutsideIn algorithm?  Yes,
+because all g's free variables are top-level; that is they themselves
+have no free type variables, and it is the type variables in the
+environment that makes things tricky for OutsideIn generalisation.
+
+Here's the invariant:
+   If an Id has ClosedTypeId=True (in its IdBindingInfo), then
+   the Id's type is /definitely/ closed (has no free type variables).
+   Specifically,
+       a) The Id's actual type is closed (has no free tyvars)
+       b) Either the Id has a (closed) user-supplied type signature
+          or all its free variables are Global/ClosedLet
+             or NonClosedLet with ClosedTypeId=True.
+          In particular, none are NotLetBound.
+
+Why is (b) needed?   Consider
+    \x. (x :: Int, let y = x+1 in ...)
+Initially x::alpha.  If we happen to typecheck the 'let' before the
+(x::Int), y's type will have a free tyvar; but if the other way round
+it won't.  So we treat any let-bound variable with a free
+non-let-bound variable as not ClosedTypeId, regardless of what the
+free vars of its type actually are.
+
+But if it has a signature, all is well:
+   \x. ...(let { y::Int; y = x+1 } in
+           let { v = y+2 } in ...)...
+Here the signature on 'v' makes 'y' a ClosedTypeId, so we can
+generalise 'v'.
+
+Note that:
+
+  * A top-level binding may not have ClosedTypeId=True, if it suffers
+    from the MR
+
+  * A nested binding may be closed (eg 'g' in the example we started
+    with). Indeed, that's the point; whether a function is defined at
+    top level or nested is orthogonal to the question of whether or
+    not it is closed.
+
+  * A binding may be non-closed because it mentions a lexically scoped
+    *type variable*  Eg
+        f :: forall a. blah
+        f x = let g y = ...(y::a)...
+
+Under OutsideIn we are free to generalise an Id all of whose free
+variables have ClosedTypeId=True (or imported).  This is an extension
+compared to the JFP paper on OutsideIn, which used "top-level" as a
+proxy for "closed".  (It's not a good proxy anyway -- the MR can make
+a top-level binding with a free type variable.)
+
+Note [Type variables in the type environment]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type environment has a binding for each lexically-scoped
+type variable that is in scope.  For example
+
+  f :: forall a. a -> a
+  f x = (x :: a)
+
+  g1 :: [a] -> a
+  g1 (ys :: [b]) = head ys :: b
+
+  g2 :: [Int] -> Int
+  g2 (ys :: [c]) = head ys :: c
+
+* The forall'd variable 'a' in the signature scopes over f's RHS.
+
+* The pattern-bound type variable 'b' in 'g1' scopes over g1's
+  RHS; note that it is bound to a skolem 'a' which is not itself
+  lexically in scope.
+
+* The pattern-bound type variable 'c' in 'g2' is bound to
+  Int; that is, pattern-bound type variables can stand for
+  arbitrary types. (see
+    GHC proposal #128 "Allow ScopedTypeVariables to refer to types"
+    https://github.com/ghc-proposals/ghc-proposals/pull/128,
+  and the paper
+    "Type variables in patterns", Haskell Symposium 2018.
+
+
+This is implemented by the constructor
+   ATyVar Name TcTyVar
+in the type environment.
+
+* The Name is the name of the original, lexically scoped type
+  variable
+
+* The TcTyVar is sometimes a skolem (like in 'f'), and sometimes
+  a unification variable (like in 'g1', 'g2').  We never zonk the
+  type environment so in the latter case it always stays as a
+  unification variable, although that variable may be later
+  unified with a type (such as Int in 'g2').
+-}
+
+instance Outputable IdBindingInfo where
+  ppr NotLetBound = text "NotLetBound"
+  ppr ClosedLet = text "TopLevelLet"
+  ppr (NonClosedLet fvs closed_type) =
+    text "TopLevelLet" <+> ppr fvs <+> ppr closed_type
+
+--------------
+pprTcTyThingCategory :: TcTyThing -> SDoc
+pprTcTyThingCategory = text . capitalise . tcTyThingCategory
+
+tcTyThingCategory :: TcTyThing -> String
+tcTyThingCategory (AGlobal thing)    = tyThingCategory thing
+tcTyThingCategory (ATyVar {})        = "type variable"
+tcTyThingCategory (ATcId {})         = "local identifier"
+tcTyThingCategory (ATcTyCon {})      = "local tycon"
+tcTyThingCategory (APromotionErr pe) = peCategory pe
diff --git a/compiler/GHC/Tc/Utils/Monad.hs b/compiler/GHC/Tc/Utils/Monad.hs
index 75b74cbb35..0cd69c95bb 100644
--- a/compiler/GHC/Tc/Utils/Monad.hs
+++ b/compiler/GHC/Tc/Utils/Monad.hs
@@ -1275,10 +1275,13 @@ getCtLocM :: CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
 getCtLocM origin t_or_k
   = do { env <- getLclEnv
        ; return (CtLoc { ctl_origin   = origin
-                       , ctl_env      = env
+                       , ctl_env      = mkCtLocEnv env
                        , ctl_t_or_k   = t_or_k
                        , ctl_depth    = initialSubGoalDepth }) }
 
+mkCtLocEnv :: TcLclEnv -> CtLocEnv
+mkCtLocEnv lcl_env = CtLocEnv
+
 setCtLocM :: CtLoc -> TcM a -> TcM a
 -- Set the SrcSpan and error context from the CtLoc
 setCtLocM (CtLoc { ctl_env = lcl }) thing_inside
diff --git a/compiler/GHC/Types/LclEnv.hs b/compiler/GHC/Types/LclEnv.hs
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/compiler/GHC/Types/LclEnv.hs
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index fc2151f547..7735a28b44 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -708,6 +708,7 @@ Library
         GHC.Tc.Errors.Hole.FitTypes
         GHC.Tc.Errors.Ppr
         GHC.Tc.Errors.Types
+        GHC.Tc.Errors.Types.PromotionErr
         GHC.Tc.Gen.Annotation
         GHC.Tc.Gen.App
         GHC.Tc.Gen.Arrow
@@ -740,6 +741,11 @@ Library
         GHC.Tc.Solver.Types
         GHC.Tc.TyCl
         GHC.Tc.TyCl.Build
+        GHC.Tc.Types.LclEnv
+        GHC.Tc.Types.TcIdSigInfo
+        GHC.Tc.Types.TH
+        GHC.Tc.Types.TcRef
+        GHC.Tc.Types.TcTyThing
         GHC.Tc.TyCl.Class
         GHC.Tc.TyCl.Instance
         GHC.Tc.TyCl.PatSyn