Cross-module-inlining behaves inconsistently and differently than friending

[gebner]

Consider the following four files:

// A.fsti
module A
val t: Type0
val s0: Type0
// We wrap the type in a match to trigger automatic coercion.
inline_for_extraction let s1 b = if b then t else s0
inline_for_extraction let s = s1 false
val t_eq_s: squash (t==s)

// A.fst
module A
let t = nat
let s0 = nat
let t_eq_s = ()

// B.fsti
module B

// B.fst
module B
open A
let f (x:t) : s = x

Extracting ocaml code from B.fst results in this function, expectedly using magic:

let (f : A.t -> A.s0) = fun uu___ -> (fun x -> Obj.magic x) uu___

If we add friend A to B.fst, then extraction can (again, as expected) see through the type definitions:

let (f : A.t -> A.s0) = fun x -> x

However, --cmi uses magic (while it should probably behave as if everything was in the same file). Even more surprisingly, if you tag either t or s0 as inline_for_extraction, then extraction with --cmi sees through the other definition as well (even though they are not defined in terms of each other):

let (f : Prims.nat -> A.s0) = fun x -> x

This is potentially related to the extraction failure in https://github.com/project-everest/mitls-fstar/pull/260