Furher work on monadic tcTypeKindwip/T15952

This version is nearly validate-clean, modulo a failure in
   rename/should_compile/T4239

But Richard and I now plan a different path, so I'm going
to park this.

11 files changed, 56 insertions, 54 deletions

diff --git a/compiler/typecheck/Inst.hs b/compiler/typecheck/Inst.hs
index defa67b6dd..48dbac0361 100644
--- a/compiler/typecheck/Inst.hs
+++ b/compiler/typecheck/Inst.hs
@@ -568,7 +568,6 @@ tcInstTyBinder subst (Anon ty)
 -------------------------------
 -- | This takes @a ~# b@ and returns @a ~~ b@.
 mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
--- monadic just for convenience with mkEqBoxTy
 mkHEqBoxTy co ty1 ty2
   = do { k1 <- tcTypeKindM ty1
        ; k2 <- tcTypeKindM ty2
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 5d9aabeaf0..6cca7a3c48 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -1040,7 +1040,8 @@ can_eq_nc_forall ev eq_rel s1 s2
     -- than putting it in the work list
     unify loc role ty1 ty2
       = do { already_eq <- ty1 `tcEqTypeM` ty2
-           ; if already_eq then return (mkTcReflCo role ty1, emptyBag)
+           ; if already_eq
+             then return (mkTcReflCo role ty1, emptyBag)
              else do { (wanted, co) <- newWantedEq loc role ty1 ty2
                      ; return (co, unitBag (mkNonCanonical wanted)) } }
 
@@ -1813,21 +1814,15 @@ canEqTyVar :: CtEvidence          -- ev :: lhs ~ rhs
            -> TcType -> TcType      -- rhs: already flat
            -> TcS (StopOrContinue Ct)
 canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
- = do { let k1 = tyVarKind tv1
-      ; k2 <- tcTypeKindM xi2
-      ; homo_kind <- tcEqTypeM k1 k2
-      ; if homo_kind
-        then canEqTyVarHomo  ev eq_rel swapped tv1 ps_ty1    xi2 ps_xi2
-        else canEqTyVarTake2 ev eq_rel swapped tv1 ps_ty1 k1 xi2 ps_xi2 k2 }
-
-canEqTyVarTake2 :: CtEvidence          -- ev :: lhs ~ rhs
-                -> EqRel -> SwapFlag
-                -> TcTyVar -> TcType -> TcKind   -- tv1, its pretty form, and its kind
-                -> TcType  -> TcType -> TcKind   -- rhs, its pretty form, and its kind
-                                                 -- Both tv1 and rhs are already flat
-                -> TcS (StopOrContinue Ct)
-canEqTyVarTake2 ev eq_rel swapped tv1 ps_ty1 k1 xi2 ps_xi2 k2
-  = do { -- Note [Flattening] in TcFlatten gives us (F2), which says that
+  = do { let k1 = tyVarKind tv1
+       ; k2 <- tcTypeKindM xi2
+       ; homo_kind <- tcEqTypeM k1 k2
+       ; if homo_kind
+         then canEqTyVarHomo  ev eq_rel swapped tv1 ps_ty1    xi2 ps_xi2
+         else
+
+    -- So the LHS and RHS don't have equal kinds, even modulo zonking
+    do { -- Note [Flattening] in TcFlatten gives us (F2), which says that
          -- flattening is always homogeneous (doesn't change kinds). But
          -- perhaps by flattening the kinds of the two sides of the equality
          -- at hand makes them equal. So let's try that.
@@ -1842,7 +1837,7 @@ canEqTyVarTake2 ev eq_rel swapped tv1 ps_ty1 k1 xi2 ps_xi2 k2
                         , ppr flat_k2
                         , ppr k2_co ])
 
-         -- we know the LHS is a tyvar. So let's dump all the coercions on the RHS
+         -- We know the LHS is a tyvar. So let's dump all the coercions on the RHS
          -- If flat_k1 == flat_k2, let's dump all the coercions on the RHS and
          -- then call canEqTyVarHomo. If they don't equal, just rewriteEqEvidence
          -- (as an optimization, so that we don't have to flatten the kinds again)
@@ -1879,7 +1874,7 @@ canEqTyVarTake2 ev eq_rel swapped tv1 ps_ty1 k1 xi2 ps_xi2 k2
        ; new_ev <- rewriteEqEvidence ev swapped new_lhs new_rhs lhs_co rhs_co
          -- no longer swapped, due to rewriteEqEvidence
        ; canEqTyVarHetero new_ev eq_rel tv1 sym_k1_co flat_k1 ps_ty1
-                                        new_rhs flat_k2 ps_rhs } }
+                                        new_rhs flat_k2 ps_rhs } } }
   where
     xi1 = mkTyVarTy tv1
     loc  = ctEvLoc ev
