www

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

invariant-phantom-tr-assumptions2.rkt (2364B)

      1 #lang typed/racket
      2 
      3 (: f (→ (→ (U (Rec R (List (List 'a R)
      4                            (List 'b R)))
      5               (Rec R (List (List 'a R)
      6                            (List 'c R))))
      7            Void)
      8         Void))
      9 (define (f x) (void))
     10 
     11 (ann f (→ (→ (U (Rec K (List (List 'a K) (List 'c K)))
     12                 (Rec W (List (List 'a W) (List 'b W))))
     13              Void) Void))
     14 
     15 (ann f (→ (→ (U (Rec W (List (List 'a W) (List 'b W)))
     16                 (Rec K (List (List 'a K) (List 'c K))))
     17              Void) Void))
     18 
     19 (: g (→ (→ (Rec A (Rec B (List (List 'a A)
     20                                (List 'b B))))
     21            Void)
     22         Void))
     23 (define (g x) (void))
     24 
     25 (ann g
     26      (→ (→ (Rec B (Rec A (List (List 'a A)
     27                                (List 'b B))))
     28            Void)
     29         Void))
     30 
     31 (ann g
     32      (→ (→ (Rec X (List (List 'a X)
     33                         (List 'b X)))
     34            Void)
     35         Void))
     36 
     37 (define-type (≡ X Y) (List '≡ X Y))
     38 
     39 (: h (→ (→ (∀ (X1 X2) (→ (U (≡ (List 'a 'b X1)
     40                                (List 'c 'd X1))
     41                             (≡ (List 'e 'f X2)
     42                                (List 'g 'g X2)))))
     43            Void)
     44         Void))
     45 (define (h x) (void))
     46 
     47 
     48 (ann (λ ([x : (Rec R (Pairof 'a (Pairof 'b R)))]) (void))
     49        (-> (Rec R (Pairof 'a (Pairof 'b R))) Void))
     50 
     51 (ann (λ ([x : (Rec R (Pairof 'a (Pairof 'b R)))]) (void))
     52        (-> (Pairof 'a (Rec R (Pairof 'b (Pairof 'a R)))) Void))
     53 
     54 (ann (λ ([x : (Rec R (List 'a (List 'b R)))]) (void))
     55        (-> (List 'a (Rec R (List 'b (List 'a R)))) Void))
     56 
     57 (ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
     58        (-> (Rec R (Pairof 'a (Pairof R (Pairof (List 'b R) Null)))) Void))
     59 
     60 (ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
     61        (-> (Pairof 'a (Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))) Void))
     62 
     63 (ann (λ ([x : (Rec R (List 'a R (List 'b R)))]) (void))
     64        (-> (Pairof 'a (Pairof (Pairof 'a
     65                                       (Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))
     66                                       )
     67                               (Pairof (List 'b (Pairof 'a
     68                                                        (Rec R (Pairof (Pairof 'a R) (Pairof (List 'b (Pairof 'a R)) Null)))
     69                                                        )) Null))) Void))