commit 1167407cfe612737e9f43c6c01856ed5d0a826d9
parent a0f4d9e3a9fb9719f6382f5b57c8c00586ec77ce
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 5 Apr 2016 10:55:02 -0400
fix type constructor arity err causing inf loop
- lambda now supports (implicit) polymorphic type annotations
- (unrelated to this commit) many tests seem to be failing due to a
slight change in err msg
Diffstat:
3 files changed, 44 insertions(+), 6 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -222,9 +222,9 @@
#:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
#'(StructName ...) #'((fld ...) ...))
#:with (Cons? ...) (stx-map mk-? #'(StructName ...))
-; #:with get-Name-info (format-id #'Name "get-~a-info" #'Name)
;; types, but using RecName instead of Name
#:with ((τ/rec ...) ...) (subst #'RecName #'Name #'((τ ...) ...))
+ #:with (Y ...) (generate-temporaries #'(X ...))
#`(begin
(define-type-constructor Name
#:arity = #,(stx-length #'(X ...))
@@ -233,15 +233,21 @@
(let-syntax
([RecName
(syntax-parser
- [(_ . rst)
+ [(_ Y ...)
;; - this is a placeholder to break the recursion
;; - clients, like match, must manually unfold by
;; replacing the entire (#%plain-app RecName ...) stx
;; - to preserve polymorphic recursion, the entire stx
- ;; should be replaced but with #'rst as the args
+ ;; should be replaced but with X ... as the args
;; in place of args in the input type
;; (see subst-special in typecheck.rkt)
- (assign-type #'(#%plain-app RecName . rst) #'#%type)])])
+ (assign-type #'(#%plain-app RecName Y ...) #'#%type)]
+ [(~and err (_ . rst))
+ (type-error #:src #'err
+ #:msg (format "type constructor ~a expects ~a args, given ~a: ~a"
+ (syntax->datum #'Name) (stx-length #'(X ...))
+ (stx-length #'rst) (string-join (stx-map type->str #'rst) ", ")))]
+ )])
('Cons 'StructName Cons? [acc τ/rec] ...) ...))
#:no-provide)
(struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
@@ -691,7 +697,14 @@
#:with (~∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx)
#`(Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))]
[(_ . rst)
- #'(Λ () (ext-stlc:λ . rst))])
+ (let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
+ (with-handlers ([exn:fail:syntax:unbound?
+ (λ (e)
+ (define X (stx-car (exn:fail:syntax-exprs e)))
+ ; X is tainted, so need to launder it
+ (define Y (datum->syntax #'rst (syntax->datum X)))
+ (L (cons Y Xs)))])
+ (local-expand #`(Λ #,Xs (ext-stlc:λ . rst)) 'expression null)))])
;; #%app --------------------------------------------------
diff --git a/tapl/tests/mlish/polyrecur.mlish b/tapl/tests/mlish/polyrecur.mlish
@@ -88,3 +88,28 @@
(check-type
(flatten (Node 1 (Node (tup 2 3) (Leaf (tup (tup 4 5) (tup 6 7))))))
: (List Int) -> (list 1 6 7 4 5 2 3))
+
+
+;; catch type constructor arity error; should not loop
+(define-type (BankersDeque A)
+ [BD Int (List A) Int (List A)])
+
+(define-type (ImplicitCatDeque A)
+ [Shall (BankersDeque A)]
+ [Dp (BankersDeque A)
+ (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A)))
+ (BankersDeque A)
+ (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A)))
+ (BankersDeque A)])
+
+(define-type (CmpdElem A)
+ [Simple (BankersDeque A)]
+ [Cmpd (BankersDeque A)
+ (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A))))
+ (BankersDeque A)])
+
+
+(typecheck-fail
+ (λ ([icd : (ImplicitCatDeque A)]) icd)
+ #:with-msg
+ "type constructor ImplicitCatDeque expects 1 args, given 2")
diff --git a/tapl/typecheck.rkt b/tapl/typecheck.rkt
@@ -712,7 +712,7 @@
(merge-type-tags (syntax-track-origin τ #'y #'y))]
[(esub ...)
#:with (esub_subst ...) (stx-map (λ (e1) (subst τ x e1 cmp)) #'(esub ...))
- (syntax-track-origin #'(esub_subst ...) e x)]
+ (syntax-track-origin (syntax/loc e (esub_subst ...)) e x)]
[_ e]))
(define (substs τs xs e [cmp bound-identifier=?])
