Commit 24d76153 authored by Ben Gamari's avatar Ben Gamari Committed by Ben Gamari

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
parent bc953fcd
......@@ -1530,7 +1530,7 @@ addrPrimTyConKey, arrayPrimTyConKey, arrayArrayPrimTyConKey, boolTyConKey,
weakPrimTyConKey, mutableArrayPrimTyConKey, mutableArrayArrayPrimTyConKey,
mutableByteArrayPrimTyConKey, orderingTyConKey, mVarPrimTyConKey,
ratioTyConKey, rationalTyConKey, realWorldTyConKey, stablePtrPrimTyConKey,
stablePtrTyConKey, anyTyConKey, eqTyConKey, heqTyConKey,
stablePtrTyConKey, eqTyConKey, heqTyConKey,
smallArrayPrimTyConKey, smallMutableArrayPrimTyConKey :: Unique
addrPrimTyConKey = mkPreludeTyConUnique 1
arrayPrimTyConKey = mkPreludeTyConUnique 3
......@@ -1566,7 +1566,6 @@ rationalTyConKey = mkPreludeTyConUnique 33
realWorldTyConKey = mkPreludeTyConUnique 34
stablePtrPrimTyConKey = mkPreludeTyConUnique 35
stablePtrTyConKey = mkPreludeTyConUnique 36
anyTyConKey = mkPreludeTyConUnique 37
eqTyConKey = mkPreludeTyConUnique 38
heqTyConKey = mkPreludeTyConUnique 39
arrayArrayPrimTyConKey = mkPreludeTyConUnique 40
......@@ -1723,21 +1722,24 @@ proxyPrimTyConKey = mkPreludeTyConUnique 176
specTyConKey :: Unique
specTyConKey = mkPreludeTyConUnique 177
smallArrayPrimTyConKey = mkPreludeTyConUnique 178
smallMutableArrayPrimTyConKey = mkPreludeTyConUnique 179
anyTyConKey :: Unique
anyTyConKey = mkPreludeTyConUnique 178
smallArrayPrimTyConKey = mkPreludeTyConUnique 179
smallMutableArrayPrimTyConKey = mkPreludeTyConUnique 180
staticPtrTyConKey :: Unique
staticPtrTyConKey = mkPreludeTyConUnique 180
staticPtrTyConKey = mkPreludeTyConUnique 181
staticPtrInfoTyConKey :: Unique
staticPtrInfoTyConKey = mkPreludeTyConUnique 181
staticPtrInfoTyConKey = mkPreludeTyConUnique 182
callStackTyConKey :: Unique
callStackTyConKey = mkPreludeTyConUnique 182
callStackTyConKey = mkPreludeTyConUnique 183
-- Typeables
typeRepTyConKey :: Unique
typeRepTyConKey = mkPreludeTyConUnique 183
typeRepTyConKey = mkPreludeTyConUnique 184
---------------- Template Haskell -------------------
-- THNames.hs: USES TyConUniques 200-299
......
......@@ -69,9 +69,6 @@ module TysPrim(
eqReprPrimTyCon, -- ty1 ~R# ty2 (at role Representational)
eqPhantPrimTyCon, -- ty1 ~P# ty2 (at role Phantom)
-- * Any
anyTy, anyTyCon, anyTypeOfKind,
-- * SIMD
#include "primop-vector-tys-exports.hs-incl"
) where
......@@ -144,7 +141,6 @@ primTyCons
, wordPrimTyCon
, word32PrimTyCon
, word64PrimTyCon
, anyTyCon
, eqPrimTyCon
, eqReprPrimTyCon
, eqPhantPrimTyCon
......@@ -897,83 +893,6 @@ threadIdPrimTy = mkTyConTy threadIdPrimTyCon
threadIdPrimTyCon :: TyCon
threadIdPrimTyCon = pcPrimTyCon0 threadIdPrimTyConName PtrRep
{-
************************************************************************
* *
Any
* *
************************************************************************
Note [Any types]
~~~~~~~~~~~~~~~~
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
primitive 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.
* It is lifted, and hence represented by a pointer
* It is inhabited by at least one value, namely bottom
* You can unsafely coerce any lifted type to Any, and back.
* 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 used to instantiate otherwise un-constrained type variables
For example length Any []
See Note [Strangely-kinded void TyCons]
Note [Strangely-kinded void TyCons]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
See Trac #959 for more examples
When the type checker finds a type variable with no binding, which
means it can be instantiated with an arbitrary type, it usually
instantiates it to Void. Eg.
length []
===>
length Any (Nil Any)
But in really obscure programs, the type variable might have a kind
other than *, so we need to invent a suitably-kinded type.
This commit uses
Any for kind *
Any(*->*) for kind *->*
etc
-}
anyTyConName :: Name
anyTyConName = mkPrimTc (fsLit "Any") anyTyConKey anyTyCon
anyTy :: Type
anyTy = mkTyConTy anyTyCon
anyTyCon :: TyCon
anyTyCon = mkFamilyTyCon anyTyConName binders res_kind [kKiVar] Nothing
(ClosedSynFamilyTyCon Nothing)
Nothing
NotInjective
where
binders = [Named kKiVar Specified]
res_kind = mkTyVarTy kKiVar
anyTypeOfKind :: Kind -> Type
anyTypeOfKind kind = TyConApp anyTyCon [kind]
{-
************************************************************************
* *
......
......@@ -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
......
......@@ -2578,52 +2578,6 @@ pseudoop "seq"
{\tt a}. If you need to guarantee a specific order of evaluation,
you must use the function {\tt pseq} from the "parallel" package. }
primtype Any
{ The type constructor {\tt Any} is type to which you can unsafely coerce any
lifted type, and back.
* It is lifted, and hence represented by a pointer
* It does not claim to be a {\it data} type, and that's important for
the code generator, because the code gen may {\it enter} a data value
but never enters a function value.
It's also used to instantiate un-constrained type variables after type
checking. For example, {\tt length} has type
{\tt length :: forall a. [a] -> Int}
and the list datacon for the empty list has type
{\tt [] :: forall a. [a]}
In order to compose these two terms as {\tt length []} a type
application is required, but there is no constraint on the
choice. In this situation GHC uses {\tt Any}:
{\tt length (Any *) ([] (Any *))}
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
kind polymorphic setting, a similar example to the length of the empty
list can be given at the type level:
{\tt type family Length (l :: [k]) :: Nat}
{\tt type instance Length [] = Zero}
When {\tt Length} is applied to the empty (promoted) list it will have
the kind {\tt Length AnyK []}.
{\tt AnyK} is currently not exported and cannot be used directly, but
you might see it in debug output from the compiler.
}
pseudoop "unsafeCoerce#"
a -> b
{ The function {\tt unsafeCoerce\#} allows you to side-step the typechecker entirely. That
......
......@@ -39,7 +39,7 @@ import CoreUtils ( exprType, eqExpr, mkTick, mkTicks,
import PprCore ( pprRules )
import Type ( Type, substTy, mkTCvSubst )
import TcType ( tcSplitTyConApp_maybe )
import TysPrim ( anyTypeOfKind )
import TysWiredIn ( anyTypeOfKind )
import Coercion
import CoreTidy ( tidyRules )
import Id
......
......@@ -74,6 +74,9 @@ module GHC.Exts
-- * The Constraint kind
Constraint,
-- * The Any type
Any,
-- * Overloaded lists
IsList(..)
) where
......
{-# LANGUAGE MagicHash, NoImplicitPrelude, TypeFamilies, UnboxedTuples,
MultiParamTypeClasses, RoleAnnotations, CPP, TypeOperators #-}
MultiParamTypeClasses, RoleAnnotations, CPP, TypeOperators,
PolyKinds #-}
-----------------------------------------------------------------------------
-- |
-- Module : GHC.Types
......@@ -29,6 +30,7 @@ module GHC.Types (
isTrue#,
SPEC(..),
Nat, Symbol,
Any,
type (~~), Coercible,
TYPE, RuntimeRep(..), Type, type (*), type (), Constraint,
-- The historical type * should ideally be written as
......@@ -79,6 +81,23 @@ data Nat
-- Declared here because class IP needs it
data Symbol
{- *********************************************************************
* *
Any
* *
********************************************************************* -}
-- | The type constructor 'Any' is type to which you can unsafely coerce any
-- lifted type, and back. More concretely, for a lifted type @t@ and
-- value @x :: t@, -- @unsafeCoerce (unsafeCoerce x :: Any) :: t@ is equivalent
-- to @x@.
--
type family Any :: k where { }
-- See Note [Any types] in TysWiredIn. Also, for a bit of history on Any see
-- #10886. Note that this must be a *closed* type family: we need to ensure
-- that this can't reduce to a `data` type for the results discussed in
-- Note [Any types].
{- *********************************************************************
* *
Lists
......
module T5441a where
import Unsafe.Coerce (unsafeCoerce)
import GHC.Prim (Any)
import GHC.Base (Any)
listmap :: (a -> b) -> [a] -> [b]
listmap f [] = []
......
......@@ -32,7 +32,7 @@ import Data.ByteString (ByteString)
import qualified Data.ByteString as B
import qualified Data.ByteString.Lazy as BL
import GHC.Prim
import GHC.Base (Any)
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Syntax as TH
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment