enable proposition propagation when checking module-level exprs (#1225)

close #782

Author: capfredf

typed-racket-lib/typed-racket/typecheck/signatures.rkt

@@ -15,6 +15,10 @@
    [cond-contracted tc-expr/t (syntax? . -> . Type?)]
    [cond-contracted tc-expr/t* (syntax? . -> . (values Type? boolean?))]
    [cond-contracted single-value ((syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]
+   [cond-contracted tc-expr-seq (->* ((listof syntax?) (-> syntax? tc-results/c full-tc-results/c))
+                                     (tc-results/c
+                                      #:unreachable-op (-> (listof syntax?) void?))
+                                     full-tc-results/c)]
    [cond-contracted tc-dep-fun-arg ((syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
 
 (define-signature check-subforms^

typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt

@@ -407,34 +407,47 @@
         "expected single value, got multiple (or zero) values")]))
 
 
+(define (tc-expr-seq exps tc-expr
+                     [tail-expected (-tc-any-results #f)]
+                     #:unreachable-op [unreachable-op #f])
+  (define any-res (-tc-any-results #f))
+  (if (null? exps)
+      (-tc-any-results -tt)
+      (let loop ([exps exps])
+        (match exps
+          [(list tail-exp) (tc-expr tail-exp tail-expected)]
+          [(cons e rst)
+           (define props
+             (match (tc-expr e any-res)
+               [(tc-any-results: p) (list p)]
+               [(tc-results: tcrs _)
+                (map (match-lambda
+                       [(tc-result: _ (PropSet: p+ p-) _)
+                        (-or p+ p-)])
+                     tcrs)]))
+           (with-lexical-env+props
+             props
+             #:expected any-res
+             ;; If `e` is ill-typed and unreachable-op is supplied, call
+             ;; unreachable-op. Otherwise, check the subsequent expressions
+             #:unreachable (if unreachable-op
+                               (unreachable-op rst)
+                               (loop rst))
+             ;; Keep going with an environment extended with the
+             ;; propositions that are true if execution reaches this
+             ;; point.
+             (loop rst))]))))
+
 ;; tc-body/check: syntax? tc-results? -> tc-results?
 ;; Body must be a non empty sequence of expressions to typecheck.
 ;; The final one will be checked against expected.
 (define (tc-body/check body expected)
-  (define any-res (-tc-any-results #f))
-  (define exps (syntax->list body))
-  (let loop ([exps exps])
-    (match exps
-      [(list tail-exp) (tc-expr/check tail-exp expected)]
-      [(cons e rst)
-       (define results (tc-expr/check e any-res))
-       (define props
-         (match results
-           [(tc-any-results: p) (list p)]
-           [(tc-results: tcrs _)
-            (map (match-lambda
-                   [(tc-result: _ (PropSet: p+ p-) _)
-                    (-or p+ p-)])
-                 tcrs)]))
-       (with-lexical-env+props
-         props
-         #:expected any-res
-         ;; If `e` bails out, mark the rest as ignored.
-         #:unreachable (for-each register-ignored! rst)
-         ;; Keep going with an environment extended with the
-         ;; propositions that are true if execution reaches this
-         ;; point.
-         (loop rst))])))
+  (tc-expr-seq (syntax->list body)
+               tc-expr/check
+               expected
+               #:unreachable-op
+               ;; the expr bails out, mark the rest as ignored
+               (lambda (rst) (for-each register-ignored! rst))))
 
 ;; find-stx-type : Any [(or/c Type? #f)] -> Type?
 ;; recursively find the type of either a syntax object or the result of syntax-e

typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt

@@ -306,7 +306,7 @@
 ;; typecheck the expressions of a module-top-level form
 ;; no side-effects
 ;; syntax? -> (or/c 'no-type tc-results/c)
-(define (tc-toplevel/pass2 form [expected (-tc-any-results -tt)])
+(define (tc-toplevel/pass2 form [expected (-tc-any-results #f)])
   (do-time (format "pass2 ~a line ~a"
                    (if #t
                        (substring (~a (syntax-source form))
@@ -517,7 +517,10 @@
   (do-time "computed def-tbl")
   ;; typecheck the expressions and the rhss of defintions
   ;(displayln "Starting pass2")
-  (for-each tc-toplevel/pass2 forms)
+  (tc-expr-seq forms (lambda (expr expected)
+                       (match (tc-toplevel/pass2 expr expected)
+                                   [(? full-tc-results/c r) r]
+                                   [_ (-tc-any-results -tt)])))
   (do-time "Finished pass2")
   ;; check that declarations correspond to definitions
   ;; and that any additional parsed apps are sensible

typed-racket-test/succeed/gh-issue-782.rkt

@@ -0,0 +1,6 @@
+#lang typed/racket/base
+
+(define x : (U String (Listof Any)) '(1))
+(unless (list? x)
+  (error "not a list" x))
+(length x)