First pass of changes from PR review

Author: btlachance

typed-racket-doc/typed-racket/scribblings/reference/typed-contracts.scrbl

@@ -77,6 +77,7 @@ currently supported in Typed Racket.
               @defthing[natural-number/c (FlatCon Any Natural)]
               @defproc[(string-len/c [len Real])
                        (FlatCon Any String)]
+              @defthing[false/c (Con Any False)]
               @defthing[printable/c (FlatCon Any Any)]
               @defproc[(listof [c (Con a b)])
                        (Con (Listof a) (Listof b))]

typed-racket-lib/typed-racket/base-env/contract-prims.rkt

@@ -21,11 +21,10 @@
          ;; syntax objects for surface-level types (e.g. Real instead of -Real)
          (base-env base-types base-types-extra)
          (prefix-in untyped: racket/contract/base))
-(provide (except-out (all-defined-out)
-                     define-contract)
-         ;; TODO: since we don't support all of the p/c-item forms (exists,
-         ;; struct, etc.), we really should provide our own versions of these
-         ;; two forms that give good "x is unsupported" messages
+(provide ;; TODO:  we don't support all of the p/c-item forms
+         ;; (exists, struct, etc.), we really should provide our own
+         ;; versions of provide/contract and contract-out that give
+         ;; good "x is unsupported" messages
          (rename-out [untyped:provide/contract provide/contract]
                      [untyped:contract-out contract-out]
                      [untyped:contract contract]))
