fix expected type propagation problem (in lam2) in turnstile/mlish

macrotypes/type-constraints.rkt

@@ -161,7 +161,7 @@
 ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx)
 ;; looks up each X in the constraints, returning the X if it's unconstrained
 (define (lookup-Xs/keep-unsolved Xs cs)
-  (for/list ([X (in-list (stx->list Xs))])
+  (for/list ([X (in-stx-list Xs)])
     (or (lookup X cs) X)))
 
 ;; instantiate polymorphic types

turnstile/examples/mlish.rkt

@@ -86,9 +86,7 @@
   ;; find-free-Xs : (Stx-Listof Id) Type -> (Listof Id)
   ;; finds the free Xs in the type
   (define (find-free-Xs Xs ty)
-    (for/list ([X (in-list (stx->list Xs))]
-               #:when (stx-contains-id? ty X))
-      X))
+    (for/list ([X (in-stx-list Xs)] #:when (stx-contains-id? ty X)) X))
 
   ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
   ;;   stx = the application stx = (#%app e_fn e_arg ...)
@@ -104,8 +102,9 @@
     (syntax-parse tyXs
       [(τ_inX ... τ_outX)
        ;; generate initial constraints with expected type and τ_outX
-       #:with (~?∀ Vs expected-ty) (and (get-expected-type stx)
-                                        ((current-type-eval) (get-expected-type stx)))
+       #:with (~?∀ Vs expected-ty)
+              (and (get-expected-type stx)
+                   ((current-type-eval) (get-expected-type stx)))
        (define initial-cs
          (if (and (syntax-e #'expected-ty) (stx-null? #'Vs))
              (add-constraints Xs '() (list (list #'expected-ty #'τ_outX)))
@@ -114,8 +113,8 @@
          [(_ e_fn . args)
           (define-values (as- cs)
               (for/fold ([as- null] [cs initial-cs])
-                        ([a (in-list (syntax->list #'args))]
-                         [tyXin (in-list (syntax->list #'(τ_inX ...)))])
+                        ([a (in-stx-list #'args)]
+                         [tyXin (in-stx-list #'(τ_inX ...))])
                 (define ty_in (inst-type/cs Xs cs tyXin))
                 (define/with-syntax [a- ty_a]
                   (infer+erase (if (empty? (find-free-Xs Xs ty_in))
@@ -149,7 +148,7 @@
   (define (covariant-Xs? ty)
     (syntax-parse ((current-type-eval) ty)
       [(~?∀ Xs ty)
-       (for/and ([X (in-list (syntax->list #'Xs))])
+       (for/and ([X (in-stx-list #'Xs)])
          (covariant-X? X #'ty))]))
 
   ;; find-X-variance : Id Type [Variance] -> Variance
@@ -186,7 +185,7 @@
          (for/list ([arg-variance (in-list (get-arg-variances #'tycons))])
            (variance-compose ctxt-variance arg-variance)))
        (for/fold ([acc (make-list (length Xs) irrelevant)])
-                 ([τ (in-list (syntax->list #'[τ ...]))]
+                 ([τ (in-stx-list #'[τ ...])]
                   [τ-ctxt-variance (in-list τ-ctxt-variances)])
          (map variance-join
               acc
@@ -856,7 +855,7 @@
    [⊢ (λ- (x- ...) body-)]]
   [(λ ([x : τ_x] ...) body) ⇐ (~?∀ (V ...) (~ext-stlc:→ τ_in ... τ_out)) ≫
    #:with [X ...] (compute-tyvars #'(τ_x ...))
-   [([X ≫ X- :: #%type] ...) () ⊢ [τ_x ≫ τ_x- ⇐ #%type] ...]
+   [([X ≫ X- :: #%type] ...) () ⊢ [τ_x ≫ τ_x- ⇐ :: #%type] ...]
    [τ_in τ⊑ τ_x- #:for x] ...
    ;; TODO is there a way to have λs that refer to ids defined after them?
    [([V ≫ V- :: #%type] ... [X- ≫ X-- :: #%type] ...) ([x ≫ x- : τ_x-] ...)

turnstile/examples/tests/mlish-tests.rkt

@@ -295,7 +295,7 @@
    [Nil -> 3])
  : Int ⇒ 6)
             
-;; check expected-type propagation for other match paterns
+;; check expected-type propagation for other match patterns
 
 (define-type (Option A)
   (None)
@@ -450,6 +450,13 @@
 
 (define (ok [a : A] → (Result A B))
   (Ok a))
+
+;; Cannot infer concrete type for B in (Result A B).
+;; Need expected type (see (inst result-if-1 ...) example below)
+(typecheck-fail
+ (λ ([a : Int]) (ok (Cons a Nil)))
+ #:with-msg "Could not infer instantiation of polymorphic function ok")
+
 (define (error [b : B] → (Result A B))
   (Error b))
 
@@ -512,6 +519,7 @@
             : (→ (→ Int (Result (List Int) (List String)))
                  (→ String (Result (List Int) (List String)))
                  (Result (List Int) (List String))))
+
 (check-type (((inst result-if-1 Int String (List Int) (List String)) (Ok 1))
              (λ ([a : Int])    (ok (Cons a Nil)))
              (λ ([b : String]) (error (Cons b Nil))))
@@ -671,7 +679,7 @@
 (typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
 (typecheck-fail (ann 1 : 1) #:with-msg "not a well-formed type")
 (typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a well-formed type")
-(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given #%type\n *expression: Int")
+(typecheck-fail (ann Int : Int) #:with-msg "expected Int, given an invalid expression\n *expression: Int")
 
 ; let
 (check-type (let () (+ 1 1)) : Int ⇒ 2)