Make tc-literal deal with complicated expected types better.

Also fixes bug in literal heterogeneous vector typing.

Closes PR 13842.

pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-literal.rkt

@@ -3,7 +3,7 @@
 (require "../utils/utils.rkt"
          racket/match
          (typecheck signatures check-below)
-         (types abbrev numeric-tower utils subtype union generalize)
+         (types abbrev numeric-tower utils resolve subtype union generalize)
          (rep type-rep)
          (only-in (infer infer) restrict)
          (utils tc-utils stxclass-util)
@@ -76,7 +76,7 @@
     [i:regexp  -Regexp]
     [(~and i ()) (-val '())]
     [(i . r)
-     (match (and expected (restrict expected (-pair Univ Univ) 'orig))
+     (match (and expected (resolve (restrict expected (-pair Univ Univ) 'orig)))
        [(Pair: a-ty d-ty)
         (-pair
          (tc-literal #'i a-ty)
@@ -84,28 +84,30 @@
        [t 
         (-pair (tc-literal #'i) (tc-literal #'r))])]
     [(~var i (3d vector?))
-     (match (and expected (restrict expected (-vec Univ) 'orig))
+     (match (and expected (resolve (restrict expected -VectorTop 'orig)))
        [(Vector: t)
-        (make-Vector (apply Un
+        (make-Vector
-                            t ;; so that this isn't (Un) when we get no elems
+          (check-below
-                            (for/list ([l (in-vector (syntax-e #'i))])
+            (apply Un
-                              (tc-literal l t))))]
+              (for/list ([l (in-vector (syntax-e #'i))])
+                (tc-literal l t)))
+            t))]
        [(HeterogeneousVector: ts)
         (make-HeterogeneousVector
          (for/list ([l (in-vector (syntax-e #'i))]
                     [t (in-list ts)])
-           check-below (tc-literal l t) t))]
+           (check-below (tc-literal l t) t)))]
        [_ (make-HeterogeneousVector (for/list ([l (in-vector (syntax-e #'i))])
                                       (generalize (tc-literal l #f))))])]
     [(~var i (3d hash?))
-     (match expected
+     (match (and expected (resolve (restrict expected -HashTop 'orig)))
        [(Hashtable: k v)
         (let* ([h (syntax-e #'i)]
                [ks (hash-map h (lambda (x y) (tc-literal x k)))]
                [vs (hash-map h (lambda (x y) (tc-literal y v)))])
-          (check-below (apply Un ks) k)
+          (make-Hashtable
-          (check-below (apply Un vs) v)
+            (check-below (apply Un ks) k)
-          expected)]
+            (check-below (apply Un vs) v)))]
        [_ (let* ([h (syntax-e #'i)]
                  [ks (hash-map h (lambda (x y) (tc-literal x)))]
                  [vs (hash-map h (lambda (x y) (tc-literal y)))])

pkgs/typed-racket-pkgs/typed-racket-tests/tests/typed-racket/optimizer/tests/binary-nonzero-fixnum.rkt

@@ -1,6 +1,6 @@
 #;
 (
-TR opt: binary-nonzero-fixnum.rkt 11:8 (vector-length (quote #(1 2 3))) -- vector-length
+TR opt: binary-nonzero-fixnum.rkt 11:8 (vector-length (quote #(1 2 3))) -- known-length vector-length
 TR opt: binary-nonzero-fixnum.rkt 11:0 (modulo (vector-length (quote #(1 2 3))) 2) -- binary nonzero fixnum
 1
 )

pkgs/typed-racket-pkgs/typed-racket-tests/tests/typed-racket/optimizer/tests/fixnum-comparison.rkt

@@ -1,6 +1,6 @@
 #;
 (
-TR opt: fixnum-comparison.rkt 12:3 (vector-length (quote #(1 2 3))) -- vector-length
+TR opt: fixnum-comparison.rkt 12:3 (vector-length (quote #(1 2 3))) -- known-length vector-length
 TR opt: fixnum-comparison.rkt 12:29 (string-length "asdf") -- string-length
 TR opt: fixnum-comparison.rkt 12:0 (< (vector-length (quote #(1 2 3))) (string-length "asdf")) -- binary fixnum comp
 #t

pkgs/typed-racket-pkgs/typed-racket-tests/tests/typed-racket/unit-tests/typecheck-tests.rkt

@@ -58,12 +58,28 @@
             (make-TypeFilter (-val #f) p var))
        (make-Path p var)))
 
+(begin-for-syntax
+  (define-splicing-syntax-class return
+    (pattern ty:expr #:attr v #'(ret ty))
+    (pattern (~seq #:ret r:expr) #:attr v #'r))
+
+  (define-splicing-syntax-class expected
+    (pattern (~seq #:expected v:expr))
+    (pattern (~seq) #:attr v #'#f)))
 
 ;; check that a literal typechecks correctly
 (define-syntax tc-l
-  (syntax-rules ()
+  (syntax-parser
-    [(_ lit ty)
+    [(_ lit ty exp:expected)
-     (check-type-equal? (format "~s" 'lit) (tc-literal #'lit) ty)]))
+     #'(check-type-equal? (format "~s" 'lit) (tc-literal #'lit exp.v) ty)]))
+
+(define-syntax tc-l/err
+  (syntax-parser
+    [(_ expr exp:expected)
+     #'(test-exn (format "~a" 'expr)
+                 exn:fail:syntax?
+                 (lambda () (tc-literal #'expr exp.v)))]))
+
 
 
 (define (expand-helper stx k)
@@ -91,14 +107,6 @@
                               (tc-expr/check stx expected)
                               (tc-expr stx)))))]))
 
-(begin-for-syntax
-  (define-splicing-syntax-class return
-    (pattern ty:expr #:attr v #'(ret ty))
-    (pattern (~seq #:ret r:expr) #:attr v #'r))
-
-  (define-splicing-syntax-class expected
-    (pattern (~seq #:expected v:expr))
-    (pattern (~seq) #:attr v #'#f)))
 
 (define-syntax (tc-e stx)
   (syntax-parse stx
@@ -1686,6 +1694,21 @@
    [tc-l (3 . 4) (-pair -PosByte -PosByte)]
    [tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -Integer -Integer)]
    [tc-l #hasheq((a . q) (b . w)) (make-Hashtable -Symbol -Symbol)])
+   [tc-l #hash{[:a . :b]}
+         (let ([rec-type (-mu X (make-Hashtable (t:Un -Symbol X) (t:Un -Symbol X)))])
+           (make-Hashtable (t:Un -Symbol rec-type) (t:Un -Symbol rec-type)))
+         #:expected (-mu X (make-Hashtable (t:Un -Symbol X) (t:Un -Symbol X)))]
+   [tc-l #hash{[:a . :b]}
+         (make-Hashtable (-val ':a) (-val ':b))
+         #:expected (t:Un (-val #f) (make-Hashtable (-val ':a) (-val ':b)))]
+   [tc-l #(:a :b)
+         (-vec (t:Un (-val ':a) (-val ':b) (-mu X (-vec (t:Un (-val ':a) (-val ':b) X)))))
+         #:expected (-mu X (-vec (t:Un (-val ':a) (-val ':b) X)))]
+   [tc-l (#(:a) . :b)
+         (-pair (-vec (t:Un (-val ':a) (-mu X (-pair (-vec (t:Un (-val ':a) X)) (t:Un (-val ':b) X)))))
+                (-val ':b))
+         #:expected (-mu X (-pair (-vec (t:Un (-val ':a) X)) (t:Un (-val ':b) X)))]
+   [tc-l/err #(1 2) #:expected (make-HeterogeneousVector (list -Number -Symbol))]
   ))