Nested patterns, refinements and branches with Tot functions

Type inference fails incorrectly in this case

```
module NestedPatternsAndTotBranches

assume val f : unit -> Tot (option nat)
assume val h : int -> Tot int
assume val k : unit -> Tot int

let ff () : unit -> Tot int =
let y = f () in
match 0, y (* fails: y expected to have type (option int) rather than (option nat) *) with
| _, Some r -> (fun z -> h r)
| _ -> k
```