Introduce tcTypeKind, and use it
authorSimon Peyton Jones <simonpj@microsoft.com>
Mon, 3 Dec 2018 11:30:22 +0000 (11:30 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Mon, 3 Dec 2018 13:42:40 +0000 (13:42 +0000)
In the type checker Constraint and * are distinct; and the function
that takes the kind of a type should respect that distinction
(Trac #15971).

This patch implements the change:

* Introduce Type.tcTypeKind, and use it throughout the type
  inference engine

* Add new Note [Kinding rules for types] for the kinding
  rules, especially for foralls.

* Redefine
    isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
  (it had a much more complicated definition before)

Some miscellaneous refactoring

* Get rid of TyCoRep.isTYPE, Kind.isTYPEApp,
  in favour of TyCoRep.kindRep, kindRep_maybe

* Rename Type.getRuntimeRepFromKind_maybe
  to getRuntimeRep_maybe

I did some spot-checks on compiler perf, and it really doesn't
budge (as expected).

27 files changed:
compiler/typecheck/ClsInst.hs
compiler/typecheck/FamInst.hs
compiler/typecheck/Inst.hs
compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcDeriv.hs
compiler/typecheck/TcDerivInfer.hs
compiler/typecheck/TcErrors.hs
compiler/typecheck/TcExpr.hs
compiler/typecheck/TcFlatten.hs
compiler/typecheck/TcHsSyn.hs
compiler/typecheck/TcHsType.hs
compiler/typecheck/TcInteract.hs
compiler/typecheck/TcMType.hs
compiler/typecheck/TcPat.hs
compiler/typecheck/TcPatSyn.hs
compiler/typecheck/TcRnDriver.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSimplify.hs
compiler/typecheck/TcSplice.hs
compiler/typecheck/TcTyClsDecls.hs
compiler/typecheck/TcType.hs
compiler/typecheck/TcTypeable.hs
compiler/typecheck/TcUnify.hs
compiler/typecheck/TcValidity.hs
compiler/types/Kind.hs
compiler/types/TyCoRep.hs
compiler/types/Type.hs

index c777c4b..1b6ab12 100644 (file)
@@ -459,7 +459,7 @@ doTyApp :: Class -> Type -> Type -> KindOrType -> TcM ClsInstResult
 --    (Typeable f, Typeable Int, Typeable Char)  --> (after some simp. steps)
 --    Typeable f
 doTyApp clas ty f tk
-  | isForAllTy (typeKind f)
+  | isForAllTy (tcTypeKind f)
   = return NoInstance -- We can't solve until we know the ctr.
   | otherwise
   = return $ OneInst { cir_new_theta = map (mk_typeable_pred clas) [f, tk]
@@ -472,7 +472,7 @@ doTyApp clas ty f tk
 
 -- Emit a `Typeable` constraint for the given type.
 mk_typeable_pred :: Class -> Type -> PredType
-mk_typeable_pred clas ty = mkClassPred clas [ typeKind ty, ty ]
+mk_typeable_pred clas ty = mkClassPred clas [ tcTypeKind ty, ty ]
 
   -- Typeable is implied by KnownNat/KnownSymbol. In the case of a type literal
   -- we generate a sub-goal for the appropriate class.
index 623d465..144b315 100644 (file)
@@ -187,8 +187,8 @@ newFamInst flavor axiom@(CoAxiom { co_ax_tc = fam_tc })
                          , fi_rhs      = rhs'
                          , fi_axiom    = axiom }) }
   where
-    lhs_kind = typeKind (mkTyConApp fam_tc lhs)
-    rhs_kind = typeKind rhs
+    lhs_kind = tcTypeKind (mkTyConApp fam_tc lhs)
+    rhs_kind = tcTypeKind rhs
     tcv_set  = mkVarSet (tvs ++ cvs)
     pp_ax    = pprCoAxiom axiom
     CoAxBranch { cab_tvs = tvs
index afc6370..284d6a9 100644 (file)
@@ -305,7 +305,7 @@ instTyVarsWith orig tvs tys
            ; go (extendTCvSubst subst tv (ty `mkCastTy` co)) tvs tys }
       where
         tv_kind = substTy subst (tyVarKind tv)
-        ty_kind = typeKind ty
+        ty_kind = tcTypeKind ty
 
     go _ _ _ = pprPanic "instTysWith" (ppr tvs $$ ppr tys)
 
@@ -581,15 +581,15 @@ mkHEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
 mkHEqBoxTy co ty1 ty2
   = return $
     mkTyConApp (promoteDataCon heqDataCon) [k1, k2, ty1, ty2, mkCoercionTy co]
-  where k1 = typeKind ty1
-        k2 = typeKind ty2
+  where k1 = tcTypeKind ty1
+        k2 = tcTypeKind ty2
 
 -- | This takes @a ~# b@ and returns @a ~ b@.
 mkEqBoxTy :: TcCoercion -> Type -> Type -> TcM Type
 mkEqBoxTy co ty1 ty2
   = return $
     mkTyConApp (promoteDataCon eqDataCon) [k, ty1, ty2, mkCoercionTy co]
-  where k = typeKind ty1
+  where k = tcTypeKind ty1
 
 {-
 ************************************************************************
index 46e5d82..dce9a10 100644 (file)
@@ -1319,8 +1319,8 @@ can_eq_app ev s1 t1 s2 t2
        ; canEqNC evar_s NomEq s1 s2 }
 
   where
-    s1k = typeKind s1
-    s2k = typeKind s2
+    s1k = tcTypeKind s1
+    s2k = tcTypeKind s2
 
     k1 `mismatches` k2
       =  isForAllTy k1 && not (isForAllTy k2)
