Something is fishy with GADT data con allocation size
Consider the program
module B where
import GHC.Exts
type NP :: [Type] -> Type
data NP xs where
UNil :: NP '[]
This will give rise to the following Cmm:
[UNil_entry() { // []
{ info_tbls: [(cE4,
label: UNil_info
rep: HeapRep static { Fun {arity: 1 fun_type: ArgSpec 3} }
srt: Nothing)]
stack_info: arg_space: 8
}
{offset
cE4:
unwind Sp = Just Sp;
unwind Sp = Just Sp;
Hp = Hp + 16;
if (Hp > HpLim) (likely: False) goto cE8; else goto cE7;
cE8:
unwind Sp = Just Sp;
HpAlloc = 16;
unwind Sp = Just Sp;
R1 = UNil_closure;
call (stg_gc_fun)(R1) args: 8, res: 0, upd: 8;
cE7:
unwind Sp = Just Sp;
I64[Hp - 8] = UNil_con_info;
R1 = Hp - 7;
call (P64[Sp])(R1) args: 8, res: 0, upd: 8;
}
},
section ""data" . UNil_closure" {
UNil_closure:
const UNil_info;
}]
Note that UNil_entry
allocates the wrong amount: We reserve two words on the heap despite this being a nullary constructor.
Presumably the latter is due to the code generator treating the xs ~# '[]
equality evidence as runtime-relevant.