Inconsistent thunking on extraction with interfaces

Noticed while trying to fix #2094. The example here is bit artificial but I'm running into this same problem when extracting the library after a patch.

A.fsti:
```fstar
module A

val empty : #a:Type -> int
```

A.fst:a
```fstar
module A

let empty #_ = 42
```

B.fst:
```fstar
module B

open A

let y = 1 + empty #bool
```

After extraction:
A.ml:
```ocaml
open Prims
let empty : 'uuuuu . Prims.int = (Prims.of_int (42))
```

B.ml:
```ocaml
open Prims
let (y : Prims.int) = Prims.int_one + (A.empty ())
```

Which is clearly ill-typed. As far as I can see the problem comes since when extracting `B`, we do not have the definition for `empty`, which is then taken to be `FStar.All.failwith "Not yet implemented:empty"`. This in turn will fail the value check, and hence gain a thunk. Not sure what's the reasonable thing to do here.

Start with the A.fsti, A.fst, and B.fst example, then compare the extracted A.ml and B.ml outputs. Investigate the extraction value check and thunking behavior when B is extracted without A's definition in scope; done means the generated A.ml and B.ml type-check consistently.

Written by the indexing model from the issue text.