Some (possibly known) interleaving name resolution headaches

[msprotz]

This is a minimal repro from something that happened to me recently in HACL. Generally, it's oftentimes advised to not reuse field names within a single module; however, with the semantics of interleaving, I find myself either giving up on open entirely, which is tedious when projectors are involved, or adopting globally-unique field names for my records, which is not optimal either.

I'm not sure there's a good solution for this knowing the semantics of interleaving. CC @mtzguido since he's been helping out with name resolution recently.

Thanks,

Jonathan

jonathan@absinthe:/tmp $ cat A.fst
module A

type t = {
  key: int;
}
jonathan@absinthe:/tmp $ cat B.fsti
module B

open A

val t: Type0

let f (x: A.t): int = x.key
jonathan@absinthe:/tmp $ fstar.exe --cache_checked_modules A.fst
Verified module: A
All verification conditions discharged successfully
jonathan@absinthe:/tmp $ fstar.exe --cache_checked_modules B.fsti
Verified i'face (or impl+i'face): B
All verification conditions discharged successfully
jonathan@absinthe:/tmp $ # The fsti is properly interpreted when standalone, but ceases to work when interleaved with its fst -- the names of the fields in the fst shadow an open that exists in the fsti only
jonathan@absinthe:/tmp $ cat B.fst
module B

type t = {
  key: string;
}
jonathan@absinthe:/tmp $ fstar.exe --cache_checked_modules B.fst
B.fsti(7,22-7,23): (Error 189) Expected expression of type "B.t"; got expression "x" of type "A.t" (see also B.fsti(7,7-7,8))
1 error was reported (see above)