[racket] typed racket: ordering of cond clauses?

From: Danny Yoo (dyoo at cs.wpi.edu)
Date: Tue Mar 1 16:10:16 EST 2011

I'm hitting a type error that I've tried to reduce in the following program.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#lang typed/racket/base
(require racket/list)

(define-type CompileTimeEnvironmentEntry (U False
                                            Symbol
                                            Prefix
                                            ))

(define-struct: Prefix ([names : (Listof Symbol)])  #:transparent)
(define-type CompileTimeEnvironment (Listof CompileTimeEnvironmentEntry))


(: find-variable (Symbol CompileTimeEnvironment -> Boolean))
(define (find-variable name cenv)
  (let: loop : Boolean ([cenv : CompileTimeEnvironment cenv]
                               [depth : Natural 0])
        (cond [(empty? cenv)
               (error 'find-variable "Unable to find ~s in the
environment" name)]
              [else
               (let: ([elt : CompileTimeEnvironmentEntry (first cenv)])
                 (cond

                   [(Prefix? elt)
                    (cond [(member name (Prefix-names elt))
                           #t]
                          [else
                           (loop (rest cenv) (add1 depth))])]

                   [(symbol? elt)
                    (cond
                      [(eq? name elt)
                       #t]
                      [else
                       (loop (rest cenv) (add1 depth))])]

                   ;; Why does this have to be the first or second
clause to typecheck?
                   [(eq? #f elt)
                    (loop (rest cenv) (add1 depth))]))])))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


Typed Racket reports that I haven't accounted for all cases in the
inner cond of find-variable, but this is weird because elt can only
either be a Prefix, a symbol, or false.  Furthermore, as the comment
in find-variable says, if I move the third clause that tests #f up so
it's the first to be tested, this makes Typed Racket happy.  I don't
understand why that should have that effect.


Posted on the users mailing list.