diff --git a/racket/typed/core-expressions.rkt b/racket/typed/core-expressions.rkt index 4f9095e..6480f4f 100644 --- a/racket/typed/core-expressions.rkt +++ b/racket/typed/core-expressions.rkt @@ -158,10 +158,11 @@ [⊢ (match- e- [p- s-] ... [_ (#%app- error- "incomplete pattern match")]) (⇒ : (U τ-s ...)) - ;; TODO losing branching information here - (⇒ ν-ep (eps ... ...)) + (⇒ ν-ep #,(make-Branch #'((eps ...) ...))) (⇒ ν-f #,(make-Branch #'((fs ...) ...))) - (⇒ ν-s (ss ... ...))]) + (⇒ ν-s #,(make-Branch #'((ss ...) ...)))]) + + (define-typed-syntax (tuple e:expr ...) ≫ [⊢ e ≫ e- (⇒ : τ)] ... diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt index fe576c4..d8bd35a 100644 --- a/racket/typed/roles.rkt +++ b/racket/typed/roles.rkt @@ -310,6 +310,7 @@ identity)) (define-typed-syntax spawn + ;; TODO - do the lack of #:cut-s cause bad error messages here? [(spawn τ-c:type s) ≫ #:fail-unless (flat-type? #'τ-c.norm) "Communication type must be first-order" ;; TODO: check that each τ-f is a Role