Make a smart mkAppTyM

This patch finally delivers on Trac #15952.  Specifically

* Completely remove Note [The tcType invariant], along with
  its complicated consequences (IT1-IT6).

* Replace Note [The well-kinded type invariant] with:

      Note [The Purely Kinded Type Invariant (PKTI)]

* Instead, establish the (PKTI) in TcHsType.tcInferApps,
  by using a new function mkAppTyM when building a type
  application.  See Note [mkAppTyM].

* As a result we can remove the delicate mkNakedXX functions
  entirely.  Specifically, mkNakedCastTy retained lots of
  extremly delicate Refl coercions which just cluttered
  everything up, and(worse) were very vulnerable to being
  silently eliminated by (say) substTy. This led to a
  succession of bug reports.

The result is noticeably simpler to explain, simpler
to code, and Richard and I are much more confident that
it is correct.

It does not actually fix any bugs, but it brings us closer.
E.g. I hoped it'd fix #15918 and #15799, but it doesn't quite
do so.  However, it makes it much easier to fix.

I also did a raft of other minor refactorings:

* Use tcTypeKind consistently in the type checker

* Rename tcInstTyBinders to tcInvisibleTyBinders,
  and refactor it a bit

* Refactor tcEqType, pickyEqType, tcEqTypeVis
  Simpler, probably more efficient.

* Make zonkTcType zonk TcTyCons, at least if they have
  any free unification variables -- see zonk_tc_tycon
  in TcMType.zonkTcTypeMapper.

  Not zonking these TcTyCons was actually a bug before.

* Simplify try_to_reduce_no_cache in TcFlatten (a lot)

* Combine checkExpectedKind and checkExpectedKindX.
  And then combine the invisible-binder instantation code
  Much simpler now.

* Fix a little bug in TcMType.skolemiseQuantifiedTyVar.
  I'm not sure how I came across this originally.

* Fix a little bug in TyCoRep.isUnliftedRuntimeRep
  (the ASSERT was over-zealous).  Again I'm not certain
  how I encountered this.

* Add a missing solveLocalEqualities in
  TcHsType.tcHsPartialSigType.
  I came across this when trying to get level numbers
  right.

6 files changed, 84 insertions, 49 deletions

diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index 7bb85740ac..733c11977e 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -430,7 +430,7 @@ splitAppCo_maybe (TyConAppCo r tc args)
   , Just (args', arg') <- snocView args
   = Just ( mkTyConAppCo r tc args', arg' )
 
-  | mightBeUnsaturatedTyCon tc
+  | not (mustBeSaturated tc)
     -- Never create unsaturated type family apps!
   , Just (args', arg') <- snocView args
   , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 1d48ed05b5..0e9a599573 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -1159,7 +1159,7 @@ etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
   = ASSERT( tc == tc2 ) Just cos2
 
 etaTyConAppCo_maybe tc co
-  | mightBeUnsaturatedTyCon tc
+  | not (mustBeSaturated tc)
   , (Pair ty1 ty2, r) <- coercionKindRole co
   , Just (tc1, tys1)  <- splitTyConApp_maybe ty1
   , Just (tc2, tys2)  <- splitTyConApp_maybe ty2
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index f7c21b7626..8dead3042d 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -917,8 +917,9 @@ isLiftedRuntimeRep rep
 
 isUnliftedRuntimeRep rep
   | Just rep' <- coreView rep          = isUnliftedRuntimeRep rep'
-  | TyConApp rr_tc args <- rep
-  , isUnliftedRuntimeRepTyCon rr_tc    = ASSERT( null args ) True
+  | TyConApp rr_tc _ <- rep   -- NB: args might be non-empty
+                              --     e.g. TupleRep
+  , isUnliftedRuntimeRepTyCon rr_tc    = True
   | otherwise                          = False
 
 isUnliftedRuntimeRepTyCon :: TyCon -> Bool
