diff options
| -rw-r--r-- | compiler/coreSyn/MkCore.hs | 4 | ||||
| -rw-r--r-- | compiler/prelude/TysPrim.hs | 127 | ||||
| -rw-r--r-- | compiler/prelude/TysWiredIn.hs | 28 |
3 files changed, 109 insertions, 50 deletions
diff --git a/compiler/coreSyn/MkCore.hs b/compiler/coreSyn/MkCore.hs index d9a7a21f2f..b575e8a48a 100644 --- a/compiler/coreSyn/MkCore.hs +++ b/compiler/coreSyn/MkCore.hs @@ -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) diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs index 19728ee430..7430ec82c1 100644 --- a/compiler/prelude/TysPrim.hs +++ b/compiler/prelude/TysPrim.hs @@ -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] diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs index 11aea78549..0775d06a11 100644 --- a/compiler/prelude/TysWiredIn.hs +++ b/compiler/prelude/TysWiredIn.hs @@ -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) |