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.