Should the type-checker force returned tuples to be destructed?

[n-osborne]

Currently, Gospel doesn't accept:

val f : int -> int * int
(*@ y = f x *)

$ gospel check file.mli
2 | (*@ y = f x *)
            ^
File "file.mli", line 2, characters 8-9:
Error: Type checking error: too few returned values: when a function returns
       a tuple, the gospel header should name each member of the tuple; so
       the header of a function returning a pair might be "x,y = ...".

But this is not the case for nested tuples, gospel check will be happy with

val f : int -> int * (int * int)
(*@ y,z = f x *)

But raises a syntax error with

val f : int -> int * (int * int)
(*@ y,(a,b) = f x *)