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.

1 files changed, 48 insertions, 25 deletions

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.