Monomorphizations leak into interfaces and lead to incorrect code in combination with CAbstractStruct

[nikswamy]

Here's a repro:

------Abstract.fsti----------
module Abstract

val t (a:Type0) : Type0

val make (#a:Type0) (x:a) : t a
val read (#a:Type0) (x:t a) : a
------Abstract.fst----------
module Abstract

type t a = (bool & a)

let make #a x = (false, x)
let read #a t = snd t
------Parameter.fsti----------
module Parameter

[@@CAbstractStruct]
type param = {
  param_one: bool;
  param_two: bool
}
------Main.fsti----------
module Main
open FStar.HyperStack.ST
module B = LowStar.Buffer

[@@CAbstractStruct]
val handle : Type0

val init (_:unit)
  : ST (B.pointer handle)
       (requires fun _ -> True)
       (ensures fun _ _ _ -> True)
------Main.fst----------
module Main
module HS = FStar.HyperStack
module B = LowStar.Buffer

[@@CAbstractStruct]
noeq
type handle = {
  something: bool;
  another: Abstract.t Parameter.param;
}

let init (_:unit) =
  let h = {
    something = false;
    another = Abstract.make Parameter.({ param_one = true; param_two = false })
  } in
  B.malloc HS.root h 1ul

When using krml version 7008464 and krml -bundle Main=* leads to

#ifndef __Main_H
#define __Main_H

#include "krmllib.h"


typedef struct Parameter_param_s Parameter_param;

typedef struct K___bool_Parameter_param_s
{
  bool fst;
  Parameter_param snd;
}
K___bool_Parameter_param;

typedef struct Main_handle_s Main_handle;

Main_handle *Main_init();


#define __Main_H_DEFINED
#endif

With the error

✘ [CC,./Main.c] (use -verbose to see the output)
In file included from ./Main.c:8:
./Main.h:21:19: error: field ‘snd’ has incomplete type
   21 |   Parameter_param snd;

Note that Parameter_param is an alias for an abstract struct but is used in a field of a struct K___bool_Parameter_param_s.

If you remove the CAbstractStruct annotation on Parameter.param you get:

typedef struct Parameter_param_s
{
  bool param_one;
  bool param_two;
}
Parameter_param;

typedef struct K___bool_Parameter_param_s
{
  bool fst;
  Parameter_param snd;
}
K___bool_Parameter_param;

typedef struct Main_handle_s Main_handle;

Main_handle *Main_init();

Which is no longer incorrect. But, this has leaked the monomorphizations into the interface Main.h, even though the -bundle Main=* says that only the interface of Main.fsti should be taken as entrypoints. Indeed, the K___bool_Parameter_param is unused in Main.h.

I suspect that by ensuring that monomorphizations don't leak into interfaces, the first issue of illegal code would also be solved.

[nikswamy]

cc @tahina-pro @arvinda ... managed to get a minimization of the compilation failure we were looking at

[msprotz]

The fix for this one is now in #256