fix more stx-parse err msgs; and other err msgs

- all tests now passing

tapl/mlish.rkt

@@ -99,10 +99,12 @@
                  (cons #'a- as-)
                  (stx-append cs (compute-constraint (list tyXin #'ty_a))))))
          (define maybe-solved-tys (try-to-solve Xs cs))
+         
          (if maybe-solved-tys
              (list (reverse as-) maybe-solved-tys)
              (type-error #:src stx
-              #:msg (mk-app-err-msg stx #:expected #'(τ_inX ...) #:given (infers+erase #'args)
+              #:msg (mk-app-err-msg stx #:expected #'(τ_inX ...) 
+                                        #:given (stx-map stx-cadr (infers+erase #'args))
                      #:note (format "Could not infer instantiation of polymorphic function ~a."
                                     (syntax->datum #'e_fn)))))])]))
 
@@ -289,13 +291,16 @@
                         (infer+erase (syntax-property e 'expected-type τ_e)))
                       #'(e_arg ...) #'(τ_in.norm (... ...)))
               #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
-                           (mk-app-err-msg (syntax/loc stx (C e_arg ...))
+                           (mk-app-err-msg (syntax/loc stx (#%app C e_arg ...))
                             #:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
                             #:name (format "constructor ~a" 'Cons))
               (⊢ (StructName e_arg- ...) : (Name τ_X (... ...)))]
              [(C . args) ; no type annotations, must infer instantiation
               #:with StructName/ty 
-                     (⊢ StructName : (∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
+                     (syntax-property
+                       (⊢ StructName : (∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
+                       'orig
+                       (list #'C))
               ; stx/loc transfers expected-type
               (syntax/loc stx (mlish:#%app StructName/ty . args))]))
          ...)]))
@@ -604,14 +609,15 @@
         #:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
         #:fail-unless (set=? (syntax->datum #'(Clause ...))
                              (syntax->datum #'(ConsAll ...)))
-                      (string-append
-                       "clauses not exhaustive; missing: "
-                       (string-join      
-                           (map symbol->string
-                                (set-subtract 
-                                    (syntax->datum #'(ConsAll ...))
-                                  (syntax->datum #'(Clause ...))))
-                         ", "))
+                      (type-error #:src stx
+                       #:msg (string-append
+                              "match: clauses not exhaustive; missing: "
+                              (string-join      
+                                (map symbol->string
+                                     (set-subtract 
+                                       (syntax->datum #'(ConsAll ...))
+                                       (syntax->datum #'(Clause ...))))
+                                ", ")))
         #:with ((_ ((~literal quote) Cons) ((~literal quote) StructName) Cons? [_ acc τ] ...) ...)
                (map ; ok to compare symbols since clause names can't be rebound
                 (lambda (Cl) 
@@ -716,6 +722,9 @@
     [(stx-null? #'Xs)
      (syntax-parse #'(e_args tyX_args)
        [((e_arg ...) (τ_inX ... _))
+        #:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...))
+                      (mk-app-err-msg stx #:expected #'(τ_inX ...) 
+                                      #:note "Wrong number of arguments.")
         #:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args))
         #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
     [else

tapl/tests/mlish-tests.rkt

@@ -189,7 +189,7 @@
 (typecheck-fail (ConsI #f INil)
  #:with-msg 
  (expected "Int, IntList" #:given "Bool, IntList"
-  #:note "Type error applying constructor ConsI"))
+  #:note "Type error applying.*ConsI"))
 
 ;; annotated
 (check-type (Nil {Int}) : (List Int))
@@ -215,15 +215,15 @@
 (typecheck-fail (Cons 1 (Nil {Bool}))
  #:with-msg 
  (expected "Int, (List Int)" #:given "Int, (List Bool)"
-  #:note "Type error applying constructor Cons"))
+  #:note "Type error applying.*Cons"))
 (typecheck-fail (Cons {Bool} 1 (Nil {Int}))
  #:with-msg 
  (expected "Bool, (List Bool)" #:given "Int, (List Int)"
-  #:note "Type error applying constructor Cons"))
+  #:note "Type error applying.*Cons"))
 (typecheck-fail (Cons {Bool} 1 Nil)
  #:with-msg 
  (expected "Bool, (List Bool)" #:given "Int, (List Bool)"
-  #:note "Type error applying constructor Cons"))
+  #:note "Type error applying.*Cons"))
 
 (typecheck-fail (match Nil with [Cons x xs -> 2] [Nil -> 1])
                 #:with-msg "add annotations")

tapl/tests/mlish/bg/basics.mlish

@@ -59,7 +59,7 @@
 (check-type
   (permutations (Nil {Int}))
   : (List (List Int))
-  ⇒ (Cons (Nil {(List Int)}) Nil))
+  ⇒ (Cons (Nil {Int}) Nil))
 
 (check-type
   (permutations (Cons 1 Nil))

tapl/typecheck.rkt

@@ -584,9 +584,12 @@
                       (if (stx-null? #'extra-bvs)
                           #'extra-info
                           (substs #'τs- #'extra-bvs #'extra-info))
+               (add-orig
                 (assign-type 
-                  (syntax/loc stx (τ-internal (λ bvs- (#%expression extra-info-inst) . τs-))) 
-                  #'k_result)]
+                  (syntax/loc stx 
+                    (τ-internal (λ bvs- (#%expression extra-info-inst) . τs-))) 
+                  #'k_result)
+                #'(τ . args))]
              ;; else fail with err msg
              [_
               (type-error #:src stx