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

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

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

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

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

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