false negative with recursive predicates

[ilya-klyuchnikov]

TR accepts a program that should be rejected:

#lang typed/racket/base

(: a*? (-> Any Boolean : (Listof 'a)))
(define (a*? l)
  (cond
    [(null? l) #t]
    [(pair? l) (and
                (equal? (car l) 'a)
                (a*? (cdr l)))]
    [else #f]))

(: use-a*? (-> Any 'a))
(define (use-a*? arg)
  (if (a*? arg)
      (car arg) ; IT MAY BE NULL!!
      'a))

Reproducible with the 9.0 distribution.

[mfelleisen]

Not a bug. This is a standard issue with type systems.

If you really want to make sure that a*? checks for `(Pairof 'a (Listof 'a)) you can do it like this:

#lang typed/racket/base

(: a*? (-> Any Boolean : (Pairof 'a (Listof 'a))))
(define (a*? l)
  (: a*? (-> Any Boolean : (Listof 'a)))
  (define (a*? l)
    (cond
      [(null? l) #true]
      [(pair? l) (and
                  (equal? (car l) 'a)
                  (a*? (cdr l)))]
      [else #f]))
  (if (pair? l) (a*? l) #false))

(: use-a*? (-> Any 'a))
(define (use-a*? arg)
  (if (a*? arg)
      (car arg)
      (error 'use-a*? "bad argument: ~a" arg)))
  
(use-a*? '[])