owned this note
owned this note
Published
Linked with GitHub
# Incorporating Kinds Are Calling Conventions
## Overall goal
Extend Core so that
* The kind of a type expresses its arity (as well as levity and representation, which it does now).
* Two lambdas: one "old" lamda, and a new arity-aware one; similarly two arrow type constructors `(->)` and `(~>)`.
## Status
**Shant's [google doc](https://docs.google.com/document/d/1TJjZL3qjq3fa5IPP2Am5Gf82vd7yoaQivUGnvdW-N1o/edit)**
* Question: long term, do we want the RuntimeInfo structure to be a pair? Maybe yes... convenient when you want to be polymorphic in both.
* Question: do we want to expose `RuntimeInfo` to users, or make it abstract, with accessor functions?
## Notes
* `data RuntimeRepInfo` avoids the need for a big linear case. But for now we put up with the big linear case.
## Overview
Example for the arity WW transformation:
```hs
map :: (a->b) -> [a] -> [b]
map1 :: (a~>b) ~> [a] ~> [b]
map1 = \~f \~xs. case xs of
(x:xs) -> f x : map1 f xs
[] -> []
map f xs = map1 (\~x. f x) xs
```
NB: Not only the outer (first-order) level of lambdas of the worker is squiggled, but also the inner (second-order) level.
How to encode the type of ~> within GHC? With -XLinearTypes, we currently have
```hs
Int %m -> Int
type Multiplicity = Type
data Type = TyVarTy TyVar
| FunTy Multiplicity Squiggle Type Type
| TyConApp TyCon [Type]
| ForAllTy TyVar Type
data Expr = Var Var
| Lam Var Expr
| App Expr Expr
| Case ...
| Let ...
```
every Id has an IdInfo, one field of which is Multiplicity
Not a nice trick, but at least the same trick.
*Digression: Shant and Paul's idea involved extending `TYPE` with an additional argument. They were annoyed by the fact that the compiler/Haskell's type system couldn't help with the refactoring by pointing out potential (runtime) errors in advance, and would probably long for something like classic GADT
à la (STITCH, viz.)*
```hs
data Type k where
AppTy::: Type (k1->k2) -> Type k1 -> Type k2
```
## What we have
Shant then gave a rough account of what he did. Basically, he replaced `RuntimeRep` with `RuntimeInfo` below:
```hs
-- in GHC.Types.RepType:
data RuntimeRep = VecRep VecCount VecElem -- ^ a SIMD vector type
| TupleRep [RuntimeRep] -- ^ An unboxed tuple of the given reps
| SumRep [RuntimeRep] -- ^ An unboxed sum of the given reps
| BoxedRep Levity -- ^ boxed; represented by a pointer
| IntRep -- ^ signed, word-sized value
...etc...
type Levity = Type
data Levity = Lifted
| Unlifted
data RuntimeInfo = RInfo {rep :: RuntimeRep, conv :: CallingConv}
data CallingConv = ConvEval
| ConvCall [RuntimeRep]
data RuntimeRep = .... | BoxedRep Levity | ...
```
#### `RuntimeInfo` permits illegal states
As Sebastian already implied in a mail he sent, he was a bit confused why the proposed `RuntimeInfo` allows illegal states such as `RInfo IntRep (ConvCall [AddrRep])`. Paul brought up the need to want to define types that are rep-poly but not calling-conv-poly and vice versa. It would be good to have examples here for that. Paul also said there are some in the paper, which we can probably just copy here.
##### Encoding 1: `RuntimeRep`-inside-of-`ConvEval`
Suppose we have instead
```hs
TYPE :: CallingConv -> Type
data CallingConv = ConvEval RuntimeRep
| ConvCall [CallingConv]
data RuntimeRep = ... as today ...
```
Counter-example `Array#` from section 4.4:
```hs
Array# :: forall lev. TYPE (ConvEval (BoxedRep lev)) -> TYPE (ConvEval UnliftedRep)
```
This wouldn't allow us to store `Int ~> Int :: TYPE (ConvCall [ConvEval LiftedRep])` in the array.
##### Encoding 2: `CallingConv`-instead-of-`BoxedRep`
Suppose we have instead
```hs
data RuntimeRep = ...
| BoxedRep CallingConv
...
```
Counter-example `revapp` from section 4.5:
```hs
revapp :: forall conv (t1 :: TYPE (BoxedRep conv)) rep (t2 :: TYPE rep). t1 ~> (t1 ~> t2) ~> t2
revapp x f = f x
```
Suppose this type-checks. Then, `revapp 23 (g :: Int ~> Int ~> Int) 42` type-checks. But so should `App (revapp 23 (h :: Int ~> {Int ~> Int}) 42`! The same generated code for `revapp` has to eval its body expr `f x` in the latter case and apply it in the former. SG: Feel free to improve explanation
Previously, we could assume that all GC'd pointers can be entered/eval'd (even if that is a no-op). With ~>, not so much, it seems.
Paul remarks that we then can't represent error:
```
error :: forall (r::RuntimeRep). String -> TYPE r
```
But now we can't tell the calling convention of the result type. (Simon asks: do we care?)
##### Encoding 2+: But what if we *could* eval ~> types?
Suppose we have Encoding 2. Our issue with `revapp` was that we couldn't generate code for its body, `f x`. But all the information we seek for dynamic dispatch is right there!
E.g., knowing that the arg `f` has type `t1 ~> t2`, we see that its arity is `BoxedRep conv,arity(rep)`. Since we know that `revapp` will be passed `arity(rep)` many args, this is enough to do a saturated call to `f`! Like this (pretty much a [generic apply](https://gitlab.haskell.org/ghc/ghc/-/wikis/commentary/rts/haskell-execution/function-calls#generic-apply)):
1. Look at the info pointer of `f` ("eval", as in eval/apply), find out how many args it takes (this will usually be encoded in the tagged pointer of `f`). Let's say the answer is 10. Then `revapp` will have 11 args.
2. Put `x` in arg position 1 (it's already there).
3. Shift arguments 3 to 11 down by one (so that they are in arg positions 2 to 10). So R3 -> R2, R4 -> R3, ..., adjust stack. In general (for other functions than `revapp`), we might also have to be able to "shift up".
4. Jump to the code for `f` ("apply")
Note how arity polymorphism ended up as a generic apply function. It's a bit curious how `arity(rep)` can't be erased and ends up in the info table pointer/pointer tag, but isn't that exactly the mechanism we already have in GHC today?
Arguably, this would probably need changing the semantics of $\mathcal{ML}$ to account for generic application/runtime information...
*Paul:* Instead, you can always get the functionality proposed in encoding 2+ by using a `->` arrow instead of `~>`. The `->` arrow:
1. Can be used with *any* argument and return types:
```hs
(->) :: forall (r1 :: RuntimeInfo) (r2 :: RuntimeInfo).
TYPE r1 -> TYPE r2 -> Type
```
In other words, there is no need to know the calling convention of `b` in `a -> b`.
2. Falls back to a dynamic calling convention when one cannot be inferred from its context. For example, we can lookup the definition of `(+)` to find that it's arity is 2, and statically compile `1 + 2` as a binary function call. In contrast, the call `f x` inside `revapp x f` is to a lambda-bound `f`; we cannot look up the definition of `f` and so the calling convention of `f x` is checked dynamically.
This lets us write a definition of `revapp` that does not statically track the calling convention of `b` in its type & kind:
```hs
revapp :: forall (cc :: CallingConv) (ri :: RuntimeInfo)
(a :: TYPE ('RInfo 'LiftedRep cc))
(b :: TYPE ri).
a ~> (a -> b) ~> (# #) -> b
:: TYPE ('RInfo 'UnliftedRep ('CallConv ['LiftedRep, 'LiftedRep]))
revapp x f _ = f x
```
The kind of `revapp` says its calling convention takes exactly two (lifted) pointer arguments, so all calls `revapp x f` will be statically compiled to a single binary call without dynamic arity checks. However, the higher-order argument is `f :: a -> b :: Type`, so the call `f x` cannot be statically compiled to a unary call (or any other calling convention). Instead, the calling convention of `f` is checked at runtime to see if it is under-/over-/perfectly-saturated. This dynamic call to `f` is triggered by the final application of the empty tuple argument in `revapp x f (# #)`. Without the final empty argument, we have the closure `revapp x f :: (# #) -> b :: TYPE ('RInfo ('LiftedRep 'EvalConv))` whose kind explicitly says that it can be evaluated.
Note that `f :: a -> b` has a completely unknown arity at compile time; it might even have arity 0 if it is a thunk that needs to be evaluated. But what if we want to say in the types that `f` takes *at least* one argument, but maybe more? We can use the same encoding as in the definition of `revapp` itself, to accept the first argument of type `a` statically and trigger the dynamic check for more arguments in a separate step using a `->` arrow with an empty argument. This is done like so:
```hs
revapp :: forall (cc :: CallingConv) (ri :: RuntimeInfo)
(a :: TYPE ('RInfo 'LiftedRep cc))
(b :: TYPE ri).
a ~> (a ~> (# #) -> b) ~> (# #) -> b
:: TYPE ('RInfo 'UnliftedRep ('CallConv ['LiftedRep, 'LiftedRep]))
revapp x f = f x
```
Now the call to `f x` is done statically as one step, which returns a closure that may ask for more arguments.
*Note:* The type `(# #) -> b` is interchangable with the closure type `{b}` from the ICFP'20 paper. The two type constructors can be defined in terms of one another (with the help of empty tuples and the primitive function arrow `~>`). Taking `a -> b` as primitive we have:
```hs
type {b} = (# #) -> b
```
Taking `{b}` as primitive we have:
```hs
type a -> b = {a ~> b}
```
---
Then Shant showcased how he extended the `typePrimRep` function to turn the `RuntimeInfo` into the new `PrimInfo`. Context (for the status quo in GHC):
```hs
typePrimRep :: HasDebugCallStack => Type -> [PrimRep]
typePrimRep ty = kindPrimRep (typeKind ty)
kindPrimRep :: Kind {- = TyConApp TYPE [rr] -}
-> [PrimRep]
kindPrimRep (TyConApp tc [rr]) = runtimeRepPrimRep rr
kindPrimrep _ = panic
where arg to be of form (TYPE rr)
runtimeRepPrimRep :: Type {- :: RuntimeRep -}
-> [PrimRep]
runtimeRepPrimRep (TyConApp tc tys)
| tc == intRepTyCon = [IntRep]
| tc == wordRepTyCon = [WordRep]
| tc == vecRepTyCon = map runtimeRepPrimRep tys
...
| otherwise = panic
runtimeRepPrimRep :: HasDebugCallStack => SDoc -> Type -> [PrimRep]
runtimeRepPrimRep doc rr_ty
| Just rr_ty' <- coreView rr_ty
= runtimeRepPrimRep doc rr_ty'
| TyConApp rr_dc args <- rr_ty
, RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
= fun args
| otherwise
= pprPanic "runtimeRepPrimRep" (doc $$ ppr rr_ty)
```
Simon argued that the impl could simply discard the calling conv
```hs
kindPrimRep (TyConApp tc [_, rr]) = runtimeRepPrimRep rr
```
for the MVP, where code generation is not affected yet at all.
Afterwards, we hunted down the reason for a bug in Shant's impl relating to `pcPrimRep` and concluded the call.
# Call on 2021-05-04
We gave Richard an introduction and then focused on the kind errors relating to unboxed tuples.
## Specification for unboxed tuples types and kinds
Richard nudged us into writing out the kind of the unboxed pair type constructor and the type of the unboxed pair data constructor, as follows:
```hs
-- Type constructor
type (# , #) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(v1 :: CallingConv) (v2 :: CallingConv).
TYPE (RInfo r1 v1) -> TYPE (RInfo r2 v2)
-> TYPE (RInfo (TupleRep [r1, r2]) ConvEval)
-- Data constructor
(# , #) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
(v1 :: CallingConv) (v2 :: CallingConv).
(a :: TYPE (RInfo r1 v1))
(b :: TYPE (RInfo r2 v2)).
a -> b -> (# , #) r1 r2 v1 v2 a b
```
NB: `TupleRep` takes a list of `RuntimeRep`, not `RuntimeInfo`.
Richard was sure that the kind errors that Shant was experiencing would go away if the type and data constructors were kinded/typed according to this spec.
## Discussion: Kinds are (could be) STG's types
Meta-point by Sebastian: think of the passage from
om Core to STG, as moving `x :: ty :: ki` to `x :: ki`. That is, we forget all the *type* distinctions, retaining only *kind* distinctions. Kinds classify types, which classify values; so kinds also classify values, but with a coarser mesh.
Sebastian pointed out that by only storing `RuntimeRep` in the field of `TupleRep`, we thus lose STG type/kind safety for examples like the following (assuming the `x :: ty :: ki` to `x :: ki` move for STG "types"):
```hs
f -- :: Int# ~> Int# in Core, but the following kind in STG
:: TYPE (RInfo (BoxedRep Unlifted) (ConvCall [IntRep]))
f x = ...
y -- :: Int# in Core, but the following kind in STG
:: TYPE (RInfo IntRep ConvEval)
y = ...
...
case (#,#) f y :: TYPE (RInfo (TupleRep [BoxedRep Unlifted,IntRep]) ConvEval) of
(#,#) (g :: TYPE (RInfo (BoxedRep Unlifted) (ConvCall [IntRep,IntRep])))
-- this is the bad boy ^^^^^^
(z :: TYPE (RInfo IntRep ConvEval))
-> g z 42#
```
Here, we call the arity 1 function `f` with arity 2. There's no way to catch this in the type system of STG, as the `CallingConv` the TYPE of `g` can be chosen freely. So well-typedness doesn't guarantee progress; the above expression is well-typed but stuck at runtime.
Sebastian can see how the kind system is not expressive enough in more cases than just `TupleRep`:
1. Why doesn't `ConvCall` specify a returned `RuntimeInfo`?
2. Why does the arity only take `RuntimeRep` and not full `RuntimeInfo`?
It's questionable if it's worth fixing `ConvCall`. So if we don't fix it, why fix `TupleRep`? SG argues that fixing `ConvCall` will make more valid programs we output typeable, but it will not impact progress, while fixing `TupleRep` does.
## A small problem with having levity in the rep field. (Our stop-gap.)
**Example** (moving levity over to `ConvEval`, from `BoxedRep`):
``` hs
revapp :: forall (r :: RuntimeRep) (v :: CallingConv) (l :: Levity)
(a :: TYPE (RInfo BoxedRep v))
(b :: TYPE (RInfo r (ConvEval l))).
a ~> (a ~> b) ~> b
:: TYPE (RInfo BoxedRep (ConvCall [BoxedRep, BoxedRep]))
revapp x f = f x
```
(NB: a *caller* of revapp needs to know levity of x, to know whether to use call-by-value or call-by-need; but revapp *itself* doesn't need to know.)
But if we move levity into the representation field (our stop-gap), we can't get the above levity polymorphism. Let's try!
```
revapp :: forall (r :: RuntimeRep (v :: CallingConv) (l :: Levity)
(a :: TYPE (RInfo (BoxedRep l) v))
(b :: TYPE (RInfo r ConvEval)).
a ~> (a ~> b) ~> b
:: TYPE (RInfo (BoxedRep Unlifted) (ConvCall [BoxedRep l, BoxedRep Unlifted]))
-- ^^^^ no no no
revapp x f = f x
```
See also https://gitlab.haskell.org/ghc/ghc/-/issues/19487 for why SG thinks the `l` in the kind could simply be replaced by `UnknownLevity`.
SG thinks that by having `TupleRep` list `RuntimeInfo` instead of `RuntimeRep` we might get similar problems (example needed).
## Reviewing Shant's code that builds the types and kinds of unboxed tuple constructors
```hs
mk_tuple Unboxed arity = (tycon, tuple_con)
where
tycon = mkTupleTyCon tc_name tc_binders tc_res_kind tc_arity tuple_con
UnboxedTuple flavour
-- See Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
-- Kind: forall (k1:RuntimeRep) (k2:RuntimeRep). TYPE k1 -> TYPE k2 -> #
tc_binders = mkTemplateTyConBinders (replicate arity runtimeInfoTy)
(\ks -> map tYPE ks)
tc_res_kind =
rr_tys
tc_arity = arity * 2
flavour = UnboxedAlgTyCon $ Just (mkPrelTyConRepName tc_name)
dc_tvs = binderVars tc_binders
(rr_tys, dc_arg_tys) = splitAt arity (mkTyVarTys dc_tvs)
tuple_con = pcDataCon dc_name dc_tvs dc_arg_tys tycon
boxity = Unboxed
modu = gHC_PRIM
tc_name = mkWiredInName modu (mkTupleOcc tcName boxity arity) tc_uniq
(ATyCon tycon) BuiltInSyntax
dc_name = mkWiredInName modu (mkTupleOcc dataName boxity arity) dc_uniq
(AConLike (RealDataCon tuple_con)) BuiltInSyntax
tc_uniq = mkTupleTyConUnique boxity arity
dc_uniq = mkTupleDataConUnique boxity arity
unboxedTupleSumKind tc rr_tys
= tYPE $ mkTyConApp runtimeInfoDataConTyCon [(mkTyConApp tc [mkPromotedListTy runtimeRepTy rr_tys]), convEvalDataConTy]
```
Problem: `unboxedTupleSumKind` expects `rr_tys` to have kind `RuntimeRep`. The `rr_tys` declared in `mk_tuple` probably has kind `RuntimeInfo`. There are a few other call sites of `unboxedTupleSumKind` in the type checker that should be checked.
## Matching Unboxed Tuple implemementation with paper spec
``` hs
-- mk_tuple creates the type AND data constructors
mk_tuple Unboxed arity = (tycon, tuple_con)
where
tycon = mkTupleTyCon tc_name tc_binders tc_res_kind tc_arity tuple_con
UnboxedTuple flavour
tc_binders = mkTemplateTyConBinders (take (arity * 2) $ cycle [runtimeRepTy, callingConvTy])
(\ris -> map (\(r,c) -> tYPE $ rInfo r c) (take2 ris))
tc_res_kind = unboxedTupleKind ri_tys
tc_arity = arity * 3
flavour = UnboxedAlgTyCon $ Just (mkPrelTyConRepName tc_name)
dc_tvs = binderVars tc_binders
(ri_tys, dc_arg_tys) = splitAt (arity * 2) (mkTyVarTys dc_tvs)
tuple_con = pcDataCon dc_name dc_tvs dc_arg_tys tycon
...
```
``` hs
-- typechecking unboxed tuples
finish_tuple :: HsType GhcRn
-> TupleSort
-> [TcType] -- ^ argument types
-> [TcKind] -- ^ of these kinds
-> TcKind -- ^ expected kind of the whole tuple
-> TcM TcType
finish_tuple rn_ty tup_sort tau_tys tau_kinds exp_kind = do
traceTc "finish_tuple" (ppr tup_sort $$ ppr tau_kinds $$ ppr exp_kind)
case tup_sort of
...
UnboxedTuple -> do
let tycon = tupleTyCon Unboxed arity
tau_reps = map kindRep tau_kinds
tau_ccs = map kindConv tau_kinds
reps_ccs = interleave tau_reps tau_ccs
-- See also Note [Unboxed tuple RuntimeRep vars] in GHC.Core.TyCon
arg_tys = reps_ccs ++ tau_tys
res_kind = unboxedTupleKind reps_ccs
checkTupSize arity
check_expected_kind (mkTyConApp tycon arg_tys) res_kind
where
arity = length tau_tys
check_expected_kind ty act_kind =
checkExpectedKind rn_ty ty act_kind exp_kind
```
``` hs
type Type = TYPE (RInfo LiftedRep ConvEval)
TYPE :: RuntimeInfo -> Type
data RuntimeInfo = RInfo RuntimeRep CallingConv
```
``` hs
-- Type constructor for (#,#)
(#,#) :: forall (k0 :: RuntimeRep) (k1 :: CallingConv)
(k2 :: RuntimeRep) (k3 :: CallingConv).
TYPE (RInfo k0 k1)
-> TYPE (RInfo k2 k3)
-> TYPE ('RInfo ('TupleRep '[k0, k2]) 'ConvEval)
-- data constructor for (#,#)
(#,#) :: forall (k0 :: RuntimeRep) (k1 :: CallingConv)
(k2 :: RuntimeRep) (k3 :: CallingConv)
(a :: TYPE ('RInfo k0 k1))
(b :: TYPE ('RInfo k2 k3)).
a -> b -> (#,#) k0 k1 k2 k3 a b
```
OR! Alternative kind for (#,#):
```
-- Type constructor for (#,#)
(#,#) :: forall (r1 :: RuntimeInfo) (r2 :: RuntimeInfo).
TYPE r1
-> TYPE r2
-> TYPE ('RInfo ('TupleRep '[GetRep r1, GetRep r2]) 'ConvEval)
-- data constructor for (#,#)
(#,#) :: forall (r1 :: RuntimeInfo) (r2 :: RuntimeInfo)
(a :: TYPE r1)
(b :: TYPE r2).
a -> b -> (#,#) r1 r2 a b
```
The kind for `error` in terms of `'RInfo` constructor:
```
error :: forall (r::RuntimeRep)
(a :: TYPE ('RInfo r 'ConvEval)).
String -> a
```
```
f :: forall (rr::RuntimeInfo) (a::TYPE rr). (GetConv rr ~ ConEval) =>
f s = errror (s++ s)
```
```
[W] RInfo a b ~ c -- c::RuntimeInfo is a skolem
```
Then you might hope solve this by using the eta rule: `c ~ RInfo (GetRep c) (GetConv c)`
```
-- this error was caused by tyVars of RuntimeRep
-- being incorrectly defaulted
getRuntimeInfo
(#,#) :: TYPE
('RInfo
('RInfo ('TupleRep '[]) 'ConvEval) ('RInfo 'LiftedRep 'ConvEval))
-> TYPE ('RInfo (State# RealWorld) a_ae5)
-> TYPE
('RInfo
('TupleRep '[ 'RInfo ('TupleRep '[]) 'ConvEval, State# RealWorld])
'ConvEval)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Core/Type.hs:2123:18 in ghc:GHC.Core.Type
```
``` hs
defaultTyVar :: Bool -- True <=> please default this kind variable to *
-> TcTyVar -- If it's a MetaTyVar then it is unbound
-> TcM Bool -- True <=> defaulted away altogether
defaultTyVar default_kind tv
...
| isRuntimeRepVar tv -- Do not quantify over a RuntimeRep var
-- unless it is a TyVarTv, handled earlier
= do { traceTc "Defaulting a RuntimeRep var to LiftedRep" (ppr tv)
-- was defaulting to (RInfo LiftedRep ConvEval) rather than
-- just LiftedRep
; writeMetaTyVar tv liftedRepTy
; return True }
```
```
(r :: RuntimeInfo) (TYPE r)
(TYPE ('RInfo rr cc))
```
``` hs
newOpenTypeKind :: TcM TcKind
newOpenTypeKind
= do { rr <- newFlexiTyVarTy runtimeRepTy
; cc <- newFlexiTyVarTy callingConvTy
; return (tYPE $ rInfo rr cc) }
```
These changes fixed the issues we were having in typechecking unboxed tuples, and now we have new errors!
```
libraries/ghc-prim/GHC/Magic.hs:101:24: error:
• Couldn't match kind ‘q’ with ‘'GHC.Types.RInfo t2 t3’
Expected a type, but ‘a’ has kind ‘TYPE q’
‘q’ is a rigid type variable bound by
an explicit forall (q :: RuntimeInfo) (r :: RuntimeInfo)
(a :: TYPE q) (b :: TYPE r)
at libraries/ghc-prim/GHC/Magic.hs:99:20
• In the type signature:
oneShot :: forall (q :: RuntimeInfo)
(r :: RuntimeInfo)
(a :: TYPE q)
(b :: TYPE r). (a -> b) -> a -> b
|
101 | (a -> b) -> a -> b
| ^
libraries/ghc-prim/GHC/Magic.hs:101:29: error:
• Couldn't match kind ‘r’ with ‘'GHC.Types.RInfo t4 t5’
Expected a type, but ‘b’ has kind ‘TYPE r’
‘r’ is a rigid type variable bound by
an explicit forall (q :: RuntimeInfo) (r :: RuntimeInfo)
(a :: TYPE q) (b :: TYPE r)
at libraries/ghc-prim/GHC/Magic.hs:99:39
• In the type signature:
oneShot :: forall (q :: RuntimeInfo)
(r :: RuntimeInfo)
(a :: TYPE q)
(b :: TYPE r). (a -> b) -> a -> b
|
101 | (a -> b) -> a -> b
| ^
libraries/ghc-prim/GHC/Magic.hs:115:38: error:
• Couldn't match kind ‘r’ with ‘'GHC.Types.RInfo t0 t1’
Expected a type, but ‘o’ has kind ‘TYPE r’
‘r’ is a rigid type variable bound by
an explicit forall (r :: RuntimeInfo) (o :: TYPE r)
at libraries/ghc-prim/GHC/Magic.hs:114:19
• In the type signature:
runRW# :: forall (r :: RuntimeInfo)
(o :: TYPE r). (State# RealWorld -> o) -> o
|
115 | (State# RealWorld -> o) -> o
|
```
``` hs
oneShot :: forall (q :: RuntimeInfo) (r :: RuntimeInfo)
(a :: TYPE q) (b :: TYPE r).
(a -> b) -> a -> b
oneShot f = f
oneShot2 :: forall (rep1 :: RuntimeRep) (cc1 :: CallingConv)
(rep2 :: RuntimeRep) (cc2 :: CallingConv)
(a :: TYPE (RInfo rep cc)) (b :: TYPE (RInfo rep2 cc2)).
(a -> b) -> a -> b
```
Cannot write `oneShot = oneShot2`
```hs
funTyCon :: TyCon
funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
where
-- See also unrestrictedFunTyCon
tc_bndrs = [ mkNamedTyConBinder Required multiplicityTyVar
, mkNamedTyConBinder Inferred runtimeInfo1TyVar
, mkNamedTyConBinder Inferred runtimeInfo2TyVar ]
++ mkTemplateAnonTyConBinders [ tYPE runtimeInfo1Ty
, tYPE runtimeInfo2Ty
]
tc_rep_nm = mkPrelTyConRepName funTyConName
(->) :: forall (m:Multiplicty) (r1 :: RuntimeInfo) (r2::RuntimeInfo).
TYPE r1 -> TYPE r2 -> Type
```
``` hs
kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
kindRep_maybe kind
| TyConApp tc [arg] <- coreFullView kind
, tc `hasKey` tYPETyConKey
, TyConApp rinfo [rep, conv] <- coreFullView arg
, rinfo `hasKey` runtimeInfoDataConKey = Just rep
| otherwise = Nothing
```
``` hs
tc_fun_type :: TcTyMode -> HsArrow GhcRn -> LHsType GhcRn -> LHsType GhcRn -> TcKind
-> TcM TcType
tc_fun_type mode mult ty1 ty2 exp_kind = case mode_tyki mode of
TypeLevel ->
do { arg_k <- newOpenTypeKind
; res_k <- newOpenTypeKind
; ty1' <- tc_lhs_type mode ty1 arg_k
; ty2' <- tc_lhs_type mode ty2 res_k
; mult' <- tc_mult mode mult
; checkExpectedKind (HsFunTy noExtField mult ty1 ty2) (mkVisFunTy mult' ty1' ty2')
liftedTypeKind exp_kind }
KindLevel -> -- no representation polymorphism in kinds. yet.
do { ty1' <- tc_lhs_type mode ty1 liftedTypeKind
; ty2' <- tc_lhs_type mode ty2 liftedTypeKind
; mult' <- tc_mult mode mult
; checkExpectedKind (HsFunTy noExtField mult ty1 ty2) (mkVisFunTy mult' ty1' ty2')
liftedTypeKind exp_kind }
```
## GetRep and GetConv
in ghc-prim/Types.hs
```hs
type family GetRep (ri :: RuntimeInfo) :: RuntimeRep where
GetRep ('RInfo rep _) = rep
type family GetConv (ri :: RuntimeInfo) :: CallingConv where
GetConv ('RInfo _ conv) = conv
```
In GHC/Core/Type.hs
```hs
kindRep_maybe :: HasDebugCallStack => Kind -> Maybe Type
kindRep_maybe kind
| TyConApp tc [arg] <- coreFullView kind
, tc `hasKey` tYPETyConKey = Just $ getRep arg
| otherwise = Nothing
-- | Given a type (RInfo rr cc) extracts its RuntimeRep
-- classifier rr.
getRep :: Type -> Type
getRep rinfo
| TyConApp rinfo [rep, _] <- coreFullView rinfo
, rinfo `hasKey` runtimeInfoDataConKey = rep
| otherwise = mkTyConApp getRepTyCon [rinfo]
kindConv_maybe :: HasDebugCallStack => Kind -> Maybe Type
kindConv_maybe kind
| TyConApp tc [arg] <- coreFullView kind
, tc `hasKey` tYPETyConKey = Just $ getConv arg
| otherwise = Nothing
-- | Given a type (RInfo rr cc) extracts its CallingConv
-- classifier cc.
getConv :: Type -> Type
getConv rinfo
| TyConApp rinfo [_, conv] <- coreFullView rinfo
, rinfo `hasKey` runtimeInfoDataConKey = conv
| otherwise = mkTyConApp getConvTyCon [rinfo]
```
```hs
coreView ty@(TyConApp tc tys)
| Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
-- This equation is exactly like tcView
-- At the Core level, Constraint = Type
-- See Note [coreView vs tcView]
| isConstraintKindCon tc
= ASSERT2( null tys, ppr ty )
Just liftedTypeKind
| tc `hasKey` getRepTyConKey
= Just $ getRep ty
| tc `hasKey` getConvTyConKey
= Just $ getConv ty
where
getRep ty
| TyConApp getRepTyCon [rinfo] <- ty
, TyConApp rinfo [rep, conv] <- rinfo = rep
| otherwise = ty
getConv ty
| TyConApp getConvTyCon [rinfo] <- ty
, TyConApp rinfo [rep, conv] <- rinfo = conv
| otherwise = ty
coreView _ = Nothing
{-# INLINE coreFullView #-}
coreFullView :: Type -> Type
-- ^ Iterates 'coreView' until there is no more to synonym to expand.
-- See Note [Inlining coreView].
coreFullView ty@(TyConApp tc _)
| isTypeSynonymTyCon tc || isConstraintKindCon tc
|| tc `hasKey` getRepTyConKey || tc `hasKey` getConvTyConKey
= go ty
where
go ty
| Just ty' <- coreView ty = go ty'
| otherwise = ty
coreFullView ty = ty
```
```
(GHC version 9.1.0.20210528:
mkTyConKindRepBinds(TyConApp)
GetRep
GetRep ('RInfo ('TupleRep '[]) 'ConvEval)
Call stack:
CallStack (from HasCallStack):
callStackDoc, called at compiler/GHC/Utils/Panic.hs:181:37 in ghc:GHC.Utils.Panic
pprPanic, called at compiler/GHC/Tc/Instance/Typeable.hs:593:9 in ghc:GHC.Tc.Instance.Typeable
```
```hs
{-# INLINE tcView #-}
tcView :: Type -> Maybe Type
tcView ty@(TyConApp tc tys) | Just (tenv, rhs, tys') <- expandSynTyCon_maybe tc tys
= Just (mkAppTys (substTy (mkTvSubstPrs tenv) rhs) tys')
-- The free vars of 'rhs' should all be bound by 'tenv', so it's
-- ok to use 'substTy' here.
-- See also Note [The substitution invariant] in GHC.Core.TyCo.Subst.
-- Its important to use mkAppTys, rather than (foldl AppTy),
-- because the function part might well return a
-- partially-applied type constructor; indeed, usually will!
| tc `hasKey` getRepTyConKey
, [TyConApp rinfo [rep, _conv]] <- tys
, rinfo `hasKey` runtimeInfoDataConKey
= Just rep
| tc `hasKey` getConvTyConKey
, [TyConApp rinfo [_rep, conv]] <- tys
, rinfo `hasKey` runtimeInfoDataConKey
= Just conv
tcView _ = Nothing
```
```
type T a = a->a
```
The type `T Int` is *equal (eqType) to* `Int -> Int`
But for
```
type family F [a] = a -> a
```
the type `F [Int]` is *not* equal to `Int -> Int`.
```
f ty | Just ty' <- tcView ty = f ty'
f (TyConApp tc tys) = ...
...
```
After inlining
```
f (TyConApp tc tys) | expandsyn = f ty' -- result of inlining tcview
f (TyConApp tc tys) = ... -- the second line of the original f
```
# Alternative designs
From the paper:
```
f :: forall c::CallingConv. (a :: TYPE (RR PtrRep c). blah
```
With type functions, keeping `RuntimeInfo`
```
f :: forall r::RuntimeInfo. (a :: TYPE r). (Rep r ~ PtrRep) => a -> blah
f x = blah
```
Richard's version:
```
f :: forall r::RuntimeInfo. (a :: TYPE r). (FixedRep r PtrRep) => a -> blah
f x = blah
```
```
f1 :: forall a. a -> forall b. b -> blah
f1 = blah
f1_worker :: forall (# 0 a :: Type, _ :: a, 0 b :: Type, _ :: b #) -> blah{a,b}
f1_worker (# _ , x , _ , y #) = blah
f2 :: forall a b. a -> b -> blah
f2 x y = blah
f2_worker :: forall a b. (# a, b #) -> blah
f2_worker (# x, y #) = blah
```
## Uncurrying
[Types are Calling Conventions](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/08/tacc-hs09.pdf) used unboxed tuples to encode "multiple args"
https://www.microsoft.com/en-us/research/publication/making-a-faster-curry-with-extensional-types/, Section 8.1
Essentially we'd need a new uncurried arrow type
```
ty :: qauntifiers -> ty
| ...
quantifiers ::= /* empty */
| ty, quantifiers
| (var::ty), quantifiers
```
and a similar term former
```
data Expr = ... | Lam [Var] Expr | App Expr [Expr]
```
```
data T = MkT (Int -> Bool -> Int -> Int)
f :: <Int Bool> -> Int -> Int
f = \x y.\z. e
-- SG: this takes two args (in R1 R2) and allocates
-- and returns a closrue
g = MkT f -- Ill typed
g = MkF f_imp -- Well typed
f_imp = \p. \q. \r. f p q r
-- SG: This takes one argument (n R1) and allocates
-- and returns a closure, of one argumetn...
h x = case x of MkT t -> t 3 True
p x = f x True
$wzipWith :: (<a b> -> c) -> [a] -> [b] -> [c]
$wzipWith f (x:xs) (y:ys) = f x y : zipwith f xs ys
-- zipWith f xs ys -- here f is compiled to take 3 args!
wurble :: (Int -> Int -> Int) -> Int -> Int
wurble f = f 1
blah :: <Int Int> -> Int
blah x y = x + y
-- SG: This takes two arguments (in R1 and RT) and
-- returns R1+R2
blah2 :: Int -> Int -> Int
blah2 x y = x + y
-- SG: This takes one arguments (in R1 and
-- returns a closure
blah3 :: <Int Int Int> -> Int
blah3 x y z = x + y + z
blah4 :: <Int Int> -> Int -> Int
blah4 x y = \z. x + y + z
garble :: (Int -> Int -> Int -> Int) -> Int -> Int
garble f = f 1 2
garble' :: (<Int Int> -> Int -> Int) -> Int -> Int
garble' f = f 1 2
-- How do we express that `f` only takes one argument?
-- Like this? What is the difference between <Int> and Int?
-- Surely it's rather a property of the arrow that follows <Int>.
garble1 :: (<Int> -> Int -> Int) -> Int -> Int
garble1 f = f 1
-- (wurble blah) and (wurble blah2)
(\x. blah 1 x) :: Int -> Int
$wzipWith :: (<a b> -> c) -> [a] -> [b] -> [c]
$wzipWith f (x:xs) (y:ys) = f x y : zipwith f xs ys
.... wurble blah ...
case x of MkT ff -> let gg = ff 3 in map gg boozel
```
f's closure has an info table with (a) code for invocation with three args, (b) arity info saying "I need two groups of args"
f_imp's closure has an info-table with (a) code for invocation (with three arguments) (b) arity info saying "I need three args"
At the unknown call in `h`, we do a dynamic check, just as today.
**Paul's claim (new to Simon)** Mixing static and dynamic arity checks (Section 7) is
* compatible with the story in the paper,
* but *not* compatible with uncurrying.
We must keep the dynamic arity checks, else MkT becomes terribly inefficient, forcing the one-arg-at-a-time mechanism, even for arity-3 functions!
Possible way to approach combined static/dynamic arity checks with currying/uncurrying: Use *two* arrow types:
1. The curried arrow type `a -> b`, which is dynamically checked for arity when called at runtime
2. The uncurried arrow type `<a1..an> -> b` which is not dynamically checked for arity at runtime when called.
Note that there is a difference between the type `Int -> Int` versus the singleton uncurried arrow `<Int> -> Int`.
## GetRep and GetConv Simplification
As per what was discussed in the previous meeting, we removed GetRep and GetConv simplification from ```coreView``` and put it off until code gen.
As such we had to modify ```isKindLevPoly``` to see through the applications of ```GetRep``` and ```GetConv```.
```haskell=
isKindLevPoly :: Kind -> Bool
isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
go k
where
...
go ty@(TyConApp tc tys)
| Just rep <- simplifyRep ty
= go rep
| Just conv <- simplifyConv ty
= go conv
| otherwise
= isFamilyTyCon tc || any go tys
...
```
Once that change was made, errors popped up in ```runtimeRepPrimRep``` due to unsimplified applications of GetRep
```
ghc-stage1: panic! (the 'impossible' happened)
(GHC version 9.1.0.20210528:
runtimeRepPrimRep
tupleRepDataCon [GetRep ('RInfo 'WordRep 'ConvEval),
GetRep ('RInfo 'WordRep 'ConvEval)]
GetRep ('RInfo 'WordRep 'ConvEval)
```
In order to simplify these terms, we added the following clause to ```runtimeRepPrimRep```
```haskell=
runtimeRepPrimRep :: HasDebugCallStack => SDoc -> Type -> [PrimRep]
runtimeRepPrimRep doc rr_ty
| Just rr_ty' <- coreView rr_ty
= runtimeRepPrimRep doc rr_ty'
-- Clause for simplifying GetRep applications
| Just rr_ty' <- simplifyRep rr_ty
= runtimeRepPrimRep doc rr_ty'
| TyConApp rr_dc args <- rr_ty
, RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
= fun args
| otherwise
= pprPanic "runtimeRepPrimRep" (doc $$ ppr rr_ty)
```
## runtimeRepPrimRep_maybe
```=haskell
runtimeRepPrimRep :: HasDebugCallStack => SDoc -> Type -> [PrimRep]
runtimeRepPrimRep doc rr_ty
| Just p_reps <- runtimeRepPrimRep_maybe doc rr_ty
= p_reps
| otherwise
= pprPanic "runtimeRepPrimRep" (doc $$ ppr rr_ty)
runtimeRepPrimRep_maybe :: HasDebugCallStack => SDoc -> Type -> Maybe [PrimRep]
runtimeRepPrimRep_maybe doc rr_ty
| Just rr_ty' <- coreView rr_ty
= runtimeRepPrimRep_maybe doc rr_ty'
| Just rr_ty' <- simplifyRep rr_ty
= runtimeRepPrimRep_maybe doc rr_ty'
| TyConApp rr_dc args <- rr_ty
, RuntimeRep fun <- tyConRuntimeRepInfo rr_dc
= Just $ fun args
| otherwise
= Nothing
```
Our hope was also to be able to use ```runtimeRepPrimRep_maybe``` within ```isLiftedRuntimeRep``` and ```isUnliftedRuntimeRep```.
The issue with this approach is in the handling of singleton Tuples.
```=Haskell
runtimeRepPrimRep (TupleRep [LiftedRep]) = [LiftedRep]
runtimeRepPrimRep LiftedRep = [LiftedRep]
-- should be
isLiftedRuntimeRep (TupleRep [LiftedRep]) = False
-- with runtimeRepPrimRep_maybe approach
isLiftedRuntimeRep (TupleRep [LiftedRep]) = True
```
### The Solution
An additional function which uses simplifyRep and returns a ```Maybe Levity```: ```Just lev``` in the case where the levity is concrete, and ```Nothing``` when it is polymorphic.
```=haskell
data Levity = Lifted | Unlifted
-- LIbrary:
-- data RuntimeRep = LiftedRep | UnliftedRep | IntRep ...
runtimeInfoLevity_maybe :: Type -> Maybe Levity
-- (runtimeRepLevity_maybe (ty :: RuntimeInfo))
-- takes a type of kind RuntimeInfo, and returns
-- (Just lev) if we can figure out its levity for certain,
-- and Nothing if we can't (eg levity polymorphic)
runtimeInfoLevity_maybe rinfo
| Just (_, [rep, _conv]) <- splitTyConApp_maybe rinfo
, Just (tc, _) <- splitTyConApp_maybe (simplifyRep rep `orElse` rep)
= Just (if tc `hasKey` liftedRepDataConKey
then Lifted else Unlifted)
| otherwise
= Nothing
```
We have quarantined ```simplifyRep``` inside ```RepType``` where ```runtimeRepPrimRep``` and ```runtimeInfoLevity_maybe``` are defined. The latter two are then exported and used within the lev-poly and isLifted checks.
```=haskell
isRuntimeInfoLevPoly :: Type -> Bool
isRuntimeInfoLevPoly ty
| Nothing <- runtimeInfoLevity_maybe ty
= True
| otherwise
= False
isKindLevPoly :: Kind -> Bool
isKindLevPoly k = ASSERT2( isLiftedTypeKind k || _is_type, ppr k )
go k
where
...
go ty@(TyConApp tc tys)
| tc `hasKey` runtimeInfoDataConKey
= isRuntimeInfoLevPoly ty
| otherwise
= isFamilyTyCon tc || any go tys
...
```
```
isLiftedTypeKind :: Kind -> Bool
isLiftedTypeKind kind
= case kindInfo_maybe kind of
Just rinfo -> isLiftedRuntimeInfo rinfo
Nothing -> False
isLiftedRuntimeInfo :: Type -> Bool
isLiftedRuntimeInfo ty
| Just Lifted <- runtimeInfoLevity_maybe ty
= True
| otherwise
= False
```
## Other Issue
```
TYPE
('RInfo
('SumRep
'[GetRep ('RInfo 'LiftedRep 'ConvEval),
GetRep ('RInfo 'UnliftedRep 'ConvEval)])
'ConvEval)
TYPE
('RInfo
('SumRep
'[GetRep ('RInfo 'LiftedRep 'ConvEval),
GetRep ('RInfo 'UnliftedRep 'ConvEval)])
'ConvEval)
LT
```
```
(first kind) (GHC.Types.GetRep{(w) tc 3cU}
(second kind) (GHC.Types.GetRep{tc r7T}
```
```haskell
simplifyRep :: Type -> Maybe Type
simplifyRep rep
| Just rinfo <- getRepArg_maybe rep
, (TyConApp rinfo [rep', _]) <- rinfo
= Just rep'
| otherwise
= Nothing
```
GHC.Types.Name
```
pprExternal debug sty uniq mod occ is_wired is_builtin
| codeStyle sty = ppr mod <> char '_' <> ppr_z_occ_name occ
-- In code style, always qualify
-- ToDo: maybe we could print all wired-in things unqualified
-- in code style, to reduce symbol table bloat?
| debug = pp_mod <> ppr_occ_name occ
<> braces (hsep [if is_wired then text "(w)" else empty,
pprNameSpaceBrief (occNameSpace occ),
pprUnique uniq])
```
Google Drive
Gist
Clipboard
Sign in with Wallet