@@ -3448,6 +3449,8 @@ pprPrecTypeX env prec ty
     if debugStyle sty           -- Use debugPprType when in
     then debug_ppr_ty prec ty   -- when in debug-style
     else pprPrecIfaceType prec (tidyToIfaceTypeStyX env ty sty)
+    -- NB: debug-style is used for -dppr-debug
+    --     dump-style  is used for -ddump-tc-trace etc
 
 pprTyLit :: TyLit -> SDoc
 pprTyLit = pprIfaceTyLit . toIfaceTyLit
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index eb0b84d47e..058f090f59 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -50,7 +50,7 @@ module TyCon(
         isTupleTyCon, isUnboxedTupleTyCon, isBoxedTupleTyCon,
         isUnboxedSumTyCon, isPromotedTupleTyCon,
         isTypeSynonymTyCon,
-        mightBeUnsaturatedTyCon,
+        mustBeSaturated,
         isPromotedDataCon, isPromotedDataCon_maybe,
         isKindTyCon, isLiftedTypeKindTyConName,
         isTauTyCon, isFamFreeTyCon,
@@ -69,7 +69,8 @@ module TyCon(
         isTyConAssoc, tyConAssoc_maybe, tyConFlavourAssoc_maybe,
         isImplicitTyCon,
         isTyConWithSrcDataCons,
-        isTcTyCon, isTcLevPoly,
+        isTcTyCon, setTcTyConKind,
+        isTcLevPoly,
 
         -- ** Extracting information out of TyCons
         tyConName,
@@ -108,7 +109,7 @@ module TyCon(
         pprPromotionQuote, mkTyConKind,
 
         -- ** Predicated on TyConFlavours
-        tcFlavourCanBeUnsaturated, tcFlavourIsOpen,
+        tcFlavourIsOpen,
 
         -- * Runtime type representation
         TyConRepName, tyConRepName_maybe,
@@ -1930,11 +1931,11 @@ isFamFreeTyCon _                                          = True
 --            (T ~N d), (a ~N e) and (b ~N f)?
 -- Specifically NOT true of synonyms (open and otherwise)
 --
--- It'd be unusual to call mightBeUnsaturatedTyCon on a regular H98
+-- It'd be unusual to call mustBeSaturated on a regular H98
 -- type synonym, because you should probably have expanded it first
 -- But regardless, it's not decomposable
-mightBeUnsaturatedTyCon :: TyCon -> Bool
-mightBeUnsaturatedTyCon = tcFlavourCanBeUnsaturated . tyConFlavour
+mustBeSaturated :: TyCon -> Bool
+mustBeSaturated = tcFlavourMustBeSaturated . tyConFlavour
 
 -- | Is this an algebraic 'TyCon' declared with the GADT syntax?
 isGadtSyntaxTyCon :: TyCon -> Bool
@@ -2131,6 +2132,14 @@ isTcTyCon :: TyCon -> Bool
 isTcTyCon (TcTyCon {}) = True
 isTcTyCon _            = False
 
+setTcTyConKind :: TyCon -> Kind -> TyCon
+-- Update the Kind of a TcTyCon
+-- The new kind is always a zonked version of its previous
+-- kind, so we don't need to update any other fields.
+-- See Note [The Purely Kinded Invariant] in TcHsType
+setTcTyConKind tc@(TcTyCon {}) kind = tc { tyConKind = kind }
+setTcTyConKind tc              _    = pprPanic "setTcTyConKind" (ppr tc)
+
 -- | Could this TyCon ever be levity-polymorphic when fully applied?
 -- True is safe. False means we're sure. Does only a quick check
 -- based on the TyCon's category.
@@ -2504,19 +2513,19 @@ tyConFlavour (PromotedDataCon {}) = PromotedDataConFlavour
 tyConFlavour (TcTyCon { tcTyConFlavour = flav }) = flav
 
 -- | Can this flavour of 'TyCon' appear unsaturated?
-tcFlavourCanBeUnsaturated :: TyConFlavour -> Bool
-tcFlavourCanBeUnsaturated ClassFlavour            = True
-tcFlavourCanBeUnsaturated DataTypeFlavour         = True
-tcFlavourCanBeUnsaturated NewtypeFlavour          = True
-tcFlavourCanBeUnsaturated DataFamilyFlavour{}     = True
-tcFlavourCanBeUnsaturated TupleFlavour{}          = True
-tcFlavourCanBeUnsaturated SumFlavour              = True
-tcFlavourCanBeUnsaturated AbstractTypeFlavour     = True
-tcFlavourCanBeUnsaturated BuiltInTypeFlavour      = True
-tcFlavourCanBeUnsaturated PromotedDataConFlavour  = True
-tcFlavourCanBeUnsaturated TypeSynonymFlavour      = False
-tcFlavourCanBeUnsaturated OpenTypeFamilyFlavour{} = False
-tcFlavourCanBeUnsaturated ClosedTypeFamilyFlavour = False
+tcFlavourMustBeSaturated :: TyConFlavour -> Bool
+tcFlavourMustBeSaturated ClassFlavour            = False
+tcFlavourMustBeSaturated DataTypeFlavour         = False
+tcFlavourMustBeSaturated NewtypeFlavour          = False
+tcFlavourMustBeSaturated DataFamilyFlavour{}     = False
+tcFlavourMustBeSaturated TupleFlavour{}          = False
+tcFlavourMustBeSaturated SumFlavour              = False
+tcFlavourMustBeSaturated AbstractTypeFlavour     = False
+tcFlavourMustBeSaturated BuiltInTypeFlavour      = False
+tcFlavourMustBeSaturated PromotedDataConFlavour  = False
+tcFlavourMustBeSaturated TypeSynonymFlavour      = True
+tcFlavourMustBeSaturated OpenTypeFamilyFlavour{} = True
+tcFlavourMustBeSaturated ClosedTypeFamilyFlavour = True
 
 -- | Is this flavour of 'TyCon' an open type family or a data family?
 tcFlavourIsOpen :: TyConFlavour -> Bool
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 142da4c79c..6590489b01 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -539,9 +539,11 @@ data TyCoMapper env m
           -- ^ 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
+          -- ^ This is used only for TcTyCons
+          -- a) To zonk TcTyCons
+          -- b) To turn TcTyCons into TyCons.
+          --    See Note [Type checking recursive type and class declarations]
+          --    in TcTyClsDecls
       }
 
 {-# INLINABLE mapType #-}  -- See Note [Specialising mappers]
@@ -553,12 +555,18 @@ mapType mapper@(TyCoMapper { tcm_smart = smart, tcm_tyvar = tyvar
   where
     go (TyVarTy tv) = tyvar env tv
     go (AppTy t1 t2) = mkappty <$> go t1 <*> go t2
-    go t@(TyConApp tc []) | not (isTcTyCon tc)
-                          = return t  -- avoid allocation in this exceedingly
-                                      -- common case (mostly, for *)
-    go (TyConApp tc tys)
+    go ty@(TyConApp tc tys)
+      | isTcTyCon tc
       = do { tc' <- tycon tc
            ; mktyconapp tc' <$> mapM go tys }
+
+      -- Not a TcTyCon
+      | null tys    -- Avoid allocation in this very
+      = return ty   -- common case (E.g. Int, LiftedRep etc)
+
+      | otherwise
+      = mktyconapp tc <$> mapM go tys 
+
     go (FunTy arg res)   = FunTy <$> go arg <*> go res
     go (ForAllTy (Bndr tv vis) inner)
       = do { (env', tv') <- tycobinder env tv vis
@@ -587,7 +595,9 @@ 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)
-      = do { tc' <- tycon tc
+      = do { tc' <- if isTcTyCon tc
+                    then tycon tc
+                    else return tc
            ; mktyconappco r tc' <$> mapM go args }
     go (AppCo c1 c2) = mkappco <$> go c1 <*> go c2
     go (ForAllCo tv kind_co co)
@@ -720,6 +730,10 @@ mkAppTy ty1               ty2 = AppTy ty1 ty2
         --
         -- Here Id is partially applied in the type sig for Foo,
         -- but once the type synonyms are expanded all is well
+        --
+        -- Moreover in TcHsTypes.tcInferApps we build up a type
+        --   (T t1 t2 t3) one argument at a type, thus forming
+        --   (T t1), (T t1 t2), etc
 
 mkAppTys :: Type -> [Type] -> Type
 mkAppTys ty1                []   = ty1
@@ -758,7 +772,7 @@ repSplitAppTy_maybe (AppTy ty1 ty2)
   = Just (ty1, ty2)
 
 repSplitAppTy_maybe (TyConApp tc tys)
-  | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
+  | not (mustBeSaturated tc) || tys `lengthExceeds` tyConArity tc
   , Just (tys', ty') <- snocView tys
   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 
@@ -770,6 +784,8 @@ repSplitAppTy_maybe _other = Nothing
 tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
 -- any coreView stuff is already done. Refuses to look through (c => t)
+-- The "Rep" means that we assumes that any tcView stuff is already done.
+-- Refuses to look through (c => t)
 tcRepSplitAppTy_maybe (FunTy ty1 ty2)
   | isPredTy ty1
   = Nothing  -- See Note [Decomposing fat arrow c=>t]
@@ -782,13 +798,14 @@ tcRepSplitAppTy_maybe (FunTy ty1 ty2)
 
 tcRepSplitAppTy_maybe (AppTy ty1 ty2)    = Just (ty1, ty2)
 tcRepSplitAppTy_maybe (TyConApp tc tys)
-  | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
+  | not (mustBeSaturated tc) || tys `lengthExceeds` tyConArity tc
   , Just (tys', ty') <- snocView tys
   = Just (TyConApp tc tys', ty')    -- Never create unsaturated type family apps!
 tcRepSplitAppTy_maybe _other = Nothing
 
 -- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
 tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+-- The "Rep" means that we assumes that any tcView stuff is already done.
 -- Defined here to avoid module loops between Unify and TcType.
 tcRepSplitTyConApp_maybe (TyConApp tc tys)
   = Just (tc, tys)
@@ -804,6 +821,7 @@ tcRepSplitTyConApp_maybe _
 
 -- | Like 'tcSplitTyConApp' but doesn't look through type synonyms.
 tcRepSplitTyConApp :: HasCallStack => Type -> (TyCon, [Type])
+-- The "Rep" means that we assumes that any tcView stuff is already done.
 -- Defined here to avoid module loops between Unify and TcType.
 tcRepSplitTyConApp ty =
   case tcRepSplitTyConApp_maybe ty of
@@ -829,8 +847,8 @@ splitAppTys ty = split ty ty []
     split _       (AppTy ty arg)        args = split ty ty (arg:args)
     split _       (TyConApp tc tc_args) args
       = let -- keep type families saturated
-            n | mightBeUnsaturatedTyCon tc = 0
-              | otherwise                  = tyConArity tc
+            n | mustBeSaturated tc = tyConArity tc
+              | otherwise          = 0
             (tc_args1, tc_args2) = splitAt n tc_args
         in
         (TyConApp tc tc_args1, tc_args2 ++ args)
@@ -849,8 +867,8 @@ repSplitAppTys ty = split ty []
   where
     split (AppTy ty arg) args = split ty (arg:args)
     split (TyConApp tc tc_args) args
-      = let n | mightBeUnsaturatedTyCon tc = 0
-              | otherwise                  = tyConArity tc
+      = let n | mustBeSaturated tc = tyConArity tc
+              | otherwise          = 0
             (tc_args1, tc_args2) = splitAt n tc_args
         in
         (TyConApp tc tc_args1, tc_args2 ++ args)
@@ -967,9 +985,6 @@ In the compiler we maintain the invariant that all saturated applications of
 See #11714.
 -}
 
-isFunTy :: Type -> Bool
-isFunTy ty = isJust (splitFunTy_maybe ty)
-
 splitFunTy :: Type -> (Type, Type)
 -- ^ Attempts to extract the argument and result types from a type, and
 -- panics if that is not possible. See also 'splitFunTy_maybe'
@@ -1011,6 +1026,8 @@ piResultTy ty arg = case piResultTy_maybe ty arg of
                       Nothing  -> pprPanic "piResultTy" (ppr ty $$ ppr arg)
 
 piResultTy_maybe :: Type -> Type -> Maybe Type
+-- We don't need a 'tc' version, because
+-- this function behaves the same for Type and Constraint
 piResultTy_maybe ty arg
   | Just ty' <- coreView ty = piResultTy_maybe ty' arg
 
@@ -1460,11 +1477,17 @@ isForAllTy_co _             = False
 
 -- | Is this a function or forall?
 isPiTy :: Type -> Bool
-isPiTy ty | Just ty' <- coreView ty = isForAllTy ty'
+isPiTy ty | Just ty' <- coreView ty = isPiTy ty'
 isPiTy (ForAllTy {}) = True
 isPiTy (FunTy {})    = True
 isPiTy _             = False
 
+-- | Is this a function?
+isFunTy :: Type -> Bool
+isFunTy ty | Just ty' <- coreView ty = isFunTy ty'
+isFunTy (FunTy {}) = True
+isFunTy _          = False
+
 -- | Take a forall type apart, or panics if that is not possible.
 splitForAllTy :: Type -> (TyCoVar, Type)
 splitForAllTy ty
@@ -2705,6 +2728,7 @@ Note that:
 
 -----------------------------
 typeKind :: HasDebugCallStack => Type -> Kind
+-- No need to expand synonyms
 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
 typeKind (LitTy l)         = typeLiteralKind l
 typeKind (FunTy {})        = liftedTypeKind
@@ -2732,6 +2756,7 @@ typeKind ty@(ForAllTy {})
 
 -----------------------------
 tcTypeKind :: HasDebugCallStack => Type -> Kind
+-- No need to expand synonyms
 tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
 tcTypeKind (LitTy l)         = typeLiteralKind l
 tcTypeKind (TyVarTy tyvar)   = tyVarKind tyvar
@@ -2739,8 +2764,8 @@ tcTypeKind (CastTy _ty co)   = pSnd $ coercionKind co
 tcTypeKind (CoercionTy co)   = coercionType co
 
 tcTypeKind (FunTy arg res)
-  | isPredTy arg && isPredTy res = constraintKind
-  | otherwise                    = liftedTypeKind
+  | isPredTy arg, isPredTy res = constraintKind
+  | otherwise                  = liftedTypeKind
 
 tcTypeKind (AppTy fun arg)
   = go fun [arg]
@@ -2765,16 +2790,14 @@ tcTypeKind ty@(ForAllTy {})
     body_kind = tcTypeKind body
 
 
-isPredTy :: Type -> Bool
+isPredTy :: HasDebugCallStack => Type -> Bool
 -- See Note [Types for coercions, predicates, and evidence]
 isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
 
 --------------------------
 typeLiteralKind :: TyLit -> Kind
-typeLiteralKind l =
-  case l of
-    NumTyLit _ -> typeNatKind
-    StrTyLit _ -> typeSymbolKind
+typeLiteralKind (NumTyLit {}) = typeNatKind
+typeLiteralKind (StrTyLit {}) = typeSymbolKind
 
 -- | Returns True if a type is levity polymorphic. Should be the same
 -- as (isKindLevPoly . typeKind) but much faster.
diff --git a/compiler/types/Type.hs-boot b/compiler/types/Type.hs-boot
index 84fbaca6f7..d9ea519a08 100644
--- a/compiler/types/Type.hs-boot
+++ b/compiler/types/Type.hs-boot
@@ -8,7 +8,7 @@ import Var ( TyCoVar )
 import {-# SOURCE #-} TyCoRep( Type, Coercion )
 import Util
 
-isPredTy     :: Type -> Bool
+isPredTy     :: HasDebugCallStack => Type -> Bool
 isCoercionTy :: Type -> Bool
 
 mkAppTy    :: Type -> Type -> Type