Make syntax class for syntax properties.

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

@@ -90,6 +90,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
                 [typed-racket/env/type-name-env (register-type-name)]))
 
 (define-for-syntax (ignore stx) (ignore-property stx #t))
+(define-for-syntax (ignore-some stx) (ignore-some-property stx #t))
 
 (begin-for-syntax
   (define-syntax-class opt-parent
@@ -233,10 +234,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
   (syntax-parse stx
     [(_ name:id ty:expr)
      #`(begin
-         #,(ignore-property (if (eq? (syntax-local-context) 'top-level)
+         #,(ignore (if (eq? (syntax-local-context) 'top-level)
                        #'(define name (procedure-rename (make-predicate ty) 'name))
-                                (flat-contract-def-property  #'(define name #f) #'ty))
+                       (flat-contract-def-property  #'(define name #f) #'ty)))
-                            #t)
          ;; not a require, this is just the unchecked declaration syntax
          #,(internal #'(require/typed-internal name (Any -> Boolean : ty))))]))
 
@@ -256,7 +256,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
                type)))
 
          #`(ann
-             #,(external-check-property (ignore-some-property name #t) check-valid-type)
+             #,(external-check-property (ignore-some name) check-valid-type)
              (Any -> Boolean : ty)))
        (let ([typ (parse-type #'ty)])
          (if (Error? typ)
@@ -264,15 +264,14 @@ This file defines two sorts of primitives. All of them are provided into any mod
              #`(error 'make-predicate "Couldn't parse type")
              #`(#%expression
                 (ann
-                 #,(ignore-some-property
+                 #,(ignore-some
                     (type->contract
                      typ
                      ;; must be a flat contract
                      #:kind 'flat
                      ;; the value is not from the typed side
                      #:typed-side #f
-                     (type->contract-fail typ #'ty #:ctc-str "predicate"))
+                     (type->contract-fail typ #'ty #:ctc-str "predicate")))
-                    #t)
                  (Any -> Boolean : ty))))))]))
 
 (define-syntax (cast stx)
@@ -281,7 +280,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
      (define (apply-contract ctc-expr)
        #`(#%expression
            (ann
-             #,(ignore-some-property
+             #,(ignore-some
                  #`(let-values (((val) #,(with-type-property #'(ann v Any) #t)))
                      (contract
                        #,ctc-expr
@@ -289,8 +288,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
                        'cast
                        'typed-world
                        val
-                       (quote-syntax #,stx)))
+                       (quote-syntax #,stx))))
-                 #t)
              ty)))
 
      (cond [(not (unbox typed-context?)) ; no-check, don't check
@@ -328,12 +326,12 @@ This file defines two sorts of primitives. All of them are provided into any mod
      (with-syntax ([hidden (generate-temporary #'pred)])
        (quasisyntax/loc stx
          (begin
-           #,(ignore-property #'(define pred-cnt (any/c . c-> . boolean?)) #t)
+           #,(ignore #'(define pred-cnt (any/c . c-> . boolean?)))
            #,(internal #'(require/typed-internal hidden (Any -> Boolean : (Opaque pred))))
            #,(if (attribute ne)
                  (internal (syntax/loc stx (define-type-alias-internal ty (Opaque pred))))
                  (syntax/loc stx (define-type-alias ty (Opaque pred))))
-           #,(ignore-property #'(require/contract pred hidden pred-cnt lib) #t))))]))
+           #,(ignore #'(require/contract pred hidden pred-cnt lib)))))]))
 
 (begin-for-syntax
   (define-syntax-class type-variables
@@ -530,9 +528,8 @@ This file defines two sorts of primitives. All of them are provided into any mod
     [(_ nm ((~describe "field specification" [fld:optionally-annotated-name]) ...) [proc : proc-ty])
      (with-syntax*
       ([proc* (with-type-property #'(ann proc : proc-ty) #t)]
-       [d-s (ignore-some-property (syntax/loc stx (define-struct nm (fld.name ...)
+       [d-s (ignore-some (syntax/loc stx (define-struct nm (fld.name ...)
-                                               #:property prop:procedure proc*))
+                                      #:property prop:procedure proc*)))]
-                                  #t)]
        [dtsi (quasisyntax/loc stx (dtsi/exec* () nm (fld ...) proc-ty))])
       #'(begin d-s dtsi))]))
 
@@ -603,9 +600,8 @@ This file defines two sorts of primitives. All of them are provided into any mod
            opts:struct-options)
         (let ([mutable? (if (attribute opts.mutable?) #'(#:mutable) #'())]
               [cname (second (build-struct-names #'nm.name empty #t #t))])
-          (with-syntax ([d-s (ignore-some-property
+          (with-syntax ([d-s (ignore-some
-                               (syntax/loc stx (define-struct nm (fs.fld ...) . opts))
+                               (syntax/loc stx (define-struct nm (fs.fld ...) . opts)))]
-                               #t)]
                         [dtsi (quasisyntax/loc stx
                                 (dtsi* (vars.vars ...) nm (fs ...)
                                        #:maker #,cname
@@ -632,10 +628,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
        [(_ vars:maybe-type-vars nm:struct-name/new (fs:fld-spec ...)
            opts:struct-options)
         (let ([mutable? (if (attribute opts.mutable?) #'(#:mutable) #'())])
-          (with-syntax ([d-s (ignore-property (quasisyntax/loc stx
+          (with-syntax ([d-s (ignore (quasisyntax/loc stx
                                        (struct #,@(attribute nm.new-spec) (fs.fld ...)
-                                                        . opts))
+                                               . opts)))]
-                                              #t)]
                         [dtsi (quasisyntax/loc stx
                                 (dtsi* (vars.vars ...)
                                        nm.old-spec (fs ...)
@@ -1161,9 +1156,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
            (list
              (attribute args.required-pos)
              (attribute args.optional-pos))))
-       (syntax-property
+       (opt-lambda-property
-         (syntax-property d 'kw-lambda kw-property)
+         (kw-lambda-property d kw-property)
-         'opt-lambda opt-property)]
+         opt-property)]
        ;; This is an error and will be caught by the real lambda
       [_ d])]))
 

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/global-env.rkt

@@ -4,6 +4,7 @@
 ;; maps identifiers to their types, updated by mutation
 
 (require "../types/tc-error.rkt"
+         syntax/parse
          syntax/id-table
          racket/lazy-require) 
 (provide register-type register-type-if-undefined
@@ -11,6 +12,7 @@
          maybe-finish-register-type
          register-type/undefined
          lookup-type
+         typed-id^
          register-types
          unregister-type
          check-all-registered-types
@@ -64,6 +66,12 @@
         [(procedure? v) (define t (v)) (register-type id t) t]
         [else v]))
 
+(define-syntax-class typed-id^
+  #:attributes (type)
+  (pattern i:id
+    #:attr type (lookup-type #'i #f)
+    #:when (attribute type)))
+
 (define (maybe-finish-register-type id)
   (let ([v (free-id-table-ref the-mapping id)])
     (if (box? v)

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/env/scoped-tvar-env.rkt

@@ -4,6 +4,7 @@
 
 (require "../utils/utils.rkt"
          (for-template racket/base)
+         (private syntax-properties)
          syntax/parse
          syntax/id-table
          racket/match
@@ -31,9 +32,8 @@
           [(#%expression e) (loop #'e)]
           [(~or (case-lambda formals . body) (#%plain-lambda formals . body))
            (add-vars stx)]
-          [(let-values ([(f) fun]) . body)
+          [(~and (let-values ([(f) fun]) . body)
-           #:when (or (syntax-property stx 'kw-lambda)
+                 (~or _:kw-lambda^ :opt-lambda^))
-                      (syntax-property stx 'opt-lambda))
            (add-vars #'fun)]
           [e (void)]))]))
 

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/optimizer/optimizer.rkt

@@ -18,15 +18,12 @@
   #:literal-sets (kernel-literals)
   #:attributes (opt)
   ;; Can't optimize this code because it isn't typechecked
-  (pattern opt:expr
+  (pattern (~or opt:ignore^ opt:ignore-some^ opt:with-handlers^))
-    #:when (or (ignore-property #'opt)
-               (ignore-some-property #'opt)
-               (with-handlers-property #'opt)))
 
   ;; Can't optimize the body of this code because it isn't typechecked
-  (pattern ((~and op let-values)
+  (pattern (~and _:kw-lambda^
-            ([(i:id) e-rhs:opt-expr]) e-body:expr ...)
+             ((~and op let-values)
-           #:when (kw-lambda-property this-syntax)
+              ([(i:id) e-rhs:opt-expr]) e-body:expr ...))
            #:with opt (quasisyntax/loc/origin this-syntax #'op
                         (op ([(i) e-rhs.opt]) e-body ...)))
 

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

@@ -1,43 +1,55 @@
 #lang racket/base
-(require (for-syntax racket/base syntax/parse))
+(require
+  syntax/parse
+  (for-syntax racket/base syntax/parse racket/syntax))
 
-(define-syntax define-properties
+(define-syntax (define-properties stx)
-  (syntax-parser
+  (define-syntax-class clause
-    ((_ (name:id sym:id) ...)
+    (pattern (root:id sym:id)
-     (with-syntax (((symbol ...) (generate-temporaries #'(sym ...))))
+      #:with name (format-id #'root "~a-property" #'root)
+      #:with syntax-class-name (format-id #'root "~a^" #'root)
+      #:with symbol (generate-temporary #'sym)))
+
+  (syntax-parse stx
+    ((_ :clause ...)
      #`(begin
          (begin
            ;; TODO: make this an uninterned symbol once the phasing issue of the unit
            ;; tests is fixed
            (define symbol 'sym)
-             (provide name)
+           (provide name syntax-class-name)
            (define name
               (case-lambda
                 ((stx) (syntax-property stx symbol))
-                 ((stx value) (syntax-property stx symbol value))))) ...)))))
+                ((stx value) (syntax-property stx symbol value))))
+            (define-syntax-class syntax-class-name
+              #:attributes (value)
+              (pattern e
+               #:attr value (name #'e)
+               #:when (attribute value)))) ...))))
 
 ;;TODO add contracts on the properties
 ;;TODO make better interface for properties with values of only #t
 
 (define-properties
-  (plambda-property typechecker:plambda)
+  (plambda typechecker:plambda)
-  (ignore-property typechecker:ignore)
+  (ignore typechecker:ignore)
-  (ignore-some-property typechecker:ignore-some)
+  (ignore-some typechecker:ignore-some)
-  (contract-def/maker-property typechecker:contract-def/maker)
+  (contract-def/maker typechecker:contract-def/maker)
-  (contract-def-property typechecker:contract-def)
+  (contract-def typechecker:contract-def)
-  (flat-contract-def-property typechecker:flat-contract-def)
+  (flat-contract-def typechecker:flat-contract-def)
-  (external-check-property typechecker:external-check)
+  (external-check typechecker:external-check)
-  (with-type-property typechecker:with-type)
+  (with-type typechecker:with-type)
-  (type-ascription-property type-ascription)
+  (type-ascription type-ascription)
-  (type-inst-property type-inst)
+  (type-inst type-inst)
-  (type-label-property type-label)
+  (type-label type-label)
-  (type-dotted-property type-dotted)
+  (type-dotted type-dotted)
-  (exn-handler-property typechecker:exn-handler)
+  (exn-handler typechecker:exn-handler)
-  (exn-body-property typechecker:exn-body)
+  (exn-body typechecker:exn-body)
-  (with-handlers-property typechecker:with-handlers)
+  (with-handlers typechecker:with-handlers)
-  (struct-info-property struct-info)
+  (struct-info struct-info)
-  (opt-lambda-property opt-lambda)
+  (opt-lambda opt-lambda)
-  (kw-lambda-property kw-lambda)
+  (kw-lambda kw-lambda)
-  (tail-position-property typechecker:called-in-tail-position)
+  (tail-position typechecker:called-in-tail-position)
   )
 

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-annotation.rkt

@@ -7,6 +7,7 @@
          (except-in (types subtype union utils generalize))
          (private parse-type syntax-properties)
          (contract-req)
+         syntax/parse
          racket/match)
 
 (provide type-annotation
@@ -36,16 +37,12 @@
         (parse-type/id stx prop)))
   ;(unless let-binding (error 'ohno))
   ;(printf "in type-annotation:~a\n" (syntax->datum stx))
-  (cond
+  (syntax-parse stx
-    [(type-label-property stx) => pt]
+    [(~or v:type-label^ v:type-ascription^) (pt (attribute v.value))]
-    [(type-ascription-property stx) => pt]
+    [i:typed-id^
-    ;; this is so that : annotation works in internal def ctxts
-    [(and (identifier? stx) (lookup-type stx (lambda () #f)))
-     =>
-     (lambda (t)
      (maybe-finish-register-type stx)
-       t)]
+     (attribute i.type)]
-    [else #f]))
+    [_ #f]))
 
 ;(trace type-annotation)
 
@@ -55,30 +52,27 @@
     (if (syntax? prop)
         (parse-tc-results prop)
         (parse-tc-results/id stx prop)))
-  (cond
+  (syntax-parse stx
-    [(type-ascription-property stx)
+    [s:type-ascription^
-     =>
+     (let loop ((prop (attribute s.value)))
-     (lambda (prop)
-       (let loop ((prop prop))
        (if (pair? prop)
            (loop (cdr prop))
-             (pt prop))))]
+           (pt prop)))]
-    [else #f]))
+    [_ #f]))
 
 (define (remove-ascription stx)
   (type-ascription-property
     stx 
-    (cond
+    (syntax-parse stx
-      [(type-ascription-property stx)
+      [s:type-ascription^
-       =>
+       (define prop (attribute s.value))
-       (lambda (prop)
        (if (pair? prop)
            (let loop ((prop (cdr prop)) (last (car prop)))
              (if (pair? prop)
                  (cons last (loop (cdr prop) (car prop)))
                  last))
-               #f))]
+             #f)]
-      [else #f])))
+      [_ #f])))
 
 ;; get the type annotation of this identifier, otherwise error
 ;; if #:default is provided, return that instead of error
@@ -143,5 +137,6 @@
       (tc-error "Body had type:\n~a\nVariable had type:\n~a\n" e-type ty))))
 
 (define (dotted? stx)
-  (cond [(type-dotted-property stx) => syntax-e]
+  (syntax-parse stx
-        [else #f]))
+    [v:type-dotted^ (syntax-e (attribute v.value))]
+    [_ #f]))

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

@@ -19,6 +19,7 @@
  unstable/list
  unstable/sequence
  (contract-req)
+ (for-syntax racket/base syntax/parse racket/syntax)
  (for-template racket/base racket/contract racket/set (utils any-wrap)
                (prefix-in t: (types numeric-predicates))
                (only-in unstable/contract sequence/c)
@@ -27,25 +28,27 @@
 ;; These check if either the define form or the body form has the syntax
 ;; property. Normally the define form will have the property but lifting an
 ;; expression to the module level will put the property on the body.
-(define-values (typechecker:contract-def
+(define-syntax (contract-finders stx)
-                typechecker:flat-contract-def
+  (define-syntax-class clause
-                typechecker:contract-def/maker)
+    (pattern name:id
-  (let ()
+      #:with external-name (format-id #'name "typechecker:~a" #'name)
-    (define ((get-contract-def property) stx)
+      #:with syntax-class-name (format-id #'name "~a^" #'name)))
-      (or (property stx)
+  (syntax-parse stx
-          (syntax-case stx (define-values)
+    [(_ #:union union-name:id :clause ... )
-            ((define-values (name) body)
+     #'(begin
-             (property #'body))
+         (define external-name
-            (_ #f))))
+           (syntax-parser
-    (values
+              #:literal-sets (kernel-literals)
-      (get-contract-def contract-def-property)
+              [(~or (~var v syntax-class-name)
-      (get-contract-def flat-contract-def-property)
+                    (define-values (_) (~var v syntax-class-name)))
-      (get-contract-def contract-def/maker-property))))
+               (attribute v.value)]
+              [_ #f])) ...
+         (define (union-name stx)
+           (or (external-name stx) ...)))]))
 
-(define (define/fixup-contract? stx)
+(contract-finders
-  (or (typechecker:contract-def stx)
+  #:union define/fixup-contract?
-      (typechecker:flat-contract-def stx)
+  contract-def flat-contract-def contract-def/maker)
-      (typechecker:contract-def/maker stx)))
 
 ;; type->contract-fail : Syntax Type #:ctc-str String
 ;;                       -> #:reason (Option String) -> Void

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

@@ -54,21 +54,18 @@
   (let loop ([form form])
     (parameterize ([current-orig-stx form])
       (syntax-parse form
-        [stx
         ;; if this needs to be checked
-         #:when (with-type-property form)
+        [stx:with-type^
          ;; the form should be already ascribed the relevant type
          (tc-expr form)]
-        [stx
         ;; this is a handler function
-         #:when (exn-handler-property form)
+        [stx:exn-handler^
          (let ([t (single-value form)])
            (match t
              [(tc-result1: t)
               (set! handler-tys (cons (get-result-ty t) handler-tys))]))]
-        [stx
         ;; this is the body of the with-handlers
-         #:when (exn-body-property form)
+        [stx:exn-body^
          (set! body-stx form)
          (set! body-ty (tc-expr form))]
         [(a . b)
@@ -82,18 +79,15 @@
   (let loop ([form form])
     (parameterize ([current-orig-stx form])
       (syntax-parse form
-        [stx
         ;; if this needs to be checked
-         #:when (with-type-property form)
+        [stx:with-type^
          ;; the form should be already ascribed the relevant type
          (tc-expr form)]
-        [stx
         ;; this is a handler function
-         #:when (exn-handler-property form)
+        [stx:exn-handler^
          (tc-expr/check form (ret (-> (Un) (tc-results->values expected))))]
-        [stx
         ;; this is the body of the with-handlers
-         #:when (exn-body-property form)
+        [stx:exn-body^
          (tc-expr/check form expected)]
         [(a . b)
          (begin
@@ -107,9 +101,8 @@
 (define (check-subforms/ignore form)
   (let loop ([form form])
     (syntax-parse form
-      [stx
       ;; if this needs to be checked
-       #:when (with-type-property form)
+      [stx:with-type^
        ;; the form should be already ascribed the relevant type
        (void (tc-expr form))]
       [(a . b)

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

@@ -17,9 +17,7 @@
 
 
 (define-syntax-class annotated-op
-  (pattern i:identifier
+  (pattern (~and i:identifier (~or :type-inst^ :type-ascription^))))
-           #:when (or (type-inst-property #'i) 
-                      (type-ascription-property #'i))))
 
 (define-tc/app-syntax-class (tc/app-annotated expected)
   ;; Just do regular typechecking if we have one of these.

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

@@ -180,11 +180,9 @@
     (syntax-parse form
       #:literal-sets (kernel-literals)
       #:literals (find-method/who)
-      [stx
+      [stx:with-handlers^
-       #:when (with-handlers-property form)
        (check-subforms/with-handlers/check form expected)]
-      [stx
+      [stx:ignore-some^
-       #:when (ignore-some-property form)
        (check-subforms/ignore form)
        ;; We trust ignore to be only on syntax objects objects that are well typed
        expected]
@@ -267,8 +265,7 @@
                    (#%plain-app _ _ _arg-var2 ...))))))
        (tc/send #'find-app #'rcvr #'meth #'(args ...) expected)]
       ;; kw function def
-      [(let-values ([(_) fun]) . body)
+      [(~and (let-values ([(f) fun]) . body) _:kw-lambda^)
-       #:when (syntax-property form 'kw-lambda)
        (match expected
          [(tc-result1: (and f (or (Function: _)
                                   (Poly: _ (Function: _)))))
@@ -277,13 +274,12 @@
           (tc-error/expr "Keyword functions must have function type, given ~a" expected)])
        expected]
       ;; opt function def
-      [(let-values ([(f) fun]) . body)
+      [(~and (let-values ([(f) fun]) . body) opt:opt-lambda^)
-       #:when (syntax-property form 'opt-lambda)
        (define conv-type
          (match expected
            [(tc-result1: fun-type)
             (match-define (list required-pos optional-pos)
-              (syntax-property form 'opt-lambda))
+                          (attribute opt.value))
             (opt-convert fun-type required-pos optional-pos)]
            [_ #f]))
        (match-define (tc-result1: returned-fun-type)
@@ -321,14 +317,12 @@
       #:literal-sets (kernel-literals)
       #:literals (#%app lambda find-method/who)
       ;;
-      [stx
+      [stx:with-handlers^
-       #:when (with-handlers-property form)
        (let ([ty (check-subforms/with-handlers form)])
          (unless ty
            (int-err "internal error: with-handlers"))
          ty)]
-      [stx
+      [stx:ignore-some^
-       #:when (ignore-some-property form)
        (check-subforms/ignore form)
        (ret Univ)]
       ;; explicit failure

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

@@ -87,18 +87,11 @@
           (tc-body/check body (erase-filter expected))
           (tc-body body)))))))
 
-(define (tc-expr/maybe-expected/t e name)
+(define (tc-expr/maybe-expected/t e names)
-  (define expecteds
+  (syntax-parse names
-    (map (lambda (stx) (lookup-type stx (lambda () #f))) name))
+    [(i:typed-id^ ...)
-  (define mk (if (and (pair? expecteds) (null? (cdr expecteds)))
+     (tc-expr/check e (-values (attribute i.type)))]
-                 car
+    [_ (tc-expr e)]))
-                 -values))
-  (define tcr
-    (if
-     (andmap values expecteds)
-     (tc-expr/check e (mk expecteds))
-     (tc-expr e)))
-  tcr)
 
 (define (tc/letrec-values namess exprs body form [expected #f])
   (let* ([names (stx-map syntax->list namess)]
@@ -206,11 +199,11 @@
 ;; say that this binding is only called in tail position
 (define ((tc-expr-t/maybe-expected expected) e)
   (syntax-parse e #:literals (#%plain-lambda)
-    [(#%plain-lambda () _)
+    [(~and (#%plain-lambda () _) _:tail-position^)
-     #:fail-unless (and expected (tail-position-property e)) #f
+     #:when expected
      (tc-expr/check e (ret (t:-> (tc-results->values expected))))]
-    [_
+    [_:tail-position^
-     #:fail-unless (and expected (tail-position-property e)) #f
+     #:when expected
      (tc-expr/check e expected)]
     [_ (tc-expr e)]))
 

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

@@ -59,8 +59,7 @@
       ;#:literal-sets (kernel-literals)
 
       ;; forms that are handled in other ways
-      [stx
+      [(~or _:ignore^ _:ignore-some^)
-       #:when (or (ignore-property form) (ignore-some-property form))
        (list)]
 
       [((~literal module) n:id spec ((~literal #%plain-module-begin) body ...))
@@ -116,29 +115,29 @@
 
       ;; values definitions
       [(define-values (var ...) expr)
-       (let* ([vars (syntax->list #'(var ...))])
+       (define vars (syntax->list #'(var ...)))
-         (cond
+       (syntax-parse vars
          ;; if all the variables have types, we stick them into the environment
-           [(andmap type-label-property vars)
+         [(v:type-label^ ...)
           (let ([ts (map (λ (x) (get-type x #:infer #f)) vars)])
             (for-each register-type-if-undefined vars ts)
             (map make-def-binding vars ts))]
          ;; if this already had an annotation, we just construct the binding reps
-           [(andmap (lambda (s) (lookup-type s (lambda () #f))) vars)
+         [(v:typed-id^ ...)
           (define top-level? (eq? (syntax-local-context) 'top-level))
           (for ([var (in-list vars)])
             (when (dict-has-key? unann-defs var)
               (free-id-table-remove! unann-defs var))
             (finish-register-type var top-level?))
-            (map (lambda (s) (make-def-binding s (lookup-type s))) vars)]
+          (stx-map make-def-binding #'(v ...) (attribute v.type))]
          ;; special case to infer types for top level defines
-           [else
+         [_
           (match (get-type/infer vars #'expr tc-expr tc-expr/check)
             [(tc-results: ts)
              (for/list ([i (in-list vars)] [t (in-list ts)])
                (register-type i t)
                (free-id-table-set! unann-defs i #t)
-                 (make-def-binding i t))])]))]
+               (make-def-binding i t))])])]
 
       ;; to handle the top-level, we have to recur into begins
       [(begin . rest)
@@ -164,13 +163,11 @@
     (syntax-parse form
       #:literal-sets (kernel-literals)
       ;; these forms we have been instructed to ignore
-      [stx
+      [stx:ignore^
-       #:when (ignore-property form)
        (void)]
 
       ;; this is a form that we mostly ignore, but we check some interior parts
-      [stx
+      [stx:ignore-some^
-       #:when (ignore-some-property form)
        (check-subforms/ignore form)]
 
       ;; these forms should always be ignored
@@ -185,13 +182,14 @@
       [(define-values () expr)
        (tc-expr/check #'expr (ret empty))]
       [(define-values (var ...) expr)
-       (unless (for/and ([v (in-syntax #'(var ...))])
+       #:when (for/and ([v (in-syntax #'(var ...))])
                 (free-id-table-ref unann-defs v (lambda _ #f)))
-         (let ([ts (stx-map lookup-type #'(var ...))])
+       (void)]
+      [(define-values (var:typed-id^ ...) expr)
+       (let ([ts (attribute var.type)])
          (when (= 1 (length ts))
            (add-scoped-tvars #'expr (lookup-scoped-tvars (stx-car #'(var ...)))))
-           (tc-expr/check #'expr (ret ts))))
+         (tc-expr/check #'expr (ret ts))) ]
-       (void)]
 
       ;; to handle the top-level, we have to recur into begins
       [(begin) (void)]
@@ -365,9 +363,9 @@
 ;; syntax -> (values #f (or/c void? tc-results/c))
 (define (tc-toplevel-form form)
   (syntax-parse form
-    [((~literal begin) e ...)
     ;; Don't open up `begin`s that are supposed to be ignored
-     #:when (not (or (ignore-property form) (ignore-some-property form)))
+    [(~and ((~literal begin) e ...)
+           (~not (~or _:ignore^ _:ignore-some^)))
      (define result
        (for/last ([form (in-syntax #'(e ...))])
          (define-values (_ result) (tc-toplevel-form form))