diff --git a/compiler/prelude/TysPrim.lhs b/compiler/prelude/TysPrim.lhs
index ae9a11ebfed4a919d32b26387a481cad9fd2daf8..0547c910fe2dff86c25ad5baebff91dcbe0e8855 100644
--- a/compiler/prelude/TysPrim.lhs
+++ b/compiler/prelude/TysPrim.lhs
@@ -701,7 +701,7 @@ threadIdPrimTyCon = pcPrimTyCon0 threadIdPrimTyConName PtrRep
 
 Note [Any types]
 ~~~~~~~~~~~~~~~~
-The type constructor Any of kind forall k. k -> k has these properties:
+The type constructor Any of kind forall k. k has these properties:
 
   * It is defined in module GHC.Prim, and exported so that it is 
     available to users.  For this reason it's treated like any other 
@@ -714,7 +714,7 @@ The type constructor Any of kind forall k. k -> k has these properties:
              g :: ty ~ (Fst ty, Snd ty)
     If Any was a *data* type, then we'd get inconsistency because 'ty'
     could be (Any '(k1,k2)) and then we'd have an equality with Any on
-    one side and '(,) on the other
+    one side and '(,) on the other. See also #9097.
 
   * It is lifted, and hence represented by a pointer
 
@@ -771,20 +771,12 @@ anyTy :: Type
 anyTy = mkTyConTy anyTyCon
 
 anyTyCon :: TyCon
-anyTyCon = mkLiftedPrimTyCon anyTyConName kind [Nominal] PtrRep
-  where kind = ForAllTy kKiVar (mkTyVarTy kKiVar)
-
-{-   Can't do this yet without messing up kind proxies
--- RAE: I think you can now.
-anyTyCon :: TyCon
-anyTyCon = mkSynTyCon anyTyConName kind [kKiVar] 
+anyTyCon = mkSynTyCon anyTyConName kind [kKiVar] [Nominal]
                       syn_rhs
                       NoParentTyCon
   where 
     kind = ForAllTy kKiVar (mkTyVarTy kKiVar)
-    syn_rhs = SynFamilyTyCon { synf_open = False, synf_injective = True }
-                  -- NB Closed, injective
--}
+    syn_rhs = AbstractClosedSynFamilyTyCon
 
 anyTypeOfKind :: Kind -> Type
 anyTypeOfKind kind = TyConApp anyTyCon [kind]
diff --git a/compiler/prelude/primops.txt.pp b/compiler/prelude/primops.txt.pp
index 764ba103f23186961aca1d9ac2d943be609362d8..4851315eb488c89f4a6b2fa425a31e8898c001cf 100644
--- a/compiler/prelude/primops.txt.pp
+++ b/compiler/prelude/primops.txt.pp
@@ -2437,7 +2437,7 @@ pseudoop   "seq"
    { Evaluates its first argument to head normal form, and then returns its second
 	argument as the result. }
 
-primtype Any k
+primtype Any
 	{ The type constructor {\tt Any} is type to which you can unsafely coerce any
 	lifted type, and back.
 
@@ -2462,8 +2462,11 @@ primtype Any k
 
 	{\tt length (Any *) ([] (Any *))}
 
-        Note that {\tt Any} is kind polymorphic, and takes a kind {\tt k} as its
-        first argument. The kind of {\tt Any} is thus {\tt forall k. k -> k}.}
+        Above, we print kinds explicitly, as if with
+        {\tt -fprint-explicit-kinds}.
+
+        Note that {\tt Any} is kind polymorphic; its kind is thus
+        {\tt forall k. k}.}
 
 primtype AnyK
         { The kind {\tt AnyK} is the kind level counterpart to {\tt Any}. In a