diff --git a/compiler/typecheck/TcDeriv.hs b/compiler/typecheck/TcDeriv.hs
index fde558100b..da3fee6b3d 100644
--- a/compiler/typecheck/TcDeriv.hs
+++ b/compiler/typecheck/TcDeriv.hs
@@ -833,16 +833,18 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
                    ; final_inst_ty_kind <- tcTypeKindM (mkTyConApp tc final_tc_args')
                    ; let via_match = tcUnifyTy final_inst_ty_kind final_via_kind
 
-                   ; checkTc (isJust via_match) $
-                     derivingViaKindErr cls final_inst_ty_kind
-                                        via_ty final_via_kind
-
-                   ; let Just via_subst = via_match
-                         (final_tkvs, final_cls_tys, final_tc_args)
-                            = propagate_subst via_subst tkvs'
+                   ; case via_match of
+                       Nothing -> derivingViaKindErr cls final_inst_ty_kind
+                                                     via_ty final_via_kind
+
+                       Just via_subst
+                         -> pure ( final_tkvs, final_cls_tys, final_tc_args
+                                 , Just $ ViaStrategy $ substTy via_subst via_ty ) }
+                         where
+                            let (final_tkvs, final_cls_tys, final_tc_args)
+                                    = propagate_subst via_subst tkvs'
                                               final_cls_tys' final_tc_args'
