www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

assumption-equivalent-types-same-type.rkt (1075B)

      1 #lang typed/racket
      2 
      3 ;; Check that equivalent type specifications are correctly interpreted as
      4 ;; being the same type by Typed/Racket.
      5 ;; 
      6 ;; This was not the case in some situations in older versions of Typed/Racket,
      7 ;; but I am not sure whether this reproduces the same issue, or whether this
      8 ;; file would typecheck in older versions too.
      9 
     10 (let ()
     11   (define-type (Foo X)
     12     (U X (List 'foo (Bar X) (Foo X))))
     13 
     14   (define-type (Bar Y)
     15     (List 'bar (Foo Y)))
     16 
     17   (define-type (Foo2 X)
     18     (U X (List 'foo (Bar2 X) (Foo2 X))))
     19 
     20   (define-type (Bar2 Y)
     21     (List 'bar (Foo2 Y)))
     22 
     23   (λ #:∀ (A) ([x : (Foo A)])
     24     ;; Check here:
     25     (ann (ann x (Foo2 A)) (Foo A)))
     26   
     27   (void))
     28 
     29 (struct (a b) st-foo ([a : a] [b : b]))
     30 (struct (a) st-bar ([a : a]))
     31 
     32 (let ()
     33   (define-type (Foo X)
     34     (U X (st-foo (Bar X) (Foo X))))
     35 
     36   (define-type (Bar Y)
     37     (st-bar (Foo Y)))
     38 
     39   (define-type (Foo2 X)
     40     (U X (st-foo (Bar2 X) (Foo2 X))))
     41 
     42   (define-type (Bar2 Y)
     43     (st-bar (Foo2 Y)))
     44 
     45   (λ #:∀ (A) ([x : (Foo A)])
     46     ;; Check here:
     47     (ann (ann x (Foo2 A)) (Foo A)))
     48   
     49   (void))