Remove the type-checking knot.

Bug #15380 hangs because a knot-tied TyCon ended up in a kind.
Looking at the code in tcInferApps, I'm amazed this hasn't happened
before! I couldn't think of a good way to fix it (with dependent
types, we can't really keep types out of kinds, after all), so
I just went ahead and removed the knot.

This was remarkably easy to do. In tcTyVar, when we find a TcTyCon,
just use it. (Previously, we looked up the knot-tied TyCon and used
that.) Then, during the final zonk, replace TcTyCons with the real,
full-blooded TyCons in the global environment. It's all very easy.

The new bit is explained in the existing
Note [Type checking recursive type and class declarations]
in TcTyClsDecls.

Naturally, I removed various references to the knot and the
zonkTcTypeInKnot (and related) functions. Now, we can print types
during type checking with abandon!

NB: There is a teensy error message regression with this patch,
around the ordering of quantified type variables. This ordering
problem is fixed (I believe) with the patch for #14880. The ordering
affects only internal variables that cannot be instantiated with
any kind of visible type application.

There is also a teensy regression around the printing of types
in TH splices. I think this is really a TH bug and will file
separately.

Test case: dependent/should_fail/T15380

21 files changed, 232 insertions, 236 deletions

diff --git a/compiler/basicTypes/DataCon.hs b/compiler/basicTypes/DataCon.hs
index f174130cec..9b62c27df3 100644
--- a/compiler/basicTypes/DataCon.hs
+++ b/compiler/basicTypes/DataCon.hs
@@ -844,27 +844,27 @@ isMarkedStrict _               = True   -- All others are strict
 
 -- | Build a new data constructor
 mkDataCon :: Name
-          -> Bool           -- ^ Is the constructor declared infix?
-          -> TyConRepName   -- ^  TyConRepName for the promoted TyCon
-          -> [HsSrcBang]    -- ^ Strictness/unpack annotations, from user
-          -> [FieldLabel]   -- ^ Field labels for the constructor,
-                            -- if it is a record, otherwise empty
-          -> [TyVar]        -- ^ Universals.
-          -> [TyVar]        -- ^ Existentials.
-          -> [TyVarBinder]  -- ^ User-written 'TyVarBinder's.
-                            --   These must be Inferred/Specified.
-                            --   See @Note [TyVarBinders in DataCons]@
-          -> [EqSpec]       -- ^ GADT equalities
-          -> ThetaType      -- ^ Theta-type occuring before the arguments proper
-          -> [Type]         -- ^ Original argument types
-          -> Type           -- ^ Original result type
-          -> RuntimeRepInfo -- ^ See comments on 'TyCon.RuntimeRepInfo'
-          -> TyCon          -- ^ Representation type constructor
-          -> ConTag         -- ^ Constructor tag
-          -> ThetaType      -- ^ The "stupid theta", context of the data
-                            -- declaration e.g. @data Eq a => T a ...@
-          -> Id             -- ^ Worker Id
-          -> DataConRep     -- ^ Representation
+          -> Bool               -- ^ Is the constructor declared infix?
+          -> TyConRepName       -- ^  TyConRepName for the promoted TyCon
+          -> [HsSrcBang]        -- ^ Strictness/unpack annotations, from user
+          -> [FieldLabel]       -- ^ Field labels for the constructor,
+                                -- if it is a record, otherwise empty
+          -> [TyVar]            -- ^ Universals.
+          -> [TyVar]            -- ^ Existentials.
+          -> [TyVarBinder]      -- ^ User-written 'TyVarBinder's.
+                                --   These must be Inferred/Specified.
+                                --   See @Note [TyVarBinders in DataCons]@
+          -> [EqSpec]           -- ^ GADT equalities
+          -> KnotTied ThetaType -- ^ Theta-type occuring before the arguments proper
+          -> [KnotTied Type]    -- ^ Original argument types
+          -> KnotTied Type      -- ^ Original result type
+          -> RuntimeRepInfo     -- ^ See comments on 'TyCon.RuntimeRepInfo'
+          -> KnotTied TyCon     -- ^ Representation type constructor
+          -> ConTag             -- ^ Constructor tag
+          -> ThetaType          -- ^ The "stupid theta", context of the data
+                                -- declaration e.g. @data Eq a => T a ...@
+          -> Id                 -- ^ Worker Id
+          -> DataConRep         -- ^ Representation
           -> DataCon
   -- Can get the tag from the TyCon
 
@@ -1429,8 +1429,8 @@ buildAlgTyCon tc_name ktvs roles cType stupid_theta rhs
   where
     binders = mkTyConBindersPreferAnon ktvs liftedTypeKind
 
-buildSynTyCon :: Name -> [TyConBinder] -> Kind   -- ^ /result/ kind
-                  -> [Role] -> Type -> TyCon
+buildSynTyCon :: Name -> [KnotTied TyConBinder] -> Kind   -- ^ /result/ kind
+              -> [Role] -> KnotTied Type -> TyCon
 buildSynTyCon name binders res_kind roles rhs
   = mkSynonymTyCon name binders res_kind roles rhs is_tau is_fam_free
   where
diff --git a/compiler/iface/BuildTyCl.hs b/compiler/iface/BuildTyCl.hs
index 43e9408430..3ddd355a6d 100644
--- a/compiler/iface/BuildTyCl.hs
+++ b/compiler/iface/BuildTyCl.hs
@@ -8,7 +8,7 @@
 module BuildTyCl (
         buildDataCon,
         buildPatSyn,
-        TcMethInfo, buildClass,
+        TcMethInfo, MethInfo, buildClass,
         mkNewTyConRhs,
         newImplicitBinder, newTyConRepName
     ) where
@@ -104,10 +104,11 @@ buildDataCon :: FamInstEnvs
            -> [TyVar]                  -- Existentials
            -> [TyVarBinder]            -- User-written 'TyVarBinder's
            -> [EqSpec]                 -- Equality spec
-           -> ThetaType                -- Does not include the "stupid theta"
+           -> KnotTied ThetaType       -- Does not include the "stupid theta"
                                        -- or the GADT equalities
-           -> [Type] -> Type           -- Argument and result types
-           -> TyCon                    -- Rep tycon
+           -> [KnotTied Type]          -- Arguments
+           -> KnotTied Type            -- Result types
+           -> KnotTied TyCon           -- Rep tycon
            -> NameEnv ConTag           -- Maps the Name of each DataCon to its
                                        -- ConTag
            -> TcRnIf m n DataCon
@@ -213,7 +214,8 @@ buildPatSyn src_name declared_infix matcher@(matcher_id,_) builder
 
 
 ------------------------------------------------------
-type TcMethInfo     -- A temporary intermediate, to communicate
+type TcMethInfo = MethInfo  -- this variant needs zonking
+type MethInfo       -- A temporary intermediate, to communicate
                     -- between tcClassSigs and buildClass.
   = ( Name   -- Name of the class op
     , Type   -- Type of the class op
@@ -237,7 +239,7 @@ buildClass :: Name  -- Name of the class/tycon (they have the same Name)
            -> [FunDep TyVar]               -- Functional dependencies
            -- Super classes, associated types, method info, minimal complete def.
            -- This is Nothing if the class is abstract.
-           -> Maybe (ThetaType, [ClassATItem], [TcMethInfo], ClassMinimalDef)
+           -> Maybe (KnotTied ThetaType, [ClassATItem], [KnotTied MethInfo], ClassMinimalDef)
            -> TcRnIf m n Class
 
 buildClass tycon_name binders roles fds Nothing
diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index b409c0768d..00602ecba5 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -443,7 +443,7 @@ checkFamInstConsistency directlyImpMods
            -- as quickly as possible, so that we aren't typechecking
            -- values with inconsistent axioms in scope.
            --
-           -- See also Note [Tying the knot] and Note [Type-checking inside the knot]
+           -- See also Note [Tying the knot]
            -- for why we are doing this at all.
            ; let check_now = famInstEnvElts env1
            ; mapM_ (checkForConflicts (emptyFamInstEnv, env2))           check_now
diff --git a/compiler/typecheck/TcEnv.hs b/compiler/typecheck/TcEnv.hs
index a703e57c3d..a5a900410f 100644
--- a/compiler/typecheck/TcEnv.hs
+++ b/compiler/typecheck/TcEnv.hs
@@ -18,7 +18,7 @@ module TcEnv(
         tcExtendGlobalEnv, tcExtendTyConEnv,
         tcExtendGlobalEnvImplicit, setGlobalTypeEnv,
         tcExtendGlobalValEnv,
-        tcLookupLocatedGlobal, tcLookupGlobal,
+        tcLookupLocatedGlobal, tcLookupGlobal, tcLookupGlobalOnly,
         tcLookupTyCon, tcLookupClass,
         tcLookupDataCon, tcLookupPatSyn, tcLookupConLike,
         tcLookupLocatedGlobalId, tcLookupLocatedTyCon,
@@ -229,6 +229,15 @@ tcLookupGlobal name
             Failed msg      -> failWithTc msg
         }}}
 
