[racket] typed scheme require question
I'm using Racket 5.0. I'm a little confused by the following.
I'm using typed/racket/base, and tried writing list-length using
'rest'. rest isn't bound, so I did a typed/require to introduce the
'rest' binding.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#lang typed/racket/base
(require/typed racket/list
[rest (All (A) ((Listof A) -> (Listof A)))])
(: list-length (All (A) ((Listof A) -> Integer)))
(define (list-length l)
(cond
[(null? l)
0]
[else
(add1 (list-length (rest l)))]))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
This worked as expected. I then wanted to see how the system responds
if I try using the untyped version; I wanted to see the kind of error
message I'd get back. To my surprise, I didn't see any error when I
did the following:
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#lang typed/racket/base
(require racket/list)
(: list-length (All (A) ((Listof A) -> Integer)))
(define (list-length l)
(cond
[(null? l)
0]
[else
(add1 (list-length (rest l)))]))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
I'm guessing that the type-checker has some hardcoded notion of the
types for racket/list functions. Is this true?