Opened 8 years ago

Closed 7 years ago

#1039 closed defect (fixed)

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

Reported by: sjamaan Owned by:
Priority: major Milestone: 4.9.0
Component: scrutinizer Version: 4.8.x
Keywords: Cc:
Estimated difficulty:


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

(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))))

Change History (4)

comment:1 Changed 8 years ago by sjamaan

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.

comment:2 Changed 7 years ago by sjamaan

See also #1063 which is probably related

comment:3 Changed 7 years ago by evhan

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.

comment:4 Changed 7 years ago by sjamaan

Resolution: fixed
Status: newclosed

Fixed by 504ec7a

Note: See TracTickets for help on using tickets.