diff --git a/stlc-tests.rkt b/stlc-tests.rkt
index 5113568..7160328 100644
--- a/stlc-tests.rkt
+++ b/stlc-tests.rkt
@@ -125,4 +125,15 @@
 (check-type-and-result 
  (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolCons #f (BoolNull)))
  : IntList => (Cons 1 (Null)))
-(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
\ No newline at end of file
+(check-not-type (map/BoolList (λ ([b : Bool]) (if b 0 1)) (BoolNull)) : BoolList)
+;; check typename is available
+(check-type (λ ([lst : IntList]) 
+              (cases lst
+                [Null () (None)]
+                [Cons (x xs) (Just x)]))
+            : (→ IntList MaybeInt))
+(check-type ((λ ([lst : IntList]) 
+              (cases lst
+                [Null () (None)]
+                [Cons (x xs) (Just x)]))
+             (Null)) : MaybeInt)
\ No newline at end of file
diff --git a/stlc.rkt b/stlc.rkt
index 06da1af..74feac0 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -201,7 +201,8 @@
      #:when (or (null? (syntax->list #'(τ_result ...)))
                 (andmap (λ (τ) (type=? τ (car (syntax->list #'(τ_result ...)))))
                         (cdr (syntax->list #'(τ_result ...)))))
-     #`(match e+ [(Cons+ x+ ...) body+ ... body_result+] ...)]))
+     (⊢ (syntax/loc stx (match e+ [(Cons+ x+ ...) body+ ... body_result+] ...))
+        (car (syntax->list #'(τ_result ...))))]))
 
 ;; typed forms ----------------------------------------------------------------
 (define-syntax (datum/tc stx)