Skip to content

WIP: Levity polymorphic arrays

Andrew Martin requested to merge andrewthad/ghc:levity-polymorphic-arrays into master

Implement phase 2 of the GHC Proposal 203: Boxed Rep Proposal. Phase 1 of this proposal was completed in !4612 (merged).

The goal here is to adjust the types of several primops and the kind of several primitive types. For example:

data Array# :: forall (v :: Levity). TYPE ('BoxedRep v) -> Type
indexArray# :: forall {v :: Levity} (a :: TYPE ('BoxedRep v)). Array# a -> Int# -> a

Note above that in indexArray#, v is not eligible for VTA. This is for backwards compatibility. Array-based and MutVar-based primop will have more general types after this change. Conversely, liveliness primops (e.g. touch#, mkWeak#) will have more restrictive types:

touch# :: forall {v :: Levity} (u :: TYPE ('BoxedRep v)).
  u -> State# RealWorld -> State# RealWorld

Currently, liveliness primops accept "open type" (forall (r :: RuntimeRep). TYPE r) in places where only a boxed value makes sense. This part of the MR is not backwards compatible, but it will only cause compile-time failure for users who were doing unsound operations that GHC's type checker was previously unable to shoot down (e.g. touch# 42# s0#).

Edited by Andrew Martin

Merge request reports