abort/cc under a call/prompt cannot be invoked normally

[dannypsnl]

What version of Racket are you using?

v8.12 [cs]

What program did you run?

#lang typed/racket
(require/typed racket/control
               [abort/cc
                ((Prompt-Tagof Any (-> Any Void))
                 (-> Any Void)
                 Number
                 -> Void)]
               [call/prompt
                ((-> Void)
                 (Prompt-Tagof Any (-> Any Void))
                 Any
                 -> Any)])

(: tag : (Prompt-Tagof Any (-> Any Void)))
(define tag (make-continuation-prompt-tag 'tag))

(: f : -> Void)
(define (f)
  (println 1)
  (call/cc (λ ([k : (-> Any Void)]) (abort/cc tag k 2)))
  (println 3)
  (call/cc (λ ([k : (-> Any Void)]) (abort/cc tag k 4)))
  (println 5))

(call/prompt f
             tag
             (λ ([resume : (-> Any Void)]
                 [v : Number])
               (println v)
               (resume 'ignore)))

What should have happened?

As a very similar untyped version can print 1-5 in order.

#lang racket
(require racket/control)

(define tag (make-continuation-prompt-tag 'tag))

(define (f)
  (println 1)
  (call/cc (λ (k) (abort/cc tag k 2)))
  (println 3)
  (call/cc (λ (k) (abort/cc tag k 4)))
  (println 5))

(call/prompt f
             tag
             (λ (resume v)
               (println v)
               (resume)))

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

At (abort/cc tag k 2) invoke

result arity mismatch;
 expected number of values not received
  expected: 2
  received: 1
  at: use of prompt-abort redirecting procedure
  arguments...:

[rfindler]

Looks like a bug in the contract system somewhere. This program produces the same error:

#lang racket
(require racket/control)

(define/contract abort/cc+contract
  (-> (prompt-tag/c (-> any/c void?))
      (-> any/c void?)
      number?
      void?)
   abort/cc)

(define tag (make-continuation-prompt-tag 'tag))

(define (f)
  (println 1)
  (call/cc (λ (k) (abort/cc+contract tag k 2)))
  (println 3)
  (call/cc (λ (k) (abort/cc+contract tag k 4)))
  (println 5))

(call/prompt f
             tag
             (λ (resume v)
               (println v)
               (resume)))

[dannypsnl]

update, I got a working version, though I hasn't fully understand the type check

#lang typed/racket
(require/typed racket/control
               [abort/cc
                ((Prompt-Tagof Number (-> (-> Number Void) Number Void))
                 (-> Number Void)
                 Number
                 -> Void)]
               [call/prompt
                ((-> Void)
                 (Prompt-Tagof Number (-> (-> Number Void) Number Void))
                 (-> (-> Number Void) Number Void)
                 -> Void)])

(: tag : (Prompt-Tagof Number (-> (-> Number Void) Number Void)))
(define tag (make-continuation-prompt-tag 'tag))

(: f : -> Void)
(define (f)
  (println 1)
  (println (call/cc (λ ([k : (-> Number Void)]) (abort/cc tag k 2))))
  (println 3)
  (println (call/cc (λ ([k : (-> Number Void)]) (abort/cc tag k 4))))
  (println 5))

(call/prompt f
             tag
             (λ ([resume : (-> Number Void)]
                 [v : Number])
               (println v)
               (resume 10)))