Checkpoint after renamingwip/t11715

50 files changed, 202 insertions, 186 deletions

diff --git a/compiler/basicTypes/MkId.hs b/compiler/basicTypes/MkId.hs
index 002132acd2..7824b5a141 100644
--- a/compiler/basicTypes/MkId.hs
+++ b/compiler/basicTypes/MkId.hs
@@ -1114,10 +1114,10 @@ unsafeCoerceId
                        `setUnfoldingInfo`  mkCompulsoryUnfolding rhs
 
     -- unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
-    --                         (a :: TYPEvis r1) (b :: TYPEvis r2).
+    --                         (a :: TYPE r1) (b :: TYPE r2).
     --                         a -> b
     bndrs = mkTemplateKiTyVars [runtimeRepTy, runtimeRepTy]
-                               (\ks -> map tYPEvis ks)
+                               (\ks -> map tYPE ks)
 
     [_, _, a, b] = mkTyVarTys bndrs
 
@@ -1301,7 +1301,7 @@ unboxed values (unsafeCoerce 3#).
 
 In contrast unsafeCoerce# is even more dangerous because you *can* use
 it on unboxed things, (unsafeCoerce# 3#) :: Int. Its type is
-   forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a: TYPEvis r1) (b: TYPEvis r2). a -> b
+   forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a: TYPE r1) (b: TYPE r2). a -> b
 
 Note [seqId magic]
 ~~~~~~~~~~~~~~~~~~
@@ -1464,7 +1464,7 @@ no further floating will occur. This allows us to safely inline things like
 While the definition of @GHC.Magic.runRW#@, we override its type in @MkId@
 to be open-kinded,
 