-                   ; pure ( final_tkvs, final_cls_tys, final_tc_args
-                          , Just $ ViaStrategy $ substTy via_subst via_ty ) }
+
 
               _ -> pure ( tkvs', final_cls_tys', final_tc_args'
                         , mb_deriv_strat' )
diff --git a/compiler/typecheck/TcDerivInfer.hs b/compiler/typecheck/TcDerivInfer.hs
index df1a3a51fc..79f4ba1c9f 100644
--- a/compiler/typecheck/TcDerivInfer.hs
+++ b/compiler/typecheck/TcDerivInfer.hs
@@ -194,7 +194,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
            -- See Note [Inferring the instance context]
            mk_functor_like_constraints orig t_or_k cls
               = map $ \ty -> let ki = tcTypeKind ty in
-                                 -- OK to use typeKind because 'ty' is a fully
+                                 -- OK to use tcTypeKind because 'ty' is a fully
                                  -- zonked constructor argument type
                              ( [ mk_cls_pred orig t_or_k cls ty
                                , mkPredOrigin orig KindLevel
@@ -236,13 +236,13 @@ inferConstraintsDataConArgs inst_ty inst_tys
              | main_cls `hasKey` dataClassKey
              = do { rep_tc_arg_kinds <- lift $ mapM tcTypeKindM rep_tc_args
                   ; if all isLiftedTypeKind rep_tc_arg_kinds
-                    then return [mkThetaOriginFromPreds constrs]
+                    then return [mkThetaOriginFromPreds preds]
                     else return [] }
              | otherwise
              = return []
              where
-               constrs = [ mk_cls_pred deriv_origin t_or_k main_cls ty
-                         | (t_or_k, ty) <- zip t_or_ks rep_tc_args ]
+               preds = [ mk_cls_pred deriv_origin t_or_k main_cls ty
+                       | (t_or_k, ty) <- zip t_or_ks rep_tc_args ]
 
            mk_cls_pred orig t_or_k cls ty
                 -- Don't forget to apply to cls_tys' too
diff --git a/compiler/typecheck/TcDerivUtils.hs b/compiler/typecheck/TcDerivUtils.hs
index 86205de5fd..4764d08861 100644
--- a/compiler/typecheck/TcDerivUtils.hs
+++ b/compiler/typecheck/TcDerivUtils.hs
@@ -387,20 +387,27 @@ instance Outputable ThetaOrigin where
 mkPredOrigin :: CtOrigin -> TypeOrKind -> PredType -> PredOrigin
 mkPredOrigin origin t_or_k pred = PredOrigin pred origin t_or_k
 
+substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin
+substPredOrigin subst (PredOrigin pred origin t_or_k)
+  = PredOrigin (substTy subst pred) origin t_or_k
+
 mkThetaOrigin :: CtOrigin -> TypeOrKind
               -> [TyVar] -> [TyVar] -> ThetaType -> ThetaType
               -> ThetaOrigin
-mkThetaOrigin origin t_or_k skols metas givens
-  = ThetaOrigin skols metas givens . map (mkPredOrigin origin t_or_k)
+mkThetaOrigin origin t_or_k skols metas givens wanteds
+  = ThetaOrigin { to_anyclass_skols   = skols
+                , to_anyclass_metas   = metas
+                , to_anyclass_givens  = givens
+                , to_anyclass_wanteds = map (mkPredOrigin origin t_or_k) wanteds }
 
 -- A common case where the ThetaOrigin only contains wanted constraints, with
 -- no givens or locally scoped type variables.
 mkThetaOriginFromPreds :: [PredOrigin] -> ThetaOrigin
-mkThetaOriginFromPreds = ThetaOrigin [] [] []
-
-substPredOrigin :: HasCallStack => TCvSubst -> PredOrigin -> PredOrigin
-substPredOrigin subst (PredOrigin pred origin t_or_k)
-  = PredOrigin (substTy subst pred) origin t_or_k
+mkThetaOriginFromPreds wanted
+  = ThetaOrigin { to_anyclass_skols   = []
+                , to_anyclass_metas   = []
+                , to_anyclass_givens  = []
+                , to_anyclass_wanteds = wanted }
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index a4f5a99485..c6ac426010 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -603,7 +603,7 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics })
 
     is_user_type_error ct _ = isUserTypeErrorCt ct
 
-    is_homo_equality _ (EqPred _ ty1 ty2) = typeKind ty1 `tcEqType` typeKind ty2
+    is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTpeKind ty2
     is_homo_equality _ _                  = False
 
     is_equality _ (EqPred {}) = True
@@ -1177,7 +1177,7 @@ mkHoleError tidy_simples ctxt ct@(CHoleCan { cc_hole = hole })
   where
     occ       = holeOcc hole
     hole_ty   = ctEvPred (ctEvidence ct)
-    hole_kind = typeKind hole_ty
+    hole_kind = tcTypeKind hole_ty
     tyvars    = tyCoVarsOfTypeList hole_ty
 
     hole_msg = case hole of
@@ -1500,9 +1500,9 @@ mkEqErr1 ctxt ct   -- Wanted or derived;
                          || not (cty1 `pickyEqType` cty2)
                          -> hang (text "When matching" <+> sub_what)
                                2 (vcat [ ppr cty1 <+> dcolon <+>
-                                         ppr (typeKind cty1)
+                                         ppr (tcTypeKind cty1)
                                        , ppr cty2 <+> dcolon <+>
-                                         ppr (typeKind cty2) ])
+                                         ppr (tcTypeKind cty2) ])
                        _ -> text "When matching the kind of" <+> quotes (ppr cty1)
               msg2 = case sub_o of
                        TypeEqOrigin {}
@@ -1750,7 +1750,7 @@ mkTyVarEqErr' dflags ctxt report ct oriented tv1 co1 ty2
         -- Not an occurs check, because F is a type function.
   where
     Pair _ k1 = tcCoercionKind co1
-    k2        = typeKind ty2
+    k2        = tcTypeKind ty2
 
     ty1 = mkTyVarTy tv1
     occ_check_expand       = occCheckForErrors dflags tv1 ty2
@@ -2516,7 +2516,7 @@ mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_over
                , not (isTypeFamilyTyCon tc)
                = hang (text "GHC can't yet do polykinded")
                     2 (text "Typeable" <+>
-                       parens (ppr ty <+> dcolon <+> ppr (typeKind ty)))
+                       parens (ppr ty <+> dcolon <+> ppr (tcTypeKind ty)))
                | otherwise
                = empty
 