+-- Look up only in this module's global env't. Don't look in imports, etc.
+-- Panic if it's not there.
+tcLookupGlobalOnly :: Name -> TcM TyThing
+tcLookupGlobalOnly name
+  = do { env <- getGblEnv
+       ; return $ case lookupNameEnv (tcg_type_env env) name of
+                    Just thing -> thing
+                    Nothing    -> pprPanic "tcLookupGlobalOnly" (ppr name) }
+
 tcLookupDataCon :: Name -> TcM DataCon
 tcLookupDataCon name = do
     thing <- tcLookupGlobal name
diff --git a/compiler/typecheck/TcHsSyn.hs b/compiler/typecheck/TcHsSyn.hs
index a4a25620e7..77e2a246cb 100644
--- a/compiler/typecheck/TcHsSyn.hs
+++ b/compiler/typecheck/TcHsSyn.hs
@@ -34,8 +34,9 @@ module TcHsSyn (
         zonkTyVarBindersX, zonkTyVarBinderX,
         emptyZonkEnv, mkEmptyZonkEnv,
         zonkTcTypeToType, zonkTcTypeToTypes, zonkTyVarOcc,
-        zonkCoToCo, zonkSigType,
-        zonkEvBinds, zonkTcEvBinds
+        zonkCoToCo,
+        zonkEvBinds, zonkTcEvBinds,
+        zonkTcMethInfoToMethInfo
   ) where
 
 #include "HsVersions.h"
@@ -47,11 +48,13 @@ import Id
 import IdInfo
 import TcRnMonad
 import PrelNames
+import BuildTyCl ( TcMethInfo, MethInfo )
 import TcType
 import TcMType
+import TcEnv   ( tcLookupGlobalOnly )
 import TcEvidence
 import TysPrim
-import TyCon   ( isUnboxedTupleTyCon )
+import TyCon
 import TysWiredIn
 import TyCoRep( CoercionHole(..) )
 import Type
@@ -1675,11 +1678,20 @@ zonkCoHole env hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
 zonk_tycomapper :: TyCoMapper ZonkEnv TcM
 zonk_tycomapper = TyCoMapper
   { tcm_smart = True   -- Establish type invariants
-                       -- See Note [Type-checking inside the knot] in TcHsType
   , tcm_tyvar = zonkTyVarOcc
   , tcm_covar = zonkCoVarOcc
   , tcm_hole  = zonkCoHole
-  , tcm_tybinder = \env tv _vis -> zonkTyBndrX env tv }
+  , tcm_tybinder = \env tv _vis -> zonkTyBndrX env tv
+  , tcm_tycon = zonkTcTyConToTyCon }
+
+-- Zonk a TyCon by changing a TcTyCon to a regular TyCon
+zonkTcTyConToTyCon :: TcTyCon -> TcM TyCon
+zonkTcTyConToTyCon tc
+  | isTcTyCon tc = do { thing <- tcLookupGlobalOnly (getName tc)
+                      ; case thing of
+                          ATyCon real_tc -> return real_tc
+                          _              -> pprPanic "zonkTcTyCon" (ppr tc $$ ppr thing) }
+  | otherwise    = return tc -- it's already zonked
 
 -- Confused by zonking? See Note [What is zonking?] in TcMType.
 zonkTcTypeToType :: ZonkEnv -> TcType -> TcM Type
@@ -1691,18 +1703,19 @@ zonkTcTypeToTypes env tys = mapM (zonkTcTypeToType env) tys
 zonkCoToCo :: ZonkEnv -> Coercion -> TcM Coercion
 zonkCoToCo = mapCoercion zonk_tycomapper
 
