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

Fix inference of two recursive types.

Browse Source 
Closes PR14608.
This commit is contained in:
Eric Dobson 2014-06-27 22:52:12 -07:00
parent cfe35fa0a4
commit e9899a07a6
2 changed files with 15 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/infer/infer-unit.rkt
View File

@ -571,16 +571,10 @@
[((Set: t) (Sequence: (list t*))) [((Set: t) (Sequence: (list t*)))
(cg t t*)] (cg t t*)]
;; if we have two mu's, we rename them to have the same variable ;; Mu's just get unfolded
;; and then compare the bodies ;; We unfold S first so that unions are handled in S before T
;; This relies on (B 0) only unifying with itself,
;; and thus only hitting the first case of this `match'
[((Mu-unsafe: s) (Mu-unsafe: t))
(cg s t)]
;; other mu's just get unfolded
[(s (? Mu? t)) (cg s (unfold t))]
[((? Mu? s) t) (cg (unfold s) t)] [((? Mu? s) t) (cg (unfold s) t)]
[(s (? Mu? t)) (cg s (unfold t))]
;; resolve applications ;; resolve applications
[((App: _ _ _) _) [((App: _ _ _) _)

12
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/infer-tests.rkt
View File

@ -245,6 +245,18 @@
(-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b)) (-pair (->... (list) ((-v b) b) Univ) (make-ListDots (-v b) 'b))
#:indices '(b) #:fail] #:indices '(b) #:fail]
[infer-t
(-lst (-mu A (Un (-v b) (-lst A))))
(-mu C (Un (-v b2) (-lst C)))
#:vars '(b2)
#:result [(-vec (-v b2)) (-vec (-lst (-mu A (Un (-v b) (-lst A)))))]]
[infer-t
(-mlst (-val 'b))
(-mlst (-v a))
#:vars '(a)
#:result [(-seq (-v a)) (-seq (-val 'b))]]
;; Currently Broken ;; Currently Broken
;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b)) ;(infer-t (make-ListDots -Symbol 'b) (-pair -Symbol (-lst -Symbol)) #:indices '(b))
[i2-t (-v a) N ('a N)] [i2-t (-v a) N ('a N)]