add errors for invalid types

tapl/tests/rackunit-typechecking.rkt

@@ -8,6 +8,7 @@
   (syntax-parse stx #:datum-literals (:)
     [(_ e : τ ⇒ v) #'(check-type-and-result e : τ ⇒ v)]
     [(_ e : τ-expected)
+     #:fail-unless (is-type? #'τ-expected) (errmsg:bad-type #'τ-expected)
      #:with e+ (expand/df #'e)
      #:with τ (typeof #'e+)
      #:fail-unless
@@ -21,6 +22,7 @@
 (define-syntax (check-not-type stx)
   (syntax-parse stx #:datum-literals (:)
     [(_ e : not-τ)
+     #:fail-unless (is-type? #'not-τ) (errmsg:bad-type #'not-τ)
      #:with e+ (expand/df #'e)
      #:with τ (typeof #'e+)
      #:fail-when 

tapl/tests/stlc+lit-tests.rkt

@@ -2,20 +2,21 @@
 (require "rackunit-typechecking.rkt")
 
 (check-type 1 : Int)
-(check-not-type 1 : Bool)
-(typecheck-fail "one")
-(typecheck-fail #f)
+;(check-not-type 1 : (Int → Int))
+(typecheck-fail "one") ; unsupported literal
+(typecheck-fail #f) ; unsupported literal
 (check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int))
 (check-not-type (λ ([x : Int]) x) : Int)
 (check-type (λ ([x : Int]) x) : (Int → Int))
 (check-type (λ ([f : (Int → Int)]) 1) : ((Int → Int) → Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
-;((λ ([x : Bool]) x) 1)
-;(λ ([x : Bool]) x)
-(typecheck-fail (λ ([f : Int]) (f 1 2)))
+(typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool is not valid type
+(typecheck-fail (λ ([x : Bool]) x)) ; Bool is not valid type
+(typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
 (check-type (λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y))
             : ((Int Int → Int) Int Int → Int))
 (check-type ((λ ([f : (Int Int → Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
-(typecheck-fail (+ 1 (λ ([x : Int]) x)))
-(typecheck-fail (λ ([x : (Int → Int)]) (+ x x)))
+(typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
+(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be Int
+(typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)

tapl/typecheck.rkt

@@ -47,10 +47,11 @@
 
 ;; type classes
 (begin-for-syntax
+  (define (errmsg:bad-type τ)
+    (format "~a is not a valid type" (syntax->datum τ)))
   (define-syntax-class typed-binding #:datum-literals (:)
-    (pattern [x:id : τ])
-    (pattern
-     any
+    (pattern [x:id : τ] #:fail-unless (is-type? #'τ) (errmsg:bad-type #'τ))
+    (pattern (~not [x:id : τ])
      #:with x #f
      #:with τ #f
      #:fail-when #t
@@ -58,6 +59,10 @@
              (syntax->datum #'any)))))
 
 (begin-for-syntax
+  (define (is-type? τ)
+    (if (identifier? τ)
+        (identifier-binding τ)
+        (stx-andmap is-type? τ)))
   ;; ⊢ : Syntax Type -> Syntax
   ;; Attaches type τ to (expanded) expression e.
 ;  (define (⊢ e τ) (syntax-property (quasisyntax/loc e #,e) 'type τ))