[racket] typed racket: ordering of cond clauses?
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.