Lack of bidirectionality with records

noeq
type inj (t1 t2 : Type) = {
  f : t1 -> t2;
}

let double (x:nat) : inj nat nat = {
  f = (fun x -> x+1);
}

This fails with

- Subtyping check failed
- Expected type inj nat nat got type inj int int

The annotation on double should force the right instantiation for the implicits of the record constructor. Note this also fails even if we annotate that x is a nat:

- Subtyping check failed
- Expected type inj nat nat got type inj nat int

Start by running the two F* reproducer snippets and inspect how the record constructor instantiates its implicit types under the annotated return type. Trace the bidirectional type-checking path for the function field; done means both examples typecheck as inj nat nat without subtyping failures.