[racket-dev] Five feature/limitation interactions conspire to drive mad

On Jan 2, 2013, at 4:51 PM, Vincent St-Amour wrote:

>> 
>> It would be really handy if TR could give counterexamples in these 
>> cases. "This is how you can end up with an exact zero by multiplying an 
>> exact rational and a flonum: (* 0 1.0)."
> 
> Since most TR optimization failures can be traced back to a failure to
> typecheck at an optimizable type, Optimization Coach should be able to
> help you here. It doesn't currently provide counter-examples, but I'll
> look into it.
> 
> However, OC requires a program that typechecks, so it doesn't always
> apply. Perhaps applying optimization coaching techniques (especially
> proximity) to type error messages would work. Worth a try.


Absolutely worth a try. I doubt anyone else has done type checking with counter-example generation. -- Matthias