Type mismatch issue of sub1

Question

I can't figure out why the sub1 function in pick1 has type mismatch issue,but pick0 don't

(define-predicate one? One)
(: pick1 (-> Positive-Integer (Listof Any) Any))
(define pick1
  (λ(n lat)
    (cond [(one? n) (car lat)]
          [else (pick1 (sub1 n)
                       (cdr lat))])))

I have tried this workaround, but I think this is not a right way to fix this issue.

(: pick1-workaround (-> Positive-Integer (Listof Any) Any))
(define pick1-workaround 
  (λ(n lat)
    (cond [(one? n) (car lat)]
          [else (pick1-workaround  (cast (sub1 n) Positive-Integer)
                                   (cdr lat))])))

pick0 don't have this issue.

;;(: pick0 (-> Natural (Listof Any) Any))
(define pick0
  (λ(n lat)
    (cond [(zero? n) (car lat)]
          [else (pick0 (sub1 n)
                       (cdr lat))])))

Answer 1

What you implicitly want Typed Racket to reason is that if x is in Positive-Integer - One, then (sub1 x) is in Positive-Integer. While it is easy for human to see that this is true, I think the problem is that Typed Racket does not know how to describe Positive-Integer - One = {2, 3, 4, ...}.

On the other hand, your pick0 works. This version of pick1 also works:

(: pick1 (-> Positive-Integer (Listof Any) Any))
(define pick1
  (λ (n lat)
    (define n* (sub1 n))
    (cond 
      [(zero? n*) (car lat)]
      [else (pick1 n* (cdr lat))])))

I think the reason is that Typed Racket knows that if x is in Positive-Integer, then (sub1 x) is in Natural, and it recognizes that (sub1 x) in the else branch must be in Natural - {0} = Positive-Integer (via occurrence typing), allowing it to successfully type check the program.