From 9d812c08b7c9b92e5c9af1036d088244586c7d4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Georges=20Dup=C3=A9ron?= Date: Fri, 29 Sep 2017 17:15:10 +0200 Subject: [PATCH] =?UTF-8?q?Hopefully=20not=20unsound=20fix=20for=20the=20(?= =?UTF-8?q?Cons=20(=CE=BB=20([x=20:=20Y])=20x)=20Nil)=20bug.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- macrotypes/examples/mlish.rkt | 2 +- macrotypes/examples/tests/mlish-tests.rkt | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt index 94ec627..3adea15 100644 --- a/macrotypes/examples/mlish.rkt +++ b/macrotypes/examples/mlish.rkt @@ -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)]) diff --git a/macrotypes/examples/tests/mlish-tests.rkt b/macrotypes/examples/tests/mlish-tests.rkt index 24d143c..52647b2 100644 --- a/macrotypes/examples/tests/mlish-tests.rkt +++ b/macrotypes/examples/tests/mlish-tests.rkt @@ -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))))