From 480feb961c706bd813f07ca5fc2d5e8bb3271839 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Tue, 25 Feb 2020 16:14:30 -0500
Subject: [PATCH] improve spawn error messages

---
 racket/typed/roles.rkt       | 26 +++++++++++++++++++++++---
 racket/typed/tests/spawn.rkt | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 58 insertions(+), 3 deletions(-)
 create mode 100644 racket/typed/tests/spawn.rkt

diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 2105cc1..fe576c4 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -326,9 +326,9 @@
                 "Spawned actors not valid in dataspace"
   #:fail-unless (project-safe? (∩ (strip-? #'τ-o) #'τ-c.norm)
                                #'τ-i)
-                "Not prepared to handle all inputs"
-  #:fail-unless (project-safe? #'τ-o/i #'τ-i/i)
-                "Not prepared to handle internal events"
+                (string-append "Not prepared to handle inputs:\n" (make-actor-error-message #'τ-i #'τ-o #'τ-c.norm))
+  #:fail-unless (project-safe? (∩ (strip-? #'τ-o/i) #'τ-o/i) #'τ-i/i)
+                (string-append "Not prepared to handle internal events:\n" (make-actor-error-message #'τ-i/i #'τ-o/i #'τ-o/i))
   --------------------------------------------------------------------------------------------
   [⊢ (syndicate:spawn (syndicate:on-start s-)) (⇒ : ★/t)
                                                (⇒ ν-s (τ-final))]]
@@ -338,6 +338,26 @@
    ----------------------------------------
    [≻ (spawn #,τc s)]])
 
+;; Type Type Type -> String
+(define-for-syntax (make-actor-error-message τ-i τ-o τ-c)
+  (define mismatches (find-surprising-inputs τ-i τ-o τ-c))
+  (string-join (map type->str mismatches) ",\n"))
+
+;; Type Type Type -> (Listof Type)
+(define-for-syntax (find-surprising-inputs τ-i τ-o τ-c)
+  (define incoming (∩ (strip-? τ-o) τ-c))
+  ;; Type -> (Listof Type)
+  (let loop ([ty incoming])
+    (syntax-parse ty
+      [(~U* τ ...)
+       (apply append (map loop (syntax->list #'(τ ...))))]
+      [_
+       (cond
+         [(project-safe? ty τ-i)
+          '()]
+         [else
+          (list ty)])])))
+
 (define-typed-syntax (dataspace τ-c:type s ...) ≫
   #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order"
   #:mode (communication-type-mode #'τ-c.norm)
diff --git a/racket/typed/tests/spawn.rkt b/racket/typed/tests/spawn.rkt
new file mode 100644
index 0000000..e16195d
--- /dev/null
+++ b/racket/typed/tests/spawn.rkt
@@ -0,0 +1,35 @@
+#lang typed/syndicate/roles
+
+(require rackunit/turnstile)
+
+(check-type
+  (spawn (U (Tuple Int) (Observe (Tuple ★/t)))
+   (start-facet _
+     (on (asserted (tuple $x))
+         (add1 x))))
+  ;; wanted: ν-s ((Actor (Tuple Int)))
+  : ★/t)
+
+(typecheck-fail
+ (spawn (U (Tuple String) (Observe (Tuple ★/t)))
+        (start-facet _
+                     (on (asserted (tuple $x:Int))
+                         (add1 x))))
+ #:with-msg "spawn: Not prepared to handle inputs:\n\\(Tuple- String\\)")
+
+(check-type
+ (spawn (U)
+        (start-facet _
+                     (know (tuple 5))
+                     (on (know (tuple $x:Int))
+                         (add1 x))))
+ ;; wanted: ν-s ((Actor (U)))
+ : ★/t)
+
+(typecheck-fail
+ (spawn (U)
+        (start-facet _
+                     (know (tuple "hi"))
+                     (on (know (tuple $x:Int))
+                         (add1 x))))
+ #:with-msg "spawn: Not prepared to handle internal events:\n\\(Tuple- String\\)")