Type ascriptions on parameterised let expressions ignore type refinement

Expressions of the form

let f x : t2 = e1 <: refinedtype // x not free in e1
let g (x : t1) : t2 = e2 <: refinedtype // x may be free in e1

where `refinedtype` is a refinement type (e.g. `b:bool{false}`) appear to ignore the refinements on the type ascription. For example, the following bindings are unexpectedly not rejected:

let f x : bool = true <: (b:bool{false})
let g (x : bool) : bool = x <: (b:bool{false})

Note that the ascription isn't totally ignored, it just seems to be the refinement: if it is a refinement of a different type altogether then it still fails (e.g. `b:int{false}` when `bool` is expected). The refinement is also still used for type inference, as such the following fails as expected when checking `q`

let h x : bool = x <: (b:bool{false})
let q = f true

Note also, that this doesn't seem to occur for non-parameterised lets: the following fails as expected:

let z : bool = true <: (b:bool{false})

Tested on fstar_2021.06.06_Windows_x64 (from the website) and fstar_2022.02.12_Windows_x64 (latest pre-release from GitHub)

Still occurring in 2025.02.06 (Windows x64)