Add support for typechecking contracted functions

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt

@@ -9,6 +9,7 @@
          "tc-app/tc-app-objects.rkt"
          "tc-app/tc-app-special.rkt"
          "tc-app/tc-app-values.rkt"
+         "tc-app/tc-app-contracts.rkt"
          "tc-app/tc-app-main.rkt"
          "signatures.rkt")
 
@@ -23,4 +24,5 @@
         tc-app-hetero@ tc-app-list@ tc-app-apply@
         (() tc-app-values@)
         tc-app-keywords@
-        tc-app-objects@ tc-app-eq@ tc-app-lambda@ tc-app-special@))
+        tc-app-objects@ tc-app-eq@ tc-app-lambda@ tc-app-special@
+        tc-app-contracts@))

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/signatures.rkt

@@ -36,3 +36,6 @@
 (define-signature tc-app-special^
   ([cond-contracted tc/app-special checker/c]))
 
+(define-signature tc-app-contracts^
+  ([cond-contracted tc/app-contracts checker/c]))
+

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt

@@ -0,0 +1,40 @@
+#lang racket/unit
+
+;; This module provides custom type-checking rules for the expansion
+;; of contracted values
+
+(require "../../utils/utils.rkt"
+         "signatures.rkt"
+         "utils.rkt"
+         syntax/parse syntax/stx racket/match
+         racket/dict
+         racket/format
+         (env global-env)
+         (typecheck signatures)
+         (types base-abbrev resolve subtype union utils)
+         (rep type-rep)
+         (utils tc-utils)
+         (for-template racket/base
+                       ;; shift -1 because it's provided +1
+                       racket/contract/private/provide))
+
+(import tc-expr^)
+(export tc-app-contracts^)
+
+(define-tc/app-syntax-class (tc/app-contracts expected)
+  (pattern (ctc-id:id blame e ...)
+    ;; check that this is an application from the contract system
+    #:when (contract-rename-id-property #'ctc-id)
+    (check-contract #'ctc-id #'(e ...) expected)))
+
+;; Assume that the contracted thing is of the same type the type
+;; environment assigned to the exported identifier. Note that this
+;; is only sound if the contract is a chaperone contract, so don't
+;; put things in the base type environment if they have impersonator
+;; contracts installed.
+(define (check-contract orig-value-id other-args expected)
+  (tc-expr/check #`(#%plain-app
+                    #,(contract-rename-id-property orig-value-id)
+                    . #,other-args)
+                 expected))
+

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt

@@ -10,7 +10,10 @@
          (rep type-rep)
          (utils tc-utils)
          (r:infer infer)
-         (for-label racket/base))
+         (for-label racket/base)
+         ;; adjusted -1 since it's provided for-syntax
+         (only-in (for-template racket/contract/private/provide)
+                  contract-neg-party-property))
 
 
 (import tc-expr^)
@@ -24,10 +27,17 @@
                  ((#%plain-app cpce s-kp fn kpe kws num)
                   kw-list
                   (#%plain-app list . kw-arg-list)
-                  . pos-args))
+                  . *pos-args))
     #:declare cpce (id-from 'checked-procedure-check-and-extract 'racket/private/kw)
     #:declare s-kp (id-from 'struct:keyword-procedure 'racket/private/kw)
     #:declare kpe  (id-from 'keyword-procedure-extract 'racket/private/kw)
+    ;; If this application is of a module boundary contract function or not
+    ;; If #t, then the contract system has inserted an extra argument which we
+    ;; need to ignore
+    #:attr boundary-ctc? (contract-neg-party-property #'fn)
+    #:with pos-args (if (attribute boundary-ctc?)
+                        (stx-cdr #'*pos-args)
+                        #'*pos-args)
     (match (tc-expr #'fn)
       [(tc-result1:
         (Poly: vars

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt

@@ -12,7 +12,8 @@
 
 (import tc-expr^ tc-app-keywords^
         tc-app-hetero^ tc-app-list^ tc-app-apply^ tc-app-values^
-        tc-app-objects^ tc-app-eq^ tc-app-lambda^ tc-app-special^)
+        tc-app-objects^ tc-app-eq^ tc-app-lambda^ tc-app-special^
+        tc-app-contracts^)
 (export tc-app^)
 
 (define-tc/app-syntax-class (tc/app-regular* expected)
@@ -34,6 +35,7 @@
   tc/app-objects
   tc/app-lambda
   tc/app-special
+  tc/app-contracts
   tc/app-regular*)
 
 ;; the main dispatching function

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

@@ -17,7 +17,9 @@
          (only-in racket/list split-at)
          (typecheck internal-forms tc-envops)
          ;; Needed for current implementation of typechecking letrec-syntax+values
-         (for-template (only-in racket/base letrec-values))
+         (for-template (only-in racket/base letrec-values)
+                       ;; see tc-app-contracts.rkt
+                       racket/contract/private/provide)
 
          (for-label (only-in '#%paramz [parameterization-key pz:pk])
                     (only-in racket/private/class-internal find-method/who)))
@@ -35,7 +37,9 @@
 ;; tc-id : identifier -> tc-results
 (define/cond-contract (tc-id id)
   (--> identifier? full-tc-results/c)
-  (let* ([ty (lookup-type/lexical id)])
+  (define rename-id (contract-rename-id-property id))
+  (define id* (or rename-id id))
+  (let* ([ty (lookup-type/lexical id*)])
     (ret ty
          (make-FilterSet (-not-filter (-val #f) id)
                          (-filter (-val #f) id))

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

@@ -18,6 +18,7 @@
          (for-template
           (only-in syntax/location quote-module-name)
           racket/base
+          racket/contract/private/provide
           (env env-req)))
 
 (provide/cond-contract
@@ -103,6 +104,10 @@
        (register-scoped-tvars #'t.id (parse-literal-alls #'t.type))
        (list)]
 
+      ;; definitions lifted from contracts should be ignored
+      [(define-values (lifted) expr)
+       #:when (contract-lifted-property #'expr)
+       (list)]
 
       ;; values definitions
       [(define-values (var ...) expr)
@@ -150,6 +155,11 @@
       #:literals (define-values begin)
       [(~or _:ignore^ _:ignore-some^) (list)]
 
+      ;; definitions lifted from contracts should be ignored
+      [(define-values (lifted) expr)
+       #:when (contract-lifted-property #'expr)
+       (list)]
+
       [(define-values (var ...) expr)
        (define vars (syntax->list #'(var ...)))
        (syntax-parse vars
@@ -211,6 +221,11 @@
       ;; module* is not expanded, so it doesn't have a `#%plain-module-begin`
       [(module* n spec body ...) 'no-type]
 
+      ;; definitions lifted from contracts should be ignored
+      [(define-values (lifted) expr)
+       #:when (contract-lifted-property #'expr)
+       'no-type]
+
       ;; definitions just need to typecheck their bodies
       [(define-values () expr)
        (tc-expr/check #'expr (ret empty))