Typechecking of applications ignores expected type

[mtzguido]

type natlt (n:nat) = x:nat{ x < n }

let test1 (n:nat) : natlt n -> natlt (n+1) =
  id #_ (fun i -> i+1)

This fails, as when we check the lambda we check against an expected type of ?u1, an unresolved uvar for the #_, and it ends up choosing int as the type of the binder for i.