Krml shifts the names of parameters in function signatures with erased arguments

[nikswamy]

Consider this:

module Shifting
open FStar.Ghost
assume
val callback (#erased_x:erased bool) (concrete_y:bool) (#erased_z:erased bool) (concrete_a:bool) : bool

let test (#erased_x:erased bool) (concrete_y:bool) (#erased_z:erased bool) (concrete_a:bool) = concrete_y && concrete_a

It produces

/* 
  This file was generated by KreMLin <https://github.com/FStarLang/kremlin>
  KreMLin invocation: C:\cygwin64\home\nswam\workspace\everest\kremlin\_build\src\Kremlin.native out.krml -skip-compilation -dast
  F* version: <unknown>
  KreMLin version: 332d8a00
 */

#ifndef __Shifting_H
#define __Shifting_H

#include "kremlib.h"




extern bool Shifting_callback(bool erased_x, bool concrete_y);

bool Shifting_test(bool concrete_y, bool concrete_a);


#define __Shifting_H_DEFINED
#endif

Note the -dast dump contains:

SHIFTING:
  
  external Shifting_callback : () -> bool -> () -> bool -> bool
  
  function
  Shifting_test
  <0>(
    erased_x(0, ): (),
    concrete_y(0, ): bool,
    erased_z(0, ): (),
    concrete_a(0, ): bool
  ):
  bool
  { (&&,bool_t) @2 @0 }

It doesn't show the names in the signature of Shifting_callback. But notice that F* has not fully erased those arguments ... they are there as units. And krml does unit elimination and I guess in the process shifts the names around?

Would be nice to fix this, since when linking at the C level, the parameter names of the generated externs are quite confusing.