5cd5f772d6
Since these promises re-evaluate their bodies every time they are forced, allowing them makes `force` not idempotent and not safe to treat as a path. This change is slightly backwards-incompatible, since programs that previously passed `delay/name` promises across the typed boundary will now fail at runtime. The alternative is also incompatible: stop treating `force` as a path. Since `delay/name` is quite obscure, this approach seems like the safer choice.
30 lines
954 B
Racket
30 lines
954 B
Racket
#;
|
|
(exn-pred "delay/name")
|
|
#lang racket
|
|
|
|
;; delay/name is a macro, so we wrap it with a function so we can type it:
|
|
(module untyped racket
|
|
(provide delay/name/thunk)
|
|
(define (delay/name/thunk f) (delay/name (f))))
|
|
|
|
;; Now we require/typed our function
|
|
(module typed-delay/name/thunk typed/racket
|
|
(require/typed (submod ".." untyped) [delay/name/thunk (∀ (T) (→ (→ T) (Promise T)))])
|
|
(provide delay/name/thunk))
|
|
|
|
;; This module shows the bug:
|
|
(module bug typed/racket
|
|
(require (submod ".." typed-delay/name/thunk))
|
|
|
|
(define mutable : (U 'a 'b) 'a)
|
|
|
|
(define ab-mut (delay/name/thunk (λ () (begin0 mutable
|
|
(set! mutable 'b))))) ;; BAD BAD BAD!
|
|
|
|
(ann (if (eq? (force ab-mut) 'a) ;; Here, (eq? (force ab-mut) 'a)
|
|
(force ab-mut) ;; But here, (eq? (force ab-mut) 'b)
|
|
#f)
|
|
(U 'a #f))) ;; This typechecks, and throws no warning, but prints 'b !!!
|
|
|
|
(require 'bug)
|