Path manipulation now works with SomeSystemPath correctly.

collects/tests/typed-scheme/succeed/paths.rkt

@@ -0,0 +1,58 @@
+#lang typed/racket
+
+(: foo-path Path)
+(define foo-path (build-path "foo" "bar" 'same 'up))
+
+;Check predicates are always true
+(+ (if (path? foo-path) 2 'two)
+   (if (path-for-some-system? foo-path) 3 'three))
+
+(: current-system (U 'unix 'windows))
+(define current-system (system-path-convention-type))
+
+(: other-system (U 'unix 'windows))
+(define other-system
+ (case (system-path-convention-type)
+  ((unix) 'windows)
+  ((windows) 'unix)))
+
+(: other-foo-path SomeSystemPath)
+(define other-foo-path
+ (build-path/convention-type other-system
+  (string->some-system-path "foo" other-system) 
+  (string->some-system-path "bar" other-system) 
+  'same 
+  'up))
+
+
+(path->string foo-path)
+(some-system-path->string other-foo-path)
+(path->bytes foo-path)
+(path->bytes other-foo-path)
+
+(bytes->path #"foo" other-system)
+(string->path "foo")
+
+(bytes->path-element #"foo" other-system)
+(string->path-element "foo")
+
+
+(cleanse-path foo-path)
+(cleanse-path other-foo-path)
+
+(expand-user-path foo-path)
+
+(absolute-path? other-foo-path)
+(relative-path? other-foo-path)
+(complete-path? other-foo-path)
+
+
+
+
+(split-path foo-path)
+(split-path other-foo-path)
+
+
+;Original Soundness bug
+(when (path? other-foo-path) (error 'path "This shouldn't be raised"))
+

collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt

@@ -868,6 +868,25 @@
         [tc-e (in-hash #hash((1 . 2))) (-seq -Integer -Integer)]
         [tc-e (in-hash-keys #hash((1 . 2))) (-seq -Integer)]
         [tc-e (in-hash-values #hash((1 . 2))) (-seq -Integer)]
+
+        ;;Path tests
+        (tc-e (bytes->path #"foo" 'unix) -SomeSystemPath)
+        (tc-e (bytes->path #"foo") -Path)
+        (tc-e (bytes->path-element #"foo") -Path)
+        (tc-e (bytes->path-element #"foo" 'windows) -SomeSystemPath)
+
+        (tc-e (cleanse-path "foo") -Path)
+        (tc-e (cleanse-path (string->some-system-path "foo" 'unix)) -SomeSystemPath)
+        (tc-e (simplify-path "foo") -Path)
+        (tc-e (simplify-path "foo" #t) -Path)
+        (tc-e (simplify-path (string->some-system-path "foo" 'unix) #f) -SomeSystemPath)
+        (tc-e (path->directory-path "foo") -Path)
+        (tc-e (path->directory-path (string->some-system-path "foo" 'unix)) -SomeSystemPath)
+
+
+        
+
+
         )
   (test-suite
    "check-type tests"

collects/typed-scheme/base-env/base-env.rkt

@@ -391,10 +391,8 @@
 
 [string-copy (-> -String -String)]
 [string->immutable-string (-> -String -String)]
-[string->path (-> -String -Path)]
 
 
-[build-path ((list -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -Path)]
 [with-input-from-file
  (-poly (a) (->key -Pathlike (-> a) #:mode (one-of/c 'binary 'text) #f a))]
 [with-output-to-file
@@ -532,7 +530,6 @@
 [seconds->date (-Integer . -> . (make-Name #'date))]
 [current-seconds (-> -Integer)]
 [current-print (-Param (Univ . -> . Univ) (Univ . -> . Univ))]
-[path->string (-> -Path -String)]
 
 [link-exists? (-> -Pathlike B)]
 [directory-exists? (-> -Pathlike B)]
@@ -550,6 +547,88 @@
 [file-size (-> -Pathlike -Nat)]
 
 
+;; path manipulation
+
+[path? (make-pred-ty -Path)]
+[path-string? (-> Univ B)]
+[path-for-some-system? (make-pred-ty -SomeSystemPath)]
+
+[string->path (-> -String -Path)]
+[bytes->path (cl->* (-> -Bytes -Path) (-> -Bytes -PathConventionType -SomeSystemPath))]
+[path->string (-> -Path -String)]
+[path->bytes (-> -SomeSystemPath -Bytes)]
+
+[string->path-element (-> -String -Path)]
+[bytes->path-element (cl->* (-> -Bytes -Path) (-> -Bytes -PathConventionType -SomeSystemPath))]
+[path-element->string (-> -Path -String)]
+[path-element->bytes (-> -SomeSystemPath -Bytes)]
+
+[path-convention-type (-> -SomeSystemPath -PathConventionType)]
+[system-path-convention-type (-> -PathConventionType)]
+
+
+
+[build-path (cl->*
+  ((list -Pathlike*) -Pathlike* . ->* . -Path)
+  ((list -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -SomeSystemPath))]
+[build-path/convention-type 
+  ((list -PathConventionType -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -SomeSystemPath)]
+
+[absolute-path? (-> -SomeSystemPath B)]
+[relative-path? (-> -SomeSystemPath B)]
+[complete-path? (-> -SomeSystemPath B)]
+
+[path->complete-path
+ (cl->* (-> -Pathlike -Path)
+        (-> -Pathlike -Pathlike -Path)
+        (-> -SomeSystemPathlike -SomeSystemPathlike -SomeSystemPath))]
+
+[path->directory-path 
+ (cl->* (-> -Pathlike -Path)
+        (-> -SomeSystemPathlike -SomeSystemPath))]
+
+[resolve-path (-> -Path -Path)]
+[cleanse-path 
+ (cl->* (-> -Pathlike -Path)
+        (-> -SomeSystemPathlike -SomeSystemPath))]
+[expand-user-path (-> -Path -Path)]
+
+[simplify-path
+ (cl->* 
+  (-Pathlike . -> . -Path)
+  (-Pathlike B . -> . -Path)
+  (-SomeSystemPathlike B . -> . -SomeSystemPath))]
+
+[normal-case-path
+ (cl->* (-> -Pathlike -Path)
+        (-> -SomeSystemPathlike -SomeSystemPath))]
+
+[split-path
+ (cl->*
+  (-> -Pathlike
+      (-values (list
+                (Un -Path (-val 'relative) (-val #f))
+                (Un -Path (-val 'up) (-val 'same))
+                B)))
+  (-> -SomeSystemPathlike
+      (-values (list
+                (Un -SomeSystemPath (-val 'relative) (-val #f))
+                (Un -SomeSystemPath (-val 'up) (-val 'same))
+                B))))]
+
+[path-replace-suffix 
+ (cl->*
+  (-> -Pathlike (Un -String -Bytes) -Path)
+  (-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))]
+
+[path-add-suffix 
+ (cl->*
+  (-> -Pathlike (Un -String -Bytes) -Path)
+  (-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))]
+
+
+
+
 [hash? (make-pred-ty (make-HashtableTop))]
 [hash-eq? (-> (make-HashtableTop) B)]
 [hash-eqv? (-> (make-HashtableTop) B)]
@@ -749,8 +828,6 @@
 
 [object-name (Univ . -> . Univ)]
 
-[path? (make-pred-ty -Path)]
-[path-for-some-system? (make-pred-ty -SomeSystemPath)]
 
 ;; scheme/function
 [const (-poly (a) (-> a (->* '() Univ a)))]
@@ -855,11 +932,6 @@
 [string->some-system-path 
  (-String (Un (-val 'unix) (-val 'windows)) . -> . -SomeSystemPath)]
 
-[simplify-path (-SomeSystemPathlike [B] . ->opt . -SomeSystemPath)]
-[path->complete-path
- (cl->* (-> -Pathlike -Path)
-        (-> -SomeSystemPathlike -SomeSystemPathlike -SomeSystemPath))]
-[system-path-convention-type (-> (Un (-val 'unix) (-val 'windows)))]
 
 
 ;; scheme/file

collects/typed-scheme/types/abbrev.rkt

@@ -166,8 +166,10 @@
 (define -SomeSystemPath (*Un -Path -OtherSystemPath))
 (define -Pathlike (*Un -String -Path))
 (define -SomeSystemPathlike (*Un -String -SomeSystemPath))
-;(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
+(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same)))
 (define -SomeSystemPathlike* (*Un -String -SomeSystemPath(-val 'up) (-val 'same)))
+(define -PathConventionType (*Un (-val 'unix) (-val 'windows)))
+
 (define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String))
 
 (define -top (make-Top))