Failure of type inference with repeated variables

Lax-typechecking the following snippet

```F#
let f (x y : int) (w:(b:bool & (if b then equals x y else equals y x))) =
match w with
| (| b, Refl |) -> ()
```

fails with the error
```
(Error) (equals (?26524 x y w b) (?26524 x y w b)) is not a subtype of the expected type (match b with
| true -> (equals x y)
|_ -> (equals y x))
```