search

racket / typed-racket

Typed Racket
Other
522 stars 105 forks source link

In some cases, the propositional information is lost when defining predicate. #1159

Open NoahStoryM opened 2 years ago

NoahStoryM commented 2 years ago

What version of Racket are you using?

v8.2

What program did you run?

#lang typed/racket/base

(define-type Num-LS  (Listof Number))
(define-type Num-MLS (MListof Number))
(define-type Nums (U Num-LS Num-MLS))

(: num-mls? [-> (U EOF Nums) Boolean : Num-MLS])
(define (num-mls? ns)
  (and (not (eof-object? ns))
       (or (null? ns) (mpair? ns))))

What should have happened?

No error.

And there is no problem with the following code:

(: num-ls?  [-> (U EOF Nums) Boolean : Num-LS])
(define (num-ls?  ns)
  (and (not (eof-object? ns))
       (or (null? ns) (pair?  ns))))

(: num-mls? [-> (U Symbol Nums) Boolean : Num-MLS])
(define (num-mls? ns)
  (and (not (symbol? ns))
       (or (null? ns) (mpair? ns))))

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

draft.rkt:9:2: Type Checker: type mismatch;
 mismatch in proposition
  expected: ((: ns Num-MLS) | (! ns Num-MLS))
  given: (Bot | Top)
  in: (and (not (eof-object? ns)) (or (null? ns) (mpair? ns)))
  location...:
   draft.rkt:9:2
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:391:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:635: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
NoahStoryM commented 2 years ago

What version of Racket are you using?

v8.3

What program did you run?

#lang typed/racket/base

(define-type Non-Hash (Refine [t : Any] (! t HashTableTop)))
(ann eof Non-Hash)

What should have happened?

#<eof>

And there is no problem with the following code:

#lang typed/racket/base

(define-type Non-Symbol (Refine [t : Any] (! t Symbol)))
(ann eof Non-Symbol)

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

draft.rkt:4:5: Type Checker: type mismatch
  expected: Non-Hash
  given: EOF
  in: eof
  location...:
   draft.rkt:4:5
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:407:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:651: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