Loss of argument type refinement when the function is inside a record

[aseemr]

@john-ml reports the following failing code:

noeq type fn a b = {
  f: a -> b
}
let extract_left #a #b : fn (x:either a b{Inl? x}) a = {
  f = (fun (Inl x) -> x);
}