$Id: tc-bugs.txt,v 1.7 2005/05/17 05:20:33 leavens Exp $

Author:  Brian Dorn

The following is our known bugs list for the rule based type checker.

---------------------------------------------------------------------
Because the checker is so slow it's quite painful that it only gives
one error at a time.  When I'm trying to get the interpreters to type
check, it takes more time than it takes to type out this report to
type check, and then I just find *one* type error...

---------------------------------------------------------------------
Recursively defined defreps don't appear to get downed correctly
  Example:  tc-tree.scm
  Expected:  This should typecheck correctly

  Thoughts:  There also appears to be strange output on the call to cdr
    on this one (extra parens).

---------------------------------------------------------------------

Try a module with the wrong name (that doesn't correspond to the file
it's in).  Works in DrScheme (without an error report), but dies in
Chez Scheme.  

;; in file foo.scm
(module bar (lib "typedscm.ss" "lib342")
   (provide x)
   (define x 3)
)

   Expected:  It probably should give an error report in both cases.
   Thoughts:  Add to the parser?

--------------------------------------------------------------------

If we have a module that doesn't have a provided name,
in Chez Scheme it dies....

;; file missing.scm
(module missing (lib "typedscm.ss" "lib342")
   (provide x)
   (deftype x number)
)

typed> (require "missing.scm")
x : number

Error: missing definition for export(s) (x).

Process scheme finished

  Expected:  This should give a type error...
  Thoughts:  Add a side condition for this in module rule.

--------------------------------------------------------------------

It would be nice if the checker warned about names that are given
deftypes that are not defined; these may be spelling mistakes:

(deftype fool number)
(define foo 3)

Currently this passes.

In general any other checks for consistency between declared names and
definitions might be useful, such as the opposite of the above check
and checks for double deftypes for the same name.
--------------------------------------------------------------------

I don't see why there is an extra set of parentheses around the syntax
below:

3-5-reducer.scm: lines 225 to 229: Type mismatch between inferred and
expected types
   Syntax: ((letrec ((loop (lambda (reg-list) (and (not (null?
   reg-list)) (or (pred (car reg-list)) (loop (cdr reg-list)))))))
   (loop *env-registry*)))
   Expected: (forall (t) (-> (t) boolean))
   Inferred: boolean
Skipping evaluation because of the type errors...

I think better would be:

3-5-reducer.scm: lines 225 to 229: Type mismatch between inferred and
expected types
   Syntax: (letrec ((loop (lambda (reg-list) (and (not (null?
   reg-list)) (or (pred (car reg-list)) (loop (cdr reg-list)))))))
   (loop *env-registry*))
   Expected: (forall (t) (-> (t) boolean))
   Inferred: boolean
Skipping evaluation because of the type errors...

--------------------------------------------------------------------

Figure out the test cases in scheme-annotate.tst that are commented out.
Something isn't working wiht definitions at the start of bodies quite right...