add define-type-alias, changes:

- types must be expanded (with manual handling of #%app)
- type constructors must be prefix
- base types and constructors must be run time identifiers

tapl/README.md

@@ -0,0 +1,9 @@
+extension hierarchy
+
+A file2 that is immediately below a file1 extends that file1.
+
+1) stlc.rkt
+2) stlc+lit.rkt
+3) ext-stlc.rkt
+4) stlc+tup.rkt
+5) stlc+var.rkt

tapl/ext-stlc.rkt

@@ -37,12 +37,12 @@
     [(_ . s:str) (⊢ (syntax/loc stx (#%datum . s)) #'String)]
     [(_ . x) #'(stlc:#%datum . x)]))
 
-(define-primop zero? : (Int → Bool))
-(define-primop = : (Int Int → Bool))
-(define-primop - : (Int Int → Int))
-(define-primop add1 : (Int → Int))
-(define-primop sub1 : (Int → Int))
-(define-primop not : (Bool → Bool))
+(define-primop zero? : (→ Int Bool))
+(define-primop = : (→ Int Int Bool))
+(define-primop - : (→ Int Int Int))
+(define-primop add1 : (→ Int Int))
+(define-primop sub1 : (→ Int Int))
+(define-primop not : (→ Bool Bool))
 
 (define-syntax (and/tc stx)
   (syntax-parse stx

tapl/notes.txt

@@ -0,0 +1,27 @@
+macro system requirements:
+- depth-first expansion, i.e., localexpand, and stop-lists
+- language form hooks, e.g., #%app, etc
+- literal types, e.g. integer syntax class, ie compile time literal type tag
+- identifiers and free-identifier=?
+- syntax-parse or other pattern matching
+
+Type constructors must be prefix (and not infix) and must be functions
+- because in order to support type aliases:
+  - types must be expanded,
+  - and having a macro identifier (ie, an alias) in the function position
+    makes the expander error (constructor is ok bc it is run time identifier)
+
+Type expansion problem: what to do about #%app?
+1) use the #%app in scope: 
+  - may do type checking and error bc types dont have types
+2) use the racket #%app:
+  - may work but how to do this without ruining context of other
+   identifiers (ie types)
+Solution: do #1, but
+1) stop at the #%app
+2) manually drop it and continue expanding rest
+
+Types must be identifiers, but not macros
+- cannot be macros if we want to use expansion for type aliases
+  - because then what does a base type like Int expand to?
+  - if we define Int as a runtime identifier, then expansion will stop at Int

tapl/stlc+lit.rkt

@@ -20,7 +20,7 @@
 
 (define-base-type Int)
 
-(define-primop + : (Int Int → Int))
+(define-primop + : (→ Int Int Int))
 
 (define-syntax (datum/tc stx)
   (syntax-parse stx

tapl/stlc+tup.rkt

@@ -14,16 +14,18 @@
 ;; Terms:
 ;; - terms from ext-stlc.rkt
 
+(define-type-constructor ×)
+
 (define-syntax (tup stx)
   (syntax-parse stx
     [(_ e ...)
      #:with ((e- τ) ...) (infers+erase #'(e ...))
-     (⊢ #'(list e- ...) #'(τ ...))]))
+     (⊢ #'(list e- ...) #'(× τ ...))]))
 (define-syntax (proj stx)
   (syntax-parse stx
     [(_ tup n:integer)
      #:with (tup- τ_tup) (infer+erase #'tup)
-     #:fail-unless (not (identifier? #'τ_tup)) "not tuple type"
-     #:fail-unless (< (syntax->datum #'n) (stx-length #'τ_tup)) "proj index too large"
-     (⊢ #'(list-ref tup n) (stx-list-ref #'τ_tup (syntax->datum #'n)))]))
+     #:fail-unless (×? #'τ_tup) "not tuple type"
+     #:fail-unless (< (add1 (syntax->datum #'n)) (stx-length #'τ_tup)) "proj index too large"
+     (⊢ #'(list-ref tup n) (stx-list-ref #'τ_tup (add1 (syntax->datum #'n))))]))
    

tapl/stlc+var.rkt

@@ -14,6 +14,11 @@
 ;; Terms:
 ;; - terms from stlc+tup.rkt
 
-(provide Tmp Tmp2)
-(define-syntax Tmp (make-rename-transformer #'Int))
-(define-syntax Tmp2 (λ (stx) (syntax-parse stx [x:id #'(Int Int → Int)])))
+;(provide Integer)
+;(define-syntax Integer (make-rename-transformer #'Int))
+;(define-syntax Integer (λ (stx) (syntax-parse stx [x:id #'Int])))
+(define-type-alias Integer Int)
+;(provide ArithBinOp)
+; expanded form must have context of its use, so it has the proper #%app
+;(define-syntax ArithBinOp (λ (stx) (syntax-parse stx [x:id (datum->syntax #'x '(→ Int Int Int))])))
+(define-type-alias ArithBinOp (→ Int Int Int))

tapl/stlc.rkt

@@ -19,7 +19,7 @@
   (syntax-parse stx 
     [(_ (b:typed-binding ...) e)
      #:with (xs- e- τ_res) (infer/type-ctxt+erase #'(b ...) #'e)
-     (⊢ #'(λ xs- e-) #'(b.τ ... → τ_res))]))
+     (⊢ #'(λ xs- e-) #'(→ b.τ ... τ_res))]))
 
 (define-syntax (app/tc stx)
   (syntax-parse stx #:literals (→)
@@ -28,7 +28,7 @@
      #:fail-unless (→? #'τ_fn)
                    (format "Type error: Attempting to apply a non-function ~a with type ~a\n"
                            (syntax->datum #'e_fn) (syntax->datum #'τ_fn))
-     #:with (τ ... → τ_res) #'τ_fn
+     #:with (→ τ ... τ_res) #'τ_fn
      #:with ((e_arg- τ_arg) ...) (infers+erase #'(e_arg ...))
      #:fail-unless (types=? #'(τ ...) #'(τ_arg ...))
                    (string-append

tapl/tests/ext-stlc-tests.rkt

@@ -7,7 +7,7 @@
 (check-type "one" : String) ; literal now supported
 (check-type #f : Bool) ; literal now supported
 
-(check-type (λ ([x : Bool]) x) : (Bool → Bool)) ; Bool is now valid type
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
 
 ;; Unit
 (check-type (void) : Unit)
@@ -45,7 +45,7 @@
 
 ;; recursive
 (check-type
- (letrec ([(countdown : (Int → String))
+ (letrec ([(countdown : (→ Int String))
            (λ ([i : Int])
              (if (= i 0)
                  "liftoff"
@@ -54,11 +54,11 @@
 
 ;; mutually recursive
 (check-type
- (letrec ([(is-even? : (Int → Bool))
+ (letrec ([(is-even? : (→ Int Bool))
            (λ ([n : Int])
              (or (zero? n)
                  (is-odd? (sub1 n))))]
-          [(is-odd? : (Int → Bool))
+          [(is-odd? : (→ Int Bool))
            (λ ([n : Int])
              (and (not (zero? n))
                   (is-even? (sub1 n))))])
@@ -70,19 +70,19 @@
 ;(check-not-type 1 : (Int → Int))
 ;(typecheck-fail "one") ; literal now supported
 ;(typecheck-fail #f) ; literal now supported
-(check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int))
+(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) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now 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)
+(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))) ; adding non-Int
-(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be 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/tests/stlc+lit-tests.rkt

@@ -2,21 +2,21 @@
 (require "rackunit-typechecking.rkt")
 
 (check-type 1 : Int)
-;(check-not-type 1 : (Int → Int))
+(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-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) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 (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)
+(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))) ; adding non-Int
-(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be 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/tests/stlc+tup-tests.rkt

@@ -2,12 +2,12 @@
 (require "rackunit-typechecking.rkt")
 
 ;; tests for tuples
-(check-type (tup 1 2 3) : (Int Int Int))
-(check-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Unit String Bool (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Int Unit Bool (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Int String Unit (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Unit)))
+(check-type (tup 1 2 3) : (× Int Int Int))
+(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
 
 (check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
 (check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
@@ -22,7 +22,7 @@
 (check-type "one" : String) ; literal now supported
 (check-type #f : Bool) ; literal now supported
 
-(check-type (λ ([x : Bool]) x) : (Bool → Bool)) ; Bool is now valid type
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
 
 ;; Unit
 (check-type (void) : Unit)
@@ -60,7 +60,7 @@
 
 ;; recursive
 (check-type
- (letrec ([(countdown : (Int → String))
+ (letrec ([(countdown : (→ Int String))
            (λ ([i : Int])
              (if (= i 0)
                  "liftoff"
@@ -69,11 +69,11 @@
 
 ;; mutually recursive
 (check-type
- (letrec ([(is-even? : (Int → Bool))
+ (letrec ([(is-even? : (→ Int Bool))
            (λ ([n : Int])
              (or (zero? n)
                  (is-odd? (sub1 n))))]
-          [(is-odd? : (Int → Bool))
+          [(is-odd? : (→ Int Bool))
            (λ ([n : Int])
              (and (not (zero? n))
                   (is-even? (sub1 n))))])
@@ -85,19 +85,19 @@
 ;(check-not-type 1 : (Int → Int))
 ;(typecheck-fail "one") ; literal now supported
 ;(typecheck-fail #f) ; literal now supported
-(check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int))
+(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) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now 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)
+(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))) ; adding non-Int
-(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be 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/tests/stlc+var-tests.rkt

@@ -1,15 +1,19 @@
 #lang s-exp "../stlc+var.rkt"
 (require "rackunit-typechecking.rkt")
 
-(check-type ((λ ([x : Tmp]) (+ x 2)) 3) : Tmp)
+(check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer)
+(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int)
+(check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer)
+(check-type + : ArithBinOp)
+(check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int))
 
 ;; tests for tuples -----------------------------------------------------------
-(check-type (tup 1 2 3) : (Int Int Int))
-(check-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Unit String Bool (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Int Unit Bool (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Int String Unit (Int Int → Int)))
-(check-not-type (tup 1 "1" #f +) : (Int String Bool (Int Int → Unit)))
+(check-type (tup 1 2 3) : (× Int Int Int))
+(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int)))
+(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit)))
 
 (check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1)
 (check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2")
@@ -24,7 +28,7 @@
 (check-type "one" : String) ; literal now supported
 (check-type #f : Bool) ; literal now supported
 
-(check-type (λ ([x : Bool]) x) : (Bool → Bool)) ; Bool is now valid type
+(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
 
 ;; Unit
 (check-type (void) : Unit)
@@ -62,7 +66,7 @@
 
 ;; recursive
 (check-type
- (letrec ([(countdown : (Int → String))
+ (letrec ([(countdown : (→ Int String))
            (λ ([i : Int])
              (if (= i 0)
                  "liftoff"
@@ -71,11 +75,11 @@
 
 ;; mutually recursive
 (check-type
- (letrec ([(is-even? : (Int → Bool))
+ (letrec ([(is-even? : (→ Int Bool))
            (λ ([n : Int])
              (or (zero? n)
                  (is-odd? (sub1 n))))]
-          [(is-odd? : (Int → Bool))
+          [(is-odd? : (→ Int Bool))
            (λ ([n : Int])
              (and (not (zero? n))
                   (is-even? (sub1 n))))])
@@ -87,19 +91,19 @@
 ;(check-not-type 1 : (Int → Int))
 ;(typecheck-fail "one") ; literal now supported
 ;(typecheck-fail #f) ; literal now supported
-(check-type (λ ([x : Int] [y : Int]) x) : (Int Int → Int))
+(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) : (→ Int Int))
+(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type
 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now 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)
+(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))) ; adding non-Int
-(typecheck-fail (λ ([x : (Int → Int)]) (+ x x))) ; x should be 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/tests/stlc-tests.rkt

@@ -1,4 +1,4 @@
 #lang s-exp "../stlc.rkt"
-(require "typecheck-testing.rkt")
+(require "rackunit-typechecking.rkt")
 
 ;; cannot have tests without base types

tapl/typecheck.rkt

@@ -26,9 +26,11 @@
      #:with τ? (format-id #'τ "~a?" #'τ)
      #'(begin
          (provide τ (for-syntax τ?))
-         (define-syntax (τ stx)
+         #;(define-syntax (τ stx)
            (syntax-parse stx
-             [_ (error 'Int "Cannot use type at run time.")]))
+;             [_ #'(error 'Int "Cannot use type at run time.")]))
+             [_ #'τ]))
+         (define τ (void) #;(error 'Int "Cannot use type at run time."))
          (define-for-syntax (τ? τ1)
            (type=? τ1 #'τ)))]))
 
@@ -38,9 +40,11 @@
      #:with τ? (format-id #'τ "~a?" #'τ)
      #'(begin
          (provide τ (for-syntax τ?))
-         (define-syntax (τ stx)
+         #;(define-syntax (τ stx)
            (syntax-parse stx
-             [_ (error 'Int "Cannot use type at run time.")]))
+;             [_ #'(error 'Int "Cannot use type at run time.")]))
+             [_ #'τ]))
+         (define τ (void))
          (define-for-syntax (τ? stx)
            (syntax-parse stx
              [(τ_arg (... ...))
@@ -48,20 +52,20 @@
                 (type=? #'τ id))]
              [_ #f]))
          )]))
-;(define-syntax (define-constant-type stx)
-;  (syntax-parse stx
-;    [(_ τ:id)
-;     #:with constructor
-;            (datum->syntax #'τ (string->symbol (string-downcase (symbol->string (syntax>datum #'τ)))))
-;     #:with const-name
-;            (generate-temporary #'constructor)
-;     #'(begin
-;         (provide τ constructor)
-;         (struct
-;         (define-syntax (τ stx)
-;           (syntax-parse stx
-;             [_ (error 'Int "Cannot use type at run time.")])))]))
 
+(define-syntax (define-type-alias stx)
+  (syntax-parse stx
+    [(_ τ:id τ-expanded)
+     #`(begin
+         (provide τ)
+         #,(if (identifier? #'τ-expanded)
+               #'(define-syntax τ (make-rename-transformer #'τ-expanded))
+               #'(define-syntax τ
+                   (λ (stx)
+                     (syntax-parse stx
+                       ; τ-expanded must have the context of its use, not definition
+                       ; so the appropriate #%app is used
+                       [x:id (datum->syntax #'x 'τ-expanded)])))))]))
 ;; type classes
 (begin-for-syntax
   (define (errmsg:bad-type τ)
@@ -112,7 +116,7 @@
 
   (define (infer+erase e)
     (define e+ (expand/df e))
-    (list e+ (typeof e+)))
+    (list e+ (eval-τ (typeof e+))))
   (define (infers+erase es)
     (stx-map infer+erase es))
   (define (types=? τs1 τs2)
@@ -138,9 +142,27 @@
   #;(define (assert-types es τs)
     (stx-andmap assert-type es τs))
 
+  (define (eval-τ τ)
+    (define app (datum->syntax τ '#%app)) ; #%app in τ's ctxt
+    ;; stop right before expanding #%app
+    (define maybe-app-τ (local-expand τ 'expression (list app)))
+    ;; manually remove app and recursively expand
+    (if (identifier? maybe-app-τ) ; base type
+        maybe-app-τ
+        (syntax-parse maybe-app-τ
+          [(τ ...)
+           #:with (τ-exp ...) (stx-map eval-τ #'(τ ...))
+           #'(τ-exp ...)])))
+  
   ;; type=? : Type Type -> Boolean
   ;; Indicates whether two types are equal
-  (define (type=? τ1 τ2)
+  (define (type=? τa τb)
+    ;; expansion, and thus eval-τ is idempotent,
+    ;; so should be ok to expand even if τa or τb are already expanded
+    (define τ1 (eval-τ τa))
+    (define τ2 (eval-τ τb))
+;    (printf "t1: ~a => ~a\n" (syntax->datum τa) (syntax->datum τ1))
+;    (printf "t2: ~a => ~a\n" (syntax->datum τb) (syntax->datum τ2))
     (syntax-parse #`(#,τ1 #,τ2)
       ; → should not be datum literal;
       ; adding a type constructor should extend type equality