Summary

Scrutinizer's behaviour differs between (list-of x) and (list x)

Metadata

Description

Looks like this should give a scrutinizer warning, but it doesn't:

 #!scm
 (module whatever ()
   (import chicken scheme)
 
   ;; Change "list-of" to "list" and it's still correct, but we do get a warning
   (: foo (forall (a) (a -> (list-of a))))
   (define (foo x)
     (cons x '()))
 
   (display (car (car (foo 1))))
   (newline)
 )

Changes and comments

[2013-08-04 18:13:11 UTC] sjamaan wrote:

The problem appears to be that CAR is defined as FORALL a: (pair a *) -> a, and canonicalize-list-type is invoked on this to match it against the (list-of fixnum). The "any type of pair" cannot be canonicalized, which causes it to return an inexact match.

I'm not sure yet how to fix this, but it seems that somehow it ought to be able to match at least the a type against fixnum.

[2013-11-15 21:01:33 UTC] sjamaan wrote:

See also #1063 which is probably related

[2013-12-26 22:35:35 UTC] evhan wrote:

I agree, it seems to me that in the case of (pair x *) <-> (list-of x), matching should follow the pair form as far as possible.

The important difference between the list and list-of branches when scrutinizing this ticket's example is that list walks its pair form, which has the side effect of unifying x from the type environment, while list-of doesn't. But, even though (pair x *) can't be rewritten to (list x ...) or (list-of x), I think we can still match the x component in order to keep its type in play.

[2014-01-09 23:02:17 UTC] sjamaan changed status from new to closed

[2014-01-09 23:02:17 UTC] sjamaan set resolution to fixed

[2014-01-09 23:02:17 UTC] sjamaan wrote:

Fixed by 504ec7a