diff --git a/compiler/typecheck/TcHsType.hs b/compiler/typecheck/TcHsType.hs
index 5fb0d986d1..543862f109 100644
--- a/compiler/typecheck/TcHsType.hs
+++ b/compiler/typecheck/TcHsType.hs
@@ -1008,7 +1008,7 @@ checkExpectedKindX pp_hs_ty ty act_kind exp_kind
     -- We need to make sure that both kinds have the same number of implicit
     -- foralls out front. If the actual kind has more, instantiate accordingly.
     -- Otherwise, just pass the type & kind through: the errors are caught
-    -- in unifyType.  
+    -- in unifyType.
     match_invisibles ty act_kind
       = do { n_act_invis_bndrs <- invisibleTyBndrCountM act_kind
            ; if n_act_invis_bndrs == 0 then return (ty, act_kind)
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 7d3dd91fd1..50f1806a96 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -2522,4 +2522,4 @@ formatLevPolyErr ty
                , text "Kind:" <+> pprWithTYPE tidy_ki ])
   where
     (tidy_env, tidy_ty) = tidyOpenType emptyTidyEnv ty
-    tidy_ki             = tidyType tidy_env (typeKind ty)
+    tidy_ki             = tidyType tidy_env (tcTypeKind ty)
diff --git a/compiler/typecheck/TcRnDriver.hs b/compiler/typecheck/TcRnDriver.hs
index 8ed21f2d81..5c5bca8a26 100644
--- a/compiler/typecheck/TcRnDriver.hs
+++ b/compiler/typecheck/TcRnDriver.hs
@@ -2413,8 +2413,7 @@ tcRnType hsc_env normalise rdr_type
                         ; return ty' }
                 else return ty ;
 
-       ; kind' <- tcTypeKindM ty'
-       ; return (ty', mkInvForAllTys kvs kind') }
+       ; return (ty', mkInvForAllTys kvs kind) }
 
 {- Note [TcRnExprMode]
 ~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/typecheck/TcSplice.hs b/compiler/typecheck/TcSplice.hs
index 08b2992809..49829d76a4 100644
--- a/compiler/typecheck/TcSplice.hs
+++ b/compiler/typecheck/TcSplice.hs
@@ -1199,7 +1199,7 @@ reifyInstances th_nm th_tys
                 -- In particular, the type might have kind
                 -- variables inside it (Trac #7477)
 
-        ; traceTc "reifyInstances" (ppr ty $$ ppr (typeKind ty))
+        ; traceTc "reifyInstances" (ppr ty $$ ppr (tcTypeKind ty))
         ; case splitTyConApp_maybe ty of   -- This expands any type synonyms
             Just (tc, tys)                 -- See Trac #7910
                | Just cls <- tyConClass_maybe tc
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index 2bae076010..3567bfba59 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -2439,8 +2439,8 @@ rejigConRes tmpl_bndrs res_tmpl dc_inferred_tvs dc_specified_tvs res_ty
         -- So we return ( [a,b,z], [x,y]
         --              , [], [x,y,z]
         --              , [a~(x,y),b~z], <arg-subst> )
-  | Just subst <- ASSERT( isLiftedTypeKind (typeKind res_ty) )
-                  ASSERT( isLiftedTypeKind (typeKind res_tmpl) )
+  | Just subst <- ASSERT( isLiftedTypeKind (tcTypeKind res_ty) )
+                  ASSERT( isLiftedTypeKind (tcTypeKind res_tmpl) )
                   tcMatchTy res_tmpl res_ty
   = let (univ_tvs, raw_eqs, kind_subst) = mkGADTVars tmpl_tvs dc_tvs subst
         raw_ex_tvs = dc_tvs `minusList` univ_tvs
@@ -2960,8 +2960,8 @@ checkValidDataCon dflags existential_ok tc con
               orig_res_ty = dataConOrigResTy con
         ; traceTc "checkValidDataCon" (vcat
               [ ppr con, ppr tc, ppr tc_tvs
-              , ppr res_ty_tmpl <+> dcolon <+> ppr (typeKind res_ty_tmpl)
-              , ppr orig_res_ty <+> dcolon <+> ppr (typeKind orig_res_ty)])
+              , ppr res_ty_tmpl <+> dcolon <+> ppr (tcTypeKind res_ty_tmpl)
+              , ppr orig_res_ty <+> dcolon <+> ppr (tcTypeKind orig_res_ty)])
 
 
         ; checkTc (isJust (tcMatchTy res_ty_tmpl