The type checker doesn't see the combined domain of all the arrows.

[NoahStoryM]

What version of Racket are you using?

v8.4 [cs]

What program did you run?

#lang typed/racket/base

(define-predicate ns? (Listof Natural))
(: mul (case-> [-> One]

               [-> False False]
               [-> Natural Natural]

               [-> False (Option Natural) False]
               [-> (Option Natural) False False]
               [-> Natural Natural Natural]

               [-> False (Option Natural) (Option Natural) * False]
               [-> (Option Natural) False (Option Natural) * False]
               [-> Natural Natural Natural * Natural]
               [-> Natural Natural (Option Natural) * (Option Natural)]))
(define mul
  (case-lambda
    [()  1]
    [(n) n]
    [(n1 n2) (and n1 n2 (* n1 n2))]
    [(n1 n2 . ns)
     (and n1 n2 (ns? ns)
          (apply mul (mul n1 n2) ns))]))

(apply mul (mul 1 2) '(3 4 5 6 7))

What should have happened?

5040

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

draft.rkt:24:10: Type Checker: Bad arguments to function in `apply':
Domains: Nonnegative-Integer Nonnegative-Integer (U Exact-Nonnegative-Integer False) *
         (U Exact-Nonnegative-Integer False) False (U Exact-Nonnegative-Integer False) *
         False (U Exact-Nonnegative-Integer False) (U Exact-Nonnegative-Integer False) *
         Nonnegative-Integer 
         False 
          
Arguments: Nonnegative-Integer (Listof Nonnegative-Integer)

  in: (apply mul (mul n1 n2) ns)
  location...:
   draft.rkt:24:10
  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.

To make sure the type of mul and the type of the apply expression are correct, I tried defining mul with for/fold and it worked:

#lang typed/racket/base

(define-predicate ns? (Listof Natural))
(: mul (case-> [-> One]

               [-> False False]
               [-> Natural Natural]

               [-> False (Option Natural) False]
               [-> (Option Natural) False False]
               [-> Natural Natural Natural]

               [-> False (Option Natural) (Option Natural) * False]
               [-> (Option Natural) False (Option Natural) * False]
               [-> Natural Natural Natural * Natural]
               [-> Natural Natural (Option Natural) * (Option Natural)]))
(define mul
  (case-lambda
    [()  1]
    [(n) n]
    [(n1 n2) (and n1 n2 (* n1 n2))]
    [(n1 n2 . ns)
     (and n1 n2 (ns? ns)
          (for/fold ([res : Natural (mul n1 n2)])
                    ([n (in-list ns)])
            (mul res n)))]))

(apply mul (mul 1 2) '(3 4 5 6 7))

[capfredf]

duplicate of #691

[NoahStoryM]

Hi @capfredf , it seems that #1200 doesn't fix this issue, and I guess this issue is not a duplicate of #691.

[capfredf]

The problem is the type-checker now only treats each arrow individually and it doesn't see the combined domain of all the arrows, so to speak.

Here is a minimum non-working example analogous to your code:

(: mwe (case-> [-> Natural Natural]
               [-> Natural Natural Natural]
               [-> Natural Natural Natural * Natural]))


(define mwe
  (case-lambda
    [(a) 42]
    [(a b . c) 126]))

(apply mwe 1 (ann '(1 1) (Listof Natural))) ;; failed
(apply mwe 1 '(1 1))) ;; happy

Here, the first apply mwe is called with 1 and (ann '(1 1) (Listof Natural), both of which together make a list with at least one element. However, the last arrow expects a list with at least two elements. The type checkers fails to see all the arrows together make a list with at one element acceptable.

In your workaround, if you annotate '(3 4 5 6 7) with (Listof Natural) on the last line, the code will fail too.