diff --git a/racket/typed/syndicate/core-expressions.rkt b/racket/typed/syndicate/core-expressions.rkt
index bc92162..3c04791 100644
--- a/racket/typed/syndicate/core-expressions.rkt
+++ b/racket/typed/syndicate/core-expressions.rkt
@@ -264,8 +264,15 @@
        (quasisyntax/loc pat
          (tuple #,@(stx-map elaborate-pattern #'(p ...))))]
       [(~constructor-exp ctor p ...)
+       (define field-tys (ctor-field-tys #'ctor))
+       (define sub-pats
+         (for/list ([field-pat (in-syntax #'(p ...))]
+                    [field-ty? (in-list field-tys)])
+           (if field-ty?
+               (elaborate-pattern/with-type field-pat field-ty?)
+               (elaborate-pattern field-pat))))
        (quasisyntax/loc pat
-         (ctor #,@(stx-map elaborate-pattern #'(p ...))))]
+         (ctor #,@sub-pats))]
       [e:expr
        #'e]))
 
diff --git a/racket/typed/syndicate/core-types.rkt b/racket/typed/syndicate/core-types.rkt
index 4684ade..b98f344 100644
--- a/racket/typed/syndicate/core-types.rkt
+++ b/racket/typed/syndicate/core-types.rkt
@@ -663,7 +663,18 @@
     (pattern (~seq #:type-constructor TypeCons:id))
     (pattern (~seq) #:attr TypeCons #f))
 
-  (struct user-ctor (typed-ctor untyped-ctor type-tag type-ctor field-ids)
+  (define-syntax-class slot-decl
+    #:attributes (name type)
+    (pattern name:id #:attr type #f)
+    (pattern [name:id (~optional (~datum :)) type]))
+
+  ;; typed-ctor   : ID; the name of function implementing the type rule
+  ;; untyped-ctor : ID; the name of the constructor for the (run time) struct
+  ;; type-tag     : ID; a unique tag for instances of this type
+  ;; type-ctor    : ID: the name of the type constructor for instances of this struct
+  ;; field-ids    : (Listof ID): the names of each field accessor
+  ;; field-tys    : (Listof (U #f Syntax)): the default type (serialized) of each field, if known
+  (struct user-ctor (typed-ctor untyped-ctor type-tag type-ctor field-ids field-tys)
     #:property prop:procedure
     (lambda (v stx)
       (define transformer (user-ctor-typed-ctor v))
@@ -675,11 +686,11 @@
 (define-syntax (define-constructor* stx)
   (syntax-parse stx
     #:datum-literals (:)
-    [(_ (Cons:id : TyCons:id slot:id ...) clause ...)
+    [(_ (Cons:id : TyCons:id slot:slot-decl ...) clause ...)
      #'(define-constructor (Cons slot ...)
          #:type-constructor TyCons
          clause ...)]
-    [(_ (Cons:id slot:id ...) clause ...)
+    [(_ (Cons:id slot:slot-decl ...) clause ...)
      #:with TyCons ((current-type-constructor-convention) #'Cons)
      (syntax/loc stx
        (define-constructor (Cons slot ...)
@@ -711,7 +722,7 @@
 
 (define-syntax (define-constructor stx)
   (syntax-parse stx
-    [(_ (Cons:id slot:id ...)
+    [(_ (Cons:id slot:slot-decl ...)
         ty-cons:type-constructor-decl
         (~seq #:with
               Alias AliasBody) ...)
@@ -721,14 +732,18 @@
      #:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)
      #:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)
      #:with (StructName Cons- type-tag) (generate-temporaries #'(Cons Cons Cons))
-     #:with (accessor ...) (for/list ([slot-name (in-syntax #'(slot ...))])
+     #:with (accessor ...) (for/list ([slot-name (in-syntax #'(slot.name ...))])
                              (format-id slot-name "~a-~a" #'Cons slot-name))
-     #:with (accessor- ...) (for/list ([slot-name (in-syntax #'(slot ...))])
+     #:with (accessor- ...) (for/list ([slot-name (in-syntax #'(slot.name ...))])
                               (format-id #'StructName "~a-~a" #'StructName slot-name))
-     #:with (acc-defs ...) (mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot ...))
+     #:with (acc-defs ...) (mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot.name ...))
+     #:with (field-ty? ...) (for/list ([ty? (in-list (attribute slot.type))])
+                              (if ty?
+                                  (serialize-syntax (type-eval ty?))
+                                  #'#f))
      (define arity (stx-length #'(slot ...)))
      #`(begin-
-         (struct- StructName (slot ...) #:reflection-name 'Cons #:transparent)
+         (struct- StructName (slot.name ...) #:reflection-name 'Cons #:transparent)
          (define-for-syntax (TypeConsExtraInfo stx)
            (list #'type-tag #'MakeTypeCons #'GetTypeParams))
          (define-product-type TypeCons
@@ -739,9 +754,14 @@
          (define-syntax MakeTypeCons (mk-ctor-rewriter #'TypeCons))
          (define-syntax GetTypeParams (mk-type-params-fetcher #'TypeCons))
          (define-syntax Cons
-           (user-ctor #'Cons- #'StructName 'type-tag #'TypeCons (list #'accessor ...)))
+           (user-ctor #'Cons-
+                      #'StructName
+                      'type-tag
+                      #'TypeCons
+                      (list #'accessor ...)
+                      (list #'field-ty? ...)))
          (define-syntax Cons- (mk-constructor-type-rule #,arity #'StructName #'TypeCons))
-         #,@(mk-accessors #'(accessor ...) #'(accessor- ...) #'TypeCons #'(slot ...)))]))
+         acc-defs ...)]))
 
 (define-for-syntax (mk-accessors accessors accessors- TypeCons slots)
   (for/list ([accessor (in-syntax accessors)]
@@ -750,13 +770,16 @@
     (quasisyntax/loc TypeCons
       (define-typed-variable-rename+ #,accessor ≫ #,accessor- : (∀+ #,slots (→fn (#,TypeCons #,@slots) #,slot))))))
 
-(define-for-syntax ((define-struct-accs accs/rev TypeCons lib) stx)
+(define-for-syntax ((define-struct-accs accs/rev field-accs? TypeCons lib) stx)
   (syntax-parse stx
     [(_ ucons:id)
-     (define accs (cleanup-accs #'ucons accs/rev))
-     (define accs- (map mk-- accs))
+     (define cleaned-accs (cleanup-accs #'ucons accs/rev))
+     (define accs (if (empty? field-accs?)
+                      cleaned-accs
+                      (format-all #'ucons field-accs?)))
+     (define accs- (map mk-- cleaned-accs))
      (define slots (generate-temporaries accs))
-     (define renames (for/list ([acc (in-list accs)]
+     (define renames (for/list ([acc (in-list cleaned-accs)]
                                 [acc- (in-list accs-)])
                        #`[#,acc #,acc-]))
      (quasisyntax/loc TypeCons
@@ -764,10 +787,13 @@
          (require- (only-in- #,lib #,@renames))
          #,@(mk-accessors accs accs- TypeCons slots)))]))
 
-(define-for-syntax (cleanup-accs ucons accs/rev)
-  (for/list ([acc (in-list (reverse accs/rev))])
+(define-for-syntax (format-all ucons accs)
+  (for/list ([acc (in-list accs)])
     (format-id ucons "~a" (syntax-e acc))))
 
+(define-for-syntax (cleanup-accs ucons accs/rev)
+  (format-all ucons (reverse accs/rev)))
+
 ;; (require-struct chicken #:as Chicken #:from "some-mod.rkt") will
 ;;  - extract the struct-info for chicken, and ensure that it is immutable, has a set number of fields
 ;;  - determine the number of slots, N, chicken has
@@ -777,34 +803,66 @@
 ;; TODO: this implementation shares a lot with that of define-constructor
 (define-syntax (require-struct stx)
   (syntax-parse stx
-    [(_ ucons:id #:as ty-cons:id #:from lib (~optional (~and omit-accs #:omit-accs)))
+    [(_ ucons:id #:as ty-cons:id #:from lib
+        (~optional (~seq slot:slot-decl ...))
+        (~optional (~and omit-accs #:omit-accs)))
      ;; TBH I'm not sure why I don't need to SLIAB TypeCons and Cons-
-     (with-syntax* ([TypeCons #'ty-cons]
-                    [MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)]
-                    [GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)]
-                    [TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)]
-                    [TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)]
-                    [Cons- (format-id #'ucons "~a/checked" #'ucons)]
-                    [orig-struct-info (generate-temporary #'ucons)]
-                    [type-tag (generate-temporary #'ucons)])
-       (quasisyntax/loc stx
-         (begin-
-           (require- (only-in- lib [ucons orig-struct-info]))
-           (begin-for-syntax
-             (define info (syntax-local-value #'orig-struct-info))
-             (unless (struct-info? info)
-               (raise-syntax-error #f "expected struct" #'#,stx #'ucons))
-             (match-define (list desc cons pred accs/rev muts sup) (extract-struct-info info))
-             (when (and (cons? accs/rev) (false? (last accs/rev)))
-               (raise-syntax-error #f "number of slots must be exact" #'#,stx #'ucons))
-             (unless (boolean? sup)
-               (raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons))
-             (define arity (length accs/rev))
-             )
-           (define-syntax finish-type-defs
-             (finish-require-struct-typedef #'lib #'Cons- #'TypeConsExtraInfo #'type-tag #'MakeTypeCons #'GetTypeParams #'orig-struct-info #'accs/rev arity #,(attribute omit-accs)))
-           (finish-type-defs ucons TypeCons)
-           )))]))
+     #:with TypeCons #'ty-cons
+     #:with MakeTypeCons (format-id #'TypeCons "make-~a" #'TypeCons)
+     #:with GetTypeParams (format-id #'TypeCons "get-~a-type-params" #'TypeCons)
+     #:with TypeConsExpander (format-id #'TypeCons "~~~a" #'TypeCons)
+     #:with TypeConsExtraInfo (format-id #'TypeCons "~a-extra-info" #'TypeCons)
+     #:with Cons- (format-id #'ucons "~a/checked" #'ucons)
+     #:with orig-struct-info (generate-temporary #'ucons)
+     #:with type-tag (generate-temporary #'ucons)
+     #:with (field-ty? ...) (for/list ([ty? (in-list (attribute slot.type))])
+                              (if ty?
+                                  #`#,(serialize-syntax (type-eval ty?))
+                                  #f))
+     #:with (field-acc ...) (for/list ([name? (in-list (attribute slot.name))])
+                              (if name?
+                                  (format-id #'ucons "~a-~a" #'ucons name?)
+                                  #f))
+     (quasisyntax/loc stx
+       (begin-
+         (require- (only-in- lib [ucons orig-struct-info]))
+         (begin-for-syntax
+           (define info (syntax-local-value #'orig-struct-info))
+           (unless (struct-info? info)
+             (raise-syntax-error #f "expected struct" #'#,stx #'ucons))
+           (match-define (list desc cons pred accs/rev muts sup) (extract-struct-info info))
+           (when (and (cons? accs/rev) (false? (last accs/rev)))
+             (raise-syntax-error #f "number of slots must be exact" #'#,stx #'ucons))
+           (unless (boolean? sup)
+             (raise-syntax-error #f "structs with super-type not supported" #'#,stx #'ucons))
+           (define arity (length accs/rev))
+           (define field-tys (list #'field-ty? ...))
+           (define field-accs? (list #'field-acc ...))
+           (define slots-given (length field-tys))
+           (unless (or (zero? slots-given)
+                       (equal? slots-given arity))
+             (raise-syntax-error
+              #f
+              (format "incorrect number of slots specified, given ~a expected ~a" slots-given arity)
+              #'#,stx
+              #'(slot ...)))
+           )
+         (define-syntax finish-type-defs
+           (finish-require-struct-typedef #'lib
+                                          #'Cons-
+                                          #'TypeConsExtraInfo
+                                          #'type-tag
+                                          #'MakeTypeCons
+                                          #'GetTypeParams
+                                          #'orig-struct-info
+                                          #'accs/rev
+                                          arity
+                                          #,(attribute omit-accs)
+                                          #'field-tys
+                                          #'field-accs?
+                                          #;(list #'field-acc ...)))
+         (finish-type-defs ucons TypeCons)
+         ))]))
 
 ;; This is so that the arity of the struct can be included in the generated typedef
 (define-for-syntax ((finish-require-struct-typedef lib
@@ -816,10 +874,15 @@
                                                    orig-struct-info
                                                    accs/rev
                                                    arity
-                                                   omit-accs?)
+                                                   omit-accs?
+                                                   field-tys
+                                                   field-accs?)
                     stx)
   (syntax-parse stx
     [(_ ucons:id TypeCons:id)
+     #:with field-accs #`(if (empty? #,field-accs?)
+                             (cleanup-accs #'ucons #,accs/rev)
+                             (format-all #'ucons #,field-accs?))
      (quasisyntax/loc #'ucons
        (begin-
          (define-for-syntax (#,TypeConsExtraInfo stx)
@@ -832,12 +895,17 @@
          (define-syntax #,GetTypeParams (mk-type-params-fetcher #'TypeCons))
          (define-syntax #,Cons- (mk-constructor-type-rule #,arity #'#,orig-struct-info #'TypeCons))
          (define-syntax ucons
-           (user-ctor #'#,Cons- #'#,orig-struct-info '#,type-tag #'TypeCons (cleanup-accs #'ucons #,accs/rev)))
+           (user-ctor #'#,Cons-
+                      #'#,orig-struct-info
+                      '#,type-tag
+                      #'TypeCons
+                      field-accs
+                      #,field-tys))
          #,(unless omit-accs?
              (quasisyntax/loc #'ucons
                (begin-
                  (define-syntax mk-struct-accs
-                   (define-struct-accs #,accs/rev #'TypeCons #'#,lib))
+                   (define-struct-accs #,accs/rev #,field-accs? #'TypeCons #'#,lib))
                  (mk-struct-accs ucons))))))]))
 
 (begin-for-syntax
@@ -900,7 +968,15 @@
   ;; requires (ctor-id? stx)
   ;; fetch the type tag
   (define (ctor-type-tag stx)
-    (user-ctor-type-tag (syntax-local-value stx (const #f)))))
+    (user-ctor-type-tag (syntax-local-value stx (const #f))))
+
+  ;; requires (ctor-id? stx)
+  ;; fetch the field types
+  (define (ctor-field-tys stx)
+    (define tys (user-ctor-field-tys (syntax-local-value stx (const #f))))
+    (for/list ([ty? (in-list tys)])
+      (and ty? (deserialize-syntax ty?))))
+  )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Require & Provide
@@ -922,9 +998,13 @@
 
   (define-syntax-class struct-require-clause
     #:datum-literals (:)
-    #:attributes (Cons TyCons omit-accs)
-    (pattern [#:struct Cons:id #:as TyCons:id (~optional (~and omit-accs #:omit-accs))])
-    (pattern [#:struct Cons:id (~optional (~and omit-accs #:omit-accs))]
+    #:attributes (Cons TyCons omit-accs [slot 1] [slot.name 1] [slot.type 1])
+    (pattern [#:struct Cons:id #:as TyCons:id
+              (~optional (~seq slot:slot-decl ...))
+              (~optional (~and omit-accs #:omit-accs))])
+    (pattern [#:struct Cons:id
+              (~optional (~seq slot:slot-decl ...))
+              (~optional (~and omit-accs #:omit-accs))]
              #:attr TyCons ((current-type-constructor-convention) #'Cons)))
   )
 
@@ -941,7 +1021,10 @@
      #:with (name- ...) (format-ids "~a-" #'(name ...))
      (syntax/loc stx
        (begin-
-         (require-struct struct-clause.Cons #:as struct-clause.TyCons #:from lib (~? struct-clause.omit-accs)) ...
+         (require-struct struct-clause.Cons #:as struct-clause.TyCons
+                         #:from lib
+                         (~? (~@ struct-clause.slot ...))
+                         (~? struct-clause.omit-accs)) ...
          opaque-clause.type-definition ...
          (require (only-in lib [name name-] ...))
          (define-syntax name
diff --git a/racket/typed/syndicate/roles.rkt b/racket/typed/syndicate/roles.rkt
index fd9b8d8..90a9117 100644
--- a/racket/typed/syndicate/roles.rkt
+++ b/racket/typed/syndicate/roles.rkt
@@ -386,7 +386,7 @@
                  "expected exactly one Role for body"
   #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-f ...))
   #:fail-unless (<: #'τ-o #'τ-c.norm)
-                (format "Outputs ~a not valid in dataspace ~a" (make-output-error-message #'τ-o #'τ-c.norm) (type->str #'τ-c.norm))
+                (format "Outputs ~a not valid in dataspace ~a" (make-output-error-message #'τ-o #'τ-c.norm) (type->strX #'τ-c.norm))
   #:with τ-final #;(mk-Actor- #'(τ-c.norm)) (mk-ActorWithRole- #'(τ-c.norm τ-f ...))
   #:fail-unless (<: #'τ-a #'τ-final)
                 "Spawned actors not valid in dataspace"
@@ -402,11 +402,33 @@
    #:do [(define τc (current-communication-type))]
    #:when τc
    ----------------------------------------
-   [≻ (spawn #,τc s)]])
+   [≻ (spawn #,τc s)]]
+  [(spawn s) ≫
+   [⊢ (block s) ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs)) (⇒ ν-f (~effs τ-f ...))]
+   ;; TODO: s shouldn't refer to facets or fields!
+   #:fail-unless (and (stx-andmap Role? #'(τ-f ...))
+                      (= 1 (length (syntax->list #'(τ-f ...)))))
+   "expected exactly one Role for body"
+   #:with (τ-i τ-o τ-i/i τ-o/i τ-a) (analyze-roles #'(τ-f ...))
+   #:fail-unless (project-safe? (∩ (strip-? #'τ-o/i) #'τ-o/i) #'τ-i/i)
+                 (string-append "Not prepared to handle internal events:\n" (make-actor-error-message #'τ-i/i #'τ-o/i #'τ-o/i))
+  #:with τ-i/o (pattern-matching-assertions #'τ-i)
+  #:with (~U* (~AnyActor τ-c/spawned) ...) #'τ-a
+  #:with τ-c/this-actor (type-eval #'(U τ-i/o τ-o))
+  #:with τ-c/final (type-eval #'(U τ-c/this-actor τ-c/spawned ...))
+  #:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c/final)
+                               #'τ-i)
+                (string-append "Not prepared to handle inputs:\n" (make-actor-error-message #'τ-i #'τ-o #'τ-c/final))
+  #:with τ-final (mk-ActorWithRole- #'(τ-c/final τ-f ...))
+  #:fail-unless (<: #'τ-a #'τ-final)
+                "Spawned actors not valid in dataspace"
+  ----------------------------------------
+  [⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
+                                               (⇒ ν-s (τ-final))]])
 
 ;; (Listof Type) -> String
 (define-for-syntax (tys->str tys)
-  (string-join (map type->str tys) ",\n"))
+  (string-join (map type->strX tys) ",\n"))
 
 ;; Type Type -> String
 (define-for-syntax (make-output-error-message τ-o τ-c)
@@ -425,11 +447,12 @@
 
 ;; Type Type Type -> String
 (define-for-syntax (make-actor-error-message τ-i τ-o τ-c)
-  (define mismatches (find-surprising-inputs τ-i τ-o τ-c))
+  (define mismatches (find-surprising-inputs τ-i τ-o τ-c
+                                             (lambda (t1 t2) (not (project-safe? t1 t2)))))
   (tys->str mismatches))
 
 ;; Type Type Type -> (Listof Type)
-(define-for-syntax (find-surprising-inputs τ-i τ-o τ-c)
+(define-for-syntax (find-surprising-inputs τ-i τ-o τ-c surprising?)
   (define incoming (∩ (strip-? τ-o) τ-c))
   ;; Type -> (Listof Type)
   (let loop ([ty incoming])
@@ -438,44 +461,56 @@
        (apply append (map loop (syntax->list #'(τ ...))))]
       [_
        (cond
-         [(project-safe? ty τ-i)
-          '()]
+         [(surprising? ty τ-i)
+          (list ty)]
          [else
-          (list ty)])])))
+          (list)])])))
 
-(define-typed-syntax (dataspace τ-c:type s ...) ≫
-  #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
-  #:mode (communication-type-mode #'τ-c.norm)
-    [
-     [⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
-    ]
-  #:with τ-actor (mk-Actor- #'(τ-c.norm))
-  #:do [(define errs (for/list ([t (in-syntax #'(τ-s ... ...))]
-                                #:unless (<: t #'τ-actor))
-                       t))]
-  #:fail-unless (empty? errs) (make-dataspace-error-message errs #'τ-c.norm)
-  ;; #:fail-unless (stx-andmap (lambda (t) (<: t #'τ-actor)) #'(τ-s ... ...))
-  ;;               "Not all actors conform to communication type"
-  #:with τ-ds-i (strip-inbound #'τ-c.norm)
-  #:with τ-ds-o (strip-outbound #'τ-c.norm)
-  #:with τ-relay (relay-interests #'τ-c.norm)
-  #:with τ-ds-act (mk-Actor- (list (mk-U*- #'(τ-ds-i τ-ds-o τ-relay))))
-  -----------------------------------------------------------------------------------
-  [⊢ (syndicate:dataspace s- ...) (⇒ : ★/t)
-                                  (⇒ ν-s (τ-ds-act))])
+(define-typed-syntax dataspace
+  [(dataspace τ-c:type s ...) ≫
+   #:cut
+   #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
+   #:mode (communication-type-mode #'τ-c.norm)
+     [
+      [⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
+     ]
+   #:with τ-actor (mk-Actor- #'(τ-c.norm))
+   #:do [(define errs (for/list ([t (in-syntax #'(τ-s ... ...))]
+                                 #:unless (<: t #'τ-actor))
+                        t))]
+   #:fail-unless (empty? errs) (make-dataspace-error-message errs #'τ-c.norm)
+   ;; #:fail-unless (stx-andmap (lambda (t) (<: t #'τ-actor)) #'(τ-s ... ...))
+   ;;               "Not all actors conform to communication type"
+   #:with τ-ds-i (strip-inbound #'τ-c.norm)
+   #:with τ-ds-o (strip-outbound #'τ-c.norm)
+   #:with τ-relay (relay-interests #'τ-c.norm)
+   #:with τ-ds-act (mk-Actor- (list (mk-U*- #'(τ-ds-i τ-ds-o τ-relay))))
+   -----------------------------------------------------------------------------------
+   [⊢ (syndicate:dataspace s- ...) (⇒ : ★/t)
+                                   (⇒ ν-s (τ-ds-act))]]
+  [(dataspace s ...) ≫
+   [⊢ s ≫ s- (⇒ ν-ep (~effs)) (⇒ ν-s (~effs τ-s ...)) (⇒ ν-f (~effs))] ...
+   #:cut
+   #:with ((~AnyActor τc/spawned) ...) #'(τ-s ... ...)
+   #:with τc (type-eval #'(U τc/spawned ...))
+   -----------------------------------------------------------------------------------
+   [≻ (dataspace τc s- ...)]])
 
 ;; (Listof Type) Type -> String
 (define-for-syntax (make-dataspace-error-message errs tc)
   (with-output-to-string
     (lambda ()
-      (printf "Not all actors conform to communication type; found the following mismatches:\n")
+      (printf "Not all actors conform to communication type:\n")
+      (pretty-display (type->strX tc))
+      (printf "found the following mismatches:\n")
       (for ([err (in-list errs)])
         (syntax-parse err
           [(~AnyActor τ)
-           (printf "Actor with communication type ~a:\n" (type->str #'τ))
+           (printf "Actor with communication type ~a:\n" (type->strX #'τ))
            (cond
              [(<: #'τ tc)
-              (define msg (make-actor-error-message #'τ #'τ tc))
+              (define mismatches (find-surprising-inputs #'τ #'τ tc (lambda (t1 t2) (not (<: t1 t2)))))
+              (define msg (tys->str mismatches))
               (printf "  unprepared to handle inputs: ~a\n" msg)]
              [else
               (define msg (make-output-error-message #'τ tc))
@@ -666,17 +701,26 @@
 
 ;; n.b. this is a blocking operation, so an actor that uses this internally
 ;; won't necessarily terminate.
-(define-typed-syntax (run-ground-dataspace τ-c:type s ...) ≫
-  ;;#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
-  #:mode (communication-type-mode #'τ-c.norm)
-  [
+(define-typed-syntax run-ground-dataspace
+  [(run-ground-dataspace τ-c:type s ...) ≫
+   ;;#:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
+   #:mode (communication-type-mode #'τ-c.norm)
+   [
+    [⊢ s ≫ s- (⇒ : t1)] ...
+    [⊢ (dataspace τ-c.norm s- ...) ≫ _ (⇒ : t2)]
+   ]
+   #:with τ-out (strip-outbound #'τ-c.norm)
+   -----------------------------------------------------------------------------------
+   [⊢ (#%app- syndicate:run-ground (#%app- syndicate:capture-actor-actions (lambda- () (#%app- list- s- ...))))
+      (⇒ : (AssertionSet τ-out))]]
+  [(run-ground-dataspace s ...) ≫
    [⊢ s ≫ s- (⇒ : t1)] ...
-   [⊢ (dataspace τ-c.norm s- ...) ≫ _ (⇒ : t2)]
-  ]
-  #:with τ-out (strip-outbound #'τ-c.norm)
-  -----------------------------------------------------------------------------------
-  [⊢ (#%app- syndicate:run-ground (#%app- syndicate:capture-actor-actions (lambda- () (#%app- list- s- ...))))
-     (⇒ : (AssertionSet τ-out))])
+   [⊢ (dataspace s- ...) ≫ _ (⇒ : t2)]
+   #:with τ-out (strip-outbound #'τ-c.norm)
+   -----------------------------------------------------------------------------------
+   [⊢ (#%app- syndicate:run-ground (#%app- syndicate:capture-actor-actions (lambda- () (#%app- list- s- ...))))
+      (⇒ : (AssertionSet τ-out))]
+   ])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Utilities
diff --git a/racket/typed/tests/removing-annotations.rkt b/racket/typed/tests/removing-annotations.rkt
new file mode 100644
index 0000000..6eb27ff
--- /dev/null
+++ b/racket/typed/tests/removing-annotations.rkt
@@ -0,0 +1,41 @@
+#lang typed/syndicate
+
+(require rackunit/turnstile)
+
+(define-constructor* (run [distance : Int] [windy? : Bool]))
+
+(check-type
+ (spawn
+  (start-facet runner
+    (assert (run 5 #t))))
+ : ★/t)
+
+(check-type
+ (spawn
+  (start-facet longer
+    (on (asserted (run $d $w?))
+        (printf "run ~a ~a\n" (add1 d) (if w? "brr" "")))))
+ : ★/t)
+
+(check-type
+ (dataspace
+  (spawn
+   (start-facet runner
+                (assert (run 5 #t))))
+  (spawn
+   (start-facet longer
+                (on (asserted (run $d $w?))
+                    (printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
+ : ★/t)
+
+(typecheck-fail
+ (dataspace
+  (spawn
+   (start-facet runner
+                ;; NB
+                (assert (run "FAR" #t))))
+  (spawn
+   (start-facet longer
+                (on (asserted (run $d $w?))
+                    (printf "run ~a ~a\n" (add1 d) (if w? "brr" ""))))))
+ #:verb-msg "unprepared to handle inputs: (RunT String Bool)")
diff --git a/racket/typed/tests/require-struct.rkt b/racket/typed/tests/require-struct.rkt
new file mode 100644
index 0000000..a4ab7d6
--- /dev/null
+++ b/racket/typed/tests/require-struct.rkt
@@ -0,0 +1,12 @@
+#lang typed/syndicate
+
+(require rackunit/turnstile)
+
+(require/typed "struct-provider.rkt"
+  [#:struct donkey [weight : Int] [grey? : Bool]])
+
+(check-type (donkey 5 #t)
+            : (DonkeyT Int Bool))
+
+(check-type (donkey-grey? (donkey 5 #t))
+            : Bool)
diff --git a/racket/typed/tests/struct-provider.rkt b/racket/typed/tests/struct-provider.rkt
new file mode 100644
index 0000000..557301b
--- /dev/null
+++ b/racket/typed/tests/struct-provider.rkt
@@ -0,0 +1,5 @@
+#lang racket
+
+(struct donkey (weight stubborn?) #:transparent)
+
+(provide (struct-out donkey))