Skip to content

Eliminate `VoidRep :: PrimRep`, define pre-unarise `type CoreRep = [PrimRep]`

(This is about PrimRep, the data type internal to the compiler that we use to encode how a type will be mapped to registers. It's decoupled from the RuntimeRep data type, which is exported from base and thus wired into the compiler.)

Currently after unarisation, we have the invariant that each binder's representation is

  • a single PrimRep
  • that is not VoidRep

And try to track where we allow VoidRep and where we don't with a NonVoid wrapper.

I propose

  1. to delete VoidRep from PrimRep
  2. define type CoreRep = [PrimRep] and use it as the pre-unarise representation where needed
  3. use [] in place of VoidRep

(3) means we'll get type errors where we previously construct VoidReps as (singleton) PrimReps. And that's probably OK; if we really need 0-or-1-PrimRep, use Maybe PrimRep (or a custom ismorphic data type). (With refinement or dependent types we could simply make [PrimRep] length-indexed and express the particular width we need at use sites.)

Also note that we have a slightly weird isomorphism on [PrimRep] today: [] :: PrimRep shares the same representation with [VoidRep], [VoidRep, VoidRep], etc.. My proposal would get rid of that wart.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information