@@ -37,6 +36,7 @@
   (syntax-parse stx
     [(_  :def ...)
      #'(begin
+         (provide ctc ...)
          (define-syntax ctc
            (make-variable-like-transformer
             #`(#,(ignore-some-expr-property #'#%expression #'ty)
@@ -62,9 +62,7 @@
            (-> Integer Integer (FlatCon Any Integer)))]
   [natural-number/c (FlatCon Any Natural)]
   [string-len/c (-> Real (FlatCon Any String))]
-  ;; Because we can use FlatCon in function position and because false/c = #f,
-  ;; giving it the type below is not sound
-  ;; [false/c (FlatCon Any False)]
+  [false/c (Con Any False)]
   [printable/c (FlatCon Any Any)]
   ;; one-of/c
   ;; vectorof

typed-racket-lib/typed-racket/infer/infer-unit.rkt

@@ -617,23 +617,21 @@
         [((Distinction: _ _ S) T)
          (cg S T obj)]
 
-        ;; XXX only barely noticed that cg takes an obj parameter
-        ;; halfway through the rebase
         [((Con: S-pre S-post) (Con: T-pre T-post))
-         (% cset-meet (cg T-pre S-pre obj) (cg S-post T-post obj))]
+         (% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
         [((FlatCon: S-pre S-post) (FlatCon: T-pre T-post))
-         (% cset-meet (cg T-pre S-pre obj) (cg S-post T-post obj))]
+         (% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
         [((FlatCon: S-pre S-post) (Con: T-pre T-post))
-         (% cset-meet (cg T-pre S-pre obj) (cg S-post T-post obj))]
+         (% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
         [((and (PredicateProp: (PropSet: (TypeProp: _ S-post) _))
                (Fun: (list (Arrow: (list S-pre) _ _ _))))
           ;; Apparently I can't just have the FlatCon case -- is the inference
           ;; not aware of the subtyping relation?
           (Con*: T-pre T-post))
-         (% cset-meet (cg T-pre S-pre obj) (cg S-post T-post obj))]
+         (% cset-meet (cg T-pre S-pre) (cg S-post T-post))]
         [((Fun: (list (Arrow: (list S-pre) _ _ _)))
           (Con*: T-pre T-post))
-         (% cset-meet (cg T-pre S-pre obj) (cg S-pre T-post obj))]
+         (% cset-meet (cg T-pre S-pre) (cg S-pre T-post))]
 
         ;; two structs with the same name
         ;; just check pairwise on the fields

typed-racket-lib/typed-racket/infer/infer.rkt

@@ -6,7 +6,7 @@
                   define-values/invoke-unit/infer link
                   only))
 
-(provide-signature-elements intersect^ infer^ (only constraints^ meet join))
+(provide-signature-elements intersect^ infer^)
 
 (define-values/invoke-unit/infer
   (link infer@ constraints@ dmap@ intersect@))

typed-racket-lib/typed-racket/types/pairwise-intersect.rkt

@@ -13,7 +13,7 @@
 
 (provide pairwise-intersect)
 
-(define (pairwise-intersect/arr s t)
+(define (pairwise-intersect/arrow s t)
   (match* (s t)
     [((Arrow: s-dom s-rest s-kws s-rng)
       (Arrow: t-dom t-rest t-kws t-rng))
@@ -84,7 +84,7 @@
     [(u (Univ:)) u]
     [((Fun: arr1s) (Fun: arr2s))
      #:when (= (length arr1s) (length arr2s))
-     (make-Fun (map pairwise-intersect/arr arr1s arr2s))]
+     (make-Fun (map pairwise-intersect/arrow arr1s arr2s))]
     [((Result: ss pset-s o1) (Result: ts pset-t o2))
      (make-Result (pairwise-intersect ss ts)
                   (pairwise-intersect/prop-set pset-s pset-t)

typed-racket-lib/typed-racket/types/subtype.rkt

@@ -706,8 +706,8 @@
    (match t2
      [(Con: t2-pre t2-post)
       (subtype-seq A
-                   (subtype* A t2-pre t1-pre obj)
-                   (subtype* A t1-post t2-post obj))]
+                   (subtype* t2-pre t1-pre)
+                   (subtype* t1-post t2-post))]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Continuation-Mark-Keyof (Continuation-Mark-Keyof: val1))
    (match t2
@@ -813,12 +813,12 @@
    (match t2
      [(FlatCon: t2-pre t2-post)
       (subtype-seq A
-                   (subtype* A t2-pre t1-pre)
-                   (subtype* A t1-post t2-post))]
+                   (subtype* t2-pre t1-pre)
+                   (subtype* t1-post t2-post))]
      [(Con: t2-pre t2-post)
       (subtype-seq A
-                   (subtype* A t2-pre t1-pre)
-                   (subtype* A t1-post t2-post))]
+                   (subtype* t2-pre t1-pre)
+                   (subtype* t1-post t2-post))]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Fun (Fun: arrows1))
    (match* (t2 arrows1)
@@ -842,12 +842,11 @@
      [((or (FlatCon: t2-pre t2-post)
            (Con: t2-pre t2-post))
        _)
-      ;; XXX hacks
       (match t1
         [(ConFn*: t1-pre t1-post)
          (subtype-seq A
-                      (subtype* A t2-pre t1-pre)
-                      (subtype* A t1-post t2-post))])]
+                      (subtype* t2-pre t1-pre)
+                      (subtype* t1-post t2-post))])]
      [(_ _) (continue<: A t1 t2 obj)])]
   [(case: Future (Future: elem1))
    (match t2

typed-racket-lib/typed-racket/utils/contract-utils.rkt

@@ -62,7 +62,7 @@
 ;; Assumes ty has non-#f confn-type-components
 (define (confn-out ty) (cadr (confn-type-components ty)))
 ;; confn-type-components : Type? -> #f or ConFnInfo
-;; Note: only gets components for functions with a single unary arr
+;; Note: only gets components for functions with a single unary arrow
 (define (confn-type-components ty)
   ;; TODO: find all unary arities and union their inputs/meet their outputs
   (match ty

typed-racket-lib/typed/racket/contract.rkt

@@ -1,11 +1,5 @@
 #lang typed-racket/minimal
 (require racket/require
-         ;; (subtract-in racket/contract
-         ;;              typed-racket/base-env/contract-prims)
          typed-racket/base-env/contract-prims)
 
-(provide (all-from-out typed-racket/base-env/contract-prims)
-         ;; (except-out (all-from-out racket/contract) case-> ->* ->)
-         ;; (rename-out [case-> case->/c]
-         ;;             [->* ->*/c])
-         )
+(provide (all-from-out typed-racket/base-env/contract-prims))

typed-racket-test/unit-tests/typed-contracts-tests.rkt

@@ -44,7 +44,7 @@
     [tc-e (integer-in 17 71) (-FlatCon Univ -PosInt)]
     [tc-e (string-len/c 3) (-FlatCon Univ -String)]
     [tc-e natural-number/c (-FlatCon Univ -Nat)]
-    [tc-e false/c (-FlatCon Univ -False)]
+    [tc-e false/c (-Con Univ -False)]
     [tc-e printable/c (-FlatCon Univ Univ)]
     [tc-e (listof (>/c 5)) (-Con (-lst Univ) (-lst -Real))]
     [tc-e (listof string?) (-Con (-lst Univ) (-lst -String))]