Originally submitted on: Thu Jan 22 17:40:01 -0500 2015 <div class="highlight hi

occurrence typing fails in strange ways for when/unless about typed-racket HOT 2 CLOSED

mfelleisen commented on June 18, 2024

occurrence typing fails in strange ways for when/unless

from typed-racket.

Comments (2)

takikawa commented on June 18, 2024

On Thu, 22 Jan 2015 18:02:32 -0500, asumu at ccs dot neu dot edu wrote:

On 2015-01-22 17:40:02 -0500, [email protected] wrote:

*** Description:
(unless l
(error 'f ""))
(define &^%$ l) ;; comment this line out and it type-checks
l)

I don't have a fix for this, but I do have an explanation for why it
doesn't work.

Without the extra definition, the expansion looks something like this:

  (define-values:4
   (f)
   (lambda:7
    (l)
    (if:8 l (#%app:8 void:8) (let-values:8 () (#%app:9 error 'f (quote ""))))
    l))

which TR can deal with fine because the if expression and l come right
after each other in the function body.

With the extra definition, the expansion looks different:

  (define-values:4
   (f)
   (lambda:7
    (l)
    (letrec-values
     ((()
       (begin:13
        (if:8
         l
         (#%app:8 void:8)
         (let-values:8 () (#%app:14 error 'f (quote ""))))
        (#%app:13 values:13)))
      ((&^%$) l))
     l)))

In this case, the if expression got stuck in a letrec-values RHS.
The problem is that TR currently does not propagate the refinements from
the RHS to the point where the body is typechecked.

Cheers,
Asumu

from typed-racket.

mfelleisen commented on June 18, 2024

On Thu, 22 Jan 2015 18:15:12 -0500, matthias at ccs dot neu dot edu wrote:

The workaround is this:

#lang typed/racket

(: f (-> (U False [Listof String]) [Listof String]))
(define (f l)
  (unless l
    (error 'f ""))
  (g l))
(: g (-> [Listof String] [Listof String]))
(define (g l)
  (define &^%$ l) 
  l)

On Jan 22, 2015, at 6:02 PM, Asumu Takikawa [email protected] wrote:

>> *** Description:
>>  (unless l
>>    (error 'f ""))
>>  (define &^%$ l) ;; comment this line out and it type-checks 
>>  l)
>  (define-values:4
>   (f)
>   (lambda:7
>    (l)
>    (if:8 l (#%app:8 void:8) (let-values:8 () (#%app:9 error 'f (quote ""))))
>    l))
>  (define-values:4
>   (f)
>   (lambda:7
>    (l)
>    (letrec-values
>     ((()
>       (begin:13
>        (if:8
>         l
>         (#%app:8 void:8)
>         (let-values:8 () (#%app:14 error 'f (quote ""))))
>        (#%app:13 values:13)))
>      ((&^%$) l))
>     l)))