Cannot extract functions with type annotations using Karamel

[gebner]

In some cases, functions defined using the fn foo (...) : ty = args { ... } syntax cannot be extracted using Karamel:

module ExtractionTest

let noop = x:SizeT.t -> stt SizeT.t emp (fun y -> pure (y == x))

(*
Cannot re-check ExtractionTest.foo as valid Low* and will not extract it.  If ExtractionTest.foo is not meant to be extracted, consider marking it as Ghost, noextract, or using a bundle. If it is meant to be extracted, use -dast for further debugging.

Warning 4: in top-level declaration ExtractionTest.foo, in file ExtractionTest: Malformed input:
subtype mismatch, size_t (a.k.a. size_t) vs size_t -> size_t (a.k.a. size_t -> size_t)
*)
inline_for_extraction
```pulse
fn foo () : noop = x { x }

// Extracts fine

fn foo' () requires emp returns z:SizeT.t ensures pure (z == 42sz) {
  foo () 42sz;
}

The OCaml extraction looks fine though:
```ocaml
type noop = FStar_SizeT.t -> FStar_SizeT.t
let foo uu___ x = x

Adding the following function already breaks fstar.exe --codegen krml --extract:

(*
Unexpected error; please file a bug report, ideally with a minimized version of the source program that triggered the error.
Failure("Impossible: Tm_unknown")
*)
let foo'' = foo () 42sz

[gebner]

Apparently I missed a warning during extraction: Not extracting Bug9.foo to KaRaMeL (function type annotation has less arrows than the number of arguments; please mark the return type abbreviation as inline_for_extraction)

Adding inline_for_extraction to noop makes extraction work again. (Though it would be great if this was an error and not a crash.)