typed-racket icon indicating copy to clipboard operation
typed-racket copied to clipboard

In some cases the type checker cannot infer the type of `andmap`.

Open NoahStoryM opened this issue 3 years ago • 0 comments

What version of Racket are you using?

v8.4 [cs]

What program did you run?

#lang typed/racket

(: s? [-> Any Boolean : (U Symbol (Listof Symbol))])
(define s?
  (λ (arg)
    (or (symbol? arg)
        (and (list? arg)
             (andmap symbol? arg)))))

What should have happened?

No error.

If you got an error message, please include it here.

draft.rkt:10:13: Type Checker: Polymorphic function `andmap' could not be applied to arguments:
Types: (-> a c : d) (Listof a)  -> (c : ((: (0 1) (Listof d)) | (! (0 1) (Listof d))))
       (-> a b ... b c) (Listof a) (Listof b) ... b -> (U True c)
Arguments: (-> Any Boolean : Symbol) (Listof Any)
Expected result: Boolean

  in: (andmap symbol? arg)
  location...:
   draft.rkt:10:13
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:414:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:653:0: tc-module
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:101:12
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:22:4

More.

The following two pieces of code both work:

#lang typed/racket

(: s? [-> Any Boolean : (U Symbol (Listof Symbol))])
(define s?
  (λ (arg)
    (or (symbol? arg)
        (and (list? arg)
             ((inst andmap Any Boolean Symbol) symbol? arg)))))

#lang typed/racket

(: listof? (All (A) [-> [-> Any Boolean : A]
                        [-> Any Boolean : (Listof A)]]))
(define listof?
  (λ (pred)
    (λ (arg)
      (and (list? arg)
           (andmap pred arg)))))

(: s? [-> Any Boolean : (U Symbol (Listof Symbol))])
(define s?
  (λ (arg)
    (or (symbol? arg)
        ((listof? symbol?) arg))))

NoahStoryM avatar Mar 08 '22 07:03 NoahStoryM