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.

2 files changed, 2 insertions, 12 deletions

diff --git a/compiler/hsSyn/HsTypes.hs b/compiler/hsSyn/HsTypes.hs
index 5eeca6eac2..fa87613416 100644
--- a/compiler/hsSyn/HsTypes.hs
+++ b/compiler/hsSyn/HsTypes.hs
@@ -57,8 +57,7 @@ module HsTypes (
         splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
         splitLHsPatSynTy,
         splitLHsForAllTy, splitLHsQualTy, splitLHsSigmaTy,
-        splitHsFunType,
-        splitHsAppTys, hsTyGetAppHead_maybe,
+        splitHsFunType, hsTyGetAppHead_maybe,
         mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
         ignoreParens, hsSigType, hsSigWcType,
         hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
@@ -1137,15 +1136,6 @@ The SrcSpan is the span of the original HsPar
 
 -}
 
-splitHsAppTys :: HsType GhcRn -> (LHsType GhcRn, [LHsTypeArg GhcRn])
-splitHsAppTys e = go (noLoc e) []
-  where
-    go :: LHsType GhcRn -> [LHsTypeArg GhcRn]
-       -> (LHsType GhcRn, [LHsTypeArg GhcRn])
-    go (L _ (HsAppTy _ f a))      as = go f (HsValArg a : as)
-    go (L _ (HsAppKindTy l ty k)) as = go ty (HsTypeArg l k : as)
-    go (L sp (HsParTy _ f))       as = go f (HsArgPar sp : as)
-    go f                          as = (f,as)
 --------------------------------
 splitLHsPatSynTy :: LHsType pass
                  -> ( [LHsTyVarBndr pass]    -- universals
diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index 9cd3a207ad..72c70a83ab 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -667,7 +667,7 @@ typeToLHsType ty
       | tyConAppNeedsKindSig True tc (length args)
         -- We must produce an explicit kind signature here to make certain
         -- programs kind-check. See Note [Kind signatures in typeToLHsType].
-      = nlHsParTy $ noLoc $ HsKindSig NoExt lhs_ty (go (typeKind ty))
+      = nlHsParTy $ noLoc $ HsKindSig NoExt lhs_ty (go (tcTypeKind ty))
       | otherwise = lhs_ty
        where
         arg_flags :: [ArgFlag]