suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

start mlish lang

Browse Source
This commit is contained in:
Stephen Chang 2016-02-22 19:23:14 -05:00
parent a82a833b43
commit dbfd52bf0f
10 changed files with 464 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

164
tapl/mlish.rkt Normal file
View File

@ -0,0 +1,164 @@
#lang s-exp "typecheck.rkt"
(require (for-syntax syntax/id-set))
(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let
#:rename [~→ ~ext-stlc:→])
(require (only-in "sysf.rkt" inst ~∀ ∀ Λ))
(require (only-in "stlc+rec-iso.rkt" case fld unfld μ × ∨ var tup define-type-alias)
(prefix-in stlc+rec-iso: (only-in "stlc+rec-iso.rkt" define)))
;(reuse cons [head hd] [tail tl] nil [isnil nil?] List ~List list #:from "stlc+cons.rkt")
;(reuse tup × proj #:from "stlc+tup.rkt")
;(reuse define-type-alias #:from "stlc+reco+var.rkt")
;(provide hd tl nil?)
(provide (rename-out [lifted→ →]))
(provide define-type match)
(provide (rename-out [ext-stlc:let let]))
;; ML-like language with no type inference
;; type inference constraint solving
(begin-for-syntax
(define (compute-constraint τ1-τ2)
(syntax-parse τ1-τ2
[(X:id τ) #'((X τ))]
[((~Any τ1 ...) (~Any τ2 ...))
(compute-constraints #'((τ1 τ2) ...))]
; should only be monomorphic?
[((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
(compute-constraints #'((τ1 τ2) ...))]
[_ #:when (displayln τ1-τ2) #'()]))
(define (compute-constraints τs)
;(printf "constraints: ~a\n" (syntax->datum τs))
(stx-appendmap compute-constraint τs))
(define (solve-constraint x-τ)
(syntax-parse x-τ
[(X:id τ) #'((X τ))]
[_ #'()]))
(define (solve-constraints cs)
(stx-appendmap compute-constraint cs))
(define (lookup x substs)
(syntax-parse substs
[((y:id τ) . rst)
#:when (free-identifier=? #'y x)
#'τ]
[(_ . rst) (lookup x #'rst)]
[() false])))
(define-type-constructor Tmp #:arity >= 0 #:bvs >= 0) ; need a >= 0 arity
(define-syntax (define-type stx)
(syntax-parse stx
[(_ (Name:id X:id ...)
;; constructors must have the form (Cons τ ...)
;; but the first ~or clause accepts 0-arg constructors as ids
;; the ~and is required to bind the duplicate Cons ids (see Ryan's email)
(~and (~or (~and IdCons:id (~parse (Cons τ ...) #'(IdCons)))
(Cons τ ...))) ...)
#:with (StructName ...) (generate-temporaries #'(Cons ...))
#:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((fld ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
#:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
#'(StructName ...) #'((fld ...) ...))
#`(begin
(define-type-constructor Name
#:arity = #,(stx-length #'(X ...))
#:other-prop variants #'(X ...) #'((Cons τ ...) ...))
(struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
(define-syntax (Cons stx)
(syntax-parse stx
[C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)]
[_:id
#:when (and (not (stx-null? #'(X ...)))
(not (stx-null? #'(τ ...))))
(type-error
#:src stx
#:msg
(string-append
(format "constructor ~a must instantiate ~a type argument(s): "
'Cons (stx-length #'(X ...)))
(string-join (stx-map type->str #'(X ...)) ", ")
"\n"
(format "and be applied to ~a arguments with type(s): "(stx-length #'(τ ...)))
(string-join (stx-map type->str #'(τ ...)) ", ")))]
[(_ τs e_arg ...)
#:when (brace? #'τs) ; commit
#:with {~! τ_X:type (... ...)} #'τs
#:with ([e_arg- τ_arg] ...) (stx-map infer+erase #'(e_arg ...))
#:with (τ_in:type (... ...))
(stx-map (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t)) #'(τ ...))
#:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
;; need to duplicate #%app err msg here, to attach additional props
(string-append
(format "~a (~a:~a) Arguments to constructor ~a have wrong type(s), "
(syntax-source stx) (syntax-line stx) (syntax-column stx)
'Cons)
"or wrong number of arguments:\nGiven:\n"
(string-join
(map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
(syntax->datum #'(e_arg ...))
(stx-map type->str #'(τ_arg ...)))
"\n" #:after-last "\n")
(format "Expected: ~a arguments with type(s): "
(stx-length #'(τ_in (... ...))))
(string-join (stx-map type->str #'(τ_in (... ...))) ", "))
#:with τ_out (syntax-property
(syntax-property #'(Name τ_X (... ...)) 'constructor #'Cons)
'accessors
#'(acc ...))
(⊢ (StructName e_arg- ...) : τ_out)]
[(C . args) #:when (stx-null? #'(X ...)) #'(C {} . args)] ; no tyvars, no annotations
[(C . args) ; no type annotations, must infer instantiation
#:with ([arg- τarg] (... ...)) (infers+erase #'args)
#:with (~Tmp Ys τ+ (... ...)) ((current-type-eval) #'(Tmp (X ...) τ ...))
#:with cs (compute-constraints #'((τ+ τarg) (... ...)))
#:with (τ_solved (... ...)) (stx-map (λ (y) (lookup y #'cs)) #'Ys)
#'(C {τ_solved (... ...)} . args)]))
...)]))
(define-syntax (match stx)
(syntax-parse stx #:datum-literals (with ->)
[(_ e with . clauses)
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
#:with ([Clause:id x ... -> e_c] ...) (stx-sort #'clauses symbol<?)
#:with [e- τ_e] (infer+erase #'e)
#:with ((Cons τ ...) ...) (stx-sort (syntax-property #'τ_e 'variants) symbol<?)
#:fail-unless (= (stx-length #'(Clause ...)) (stx-length #'(Cons ...))) "wrong number of case clauses"
#:fail-unless (typechecks? #'(Clause ...) #'(Cons ...)) "case clauses not exhaustive"
#:with (((x- ...) e_c- τ_ec) ...)
(stx-map (λ (bs e) (infer/ctx+erase bs e)) #'(([x : τ] ...) ...) #'(e_c ...))
#:fail-unless (same-types? #'(τ_ec ...)) "branches have different types"
#:with C (syntax-property #'τ_e 'constructor)
#:with (_ (x_out ...) e_out τ_out) (stx-assoc #'C #'((Clause (x- ...) e_c- τ_ec) ...))
#:with (acc ...) (syntax-property #'τ_e 'accessors)
(⊢ (let ([x_out (acc e-)] ...) e_out) : τ_out)]))
(define-syntax lifted→ ; wrap → with ∀
(syntax-parser
[(_ . rst) #'(∀ () (ext-stlc:→ . rst))]))
(define-primop + : (lifted→ Int Int Int))
(define-primop - : (lifted→ Int Int Int))
(define-primop void : (lifted→ Unit))
(define-primop = : (lifted→ Int Int Bool))
(define-primop zero? : (lifted→ Int Bool))
(define-primop sub1 : (lifted→ Int Int))
(define-primop add1 : (lifted→ Int Int))
(define-primop not : (lifted→ Bool Bool))
(define-primop abs : (lifted→ Int Int))
; all λs have type (∀ (X ...) (→ τ_in ... τ_out))
(define-typed-syntax liftedλ #:export-as λ #:datum-literals (:)
[(_ . rst)
#'(Λ () (ext-stlc:λ . rst))])
(define-typed-syntax new-app #:export-as #%app
[(_ τs f . args)
#:when (brace? #'τs)
#'(ext-stlc:#%app (inst f . τs) . args)]
[(_ f . args)
#'(ext-stlc:#%app (inst f) . args)])

10
tapl/notes.txt
View File

@ -1,3 +1,13 @@
2016-02-19
Implementing algebraic data types
- macro cannot define type-alias and constructor functions that produce
variant values
- not only because adts should be an abstraction (ie not type alias)
- constructor output will have variant type and not the type defined
- macro should basically expand to list implementation in stlc+cons.rkt
- where to store the names of the variants (as stx prop?)
2015-10-09
TODO: variant case should call current-join?

3
tapl/stlc+lit.rkt
View File

@ -21,6 +21,9 @@
#:with op/tc (generate-temporary #'op)
#'(begin
(provide (rename-out [op/tc op]))
(define-primop op/tc op : τ))]
[(_ op/tc op : τ)
#'(begin
#;(define-syntax op/tc (make-rename-transformer (assign-type #'op #'τ)))
; rename transformer doesnt seem to expand at the right time
; - op still has no type in #%app

2
tapl/stlc.rkt
View File

@ -80,7 +80,7 @@
(string-append
(format "~a (~a:~a) Arguments to function ~a have wrong type(s), "
(syntax-source stx) (syntax-line stx) (syntax-column stx)
(syntax->datum #'e_fn))
(syntax->datum #'e_fn-))
"or wrong number of arguments:\nGiven:\n"
(string-join
(map (λ (e t) (format " ~a : ~a" e t)) ; indent each line

8
tapl/stx-utils.rkt
View File

@ -39,8 +39,12 @@
(define (stx-str=? s1 s2)
(string=? (syntax-e s1) (syntax-e s2)))
(define (stx-sort stx cmp)
(sort (syntax->list stx) (λ (stx1 stx2) (cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))))
(define (stx-sort stx cmp #:key [key-fn (λ (x) x)])
(sort
(syntax->list stx)
(λ (stx1 stx2)
(cmp (syntax-e (stx-car stx1)) (syntax-e (stx-car stx2))))
#:key key-fn))
(define (stx-fold f base . lsts)
(apply foldl f base (map syntax->list lsts)))

7
tapl/sysf.rkt
View File

@ -21,4 +21,9 @@
(define-typed-syntax inst
[(_ e τ:type ...)
#:with (e- (tvs (τ_body))) (⇑ e as ∀)
(⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))])
;#:with [e- (~and t (~∀ tvs τ_body))] (infer+erase #'e)
;#:with (_ Xs τ_orig) (get-orig #'t) ; doesnt work with implicit lifted→
;#:with new-orig (substs #'(τ ...) #'Xs #'τ_orig)
;(⊢ e- : #,(add-orig (substs #'(τ.norm ...) #'tvs #'τ_body) #'new-orig))]
(⊢ e- : #,(substs #'(τ.norm ...) #'tvs #'τ_body))]
[(_ e) #'e])

2
tapl/tests/ext-stlc-tests.rkt
View File

@ -29,7 +29,7 @@
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
(begin 1 2 3)
#:with-msg "Expected expression \"1\" to have Unit type, got: Int")
#:with-msg "Expected expression 1 to have Unit type, got: Int")
(check-type (begin (void) 1) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)

2
tapl/tests/infer-tests.rkt
View File

@ -223,7 +223,7 @@
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
(begin 1 2 3)
#:with-msg "Expected expression \"1\" to have Unit type, got: Int")
#:with-msg "Expected expression 1 to have Unit type, got: Int")
(check-type (begin (void) 1) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)

224
tapl/tests/mlish-tests.rkt Normal file
View File

@ -0,0 +1,224 @@
#lang s-exp "../mlish.rkt"
(require "rackunit-typechecking.rkt")
(define-type (IntList)
INil
(ConsI Int (IntList)))
(check-type INil : (IntList))
(check-type (ConsI 1 INil) : (IntList))
(check-type
(match INil with
[INil -> 1]
[ConsI x xs -> 2]) : Int ⇒ 1)
(check-type
(match (ConsI 1 INil) with
[INil -> 1]
[ConsI x xs -> 2]) : Int ⇒ 2)
(typecheck-fail (match 1 with [INil -> 1]))
(define-type (List X)
(Nil)
(Cons X (List X)))
(check-type (Nil {Int}) : (List Int))
(check-type (Cons 1 (Nil {Int})) : (List Int))
(check-type (Cons 1 (Cons 2 (Nil {Int}))) : (List Int))
(define-type (Tree X)
(Leaf X)
(Node (Tree X) (Tree X)))
(check-type (Leaf 10) : (Tree Int))
(check-type (Node (Leaf 10) (Leaf 11)) : (Tree Int))
(typecheck-fail (Cons 1 (Nil {Bool}))
#:with-msg "wrong type\\(s\\)")
(check-type
(match (Nil {Int}) with
[Cons x xs -> 2]
[Nil -> 1])
: Int ⇒ 1)
(check-type
(match (Nil {Int}) with
[Nil -> 1]
[Cons x xs -> 2])
: Int ⇒ 1)
(check-type
(match (Cons 1 (Nil {Int})) with
[Nil -> 3]
[Cons y ys -> (+ y 4)])
: Int ⇒ 5)
(check-type
(match (Cons 1 (Nil {Int})) with
[Cons y ys -> (+ y 5)]
[Nil -> 3])
: Int ⇒ 6)
; ext-stlc tests --------------------------------------------------
; tests for stlc extensions
; new literals and base types
(check-type "one" : String) ; literal now supported
(check-type #f : Bool) ; literal now supported
(check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type
;; Unit
(check-type (void) : Unit)
(check-type void : (→ Unit))
(typecheck-fail
((λ ([x : Unit]) x) 2)
#:with-msg
"Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Unit")
(typecheck-fail
((λ ([x : Unit]) x) void)
#:with-msg
"Arguments to function.+have wrong type.+Given:.+(→ Unit).+Expected:.+Unit")
(check-type ((λ ([x : Unit]) x) (void)) : Unit)
;; begin
(check-type (begin 1) : Int)
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
(begin 1 2 3)
#:with-msg "Expected expression 1 to have Unit type, got: Int")
(check-type (begin (void) 1) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (begin (void) x)) 1) : Int)
(check-type ((λ ([x : Int]) (begin x)) 1) : Int)
(check-type ((λ ([x : Int]) (begin (begin x))) 1) : Int)
(check-type ((λ ([x : Int]) (begin (void) (begin (void) x))) 1) : Int)
(check-type ((λ ([x : Int]) (begin (begin (void) x))) 1) : Int)
;;ascription
(check-type (ann 1 : Int) : Int ⇒ 1)
(check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10)
(typecheck-fail (ann 1 : Bool) #:with-msg "ann: 1 does not have type Bool")
;ann errs
(typecheck-fail (ann 1 : Complex) #:with-msg "unbound identifier")
(typecheck-fail (ann 1 : 1) #:with-msg "not a valid type")
(typecheck-fail (ann 1 : (λ ([x : Int]) x)) #:with-msg "not a valid type")
(typecheck-fail (ann Int : Int) #:with-msg "does not have type Int")
; let
(check-type (let () (+ 1 1)) : Int ⇒ 2)
(check-type (let ([x 10]) (+ 1 2)) : Int)
(check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30)
(typecheck-fail
(let ([x #f]) (+ x 1))
#:with-msg
"Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
(typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))
#:with-msg "x: unbound identifier")
(check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21)
(typecheck-fail
(let* ([x #t] [y (+ x 1)]) 1)
#:with-msg
"Arguments to function \\+.+have wrong type.+Given:.+Bool.+Int.+Expected:.+Int.+Int")
; letrec
(typecheck-fail
(letrec ([(x : Int) #f] [(y : Int) 1]) y)
#:with-msg
"letrec: type check fail, args have wrong type:\n#f has type Bool, expected Int")
(typecheck-fail
(letrec ([(y : Int) 1] [(x : Int) #f]) x)
#:with-msg
"letrec: type check fail, args have wrong type:.+#f has type Bool, expected Int")
(check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3)
;; recursive
(check-type
(letrec ([(countdown : (→ Int String))
(λ ([i : Int])
(if (= i 0)
"liftoff"
(countdown (- i 1))))])
(countdown 10)) : String ⇒ "liftoff")
;; mutually recursive
(check-type
(letrec ([(is-even? : (→ Int Bool))
(λ ([n : Int])
(or (zero? n)
(is-odd? (sub1 n))))]
[(is-odd? : (→ Int Bool))
(λ ([n : Int])
(and (not (zero? n))
(is-even? (sub1 n))))])
(is-odd? 11)) : Bool ⇒ #t)
;; check some more err msgs
(typecheck-fail
(and "1" #f)
#:with-msg "Expected expression \"1\" to have Bool type, got: String")
(typecheck-fail
(and #t "2")
#:with-msg
"Expected expression \"2\" to have Bool type, got: String")
(typecheck-fail
(or "1" #f)
#:with-msg
"Expected expression \"1\" to have Bool type, got: String")
(typecheck-fail
(or #t "2")
#:with-msg
"Expected expression \"2\" to have Bool type, got: String")
(typecheck-fail
(if "true" 1 2)
#:with-msg
"Expected expression \"true\" to have Bool type, got: String")
(typecheck-fail
(if #t 1 "2")
#:with-msg
"branches have incompatible types: Int and String")
;; tests from stlc+lit-tests.rkt --------------------------
; most should pass, some failing may now pass due to added types/forms
(check-type 1 : Int)
;(check-not-type 1 : (Int → Int))
;(typecheck-fail "one") ; literal now supported
;(typecheck-fail #f) ; literal now supported
(check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
(check-not-type (λ ([x : Int]) x) : Int)
(check-type (λ ([x : Int]) x) : (→ Int Int))
(check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
(check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
(typecheck-fail
((λ ([x : Bool]) x) 1)
#:with-msg
"Arguments to function.+have wrong type.+Given:.+Int.+Expected:.+Bool")
;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type
(typecheck-fail
(λ ([f : Int]) (f 1 2))
#:with-msg
"Expected expression f to have → type, got: Int")
(check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
: (→ (→ Int Int Int) Int Int Int))
(check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2)
: Int ⇒ 3)
(typecheck-fail
(+ 1 (λ ([x : Int]) x))
#:with-msg
"Arguments to function \\+ have wrong type.+Given:\n 1 : Int.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
(typecheck-fail
(λ ([x : (→ Int Int)]) (+ x x))
#:with-msg
"Arguments to function \\+ have wrong type.+Given:.+(→ Int Int).+Expected: 2 arguments with type.+Int\\, Int")
(typecheck-fail
((λ ([x : Int] [y : Int]) y) 1)
#:with-msg "Arguments to function.+have.+wrong number of arguments")
(check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)

57
tapl/typecheck.rkt
View File

@ -2,8 +2,8 @@
(require
(for-syntax (except-in racket extends)
syntax/parse racket/syntax syntax/stx racket/stxparam
"stx-utils.rkt"
syntax/parse/debug)
syntax/parse/debug
"stx-utils.rkt")
(for-meta 2 racket/base syntax/parse racket/syntax syntax/stx "stx-utils.rkt")
(for-meta 3 racket/base syntax/parse racket/syntax)
racket/bool racket/provide racket/require)
@ -12,7 +12,8 @@
(except-out (all-from-out racket/base) #%module-begin)
(for-syntax (all-defined-out)) (all-defined-out)
(for-syntax
(all-from-out racket syntax/parse racket/syntax syntax/stx "stx-utils.rkt"))
(all-from-out racket syntax/parse racket/syntax syntax/stx
"stx-utils.rkt"))
(for-meta 2 (all-from-out racket/base syntax/parse racket/syntax)))
;; type checking functions/forms
@ -154,6 +155,8 @@
(define ty (syntax-property stx tag))
(if (cons? ty) (car ty) ty))
(define type-pat "[A-Za-z]+")
;; - infers type of e
;; - checks that type of e matches the specified type
;; - erases types in e
@ -165,14 +168,34 @@
#:with τ? (mk-? #'tycon)
#:with τ-get (format-id #'tycon "~a-get" #'tycon)
#:with τ-expander (format-id #'tycon "~~~a" #'tycon)
#'(syntax-parse (infer+erase #'e) #:context #'e
#'(syntax-parse
;; when type error, prefer outer err msg
(with-handlers ([exn:fail?
(λ (ex)
(define matched-ty
(regexp-match
(pregexp
(string-append "got\\:\\s(" type-pat ")"))
(exn-message ex)))
(unless matched-ty
(raise ex (current-continuation-marks)))
(define t-in-msg
(datum->syntax #'here
(string->symbol
(cadr matched-ty))))
(list #'e t-in-msg))])
(infer+erase #'e))
#:context #'e
[(e- τ_e_)
#:with τ_e ((current-promote) #'τ_e_)
#:fail-unless (τ? #'τ_e)
(format
"~a (~a:~a): Expected expression ~s to have ~a type, got: ~a"
(syntax-source #'e) (syntax-line #'e) (syntax-column #'e)
(syntax->datum #'e) 'tycon (type->str #'τ_e))
(syntax-parse #'e-
['x (syntax-e #'x)]
[_ (syntax->datum #'e-)])
'tycon (type->str #'τ_e))
#;(if (stx-pair? #'τ_e)
(syntax-parse #'τ_e
[(τ-expander . args) #'(e- args)])
@ -193,8 +216,11 @@
(λ (e t)
(or (τ? t)
(type-error #:src e
#:msg "Expected expression ~s to have ~a type, got: ~a"
e (quote-syntax tycon) t)))
#:msg
(string-append
(format "Expected expression ~s" (syntax->datum e))
" to have ~a type, got: ~a")
(quote-syntax tycon) t)))
#'es
#'(τ_e (... ...)))
;#:with args (τ-get #'τ_e)
@ -430,7 +456,10 @@
(~seq #:bvs (~and (~parse has-bvs? #'#t) bvs-op) bvs-n:exact-nonnegative-integer)
#:defaults ([bvs-op #'=][bvs-n #'0]))
(~optional (~seq #:arr (~and (~parse has-annotations? #'#t) tycon))
#:defaults ([tycon #'void])))
#:defaults ([tycon #'void]))
(~optional (~seq #:other-prop other-key other-bvs other-val)
#:defaults ([other-key #'#f]))
)
#:with #%kind (format-id #'kind "#%~a" #'kind)
#:with τ-internal (generate-temporary #'τ)
#:with τ? (mk-? #'τ)
@ -509,7 +538,11 @@
#:with k_result (if #,(attribute has-annotations?)
#'(tycon k_arg (... ...))
#'#%kind)
(assign-type #'(τ-internal (λ bvs- void . τs-)) #'k_result)]
#:with result
(assign-type (syntax/loc stx (τ-internal (λ bvs- void . τs-))) #'k_result)
#,(if (syntax-e #'other-key)
#`(syntax-property #'result 'other-key (substs #'args #,#'other-bvs #,#'other-val))
#'#'result)]
;; else fail with err msg
[_
(type-error #:src stx
@ -612,6 +645,12 @@
; substitution
(begin-for-syntax
(define-syntax ~Any ; matches any tycon
(pattern-expander
(syntax-parser
[(_ x ...)
#'((~literal #%plain-app) _
((~literal #%plain-lambda) bvs (~literal void) x ...))])))
(define (merge-type-tags stx)
(define t (syntax-property stx 'type))
(or (and (pair? t)