Comments only
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 20 Jul 2016 14:28:10 +0000 (15:28 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Thu, 21 Jul 2016 08:49:44 +0000 (09:49 +0100)
compiler/coreSyn/MkCore.hs
compiler/prelude/TysPrim.hs
compiler/prelude/TysWiredIn.hs

index d9a7a21..b575e8a 100644 (file)
@@ -722,8 +722,6 @@ mkRuntimeErrorId :: Name -> Id
 -- which diverges after being given one argument
 -- The Addr# is expected to be the address of
 --   a UTF8-encoded error string
--- For the RuntimeRep part, see
---   Note [Error and friends have an "open-tyvar" forall]
 mkRuntimeErrorId name
  = mkVanillaGlobalWithInfo name runtime_err_ty bottoming_info
  where
@@ -743,6 +741,8 @@ mkRuntimeErrorId name
     strict_sig = mkClosedStrictSig [evalDmd] exnRes
               -- exnRes: these throw an exception, not just diverge
 
+    -- forall (rr :: RuntimeRep) (a :: rr). Addr# -> a
+    --   See Note [Error and friends have an "open-tyvar" forall]
     runtime_err_ty = mkSpecSigmaTy [runtimeRep1TyVar, openAlphaTyVar] []
                                    (mkFunTy addrPrimTy openAlphaTy)
 
index 19728ee..7430ec8 100644 (file)
@@ -351,43 +351,91 @@ funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
 *                                                                      *
 ************************************************************************
 
-Note [TYPE]
-~~~~~~~~~~~
-There are a few places where we wish to be able to deal interchangeably
-with kind * and kind #. unsafeCoerce#, error, and (->) are some of these
-places. The way we do this is to use runtime-representation polymorphism.
-
-We have
-
-    data RuntimeRep = PtrRepLifted | PtrRepUnlifted | ...
-
-and a magical constant (tYPETyCon)
-
-    TYPE :: RuntimeRep -> TYPE PtrRepLifted
-
-We then have synonyms (liftedTypeKindTyCon, unliftedTypeKindTyCon)
-
-    type * = TYPE PtrRepLifted
-    type # = TYPE PtrRepUnlifted
-
-The (...) in the definition for RuntimeRep includes possibilities for
-the unboxed, unlifted representations, isomorphic to the PrimRep type
-in TyCon. RuntimeRep is itself declared in GHC.Types.
-
-An alternative design would be to have
-
-  data RuntimeRep = PtrRep Levity | ...
-  data Levity = Lifted | Unlifted
-
-but this slowed down GHC because every time we looked at *, we had to
-follow a bunch of pointers. When we have unpackable sums, we should
-go back to the stratified representation. This would allow, for example:
-
-    unsafeCoerce# :: forall (r1 :: RuntimeRep) (v2 :: Levity)
-                            (a :: TYPE v1) (b :: TYPE v2). a -> b
-
-TYPE replaces the old sub-kinding machinery. We call variables `a` and `b`
-above "runtime-representation polymorphic".
+Note [TYPE and RuntimeRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+All types that classify values have a kind of the form (TYPE rr), where
+
+    data RuntimeRep     -- Defined in ghc-prim:GHC.Types
+      = PtrRepLifted
+      | PtrRepUnlifted
+      | IntRep
+      | FloatRep
+      .. etc ..
+
+    rr :: RuntimeRep
+
+    TYPE :: RuntimeRep -> TYPE 'PtrRepLifted  -- Built in
+
+So for example:
+    Int        :: TYPE 'PtrRepLifted
+    Array# Int :: TYPE 'PtrRepUnlifted
+    Int#       :: TYPE 'IntRep
+    Float#     :: TYPE 'FloatRep
+    Maybe      :: TYPE 'PtrRepLifted -> TYPE 'PtrRepLifted
+
+We abbreviate '*' specially:
+    type * = TYPE 'PtrRepLifted
+
+The 'rr' parameter tells us how the value is represented at runime.
+
+Generally speaking, you can't be polymorphic in 'rr'.  E.g
+   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
+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 :: TYPE rr'.
+
+* 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 :: 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 :: TYPE r1) (b :: TYPE r2).
+                     a -> b -> TYPE 'UnboxedTupleRep
+     See Note [Unboxed tuple kinds]
+
+Note [Unboxed tuple kinds]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+What kind does (# Int, Float# #) have?
+The "right" answer would be
+    TYPE ('UnboxedTupleRep [PtrRepLifted, FloatRep])
+Currently we do not do this.  We just have
+    (# Int, Float# #) :: TYPE 'UnboxedTupleRep
+which does not tell us exactly how is is represented.
+
+Note [PrimRep and kindPrimRep]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+As part of its source code, in TyCon, GHC has
+  data PrimRep = PtrRep | IntRep | FloatRep | ...etc...
+
+Notice that
+ * RuntimeRep is part of the syntax tree of the program being compiled
+     (defined in a library: ghc-prim:GHC.Types)
+ * PrimRep is part of GHC's source code.
+     (defined in TyCon)
+
+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" [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
+where 'rr_dc' is a promoteed data constructor from RuntimeRep. So
+now we need to go from 'dc' to the correponding PrimRep.  We store this
+PrimRep in the promoted data constructor itself: see TyCon.promDcRepInfo.
 
 -}
 
@@ -400,7 +448,7 @@ tYPETyCon = mkKindTyCon tYPETyConName
                         [Nominal]
                         (mkPrelTyConRepName tYPETyConName)
 
-   -- See Note [TYPE]
+   -- See Note [TYPE and RuntimeRep]
    -- NB: unlifted is wired in because there is no way to parse it in
    -- Haskell. That's the only reason for wiring it in.
 unliftedTypeKindTyCon = mkSynonymTyCon unliftedTypeKindTyConName
@@ -425,7 +473,8 @@ mkPrimTcName built_in_syntax occ key tycon
   = mkWiredInName gHC_PRIM (mkTcOccFS occ) key (ATyCon tycon) built_in_syntax
 
 -----------------------------
--- | Given a RuntimeRep, applies TYPE to it. See Note [TYPE].
+-- | Given a RuntimeRep, applies TYPE to it.
+-- see Note [TYPE and RuntimeRep]
 tYPE :: Type -> Type
 tYPE rr = TyConApp tYPETyCon [rr]
 
index 11aea78..0775d06 100644 (file)
@@ -301,6 +301,10 @@ The type constructor Any,
 
 It has these properties:
 
+  * 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``.
+
   * 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:
@@ -317,7 +321,7 @@ It has these properties:
   * 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.
+  * 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
@@ -326,6 +330,12 @@ It has these properties:
   * 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)
 
+  * If (Any k) is the type of a value, it must be a /lifted/ value. So
+    if we have (Any @(TYPE rr)) then rr must be 'PtrRepLifted.  See
+    Note [TYPE and RuntimeRep] in TysPrim.  This is a convenient
+    invariant, and makes isUnliftedTyCon well-defined; otherwise what
+    would (isUnliftedTyCon Any) be?
+
 It's used to instantiate un-constrained type variables after type checking. For
 example, 'length' has type
 
@@ -343,10 +353,6 @@ choice.  In this situation GHC uses '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.
@@ -786,7 +792,7 @@ mk_tuple Unboxed arity = (tycon, tuple_con)
                          UnboxedTuple flavour
 
     -- See Note [Unboxed tuple RuntimeRep vars] in TyCon
-    -- Kind:  forall (k1:RuntimeRep) (k2:RuntimeRep). TYPE k2 -> TYPE k2 -> #
+    -- Kind:  forall (k1:RuntimeRep) (k2:RuntimeRep). TYPE k1 -> TYPE k2 -> #
     tc_binders = mkTemplateTyConBinders (nOfThem arity runtimeRepTy)
                                         (\ks -> map tYPE ks)
 
@@ -980,14 +986,18 @@ mk_class tycon sc_pred sc_sel_id
 *                                                                      *
 ********************************************************************* -}
 
--- For information about the usage of the following type, see Note [TYPE]
--- in module TysPrim
+-- For information about the usage of the following type,
+-- see Note [TYPE and RuntimeRep] in module TysPrim
 runtimeRepTy :: Type
 runtimeRepTy = mkTyConTy runtimeRepTyCon
 
 liftedTypeKindTyCon, starKindTyCon, unicodeStarKindTyCon :: TyCon
 
-   -- See Note [TYPE] in TysPrim
+-- Type syononyms; see Note [TYPE and RuntimeRep] in TysPrim
+-- type Type = tYPE 'PtrRepLifted
+-- type *    = tYPE 'PtrRepLifted
+-- type *    = tYPE 'PtrRepLifted  -- Unicode variant
+
 liftedTypeKindTyCon   = mkSynonymTyCon liftedTypeKindTyConName
                                        [] liftedTypeKind []
                                        (tYPE ptrRepLiftedTy)