Initial support for typed units in typed racket.

Most unit forms are supported, including most of the "infer" forms that
infer imports/exports/linkages from the current context.

Notably, none of the structural linking forms for units are supported, and
`define-unit-binding` is also currently unsupported.

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

@@ -25,6 +25,7 @@
  (only-in (types numeric-tower) [-Number N])
  (only-in (rep type-rep)
           make-ClassTop
+          make-UnitTop
           make-Name
           make-ValuesDots
           make-MPairTop
@@ -1159,6 +1160,9 @@
 [object-info (-> (-object) (-values (list (Un (make-ClassTop) (-val #f)) -Boolean)))]
 ;; TODO: class-info (is this sound to allow?)
 
+;; Section 7.8 (Unit Utilities)
+[unit? (make-pred-ty (make-UnitTop))]
+
 ;; Section 9.1
 [exn:misc:match? (-> Univ B)]
 ;; this is a hack

typed-racket-lib/typed-racket/base-env/base-special-env.rkt

@@ -13,6 +13,7 @@
  (rename-in (types abbrev numeric-tower union) [make-arr* make-arr])
  (for-syntax racket/base syntax/parse
              (only-in racket/syntax syntax-local-eval)))
+(provide make-template-identifier)
 
 (define (make-template-identifier what where)
   (let ([name (module-path-index-resolve (module-path-index-join where #f))])

typed-racket-lib/typed-racket/base-env/base-types-extra.rkt

@@ -16,7 +16,7 @@
 ;; special type names that are not bound to particular types
 (define-other-types
   -> ->* case-> U Rec All Opaque Vector
-  Parameterof List List* Class Object Values AnyValues Instance Refinement
+  Parameterof List List* Class Object Unit Values AnyValues Instance Refinement
   pred Struct Struct-Type Prefab Top Bot Distinction)
 
 (provide (rename-out [All ∀]

typed-racket-lib/typed-racket/base-env/base-types.rkt

@@ -126,6 +126,7 @@
 [Continuation-Mark-KeyTop -Continuation-Mark-KeyTop]
 [Struct-TypeTop (make-StructTypeTop)]
 [ClassTop (make-ClassTop)]
+[UnitTop (make-UnitTop)]
 [Keyword -Keyword]
 [Thread -Thread]
 [Resolved-Module-Path -Resolved-Module-Path]

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

@@ -19,13 +19,15 @@
 
 (provide require/opaque-type require-typed-struct-legacy require-typed-struct
          require/typed-legacy require/typed require/typed/provide
-         require-typed-struct/provide cast make-predicate define-predicate)
+         require-typed-struct/provide cast make-predicate define-predicate
+         require-typed-signature)
 
 (module forms racket/base
   (require (for-syntax racket/lazy-require racket/base))
   (begin-for-syntax 
     (lazy-require [(submod "..")
-                   (require/opaque-type 
+                   (require/opaque-type
+                    require-typed-signature
                     require-typed-struct-legacy
                     require-typed-struct
                     require/typed-legacy require/typed require/typed/provide
@@ -36,7 +38,8 @@
        (with-syntax ([(names ...) (generate-temporaries #'(id ...))])
          #'(begin (provide (rename-out [names id] ...))
                   (define-syntax (names stx) (id stx)) ...))]))
-  (def require/opaque-type 
+  (def require/opaque-type
+        require-typed-signature
         require-typed-struct-legacy
         require-typed-struct
         require/typed-legacy require/typed require/typed/provide
@@ -121,6 +124,11 @@
               (~var constructor (opt-constructor legacy #'nm.nm))]
              #:with (constructor-parts ...) #'constructor.value))
 
+  (define-syntax-class signature-clause
+    #:literals (:)
+    #:attributes (sig-name [var 1] [type 1])
+    (pattern [#:signature sig-name:id ([var:id : type] ...)]))
+
   (define-syntax-class opaque-clause
     ;#:literals (opaque)
     #:attributes (ty pred opt)
@@ -135,6 +143,8 @@
      #`(require/opaque-type oc.ty oc.pred #,lib . oc.opt))
    (pattern (~var strc (struct-clause legacy)) #:attr spec
      #`(require-typed-struct strc.nm (strc.body ...) strc.constructor-parts ... #,lib))
+   (pattern sig:signature-clause #:attr spec
+     #`(require-typed-signature sig.sig-name (sig.var ...) (sig.type ...) #,lib))
    (pattern sc:simple-clause #:attr spec
      #`(require/typed #:internal sc.nm sc.ty #,lib)))
 
@@ -442,3 +452,18 @@
                            [sel (nm -> ty)]) ...)))]))
 
   (values (rts #t) (rts #f))))
+
+(define (require-typed-signature stx)
+  (syntax-parse stx
+    #:literals (:)
+    [(_ sig-name:id (var ...) (type ...) lib)
+     (quasisyntax/loc stx
+       (begin
+         (require (only-in lib sig-name))
+         #,(internal (quasisyntax/loc stx
+                       (define-signature-internal sig-name
+                         #:parent-signature #f
+                         ([var type] ...)
+                         ;; infer parent relationships using the static information
+                         ;; bound to this signature
+                         #:check? #t)))))]))

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

@@ -0,0 +1,108 @@
+#lang racket/base
+
+;; This file implements unit signatures for typed racket
+
+(provide define-signature)
+
+(require "../utils/utils.rkt"
+         "colon.rkt"
+         (for-syntax syntax/parse
+                     racket/base
+                     racket/list
+                     racket/syntax
+                     syntax/kerncase
+                     "../private/syntax-properties.rkt"
+                     (typecheck internal-forms)
+                     syntax/id-table
+                     racket/dict
+                     racket/unit-exptime
+                     (utils tc-utils))
+         (only-in racket/unit
+                  [define-signature untyped-define-signature]
+                  extends)
+         (for-label "colon.rkt")
+         (submod "../typecheck/internal-forms.rkt" forms)
+         (only-in "../../typed/racket/base.rkt" define-type))
+
+(begin-for-syntax 
+  (define-literal-set colon #:for-label (:))
+  
+  ;; TODO: there should be a more extensible way of handling signatures
+  (define-syntax-class signature-forms
+    (pattern (form:def-sig-form ...)))
+  
+  (define-syntax-class def-sig-form
+    #:attributes (internal-form erased)
+    (pattern :sig-var-form
+             #:attr kind 'var)
+    ;; The define-type form is explicitly disallowed until I can figure out how
+    ;; to sensibly support them in signature definitions - dfeltey
+    (pattern :sig-type-form
+             #:fail-when #t "type definitions are not allowed within signature definitions"
+             #:attr kind 'type))
+  
+  (define-syntax-class sig-var-form
+    #:literal-sets (colon)
+    (pattern [name:id : type]
+             #:with internal-form #'(name type)
+             #:with erased #'name))
+
+  ;; Preliminary support for type definitions in signatures
+  ;; The form is allowed in signature definitions, but currently
+  ;; fails on parsing.
+  ;; In the future supporting type definitions inside of signatures
+  ;; would be a worthwhile feature, but their implemention is not obvious
+  (define-syntax-class sig-type-form
+    #:literals (define-type)
+    (pattern (define-type t ty)
+             ;; These attributes are dummy values
+             #:attr internal-form #f
+             #:attr erased #f))
+  
+  (define-splicing-syntax-class extends-form
+    #:literals (extends)
+    (pattern (~seq extends super:id)
+             #:with internal-form #'super
+             #:with extends-id #'super
+             #:attr form #'(extends super))
+    (pattern (~seq)
+             #:with internal-form #'#f
+             #:with extends-id '()
+             #:attr form '())))
+
+
+;; process-signature-forms : (listof syntax?) -> (listof (pairof id id))
+;; Processes the raw syntax of signature forms and returns a list
+;; of pairs representing names and types bound by the signature
+(define-for-syntax (process-signature-forms forms)
+  (for/list ([form (in-list forms)])
+    (syntax-parse form
+      [member:sig-var-form
+       (syntax-e #'member.internal-form)])))
+
+
+;; typed define-signature macro
+;; This expands into the untyped define-signature syntax as well as an
+;; internal form used by TR to register signatures in the signature environment
+;; The `define-signature-internal` form specifies
+;; - the `name` of the signature being defined
+;; - it's parent-signature, or #f if this signature does not extend another signature
+;; - the list of member variables contained in this signature along with their types
+;; - and a boolean flag indicating whether the signature came from an instance of
+;;   require/typed in which case additional checking must occur when the internal
+;;   form is parsed
+(define-syntax (define-signature stx)
+  (syntax-parse stx
+    [(_ sig-name:id super-form:extends-form forms:signature-forms)
+     (define members (process-signature-forms (syntax->list #'forms)))
+     (define erased-members (map car members))
+     #`(begin
+         #,(ignore (quasisyntax/loc stx
+                     (untyped-define-signature sig-name #,@(attribute super-form.form)
+                                               (#,@erased-members))))
+         #,(internal (quasisyntax/loc stx
+                       (define-signature-internal sig-name
+                         #:parent-signature super-form.internal-form
+                         (#,@members)
+                         ;; no need to further check parent information
+                         #:check? #f))))]))

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

@@ -0,0 +1,492 @@
+#lang racket/base
+
+;; Primitive forms for units/signatures
+
+(provide unit
+         define-unit
+         compound-unit 
+         define-compound-unit
+         compound-unit/infer
+         define-compound-unit/infer
+         invoke-unit
+         invoke-unit/infer
+         define-values/invoke-unit
+         define-values/invoke-unit/infer
+         unit-from-context
+         define-unit-from-context)
+
+
+(require  "../utils/utils.rkt"
+          "colon.rkt"
+          (for-syntax syntax/parse
+                      racket/base
+                      racket/list
+                      racket/match
+                      racket/syntax
+                      racket/sequence
+                      syntax/context
+                      syntax/flatten-begin
+                      syntax/kerncase
+                      "../private/syntax-properties.rkt"
+                      (typecheck internal-forms)
+                      syntax/id-table
+                      racket/dict
+                      racket/unit-exptime
+                      syntax/strip-context
+                      (utils tc-utils)
+                      syntax/id-table
+                      syntax/id-set)
+          (prefix-in untyped- (only-in racket/unit
+                                       define-signature
+                                       unit
+                                       invoke-unit
+                                       invoke-unit/infer
+                                       compound-unit
+                                       define-unit
+                                       define-compound-unit
+                                       define-values/invoke-unit
+                                       define-values/invoke-unit/infer
+                                       compound-unit/infer
+                                       define-compound-unit/infer
+                                       unit-from-context
+                                       define-unit-from-context))
+          (only-in racket/unit
+                   extends
+                   import
+                   export
+                   init-depend
+                   link
+                   prefix
+                   rename)
+          "base-types.rkt"
+          "base-types-extra.rkt"
+          (for-label "colon.rkt")
+          (for-template (rep type-rep))
+          (submod "../typecheck/internal-forms.rkt" forms))
+
+(begin-for-syntax
+  (define-literal-set colon #:for-label (:))
+
+  ;; process-definition-form handles all of the `define-` style unit macros
+  ;; such as define-unit, define-compound-unit, define-unit-from-context. but
+  ;; not the corresponding unit, compound-unit, etc forms
+  ;; Performs local expansion in order to apply a syntax property to the
+  ;; subexpression of the `define-*` form correpsonding to the body of the
+  ;; definition being created
+  ;; - eg for a define-unit form, a syntax property will be attached to the
+  ;;   subexpression that creates the unit
+  (define (process-definition-form apply-property stx)
+    (define exp-stx (local-expand stx (syntax-local-context) (kernel-form-identifier-list)))
+    (syntax-parse exp-stx
+      #:literal-sets (kernel-literals)
+      [(begin e ...)
+       (quasisyntax/loc stx
+         (begin #,@(map (λ (e) (process-definition-form apply-property e))
+                        (syntax->list #'(e ...)))))]
+      [(define-values (name ...) rhs)
+       (quasisyntax/loc stx (define-values (name ...) #,(ignore (apply-property #'rhs))))]
+      ;; define-syntaxes that actually create the binding given in the
+      ;; `define-*` macro will fall through to this case, and should be left as-is
+      [_ exp-stx]))
+
+
+  (define-splicing-syntax-class init-depend-form
+    #:literals (init-depend)
+    (pattern (~and this-syntax (init-depend sig:id ...))
+             #:attr form (list #'this-syntax)
+             #:with names #'(sig ...))
+    (pattern (~seq)
+             #:attr form '()
+             #:with names #'()))
+  
+  ;; The `rename` attribute in the sig-spec syntax class is used to correctly
+  ;; map names of signature bound variables in unit bodies to their names in
+  ;; the fully expanded syntax. It applies prefixes and renamings from
+  ;; signature specifications to identifiers.
+  (define-syntax-class sig-spec
+    #:literals (prefix rename)
+    (pattern sig-id:id
+             #:attr rename (lambda (id) id)
+             #:with sig-name #'sig-id)
+    (pattern (prefix p:id sig:sig-spec)
+             #:attr rename (lambda (id) (format-id #'sig.sig-name
+                                                 "~a~a"
+                                                 #'p
+                                                 ((attribute sig.rename) id)))
+             #:with sig-name #'sig.sig-name)
+    (pattern (rename sig:sig-spec (new:id old:id) ...)
+             #:attr rename 
+             (lambda (id)
+               (define (lookup id)
+                 (for/first ([old-id (in-syntax #'(old ...))]
+                             [new-id (in-syntax #'(new ...))]
+                             #:when (free-identifier=? id old-id))
+                   new-id))
+               (define rn ((attribute sig.rename) id))
+               (or (lookup rn) rn))
+             #:with sig-name #'sig.sig-name)))
+
+
+;; imports/members : identifier? -> syntax?
+;; given an identifier bound to a signature
+;; returns syntax containing the signature name and the names of each variable contained
+;; in the signature, this is needed to typecheck define-values/invoke-unit forms
+(define-for-syntax (imports/members sig-id)
+  (define-values (_1 imp-mem _2 _3) (signature-members sig-id sig-id))
+  #`(#,sig-id #,@(map (lambda (id)
+                        (local-expand
+                         id
+                         (syntax-local-context)
+                         (kernel-form-identifier-list)))
+                      imp-mem)))
+
+;; Given a list of signature specs
+;; Processes each signature spec to determine the variables exported
+;; and produces syntax containing the signature id and the exported variables
+(define-for-syntax (process-dv-exports es)
+  (for/list ([e (in-list es)])
+    (syntax-parse e
+      [s:sig-spec
+       (define sig-id #'s.sig-name)
+       (define renamer (attribute s.rename))
+       (define-values (_1 ex-mem _2 _3) (signature-members sig-id sig-id))
+       #`(#,sig-id #,@(map renamer ex-mem))])))
+
+;; Typed macro for define-values/invoke-unit
+;; This has to be handled specially because the types of
+;; the defined values must be registered in the environment
+(define-syntax (define-values/invoke-unit stx)
+  (syntax-parse stx 
+    #:literals (import export)
+    [(_ unit-expr
+        (import isig:sig-spec ...)
+        (export esig:sig-spec ...))
+     (define imports-stx (syntax->list #'(isig.sig-name ...)))
+     (define exports-stx (syntax->list #'(esig ...)))
+     (define/with-syntax temp (syntax-local-introduce (generate-temporary)))
+     #`(begin
+         #,(internal (quasisyntax/loc stx
+                       (define-values/invoke-unit-internal
+                         (#,@(map imports/members imports-stx))
+                         (#,@(process-dv-exports exports-stx)))))
+         (: temp (Unit (import isig.sig-name ...)
+                       (export esig.sig-name ...)
+                       (init-depend isig.sig-name ...)
+                       AnyValues))
+         (define temp unit-expr)
+         #,(ignore (quasisyntax/loc stx
+                     (untyped-define-values/invoke-unit unit-expr
+                                                        (import isig ...)
+                                                        (export esig ...)))))]))
+(begin-for-syntax
+  ;; flat signatures allow easy comparisons of whether one
+  ;; such flat-signature implements another
+  ;; - name is the identifier corresponding to the signatures name
+  ;; - implements is a free-id-set of this signature and all its ancestors
+  ;; flat-signatures enable a comparison of whether one signature implements
+  ;; another as a subset comparison on their contained sets of parent signatures
+  (struct flat-signature (name implements) #:transparent)
+
+  ;; implements? : flat-signature? flat-signature? -> Boolean
+  ;; true iff signature sig1 implements signature sig2
+  (define (implements? sig1 sig2)
+    (match* (sig1 sig2)
+      [((flat-signature name1 impls1) (flat-signature name2 impls2))
+       (free-id-subset? impls2 impls1)]))
+
+  ;; Given: a list of identifiers bound to static unit information
+  ;; Returns: two lists
+  ;; 1. A list of flat-signatures representing the signatures imported by
+  ;;    the given units
+  ;; 2. A list of flat-signatures representing the signatures exported by
+  ;;    the given units
+  (define (get-imports/exports unit-ids)
+    (define-values (imports exports) 
+      (for/fold ([imports null]
+                 [exports null])
+                ([unit-id (in-list unit-ids)])
+        (match-define-values ((list (cons _ new-imports) ...)
+                              (list (cons _ new-exports) ...))
+                             (unit-static-signatures unit-id unit-id))
+        (values (append imports new-imports) (append exports new-exports))))
+    (values (map make-flat-signature imports)
+            (map make-flat-signature exports)))
+
+  ;; Given the id of a signature, return a corresponding flat-signature
+  (define (make-flat-signature sig-name)
+    (flat-signature sig-name (get-signature-ancestors sig-name)))
+
+  ;; Walk the chain of parent signatures to build a list, and convert it to
+  ;; a free-id-set
+  (define (get-signature-ancestors sig)
+    (immutable-free-id-set
+     (with-handlers ([exn:fail:syntax? (λ (e) null)])
+       (let loop ([sig sig] [ancestors null])
+         (define-values (parent _1 _2 _3) (signature-members sig sig)) 
+         (if parent
+             (loop parent (cons sig ancestors))
+             (cons sig ancestors))))))
+  
+  ;; Calculate the set of inferred imports for a list of units
+  ;; The inferred imports are those which are not provided as
+  ;; exports from any of the units taking signature subtyping into account
+  (define (infer-imports unit-ids)
+    (define-values (imports exports) (get-imports/exports unit-ids))
+    (define remaining-imports (remove* exports imports implements?))
+    (map flat-signature-name remaining-imports))
+
+  ;; infer-exports returns all the exports from linked
+  ;; units rather than just those that are not also
+  ;; imported
+  (define (infer-exports unit-ids)
+    (define-values (imports exports) (get-imports/exports unit-ids))
+    (map flat-signature-name exports))
+
+  (define-splicing-syntax-class maybe-exports
+    #:literals (export)
+    (pattern (~seq)
+             #:attr exports #f)
+    (pattern (export sig:id ...)
+             #:attr exports (syntax->list #'(sig ...))))
+  
+  (define-syntax-class dviu/infer-unit-spec
+    #:literals (link)
+    (pattern unit-id:id
+             #:attr unit-ids (list #'unit-id))
+    (pattern (link uid-inits:id ...)
+             #:attr unit-ids (syntax->list #'(uid-inits ...)))))
+
+;; Note: This may not correctly handle all use cases of
+;; define-values/invoke-unit/infer
+;; inferred imports and exports are handled in the following way
+;; - the exports of ALL units being linked are added to the export list
+;;   to be registered in tc-toplevel, this appears to be how exports are treated
+;;   by the unit inference process
+;; - inferred imports are those imports which are not provided by
+;;   any of the exports
+;; This seems to correctly handle both recursive and non-recursive
+;; linking patterns
+(define-syntax (define-values/invoke-unit/infer stx)
+  (syntax-parse stx
+    [(_ exports:maybe-exports us:dviu/infer-unit-spec)
+     (define inferred-imports (infer-imports (attribute us.unit-ids)))
+     (define inferred-exports (or (attribute exports.exports)
+                                  (infer-exports (attribute us.unit-ids))))
+     #`(begin
+         #,(internal (quasisyntax/loc stx
+                       (define-values/invoke-unit-internal
+                         (#,@(map imports/members inferred-imports))
+                         (#,@(process-dv-exports inferred-exports)))))
+         #,(ignore
+            (quasisyntax/loc stx (untyped-define-values/invoke-unit/infer #,@#'exports us))))]))
+
+(define-syntax (invoke-unit/infer stx)
+  (syntax-parse stx 
+    [(_ . rest)
+     (ignore
+      (tr:unit:invoke-property
+       (quasisyntax/loc stx (untyped-invoke-unit/infer . rest)) 'infer))]))
+
+;; The typed invoke-unit macro must attach a syntax property to the expression
+;; being invoked in order to reliably find it during typechecking.
+;; Otherwise the expanded syntax may be confused for that of invoke-unit/infer
+;; and be typechecked incorrectly
+(define-syntax (invoke-unit stx)
+  (syntax-parse stx
+    [(invoke-unit expr . rest)
+     (ignore
+      (tr:unit:invoke-property
+       (quasisyntax/loc stx
+         (untyped-invoke-unit
+          #,(tr:unit:invoke:expr-property #'expr #t)
+          . rest)) #t))]))
+
+;; Trampolining macro that cooperates with the unit macro in order
+;; to add information needed for typechecking units
+;; Essentially head expands each expression in the body of a unit
+;;  - leaves define-syntaxes forms alone, to allow for macro definitions in unit bodies
+;;  - Inserts syntax into define-values forms that allow mapping the names of definitions
+;;    to their bodies during type checking
+;;  - Also specially handles type annotations in order to correctly associate variables
+;;    with their types
+;;  - All other expressions are marked as 'expr for typechecking
+(define-syntax (add-tags stx)
+  (syntax-parse stx
+    [(_ e)
+     (define exp-e (local-expand #'e (syntax-local-context) (kernel-form-identifier-list)))
+     (syntax-parse exp-e
+       #:literals (begin define-values define-syntaxes :)
+       [(begin b ...)
+        #'(add-tags b ...)]
+       [(define-syntaxes (name:id ...) rhs:expr)
+        exp-e]
+       ;; Annotations must be handled specially
+       ;; Exported variables are renamed internally in units, which leads
+       ;; to them not being correctly associated with their type annotations
+       ;; This extra bit of inserted syntax allows the typechecker to
+       ;; properly associate all annotated variables with their types.
+       ;; The inserted lambda expression will be expanded to the internal
+       ;; name of the variable being annotated, this internal name
+       ;; can then be associated with the type annotation during typechecking
+       [(define-values () (colon-helper (: name:id type) rest ...))
+        (quasisyntax/loc stx
+          (define-values ()
+            #,(tr:unit:body-exp-def-type-property
+               #`(#%expression
+                  (begin (void (lambda () name))
+                         (colon-helper (: name type) rest ...)))
+               'def/type)))]
+       [(define-values (name:id ...) rhs)
+        (quasisyntax/loc stx
+          (define-values (name ...)
+            #,(tr:unit:body-exp-def-type-property
+               #'(#%expression
+                  (begin
+                    (void (lambda () name ... (void)))
+                    rhs))
+               'def/type)))]
+       [_
+        (tr:unit:body-exp-def-type-property exp-e 'expr)])]
+    [(_ e ...)
+     #'(begin (add-tags e) ...)]))
+
+(define-syntax (unit stx)
+  (syntax-parse stx
+    #:literals (import export)
+    [(unit imports exports init-depends:init-depend-form e ...)
+     (ignore
+      (tr:unit
+       (quasisyntax/loc stx
+         (untyped-unit
+          imports
+          exports
+          #,@(attribute init-depends.form)
+          (add-tags e ...)))))]))
+
+(define-syntax (define-unit stx)
+  (syntax-parse stx
+    #:literals (import export)
+    [(define-unit uid:id
+       imports
+       exports
+       init-depends:init-depend-form
+       e ...)
+     (process-definition-form
+      (λ (stx) (tr:unit stx))
+      (quasisyntax/loc stx
+        (untyped-define-unit uid
+          imports
+          exports
+          #,@(attribute init-depends.form)
+          (add-tags e ...))))]))
+
+(begin-for-syntax
+  (define-syntax-class compound-imports
+    #:literals (import)
+    (pattern (import lb:link-binding ...)
+             #:attr import-tags (syntax->list #'(lb.link-id ...))))
+  (define-syntax-class compound-links
+    #:literals (link)
+    (pattern (link ld:linkage-decl ...)
+             #:attr all-export-links (map syntax->list (syntax->list #'(ld.exported-keys ...)))
+             #:attr all-import-links (map syntax->list (syntax->list #'(ld.imported-keys ...)))))
+  (define-syntax-class linkage-decl
+    (pattern ((lb:link-binding ...)
+              unit-expr:expr
+              link-id:id ...)
+             #:attr exported-keys #'(lb.link-id ...)
+             #:with imported-keys #'(link-id ...)))
+  (define-syntax-class link-binding
+    (pattern (link-id:id : sig-id:id)))
+
+  ;; build-compound-unit-prop : (listof id) (listof (listof id?)) (listof id?)
+  ;;                         -> (list (listof symbol?) 
+  ;;                                  (listof (listof symbol?))
+  ;;                                  (listof (listof symbol?)))
+  ;; Process the link bindings of a compound-unit form
+  ;; to return a syntax property used for typechecking compound-unit forms
+  ;; The return value is a list to be attached as a syntax property to compound-unit
+  ;; forms.
+  ;; The list contains 3 elements
+  ;; - The first element is a list of symbols corresponding to the link-ids of
+  ;;   the compound-unit's imports
+  ;; - The second element is a list of lists of symbols, corresponding to the
+  ;;   link-ids exported by units in the compound-unit's linking clause
+  ;; - The last element is also a list of lists of symbols, corresponding to the
+  ;;   link-ids being imported by units in the compound-unit's linking clause
+  (define (build-compound-unit-prop import-tags all-import-links all-export-links)
+    (define table
+      (make-immutable-free-id-table
+       (for/list ([link (in-list (append import-tags (flatten all-export-links)))])
+         (cons link (gensym (syntax-e link))))))
+    (define imports-tags
+      (map (λ (id) (free-id-table-ref table id #f)) import-tags))
+    (define units-exports
+      (map
+       (λ (lst) (map (λ (id) (free-id-table-ref table id #f)) lst))
+       all-export-links))
+    (define units-imports
+      (for/list ([unit-links (in-list all-import-links)])
+        (for/list ([unit-link (in-list unit-links)])
+          (free-id-table-ref table unit-link #f))))
+    (list imports-tags units-exports units-imports)))
+
+(define-syntax (compound-unit stx)
+  (syntax-parse stx
+    [(_ imports:compound-imports
+        exports
+        links:compound-links)
+     (define import-tags (attribute imports.import-tags))
+     (define all-import-links (attribute links.all-import-links))
+     (define all-export-links (attribute links.all-export-links))
+     (define prop (build-compound-unit-prop import-tags all-import-links all-export-links))
+     (ignore (tr:unit:compound-property
+              (quasisyntax/loc stx (untyped-compound-unit imports exports links))
+              prop))]))
+
+(define-syntax (define-compound-unit stx)
+  (syntax-parse stx
+    [(_ uid 
+        imports:compound-imports
+        exports
+        links:compound-links)
+     (define import-tags (attribute imports.import-tags))
+     (define all-import-links (attribute links.all-import-links))
+     (define all-export-links (attribute links.all-export-links))
+     (define prop (build-compound-unit-prop import-tags all-import-links all-export-links))
+     (process-definition-form
+      (λ (stx) (tr:unit:compound-property stx prop))
+      (quasisyntax/loc stx
+        (untyped-define-compound-unit uid imports exports links)))]))
+
+(define-syntax (compound-unit/infer stx)
+  (syntax-parse stx
+    #:literals (import export link)
+    [(_ . rest)
+     (ignore
+      (tr:unit:compound-property
+       (quasisyntax/loc stx
+         (untyped-compound-unit/infer . rest))
+       'infer))]))
+
+(define-syntax (define-compound-unit/infer stx)
+  (syntax-parse stx
+    [(_ . rest)
+     (process-definition-form 
+      (λ (stx) (tr:unit:compound-property stx'infer))
+      (quasisyntax/loc stx (untyped-define-compound-unit/infer . rest)))]))
+
+(define-syntax (unit-from-context stx)
+  (syntax-parse stx
+    [(_ . rest)
+     (ignore
+      (tr:unit:from-context
+       (quasisyntax/loc stx
+         (untyped-unit-from-context . rest))))]))
+
+(define-syntax (define-unit-from-context stx)
+  (syntax-parse stx
+    [(_ . rest)
+     (process-definition-form
+      (λ (stx) (tr:unit:from-context stx))
+      (quasisyntax/loc stx (untyped-define-unit-from-context . rest)))]))

typed-racket-lib/typed-racket/env/init-envs.rkt

@@ -8,11 +8,12 @@
          "type-name-env.rkt"
          "type-alias-env.rkt"
          "mvar-env.rkt"
+         "signature-env.rkt"
          (rename-in racket/private/sort [sort raw-sort])
          (rep type-rep object-rep filter-rep rep-utils free-variance)
          (for-syntax syntax/parse racket/base)
          (types abbrev union)
-         racket/dict racket/list
+         racket/dict racket/list racket/promise
          mzlib/pconvert racket/match)
 
 (provide ;; convenience form for defining an initial environment
@@ -26,7 +27,8 @@
          tvariance-env-init-code
          talias-env-init-code
          env-init-code
-         mvar-env-init-code)
+         mvar-env-init-code
+         signature-env-init-code)
 
 (define-syntax (define-initial-env stx)
   (syntax-parse stx
@@ -118,6 +120,16 @@
               (set-box! cache-box
                         (dict-set (unbox cache-box) v (list name class-type))))
             (if cache-box name class-type)])]
+    [(Signature: name extends mapping)
+     (define (serialize-mapping m)
+       (map (lambda (id/ty) 
+              (define id (car id/ty))
+              (define ty (force (cdr id/ty)))
+              `(cons (quote-syntax ,id) ,(sub ty)))
+            m))
+     `(make-Signature (quote-syntax ,name)
+                      (quote-syntax ,extends)
+                      (list ,@(serialize-mapping mapping)))]
     [(arr: dom rng rest drest kws)
      `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws))]
     [(TypeFilter: t p)
@@ -184,3 +196,8 @@
   (make-init-code
     (λ (f) (dict-map mvar-env f))
     (lambda (id v) (and v #`(register-mutated-var #'#,id)))))
+
+(define (signature-env-init-code)
+  (make-init-code
+   signature-env-map
+   (lambda (id sig) #`(register-signature! #'#,id #,(quote-type sig)))))

typed-racket-lib/typed-racket/env/signature-env.rkt

@@ -0,0 +1,69 @@
+#lang racket/base
+
+;; Environment for signature definitions
+;; to track bindings and type definitions inside of signatures
+
+(provide register-signature!
+         finalize-signatures!
+         lookup-signature
+         signature-env-map
+         with-signature-env/extend)
+
+(require syntax/id-table
+         racket/match
+         racket/promise
+         (for-syntax syntax/parse racket/base)
+         "../utils/utils.rkt"
+         (utils tc-utils)
+         (rep type-rep))
+
+;; initial signature environment
+(define signature-env (make-parameter (make-immutable-free-id-table)))
+
+;; register-signature! : identifier? Signature? -> Void
+;; adds a mapping from the given identifier to the given signature
+;; in the signature environment
+(define (register-signature! id sig)
+  (when (lookup-signature id)
+    (tc-error/fields "duplicate signature definition"
+                     "identifier" (syntax-e id)))
+  (signature-env (free-id-table-set (signature-env) id sig)))
+
+
+(define-syntax-rule (with-signature-env/extend ids sigs . b)
+  (let ([ids* ids]
+        [sigs* sigs])
+    (define new-env 
+      (for/fold ([env (signature-env)])
+                ([id (in-list ids*)]
+                 [sig (in-list sigs*)])
+        (free-id-table-set env id sig)))
+    (parameterize ([signature-env new-env]) . b)))
+
+;; Iterate over the signature environment forcing the types of bindings
+;; in each signature
+(define (finalize-signatures!)
+  (signature-env
+   (make-immutable-free-id-table
+    (signature-env-map
+     (lambda (id sig)
+       (cons
+        id
+        (match sig
+          [(Signature: name extends mapping)
+           (make-Signature
+            name
+            extends
+            (map
+             (match-lambda [(cons id ty) (cons id (force ty))])
+             mapping))]
+          [_ #f])))))))
+
+;; lookup-signature : identifier? -> (or/c #f Signature?)
+;; look up the signature corresponding to the given identifier
+;; in the signature environment
+(define (lookup-signature id)
+  (free-id-table-ref (signature-env) id #f))
+
+(define (signature-env-map f)
+  (free-id-table-map (signature-env) f))

typed-racket-lib/typed-racket/env/signature-helper.rkt

@@ -0,0 +1,157 @@
+#lang racket/base
+
+;; This module provides helper functions for typed signatures
+
+(require "../utils/utils.rkt"
+         syntax/id-set
+         (utils tc-utils)
+         (env signature-env)
+         (rep type-rep)
+         (private parse-type)
+         syntax/parse
+         racket/list
+         racket/match
+         racket/promise
+         racket/unit-exptime
+         (for-template racket/base
+                       (submod "../typecheck/internal-forms.rkt" forms)))
+
+(provide parse-and-register-signature! signature->bindings signatures->bindings)
+
+;; parse-signature : Syntax -> Signature
+;; parses the internal syntax of a signature form to build the internal representation
+;; of a typed signature and registers the internal representation with the
+;; Signature environment
+;; The parsed syntax is created by uses of `define-signature-internal` which are
+;; inserted by the typed version of the `define-signature` macro, this function
+;; uses that syntax to created a Typed Representation of the signature to
+;; place in the Signature environment
+;; The parsed syntax contains the following fields:
+;; - name is the name of the signature being defined
+;; - the parent-signature is the name of the signature being extended or #f
+;;   if the signature defintion does not extend any signature
+;; - a list of bindings, each of the form [name : Type], for each variable
+;;   in the signature
+;; - The check field indicates that this syntax came from a use of require/typed
+;;   using the #:signature clause, and listed bindings muct be checked to ensure
+;;   they are consistent with the statically known signature variables
+(define (parse-and-register-signature! form)
+  (syntax-parse form
+    #:literal-sets (kernel-literals)
+    #:literals (values define-signature-internal)
+    [(define-values ()
+       (begin
+         (quote-syntax
+          (define-signature-internal name
+            #:parent-signature super
+            (binding ...)
+            #:check? check) #:local)
+              (#%plain-app values)))
+     (define raw-map (syntax->list #'(binding ...)))
+     (define check? (syntax->datum #'check))
+     (define extends (get-extended-signature #'name #'super check? form))
+     (define super-bindings (get-signature-mapping extends))
+     (define new-bindings (map parse-signature-binding raw-map))
+     (define pre-mapping (append super-bindings new-bindings))
+
+     ;; Make sure a require/typed signature has bindings listed
+     ;; that are consistent with its statically determined bindings
+     (when check?
+       (check-signature-bindings #'name (map car pre-mapping) form))
+
+     ;; require/typed signature bindings may not be in the correct order
+     ;; this fixes the ordering based on the static order determined
+     ;; by signature-members
+     (define mapping (if check?
+                         (fix-order #'name pre-mapping)
+                         pre-mapping))
+     (define signature (make-Signature #'name extends mapping))
+     (register-signature! #'name signature)]))
+
+;; check-signature-bindings : Identifier (Listof Identifier) -> Void
+;; checks that the bindings of a signature identifier are consistent with
+;; those listed in a require/typed clause
+(define (check-signature-bindings name vars stx)
+  (match-define-values (_ inferred-vars inferred-defs _) (signature-members name name))
+  (define (make-id-set set) (immutable-free-id-set set #:phase (add1 (syntax-local-phase-level))))
+  (define inferred-vars-set (make-id-set inferred-vars))
+  (define vars-set (make-id-set vars))
+  (unless (empty? inferred-defs)
+    (tc-error/stx name "untyped signatures containing definitions are prohibited"))
+  (unless (free-id-set=? inferred-vars-set vars-set)
+    (tc-error/fields "required signature declares inconsistent members"
+                     "expected members" (map syntax-e inferred-vars)
+                     "received members" (map syntax-e vars)
+                     #:stx stx)))
+
+;; get-extended-signature : Identifier Syntax Boolean -> (Option Signature)
+;; Checks if the extended signature information must be inferred and looks
+;; up the super signature in the environment
+;; Raises an error if a super signature is inferred that is not in the
+;; signature environment indicative of a signature that should be require/typed
+;; but was not, a typed binding for the parent signature is necessary to correctly
+;; check subtyping for units
+(define (get-extended-signature name super check? stx)
+  (cond
+   [check?
+    (match-define-values (inferred-super _ _ _) (signature-members name name))
+    (and inferred-super
+         (or (and (lookup-signature inferred-super) inferred-super)
+             (tc-error/fields "required signature extends an untyped signature"
+                              "required signature" (syntax-e name)
+                              "extended signature" (syntax-e inferred-super)
+                              #:stx stx)))]
+   [(not (syntax->datum super)) #f]
+   ;; This case should probably be an error, because if the signature was not false
+   ;; the lookup may still silently fail which should not be allowed here
+   [else (or (and (lookup-signature super) super)
+             (tc-error/fields "signature definition extends untyped signature"
+                              "in the definition of signature" (syntax-e name)
+                              "which extends signature" (syntax-e super)
+                              #:stx stx))]))
+
+;; parse-signature-binding : Syntax -> (list/c identifier? syntax?)
+;; parses the binding forms inside of a define signature into the 
+;; form used by the Signature type representation
+;; The call to `parse-type` is delayed to allow signatures and type aliases
+;; to be mutually recursive, after aliases are registered in the environment
+;; the promise will be forced to perform the actual type parsing
+(define (parse-signature-binding binding-stx)
+  (syntax-parse binding-stx
+    [[name:id type]
+     (cons #'name (delay (parse-type #'type)))]))
+
+;; signature->bindings : identifier? -> (listof (cons/c identifier? type?))
+;; GIVEN: a signature name
+;; RETURNS: the list of variables bound by that signature
+;;          inherited bindings come first
+(define (signature->bindings sig-id)
+  (define sig (lookup-signature sig-id))
+  (let loop ([sig (Signature-extends sig)]
+             [mapping (Signature-mapping sig)]
+             [bindings null])
+    (if sig
+        (loop (Signature-extends (lookup-signature sig))
+              (Signature-mapping (lookup-signature sig))
+              (append mapping bindings))
+        (append mapping bindings))))
+
+;; (listof identifier?) -> (listof (cons/c identifier? type?))
+;; GIVEN: a list of signature names
+;; RETURNS: the list of all bindings from those signatures
+;; TODO: handle required renamings/prefix/only/except
+(define (signatures->bindings ids)
+  (append-map signature->bindings ids))
+
+;; get-signature-mapping : (Option Signature) -> (Listof (Cons Id Type))
+(define (get-signature-mapping sig)
+  (if sig (Signature-mapping (lookup-signature sig)) null))
+
+;; fix-order : id (listof (cons/c id type?)) -> (listof (cons/c id type?)
+;; Returns a reordered list of signature bindings to match the order given
+;; by signature-members
+(define (fix-order sig-id sig-bindings)
+  (match-define-values (_ members _ _) (signature-members sig-id sig-id))
+  (map
+   (lambda (id) (assoc id sig-bindings free-transformer-identifier=?))
+   members))

typed-racket-lib/typed-racket/private/parse-type.rkt

@@ -5,13 +5,14 @@
 (require "../utils/utils.rkt"
          (except-in (rep type-rep object-rep) make-arr)
          (rename-in (types abbrev union utils filter-ops resolve
-                           classes prefab)
+                           classes prefab signatures)
                     [make-arr* make-arr])
          (utils tc-utils stxclass-util literal-syntax-class)
          syntax/stx (prefix-in c: (contract-req))
          syntax/parse racket/sequence
          (env tvar-env type-alias-env mvar-env
-              lexical-env index-env row-constraint-env)
+              lexical-env index-env row-constraint-env
+              signature-env)
          racket/dict
          racket/list
          racket/promise
@@ -20,6 +21,7 @@
          "parse-classes.rkt"
          (for-label
            (except-in racket/base case-lambda)
+           racket/unit
            "../base-env/colon.rkt"
            "../base-env/base-types-extra.rkt"
            ;; match on the `case-lambda` binding in the TR primitives
@@ -79,6 +81,10 @@
 (define-literal-syntax-class #:for-label cons)
 (define-literal-syntax-class #:for-label Class)
 (define-literal-syntax-class #:for-label Object)
+(define-literal-syntax-class #:for-label Unit)
+(define-literal-syntax-class #:for-label import)
+(define-literal-syntax-class #:for-label export)
+(define-literal-syntax-class #:for-label init-depend)
 (define-literal-syntax-class #:for-label Refinement)
 (define-literal-syntax-class #:for-label Instance)
 (define-literal-syntax-class #:for-label List)
@@ -376,6 +382,42 @@
                                  "given" v)
                     (make-Instance (Un)))
              (make-Instance v)))]
+      [(:Unit^ (:import^ import:id ...)
+               (:export^ export:id ...)
+               (~optional (:init-depend^ init-depend:id ...) 
+                          #:defaults ([(init-depend 1) null]))
+               (~optional result
+                          #:defaults ([result #f])))
+       ;; Lookup an identifier in the signature environment
+       ;; Fail with a parse error, if the lookup returns #f
+       (define (id->sig id)
+         (or (lookup-signature id)
+             (parse-error #:stx id
+                          #:delayed? #f
+                          "Unknown signature used in Unit type"
+                          "signature" (syntax-e id))))
+       (define (import/export-error)
+         (parse-error #:stx stx
+                      #:delayed? #f
+                      "Unit types must import and export distinct signatures"))
+       (define (init-depend-error)
+         (parse-error
+            #:stx stx
+            #:delayed? #f
+            "Unit type initialization dependencies must be a subset of imports"))
+       (define imports
+         (check-imports/exports (stx-map id->sig #'(import ...)) import/export-error))
+       (define exports
+         (check-imports/exports (stx-map id->sig #'(export ...)) import/export-error))
+       (define init-depends
+         (check-init-depends/imports (stx-map id->sig #'(init-depend ...))
+                                     imports
+                                     init-depend-error))
+       (define res (attribute result))
+       (make-Unit imports
+                  exports
+                  init-depends
+                  (if res (parse-values-type res) (-values (list -Void))))]
       [(:List^ ts ...)
        (parse-list-type stx)]
       [(:List*^ ts ... t)

typed-racket-lib/typed-racket/private/syntax-properties.rkt

@@ -74,5 +74,10 @@
   (tr:class:local-table tr:class:local-table)
   (tr:class:name-table tr:class:name-table)
   (tr:class:def tr:class:def)
-  )
+  (tr:unit tr:unit #:mark)
+  (tr:unit:body-exp-def-type tr:unit:body-exp-def-type)
+  (tr:unit:invoke tr:unit:invoke)
+  (tr:unit:invoke:expr tr:unit:invoke:expr)
+  (tr:unit:compound tr:unit:compound)
+  (tr:unit:from-context tr:unit:from-context #:mark))
 

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

@@ -396,6 +396,7 @@
         [(Prompt-TagTop:) (only-untyped prompt-tag?/sc)]
         [(Continuation-Mark-KeyTop:) (only-untyped continuation-mark-key?/sc)]
         [(ClassTop:) (only-untyped class?/sc)]
+        [(UnitTop:) (only-untyped unit?/sc)]
         [(StructTypeTop:) (struct-type/sc null)]
         ;; TODO Figure out how this should work
         ;[(StructTop: s) (struct-top/sc s)]
@@ -512,6 +513,25 @@
          (if seal/sc
              (and/sc seal/sc sc-for-class)
              sc-for-class)]
+        [(Unit: imports exports init-depends results)
+         (define (traverse sigs)
+           (for/list ([sig (in-list sigs)])
+             (define mapping 
+               (map
+                (match-lambda 
+                  [(cons id type) (cons id (t->sc type))])
+                (Signature-mapping sig)))
+             (signature-spec (Signature-name sig) (map car mapping) (map cdr mapping))))
+         
+         (define imports-specs (traverse imports))
+         (define exports-specs (traverse exports))
+         (define init-depends-ids (map Signature-name init-depends))
+         (match results
+           [(? AnyValues?)
+            (fail #:reason (~a "cannot generate contract for unit type"
+                               " with unknown return values"))]
+           [(Values: (list (Result: rngs _ _) ...))
+            (unit/sc imports-specs exports-specs init-depends-ids (map t->sc rngs))])]
         [(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?)
          (cond
            [(dict-ref recursive-values nm #f)]

typed-racket-lib/typed-racket/rep/type-rep.rkt

@@ -66,7 +66,8 @@
           (not (Values? e))
           (not (ValuesDots? e))
           (not (AnyValues? e))
-          (not (Result? e)))))
+          (not (Result? e))
+          (not (Signature? e)))))
 
 ;; (or/c Type/c Values? Results?)
 ;; Anything that can be treated as a Values by sufficient expansion
@@ -77,7 +78,8 @@
           (not (arr? e))
           (not (fld? e))
           (not (ValuesDots? e))
-          (not (AnyValues? e)))))
+          (not (AnyValues? e))
+          (not (Signature? e)))))
 
 (define Type/c (flat-named-contract 'Type Type/c?))
 (define Values/c (flat-named-contract 'Values Values/c?))
@@ -555,6 +557,35 @@
 ;; cls : Class
 (def-type Instance ([cls Type/c]) [#:key 'instance])
 
+;; interp:
+;; name is the id of the signature
+;; extends is the extended signature or #f
+;; mapping maps variables in a signature to their types
+;; This is not a type because signatures are not values
+(def-type Signature ([name identifier?]
+                     [extends (or/c identifier? #f)]
+                     [mapping (listof (cons/c identifier? (or/c promise? Type/c)))])
+  [#:frees (lambda (f) null)]
+  [#:fold-rhs (*Signature name extends mapping)])
+
+;; The supertype of all units, ie values recognized by the
+;; predicate unit?
+(def-type UnitTop () [#:fold-rhs #:base] [#:key 'unit])
+
+;; interp: imports is the list of imported signatures
+;;         exports is the list of exported signatures
+;;         init-depends is the list of init-depend signatures
+;;         result is the type of the body of the unit
+(def-type Unit ([imports (listof Signature?)]
+                [exports (listof Signature?)]
+                [init-depends (listof Signature?)]
+                [result SomeValues/c])
+  [#:frees (lambda (f) (f result))]
+  [#:fold-rhs (*Unit (map type-rec-id imports)
+                     (map type-rec-id exports)
+                     (map type-rec-id init-depends)
+                     (type-rec-id result))])
+
 ;; sequences
 ;; includes lists, vectors, etc
 ;; tys : sequence produces this set of values at each step

typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt

@@ -6,7 +6,7 @@
 
 (require "simple.rkt" "structural.rkt"
          (for-template racket/base racket/list racket/set racket/promise
-                       racket/class racket/async-channel))
+                       racket/class racket/unit racket/async-channel))
 (provide (all-defined-out))
 
 (define identifier?/sc (flat/sc #'identifier?))
@@ -34,5 +34,6 @@
 (define continuation-mark-key?/sc (flat/sc #'continuation-mark-key?))
 
 (define class?/sc (flat/sc #'class?))
+(define unit?/sc (flat/sc #'unit?))
 
 (define struct-type?/sc (flat/sc #'struct-type?))

typed-racket-lib/typed-racket/static-contracts/combinators/unit.rkt

@@ -0,0 +1,109 @@
+#lang racket/base
+
+;; Static contracts for unit contracts
+
+(require "../structures.rkt" "../constraints.rkt"
+         racket/list racket/match
+         racket/dict
+         racket/contract
+         racket/syntax
+         (for-template racket/base racket/unit)
+         (for-syntax racket/base syntax/parse))
+
+
+(provide
+ (contract-out 
+  [struct signature-spec ([name identifier?]
+                          [members (listof identifier?)]
+                          [scs (listof static-contract?)])]
+  [unit/sc (-> (listof signature-spec?) 
+               (listof signature-spec?)
+               (listof identifier?)
+               (listof static-contract?) 
+               static-contract?)]))
+
+
+(struct signature-spec (name members scs) #:transparent)
+
+(struct unit-combinator combinator ()
+        #:transparent
+        #:property prop:combinator-name "unit/sc"
+        #:methods gen:sc
+        [(define (sc-map v f) 
+           (match v
+             [(unit-combinator unit-spec)
+              (unit-combinator (unit-spec-sc-map f unit-spec))]))
+         (define (sc-traverse v f)
+           (match v
+             [(unit-combinator unit-spec)
+              (unit-spec-sc-map f unit-spec)
+              (void)]))
+         (define (sc->contract v f)
+           (unit/sc->contract v f))
+         (define (sc->constraints v f)
+           (merge-restricts* 'chaperone (map f (unit-spec->list (combinator-args v)))))])
+
+(define unit-spec->list
+  (match-lambda
+   [(unit-spec imports exports init-depends invoke)
+    (flatten (append (filter-map signature-spec-scs imports)
+                     (filter-map signature-spec-scs exports)
+                     ;; init-depends do not show up because
+                     ;; there are no contracts attached
+                     (filter-map (lambda (x) x) invoke)))]))
+
+(struct unit-spec (imports exports init-depends invoke) 
+        #:transparent
+        #:property prop:sequence unit-spec->list)
+
+(define (unit-spec-sc-map f seq)
+  (match seq
+    [(unit-spec imports exports init-depends invokes)
+     (unit-spec
+      (map (signature-spec-sc-map f) imports)
+      (map (signature-spec-sc-map f) exports)
+      ;; leave init-depends alone since they don't contain contracts
+      init-depends
+      (map (lambda (invoke) (and invoke (f invoke 'covariant))) invokes))]))
+
+(define ((signature-spec-sc-map f) seq)
+  (match seq
+    [(signature-spec name (list ids ...) (list scs ...))
+     (signature-spec
+      name
+      ids
+      (map (lambda (sc) (and sc (f sc 'invariant))) scs))]))
+
+
+(define (unit/sc->contract v f)
+  (match v
+    [(unit-combinator 
+      (unit-spec (list imports ...)
+                 (list exports ...)
+                 (list deps ...)
+                 (list invoke/scs ...)))
+     
+     (define (sig-spec->syntax sig-spec)
+       (match sig-spec
+         [(signature-spec name members scs)
+          (define member-stx
+            (map (lambda (id sc) #`(#,id #,(f sc))) members scs))
+          #`(#,name #,@member-stx)]))
+     
+     (define (invokes->contract lst)
+       (cond
+        ;; just a single contract
+        [(= 1 (length lst))
+         #`#,(f (first lst))]
+        ;; values contract
+        [else 
+         #`(values #,@(map f lst))]))
+     
+     #`(unit/c
+        (import #,@(map sig-spec->syntax imports))
+        (export #,@(map sig-spec->syntax exports))
+        (init-depend #,@deps)
+        #,(invokes->contract invoke/scs))]))
+
+(define (unit/sc imports exports init-depends invoke)
+  (unit-combinator (unit-spec imports exports init-depends invoke)))

typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt

@@ -0,0 +1,753 @@
+#lang racket/unit
+
+;; This module provides a unit for type-checking units
+;; The general strategy for typechecking all of the racket/unit forms
+;; is to match the entire expanded syntax and parse out the relevant
+;; pieces of information.
+;;
+;; Each typing rule knows the expected expansion of the form being checked
+;; and specifically parses that syntax. This implementation is extremely
+;; brittle and will require changes should the expansion of any of the unit
+;; forms change.
+;;
+;; For unit forms the general idea is to parse expanded syntax to find information
+;; related to:
+;; - imports
+;; - exports
+;; - init-depend
+;; - subexpressions that require typechecking
+;; And use these pieces to typecheck the entire form
+;;
+;; For the `unit` form imports, exports, and init-depends are parsed to generate
+;; the type of the expression and to typecheck the body of the unit since imported signatures
+;; introduce bindings of variables to types, and exported variables must be defined
+;; with subtypes of their expected types.
+;;
+;; The `invoke-unit` expansion is more complex and depends on whether or not
+;; imports were specified. In the case of no imports, the strategy is simply to
+;; find the expression being invoked and ensure it has the type of a unit with
+;; no imports. When there are imports to an `invoke-unit` form, the syntax contains
+;; local definitions of units defined using `unit-from-context`. These forms
+;; are parsed to determine which imports were declared to check subtyping on the
+;; invoked expression and to ensure that imports pulled from the current context
+;; have the correct types.
+;;
+;; The `compound-unit` expansion contains information about the imports and exports
+;; of each unit expression being linked. Additionally the typed `compound-unit` macro
+;; attaches a syntax property that specifies the exact linking structure of the compound
+;; unit. These pieces of information enable the calculation of init-depends for the entire
+;; compound unit and to properly check subtyping on each linked expression.
+;;
+;; `unit-from-context` is handled similarly to `invoke-unit`, the expansion is exactly
+;; that of a unit created using the `unit` form, but lacks the annotations that are placed
+;; there by the typed `unit` macro. In this case the body of the unit is searched for
+;; syntax corresponding to definitions which are checked against the declared exports
+;; to ensure the form is well typed.
+;;
+;; The handling of the various `infer` forms (invoke-unit/infer compound-unit/infer)
+;; is generally identical to the corresponding form lacking inference, however, in these
+;; cases typechecking can be more lax. In particular, the unit implementation knows that
+;; only valid unit expressions are used in these forms and so there is no need to typecheck
+;; each unit subexpression unless it is needed to determine the result type. The
+;; `compund-unit/infer` form, however, requires the cooperation of the unit implementation
+;; to attach a syntax property that specified the init-depends of the compound unit, otherwise
+;; this information is extremely difficult to obtain from the syntax alone.
+
+(require "../utils/utils.rkt"
+         syntax/id-set
+         racket/set
+         racket/dict
+         racket/format
+         racket/list
+         racket/match
+         racket/syntax
+         syntax/id-table
+         syntax/parse
+         syntax/stx
+         syntax/strip-context
+         racket/unit-exptime
+         "signatures.rkt"
+         (private parse-type syntax-properties type-annotation)
+         (only-in (base-env base-special-env) make-template-identifier)
+         (env lexical-env tvar-env global-env 
+              signature-env signature-helper)
+         (types utils abbrev union subtype resolve generalize signatures)
+         (typecheck check-below internal-forms)
+         (utils tc-utils)
+         (rep type-rep)
+         (for-syntax racket/base racket/unit-exptime syntax/parse)
+         (for-template racket/base
+                       racket/unsafe/undefined
+                       (submod "internal-forms.rkt" forms)))
+
+(import tc-let^ tc-expr^)
+(export check-unit^)
+
+;; Syntax class definitions
+;; variable annotations are modified by the expansion of the typed unit
+;; macro in order to allow annotations on exported variables, this
+;; syntax class allows conversion back to the usual internal syntax
+;; for type annotations which may be used by tc-letrec/values
+(define-syntax-class unit-body-annotation
+  #:literal-sets (kernel-literals)
+  #:literals (void values :-internal cons)
+  (pattern
+   (#%expression
+    (begin
+      (#%plain-app void (#%plain-lambda () var-int))
+      (begin
+        (quote-syntax
+         (:-internal var:id t) #:local)
+        (#%plain-app values))))
+   #:attr name #'var
+   #:attr fixed-form (quasisyntax/loc this-syntax
+                       (begin
+                           (quote-syntax (:-internal var-int t) #:local)
+                           (#%plain-app values)))))
+
+;; Syntax class matching the syntax of the rhs of definitions within unit bodies
+;; The typed unit macro attaches the lambda to allow unit typechecking to associate
+;; variable names with their definitions which are otherwise challenging to recover
+(define-syntax-class unit-body-definition
+  #:literal-sets (kernel-literals)
+  #:literals (void)
+  (pattern
+   (#%expression
+    (begin
+      (#%plain-app void (#%plain-lambda () var:id ... (#%plain-app void)))
+      e))
+   #:with vars #'(var ...)
+   #:with body #'e))
+
+;; Process the syntax of annotations and definitions from a unit
+;; produces two values representing the names and the exprs corresponding
+;; to each definition or annotation
+;; Note:
+;; - definitions may produce multiple names via define-values
+;; - annotations produce no names
+(define (process-ann/def-for-letrec ann/defs)
+  (for/fold ([names #`()]
+             [exprs #`()])
+            ([a/d (in-list ann/defs)])
+    (syntax-parse a/d
+      [a:unit-body-annotation
+       (define name (attribute a.name))
+       ;; TODO:
+       ;; Duplicate annotations from imports
+       ;; are not currently detected due to a bug
+       ;; in tc/letrec-values
+       ;; See Problem Report: 15145
+       (define fixed (attribute a.fixed-form))
+       (values #`(#,@names ()) #`(#,@exprs #,fixed))]
+      [d:unit-body-definition
+       (values #`(#,@names d.vars) #`(#,@exprs d.body))])))
+
+;; A Sig-Info is a (sig-info identifier? (listof identifier?) (listof identifier?))
+;; name is the identifier corresponding to the signature this sig-info represents
+;; externals is the list of external names for variables in the signature
+;; internals is the list of internal names for variables in the signature
+;; Note:
+;; - external names are those attached to signatures stored in static information
+;;   and in the Siganture representation
+;; - internal names are the internal renamings of those variables in fully expanded
+;;   unit syntax, this renaming is performed by the untyped unit macro
+;; - All references within a unit body use the internal names
+(struct sig-info (name externals internals) #:transparent)
+
+;; Process the various pieces of the fully expanded unit syntax to produce
+;; sig-info structures for the unit's imports and exports, and a list of the
+;; identifiers corresponding to init-depends of the unit
+(define (process-unit-syntax import-sigs import-internal-ids import-tags
+                             export-sigs export-temp-ids export-temp-internal-map
+                             init-depend-tags)
+  ;; build a mapping of import-tags to import signatures
+  ;; since init-depends are referenced by the tags only in the expanded syntax
+  ;; this map is used to determine the actual signatures corresponding to the
+  ;; given signature tags of the init-depends
+  (define tag-map (make-immutable-free-id-table (map cons import-tags import-sigs)))
+  (define lookup-temp (λ (temp) (free-id-table-ref export-temp-internal-map temp #f)))
+  
+  (values (for/list ([sig-id  (in-list import-sigs)]
+                     [sig-internal-ids (in-list import-internal-ids)])
+            (sig-info sig-id
+                      (map car (Signature-mapping (lookup-signature sig-id)))
+                      sig-internal-ids))
+          ;; export-temp-ids is a flat list which must be processed
+          ;; sequentially to map them to the correct internal/external identifiers
+          (let-values ([(_ si)
+                        (for/fold ([temp-ids export-temp-ids]
+                                   [sig-infos '()])
+                                  ([sig (in-list export-sigs)])
+                          (define external-ids
+                            (map car (Signature-mapping (lookup-signature sig))))
+                          (define len (length external-ids))
+                          (values (drop temp-ids len)
+                                  (cons (sig-info sig
+                                                  external-ids
+                                                  (map lookup-temp (take temp-ids len)))
+                                        sig-infos)))])
+            (reverse si))
+          (map (λ (x) (free-id-table-ref tag-map x #f)) init-depend-tags)))
+
+;; The following three syntax classes are used to parse specific pieces of
+;; information from parts of the expansion of units
+
+;; Needed to parse out signature names, and signature-tags from the unit syntax
+;; the tags are used to lookup init-depend signatures
+(define-syntax-class sig-vector
+  #:literal-sets (kernel-literals)
+  #:literals (vector-immutable cons)
+  (pattern (#%plain-app 
+            vector-immutable
+            (#%plain-app cons 
+                         (quote sig:id)
+                         (#%plain-app vector-immutable sig-tag tag-rest ...))
+            ...)
+           #:with sigs #'(sig ...)
+           #:with sig-tags #'(sig-tag ...)))
+
+(define-syntax-class init-depend-list
+  #:literal-sets (kernel-literals)
+  #:literals (list cons)
+  (pattern (#%plain-app list (#%plain-app cons _ sig-tag) ...)
+           #:with init-depend-tags #'(sig-tag ...)))
+
+(define-syntax-class export-table
+  #:literal-sets (kernel-literals)
+  #:literals (make-immutable-hash list cons vector-immutable check-not-unsafe-undefined unbox)
+  (pattern (#%plain-app
+            make-immutable-hash
+            (#%plain-app
+             list
+             (#%plain-app
+              cons
+              signature-tag:id
+              (#%plain-app
+               vector-immutable
+               (#%plain-lambda () 
+                 (#%plain-app check-not-unsafe-undefined (#%plain-app unbox export-temp-id) external-id))
+               ...))
+             ...))
+           #:attr export-temp-ids (map syntax->list (syntax->list #'((export-temp-id ...) ...)))))
+
+;; This syntax class matches the whole expansion of unit forms
+(define-syntax-class unit-expansion
+  #:literal-sets (kernel-literals)
+  #:attributes (body-stx 
+                import-internal-ids 
+                import-sigs 
+                import-sig-tags 
+                export-sigs 
+                export-temp-ids
+                init-depend-tags)
+  (pattern (#%plain-app
+            make-unit:id
+            name:expr 
+            import-vector:sig-vector
+            export-vector:sig-vector
+            list-dep:init-depend-list
+            (let-values (_ ...)
+              (let-values (_ ...)
+                (#%expression
+                 (#%plain-lambda ()
+                   (let-values (((export-temp-id:id) _) ...)
+                     (#%plain-app
+                      values
+                      (#%plain-lambda (import-table:id)
+                                      (let-values (((import:id ...) _) ...)
+                                        unit-body:expr))
+                      et:export-table
+                      _ ...)))))))
+           #:attr import-sigs (syntax->list #'import-vector.sigs)
+           #:attr import-sig-tags (syntax->list #'import-vector.sig-tags)
+           #:attr export-sigs (syntax->list #'export-vector.sigs)
+           #:attr export-temp-ids (syntax->list #'(export-temp-id ...))
+           #:attr init-depend-tags (syntax->list #'list-dep.init-depend-tags)
+           #:attr import-internal-ids (map syntax->list (syntax->list #'((import ...) ...)))
+           #:with body-stx #'unit-body))
+
+;; Extract the identifiers referenced in unit-from-context and invoke-unit forms
+;; in order to typecheck them in the current environment
+ (define (extract-definitions stx)
+   (trawl-for-property
+    stx
+    (lambda (stx) (syntax-parse stx [((int:id) ref:id) #t] [_ #f]))
+    (lambda (stx) (syntax-parse stx [((int:id) ref:id) #'ref]))))
+
+;; Syntax inside the expansion of units that allows recovering a mapping
+;; from temp-ids of exports to their internal identifiers
+(define-syntax-class export-temp-internal-map-elem
+  #:literal-sets (kernel-literals)
+  #:literals (set-box!)
+  (pattern (#%plain-app set-box! temp-id:id internal-id:id)))
+
+(define export-map-elem?
+  (syntax-parser [e:export-temp-internal-map-elem #t]
+                 [_ #f]))
+(define extract-export-map-elem
+  (syntax-parser [e:export-temp-internal-map-elem (cons #'e.temp-id #'e.internal-id)]))
+
+;; get a reference to the actual `invoke-unit/core` function to properly parse
+;; the fully expanded syntax of `invoke-unit` forms
+(define invoke-unit/core (make-template-identifier 'invoke-unit/core 'racket/unit))
+
+;; Syntax class for all the various expansions of invoke-unit forms
+;; This also includes the syntax for the invoke-unit/infer forms
+(define-syntax-class invoke-unit-expansion
+  #:literal-sets (kernel-literals)
+  (pattern (#%plain-app iu/c unit-expr)
+           #:when (free-identifier=? #'iu/c invoke-unit/core)
+           #:attr units '()
+           #:attr expr #'unit-expr
+           #:attr imports '())
+  (pattern
+   (let-values ()
+     body:invoke-unit-linkings)
+   #:attr units (attribute body.units)
+   #:attr expr (attribute body.expr)
+   #:attr imports (attribute body.imports)))
+
+(define-syntax-class invoke-unit-linkings
+  #:literal-sets (kernel-literals)
+  (pattern
+   (let-values ([(u-temp:id)
+                 (let-values ([(deps) _]
+                              [(sig-provider) _] ...
+                              [(temp) ie:invoked-expr])
+                   _ ...)])
+     (#%plain-app iu/c (#%plain-app values _)))
+   #:when (free-identifier=? #'iu/c invoke-unit/core)
+   #:attr units '()
+   #:attr expr (if (tr:unit:invoke:expr-property #'ie) #'ie #'ie.invoke-expr)
+   #:attr imports '())
+  (pattern
+   (let-values ([(temp-id) u:unit-expansion])
+     rest:invoke-unit-linkings)
+   #:attr units (cons #'u (attribute rest.units))
+   #:attr expr (attribute rest.expr)
+   #:attr imports (append (attribute u.export-sigs) (attribute rest.imports))))
+
+;; This should be used ONLY when an invoke/infer is used with the link clause ...
+(define-syntax-class invoked-expr
+  #:literal-sets (kernel-literals)
+  #:literals (values)
+  (pattern
+   (let-values ([(deps2:id) _]
+                [(local-unit-id:id) unit:id] ...
+                [(invoke-temp) invoke-unit])
+     _ ...)
+   #:attr invoke-expr #'invoke-unit)
+  (pattern invoke-expr:expr))
+
+;; Compound Unit syntax classes
+(define-syntax-class compound-unit-expansion
+  #:literal-sets (kernel-literals)
+  #:literals (vector-immutable cons)
+  (pattern 
+   (let-values ([(deps:id) _]
+                [(local-unit-name) unit-expr] ...)
+     (~seq (#%plain-app check-unit _ ...)
+           (#%plain-app check-sigs _
+                        (#%plain-app 
+                         vector-immutable
+                         (#%plain-app cons (quote import-sig:id) _) ...)
+                        (#%plain-app
+                         vector-immutable
+                         (#%plain-app cons (quote export-sig:id) _) ...)
+                        _)
+           (let-values ([(fht) _]
+                        [(rht) _])
+             _ ...)) ...
+     (#%plain-app
+            make-unit:id
+            name:expr 
+            import-vector:sig-vector
+            export-vector:sig-vector
+            deps-ref
+            internals))
+   #:attr unit-exprs (syntax->list #'(unit-expr ...))
+   #:attr unit-imports (map syntax->list (syntax->list #'((import-sig ...) ...)))
+   #:attr unit-exports (map syntax->list (syntax->list #'((export-sig ...) ...)))
+   #:attr compound-imports (syntax->list #'import-vector.sigs)
+   #:attr compound-exports (syntax->list #'export-vector.sigs)))
+
+;; A cu-expr-info represents an element of the link clause in
+;; a compound-unit form
+;; - expr : the unit expression being linked
+;; - import-sigs : the Signatures specified as imports for this link-element
+;; - import-links : the symbols that correspond to the link-bindings
+;;                  imported by this unit
+;; - export-sigs : the Signatures specified as exports for this link-element
+;; - export-links : the symbols corresponding to the link-bindings exported
+;;                  by this unit
+(struct cu-expr-info (expr import-sigs import-links export-sigs export-links)
+  #:transparent)
+
+;; parse-compound-unit : Syntax -> (Values (Listof (Cons Symbol Id))
+;;                                         (Listof Symbol)
+;;                                         (Listof Signature)
+;;                                         (Listof Signature)
+;;                                         (Listof cu-expr-info))
+;; Returns a mapping of link-ids to sig-ids, a list of imported sig ids
+;; a list of exported link-ids
+(define (parse-compound-unit stx)
+  (define (list->sigs l) (map lookup-signature l))
+  (syntax-parse stx
+    [cu:compound-unit-expansion
+     (define link-binding-info (tr:unit:compound-property stx))
+     (match-define (list cu-import-syms unit-export-syms unit-import-syms)
+       link-binding-info)
+     (define compound-imports (attribute cu.compound-imports))
+     (define compound-exports (attribute cu.compound-exports))
+     (define unit-exprs (attribute cu.unit-exprs))
+     (define unit-imports (attribute cu.unit-imports))
+     (define unit-exports (attribute cu.unit-exports))
+     ;; Map signature ids to link binding symbols
+     (define mapping
+       (let ()
+         (define link-syms (append cu-import-syms (flatten unit-export-syms)))
+         (define sig-ids (append compound-imports (flatten unit-exports)))
+         (map cons link-syms (map lookup-signature sig-ids))))
+     (define cu-exprs
+       (for/list ([unit-expr (in-list unit-exprs)]
+                  [import-sigs (in-list unit-imports)]
+                  [import-links (in-list unit-import-syms)]
+                  [export-sigs (in-list unit-exports)]
+                  [export-links (in-list unit-export-syms)])
+         (cu-expr-info unit-expr
+                       (list->sigs import-sigs) import-links
+                       (list->sigs export-sigs) export-links)))
+     (values 
+      mapping
+      cu-import-syms
+      (list->sigs compound-imports)
+      (list->sigs compound-exports)
+      cu-exprs)]))
+
+;; Sig-Info -> (listof (pairof identifier? Type))
+;; GIVEN: signature information
+;; RETURNS: a mapping from internal names to types
+(define (make-local-type-mapping si)
+  (define sig (lookup-signature (sig-info-name si)))
+  (define internal-names (sig-info-internals si))
+  (define sig-types 
+    (map cdr (Signature-mapping sig)))
+  (map cons internal-names sig-types))
+
+;; Syntax Option<TCResults> -> TCResults
+;; Type-check a unit form
+(define (check-unit form [expected #f])
+  (define expected-type
+    (match expected
+      [(tc-result1: type) (resolve type)]
+      [_ #f]))
+  (match expected-type
+    [(? Unit? unit-type)
+     (ret (parse-and-check-unit form unit-type))]
+    [_ (ret (parse-and-check-unit form #f))]))
+
+;; Syntax Option<TCResultss> -> TCResults
+
+(define (check-invoke-unit form [expected #f])
+  (define expected-type 
+    (match expected
+      [(tc-result1: type) (resolve type)]
+      [_ #f]))
+  (ret (parse-and-check-invoke form expected-type)))
+
+(define (check-compound-unit form [expected #f])
+  (define infer? (eq? (tr:unit:compound-property form) 'infer))
+  (define expected-type
+    (match expected
+      [(tc-result1: type) (resolve type)]
+      [_ #f]))
+  (if infer?
+      (ret (parse-and-check-compound/infer form expected-type))
+      (ret (parse-and-check-compound form expected-type))))
+
+(define (check-unit-from-context form [expected #f])
+  (define expected-type
+    (match expected
+      [(tc-result1: type) (resolve type)]
+      [_ #f]))
+  (ret (parse-and-check-unit-from-context form expected-type)))
+
+(define (parse-and-check-unit-from-context form expected-type)
+  (syntax-parse form
+    [u:unit-expansion
+     (define export-sigs (map lookup-signature (attribute u.export-sigs)))
+     (define body-stx (attribute u.body-stx))
+     (for ([sig (in-list export-sigs)])
+       (define ids (extract-definitions body-stx))
+       (define types (map cdr (Signature-mapping sig)))
+       (for ([type (in-list types)]
+             [id (in-list ids)])
+         (define lexical-type (lookup-type/lexical id))
+         (unless (subtype lexical-type type)
+           (tc-error/fields "type mismatch in unit-from-context export"
+                            "expected" type
+                            "given" lexical-type
+                            "exported variable" (syntax-e id)
+                            "exported-signature" (syntax-e (Signature-name sig))
+                            #:stx form
+                            #:delayed #t))))
+     (-unit null export-sigs null (-values (list -Void)))]))
+
+(define (parse-and-check-compound form expected-type)
+  (define-values (link-mapping
+                  import-syms
+                  import-sigs
+                  export-sigs
+                  cu-exprs)
+    (parse-compound-unit form))
+  
+  (define (lookup-link-id id) (dict-ref link-mapping id #f))
+  (define-values (check _ init-depends)
+    (for/fold ([check -Void]
+               [seen-init-depends import-syms]
+               [calculated-init-depends '()])
+              ([form (in-list cu-exprs)])
+      (match-define (cu-expr-info unit-expr-stx
+                                  import-sigs
+                                  import-links
+                                  export-sigs
+                                  export-links)
+        form)
+      (define unit-expected-type 
+        (-unit import-sigs 
+               export-sigs 
+               (map lookup-link-id (set-intersect seen-init-depends import-links))
+               ManyUniv))
+      (define unit-expr-type (tc-expr/t unit-expr-stx))
+      (check-below unit-expr-type unit-expected-type)
+      (define-values (body-type new-init-depends)
+        (match unit-expr-type
+          [(Unit: _ _ ini-deps ty)
+           ;; init-depends here are strictly subsets of the units imports
+           ;; but these may not exactly match with the provided links
+           ;; so all of the extended signatures must be traversed to find the right
+           ;; signatures for init-depends
+           (define extended-imports
+             (map cons import-links
+                  (map (λ (l) (map Signature-name (flatten-sigs l))) import-sigs)))
+           (define init-depend-links
+             (for*/list ([sig-name (in-list (map Signature-name ini-deps))]
+                         [(import-link import-family) (in-dict extended-imports)]
+                         #:when (member sig-name import-family free-identifier=?))
+               import-link))
+           ;; new init-depends are the init-depends of this unit that
+           ;; overlap with the imports to the compound-unit
+           (values ty (set-intersect import-syms init-depend-links))]
+          ;; unit-expr was not actually a unit, but we want to delay the errors
+          [_ (values #f '())]))
+      (values body-type
+              ;; Add the exports to the list of seen-init-depends
+              (set-union seen-init-depends export-links)
+              ;; Add the new-init-depends to those already calculated
+              (set-union calculated-init-depends new-init-depends))))
+  (if check
+      (-unit import-sigs
+             export-sigs
+             (map lookup-link-id init-depends)
+             check)
+      ;; Error case when one of the links was not a unit
+      -Bottom))
+
+(define (parse-and-check-compound/infer form expected-type)
+  (define init-depend-refs (syntax-property form 'unit:inferred-init-depends))
+  (syntax-parse form
+    [cu:compound-unit-expansion
+     (define unit-exprs (attribute cu.unit-exprs))
+     (define compound-imports (map lookup-signature (attribute cu.compound-imports)))
+     (define compound-exports (map lookup-signature (attribute cu.compound-exports)))
+     (define import-vector (apply vector compound-imports))
+     (define import-length (vector-length import-vector))
+     (unless (and (list? init-depend-refs)
+                  (andmap (λ (i) (and (exact-nonnegative-integer? i) (< i import-length)))
+                          init-depend-refs))
+       (int-err "malformed syntax property attached to compound-unit/infer form"))
+     (define compound-init-depends
+       (map (lambda (i) (vector-ref import-vector i)) init-depend-refs))
+     (define resulting-unit-expr (last unit-exprs))
+     (define final-unit-invoke-type (tc-expr/t resulting-unit-expr))
+     ;; This type should always be a unit
+     (match-define (Unit: _ _ _ compound-invoke-type) final-unit-invoke-type)
+     (-unit compound-imports compound-exports compound-init-depends compound-invoke-type)]))
+
+(define (parse-and-check-invoke form expected-type)
+  (syntax-parse form 
+    [iu:invoke-unit-expansion
+     (define infer? (eq? 'infer (tr:unit:invoke-property form)))
+     (define invoked-unit (attribute iu.expr))
+     (define import-sigs (map lookup-signature (attribute iu.imports)))
+     (define linking-units (attribute iu.units))
+     (define unit-expr-type (tc-expr/t invoked-unit))
+     ;; TODO: Better error message/handling when the folling check-below "fails"
+     (unless infer?
+       (check-below unit-expr-type (-unit import-sigs null import-sigs ManyUniv)))
+     (for ([unit (in-list linking-units)]
+           [sig (in-list import-sigs)])
+       (define ids (extract-definitions unit))
+       (define types (map cdr (Signature-mapping sig)))
+       (for ([type (in-list types)]
+             [id (in-list ids)])
+         (define lexical-type (lookup-type/lexical id))
+         (unless (subtype lexical-type type)
+           (tc-error/fields "type mismatch in invoke-unit import"
+                            "expected" type
+                            "given" lexical-type
+                            "imported variable" (syntax-e id)
+                            "imported signature" (syntax-e (Signature-name sig))
+                            #:stx form
+                            #:delayed? #t))))
+     (cond
+       [(Unit? unit-expr-type)
+        (define result-type (Unit-result unit-expr-type))
+        (match result-type
+          [(Values: (list (Result: t _ _) ...)) t]
+          [(AnyValues: f) ManyUniv]
+          [(ValuesDots: (list (Result: t _ _) ...) _ _) t])]
+       [else -Bottom])]))
+
+;; Parse and check unit syntax
+(define (parse-and-check-unit form expected)
+  (syntax-parse form
+    [u:unit-expansion
+     ;; extract the unit body syntax
+     (define body-stx #'u.body-stx)
+     (define import-sigs (attribute u.import-sigs))
+     (define import-internal-ids (attribute u.import-internal-ids))
+     (define import-tags (attribute u.import-sig-tags))
+     (define export-sigs (attribute u.export-sigs))
+     (define export-temp-ids (attribute u.export-temp-ids))
+     (define init-depend-tags (attribute u.init-depend-tags))
+     (define export-temp-internal-map
+       (make-immutable-free-id-table
+        (trawl-for-property body-stx export-map-elem? extract-export-map-elem)))
+     (define-values (imports-info exports-info init-depends)
+       (process-unit-syntax import-sigs import-internal-ids import-tags
+                            export-sigs export-temp-ids export-temp-internal-map
+                            init-depend-tags))
+
+     ;; Get Signatures to build Unit type
+     (define import-signatures (map lookup-signature (map sig-info-name imports-info)))
+     (define export-signatures (map lookup-signature (map sig-info-name exports-info)))
+     (define init-depend-signatures (map lookup-signature init-depends))
+
+     (unless (distinct-signatures? import-signatures)
+       (tc-error/expr "unit expressions must import distinct signatures"))
+     ;; this check for exports may be unnecessary
+     ;; the unit macro seems to check it as well
+     (unless (distinct-signatures? export-signatures)
+       (tc-error/expr "unit expresssions must export distinct signatures"))
+     
+     (define local-sig-type-map
+       (apply append (map make-local-type-mapping imports-info)))
+     (define export-signature-type-map
+       (map (lambda (si)
+              (cons (sig-info-name si) (make-local-type-mapping si)))
+            exports-info))
+
+     ;; Thunk to pass to tc/letrec-values to check export subtyping
+     ;; These subtype checks can only be checked within the dynamic extent
+     ;; of the call to tc/letrec-values because they need to lookup
+     ;; variables in the type environment as modified by typechecking
+     (define (check-exports-thunk)
+       (for* ([sig-mapping (in-list export-signature-type-map)]
+              [sig (in-value (car sig-mapping))]
+              [mapping (in-value (cdr sig-mapping))]
+              [(id expected-type) (in-dict mapping)])
+         (define id-lexical-type (lookup-type/lexical id))
+         (unless (subtype id-lexical-type expected-type)
+           (tc-error/fields "type mismatch in unit export"
+                            "expected" expected-type
+                            "given" id-lexical-type
+                            "exported variable" (syntax-e id)
+                            "exported signature" (syntax-e sig)
+                            #:delayed? #t))))
+     
+     (define import-name-map
+       (append-map (lambda (si) (map cons (sig-info-externals si) (sig-info-internals si)))
+                   imports-info))
+     (define export-name-map
+       (append-map (lambda (si) (map cons (sig-info-externals si) (sig-info-internals si))) 
+                   exports-info))
+     
+     (define body-forms 
+       (trawl-for-property body-stx tr:unit:body-exp-def-type-property))
+     
+     (define last-form 
+       (or (and (not (empty? body-forms)) (last body-forms))))
+     
+     ;; get expression forms, if the body was empty or ended with
+     ;; a definition insert a `(void)` expression to be typechecked
+     ;; This is necessary because we defer to tc/letrec-values for typechecking
+     ;; unit bodies, but a unit body may contain only definitions whereas letrec bodies
+     ;; cannot, in this case we insert dummy syntax representing a call to the void 
+     ;; function in order to correctly type the body of the unit.
+     (define expression-forms
+       (let ([exprs 
+              (filter
+               (lambda (stx) (eq? (tr:unit:body-exp-def-type-property stx) 'expr))
+               body-forms)])
+         (cond
+           [(or (not last-form) (eq? (tr:unit:body-exp-def-type-property last-form) 'def/type))
+            (append exprs (list #'(#%plain-app void)))]
+           [else exprs])))
+
+     
+     
+     ;; Filter out the annotation and definition syntax from the unit body
+     ;; For the purposes of typechecking, annotations and definitions
+     ;; are essentially lifted to the top of the body and all expressions
+     ;; are placed at the end (possibly with the addition of a (void) expression
+     ;; as described above), since the types of definitions and annotations
+     ;; must scope over the entire body of the unit, this is valid for purposes
+     ;; of typechecking
+     (define annotation/definition-forms
+       (filter
+        (lambda (stx) (eq? (tr:unit:body-exp-def-type-property stx) 'def/type))
+        body-forms))
+     
+     (define-values (ann/def-names ann/def-exprs)
+       (process-ann/def-for-letrec annotation/definition-forms))
+
+     (define signature-annotations
+       (for/list ([(k v) (in-dict local-sig-type-map)])
+         (cons k (-> v))))
+     (define unit-type
+       (with-lexical-env/extend-types
+         (map car signature-annotations)
+         (map cdr signature-annotations)
+         ;; Typechecking a unit body is structurally similar to that of
+         ;; checking a let-body, so we resuse the machinary for checking
+         ;; let expressions
+         (define res (tc/letrec-values ann/def-names
+                                       ann/def-exprs
+                                       (quasisyntax/loc form (#,@expression-forms))
+                                       #f
+                                       check-exports-thunk))
+         (define invoke-type
+           (match res
+             [(tc-results: tps) (-values tps)]))
+         (-unit import-signatures
+                export-signatures
+                init-depend-signatures
+                invoke-type)))
+     unit-type]))
+
+;; Based on the function of the same name in check-class-unit.rkt
+;; trawl-for-property : Syntax (Syntax -> Any) [(Syntax -> A)] -> (Listof A)
+;; Search through the given syntax for pieces of syntax that satisfy
+;; the accessor predicate, then apply the extractor function to  all such syntaxes 
+(define (trawl-for-property form accessor [extractor values])
+  (define (recur-on-all stx-list)
+    (apply append (map (λ (stx) (trawl-for-property stx accessor extractor)) stx-list)))
+  (syntax-parse form
+    #:literal-sets (kernel-literals)
+    [stx
+     #:when (accessor #'stx)
+     (list (extractor form))]
+    [_
+     (define list? (syntax->list form))
+     (if list? (recur-on-all list?) '())]))

typed-racket-lib/typed-racket/typecheck/internal-forms.rkt

@@ -29,12 +29,16 @@
   typed-require/struct
   predicate-assertion
   type-declaration
+  typed-define-signature
+  typed-define-values/invoke-unit
   typecheck-failure
 
   type-alias?
   new-subtype-def?
   typed-struct?
-  typed-struct/exec?)
+  typed-struct/exec?
+  typed-define-signature?
+  typed-define-values/invoke-unit?)
 
 (module forms racket/base
   (require (for-syntax racket/base))
@@ -59,7 +63,9 @@
                   assert-predicate-internal
                   declare-refinement-internal
                   :-internal
-                  typecheck-fail-internal))
+                  typecheck-fail-internal
+                  define-signature-internal
+                  define-values/invoke-unit-internal))
 
 (require (submod "." forms) (submod "." forms literal-set))
 
@@ -91,6 +97,11 @@
            #:attr type-only (attribute options.type-only)
            #:attr maker (or (attribute options.maker) #'nm.nm)))
 
+(define-syntax-class dviu-import/export
+  (pattern (sig-id:id member-id:id ...)
+           #:with sig #'sig-id
+           #:with members #'(member-id ...)))
+
 ;;; Internal form syntax matching
 
 (define-literal-set internal-form-literals #:for-label
@@ -145,7 +156,21 @@
   [predicate-assertion
     (assert-predicate-internal type predicate)]
   [type-declaration
-    (:-internal id:identifier type)])
+    (:-internal id:identifier type)]
+  ;; the check field indicates whether this signature is being 
+  ;; required from an untyped context in which case the super
+  ;; value is ignored and information about parent signatures
+  ;; is inferred from static information bound to the signature
+  ;; identifier
+  [typed-define-signature
+   (define-signature-internal name #:parent-signature super (binding ...) #:check? check)]
+  ;; This should be a decent initial attempt at making
+  ;; define-values/invoke-unit work, the unit-expr is
+  ;; unnecessary at this point since it will be handled
+  ;; when expressions are typechecked
+  [typed-define-values/invoke-unit
+   (define-values/invoke-unit-internal (import:dviu-import/export ...)
+                                       (export:dviu-import/export ...))])
 
 ;; Define separately outside of `define-internal-classes` since this form
 ;; is meant to appear in expression positions, so it doesn't make sense to use

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

@@ -22,6 +22,12 @@
 (define-signature check-class^
   ([cond-contracted check-class (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]))
 
+(define-signature check-unit^
+  ([cond-contracted check-unit (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]
+   [cond-contracted check-invoke-unit (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]
+   [cond-contracted check-compound-unit (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]
+   [cond-contracted check-unit-from-context (syntax? (or/c tc-results/c #f) . -> . full-tc-results/c)]))
+
 (define-signature tc-if^
   ([cond-contracted tc/if-twoarm ((syntax? syntax? syntax?) ((or/c tc-results/c #f)) . ->* . full-tc-results/c)]))
 

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

@@ -28,7 +28,7 @@
                     (only-in racket/private/class-internal find-method/who)))
 
 (import tc-if^ tc-lambda^ tc-app^ tc-let^ tc-send^ check-subforms^ tc-literal^
-        check-class^ tc-expression^)
+        check-class^ check-unit^ tc-expression^)
 (export tc-expr^)
 
 (define-literal-set tc-expr-literals #:for-label
@@ -123,6 +123,15 @@
       ;; a TR-annotated class
       [stx:tr:class^
        (check-class form expected)]
+      ;; Unit forms
+      [stx:tr:unit^
+       (check-unit form expected)]
+      [stx:tr:unit:invoke^
+       (check-invoke-unit form expected)]
+      [stx:tr:unit:compound^
+       (check-compound-unit form expected)]
+      [stx:tr:unit:from-context^
+       (check-unit-from-context form expected)]
       [stx:exn-handlers^
        (register-ignored! form)
        (check-subforms/with-handlers form expected) ]

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

@@ -6,7 +6,8 @@
          (only-in (types abbrev) (-> t:->) [->* t:->*])
          (private type-annotation parse-type syntax-properties)
          (env lexical-env type-alias-helper mvar-env
-              global-env scoped-tvar-env)
+              global-env scoped-tvar-env 
+              signature-env signature-helper)
          (rep filter-rep object-rep type-rep)
          syntax/free-vars
          (typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops)
@@ -37,7 +38,9 @@
 ;; Checks that the body has the expected type when names are bound to the types spcified by results.
 ;; The exprs are also typechecked by using expr->type.
 ;; TODO: make this function sane.
-(define/cond-contract (do-check expr->type namess expected-results exprs body expected)
+;; The `check-thunk` argument serves the same purpose as in tc/letrec-values
+(define/cond-contract (do-check expr->type namess expected-results exprs body expected 
+                                [check-thunk void])
   ((syntax? tc-results/c . -> . any/c)
    (listof (listof identifier?)) (listof (listof tc-result?))
    (listof syntax?) syntax? (or/c #f tc-results/c)
@@ -94,6 +97,9 @@
           (match results
             [(list (tc-result: ts fs os) ...)
              (expr->type expr (ret ts fs os))]))
+        ;; Perform additional context-dependent checking that needs to be done
+        ;; in the context of the letrec body
+        (check-thunk)
         ;; typecheck the body
         (tc-body/check body (and expected (erase-filter expected)))))))
 
@@ -107,15 +113,23 @@
 (define (regsiter-aliases-and-declarations names exprs)
   ;; Collect the declarations, which are represented as expressions.
   ;; We put them back into definitions to reuse the existing machinery
-  (define-values (type-aliases declarations)
-    (for/fold ([aliases '()] [declarations '()])
+  (define-values (type-aliases declarations signature-forms)
+    (for/fold ([aliases '()] [declarations '()] [signature-forms '()])
               ([body (in-list exprs)])
       (syntax-parse #`(define-values () #,body)
         [t:type-alias
-         (values (cons #'t aliases) declarations)]
+         (values (cons #'t aliases) declarations signature-forms)]
         [t:type-declaration
-         (values aliases (cons (list #'t.id #'t.type) declarations))]
-        [_ (values aliases declarations)])))
+         (values aliases (cons (list #'t.id #'t.type) declarations) signature-forms)]
+        [t:typed-define-signature
+           (values aliases declarations (cons #'t signature-forms))]
+        [_ (values aliases declarations signature-forms)])))
+
+  ;; add signature names to the signature environment, deferring type parsing
+  ;; until after aliases are registered to allow mutually recursive references
+  ;; between signatures and type aliases
+  (for/list ([sig-form (in-list (reverse signature-forms))])
+    (parse-and-register-signature! sig-form))
 
   (define-values (alias-names alias-map) (get-type-alias-info type-aliases))
   (register-all-type-aliases alias-names alias-map)
@@ -130,14 +144,22 @@
   (for ([n (in-list names)] [b (in-list exprs)])
     (syntax-case n ()
       [(var) (add-scoped-tvars b (lookup-scoped-tvars #'var))]
-      [_ (void)])))
+      [_ (void)]))
 
-(define (tc/letrec-values namess exprs body [expected #f])
+  ;; Finalize signatures, by parsing member types
+  (finalize-signatures!))
+
+;; The `thunk` argument is run only for its side effects 
+;; It is used to perform additional context-dependent checking
+;; within the context of a letrec body.
+;; For example, it is used to typecheck units and ensure that exported
+;; variables are exported at the correct types
+(define (tc/letrec-values namess exprs body [expected #f] [check-thunk void])
   (let* ([names (stx-map syntax->list namess)]
          [orig-flat-names (apply append names)]
          [exprs (syntax->list exprs)])
     (regsiter-aliases-and-declarations names exprs)
-
+    
     ;; First look at the clauses that do not bind the letrec names
     (define all-clauses
       (for/list ([name-lst names] [expr exprs])
@@ -153,19 +175,21 @@
 
     ;; Check those and then check the rest in the extended environment
     (check-non-recursive-clauses
-      ordered-clauses
-      (lambda ()
-        (cond
-          ;; after everything, check the body expressions
-          [(null? remaining-names)
-           (tc-body/check body (and expected (erase-filter expected)))]
-          [else
-           (define flat-names (apply append remaining-names))
-           (do-check tc-expr/check
-                     remaining-names
-                     ;; types the user gave.
-                     (map (λ (l) (map tc-result (map get-type l))) remaining-names)
-                     remaining-exprs body expected)])))))
+     ordered-clauses
+     (lambda ()
+       (cond
+         ;; after everything, check the body expressions
+         [(null? remaining-names)
+          (check-thunk)
+          (tc-body/check body (and expected (erase-filter expected)))]
+         [else
+          (define flat-names (apply append remaining-names))
+          (do-check tc-expr/check
+                    remaining-names
+                    ;; types the user gave.
+                    (map (λ (l) (map tc-result (map get-type l))) remaining-names)
+                    remaining-exprs body expected
+                    check-thunk)])))))
 
 ;; An lr-clause is a
 ;;   (lr-clause (Listof Identifier) Syntax)

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

@@ -9,10 +9,13 @@
          (private parse-type type-annotation syntax-properties type-contract)
          (env global-env init-envs type-name-env type-alias-env
               lexical-env env-req mvar-env scoped-tvar-env
-              type-alias-helper)
+              type-alias-helper signature-env signature-helper)
          (utils tc-utils redirect-contract)
          "provide-handling.rkt" "def-binding.rkt" "tc-structs.rkt"
          "typechecker.rkt" "internal-forms.rkt"
+         (typecheck provide-handling def-binding tc-structs
+                    typechecker internal-forms 
+                    check-below)
          syntax/location
          racket/format
          (for-template
@@ -115,6 +118,15 @@
       [(define-values (lifted) expr)
        #:when (contract-lifted-property #'expr)
        (list)]
+      
+      ;; register types of variables defined by define-values/invoke-unit forms
+      [dviu:typed-define-values/invoke-unit
+       (for ([export-sig (in-list (syntax->list #'(dviu.export.sig ...)))]
+             [export-ids (in-list (syntax->list #'(dviu.export.members ...)))])
+         (for ([id (in-list (syntax->list  export-ids))]
+               [ty (in-list (map cdr (signature->bindings export-sig)))])
+           (register-type-if-undefined id ty)))
+       (list)]
 
       ;; values definitions
       [(define-values (var ...) expr)
@@ -208,9 +220,22 @@
     (syntax-parse form
       #:literal-sets (kernel-literals)
       ;; need to special case this to avoid errors at top-level
-      [stx:tr:class^
+      [(~or stx:tr:class^
+            stx:tr:unit^
+            stx:tr:unit:invoke^
+            stx:tr:unit:compound^
+            stx:tr:unit:from-context^)
        (tc-expr #'stx)]
-
+      ;; Handle define-values/invoke-unit form typechecking, by making sure that
+      ;; inferred imports have the correct types
+      [dviu:typed-define-values/invoke-unit
+       (for ([import-sig (in-list (syntax->list #'(dviu.import.sig ...)))]
+             [import-ids (in-list (syntax->list #'(dviu.import.members ...)))])
+         (for ([member (in-list (syntax->list  import-ids))]
+               [expected-type (in-list (map cdr (signature->bindings import-sig)))])
+           (define lexical-type (lookup-type/lexical member))
+           (check-below lexical-type expected-type)))
+       'no-type]
       ;; these forms we have been instructed to ignore
       [stx:ignore^
        'no-type]
@@ -289,16 +314,23 @@
 (define (type-check forms0)
   (define forms (syntax->list forms0))
   (do-time "before form splitting")
-  (define-values (type-aliases struct-defs stx-defs0 val-defs0 provs)
+  (define-values (type-aliases struct-defs stx-defs0 val-defs0 provs signature-defs)
     (filter-multiple
      forms
      type-alias? 
      (lambda (e) (or (typed-struct? e) (typed-struct/exec? e)))
      parse-syntax-def
      parse-def
-     provide?))
+     provide?
+     typed-define-signature?))
   (do-time "Form splitting done")
 
+  ;; Register signatures in the signature environment
+  ;; but defer type parsing to allow mutually recursive refernces
+  ;; between signatures and type aliases
+  (for ([sig-form signature-defs])
+    (parse-and-register-signature! sig-form))
+
   (define-values (type-alias-names type-alias-map)
     (get-type-alias-info type-aliases))
 
@@ -313,6 +345,7 @@
   (do-time "after adding type names")
 
   (register-all-type-aliases type-alias-names type-alias-map)
+  (finalize-signatures!)
 
   (do-time "starting struct handling")
   ;; Parse and register the structure types
@@ -427,6 +460,7 @@
                 #,(tname-env-init-code)
                 #,(tvariance-env-init-code)
                 #,(mvar-env-init-code mvar-env)
+                #,(signature-env-init-code)
                 #,(make-struct-table-code)
                 #,@(for/list ([a (in-list aliases)])
                      (match-define (list from to) a)
@@ -447,7 +481,7 @@
             ;; appropriate-phase `require` statically in a module
             ;; that's non-dynamically depended on by
             ;; `typed/racket`. That makes for confusing non-local
-            ;; dependencies, though, so we do it here. 
+            ;; dependencies, though, so we do it here.
             (require typed-racket/utils/redirect-contract)
             ;; We need a submodule for a for-syntax use of
             ;; `define-runtime-module-path`:

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

@@ -10,11 +10,12 @@
          "tc-literal.rkt" "tc-expression.rkt"
          "tc-send.rkt"
          "tc-expr-unit.rkt" "check-subforms-unit.rkt"
-         "check-class-unit.rkt")
+         "check-class-unit.rkt"
+         "check-unit-unit.rkt")
 
 (provide-signature-elements tc-expr^ check-subforms^ tc-literal^)
 
 (define-values/invoke-unit/infer
   (link tc-if@ tc-lambda@ tc-app-combined@ tc-let@ tc-expr@
         tc-send@ check-subforms@ tc-apply@ tc-literal@
-        check-class@ tc-expression@))
+        check-class@ check-unit@ tc-expression@))

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

@@ -68,6 +68,8 @@
 (define -inst make-Instance)
 (define (-prefab key . types)
   (make-Prefab (normalize-prefab-key key (length types)) types))
+(define -unit make-Unit)
+(define -signature make-Signature)
 
 (define (-seq . args) (make-Sequence args))
 

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

@@ -510,6 +510,14 @@
     [(Instance: t) `(Instance ,(t->s t))] ; for cases like Error
     [(ClassTop:) 'ClassTop]
     [(? Class?) (class->sexp type)]
+    [(Unit: (list imports ...) (list exports ...) (list init-depends ...) body)
+     `(Unit
+       (import ,@(map t->s imports))
+       (export ,@(map t->s exports))
+       (init-depend ,@(map t->s init-depends))
+       ,(t->s body))]
+    [(Signature: name extends mapping)
+     (syntax->datum name)]
     [(Result: t (or (NoFilter:) (FilterSet: (Top:) (Top:))) (or (NoObject:) (Empty:))) (type->sexp t)]
     [(Result: t fs (Empty:)) `(,(type->sexp t) : ,(filter->sexp fs))]
     [(Result: t fs lo) `(,(type->sexp t) : ,(filter->sexp fs) : ,(object->sexp lo))]

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

@@ -0,0 +1,75 @@
+#lang racket/base
+
+;; This module provides helper functions for typed signatures needed for 
+;; checking subtyping and parsing unit types
+
+(require "../utils/utils.rkt"
+         (env signature-env)
+         (rep type-rep)
+         syntax/parse
+         syntax/id-set
+         racket/list
+         (only-in racket/set subset?)
+         (for-template racket/base
+                       (typecheck internal-forms)))
+
+(provide check-sub-signatures?
+         distinct-signatures?
+         flatten-sigs
+         check-imports/exports
+         check-init-depends/imports)
+
+;; (listof Signature?) procedure? -> (listof Signature?)
+;; given a list of imported/exported signatures
+;; and a parse-error procedure, ensures that the signatures are
+;; valid in that there are no overlapping signatures
+;; Returns the given list or raises an error
+(define (check-imports/exports sigs error-proc)
+  (unless (distinct-signatures? sigs) (error-proc))
+  sigs)
+
+;; (listof Signature?) (listof Signature?) procedure? -> (listof Signature?)
+;; Ensures that the init-depends signatures are a subset of the import signatures
+;; an equal? based subset check is the right thing, since each init-depend
+;; must be equal to an imported signature
+(define (check-init-depends/imports init-depends imports error-proc)
+  (unless (subset? init-depends imports) (error-proc))
+  init-depends)
+
+;; check-sub-signatures? : (listof Signature) (listof Signature) -> boolean?
+;; checks that the first list of signatures can be used to implement the second
+;; list of signatures
+(define (check-sub-signatures? sub-sigs sup-sigs)
+  (define sub-exts (immutable-free-id-set (append-map signature-extensions sub-sigs)))
+  (define sup-exts (immutable-free-id-set (append-map signature-extensions sup-sigs)))
+  (free-id-subset? sup-exts sub-exts))
+
+;; signature-extensions : (or/c #f identifier?) -> (listof identifier?)
+;; returns the list (chain) of names of each signature that
+;; the given signature extends including itself
+;; returns '() when given #f
+(define (signature-extensions sig*)
+  (let ([sig (and sig* (if (Signature? sig*) sig* (lookup-signature sig*)))])
+    (if sig
+        (cons (Signature-name sig)
+              (signature-extensions (Signature-extends sig)))
+        null)))
+
+(define (flatten-sigs sig*)
+  (let ([sig (and sig* (if (Signature? sig*) sig* (lookup-signature sig*)))])
+    (if sig
+        (cons sig (flatten-sigs (Signature-extends sig)))
+        null)))
+
+
+;;  : (listof Signature) -> boolean
+;; returns true iff the list of signatures contains no duplicates under
+;; extension
+(define (distinct-signatures? sigs)
+  (define sig-ids (append-map signature-extensions sigs))
+  (distinct-ids? sig-ids))
+
+;; distinct-ids? : (listof id) -> boolean?
+;; returns true iff the signature ids are all distinct
+(define (distinct-ids? sigs)
+  (not (check-duplicates sigs free-identifier=?)))

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

@@ -33,6 +33,7 @@
      [ChannelTop ()]
      [Async-ChannelTop ()]
      [ClassTop ()]
+     [UnitTop ()]
      [Continuation-Mark-KeyTop ()]
      [Error ()]
      [HashtableTop ()]

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

@@ -5,7 +5,7 @@
          (rep type-rep filter-rep object-rep rep-utils)
          (utils tc-utils early-return)
          (types utils resolve base-abbrev match-expanders
-                numeric-tower substitute current-seen prefab)
+                numeric-tower substitute current-seen prefab signatures)
          (for-syntax racket/base syntax/parse racket/sequence))
 
 (lazy-require
@@ -692,6 +692,17 @@
                (or (and init-rest init-rest*
                         (sub init-rest init-rest*))
                    (and (not init-rest) (not init-rest*))))]
+         [((? Unit?) (UnitTop:)) A0]
+         ;; For Unit types invoke-types are covariant
+         ;; imports and init-depends are covariant in that importing fewer
+         ;; signatures results in a subtype
+         ;; exports conversely are contravariant, subtypes export more signatures
+         [((Unit: imports exports init-depends t) (Unit: imports* exports* init-depends* t*))
+          (and (check-sub-signatures? imports* imports)
+               (check-sub-signatures? exports exports*)
+               (check-sub-signatures? init-depends* init-depends)
+               (subtype-seq A0
+                            (subtype* t t*)))]
          ;; otherwise, not a subtype
          [(_ _) #f])))
      (when (null? A)

typed-racket-lib/typed/racket.rkt

@@ -2,11 +2,14 @@
 
 (require typed/racket/base racket/require
          (subtract-in racket typed/racket/base racket/contract
-                      typed/racket/class)
+                      typed/racket/class
+                      typed/racket/unit)
          typed/racket/class
-         (for-syntax racket/base))
+         typed/racket/unit
+	 (for-syntax racket/base))
 (provide (all-from-out racket
                        typed/racket/base
-                       typed/racket/class)
-         (for-syntax (all-from-out racket/base))
+                       typed/racket/class
+                       typed/racket/unit)
+	 (for-syntax (all-from-out racket/base))
          class)

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

@@ -0,0 +1,33 @@
+#lang racket/base
+
+(require (except-in racket/unit
+                    define-signature
+                    unit
+                    invoke-unit
+                    invoke-unit/infer
+                    compound-unit
+                    define-unit
+                    define-compound-unit
+                    define-values/invoke-unit
+                    define-values/invoke-unit/infer
+                    compound-unit/infer
+                    define-compound-unit/infer
+                    unit-from-context
+                    define-unit-from-context)
+         typed-racket/base-env/unit-prims
+         typed-racket/base-env/signature-prims)
+
+(provide define-signature
+         unit
+         invoke-unit
+         invoke-unit/infer
+         compound-unit
+         define-unit
+         define-compound-unit
+         define-values/invoke-unit
+         define-values/invoke-unit/infer
+         compound-unit/infer
+         define-compound-unit/infer
+         unit-from-context
+         define-unit-from-context
+         (all-from-out racket/unit))

typed-racket-test/fail/bad-ann-from-macro-in-unit.rkt

@@ -0,0 +1,16 @@
+#;
+(exn-pred (regexp-quote "type mismatch\n  expected: Integer\n  given: String"))
+#lang typed/racket
+
+(require (for-syntax syntax/parse))
+
+
+(unit (import)
+      (export)
+      (define-syntax (my-define stx)
+        (syntax-parse stx
+          [(_ name:id #:with-type type expr)
+           #'(begin
+               (: name type)
+               (define name expr))]))
+      (my-define bad #:with-type Integer "BAD"))

typed-racket-test/fail/def-val-inv-unit-sig-mismatch.rkt

@@ -0,0 +1,7 @@
+#;
+(exn-pred (regexp-quote "type mismatch\n  expected: (Unit (import) (export x-sig) (init-depend) Any)\n  given: (Unit (import) (export) (init-depend) Void)"))
+#lang typed/racket
+
+(define-signature x-sig ([x : Integer]))
+
+(define-values/invoke-unit (unit (import) (export)) (import) (export x-sig))

typed-racket-test/fail/dviu-has-imports.rkt

@@ -0,0 +1,7 @@
+#;
+(exn-pred (regexp-quote "type mismatch\n  expected: (Unit (import) (export) (init-depend) Any)\n  given: (Unit (import x-sig) (export) (init-depend) Integer)"))
+
+#lang typed/racket
+
+(define-signature x-sig ([x : Integer]))
+(define-values/invoke-unit (unit (import x-sig) (export) x) (import) (export))

typed-racket-test/fail/dviu-infer-deps-bad.rkt

@@ -0,0 +1,19 @@
+#;
+(exn-pred #rx"unit depends on initialization of later unit")
+#lang typed/racket
+
+;; This program errors at compile time, but the check is from
+;; the untyped implementation of define-values/invoke-unit/infer
+
+(define-signature s^ ([a : Integer]))
+(define-signature t^ ([b : Integer]))
+(define-unit u@
+  (import s^)
+  (export t^)
+  (init-depend s^)
+  (define b a))
+(define-unit v@
+  (import)
+  (export s^)
+  (define a 2))
+(define-values/invoke-unit/infer (export) (link u@ v@))

typed-racket-test/fail/dviu-infer-fact-no-link.rkt

@@ -0,0 +1,22 @@
+#;
+(exn-pred #rx"define-values/invoke-unit: unit argument expects an untagged import with signature fact\\^")
+#lang typed/racket
+
+(define-signature fact^ ([fact : (-> Natural Natural)]))
+
+
+(define-unit fact@
+  (import (prefix i: fact^))
+  (export fact^)
+  (: fact (-> Natural Natural))
+  (define (fact n)
+    (if (= 0 n)
+        1
+        (* n (i:fact (sub1 n))))))
+
+;; without link this should fail
+;; see the corresponging successful test
+;; dviu-infer-fact.rkt in the succeed directory
+(define-values/invoke-unit/infer fact@)
+
+(fact 5)

typed-racket-test/fail/dviu-not-a-unit.rkt

@@ -0,0 +1,5 @@
+#;
+(exn:pred #rx"type mismatch")
+#lang typed/racket
+
+(define-values/invoke-unit 1 (import) (export))

typed-racket-test/fail/dviu-not-subtype.rkt

@@ -0,0 +1,10 @@
+#;
+(exn-pred #rx"type mismatch")
+#lang typed/racket
+
+(define-signature x-sig ([x : Integer]))
+(define-signature x-sub extends x-sig ([xx : Integer]))
+
+(define u (unit (import) (export x-sig) (define x 1)))
+
+(define-values/invoke-unit u (import) (export x-sub))

typed-racket-test/fail/extend-untyped-signature.rkt

@@ -0,0 +1,13 @@
+#;
+(exn-pred #rx"signature definition extends untyped signature")
+#lang racket
+
+(module ut1 racket
+  (provide a^)
+  (define-signature a^ (a)))
+
+(module t1 typed/racket
+  (require (submod ".." ut1))
+  (define-signature a-sub^ extends a^ ())
+  (unit (import a-sub^) (export) a))
+  

typed-racket-test/fail/signature-escape.rkt

@@ -0,0 +1,18 @@
+#;
+(exn-pred (regexp-quote "type mismatch\n  expected: (Unit (import bad^) (export) (init-depend bad^) AnyValues)\n  given: (Unit (import bad^) (export) (init-depend) Void)\n  in: (invoke-unit bad (import bad^))"))
+#lang typed/racket
+
+;; The full error message for this prorgam is
+;; Type Checker: type mismatch
+;; expected: (Unit (import bad^) (export) (init-depend bad^) AnyValues)
+;; given: (Unit (import bad^) (export) (init-depend) Void)
+;; in: (invoke-unit bad (import bad^))
+
+
+(define-signature bad^ ())
+(define bad
+  (let ()
+    (define-signature bad^ ())
+    (unit (import bad^) (export))))
+
+(invoke-unit bad (import bad^))

typed-racket-test/fail/unit-contract-missing-init-depends.rkt

@@ -0,0 +1,20 @@
+#;
+(exn-pred #rx"contract does not list initialization dependency a\\^")
+
+#lang racket
+
+(module untyped racket
+  (provide (all-defined-out))
+  (define-signature a^ (a))
+  (define-unit u
+    (import a^)
+    (export)
+    (init-depend a^)
+    a))
+
+(module typed typed/racket
+  (require/typed (submod ".." untyped)
+    [#:signature a^ ([a : Any])]
+    [u (Unit (import a^) (export) Any)]))
+
+(require 'typed)

typed-racket-test/fail/unit-ctc-init-depends.rkt

@@ -0,0 +1,24 @@
+#;
+(exn-pred #rx"x@: broke its own contract;\n contract does not list initialization dependency x\\^")
+#lang racket
+
+
+(module untyped racket
+  (provide x^ x@)
+  (define-signature x^ (x))
+  (define x@ 
+    (unit
+      (import x^)
+      (export)
+      (init-depend x^)
+      x)))
+
+(module typed typed/racket
+  (require/typed (submod ".." untyped)
+    [#:signature x^ ([x : Integer])]
+    [x@ (Unit (import x^)
+              (export)
+              Integer)]))
+
+(require 'typed)
+

typed-racket-test/fail/unit-import-wrong-type.rkt

@@ -0,0 +1,13 @@
+#;
+(exn-pred #rx"Type Checker: type mismatch\n  expected: Integer\n  given: String")
+#lang typed/racket/base
+(require typed/racket/unit)
+
+
+(define-signature x^ ([x : String]))
+
+(unit (import x^)
+      (export )
+      (: y Integer)
+      (define y x)
+      y)

typed-racket-test/fail/unit-typed-untyped-1.rkt

@@ -0,0 +1,14 @@
+#;
+(exn-pred #rx"u: broke its own contract\n  promised: Integer")
+#lang racket
+
+(module untyped racket
+  (provide u)
+  (define u (unit (import) (export) "not an integer")))
+
+(module typed typed/racket
+  (require/typed (submod ".." untyped)
+    [u (Unit (import) (export) Integer)])
+  (invoke-unit u))
+
+(require 'typed)

typed-racket-test/fail/unit-typed-untyped-2.rkt

@@ -0,0 +1,19 @@
+#;
+(exn-pred #rx"u: contract violation\n  expected: Integer")
+#lang racket
+
+(module typed typed/racket
+  (provide (all-defined-out))
+  (define-signature x^ ([x : Integer]))
+  (define-signature y^ ([y : (-> Integer Integer)]))
+
+  (define u
+    (unit (import x^) (export y^) (define (y n) x))))
+
+(module untyped racket
+  (require (submod ".." typed))
+  (define x 11)
+  (define-values/invoke-unit u (import x^) (export y^))
+  (y "not an integer"))
+
+(require 'untyped)

typed-racket-test/succeed/define-values-invoke-unit-subtyping.rkt

@@ -0,0 +1,11 @@
+#lang typed/racket
+
+(define-signature a1^ ([a1 : Integer]))
+(define-signature a2^ extends a1^ ([a2 : Integer]))
+(define-signature b^ ([b : Integer]))
+
+(define-unit u1 (import) (export a2^) (define a1 6) (define a2 7))
+(define-unit u2 (import a1^) (export b^) (define b (+ a1 11)))
+
+
+(define-values/invoke-unit/infer (export) (link u1 u2))

typed-racket-test/succeed/dviu-infer-deps-ok.rkt

@@ -0,0 +1,14 @@
+#lang typed/racket
+
+(define-signature s^ ([a : Integer]))
+(define-signature t^ ([b : Integer]))
+(define-unit u@
+  (import s^)
+  (export t^)
+  (init-depend s^)
+  (define b a))
+(define-unit v@
+  (import)
+  (export s^)
+  (define a 2))
+(define-values/invoke-unit/infer (export) (link v@ u@))

typed-racket-test/succeed/dviu-infer-fact.rkt

@@ -0,0 +1,20 @@
+#lang typed/racket
+
+(define-signature fact^ ([fact : (-> Natural Natural)]))
+
+
+(define-unit fact@
+  (import (prefix i: fact^))
+  (export fact^)
+  (: fact (-> Natural Natural))
+  (define (fact n)
+    (if (= 0 n)
+        1
+        (* n (i:fact (sub1 n))))))
+
+;; without link this should fail
+;; see the corresponding test for failure:
+;; dviu-infer-fact-no-link.rkt in the fail directory
+(define-values/invoke-unit/infer (link fact@))
+
+(fact 5)

typed-racket-test/succeed/dviu-unit-from-context.rkt

@@ -0,0 +1,10 @@
+#lang typed/racket
+
+(define-signature yz-sig ([y : Integer] [z : Integer]))
+(define y 1)
+(define z 10)
+(define-values/invoke-unit (unit-from-context yz-sig)
+  (import)
+  (export (prefix x: yz-sig)))
+(+ x:y x:z)
+

typed-racket-test/succeed/macro-in-unit.rkt

@@ -0,0 +1,27 @@
+#lang typed/racket
+
+
+(require (for-syntax syntax/parse))
+
+(define-signature x^ ([x : Integer] [y : String] [z : (-> Symbol)]))
+
+(unit (import)
+      (export x^)
+      (define-syntax (my-define stx)
+        (syntax-parse stx
+          [(_ name:id expr:exact-integer)
+           #'(begin
+               (: name Integer)
+               (define name expr))]
+          [(_ name:id expr:str)
+           #'(begin
+               (: name String)
+               (define name expr))]
+          [(_ name:id #:with-type type expr)
+           #'(begin
+               (: name type)
+               (define name expr))]))
+      (my-define x 17)
+      (my-define a "hello")
+      (my-define y "a string")
+      (my-define z #:with-type (-> Symbol) (λ () (string->symbol y))))

typed-racket-test/succeed/simple-unit-scope.rkt

@@ -0,0 +1,7 @@
+#lang typed/racket
+
+(define-signature y^ ([y : Integer]))
+
+(let ((y 1))
+  (unit (import) (export y^)
+        (define y 2)))

typed-racket-test/succeed/unit-3x-2.rkt

@@ -0,0 +1,67 @@
+#lang typed/racket
+
+(define-signature is-3x-sig ([is-3x : (-> Natural Boolean)]))
+(define-signature is-3x+1-sig ([is-3x+1 : (-> Natural Boolean)]))
+(define-signature is-3x+2-sig ([is-3x+2 : (-> Natural Boolean)]))
+
+(define is-3x-unit
+  (unit 
+    (import is-3x+2-sig)
+    (export is-3x-sig)
+    (: is-3x (-> Natural Boolean))
+    (define (is-3x x)
+      (or (= 0 x) (is-3x+2 (sub1 x))))))
+
+(define is-3x+2-unit
+  (unit 
+    (import is-3x+1-sig)
+    (export is-3x+2-sig)
+    (: is-3x+2 (-> Natural Boolean))
+    (define (is-3x+2 x)
+      (and (> x 0) (is-3x+1 (sub1 x))))))
+
+(define is-3x+1-unit
+  (unit
+    (import is-3x-sig)
+    (export is-3x+1-sig)
+    (: is-3x+1 (-> Natural Boolean))
+    (define (is-3x+1 x)
+      (and (> x 0) (is-3x (sub1 x))))))
+
+(define 3x-compound1
+  (compound-unit (import (IS-3X : is-3x-sig))
+                 (export IS-3X+1 IS-3X+2)
+                 (link (((IS-3X+1 : is-3x+1-sig)) is-3x+1-unit IS-3X)
+                       (((IS-3X+2 : is-3x+2-sig)) is-3x+2-unit IS-3X+1))))
+
+(define 3x-compound2
+  (compound-unit (import)
+                 (export IS-3X)
+                 (link (((IS-3X : is-3x-sig)) is-3x-unit IS-3X+2)
+                       (((IS-3X+1 : is-3x+1-sig)
+                         (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X))))
+
+(define 3x-run-unit
+  (unit 
+    (import is-3x-sig is-3x+1-sig is-3x+2-sig)
+    (export)
+    (list (is-3x 1)
+          (is-3x 3)
+          (is-3x+1 5)
+          (is-3x+1 7)
+          (is-3x+2 4)
+          (is-3x+2 8))))
+
+(define 3x-compound3
+  (compound-unit (import)
+                 (export IS-3X IS-3X+1 IS-3X+2)
+                 (link (((IS-3X : is-3x-sig)) 3x-compound2)
+                       (((IS-3X+1 : is-3x+1-sig)
+                         (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X)
+                       (() 3x-run-unit IS-3X IS-3X+1 IS-3X+2))))
+
+
+(define-values/invoke-unit 3x-compound3 (import) (export is-3x-sig is-3x+1-sig (rename is-3x+2-sig (y is-3x+2))))
+(list (y 8)
+      (is-3x+1 7)
+      (is-3x 6))

typed-racket-test/succeed/unit-3x.rkt

@@ -0,0 +1,71 @@
+#lang typed/racket
+
+(define-signature is-3x-sig ([is-3x : (-> Natural Boolean)]))
+(define-signature is-3x+1-sig ([is-3x+1 : (-> Natural Boolean)]))
+(define-signature is-3x+2-sig ([is-3x+2 : (-> Natural Boolean)]))
+
+(define is-3x-unit
+  (unit 
+    (import is-3x+2-sig)
+    (export is-3x-sig)
+    (: is-3x (-> Natural Boolean))
+    (define (is-3x x)
+      (or (= 0 x) (is-3x+2 (sub1 x))))))
+
+(define is-3x+2-unit
+  (unit 
+    (import is-3x+1-sig)
+    (export is-3x+2-sig)
+    (: is-3x+2 (-> Natural Boolean))
+    (define (is-3x+2 x)
+      (and (> x 0) (is-3x+1 (sub1 x))))))
+
+(define is-3x+1-unit
+  (unit
+    (import is-3x-sig)
+    (export is-3x+1-sig)
+    (: is-3x+1 (-> Natural Boolean))
+    (define (is-3x+1 x)
+      (and (> x 0) (is-3x (sub1 x))))))
+
+(define 3x-compound1
+  (compound-unit (import (IS-3X : is-3x-sig))
+                 (export IS-3X+1 IS-3X+2)
+                 (link (((IS-3X+1 : is-3x+1-sig)) is-3x+1-unit IS-3X)
+                       (((IS-3X+2 : is-3x+2-sig)) is-3x+2-unit IS-3X+1))))
+
+(define 3x-compound2
+  (compound-unit (import)
+                 (export IS-3X)
+                 (link (((IS-3X : is-3x-sig)) is-3x-unit IS-3X+2)
+                       (((IS-3X+1 : is-3x+1-sig)
+                         (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X))))
+
+(define 3x-run-unit
+  (unit 
+    (import is-3x-sig is-3x+1-sig is-3x+2-sig)
+    (export)
+    (list (is-3x 1)
+          (is-3x 3)
+          (is-3x+1 5)
+          (is-3x+1 7)
+          (is-3x+2 4)
+          (is-3x+2 8))))
+
+(define 3x-compound3
+  (compound-unit (import)
+                 (export IS-3X IS-3X+1 IS-3X+2)
+                 (link (((IS-3X : is-3x-sig)) 3x-compound2)
+                       (((IS-3X+1 : is-3x+1-sig)
+                         (IS-3X+2 : is-3x+2-sig)) 3x-compound1 IS-3X)
+                       (() 3x-run-unit IS-3X IS-3X+1 IS-3X+2))))
+
+(invoke-unit 3x-compound3)
+
+(define-values/invoke-unit 3x-compound3 (import) (export is-3x-sig is-3x+1-sig is-3x+2-sig))
+
+(list (is-3x+2 8)
+      (is-3x+1 7)
+      (is-3x 6))
+
+

typed-racket-test/succeed/unit-typed-untyped-compound-1.rkt

@@ -0,0 +1,20 @@
+#lang racket
+
+(module typed typed/racket
+  (provide (all-defined-out))
+  (define-signature x^ ([x : Integer]))
+  (define u (unit (import x^) (export) (lambda ([n : Integer]) (+ n x)))))
+
+(module untyped racket
+  (require (submod ".." typed))
+  (define v (unit (import) (export x^) (define x 11)))
+  (define w (compound-unit
+             (import)
+             (export)
+             (link (([X : x^]) v)
+                   (() u X))))
+
+  (define f (invoke-unit w))
+  (f 6))
+
+(require 'untyped)

typed-racket-test/succeed/unit-typed-untyped-compound-2.rkt

@@ -0,0 +1,22 @@
+#lang racket
+
+(module untyped racket
+  (provide (all-defined-out))
+  (define-signature x^ (x))
+  (define u (unit (import x^) (export) (lambda (n) (+ n x)))))
+
+(module typed typed/racket
+  (require/typed (submod ".." untyped)
+    [#:signature x^ ([x : Integer])]
+    [u (Unit (import x^) (export) (-> Integer Integer))])
+  (define v (unit (import) (export x^) (define x 11)))
+  (define w (compound-unit
+             (import)
+             (export)
+             (link (([X : x^]) v)
+                   (() u X))))
+
+  (define f (invoke-unit w))
+  (f 6))
+
+(require 'typed)

typed-racket-test/succeed/unit-typed-untyped-values.rkt

@@ -0,0 +1,17 @@
+#lang racket
+
+(module typed typed/racket
+  (provide (all-defined-out))
+  (define u 
+    (unit (import)
+          (export)
+          (values (lambda ([x : String]) x) 
+                  (lambda ([n : Integer]) (sqr n))))))
+
+(module untyped racket
+  (require (submod ".." typed))
+  (define-values (f g) (invoke-unit u))
+  (f "string")
+  (g 5))
+
+(require 'untyped)

typed-racket-test/succeed/units-no-sigs.rkt

@@ -0,0 +1,33 @@
+#lang typed/racket
+
+(define-signature yz-sig ([y : Integer] [z : Integer]))
+
+(let ((y 1)
+      (z 10))
+  (define u (unit (import) (export yz-sig)
+                  (define y 2)
+                  (define z 3)))
+  (define u1 (unit (import) (export)
+                   y))
+  (define u2 (unit (import (only yz-sig z)) (export)
+                   y))
+  (define u3 (unit (import (except yz-sig y)) (export)
+                   y))
+  (define u4 (unit (import (prefix s: yz-sig)) (export)
+                   y))
+  (define u5 (unit (import (rename yz-sig (r y))) (export)
+                   y))
+  (define u6 (unit (import yz-sig) (export)
+                   y))
+  (: l (-> (Unit (import yz-sig) (export) Integer) Integer))
+  (define (l x)
+    (invoke-unit
+     (compound-unit (import) (export)
+                    (link (((YZ : yz-sig)) u)
+                          (() x YZ)))))
+  (invoke-unit u1)
+  (l u2)
+  (l u3)
+  (l u4)
+  (l u5)
+  (l u6))

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

@@ -44,4 +44,5 @@
   "rep-tests.rkt"
   "prims-tests.rkt"
   "tooltip-tests.rkt"
-  "prefab-tests.rkt")
+  "prefab-tests.rkt"
+  "typed-units-tests.rkt")

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

@@ -246,7 +246,19 @@
               (t (-class #:method ([m (-polydots (x) (->... (list) (x x) -Void))])))
               (t (-class #:method ([m (-polyrow (x) (list null null null null)
                                         (-> (-class #:row (-v x)) -Void))])))
-
+              
+              ;; units
+              ;; These tests do not have sufficient coverage because more
+              ;; coverage requires a proper set up of the signature environment.
+              ;; Further coverage of unit contract compilations occurs in
+              ;; integration tests.
+              (t-sc (-unit null null null (-values (list -Integer)))
+                    (unit/sc null null null (list integer/sc)))
+              (t-sc (-unit null null null (-values (list -Integer -Number)))
+                    (unit/sc null null null (list integer/sc number/sc)))
+              (t-sc (-unit null null null (-values (list)))
+                    (unit/sc null null null null))
+                            
               ;; typed/untyped interaction tests
               (t-int (-poly (a) (-> a a))
                      (λ (f) (f 1))

typed-racket-test/unit-tests/parse-type-tests.rkt

@@ -21,6 +21,7 @@
          (only-in (base-env case-lambda) case-lambda)
          (prefix-in un: (only-in racket/class init init-field field augment))
          (only-in typed/racket/class init init-field field augment)
+         (only-in racket/unit import export init-depend)
 
          rackunit)
 
@@ -381,6 +382,26 @@
            ((Class #:row-var r (init y)) -> (Class #:row-var r)))]
    [FAIL (All (r #:row (init x y z) (field f) m n)
            ((Class #:row-var r a b c) -> (Class #:row-var r)))]
+   
+   ;; parsing tests for Unit types
+   ;; These are only simple tests because checking types
+   ;; with signatures requires interaction with the Signature
+   ;; environment. Additionally, more complex tests of Unit
+   ;; type parsing happens in unit-tests and integrations tests as well
+   [(Unit (import) (export) (init-depend) String)
+    (make-Unit null null null (-values (list -String)))]
+   [(Unit (import) (export) String)
+    (make-Unit null null null (-values (list -String)))]
+   [(Unit (import) (export) (init-depend))
+    (make-Unit null null null (-values (list -Void)))]
+   [(Unit (import) (export))
+    (make-Unit null null null (-values (list -Void)))]
+   [UnitTop (make-UnitTop)]
+   [FAIL (Unit (export) String)]
+   [FAIL (Unit (import) String)]
+   [FAIL (Unit (init-depend) String)]
+   [FAIL (Unit (import bad) (export) String)]
+   [FAIL (Unit (import) (export bad) String)]
    ))
 
 ;; FIXME - add tests for parse-values-type, parse-tc-results

typed-racket-test/unit-tests/static-contract-conversion-tests.rkt

@@ -48,7 +48,6 @@
            (with-check-info (['static sc])
              (fail-check "Type was incorrectly converted to contract"))))]))
 
-
 (define tests
   (test-suite "Conversion Tests"
     (t/sc (-Number . -> . -Number))
@@ -70,4 +69,11 @@
     (t/sc (-mu a (-box a)))
     (t/sc (-mu sexp (Un -Null -Symbol (-pair sexp sexp) (-vec sexp) (-box sexp))))
     (t/sc (-mu a (-> a a)))
-    (t/sc (-seq -Symbol))))
+    (t/sc (-seq -Symbol))
+    ;; These tests for unit static contracts are insufficient, but
+    ;; in order to test Unit types the signature environment must be
+    ;; set up correctly. More complex cases of compilation to unit/c
+    ;; contracts are tested by integration tests.
+    (t/sc (-unit null null null (-values (list -String))))
+    (t/sc (-unit null null null (-values (list -Symbol -String))))
+    (t/fail (-unit null null null ManyUniv))))

typed-racket-test/unit-tests/type-printer-tests.rkt

@@ -137,7 +137,38 @@
     (check-prints-as? (cl->* (->opt -Pathlike [-String] -Void)
                              (->optkey Univ [-String] #:rest -String #:x -String #t -Void))
                       (string-append "(case-> (->* (Path-String) (String) Void) "
-                                     "(->* (Any #:x String) (String) #:rest String Void))")))
+                                     "(->* (Any #:x String) (String) #:rest String Void))"))
+    (check-prints-as? (make-Unit null null null -String)
+                      "(Unit (import) (export) (init-depend) String)")
+    ;; Setup for slightly more complex unit printing test
+    (let* ([a^ (make-Signature #'a^ #f null)]
+           [a-sub^ (make-Signature #'a-sub^ a^ (list (cons #'a -String)))]
+           [b^ (make-Signature #'b^ #f (list (cons #'b -Integer)))]
+           [c^ (make-Signature #'c^ #f (list (cons #'c -Symbol)))]
+           [d^ (make-Signature #'d^ #f (list (cons #'d -String)))])
+      (check-prints-as? (make-Unit (list a^) null null -String)
+                        "(Unit (import a^) (export) (init-depend) String)")
+      (check-prints-as? (make-Unit (list a^) (list b^) null -String)
+                        "(Unit (import a^) (export b^) (init-depend) String)")
+      (check-prints-as? (make-Unit (list a^) (list b^) (list a^) -String)
+                        "(Unit (import a^) (export b^) (init-depend a^) String)")
+      (check-prints-as? (make-Unit (list a-sub^) null null -String)
+                        "(Unit (import a-sub^) (export) (init-depend) String)")
+      (check-prints-as? (make-Unit (list a-sub^) null (list a-sub^)  -String)
+                        "(Unit (import a-sub^) (export) (init-depend a-sub^) String)")
+      (check-prints-as? (make-Unit null (list a-sub^) null -String)
+                        "(Unit (import) (export a-sub^) (init-depend) String)")
+      (check-prints-as? (make-Unit (list a^ b^) (list c^ d^) null -String)
+                        "(Unit (import a^ b^) (export c^ d^) (init-depend) String)")
+      (check-prints-as? (make-Unit (list a^ b^) null null -String)
+                        "(Unit (import a^ b^) (export) (init-depend) String)")
+      (check-prints-as? (make-Unit null (list c^ d^) null -String)
+                        "(Unit (import) (export c^ d^) (init-depend) String)")
+      (check-prints-as? (make-Unit (list a^ b^) (list c^ d^) (list b^) -String)
+                        "(Unit (import a^ b^) (export c^ d^) (init-depend b^) String)")
+      (check-prints-as? (make-Unit (list a^ b^) (list c^ d^) (list b^ a^) -String)
+                        "(Unit (import a^ b^) (export c^ d^) (init-depend b^ a^) String)"))
+    (check-prints-as? (make-UnitTop) "UnitTop"))
    (test-suite
     "Pretty printing tests"
     (check-pretty-prints-as? (-val 3) "3")

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

@@ -0,0 +1,775 @@
+#lang racket/base
+
+;; Unit tests for typed units
+
+(require (submod "typecheck-tests.rkt" test-helpers)
+         (except-in "test-utils.rkt" private)
+         (for-syntax racket/base
+                     typed-racket/tc-setup
+                     typed-racket/utils/tc-utils))
+
+(provide tests)
+(gen-test-main)
+
+(begin-for-syntax
+  ;; for checking the printing of type aliases
+  (current-type-names (init-current-type-names)))
+
+;; see typecheck-tests.rkt for rationale on imports
+(require rackunit
+         typed/racket/unit
+         (except-in typed-racket/utils/utils private)
+         (except-in (base-env extra-procs prims class-prims
+                              base-types base-types-extra)
+                    define lambda λ case-lambda)
+         (prefix-in tr: (only-in (base-env prims) define lambda λ case-lambda))
+         (for-syntax (rep type-rep filter-rep object-rep)
+                     (rename-in (types abbrev union numeric-tower filter-ops utils)
+                                [Un t:Un]
+                                [-> t:->])))
+
+(define tests
+  (test-suite
+   "unit typechecking tests"
+   ;; simple tests that annotations work appropriately
+   [tc-e
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (unit
+        (import)
+        (export a^)
+        (: a Natural)
+        (define a 5))
+      (void))
+    -Void]
+   [tc-err
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (unit
+        (import)
+        (export a^)
+        (: a String)
+        (define a 5))
+      (error ""))]
+   [tc-e
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (unit
+        (import)
+        (export a^)
+        (: a Integer)
+        (define a 5)
+        (: b String)
+        (define b "foo"))
+      (void))
+    -Void]
+   [tc-err
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (unit
+        (import)
+        (export a^)
+        (: a Integer)
+        (define a 5)
+        (: b String)
+        (define b 5)e)
+      (error ""))]
+
+   [tc-e
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (define-type-alias Foo (Unit (import a^) (export) Integer))
+      (define a 17)
+      (: u (Unit (import a^) (export) Integer))
+      (define u (unit (import a^) (export) a))
+      (invoke-unit u (import a^)))
+    -Integer]
+
+   [tc-e
+    (let ()
+      (define-type-alias Foo (U Integer (Unit (import a^) (export) Foo)))
+      (define-signature a^ ([a : Foo]))
+      (: u Foo)
+      (define u (unit (import a^) (export) a))
+      (define a 11)
+      (invoke-unit (assert u unit?) (import a^))
+      (void))
+    -Void]
+
+   #|
+   This should typecheck, but doesn't because fact has no type annotation
+   
+   (define-signature fact^
+     ([fact : (-> Integer Integer)]))
+
+
+
+   (define-unit fact@
+   (import (prefix i: fact^))
+   (export fact^)
+   (define (fact n) 
+   (if (< n 1) 
+   1
+   (* n (i:fact (sub1 n)))))
+   fact)
+   |#
+  [tc-e
+   (let ()
+     (define-signature a^ ())
+     (define-signature b^ ())
+     
+     (define-unit u
+       (import a^)
+       (export))
+
+     (define-unit v
+       (import)
+       (export a^ b^)
+       5)
+
+     (define-compound-unit/infer w
+       (import)
+       (export)
+       (link (() u A)
+             (([A : a^] [B : b^]) v)))
+     
+     (define-compound-unit/infer w2
+       (import [A : a^])
+       (export)
+       (link (() u A)))
+
+     (define-compound-unit/infer w3
+       (import) 
+       (export)
+       (link u v))
+     
+     (define-compound-unit/infer w4
+       (import a^)
+       (export)
+       (link u))
+     (void))
+   -Void]
+   
+   [tc-err
+    (let ()
+      (unit (import)
+            (export)
+        (+ 1 "bad"))
+      (error ""))]
+
+   ;; factorial with units
+   [tc-e
+    (let ()
+      (define-signature fact^ ([fact : (-> Integer Natural)]))
+      
+      (define-unit fact@
+        (import (prefix i: fact^))
+        (export fact^)
+        (: fact (-> Integer Natural))
+        (define (fact n)
+          (if (<= n 1) 1 (* n (i:fact (sub1 n)))))
+        fact)
+      
+      (define-compound-unit/infer fact-c@
+        (import)
+        (export)
+        (link fact@))
+      
+      (define factorial (invoke-unit fact-c@))
+      
+      (factorial 5))
+    -Nat]
+
+   ;; factorial + invoke-unit/infer
+   [tc-e
+    (let ()
+      (define-signature fact^ ([fact : (-> Integer Natural)]))
+      (define-unit fact@
+        (import (prefix i: fact^))
+        (export fact^)
+        (: fact (-> Integer Natural))
+        (define (fact n)
+          (if (<= n 1) 1 (* n (i:fact (sub1 n)))))
+        fact)
+      (define fact (invoke-unit/infer fact@))
+      (fact 5))
+    -Nat]
+   [tc-e
+    (let ()
+      (define a 11)
+      (let ()
+        (define-signature a^ ([a : Integer]))
+        (define-unit u
+          (import a^)
+          (export)
+          (: x Integer)
+          (define x a)
+          x)
+        (invoke-unit/infer u)))
+    -Integer]
+
+   ;; Make sure scoping doesn't break the typed unit expansion/typechecking
+   [tc-e
+    (let ()
+      (define-signature x^ ([x : Number]))
+      (define u 
+        (unit 
+          (import x^)
+          (export)
+          (unit (import x^) (export) x)))
+      (void))
+    -Void]
+   [tc-e
+    (let ()
+      (define-signature x^ ([x : Number]))
+      (unit 
+        (import)
+        (export x^)
+        (define x^ "FOOBAR")
+        (define x 5))
+      (void))
+    -Void]
+
+   [tc-e
+    (let ()
+      (define-signature x^ ([x : (-> Integer Integer)]))
+      (unit 
+        (import x^)
+        (export)
+        (define-signature x^ ([y : (-> Natural Real)]))
+        (unit
+          (import)
+          (export x^)
+          (define y x))
+        (void))
+      (void))
+    -Void]
+
+   ;; Tests adapted from racket-tests/tests/units/test-unit.rkt
+   [tc-e
+    (begin (invoke-unit (unit (import) (export) 12)) (void))
+    -Void]
+
+   [tc-e
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (define-signature y-sig ([y : Integer]))
+      (define-signature z-sig ([z : Integer]))
+      (define-signature empty-sig ())
+
+      (invoke-unit
+       (compound-unit (import) (export)
+                      (link (((X : x-sig) (Y : y-sig)) (unit (import empty-sig z-sig)
+                                                         (export y-sig x-sig)
+                                                         (define x 1)
+                                                         (define y 2))
+                             Z E)
+                            (((Z : z-sig) (E : empty-sig)) (unit (import x-sig y-sig)
+                                                             (export empty-sig z-sig)
+                                                             (define z 3)
+                                                             3) X Y)))))
+    -PosByte]
+
+   [tc-e
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (define-signature xy-sig ([x : Integer] [y : Integer]))
+      (define-signature b-sig ([b : Integer]))
+
+      (let ((un (compound-unit (import) (export S U)
+                               (link (((S : x-sig)) (unit (import) (export x-sig) (define x 10)))
+                                     (((U : xy-sig)) (unit (import) (export xy-sig) (define x 11) (define y 12)))))))
+        (invoke-unit
+         (compound-unit (import) (export)
+                        (link (((S : x-sig) (U : xy-sig)) un)
+                              (((B : b-sig)) (unit (import x-sig) (export b-sig) (define b x)) S)
+                              (() (unit (import b-sig xy-sig) (export) (list b x y)) B U)))))
+      (void))
+    -Void]
+
+   [tc-e
+    (let ()
+      (define-signature even-sig ([even : (-> Integer Boolean)]))
+      (define-signature odd-sig ([odd : (-> Integer Boolean)]))
+      
+      (define even-unit
+        (unit (import odd-sig)
+          (export even-sig)
+          (: even (-> Integer Boolean))
+          (define (even x)
+            (or (= 0 x) (odd (sub1 x))))))
+      
+      (define odd-unit
+        (unit (import even-sig)
+        (export odd-sig)
+        (: odd (-> Integer Boolean))
+        (define (odd x)
+          (and (> x 0) (even (sub1 x))))
+        (define x (odd 11))
+        x))
+      
+      (define run-unit
+        (compound-unit (import)
+                       (export)
+                       (link (((EVEN : even-sig)) even-unit ODD)
+                             (((ODD : odd-sig)) odd-unit EVEN))))
+
+      (invoke-unit run-unit))
+    -Boolean]
+
+   [tc-e
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (define-signature yz-sig ([y : Integer] [z : Integer]))
+      (invoke-unit
+        (compound-unit
+         (import)
+         (export)
+         (link (((T : yz-sig))
+                (unit (import x-sig) (export yz-sig)
+                  (define-values (y a) (values 1 2))
+                  (define-values (b z) (values y a)))
+                S)
+               (((S : x-sig))
+                (unit (import yz-sig) (export x-sig) (define x 3) (+ y z)) T)))))
+    -Integer]
+
+   [tc-e
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (invoke-unit
+       (unit 
+         (import)
+         (export x-sig)
+         (define-syntax (y stx)
+           (syntax-case stx ()
+             ((_ x) #'(define x 1))))
+         (y x)
+         x)))
+    -One]
+
+   [tc-e
+    (let ()
+      (define-signature fact-sig ([fact : (-> Natural Natural)] [n : Natural]))
+      (invoke-unit
+       (compound-unit (import) (export)
+                      (link (((F : fact-sig)) (unit (import (except (rename fact-sig (f-in fact)) n))
+                                                (export (rename fact-sig (f-out fact)))
+                                                (define n 1)
+                                                (: f-out (-> Natural Natural))
+                                                (define (f-out x) (if (= 0 x)
+                                                                      1
+                                                                      (* x (f-in (sub1 x))))))
+                             F)
+                            (() (unit (import (only fact-sig fact)) (export)
+                                  (define n 2)
+                                  (fact 4))
+                             F)))))
+    -Nat]
+
+   [tc-e
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (invoke-unit
+       (compound-unit (import) (export)
+                      (link (((S : x-sig)) (unit (import) (export x-sig) (define x 1)))
+                            (() (unit (import (prefix s: x-sig)) (export) s:x) S)))))
+    -Integer]
+
+   [tc-e
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (define-signature xy-sig ([x : Integer] [y : Integer]))
+      (define-signature yz-sig ([y : Integer] [z : Integer]))
+      (define-signature sx ([x : Integer]))
+      (define-signature sy ([y : Integer]))
+      (define-signature sz ([z : Integer]))
+      (invoke-unit
+       (compound-unit (import) (export)
+                      (link (((S : x-sig) (T : yz-sig) (U : xy-sig))
+                             (unit (import) (export (rename x-sig (s:x x))
+                                                    (rename yz-sig (t:y y) (t:z z))
+                                                    (prefix u: xy-sig))
+                               (define x 1) (define y 2) (define z 3)
+                               (define s:x x) (define t:y y) (define t:z z) (define u:x x) (define u:y y)))
+                            (((SX : sx)) (unit (import (prefix s: x-sig)) (export sx) (define x s:x)) S)
+                            (((SY : sy)) (unit (import (prefix u: xy-sig)) (export sy) (define y u:y)) U)
+                            (((SZ : sz)) (unit (import (prefix t: yz-sig)) (export sz) (define z t:z)) T)
+                            (() (unit (import sx sy sz) (export) (+ x y z)) SX SY SZ)))))
+    -Integer]
+
+   [tc-e
+    (let ()
+      (define-signature b-sig ([b : Integer]))
+      (let ([b : String "WRONG b"])
+        (define u1 (unit (import) (export b-sig) (define b 2)))
+        (define u2 (unit (import b-sig) (export) b))
+        (invoke-unit (compound-unit (import) (export)
+                                    (link (((B : b-sig)) u1)
+                                          (() u2 B))))))
+    -Integer]
+
+   ;; subtyping tests
+   [tc-e
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (define-signature y-sig ([y : Integer]))
+      (define-signature x-sub extends x-sig ([xx : Integer]))
+      (define-signature y-sub extends y-sig ([yy : Integer]))
+            
+      (define u1 (unit (import x-sig) (export y-sub) (define y (add1 x)) (define yy 2) (+ x y yy)))
+      (define u2 (unit (import y-sig) (export x-sub) (define x 3) (define xx 44)))
+
+      (invoke-unit
+         (compound-unit (import) (export)
+                        (link (((S1 : x-sig)) u2 S2)
+                              (((S2 : y-sig)) u1 S1)))))
+    -Integer]
+   ;; Make sure let expressions order the signature processing correctly
+   [tc-e
+    (let ()
+      (let ()
+        (define-signature y-sig ([y : Integer]))
+        (define-signature y-sub extends y-sig ([yy : String]))
+        (unit (import) (export y-sub) (define y 1) (define yy "yy is a string"))
+        (void)))
+    -Void]
+
+   ;; check that invoke-unit and invoke-unit/infer both work correctly
+   [tc-e
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (define-signature aa^ extends a^ ([aa : String]))
+
+      (define-unit u (import a^) (export) a)
+      (define a 1)
+      (define aa "One")
+      (invoke-unit/infer u))
+    -Integer]
+
+   [tc-e
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (define-signature aa^ extends a^ ([aa : String]))
+
+      (define-unit u (import a^) (export) a)
+      (define a 1)
+      (define aa "One")
+      (invoke-unit u (import aa^)))
+    -Integer]
+
+   ;; Sanity checking combinations of compound-unit and invoke-unit
+   [tc-e
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (define u@ (unit (import) (export a^) (define a 5)))
+      (invoke-unit
+       (compound-unit
+        (import)
+        (export)
+        (link (((a^1 : a^)) u@)
+              (()
+               (unit
+                 (import a^)
+                 (export)
+                 (values a))
+               a^1))) (import)))
+    -Integer]
+
+   [tc-e
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (define-unit u@ (import) (export a^) (define a 5))
+      (invoke-unit
+       (compound-unit
+        (import)
+        (export)
+        (link (((a^1 : a^)) u@)
+              (()
+               (unit
+                 (import a^)
+                 (export)
+                 (values a))
+               a^1))) (import)))
+    -Integer]
+
+    ;; make sure that invoke-unit/infer works when there is a link clause
+    [tc-e
+     (let ()
+       (define-signature a^ ([a : Integer]))
+
+       (define-unit u (import) (export a^) (define a 5))
+       (define-unit v (import a^) (export) a)
+
+       (invoke-unit/infer (link u v)))
+     -Integer]
+
+    ;; unit-from-context and define-unit-from-context tests
+    [tc-e
+     (let ()
+       (define-signature a^ ([a : Integer]))
+       (define a 17)
+       (define-unit u (import a^) (export) a)
+       (define-unit-from-context v a^)
+       (define w (compound-unit/infer (import) (export) (link v u)))
+       (invoke-unit w))
+     -Integer]
+
+    [tc-e
+     (let ()
+       (define-signature a^ ([a : Integer]))
+       (define a 17)
+       (define-unit u (import a^) (export) a)
+       (define-unit-from-context v a^)
+       (invoke-unit/infer (link v u)))
+     -Integer]
+
+    [tc-e
+     (let ()
+       (define-signature a^ ([a : Integer]))
+       (define a 17)
+       (define u (unit-from-context a^))
+       (define v (unit (import a^) (export) a))
+       (invoke-unit
+        (compound-unit
+         (import)
+         (export)
+         (link (([A : a^]) u)
+               (() v A)))
+        (import)))
+     -Integer]
+
+    ;; Make sure body annotations for exports are checked
+    [tc-err
+     (let ()
+       (define-signature a^ ([a : Integer]))
+       (unit
+         (import)
+         (export a^)
+         (: a String)
+         (define a 5))
+       (error ""))]
+    ;; and for non-exports as well
+    [tc-err
+     (let ()
+       (define-signature a^ ([a : Integer]))
+       (unit
+         (import)
+         (export a^)
+         (: b String)
+         (define b 12)
+         (define a 5))
+       (error ""))]
+
+   ;; init-depends type errors with compound-unit/define-compound-unit
+   [tc-err
+    (let ()
+      (define-signature a ())
+      (define-signature aa extends a ())
+      (define-unit u1
+        (import )
+        (export aa))
+      (define-unit u2
+        (import a)
+        (export)
+        (init-depend a))
+      (define-unit u3
+        (import)
+        (export aa))
+      (compound-unit
+       (import [A1 : a])
+       (export)
+       (link
+        (([A2 : a]) u1 )
+        (() u2 A)
+        (([A : aa]) u3)))
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (define-signature a ())
+      (define-unit u1
+        (import )
+        (export a))
+      (define-unit u2
+        (import a)
+        (export)
+        (init-depend a))
+      (define-unit u3
+        (import)
+        (export a))
+      (compound-unit
+       (import [A1 : a])
+       (export)
+       (link
+        (([A2 : a]) u1 )
+        (() u2 A)
+        (([A : a]) u3)))
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (define-signature a ())
+      (define-signature aa extends a ())
+      (define-unit u1
+        (import )
+        (export aa))
+      (define-unit u2
+        (import aa)
+        (export))
+      (define-unit u3
+        (import)
+        (export))
+      (compound-unit
+       (import)
+       (export)
+       (link
+        (([A : a]) u1 )
+        (() u2 A)))
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (define-signature a ())
+      (define-unit u1
+        (import )
+        (export a))
+      (define-unit u2
+        (import a)
+        (export)
+        (init-depend a))
+      (define-unit u3
+        (import)
+        (export a))
+      (define-compound-unit w
+        (import [A1 : a])
+        (export)
+        (link
+         (([A2 : a]) u1 )
+         (() u2 A)
+         (([A : a]) u3)))
+      (error ""))]
+
+   ;; inference
+   [tc-err
+    (let ()
+      (invoke-unit/infer 1)
+      (error ""))]
+
+   [tc-err 
+    (let ()
+      (compound-unit (import) (export) (link (() 1)))
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (compound-unit (import) (export)
+                     (link (() (unit (import x-sig) (export)))))
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (compound-unit (import) (export)
+                     (link (([X : x-sig]) (unit (import) (export)))))
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (invoke-unit 1)
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (define-signature x-sig ([x : Integer]))
+      (invoke-unit (unit (import x-sig) (export) x))
+      (error ""))]
+
+   [tc-err
+    (let ()
+      (define-signature x^ ([x : String]))
+      (unit (import x^) (export)
+        (: y Integer)
+        (define y x)
+        y)
+      (error ""))]
+   
+   ;; Type mismatch in unit body
+   [tc-err
+    (let ()  
+      (unit (import) (export)
+        (: x String)
+        (define x 5))
+      (error ""))]
+   [tc-err
+    (let ()
+      (define-signature a^ ([a : String]))
+      (unit (import) (export a^) (define a 5))
+      (error ""))]
+   [tc-err
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (define a "foo")
+      (invoke-unit (unit (import a^) (export) a) (import a^))
+      (error ""))]
+   [tc-err
+    (let ()
+      (define-signature a^ ([a : Integer]))
+      (unit
+        (import a^)
+        (export)
+        (: x String)
+        (define x a))
+      (error ""))]
+   ;; units can only import/export distinct sets of signatures
+   [tc-err
+    (let ()
+      (define-signature a^ ())
+      (define-signature b^ extends a^ ())
+      (define-siganture c^ extends a^ ())
+      (unit (import b^ c^) (export))
+      (error ""))]
+
+   ;; invoking a unit which imports a locally defined signature is a type error
+   ;; even if it is invoked with an import of the same name
+   [tc-err
+    (let ()
+      (define-signature bad^ ())
+      (define bad
+        (let ()
+          (define-signature bad^ ())
+          (unit (import bad^) (export))))
+      (invoke-unit bad (import bad^))
+      (error ""))]
+   
+   ;; This tests that the linking clauses in compound-unit forms
+   ;; are correctly satisfied
+   ;; This is fairly subtle, and the type mismatch error
+   ;; message doesn't make it obvious why it fails to typecheck
+   [tc-err
+    (let ()
+      (define-signature a^ ())
+       
+      (define-unit a1
+        (import)
+        (export a^))
+       
+      (define-unit a2
+        (import)
+        (export a^))
+       
+      (define-unit u
+        (import a^)
+        (export)
+        (init-depend a^))
+       
+      (define-compound-unit w
+        (import)
+        (export)
+        (link
+         (([A1 : a^]) a1)
+         (() u A2)
+         (([A2 : a^]) a2)))
+      (error ""))]))
+

typed-racket-test/xfail/fact-unit.rkt

@@ -0,0 +1,18 @@
+#lang typed/racket
+
+;; It would be nice if this program could typecheck, but because the types
+;; of unannotated exports are not added to the type environment the type
+;; the fact function is not inferred correctly. Adding a type annotation
+;; to fact allows this program to run.
+
+(define-signature fact^
+  ([fact : (-> Integer Integer)]))
+
+(define-unit fact@
+  (import (prefix i: fact^))
+  (export fact^)
+  (define (fact n) 
+    (if (< n 1) 
+        1
+        (* n (i:fact (sub1 n)))))
+  fact)