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

Hopefully not unsound fix for the (Cons (λ ([x : Y]) x) Nil) bug.

Browse Source
This commit is contained in:
Georges Dupéron 2017-09-29 17:15:10 +02:00
parent 6247b62d24
commit 9d812c08b7
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
macrotypes/examples/mlish.rkt
View File

@ -945,7 +945,7 @@
#:with τ_out* (syntax-parse #'τ_out
[(~?∀ (X ...) (~?∀ (Y ...) τ_out))
(for ([X (in-list (syntax->list #'(X ...)))]
#:when (stx-contains-id? #'Xs* X))
#:when (stx-contains-id? #'Xs X)) ;; To cause an error, the X must be part of the original signature (I think?)
(unless (covariant-X? X #'τ_out)
(raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn)))
#'(?∀ (X ... Y ...) τ_out)])

4
macrotypes/examples/tests/mlish-tests.rkt
View File

@ -389,8 +389,8 @@
: (→ (→/test X X) (List (→/test X X)) (List (→/test X X))))
(check-type map : (→/test (→ X Y) (List X) (List Y)))
#;(check-type (Cons (λ ([x : X]) x) Nil)
: (List (→/test {X} X X)))
(check-type (Cons (λ ([x : X]) x) Nil)
: (List (→/test {X} X X)))
(define (nn [x : X] -> (→ (× X (→ Y Y))))
(λ () (tup x (λ ([x : Y]) x))))