add τ⊑ #:for expression syntax

tapl/typecheck.rkt

@@ -412,6 +412,16 @@
             (type->str τ_expected)
             (type->str τ_given)))
 
+  ;; typecheck-fail-msg/multi : (Stx-Listof Type) (Stx-Listof Type) (Stx-Listof Stx) -> String
+  (define (typecheck-fail-msg/multi τs_expected τs_given expressions)
+    (format (string-append "type mismatch\n"
+                           "  expected:    ~a\n"
+                           "  given:       ~a\n"
+                           "  expressions: ~a")
+            (string-join (stx-map type->str τs_expected) ", ")
+            (string-join (stx-map type->str τs_given) ", ")
+            (string-join (map ~s (stx-map syntax->datum expressions)) ", ")))
+
   ;; typecheck-fail-msg/multi/no-exprs : (Stx-Listof Type) (Stx-Listof Type) -> String
   (define (typecheck-fail-msg/multi/no-exprs τs_expected τs_given)
     (format (string-append "type mismatch\n"

tapl/typed-lang-builder/fsub.rkt

@@ -85,7 +85,7 @@
 (define-typed-syntax inst
   [(inst e τ:type ...) ≫
    [⊢ [[e ≫ e-] ⇒ : (~∀ ([tv <: τ_sub] ...) τ_body)]]
-   [τ.norm τ⊑ τ_sub] ...
+   [τ.norm τ⊑ τ_sub #:for τ] ...
    [#:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)]
    --------
    [⊢ [[_ ≫ e-] ⇒ : τ_inst]]])

tapl/typed-lang-builder/mlish.rkt

@@ -848,7 +848,7 @@
    [#:with [X ...] (compute-tyvars #'(τ_x ...))]
    [([X : #%type ≫ X-] ...) ()
     ⊢ [[τ_x ≫ τ_x-] ⇐ : #%type] ...]
-   [τ_in τ⊑ τ_x-] ...
+   [τ_in τ⊑ τ_x- #:for x] ...
    ;; TODO is there a way to have λs that refer to ids defined after them?
    [([V : #%type ≫ V-] ... [X- : #%type ≫ X--] ...) ([x : τ_x- ≫ x-] ...)
     ⊢ [[body ≫ body-] ⇐ : τ_out]]
@@ -868,7 +868,7 @@
 
 ;; #%app --------------------------------------------------
 (define-typed-syntax mlish:#%app #:export-as #%app
-  [(_ e_fn . e_args) ≫
+  [(_ e_fn e_arg ...) ≫
    ;; compute fn type (ie ∀ and →)
    [⊢ [[e_fn ≫ e_fn-] ⇒ : (~?∀ Xs (~ext-stlc:→ . tyX_args))]]
    ;; solve for type variables Xs
@@ -877,12 +877,12 @@
    [#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)]
    [#:with (unsolved-X ...) (find-free-Xs #'Xs* #'τ_out)]
    ;; arity check
-   [#:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
-    (num-args-fail-msg #'e_fn #'[τ_in ...] #'e_args)]
+   [#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+    (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])]
    ;; compute argument types
    [#:with (τ_arg ...) (stx-map typeof #'(e_arg- ...))]
    ;; typecheck args
-   [τ_arg τ⊑ τ_in] ...
+   [τ_arg τ⊑ τ_in #:for e_arg] ...
    [#:with τ_out* (if (stx-null? #'(unsolved-X ...))
                       #'τ_out
                       (syntax-parse #'τ_out

tapl/typed-lang-builder/typed-lang-builder.rkt

@@ -161,11 +161,21 @@
              #'[(~post
                  (~fail #:unless (typecheck? #'a #'b)
                         (typecheck-fail-msg/1/no-expr #'b #'a)))]]
+    [pattern [a τ⊑ b #:for e]
+             #:with [pat ...]
+             #'[(~post
+                 (~fail #:unless (typecheck? #'a #'b)
+                        (typecheck-fail-msg/1 #'b #'a #'e)))]]
     [pattern (~seq [a τ⊑ b] ooo:elipsis)
              #:with [pat ...]
              #'[(~post
                  (~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
                         (typecheck-fail-msg/multi/no-exprs #'[b ooo] #'[a ooo])))]]
+    [pattern (~seq [a τ⊑ b #:for e] ooo:elipsis)
+             #:with [pat ...]
+             #'[(~post
+                 (~fail #:unless (typechecks? #'[a ooo] #'[b ooo])
+                        (typecheck-fail-msg/multi #'[b ooo] #'[a ooo] #'[e ooo])))]]
     [pattern [#:when condition:expr]
              #:with [pat ...]
              #'[(~fail #:unless condition)]]