fix typecheck-fail to use check-exn correctly and fix all the broken tests

tapl/stlc+reco+var.rkt

@@ -84,7 +84,7 @@
     [any
      (type-error #:src #'any
                  #:msg (string-append
-                        "Improper usage of type constructor ∨: ~a,"
+                        "Improper usage of type constructor ∨: ~a, "
                         "expected (∨ [label:id : τ:type] ...+)")
                  #'any)]))
 (begin-for-syntax

tapl/tests/exist-tests.rkt

@@ -179,11 +179,11 @@
 (typecheck-fail
  (pack (Int 1) as Int)
  #:with-msg
- "Expected type of expression to match pattern \\(∃ \\(\\(X)) τ_body), got: Int")
+ "Expected ∃ type, got: Int")
 (typecheck-fail
  (open ([(X x) <= 2]) 3)
  #:with-msg
- "Expected type of expression to match pattern \\(∃ \\(\\(X)) τ_body), got: Int")
+ "Expected expression 2 to have ∃ type, got: Int")
 
 ;; previous tets from stlc+reco+var-tests.rkt ---------------------------------
 ;; define-type-alias

tapl/tests/rackunit-typechecking.rkt

@@ -70,26 +70,19 @@
      #:with msg:str 
             (eval-syntax (datum->syntax #'here (syntax->datum #'msg-pat)))
      #:when (with-check-info*
-             (list (make-check-location (build-source-location-list stx)))
+             (list (make-check-expected (syntax-e #'msg))
+                   (make-check-expression (syntax->datum stx))
+                   (make-check-location (build-source-location-list stx))
+                   (make-check-name 'typecheck-fail)
+                   (make-check-params (list (syntax->datum #'e) (syntax-e #'msg))))
              (λ ()
                (check-exn
-                (λ (ex) (or (exn:fail? ex) (exn:test:check? ex)))
+                (λ (ex)
+                  (and (or (exn:fail? ex) (exn:test:check? ex))
+                       ; check err msg matches
+                       (regexp-match? (syntax-e #'msg) (exn-message ex))))
                 (λ ()
-                  (with-handlers
-                      ; check err msg matches
-                      ([exn:fail?
-                        (λ (ex)
-                          (unless (regexp-match? (syntax-e #'msg) (exn-message ex))
-                            (printf
-                             (string-append
-                              "ERROR-MSG ERROR: wrong err msg produced by expression ~v:\n"
-                              "EXPECTED:\nmsg matching pattern ~v,\nGOT:\n~v\n")
-                             (syntax->datum #'e) (syntax-e #'msg) (exn-message ex)))
-                          (raise ex))])
-                    (expand/df #'e)))
-                (format
-                 "Expected type check failure but expression ~a has valid type, OR wrong err msg received."
-                 (syntax->datum #'e)))))
+                  (expand/df #'e)))))
      #'(void)]))
 
 (define-syntax (check-runtime-exn stx)

tapl/tests/stlc+box-tests.rkt

@@ -18,19 +18,19 @@
 (typecheck-fail
  (λ ([lst : (Ref Int Int)]) lst)
  #:with-msg
- "Improper usage of type constructor Ref: \\(Ref Int Int), expected pattern \\(Ref τ)")
+ "Improper usage of type constructor Ref: \\(Ref Int Int\\), expected = 1 arguments")
 (typecheck-fail
  (λ ([lst : (Ref)]) lst)
  #:with-msg
- "Improper usage of type constructor Ref: \\(Ref), expected pattern \\(Ref τ)")
+ "Improper usage of type constructor Ref: \\(Ref\\), expected = 1 arguments")
 (typecheck-fail
  (deref 1)
  #:with-msg
- "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
+ "Expected expression 1 to have Ref type, got: Int")
 (typecheck-fail
  (:= 1 1)
  #:with-msg
- "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
+ "Expected expression 1 to have Ref type, got: Int")
 
 ;; previous tests: ------------------------------------------------------------
 (typecheck-fail (cons 1 2))

tapl/tests/stlc+cons-tests.rkt

@@ -2,7 +2,7 @@
 (require "rackunit-typechecking.rkt")
 
 (typecheck-fail (cons 1 2)
-                #:with-msg "Expected type with pattern: \\(List τ)")
+                #:with-msg "Expected expression 2 to have List type, got: Int")
 ;(typecheck-fail (cons 1 nil)
 ;                #:with-msg "nil: requires type annotation")
 (check-type (cons 1 nil) : (List Int))
@@ -15,15 +15,15 @@
 (typecheck-fail
  (nil (Int))
  #:with-msg
- "Improperly formatted type annotation: \\(Int); should have shape {τ}, where τ is a valid type.")
+ "Improperly formatted type annotation: \\(Int\\); should have shape {τ}, where τ is a valid type.")
 (typecheck-fail
  (λ ([lst : (List Int Int)]) lst)
  #:with-msg
- "Improper usage of type constructor List: \\(List Int Int), expected pattern \\(List τ)")
+ "Improper usage of type constructor List: \\(List Int Int\\), expected = 1 arguments")
 (typecheck-fail
  (λ ([lst : (List)]) lst)
  #:with-msg
- "Improper usage of type constructor List: \\(List), expected pattern \\(List τ)")
+ "Improper usage of type constructor List: \\(List\\), expected = 1 arguments")
 ;; passes bc ⇒-rhs is only used for its runtime value
 (check-type (nil {Int}) : (List Int) ⇒ (nil {Bool}))
 (check-not-type (nil {Bool}) : (List Int))
@@ -35,7 +35,7 @@
 (typecheck-fail
  (isnil (head fn-lst))
  #:with-msg
- "Expected type of expression \\(head fn-lst) to match pattern \\(List τ), got: \\(→ Int Int)")
+ "Expected expression \\(head fn-lst\\) to have List type, got: \\(→ Int Int\\)")
 (check-type (isnil (tail fn-lst)) : Bool ⇒ #t)
 (check-type (head fn-lst) : (→ Int Int))
 (check-type ((head fn-lst) 25) : Int ⇒ 35)
@@ -45,7 +45,7 @@
 (typecheck-fail
  (cons 1 1)
  #:with-msg
- "Expected type of expression to match pattern \\(List τ), got: Int")
+ "Expected expression 1 to have List type, got: Int")
 
 ;; previous tests: ------------------------------------------------------------
 ;; define-type-alias

tapl/tests/stlc+effect-tests.rkt

@@ -24,19 +24,19 @@
 (typecheck-fail
  (λ ([lst : (Ref Int Int)]) lst)
  #:with-msg
- "Improper usage of type constructor Ref: \\(Ref Int Int), expected pattern \\(Ref τ)")
+ "Improper usage of type constructor Ref: \\(Ref Int Int\\), expected = 1 arguments")
 (typecheck-fail
  (λ ([lst : (Ref)]) lst)
  #:with-msg
- "Improper usage of type constructor Ref: \\(Ref), expected pattern \\(Ref τ)")
+ "Improper usage of type constructor Ref: \\(Ref\\), expected = 1 arguments")
 (typecheck-fail
  (deref 1)
  #:with-msg
- "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
+ "Expected Ref type, got: Int")
 (typecheck-fail
  (:= 1 1)
  #:with-msg
- "Expected type of expression.+to match pattern \\(Ref τ), got: Int")
+ "Expected Ref type, got: Int")
 
 ;; previous tests: ------------------------------------------------------------
 (typecheck-fail (cons 1 2))

tapl/tests/stlc+lit-tests.rkt

@@ -22,7 +22,7 @@
  #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
 (typecheck-fail
  (λ ([x : (→)]) x)
- #:with-msg "Improper usage of type constructor →: \\(→), expected >= 1 arguments")
+ #:with-msg "Improper usage of type constructor →: \\(→\\), expected >= 1 arguments")
 
 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)

tapl/tests/stlc+rec-iso-tests.rkt

@@ -56,11 +56,11 @@
 (typecheck-fail
  (fld {Int} 1)
  #:with-msg
- "Expected type of expression to match pattern \\(μ \\(\\(tv)) τ_body), got: Int")
+ "Expected μ type, got: Int")
 (typecheck-fail
  (unfld {Int} 1)
  #:with-msg
- "Expected type of expression to match pattern \\(μ \\(\\(tv)) τ_body), got: Int")
+ "Expected μ type, got: Int")
 
 ;; previous stlc+var tests ----------------------------------------------------
 ;; define-type-alias
@@ -157,7 +157,7 @@
 (typecheck-fail
  (proj 1 2)
  #:with-msg
- "Expected type of expression 1 to match pattern \\(× τ ...), got: Int")
+ "Expected expression 1 to have × type, got: Int")
 
 ;; ext-stlc.rkt tests ---------------------------------------------------------
 ;; should still pass

tapl/tests/stlc+reco+var-tests.rkt

@@ -109,25 +109,25 @@
  "Expected expression 1 to have ∨ type, got: Int")
 (typecheck-fail
  (λ ([x : (∨)]) x)
- #:with-msg "Improper usage of type constructor ∨: \\(∨), expected \\(∨ [label:id : τ:type] ...+)")
+ #:with-msg "Improper usage of type constructor ∨: \\(∨\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
 (typecheck-fail
  (λ ([x : (∨ 1)]) x)
- #:with-msg "Improper usage of type constructor ∨: \\(∨ 1\\), expected \\(∨ [label:id : τ:type] ...+)")
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ 1\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
 (typecheck-fail
  (λ ([x : (∨ [1 2])]) x)
- #:with-msg "Improper usage of type constructor ∨: \\(∨ (1 2)), expected \\(∨ [label:id : τ:type] ...+)")
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(1 2\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
 (typecheck-fail
  (λ ([x : (∨ [a 2])]) x)
- #:with-msg "Improper usage of type constructor ∨: \\(∨ (a 2)), expected \\(∨ [label:id : τ:type] ...+)")
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a 2\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
 (typecheck-fail
  (λ ([x : (∨ [a Int])]) x)
- #:with-msg "Improper usage of type constructor ∨: \\(∨ (a Int)), expected \\(∨ [label:id : τ:type] ...+)")
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a Int\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
 (typecheck-fail
  (λ ([x : (∨ [1 : Int])]) x)
- #:with-msg "Improper usage of type constructor ∨: \\(∨ (1 : Int)), expected \\(∨ [label:id : τ:type] ...+)")
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(1 : Int\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
 (typecheck-fail
  (λ ([x : (∨ [a : 1])]) x)
- #:with-msg "Improper usage of type constructor ∨: \\(∨ (a : 1)), expected \\(∨ [label:id : τ:type] ...+)")
+ #:with-msg "Improper usage of type constructor ∨: \\(∨ \\(a : 1\\)\\), expected \\(∨ \\[label:id : τ:type\\] ...+\\)")
 
 ;; previous tuple tests: ------------------------------------------------------------
 ;; wont work anymore

tapl/tests/sysf-tests.rkt

@@ -27,7 +27,7 @@
 (typecheck-fail
  (inst 1 Int)
  #:with-msg
- "Expected type of expression to match pattern \\(∀ \\(\\(x ...)) body), got: Int")
+ "Expected expression 1 to have ∀ type, got: Int")
 
 ;; polymorphic arguments
 (check-type (Λ (t) (λ ([x : t]) x)) : (∀ (t) (→ t t)))

tapl/typecheck.rkt

@@ -139,7 +139,7 @@
 
 (define-syntax add-expected
   (syntax-parser
-    [(_ e τ) (add-expected-ty #'e #'τ)]))
+    [(_ e τ) (add-orig (add-expected-ty #'e #'τ) (get-orig #'e))]))
 (define-syntax pass-expected
   (syntax-parser
     [(_ e stx) (add-expected-ty #'e (get-expected-type #'stx))]))
@@ -219,9 +219,9 @@
             (format
              "~a (~a:~a): Expected expression ~s to have ~a type, got: ~a"
              (syntax-source #'e) (syntax-line #'e) (syntax-column #'e)
-             (syntax-parse #'e-
-               ['x (syntax-e #'x)]
-               [_ (syntax->datum #'e-)])
+             (if (has-orig? #'e-)
+                 (syntax->datum (get-orig #'e-))
+                 (syntax->datum #'e))
              'tycon (type->str #'τ_e))
             (syntax-parse #'τ_e
               [(τ-expander . args) #'(e- args)]
@@ -407,6 +407,8 @@
     (set-stx-prop/preserved stx 'orig (cons orig origs)))
   (define (get-orig τ)
     (car (reverse (or (syntax-property τ 'orig) (list τ)))))
+  (define (has-orig? stx)
+    (and (syntax-property stx 'orig) #true))
   (define (type->str ty)
     (define τ (get-orig ty))
     (cond