$Id: tc-bugs.txt,v 1.23 2006/03/07 06:57:05 leavens Exp $ Author: Brian Dorn and Gary T. Leavens The following is our known bugs list for the rule based type checker. See tests/bugs for files that demonstrate known bugs. --------------------------------------------------------------------- The basic problem with the speed of the type checker for large programs (like the type checker itself) is that it type checks all modules that are required in a module. Instead, when a module requires another module, it should: - check that all provided identifiers have a deftype (assuming that the module is in the typedscm dialect) - use the deftypes for the provided identifiers This would be a big win in letting the type checker type check itself. --------------------------------------------------------------------- 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... -------------------------------------------------------------------- If we have a module that doesn't have a provided name, in Chez Scheme it dies.... ;; file tests/bugs/missing.scm (module missing (lib "typedscm.ss" "typedscm") (provide x) (deftype x number) ) typed> (require "tests/bugs/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: ;; file tests/bugs/missing2.scm (deftype fool number) (define foo 3) typed> (load "tests/bugs/missing2.scm") Type checking "tests/bugs/missing2.scm" ... ... done type checking "tests/bugs/missing2.scm" foo : number fool : number typed> fool Error: variable fool is not bound. Process scheme finished 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. -------------------------------------------------------------------- Figure out the test cases in scheme-annotate.tst that are commented out. Something isn't working with definitions at the start of bodies quite right. typed> (load "tests/bugs/local-definitions1.scm") Type checking "tests/bugs/local-definitions1.scm" ... ... done type checking "tests/bugs/local-definitions1.scm" tests/bugs/local-definitions1.scm: line 3: Type mismatch between inferred and expected types Syntax: (define even? (lambda (n) (if (zero? n) #t (odd? (- n 1))))) Expected: module Inferred: module Skipping evaluation because of the type errors... ------------------------------------------------------------------- Do expressions have been added to tc-scheme-annotate, but the tests don't work when the one part that is commented out isn't commented out... When they work, add code for do-stmts. -------------------------------------------------------------------- There is a problem checking "error-tests/bad-typedef-for-constructor.scm" typed> (load "tests/bugs/bad-typedef-for-constructor.scm") Type checking "tests/bugs/bad-typedef-for-constructor.scm" ... ERROR: tc:function-type-expr->arg-types: not a function-type-expr: (tc:basic-type-expr road-map) Process scheme finished -------------------------------------------------------------------- This code in tests/bugs/unification-bug.scm: (define (hash-rehasher pred) (let ((hashfun (predicate->hash pred))) (lambda (hashtab newk) (let ((newtab (make-hash-table newk))) (hash-for-each (lambda (key value) (let ((num (hashfun key newk))) (vector-set! newtab num (cons (cons key value) (vector-ref newtab num))))) hashtab) newtab)))) typed> (load "tests/bugs/unification-bug.scm") Type checking "tests/bugs/unification-bug.scm" ... ... done type checking "tests/bugs/unification-bug.scm" tests/bugs/unification-bug.scm: line 201: Operator and argument types don't match Offending call: (vector-set! newtab num (cons (cons key value) (vector-ref newtab num))) Operator type : (forall (t) (-> ((vector-of t) number t) void)) Argument type list: ((forall (s t) (vector-of (list-of (pair-of s t)))) number (list-of datum)) Skipping evaluation because of the type errors... The problem seems to be that a type such as (forall (s t2) (vector-of (list-of (pair-of s t2)))) doesn't unify with (vector-of t) even though t is arbitrary. Should that work, resulting in a binding from t to (forall (s t2) (list-of (pair-of s t2)))? (I'm not sure...) ------------------------------------------------------- It would be nice to have error messages for calls pinpoint which arguments are not matching, instead of relying on the reader to do that. For example, instead of foo.scm: line 9: Operator and argument types don't match Offending call: (binary-op-exp (foo left) plus-op (foo left)) Operator type : (-> (arith-expr infix-op arith-expr) arith-expr) Argument type list: ((forall (t) t) (-> () infix-op) (forall (t) t)) It would be better to have something like: foo.scm: line 9: Operator and argument types in call don't match Actual argument: plus-op Expected type : infix-op Actual arg type: (-> () infix-op) perhaps with some additional information about the surrounding call. -------------------------------- The test in tests/bugs/not-found-error.scm shows a case where the checker overgeneralizes the type. The error goes away if you don't declare one type, and hence the problem seems to be with top-down type checking.