diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt index 3559578ecf..19bb8a3da6 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt @@ -176,10 +176,8 @@ [(e e) (empty-cset X Y)] [(e (Top:)) (empty-cset X Y)] ;; FIXME - is there something to be said about the logical ones? - [((TypeFilter: s p i) (TypeFilter: t p i)) - (% cset-meet (cgen V X Y s t) (cgen V X Y t s))] - [((NotTypeFilter: s p i) (NotTypeFilter: t p i)) - (% cset-meet (cgen V X Y s t) (cgen V X Y t s))] + [((TypeFilter: s p i) (TypeFilter: t p i)) (cgen/inv V X Y s t)] + [((NotTypeFilter: s p i) (NotTypeFilter: t p i)) (cgen/inv V X Y s t)] [(_ _) #f])) ;; s and t must be *latent* filter sets @@ -337,10 +335,14 @@ (for/list/fail ([s (in-list flds-s)] [t (in-list flds-t)]) (match* (s t) ;; mutable - invariant - [((fld: s _ #t) (fld: t _ #t)) (cset-meet (cgen V X Y s t) (cgen V X Y t s))] + [((fld: s _ #t) (fld: t _ #t)) (cgen/inv V X Y s t)] ;; immutable - covariant [((fld: s _ #f) (fld: t _ #f)) (cgen V X Y s t)])))) +(define (cgen/inv V X Y s t) + (% cset-meet (cgen V X Y s t) (cgen V X Y t s))) + + ;; V : a set of variables not to mention in the constraints ;; X : the set of type variables to be constrained ;; Y : the set of index variables to be constrained @@ -357,6 +359,9 @@ (define/cond-contract (cg S T) (Type/c Type/c . -> . (or/c #f cset?)) (cgen V X Y S T)) + (define/cond-contract (cg/inv S T) + (Type/c Type/c . -> . cset?) + (cgen/inv V X Y S T)) ;; this places no constraints on any variables in X (define empty (empty-cset X Y)) ;; this constrains just x (which is a single var) @@ -638,24 +643,24 @@ ;; Invariant here because struct types aren't subtypes just because the ;; structs are (since you can make a constructor from the type). [((StructType: s) (StructType: t)) - (% cset-meet (cg s t) (cg t s))] + (cg/inv s t)] ;; vectors are invariant - generate constraints *both* ways [((Vector: e) (Vector: e*)) - (% cset-meet (cg e e*) (cg e* e))] + (cg/inv e e*)] ;; boxes are invariant - generate constraints *both* ways [((Box: e) (Box: e*)) - (% cset-meet (cg e e*) (cg e* e))] + (cg/inv e e*)] [((MPair: s t) (MPair: s* t*)) - (% cset-meet (cg s s*) (cg s* s) (cg t t*) (cg t* t))] + (% cset-meet (cg/inv s s*) (cg/inv t t*))] [((Channel: e) (Channel: e*)) - (% cset-meet (cg e e*) (cg e* e))] + (cg/inv e e*)] [((ThreadCell: e) (ThreadCell: e*)) - (% cset-meet (cg e e*) (cg e* e))] + (cg/inv e e*)] [((Continuation-Mark-Keyof: e) (Continuation-Mark-Keyof: e*)) - (% cset-meet (cg e e*) (cg e* e))] + (cg/inv e e*)] [((Prompt-Tagof: s t) (Prompt-Tagof: s* t*)) - (% cset-meet (cg s s*) (cg s* s) (cg t t*) (cg t* t))] + (% cset-meet (cg/inv s s*) (cg/inv t t*))] [((Promise: e) (Promise: e*)) (cg e e*)] [((Ephemeron: e) (Ephemeron: e*)) @@ -690,7 +695,7 @@ ;; we assume all HTs are mutable at the moment [((Hashtable: s1 s2) (Hashtable: t1 t2)) ;; for mutable hash tables, both are invariant - (% cset-meet (cg t1 s1) (cg s1 t1) (cg t2 s2) (cg s2 t2))] + (% cset-meet (cg/inv s1 t1) (cg/inv s2 t2))] ;; syntax is covariant [((Syntax: s1) (Syntax: s2)) (cg s1 s2)]