Annotation `[@@@ strictly_positive]` doesn't work in some cases

[TWal]

See the following code:

type strictly_positive_func = [@@@ strictly_positive] _:Type0 -> Type0

[@@expect_failure [3]]
noeq
type ty1_fail (test: strictly_positive_func) =
  | C1f: test (ty1_fail test) -> ty1_fail test

// Workaround: inline `strictly_positive_func`
noeq
type ty1_success (test: ([@@@ strictly_positive] _:Type0 -> Type0)) =
  | C1s: test (ty1_success test) -> ty1_success test

noeq
type strictly_positive_record = {
  t: [@@@ strictly_positive] bytes:Type0 -> Type0
}

[@@expect_failure [3]]
noeq
type ty2_fail (test:strictly_positive_record) =
  | C2f: test.t (ty2_fail test) -> ty2_fail test

// Workaround: do it by pattern matching
noeq
type ty2_success (test:strictly_positive_record) =
  | C2s: (let {t} = test in t (ty2_success test)) -> ty2_success test