www

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

invariant-phantom-tr-assumptions.rkt (1040B)

      1 #lang typed/racket
      2 
      3 (struct A ())
      4 (struct B A ())
      5 (struct C A ())
      6 
      7 (: f (→ (U 'x A) Void))
      8 (define (f _) (void))
      9 
     10 (let ()
     11   (ann f (→ (U B C) Void))
     12   (ann f (→ (U 'x B C) Void))
     13   (ann f (→ (U 'x C) Void))
     14   (ann f (→ (U 'x A C) Void))
     15   (ann f (→ (U 'x) Void))
     16   (ann f (→ (U) Void))
     17   (void))
     18 
     19 ;;;;;;;;;;
     20 
     21 ;; Reverse order (BB, CC and DD are more precise invariants than AA)
     22 (struct AA ())
     23 (struct BB AA ())
     24 (struct CC AA ())
     25 (struct DD AA ())
     26 
     27 (define-type (Invariant X) (→ X Void))
     28 
     29 (: g (→ (U (Invariant 'x) (Invariant BB) (Invariant CC)) Void))
     30 (define (g _) (void))
     31 
     32 ;; Everything works as expected
     33 (let ()
     34   (ann g (→ (U (Invariant BB) (Invariant CC)) Void))
     35   (ann g (→ (U (Invariant 'x) (Invariant BB) (Invariant CC)) Void))
     36   (ann g (→ (U (Invariant 'x) (Invariant CC)) Void))
     37   (ann g (→ (U (Invariant 'x)) Void))
     38   (ann g (→ (U) Void))
     39   ;; AA works, as it should
     40   (ann g (→ (U (Invariant 'x) (Invariant AA) (Invariant CC)) Void))
     41   (ann g (→ (U (Invariant 'x) (Invariant AA)) Void))
     42   (void))