From 4dd2b66d2b1bfd2e024703f5607b4795a98f31e1 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 14 Oct 2015 14:55:12 -0400
Subject: [PATCH] generalize fomega ty= to avoid specific types; add tests

- fixes fomega bug where kind annotations were not being compared
- fix subst bug: must tranfer props (ie types) when replacing an id
- add exist tests to check proper subst in ty=
---
 tapl/fomega.rkt              | 18 ++++++++----------
 tapl/tests/exist-tests.rkt   | 10 ++++++++++
 tapl/tests/fomega-tests.rkt  |  6 ++++++
 tapl/tests/fomega2-tests.rkt |  3 +++
 tapl/typecheck.rkt           | 10 +++++-----
 5 files changed, 32 insertions(+), 15 deletions(-)

diff --git a/tapl/fomega.rkt b/tapl/fomega.rkt
index dbe2f88..f375f42 100644
--- a/tapl/fomega.rkt
+++ b/tapl/fomega.rkt
@@ -69,19 +69,16 @@
   (define (type=? t1 t2)
     (or (and (★? t1) (#%type? t2))
         (and (#%type? t1) (★? t2))
-        (and (syntax-parse (list t1 t2) #:datum-literals (:)
-               [((~∀ ([tv1 : k1]) tbody1)
-                 (~∀ ([tv2 : k2]) tbody2))
-                ((current-type=?) #'k1 #'k2)]
-               [_ #t])
-             (old-type=? t1 t2))))
+        (let ([k1 (typeof t1)][k2 (typeof t2)])
+          (and (or (and (not k1) (not k2))
+                   (and k1 k2 ((current-type=?) k1 k2)))
+               (old-type=? t1 t2)))))
   (current-type=? type=?)
   (current-typecheck-relation (current-type=?)))
 
 (define-typed-syntax Λ
   [(_ bvs:kind-ctx e)
-   #:with ((tv- ...) e- τ_e)
-          (infer/ctx+erase #'bvs #'e)
+   #:with ((tv- ...) e- τ_e) (infer/ctx+erase #'bvs #'e)
    (⊢ e- : (∀ ([tv- : bvs.kind] ...) τ_e))])
 
 (define-typed-syntax inst
@@ -100,10 +97,11 @@
 (define-typed-syntax tyλ
   [(_ bvs:kind-ctx τ_body)
    #:with (tvs- τ_body- k_body) (infer/ctx+erase #'bvs #'τ_body)
-   #:when ((current-kind?) #'k_body)
+   #:fail-unless ((current-kind?) #'k_body)
+                 (format "not a valid kind: ~a\n" (type->str #'k_body))
    (⊢ (λ tvs- τ_body-) : (⇒ bvs.kind ... k_body))])
 
-(define-typed-syntax tyapp #:export-as tyapp
+(define-typed-syntax tyapp
   [(_ τ_fn τ_arg ...)
    #:with [τ_fn- (k_in ... k_out)] (⇑ τ_fn as ⇒)
    #:with ([τ_arg- k_arg] ...) (infers+erase #'(τ_arg ...))
diff --git a/tapl/tests/exist-tests.rkt b/tapl/tests/exist-tests.rkt
index 1a98af0..452503e 100644
--- a/tapl/tests/exist-tests.rkt
+++ b/tapl/tests/exist-tests.rkt
@@ -7,6 +7,16 @@
 (check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X))
 (typecheck-fail (pack (Int #t) as (∃ (X) X)))
 
+(check-type (pack (Int (pack (Int 0) as (∃ (X) X))) as (∃ (Y) (∃ (X) X)))
+            : (∃ (Y) (∃ (X) X)))
+(check-type (pack (Int +) as (∃ (X) (→ X Int Int))) : (∃ (X) (→ X Int Int)))
+(check-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
+                  as (∃ (Y) (∃ (X) (→ X Y Int))))
+            : (∃ (Y) (∃ (X) (→ X Y Int))))
+(check-not-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int))))
+                      as (∃ (Y) (∃ (X) (→ X Y Int))))
+                : (∃ (X) (∃ (X) (→ X X Int))))
+
 ; cant typecheck bc X has local scope, and no X elimination form
 ;(check-type (open ([(X x) <= (pack (Int 0) as (∃ (X) X))]) x) : X) 
 
diff --git a/tapl/tests/fomega-tests.rkt b/tapl/tests/fomega-tests.rkt
index 24aec02..7b145b3 100644
--- a/tapl/tests/fomega-tests.rkt
+++ b/tapl/tests/fomega-tests.rkt
@@ -9,6 +9,12 @@
 (typecheck-fail (→ 1))
 (check-type 1 : Int)
 
+(typecheck-fail (tyλ ([x : ★]) 1) #:with-msg "not a valid kind: Int")
+
+(check-type (Λ ([X : ★]) (λ ([x : X]) x)) : (∀ ([X : ★]) (→ X X)))
+(check-not-type (Λ ([X : ★]) (λ ([x : X]) x)) :
+                (∀ ([X : (∀★ ★)]) (→ X X)))
+
 ;(check-type (∀ ([t : ★]) (→ t t)) : ★)
 (check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
 (check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
diff --git a/tapl/tests/fomega2-tests.rkt b/tapl/tests/fomega2-tests.rkt
index 7154f59..a3eeaec 100644
--- a/tapl/tests/fomega2-tests.rkt
+++ b/tapl/tests/fomega2-tests.rkt
@@ -9,6 +9,9 @@
 (typecheck-fail (→ 1))
 (check-type 1 : Int)
 
+;; this should error but it doesnt
+#;(λ ([x : ★]) 1)
+
 ;(check-type (∀ ([t : ★]) (→ t t)) : ★)
 (check-type (∀ ([t : ★]) (→ t t)) : (∀★ ★))
 (check-type (→ (∀ ([t : ★]) (→ t t)) (→ Int Int)) : ★)
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
index 6ebc9c1..164f33f 100644
--- a/tapl/typecheck.rkt
+++ b/tapl/typecheck.rkt
@@ -136,7 +136,9 @@
   
   ;; typeof : Syntax -> Type or #f
   ;; Retrieves type of given stx, or #f if input has not been assigned a type.
-  (define (typeof stx #:tag [tag 'type]) (syntax-property stx tag))
+  (define (typeof stx #:tag [tag 'type])
+    (define ty (syntax-property stx tag))
+    (if (cons? ty) (car ty) ty))
 
   ;; - infers type of e
   ;; - checks that type of e matches the specified type
@@ -457,9 +459,7 @@
                             (format "wrong number of type vars, expected ~a ~a" 'bvs-op 'bvs-n)
               #:fail-unless (op (stx-length #'args) n)
                             (format "wrong number of arguments, expected ~a ~a" 'op 'n)
-              #:with (bvs- τs- _)
-                     (infers/ctx+erase #'bvs #'args) ;#'([bv : #%kind] (... ...)) #'args
-;                                       #:expand (current-type-eval))
+              #:with (bvs- τs- _) (infers/ctx+erase #'bvs #'args)
                #:with (~! (~var _ kind) (... ...)) #'τs-
                #:with ([tv (~datum :) k_arg] (... ...)) #'bvs
 ;               #:with (k_arg+ (... ...)) (stx-map (current-type-eval) #'(k_arg (... ...)))
@@ -572,7 +572,7 @@
   ; subst τ for y in e, if (bound-id=? x y)
   (define (subst τ x e)
     (syntax-parse e
-      [y:id #:when (bound-identifier=? e x) τ]
+      [y:id #:when (bound-identifier=? e x) (syntax-track-origin τ #'y #'y)]
       [(esub ...)
        #:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1)) #'(esub ...))
        (syntax-track-origin #'(esub_subst ...) e x)]