From adf34fd219843fa65c46d192c40b365110356581 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 20 May 2015 15:20:43 -0400
Subject: [PATCH] add errors for invalid types

---
 tapl/tests/rackunit-typechecking.rkt |  2 ++
 tapl/tests/stlc+lit-tests.rkt        | 17 +++++++++--------
 tapl/typecheck.rkt                   | 11 ++++++++---
 3 files changed, 19 insertions(+), 11 deletions(-)

diff --git a/tapl/tests/rackunit-typechecking.rkt b/tapl/tests/rackunit-typechecking.rkt
index 77ba8b9..e7a6bce 100644
--- a/tapl/tests/rackunit-typechecking.rkt
+++ b/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 
diff --git a/tapl/tests/stlc+lit-tests.rkt b/tapl/tests/stlc+lit-tests.rkt
index 253dc3e..36004c6 100644
--- a/tapl/tests/stlc+lit-tests.rkt
+++ b/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)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 31ef5cd..adafa79 100644
--- a/tapl/typecheck.rkt
+++ b/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 τ))