Type ascriptions within patterns on binders are dropped

[W95Psp]

Hi,

Type ascriptions within patterns on binders seem to have no effect. For instance, f and g below have a pattern as their first binder, pattern which is ascribe the variable x with type int. That ascription is just dropped: in f the two ascriptions are incoherent, while in g, the ascription should force x to be an integer, however, F* accepts to return it as a string. Note that "root" ascriptions are not dropped, as illustrated by h.

type foo t = | Foo: t -> foo t
let f ((Foo (x: int)): foo string): string = x
let g ((Foo (x: int))): string = x
[@@expect_failure]
let h ((Foo x): foo string): int = x

Such nested ascriptions appear to work on match branches:

type bar t = 
  | Bar0: t -> bar t
  | Bar1: t -> bar t

[@@expect_failure]
let i = fun x -> match x with
    | Bar0 (x: string) -> x
    | Bar1 (x: int) -> x

In both cases, type ascriptions within patterns are only allowed on variables. I wonder if this limitation could be dropped.

I guess patterns on binder desugar differently than patterns in match branches. I have an issue with this bringing support for type ascriptions in let operators in PR #2666. More specifically:

let* x0: t0 = e0
and* x1: t1 = e1 in
body

desugars to:

(let*) ((and*) e0 e1) (fun (x0: t0, x1: t1) -> body)

where x0 ad x1 could actually be non-trivial patterns (i.e. not just names). To solve this issue, I have a hoist_pat_ascription function that hoists nested pattern ascriptions as one "root" ascription, but that works only for tuple and list patterns.