From 4420f6cd7447b86fef8aae972135ea78f4546785 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Fri, 17 May 2019 16:13:05 -0400
Subject: [PATCH] improve handling of type variables

---
 racket/typed/core-types.rkt        | 10 +++++++++-
 racket/typed/tests/expressions.rkt | 14 ++++++++++++++
 2 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index c49cdb1..ade8952 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -773,6 +773,7 @@
   (current-typecheck-relation <:))
 
 ;; Flat-Type Flat-Type -> Type
+;; Intersection
 (define-for-syntax (∩ t1 t2)
   (unless (and (flat-type? t1) (flat-type? t2))
     (error '∩ "expected two flat-types"))
@@ -785,6 +786,9 @@
      (type-eval #`(U #,@(stx-map (lambda (t) (∩ t t2)) #'(τ1 ...))))]
     [(_ (~U* τ2:type ...))
      (type-eval #`(U #,@(stx-map (lambda (t) (∩ t1 t)) #'(τ2 ...))))]
+    [(X:id Y:id)
+     #:when (free-identifier=? #'X #'Y)
+     #'X]
     [((~AssertionSet τ1) (~AssertionSet τ2))
      #:with τ12 (∩ #'τ1 #'τ2)
      (type-eval #'(AssertionSet τ12))]
@@ -814,9 +818,10 @@
 ;; first type is the contents of the set/dataspace
 ;; second type is the type of a pattern
 (define-for-syntax (project-safe? t1 t2)
+  ;; TODO - not sure how to handle type variables
   (define (project-safe* t1 t2)
     (syntax-parse #`(#,t1 #,t2)
-      [(_ (~Bind τ2:type))
+      [(_ (~Bind τ2))
        (and (finite? t1) (<: t1 #'τ2))]
       [(_ ~Discard)
        #t]
@@ -850,6 +855,9 @@
     [~★/t #f]
     [(~U* τ:type ...)
      (stx-andmap finite? #'(τ ...))]
+    ;; TODO - this is questionable. maybe need a kind for assertions?
+    [X:id
+     #t]
     [(~Base _) #t]
     [(~Any/bvs τ-cons () τ ...)
      (stx-andmap finite? #'(τ ...))]))
diff --git a/racket/typed/tests/expressions.rkt b/racket/typed/tests/expressions.rkt
index 8630d2e..3deb30d 100644
--- a/racket/typed/tests/expressions.rkt
+++ b/racket/typed/tests/expressions.rkt
@@ -53,3 +53,17 @@
             : Int
             ⇒ 43)
 
+;; test type variable scoping
+
+(define (∀ (X) (id4 [x : X] -> X))
+  (match x
+    [(bind y X) y]))
+
+(check-type ((inst id2 String) "shelly flowers")
+            : String
+            ⇒ "shelly flowers")
+(define id5
+  (Λ [τ]
+     (lambda ([x : τ])
+       (match x
+         [(bind y τ) y]))))