Struct predicate from untyped module fails across shallow/deep boundary

[NoahStoryM]

What version of Racket are you using?
8.18 [cs]

What program did you run?

#lang typed/racket

(module m typed/racket/shallow
  (module n racket
    (provide (all-defined-out))
    (struct v () #:property prop:sequence (λ (v) '()))
    (define (make-v) (v))
    (define (v?? v)
      (cond
        [(v? v) (displayln "yes") #t]
        [else   (displayln "no")  #f])))
  (require/typed 'n
    [make-v (∀ (a) (→ (Sequenceof a)))]
    [v?? (→ Any Boolean)])
  (provide (all-defined-out))
  (define v? v??)
  (define v (inst make-v Nothing)))
(require 'm)

(v? (v))

What should have happened?
The value created by (v) is an instance of the v struct, so the predicate v? should identify it. If the top-level language is changed from #lang typed/racket to #lang typed/racket/shallow, the program behaves as expected:

yes
#t

If you got an error message, please include it here.
The actual output is:

no
#f

[NoahStoryM]

Here is a follow-up with a slightly modified example. If I change the type of make-v to (→ SequenceTop), Typed Racket fails with a contract error.

Code:

#lang typed/racket

(module m typed/racket/shallow
  (module n racket
    (provide (all-defined-out))
    (struct v () #:property prop:sequence (λ (v) '()))
    (define (make-v) (v))
    (define (v?? v)
      (cond
        [(v? v) (displayln "yes") #t]
        [else   (displayln "no")  #f])))
  (require/typed 'n
    [make-v (→ SequenceTop)]
    [v?? (→ Any Boolean)])
  (provide (all-defined-out))
  (define v? v??)
  (define v make-v))
(require 'm)

(v? (v))

Error:

v: broke its own contract
  any-wrap/c: Unable to protect opaque value passed as `Any`
  value: #<v>
  in: the 2nd conjunct of
      the range of
      (-> (and/c sequence? Any))