@@ -1790,9 +1790,9 @@ canCFunEqCan ev fn tys fsk
                         vcat [ text "Kind co:" <+> ppr kind_co
                              , text "RHS:" <+> ppr fsk <+> dcolon <+> ppr (tyVarKind fsk)
                              , text "LHS:" <+> hang (ppr (mkTyConApp fn tys))
-                                                  2 (dcolon <+> ppr (typeKind (mkTyConApp fn tys)))
+                                                  2 (dcolon <+> ppr (tcTypeKind (mkTyConApp fn tys)))
                              , text "New LHS" <+> hang (ppr new_lhs)
-                                                     2 (dcolon <+> ppr (typeKind new_lhs)) ]
+                                                     2 (dcolon <+> ppr (tcTypeKind new_lhs)) ]
                       ; (ev', new_co, new_fsk)
                           <- newFlattenSkolem flav (ctEvLoc ev) fn tys'
                       ; let xi = mkTyVarTy new_fsk `mkCastTy` kind_co
@@ -1882,7 +1882,7 @@ canEqTyVar ev eq_rel swapped tv1 ps_ty1 xi2 ps_xi2
     xi1 = mkTyVarTy tv1
 
     k1 = tyVarKind tv1
-    k2 = typeKind xi2
+    k2 = tcTypeKind xi2
 
     loc  = ctEvLoc ev
     flav = ctEvFlavour ev
@@ -1936,7 +1936,7 @@ canEqTyVarHetero ev eq_rel tv1 co1 ki1 ps_tv1 xi2 ki2 ps_xi2
     loc  = ctev_loc ev
     role = eqRelRole eq_rel
 
--- guaranteed that typeKind lhs == typeKind rhs
+-- guaranteed that tcTypeKind lhs == tcTypeKind rhs
 canEqTyVarHomo :: CtEvidence
                -> EqRel -> SwapFlag
                -> TcTyVar                -- lhs: tv1
@@ -2288,7 +2288,7 @@ rewriteEqEvidence :: CtEvidence         -- Old evidence :: olhs ~ orhs (not swap
                                         --              or orhs ~ olhs (swapped)
                   -> SwapFlag
                   -> TcType -> TcType   -- New predicate  nlhs ~ nrhs
-                                        -- Should be zonked, because we use typeKind on nlhs/nrhs
+                                        -- Should be zonked, because we use tcTypeKind on nlhs/nrhs
                   -> TcCoercion         -- lhs_co, of type :: nlhs ~ olhs
                   -> TcCoercion         -- rhs_co, of type :: nrhs ~ orhs
                   -> TcS CtEvidence     -- Of type nlhs ~ nrhs
@@ -2364,7 +2364,7 @@ unifyWanted :: CtLoc -> Role
 -- See Note [unifyWanted and unifyDerived]
 -- The returned coercion's role matches the input parameter
 unifyWanted loc Phantom ty1 ty2
-  = do { kind_co <- unifyWanted loc Nominal (typeKind ty1) (typeKind ty2)
+  = do { kind_co <- unifyWanted loc Nominal (tcTypeKind ty1) (tcTypeKind ty2)
        ; return (mkPhantomCo kind_co ty1 ty2) }
 
 unifyWanted loc role orig_ty1 orig_ty2
index e2a314c..4bbb42d 100644 (file)
@@ -629,8 +629,8 @@ deriveStandalone (L loc (DerivDecl _ deriv_ty mbl_deriv_strat overlap_mode))
              -- Perform an additional unification with the kind of the `via`
              -- type and the result of the previous kind unification.
              Just (ViaStrategy via_ty) -> do
-               let via_kind     = typeKind via_ty
-                   inst_ty_kind = typeKind inst_ty'
+               let via_kind     = tcTypeKind via_ty
+                   inst_ty_kind = tcTypeKind inst_ty'
                    mb_match     = tcUnifyTy inst_ty_kind via_kind
 
                checkTc (isJust mb_match)
@@ -788,7 +788,7 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
                                 -- See Note [tc_args and tycon arity]
               (tc_args_to_keep, args_to_drop)
                               = splitAt n_args_to_keep tc_args
-              inst_ty_kind    = typeKind (mkTyConApp tc tc_args_to_keep)
+              inst_ty_kind    = tcTypeKind (mkTyConApp tc tc_args_to_keep)
 
               -- Match up the kinds, and apply the resulting kind substitution
               -- to the types.  See Note [Unify kinds in deriving]
@@ -828,9 +828,9 @@ deriveTyData tvs tc tc_args mb_deriv_strat deriv_pred
               -- type and the result of the previous kind unification.
               Just (ViaStrategy via_ty) -> do
                 let final_via_ty   = via_ty
-                    final_via_kind = typeKind final_via_ty
+                    final_via_kind = tcTypeKind final_via_ty
                     final_inst_ty_kind
-                              = typeKind (mkTyConApp tc final_tc_args')
+                              = tcTypeKind (mkTyConApp tc final_tc_args')
                     via_match = tcUnifyTy final_inst_ty_kind final_via_kind
 
                 checkTc (isJust via_match)
index b026f1d..ba45e09 100644 (file)
@@ -157,7 +157,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
            is_generic  = main_cls `hasKey` genClassKey
            is_generic1 = main_cls `hasKey` gen1ClassKey
            -- is_functor_like: see Note [Inferring the instance context]
-           is_functor_like = typeKind inst_ty `tcEqKind` typeToTypeKind
+           is_functor_like = tcTypeKind inst_ty `tcEqKind` typeToTypeKind
                           || is_generic1
 
            get_gen1_constraints :: Class -> CtOrigin -> TypeOrKind -> Type
@@ -191,7 +191,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
            -- message which points out the kind mismatch.
            -- See Note [Inferring the instance context]
            mk_functor_like_constraints orig t_or_k cls
-              = map $ \ty -> let ki = typeKind ty in
+              = map $ \ty -> let ki = tcTypeKind ty in
                              ( [ mk_cls_pred orig t_or_k cls ty
                                , mkPredOrigin orig KindLevel
                                    (mkPrimEqPred ki typeToTypeKind) ]
@@ -232,7 +232,7 @@ inferConstraintsDataConArgs inst_ty inst_tys
              where
                constrs
                  | main_cls `hasKey` dataClassKey
-                 , all (isLiftedTypeKind . typeKind) rep_tc_args
+                 , all (isLiftedTypeKind . tcTypeKind) rep_tc_args
                  = [ mk_cls_pred deriv_origin t_or_k main_cls ty
                    | (t_or_k, ty) <- zip t_or_ks rep_tc_args]
                  | otherwise
index cfd364f..df307f2 100644 (file)
@@ -38,7 +38,7 @@ import HsBinds ( PatSynBind(..) )
 import Name
 import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
                , mkRdrUnqual, isLocalGRE, greSrcSpan )
-import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey, tYPETyConKey )
+import PrelNames ( typeableClassName )
 import Id
 import Var
 import VarSet
@@ -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` tcTypeKind 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
@@ -1919,12 +1919,10 @@ misMatchMsg ct oriented ty1 ty2
   -- These next two cases are when we're about to report, e.g., that
   -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
   -- lifted vs. unlifted
-  | Just (tc1, []) <- splitTyConApp_maybe ty1
-  , tc1 `hasKey` liftedRepDataConKey
+  | isLiftedRuntimeRep ty1
   = lifted_vs_unlifted
 
-  | Just (tc2, []) <- splitTyConApp_maybe ty2
-  , tc2 `hasKey` liftedRepDataConKey
+  | isLiftedRuntimeRep ty2
   = lifted_vs_unlifted
 
   | otherwise  -- So now we have Nothing or (Just IsSwapped)
@@ -2060,14 +2058,13 @@ mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act
         kind_desc | tcIsConstraintKind exp = text "a constraint"
 
                     -- TYPE t0
-                  | Just (tc, [arg]) <- tcSplitTyConApp_maybe exp
-                  , tc `hasKey` tYPETyConKey
-                  , tcIsTyVarTy arg      = sdocWithDynFlags $ \dflags ->
-                                           if gopt Opt_PrintExplicitRuntimeReps dflags
-                                           then text "kind" <+> quotes (ppr exp)
-                                           else text "a type"
+                  | Just arg <- kindRep_maybe exp
+                  , tcIsTyVarTy arg = sdocWithDynFlags $ \dflags ->
+                                      if gopt Opt_PrintExplicitRuntimeReps dflags
+                                      then text "kind" <+> quotes (ppr exp)
+                                      else text "a type"
 
-                  | otherwise            = text "kind" <+> quotes (ppr exp)
+                  | otherwise       = text "kind" <+> quotes (ppr exp)
 
     num_args_msg = case level of
       KindLevel
@@ -2520,7 +2517,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
 
index 9eaead5..8afcc8b 100644 (file)
@@ -388,7 +388,7 @@ tcExpr expr@(OpApp fix arg1 op arg2) res_ty
        -- The *result* type can have any kind (Trac #8739),
        -- so we don't need to check anything for that
        ; _ <- unifyKind (Just (XHsType $ NHsCoreTy arg2_sigma))
-                        (typeKind arg2_sigma) liftedTypeKind
+                        (tcTypeKind arg2_sigma) liftedTypeKind
            -- ignore the evidence. arg2_sigma must have type * or #,
            -- because we know arg2_sigma -> or_res_ty is well-kinded
            -- (because otherwise matchActualFunTys would fail)
@@ -1347,7 +1347,7 @@ tcArgs fun orig_fun_ty fun_orig orig_args herald
                                       --     substitution is kind-respecting
                     ; traceTc "VTA" (vcat [ppr tv, debugPprType kind
                                           , debugPprType ty_arg
-                                          , debugPprType (typeKind ty_arg)
+                                          , debugPprType (tcTypeKind ty_arg)
                                           , debugPprType inner_ty
                                           , debugPprType insted_ty ])
 
index add0a6f..b3c41a5 100644 (file)
@@ -771,7 +771,7 @@ flattenArgsNom :: CtEvidence -> TyCon -> [TcType] -> TcS ([Xi], [TcCoercion], Tc
 --      ctEvFlavour ev = Nominal
 -- and we want to flatten all at nominal role
 -- The kind passed in is the kind of the type family or class, call it T
--- The last coercion returned has type (typeKind(T xis) ~N typeKind(T tys))
+-- The last coercion returned has type (tcTypeKind(T xis) ~N tcTypeKind(T tys))
 --
 -- For Derived constraints the returned coercion may be undefined
 -- because flattening may use a Derived equality ([D] a ~ ty)
@@ -800,8 +800,8 @@ flattenArgsNom ev tc tys
 
 Key invariants:
   (F0) co :: xi ~ zonk(ty)
-  (F1) typeKind(xi) succeeds and returns a fully zonked kind
-  (F2) typeKind(xi) `eqType` zonk(typeKind(ty))
+  (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
+  (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
 
 Note that it is flatten's job to flatten *every type function it sees*.
 flatten is only called on *arguments* to type functions, by canEqGiven.
@@ -814,7 +814,7 @@ Because flattening zonks and the returned coercion ("co" above) is also
 zonked, it's possible that (co :: xi ~ ty) isn't quite true. So, instead,
 we can rely on this fact:
 
-  (F1) typeKind(xi) succeeds and returns a fully zonked kind
+  (F1) tcTypeKind(xi) succeeds and returns a fully zonked kind
 
 Note that the left-hand type of co is *always* precisely xi. The right-hand
 type may or may not be ty, however: if ty has unzonked filled-in metavariables,
@@ -824,14 +824,14 @@ occasionally have to explicitly zonk, when (co :: xi ~ ty) is important
 even before we zonk the whole program. For example, see the FTRNotFollowed
 case in flattenTyVar.
 
-Why have these invariants on flattening? Because we sometimes use typeKind
+Why have these invariants on flattening? Because we sometimes use tcTypeKind
 during canonicalisation, and we want this kind to be zonked (e.g., see
 TcCanonical.canEqTyVar).
 
 Flattening is always homogeneous. That is, the kind of the result of flattening is
 always the same as the kind of the input, modulo zonking. More formally:
 
-  (F2) typeKind(xi) `eqType` zonk(typeKind(ty))
+  (F2) tcTypeKind(xi) `eqType` zonk(tcTypeKind(ty))
 
 This invariant means that the kind of a flattened type might not itself be flat.
 
@@ -1162,7 +1162,7 @@ flatten_args :: [TyCoBinder] -> Bool -- Binders, and True iff any of them are
              -> [Role] -> [Type]     -- these are in 1-to-1 correspondence
              -> FlatM ([Xi], [Coercion], CoercionN)
 -- Coercions :: Xi ~ Type, at roles given
--- Third coercion :: typeKind(fun xis) ~N typeKind(fun tys)
+-- Third coercion :: tcTypeKind(fun xis) ~N tcTypeKind(fun tys)
 -- That is, the third coercion relates the kind of some function (whose kind is
 -- passed as the first parameter) instantiated at xis to the kind of that
 -- function instantiated at the tys. This is useful in keeping flattening
@@ -1294,7 +1294,7 @@ flatten_args_slow orig_binders orig_inner_ki orig_fvs orig_roles orig_tys
                                       ; return (ty, mkReflCo Phantom ty) }
 
              -- By Note [Flattening] invariant (F2),
-             -- typeKind(xi) = typeKind(ty). But, it's possible that xi will be
+             -- tcTypeKind(xi) = tcTypeKind(ty). But, it's possible that xi will be
              -- used as an argument to a function whose kind is different, if
              -- earlier arguments have been flattened to new types. We thus
              -- need a coercion (kind_co :: old_kind ~ new_kind).
@@ -1475,7 +1475,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys
              do { let tc_roles  = tyConRolesRepresentational tc
                       arg_roles = dropList xis tc_roles
                 ; (arg_xis, arg_cos, kind_co)
-                    <- flatten_vector (typeKind fun_xi) arg_roles arg_tys
+                    <- flatten_vector (tcTypeKind fun_xi) arg_roles arg_tys
 
                   -- Here, we have fun_co :: T xi1 xi2 ~ ty
                   -- and we need to apply fun_co to the arg_cos. The problem is
@@ -1494,7 +1494,7 @@ flatten_app_ty_args fun_xi fun_co arg_tys
                 ; return (app_xi, app_co, kind_co) }
            Nothing ->
              do { (arg_xis, arg_cos, kind_co)
-                    <- flatten_vector (typeKind fun_xi) (repeat Nominal) arg_tys
+                    <- flatten_vector (tcTypeKind fun_xi) (repeat Nominal) arg_tys
                 ; let arg_xi = mkAppTys fun_xi arg_xis
                       arg_co = mkAppCos fun_co arg_cos
                 ; return (arg_xi, arg_co, kind_co) }
@@ -1514,7 +1514,7 @@ flatten_ty_con_app tc tys
 homogenise_result :: Xi              -- a flattened type
                   -> Coercion        -- :: xi ~r original ty
                   -> Role            -- r
-                  -> CoercionN       -- kind_co :: typeKind(xi) ~N typeKind(ty)
+                  -> CoercionN       -- kind_co :: tcTypeKind(xi) ~N tcTypeKind(ty)
                   -> (Xi, Coercion)  -- (xi |> kind_co, (xi |> kind_co)
                                      --   ~r original ty)
 homogenise_result xi co r kind_co
@@ -1624,9 +1624,9 @@ flatten_fam_app tc tys  -- Can be over-saturated
 flatten_exact_fam_app_fully :: TyCon -> [TcType] -> FlatM (Xi, Coercion)
 flatten_exact_fam_app_fully tc tys
   -- See Note [Reduce type family applications eagerly]
-     -- the following typeKind should never be evaluated, as it's just used in
+     -- the following tcTypeKind should never be evaluated, as it's just used in
      -- casting, and casts by refl are dropped
-  = do { let reduce_co = mkNomReflCo (typeKind (mkTyConApp tc tys))
+  = do { let reduce_co = mkNomReflCo (tcTypeKind (mkTyConApp tc tys))
        ; mOut <- try_to_reduce_nocache tc tys reduce_co id
        ; case mOut of
            Just out -> pure out
@@ -1636,7 +1636,7 @@ flatten_exact_fam_app_fully tc tys
                    <- setEqRel NomEq $  -- just do this once, instead of for
                                         -- each arg
                       flatten_args_tc tc (repeat Nominal) tys
-                      -- kind_co :: typeKind(F xis) ~N typeKind(F tys)
+                      -- kind_co :: tcTypeKind(F xis) ~N tcTypeKind(F tys)
                ; eq_rel   <- getEqRel
                ; cur_flav <- getFlavour
                ; let role   = eqRelRole eq_rel
@@ -1711,8 +1711,8 @@ flatten_exact_fam_app_fully tc tys
 
     try_to_reduce :: TyCon   -- F, family tycon
                   -> [Type]  -- args, not necessarily flattened
-                  -> CoercionN -- kind_co :: typeKind(F args) ~N
-                               --            typeKind(F orig_args)
+                  -> CoercionN -- kind_co :: tcTypeKind(F args) ~N
+                               --            tcTypeKind(F orig_args)
                                -- where
                                -- orig_args is what was passed to the outer
                                -- function
@@ -1749,8 +1749,8 @@ flatten_exact_fam_app_fully tc tys
 
     try_to_reduce_nocache :: TyCon   -- F, family tycon
                           -> [Type]  -- args, not necessarily flattened
-                          -> CoercionN -- kind_co :: typeKind(F args)
-                                       --            ~N typeKind(F orig_args)
+                          -> CoercionN -- kind_co :: tcTypeKind(F args)
+                                       --            ~N tcTypeKind(F orig_args)
                                        -- where
                                        -- orig_args is what was passed to the
                                        -- outer function
@@ -2060,7 +2060,7 @@ unflattenWanteds tv_eqs funeqs
                         -- NB: unlike unflattenFmv, filling a fmv here /does/
                         --     bump the unification count; it is "improvement"
                         -- Note [Unflattening can force the solver to iterate]
-      = ASSERT2( tyVarKind tv `eqType` typeKind rhs, ppr ct )
+      = ASSERT2( tyVarKind tv `eqType` tcTypeKind rhs, ppr ct )
            -- CTyEqCan invariant should ensure this is true
         do { is_filled <- isFilledMetaTyVar tv
            ; elim <- case is_filled of
index 16cee70..6834af9 100644 (file)
@@ -1039,7 +1039,7 @@ zonk_cmd_top env (HsCmdTop (CmdTopTc stack_tys ty ids) cmd)
        new_ty <- zonkTcTypeToTypeX env ty
        new_ids <- mapSndM (zonkExpr env) ids
 
-       MASSERT( isLiftedTypeKind (typeKind new_stack_tys) )
+       MASSERT( isLiftedTypeKind (tcTypeKind new_stack_tys) )
          -- desugarer assumes that this is not levity polymorphic...
          -- but indeed it should always be lifted due to the typing
          -- rules for arrows
index 4a4d49b..3b36281 100644 (file)
@@ -507,7 +507,7 @@ missing any patterns.
 Note [The tcType invariant]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 (IT1) If    tc_ty = tc_hs_type hs_ty exp_kind
-      then  typeKind tc_ty = exp_kind
+      then  tcTypeKind tc_ty = exp_kind
 without any zonking needed.  The reason for this is that in
 tcInferApps we see (F ty), and we kind-check 'ty' with an
 expected-kind coming from F.  Then, to make the resulting application
@@ -520,17 +520,17 @@ The tcType invariant also applies to checkExpectedKind:
 (IT2) if
         (tc_ty, _, _) = checkExpectedKind ty act_ki exp_ki
       then
-        typeKind tc_ty = exp_ki
+        tcTypeKind tc_ty = exp_ki
 
 These other invariants are all necessary, too, as these functions
 are used within tc_hs_type:
 
-(IT3) If (ty, ki) <- tc_infer_hs_type ..., then typeKind ty == ki.
+(IT3) If (ty, ki) <- tc_infer_hs_type ..., then tcTypeKind ty == ki.
 
 (IT4) If (ty, ki) <- tc_infer_hs_type ..., then zonk ki == ki.
       (In other words, the result kind of tc_infer_hs_type is zonked.)
 
-(IT5) If (ty, ki) <- tcTyVar ..., then typeKind ty == ki.
+(IT5) If (ty, ki) <- tcTyVar ..., then tcTypeKind ty == ki.
 
 (IT6) If (ty, ki) <- tcTyVar ..., then zonk ki == ki.
       (In other words, the result kind of tcTyVar is zonked.)
@@ -587,7 +587,7 @@ tc_infer_hs_type mode (HsSpliceTy _ (HsSpliced _ _ (HsSplicedTy ty)))
 tc_infer_hs_type mode (HsDocTy _ ty _) = tc_infer_lhs_type mode ty
 tc_infer_hs_type _    (XHsType (NHsCoreTy ty))
   = do { ty <- zonkTcType ty  -- (IT3) and (IT4) of Note [The tcType invariant]
-       ; return (ty, typeKind ty) }
+       ; return (ty, tcTypeKind ty) }
 tc_infer_hs_type mode other_ty
   = do { kv <- newMetaKindVar
        ; ty' <- tc_hs_type mode other_ty kv
@@ -745,7 +745,7 @@ tc_hs_type mode rn_ty@(HsSumTy _ hs_tys) exp_kind
   = do { let arity = length hs_tys
        ; arg_kinds <- mapM (\_ -> newOpenTypeKind) hs_tys
        ; tau_tys   <- zipWithM (tc_lhs_type mode) hs_tys arg_kinds
-       ; let arg_reps = map getRuntimeRepFromKind arg_kinds
+       ; let arg_reps = map kindRep arg_kinds
              arg_tys  = arg_reps ++ tau_tys
        ; checkExpectedKind rn_ty
                            (mkTyConApp (sumTyCon arity) arg_tys)
@@ -872,7 +872,7 @@ finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind
        ; checkExpectedKind rn_ty (mkTyConApp tycon arg_tys) res_kind exp_kind }
   where
     arity = length tau_tys
-    tau_reps = map getRuntimeRepFromKind tau_kinds
+    tau_reps = map kindRep tau_kinds
     res_kind = case tup_sort of
                  UnboxedTuple    -> unboxedTupleKind tau_reps
                  BoxedTuple      -> liftedTypeKind
@@ -897,7 +897,7 @@ tcInferApps :: TcTyMode
             -> TcKind               -- ^ Function kind (zonked)
             -> [LHsType GhcRn]      -- ^ Args
             -> TcM (TcType, TcKind) -- ^ (f args, args, result kind)
--- Precondition: typeKind fun_ty = fun_ki
+-- Precondition: tcTypeKind fun_ty = fun_ki
 --    Reason: we will return a type application like (fun_ty arg1 ... argn),
 --            and that type must be well-kinded
 --            See Note [The tcType invariant]
@@ -1079,7 +1079,7 @@ tcTyVar mode name         -- Could be a tyvar, a tycon, or a datacon
                           -- want to zonk the kind, leaving the TyVar
                           -- un-zonked  (Trac #14873)
                           do { ty <- zonkTcTyVar tv
-                             ; return (ty, typeKind ty) }
+                             ; return (ty, tcTypeKind ty) }
 
            ATcTyCon tc_tc -> do { -- See Note [GADT kind self-reference]
                                   unless
index 0833b33..277e324 100644 (file)
@@ -1634,8 +1634,8 @@ solveByUnification wd tv xi
        ; traceTcS "Sneaky unification:" $
                        vcat [text "Unifies:" <+> ppr tv <+> text ":=" <+> ppr xi,
                              text "Coercion:" <+> pprEq tv_ty xi,
-                             text "Left Kind is:" <+> ppr (typeKind tv_ty),
-                             text "Right Kind is:" <+> ppr (typeKind xi) ]
+                             text "Left Kind is:" <+> ppr (tcTypeKind tv_ty),
+                             text "Right Kind is:" <+> ppr (tcTypeKind xi) ]
 
        ; unifyTyVar tv xi
        ; setEvBindIfWanted wd (evCoercion (mkTcNomReflCo xi)) }
index 3500b72..1516480 100644 (file)
@@ -684,7 +684,7 @@ newFskTyVar fam_ty
                               , mtv_ref   = ref
                               , mtv_tclvl = tclvl }
              name = mkMetaTyVarName uniq (fsLit "fsk")
-       ; return (mkTcTyVar name (typeKind fam_ty) details) }
+       ; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
 
 newFmvTyVar :: TcType -> TcM TcTyVar
 -- Very like newMetaTyVar, except sets mtv_tclvl to one less
@@ -697,7 +697,7 @@ newFmvTyVar fam_ty
                               , mtv_ref   = ref
                               , mtv_tclvl = tclvl }
              name = mkMetaTyVarName uniq (fsLit "s")
-       ; return (mkTcTyVar name (typeKind fam_ty) details) }
+       ; return (mkTcTyVar name (tcTypeKind fam_ty) details) }
 
 newMetaDetails :: MetaInfo -> TcM TcTyVarDetails
 newMetaDetails info
@@ -785,8 +785,8 @@ writeMetaTyVarRef tyvar ref ty
        -- Zonk kinds to allow the error check to work
        ; zonked_tv_kind <- zonkTcType tv_kind
        ; zonked_ty      <- zonkTcType ty
-       ; let zonked_ty_kind = typeKind zonked_ty  -- need to zonk even before typeKind;
-                                                  -- otherwise, we can panic in piResultTy
+       ; 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
                           || tcEqKind zonked_ty_kind zonked_tv_kind
              -- Hack alert! tcIsConstraintKind: see TcHsType
@@ -2190,4 +2190,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)
index 19ec6de..ba3603f 100644 (file)
@@ -351,7 +351,7 @@ tc_pat penv (LazyPat x pat) pat_ty thing_inside
 
         -- Check that the expected pattern type is itself lifted
         ; pat_ty <- readExpType pat_ty
-        ; _ <- unifyType Nothing (typeKind pat_ty) liftedTypeKind
+        ; _ <- unifyType Nothing (tcTypeKind pat_ty) liftedTypeKind
 
         ; return (LazyPat x pat', res) }
 
index 4942a8b..ea1f483 100644 (file)
@@ -193,8 +193,8 @@ mkProvEvidence :: EvId -> Maybe (PredType, EvTerm)
 -- See Note [Equality evidence in pattern synonyms]
 mkProvEvidence ev_id
   | EqPred r ty1 ty2 <- classifyPredType pred
-  , let k1 = typeKind ty1
-        k2 = typeKind ty2
+  , let k1 = tcTypeKind ty1
+        k2 = tcTypeKind ty2
         is_homo = k1 `tcEqType` k2
         homo_tys   = [k1, ty1, ty2]
         hetero_tys = [k1, k2, ty1, ty2]
index 2250f72..b13ae21 100644 (file)
@@ -2415,7 +2415,7 @@ tcRnType hsc_env normalise rdr_type
                         ; return ty' }
                 else return ty ;
 
-       ; return (ty', mkInvForAllTys kvs (typeKind ty')) }
+       ; return (ty', mkInvForAllTys kvs (tcTypeKind ty')) }
 
 {- Note [TcRnExprMode]
 ~~~~~~~~~~~~~~~~~~~~~~
index ad3122b..205a2bd 100644 (file)
@@ -1700,7 +1700,7 @@ data Ct
        --   * tv not in tvs(rhs)   (occurs check)
        --   * If tv is a TauTv, then rhs has no foralls
        --       (this avoids substituting a forall for the tyvar in other types)
-       --   * typeKind ty `tcEqKind` typeKind tv; Note [Ct kind invariant]
+       --   * tcTypeKind ty `tcEqKind` tcTypeKind tv; Note [Ct kind invariant]
        --   * rhs may have at most one top-level cast
        --   * rhs (perhaps under the one cast) is not necessarily function-free,
        --       but it has no top-level function.
@@ -1723,7 +1723,7 @@ data Ct
   | CFunEqCan {  -- F xis ~ fsk
        -- Invariants:
        --   * isTypeFamilyTyCon cc_fun
-       --   * typeKind (F xis) = tyVarKind fsk; Note [Ct kind invariant]
+       --   * tcTypeKind (F xis) = tyVarKind fsk; Note [Ct kind invariant]
        --   * always Nominal role
       cc_ev     :: CtEvidence,  -- See Note [Ct/evidence invariant]
       cc_fun    :: TyCon,       -- A type function
index ac283fa..4e8fe3b 100644 (file)
@@ -2121,7 +2121,7 @@ to ensure that instance declarations match.  For example consider
      foo x = show (\_ -> True)
 
 Then we'll get a constraint (Show (p ->q)) where p has kind (TYPE r),
-and that won't match the typeKind (*) in the instance decl.  See tests
+and that won't match the tcTypeKind (*) in the instance decl.  See tests
 tc217 and tc175.
 
 We look only at touchable type variables. No further constraints
@@ -2335,7 +2335,7 @@ floatEqualities skols given_ids ev_binds_var no_given_eqs
     is_float_eq_candidate ct
       | pred <- ctPred ct
       , EqPred NomEq ty1 ty2 <- classifyPredType pred
-      , typeKind ty1 `tcEqType` typeKind ty2
+      , tcTypeKind ty1 `tcEqType` tcTypeKind ty2
       = case (tcGetTyVar_maybe ty1, tcGetTyVar_maybe ty2) of
           (Just tv1, _) -> float_tv_eq_candidate tv1 ty2
           (_, Just tv2) -> float_tv_eq_candidate tv2 ty1
index d3e1464..7e34dae 100644 (file)
@@ -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
@@ -1639,7 +1639,7 @@ annotThType :: Bool   -- True <=> annotate
 annotThType _    _  th_ty@(TH.SigT {}) = return th_ty
 annotThType True ty th_ty
   | not $ isEmptyVarSet $ filterVarSet isTyVar $ tyCoVarsOfType ty
-  = do { let ki = typeKind ty
+  = do { let ki = tcTypeKind ty
        ; th_ki <- reifyKind ki
        ; return (TH.SigT th_ty th_ki) }
 annotThType _    _ th_ty = return th_ty
@@ -1944,7 +1944,7 @@ reify_tc_app tc tys
     -- See Note [Kind annotations on TyConApps]
     maybe_sig_t th_type
       | needs_kind_sig
-      = do { let full_kind = typeKind (mkTyConApp tc tys)
+      = do { let full_kind = tcTypeKind (mkTyConApp tc tys)
            ; th_full_kind <- reifyKind full_kind
            ; return (TH.SigT th_type th_full_kind) }
       | otherwise
index c097d50..eda86f9 100644 (file)
@@ -2441,8 +2441,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
@@ -2962,8 +2962,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
index df1ec91..90d4408 100644 (file)
@@ -122,7 +122,7 @@ module TcType (
 
   --------------------------------
   -- Rexported from Kind
-  Kind, typeKind,
+  Kind, typeKind, tcTypeKind,
   liftedTypeKind,
   constraintKind,
   isLiftedTypeKind, isUnliftedTypeKind, classifiesTypeWithValues,
@@ -1296,7 +1296,7 @@ See also Note [The tcType invariant] in TcHsType.
 
 During type inference, we maintain this invariant
 
-   (INV-TK): it is legal to call 'typeKind' on any Type ty,
+   (INV-TK): it is legal to call 'tcTypeKind' on any Type ty,
              /without/ zonking ty
 
 For example, suppose
@@ -1306,12 +1306,12 @@ For example, suppose
     a :: kappa
 then consider the type
     (a Int)
-If we call typeKind on that, we'll crash, because the (un-zonked)
+If we call tcTypeKind on that, we'll crash, because the (un-zonked)
 kind of 'a' is just kappa, not an arrow kind.  If we zonk first
 we'd be fine, but that is too tiresome, so instead we maintain
 (INV-TK).  So we do not form (a Int); instead we form
     (a |> co) Int
-and typeKind has no problem with that.
+and tcTypeKind has no problem with that.
 
 Bottom line: we want to keep that 'co' /even though it is Refl/.
 
@@ -1563,7 +1563,7 @@ tcSplitFunTy_maybe :: Type -> Maybe (Type, Type)
 tcSplitFunTy_maybe ty | Just ty' <- tcView ty         = tcSplitFunTy_maybe ty'
 tcSplitFunTy_maybe (FunTy arg res) | not (isPredTy arg) = Just (arg, res)
 tcSplitFunTy_maybe _                                    = Nothing
-        -- Note the typeKind guard
+        -- Note the tcTypeKind guard
         -- Consider     (?x::Int) => Bool
         -- We don't want to treat this as a function type!
         -- A concrete example is test tc230:
@@ -1714,8 +1714,8 @@ tcEqType ty1 ty2
   = isNothing (tc_eq_type tcView ki1 ki2) &&
     isNothing (tc_eq_type tcView ty1 ty2)
   where
-    ki1 = typeKind ty1
-    ki2 = typeKind ty2
+    ki1 = tcTypeKind ty1
+    ki2 = tcTypeKind ty2
 
 -- | Just like 'tcEqType', but will return True for types of different kinds
 -- as long as their non-coercion structure is identical.
@@ -1732,8 +1732,8 @@ tcEqTypeVis :: TcType -> TcType -> Maybe Bool
 tcEqTypeVis ty1 ty2
   = tc_eq_type tcView ty1 ty2 <!> invis (tc_eq_type tcView ki1 ki2)
   where
-    ki1 = typeKind ty1
-    ki2 = typeKind ty2
+    ki1 = tcTypeKind ty1
+    ki2 = tcTypeKind ty2
 
       -- convert Just True to Just False
     invis :: Maybe Bool -> Maybe Bool
@@ -1970,8 +1970,8 @@ boxEqPred eq_rel ty1 ty2
                                     --       so we can't abstract over it
                                     -- Nothing fundamental: we could add it
  where
-   k1 = typeKind ty1
-   k2 = typeKind ty2
+   k1 = tcTypeKind ty1
+   k2 = tcTypeKind ty2
    homo_kind = k1 `tcEqType` k2
 
 pickCapturedPreds
index 90a4a83..1fe2c68 100644 (file)
@@ -28,7 +28,6 @@ import TysWiredIn ( tupleTyCon, sumTyCon, runtimeRepTyCon
 import Name
 import Id
 import Type
-import Kind ( isTYPEApp )
 import TyCon
 import DataCon
 import Module
@@ -430,7 +429,7 @@ typeIsTypeable :: Type -> Bool
 typeIsTypeable ty
   | Just ty' <- coreView ty         = typeIsTypeable ty'
 typeIsTypeable ty
-  | Just _ <- isTYPEApp ty          = True
+  | isJust (kindRep_maybe ty)       = True
 typeIsTypeable (TyVarTy _)          = True
 typeIsTypeable (AppTy a b)          = typeIsTypeable a && typeIsTypeable b
 typeIsTypeable (FunTy a b)          = typeIsTypeable a && typeIsTypeable b
@@ -549,11 +548,15 @@ mkKindRepRhs :: TypeableStuff
 mkKindRepRhs stuff@(Stuff {..}) in_scope = new_kind_rep
   where
     new_kind_rep k
-        -- We handle TYPE separately to make it clear to consumers
-        -- (e.g. serializers) that there is a loop here (as
-        -- TYPE :: RuntimeRep -> TYPE 'LiftedRep)
-      | Just rr <- isTYPEApp k
-      = return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon rr
+        -- We handle (TYPE LiftedRep) etc separately to make it
+        -- clear to consumers (e.g. serializers) that there is
+        -- a loop here (as TYPE :: RuntimeRep -> TYPE 'LiftedRep)
+      | not (tcIsConstraintKind k)    -- Typeable respects the Constraint/* distinction
+                                      -- so do not follow the special case here
+      , Just arg <- kindRep_maybe k
+      , Just (tc, []) <- splitTyConApp_maybe arg
+      , Just dc <- isPromotedDataCon_maybe tc
+      = return $ nlHsDataCon kindRepTYPEDataCon `nlHsApp` nlHsDataCon dc
 
     new_kind_rep (TyVarTy v)
       | Just idx <- lookupCME in_scope v
index fd661c9..f51c724 100644 (file)
@@ -440,7 +440,7 @@ matchExpectedAppTy orig_ty
            ; co <- unifyType Nothing (mkAppTy ty1 ty2) orig_ty
            ; return (co, (ty1, ty2)) }
 
-    orig_kind = typeKind orig_ty
+    orig_kind = tcTypeKind orig_ty
     kind1 = mkFunTy liftedTypeKind orig_kind
     kind2 = liftedTypeKind    -- m :: * -> k
                               -- arg type :: *
@@ -911,7 +911,7 @@ fill_infer_result orig_ty (IR { ir_uniq = u, ir_lvl = res_lvl
       = do { let ty_lvl = tcTypeLevel ty
            ; MASSERT2( not (ty_lvl `strictlyDeeperThan` res_lvl),
                        ppr u $$ ppr res_lvl $$ ppr ty_lvl $$
-                       ppr ty <+> dcolon <+> ppr (typeKind ty) $$ ppr orig_ty )
+                       ppr ty <+> dcolon <+> ppr (tcTypeKind ty) $$ ppr orig_ty )
            ; cts <- readTcRef ref
            ; case cts of
                Just already_there -> pprPanic "writeExpType"
@@ -993,12 +993,12 @@ promoteTcType dest_lvl ty
     dont_promote_it :: TcM (TcCoercion, TcType)
     dont_promote_it  -- Check that ty :: TYPE rr, for some (fresh) rr
       = do { res_kind <- newOpenTypeKind
-           ; let ty_kind = typeKind ty
+           ; let ty_kind = tcTypeKind ty
                  kind_orig = TypeEqOrigin { uo_actual   = ty_kind
                                           , uo_expected = res_kind
                                           , uo_thing    = Nothing
                                           , uo_visible  = False }
-           ; ki_co <- uType KindLevel kind_orig (typeKind ty) res_kind
+           ; ki_co <- uType KindLevel kind_orig (tcTypeKind ty) res_kind
            ; let co = mkTcGReflRightCo Nominal ty ki_co
            ; return (co, ty `mkCastTy` ki_co) }
 
@@ -1639,10 +1639,10 @@ uUnfilledVar2 origin t_or_k swapped tv1 ty2
     go dflags cur_lvl
       | canSolveByUnification cur_lvl tv1 ty2
       , Just ty2' <- metaTyVarUpdateOK dflags tv1 ty2
-      = do { co_k <- uType KindLevel kind_origin (typeKind ty2') (tyVarKind tv1)
+      = do { co_k <- uType KindLevel kind_origin (tcTypeKind ty2') (tyVarKind tv1)
            ; traceTc "uUnfilledVar2 ok" $
              vcat [ ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1)
-                  , ppr ty2 <+> dcolon <+> ppr (typeKind  ty2)
+                  , ppr ty2 <+> dcolon <+> ppr (tcTypeKind  ty2)
                   , ppr (isTcReflCo co_k), ppr co_k ]
 
            ; if isTcReflCo co_k  -- only proceed if the kinds matched.
index a3f4e2f..f82e394 100644 (file)
@@ -319,7 +319,7 @@ checkValidType :: UserTypeCtxt -> Type -> TcM ()
 -- Assumes argument is fully zonked
 -- Not used for instance decls; checkValidInstance instead
 checkValidType ctxt ty
-  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (typeKind ty))
+  = do { traceTc "checkValidType" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty))
        ; rankn_flag  <- xoptM LangExt.RankNTypes
        ; impred_flag <- xoptM LangExt.ImpredicativeTypes
        ; let gen_rank :: Rank -> Rank
@@ -382,7 +382,7 @@ checkValidType ctxt ty
        --     and there may be nested foralls for the subtype test to examine
        ; checkAmbiguity ctxt ty
 
-       ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (typeKind ty)) }
+       ; traceTc "checkValidType done" (ppr ty <+> text "::" <+> ppr (tcTypeKind ty)) }
 
 checkValidMonoType :: Type -> TcM ()
 -- Assumes argument is fully zonked
@@ -403,7 +403,7 @@ checkTySynRhs ctxt ty
   | otherwise
   = return ()
   where
-    actual_kind = typeKind ty
+    actual_kind = tcTypeKind ty
 
 {-
 Note [Higher rank types]
@@ -506,7 +506,7 @@ check_type env ctxt rank ty
     tvs          = binderVars tvbs
     (env', _)    = tidyVarBndrs env tvs
 
-    tau_kind              = typeKind tau
+    tau_kind              = tcTypeKind tau
     phi_kind | null theta = tau_kind
              | otherwise  = liftedTypeKind
         -- If there are any constraints, the kind is *. (#11405)
index f88bbe1..17c8041 100644 (file)
@@ -7,7 +7,6 @@ module Kind (
 
         -- ** Predicates on Kinds
         isLiftedTypeKind, isUnliftedTypeKind,
-        isTYPEApp,
         isConstraintKindCon,
 
         classifiesTypeWithValues,
@@ -18,9 +17,7 @@ module Kind (
 
 import GhcPrelude
 
-import {-# SOURCE #-} Type    ( coreView
-                              , splitTyConApp_maybe )
-import {-# SOURCE #-} DataCon ( DataCon )
+import {-# SOURCE #-} Type    ( coreView )
 
 import TyCoRep
 import TyCon
@@ -28,6 +25,7 @@ import PrelNames
 
 import Outputable
 import Util
+import Data.Maybe( isJust )
 
 {-
 ************************************************************************
@@ -64,15 +62,6 @@ during type inference.
 isConstraintKindCon :: TyCon -> Bool
 isConstraintKindCon tc = tyConUnique tc == constraintKindTyConKey
 
-isTYPEApp :: Kind -> Maybe DataCon
-isTYPEApp (TyConApp tc args)
-  | tc `hasKey` tYPETyConKey
-  , [arg] <- args
-  , Just (tc, []) <- splitTyConApp_maybe arg
-  , Just dc <- isPromotedDataCon_maybe tc
-  = Just dc
-isTYPEApp _ = Nothing
-
 -- | Tests whether the given kind (which should look like @TYPE x@)
 -- is something other than a constructor tree (that is, constructors at every node).
 -- E.g.  True of   TYPE k, TYPE (F Int)
@@ -92,12 +81,7 @@ isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
     go CastTy{}          = True
     go CoercionTy{}      = True
 
-    _is_type
-      | TyConApp typ [_] <- k
-      = typ `hasKey` tYPETyConKey
-      | otherwise
-      = False
-
+    _is_type = classifiesTypeWithValues k
 
 -----------------------------------------
 --              Subkinding
@@ -110,4 +94,4 @@ isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
 -- like *, #, TYPE Lifted, TYPE v, Constraint.
 classifiesTypeWithValues :: Kind -> Bool
 -- ^ True of any sub-kind of OpenTypeKind
-classifiesTypeWithValues = isTYPE (const True)
+classifiesTypeWithValues k = isJust (kindRep_maybe k)
index db82deb..c7592c5 100644 (file)
@@ -44,8 +44,10 @@ module TyCoRep (
         mkForAllTy,
         mkTyCoPiTy, mkTyCoPiTys,
         mkPiTys,
-        isTYPE,
+
+        kindRep_maybe, kindRep,
         isLiftedTypeKind, isUnliftedTypeKind,
+        isLiftedRuntimeRep, isUnliftedRuntimeRep,
         isRuntimeRepTy, isRuntimeRepVar,
         sameVis,
 
@@ -857,40 +859,61 @@ mkTyConTy tycon = TyConApp tycon []
 Some basic functions, put here to break loops eg with the pretty printer
 -}
 
--- | If a type is @'TYPE' r@ for some @r@, run the predicate argument on @r@.
--- Otherwise, return 'False'.
---
--- This function does not distinguish between 'Constraint' and 'Type'. For a
--- version which does distinguish between the two, see 'tcIsTYPE'.
-isTYPE :: (   Type    -- the single argument to TYPE; not a synonym
-           -> Bool )  -- what to return
-       -> Kind -> Bool
-isTYPE f ki | Just ki' <- coreView ki = isTYPE f ki'
-isTYPE f (TyConApp tc [arg])
-  | tc `hasKey` tYPETyConKey
-  = go arg
-    where
-      go ty | Just ty' <- coreView ty = go ty'
-      go ty = f ty
-isTYPE _ _ = False
+-- | Extract the RuntimeRep classifier of a type from its kind. For example,
+-- @kindRep * = LiftedRep@; Panics if this is not possible.
+-- Treats * and Constraint as the same
+kindRep :: HasDebugCallStack => Kind -> Type
+kindRep k = case kindRep_maybe k of
+              Just r  -> r
+              Nothing -> pprPanic "kindRep" (ppr k)
+
+-- | Given a kind (TYPE rr), extract its RuntimeRep classifier rr.
+-- For example, @kindRep_maybe * = Just LiftedRep@
+-- Returns 'Nothing' if the kind is not of form (TYPE rr)
+-- Treats * and Constraint as the same
+kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
+kindRep_maybe kind
+  | Just kind' <- coreView kind = kindRep_maybe kind'
+  | TyConApp tc [arg] <- kind
+  , tc `hasKey` tYPETyConKey    = Just arg
+  | otherwise                   = Nothing
 
 -- | This version considers Constraint to be the same as *. Returns True
 -- if the argument is equivalent to Type/Constraint and False otherwise.
 -- See Note [Kind Constraint and kind Type]
 isLiftedTypeKind :: Kind -> Bool
-isLiftedTypeKind = isTYPE is_lifted
-  where
-    is_lifted (TyConApp lifted_rep []) = lifted_rep `hasKey` liftedRepDataConKey
-    is_lifted _                        = False
+isLiftedTypeKind kind
+  = case kindRep_maybe kind of
+      Just rep -> isLiftedRuntimeRep rep
+      Nothing  -> False
 
 -- | Returns True if the kind classifies unlifted types and False otherwise.
 -- Note that this returns False for levity-polymorphic kinds, which may
 -- be specialized to a kind that classifies unlifted types.
 isUnliftedTypeKind :: Kind -> Bool
-isUnliftedTypeKind = isTYPE is_unlifted
-  where
-    is_unlifted (TyConApp rr _args) = elem (getUnique rr) unliftedRepDataConKeys
-    is_unlifted _                   = False
+isUnliftedTypeKind kind
+  = case kindRep_maybe kind of
+      Just rep -> isUnliftedRuntimeRep rep
+      Nothing  -> False
+
+isLiftedRuntimeRep, isUnliftedRuntimeRep :: Type -> Bool
+-- isLiftedRuntimeRep is true of LiftedRep :: RuntimeRep
+-- Similarly isUnliftedRuntimeRep
+isLiftedRuntimeRep rep
+  | Just rep' <- coreView rep          = isLiftedRuntimeRep rep'
+  | TyConApp rr_tc args <- rep
+  , rr_tc `hasKey` liftedRepDataConKey = ASSERT( null args ) True
+  | otherwise                          = False
+
+isUnliftedRuntimeRep rep
+  | Just rep' <- coreView rep          = isUnliftedRuntimeRep rep'
+  | TyConApp rr_tc args <- rep
+  , isUnliftedRuntimeRepTyCon rr_tc    = ASSERT( null args ) True
+  | otherwise                          = False
+
+isUnliftedRuntimeRepTyCon :: TyCon -> Bool
+isUnliftedRuntimeRepTyCon rr_tc
+  = elem (getUnique rr_tc) unliftedRepDataConKeys
 
 -- | Is this the type 'RuntimeRep'?
 isRuntimeRepTy :: Type -> Bool
index e489551..0fff81c 100644 (file)
@@ -53,7 +53,7 @@ module Type (
         mkStrLitTy, isStrLitTy,
         isLitTy,
 
-        getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,
+        getRuntimeRep_maybe, kindRep_maybe, kindRep,
 
         mkCastTy, mkCoercionTy, splitCastTy_maybe,
 
@@ -126,13 +126,13 @@ module Type (
         isPrimitiveType, isStrictType,
         isRuntimeRepTy, isRuntimeRepVar, isRuntimeRepKindedTy,
         dropRuntimeRepArgs,
-        getRuntimeRep, getRuntimeRepFromKind,
+        getRuntimeRep,
 
         -- * Main data types representing Kinds
         Kind,
 
         -- ** Finding the kind of a type
-        typeKind, isTypeLevPoly, resultIsLevPoly,
+        typeKind, tcTypeKind, isTypeLevPoly, resultIsLevPoly,
         tcIsLiftedTypeKind, tcIsConstraintKind, tcReturnsConstraintKind,
 
         -- ** Common Kind
@@ -246,7 +246,8 @@ import Class
 import TyCon
 import TysPrim
 import {-# SOURCE #-} TysWiredIn ( listTyCon, typeNatKind, unitTy
-                                 , typeSymbolKind, liftedTypeKind )
+                                 , typeSymbolKind, liftedTypeKind
+                                 , constraintKind )
 import PrelNames
 import CoAxiom
 import {-# SOURCE #-} Coercion( mkNomReflCo, mkGReflCo, mkReflCo
@@ -336,12 +337,14 @@ import Control.Monad    ( guard )
 
 Note [coreView vs tcView]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
-So far as the typechecker is concerned, 'Constraint' and 'TYPE LiftedRep' are distinct kinds.
+So far as the typechecker is concerned, 'Constraint' and 'TYPE
+LiftedRep' are distinct kinds.
 
 But in Core these two are treated as identical.
 
-We implement this by making 'coreView' convert 'Constraint' to 'TYPE LiftedRep' on the fly.
-The function tcView (used in the type checker) does not do this.
+We implement this by making 'coreView' convert 'Constraint' to 'TYPE
+LiftedRep' on the fly.  The function tcView (used in the type checker)
+does not do this.
 
 See also Trac #11715, which tracks removing this inconsistency.
 
@@ -1240,22 +1243,6 @@ newTyConInstRhs tycon tys
                            CastTy
                            ~~~~~~
 A casted type has its *kind* casted into something new.
-
-Note [Weird typing rule for ForAllTy]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Here is the (truncated) typing rule for the dependent ForAllTy:
-
-inner : kind
-------------------------------------
-ForAllTy (Bndr tyvar vis) inner : kind
-
-inner : TYPE r
-------------------------------------
-ForAllTy (Bndr covar vis) inner : TYPE
-
-Note that when inside the binder is a tyvar, neither the inner type nor for
-ForAllTy itself have to have kind *! But, it means that we should push any kind
-casts through the ForAllTy. The only trouble is avoiding capture.
 -}
 
 splitCastTy_maybe :: Type -> Maybe (Type, Coercion)
@@ -1764,27 +1751,6 @@ When treated as a user type, predicates are invisible and are
 implicitly instantiated; but coercion types, and non-pred evidence
 types, are just regular old types.
 
-Note [isPredTy complications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-You would think that we could define
-  isPredTy ty = isConstraintKind (typeKind ty)
-But there are a number of complications:
-
-* isPredTy is used when printing types, which can happen in debug
-  printing during type checking of not-fully-zonked types.  So it's
-  not cool to say isConstraintKind (typeKind ty) because, absent
-  zonking, the type might be ill-kinded, and typeKind crashes. Hence the
-  rather tiresome story here
-
-* isPredTy must return "True" to *unlifted* coercions, such as (t1 ~# t2)
-  and (t1 ~R# t2), which are not of kind Constraint!  Currently they are
-  of kind #.
-
-* If we do form the type '(C a => C [a]) => blah', then we'd like to
-  print it as such. But that means that isPredTy must return True for
-  (C a => C [a]).  Admittedly that type is illegal in Haskell, but we
-  want to print it nicely in error messages.
-
 Note [Evidence for quantified constraints]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The superclass mechanism in TcCanonical.makeSuperClasses risks
@@ -1830,11 +1796,9 @@ tcIsConstraintKind ty
 -- treats them as the same type, see 'isLiftedTypeKind'.
 tcIsLiftedTypeKind :: Kind -> Bool
 tcIsLiftedTypeKind ty
-  | Just (type_tc, [arg]) <- tcSplitTyConApp_maybe ty
-  , type_tc `hasKey` tYPETyConKey
-  , Just (lifted_rep_tc, args) <- tcSplitTyConApp_maybe arg
-  , lifted_rep_tc `hasKey` liftedRepDataConKey
-  = ASSERT2( null args, ppr ty ) True
+  | Just (tc, [arg]) <- tcSplitTyConApp_maybe ty    -- Note: tcSplit here
+  , tc `hasKey` tYPETyConKey
+  = isLiftedRuntimeRep arg
   | otherwise
   = False
 
@@ -1868,57 +1832,6 @@ isCoVarType ty
   = True
 isCoVarType _ = False
 
--- | Is the type suitable to classify a given/wanted in the typechecker?
-isPredTy :: Type -> Bool
--- See Note [isPredTy complications]
--- NB: /not/ true of (t1 ~# t2) or (t1 ~R# t2)
---     See Note [Types for coercions, predicates, and evidence]
-isPredTy ty = go ty []
-  where
-    go :: Type -> [KindOrType] -> Bool
-    -- Since we are looking at the kind,
-    -- no need to look through type synonyms
-    go (AppTy ty1 ty2)   args       = go ty1 (ty2 : args)
-    go (TyVarTy tv)      args       = go_k (tyVarKind tv) args
-    go (TyConApp tc tys) args       = ASSERT( null args )  -- TyConApp invariant
-                                      go_k (tyConKind tc) tys
-    go (FunTy arg res) []
-      | isPredTy arg                = isPredTy res   -- (Eq a => C a)
-      | otherwise                   = False          -- (Int -> Bool)
-    go (ForAllTy _ ty) []           = go ty []
-    go (CastTy _ co) args           = go_k (pSnd (coercionKind co)) args
-    go _ _ = False
-
-    go_k :: Kind -> [KindOrType] -> Bool
-    -- True <=> ('k' applied to 'kts') = Constraint
-    go_k k [] = tcIsConstraintKind k
-    go_k k (arg:args) = case piResultTy_maybe k arg of
-                          Just k' -> go_k k' args
-                          Nothing -> WARN( True, text "isPredTy" <+> ppr ty )
-                                     False
-       -- This last case shouldn't happen under most circumstances. It can
-       -- occur if we call isPredTy during kind checking, especially if one
-       -- of the following happens:
-       --
-       -- 1. There is actually a kind error.  Example in which this showed up:
-       --    polykinds/T11399
-       --
-       -- 2. A type constructor application appears to be oversaturated. An
-       --    example of this occurred in GHC Trac #13187:
-       --
-       --      {-# LANGUAGE PolyKinds #-}
-       --      type Const a b = b
-       --      f :: Const Int (,) Bool Char -> Char
-       --
-       --    We call isPredTy (Const k1 k2 Int (,) Bool Char
-       --    where k1,k2 are unification variables that have been
-       --    unified to *, and (*->*->*) resp, /but not zonked/.
-       --    This shows that isPredTy can report a false negative
-       --    if a constraint is similarly oversaturated, but
-       --    it's hard to do better than isPredTy currently does without
-       --    zonking, so we punt on such cases for now.  This only happens
-       --    during debug-printing, so it doesn't matter.
-
 isClassPred, isEqPred, isNomEqPred, isIPPred :: PredType -> Bool
 isClassPred ty = case tyConAppTyCon_maybe ty of
     Just tyCon | isClassTyCon tyCon -> True
@@ -2350,10 +2263,9 @@ isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool
 isLiftedType_maybe ty = go (getRuntimeRep ty)
   where
     go rr | Just rr' <- coreView rr = go rr'
-    go (TyConApp lifted_rep [])
-      | lifted_rep `hasKey` liftedRepDataConKey = Just True
-    go (TyConApp {}) = Just False -- everything else is unlifted
-    go _             = Nothing    -- levity polymorphic
+          | isLiftedRuntimeRep rr  = Just True
+          | TyConApp {} <- rr      = Just False  -- Everything else is unlifted
+          | otherwise              = Nothing     -- levity polymorphic
 
 -- | See "Type#type_classification" for what an unlifted type is.
 -- Panics on levity polymorphic types.
@@ -2385,7 +2297,7 @@ dropRuntimeRepArgs = dropWhile isRuntimeRepKindedTy
 -- possible.
 getRuntimeRep_maybe :: HasDebugCallStack
                     => Type -> Maybe Type
-getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind
+getRuntimeRep_maybe = kindRep_maybe . typeKind
 
 -- | Extract the RuntimeRep classifier of a type. For instance,
 -- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
@@ -2395,30 +2307,6 @@ getRuntimeRep ty
       Just r  -> r
       Nothing -> pprPanic "getRuntimeRep" (ppr ty <+> dcolon <+> ppr (typeKind ty))
 
--- | Extract the RuntimeRep classifier of a type from its kind. For example,
--- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible.
-getRuntimeRepFromKind :: HasDebugCallStack
-                      => Type -> Type
-getRuntimeRepFromKind k =
-    case getRuntimeRepFromKind_maybe k of
-      Just r  -> r
-      Nothing -> pprPanic "getRuntimeRepFromKind"
-                           (ppr k <+> dcolon <+> ppr (typeKind k))
-
--- | Extract the RuntimeRep classifier of a type from its kind. For example,
--- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not
--- possible.
-getRuntimeRepFromKind_maybe :: HasDebugCallStack
-                            => Type -> Maybe Type
-getRuntimeRepFromKind_maybe = go
-  where
-    go k | Just k' <- coreView k = go k'
-    go k
-      | Just (_tc, [arg]) <- splitTyConApp_maybe k
-      = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
-        Just arg
-    go _ = Nothing
-
 isUnboxedTupleType :: Type -> Bool
 isUnboxedTupleType ty
   = tyConAppTyCon (getRuntimeRep ty) `hasKey` tupleRepDataConKey
@@ -2752,34 +2640,130 @@ nonDetCmpTc tc1 tc2
         The kind of a type
 *                                                                      *
 ************************************************************************
+
+Note [typeKind vs tcTypeKind]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have two functions to get the kind of a type
+
+  * typeKind   ignores  the distinction between Constraint and *
+  * tcTypeKind respects the distinction between Constraint and *
+
+tcTypeKind is used by the type inference engine, for which Constraint
+and * are different; after that we use typeKind.
+
+See also Note [coreView vs tcView]
+
+Note [Kinding rules for types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In typeKind we consider Constraint and (TYPE LiftedRep) to be identical.
+We then have
+
+         t1 : TYPE rep1
+         t2 : TYPE rep2
+   (FUN) ----------------
+         t1 -> t2 : Type
+
+         ty : TYPE rep
+         `a` is not free in rep
+(FORALL) -----------------------
+         forall a. ty : TYPE rep
+
+In tcTypeKind we consider Constraint and (TYPE LiftedRep) to be distinct:
+
+          t1 : TYPE rep1
+          t2 : TYPE rep2
+    (FUN) ----------------
+          t1 -> t2 : Type
+
+          t1 : Constraint
+          t2 : TYPE rep
+  (PRED1) ----------------
+          t1 => t2 : Type
+
+          t1 : Constraint
+          t2 : Constraint
+  (PRED2) ---------------------
+          t1 => t2 : Constraint
+
+          ty : TYPE rep
+          `a` is not free in rep
+(FORALL1) -----------------------
+          forall a. ty : TYPE rep
+
+          ty : Constraint
+(FORALL2) -------------------------
+          forall a. ty : Constraint
+
+Note that:
+* The only way we distinguish '->' from '=>' is by the fact
+  that the argument is a PredTy.  Both are FunTys
 -}
 
+-----------------------------
 typeKind :: HasDebugCallStack => Type -> Kind
 typeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
-typeKind (AppTy fun arg)   = typeKind_apps fun [arg]
 typeKind (LitTy l)         = typeLiteralKind l
 typeKind (FunTy {})        = liftedTypeKind
 typeKind (TyVarTy tyvar)   = tyVarKind tyvar
 typeKind (CastTy _ty co)   = pSnd $ coercionKind co
 typeKind (CoercionTy co)   = coercionType co
-typeKind ty@(ForAllTy (Bndr tv _) _)
-  | isTyVar tv                     -- See Note [Weird typing rule for ForAllTy].
-  = case occCheckExpand tvs k of   -- We must make sure tv does not occur in kind
-      Just k' -> k'                -- As it is already out of scope!
+
+typeKind (AppTy fun arg)
+  = go fun [arg]
+  where
+    -- Accumulate the type arugments, so we can call piResultTys,
+    -- rather than a succession of calls to piResultTy (which is
+    -- asymptotically costly as the number of arguments increases)
+    go (AppTy fun arg) args = go fun (arg:args)
+    go fun             args = piResultTys (typeKind fun) args
+
+typeKind ty@(ForAllTy {})
+  = case occCheckExpand tvs body_kind of   -- We must make sure tv does not occur in kind
+      Just k' -> k'                        -- As it is already out of scope!
       Nothing -> pprPanic "typeKind"
-                  (ppr ty $$ ppr k $$ ppr tvs $$ ppr body)
+                  (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
+  where
+    (tvs, body) = splitTyVarForAllTys ty
+    body_kind   = typeKind body
+
+-----------------------------
+tcTypeKind :: HasDebugCallStack => Type -> Kind
+tcTypeKind (TyConApp tc tys) = piResultTys (tyConKind tc) tys
+tcTypeKind (LitTy l)         = typeLiteralKind l
+tcTypeKind (TyVarTy tyvar)   = tyVarKind tyvar
+tcTypeKind (CastTy _ty co)   = pSnd $ coercionKind co
+tcTypeKind (CoercionTy co)   = coercionType co
+
+tcTypeKind (FunTy arg res)
+  | isPredTy arg && isPredTy res = constraintKind
+  | otherwise                    = liftedTypeKind
+
+tcTypeKind (AppTy fun arg)
+  = go fun [arg]
+  where
+    -- Accumulate the type arugments, so we can call piResultTys,
+    -- rather than a succession of calls to piResultTy (which is
+    -- asymptotically costly as the number of arguments increases)
+    go (AppTy fun arg) args = go fun (arg:args)
+    go fun             args = piResultTys (tcTypeKind fun) args
+
+tcTypeKind ty@(ForAllTy {})
+  | tcIsConstraintKind body_kind
+  = constraintKind
+
+  | otherwise
+  = case occCheckExpand tvs body_kind of   -- We must make sure tv does not occur in kind
+      Just k' -> k'                        -- As it is already out of scope!
+      Nothing -> pprPanic "tcTypeKind"
+                  (ppr ty $$ ppr tvs $$ ppr body <+> dcolon <+> ppr body_kind)
   where
     (tvs, body) = splitTyVarForAllTys ty
-    k           = typeKind body
-typeKind (ForAllTy {})     = liftedTypeKind
-
-typeKind_apps :: HasDebugCallStack => Type -> [Type] -> Kind
--- The sole purpose of the function is to accumulate
--- the type arugments, so we can call piResultTys, rather than
--- a succession of calls to piResultTy (which is asymptotically
--- less efficient as the number of arguments increases)
-typeKind_apps (AppTy fun arg) args = typeKind_apps fun (arg:args)
-typeKind_apps fun             args = piResultTys (typeKind fun) args
+    body_kind = tcTypeKind body
+
+
+isPredTy :: Type -> Bool
+-- See Note [Types for coercions, predicates, and evidence]
+isPredTy ty = tcIsConstraintKind (tcTypeKind ty)
 
 --------------------------
 typeLiteralKind :: TyLit -> Kind