occurrence typing fails on Listof vs List

[mfelleisen]

Originally submitted on: Thu Jan 22 14:20:01 -0500 2015

Occurrence typing fails on the [Listof (U A B)] vs [List (U A B)]. See program below.

Logically this makes no sense because if cadr and friends succeed, the type can be split.

Steps to Reproduce:

#lang typed/racket

(define-type Line String)

(: line-specification? (-> String (U False [Listof Line])))
(define (line-specification? line)
  (: r (U False [Pairof String [Listof (U False String)]]))
  (define r '("a" "b") #;(regexp-match #px"--* (.*)" line))
  (cond
    [(and r) (if (cadr r) (string-split (cadr r)) #f)]
    [else '()]))

Release:

6.1.1.8--2015-01-03(-/f)

Environment:

macosx "Darwin antarctica.ccs.neu.edu 12.5.0 Darwin Kernel Version 12.5.0: Sun Sep 29
 13:33:47 PDT 2013; root:xnu-2050.48.12~1/RELEASE_X86_64 x86_64" (x86_64-macosx/3m)
 (get-display-depth) = 32
Human Language: english
(current-memory-use) 913381128
raco pkg (show):
Installation-wide:
 Package                 Checksum     Source
 ansi                    2770248a...  catalog ansi
 github://github.com/tonyg/racket-ansi/master
 benchmark               45992763...  catalog benchmark
 git://github.com/stamourv/racket-benchmark#master
 graph                   9528fd5f...  catalog graph
 github://github.com/stchang/graph/master
 honu                    6a982c11...  catalog honu git://github.com/racket/honu
 htdp                    76ca9ca3...  clone /Users/matthias/plt/extra-pkgs/htdp/htdp
 git://github.com/racket/htdp/?path=htdp
 main-distribution       67868e03...  catalog main-distribution
 git://github.com/racket/main-distribution
 main-distribution-test  ca4a870e...  catalog main-distribution-test
 git://github.com/racket/main-distribution-test
 marketplace             e48aabc2...  catalog marketplace
 github://github.com/tonyg/marketplace/typeless
 racket-lib                           static-link /Users/matthias/plt/pkgs/racket-lib
 rackunit                466a679c...  clone
 /Users/matthias/plt/extra-pkgs/rackunit/rackunit
 git://github.com/racket/rackunit/?path=rackunit
 [217 auto-installed packages not shown]
User-specific for installation "development":
 [none]

Collections:
("/Users/matthias/0Unison/collects/"
 (".DS_Store" "compiled" "date" "finance" "info-domain" "info.ss" "pdf.ss~" "session"
 "short" "testing" "tll-collects" "utils" "web"))
("/Users/matthias/Library/Racket/development/collects"
 (non-existent-path))
("/Users/matthias/plt/racket/collects"
 (".gitignore" "acks" "compiler" "data" "db" "dynext" "ffi" "file" "info" "info-domain"
 "json" "launcher" "net" "openssl" "pkg" "planet" "racket" "raco" "reader" "realm" "s-exp"
 "setup" "syntax" "unstable" "version" "xml"))

Recent Internal Errors: 
Computer Language: (("Determine language from source") (#(#t print mixed-fraction-e #f #t
 debug) (default) #() "#lang racket" #t #t ((test) (main)) #t))

This bug was converted from Gnats bug 14947.

[endobson]

I started taking a look at this yesterday, and part of the problem is what the actual type of cadr is in TR versus what you could reasonably expect. TR is currently taking the approach that type for cadr and friends only have logical information if there is no possibility of failure at runtime (i.e the pair structure is correct), but that it is also fine to apply it to a (Listof a). In your example r is not necessarily of the right structure because the inner (Listof (U String False)) could be null. Thus there is no logical information for the if to enhance the environment on. I believe this is easily fixable in some cases (which would cover this case).

The tricky cases are cadr applied to a value of the type (Pair A (Listof B)), which would currently return (U A B). So the question in these cases is what are the exact runtime failures that we allow to be not ruled out by the type? My thought is that it should be that if the runtime value that we need to be a cons-cell is null, then it should be allowed by the type.

The second issue is that inference doesn't take the object environment into account. So if we have x : (Listof (U False String)) and we know that car @ x has type String, then we still cannot infer type variables for car such that it returns a String in the expression (car x), but ((inst car String Any) x will work because typechecking does use the object environment.

[takikawa]

I have an in-progress pull request that I think solves the first part (fixing the types for cadr etc) here: https://github.com/racket/typed-racket/pull/15

But it doesn't currently pass the tests due to a type inference limitation. Also my PR probably doesn't the second issue you point out.