-    runRW# :: forall (r1 :: RuntimeRep). (o :: TYPEvis r)
+    runRW# :: forall (r1 :: RuntimeRep). (o :: TYPE r)
            => (State# RealWorld -> (# State# RealWorld, o #))
                               -> (# State# RealWorld, o #)
 
diff --git a/compiler/basicTypes/PatSyn.hs b/compiler/basicTypes/PatSyn.hs
index 0e85bf25d6..823c838c05 100644
--- a/compiler/basicTypes/PatSyn.hs
+++ b/compiler/basicTypes/PatSyn.hs
@@ -83,7 +83,7 @@ data PatSyn
              -- Matcher function.
              -- If Bool is True then prov_theta and arg_tys are empty
              -- and type is
-             --   forall (p :: RuntimeRep) (r :: TYPEvis p) univ_tvs.
+             --   forall (p :: RuntimeRep) (r :: TYPE p) univ_tvs.
              --                          req_theta
              --                       => res_ty
              --                       -> (forall ex_tvs. Void# -> r)
@@ -91,7 +91,7 @@ data PatSyn
              --                       -> r
              --
              -- Otherwise type is
-             --   forall (p :: RuntimeRep) (r :: TYPEvis r) univ_tvs.
+             --   forall (p :: RuntimeRep) (r :: TYPE r) univ_tvs.
              --                          req_theta
              --                       => res_ty
              --                       -> (forall ex_tvs. prov_theta => arg_tys -> r)
diff --git a/compiler/coreSyn/CoreSyn.hs b/compiler/coreSyn/CoreSyn.hs
index 2a5752ccb7..00b778a253 100644
--- a/compiler/coreSyn/CoreSyn.hs
+++ b/compiler/coreSyn/CoreSyn.hs
@@ -439,12 +439,12 @@ The levity-polymorphism invariants are these:
 * The type of a term-binder must not be levity-polymorphic
 * The type of the argument of an App must not be levity-polymorphic.
 
-A type (t::TYPE v r) is "levity polymorphic" if 'r' has any free variables.
+A type (t::TYPEV v r) is "levity polymorphic" if 'r' has any free variables.
 (It's OK from the code generator's point-of-view if v has free variables.)
 
 For example
-  \(r::RuntimeRep). \(a::TYPEvis r). \(x::a). e
-is illegal because x's type has kind (TYPEvis r), which has 'r' free.
+  \(r::RuntimeRep). \(a::TYPE r). \(x::a). e
+is illegal because x's type has kind (TYPE r), which has 'r' free.
 
 See Note [Levity polymorphism checking] in DsMonad to see where these
 invariants are established for user-written code.
diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs
index 0795f1840d..faf32d9375 100644
--- a/compiler/coreSyn/MkCore.hs
+++ b/compiler/coreSyn/MkCore.hs
@@ -725,7 +725,7 @@ tYPE_ERROR_ID                   = mkRuntimeErrorId typeErrorName
 
 mkRuntimeErrorId :: Name -> Id
 -- Error function
---   with type:  forall (r:RuntimeRep) (a:TYPEvis r). Addr# -> a
+--   with type:  forall (r:RuntimeRep) (a:TYPE r). Addr# -> a
 --   with arity: 1
 -- which diverges after being given one argument
 -- The Addr# is expected to be the address of
@@ -757,8 +757,8 @@ mkRuntimeErrorId name
 {- Note [Error and friends have an "open-tyvar" forall]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 'error' and 'undefined' have types
-        error     :: forall (v :: RuntimeRep) (a :: TYPEvis v). String -> a
-        undefined :: forall (v :: RuntimeRep) (a :: TYPEvis v). a
+        error     :: forall (v :: RuntimeRep) (a :: TYPE v). String -> a
+        undefined :: forall (v :: RuntimeRep) (a :: TYPE v). a
 Notice the levity polymorphism. This ensures that
 "error" can be instantiated at unboxed as well as boxed types.
 This is OK because it never returns, so the return type is irrelevant.
diff --git a/compiler/ghci/ByteCodeGen.hs b/compiler/ghci/ByteCodeGen.hs
index faaad709ea..f4b224d2a5 100644
--- a/compiler/ghci/ByteCodeGen.hs
+++ b/compiler/ghci/ByteCodeGen.hs
@@ -553,10 +553,10 @@ schemeE d s p exp@(AnnTick (Breakpoint _id _fvs) _rhs)
           -- type and hence won't be bound in the environment, but the
           -- breakpoint will otherwise work fine.
           --
-          -- NB (Trac #12007) this /also/ applies for if (ty :: TYPEvis r), where
+          -- NB (Trac #12007) this /also/ applies for if (ty :: TYPE r), where
           --    r :: RuntimeRep is a variable. This can happen in the
           --    continuations for a pattern-synonym matcher
-          --    match = /\(r::RuntimeRep) /\(a::TYPEvis r).
+          --    match = /\(r::RuntimeRep) /\(a::TYPE r).
           --            \(k :: Int -> a) \(v::T).
           --            case v of MkV n -> k n
           -- Here (k n) :: a :: Type r, so we don't know if it's lifted
diff --git a/compiler/hsSyn/HsUtils.hs b/compiler/hsSyn/HsUtils.hs
index 25529a8c26..58948cc862 100644
--- a/compiler/hsSyn/HsUtils.hs
+++ b/compiler/hsSyn/HsUtils.hs
@@ -819,7 +819,7 @@ care about the strictness of the type after the =>. For checked types
 This matters. If we don't separate out the AbsBindsSig case, then GHC runs into
 a problem when compiling
 
-  undefined :: forall (r :: RuntimeRep) (a :: TYPEvis r). HasCallStack => a
+  undefined :: forall (r :: RuntimeRep) (a :: TYPE r). HasCallStack => a
 
 Looking only after the =>, we cannot tell if this is strict or not. (GHC panics
 if you try.) Looking at the whole type, on the other hand, tells you that this
diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs
index 5371a93a89..6672d85f93 100644
--- a/compiler/iface/IfaceType.hs
+++ b/compiler/iface/IfaceType.hs
@@ -295,7 +295,7 @@ isIfaceLiftedTypeKind (IfaceTyConApp tc ITC_Nil)
 isIfaceLiftedTypeKind (IfaceTyConApp tc
                        (ITC_Vis (IfaceTyConApp vis ITC_Nil)
                         (ITC_Vis (IfaceTyConApp ptr_rep_lifted ITC_Nil) ITC_Nil)))
-  =  tc `ifaceTyConHasKey` tYPETyConKey
+  =  tc `ifaceTyConHasKey` tYPEVTyConKey
   && vis `ifaceTyConHasKey` visibleDataConKey
   && ptr_rep_lifted `ifaceTyConHasKey` liftedRepDataConKey
 isIfaceLiftedTypeKind _ = False
@@ -732,7 +732,7 @@ understandable push-back from those with pedagogy in mind, who argued that
 RuntimeRep variables would throw a wrench into nearly any teach approach since
 they appear in even the lowly ($) function's type,
 
-    ($) :: forall (w :: RuntimeRep) a (b :: TYPEvis w). (a -> b) -> a -> b
+    ($) :: forall (w :: RuntimeRep) a (b :: TYPE w). (a -> b) -> a -> b
 
 which is significantly less readable than its non levity-polymorphic type of
 
@@ -752,7 +752,7 @@ PtrLiftedRep. This is done in a pass right before pretty-printing
 -- to 'Visible'. e.g.
 --
 -- @
--- ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPEvis r).
+-- ($) :: forall (r :: GHC.Types.RuntimeRep) a (b :: TYPE r).
 --        (a -> b) -> a -> b
 -- @
 --
@@ -983,16 +983,10 @@ pprTyTcApp' ctxt_prec tc tys dflags style
   , ITC_Invis _ (ITC_Vis ty1 (ITC_Vis ty2 ITC_Nil)) <- tys
   = pprIfaceTyList ctxt_prec ty1 ty2
 
-  | tc `ifaceTyConHasKey` tYPETyConKey
-  , ITC_Vis (IfaceTyConApp vis ITC_Nil) (ITC_Vis (IfaceTyConApp rep ITC_Nil) ITC_Nil) <- tys
-  , vis `ifaceTyConHasKey` visibleDataConKey
-  , rep `ifaceTyConHasKey` liftedRepDataConKey
+  | is_known_kind tc tys visibleDataConKey liftedRepDataConKey
   = kindStar
 
-  | tc `ifaceTyConHasKey` tYPETyConKey
-  , ITC_Vis (IfaceTyConApp vis ITC_Nil) (ITC_Vis (IfaceTyConApp rep ITC_Nil) ITC_Nil) <- tys
-  , vis `ifaceTyConHasKey` invisibleDataConKey
-  , rep `ifaceTyConHasKey` liftedRepDataConKey
+  | is_known_kind tc tys invisibleDataConKey liftedRepDataConKey
   = text "Constraint"
 
   | not opt_PprStyle_Debug
@@ -1008,6 +1002,19 @@ pprTyTcApp' ctxt_prec tc tys dflags style
     info = ifaceTyConInfo tc
     tys_wo_kinds = tcArgsIfaceTypes $ stripInvisArgs dflags tys
 
+    is_known_kind tc tys vis_key rep_key
+      | tc `ifaceTyConHasKey` tYPEVTyConKey
+      , ITC_Vis (IfaceTyConApp vis ITC_Nil)
+                  (ITC_Vis (IfaceTyConApp rep ITC_Nil) ITC_Nil) <- tys
+      = vis `ifaceTyConHasKey` vis_key && rep `ifaceTyConHasKey` rep_key
+
+      | tc `ifaceTyConHasKey` tYPESynTyConKey
+      , ITC_Vis (IfaceTyConApp rep ITC_Nil) ITC_Nil <- tys
+      = vis_key == visibleDataConKey && rep `ifaceTyConHasKey` rep_key
+
+      | otherwise
+      = False
+
 -- | Pretty-print a type-level equality.
 --
 -- See Note [Equality predicates in IfaceType].
diff --git a/compiler/prelude/PrelNames.hs b/compiler/prelude/PrelNames.hs
index cea595d4b6..fcad839a02 100644
--- a/compiler/prelude/PrelNames.hs
+++ b/compiler/prelude/PrelNames.hs
@@ -1647,13 +1647,14 @@ eitherTyConKey :: Unique
 eitherTyConKey                          = mkPreludeTyConUnique 84
 
 -- Kind constructors
-liftedTypeKindTyConKey, tYPETyConKey,
-  constraintKindTyConKey, visibilityTyConKey,
+liftedTypeKindTyConKey, tYPEVTyConKey,
+  constraintKindTyConKey, visibilityTyConKey, tYPESynTyConKey,
   starKindTyConKey, unicodeStarKindTyConKey, runtimeRepTyConKey,
   vecCountTyConKey, vecElemTyConKey :: Unique
 liftedTypeKindTyConKey                  = mkPreludeTyConUnique 87
-tYPETyConKey                            = mkPreludeTyConUnique 88
+tYPEVTyConKey                           = mkPreludeTyConUnique 88
 visibilityTyConKey                      = mkPreludeTyConUnique 89
+tYPESynTyConKey                         = mkPreludeTyConUnique 90
 constraintKindTyConKey                  = mkPreludeTyConUnique 92
 starKindTyConKey                        = mkPreludeTyConUnique 93
 unicodeStarKindTyConKey                 = mkPreludeTyConUnique 94
@@ -2317,6 +2318,6 @@ The following names should be considered by GHCi to be in scope always.
 pretendNameIsInScope :: Name -> Bool
 pretendNameIsInScope n
   = any (n `hasKey`)
-    [ starKindTyConKey, liftedTypeKindTyConKey, tYPETyConKey
+    [ starKindTyConKey, liftedTypeKindTyConKey, tYPEVTyConKey
     , runtimeRepTyConKey, liftedRepDataConKey, visibleDataConKey
     , visibilityTyConKey ]
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index 6992925910..d8da4795c4 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -24,10 +24,10 @@ module TysPrim(
         openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar,
 
         -- Kind constructors...
-        tYPETyConName,
+        tYPEVTyConName, tYPEVTyCon,
 
         -- Kinds
-        tYPE, tYPEvis, primRepToRuntimeRep,
+        tYPEV, tYPE, primRepToRuntimeRep,
 
         funTyCon, funTyConName,
         primTyCons,
@@ -81,7 +81,7 @@ module TysPrim(
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TysWiredIn
-  ( runtimeRepTy, visibilityTy, visibleDataConTy, unboxedTupleKind, liftedTypeKind
+  ( runtimeRepTy, visibilityTy, unboxedTupleKind, liftedTypeKind
   , vecRepDataConTyCon, tupleRepDataConTyCon
   , liftedRepDataConTy, unliftedRepDataConTy, intRepDataConTy
   , wordRepDataConTy, int64RepDataConTy, word64RepDataConTy, addrRepDataConTy
@@ -92,7 +92,7 @@ import {-# SOURCE #-} TysWiredIn
   , int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy
   , word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy
   , doubleElemRepDataConTy
-  , mkPromotedListTy )
+  , mkPromotedListTy, tYPESynTyCon )
 
 import Var              ( TyVar, mkTyVar )
 import Name
@@ -152,7 +152,7 @@ primTyCons
     , eqReprPrimTyCon
     , eqPhantPrimTyCon
 
-    , tYPETyCon
+    , tYPEVTyCon
 
 #include "primop-vector-tycons.hs-incl"
     ]
@@ -271,8 +271,8 @@ mkTemplateKiTyVars
                              -- Result is anon arg kinds [ak1, .., akm]
     -> [TyVar]   -- [kv1:k1, ..., kvn:kn, av1:ak1, ..., avm:akm]
 -- Example: if you want the tyvars for
---   forall (r:RuntimeRep) (a:TYPEvis r) (b:*). blah
--- call mkTemplateKiTyVars [RuntimeRep] (\[r]. [TYPEvis r, *)
+--   forall (r:RuntimeRep) (a:TYPE r) (b:*). blah
+-- call mkTemplateKiTyVars [RuntimeRep] (\[r]. [TYPE r, *)
 mkTemplateKiTyVars kind_var_kinds mk_arg_kinds
   = kv_bndrs ++ tv_bndrs
   where
@@ -311,7 +311,7 @@ runtimeRep2Ty = mkTyVarTy runtimeRep2TyVar
 
 openAlphaTyVar, openBetaTyVar :: TyVar
 [openAlphaTyVar,openBetaTyVar]
-  = mkTemplateTyVars [tYPEvis runtimeRep1Ty, tYPEvis runtimeRep2Ty]
+  = mkTemplateTyVars [tYPE runtimeRep1Ty, tYPE runtimeRep2Ty]
 
 openAlphaTy, openBetaTy :: Type
 openAlphaTy = mkTyVarTy openAlphaTyVar
@@ -353,7 +353,7 @@ funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
 
 Note [TYPE and RuntimeRep]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
-All types that classify values have a kind of the form (TYPE v rr), where
+All types that classify values have a kind of the form (TYPEV v rr), where
 
     data Visibility = Visible | Invisible   -- Defined in ghc-prim:GHC.Types
 
@@ -367,19 +367,19 @@ All types that classify values have a kind of the form (TYPE v rr), where
     rr :: RuntimeRep
     v  :: Visibility
 
-    TYPE :: Visibility -> RuntimeRep -> TYPE 'LiftedRep  -- Built in
+    TYPEV :: Visibility -> RuntimeRep -> TYPEV 'Visible 'LiftedRep  -- Built in
 
 So for example:
-    Int        :: TYPE 'Visible 'LiftedRep
-    Array# Int :: TYPE 'Visible 'UnliftedRep
-    Int#       :: TYPE 'Visible 'IntRep
-    Float#     :: TYPE 'Visible 'FloatRep
-    Maybe      :: TYPE 'Visible 'LiftedRep -> TYPE 'Visible 'LiftedRep
-    (# , #)    :: TYPE 'Visible r1 -> TYPE 'Visible r2 -> TYPE 'Visible (TupleRep [r1, r2])
-    Eq         :: TYPE 'Visible 'LiftedRep -> TYPE 'Invisible 'LiftedRep
+    Int        :: TYPEV 'Visible 'LiftedRep
+    Array# Int :: TYPEV 'Visible 'UnliftedRep
+    Int#       :: TYPEV 'Visible 'IntRep
+    Float#     :: TYPEV 'Visible 'FloatRep
+    Maybe      :: TYPEV 'Visible 'LiftedRep -> TYPEV 'Visible 'LiftedRep
+    (# , #)    :: TYPEV 'Visible r1 -> TYPEV 'Visible r2 -> TYPEV 'Visible (TupleRep [r1, r2])
+    Eq         :: TYPEV 'Visible 'LiftedRep -> TYPEV 'Invisible 'LiftedRep
 
 We abbreviate '*' specially:
-    type * = TYPE 'Visible 'LiftedRep
+    type * = TYPEV 'Visible 'LiftedRep
 
 The 'v' parameter tells us whether arguments of a type of the kind are written
 visibly and 'rr' parameter tells us how the value is represented at runime.
@@ -388,10 +388,10 @@ is LiftedRep. (The other possibilities are well-formed kinds, but they are
 empty.)
 
 Because 'Visible is the vastly common case, we define
-   type TYPEvis = TYPE 'Visible
+   type TYPE = TYPEV 'Visible
 
 Generally speaking, you can't be polymorphic in 'rr'.  E.g
-   f :: forall (rr:RuntimeRep) (a:TYPEvis rr). a -> [a]
+   f :: forall (rr:RuntimeRep) (a:TYPE rr). a -> [a]
    f = /\(rr:RuntimeRep) (a:rr) \(a:rr). ...
 This is no good: we could not generate code code for 'f', because the
 calling convention for 'f' varies depending on whether the argument is
@@ -399,22 +399,22 @@ a a Int, Int#, or Float#.  (You could imagine generating specialised
 code, one for each instantiation of 'rr', but we don't do that.)
 
 Certain functions CAN be runtime-rep-polymorphic, because the code
-generator never has to manipulate a value of type 'a :: TYPEvis rr'.
+generator never has to manipulate a value of type 'a :: TYPE rr'.
 
-* error :: forall (rr:RuntimeRep) (a:TYPEvis rr). String -> a
+* error :: forall (rr:RuntimeRep) (a:TYPE rr). String -> a
   Code generator never has to manipulate the return value.
 
 * unsafeCoerce#, defined in MkId.unsafeCoerceId:
   Always inlined to be a no-op
      unsafeCoerce# :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
-                             (a :: TYPEvis r1) (b :: TYPEvis r2).
+                             (a :: TYPE r1) (b :: TYPE r2).
                              a -> b
 
 * Unboxed tuples, and unboxed sums, defined in TysWiredIn
   Always inlined, and hence specialised to the call site
      (#,#) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
-                     (a :: TYPEvis r1) (b :: TYPEvis r2).
-                     a -> b -> TYPEvis ('TupleRep '[r1, r2])
+                     (a :: TYPE r1) (b :: TYPE r2).
+                     a -> b -> TYPE ('TupleRep '[r1, r2])
 
 Note [PrimRep and kindPrimRep]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -431,7 +431,7 @@ We need to get from one to the other; that is what kindPrimRep does.
 Suppose we have a value
    (v :: t) where (t :: k)
 Given this kind
-    k = TyConApp "TYPE" [vis, rep]
+    k = TyConApp "TYPEV" [vis, rep]
 GHC needs to be able to figure out how 'v' is represented at runtime.
 It expects 'rep' to be form
     TyConApp rr_dc args
@@ -441,21 +441,21 @@ PrimRep in the promoted data constructor itself: see TyCon.promDcRepInfo.
 
 -}
 
-tYPETyCon :: TyCon
-tYPETyConName :: Name
+tYPEVTyCon :: TyCon
+tYPEVTyConName :: Name
 
-tYPETyCon = mkKindTyCon tYPETyConName
-                        (mkTemplateAnonTyConBinders [visibilityTy, runtimeRepTy])
-                        liftedTypeKind
-                        [Nominal]
-                        (mkPrelTyConRepName tYPETyConName)
+tYPEVTyCon = mkKindTyCon tYPEVTyConName
+                         (mkTemplateAnonTyConBinders [visibilityTy, runtimeRepTy])
+                         liftedTypeKind
+                         [Nominal]
+                         (mkPrelTyConRepName tYPEVTyConName)
 
 --------------------------
 -- ... and now their names
 
 -- If you edit these, you may need to update the GHC formalism
 -- See Note [GHC Formalism] in coreSyn/CoreLint.hs
-tYPETyConName             = mkPrimTyConName (fsLit "TYPE") tYPETyConKey tYPETyCon
+tYPEVTyConName             = mkPrimTyConName (fsLit "TYPEV") tYPEVTyConKey tYPEVTyCon
 
 mkPrimTyConName :: FastString -> Unique -> TyCon -> Name
 mkPrimTyConName = mkPrimTcName BuiltInSyntax
@@ -467,14 +467,14 @@ mkPrimTcName built_in_syntax occ key tycon
   = mkWiredInName gHC_PRIM (mkTcOccFS occ) key (ATyCon tycon) built_in_syntax
 
 -----------------------------
--- | Given a Visibility RuntimeRep, applies TYPE to it.
+-- | Given a Visibility and RuntimeRep, applies TYPEV to it.
 -- see Note [TYPE and RuntimeRep]
-tYPE :: Type -> Type -> Type
-tYPE v rr = TyConApp tYPETyCon [v, rr]
+tYPEV :: Type -> Type -> Type
+tYPEV v rr = TyConApp tYPEVTyCon [v, rr]
 
--- | Like 'tYPE', but assumes 'Visible'
-tYPEvis :: Type -> Type
-tYPEvis = tYPE visibleDataConTy
+-- | Like 'tYPEV', but assumes 'Visible'
+tYPE :: Type -> Type
+tYPE rep = TyConApp tYPESynTyCon [rep]
 
 {-
 ************************************************************************
@@ -490,7 +490,7 @@ pcPrimTyCon name roles rep
   = mkPrimTyCon name binders result_kind roles
   where
     binders     = mkTemplateAnonTyConBinders (map (const liftedTypeKind) roles)
-    result_kind = tYPEvis (primRepToRuntimeRep rep)
+    result_kind = tYPE (primRepToRuntimeRep rep)
 
 -- | Convert a 'PrimRep' to a 'Type' of kind RuntimeRep
 -- Defined here to avoid (more) module loops
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index 9d7d0c7648..e268f809f5 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -94,6 +94,7 @@ module TysWiredIn (
         starKindTyCon, starKindTyConName,
         unicodeStarKindTyCon, unicodeStarKindTyConName,
         liftedTypeKindTyCon, constraintKindTyCon,
+        tYPESynTyCon,
 
         -- * Parallel arrays
         mkPArrTy,
@@ -395,11 +396,12 @@ typeSymbolKindConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Symbol")
 constraintKindTyConName :: Name
 constraintKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Constraint") constraintKindTyConKey   constraintKindTyCon
 
-liftedTypeKindTyConName, starKindTyConName, unicodeStarKindTyConName
+liftedTypeKindTyConName, starKindTyConName, unicodeStarKindTyConName, tYPESynTyConName
   :: Name
 liftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Type") liftedTypeKindTyConKey liftedTypeKindTyCon
 starKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "*") starKindTyConKey starKindTyCon
 unicodeStarKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "★") unicodeStarKindTyConKey unicodeStarKindTyCon
+tYPESynTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "TYPE") tYPESynTyConKey tYPESynTyCon
 
 visibilityTyConName, runtimeRepTyConName, vecRepDataConName, tupleRepDataConName, sumRepDataConName :: Name
 visibilityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Visibility") visibilityTyConKey visibilityTyCon
@@ -580,10 +582,10 @@ typeSymbolKind = mkTyConTy typeSymbolKindCon
 constraintKindTyCon :: TyCon
 constraintKindTyCon = buildSynTyCon constraintKindTyConName []
                                     liftedTypeKind []
-                                    (tYPE invisibleDataConTy liftedRepTy)
+                                    (tYPEV invisibleDataConTy liftedRepTy)
 
 liftedTypeKind, constraintKind :: Kind
-liftedTypeKind   = tYPE visibleDataConTy liftedRepTy
+liftedTypeKind   = mkTyConApp liftedTypeKindTyCon []
 constraintKind   = mkTyConApp constraintKindTyCon []
 
 -- mkFunKind and mkForAllKind are defined here
@@ -822,11 +824,11 @@ unboxedTupleArr = listArray (0,mAX_TUPLE_SIZE) [mk_tuple Unboxed i | i <- [0..mA
 
 -- | Given the TupleRep/SumRep tycon and list of RuntimeReps of the unboxed
 -- tuple/sum arguments, produces the return kind of an unboxed tuple/sum type
--- constructor. @unboxedTupleSumKind [IntRep, LiftedRep] --> TYPEvis (TupleRep/SumRep
+-- constructor. @unboxedTupleSumKind [IntRep, LiftedRep] --> TYPE (TupleRep/SumRep
 -- [IntRep, LiftedRep])@
 unboxedTupleSumKind :: TyCon -> [Type] -> Kind
 unboxedTupleSumKind tc rr_tys
-  = tYPEvis (mkTyConApp tc [mkPromotedListTy runtimeRepTy rr_tys])
+  = tYPE (mkTyConApp tc [mkPromotedListTy runtimeRepTy rr_tys])
 
 -- | Specialization of 'unboxedTupleSumKind' for tuples
 unboxedTupleKind :: [Type] -> Kind
@@ -863,12 +865,12 @@ mk_tuple Unboxed arity = (tycon, tuple_con)
 
     -- See Note [Unboxed tuple extra vars] in TyCon
     -- Kind:  forall (v1:Visibility) (v2:Visibility)
-    --               (k1:RuntimeRep) (k2:RuntimeRep). TYPE v1 k1 -> TYPE v2 k2
-    --                                             -> TYPE (TupleRep [k1, k2])
+    --               (k1:RuntimeRep) (k2:RuntimeRep). TYPEV v1 k1 -> TYPEV v2 k2
+    --                                             -> TYPEV (TupleRep [k1, k2])
     tc_binders = mkTemplateTyConBinders (nOfThem arity visibilityTy ++
                                          nOfThem arity runtimeRepTy)
                                         (\ks -> let (vs, rs) = splitAt arity ks in
-                                                zipWith tYPE vs rs)
+                                                zipWith tYPEV vs rs)
 
     tc_res_kind = unboxedTupleKind rr_tys
 
@@ -986,7 +988,7 @@ mk_sum arity = (tycon, sum_cons)
                          UnboxedAlgTyCon
 
     tc_binders = mkTemplateTyConBinders (nOfThem arity runtimeRepTy)
-                                        (\ks -> map tYPEvis ks)
+                                        (\ks -> map tYPE ks)
 
     tyvars = binderVars tc_binders
 
@@ -1087,24 +1089,28 @@ visibilityTy = mkTyConTy visibilityTyCon
 runtimeRepTy :: Type
 runtimeRepTy = mkTyConTy runtimeRepTyCon
 
-liftedTypeKindTyCon, starKindTyCon, unicodeStarKindTyCon :: TyCon
+liftedTypeKindTyCon, starKindTyCon, unicodeStarKindTyCon, tYPESynTyCon :: TyCon
 
 -- Type syononyms; see Note [TYPE and RuntimeRep] in TysPrim
--- type Type = TYPE 'Visible 'LiftedRep
--- type *    = TYPE 'Visible 'LiftedRep
--- type *    = TYPE 'Visible 'LiftedRep  -- Unicode variant
+-- type Type = TYPEV 'Visible 'LiftedRep
+-- type *    = TYPEV 'Visible 'LiftedRep
+-- type *    = TYPEV 'Visible 'LiftedRep  -- Unicode variant
 
 liftedTypeKindTyCon   = buildSynTyCon liftedTypeKindTyConName
                                        [] liftedTypeKind []
-                                       (tYPE visibleDataConTy liftedRepTy)
+                                       (tYPE liftedRepTy)
 
 starKindTyCon         = buildSynTyCon starKindTyConName
                                        [] liftedTypeKind []
-                                       (tYPE visibleDataConTy liftedRepTy)
+                                       (tYPE liftedRepTy)
 
 unicodeStarKindTyCon  = buildSynTyCon unicodeStarKindTyConName
                                        [] liftedTypeKind []
-                                       (tYPE visibleDataConTy liftedRepTy)
+                                       (tYPE liftedRepTy)
+
+tYPESynTyCon          = buildSynTyCon tYPESynTyConName
+                                       [] (runtimeRepTy `mkFunTy` liftedTypeKind) []
+                                       (mkTyConApp tYPEVTyCon [visibleDataConTy])
 
 visibilityTyCon :: TyCon
 visibilityTyCon = pcTyCon True visibilityTyConName Nothing []
diff --git a/compiler/prelude/TysWiredIn.hs-boot b/compiler/prelude/TysWiredIn.hs-boot
index ad2b142346..e440b726ad 100644
--- a/compiler/prelude/TysWiredIn.hs-boot
+++ b/compiler/prelude/TysWiredIn.hs-boot
@@ -12,6 +12,7 @@ listTyCon :: TyCon
 typeNatKind, typeSymbolKind :: Type
 mkBoxedTupleTy :: [Type] -> Type
 
+tYPESynTyCon :: TyCon
 liftedTypeKind :: Kind
 constraintKind :: Kind
 
diff --git a/compiler/simplStg/RepType.hs b/compiler/simplStg/RepType.hs
index d1759e657e..45e199148c 100644
--- a/compiler/simplStg/RepType.hs
+++ b/compiler/simplStg/RepType.hs
@@ -46,7 +46,7 @@ import qualified Data.IntSet as IS
 
 type NvUnaryType = Type
 type UnaryType   = Type
-     -- Both are always a value type; i.e. its kind is TYPE v rr
+     -- Both are always a value type; i.e. its kind is TYPEV v rr
      -- for some rr; moreover the rr is never a variable.
      --
      --   NvUnaryType : never an unboxed tuple or sum, or void
@@ -153,7 +153,7 @@ ubxSumRepType :: [[PrimRep]] -> [SlotTy]
 ubxSumRepType constrs0
   -- These first two cases never classify an actual unboxed sum, which always
   -- has at least two disjuncts. But it could happen if a user writes, e.g.,
-  -- forall (a :: TYPEvis (SumRep [IntRep])). ...
+  -- forall (a :: TYPE (SumRep [IntRep])). ...
   -- which could never be instantiated. We still don't want to panic.
   | length constrs0 < 2
   = [WordSlot]
@@ -331,14 +331,14 @@ tyConPrimRep1 tc = case tyConPrimRep tc of
   [rep] -> rep
   _     -> pprPanic "tyConPrimRep1" (ppr tc $$ ppr (tyConPrimRep tc))
 
--- | Take a kind (of shape @TYPE v rr@) and produce the 'PrimRep's
+-- | Take a kind (of shape @TYPEV v rr@) and produce the 'PrimRep's
 -- of values of types of this kind.
 kindPrimRep :: HasDebugCallStack => SDoc -> Kind -> [PrimRep]
 kindPrimRep doc ki
   | Just ki' <- coreView ki
   = kindPrimRep doc ki'
 kindPrimRep doc (TyConApp typ [_vis, runtime_rep])
-  = ASSERT( typ `hasKey` tYPETyConKey )
+  = ASSERT( typ `hasKey` tYPEVTyConKey )
     runtimeRepPrimRep doc runtime_rep
 kindPrimRep doc ki
   = pprPanic "kindPrimRep" (ppr ki $$ doc)
@@ -358,4 +358,4 @@ runtimeRepPrimRep doc rr_ty
 -- | Convert a PrimRep back to a Type. Used only in the unariser to give types
 -- to fresh Ids. Really, only the type's representation matters.
 primRepToType :: PrimRep -> Type
-primRepToType = anyTypeOfKind . tYPEvis . primRepToRuntimeRep
+primRepToType = anyTypeOfKind . tYPE . primRepToRuntimeRep
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 9ddfce046e..77d6a46a02 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -361,7 +361,7 @@ tcExpr expr@(OpApp arg1 op fix arg2) res_ty
        ; arg2'  <- tcArg op arg2 arg2_sigma 2
 
        -- Make sure that the argument type has kind '*'
-       --   ($) :: forall (r:RuntimeRep) (a:*) (b:TYPEvis r). (a->b) -> a -> b
+       --   ($) :: forall (r:RuntimeRep) (a:*) (b:TYPE r). (a->b) -> a -> b
        -- Eg we do not want to allow  (D#  $  4.0#)   Trac #5570
        --    (which gives a seg fault)
        --
diff --git a/compiler/typecheck/TcMType.hs b/compiler/typecheck/TcMType.hs
index 86fdd02e8a..72c76f3d8e 100644
--- a/compiler/typecheck/TcMType.hs
+++ b/compiler/typecheck/TcMType.hs
@@ -417,7 +417,7 @@ inferResultToType :: InferResult -> TcM Type
 inferResultToType (IR { ir_uniq = u, ir_lvl = tc_lvl
                       , ir_ref = ref })
   = do { rr  <- newMetaTyVarTyAtLevel tc_lvl runtimeRepTy
-       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPEvis rr)
+       ; tau <- newMetaTyVarTyAtLevel tc_lvl (tYPE rr)
              -- See Note [TcLevel of ExpType]
        ; writeMutVar ref (Just tau)
        ; traceTc "Forcing ExpType to be monomorphic:"
@@ -787,10 +787,10 @@ newFlexiTyVarTys n kind = mapM newFlexiTyVarTy (nOfThem n kind)
 newOpenTypeKind :: TcM TcKind
 newOpenTypeKind
   = do { rr <- newFlexiTyVarTy runtimeRepTy
-       ; return (tYPEvis rr) }
+       ; return (tYPE rr) }
 
 -- | Create a tyvar that can be a lifted or unlifted type.
--- Returns alpha :: TYPEvis kappa, where both alpha and kappa are fresh
+-- Returns alpha :: TYPE kappa, where both alpha and kappa are fresh
 newOpenFlexiTyVarTy :: TcM TcType
 newOpenFlexiTyVarTy
   = do { kind <- newOpenTypeKind
@@ -982,7 +982,7 @@ zonkQuantifiedTyVar :: Bool     -- True  <=> this is a kind var and -XNoPolyKind
                     -> TcM (Maybe TcTyVar)
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables, and
--- default their kind (e.g. from TYPEvis v to TYPEvis Lifted)
+-- default their kind (e.g. from TYPE v to TYPE Lifted)
 -- The meta tyvar is updated to point to the new skolem TyVar.  Now any
 -- bound occurrences of the original type variable will get zonked to
 -- the immutable version.
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs
index 8e5fe83af6..587e2b8806 100644
--- a/compiler/typecheck/TcPatSyn.hs
+++ b/compiler/typecheck/TcPatSyn.hs
@@ -385,7 +385,7 @@ tcPatSynMatcher (L loc name) lpat
        ; tv_name <- newNameAt (mkTyVarOcc "r")   loc
        ; let rr_tv  = mkTcTyVar rr_name runtimeRepTy vanillaSkolemTv
              rr     = mkTyVarTy rr_tv
-             res_tv = mkTcTyVar tv_name (tYPEvis rr) vanillaSkolemTv
+             res_tv = mkTcTyVar tv_name (tYPE rr) vanillaSkolemTv
              res_ty = mkTyVarTy res_tv
              is_unlifted = null args && null prov_dicts
              (cont_args, cont_arg_tys)
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 6144ad9435..9fd160d72e 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -1729,7 +1729,7 @@ to ensure that instance declarations match.  For example consider
      instance Show (a->b)
      foo x = show (\_ -> True)
 
-Then we'll get a constraint (Show (p ->q)) where p has kind (TYPEvis r),
+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
 tc217 and tc175.
 
diff --git a/compiler/typecheck/TcTyClsDecls.hs b/compiler/typecheck/TcTyClsDecls.hs
index a3aea3b7ae..de866b7d84 100644
--- a/compiler/typecheck/TcTyClsDecls.hs
+++ b/compiler/typecheck/TcTyClsDecls.hs
@@ -273,7 +273,7 @@ Monad c in bop's type signature means that D must have kind Type->Type.
 Note: we don't treat type synonyms specially (we used to, in the past);
 in particular, even if we have a type synonym cycle, we still kind check
 it normally, and test for cycles later (checkSynCycles).  The reason
-we can get away with this is because we have more systematic TYPEvis r
+we can get away with this is because we have more systematic TYPE r
 inference, which means that we can do unification between kinds that
 aren't lifted (this historically was not true.)
 
@@ -2442,7 +2442,7 @@ checkValidClass cls
            -- a method cannot be levity polymorphic, as we have to store the
            -- method in a dictionary
            -- example of what this prevents:
-           --   class BoundedX (a :: TYPEvis r) where minBound :: a
+           --   class BoundedX (a :: TYPE r) where minBound :: a
            -- See Note [Levity polymorphism checking] in DsMonad
         ; checkForLevPoly empty tau1
 
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 12450bcf37..9302c7c58f 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -358,7 +358,7 @@ data InferResult
                             --           i.e. return a SigmaType
        , ir_ref  :: IORef (Maybe TcType) }
          -- The type that fills in this hole should be a Type,
-         -- that is, its kind should be (TYPEvis rr) for some rr
+         -- that is, its kind should be (TYPE rr) for some rr
 
 type ExpSigmaType = ExpType
 type ExpRhoType   = ExpType
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index 4dbec9903b..076f720214 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -52,7 +52,7 @@ import Name ( isSystemName )
 import Inst
 import TyCon
 import TysWiredIn
-import TysPrim( tYPEvis )
+import TysPrim( tYPE )
 import Var
 import VarSet
 import VarEnv
@@ -917,7 +917,7 @@ promoteTcType :: TcLevel -> TcType -> TcM (TcCoercion, TcType)
 -- promoteTcType level ty = (co, ty')
 --   * Returns ty'  whose max level is just 'level'
 --             and  whose kind is ~# to the kind of 'ty'
---             and  whose kind has form TYPE v rr
+--             and  whose kind has form TYPEV v rr
 --   * and co :: ty ~ ty'
 --   * and emits constraints to justify the coercion
 promoteTcType dest_lvl ty
@@ -930,7 +930,7 @@ promoteTcType dest_lvl ty
     promote_it  -- Emit a constraint  (alpha :: TYPE rr) ~ ty
                 -- where alpha and rr are fresh and from level dest_lvl
       = do { rr      <- newMetaTyVarTyAtLevel dest_lvl runtimeRepTy
-           ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPEvis rr)
+           ; prom_ty <- newMetaTyVarTyAtLevel dest_lvl (tYPE rr)
            ; let eq_orig = TypeEqOrigin { uo_actual   = ty
                                         , uo_expected = prom_ty
                                         , uo_thing    = Nothing }
@@ -939,7 +939,7 @@ promoteTcType dest_lvl ty
            ; return (co, prom_ty) }
 
     dont_promote_it :: TcM (TcCoercion, TcType)
-    dont_promote_it  -- Check that ty :: TYPEvis rr, for some (fresh) rr
+    dont_promote_it  -- Check that ty :: TYPE rr, for some (fresh) rr
       = do { res_kind <- newOpenTypeKind
            ; let ty_kind = typeKind ty
                  kind_orig = TypeEqOrigin { uo_actual   = ty_kind
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index 15573c195a..a5bc61a31b 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -388,7 +388,7 @@ checkTySynRhs ctxt ty
 -- | The kind expected in a certain context.
 data ContextKind = TheKind Kind   -- ^ a specific kind
                  | AnythingKind   -- ^ any kind will do
-                 | OpenKind       -- ^ something of the form @TYPEvis _@
+                 | OpenKind       -- ^ something of the form @TYPE _@
 
 -- Depending on the context, we might accept any kind (for instance, in a TH
 -- splice), or only certain kinds (like in type signatures).
diff --git a/compiler/types/Kind.hs b/compiler/types/Kind.hs
index 68ea16175f..b3b9b22afd 100644
--- a/compiler/types/Kind.hs
+++ b/compiler/types/Kind.hs
@@ -44,7 +44,7 @@ returnsConstraintKind = go
     go (FunTy    _ ty)  = go ty
     go other            = isConstraintKind other
 
--- | Tests whether the given kind (which should look like @TYPE v x@)
+-- | Tests whether the given kind (which should look like @TYPEV v x@)
 -- is something other than a constructor tree (that is, constructors at every node).
 isKindLevPoly :: Kind -> Bool
 isKindLevPoly k = ASSERT2( _is_type k, ppr k )
@@ -65,7 +65,7 @@ isKindLevPoly k = ASSERT2( _is_type k, ppr k )
       = _is_type ty'
 
       | TyConApp typ [_, _] <- ty
-      = typ `hasKey` tYPETyConKey
+      = typ `hasKey` tYPEVTyConKey
 
       | otherwise
       = False
@@ -90,16 +90,16 @@ okArrowResultKind = classifiesTypeWithValues
 -- indistinguishable
 
 -- | Does this classify a type allowed to have values? Responds True to things
--- like *, #, TYPEvis Lifted, TYPE v r, Constraint.
+-- like *, #, TYPE Lifted, TYPEV v r, Constraint.
 classifiesTypeWithValues :: Kind -> Bool
 classifiesTypeWithValues t | Just t' <- coreView t = classifiesTypeWithValues t'
-classifiesTypeWithValues (TyConApp tc [_,_]) = tc `hasKey` tYPETyConKey
+classifiesTypeWithValues (TyConApp tc [_,_]) = tc `hasKey` tYPEVTyConKey
 classifiesTypeWithValues _ = False
 
 {- Note [Levity polymorphism]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Is this type legal?
-   (a :: TYPEvis rep) -> Int
+   (a :: TYPE rep) -> Int
    where 'rep :: RuntimeRep'
 
 You might think not, because no lambda can have a
@@ -107,7 +107,7 @@ runtime-rep-polymorphic binder.  So no lambda has the
 above type.  BUT here's a way it can be useful (taken from
 Trac #12708):
 
-  data T rep (a :: TYPEvis rep)
+  data T rep (a :: TYPE rep)
      = MkT (a -> Int)
 
   x1 :: T LiftedRep Int
@@ -119,6 +119,6 @@ Trac #12708):
 Note that the lambdas are just fine!
 
 Hence, okArrowArgKind and okArrowResultKind both just
-check that the type is of the form (TYPEvis r) for some
+check that the type is of the form (TYPE r) for some
 representation type r.
 -}
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index e0ea62e4c7..3e3e1366f2 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -685,23 +685,23 @@ mkTyConTy tycon = TyConApp tycon []
 Some basic functions, put here to break loops eg with the pretty printer
 -}
 
-is_TYPE :: (   Type    -- the Visibility argument to TYPE; not a synonym
-            -> Type    -- the RuntimeRep argument to TYPE; not a synonym
-            -> Bool )  -- what to return
-        -> Kind -> Bool
-is_TYPE f ki | Just ki' <- coreView ki = is_TYPE f ki'
-is_TYPE f (TyConApp tc [vis, rep])
-  | tc `hasKey` tYPETyConKey
+is_TYPEV :: (   Type    -- the Visibility argument to TYPEV; not a synonym
+             -> Type    -- the RuntimeRep argument to TYPEV; not a synonym
+             -> Bool )  -- what to return
+         -> Kind -> Bool
+is_TYPEV f ki | Just ki' <- coreView ki = is_TYPEV f ki'
+is_TYPEV f (TyConApp tc [vis, rep])
+  | tc `hasKey` tYPEVTyConKey
   = go vis rep
     where
       go vis rep | Just vis' <- coreView vis = go vis' rep
                  | Just rep' <- coreView rep = go vis  rep'
                  | otherwise                 = f  vis  rep
-is_TYPE _ _ = False
+is_TYPEV _ _ = False
 
 -- | Returns True if the argument is equivalent to Type and False otherwise.
 isLiftedTypeKind :: Kind -> Bool
-isLiftedTypeKind = is_TYPE is_lifted
+isLiftedTypeKind = is_TYPEV is_lifted
   where
     is_lifted (TyConApp vis []) (TyConApp lifted_rep [])
       = vis `hasKey` visibleDataConKey && lifted_rep `hasKey` liftedRepDataConKey
@@ -711,14 +711,14 @@ isLiftedTypeKind = is_TYPE is_lifted
 -- Note that this returns False for levity-polymorphic kinds, which may
 -- be specialized to a kind that classifies unlifted types.
 isUnliftedTypeKind :: Kind -> Bool
-isUnliftedTypeKind = is_TYPE is_unlifted
+isUnliftedTypeKind = is_TYPEV is_unlifted
   where
     is_unlifted _ (TyConApp rr _args) = not (isLiftedRuntimeRepTyCon rr)
     is_unlifted _ _                   = False
 
 -- | Returns True if this kind is Constraint
 isConstraintKind :: Kind -> Bool
-isConstraintKind = is_TYPE is_constraint
+isConstraintKind = is_TYPEV is_constraint
   where
     is_constraint (TyConApp invis []) (TyConApp constraint_rep [])
       = invis `hasKey` invisibleDataConKey && constraint_rep `hasKey` liftedRepDataConKey
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index a6f9b529dc..4a5a6a2e3f 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -346,7 +346,8 @@ the kind of the unboxed tuple constructor is levity
 polymorphic. For example,
 
    (#,#) :: forall (v1 :: Visibility) (v2 :: Visbiility)
-                   (q :: RuntimeRep) (r :: RuntimeRep). TYPE v1 q -> TYPE v2 r -> #
+                   (q :: RuntimeRep) (r :: RuntimeRep). TYPEV v1 q -> TYPEV v2 r
+                -> TYPE (TupleRep [q,r])
 
 These extra tyvars cause some delicate processing around tuples,
 where we used to be able to assume that the tycon arity and the
@@ -2007,7 +2008,7 @@ isKindTyCon tc = getUnique tc `elementOfUniqSet` kindTyConKeys
 kindTyConKeys :: UniqSet Unique
 kindTyConKeys = unionManyUniqSets
   ( mkUniqSet [ liftedTypeKindTyConKey, starKindTyConKey, unicodeStarKindTyConKey
-              , constraintKindTyConKey, tYPETyConKey ]
+              , constraintKindTyConKey, tYPEVTyConKey ]
   : map (mkUniqSet . tycon_with_datacons) [ runtimeRepTyCon, visibilityTyCon
                                           , vecCountTyCon, vecElemTyCon ] )
   where
@@ -2065,7 +2066,7 @@ isTcTyCon _            = False
 -- | Could this TyCon ever be levity-polymorphic when fully applied?
 -- True is safe. False means we're sure. Does only a quick check
 -- based on the TyCon's category.
--- Precondition: The fully-applied TyCon has kind (TYPE v blah)
+-- Precondition: The fully-applied TyCon has kind (TYPEV v blah)
 isTcLevPoly :: TyCon -> Bool
 isTcLevPoly FunTyCon{}           = False
 isTcLevPoly (AlgTyCon { algTcParent = UnboxedAlgTyCon }) = True
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index a0061ce58f..10427e77b2 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -1837,7 +1837,7 @@ isFamFreeTy (CoercionTy _)    = False  -- Not sure about this
 -- | Returns Just True if this type is surely lifted, Just False
 -- if it is surely unlifted, Nothing if we can't be sure (i.e., it is
 -- levity polymorphic), and panics if the kind does not have the shape
--- TYPE v r.
+-- TYPEV v r.
 isLiftedType_maybe :: HasDebugCallStack => Type -> Maybe Bool
 isLiftedType_maybe ty = go (getRuntimeRep "isLiftedType_maybe" ty)
   where
@@ -1888,7 +1888,7 @@ getVisRuntimeRepFromKind err = go
     go k | Just k' <- coreView k = go k'
     go k
       | (_tc, [vis, arg]) <- splitTyConApp k
-      = ASSERT2( _tc `hasKey` tYPETyConKey, text err $$ ppr k )
+      = ASSERT2( _tc `hasKey` tYPEVTyConKey, text err $$ ppr k )
         (vis, arg)
     go k = pprPanic "getRuntimeRep" (text err $$
                                      ppr k <+> dcolon <+> ppr (typeKind k))
@@ -2175,7 +2175,7 @@ typeLiteralKind l =
 
 -- | Returns True if a type is levity polymorphic. Should be the same
 -- as (isKindLevPoly . typeKind) but much faster.
--- Precondition: The type has kind (TYPE v blah)
+-- Precondition: The type has kind (TYPEV v blah)
 isTypeLevPoly :: Type -> Bool
 isTypeLevPoly = go
   where
@@ -2192,8 +2192,8 @@ isTypeLevPoly = go
     check_kind = isKindLevPoly . typeKind
 
 -- | Looking past all pi-types, is the end result potentially levity polymorphic?
--- Example: True for (forall r (a :: TYPEvis r). String -> a)
--- Example: False for (forall r1 r2 (a :: TYPEvis r1) (b :: TYPEvis r2). a -> b -> Type)
+-- Example: True for (forall r (a :: TYPE r). String -> a)
+-- Example: False for (forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). a -> b -> Type)
 resultIsLevPoly :: Type -> Bool
 resultIsLevPoly = isTypeLevPoly . snd . splitPiTys
 
diff --git a/libraries/base/Data/Typeable/Internal.hs b/libraries/base/Data/Typeable/Internal.hs
index 418e0d9f9a..7caf5e1285 100644
--- a/libraries/base/Data/Typeable/Internal.hs
+++ b/libraries/base/Data/Typeable/Internal.hs
@@ -63,7 +63,7 @@ module Data.Typeable.Internal (
   ) where
 
 import GHC.Base
-import GHC.Types (TYPE)
+import GHC.Types (TYPEV)
 import GHC.Word
 import GHC.Show
 import Data.Proxy
@@ -355,11 +355,11 @@ instance Show TypeRep where
         where
           tcList = tyConOf @[] Proxy
       [TypeRep _ visCon _ [], TypeRep _ ptrRepCon _ []]
-        | tycon == tcTYPE && ptrRepCon == tc'LiftedRep
+        | tycon == tcTYPEV && ptrRepCon == tc'LiftedRep
           -> if visCon == tc'Visible then showChar '*'
                                      else showString "Constraint"
         where
-          tcTYPE         = tyConOf @TYPE            Proxy
+          tcTYPEV        = tyConOf @TYPEV           Proxy
           tc'LiftedRep   = tyConOf @'LiftedRep      Proxy
           tc'Visible     = tyConOf @'Visible        Proxy
       [a,r] | tycon == tcFun  -> showParen (p > 8) $
diff --git a/libraries/base/GHC/Err.hs b/libraries/base/GHC/Err.hs
index e1c0c206c0..2e68095940 100644
--- a/libraries/base/GHC/Err.hs
+++ b/libraries/base/GHC/Err.hs
@@ -24,7 +24,7 @@
 
 module GHC.Err( absentErr, error, errorWithoutStackTrace, undefined ) where
 import GHC.CString ()
-import GHC.Types (Char, RuntimeRep, TYPEvis)
+import GHC.Types (Char, RuntimeRep, TYPE)
 import GHC.Stack.Types
 import GHC.Prim
 import GHC.Integer ()   -- Make sure Integer is compiled first
@@ -33,7 +33,7 @@ import GHC.Integer ()   -- Make sure Integer is compiled first
 import {-# SOURCE #-} GHC.Exception( errorCallWithCallStackException )
 
 -- | 'error' stops execution and displays an error message.
-error :: forall (r :: RuntimeRep). forall (a :: TYPEvis r).
+error :: forall (r :: RuntimeRep). forall (a :: TYPE r).
          HasCallStack => [Char] -> a
 error s = raise# (errorCallWithCallStackException s ?callStack)
           -- Bleh, we should be using 'GHC.Stack.callStack' instead of
@@ -44,7 +44,7 @@ error s = raise# (errorCallWithCallStackException s ?callStack)
 -- | A variant of 'error' that does not produce a stack trace.
 --
 -- @since 4.9.0.0
-errorWithoutStackTrace :: forall (r :: RuntimeRep). forall (a :: TYPEvis r).
+errorWithoutStackTrace :: forall (r :: RuntimeRep). forall (a :: TYPE r).
                           [Char] -> a
 errorWithoutStackTrace s =
   -- we don't have withFrozenCallStack yet, so we just inline the definition
@@ -74,7 +74,7 @@ errorWithoutStackTrace s =
 -- It is expected that compilers will recognize this and insert error
 -- messages which are more appropriate to the context in which 'undefined'
 -- appears.
-undefined :: forall (r :: RuntimeRep). forall (a :: TYPEvis r).
+undefined :: forall (r :: RuntimeRep). forall (a :: TYPE r).
              HasCallStack => a
 undefined =  error "Prelude.undefined"
 
diff --git a/libraries/base/GHC/Exts.hs b/libraries/base/GHC/Exts.hs
index 03d81bf225..ff471a2c3f 100755
--- a/libraries/base/GHC/Exts.hs
+++ b/libraries/base/GHC/Exts.hs
@@ -60,7 +60,7 @@ module GHC.Exts
         type (~~),
 
         -- * Representation polymorphism
-        GHC.Prim.TYPE, TYPEvis, RuntimeRep(..), Visibility(..), VecCount(..), VecElem(..),
+        GHC.Prim.TYPEV, TYPE, RuntimeRep(..), Visibility(..), VecCount(..), VecElem(..),
 
         -- * Transform comprehensions
         Down(..), groupWith, sortWith, the,
@@ -84,7 +84,7 @@ module GHC.Exts
         IsList(..)
        ) where
 
-import GHC.Prim hiding ( coerce, TYPE )
+import GHC.Prim hiding ( coerce, TYPEV )
 import qualified GHC.Prim
 import GHC.Base hiding ( coerce )
 import GHC.Word
diff --git a/libraries/base/tests/T11334a.hs b/libraries/base/tests/T11334a.hs
index 6e1cbe7373..8b117a4ba7 100644
--- a/libraries/base/tests/T11334a.hs
+++ b/libraries/base/tests/T11334a.hs
@@ -7,6 +7,6 @@ import GHC.Types
 main :: IO ()
 main = do
   print (typeOf (Proxy :: Proxy 'Just))
-  print (typeOf (Proxy :: Proxy (TYPE 'Visible 'LiftedRep)))
-  print (typeOf (Proxy :: Proxy (TYPE 'Invisible 'LiftedRep)))
-  print (typeOf (Proxy :: Proxy (TYPE 'Visible 'UnliftedRep)))
+  print (typeOf (Proxy :: Proxy (TYPEV 'Visible 'LiftedRep)))
+  print (typeOf (Proxy :: Proxy (TYPEV 'Invisible 'LiftedRep)))
+  print (typeOf (Proxy :: Proxy (TYPEV 'Visible 'UnliftedRep)))
diff --git a/libraries/ghc-prim/GHC/Types.hs b/libraries/ghc-prim/GHC/Types.hs
index 9561c25df9..03d4704b69 100644
--- a/libraries/ghc-prim/GHC/Types.hs
+++ b/libraries/ghc-prim/GHC/Types.hs
@@ -32,8 +32,8 @@ module GHC.Types (
         Nat, Symbol,
         Any,
         type (~~), Coercible,
-        TYPE, RuntimeRep(..), Visibility(..), Type, type (*), type (★), Constraint,
-        TYPEvis,
+        TYPEV, RuntimeRep(..), Visibility(..), Type, type (*), type (★), Constraint,
+        TYPE,
           -- The historical type * should ideally be written as
           -- `type *`, without the parentheses. But that's a true
           -- pain to parse, and for little gain.
@@ -58,19 +58,19 @@ infixr 5 :
 ********************************************************************* -}
 
 -- | The kind of constraints, like @Show a@
-type Constraint = TYPE 'Invisible 'LiftedRep
+type Constraint = TYPEV 'Invisible 'LiftedRep
 
 -- | The kind of types with values. For example @Int :: Type@.
-type Type = TYPE 'Visible 'LiftedRep
+type Type = TYPE 'LiftedRep
 
 -- | A backward-compatible (pre-GHC 8.0) synonym for 'Type'
-type * = TYPE 'Visible 'LiftedRep
+type * = TYPE 'LiftedRep
 
 -- | A unicode backward-compatible (pre-GHC 8.0) synonym for 'Type'
-type ★ = TYPE 'Visible 'LiftedRep
+type ★ = TYPE 'LiftedRep
 
 -- | The kind of visible types, but with a configurable representation.
-type TYPEvis = TYPE 'Visible
+type TYPE = TYPEV 'Visible
 
 {- *********************************************************************
 *                                                                      *
diff --git a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
index 419d333661..0da0c2f884 100644
--- a/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
+++ b/testsuite/tests/dependent/should_compile/RaeJobTalk.hs
@@ -80,7 +80,7 @@ data TyCon (a :: k) where
   List :: TyCon []
   Maybe :: TyCon Maybe
   Arrow :: TyCon (->)
-  TYPE  :: TyCon TYPE
+  TYPEV  :: TyCon TYPEV
   RuntimeRep :: TyCon RuntimeRep
   Visibility :: TyCon Visibility
   LiftedRep' :: TyCon 'LiftedRep
@@ -94,7 +94,7 @@ eqTyCon Char Char = Just HRefl
 eqTyCon List List = Just HRefl
 eqTyCon Maybe Maybe = Just HRefl
 eqTyCon Arrow Arrow = Just HRefl
-eqTyCon TYPE TYPE = Just HRefl
+eqTyCon TYPEV TYPEV = Just HRefl
 eqTyCon RuntimeRep RuntimeRep = Just HRefl
 eqTyCon Visibility Visibility = Just HRefl
 eqTyCon LiftedRep' LiftedRep' = Just HRefl
@@ -215,7 +215,7 @@ instance TyConAble Char      where tyCon = Char
 instance TyConAble []        where tyCon = List
 instance TyConAble Maybe     where tyCon = Maybe
 instance TyConAble (->)      where tyCon = Arrow
-instance TyConAble TYPE      where tyCon = TYPE
+instance TyConAble TYPEV      where tyCon = TYPEV
 instance TyConAble 'LiftedRep   where tyCon = LiftedRep'
 instance TyConAble RuntimeRep    where tyCon = RuntimeRep
 instance TyConAble Visibility where tyCon = Visibility
diff --git a/testsuite/tests/dependent/should_compile/T11405.hs b/testsuite/tests/dependent/should_compile/T11405.hs
index f4260cf27c..cdb713f118 100644
--- a/testsuite/tests/dependent/should_compile/T11405.hs
+++ b/testsuite/tests/dependent/should_compile/T11405.hs
@@ -5,5 +5,5 @@ module T11405 where
 import GHC.Exts
 import GHC.Stack
 
-x :: forall (v :: RuntimeRep) (a :: TYPEvis v). (?callStack :: CallStack) => a
+x :: forall (v :: RuntimeRep) (a :: TYPE v). (?callStack :: CallStack) => a
 x = undefined
diff --git a/testsuite/tests/dependent/should_fail/T11473.hs b/testsuite/tests/dependent/should_fail/T11473.hs
index b37020d135..12d95caac6 100644
--- a/testsuite/tests/dependent/should_fail/T11473.hs
+++ b/testsuite/tests/dependent/should_fail/T11473.hs
@@ -9,13 +9,13 @@ type family Boxed (a :: k) :: *
 type instance Boxed Char# = Char
 type instance Boxed Char  = Char
 
-class BoxIt (a :: TYPEvis lev) where
+class BoxIt (a :: TYPE lev) where
     boxed :: a -> Boxed a
 
 instance BoxIt Char# where boxed x = C# x
 instance BoxIt Char  where boxed = id
 
-hello :: forall (r :: RuntimeRep). forall (a :: TYPEvis r). BoxIt a => a -> Boxed a
+hello :: forall (r :: RuntimeRep). forall (a :: TYPE r). BoxIt a => a -> Boxed a
 hello x = boxed x
 {-# NOINLINE hello #-}
 
diff --git a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
index adde8cf2ca..bbec037487 100644
--- a/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
+++ b/testsuite/tests/dependent/should_fail/TypeSkolEscape.hs
@@ -5,4 +5,4 @@ module TypeSkolEscape where
 import GHC.Types
 import GHC.Exts
 
-type Bad = forall (v :: RuntimeRep) (a :: TYPEvis v). a
+type Bad = forall (v :: RuntimeRep) (a :: TYPE v). a
diff --git a/testsuite/tests/deriving/should_fail/T12512.hs b/testsuite/tests/deriving/should_fail/T12512.hs
index f943c905e8..4d4e52c06c 100644
--- a/testsuite/tests/deriving/should_fail/T12512.hs
+++ b/testsuite/tests/deriving/should_fail/T12512.hs
@@ -6,8 +6,8 @@ module T12512 where
 
 import GHC.Exts
 
-class Wat1 (a :: TYPEvis ('TupleRep ['LiftedRep, 'LiftedRep]))
+class Wat1 (a :: TYPE ('TupleRep ['LiftedRep, 'LiftedRep]))
 deriving instance Wat1 (# a, b #)
 
-class Wat2 (a :: TYPEvis ('SumRep ['LiftedRep, 'LiftedRep]))
+class Wat2 (a :: TYPE ('SumRep ['LiftedRep, 'LiftedRep]))
 deriving instance Wat2 (# a | b #)
diff --git a/testsuite/tests/indexed-types/should_run/T11465a.hs b/testsuite/tests/indexed-types/should_run/T11465a.hs
index 48fd10b441..d3626cf198 100644
--- a/testsuite/tests/indexed-types/should_run/T11465a.hs
+++ b/testsuite/tests/indexed-types/should_run/T11465a.hs
@@ -7,7 +7,7 @@
 import GHC.Exts
 import GHC.Types
 
-class BoxIt (a :: TYPEvis 'WordRep) where
+class BoxIt (a :: TYPE 'WordRep) where
     type Boxed a :: *
     boxed :: a -> Boxed a
 
diff --git a/testsuite/tests/polykinds/T12668.hs b/testsuite/tests/polykinds/T12668.hs
index 79a7b67f45..4640903cc5 100644
--- a/testsuite/tests/polykinds/T12668.hs
+++ b/testsuite/tests/polykinds/T12668.hs
@@ -5,9 +5,9 @@ module T12668 where
 
 import GHC.Exts
 
-data Some r = Some (TYPEvis r -> TYPEvis r)
+data Some r = Some (TYPE r -> TYPE r)
 
-doSomething :: forall (r :: RuntimeRep). forall (a :: TYPEvis r). ()
+doSomething :: forall (r :: RuntimeRep). forall (a :: TYPE r). ()
             => Int -> (a -> Int) -> a -> a
 doSomething n f =
     case n of
diff --git a/testsuite/tests/polykinds/T12718.hs b/testsuite/tests/polykinds/T12718.hs
index fd1e2c7691..82d6dcd177 100644
--- a/testsuite/tests/polykinds/T12718.hs
+++ b/testsuite/tests/polykinds/T12718.hs
@@ -8,7 +8,7 @@ import qualified Prelude as P
 import GHC.Prim
 import GHC.Types
 
-class XNum (a :: TYPEvis rep) where
+class XNum (a :: TYPE rep) where
   (+) :: a -> a -> a
   fromInteger :: Integer -> a
 
@@ -24,7 +24,7 @@ instance XNum Int# where
 u :: Bool
 u = isTrue# v_
   where
-    v_ :: forall rep (a :: TYPEvis rep). XNum a => a
+    v_ :: forall rep (a :: TYPE rep). XNum a => a
     v_ = fromInteger 10
 
 main = print u
diff --git a/testsuite/tests/typecheck/should_compile/T11723.hs b/testsuite/tests/typecheck/should_compile/T11723.hs
index 53a6a75b26..1933024f2e 100644
--- a/testsuite/tests/typecheck/should_compile/T11723.hs
+++ b/testsuite/tests/typecheck/should_compile/T11723.hs
@@ -4,4 +4,4 @@ module Example where
 import Data.Typeable
 import GHC.Exts
 
-data Wat (a :: TYPEvis ('TupleRep '[])) = Wat a
+data Wat (a :: TYPE ('TupleRep '[])) = Wat a
diff --git a/testsuite/tests/typecheck/should_compile/T12911.hs b/testsuite/tests/typecheck/should_compile/T12911.hs
index bd45305696..88c2125f2b 100644
--- a/testsuite/tests/typecheck/should_compile/T12911.hs
+++ b/testsuite/tests/typecheck/should_compile/T12911.hs
@@ -6,4 +6,4 @@ module T12911 where
 import GHC.Exts
 
 data X where
-  MkX :: forall (a :: TYPEvis r). (a -> a) -> X
+  MkX :: forall (a :: TYPE r). (a -> a) -> X
diff --git a/testsuite/tests/typecheck/should_compile/T12987.hs b/testsuite/tests/typecheck/should_compile/T12987.hs
index bcddf3456b..0997985601 100644
--- a/testsuite/tests/typecheck/should_compile/T12987.hs
+++ b/testsuite/tests/typecheck/should_compile/T12987.hs
@@ -4,4 +4,4 @@ module T12987 where
 
 import GHC.Exts
 
-class NUM (a :: TYPEvis rep) where add :: a -> a -> a
+class NUM (a :: TYPE rep) where add :: a -> a -> a
diff --git a/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs b/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs
index 70c75ad49a..0607956784 100644
--- a/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs
+++ b/testsuite/tests/typecheck/should_fail/LevPolyBounded.hs
@@ -6,6 +6,6 @@ module LevPolyBounded where
 
 import GHC.Exts
 
-class XBounded (a :: TYPEvis r) where
+class XBounded (a :: TYPE r) where
   minBound :: a
   maxBound :: a
diff --git a/testsuite/tests/typecheck/should_fail/T11724.hs b/testsuite/tests/typecheck/should_fail/T11724.hs
index b5f038534f..df575bd9b5 100644
--- a/testsuite/tests/typecheck/should_fail/T11724.hs
+++ b/testsuite/tests/typecheck/should_fail/T11724.hs
@@ -4,4 +4,4 @@ module T11724 where
 
 import GHC.Exts
 
-data Foo (r :: RuntimeRep) (a :: TYPEvis r) = Foo a
+data Foo (r :: RuntimeRep) (a :: TYPE r) = Foo a
diff --git a/testsuite/tests/typecheck/should_fail/T12973.hs b/testsuite/tests/typecheck/should_fail/T12973.hs
index a21ed1a0c1..c088265ffb 100644
--- a/testsuite/tests/typecheck/should_fail/T12973.hs
+++ b/testsuite/tests/typecheck/should_fail/T12973.hs
@@ -5,9 +5,9 @@ module T12973 where
 import qualified Prelude as P
 import GHC.Exts
 
-class Num (a :: TYPEvis r) where
+class Num (a :: TYPE r) where
   (+) :: a -> a -> a
   fromInteger :: P.Integer -> a
 
-foo :: forall (a :: TYPEvis r). Num a => a
+foo :: forall (a :: TYPE r). Num a => a
 foo = 3 + 4
diff --git a/testsuite/tests/typecheck/should_fail/T13105.hs b/testsuite/tests/typecheck/should_fail/T13105.hs
index 0bbdd4cd13..44384dc19d 100644
--- a/testsuite/tests/typecheck/should_fail/T13105.hs
+++ b/testsuite/tests/typecheck/should_fail/T13105.hs
@@ -11,7 +11,7 @@ import GHC.Exts
 type family RepRep a ∷ RuntimeRep
 
 class HasRep a where
-  type Rep a ∷ TYPEvis (RepRep a)
+  type Rep a ∷ TYPE (RepRep a)
   repr ∷ a → Rep a
   abst ∷ Rep a → a
 
diff --git a/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
index 7222070e07..e912411209 100644
--- a/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
+++ b/testsuite/tests/typecheck/should_run/EtaExpandLevPoly.hs
@@ -10,16 +10,16 @@ data G a where
 
 -- tests that we don't eta-expand functions that are levity-polymorphic
 -- see CoreArity.mkEtaWW
-foo :: forall a (b :: TYPEvis a). G a -> b -> b
-foo MkG = (\x -> x) :: forall (c :: TYPEvis (TupleRep [LiftedRep, IntRep])). c -> c
+foo :: forall a (b :: TYPE a). G a -> b -> b
+foo MkG = (\x -> x) :: forall (c :: TYPE (TupleRep [LiftedRep, IntRep])). c -> c
 
 data H a where
   MkH :: H IntRep
 
 -- tests that we don't push coercions that make args levity-polymorphic
 -- see Simplify.simplCast
-bar :: forall (r :: RuntimeRep) (a :: TYPEvis r). H r -> (a -> a -> (# a, a #)) -> a -> (# a, a #)
-bar MkH = (\f x -> f x x) :: forall (b :: TYPEvis IntRep). (b -> b -> (# b, b #)) -> b -> (# b, b #)
+bar :: forall (r :: RuntimeRep) (a :: TYPE r). H r -> (a -> a -> (# a, a #)) -> a -> (# a, a #)
+bar MkH = (\f x -> f x x) :: forall (b :: TYPE IntRep). (b -> b -> (# b, b #)) -> b -> (# b, b #)
 
 main :: IO ()
 main = do
diff --git a/testsuite/tests/typecheck/should_run/T12809.hs b/testsuite/tests/typecheck/should_run/T12809.hs
index 2468f34f1b..9f6da26d76 100644
--- a/testsuite/tests/typecheck/should_run/T12809.hs
+++ b/testsuite/tests/typecheck/should_run/T12809.hs
@@ -5,7 +5,7 @@ module Main where
 
 import GHC.Exts
 
-idint :: forall (a :: TYPEvis IntRep). a -> a
+idint :: forall (a :: TYPE IntRep). a -> a
 idint x = x
 
 five _ = idint 3# +# idint 2#
@@ -32,7 +32,7 @@ g (# b, x #) = show b ++ " " ++ show (I# x)
 h :: (# Double, Int# #) -> String
 h (# d, x #) = show d ++ " " ++ show (I# x)
 
-cond :: forall (a :: TYPEvis (TupleRep [LiftedRep, IntRep])). Bool -> a -> a -> a
+cond :: forall (a :: TYPE (TupleRep [LiftedRep, IntRep])). Bool -> a -> a -> a
 cond True x _ = x
 cond False _ x = x
 
diff --git a/testsuite/tests/typecheck/should_run/TypeOf.hs b/testsuite/tests/typecheck/should_run/TypeOf.hs
index 0ba4047671..5aadf15f22 100644
--- a/testsuite/tests/typecheck/should_run/TypeOf.hs
+++ b/testsuite/tests/typecheck/should_run/TypeOf.hs
@@ -26,8 +26,8 @@ main = do
   print $ typeOf (Proxy :: Proxy 1)
   print $ typeOf (Proxy :: Proxy [1,2,3])
   print $ typeOf (Proxy :: Proxy 'EQ)
-  print $ typeOf (Proxy :: Proxy TYPE)
-  print $ typeOf (Proxy :: Proxy (TYPEvis 'LiftedRep))
+  print $ typeOf (Proxy :: Proxy TYPEV)
+  print $ typeOf (Proxy :: Proxy (TYPE 'LiftedRep))
   print $ typeOf (Proxy :: Proxy *)
   print $ typeOf (Proxy :: Proxy ★)
   print $ typeOf (Proxy :: Proxy 'LiftedRep)
diff --git a/testsuite/tests/typecheck/should_run/TypeRep.hs b/testsuite/tests/typecheck/should_run/TypeRep.hs
index 81a9f3cc44..b4ca77ee96 100644
--- a/testsuite/tests/typecheck/should_run/TypeRep.hs
+++ b/testsuite/tests/typecheck/should_run/TypeRep.hs
@@ -38,8 +38,8 @@ main = do
   print $ rep @(Proxy 1)
   print $ rep @(Proxy [1,2,3])
   print $ rep @(Proxy 'EQ)
-  print $ rep @(Proxy TYPE)
-  print $ rep @(Proxy (TYPEvis 'LiftedRep))
+  print $ rep @(Proxy TYPEV)
+  print $ rep @(Proxy (TYPE 'LiftedRep))
   print $ rep @(Proxy *)
   print $ rep @(Proxy ★)
   print $ rep @(Proxy 'LiftedRep)
diff --git a/testsuite/tests/unboxedsums/UbxSumLevPoly.hs b/testsuite/tests/unboxedsums/UbxSumLevPoly.hs
index e9402bf3b9..3275eb7dfe 100644
--- a/testsuite/tests/unboxedsums/UbxSumLevPoly.hs
+++ b/testsuite/tests/unboxedsums/UbxSumLevPoly.hs
@@ -2,7 +2,7 @@
 
 module UbxSumLevPoly where
 
--- this failed thinking that (# Any | True #) :: TYPEvis (SumRep [LiftedRep, b])
+-- this failed thinking that (# Any | True #) :: TYPE (SumRep [LiftedRep, b])
 -- But of course that b should be Lifted!
 
 -- It was due to silliness in TysWiredIn using the same uniques for different
diff --git a/testsuite/tests/unboxedsums/sum_rr.hs b/testsuite/tests/unboxedsums/sum_rr.hs
index 62fa27a326..5f799fe481 100644
--- a/testsuite/tests/unboxedsums/sum_rr.hs
+++ b/testsuite/tests/unboxedsums/sum_rr.hs
@@ -5,4 +5,4 @@ module Example where
 import Data.Typeable
 import GHC.Exts
 
-data Wat (a :: TYPEvis (SumRep '[LiftedRep, IntRep])) = Wat a
+data Wat (a :: TYPE (SumRep '[LiftedRep, IntRep])) = Wat a