From 7999f1cc8c4e29e444ee1ff07924afa5ef1876c4 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 9 Dec 2015 17:30:11 -0500
Subject: [PATCH] stlc+cons: inference testing

---
 tapl/stlc+cons.rkt             | 7 +++++--
 tapl/tests/stlc+cons-tests.rkt | 5 +++--
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/tapl/stlc+cons.rkt b/tapl/stlc+cons.rkt
index 6ed26ea..73f3e80 100644
--- a/tapl/stlc+cons.rkt
+++ b/tapl/stlc+cons.rkt
@@ -14,11 +14,14 @@
 
 (define-typed-syntax nil
   [(_ ~! τi:type-ann) (⊢ null : (List τi.norm))]
+  ; minimal type inference
+  [ni:id #:with τ (syntax-property #'ni 'type) #:when (syntax-e #'τ) (⊢ null : (List τ))] 
   [_:id #:fail-when #t (error 'nil "requires type annotation") #'(void)])
 (define-typed-syntax cons
   [(_ e1 e2)
-   #:with (e1- τ1) (infer+erase #'e1)
-   #:with (e2- (τ2)) (⇑ e2 as List)
+   #:with [e1- τ1] (infer+erase #'e1)
+   #:with e2+ (syntax-property #'e2 'type #'τ1)
+   #:with (e2- (τ2)) (⇑ e2+ as List)
    #:when (typecheck? #'τ1 #'τ2)
    (⊢ (cons e1- e2-) : (List τ1))])
 (define-typed-syntax isnil
diff --git a/tapl/tests/stlc+cons-tests.rkt b/tapl/tests/stlc+cons-tests.rkt
index 7bd3e88..14f5316 100644
--- a/tapl/tests/stlc+cons-tests.rkt
+++ b/tapl/tests/stlc+cons-tests.rkt
@@ -3,8 +3,9 @@
 
 (typecheck-fail (cons 1 2)
                 #:with-msg "Expected type with pattern: \\(List τ)")
-(typecheck-fail (cons 1 nil)
-                #:with-msg "nil: requires type annotation")
+;(typecheck-fail (cons 1 nil)
+;                #:with-msg "nil: requires type annotation")
+(check-type (cons 1 nil) : (List Int))
 (check-type (cons 1 (nil {Int})) : (List Int))
 (typecheck-fail nil #:with-msg "nil: requires type annotation")
 (typecheck-fail