check if valid type when instantiating a type alias; fixed #5

macrotypes/examples/ext-stlc.rkt

@@ -39,7 +39,7 @@
 (define-primop typed- - (→ Int Int Int))
 (define-primop typed* * : (→ Int Int Int))
 
-;; Using τ.norm leads to a "not valid type" error when file is compiled
+;; τ.norm in 1st case causes "not valid type" error when file is compiled
 (define-syntax define-type-alias
   (syntax-parser
     [(_ alias:id τ:type)
@@ -48,7 +48,9 @@
     [(_ (f:id x:id ...) ty)
      #'(define-syntax- (f stx)
          (syntax-parse stx
-           [(_ x ...) #'ty]))]))
+           [(_ x ...)
+            #:with τ:type #'ty
+            #'τ.norm]))]))
 
 (define-typed-syntax define
   [(_ x:id e)

macrotypes/examples/tests/ext-stlc-tests.rkt

@@ -1,6 +1,11 @@
 #lang s-exp "../ext-stlc.rkt"
 (require "rackunit-typechecking.rkt")
 
+;; tests for define-type-alias
+(define-type-alias (A X) (add1 X))
+
+(typecheck-fail (λ ([f : (A 1)]) f) #:with-msg "not a valid type")
+
 ;; tests for stlc extensions
 ;; new literals and base types
 (check-type "one" : String) ; literal now supported

turnstile/examples/ext-stlc.rkt

@@ -38,15 +38,18 @@
 (define-primop typed- - (→ Int Int Int))
 (define-primop typed* * : (→ Int Int Int))
 
-;; Using τ.norm leads to a "not valid type" error when file is compiled
+;; τ.norm in 1st case causes "not valid type" error when file is compiled
 (define-syntax define-type-alias
   (syntax-parser
-    [(define-type-alias alias:id τ:type)
-     #'(define-syntax alias (make-variable-like-transformer #'τ))]
-    [(define-type-alias (f:id x:id ...) ty)
-     #'(define-syntax (f stx)
+    [(_ alias:id τ:type)
+     #'(define-syntax- alias
+         (make-variable-like-transformer #'τ))]
+    [(_ (f:id x:id ...) ty)
+     #'(define-syntax- (f stx)
          (syntax-parse stx
-           [(_ x ...) #'ty]))]))
+           [(_ x ...)
+            #:with τ:type #'ty
+            #'τ.norm]))]))
 
 (define-typed-syntax define
   [(_ x:id : τ:type e:expr) ≫

turnstile/examples/tests/ext-stlc-tests.rkt

@@ -1,6 +1,11 @@
 #lang s-exp "../ext-stlc.rkt"
 (require "rackunit-typechecking.rkt")
 
+;; tests for define-type-alias
+(define-type-alias (A X) (add1 X))
+
+(typecheck-fail (λ ([f : (A 1)]) f) #:with-msg "not a valid type")
+
 ;; tests for stlc extensions
 ;; new literals and base types
 (check-type "one" : String) ; literal now supported