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
- to delete
VoidRep
fromPrimRep
- define
type CoreRep = [PrimRep]
and use it as the pre-unarise representation where needed - use
[]
in place ofVoidRep
(3) means we'll get type errors where we previously construct VoidRep
s as (singleton) PrimRep
s. 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.