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, 27 insertions, 14 deletions

diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index ffeb602382..c12c2f6e88 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -6,7 +6,7 @@
 Monadic type operations
 
 This module contains monadic operations over types that contain
-mutable type variables
+mutable type variables.
 -}
 
 {-# LANGUAGE CPP, TupleSections, MultiWayIf #-}
@@ -784,10 +784,8 @@ writeMetaTyVarRef tyvar ref ty
   = do { meta_details <- readMutVar ref;
        -- Zonk kinds to allow the error check to work
        ; zonked_tv_kind <- zonkTcType tv_kind
-       ; zonked_ty      <- zonkTcType ty
-       ; let zonked_ty_kind = tcTypeKind zonked_ty  -- Need to zonk even before typeKind;
-                                                    -- otherwise, we can panic in piResultTy
-             kind_check_ok = tcIsConstraintKind zonked_tv_kind
+       ; zonked_ty_kind <- zonkTcType ty_kind
+       ; let kind_check_ok = tcIsConstraintKind zonked_tv_kind
                           || tcEqKind zonked_ty_kind zonked_tv_kind
              -- Hack alert! tcIsConstraintKind: see TcHsType
              -- Note [Extra-constraint holes in partial type signatures]
@@ -813,6 +811,7 @@ writeMetaTyVarRef tyvar ref ty
        ; writeMutVar ref (Indirect ty) }
   where
     tv_kind = tyVarKind tyvar
+    ty_kind = tcTypeKind ty
 
     tv_lvl = tcTyVarLevel tyvar
     ty_lvl = tcTypeLevel ty
@@ -1518,15 +1517,14 @@ defaultTyVar default_kind tv
        ; writeMetaTyVar tv liftedRepTy
        ; return True }
 
-  | default_kind                 -- -XNoPolyKinds and this is a kind var
-  = do { default_kind_var tv     -- so default it to * if possible
-       ; return True }
+  | default_kind            -- -XNoPolyKinds and this is a kind var
+  = default_kind_var tv     -- so default it to * if possible
 
   | otherwise
   = return False
 
   where
-    default_kind_var :: TyVar -> TcM ()
+    default_kind_var :: TyVar -> TcM Bool
        -- defaultKindVar is used exclusively with -XNoPolyKinds
        -- See Note [Defaulting with -XNoPolyKinds]
        -- It takes an (unconstrained) meta tyvar and defaults it.
@@ -1534,11 +1532,20 @@ defaultTyVar default_kind tv
     default_kind_var kv
       | isLiftedTypeKind (tyVarKind kv)
       = do { traceTc "Defaulting a kind var to *" (ppr kv)
-           ; writeMetaTyVar kv liftedTypeKind }
+           ; writeMetaTyVar kv liftedTypeKind
+           ; return True }
       | otherwise
-      = addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
-                     , text "of kind:" <+> ppr (tyVarKind kv')
-                     , text "Perhaps enable PolyKinds or add a kind signature" ])
+      = do { addErr (vcat [ text "Cannot default kind variable" <+> quotes (ppr kv')
+                          , text "of kind:" <+> ppr (tyVarKind kv')
+                          , text "Perhaps enable PolyKinds or add a kind signature" ])
+           -- We failed to default it, so return False to say so.
+           -- Hence, it'll get skolemised.  That might seem odd, but we must either
+           -- promote, skolemise, or zap-to-Any, to satisfy TcHsType
+           --    Note [Recipe for checking a signature]
+           -- Otherwise we get level-number assertion failures. It doesn't matter much
+           -- because we are in an error siutation anyway.
+           ; return False
+        }
       where
         (_, kv') = tidyOpenTyCoVar emptyTidyEnv kv
 
@@ -1937,7 +1944,7 @@ zonkTcTypeMapper = TyCoMapper
   , tcm_covar = const (\cv -> mkCoVarCo <$> zonkTyCoVarKind cv)
   , tcm_hole  = hole
   , tcm_tycobinder = \_env tv _vis -> ((), ) <$> zonkTyCoVarKind tv
-  , tcm_tycon = return }
+  , tcm_tycon = zonk_tc_tycon }
   where
     hole :: () -> CoercionHole -> TcM Coercion
     hole _ hole@(CoercionHole { ch_ref = ref, ch_co_var = cv })
@@ -1948,6 +1955,12 @@ zonkTcTypeMapper = TyCoMapper
                Nothing -> do { cv' <- zonkCoVar cv
                              ; return $ HoleCo (hole { ch_co_var = cv' }) } }
 
+    zonk_tc_tycon tc  -- A non-poly TcTyCon may have unification
+                      -- variables that need zonking, but poly ones cannot
+      | tcTyConIsPoly tc = return tc
+      | otherwise        = do { tck' <- zonkTcType (tyConKind tc)
+                              ; return (setTcTyConKind tc tck') }
+
 -- 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