Limitation when matching pair of indexed types

[mtzguido]

noeq
type task_state : int -> Type u#2 =
  | Ready    : post:int -> task_state post

let min (post1:int) (post2:int) (x:task_state post1) (y : task_state post2) : prop =
  match x, y with
  | Ready _, Ready _ -> False

This gives:

* Error 230 at Bug.fst(10,10-10,11):
  - Variable "uu___#1116" not found

It can be circumvented by nested matches, at the possible expense of some repetition. Annotating the pair also works:

let min (post1:int) (post2:int) (x:task_state post1) (y : task_state post2) : prop =
  match (x, y) <: task_state post1 & task_state post2 with
  | (Ready _, Ready _) -> False