Kill the magic of Any

This turns `Any` into a standard wired-in type family defined in
`GHC.Types`, instead its current incarnation as a magical creature
provided by the `GHC.Prim`.  Also kill `AnyK`.

See #10886.

Test Plan: Validate

Reviewers: simonpj, goldfire, austin, hvr

Reviewed By: simonpj

Subscribers: goldfire, thomie

Differential Revision: https://phabricator.haskell.org/D2049

GHC Trac Issues: #10886

1 files changed, 87 insertions, 0 deletions

diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index 067b32b686..6fbb8212f5 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -67,6 +67,9 @@ module TysWiredIn (
         unboxedUnitTyCon, unboxedUnitDataCon,
         cTupleTyConName, cTupleTyConNames, isCTupleTyConName,
 
+        -- * Any
+        anyTyCon, anyTy, anyTypeOfKind,
+
         -- * Kinds
         typeNatKindCon, typeNatKind, typeSymbolKindCon, typeSymbolKind,
         isLiftedTypeKindTyConName, liftedTypeKind, constraintKind,
@@ -127,6 +130,7 @@ import Type
 import DataCon
 import {-# SOURCE #-} ConLike
 import TyCon
+import TyCoRep          ( TyBinder(..) )
 import Class            ( Class, mkClass )
 import RdrName
 import Name
@@ -187,6 +191,7 @@ wiredInTyCons = [ unitTyCon     -- Not treated like other tuples, because
                                 -- that it'll pre-populate the name cache, so
                                 -- the special case in lookupOrigNameCache
                                 -- doesn't need to look out for it
+              , anyTyCon
               , boolTyCon
               , charTyCon
               , doubleTyCon
@@ -275,6 +280,88 @@ floatDataConName   = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "F#")
 doubleTyConName    = mkWiredInTyConName   UserSyntax gHC_TYPES (fsLit "Double") doubleTyConKey   doubleTyCon
 doubleDataConName  = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "D#")     doubleDataConKey doubleDataCon
 
+-- Any
+
+{-
+Note [Any types]
+~~~~~~~~~~~~~~~~
+The type constructor Any,
+
+    type family Any :: k where { }
+
+It has these properties:
+
+  * It is defined in module GHC.Types, and exported so that it is
+    available to users.  For this reason it's treated like any other
+    wired-in type:
+      - has a fixed unique, anyTyConKey,
+      - lives in the global name cache
+
+  * It is a *closed* type family, with no instances.  This means that
+    if   ty :: '(k1, k2)  we add a given coercion
+             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. See also #9097 and #9636.
+
+  * When instantiated at a lifted type it is inhabited by at least one value,
+    namely bottom
+
+  * You can safely coerce any lifted type to Any, and back with unsafeCoerce.
+
+  * It does not claim to be a *data* type, and that's important for
+    the code generator, because the code gen may *enter* a data value
+    but never enters a function value.
+
+  * It is wired-in so we can easily refer to it where we don't have a name
+    environment (e.g. see Rules.matchRule for one example)
+
+It's used to instantiate un-constrained type variables after type checking. For
+example, 'length' has type
+
+  length :: forall a. [a] -> Int
+
+and the list datacon for the empty list has type
+
+  [] :: forall a. [a]
+
+In order to compose these two terms as @length []@ a type
+application is required, but there is no constraint on the
+choice.  In this situation GHC uses 'Any',
+
+> length (Any *) ([] (Any *))
+
+Above, we print kinds explicitly, as if with --fprint-explicit-kinds.
+
+Note that 'Any' is kind polymorphic since in some program we may need to use Any
+to fill in a type variable of some kind other than * (see #959 for examples).
+Its kind is thus `forall k. k``.
+
+The Any tycon used to be quite magic, but we have since been able to
+implement it merely with an empty kind polymorphic type family. See #10886 for a
+bit of history.
+-}
+
+
+anyTyConName :: Name
+anyTyConName =
+    mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Any") anyTyConKey anyTyCon
+
+anyTyCon :: TyCon
+anyTyCon = mkFamilyTyCon anyTyConName binders res_kind [kKiVar] Nothing
+                         (ClosedSynFamilyTyCon Nothing)
+                         Nothing
+                         NotInjective
+  where
+    binders  = [Named kKiVar Specified]
+    res_kind = mkTyVarTy kKiVar
+
+anyTy :: Type
+anyTy = mkTyConTy anyTyCon
+
+anyTypeOfKind :: Kind -> Type
+anyTypeOfKind kind = mkTyConApp anyTyCon [kind]
+
 -- Kinds
 typeNatKindConName, typeSymbolKindConName :: Name
 typeNatKindConName    = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Nat")    typeNatKindConNameKey    typeNatKindCon