-zonkSigType :: TcType -> TcM Type
--- Zonk the type obtained from a user type signature
--- We want to turn any quantified (forall'd) variables into TyVars
--- but we may find some free TcTyVars, and we want to leave them
--- completely alone.  They may even have unification variables inside
--- e.g.  f (x::a) = ...(e :: a -> a)....
--- The type sig for 'e' mentions a free 'a' which will be a
--- unification SigTv variable.
-zonkSigType = zonkTcTypeToType (mkEmptyZonkEnv zonk_unbound_tv)
+zonkTcMethInfoToMethInfo :: TcMethInfo -> TcM MethInfo
+zonkTcMethInfoToMethInfo (name, ty, gdm_spec)
+  = do { ty' <- zonkTcTypeToType emptyZonkEnv ty
+       ; gdm_spec' <- zonk_gdm gdm_spec
+       ; return (name, ty', gdm_spec') }
   where
-    zonk_unbound_tv :: UnboundTyVarZonker
-    zonk_unbound_tv tv = return (mkTyVarTy tv)
+    zonk_gdm :: Maybe (DefMethSpec (SrcSpan, TcType))
+             -> TcM (Maybe (DefMethSpec (SrcSpan, Type)))
+    zonk_gdm Nothing = return Nothing
+    zonk_gdm (Just VanillaDM) = return (Just VanillaDM)
+    zonk_gdm (Just (GenericDM (loc, ty)))
+      = do { ty' <- zonkTcTypeToType emptyZonkEnv ty
+           ; return (Just (GenericDM (loc, ty'))) }
 
 zonkTvSkolemising :: UnboundTyVarZonker
 -- This variant is used for the LHS of rules
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index c1ecd47783..f60f80e4e6 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -68,8 +68,8 @@ import TcValidity
 import TcUnify
 import TcIface
 import TcSimplify
+import TcHsSyn
 import TcType
-import TcHsSyn( zonkSigType )
 import Inst   ( tcInstTyBinders, tcInstTyBinder )
 import TyCoRep( TyBinder(..) )  -- Used in tcDataKindSig
 import Type
@@ -82,7 +82,6 @@ import ConLike
 import DataCon
 import Class
 import Name
-import NameEnv
 import NameSet
 import VarEnv
 import TysWiredIn
@@ -114,13 +113,6 @@ to do this on un-desugared types. Luckily, desugared types are close enough
 to HsTypes to make the error messages sane.
 
 During type-checking, we perform as little validity checking as possible.
-This is because some type-checking is done in a mutually-recursive knot, and
-if we look too closely at the tycons, we'll loop. This is why we always must
-use mkNakedTyConApp and mkNakedAppTys, etc., which never look at a tycon.
-The mkNamed... functions don't uphold Type invariants, but zonkTcTypeToType
-will repair this for us. Note that zonkTcType *is* safe within a knot, and
-can be done repeatedly with no ill effect: it just squeezes out metavariables.
-
 Generally, after type-checking, you will want to do validity checking, say
 with TcValidity.checkValidType.
 
@@ -139,20 +131,12 @@ but not all:
 - Similarly, also a GHC extension, we look through synonyms before complaining
   about the form of a class or instance declaration
 
-- Ambiguity checks involve functional dependencies, and it's easier to wait
-  until knots have been resolved before poking into them
+- Ambiguity checks involve functional dependencies
 
 Also, in a mutually recursive group of types, we can't look at the TyCon until we've
 finished building the loop.  So to keep things simple, we postpone most validity
 checking until step (3).
 
-Knot tying
-~~~~~~~~~~
-During step (1) we might fault in a TyCon defined in another module, and it might
-(via a loop) refer back to a TyCon defined in this module. So when we tie a big
-knot around type declarations with ARecThing, so that the fault-in code can get
-the TyCon being defined.
-
 %************************************************************************
 %*                                                                      *
               Check types AND do validity checking
@@ -202,8 +186,7 @@ kcHsSigType skol_info names (HsIB { hsib_body = hs_ty
 kcHsSigType  _ _ (XHsImplicitBndrs _) = panic "kcHsSigType"
 
 tcClassSigType :: SkolemInfo -> [Located Name] -> LHsSigType GhcRn -> TcM Type
--- Does not do validity checking; this must be done outside
--- the recursive class declaration "knot"
+-- Does not do validity checking
 tcClassSigType skol_info names sig_ty
   = addSigCtxt (funsSigCtxt names) (hsSigType sig_ty) $
     tc_hs_sig_type_and_gen skol_info sig_ty liftedTypeKind
@@ -224,7 +207,7 @@ tcHsSigType ctxt sig_ty
           -- Generalise here: see Note [Kind generalisation]
        ; do_kind_gen <- decideKindGeneralisationPlan sig_ty
        ; ty <- if do_kind_gen
-               then tc_hs_sig_type_and_gen skol_info sig_ty kind
+               then tc_hs_sig_type_and_gen skol_info sig_ty kind >>= zonkTcType
                else tc_hs_sig_type         skol_info sig_ty kind
 
        ; checkValidType ctxt ty
@@ -238,7 +221,7 @@ tc_hs_sig_type_and_gen :: SkolemInfo -> LHsSigType GhcRn -> Kind -> TcM Type
 --   solve equalities,
 --   and then kind-generalizes.
 -- This will never emit constraints, as it uses solveEqualities interally.
--- No validity checking, but it does zonk en route to generalization
+-- No validity checking or zonking
 tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
                                               = HsIBRn { hsib_vars = sig_vars }
                                        , hsib_body = hs_ty }) kind
@@ -249,11 +232,9 @@ tc_hs_sig_type_and_gen skol_info (HsIB { hsib_ext
          --    kind variables floating about, immediately prior to
          --    kind generalisation
 
-         -- We use the "InKnot" zonker, because this is called
-         -- on class method sigs in the knot
-       ; ty1 <- zonkPromoteTypeInKnot $ mkSpecForAllTys tkvs ty
+       ; ty1 <- zonkPromoteType $ mkSpecForAllTys tkvs ty
        ; kvs <- kindGeneralize ty1
-       ; zonkSigType (mkInvForAllTys kvs ty1) }
+       ; return (mkInvForAllTys kvs ty1) }
 
 tc_hs_sig_type_and_gen _ (XHsImplicitBndrs _) _ = panic "tc_hs_sig_type_and_gen"
 
@@ -280,6 +261,7 @@ tcHsDeriv :: LHsSigType GhcRn -> TcM ([TyVar], (Class, [Type], [Kind]))
 -- E.g.    class C (a::*) (b::k->k)
 --         data T a b = ... deriving( C Int )
 --    returns ([k], C, [k, Int], [k->k])
+-- Return values are fully zonked
 tcHsDeriv hs_ty
   = do { cls_kind <- newMetaKindVar
                     -- always safe to kind-generalize, because there
@@ -287,7 +269,8 @@ tcHsDeriv hs_ty
        ; ty <- checkNoErrs $
                  -- avoid redundant error report with "illegal deriving", below
                tc_hs_sig_type_and_gen (SigTypeSkol DerivClauseCtxt) hs_ty cls_kind
-       ; cls_kind <- zonkTcType cls_kind
+       ; cls_kind <- zonkTcTypeToType emptyZonkEnv cls_kind
+       ; ty <- zonkTcTypeToType emptyZonkEnv ty
        ; let (tvs, pred) = splitForAllTys ty
        ; let (args, _) = splitFunTys cls_kind
        ; case getClassPredTys_maybe pred of
@@ -330,6 +313,7 @@ tcDerivStrategy user_ctxt mds thing_inside
       cls_kind <- newMetaKindVar
       ty' <- checkNoErrs $
              tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) ty cls_kind
+      ty' <- zonkTcTypeToType emptyZonkEnv ty'
       let (via_tvs, via_pred) = splitForAllTys ty'
       tcExtendTyVarEnv via_tvs $ do
         (thing_tvs, thing) <- thing_inside
@@ -347,6 +331,7 @@ tcHsClsInstType :: UserTypeCtxt    -- InstDeclCtxt or SpecInstCtxt
 tcHsClsInstType user_ctxt hs_inst_ty
   = setSrcSpan (getLoc (hsSigType hs_inst_ty)) $
     do { inst_ty <- tc_hs_sig_type_and_gen (SigTypeSkol user_ctxt) hs_inst_ty constraintKind
+       ; inst_ty <- zonkTcTypeToType emptyZonkEnv inst_ty
        ; checkValidInstance user_ctxt hs_inst_ty inst_ty }
 
 ----------------------------------------------
@@ -920,7 +905,7 @@ bigConstraintTuple arity
 tcInferApps :: TcTyMode
             -> Maybe (VarEnv Kind)  -- ^ Possibly, kind info (see above)
             -> LHsType GhcRn        -- ^ Function (for printing only)
-            -> TcType               -- ^ Function (could be knot-tied)
+            -> TcType               -- ^ Function
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType GhcRn]      -- ^ Args
             -> TcM (TcType, [TcType], TcKind) -- ^ (f args, args, result kind)
@@ -943,7 +928,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
     go :: Int             -- the # of the next argument
        -> [TcType]        -- already type-checked args, in reverse order
        -> TCvSubst        -- instantiating substitution
-       -> TcType          -- function applied to some args, could be knot-tied
+       -> TcType          -- function applied to some args
        -> [TyBinder]      -- binders in function kind (both vis. and invis.)
        -> TcKind          -- function kind body (not a Pi-type)
        -> [LHsType GhcRn] -- un-type-checked args
@@ -975,8 +960,7 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
                             -- nakedSubstTy: see Note [The well-kinded type invariant]
            ; arg' <- addErrCtxt (funAppCtxt orig_hs_ty arg n) $
                      tc_lhs_type mode arg exp_kind
-           ; traceTc "tcInferApps (vis 1)" (vcat [ ppr exp_kind
-                                                 , ppr (typeKind arg') ])
+           ; traceTc "tcInferApps (vis 1)" (ppr exp_kind)
            ; let subst' = extendTvSubstBinderAndInScope subst ki_binder arg'
            ; go (n+1) (arg' : acc_args) subst'
                 (mkNakedAppTy fun arg') -- See Note [The well-kinded type invariant]
@@ -1004,7 +988,6 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
         zapped_subst                   = zapTCvSubst subst
         hs_ty = mkHsAppTys orig_hs_ty (take (n-1) orig_hs_args)
 
-
 -- | Applies a type to a list of arguments.
 -- Always consumes all the arguments, using 'matchExpectedFunKind' as
 -- necessary. If you wish to apply a type to a list of HsTypes, this is
@@ -1012,14 +995,14 @@ tcInferApps mode mb_kind_info orig_hs_ty fun_ty fun_ki orig_hs_args
 -- Used for type-checking types only.
 tcTyApps :: TcTyMode
          -> LHsType GhcRn        -- ^ Function (for printing only)
-         -> TcType               -- ^ Function (could be knot-tied)
+         -> TcType               -- ^ Function
          -> TcKind               -- ^ Function kind (zonked)
          -> [LHsType GhcRn]      -- ^ Args
          -> TcM (TcType, TcKind) -- ^ (f args, result kind)   result kind is zonked
 -- Precondition: see precondition for tcInferApps
 tcTyApps mode orig_hs_ty fun_ty fun_ki args
   = do { (ty', _args, ki') <- tcInferApps mode Nothing orig_hs_ty fun_ty fun_ki args
-       ; return (ty' `mkNakedCastTy` mkRepReflCo ki', ki') }
+       ; return (ty' `mkNakedCastTy` mkNomReflCo ki', ki') }
           -- The mkNakedCastTy is for (IT3) of Note [The tcType invariant]
 
 --------------------------
@@ -1027,7 +1010,7 @@ tcTyApps mode orig_hs_ty fun_ty fun_ki args
 -- Obeys Note [The tcType invariant]
 checkExpectedKind :: HasDebugCallStack
                   => HsType GhcRn   -- type we're checking (for printing)
-                  -> TcType         -- type we're checking (might be knot-tied)
+                  -> TcType         -- type we're checking
                   -> TcKind         -- the known kind of that type
                   -> TcKind         -- the expected kind
                   -> TcM TcType
@@ -1158,13 +1141,11 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                                     (isTypeLevel (mode_level mode))
                                     (promotionErr name TyConPE)
                                 ; check_tc tc_tc
-                                ; tc <- get_loopy_tc name tc_tc
-                                ; handle_tyfams tc tc_tc }
-                             -- mkNakedTyConApp: see Note [Type-checking inside the knot]
+                                ; handle_tyfams tc_tc }
 
            AGlobal (ATyCon tc)
              -> do { check_tc tc
-                   ; handle_tyfams tc tc }
+                   ; handle_tyfams tc }
 
            AGlobal (AConLike (RealDataCon dc))
              -> do { data_kinds <- xoptM LangExt.DataKinds
@@ -1179,7 +1160,7 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                                     ConstrainedDataConPE pred
                        Nothing   -> pure ()
                    ; let tc = promoteDataCon dc
-                   ; return (mkNakedTyConApp tc [], tyConKind tc) }
+                   ; return (mkTyConApp tc [], tyConKind tc) }
 
            APromotionErr err -> promotionErr name err
 
@@ -1194,51 +1175,35 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
 
     -- if we are type-checking a type family tycon, we must instantiate
     -- any invisible arguments right away. Otherwise, we get #11246
-    handle_tyfams :: TyCon     -- the tycon to instantiate (might be loopy)
-                  -> TcTyCon   -- a non-loopy version of the tycon
+    handle_tyfams :: TyCon     -- the tycon to instantiate
                   -> TcM (TcType, TcKind)
-    handle_tyfams tc tc_tc
-      | mightBeUnsaturatedTyCon tc_tc || mode_unsat mode
+    handle_tyfams tc
+      | mightBeUnsaturatedTyCon tc || mode_unsat mode
                                          -- This is where mode_unsat is used
-      = do { tc_kind <- zonkTcType (tyConKind tc_tc)   -- (IT6) of Note [The tcType invariant]
-           ; traceTc "tcTyVar2a" (ppr tc_tc $$ ppr tc_kind)
-           ; return (mkNakedTyConApp tc [] `mkNakedCastTy` mkRepReflCo tc_kind, tc_kind) }
+      = do { tc_kind <- zonkTcType (tyConKind tc)   -- (IT6) of Note [The tcType invariant]
+           ; traceTc "tcTyVar2a" (ppr tc $$ ppr tc_kind)
+           ; return (mkTyConApp tc [] `mkNakedCastTy` mkNomReflCo tc_kind, tc_kind) }
               -- the mkNakedCastTy ensures (IT5) of Note [The tcType invariant]
 
       | otherwise
-      = do { tc_kind <- zonkTcType (tyConKind tc_tc)
+      = do { tc_kind <- zonkTcType (tyConKind tc)
            ; let (tc_kind_bndrs, tc_inner_ki) = splitPiTysInvisible tc_kind
-           ; (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc_tc))
+           ; (tc_args, kind) <- instantiateTyN Nothing (length (tyConBinders tc))
                                                tc_kind_bndrs tc_inner_ki
-           ; let is_saturated = tc_args `lengthAtLeast` tyConArity tc_tc
+           ; let is_saturated = tc_args `lengthAtLeast` tyConArity tc
                  tc_ty
-                   | is_saturated = mkNakedTyConApp tc tc_args `mkNakedCastTy` mkRepReflCo kind
+                   | is_saturated = mkTyConApp tc tc_args `mkNakedCastTy` mkNomReflCo kind
                       -- mkNakedCastTy is for (IT5) of Note [The tcType invariant]
-                   | otherwise    = mkNakedTyConApp tc tc_args
+                   | otherwise    = mkTyConApp tc tc_args
                       -- if the tycon isn't yet saturated, then we don't want mkNakedCastTy,
                       -- because that means we'll have an unsaturated type family
                       -- We don't need it anyway, because we can be sure that the
                       -- type family kind will accept further arguments (because it is
                       -- not yet saturated)
-           -- tc and tc_ty must not be traced here, because that would
-           -- force the evaluation of a potentially knot-tied variable (tc),
-           -- and the typechecker would hang, as per #11708
-           ; traceTc "tcTyVar2b" (vcat [ ppr tc_tc <+> dcolon <+> ppr tc_kind
+           ; traceTc "tcTyVar2b" (vcat [ ppr tc <+> dcolon <+> ppr tc_kind
                                        , ppr kind ])
            ; return (tc_ty, kind) }
 
-    get_loopy_tc :: Name -> TyCon -> TcM TyCon
-    -- Return the knot-tied global TyCon if there is one
-    -- Otherwise the local TcTyCon; we must be doing kind checking
-    -- but we still want to return a TyCon of some sort to use in
-    -- error messages
-    get_loopy_tc name tc_tc
-      = do { env <- getGblEnv
-           ; case lookupNameEnv (tcg_type_env env) name of
-                Just (ATyCon tc) -> return tc
-                _                -> do { traceTc "lk1 (loopy)" (ppr name)
-                                       ; return tc_tc } }
-
     -- We cannot promote a data constructor with a context that contains
     -- constraints other than equalities, so error if we find one.
     -- See Note [Constraints handled in types] in Inst.
@@ -1252,34 +1217,6 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                 | otherwise = True
 
 {-
-Note [Type-checking inside the knot]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we are checking the argument types of a data constructor.  We
-must zonk the types before making the DataCon, because once built we
-can't change it.  So we must traverse the type.
-
-BUT the parent TyCon is knot-tied, so we can't look at it yet.
-
-So we must be careful not to use "smart constructors" for types that
-look at the TyCon or Class involved.
-
-  * Hence the use of mkNakedXXX functions. These do *not* enforce
-    the invariants (for example that we use (FunTy s t) rather
-    than (TyConApp (->) [s,t])).
-
-  * The zonking functions establish invariants (even zonkTcType, a change from
-    previous behaviour). So we must never inspect the result of a
-    zonk that might mention a knot-tied TyCon. This is generally OK
-    because we zonk *kinds* while kind-checking types. And the TyCons
-    in kinds shouldn't be knot-tied, because they come from a previous
-    mutually recursive group.
-
-  * TcHsSyn.zonkTcTypeToType also can safely check/establish
-    invariants.
-
-This is horribly delicate.  I hate it.  A good example of how
-delicate it is can be seen in Trac #7903.
-
 Note [GADT kind self-reference]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -2671,7 +2608,8 @@ zonkPromoteMapper = TyCoMapper { tcm_smart    = True
                                , tcm_tyvar    = const zonkPromoteTcTyVar
                                , tcm_covar    = const covar
                                , tcm_hole     = const hole
-                               , tcm_tybinder = const tybinder }
+                               , tcm_tybinder = const tybinder
+                               , tcm_tycon    = return }
   where
     covar cv
       = mkCoVarCo <$> zonkPromoteTyCoVarKind cv
@@ -2727,11 +2665,6 @@ zonkPromoteTyCoVarBndr tv
 zonkPromoteCoercion :: Coercion -> TcM Coercion
 zonkPromoteCoercion = mapCoercion zonkPromoteMapper ()
 
-zonkPromoteTypeInKnot :: TcType -> TcM TcType
-zonkPromoteTypeInKnot = mapType (zonkPromoteMapper { tcm_smart = False }) ()
-  -- NB: Just changing smart to False will still use the smart zonker (not suitable
-  -- for in-the-knot) for kinds. But that's OK, because kinds aren't knot-tied.
-
 {-
 ************************************************************************
 *                                                                      *
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 1a13cb9826..58138eb631 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -74,7 +74,6 @@ module TcMType (
   zonkTcTyCoVarBndr, zonkTcTyVarBinder,
   zonkTcType, zonkTcTypes, zonkCo,
   zonkTyCoVarKind, zonkTcTypeMapper,
-  zonkTcTypeInKnot,
 
   zonkEvVar, zonkWC, zonkSimples,
   zonkId, zonkCoVar,
@@ -306,8 +305,7 @@ unpackCoercionHole_maybe :: CoercionHole -> TcM (Maybe Coercion)
 unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
 
 -- | Check that a coercion is appropriate for filling a hole. (The hole
--- itself is needed only for printing. NB: This must be /lazy/ in the coercion,
--- as it's used in TcHsSyn in the presence of knots.
+-- itself is needed only for printing.
 -- Always returns the checked coercion, but this return value is necessary
 -- so that the input coercion is forced only when the output is forced.
 checkCoercionHole :: CoVar -> Coercion -> TcM Coercion
@@ -1317,11 +1315,6 @@ tcGetGlobalTyCoVars
        ; writeMutVar gtv_var gbl_tvs'
        ; return gbl_tvs' }
 
--- | Zonk a type without using the smart constructors; the result type
--- is available for inspection within the type-checking knot.
-zonkTcTypeInKnot :: TcType -> TcM TcType
-zonkTcTypeInKnot = mapType (zonkTcTypeMapper { tcm_smart = False }) ()
-
 zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
 -- Zonk a type and take its free variables
 -- With kind polymorphism it can be essential to zonk *first*
@@ -1329,20 +1322,17 @@ zonkTcTypeAndFV :: TcType -> TcM DTyCoVarSet
 --    forall k1. forall (a:k2). a
 -- where k2:=k1 is in the substitution.  We don't want
 -- k2 to look free in this type!
--- NB: This might be called from within the knot, so don't use
--- smart constructors. See Note [Type-checking inside the knot] in TcHsType
 zonkTcTypeAndFV ty
-  = tyCoVarsOfTypeDSet <$> zonkTcTypeInKnot ty
+  = tyCoVarsOfTypeDSet <$> zonkTcType ty
 
 -- | Zonk a type and call 'candidateQTyVarsOfType' on it.
--- Works within the knot.
 zonkTcTypeAndSplitDepVars :: TcType -> TcM CandidatesQTvs
 zonkTcTypeAndSplitDepVars ty
-  = candidateQTyVarsOfType <$> zonkTcTypeInKnot ty
+  = candidateQTyVarsOfType <$> zonkTcType ty
 
 zonkTcTypesAndSplitDepVars :: [TcType] -> TcM CandidatesQTvs
 zonkTcTypesAndSplitDepVars tys
-  = candidateQTyVarsOfTypes <$> mapM zonkTcTypeInKnot tys
+  = candidateQTyVarsOfTypes <$> mapM zonkTcType tys
 
 zonkTyCoVar :: TyCoVar -> TcM TcType
 -- Works on TyVars and TcTyVars
@@ -1527,7 +1517,7 @@ zonkId id
 zonkCoVar :: CoVar -> TcM CoVar
 zonkCoVar = zonkId
 
--- | A suitable TyCoMapper for zonking a type inside the knot, and
+-- | A suitable TyCoMapper for zonking a type during type-checking,
 -- before all metavars are filled in.
 zonkTcTypeMapper :: TyCoMapper () TcM
 zonkTcTypeMapper = TyCoMapper
@@ -1535,7 +1525,8 @@ zonkTcTypeMapper = TyCoMapper
   , tcm_tyvar = const zonkTcTyVar
   , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
   , tcm_hole  = hole
-  , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv }
+  , tcm_tybinder = \_env tv _vis -> ((), ) <$> zonkTcTyCoVarBndr tv
+  , tcm_tycon = return }
   where
     hole :: () -> CoercionHole -> TcM Coercion
     hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
@@ -1546,7 +1537,6 @@ zonkTcTypeMapper = TyCoMapper
                Nothing -> do { cv' <- zonkCoVar cv
                              ; return $ HoleCo (hole { ch_co_var = cv' }) } }
 
-
 -- For unbound, mutable tyvars, zonkType uses the function given to it
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --      type variable and zonks the kind too
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index cbece8b8c6..8a3b7c7946 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -213,7 +213,7 @@ tcTyClDecls tyclds role_annots
            ; tcExtendRecEnv (zipRecTyClss tc_tycons rec_tyclss) $
 
                  -- Also extend the local type envt with bindings giving
-                 -- the (polymorphic) kind of each knot-tied TyCon or Class
+                 -- a TcTyCon for each each knot-tied TyCon or Class
                  -- See Note [Type checking recursive type and class declarations]
                  -- and Note [Type environment evolution]
              tcExtendKindEnvWithTyCons tc_tycons $
@@ -225,7 +225,8 @@ tcTyClDecls tyclds role_annots
     promotion_err_env = mkPromotionErrorEnv tyclds
     ppr_tc_tycon tc = parens (sep [ ppr (tyConName tc) <> comma
                                   , ppr (tyConBinders tc) <> comma
-                                  , ppr (tyConResKind tc) ])
+                                  , ppr (tyConResKind tc)
+                                  , ppr (isTcTyCon tc) ])
 
 zipRecTyClss :: [TcTyCon]
              -> [TyCon]           -- Knot-tied
@@ -374,6 +375,8 @@ TcTyCons are used for two distinct purposes
 
     In a TcTyCon, everything is zonked after the kind-checking pass (S2).
 
+    See also Note [Type checking recursive type and class declarations].
+
 Note [Check telescope again during generalisation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The telescope check before kind generalisation is useful to catch something
@@ -907,12 +910,11 @@ without looking at T?  Delicate answer: during tcTyClDecl, we extend
 
 Then:
 
-  * During TcHsType.kcTyVar we look in the *local* env, to get the
-    known kind for T.
+  * During TcHsType.tcTyVar we look in the *local* env, to get the
+    fully-known, not knot-tied TcTyCon for T.
 
-  * But in TcHsType.ds_type (and ds_var_app in particular) we look in
-    the *global* env to get the TyCon. But we must be careful not to
-    force the TyCon or we'll get a loop.
+  * Then, in TcHsSyn.zonkTcTypeToType (and zonkTcTyCon in particular) we look in
+    the *global* env to get the TyCon.
 
 This fancy footwork (with two bindings for T) is only necessary for the
 TyCons or Classes of this recursive group.  Earlier, finished groups,
@@ -1008,11 +1010,17 @@ tcTyClDecl1 _parent roles_info
                -- TODO: Allow us to distinguish between abstract class,
                -- and concrete class with no methods (maybe by
                -- specifying a trailing where or not
+               ; sig_stuff' <- mapM zonkTcMethInfoToMethInfo sig_stuff
+                  -- this zonk is really just to squeeze out the TcTyCons
+                  -- and convert, e.g., Skolems to tyvars. We won't
+                  -- see any unfilled metavariables here.
+
                ; is_boot <- tcIsHsBootOrSig
                ; let body | is_boot, null ctxt', null at_stuff, null sig_stuff
                           = Nothing
                           | otherwise
-                          = Just (ctxt', at_stuff, sig_stuff, mindef)
+                          = Just (ctxt', at_stuff, sig_stuff', mindef)
+
                ; clas <- buildClass class_name binders roles fds' body
                ; traceTc "tcClassDecl" (ppr fundeps $$ ppr binders $$
                                         ppr fds')
@@ -1096,13 +1104,7 @@ tcFamDecl1 parent (FamilyDecl { fdInfo = fam_info, fdLName = tc_lname@(L _ tc_na
          -- for this afterwards, in TcValidity.checkValidCoAxiom
          -- Example: tc265
 
-         -- Create a CoAxiom, with the correct src location. It is Vitally
-         -- Important that we do not pass the branches into
-         -- newFamInstAxiomName. They have types that have been zonked inside
-         -- the knot and we will die if we look at them. This is OK here
-         -- because there will only be one axiom, so we don't need to
-         -- differentiate names.
-         -- See [Zonking inside the knot] in TcHsType
+         -- Create a CoAxiom, with the correct src location.
        ; co_ax_name <- newFamInstAxiomName tc_lname []
 
        ; let mb_co_ax
@@ -1301,7 +1303,7 @@ tcClassATs class_name cls ats at_defs
 -------------------------
 tcDefaultAssocDecl :: TyCon                    -- ^ Family TyCon (not knot-tied)
                    -> [LTyFamDefltEqn GhcRn]        -- ^ Defaults
-                   -> TcM (Maybe (Type, SrcSpan))   -- ^ Type checked RHS
+                   -> TcM (Maybe (KnotTied Type, SrcSpan))   -- ^ Type checked RHS
 tcDefaultAssocDecl _ []
   = return Nothing  -- No default declaration
 
@@ -1384,7 +1386,15 @@ F's own type variables, so we need to convert it to (Proxy a -> b).
 We do this by calling tcMatchTys to match them up.  This also ensures
 that x's kind matches a's and similarly for y and b.  The error
 message isn't great, mind you.  (Trac #11361 was caused by not doing a
-proper tcMatchTys here.)  -}
+proper tcMatchTys here.)
+
+Recall also that the left-hand side of an associated type family
+default is always just variables -- no tycons here. Accordingly,
+the patterns used in the tcMatchTys won't actually be knot-tied,
+even though we're in the knot. This is too delicate for my taste,
+but it works.
+
+-}
 
 -------------------------
 kcTyFamInstEqn :: TcTyCon -> LTyFamInstEqn GhcRn -> TcM ()
@@ -1438,7 +1448,7 @@ kcTyFamEqnRhs mb_clsinfo rhs_hs_ty lhs_ki
     mb_kind_env = thdOf3 <$> mb_clsinfo
 
 tcTyFamInstEqn :: TcTyCon -> Maybe ClsInstInfo -> LTyFamInstEqn GhcRn
-               -> TcM CoAxBranch
+               -> TcM (KnotTied CoAxBranch)
 -- Needs to be here, not in TcInstDcls, because closed families
 -- (typechecked here) have TyFamInstEqns
 tcTyFamInstEqn fam_tc mb_clsinfo
@@ -1457,7 +1467,6 @@ tcTyFamInstEqn fam_tc mb_clsinfo
        ; pats'      <- zonkTcTypeToTypes ze pats
        ; rhs_ty'    <- zonkTcTypeToType ze rhs_ty
        ; traceTc "tcTyFamInstEqn" (ppr fam_tc <+> pprTyVars tvs')
-          -- don't print out the pats here, as they might be zonked inside the knot
        ; return (mkCoAxBranch tvs' [] pats' rhs_ty'
                               (map (const Nominal) tvs')
                               loc) }
@@ -1680,7 +1689,7 @@ tcFamTyPats fam_tc mb_clsinfo
        ; qtkvs <- quantifyTyVars emptyVarSet vars
 
        ; when debugIsOn $
-         do { all_pats <- mapM zonkTcTypeInKnot all_pats
+         do { all_pats <- mapM zonkTcType all_pats
             ; MASSERT2( isEmptyVarSet $ coVarsOfTypes all_pats, ppr all_pats ) }
            -- This should be the case, because otherwise the solveEqualities
            -- above would fail. TODO (RAE): Update once the solveEqualities
@@ -1688,7 +1697,6 @@ tcFamTyPats fam_tc mb_clsinfo
 
        ; traceTc "tcFamTyPats" (ppr (getName fam_tc)
                                 $$ ppr all_pats $$ ppr qtkvs)
-           -- Don't print out too much, as we might be in the knot
 
            -- See Note [Free-floating kind vars] in TcHsType
        ; let all_mentioned_tvs = mkVarSet qtkvs
@@ -1842,7 +1850,7 @@ consUseGadtSyntax _                           = False
                  -- All constructors have same shape
 
 -----------------------------------
-tcConDecls :: TyCon -> ([TyConBinder], Type)
+tcConDecls :: KnotTied TyCon -> ([KnotTied TyConBinder], KnotTied Type)
            -> [LConDecl GhcRn] -> TcM [DataCon]
   -- Why both the tycon tyvars and binders? Because the tyvars
   -- have all the names and the binders have the visibilities.
@@ -1852,9 +1860,9 @@ tcConDecls rep_tycon (tmpl_bndrs, res_tmpl)
     -- It's important that we pay for tag allocation here, once per TyCon,
     -- See Note [Constructor tag allocation], fixes #14657
 
-tcConDecl :: TyCon             -- Representation tycon. Knot-tied!
+tcConDecl :: KnotTied TyCon          -- Representation tycon. Knot-tied!
           -> NameEnv ConTag
-          -> [TyConBinder] -> Type
+          -> [KnotTied TyConBinder] -> KnotTied Type
                  -- Return type template (with its template tyvars)
                  --    (tvs, T tys), where T is the family TyCon
           -> ConDecl GhcRn
@@ -2024,7 +2032,7 @@ tcConDecl _ _ _ _ (XConDecl _) = panic "tcConDecl"
 quantifyConDecl :: TcTyCoVarSet  -- outer tvs, not to be quantified over; zonked
                 -> TcType -> TcM [TcTyVar]
 quantifyConDecl gbl_tvs ty
-  = do { ty <- zonkTcTypeInKnot ty
+  = do { ty <- zonkTcType ty
        ; let fvs = candidateQTyVarsOfType ty
        ; quantifyTyVars gbl_tvs fvs }
 
@@ -2129,7 +2137,7 @@ errors reported in one pass.  See Trac #7175, and #10836.
 --      TI :: forall b1 c1. (b1 ~ c1) => b1 -> :R7T b1 c1
 -- In this case orig_res_ty = T (e,e)
 
-rejigConRes :: [TyConBinder] -> Type    -- Template for result type; e.g.
+rejigConRes :: [KnotTied TyConBinder] -> KnotTied Type    -- Template for result type; e.g.
                                   -- data instance T [a] b c ...
                                   --      gives template ([a,b,c], T [a] b c)
                                   -- Type must be of kind *!
@@ -2137,7 +2145,7 @@ rejigConRes :: [TyConBinder] -> Type    -- Template for result type; e.g.
                                   -- type variables
             -> [TyVar]            -- The constructor's user-written, specified
                                   -- type variables
-            -> Type               -- res_ty type must be of kind *
+            -> KnotTied Type      -- res_ty type must be of kind *
             -> ([TyVar],          -- Universal
                 [TyVar],          -- Existential (distinct OccNames from univs)
                 [TyVar],          -- The constructor's rejigged, user-written,
@@ -2148,7 +2156,7 @@ rejigConRes :: [TyConBinder] -> Type    -- Template for result type; e.g.
                 TCvSubst)      -- Substitution to apply to argument types
         -- We don't check that the TyCon given in the ResTy is
         -- the same as the parent tycon, because checkValidDataCon will do it
-
+-- NB: All arguments may potentially be knot-tied
 rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
         -- E.g.  data T [a] b c where
         --         MkT :: forall x y z. T [(x,y)] z z
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 79b0e7fd08..4beae385f4 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -23,6 +23,7 @@ module TcType (
   TcType, TcSigmaType, TcRhoType, TcTauType, TcPredType, TcThetaType,
   TcTyVar, TcTyVarSet, TcDTyVarSet, TcTyCoVarSet, TcDTyCoVarSet,
   TcKind, TcCoVar, TcTyCoVar, TcTyVarBinder, TcTyCon,
+  KnotTied,
 
   ExpType(..), InferResult(..), ExpSigmaType, ExpRhoType, mkCheckExpType,
 
@@ -51,8 +52,7 @@ module TcType (
   --------------------------------
   -- Builders
   mkPhiTy, mkInfSigmaTy, mkSpecSigmaTy, mkSigmaTy,
-  mkNakedTyConApp, mkNakedAppTys, mkNakedAppTy,
-  mkNakedCastTy, nakedSubstTy,
+  mkNakedAppTy, mkNakedAppTys, mkNakedCastTy, nakedSubstTy,
 
   --------------------------------
   -- Splitters
@@ -353,7 +353,6 @@ type TcTyCoVarSet   = TyCoVarSet
 type TcDTyVarSet    = DTyVarSet
 type TcDTyCoVarSet  = DTyCoVarSet
 
-
 {- *********************************************************************
 *                                                                      *
           ExpType: an "expected type" in the type checker
@@ -1451,27 +1450,17 @@ Notes:
   not substTy, because the latter uses smart constructors that do
   Refl-elimination.
 
-* None of this is to do with knot-tying, which is the (quite distinct)
-  motivation for mkNakedTyConApp
 -}
 
 ---------------
-mkNakedTyConApp :: TyCon -> [Type] -> Type
--- Builds a TyConApp
---   * without being strict in TyCon,
---   * without satisfying the invariants of TyConApp
--- A subsequent zonking will establish the invariants
--- See Note [Type-checking inside the knot] in TcHsType
-mkNakedTyConApp tc tys = TyConApp tc tys
-
 mkNakedAppTys :: Type -> [Type] -> Type
--- See Note [Type-checking inside the knot] in TcHsType
+-- See Note [The well-kinded type invariant]
 mkNakedAppTys ty1                []   = ty1
-mkNakedAppTys (TyConApp tc tys1) tys2 = mkNakedTyConApp tc (tys1 ++ tys2)
+mkNakedAppTys (TyConApp tc tys1) tys2 = mkTyConApp tc (tys1 ++ tys2)
 mkNakedAppTys ty1                tys2 = foldl AppTy ty1 tys2
 
 mkNakedAppTy :: Type -> Type -> Type
--- See Note [Type-checking inside the knot] in TcHsType
+-- See Note [The well-kinded type invariant]
 mkNakedAppTy ty1 ty2 = mkNakedAppTys ty1 [ty2]
 
 mkNakedCastTy :: Type -> Coercion -> Type
@@ -1499,7 +1488,8 @@ nakedSubstMapper
                , tcm_tyvar    = \subst tv -> return (substTyVar subst tv)
                , tcm_covar    = \subst cv -> return (substCoVar subst cv)
                , tcm_hole     = \_ hole   -> return (HoleCo hole)
-               , tcm_tybinder = \subst tv _ -> return (substTyVarBndr subst tv) }
+               , tcm_tybinder = \subst tv _ -> return (substTyVarBndr subst tv)
+               , tcm_tycon    = return }
 
 {-
 ************************************************************************
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index ac85f9ec29..3ea4f61741 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -26,6 +26,7 @@ module TyCoRep (
         Type(..),
         TyLit(..),
         KindOrType, Kind,
+        KnotTied,
         PredType, ThetaType,      -- Synonyms
         ArgFlag(..),
 
@@ -468,6 +469,11 @@ These invariants are all documented above, in the declaration for Type.
 
 -}
 
+-- | A type labeled 'KnotTied' might have knot-tied tycons in it. See
+-- Note [Type checking recursive type and class declarations] in
+-- TcTyClsDecls
+type KnotTied ty = ty
+
 {- **********************************************************************
 *                                                                       *
                   TyBinder and ArgFlag
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 7836a0258d..0a02adf0b6 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -10,7 +10,8 @@ The @TyCon@ datatype
 
 module TyCon(
         -- * Main TyCon data types
-        TyCon, AlgTyConRhs(..), visibleDataCons,
+        TyCon,
+        AlgTyConRhs(..), visibleDataCons,
         AlgTyConFlav(..), isNoParent,
         FamTyConFlav(..), Role(..), Injectivity(..),
         RuntimeRepInfo(..), TyConFlavour(..),
@@ -812,7 +813,8 @@ data TyCon
         promDcRepInfo :: RuntimeRepInfo  -- ^ See comments with 'RuntimeRepInfo'
     }
 
-  -- | These exist only during a recursive type/class type-checking knot.
+  -- | These exist only during type-checking. See Note [How TcTyCons work]
+  -- in TcTyClsDecls
   | TcTyCon {
         tyConUnique :: Unique,
         tyConName   :: Name,
@@ -1530,10 +1532,11 @@ mkSumTyCon name binders res_kind arity tyvars cons parent
         algTcParent      = parent
     }
 
--- | Makes a tycon suitable for use during type-checking.
--- The only real need for this is for printing error messages during
--- a recursive type/class type-checking knot. It has a kind because
--- TcErrors sometimes calls typeKind.
+-- | Makes a tycon suitable for use during type-checking. It stores
+-- a variety of details about the definition of the TyCon, but no
+-- right-hand side. It lives only during the type-checking of a
+-- mutually-recursive group of tycons; it is then zonked to a proper
+-- TyCon in zonkTcTyCon.
 -- See also Note [Kind checking recursive type and class declarations]
 -- in TcTyClsDecls.
 mkTcTyCon :: Name
@@ -2383,7 +2386,11 @@ instance Uniquable TyCon where
 instance Outputable TyCon where
   -- At the moment a promoted TyCon has the same Name as its
   -- corresponding TyCon, so we add the quote to distinguish it here
-  ppr tc = pprPromotionQuote tc <> ppr (tyConName tc)
+  ppr tc = pprPromotionQuote tc <> ppr (tyConName tc) <> pp_tc
+    where
+      pp_tc = getPprStyle $ \sty -> if ((debugStyle sty || dumpStyle sty) && isTcTyCon tc)
+                                    then text "[tc]"
+                                    else empty
 
 -- | Paints a picture of what a 'TyCon' represents, in broad strokes.
 -- This is used towards more informative error messages.
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index eff667d044..3a3048d773 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -16,6 +16,7 @@ module Type (
         -- $representation_types
         TyThing(..), Type, ArgFlag(..), KindOrType, PredType, ThetaType,
         Var, TyVar, isTyVar, TyCoVar, TyBinder, TyVarBinder,
+        KnotTied,
 
         -- ** Constructing and deconstructing types
         mkTyVarTy, mkTyVarTys, getTyVar, getTyVar_maybe, repGetTyVar_maybe,
@@ -505,7 +506,7 @@ this one change made a 20% allocation difference in perf/compiler/T5030.
 data TyCoMapper env m
   = TyCoMapper
       { tcm_smart :: Bool -- ^ Should the new type be created with smart
-                         -- constructors?
+                          -- constructors?
       , tcm_tyvar :: env -> TyVar -> m Type
       , tcm_covar :: env -> CoVar -> m Coercion
       , tcm_hole  :: env -> CoercionHole -> m Coercion
@@ -514,20 +515,28 @@ data TyCoMapper env m
 
       , tcm_tybinder :: env -> TyVar -> ArgFlag -> m (env, TyVar)
           -- ^ The returned env is used in the extended scope
+
+      , tcm_tycon :: TyCon -> m TyCon
+          -- ^ This is used only to turn 'TcTyCon's into 'TyCon's.
+          -- See Note [Type checking recursive type and class declarations]
+          -- in TcTyClsDecls
       }
 
 {-# INLINABLE mapType #-}  -- See Note [Specialising mappers]
 mapType :: Monad m => TyCoMapper env m -> env -> Type -> m Type
 mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
-                           , tcm_tybinder = tybinder })
+                           , tcm_tybinder = tybinder, tcm_tycon = tycon })
         env ty
   = go ty
   where
     go (TyVarTy tv) = tyvar env tv
     go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
-    go t@(TyConApp _ []) = return t  -- avoid allocation in this exceedingly
-                                     -- common case (mostly, for *)
-    go (TyConApp tc tys) = mktyconapp tc <$> mapM go tys
+    go t@(TyConApp tc []) | not (isTcTyCon tc)
+                          = return t  -- avoid allocation in this exceedingly
+                                      -- common case (mostly, for *)
+    go (TyConApp tc tys)
+      = do { tc' <- tycon tc
+           ; mktyconapp tc' <$> mapM go tys }
     go (FunTy arg res)   = FunTy <$> go arg <*> go res
     go (ForAllTy (TvBndr tv vis) inner)
       = do { (env', tv') <- tybinder env tv vis
@@ -545,7 +554,8 @@ mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
 mapCoercion :: Monad m
             => TyCoMapper env m -> env -> Coercion -> m Coercion
 mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
-                               , tcm_hole = cohole, tcm_tybinder = tybinder })
+                               , tcm_hole = cohole, tcm_tybinder = tybinder
+                               , tcm_tycon = tycon })
             env co
   = go co
   where
@@ -555,7 +565,8 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
     go (Refl ty) = Refl <$> mapType mapper env ty
     go (GRefl r ty mco) = mkgreflco r <$> mapType mapper env ty <*> (go_mco mco)
     go (TyConAppCo r tc args)
-      = mktyconappco r tc <$> mapM go args
+      = do { tc' <- tycon tc
+           ; mktyconappco r tc' <$> mapM go args }
     go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
     go (ForAllCo tv kind_co co)
       = do { kind_co' <- go kind_co
diff --git a/testsuite/tests/dependent/should_compile/T14066a.stderr b/testsuite/tests/dependent/should_compile/T14066a.stderr
index 906695f3f7..610e434d6c 100644
--- a/testsuite/tests/dependent/should_compile/T14066a.stderr
+++ b/testsuite/tests/dependent/should_compile/T14066a.stderr
@@ -1,5 +1,5 @@
 
 T14066a.hs:13:3: warning:
     Type family instance equation is overlapped:
-      forall c d (x :: c) (y :: d).
+      forall d c (x :: c) (y :: d).
         Bar x y = Bool -- Defined at T14066a.hs:13:3
diff --git a/testsuite/tests/dependent/should_fail/T15380.hs b/testsuite/tests/dependent/should_fail/T15380.hs
new file mode 100644
index 0000000000..32ea8ec724
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+
+module T15380 where
+
+import Data.Kind
+
+class Generic a where
+  type Rep a :: Type
+
+class PGeneric a where
+  type To a (x :: Rep a) :: a
+
+type family MDefault (x :: a) :: a where
+  MDefault x = To (M x)
+
+class C a where
+  type M (x :: a) :: a
+  type M (x :: a) = MDefault x
diff --git a/testsuite/tests/dependent/should_fail/T15380.stderr b/testsuite/tests/dependent/should_fail/T15380.stderr
new file mode 100644
index 0000000000..9b30078c64
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T15380.stderr
@@ -0,0 +1,6 @@
+
+T15380.hs:16:16: error:
+    • Expecting one more argument to ‘To (M x)’
+      Expected a type, but ‘To (M x)’ has kind ‘Rep (M x) -> M x’
+    • In the type ‘To (M x)’
+      In the type family declaration for ‘MDefault’
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index 59d80375ff..593b7787a1 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -34,4 +34,4 @@ test('T15245', normal, compile_fail, [''])
 test('T15215', normal, compile_fail, [''])
 test('T15308', normal, compile_fail, ['-fno-print-explicit-kinds'])
 test('T15343', normal, compile_fail, [''])
-
+test('T15380', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
index 9765244f1e..d6ba833e35 100644
--- a/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
+++ b/testsuite/tests/ghci/scripts/T6018ghcifail.stderr
@@ -46,7 +46,7 @@
 
 <interactive>:60:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
diff --git a/testsuite/tests/polykinds/T7524.stderr b/testsuite/tests/polykinds/T7524.stderr
index 26cfe39e8a..2340ce1aa6 100644
--- a/testsuite/tests/polykinds/T7524.stderr
+++ b/testsuite/tests/polykinds/T7524.stderr
@@ -2,5 +2,5 @@
 T7524.hs:5:15: error:
     Conflicting family instance declarations:
       forall k2 (a :: k2). F a a = Int -- Defined at T7524.hs:5:15
-      forall k1 k2 (a :: k1) (b :: k2).
+      forall k2 k1 (a :: k1) (b :: k2).
         F a b = Bool -- Defined at T7524.hs:6:15
diff --git a/testsuite/tests/th/T10267.stderr b/testsuite/tests/th/T10267.stderr
index 0f8e2215bc..71aca96b86 100644
--- a/testsuite/tests/th/T10267.stderr
+++ b/testsuite/tests/th/T10267.stderr
@@ -24,7 +24,7 @@ T10267.hs:8:1: error:
     • Relevant bindings include i :: a -> a (bound at T10267.hs:8:1)
       Valid hole fits include
         i :: a -> a (bound at T10267.hs:8:1)
-        j :: forall a. a -> a
+        j :: forall a0. a0 -> a0
           with j @a
           (bound at T10267.hs:8:1)
         k :: forall a. a -> a
@@ -53,10 +53,10 @@ T10267.hs:14:3: error:
     • Relevant bindings include k :: a -> a (bound at T10267.hs:14:3)
       Valid hole fits include
         k :: a -> a (bound at T10267.hs:14:3)
-        j :: forall a. a -> a
+        j :: forall a0. a0 -> a0
           with j @a
           (bound at T10267.hs:8:1)
-        i :: forall a. a -> a
+        i :: forall a0. a0 -> a0
           with i @a
           (bound at T10267.hs:8:1)
         l :: forall a. a -> a
diff --git a/testsuite/tests/typecheck/should_fail/T6018fail.stderr b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
index 8c7a273ed8..829e14ad70 100644
--- a/testsuite/tests/typecheck/should_fail/T6018fail.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018fail.stderr
@@ -66,7 +66,7 @@ T6018fail.hs:59:10: error:
 
 T6018fail.hs:62:15: error:
     Type family equation violates injectivity annotation.
-    Kind variable ‘k1’ cannot be inferred from the right-hand side.
+    Kind variable ‘k2’ cannot be inferred from the right-hand side.
     Use -fprint-explicit-kinds to see the kind arguments
     In the type family equation:
       PolyKindVars '[] = '[] -- Defined at T6018fail.hs:62:15
@@ -153,5 +153,6 @@ T6018fail.hs:129:1: error:
 T6018fail.hs:134:1: error:
     Type family equation violates injectivity annotation.
     RHS of injective type family equation is a bare type variable
-    but these LHS type and kind patterns are not bare variables: ‘*’, ‘Char’
+    but these LHS type and kind patterns are not bare variables: ‘*’,
+                                                                 ‘Char’
       FC Char a = a -- Defined at T6018fail.hs:134:1
diff --git a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
index e90dce0620..9914842013 100644
--- a/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
+++ b/testsuite/tests/typecheck/should_fail/T6018failclosed.stderr
@@ -24,11 +24,11 @@ T6018failclosed.hs:19:5: error:
 
 T6018failclosed.hs:25:5: error:
     • Type family equation violates injectivity annotation.
-      Type and kind variables ‘k1’, ‘b’
+      Type and kind variables ‘k2’, ‘b’
       cannot be inferred from the right-hand side.
       Use -fprint-explicit-kinds to see the kind arguments
       In the type family equation:
-        forall k1 k2 (b :: k1) (c :: k2).
+        forall k1 k2 (b :: k2) (c :: k1).
           JClosed Int b c = Char -- Defined at T6018failclosed.hs:25:5
     • In the equations for closed type family ‘JClosed’
       In the type family declaration for ‘JClosed’