Surprising (?) type error

Questions & Answers
1

I have been going through the typed/racket guide and encountered code like the following

#lang typed/racket

(: prop:foo (Struct-Property (-> Self Number)))
(: foo-pred (-> Any Boolean : (Has-Struct-Property prop:foo)))
(: foo-get (-> (Has-Struct-Property prop:foo)
               (Some (X)
                     (-> X Number)
                     : #:+ X)))
(define-values (prop:foo foo-pred foo-get)
  (make-struct-type-property 'foo))

(struct Num ([n : Number])
  #:property prop:foo
  (lambda ([me : Num])
          : Number
    (Num-n me)))

(: num/foo Number)
(define num/foo
  (let ([a1 : Num
            (Num 42)])
    ((foo-get a1) a1)))

(module+ test
  (require typed/rackunit)
  ;; succeeds
  (check-equal? num/foo 42))

However, The following form leads to a type error

;; type error
(module+ test
  (check-equal?
   (ann
    (let ([a1 : Num
              (Num 42)])
      ((foo-get a1) a1))
    Number)
   42))

It fails with the following error:

Type Checker: type mismatch
  expected: (B 0)
  given: Num
  in: a1

This code should be equivalent if my understanding is correct, it just inlines the body in the definition of num/foo and includes the appropriate inline annotation similar to the one on the top level define for num/foo. Can someone explain to me why the first test form succeeds and the second is a type error? Thanks

2

Interestingly enough, this works:

(module+ test
  (let ([a1 : Num (Num 42)])
    (define xxx (foo-get a1))
    (check-equal? (xxx a1) 42)))

I suggest opening an issue w/ Typed Racket.