From 7287658d64724ce2b7331eefdc4302fdeccbff7b Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 20 Apr 2022 11:43:39 -0400
Subject: [PATCH 01/16] wip

---
 .../typed-racket/base-env/prims-struct.rkt    |   8 +-
 .../private/syntax-properties.rkt             |   1 +
 .../typed-racket/rep/type-rep.rkt             |   7 +-
 .../typed-racket/typecheck/tc-structs.rkt     | 178 ++++++++++--------
 typed-racket-test/succeed/struct-props.rkt    |   2 -
 5 files changed, 108 insertions(+), 88 deletions(-)

diff --git a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
index 4dbd7384d..abf87762d 100644
--- a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
+++ b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
@@ -102,13 +102,15 @@
                                ([val (attribute prop-val)]
                                 [name (attribute prop)])
                        (cond
-                         [(free-identifier=? name #'prop:procedure)
+                         [(or (free-identifier=? name #'prop:procedure)
+                              (free-identifier=? name #'prop:evt))
                           (define tname (or (attribute type) st-name))
                           (define sty-stx (if (null? type-vars)
                                               tname
                                               (quasisyntax/loc tname
                                                 (#,tname #,@type-vars))))
-                          (maybe-extract-prop-proc-ty-ann sty-stx val)]
+                          (define-values (val^ ty^) (maybe-extract-prop-proc-ty-ann sty-stx val))
+                          (values val^ (assoc-struct-property-name-property ty^ name))]
                          [else (values val #f)])))]
              #:attr proc-ty (if (null? proc-tys) #f
                                 proc-tys)
@@ -200,7 +202,7 @@
 
 
 ;; This function tries to extract the type annotation on a lambda
-;; expression for prop:precedure.
+;; expression for prop:procedure.
 ;;
 ;; sty-stx: the syntax that represents a structure type. For a monomorhpic
 ;; structure type, sty-stx is the identifier for its name. For a polymorphic
diff --git a/typed-racket-lib/typed-racket/private/syntax-properties.rkt b/typed-racket-lib/typed-racket/private/syntax-properties.rkt
index ff753e9a6..4f7a3c470 100644
--- a/typed-racket-lib/typed-racket/private/syntax-properties.rkt
+++ b/typed-racket-lib/typed-racket/private/syntax-properties.rkt
@@ -61,6 +61,7 @@
   (type-inst type-inst)
   (row-inst row-inst)
   (st-proc-ty st-proc-ty)
+  (assoc-struct-property-name assoc-struct-property-name)
   (type-label type-label)
   (optional-non-immediate-arg optional-non-immediate-arg)
   (optional-immediate-arg optional-immediate-arg)
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 094a4b5cf..037af0466 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -806,8 +806,11 @@
 
 
 (define/cond-contract (Struct-proc* sty)
-  (-> Struct? (or/c #f Fun?))
-  (define b (Struct-proc sty))
+  (-> (or/c Poly? Struct?) (or/c #f Type?))
+  (define sty^ (match sty
+                 [(? Struct?) sty]
+                 [(Poly: _ (? Struct? sty)) sty]))
+  (define b (Struct-proc sty^))
   (and b (unbox b)))
 
 (define (make-Struct* name parent flds proc poly? pred-id properties)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 22fa3cb3a..d1f13396e 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -91,13 +91,6 @@
   (syntax-parse stx
     [t:typed-struct #'t.type-name]))
 
-;; a simple wrapper to get proc from a polymorphic or monomorhpic structure
-(define/cond-contract (get-struct-proc sty)
-  (c:-> (c:or/c Struct? Poly?) (c:or/c #f Fun?))
-  (Struct-proc (match sty
-                 [(? Struct?) sty]
-                 [(Poly: names (? Struct? sty)) sty])))
-
 
 (define/cond-contract (tc/struct-prop-values st-tname pnames pvals)
   (c:-> identifier? (c:listof identifier?) (c:listof syntax?) void?)
@@ -385,7 +378,7 @@
   (define st-type-alias (mk-type-alias type-name tvars))
   (define st-type-alias-maybe-with-proc
     (let ([maybe-proc-ty (and (or (Poly? sty) (Struct? sty))
-                              (get-struct-proc sty))])
+                              (Struct-proc sty))])
       (if maybe-proc-ty (intersect st-type-alias maybe-proc-ty)
           st-type-alias)) )
 
@@ -463,84 +456,107 @@
       (struct-names-type-name (parsed-struct-names parsed-struct))))
   (refine-variance! names stys tvarss))
 
+
+(define ((make-extract predicate mismatched-field-type-errors customized-proc property-lambda-rng-chck)
+         ty-stx st-name fld-names desc)
+  (syntax-parse ty-stx
+    #:literals (struct-field-index)
+    ;; a field index is provided
+    [n_:exact-nonnegative-integer
+     (define n (syntax-e #'n_))
+     (define max-idx (sub1 (length (struct-desc-self-fields desc))))
+     (unless (<= n max-idx)
+       (tc-error/fields
+        "index too large"
+        "index"
+        n
+        "maximum allowed index"
+        max-idx
+        #:stx ty-stx))
+     (define ty (list-ref (struct-desc-self-fields desc) n))
+     (unless (predicate ty)
+       (tc-error/fields
+        (format "field ~a is not a ~a" (syntax-e (list-ref fld-names n)) (car mismatched-field-type-errors))
+        "expected"
+        (cdr mismatched-field-type-errors)
+        "given"
+        ty
+        #:stx ty-stx))
+     ty]
+
+    ;; a field name is provided (via struct-field-index)
+    [(struct-field-index fld-nm:id)
+     (define idx (index-of fld-names #'fld-nm
+                           free-identifier=?))
+     ;; fld-nm must be valid, because invalid field names have been reported by
+     ;; struct-field-index at this point
+     (list-ref (struct-desc-self-fields desc) idx)]
+
+    [ty-stx:st-proc-ty^
+     #:do [(define ty (parse-type #'ty-stx))]
+     (match ty
+       [(Fun: (list arrs ...))
+        (make-Fun
+         (map (lambda (arr)
+                (Arrow-update
+                 arr
+                 dom
+                 rng
+                 (lambda (doms rng)
+                   (match (car doms)
+                     [(Name/simple: n)
+                      #:when (free-identifier=? n st-name)
+                      (void)]
+                     [(App: (Name/simple: rator) vars)
+                      #:when (free-identifier=? rator st-name)
+                      (void)]
+                     [(Univ:)
+                      (void)]
+                     [(or (Name/simple: (app syntax-e n)) n)
+                      (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
+                                       "expected" (syntax-e st-name)
+                                       "got" n
+                                       #:stx (st-proc-ty-property #'ty-stx))])
+                   (when property-lambda-rng-chck
+                     (property-lambda-rng-chck rng))
+                   (values (cdr doms) rng))))
+              arrs))]
+       [_
+        (tc-error/fields "type mismatch"
+                         "expected"
+                         "Procedure"
+                         "given"
+                         ty
+                         #:stx #'ty-stx)])]
+    [_
+     (customized-proc ty-stx)]))
+
+(define-syntax-rule (define-property-handling-table (name predicate msg-parts custimized-handling rng-chck) ...)
+  (make-immutable-free-id-table (list (cons name (make-extract predicate msg-parts custimized-handling rng-chck))
+                                      ...)))
+
+(define property-handling-table
+  (define-property-handling-table
+    (#'prop:procedure Fun? (cons "function" "Procedure")
+     (lambda (ty-stx)
+       (tc-error/stx ty-stx
+                     "expected: a nonnegative integer literal or an annotated lambda"))
+     #f)))
+
+
+
 ;; extract the type annotation of prop:procedure value
-(define/cond-contract (extract-proc-ty proc-ty-stx desc fld-names st-name)
+(define/cond-contract (extract-proc-ty proc-ty-stx-li desc fld-names st-name)
   (c:-> (c:listof syntax?) struct-desc? (c:listof identifier?) identifier? Type?)
 
-  (unless (equal? (length proc-ty-stx) 1)
+
+  (unless (equal? (length proc-ty-stx-li) 1)
     (tc-error "prop:procedure can only have one value assigned to it"))
 
-  (let ([proc-ty-stx (car proc-ty-stx)])
-    (syntax-parse proc-ty-stx
-      #:literals (struct-field-index)
-      ;; a field index is provided
-      [n_:exact-nonnegative-integer
-       (define n (syntax-e #'n_))
-       (define max-idx (sub1 (length (struct-desc-self-fields desc))))
-       (unless (<= n max-idx)
-         (tc-error/fields
-          "index too large"
-          "index"
-          n
-          "maximum allowed index"
-          max-idx
-          #:stx proc-ty-stx))
-       (define ty (list-ref (struct-desc-self-fields desc) n))
-       (unless (Fun? ty)
-         (tc-error/fields
-          (format "field ~a is not a function" (syntax-e (list-ref fld-names n)))
-          "expected"
-          "Procedure"
-          "given"
-          ty
-          #:stx proc-ty-stx))
-       ty]
-
-      ;; a field name is provided (via struct-field-index)
-      [(struct-field-index fld-nm:id)
-       (define idx (index-of fld-names #'fld-nm
-                             free-identifier=?))
-       ;; fld-nm must be valid, because invalid field names have been reported by
-       ;; struct-field-index at this point
-       (list-ref (struct-desc-self-fields desc) idx)]
-
-      [ty-stx:st-proc-ty^
-       #:do [(define ty (parse-type #'ty-stx))]
-       (match ty
-         [(Fun: (list arrs ...))
-          (make-Fun
-           (map (lambda (arr)
-                  (Arrow-update
-                   arr
-                   dom
-                   (lambda (doms)
-                     (match (car doms)
-                       [(Name/simple: n)
-                        #:when (free-identifier=? n st-name)
-                        (void)]
-                       [(App: (Name/simple: rator) vars)
-                        #:when (free-identifier=? rator st-name)
-                        (void)]
-                       [(Univ:)
-                        (void)]
-                       [(or (Name/simple: (app syntax-e n)) n)
-                        (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
-                                         "expected" (syntax-e st-name)
-                                         "got" n
-                                         #:stx (st-proc-ty-property #'ty-stx))])
-
-                     (cdr doms))))
-                arrs))]
-         [_
-          (tc-error/fields "type mismatch"
-                           "expected"
-                           "Procedure"
-                           "given"
-                           ty
-                           #:stx #'ty-stx)])]
-      [_
-       (tc-error/stx proc-ty-stx
-                     "expected: a nonnegative integer literal or an annotated lambda")])))
+  ;; fixme for/first -> for/list
+  (for/first ([proc-ty-stx (in-list proc-ty-stx-li)])
+    (define property-name (assoc-struct-property-name-property proc-ty-stx))
+    ((free-id-table-ref property-handling-table property-name) proc-ty-stx st-name fld-names desc)))
 
 ;; check and register types for a define struct
 ;; tc/struct : Listof[identifier] (U identifier (list identifier identifier))
diff --git a/typed-racket-test/succeed/struct-props.rkt b/typed-racket-test/succeed/struct-props.rkt
index 840023ad8..83c4c08da 100644
--- a/typed-racket-test/succeed/struct-props.rkt
+++ b/typed-racket-test/succeed/struct-props.rkt
@@ -21,8 +21,6 @@
   #:property prop:custom-write
   (lambda ([self : foo] [p : Output-Port] [m : (U Boolean 1 0)]) : Void
           (displayln (+ (foo-x self) 20) p))
-  #:property prop:evt 0
-
   #:property prop:custom-print-quotable 'always)
 
 (struct foobar^ foo ([y : Number])

From 5482ed76fa70f7a17892613936cff3545de517c5 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 20 Apr 2022 13:23:57 -0400
Subject: [PATCH 02/16] wip

---
 .../typed-racket/typecheck/tc-structs.rkt     | 54 ++++++++++++-------
 1 file changed, 36 insertions(+), 18 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index d1f13396e..79421d3f1 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -379,7 +379,8 @@
   (define st-type-alias-maybe-with-proc
     (let ([maybe-proc-ty (and (or (Poly? sty) (Struct? sty))
                               (Struct-proc sty))])
-      (if maybe-proc-ty (intersect st-type-alias maybe-proc-ty)
+      (if maybe-proc-ty
+          (intersect st-type-alias maybe-proc-ty)
           st-type-alias)) )
 
   ;; simple abstraction for handling field getters or setters
@@ -457,7 +458,7 @@
   (refine-variance! names stys tvarss))
 
 
-(define ((make-extract predicate mismatched-field-type-errors customized-proc property-lambda-rng-chck)
+(define ((make-extract check-field-type customized-proc check-doms-rng)
          ty-stx st-name fld-names desc)
   (syntax-parse ty-stx
     #:literals (struct-field-index)
@@ -474,15 +475,7 @@
         max-idx
         #:stx ty-stx))
      (define ty (list-ref (struct-desc-self-fields desc) n))
-     (unless (predicate ty)
-       (tc-error/fields
-        (format "field ~a is not a ~a" (syntax-e (list-ref fld-names n)) (car mismatched-field-type-errors))
-        "expected"
-        (cdr mismatched-field-type-errors)
-        "given"
-        ty
-        #:stx ty-stx))
-     ty]
+     (check-field-type ty-stx (list-ref fld-names n) ty)]
 
     ;; a field name is provided (via struct-field-index)
     [(struct-field-index fld-nm:id)
@@ -517,9 +510,9 @@
                                        "expected" (syntax-e st-name)
                                        "got" n
                                        #:stx (st-proc-ty-property #'ty-stx))])
-                   (when property-lambda-rng-chck
-                     (property-lambda-rng-chck rng))
-                   (values (cdr doms) rng))))
+                   (if check-doms-rng
+                       (check-doms-rng #'ty-stx (cdr doms) rng)
+                       (values (cdr doms) rng)))))
               arrs))]
        [_
         (tc-error/fields "type mismatch"
@@ -531,17 +524,42 @@
     [_
      (customized-proc ty-stx)]))
 
-(define-syntax-rule (define-property-handling-table (name predicate msg-parts custimized-handling rng-chck) ...)
-  (make-immutable-free-id-table (list (cons name (make-extract predicate msg-parts custimized-handling rng-chck))
+(define-syntax-rule (define-property-handling-table (name check-field-type custimized-handling rng-chck) ...)
+  (make-immutable-free-id-table (list (cons name (make-extract check-field-type custimized-handling rng-chck))
                                       ...)))
 
 (define property-handling-table
   (define-property-handling-table
-    (#'prop:procedure Fun? (cons "function" "Procedure")
+    (#'prop:procedure
+     (lambda (ty-stx fld-name ty)
+       (unless (Fun? ty)
+         (tc-error/fields
+          (format "field ~a is not a function" (syntax-e fld-name))
+          "expected"
+          "Procedure"
+          "given"
+          ty
+          #:stx ty-stx))
+       ty)
      (lambda (ty-stx)
        (tc-error/stx ty-stx
                      "expected: a nonnegative integer literal or an annotated lambda"))
-     #f)))
+     #f)
+    (#'prop:evt?
+     (lambda (ty-stx field-name ty)
+       (if (Evt? ty)
+           ty
+           (make-Evt (Un))))
+     (lambda (ty-stx)
+       (tc-error/stx ty-stx
+                     "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))
+     (lambda (ty-stx doms rng)
+       (unless (zero? (length doms))
+         (tc-error/stx ty-stx
+                       "expected: a function that takes only one argument"))
+       (if (Evt? rng)
+           (values doms rng)
+           (values doms (-mu x (make-Evt x))))))))
 
 
 

From 01e0b82bc7f2f0d166623af045533cf7ea914f3b Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 20 Apr 2022 14:06:20 -0400
Subject: [PATCH 03/16] wip

---
 .../typed-racket/base-env/base-env.rkt        |   2 +-
 .../typed-racket/typecheck/tc-structs.rkt     | 110 +++++++++---------
 typed-racket-test/succeed/prop-evt.rkt        |  30 +++++
 typed-racket-test/succeed/struct-props.rkt    |   2 +-
 4 files changed, 87 insertions(+), 57 deletions(-)
 create mode 100644 typed-racket-test/succeed/prop-evt.rkt

diff --git a/typed-racket-lib/typed-racket/base-env/base-env.rkt b/typed-racket-lib/typed-racket/base-env/base-env.rkt
index 14e5227b8..5447f8b43 100644
--- a/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-env.rkt
@@ -1553,7 +1553,7 @@
 [system-idle-evt (-> (-evt -Void))]
 [alarm-evt (-> -Real (-mu x (-evt x)))]
 [handle-evt? (asym-pred Univ B (-PS (-is-type 0 (-evt Univ)) -tt))]
-[prop:evt (-struct-property (Un (-evt Univ) (-> -Self ManyUniv) -Nat) #'evt?)]
+[prop:evt (-struct-property (Un (-evt Univ) (-> -Self (-evt Univ)) -Nat) #'evt?)]
 [current-evt-pseudo-random-generator
  (-Param -Pseudo-Random-Generator -Pseudo-Random-Generator)]
 
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 79421d3f1..b90702d06 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -458,7 +458,7 @@
   (refine-variance! names stys tvarss))
 
 
-(define ((make-extract check-field-type customized-proc check-doms-rng)
+(define ((make-extract check-field-type check-doms-rng error-msg)
          ty-stx st-name fld-names desc)
   (syntax-parse ty-stx
     #:literals (struct-field-index)
@@ -487,45 +487,12 @@
 
     [ty-stx:st-proc-ty^
      #:do [(define ty (parse-type #'ty-stx))]
-     (match ty
-       [(Fun: (list arrs ...))
-        (make-Fun
-         (map (lambda (arr)
-                (Arrow-update
-                 arr
-                 dom
-                 rng
-                 (lambda (doms rng)
-                   (match (car doms)
-                     [(Name/simple: n)
-                      #:when (free-identifier=? n st-name)
-                      (void)]
-                     [(App: (Name/simple: rator) vars)
-                      #:when (free-identifier=? rator st-name)
-                      (void)]
-                     [(Univ:)
-                      (void)]
-                     [(or (Name/simple: (app syntax-e n)) n)
-                      (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
-                                       "expected" (syntax-e st-name)
-                                       "got" n
-                                       #:stx (st-proc-ty-property #'ty-stx))])
-                   (if check-doms-rng
-                       (check-doms-rng #'ty-stx (cdr doms) rng)
-                       (values (cdr doms) rng)))))
-              arrs))]
-       [_
-        (tc-error/fields "type mismatch"
-                         "expected"
-                         "Procedure"
-                         "given"
-                         ty
-                         #:stx #'ty-stx)])]
-    [_
-     (customized-proc ty-stx)]))
-
-(define-syntax-rule (define-property-handling-table (name check-field-type custimized-handling rng-chck) ...)
-  (make-immutable-free-id-table (list (cons name (make-extract check-field-type custimized-handling rng-chck))
+     (check-doms-rng #'ty-stx ty st-name)
+     ]
+    [_ (tc-error/stx ty-stx error-msg)]))
+
+(define-syntax-rule (define-property-handling-table (name check-field-type rng-chck error-msg) ...)
+  (make-immutable-free-id-table (list (cons name (make-extract check-field-type rng-chck error-msg))
                                       ...)))
 
 (define property-handling-table
@@ -541,25 +508,58 @@
           ty
           #:stx ty-stx))
        ty)
-     (lambda (ty-stx)
-       (tc-error/stx ty-stx
-                     "expected: a nonnegative integer literal or an annotated lambda"))
-     #f)
-    (#'prop:evt?
+     (lambda (ty-stx ty st-name)
+       (match ty
+         [(Fun: (list arrs ...))
+          (make-Fun
+           (map (lambda (arr)
+                  (Arrow-update
+                   arr
+                   dom
+                   (lambda (doms)
+                     (match (car doms)
+                       [(Name/simple: n)
+                        #:when (free-identifier=? n st-name)
+                        (void)]
+                       [(App: (Name/simple: rator) vars)
+                        #:when (free-identifier=? rator st-name)
+                        (void)]
+                       [(Univ:)
+                        (void)]
+                       [(or (Name/simple: (app syntax-e n)) n)
+                        (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
+                                         "expected" (syntax-e st-name)
+                                         "got" n
+                                         #:stx (st-proc-ty-property ty-stx))])
+                     (cdr doms))))
+                arrs))]
+         [_
+          (tc-error/fields "type mismatch"
+                           "expected"
+                           "Procedure"
+                           "given"
+                           ty
+                           #:stx ty-stx)]))
+     "expected: a nonnegative integer literal or an annotated lambda")
+    (#'prop:evt
      (lambda (ty-stx field-name ty)
        (if (Evt? ty)
            ty
            (make-Evt (Un))))
-     (lambda (ty-stx)
-       (tc-error/stx ty-stx
-                     "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))
-     (lambda (ty-stx doms rng)
-       (unless (zero? (length doms))
-         (tc-error/stx ty-stx
-                       "expected: a function that takes only one argument"))
-       (if (Evt? rng)
-           (values doms rng)
-           (values doms (-mu x (make-Evt x))))))))
+     (lambda (ty-stx ty st-name)
+       (match ty
+         [(Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng_t _ _))))))
+          (unless (= (length doms) 1)
+            (tc-error/stx ty-stx
+                          "expected: a function that takes only one argument"))
+          (if (Evt? rng_t)
+              rng_t
+              (-mu x (make-Evt x)))]
+         [_ (if (Evt? ty)
+                ty
+                (tc-error/stx ty-stx
+                              "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))]))
+     "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event")))
 
 
 
diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
new file mode 100644
index 000000000..62f8c4302
--- /dev/null
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -0,0 +1,30 @@
+#lang typed/racket/base
+
+
+(struct aaa0 ((evt : (Evtof Number)))
+  #:property prop:evt (struct-field-index evt))
+
+(ann (sync (aaa0 (make-channel))) Number)
+
+
+(struct aaa1 ([evt : (Evtof Number)])
+  #:property prop:evt 0)
+
+(ann (sync (aaa1 (make-channel))) Number)
+
+(struct aaa2 ([evt : (Evtof Number)])
+  #:property prop:evt (lambda ([self : aaa2]) : (Evtof Number)
+                        (aaa2-evt self)))
+
+(ann (sync (aaa2 (make-channel))) Number)
+
+(struct aaa3 ([evt : (Evtof String)])
+  #:property prop:evt (ann (make-channel) (Evtof String)))
+
+(ann (sync (aaa3 (make-channel))) String)
+
+
+(struct aaa4 ([evt : (Evtof String)])
+  #:property prop:evt (make-channel))
+
+(ann (sync (aaa3 (make-channel))) String)
diff --git a/typed-racket-test/succeed/struct-props.rkt b/typed-racket-test/succeed/struct-props.rkt
index 83c4c08da..2937bce66 100644
--- a/typed-racket-test/succeed/struct-props.rkt
+++ b/typed-racket-test/succeed/struct-props.rkt
@@ -28,7 +28,7 @@
   (lambda ([self : foobar^] [p : Output-Port] [m : (U Boolean 1 0)]) : Void
           (displayln (+ (foobar^-y self) 20) p))
 
-  #:property prop:evt (make-channel)
+  #:property prop:evt (ann (make-channel) (Evtof Any))
 
   #:property prop:custom-print-quotable 'self)
 

From ee65599758c3450fb4a8fdb1be3bce85b021bf35 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 20 Apr 2022 14:28:12 -0400
Subject: [PATCH 04/16] fix

---
 typed-racket-lib/typed-racket/base-env/base-env.rkt | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/typed-racket-lib/typed-racket/base-env/base-env.rkt b/typed-racket-lib/typed-racket/base-env/base-env.rkt
index 5447f8b43..0af4e779f 100644
--- a/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-env.rkt
@@ -1553,7 +1553,7 @@
 [system-idle-evt (-> (-evt -Void))]
 [alarm-evt (-> -Real (-mu x (-evt x)))]
 [handle-evt? (asym-pred Univ B (-PS (-is-type 0 (-evt Univ)) -tt))]
-[prop:evt (-struct-property (Un (-evt Univ) (-> -Self (-evt Univ)) -Nat) #'evt?)]
+[prop:evt (-struct-property (Un (-evt Univ) (-> -Self Univ) -Nat) #'evt?)]
 [current-evt-pseudo-random-generator
  (-Param -Pseudo-Random-Generator -Pseudo-Random-Generator)]
 

From ecea12405c5384b535e4bcb557a5b27c76024bc3 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 20 Apr 2022 14:33:02 -0400
Subject: [PATCH 05/16] add todo

---
 typed-racket-lib/typed-racket/typecheck/tc-structs.rkt | 1 +
 1 file changed, 1 insertion(+)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index b90702d06..9111167d6 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -554,6 +554,7 @@
                           "expected: a function that takes only one argument"))
           (if (Evt? rng_t)
               rng_t
+              ;; fixme: return struct type alias, not always ready
               (-mu x (make-Evt x)))]
          [_ (if (Evt? ty)
                 ty

From df3b7007d77146bf3ab7e4c2b7937b0a9a9e437b Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 20 Apr 2022 14:36:29 -0400
Subject: [PATCH 06/16] fix

---
 typed-racket-test/succeed/prop-evt.rkt | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
index 62f8c4302..461a32a6c 100644
--- a/typed-racket-test/succeed/prop-evt.rkt
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -22,9 +22,3 @@
   #:property prop:evt (ann (make-channel) (Evtof String)))
 
 (ann (sync (aaa3 (make-channel))) String)
-
-
-(struct aaa4 ([evt : (Evtof String)])
-  #:property prop:evt (make-channel))
-
-(ann (sync (aaa3 (make-channel))) String)

From b82489b9e497976c97537788d2bb1d1a55bad90c Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 20 Apr 2022 20:03:23 -0400
Subject: [PATCH 07/16] fix test

---
 typed-racket-test/succeed/prop-evt.rkt | 27 ++++++++++++++++++++------
 1 file changed, 21 insertions(+), 6 deletions(-)

diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
index 461a32a6c..ba30766c3 100644
--- a/typed-racket-test/succeed/prop-evt.rkt
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -1,24 +1,39 @@
 #lang typed/racket/base
 
+(define ch ((inst make-channel Number)))
+
 
 (struct aaa0 ((evt : (Evtof Number)))
   #:property prop:evt (struct-field-index evt))
 
-(ann (sync (aaa0 (make-channel))) Number)
+(thread (lambda ()
+          (channel-put ch 10)))
+
+(ann (sync (aaa0 ch)) Number)
 
 
 (struct aaa1 ([evt : (Evtof Number)])
   #:property prop:evt 0)
 
-(ann (sync (aaa1 (make-channel))) Number)
+(thread (lambda ()
+          (channel-put ch 10)))
+
+(ann (sync (aaa1 ch)) Number)
 
 (struct aaa2 ([evt : (Evtof Number)])
   #:property prop:evt (lambda ([self : aaa2]) : (Evtof Number)
                         (aaa2-evt self)))
 
-(ann (sync (aaa2 (make-channel))) Number)
+(thread (lambda ()
+          (channel-put ch 10)))
+(ann (sync (aaa2 ch)) Number)
+
+
+(define ch2 ((inst make-channel String)))
+(struct aaa3 ()
+  #:property prop:evt (ann ch2 (Evtof String)))
 
-(struct aaa3 ([evt : (Evtof String)])
-  #:property prop:evt (ann (make-channel) (Evtof String)))
+(thread (lambda ()
+          (channel-put ch2 "10")))
 
-(ann (sync (aaa3 (make-channel))) String)
+(ann (sync (aaa3)) String)

From 2194619ac405e195bee170036acd3227346d1fc9 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Fri, 22 Apr 2022 11:10:41 -0400
Subject: [PATCH 08/16] fix

---
 .../typed-racket/typecheck/tc-structs.rkt     | 11 +++---
 .../typed-racket/types/overlap.rkt            |  7 ++++
 typed-racket-test/succeed/prop-evt.rkt        | 36 +++++++++----------
 3 files changed, 31 insertions(+), 23 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 9111167d6..aba115ce5 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -543,8 +543,9 @@
      "expected: a nonnegative integer literal or an annotated lambda")
     (#'prop:evt
      (lambda (ty-stx field-name ty)
-       (if (Evt? ty)
+       (if (subtype ty (-evt Univ))
            ty
+           ;; if the field is not an event, we get the "never ready" event type.
            (make-Evt (Un))))
      (lambda (ty-stx ty st-name)
        (match ty
@@ -552,11 +553,11 @@
           (unless (= (length doms) 1)
             (tc-error/stx ty-stx
                           "expected: a function that takes only one argument"))
-          (if (Evt? rng_t)
+          (if (subtype ty (-evt Univ))
               rng_t
-              ;; fixme: return struct type alias, not always ready
-              (-mu x (make-Evt x)))]
-         [_ (if (Evt? ty)
+              ;; if the field is not an event, we get an "always ready" event of the structure type
+              (make-Evt (parse-type st-name)))]
+         [_ (if (subtype ty (-evt Univ))
                 ty
                 (tc-error/stx ty-stx
                               "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))]))
diff --git a/typed-racket-lib/typed-racket/types/overlap.rkt b/typed-racket-lib/typed-racket/types/overlap.rkt
index dd724196c..2b7ab5706 100644
--- a/typed-racket-lib/typed-racket/types/overlap.rkt
+++ b/typed-racket-lib/typed-racket/types/overlap.rkt
@@ -50,6 +50,13 @@
   (match*/no-order
    (t1 t2)
    [(_ _) #:when (equal? t1 t2) #t]
+   ;; a struct type can overlap with a function type (via prop:procedure)
+   ;; or any event type (via prop:evt)
+   [((or (? Fun?) (? (lambda (x) (subtype x (make-Evt Univ)))))
+     (or (Name/struct: _)
+         (? Struct?)))
+    #:no-order
+    #t]
    [(_ _) #:when (disjoint-masks? (mask t1) (mask t2)) #f]
    [(_ _) #:when (seen? t1 t2) #t]
    [((Univ:) _) #:no-order #t]
diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
index ba30766c3..9536ee2de 100644
--- a/typed-racket-test/succeed/prop-evt.rkt
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -3,7 +3,7 @@
 (define ch ((inst make-channel Number)))
 
 
-(struct aaa0 ((evt : (Evtof Number)))
+(struct aaa0 ((evt : (Channelof Number)))
   #:property prop:evt (struct-field-index evt))
 
 (thread (lambda ()
@@ -12,28 +12,28 @@
 (ann (sync (aaa0 ch)) Number)
 
 
-(struct aaa1 ([evt : (Evtof Number)])
-  #:property prop:evt 0)
+;; (struct aaa1 ([evt : (Evtof Number)])
+;;   #:property prop:evt 0)
 
-(thread (lambda ()
-          (channel-put ch 10)))
+;; (thread (lambda ()
+;;           (channel-put ch 10)))
 
-(ann (sync (aaa1 ch)) Number)
+;; (ann (sync (aaa1 ch)) Number)
 
-(struct aaa2 ([evt : (Evtof Number)])
-  #:property prop:evt (lambda ([self : aaa2]) : (Evtof Number)
-                        (aaa2-evt self)))
+;; (struct aaa2 ([evt : (Channelof Number)])
+;;   #:property prop:evt (lambda ([self : aaa2]) : (Channelof Number)
+;;                         (aaa2-evt self)))
 
-(thread (lambda ()
-          (channel-put ch 10)))
-(ann (sync (aaa2 ch)) Number)
+;; (thread (lambda ()
+;;           (channel-put ch 10)))
+;; (ann (sync (aaa2 ch)) Number)
 
 
-(define ch2 ((inst make-channel String)))
-(struct aaa3 ()
-  #:property prop:evt (ann ch2 (Evtof String)))
+;; (define ch2 ((inst make-channel String)))
+;; (struct aaa3 ()
+;;   #:property prop:evt (ann ch2 (Channelof String)))
 
-(thread (lambda ()
-          (channel-put ch2 "10")))
+;; (thread (lambda ()
+;;           (channel-put ch2 "10")))
 
-(ann (sync (aaa3)) String)
+;; (ann (sync (aaa3)) String)

From 519e416353bb67682e6d921cfd0dddc7d0ea01ce Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Fri, 22 Apr 2022 11:14:22 -0400
Subject: [PATCH 09/16] fix

---
 typed-racket-test/succeed/prop-evt.rkt | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
index 9536ee2de..4a8bb91be 100644
--- a/typed-racket-test/succeed/prop-evt.rkt
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -12,13 +12,13 @@
 (ann (sync (aaa0 ch)) Number)
 
 
-;; (struct aaa1 ([evt : (Evtof Number)])
-;;   #:property prop:evt 0)
+(struct aaa1 ([evt : (Evtof Number)])
+  #:property prop:evt 0)
 
-;; (thread (lambda ()
-;;           (channel-put ch 10)))
+(thread (lambda ()
+          (channel-put ch 10)))
 
-;; (ann (sync (aaa1 ch)) Number)
+(ann (sync (aaa1 ch)) Number)
 
 ;; (struct aaa2 ([evt : (Channelof Number)])
 ;;   #:property prop:evt (lambda ([self : aaa2]) : (Channelof Number)
@@ -29,11 +29,11 @@
 ;; (ann (sync (aaa2 ch)) Number)
 
 
-;; (define ch2 ((inst make-channel String)))
-;; (struct aaa3 ()
-;;   #:property prop:evt (ann ch2 (Channelof String)))
+(define ch2 ((inst make-channel String)))
+(struct aaa3 ()
+  #:property prop:evt (ann ch2 (Channelof String)))
 
-;; (thread (lambda ()
-;;           (channel-put ch2 "10")))
+(thread (lambda ()
+          (channel-put ch2 "10")))
 
-;; (ann (sync (aaa3)) String)
+(ann (sync (aaa3)) String)

From 46582584fe6796c22491c6fc934211b6d1f81d7f Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Fri, 22 Apr 2022 11:19:14 -0400
Subject: [PATCH 10/16] fix

---
 .../typed-racket/typecheck/tc-structs.rkt            |  8 ++++----
 typed-racket-test/succeed/prop-evt.rkt               | 12 ++++++------
 2 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index aba115ce5..ddb38691a 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -549,13 +549,13 @@
            (make-Evt (Un))))
      (lambda (ty-stx ty st-name)
        (match ty
-         [(Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng_t _ _))))))
+         [(Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng-t _ _))))))
           (unless (= (length doms) 1)
             (tc-error/stx ty-stx
                           "expected: a function that takes only one argument"))
-          (if (subtype ty (-evt Univ))
-              rng_t
-              ;; if the field is not an event, we get an "always ready" event of the structure type
+          (if (subtype rng-t (-evt Univ))
+              rng-t
+              ;; if the return type is not an event, we make an event type using the structure type
               (make-Evt (parse-type st-name)))]
          [_ (if (subtype ty (-evt Univ))
                 ty
diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
index 4a8bb91be..cc3e5fb1c 100644
--- a/typed-racket-test/succeed/prop-evt.rkt
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -20,13 +20,13 @@
 
 (ann (sync (aaa1 ch)) Number)
 
-;; (struct aaa2 ([evt : (Channelof Number)])
-;;   #:property prop:evt (lambda ([self : aaa2]) : (Channelof Number)
-;;                         (aaa2-evt self)))
+(struct aaa2 ([evt : (Channelof Number)])
+  #:property prop:evt (lambda ([self : aaa2]) : (Channelof Number)
+                        (aaa2-evt self)))
 
-;; (thread (lambda ()
-;;           (channel-put ch 10)))
-;; (ann (sync (aaa2 ch)) Number)
+(thread (lambda ()
+          (channel-put ch 10)))
+(ann (sync (aaa2 ch)) Number)
 
 
 (define ch2 ((inst make-channel String)))

From 55529429c68ee2cba374450fbad31876a40084ee Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 27 Apr 2022 11:53:07 -0400
Subject: [PATCH 11/16] refactor

---
 .../typed-racket/typecheck/tc-structs.rkt     | 170 ++++++++++--------
 1 file changed, 91 insertions(+), 79 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index ddb38691a..cdec34bd8 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -458,7 +458,7 @@
   (refine-variance! names stys tvarss))
 
 
-(define ((make-extract check-field-type check-doms-rng error-msg)
+(define ((make-extract specified-field-checker supplied-proc-checker failure-msg)
          ty-stx st-name fld-names desc)
   (syntax-parse ty-stx
     #:literals (struct-field-index)
@@ -475,98 +475,110 @@
         max-idx
         #:stx ty-stx))
      (define ty (list-ref (struct-desc-self-fields desc) n))
-     (check-field-type ty-stx (list-ref fld-names n) ty)]
+     (specified-field-checker ty-stx (list-ref fld-names n) ty)]
 
-    ;; a field name is provided (via struct-field-index)
+    ;; a field name is provided via `struct-field-index`
     [(struct-field-index fld-nm:id)
-     (define idx (index-of fld-names #'fld-nm
-                           free-identifier=?))
+     (define idx (index-of fld-names #'fld-nm free-identifier=?))
      ;; fld-nm must be valid, because invalid field names have been reported by
      ;; struct-field-index at this point
-     (list-ref (struct-desc-self-fields desc) idx)]
+     (specified-field-checker ty-stx #'fld-nm (list-ref (struct-desc-self-fields desc) idx))]
 
     [ty-stx:st-proc-ty^
      #:do [(define ty (parse-type #'ty-stx))]
-     (check-doms-rng #'ty-stx ty st-name)
-     ]
-    [_ (tc-error/stx ty-stx error-msg)]))
+     (supplied-proc-checker #'ty-stx ty st-name)]
+    [_ (tc-error/stx ty-stx failure-msg)]))
 
-(define-syntax-rule (define-property-handling-table (name check-field-type rng-chck error-msg) ...)
-  (make-immutable-free-id-table (list (cons name (make-extract check-field-type rng-chck error-msg))
-                                      ...)))
+(define (define-property-handling-entry
+          #:name name
+          #:specified-field-checker specified-field-checker
+          #:supplied-proc-checker suppiled-proc-checker
+          #:failure-msg failure-msg)
+  (cons name (make-extract specified-field-checker suppiled-proc-checker failure-msg)))
 
 (define property-handling-table
-  (define-property-handling-table
-    (#'prop:procedure
-     (lambda (ty-stx fld-name ty)
-       (unless (Fun? ty)
-         (tc-error/fields
-          (format "field ~a is not a function" (syntax-e fld-name))
-          "expected"
-          "Procedure"
-          "given"
-          ty
-          #:stx ty-stx))
-       ty)
-     (lambda (ty-stx ty st-name)
-       (match ty
-         [(Fun: (list arrs ...))
-          (make-Fun
-           (map (lambda (arr)
-                  (Arrow-update
-                   arr
-                   dom
-                   (lambda (doms)
-                     (match (car doms)
-                       [(Name/simple: n)
-                        #:when (free-identifier=? n st-name)
-                        (void)]
-                       [(App: (Name/simple: rator) vars)
-                        #:when (free-identifier=? rator st-name)
-                        (void)]
-                       [(Univ:)
-                        (void)]
-                       [(or (Name/simple: (app syntax-e n)) n)
-                        (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
-                                         "expected" (syntax-e st-name)
-                                         "got" n
-                                         #:stx (st-proc-ty-property ty-stx))])
-                     (cdr doms))))
-                arrs))]
-         [_
-          (tc-error/fields "type mismatch"
-                           "expected"
-                           "Procedure"
-                           "given"
-                           ty
-                           #:stx ty-stx)]))
-     "expected: a nonnegative integer literal or an annotated lambda")
-    (#'prop:evt
-     (lambda (ty-stx field-name ty)
-       (if (subtype ty (-evt Univ))
+  (make-immutable-free-id-table
+   (list
+    (define-property-handling-entry
+      #:name
+      #'prop:procedure
+      #:specified-field-checker
+      (lambda (ty-stx fld-name ty)
+        (unless (Fun? ty)
+          (tc-error/fields
+           (format "field ~a is not a function" (syntax-e fld-name))
+           "expected"
+           "Procedure"
+           "given"
            ty
-           ;; if the field is not an event, we get the "never ready" event type.
-           (make-Evt (Un))))
-     (lambda (ty-stx ty st-name)
-       (match ty
-         [(Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng-t _ _))))))
-          (unless (= (length doms) 1)
-            (tc-error/stx ty-stx
-                          "expected: a function that takes only one argument"))
-          (if (subtype rng-t (-evt Univ))
-              rng-t
-              ;; if the return type is not an event, we make an event type using the structure type
-              (make-Evt (parse-type st-name)))]
-         [_ (if (subtype ty (-evt Univ))
-                ty
-                (tc-error/stx ty-stx
-                              "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))]))
-     "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event")))
+           #:stx ty-stx))
+        ty)
+      #:supplied-proc-checker
+      (lambda (ty-stx ty st-name)
+        (match ty
+          [(Fun: (list arrs ...))
+           (make-Fun
+            (map (lambda (arr)
+                   (Arrow-update
+                    arr
+                    dom
+                    (lambda (doms)
+                      (match (car doms)
+                        [(Name/simple: n)
+                         #:when (free-identifier=? n st-name)
+                         (void)]
+                        [(App: (Name/simple: rator) vars)
+                         #:when (free-identifier=? rator st-name)
+                         (void)]
+                        [(Univ:)
+                         (void)]
+                        [(or (Name/simple: (app syntax-e n)) n)
+                         (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
+                                          "expected" (syntax-e st-name)
+                                          "got" n
+                                          #:stx (st-proc-ty-property ty-stx))])
+                      (cdr doms))))
+                 arrs))]
+          [_
+           (tc-error/fields "type mismatch"
+                            "expected"
+                            "Procedure"
+                            "given"
+                            ty
+                            #:stx ty-stx)]))
+      #:failure-msg
+      "expected: a nonnegative integer literal or an annotated lambda")
+    (define-property-handling-entry
+      #:name
+      #'prop:evt
+      #:specified-field-checker
+      (lambda (ty-stx field-name ty)
+        (if (subtype ty (-evt Univ))
+            ty
+            ;; if the field is not an event, we get the "never ready" event type.
+            (make-Evt (Un))))
+      #:supplied-proc-checker
+      (lambda (ty-stx ty st-name)
+        (match ty
+          [(Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng-t _ _))))))
+           (unless (= (length doms) 1)
+             (tc-error/stx ty-stx
+                           "expected: a function that takes only one argument"))
+           (if (subtype rng-t (-evt Univ))
+               rng-t
+               ;; if the return type is not an event, we make an event type using the structure type
+               (make-Evt (parse-type st-name)))]
+          [_ (if (subtype ty (-evt Univ))
+                 ty
+                 (tc-error/stx ty-stx
+                               "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))]))
+      #:failure-msg
+      "expected: a nonnegative integer literal, an annotated lambda that returns an event, or an event"))))
 
 
 
 ;; extract the type annotation of prop:procedure value
-(define/cond-contract (extract-proc-ty proc-ty-stx-li desc fld-names st-name)
+(define/cond-contract (extract-prop-specified-type proc-ty-stx-li desc fld-names st-name)
   (c:-> (c:listof syntax?) struct-desc? (c:listof identifier?) identifier? Type?)
 
 
@@ -668,7 +680,7 @@
                                            (and proc-ty-stx
                                                 (not (null? proc-ty-stx))
                                                 (extend-tvars tvars
-                                                              (extract-proc-ty proc-ty-stx desc fld-names type-name)))))
+                                                              (extract-prop-specified-type proc-ty-stx desc fld-names type-name)))))
 
          (parsed-struct sty names desc (struct-info-property nm/par) type-only)]))
 

From 8bb4700a65f3922215fd2568f89033b089e295cf Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 27 Apr 2022 11:54:37 -0400
Subject: [PATCH 12/16] revert

---
 typed-racket-test/succeed/struct-props.rkt | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/typed-racket-test/succeed/struct-props.rkt b/typed-racket-test/succeed/struct-props.rkt
index 2937bce66..6d843b458 100644
--- a/typed-racket-test/succeed/struct-props.rkt
+++ b/typed-racket-test/succeed/struct-props.rkt
@@ -20,7 +20,8 @@
 (struct foobar foo ([y : Number])
   #:property prop:custom-write
   (lambda ([self : foo] [p : Output-Port] [m : (U Boolean 1 0)]) : Void
-          (displayln (+ (foo-x self) 20) p))
+    (displayln (+ (foo-x self) 20) p))
+  #:property prop:evt 0
   #:property prop:custom-print-quotable 'always)
 
 (struct foobar^ foo ([y : Number])

From 520a36184610cfc83a83e9f7ce57fac298e6c265 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 27 Apr 2022 11:59:27 -0400
Subject: [PATCH 13/16] rename

---
 .../typed-racket/base-env/prims-struct.rkt             | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
index abf87762d..872721247 100644
--- a/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
+++ b/typed-racket-lib/typed-racket/base-env/prims-struct.rkt
@@ -109,7 +109,7 @@
                                               tname
                                               (quasisyntax/loc tname
                                                 (#,tname #,@type-vars))))
-                          (define-values (val^ ty^) (maybe-extract-prop-proc-ty-ann sty-stx val))
+                          (define-values (val^ ty^) (extract-prop-specified-type-ann sty-stx val))
                           (values val^ (assoc-struct-property-name-property ty^ name))]
                          [else (values val #f)])))]
              #:attr proc-ty (if (null? proc-tys) #f
@@ -201,17 +201,17 @@
                 . opts))]))
 
 
-;; This function tries to extract the type annotation on a lambda
-;; expression for prop:procedure.
+;; This function tries to extract the type annotation from values for
+;; prop:procedure or prop:evt
 ;;
 ;; sty-stx: the syntax that represents a structure type. For a monomorhpic
 ;; structure type, sty-stx is the identifier for its name. For a polymorphic
 ;; structure type, sty-stx is in the form (structure-name type-vars ...)
 ;;
-;; val: the value expression for prop:procedure
+;; val: the value expression for the property
 ;;
 ;;Syntax Expr -> (values Syntax Syntax)
-(define-for-syntax (maybe-extract-prop-proc-ty-ann sty-stx val)
+(define-for-syntax (extract-prop-specified-type-ann sty-stx val)
   (syntax-parse val
     #:literals (-lambda ann)
     [(-lambda formals:lambda-formals ret-ty:return-ann _)

From 7c1c96a35f25e8c7a7e9d3c6609a8e0b99455190 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Wed, 27 Apr 2022 13:10:40 -0400
Subject: [PATCH 14/16] wip

---
 .../typed-racket/env/init-envs.rkt            |  4 +--
 .../typed-racket/infer/infer-unit.rkt         | 15 ++++++----
 .../typed-racket/private/type-contract.rkt    |  4 +--
 .../typed-racket/rep/type-rep.rkt             | 29 ++++++++++---------
 .../typed-racket/typecheck/tc-structs.rkt     | 17 +++++------
 .../typed-racket/types/abbrev.rkt             |  7 ++++-
 .../typed-racket/types/printer.rkt            |  4 +--
 .../typed-racket/types/subtype.rkt            | 10 ++++---
 .../unit-tests/contract-tests.rkt             |  2 +-
 9 files changed, 51 insertions(+), 41 deletions(-)

diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt
index 67ae08d39..18730c027 100644
--- a/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -265,11 +265,11 @@
      `(make-Name (quote-syntax ,stx) ,args ,struct?)]
     [(fld: t acc mut)
      `(make-fld ,(type->sexp t) (quote-syntax ,acc) ,mut)]
-    [(Struct: name parent flds proc poly? pred-id properties)
+    [(Struct: name parent flds extra-tys poly? pred-id properties)
      `(make-Struct (quote-syntax ,name)
                    ,(and parent (type->sexp parent))
                    (list ,@(map type->sexp flds))
-                   ,(and proc (type->sexp proc))
+                   ,(and extra-tys `(list ,@(map type->sexp extra-tys)))
                    ,poly?
                    (quote-syntax ,pred-id)
                    (immutable-free-id-set (list ,@(for/list ([p (in-free-id-set properties)])
diff --git a/typed-racket-lib/typed-racket/infer/infer-unit.rkt b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
index d683e26ab..f0924e492 100644
--- a/typed-racket-lib/typed-racket/infer/infer-unit.rkt
+++ b/typed-racket-lib/typed-racket/infer/infer-unit.rkt
@@ -681,14 +681,17 @@
 
         ;; two structs with the same name
         ;; just check pairwise on the fields
-        [((Struct: nm _ flds proc _ _ _) (Struct: nm* _ flds* proc* _ _ _))
+        [((Struct: nm _ flds extra-ty _ _ _) (Struct: nm* _ flds* extra-ty* _ _ _))
          #:when (free-identifier=? nm nm*)
-         (let ([proc-c
-                (cond [(and proc proc*)
-                       (cg proc proc*)]
-                      [proc* #f]
+         (let ([extra-ty-c
+                (cond [(and extra-ty extra-ty*)
+                       (for/fold ([acc empty])
+                                  ([p extra-ty]
+                                   [p* extra-ty*])
+                         (% cset-meet acc (cg p p*)))]
+                      [extra-ty* #f]
                       [else empty])])
-           (% cset-meet proc-c (cgen/flds context flds flds*)))]
+           (% cset-meet extra-ty-c (cgen/flds context flds flds*)))]
 
         ;; two prefab structs with the same key
         [((Prefab: k ss) (Prefab: k* ts))
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index 757cd77f4..191f12395 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -727,10 +727,10 @@
                               " 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? props)
+       [(Struct: nm par (list (fld: flds acc-ids mut?) ...) extra-tys poly? pred? props)
         (cond
           [(hash-ref recursive-values nm #f)]
-          [proc (fail #:reason "procedural structs are not supported")]
+          [extra-tys (fail #:reason "structs with prop:procedure or prop:evt attached are not supported")]
           [poly?
            (struct->recursive-sc #'n* nm flds
                                            (lambda (ftsc)
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 037af0466..d4731b99b 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -76,7 +76,7 @@
                      [Struct:* Struct:]
                      [Row* make-Row]
                      [make-Mu unsafe-make-Mu]
-                     [Struct-proc* Struct-proc]
+                     [Struct-extra-tys* Struct-extra-tys]
                      [make-Struct* make-Struct]
                      [Mu-names: Mu-maybe-name:]
                      [Mu-body Mu-body-unsafe]
@@ -776,41 +776,42 @@
                   ;; we can only put a function type of this box when checking the property value
                   ;; for prop:procedure, which happens after a Struct rep
                   ;; instance is created.
-                  [proc (box/c (or/c #f Fun?))]
+                  [extra-tys (box/c (or/c #f (listof Type?)))]
                   [poly? boolean?]
                   [pred-id identifier?]
                   [properties (free-id-set/c identifier?)])
-  #:no-provide (Struct: Struct-proc make-Struct)
-  [#:frees (f) (combine-frees (map f (append (let ([bv (unbox proc)])
-                                               (if bv (list bv) null))
+  #:no-provide (Struct: Struct-extra-tys make-Struct)
+  [#:frees (f) (combine-frees (map f (append (let ([bv (unbox extra-tys)])
+                                               (if bv bv null))
                                              (if parent (list parent) null)
                                              flds)))]
   [#:fmap (f) (make-Struct name
                            (and parent (f parent))
                            (map f flds)
-                           (let ([bv (unbox proc)])
-                             (box (and bv (f bv))))
+                           (let ([bv (unbox extra-tys)])
+                             (box (and bv (map f bv))))
                            poly?
                            pred-id
                            properties)]
   [#:for-each (f)
    (when parent (f parent))
    (for-each f flds)
-   (when proc (f proc))]
+   (let ([bv (unbox extra-tys)])
+     (when bv (for-each f bv)))]
   ;; This should eventually be based on understanding of struct properties.
   [#:mask (mask-union mask:struct mask:procedure)]
   [#:custom-constructor
    (let ([name (normalize-id name)]
          [pred-id (normalize-id pred-id)])
-     (make-Struct name parent flds proc poly? pred-id properties))])
+     (make-Struct name parent flds extra-tys poly? pred-id properties))])
 
 
-(define/cond-contract (Struct-proc* sty)
-  (-> (or/c Poly? Struct?) (or/c #f Type?))
+(define/cond-contract (Struct-extra-tys* sty)
+  (-> (or/c Poly? Struct?) (or/c #f (listof Type?)))
   (define sty^ (match sty
                  [(? Struct?) sty]
                  [(Poly: _ (? Struct? sty)) sty]))
-  (define b (Struct-proc sty^))
+  (define b (Struct-extra-tys sty^))
   (and b (unbox b)))
 
 (define (make-Struct* name parent flds proc poly? pred-id properties)
@@ -819,8 +820,8 @@
 (define-match-expander Struct:*
   (lambda (stx)
     (syntax-case stx ()
-      [(_ name parent flds proc poly? pred-id properties)
-       #'(Struct: name parent flds (box proc) poly? pred-id properties)])))
+      [(_ name parent flds extra-tys poly? pred-id properties)
+       #'(Struct: name parent flds (box extra-tys) poly? pred-id properties)])))
 
 
 (def-type StructTop ([name Struct?])
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index cdec34bd8..e2e1c0fdc 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -188,7 +188,7 @@
 ;; Constructs the Struct value for a structure type
 ;; The returned value has free type variables
 (define/cond-contract (mk/inner-struct-type names desc parent [property-names empty] [proc-ty #f])
-  (c:->* (struct-names? struct-desc? (c:or/c Struct? #f)) ((c:listof identifier?) (c:or/c Type? #f)) Struct?)
+  (c:->* (struct-names? struct-desc? (c:or/c Struct? #f)) ((c:listof identifier?) (c:or/c (c:listof Type?) #f)) Struct?)
 
   (let* ([this-flds (for/list ([t (in-list (struct-desc-self-fields desc))]
                                [g (in-list (struct-names-getters names))])
@@ -197,7 +197,7 @@
     (make-Struct (struct-names-struct-name names)
                  parent
                  flds
-                 (or proc-ty (and parent (Struct-proc parent)))
+                 (or proc-ty (and parent (Struct-extra-tys parent)))
                  (not (null? (struct-desc-tvars desc)))
                  (struct-names-predicate names)
                  (immutable-free-id-set property-names))))
@@ -377,10 +377,10 @@
   ;; the alias, with free type variables
   (define st-type-alias (mk-type-alias type-name tvars))
   (define st-type-alias-maybe-with-proc
-    (let ([maybe-proc-ty (and (or (Poly? sty) (Struct? sty))
-                              (Struct-proc sty))])
-      (if maybe-proc-ty
-          (intersect st-type-alias maybe-proc-ty)
+    (let ([maybe-proc-tys (and (or (Poly? sty) (Struct? sty))
+                              (Struct-extra-tys sty))])
+      (if maybe-proc-tys
+          (foldl intersect st-type-alias maybe-proc-tys)
           st-type-alias)) )
 
   ;; simple abstraction for handling field getters or setters
@@ -579,14 +579,13 @@
 
 ;; extract the type annotation of prop:procedure value
 (define/cond-contract (extract-prop-specified-type proc-ty-stx-li desc fld-names st-name)
-  (c:-> (c:listof syntax?) struct-desc? (c:listof identifier?) identifier? Type?)
+  (c:-> (c:listof syntax?) struct-desc? (c:listof identifier?) identifier? (c:listof Type?))
 
 
   (unless (equal? (length proc-ty-stx-li) 1)
     (tc-error "prop:procedure can only have one value assigned to it"))
 
-  ;; fixme for/first -> for/list
-  (for/first ([proc-ty-stx (in-list proc-ty-stx-li)])
+  (for/list ([proc-ty-stx (in-list proc-ty-stx-li)])
     (define property-name (assoc-struct-property-name-property proc-ty-stx))
     ((free-id-table-ref property-handling-table property-name) proc-ty-stx st-name fld-names desc)))
 
diff --git a/typed-racket-lib/typed-racket/types/abbrev.rkt b/typed-racket-lib/typed-racket/types/abbrev.rkt
index bb2d92470..a73113282 100644
--- a/typed-racket-lib/typed-racket/types/abbrev.rkt
+++ b/typed-racket-lib/typed-racket/types/abbrev.rkt
@@ -195,7 +195,12 @@
 
 ;; Structs
 (define (-struct name parent flds [proc #f] [poly #f] [pred #'dummy] [props (immutable-free-id-set)])
-  (make-Struct name parent flds proc poly pred props))
+  (make-Struct name parent flds
+               (cond
+                 [(and proc (not (list? proc)))
+                  (list proc)]
+                 [else proc])
+               poly pred props))
 
 ;; Function type constructors
 (define/decl top-func (make-Fun (list)))
diff --git a/typed-racket-lib/typed-racket/types/printer.rkt b/typed-racket-lib/typed-racket/types/printer.rkt
index 6342c2d8b..7525b0dd1 100644
--- a/typed-racket-lib/typed-racket/types/printer.rkt
+++ b/typed-racket-lib/typed-racket/types/printer.rkt
@@ -660,10 +660,10 @@
     [(? improper-tuple? t)
      `(List* ,@(map type->sexp (improper-tuple-elems t)))]
     [(Opaque: pred) `(Opaque ,(syntax->datum pred))]
-    [(Struct: nm par (list (fld: t _ _) ...) proc _ _ properties)
+    [(Struct: nm par (list (fld: t _ _) ...) extra-tys _ _ properties)
      `#(,(string->symbol (format "struct:~a" (syntax-e nm)))
         ,(map t->s t)
-        ,@(if proc (list (t->s proc)) null)
+        ,@(if extra-tys (list (map t->s extra-tys)) null)
         ,@(free-id-set->list properties))]
     [(? Fun?)
      (parameterize ([current-print-type-fuel
diff --git a/typed-racket-lib/typed-racket/types/subtype.rkt b/typed-racket-lib/typed-racket/types/subtype.rkt
index 652a1f5a6..dc8126d0d 100644
--- a/typed-racket-lib/typed-racket/types/subtype.rkt
+++ b/typed-racket-lib/typed-racket/types/subtype.rkt
@@ -1205,7 +1205,7 @@
      [(Sequence: (list seq-t)) (subtype* A elem1 seq-t)]
      [_ (continue<: A t1 t2 obj)])]
   [(case: Some (Some: _ _)) #f]
-  [(case: Struct (Struct: nm1 parent1 flds1 proc1 _ _ properties))
+  [(case: Struct (Struct: nm1 parent1 flds1 extras1 _ _ properties))
    (match t2
      ;; Avoid resolving things that refer to different structs.
      ;; Saves us from non-termination
@@ -1213,12 +1213,14 @@
       #:when (unrelated-structs t1 t2)
       #f]
      ;; subtyping on immutable structs is covariant
-     [(Struct: nm2 _ flds2 proc2 _ _ _)
+     [(Struct: nm2 _ flds2 extras2 _ _ _)
       #:when (free-identifier=? nm1 nm2)
       (let ([A (remember t1 t2 A)])
         (with-updated-seen A
-          (let ([A (cond [(and proc1 proc2) (subtype* A proc1 proc2)]
-                         [proc2 #f]
+          (let ([A (cond [(and extras1 extras2) (for/and ([et1 (in-list extras1)]
+                                                          [et2 (in-list extras2)])
+                                                  (subtype* A et1 et2))]
+                         [extras2 #f]
                          [else A])])
             (for/fold ([A A])
                       ([f1 (in-list flds1)]
diff --git a/typed-racket-test/unit-tests/contract-tests.rkt b/typed-racket-test/unit-tests/contract-tests.rkt
index 9d54755d9..89a57e3a5 100644
--- a/typed-racket-test/unit-tests/contract-tests.rkt
+++ b/typed-racket-test/unit-tests/contract-tests.rkt
@@ -223,7 +223,7 @@
             (-> -Symbol -Symbol))
            "two cases of arity 1")
    (t/fail (-struct #'struct-name2 #f (list (make-fld -Symbol #'acc #f)) (-> -Symbol))
-           "procedural structs are not supported")
+           "structs with prop:procedure or prop:evt attached are not supported")
    (t/fail (-Syntax (-> -Boolean -Boolean))
            "required a flat contract but generated a chaperone contract")
    (t/fail (-Syntax (-seq -Boolean))

From 132a196fb87f3eab0553991b19d2da4c1c332128 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Thu, 28 Apr 2022 20:36:03 -0400
Subject: [PATCH 15/16] rename

---
 typed-racket-lib/typed-racket/typecheck/tc-structs.rkt | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index e2e1c0fdc..9a38431b0 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -489,7 +489,7 @@
      (supplied-proc-checker #'ty-stx ty st-name)]
     [_ (tc-error/stx ty-stx failure-msg)]))
 
-(define (define-property-handling-entry
+(define (mk-handling-entry
           #:name name
           #:specified-field-checker specified-field-checker
           #:supplied-proc-checker suppiled-proc-checker
@@ -499,7 +499,7 @@
 (define property-handling-table
   (make-immutable-free-id-table
    (list
-    (define-property-handling-entry
+    (mk-handling-entry
       #:name
       #'prop:procedure
       #:specified-field-checker
@@ -548,7 +548,7 @@
                             #:stx ty-stx)]))
       #:failure-msg
       "expected: a nonnegative integer literal or an annotated lambda")
-    (define-property-handling-entry
+    (mk-handling-entry
       #:name
       #'prop:evt
       #:specified-field-checker

From 276674257a8147b2c4f42411bb9d28a14d5029e5 Mon Sep 17 00:00:00 2001
From: Fred Fu <moonsolo@gmail.com>
Date: Thu, 28 Apr 2022 21:35:56 -0400
Subject: [PATCH 16/16] wip

---
 .../typed-racket/rep/type-mask.rkt            |  1 +
 .../typed-racket/rep/type-rep.rkt             |  9 +++--
 .../typed-racket/typecheck/tc-structs.rkt     | 34 +++++++++++--------
 typed-racket-test/succeed/prop-evt.rkt        | 23 +++++++++++++
 4 files changed, 50 insertions(+), 17 deletions(-)

diff --git a/typed-racket-lib/typed-racket/rep/type-mask.rkt b/typed-racket-lib/typed-racket/rep/type-mask.rkt
index 348797657..4d14f2904 100644
--- a/typed-racket-lib/typed-racket/rep/type-mask.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-mask.rkt
@@ -144,6 +144,7 @@
  mask:other-box
  mask:set
  mask:procedure
+ mask:evt
  mask:prompt-tag
  mask:continuation-mark-key
  mask:struct
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index d4731b99b..eb632a15e 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -368,7 +368,8 @@
 ;; Evt
 ;;------
 
-(def-structural Evt ([result #:covariant]))
+(def-structural Evt ([result #:covariant])
+  [#:mask mask:evt])
 
 ;;--------
 ;; Param
@@ -799,7 +800,7 @@
    (let ([bv (unbox extra-tys)])
      (when bv (for-each f bv)))]
   ;; This should eventually be based on understanding of struct properties.
-  [#:mask (mask-union mask:struct mask:procedure)]
+  [#:mask (mask-union mask:struct mask:procedure mask:evt)]
   [#:custom-constructor
    (let ([name (normalize-id name)]
          [pred-id (normalize-id pred-id)])
@@ -830,6 +831,10 @@
   [#:for-each (f) (f name)]
   [#:mask (mask-union mask:struct mask:procedure)])
 
+(def-type Undecided-Evt ([n F?])
+  [#:frees (f) (f n)]
+  [#:fmap (f) (make-Undecide)])
+
 ;; Represents prefab structs
 ;; key  : prefab key encoding mutability, auto-fields, etc.
 ;; flds : the types of all of the prefab fields
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index 9a38431b0..ee439a762 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -486,7 +486,8 @@
 
     [ty-stx:st-proc-ty^
      #:do [(define ty (parse-type #'ty-stx))]
-     (supplied-proc-checker #'ty-stx ty st-name)]
+     (define tvars (struct-desc-tvars desc))
+     (supplied-proc-checker #'ty-stx ty (mk-type-alias st-name tvars))]
     [_ (tc-error/stx ty-stx failure-msg)]))
 
 (define (mk-handling-entry
@@ -514,7 +515,7 @@
            #:stx ty-stx))
         ty)
       #:supplied-proc-checker
-      (lambda (ty-stx ty st-name)
+      (lambda (ty-stx ty st-alias)
         (match ty
           [(Fun: (list arrs ...))
            (make-Fun
@@ -523,18 +524,18 @@
                     arr
                     dom
                     (lambda (doms)
-                      (match (car doms)
-                        [(Name/simple: n)
-                         #:when (free-identifier=? n st-name)
+                      (match* ((car doms) st-alias)
+                        [((Name/simple: n) (Name/simple: st))
+                         #:when (free-identifier=? n st)
                          (void)]
-                        [(App: (Name/simple: rator) vars)
-                         #:when (free-identifier=? rator st-name)
+                        [((App: (Name/simple: rator) _) (App: (Name/simple: st) _))
+                         #:when (free-identifier=? rator st)
                          (void)]
-                        [(Univ:)
+                        [((Univ:) _)
                          (void)]
-                        [(or (Name/simple: (app syntax-e n)) n)
+                        [((or (Name/simple: (app syntax-e n)) n) _)
                          (tc-error/fields "type mismatch in the first parameter of the function for prop:procedure"
-                                          "expected" (syntax-e st-name)
+                                          "expected" st-alias
                                           "got" n
                                           #:stx (st-proc-ty-property ty-stx))])
                       (cdr doms))))
@@ -558,16 +559,19 @@
             ;; if the field is not an event, we get the "never ready" event type.
             (make-Evt (Un))))
       #:supplied-proc-checker
-      (lambda (ty-stx ty st-name)
+      (lambda (ty-stx ty st-alias)
         (match ty
           [(Fun: (list (Arrow: doms _ _ (Values: (list (Result: rng-t _ _))))))
            (unless (= (length doms) 1)
              (tc-error/stx ty-stx
                            "expected: a function that takes only one argument"))
-           (if (subtype rng-t (-evt Univ))
-               rng-t
-               ;; if the return type is not an event, we make an event type using the structure type
-               (make-Evt (parse-type st-name)))]
+           (cond
+             [(subtype rng-t (-evt Univ))
+              rng-t]
+             [(F? rng-t) (make-Evt rng-t)]
+             [else
+              ;; if the return type is not an event, we make an event type using the structure type
+              (make-Evt st-alias)])]
           [_ (if (subtype ty (-evt Univ))
                  ty
                  (tc-error/stx ty-stx
diff --git a/typed-racket-test/succeed/prop-evt.rkt b/typed-racket-test/succeed/prop-evt.rkt
index cc3e5fb1c..3cf16925b 100644
--- a/typed-racket-test/succeed/prop-evt.rkt
+++ b/typed-racket-test/succeed/prop-evt.rkt
@@ -37,3 +37,26 @@
           (channel-put ch2 "10")))
 
 (ann (sync (aaa3)) String)
+
+
+(struct aaa4 ([b : String]) #:property prop:evt (lambda (self) : Number
+                                                  (string-length (aaa4-b self))))
+
+(ann (sync (aaa4 "hello")) aaa4)
+
+
+(struct (A) poly-aaa ([b : A]) #:property prop:evt (lambda (self) : A
+                                                     (poly-aaa-b self)))
+
+(ann (sync (poly-aaa "hello")) (poly-aaa String))
+
+(thread (lambda ()
+          (channel-put ch 10)))
+(ann (sync (poly-aaa ch))  Number)
+
+
+(struct aaa-never ([b : String]) #:property prop:evt (struct-field-index b))
+
+((lambda ([a : (Evtof Nothing)]) : String
+   "42")
+ (aaa-never "84"))